%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ANA075^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 : n001.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:01 AM UTC 2026
% Result : Theorem 7.14s 1.32s
% Output : Refutation 7.14s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ANA075^1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.20 % Computer : n001.cluster.edu
% 0.10/0.20 % Model : x86_64 x86_64
% 0.10/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.20 % Memory : 8046.5625MB
% 0.10/0.20 % OS : Linux 6.8.0-71-generic
% 0.10/0.20 % CPULimit : 300
% 0.10/0.20 % WCLimit : 300
% 0.10/0.20 % DateTime : Tue Sep 29 17:45:06 UTC 2026
% 0.10/0.20 % CPUTime :
% 0.10/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.23 Running first-order model finding
% 0.10/0.23 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.47/1.01 % (1584112)Will run a generic schedule for satisfiability detection.
% 4.47/1.01 % (1584118)% WARNING: option uhcvi not known.
% 4.47/1.01 % (1584119)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=381356676:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.47/1.01 % (1584117)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1725658638_2999 on theBenchmark for (2999ds/0Mi)
% 4.47/1.01 % (1584121)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2490968865:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.47/1.01 % (1584118)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2997135712:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.47/1.01 % (1584123)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2899713411:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.47/1.01 % (1584120)dis+10_1_sil=32000:sp=arity:random_seed=4177489247:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.47/1.01 % (1584118)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.47/1.01 % (1584121)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.47/1.01 % (1584118)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 4.47/1.01 % Exception at run slice level
% 4.47/1.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.47/1.01 % (1584122)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1062875995:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.47/1.01 % (1584130)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=543604874:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 4.47/1.01 % Exception at run slice level
% 4.47/1.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.47/1.01 % (1584133)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1389145618:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 4.47/1.01 % (1584120)Instruction limit reached!
% 4.47/1.01 % (1584120)------------------------------
% 4.47/1.01 % (1584120)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.47/1.01 % (1584120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.47/1.01 % (1584120)CaDiCaL version: 2.1.3
% 4.47/1.01 % (1584120)Termination reason: Instruction limit
% 4.47/1.01 % (1584120)Termination phase: Saturation
% 4.47/1.01 % (1584120)Time elapsed: 0.067 s
% 4.47/1.01 % (1584120)Peak memory usage: 13 MB
% 4.47/1.01 % (1584120)Instructions burned: 104 (million)
% 4.47/1.01 % (1584123)Instruction limit reached!
% 4.47/1.01 % (1584123)------------------------------
% 4.47/1.01 % (1584123)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.47/1.01 % (1584123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.47/1.01 % (1584123)CaDiCaL version: 2.1.3
% 4.47/1.01 % (1584123)Termination reason: Instruction limit
% 4.47/1.01 % (1584123)Termination phase: Saturation
% 4.47/1.01 % (1584123)Time elapsed: 0.087 s
% 4.47/1.01 % (1584123)Peak memory usage: 14 MB
% 4.47/1.01 % (1584123)Instructions burned: 160 (million)
% 4.47/1.01 % (1584135)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=953406757:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 4.47/1.01 % (1584135)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.47/1.01 % (1584135)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 4.47/1.01 % (1584121)Instruction limit reached!
% 4.47/1.01 % (1584121)------------------------------
% 4.47/1.01 % (1584121)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.47/1.01 % (1584121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.47/1.01 % (1584121)CaDiCaL version: 2.1.3
% 4.47/1.01 % (1584121)Termination reason: Instruction limit
% 4.47/1.01 % (1584121)Termination phase: Saturation
% 4.47/1.01 % (1584121)Time elapsed: 0.092 s
% 4.47/1.01 % (1584121)Peak memory usage: 13 MB
% 4.47/1.01 % (1584121)Instructions burned: 116 (million)
% 4.47/1.01 % (1584122)Instruction limit reached!
% 4.47/1.01 % (1584122)------------------------------
% 4.47/1.01 % (1584122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.14/1.32 % (1584122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.14/1.32 % (1584122)CaDiCaL version: 2.1.3
% 7.14/1.32 % (1584122)Termination reason: Instruction limit
% 7.14/1.32 % (1584122)Termination phase: Saturation
% 7.14/1.32 % (1584122)Time elapsed: 0.101 s
% 7.14/1.32 % (1584122)Peak memory usage: 12 MB
% 7.14/1.32 % (1584122)Instructions burned: 131 (million)
% 7.14/1.32 % (1584137)ott-21_1_sil=16000:fs=off:random_seed=290237300:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 7.14/1.32 % (1584138)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2766064782:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 7.14/1.32 % (1584133)Instruction limit reached!
% 7.14/1.32 % (1584133)------------------------------
% 7.14/1.32 % (1584133)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.14/1.32 % (1584133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.14/1.32 % (1584133)CaDiCaL version: 2.1.3
% 7.14/1.32 % (1584133)Termination reason: Instruction limit
% 7.14/1.32 % (1584133)Termination phase: Saturation
% 7.14/1.32 % (1584133)Time elapsed: 0.075 s
% 7.14/1.32 % (1584133)Peak memory usage: 12 MB
% 7.14/1.32 % (1584133)Instructions burned: 133 (million)
% 7.14/1.32 % (1584139)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=297697968:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 7.14/1.32 % (1584142)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=900869368:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 7.14/1.32 % Exception at run slice level
% 7.14/1.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.14/1.32 % (1584145)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4253816271:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 7.14/1.32 % Exception at run slice level
% 7.14/1.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.14/1.32 % (1584137)Instruction limit reached!
% 7.14/1.32 % (1584137)------------------------------
% 7.14/1.32 % (1584137)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.14/1.32 % (1584137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.14/1.32 % (1584137)CaDiCaL version: 2.1.3
% 7.14/1.32 % (1584137)Termination reason: Instruction limit
% 7.14/1.32 % (1584137)Termination phase: Saturation
% 7.14/1.32 % (1584137)Time elapsed: 0.084 s
% 7.14/1.32 % (1584137)Peak memory usage: 12 MB
% 7.14/1.32 % (1584137)Instructions burned: 180 (million)
% 7.14/1.32 % (1584147)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=2689763555:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi)
% 7.14/1.32 % (1584147)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 7.14/1.32 % (1584149)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1037656428:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 7.14/1.32 % (1584149)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 7.14/1.32 % (1584135)Instruction limit reached!
% 7.14/1.32 % (1584135)------------------------------
% 7.14/1.32 % (1584135)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.14/1.32 % (1584135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.14/1.32 % (1584135)CaDiCaL version: 2.1.3
% 7.14/1.32 % (1584135)Termination reason: Instruction limit
% 7.14/1.32 % (1584135)Termination phase: Saturation
% 7.14/1.32 % (1584135)Time elapsed: 0.362 s
% 7.14/1.32 % (1584135)Peak memory usage: 15 MB
% 7.14/1.32 % (1584135)Instructions burned: 685 (million)
% 7.14/1.32 % (1584151)fmb+10_1_sil=64000:random_seed=841649967:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi)
% 7.14/1.32 % (1584151)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 7.14/1.32 % Exception at run slice level
% 7.14/1.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.14/1.32 % (1584153)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1321358772:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi)
% 7.14/1.32 % Exception at run slice level
% 7.14/1.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.14/1.32 % (1584155)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2810534845:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi)
% 7.14/1.32 % Exception at run slice level
% 7.14/1.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.14/1.32 % (1584157)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3361758323:i=5131_2994 on theBenchmark for (2994ds/5131Mi)
% 7.14/1.32 % (1584157)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 7.14/1.32 % (1584138)Instruction limit reached!
% 7.14/1.32 % (1584138)------------------------------
% 7.14/1.32 % (1584138)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.14/1.32 % (1584138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.14/1.32 % (1584138)CaDiCaL version: 2.1.3
% 7.14/1.32 % (1584138)Termination reason: Instruction limit
% 7.14/1.32 % (1584138)Termination phase: Saturation
% 7.14/1.32 % (1584138)Time elapsed: 0.439 s
% 7.14/1.32 % (1584138)Peak memory usage: 14 MB
% 7.14/1.32 % (1584138)Instructions burned: 478 (million)
% 7.14/1.32 % (1584159)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=610324737:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi)
% 7.14/1.32 % (1584159)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 7.14/1.32 % (1584159)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 7.14/1.32 % (1584149)Instruction limit reached!
% 7.14/1.32 % (1584149)------------------------------
% 7.14/1.32 % (1584149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.14/1.32 % (1584149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.14/1.32 % (1584149)CaDiCaL version: 2.1.3
% 7.14/1.32 % (1584149)Termination reason: Instruction limit
% 7.14/1.32 % (1584149)Termination phase: Saturation
% 7.14/1.32 % (1584149)Time elapsed: 0.385 s
% 7.14/1.32 % (1584149)Peak memory usage: 19 MB
% 7.14/1.32 % (1584149)Instructions burned: 879 (million)
% 7.14/1.32 % (1584161)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=766972069:i=6324_2993 on theBenchmark for (2993ds/6324Mi)
% 7.14/1.32 % Exception at run slice level
% 7.14/1.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.14/1.32 % (1584163)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2486836588:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi)
% 7.14/1.32 % Exception at run slice level
% 7.14/1.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.14/1.32 % (1584165)ott-2_1_sil=16000:newcnf=on:random_seed=4269833972:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi)
% 7.14/1.32 % (1584165)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 7.14/1.32 % (1584147)Instruction limit reached!
% 7.14/1.32 % (1584147)------------------------------
% 7.14/1.32 % (1584147)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.14/1.32 % (1584147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.14/1.32 % (1584147)CaDiCaL version: 2.1.3
% 7.14/1.32 % (1584147)Termination reason: Instruction limit
% 7.14/1.32 % (1584147)Termination phase: Saturation
% 7.14/1.32 % (1584147)Time elapsed: 0.503 s
% 7.14/1.32 % (1584147)Peak memory usage: 18 MB
% 7.14/1.32 % (1584147)Instructions burned: 692 (million)
% 7.14/1.32 % (1584142)Instruction limit reached!
% 7.14/1.32 % (1584142)------------------------------
% 7.14/1.32 % (1584142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.14/1.32 % (1584142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.14/1.32 % (1584142)CaDiCaL version: 2.1.3
% 7.14/1.32 % (1584142)Termination reason: Instruction limit
% 7.14/1.32 % (1584142)Termination phase: Saturation
% 7.14/1.32 % (1584142)Time elapsed: 0.564 s
% 7.14/1.32 % (1584142)Peak memory usage: 16 MB
% 7.14/1.32 % (1584142)Instructions burned: 1179 (million)
% 7.14/1.32 % (1584168)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3007593700:i=54282_2992 on theBenchmark for (2992ds/54282Mi)
% 7.14/1.32 % Exception at run slice level
% 7.14/1.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.14/1.32 % (1584167)ott+10_1_sil=32000:tgt=ground:random_seed=678989458:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi)
% 7.14/1.32 % (1584170)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2117985482:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi)
% 7.14/1.32 % (1584170)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 7.14/1.32 % (1584165) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1584112-1584165"...
% 7.14/1.32 % (1584165)...printing done.
% 7.14/1.32 % (1584165)Refutation found. Thanks to Tanya!
% 7.14/1.32 % SZS status Theorem for theBenchmark
% 7.14/1.32 % SZS output start Proof for theBenchmark
% 7.14/1.32 thf(type_def_5, type, 'type/realax/real': $tType).
% 7.14/1.32 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 7.14/1.32 thf(func_def_0, type, 'const/trivia/I': !>[X0: $tType]:((X0 > X0))).
% 7.14/1.32 thf(func_def_1, type, 'const/sets/sup': (('type/realax/real' > $o) > 'type/realax/real')).
% 7.14/1.32 thf(func_def_2, type, 'const/sets/SUBSET': !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > $o))).
% 7.14/1.32 thf(func_def_3, type, 'const/sets/IN': !>[X0: $tType]:((X0 > (X0 > $o) > $o))).
% 7.14/1.32 thf(func_def_4, type, 'const/sets/EMPTY': !>[X0: $tType]:((X0 > $o))).
% 7.14/1.32 thf(func_def_5, type, 'const/realax/real_le': ('type/realax/real' > 'type/realax/real' > $o)).
% 7.14/1.32 thf(func_def_9, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 7.14/1.32 thf(func_def_10, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 7.14/1.32 thf(func_def_11, type, db0: !>[X0: $tType]:(X0)).
% 7.14/1.32 thf(func_def_12, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 7.14/1.32 thf(func_def_13, type, vIMP: ($o > $o > $o)).
% 7.14/1.32 thf(func_def_14, type, sK0: ('type/realax/real' > ('type/realax/real' > $o) > 'type/realax/real')).
% 7.14/1.32 thf(func_def_15, type, sK1: ('type/realax/real' > ('type/realax/real' > $o) > 'type/realax/real')).
% 7.14/1.32 thf(func_def_16, type, sK2: ('type/realax/real' > ('type/realax/real' > $o) > 'type/realax/real')).
% 7.14/1.32 thf(func_def_17, type, sK3: ('type/realax/real' > $o)).
% 7.14/1.32 thf(func_def_18, type, sK4: ('type/realax/real' > $o)).
% 7.14/1.32 thf(func_def_19, type, sK5: 'type/realax/real').
% 7.14/1.32 thf(func_def_20, type, vNOT: ($o > $o)).
% 7.14/1.32 thf(func_def_21, type, sK6: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0))).
% 7.14/1.32 thf(func_def_22, type, sK7: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0))).
% 7.14/1.32 thf(func_def_23, type, sK8: 'type/realax/real').
% 7.14/1.32 thf(func_def_25, type, db1: !>[X0: $tType]:(X0)).
% 7.14/1.32 thf(func_def_26, type, sK10: 'type/realax/real').
% 7.14/1.32 thf(func_def_27, type, sK11: 'type/realax/real').
% 7.14/1.32 thf(f1,axiom,(
% 7.14/1.32 ! [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')) => ('const/realax/real_le' @ ('const/sets/sup' @ X0) @ X1))),
% 7.14/1.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','thm/sets/REAL_SUP_LE_')).
% 7.14/1.32 thf(f3,axiom,(
% 7.14/1.32 ! [X0 : $tType,X1 : (X0 > $o),X2 : X0] : ((('const/sets/IN' @ X0 @ X2 @ X1)) = ((X1 @ X2)))),
% 7.14/1.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','thm/sets/IN_')).
% 7.14/1.32 thf(f4,axiom,(
% 7.14/1.32 ! [X0 : $tType,X1 : X0] : ~('const/sets/IN' @ X0 @ X1 @ 'const/sets/EMPTY' @ X0)),
% 7.14/1.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','thm/sets/NOT_IN_EMPTY_')).
% 7.14/1.32 thf(f6,axiom,(
% 7.14/1.32 ! [X0 : $tType,X1 : (X0 > $o),X2 : (X0 > $o)] : ((('const/sets/SUBSET' @ X0 @ X1 @ X2)) = ! [X3 : X0] : (('const/sets/IN' @ X0 @ X3 @ X1) => ('const/sets/IN' @ X0 @ X3 @ X2)))),
% 7.14/1.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','thm/sets/SUBSET_')).
% 7.14/1.32 thf(f7,axiom,(
% 7.14/1.32 ! [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)))))),
% 7.14/1.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','thm/sets/SUP_')).
% 7.14/1.32 thf(f8,conjecture,(
% 7.14/1.32 ! [X0 : ('type/realax/real' > $o),X1 : ('type/realax/real' > $o)] : ((? [X2 : 'type/realax/real'] : ! [X3 : 'type/realax/real'] : (('const/sets/IN' @ 'type/realax/real' @ X3 @ X1) => ('const/realax/real_le' @ X3 @ X2)) & ('const/sets/SUBSET' @ 'type/realax/real' @ X0 @ X1) & (X0 != 'const/sets/EMPTY' @ 'type/realax/real')) => ('const/realax/real_le' @ ('const/sets/sup' @ X0) @ ('const/sets/sup' @ X1)))),
% 7.14/1.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','thm/sets/REAL_SUP_LE_SUBSET_')).
% 7.14/1.32 thf(f9,negated_conjecture,(
% 7.14/1.32 ~ ! [X0 : ('type/realax/real' > $o),X1 : ('type/realax/real' > $o)] : ((? [X2 : 'type/realax/real'] : ! [X3 : 'type/realax/real'] : (('const/sets/IN' @ 'type/realax/real' @ X3 @ X1) => ('const/realax/real_le' @ X3 @ X2)) & ('const/sets/SUBSET' @ 'type/realax/real' @ X0 @ X1) & (X0 != 'const/sets/EMPTY' @ 'type/realax/real')) => ('const/realax/real_le' @ ('const/sets/sup' @ X0) @ ('const/sets/sup' @ X1)))),
% 7.14/1.32 inference(negated_conjecture,[status(cth)],[f8])).
% 7.14/1.32 thf(f10,plain,(
% 7.14/1.32 ! [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')) => ('const/realax/real_le' @ ('const/sets/sup' @ X0) @ X1))),
% 7.14/1.32 inference(rectify,[],[f1])).
% 7.14/1.32 thf(f11,plain,(
% 7.14/1.32 ! [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)) => ((('const/realax/real_le' @ ('const/sets/sup' @ X0) @ X1)) = $true))),
% 7.14/1.32 inference(fool_elimination,[],[f10])).
% 7.14/1.32 thf(f12,plain,(
% 7.14/1.32 ! [X0 : $tType,X1 : X0] : ~('const/sets/IN' @ X0 @ X1 @ 'const/sets/EMPTY' @ X0)),
% 7.14/1.32 inference(rectify,[],[f4])).
% 7.14/1.32 thf(f13,plain,(
% 7.14/1.32 ! [X0 : $tType,X1 : X0] : ~ ((('const/sets/IN' @ X0 @ X1 @ 'const/sets/EMPTY' @ X0)) = $true)),
% 7.14/1.32 inference(fool_elimination,[],[f12])).
% 7.14/1.32 thf(f15,plain,(
% 7.14/1.32 ! [X0 : $tType,X1 : (X0 > $o),X2 : (X0 > $o)] : ((('const/sets/SUBSET' @ X0 @ X1 @ X2)) = ! [X3 : X0] : (('const/sets/IN' @ X0 @ X3 @ X1) => ('const/sets/IN' @ X0 @ X3 @ X2)))),
% 7.14/1.32 inference(rectify,[],[f6])).
% 7.14/1.32 thf(f16,plain,(
% 7.14/1.32 ! [X0 : $tType,X1 : (X0 > $o),X2 : (X0 > $o)] : ((('const/sets/SUBSET' @ X0 @ X1 @ X2)) = ((!! @ X0 @ (^[Y0 : X0]: (('const/sets/IN' @ X0 @ Y0 @ X1) => ('const/sets/IN' @ X0 @ Y0 @ X2))))))),
% 7.14/1.32 inference(fool_elimination,[],[f15])).
% 7.14/1.32 thf(f17,plain,(
% 7.14/1.32 ! [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)))))),
% 7.14/1.32 inference(rectify,[],[f7])).
% 7.14/1.32 thf(f18,plain,(
% 7.14/1.32 ! [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)))))))),
% 7.14/1.32 inference(fool_elimination,[],[f17])).
% 7.14/1.32 thf(f19,plain,(
% 7.14/1.32 ~ ! [X0 : ('type/realax/real' > $o),X1 : ('type/realax/real' > $o)] : ((? [X2 : 'type/realax/real'] : ! [X3 : 'type/realax/real'] : (('const/sets/IN' @ 'type/realax/real' @ X3 @ X1) => ('const/realax/real_le' @ X3 @ X2)) & ('const/sets/SUBSET' @ 'type/realax/real' @ X0 @ X1) & (X0 != 'const/sets/EMPTY' @ 'type/realax/real')) => ('const/realax/real_le' @ ('const/sets/sup' @ X0) @ ('const/sets/sup' @ X1)))),
% 7.14/1.32 inference(rectify,[],[f9])).
% 7.14/1.32 thf(f20,plain,(
% 7.14/1.32 ~ ! [X0 : ('type/realax/real' > $o),X1 : ('type/realax/real' > $o)] : ((? [X2 : 'type/realax/real'] : ! [X3 : 'type/realax/real'] : (((('const/sets/IN' @ 'type/realax/real' @ X3 @ X1)) = $true) => ((('const/realax/real_le' @ X3 @ X2)) = $true)) & ((('const/sets/SUBSET' @ 'type/realax/real' @ X0 @ X1)) = $true) & ('const/sets/EMPTY' @ 'type/realax/real' != X0)) => ((('const/realax/real_le' @ ('const/sets/sup' @ X0) @ ('const/sets/sup' @ X1))) = $true))),
% 7.14/1.32 inference(fool_elimination,[],[f19])).
% 7.14/1.32 thf(f21,plain,(
% 7.14/1.32 ! [X0 : $tType,X1 : X0] : ((('const/sets/IN' @ X0 @ X1 @ 'const/sets/EMPTY' @ X0)) != $true)),
% 7.14/1.32 inference(flattening,[],[f13])).
% 7.14/1.32 thf(f22,plain,(
% 7.14/1.32 ! [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)) | ('const/sets/EMPTY' @ 'type/realax/real' = X0)))),
% 7.14/1.32 inference(ennf_transformation,[],[f11])).
% 7.14/1.32 thf(f23,plain,(
% 7.14/1.32 ! [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)) | ('const/sets/EMPTY' @ 'type/realax/real' = X0))),
% 7.14/1.32 inference(flattening,[],[f22])).
% 7.14/1.32 thf(f24,plain,(
% 7.14/1.32 ! [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)))),
% 7.14/1.32 inference(ennf_transformation,[],[f18])).
% 7.14/1.32 thf(f25,plain,(
% 7.14/1.32 ! [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))),
% 7.14/1.32 inference(flattening,[],[f24])).
% 7.14/1.32 thf(f26,plain,(
% 7.14/1.32 ? [X0 : ('type/realax/real' > $o),X1 : ('type/realax/real' > $o)] : (((('const/realax/real_le' @ ('const/sets/sup' @ X0) @ ('const/sets/sup' @ X1))) != $true) & (? [X2 : 'type/realax/real'] : ! [X3 : 'type/realax/real'] : (((('const/realax/real_le' @ X3 @ X2)) = $true) | ((('const/sets/IN' @ 'type/realax/real' @ X3 @ X1)) != $true)) & ((('const/sets/SUBSET' @ 'type/realax/real' @ X0 @ X1)) = $true) & ('const/sets/EMPTY' @ 'type/realax/real' != X0)))),
% 7.14/1.32 inference(ennf_transformation,[],[f20])).
% 7.14/1.32 thf(f27,plain,(
% 7.14/1.32 ? [X0 : ('type/realax/real' > $o),X1 : ('type/realax/real' > $o)] : (((('const/realax/real_le' @ ('const/sets/sup' @ X0) @ ('const/sets/sup' @ X1))) != $true) & ? [X2 : 'type/realax/real'] : ! [X3 : 'type/realax/real'] : (((('const/realax/real_le' @ X3 @ X2)) = $true) | ((('const/sets/IN' @ 'type/realax/real' @ X3 @ X1)) != $true)) & ((('const/sets/SUBSET' @ 'type/realax/real' @ X0 @ X1)) = $true) & ('const/sets/EMPTY' @ 'type/realax/real' != X0))),
% 7.14/1.32 inference(flattening,[],[f26])).
% 7.14/1.32 thf(f28,plain,(
% 7.14/1.32 ! [X0 : ('type/realax/real' > $o),X1 : 'type/realax/real'] : (((('const/realax/real_le' @ ('const/sets/sup' @ X0) @ X1)) = $true) | (($true != (('const/realax/real_le' @ (sK0 @ X1 @ X0) @ X1))) & ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK0 @ X1 @ X0) @ X0)))) | ('const/sets/EMPTY' @ 'type/realax/real' = X0))),
% 7.14/1.32 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP]),skolemize(X2,sK0 @ X1 @ X0)],[f23])).
% 7.14/1.32 thf(f29,plain,(
% 7.14/1.32 ! [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))),
% 7.14/1.32 inference(rectify,[],[f25])).
% 7.14/1.32 thf(f30,plain,(
% 7.14/1.32 ! [X0 : ('type/realax/real' > $o)] : ((! [X1 : 'type/realax/real'] : (((('const/realax/real_le' @ ('const/sets/sup' @ X0) @ X1)) = $true) | (($true != (('const/realax/real_le' @ (sK1 @ X1 @ X0) @ X1))) & ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK1 @ 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' @ (sK2 @ X4 @ X0) @ X4))) & ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK2 @ X4 @ X0) @ X0)))) | ('const/sets/EMPTY' @ 'type/realax/real' = X0))),
% 7.14/1.32 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP,vAPP]),skolemize(X2,sK0 @ X1 @ X0),skolemize(X2,sK0 @ X1 @ X0)],[f29])).
% 7.14/1.32 thf(f31,plain,(
% 7.14/1.32 ($true != (('const/realax/real_le' @ ('const/sets/sup' @ sK3) @ ('const/sets/sup' @ sK4)))) & ! [X3 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ X3 @ sK5))) | ($true != (('const/sets/IN' @ 'type/realax/real' @ X3 @ sK4)))) & ($true = (('const/sets/SUBSET' @ 'type/realax/real' @ sK3 @ sK4))) & ('const/sets/EMPTY' @ 'type/realax/real' != sK3)),
% 7.14/1.32 inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4,sK5]),skolemize(X0,sK3),skolemize(X1,sK4),skolemize(X2,sK5)],[f27])).
% 7.14/1.32 thf(f32,plain,(
% 7.14/1.32 ( ! [X0 : ('type/realax/real' > $o),X1 : 'type/realax/real'] : (($true = (('const/sets/IN' @ 'type/realax/real' @ (sK0 @ X1 @ X0) @ X0))) | ((('const/realax/real_le' @ ('const/sets/sup' @ X0) @ X1)) = $true) | ('const/sets/EMPTY' @ 'type/realax/real' = X0)) )),
% 7.14/1.32 inference(cnf_transformation,[],[f28])).
% 7.14/1.32 thf(f33,plain,(
% 7.14/1.32 ( ! [X0 : ('type/realax/real' > $o),X1 : 'type/realax/real'] : (($true != (('const/realax/real_le' @ (sK0 @ X1 @ X0) @ X1))) | ((('const/realax/real_le' @ ('const/sets/sup' @ X0) @ X1)) = $true) | ('const/sets/EMPTY' @ 'type/realax/real' = X0)) )),
% 7.14/1.32 inference(cnf_transformation,[],[f28])).
% 7.14/1.32 thf(f35,plain,(
% 7.14/1.32 ( ! [X0 : $tType,X2 : X0,X1 : (X0 > $o)] : (((('const/sets/IN' @ X0 @ X2 @ X1)) = ((X1 @ X2)))) )),
% 7.14/1.32 inference(cnf_transformation,[],[f3])).
% 7.14/1.32 thf(f36,plain,(
% 7.14/1.32 ( ! [X0 : $tType,X1 : X0] : (((('const/sets/IN' @ X0 @ X1 @ 'const/sets/EMPTY' @ X0)) != $true)) )),
% 7.14/1.32 inference(cnf_transformation,[],[f21])).
% 7.14/1.32 thf(f38,plain,(
% 7.14/1.32 ( ! [X0 : $tType,X2 : (X0 > $o),X1 : (X0 > $o)] : (((('const/sets/SUBSET' @ X0 @ X1 @ X2)) = ((!! @ X0 @ (^[Y0 : X0]: (('const/sets/IN' @ X0 @ Y0 @ X1) => ('const/sets/IN' @ X0 @ Y0 @ X2))))))) )),
% 7.14/1.32 inference(cnf_transformation,[],[f16])).
% 7.14/1.32 thf(f39,plain,(
% 7.14/1.32 ( ! [X3 : 'type/realax/real',X0 : ('type/realax/real' > $o),X4 : 'type/realax/real'] : (($true = (('const/sets/IN' @ 'type/realax/real' @ (sK2 @ X4 @ X0) @ X0))) | ($true = (('const/realax/real_le' @ X3 @ ('const/sets/sup' @ X0)))) | ($true != (('const/sets/IN' @ 'type/realax/real' @ X3 @ X0))) | ('const/sets/EMPTY' @ 'type/realax/real' = X0)) )),
% 7.14/1.32 inference(cnf_transformation,[],[f30])).
% 7.14/1.32 thf(f40,plain,(
% 7.14/1.32 ( ! [X3 : 'type/realax/real',X0 : ('type/realax/real' > $o),X4 : 'type/realax/real'] : (($true != (('const/realax/real_le' @ (sK2 @ 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)) )),
% 7.14/1.32 inference(cnf_transformation,[],[f30])).
% 7.14/1.32 thf(f45,plain,(
% 7.14/1.32 ('const/sets/EMPTY' @ 'type/realax/real' != sK3)),
% 7.14/1.32 inference(cnf_transformation,[],[f31])).
% 7.14/1.32 thf(f46,plain,(
% 7.14/1.32 ($true = (('const/sets/SUBSET' @ 'type/realax/real' @ sK3 @ sK4)))),
% 7.14/1.32 inference(cnf_transformation,[],[f31])).
% 7.14/1.32 thf(f47,plain,(
% 7.14/1.32 ( ! [X3 : 'type/realax/real'] : (($true != (('const/sets/IN' @ 'type/realax/real' @ X3 @ sK4))) | ($true = (('const/realax/real_le' @ X3 @ sK5)))) )),
% 7.14/1.32 inference(cnf_transformation,[],[f31])).
% 7.14/1.32 thf(f48,plain,(
% 7.14/1.32 ($true != (('const/realax/real_le' @ ('const/sets/sup' @ sK3) @ ('const/sets/sup' @ sK4))))),
% 7.14/1.32 inference(cnf_transformation,[],[f31])).
% 7.14/1.32 thf(f50,definition,(
% 7.14/1.32 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 7.14/1.32 introduced(theory,[fool_exhaustiveness_axiom])).
% 7.14/1.32 thf(f52,plain,(
% 7.14/1.32 ( ! [X0 : $tType,X2 : (X0 > $o),X1 : (X0 > $o)] : (((('const/sets/SUBSET' @ X0 @ X1 @ X2)) = $false) | ($true = ((!! @ X0 @ (^[Y0 : X0]: (('const/sets/IN' @ X0 @ Y0 @ X1) => ('const/sets/IN' @ X0 @ Y0 @ X2))))))) )),
% 7.14/1.32 inference(iff_proxy_clausification,[],[f38])).
% 7.14/1.32 thf(f53,plain,(
% 7.14/1.32 ( ! [X0 : $tType,X2 : (X0 > $o),X3 : X0,X1 : (X0 > $o)] : (((('const/sets/SUBSET' @ X0 @ X1 @ X2)) = $false) | ($true = (((^[Y0 : X0]: (('const/sets/IN' @ X0 @ Y0 @ X1) => ('const/sets/IN' @ X0 @ Y0 @ X2))) @ X3)))) )),
% 7.14/1.32 inference(pi_proxy_clausification,[],[f52])).
% 7.14/1.32 thf(f54,plain,(
% 7.14/1.32 ( ! [X0 : $tType,X2 : (X0 > $o),X3 : X0,X1 : (X0 > $o)] : (((('const/sets/SUBSET' @ X0 @ X1 @ X2)) = $false) | ($true = ((('const/sets/IN' @ X0 @ X3 @ X1) => ('const/sets/IN' @ X0 @ X3 @ X2))))) )),
% 7.14/1.32 inference(beta-eta_normalization,[],[f53])).
% 7.14/1.32 thf(f55,plain,(
% 7.14/1.32 ( ! [X0 : $tType,X2 : (X0 > $o),X3 : X0,X1 : (X0 > $o)] : (((('const/sets/SUBSET' @ X0 @ X1 @ X2)) = $false) | ((('const/sets/IN' @ X0 @ X3 @ X1)) = $false) | ((('const/sets/IN' @ X0 @ X3 @ X2)) = $true)) )),
% 7.14/1.32 inference(imp_proxy_clausification,[],[f54])).
% 7.14/1.32 thf(f74,plain,(
% 7.14/1.32 ( ! [X0 : $tType,X2 : X0,X1 : (X0 > $o)] : (((('const/sets/IN' @ X0 @ X2 @ X1)) = $true) | (((X1 @ X2)) = $false)) )),
% 7.14/1.32 inference(iff_proxy_clausification,[],[f35])).
% 7.14/1.32 thf(f100,plain,(
% 7.14/1.32 ($true != $true) | ((('const/realax/real_le' @ ('const/sets/sup' @ sK3) @ ('const/sets/sup' @ sK4))) = $false)),
% 7.14/1.32 inference(constrained_superposition,[],[f48,f50])).
% 7.14/1.32 thf(f101,plain,(
% 7.14/1.32 ( ! [X0 : 'type/realax/real'] : (($true != $true) | ($true = (('const/realax/real_le' @ X0 @ sK5))) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK4)))) )),
% 7.14/1.32 inference(constrained_superposition,[],[f47,f50])).
% 7.14/1.32 thf(f103,plain,(
% 7.14/1.32 ( ! [X0 : 'type/realax/real'] : (($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK4))) | ($true = (('const/realax/real_le' @ X0 @ sK5)))) )),
% 7.14/1.32 inference(trivial_inequality_removal,[],[f101])).
% 7.14/1.32 thf(f104,plain,(
% 7.14/1.32 ((('const/realax/real_le' @ ('const/sets/sup' @ sK3) @ ('const/sets/sup' @ sK4))) = $false)),
% 7.14/1.32 inference(trivial_inequality_removal,[],[f100])).
% 7.14/1.32 thf(f137,definition,(
% 7.14/1.32 spl9_5 <=> ('const/sets/EMPTY' @ 'type/realax/real' = sK4)),
% 7.14/1.32 introduced(definition,[new_symbols(definition,[spl9_5])],[avatar_definition])).
% 7.14/1.32 thf(f138,plain,(
% 7.14/1.32 ('const/sets/EMPTY' @ 'type/realax/real' != sK4) | spl9_5),
% 7.14/1.32 inference(avatar_component_clause,[],[f137])).
% 7.14/1.32 thf(f139,plain,(
% 7.14/1.32 ('const/sets/EMPTY' @ 'type/realax/real' = sK4) | ~spl9_5),
% 7.14/1.32 inference(avatar_component_clause,[],[f137])).
% 7.14/1.32 thf(f151,plain,(
% 7.14/1.32 ($true = (('const/sets/SUBSET' @ 'type/realax/real' @ sK3 @ 'const/sets/EMPTY' @ 'type/realax/real'))) | ~spl9_5),
% 7.14/1.32 inference(constrained_superposition,[],[f46,f139])).
% 7.14/1.32 thf(f157,plain,(
% 7.14/1.32 ( ! [X0 : $tType,X1 : X0] : (($true != $true) | ($false = (('const/sets/EMPTY' @ X0 @ X1)))) )),
% 7.14/1.32 inference(constrained_superposition,[],[f36,f74])).
% 7.14/1.32 thf(f166,plain,(
% 7.14/1.32 ( ! [X0 : $tType,X1 : X0] : (($false = (('const/sets/EMPTY' @ X0 @ X1)))) )),
% 7.14/1.32 inference(trivial_inequality_removal,[],[f157])).
% 7.14/1.32 thf(f187,plain,(
% 7.14/1.32 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : (($true = $false) | ($true = (('const/realax/real_le' @ X1 @ ('const/sets/sup' @ sK4)))) | ($true != (('const/sets/IN' @ 'type/realax/real' @ X1 @ sK4))) | ('const/sets/EMPTY' @ 'type/realax/real' = sK4) | ($true = (('const/realax/real_le' @ (sK2 @ X0 @ sK4) @ sK5)))) )),
% 7.14/1.32 inference(constrained_superposition,[],[f39,f103])).
% 7.14/1.32 thf(f202,plain,(
% 7.14/1.32 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ X1 @ ('const/sets/sup' @ sK4)))) | ($true != (('const/sets/IN' @ 'type/realax/real' @ X1 @ sK4))) | ('const/sets/EMPTY' @ 'type/realax/real' = sK4) | ($true = (('const/realax/real_le' @ (sK2 @ X0 @ sK4) @ sK5)))) )),
% 7.14/1.32 inference(trivial_inequality_removal,[],[f187])).
% 7.14/1.32 thf(f569,definition,(
% 7.14/1.32 spl9_12 <=> ('const/sets/EMPTY' @ 'type/realax/real' = (^[Y0 : 'type/realax/real']: ($false)))),
% 7.14/1.32 introduced(definition,[new_symbols(definition,[spl9_12])],[avatar_definition])).
% 7.14/1.32 thf(f570,plain,(
% 7.14/1.32 ('const/sets/EMPTY' @ 'type/realax/real' != (^[Y0 : 'type/realax/real']: ($false))) | spl9_12),
% 7.14/1.32 inference(avatar_component_clause,[],[f569])).
% 7.14/1.32 thf(f571,plain,(
% 7.14/1.32 ('const/sets/EMPTY' @ 'type/realax/real' = (^[Y0 : 'type/realax/real']: ($false))) | ~spl9_12),
% 7.14/1.32 inference(avatar_component_clause,[],[f569])).
% 7.14/1.32 thf(f1176,plain,(
% 7.14/1.32 ((('const/sets/EMPTY' @ 'type/realax/real' @ sK10)) != (((^[Y0 : 'type/realax/real']: ($false)) @ sK10))) | spl9_12),
% 7.14/1.32 inference(negative_extensionality,[],[f570])).
% 7.14/1.32 thf(f1177,plain,(
% 7.14/1.32 ($true = (('const/sets/EMPTY' @ 'type/realax/real' @ sK10))) | ($true = (((^[Y0 : 'type/realax/real']: ($false)) @ sK10))) | spl9_12),
% 7.14/1.32 inference(xor_proxy_clausification,[],[f1176])).
% 7.14/1.32 thf(f1180,plain,(
% 7.14/1.32 ($true = (('const/sets/EMPTY' @ 'type/realax/real' @ sK10))) | ($true = $false) | spl9_12),
% 7.14/1.32 inference(beta-eta_normalization,[],[f1177])).
% 7.14/1.32 thf(f1181,plain,(
% 7.14/1.32 ($true = (('const/sets/EMPTY' @ 'type/realax/real' @ sK10))) | spl9_12),
% 7.14/1.32 inference(trivial_inequality_removal,[],[f1180])).
% 7.14/1.32 thf(f1182,plain,(
% 7.14/1.32 ($true = $false) | spl9_12),
% 7.14/1.32 inference(forward_demodulation,[],[f1181,f166])).
% 7.14/1.32 thf(f1183,plain,(
% 7.14/1.32 $false | spl9_12),
% 7.14/1.32 inference(trivial_inequality_removal,[],[f1182])).
% 7.14/1.32 thf(f1184,plain,(
% 7.14/1.32 spl9_12),
% 7.14/1.32 inference(avatar_contradiction_clause,[],[f1183])).
% 7.14/1.32 thf(f1215,plain,(
% 7.14/1.32 ( ! [X0 : 'type/realax/real'] : (($true = $false) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK3))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ X0 @ 'const/sets/EMPTY' @ 'type/realax/real')))) ) | ~spl9_5),
% 7.14/1.32 inference(constrained_superposition,[],[f151,f55])).
% 7.14/1.32 thf(f1218,plain,(
% 7.14/1.32 ( ! [X2 : ('type/realax/real' > $o),X0 : 'type/realax/real',X1 : ('type/realax/real' > $o)] : (($true = $false) | ($true = (('const/realax/real_le' @ ('const/sets/sup' @ X1) @ X0))) | ('const/sets/EMPTY' @ 'type/realax/real' = X1) | ($false = (('const/sets/SUBSET' @ 'type/realax/real' @ X1 @ X2))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK0 @ X0 @ X1) @ X2)))) )),
% 7.14/1.32 inference(constrained_superposition,[],[f32,f55])).
% 7.14/1.32 thf(f1242,plain,(
% 7.14/1.32 ( ! [X2 : ('type/realax/real' > $o),X0 : 'type/realax/real',X1 : ('type/realax/real' > $o)] : (($true = (('const/realax/real_le' @ ('const/sets/sup' @ X1) @ X0))) | ('const/sets/EMPTY' @ 'type/realax/real' = X1) | ($false = (('const/sets/SUBSET' @ 'type/realax/real' @ X1 @ X2))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK0 @ X0 @ X1) @ X2)))) )),
% 7.14/1.32 inference(trivial_inequality_removal,[],[f1218])).
% 7.14/1.32 thf(f1245,plain,(
% 7.14/1.32 ( ! [X0 : 'type/realax/real'] : (($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK3))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ X0 @ 'const/sets/EMPTY' @ 'type/realax/real')))) ) | ~spl9_5),
% 7.14/1.32 inference(trivial_inequality_removal,[],[f1215])).
% 7.14/1.32 thf(f1270,plain,(
% 7.14/1.32 ( ! [X2 : ('type/realax/real' > $o),X0 : 'type/realax/real',X1 : ('type/realax/real' > $o)] : (($true = (('const/sets/IN' @ 'type/realax/real' @ (sK0 @ X0 @ X1) @ X2))) | ($true = (('const/realax/real_le' @ ('const/sets/sup' @ X1) @ X0))) | ($false = (('const/sets/SUBSET' @ 'type/realax/real' @ X1 @ X2))) | ((^[Y0 : 'type/realax/real']: ($false)) = X1)) ) | ~spl9_12),
% 7.14/1.32 inference(forward_demodulation,[],[f1242,f571])).
% 7.14/1.32 thf(f1273,plain,(
% 7.14/1.32 ( ! [X0 : 'type/realax/real'] : (($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK3)))) ) | ~spl9_5),
% 7.14/1.32 inference(forward_subsumption_resolution,[],[f1245,f36])).
% 7.14/1.32 thf(f1331,plain,(
% 7.14/1.32 ( ! [X0 : 'type/realax/real'] : (($true = $false) | ($true = (('const/realax/real_le' @ ('const/sets/sup' @ sK3) @ X0))) | ('const/sets/EMPTY' @ 'type/realax/real' = sK3)) ) | ~spl9_5),
% 7.14/1.32 inference(constrained_superposition,[],[f32,f1273])).
% 7.14/1.32 thf(f1346,plain,(
% 7.14/1.32 ( ! [X0 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ ('const/sets/sup' @ sK3) @ X0))) | ('const/sets/EMPTY' @ 'type/realax/real' = sK3)) ) | ~spl9_5),
% 7.14/1.32 inference(trivial_inequality_removal,[],[f1331])).
% 7.14/1.32 thf(f1364,plain,(
% 7.14/1.32 ( ! [X0 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ ('const/sets/sup' @ sK3) @ X0)))) ) | ~spl9_5),
% 7.14/1.32 inference(forward_subsumption_resolution,[],[f1346,f45])).
% 7.14/1.32 thf(f1375,definition,(
% 7.14/1.32 spl9_27 <=> ! [X0 : 'type/realax/real'] : ($true = (('const/realax/real_le' @ ('const/sets/sup' @ sK3) @ X0)))),
% 7.14/1.32 introduced(definition,[new_symbols(definition,[spl9_27])],[avatar_definition])).
% 7.14/1.32 thf(f1376,plain,(
% 7.14/1.32 ( ! [X0 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ ('const/sets/sup' @ sK3) @ X0)))) ) | ~spl9_27),
% 7.14/1.32 inference(avatar_component_clause,[],[f1375])).
% 7.14/1.32 thf(f1385,plain,(
% 7.14/1.32 spl9_27 | ~spl9_5),
% 7.14/1.32 inference(avatar_split_clause,[],[f1364,f137,f1375])).
% 7.14/1.32 thf(f1392,plain,(
% 7.14/1.32 (sK4 != (^[Y0 : 'type/realax/real']: ($false))) | (spl9_5 | ~spl9_12)),
% 7.14/1.32 inference(forward_demodulation,[],[f138,f571])).
% 7.14/1.32 thf(f1398,plain,(
% 7.14/1.32 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : ((sK4 = (^[Y0 : 'type/realax/real']: ($false))) | ($true = (('const/realax/real_le' @ X1 @ ('const/sets/sup' @ sK4)))) | ($true != (('const/sets/IN' @ 'type/realax/real' @ X1 @ sK4))) | ($true = (('const/realax/real_le' @ (sK2 @ X0 @ sK4) @ sK5)))) ) | ~spl9_12),
% 7.14/1.32 inference(forward_demodulation,[],[f202,f571])).
% 7.14/1.32 thf(f1446,definition,(
% 7.14/1.32 spl9_31 <=> ! [X1 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ X1 @ ('const/sets/sup' @ sK4)))) | ($true != (('const/sets/IN' @ 'type/realax/real' @ X1 @ sK4))))),
% 7.14/1.32 introduced(definition,[new_symbols(definition,[spl9_31])],[avatar_definition])).
% 7.14/1.32 thf(f1447,plain,(
% 7.14/1.32 ( ! [X1 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ X1 @ ('const/sets/sup' @ sK4)))) | ($true != (('const/sets/IN' @ 'type/realax/real' @ X1 @ sK4)))) ) | ~spl9_31),
% 7.14/1.32 inference(avatar_component_clause,[],[f1446])).
% 7.14/1.32 thf(f1449,definition,(
% 7.14/1.32 spl9_32 <=> ! [X0 : 'type/realax/real'] : ($true = (('const/realax/real_le' @ (sK2 @ X0 @ sK4) @ sK5)))),
% 7.14/1.32 introduced(definition,[new_symbols(definition,[spl9_32])],[avatar_definition])).
% 7.14/1.32 thf(f1450,plain,(
% 7.14/1.32 ( ! [X0 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ (sK2 @ X0 @ sK4) @ sK5)))) ) | ~spl9_32),
% 7.14/1.32 inference(avatar_component_clause,[],[f1449])).
% 7.14/1.32 thf(f1489,definition,(
% 7.14/1.32 spl9_38 <=> (sK4 = (^[Y0 : 'type/realax/real']: ($false)))),
% 7.14/1.32 introduced(definition,[new_symbols(definition,[spl9_38])],[avatar_definition])).
% 7.14/1.32 thf(f1490,plain,(
% 7.14/1.32 (sK4 != (^[Y0 : 'type/realax/real']: ($false))) | spl9_38),
% 7.14/1.32 inference(avatar_component_clause,[],[f1489])).
% 7.14/1.32 thf(f1497,plain,(
% 7.14/1.32 spl9_32 | spl9_31 | spl9_38 | ~spl9_12),
% 7.14/1.32 inference(avatar_split_clause,[],[f1398,f569,f1489,f1446,f1449])).
% 7.14/1.32 thf(f1515,plain,(
% 7.14/1.32 ~spl9_38 | spl9_5 | ~spl9_12),
% 7.14/1.32 inference(avatar_split_clause,[],[f1392,f569,f137,f1489])).
% 7.14/1.32 thf(f1524,plain,(
% 7.14/1.32 ( ! [X0 : 'type/realax/real'] : (($true != $true) | ($true != (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK4))) | ($true = (('const/realax/real_le' @ X0 @ ('const/sets/sup' @ sK4)))) | ('const/sets/EMPTY' @ 'type/realax/real' = sK4)) ) | ~spl9_32),
% 7.14/1.32 inference(constrained_superposition,[],[f40,f1450])).
% 7.14/1.32 thf(f1525,plain,(
% 7.14/1.32 ( ! [X0 : 'type/realax/real'] : (($true != (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK4))) | ($true = (('const/realax/real_le' @ X0 @ ('const/sets/sup' @ sK4)))) | ('const/sets/EMPTY' @ 'type/realax/real' = sK4)) ) | ~spl9_32),
% 7.14/1.32 inference(trivial_inequality_removal,[],[f1524])).
% 7.14/1.32 thf(f1528,plain,(
% 7.14/1.32 ( ! [X0 : 'type/realax/real'] : ((sK4 = (^[Y0 : 'type/realax/real']: ($false))) | ($true != (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK4))) | ($true = (('const/realax/real_le' @ X0 @ ('const/sets/sup' @ sK4))))) ) | (~spl9_12 | ~spl9_32)),
% 7.14/1.32 inference(forward_demodulation,[],[f1525,f571])).
% 7.14/1.32 thf(f1531,plain,(
% 7.14/1.32 ( ! [X0 : 'type/realax/real'] : (($true != (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK4))) | ($true = (('const/realax/real_le' @ X0 @ ('const/sets/sup' @ sK4))))) ) | (~spl9_12 | ~spl9_32 | spl9_38)),
% 7.14/1.32 inference(forward_subsumption_resolution,[],[f1528,f1490])).
% 7.14/1.32 thf(f1534,plain,(
% 7.14/1.32 spl9_31 | ~spl9_12 | ~spl9_32 | spl9_38),
% 7.14/1.32 inference(avatar_split_clause,[],[f1531,f1489,f1449,f569,f1446])).
% 7.14/1.32 thf(f1536,plain,(
% 7.14/1.32 ($true = $false) | ~spl9_27),
% 7.14/1.32 inference(constrained_superposition,[],[f1376,f104])).
% 7.14/1.32 thf(f1543,plain,(
% 7.14/1.32 $false | ~spl9_27),
% 7.14/1.32 inference(trivial_inequality_removal,[],[f1536])).
% 7.14/1.32 thf(f1544,plain,(
% 7.14/1.32 ~spl9_27),
% 7.14/1.32 inference(avatar_contradiction_clause,[],[f1543])).
% 7.14/1.32 thf(f1583,plain,(
% 7.14/1.32 ( ! [X0 : ('type/realax/real' > $o)] : (($true != $true) | ($true = (('const/realax/real_le' @ ('const/sets/sup' @ X0) @ ('const/sets/sup' @ sK4)))) | ('const/sets/EMPTY' @ 'type/realax/real' = X0) | ($true != (('const/sets/IN' @ 'type/realax/real' @ (sK0 @ ('const/sets/sup' @ sK4) @ X0) @ sK4)))) ) | ~spl9_31),
% 7.14/1.32 inference(constrained_superposition,[],[f33,f1447])).
% 7.14/1.32 thf(f1600,plain,(
% 7.14/1.32 ( ! [X0 : ('type/realax/real' > $o)] : (($true = (('const/realax/real_le' @ ('const/sets/sup' @ X0) @ ('const/sets/sup' @ sK4)))) | ('const/sets/EMPTY' @ 'type/realax/real' = X0) | ($true != (('const/sets/IN' @ 'type/realax/real' @ (sK0 @ ('const/sets/sup' @ sK4) @ X0) @ sK4)))) ) | ~spl9_31),
% 7.14/1.32 inference(trivial_inequality_removal,[],[f1583])).
% 7.14/1.32 thf(f1612,plain,(
% 7.14/1.32 ( ! [X0 : ('type/realax/real' > $o)] : (($true != (('const/sets/IN' @ 'type/realax/real' @ (sK0 @ ('const/sets/sup' @ sK4) @ X0) @ sK4))) | ($true = (('const/realax/real_le' @ ('const/sets/sup' @ X0) @ ('const/sets/sup' @ sK4)))) | ((^[Y0 : 'type/realax/real']: ($false)) = X0)) ) | (~spl9_12 | ~spl9_31)),
% 7.14/1.32 inference(forward_demodulation,[],[f1600,f571])).
% 7.14/1.32 thf(f1895,plain,(
% 7.14/1.32 ( ! [X0 : ('type/realax/real' > $o)] : (($true != $true) | ($true = (('const/realax/real_le' @ ('const/sets/sup' @ X0) @ ('const/sets/sup' @ sK4)))) | ((^[Y0 : 'type/realax/real']: ($false)) = X0) | ($true = (('const/realax/real_le' @ ('const/sets/sup' @ X0) @ ('const/sets/sup' @ sK4)))) | ($false = (('const/sets/SUBSET' @ 'type/realax/real' @ X0 @ sK4))) | ((^[Y0 : 'type/realax/real']: ($false)) = X0)) ) | (~spl9_12 | ~spl9_31)),
% 7.14/1.32 inference(constrained_superposition,[],[f1612,f1270])).
% 7.14/1.32 thf(f1901,plain,(
% 7.14/1.32 ( ! [X0 : ('type/realax/real' > $o)] : (($true != $true) | ($true = (('const/realax/real_le' @ ('const/sets/sup' @ X0) @ ('const/sets/sup' @ sK4)))) | ((^[Y0 : 'type/realax/real']: ($false)) = X0) | ($false = (('const/sets/SUBSET' @ 'type/realax/real' @ X0 @ sK4)))) ) | (~spl9_12 | ~spl9_31)),
% 7.14/1.32 inference(duplicate_literal_removal,[],[f1895])).
% 7.14/1.32 thf(f1902,plain,(
% 7.14/1.32 ( ! [X0 : ('type/realax/real' > $o)] : (($true = (('const/realax/real_le' @ ('const/sets/sup' @ X0) @ ('const/sets/sup' @ sK4)))) | ((^[Y0 : 'type/realax/real']: ($false)) = X0) | ($false = (('const/sets/SUBSET' @ 'type/realax/real' @ X0 @ sK4)))) ) | (~spl9_12 | ~spl9_31)),
% 7.14/1.32 inference(trivial_inequality_removal,[],[f1901])).
% 7.14/1.32 thf(f3079,definition,(
% 7.14/1.32 spl9_47 <=> (sK3 = (^[Y0 : 'type/realax/real']: ($false)))),
% 7.14/1.32 introduced(definition,[new_symbols(definition,[spl9_47])],[avatar_definition])).
% 7.14/1.32 thf(f3081,plain,(
% 7.14/1.32 (sK3 = (^[Y0 : 'type/realax/real']: ($false))) | ~spl9_47),
% 7.14/1.32 inference(avatar_component_clause,[],[f3079])).
% 7.14/1.32 thf(f4160,plain,(
% 7.14/1.32 ($true != $true) | (sK3 = (^[Y0 : 'type/realax/real']: ($false))) | ((('const/sets/SUBSET' @ 'type/realax/real' @ sK3 @ sK4)) = $false) | (~spl9_12 | ~spl9_31)),
% 7.14/1.32 inference(constrained_superposition,[],[f48,f1902])).
% 7.14/1.32 thf(f4161,plain,(
% 7.14/1.32 (sK3 = (^[Y0 : 'type/realax/real']: ($false))) | ((('const/sets/SUBSET' @ 'type/realax/real' @ sK3 @ sK4)) = $false) | (~spl9_12 | ~spl9_31)),
% 7.14/1.32 inference(trivial_inequality_removal,[],[f4160])).
% 7.14/1.32 thf(f4172,plain,(
% 7.14/1.32 ($true = $false) | (sK3 = (^[Y0 : 'type/realax/real']: ($false))) | (~spl9_12 | ~spl9_31)),
% 7.14/1.32 inference(forward_demodulation,[],[f4161,f46])).
% 7.14/1.32 thf(f4173,plain,(
% 7.14/1.32 (sK3 = (^[Y0 : 'type/realax/real']: ($false))) | (~spl9_12 | ~spl9_31)),
% 7.14/1.32 inference(trivial_inequality_removal,[],[f4172])).
% 7.14/1.32 thf(f4178,plain,(
% 7.14/1.32 spl9_47 | ~spl9_12 | ~spl9_31),
% 7.14/1.32 inference(avatar_split_clause,[],[f4173,f1446,f569,f3079])).
% 7.14/1.32 thf(f4238,plain,(
% 7.14/1.32 ('const/sets/EMPTY' @ 'type/realax/real' != (^[Y0 : 'type/realax/real']: ($false))) | ~spl9_47),
% 7.14/1.32 inference(constrained_superposition,[],[f45,f3081])).
% 7.14/1.32 thf(f4269,plain,(
% 7.14/1.32 $false | (~spl9_12 | ~spl9_47)),
% 7.14/1.32 inference(forward_subsumption_resolution,[],[f4238,f571])).
% 7.14/1.32 thf(f4270,plain,(
% 7.14/1.32 ~spl9_12 | ~spl9_47),
% 7.14/1.32 inference(avatar_contradiction_clause,[],[f4269])).
% 7.14/1.32 cnf(s32, plain, spl9_12, inference(sat_conversion,[],[f1184])).
% 7.14/1.32 cnf(s34, plain, ~spl9_5 | spl9_27, inference(sat_conversion,[],[f1385])).
% 7.14/1.32 cnf(s66, plain, ~spl9_12 | spl9_31 | spl9_32 | spl9_38, inference(sat_conversion,[],[f1497])).
% 7.14/1.32 cnf(s82, plain, spl9_5 | ~spl9_12 | ~spl9_38, inference(sat_conversion,[],[f1515])).
% 7.14/1.32 cnf(s84, plain, ~spl9_12 | spl9_31 | ~spl9_32 | spl9_38, inference(sat_conversion,[],[f1534])).
% 7.14/1.32 cnf(s88, plain, ~spl9_27, inference(sat_conversion,[],[f1544])).
% 7.14/1.32 cnf(s140, plain, ~spl9_12 | ~spl9_31 | spl9_47, inference(sat_conversion,[],[f4178])).
% 7.14/1.32 cnf(s145, plain, ~spl9_12 | ~spl9_47, inference(sat_conversion,[],[f4270])).
% 7.14/1.32 cnf(s149, plain, ~spl9_5, inference(rat,[],[s34,s88])).
% 7.14/1.32 cnf(s150, plain, ~spl9_47, inference(rat,[],[s145,s32])).
% 7.14/1.32 cnf(s151, plain, ~spl9_31, inference(rat,[],[s140,s150,s32])).
% 7.14/1.32 cnf(s152, plain, ~spl9_38, inference(rat,[],[s82,s149,s32])).
% 7.14/1.32 cnf(s153, plain, ~spl9_32, inference(rat,[],[s84,s152,s32,s151])).
% 7.14/1.32 cnf(s154, plain, $false, inference(rat,[],[s66,s152,s32,s153,s151])).
% 7.14/1.32 thf(f4271,plain,(
% 7.14/1.32 $false),
% 7.14/1.32 inference(avatar_sat_refutation,[],[s154])).
% 7.14/1.32 % SZS output end Proof for theBenchmark
% 7.14/1.32 % (1584165)------------------------------
% 7.14/1.32 % (1584165)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.14/1.32 % (1584165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.14/1.32 % (1584165)CaDiCaL version: 2.1.3
% 7.14/1.32 % (1584165)Termination reason: Refutation
% 7.14/1.32 % (1584165)Time elapsed: 0.362 s
% 7.14/1.32 % (1584165)Peak memory usage: 15 MB
% 7.14/1.32 % (1584165)Instructions burned: 625 (million)
% 7.14/1.32 % (1584112)Success in time 1.082 s
% 7.14/1.32 % Vampire exiting
%------------------------------------------------------------------------------