%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ANA087^1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n002.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 6.31s 1.19s
% Output : Refutation 6.31s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ANA087^1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 % Computer : n002.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Tue Sep 29 17:43:23 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.22 Running first-order model finding
% 0.08/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.38/0.99 % (1625002)Will run a generic schedule for satisfiability detection.
% 4.38/0.99 % (1625011)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3050628743:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.38/0.99 % (1625011)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.38/0.99 % (1625008)% WARNING: option uhcvi not known.
% 4.38/0.99 % (1625007)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2658271453_2999 on theBenchmark for (2999ds/0Mi)
% 4.38/0.99 % (1625010)dis+10_1_sil=32000:sp=arity:random_seed=3175991609:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.38/0.99 % (1625009)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2000659111:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.38/0.99 % (1625012)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1710668059:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.38/0.99 % (1625008)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=592777029:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.38/0.99 % (1625013)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3339773695:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.38/0.99 % Exception at run slice level
% 4.38/0.99 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.38/0.99 % (1625008)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.38/0.99 % (1625008)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 4.38/0.99 % (1625021)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2438654389:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 4.38/0.99 % Exception at run slice level
% 4.38/0.99 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.38/0.99 % (1625011)Instruction limit reached!
% 4.38/0.99 % (1625011)------------------------------
% 4.38/0.99 % (1625011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.38/0.99 % (1625011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.38/0.99 % (1625011)CaDiCaL version: 2.1.3
% 4.38/0.99 % (1625011)Termination reason: Instruction limit
% 4.38/0.99 % (1625011)Termination phase: Saturation
% 4.38/0.99 % (1625011)Time elapsed: 0.033 s
% 4.38/0.99 % (1625011)Peak memory usage: 13 MB
% 4.38/0.99 % (1625011)Instructions burned: 117 (million)
% 4.38/0.99 % (1625024)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=1870857545:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 4.38/0.99 % (1625024)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.38/0.99 % (1625024)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 4.38/0.99 % (1625023)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=895113711:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 4.38/0.99 % (1625010)Instruction limit reached!
% 4.38/0.99 % (1625010)------------------------------
% 4.38/0.99 % (1625010)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.38/0.99 % (1625010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.38/0.99 % (1625010)CaDiCaL version: 2.1.3
% 4.38/0.99 % (1625010)Termination reason: Instruction limit
% 4.38/0.99 % (1625010)Termination phase: Saturation
% 4.38/0.99 % (1625010)Time elapsed: 0.052 s
% 4.38/0.99 % (1625010)Peak memory usage: 13 MB
% 4.38/0.99 % (1625010)Instructions burned: 104 (million)
% 4.38/0.99 % (1625012)Instruction limit reached!
% 4.38/0.99 % (1625012)------------------------------
% 4.38/0.99 % (1625012)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.38/0.99 % (1625012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.38/0.99 % (1625012)CaDiCaL version: 2.1.3
% 4.38/0.99 % (1625012)Termination reason: Instruction limit
% 4.38/0.99 % (1625012)Termination phase: Saturation
% 4.38/0.99 % (1625012)Time elapsed: 0.069 s
% 4.38/0.99 % (1625012)Peak memory usage: 12 MB
% 4.38/0.99 % (1625012)Instructions burned: 133 (million)
% 4.38/0.99 % (1625027)ott-21_1_sil=16000:fs=off:random_seed=2162487747:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 4.38/0.99 % (1625028)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3252902579:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 6.31/1.19 % (1625013)Instruction limit reached!
% 6.31/1.19 % (1625013)------------------------------
% 6.31/1.19 % (1625013)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.31/1.19 % (1625013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.19 % (1625013)CaDiCaL version: 2.1.3
% 6.31/1.19 % (1625013)Termination reason: Instruction limit
% 6.31/1.19 % (1625013)Termination phase: Saturation
% 6.31/1.19 % (1625013)Time elapsed: 0.090 s
% 6.31/1.19 % (1625013)Peak memory usage: 14 MB
% 6.31/1.19 % (1625013)Instructions burned: 160 (million)
% 6.31/1.19 % (1625031)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1616686071:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 6.31/1.19 % Exception at run slice level
% 6.31/1.19 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 6.31/1.19 % (1625023)Instruction limit reached!
% 6.31/1.19 % (1625023)------------------------------
% 6.31/1.19 % (1625023)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.31/1.19 % (1625023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.19 % (1625023)CaDiCaL version: 2.1.3
% 6.31/1.19 % (1625023)Termination reason: Instruction limit
% 6.31/1.19 % (1625023)Termination phase: Saturation
% 6.31/1.19 % (1625023)Time elapsed: 0.075 s
% 6.31/1.19 % (1625023)Peak memory usage: 12 MB
% 6.31/1.19 % (1625023)Instructions burned: 132 (million)
% 6.31/1.19 % (1625033)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1962590887:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 6.31/1.19 % (1625034)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1574286084:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 6.31/1.19 % Exception at run slice level
% 6.31/1.19 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 6.31/1.19 % (1625037)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=1948842815: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)
% 6.31/1.19 % (1625037)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 6.31/1.19 % (1625027)Instruction limit reached!
% 6.31/1.19 % (1625027)------------------------------
% 6.31/1.19 % (1625027)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.31/1.19 % (1625027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.19 % (1625027)CaDiCaL version: 2.1.3
% 6.31/1.19 % (1625027)Termination reason: Instruction limit
% 6.31/1.19 % (1625027)Termination phase: Saturation
% 6.31/1.19 % (1625027)Time elapsed: 0.085 s
% 6.31/1.19 % (1625027)Peak memory usage: 12 MB
% 6.31/1.19 % (1625027)Instructions burned: 180 (million)
% 6.31/1.19 % (1625039)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=410356069:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi)
% 6.31/1.19 % (1625039)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 6.31/1.19 % (1625024)Instruction limit reached!
% 6.31/1.19 % (1625024)------------------------------
% 6.31/1.19 % (1625024)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.31/1.19 % (1625024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.19 % (1625024)CaDiCaL version: 2.1.3
% 6.31/1.19 % (1625024)Termination reason: Instruction limit
% 6.31/1.19 % (1625024)Termination phase: Saturation
% 6.31/1.19 % (1625024)Time elapsed: 0.177 s
% 6.31/1.19 % (1625024)Peak memory usage: 15 MB
% 6.31/1.19 % (1625024)Instructions burned: 688 (million)
% 6.31/1.19 % (1625041)fmb+10_1_sil=64000:random_seed=2480283559:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi)
% 6.31/1.19 % (1625041)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 6.31/1.19 % Exception at run slice level
% 6.31/1.19 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 6.31/1.19 % (1625043)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=546472824:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi)
% 6.31/1.19 % Exception at run slice level
% 6.31/1.19 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 6.31/1.19 % (1625045)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4237042422:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi)
% 6.31/1.19 % Exception at run slice level
% 6.31/1.19 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 6.31/1.19 % (1625047)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4200997012:i=5131_2997 on theBenchmark for (2997ds/5131Mi)
% 6.31/1.19 % (1625047)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 6.31/1.19 % (1625028)Instruction limit reached!
% 6.31/1.19 % (1625028)------------------------------
% 6.31/1.19 % (1625028)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.31/1.19 % (1625028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.19 % (1625028)CaDiCaL version: 2.1.3
% 6.31/1.19 % (1625028)Termination reason: Instruction limit
% 6.31/1.19 % (1625028)Termination phase: Saturation
% 6.31/1.19 % (1625028)Time elapsed: 0.265 s
% 6.31/1.19 % (1625028)Peak memory usage: 14 MB
% 6.31/1.19 % (1625028)Instructions burned: 478 (million)
% 6.31/1.19 % (1625049)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2487814390:i=1472:ins=7:fdi=8:gsp=on_2996 on theBenchmark for (2996ds/1472Mi)
% 6.31/1.19 % (1625049)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 6.31/1.19 % (1625049)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 6.31/1.19 % (1625037)Instruction limit reached!
% 6.31/1.19 % (1625037)------------------------------
% 6.31/1.19 % (1625037)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.31/1.19 % (1625037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.19 % (1625037)CaDiCaL version: 2.1.3
% 6.31/1.19 % (1625037)Termination reason: Instruction limit
% 6.31/1.19 % (1625037)Termination phase: Saturation
% 6.31/1.19 % (1625037)Time elapsed: 0.362 s
% 6.31/1.19 % (1625037)Peak memory usage: 18 MB
% 6.31/1.19 % (1625037)Instructions burned: 693 (million)
% 6.31/1.19 % (1625051)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1423872535:i=6324_2994 on theBenchmark for (2994ds/6324Mi)
% 6.31/1.19 % Exception at run slice level
% 6.31/1.19 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 6.31/1.19 % (1625053)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3220314928:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi)
% 6.31/1.19 % Exception at run slice level
% 6.31/1.19 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 6.31/1.19 % (1625055)ott-2_1_sil=16000:newcnf=on:random_seed=165243962:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi)
% 6.31/1.19 % (1625055)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 6.31/1.19 % (1625039)Instruction limit reached!
% 6.31/1.19 % (1625039)------------------------------
% 6.31/1.19 % (1625039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.31/1.19 % (1625039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.19 % (1625039)CaDiCaL version: 2.1.3
% 6.31/1.19 % (1625039)Termination reason: Instruction limit
% 6.31/1.19 % (1625039)Termination phase: Saturation
% 6.31/1.19 % (1625039)Time elapsed: 0.441 s
% 6.31/1.19 % (1625039)Peak memory usage: 16 MB
% 6.31/1.19 % (1625039)Instructions burned: 879 (million)
% 6.31/1.19 % (1625057)ott+10_1_sil=32000:tgt=ground:random_seed=363150102:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi)
% 6.31/1.19 % (1625033)Instruction limit reached!
% 6.31/1.19 % (1625033)------------------------------
% 6.31/1.19 % (1625033)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.31/1.19 % (1625033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.19 % (1625033)CaDiCaL version: 2.1.3
% 6.31/1.19 % (1625033)Termination reason: Instruction limit
% 6.31/1.19 % (1625033)Termination phase: Saturation
% 6.31/1.19 % (1625033)Time elapsed: 0.563 s
% 6.31/1.19 % (1625033)Peak memory usage: 16 MB
% 6.31/1.19 % (1625033)Instructions burned: 1181 (million)
% 6.31/1.19 % (1625059)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3508758411:i=54282_2992 on theBenchmark for (2992ds/54282Mi)
% 6.31/1.19 % Exception at run slice level
% 6.31/1.19 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 6.31/1.19 % (1625061)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1519734615:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi)
% 6.31/1.19 % (1625061)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 6.31/1.19 % (1625055) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1625002-1625055"...
% 6.31/1.19 % (1625055)...printing done.
% 6.31/1.19 % (1625055)Refutation found. Thanks to Tanya!
% 6.31/1.19 % SZS status Theorem for theBenchmark
% 6.31/1.19 % SZS output start Proof for theBenchmark
% 6.31/1.19 thf(type_def_5, type, 'type/realax/real': $tType).
% 6.31/1.19 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 6.31/1.19 thf(func_def_0, type, 'const/trivia/I': !>[X0: $tType]:((X0 > X0))).
% 6.31/1.19 thf(func_def_1, type, 'const/sets/SUBSET': !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > $o))).
% 6.31/1.19 thf(func_def_2, type, 'const/sets/inf': (('type/realax/real' > $o) > 'type/realax/real')).
% 6.31/1.19 thf(func_def_3, type, 'const/sets/IN': !>[X0: $tType]:((X0 > (X0 > $o) > $o))).
% 6.31/1.19 thf(func_def_4, type, 'const/sets/EMPTY': !>[X0: $tType]:((X0 > $o))).
% 6.31/1.19 thf(func_def_5, type, 'const/realax/real_le': ('type/realax/real' > 'type/realax/real' > $o)).
% 6.31/1.19 thf(func_def_9, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 6.31/1.19 thf(func_def_10, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 6.31/1.19 thf(func_def_11, type, db0: !>[X0: $tType]:(X0)).
% 6.31/1.19 thf(func_def_12, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 6.31/1.19 thf(func_def_13, type, vIMP: ($o > $o > $o)).
% 6.31/1.19 thf(func_def_14, type, sK0: ('type/realax/real' > ('type/realax/real' > $o) > 'type/realax/real')).
% 6.31/1.19 thf(func_def_15, type, sK1: ('type/realax/real' > ('type/realax/real' > $o) > 'type/realax/real')).
% 6.31/1.19 thf(func_def_16, type, sK2: ('type/realax/real' > ('type/realax/real' > $o) > 'type/realax/real')).
% 6.31/1.19 thf(func_def_17, type, sK3: ('type/realax/real' > $o)).
% 6.31/1.19 thf(func_def_18, type, sK4: ('type/realax/real' > $o)).
% 6.31/1.19 thf(func_def_19, type, sK5: 'type/realax/real').
% 6.31/1.19 thf(func_def_20, type, vNOT: ($o > $o)).
% 6.31/1.19 thf(func_def_21, type, sK6: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0))).
% 6.31/1.19 thf(func_def_22, type, sK7: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0))).
% 6.31/1.19 thf(func_def_23, type, sK8: 'type/realax/real').
% 6.31/1.19 thf(func_def_25, type, db1: !>[X0: $tType]:(X0)).
% 6.31/1.19 thf(func_def_26, type, sK10: 'type/realax/real').
% 6.31/1.19 thf(func_def_27, type, sK11: 'type/realax/real').
% 6.31/1.19 thf(func_def_28, type, sK12: 'type/realax/real').
% 6.31/1.19 thf(f1,axiom,(
% 6.31/1.19 ! [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')) => ('const/realax/real_le' @ X1 @ ('const/sets/inf' @ X0)))),
% 6.31/1.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p','thm/sets/REAL_LE_INF_')).
% 6.31/1.19 thf(f3,axiom,(
% 6.31/1.19 ! [X0 : $tType,X1 : (X0 > $o),X2 : X0] : ((('const/sets/IN' @ X0 @ X2 @ X1)) = ((X1 @ X2)))),
% 6.31/1.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p','thm/sets/IN_')).
% 6.31/1.19 thf(f4,axiom,(
% 6.31/1.19 ! [X0 : $tType,X1 : X0] : ~('const/sets/IN' @ X0 @ X1 @ 'const/sets/EMPTY' @ X0)),
% 6.31/1.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p','thm/sets/NOT_IN_EMPTY_')).
% 6.31/1.19 thf(f6,axiom,(
% 6.31/1.19 ! [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)))),
% 6.31/1.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p','thm/sets/SUBSET_')).
% 6.31/1.19 thf(f7,axiom,(
% 6.31/1.19 ! [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))))),
% 6.31/1.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p','thm/sets/INF_')).
% 6.31/1.19 thf(f8,conjecture,(
% 6.31/1.19 ! [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 @ X0) => ('const/realax/real_le' @ X2 @ X3)) & ('const/sets/SUBSET' @ 'type/realax/real' @ X1 @ X0) & (X1 != 'const/sets/EMPTY' @ 'type/realax/real')) => ('const/realax/real_le' @ ('const/sets/inf' @ X0) @ ('const/sets/inf' @ X1)))),
% 6.31/1.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p','thm/sets/REAL_LE_INF_SUBSET_')).
% 6.31/1.19 thf(f9,negated_conjecture,(
% 6.31/1.19 ~ ! [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 @ X0) => ('const/realax/real_le' @ X2 @ X3)) & ('const/sets/SUBSET' @ 'type/realax/real' @ X1 @ X0) & (X1 != 'const/sets/EMPTY' @ 'type/realax/real')) => ('const/realax/real_le' @ ('const/sets/inf' @ X0) @ ('const/sets/inf' @ X1)))),
% 6.31/1.19 inference(negated_conjecture,[status(cth)],[f8])).
% 6.31/1.19 thf(f10,plain,(
% 6.31/1.19 ! [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')) => ('const/realax/real_le' @ X1 @ ('const/sets/inf' @ X0)))),
% 6.31/1.19 inference(rectify,[],[f1])).
% 6.31/1.19 thf(f11,plain,(
% 6.31/1.19 ! [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)) => ((('const/realax/real_le' @ X1 @ ('const/sets/inf' @ X0))) = $true))),
% 6.31/1.19 inference(fool_elimination,[],[f10])).
% 6.31/1.19 thf(f12,plain,(
% 6.31/1.19 ! [X0 : $tType,X1 : X0] : ~('const/sets/IN' @ X0 @ X1 @ 'const/sets/EMPTY' @ X0)),
% 6.31/1.19 inference(rectify,[],[f4])).
% 6.31/1.19 thf(f13,plain,(
% 6.31/1.19 ! [X0 : $tType,X1 : X0] : ~ ((('const/sets/IN' @ X0 @ X1 @ 'const/sets/EMPTY' @ X0)) = $true)),
% 6.31/1.19 inference(fool_elimination,[],[f12])).
% 6.31/1.19 thf(f15,plain,(
% 6.31/1.19 ! [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)))),
% 6.31/1.19 inference(rectify,[],[f6])).
% 6.31/1.19 thf(f16,plain,(
% 6.31/1.19 ! [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))))))),
% 6.31/1.19 inference(fool_elimination,[],[f15])).
% 6.31/1.19 thf(f17,plain,(
% 6.31/1.19 ! [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))))),
% 6.31/1.19 inference(rectify,[],[f7])).
% 6.31/1.19 thf(f18,plain,(
% 6.31/1.19 ! [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))))))),
% 6.31/1.19 inference(fool_elimination,[],[f17])).
% 6.31/1.19 thf(f19,plain,(
% 6.31/1.19 ~ ! [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 @ X0) => ('const/realax/real_le' @ X2 @ X3)) & ('const/sets/SUBSET' @ 'type/realax/real' @ X1 @ X0) & (X1 != 'const/sets/EMPTY' @ 'type/realax/real')) => ('const/realax/real_le' @ ('const/sets/inf' @ X0) @ ('const/sets/inf' @ X1)))),
% 6.31/1.19 inference(rectify,[],[f9])).
% 6.31/1.19 thf(f20,plain,(
% 6.31/1.19 ~ ! [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 @ X0)) = $true) => ((('const/realax/real_le' @ X2 @ X3)) = $true)) & ((('const/sets/SUBSET' @ 'type/realax/real' @ X1 @ X0)) = $true) & ('const/sets/EMPTY' @ 'type/realax/real' != X1)) => ((('const/realax/real_le' @ ('const/sets/inf' @ X0) @ ('const/sets/inf' @ X1))) = $true))),
% 6.31/1.19 inference(fool_elimination,[],[f19])).
% 6.31/1.19 thf(f21,plain,(
% 6.31/1.19 ! [X0 : $tType,X1 : X0] : ((('const/sets/IN' @ X0 @ X1 @ 'const/sets/EMPTY' @ X0)) != $true)),
% 6.31/1.19 inference(flattening,[],[f13])).
% 6.31/1.19 thf(f22,plain,(
% 6.31/1.19 ! [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)) | ('const/sets/EMPTY' @ 'type/realax/real' = X0)))),
% 6.31/1.19 inference(ennf_transformation,[],[f11])).
% 6.31/1.19 thf(f23,plain,(
% 6.31/1.19 ! [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)) | ('const/sets/EMPTY' @ 'type/realax/real' = X0))),
% 6.31/1.19 inference(flattening,[],[f22])).
% 6.31/1.19 thf(f24,plain,(
% 6.31/1.19 ! [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)))),
% 6.31/1.19 inference(ennf_transformation,[],[f18])).
% 6.31/1.19 thf(f25,plain,(
% 6.31/1.19 ! [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))),
% 6.31/1.19 inference(flattening,[],[f24])).
% 6.31/1.19 thf(f26,plain,(
% 6.31/1.19 ? [X0 : ('type/realax/real' > $o),X1 : ('type/realax/real' > $o)] : (((('const/realax/real_le' @ ('const/sets/inf' @ X0) @ ('const/sets/inf' @ X1))) != $true) & (? [X2 : 'type/realax/real'] : ! [X3 : 'type/realax/real'] : (((('const/realax/real_le' @ X2 @ X3)) = $true) | ((('const/sets/IN' @ 'type/realax/real' @ X3 @ X0)) != $true)) & ((('const/sets/SUBSET' @ 'type/realax/real' @ X1 @ X0)) = $true) & ('const/sets/EMPTY' @ 'type/realax/real' != X1)))),
% 6.31/1.19 inference(ennf_transformation,[],[f20])).
% 6.31/1.19 thf(f27,plain,(
% 6.31/1.19 ? [X0 : ('type/realax/real' > $o),X1 : ('type/realax/real' > $o)] : (((('const/realax/real_le' @ ('const/sets/inf' @ X0) @ ('const/sets/inf' @ X1))) != $true) & ? [X2 : 'type/realax/real'] : ! [X3 : 'type/realax/real'] : (((('const/realax/real_le' @ X2 @ X3)) = $true) | ((('const/sets/IN' @ 'type/realax/real' @ X3 @ X0)) != $true)) & ((('const/sets/SUBSET' @ 'type/realax/real' @ X1 @ X0)) = $true) & ('const/sets/EMPTY' @ 'type/realax/real' != X1))),
% 6.31/1.19 inference(flattening,[],[f26])).
% 6.31/1.19 thf(f28,plain,(
% 6.31/1.19 ! [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)))) | ('const/sets/EMPTY' @ 'type/realax/real' = X0))),
% 6.31/1.19 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP]),skolemize(X2,sK0 @ X1 @ X0)],[f23])).
% 6.31/1.19 thf(f29,plain,(
% 6.31/1.19 ! [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))) | ((('const/sets/IN' @ 'type/realax/real' @ X3 @ X0)) != $true))) | ! [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))),
% 6.31/1.19 inference(rectify,[],[f25])).
% 6.31/1.19 thf(f30,plain,(
% 6.31/1.19 ! [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 @ (sK1 @ X1 @ X0)))) & ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK1 @ X1 @ X0) @ X0))))) & ! [X3 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ ('const/sets/inf' @ X0) @ X3))) | ((('const/sets/IN' @ 'type/realax/real' @ X3 @ X0)) != $true))) | ! [X4 : 'type/realax/real'] : (($true != (('const/realax/real_le' @ X4 @ (sK2 @ X4 @ X0)))) & ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK2 @ X4 @ X0) @ X0)))) | ('const/sets/EMPTY' @ 'type/realax/real' = X0))),
% 6.31/1.19 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP,vAPP]),skolemize(X2,sK0 @ X1 @ X0),skolemize(X2,sK0 @ X1 @ X0)],[f29])).
% 6.31/1.19 thf(f31,plain,(
% 6.31/1.19 ($true != (('const/realax/real_le' @ ('const/sets/inf' @ sK3) @ ('const/sets/inf' @ sK4)))) & ! [X3 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ sK5 @ X3))) | ($true != (('const/sets/IN' @ 'type/realax/real' @ X3 @ sK3)))) & ($true = (('const/sets/SUBSET' @ 'type/realax/real' @ sK4 @ sK3))) & ('const/sets/EMPTY' @ 'type/realax/real' != sK4)),
% 6.31/1.19 inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4,sK5]),skolemize(X0,sK3),skolemize(X1,sK4),skolemize(X2,sK5)],[f27])).
% 6.31/1.19 thf(f32,plain,(
% 6.31/1.19 ( ! [X0 : ('type/realax/real' > $o),X1 : 'type/realax/real'] : (($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)) )),
% 6.31/1.19 inference(cnf_transformation,[],[f28])).
% 6.31/1.19 thf(f35,plain,(
% 6.31/1.19 ( ! [X0 : $tType,X2 : X0,X1 : (X0 > $o)] : (((('const/sets/IN' @ X0 @ X2 @ X1)) = ((X1 @ X2)))) )),
% 6.31/1.19 inference(cnf_transformation,[],[f3])).
% 6.31/1.19 thf(f36,plain,(
% 6.31/1.19 ( ! [X0 : $tType,X1 : X0] : (((('const/sets/IN' @ X0 @ X1 @ 'const/sets/EMPTY' @ X0)) != $true)) )),
% 6.31/1.19 inference(cnf_transformation,[],[f21])).
% 6.31/1.19 thf(f38,plain,(
% 6.31/1.19 ( ! [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))))))) )),
% 6.31/1.19 inference(cnf_transformation,[],[f16])).
% 6.31/1.19 thf(f39,plain,(
% 6.31/1.19 ( ! [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' @ ('const/sets/inf' @ X0) @ X3))) | ((('const/sets/IN' @ 'type/realax/real' @ X3 @ X0)) != $true) | ('const/sets/EMPTY' @ 'type/realax/real' = X0)) )),
% 6.31/1.19 inference(cnf_transformation,[],[f30])).
% 6.31/1.19 thf(f40,plain,(
% 6.31/1.19 ( ! [X3 : 'type/realax/real',X0 : ('type/realax/real' > $o),X4 : 'type/realax/real'] : (($true != (('const/realax/real_le' @ X4 @ (sK2 @ X4 @ X0)))) | ((('const/sets/IN' @ 'type/realax/real' @ X3 @ X0)) != $true) | ($true = (('const/realax/real_le' @ ('const/sets/inf' @ X0) @ X3))) | ('const/sets/EMPTY' @ 'type/realax/real' = X0)) )),
% 6.31/1.19 inference(cnf_transformation,[],[f30])).
% 6.31/1.19 thf(f41,plain,(
% 6.31/1.19 ( ! [X0 : ('type/realax/real' > $o),X1 : 'type/realax/real',X4 : 'type/realax/real'] : (($true = (('const/sets/IN' @ 'type/realax/real' @ (sK2 @ X4 @ X0) @ X0))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK1 @ X1 @ X0) @ X0))) | ((('const/realax/real_le' @ X1 @ ('const/sets/inf' @ X0))) = $true) | ('const/sets/EMPTY' @ 'type/realax/real' = X0)) )),
% 6.31/1.19 inference(cnf_transformation,[],[f30])).
% 6.31/1.19 thf(f42,plain,(
% 6.31/1.19 ( ! [X0 : ('type/realax/real' > $o),X1 : 'type/realax/real',X4 : 'type/realax/real'] : (($true != (('const/realax/real_le' @ X4 @ (sK2 @ X4 @ X0)))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK1 @ X1 @ X0) @ X0))) | ((('const/realax/real_le' @ X1 @ ('const/sets/inf' @ X0))) = $true) | ('const/sets/EMPTY' @ 'type/realax/real' = X0)) )),
% 6.31/1.19 inference(cnf_transformation,[],[f30])).
% 6.31/1.19 thf(f43,plain,(
% 6.31/1.19 ( ! [X0 : ('type/realax/real' > $o),X1 : 'type/realax/real',X4 : 'type/realax/real'] : (($true != (('const/realax/real_le' @ X1 @ (sK1 @ X1 @ X0)))) | ((('const/realax/real_le' @ X1 @ ('const/sets/inf' @ X0))) = $true) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK2 @ X4 @ X0) @ X0))) | ('const/sets/EMPTY' @ 'type/realax/real' = X0)) )),
% 6.31/1.19 inference(cnf_transformation,[],[f30])).
% 6.31/1.19 thf(f44,plain,(
% 6.31/1.19 ( ! [X0 : ('type/realax/real' > $o),X1 : 'type/realax/real',X4 : 'type/realax/real'] : (($true != (('const/realax/real_le' @ X4 @ (sK2 @ X4 @ X0)))) | ($true != (('const/realax/real_le' @ X1 @ (sK1 @ X1 @ X0)))) | ((('const/realax/real_le' @ X1 @ ('const/sets/inf' @ X0))) = $true) | ('const/sets/EMPTY' @ 'type/realax/real' = X0)) )),
% 6.31/1.19 inference(cnf_transformation,[],[f30])).
% 6.31/1.19 thf(f45,plain,(
% 6.31/1.19 ('const/sets/EMPTY' @ 'type/realax/real' != sK4)),
% 6.31/1.19 inference(cnf_transformation,[],[f31])).
% 6.31/1.19 thf(f46,plain,(
% 6.31/1.19 ($true = (('const/sets/SUBSET' @ 'type/realax/real' @ sK4 @ sK3)))),
% 6.31/1.19 inference(cnf_transformation,[],[f31])).
% 6.31/1.19 thf(f47,plain,(
% 6.31/1.19 ( ! [X3 : 'type/realax/real'] : (($true != (('const/sets/IN' @ 'type/realax/real' @ X3 @ sK3))) | ($true = (('const/realax/real_le' @ sK5 @ X3)))) )),
% 6.31/1.19 inference(cnf_transformation,[],[f31])).
% 6.31/1.19 thf(f48,plain,(
% 6.31/1.19 ($true != (('const/realax/real_le' @ ('const/sets/inf' @ sK3) @ ('const/sets/inf' @ sK4))))),
% 6.31/1.19 inference(cnf_transformation,[],[f31])).
% 6.31/1.19 thf(f50,definition,(
% 6.31/1.19 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 6.31/1.19 introduced(theory,[fool_exhaustiveness_axiom])).
% 6.31/1.19 thf(f52,plain,(
% 6.31/1.19 ( ! [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))))))) )),
% 6.31/1.19 inference(iff_proxy_clausification,[],[f38])).
% 6.31/1.19 thf(f53,plain,(
% 6.31/1.19 ( ! [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)))) )),
% 6.31/1.19 inference(pi_proxy_clausification,[],[f52])).
% 6.31/1.19 thf(f54,plain,(
% 6.31/1.19 ( ! [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))))) )),
% 6.31/1.19 inference(beta-eta_normalization,[],[f53])).
% 6.31/1.19 thf(f55,plain,(
% 6.31/1.19 ( ! [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)) )),
% 6.31/1.19 inference(imp_proxy_clausification,[],[f54])).
% 6.31/1.19 thf(f74,plain,(
% 6.31/1.19 ( ! [X0 : $tType,X2 : X0,X1 : (X0 > $o)] : (((('const/sets/IN' @ X0 @ X2 @ X1)) = $true) | (((X1 @ X2)) = $false)) )),
% 6.31/1.19 inference(iff_proxy_clausification,[],[f35])).
% 6.31/1.19 thf(f75,plain,(
% 6.31/1.19 ( ! [X0 : $tType,X2 : X0,X1 : (X0 > $o)] : (((('const/sets/IN' @ X0 @ X2 @ X1)) = $false) | (((X1 @ X2)) = $true)) )),
% 6.31/1.19 inference(iff_proxy_clausification,[],[f35])).
% 6.31/1.19 thf(f100,plain,(
% 6.31/1.19 ($true != $true) | ((('const/realax/real_le' @ ('const/sets/inf' @ sK3) @ ('const/sets/inf' @ sK4))) = $false)),
% 6.31/1.19 inference(constrained_superposition,[],[f48,f50])).
% 6.31/1.19 thf(f101,plain,(
% 6.31/1.19 ( ! [X0 : 'type/realax/real'] : (($true != $true) | ($true = (('const/realax/real_le' @ sK5 @ X0))) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK3)))) )),
% 6.31/1.19 inference(constrained_superposition,[],[f47,f50])).
% 6.31/1.19 thf(f103,plain,(
% 6.31/1.19 ( ! [X0 : 'type/realax/real'] : (($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK3))) | ($true = (('const/realax/real_le' @ sK5 @ X0)))) )),
% 6.31/1.19 inference(trivial_inequality_removal,[],[f101])).
% 6.31/1.19 thf(f104,plain,(
% 6.31/1.19 ((('const/realax/real_le' @ ('const/sets/inf' @ sK3) @ ('const/sets/inf' @ sK4))) = $false)),
% 6.31/1.19 inference(trivial_inequality_removal,[],[f100])).
% 6.31/1.19 thf(f137,definition,(
% 6.31/1.19 spl9_5 <=> ('const/sets/EMPTY' @ 'type/realax/real' = sK3)),
% 6.31/1.19 introduced(definition,[new_symbols(definition,[spl9_5])],[avatar_definition])).
% 6.31/1.19 thf(f138,plain,(
% 6.31/1.19 ('const/sets/EMPTY' @ 'type/realax/real' != sK3) | spl9_5),
% 6.31/1.19 inference(avatar_component_clause,[],[f137])).
% 6.31/1.19 thf(f139,plain,(
% 6.31/1.19 ('const/sets/EMPTY' @ 'type/realax/real' = sK3) | ~spl9_5),
% 6.31/1.19 inference(avatar_component_clause,[],[f137])).
% 6.31/1.19 thf(f151,plain,(
% 6.31/1.19 ($true = (('const/sets/SUBSET' @ 'type/realax/real' @ sK4 @ 'const/sets/EMPTY' @ 'type/realax/real'))) | ~spl9_5),
% 6.31/1.19 inference(constrained_superposition,[],[f46,f139])).
% 6.31/1.19 thf(f157,plain,(
% 6.31/1.19 ( ! [X0 : $tType,X1 : X0] : (($true != $true) | ($false = (('const/sets/EMPTY' @ X0 @ X1)))) )),
% 6.31/1.19 inference(constrained_superposition,[],[f36,f74])).
% 6.31/1.19 thf(f159,plain,(
% 6.31/1.19 ( ! [X0 : 'type/realax/real'] : (($true != $true) | ($true = (('const/realax/real_le' @ sK5 @ X0))) | ($false = ((sK3 @ X0)))) )),
% 6.31/1.19 inference(constrained_superposition,[],[f47,f74])).
% 6.31/1.19 thf(f164,plain,(
% 6.31/1.19 ( ! [X0 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ sK5 @ X0))) | ($false = ((sK3 @ X0)))) )),
% 6.31/1.19 inference(trivial_inequality_removal,[],[f159])).
% 6.31/1.19 thf(f166,plain,(
% 6.31/1.19 ( ! [X0 : $tType,X1 : X0] : (($false = (('const/sets/EMPTY' @ X0 @ X1)))) )),
% 6.31/1.19 inference(trivial_inequality_removal,[],[f157])).
% 6.31/1.19 thf(f187,plain,(
% 6.31/1.19 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : (($true = $false) | ($true = (('const/realax/real_le' @ ('const/sets/inf' @ sK3) @ X1))) | ($true != (('const/sets/IN' @ 'type/realax/real' @ X1 @ sK3))) | ('const/sets/EMPTY' @ 'type/realax/real' = sK3) | ($true = (('const/realax/real_le' @ sK5 @ (sK2 @ X0 @ sK3))))) )),
% 6.31/1.19 inference(constrained_superposition,[],[f39,f103])).
% 6.31/1.19 thf(f202,plain,(
% 6.31/1.19 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ ('const/sets/inf' @ sK3) @ X1))) | ($true != (('const/sets/IN' @ 'type/realax/real' @ X1 @ sK3))) | ('const/sets/EMPTY' @ 'type/realax/real' = sK3) | ($true = (('const/realax/real_le' @ sK5 @ (sK2 @ X0 @ sK3))))) )),
% 6.31/1.19 inference(trivial_inequality_removal,[],[f187])).
% 6.31/1.19 thf(f211,plain,(
% 6.31/1.19 ( ! [X2 : 'type/realax/real',X0 : 'type/realax/real',X1 : ('type/realax/real' > $o)] : (($true != $true) | ($true != (('const/realax/real_le' @ X2 @ (sK1 @ 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 @ (sK2 @ X0 @ X1))))) )),
% 6.31/1.19 inference(constrained_superposition,[],[f44,f50])).
% 6.31/1.19 thf(f212,plain,(
% 6.31/1.19 ( ! [X2 : 'type/realax/real',X0 : 'type/realax/real',X1 : ('type/realax/real' > $o)] : (($true != (('const/realax/real_le' @ X2 @ (sK1 @ 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 @ (sK2 @ X0 @ X1))))) )),
% 6.31/1.19 inference(trivial_inequality_removal,[],[f211])).
% 6.31/1.19 thf(f569,definition,(
% 6.31/1.19 spl9_12 <=> ('const/sets/EMPTY' @ 'type/realax/real' = (^[Y0 : 'type/realax/real']: ($false)))),
% 6.31/1.19 introduced(definition,[new_symbols(definition,[spl9_12])],[avatar_definition])).
% 6.31/1.19 thf(f570,plain,(
% 6.31/1.19 ('const/sets/EMPTY' @ 'type/realax/real' != (^[Y0 : 'type/realax/real']: ($false))) | spl9_12),
% 6.31/1.19 inference(avatar_component_clause,[],[f569])).
% 6.31/1.19 thf(f571,plain,(
% 6.31/1.19 ('const/sets/EMPTY' @ 'type/realax/real' = (^[Y0 : 'type/realax/real']: ($false))) | ~spl9_12),
% 6.31/1.19 inference(avatar_component_clause,[],[f569])).
% 6.31/1.19 thf(f1176,plain,(
% 6.31/1.19 ((('const/sets/EMPTY' @ 'type/realax/real' @ sK10)) != (((^[Y0 : 'type/realax/real']: ($false)) @ sK10))) | spl9_12),
% 6.31/1.19 inference(negative_extensionality,[],[f570])).
% 6.31/1.19 thf(f1177,plain,(
% 6.31/1.19 ($true = (('const/sets/EMPTY' @ 'type/realax/real' @ sK10))) | ($true = (((^[Y0 : 'type/realax/real']: ($false)) @ sK10))) | spl9_12),
% 6.31/1.19 inference(xor_proxy_clausification,[],[f1176])).
% 6.31/1.19 thf(f1180,plain,(
% 6.31/1.19 ($true = (('const/sets/EMPTY' @ 'type/realax/real' @ sK10))) | ($true = $false) | spl9_12),
% 6.31/1.19 inference(beta-eta_normalization,[],[f1177])).
% 6.31/1.19 thf(f1181,plain,(
% 6.31/1.19 ($true = (('const/sets/EMPTY' @ 'type/realax/real' @ sK10))) | spl9_12),
% 6.31/1.19 inference(trivial_inequality_removal,[],[f1180])).
% 6.31/1.19 thf(f1182,plain,(
% 6.31/1.19 ($true = $false) | spl9_12),
% 6.31/1.19 inference(forward_demodulation,[],[f1181,f166])).
% 6.31/1.19 thf(f1183,plain,(
% 6.31/1.19 $false | spl9_12),
% 6.31/1.19 inference(trivial_inequality_removal,[],[f1182])).
% 6.31/1.19 thf(f1184,plain,(
% 6.31/1.19 spl9_12),
% 6.31/1.19 inference(avatar_contradiction_clause,[],[f1183])).
% 6.31/1.19 thf(f1215,plain,(
% 6.31/1.19 ( ! [X0 : 'type/realax/real'] : (($true = $false) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK4))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ X0 @ 'const/sets/EMPTY' @ 'type/realax/real')))) ) | ~spl9_5),
% 6.31/1.19 inference(constrained_superposition,[],[f151,f55])).
% 6.31/1.19 thf(f1216,plain,(
% 6.31/1.19 ( ! [X0 : 'type/realax/real'] : (($true = $false) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK4))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK3)))) )),
% 6.31/1.19 inference(constrained_superposition,[],[f46,f55])).
% 6.31/1.19 thf(f1244,plain,(
% 6.31/1.19 ( ! [X0 : 'type/realax/real'] : (($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK4))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK3)))) )),
% 6.31/1.19 inference(trivial_inequality_removal,[],[f1216])).
% 6.31/1.19 thf(f1245,plain,(
% 6.31/1.19 ( ! [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')))) ) | ~spl9_5),
% 6.31/1.19 inference(trivial_inequality_removal,[],[f1215])).
% 6.31/1.19 thf(f1273,plain,(
% 6.31/1.19 ( ! [X0 : 'type/realax/real'] : (($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK4)))) ) | ~spl9_5),
% 6.31/1.19 inference(forward_subsumption_resolution,[],[f1245,f36])).
% 6.31/1.19 thf(f1331,plain,(
% 6.31/1.19 ( ! [X0 : 'type/realax/real'] : (($true = $false) | ($true = (('const/realax/real_le' @ X0 @ ('const/sets/inf' @ sK4)))) | ('const/sets/EMPTY' @ 'type/realax/real' = sK4)) ) | ~spl9_5),
% 6.31/1.19 inference(constrained_superposition,[],[f32,f1273])).
% 6.31/1.19 thf(f1346,plain,(
% 6.31/1.19 ( ! [X0 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ X0 @ ('const/sets/inf' @ sK4)))) | ('const/sets/EMPTY' @ 'type/realax/real' = sK4)) ) | ~spl9_5),
% 6.31/1.19 inference(trivial_inequality_removal,[],[f1331])).
% 6.31/1.19 thf(f1364,plain,(
% 6.31/1.19 ( ! [X0 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ X0 @ ('const/sets/inf' @ sK4))))) ) | ~spl9_5),
% 6.31/1.19 inference(forward_subsumption_resolution,[],[f1346,f45])).
% 6.31/1.19 thf(f1375,definition,(
% 6.31/1.19 spl9_27 <=> ! [X0 : 'type/realax/real'] : ($true = (('const/realax/real_le' @ X0 @ ('const/sets/inf' @ sK4))))),
% 6.31/1.19 introduced(definition,[new_symbols(definition,[spl9_27])],[avatar_definition])).
% 6.31/1.19 thf(f1376,plain,(
% 6.31/1.19 ( ! [X0 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ X0 @ ('const/sets/inf' @ sK4))))) ) | ~spl9_27),
% 6.31/1.19 inference(avatar_component_clause,[],[f1375])).
% 6.31/1.19 thf(f1385,plain,(
% 6.31/1.19 spl9_27 | ~spl9_5),
% 6.31/1.19 inference(avatar_split_clause,[],[f1364,f137,f1375])).
% 6.31/1.19 thf(f1392,plain,(
% 6.31/1.19 (sK3 != (^[Y0 : 'type/realax/real']: ($false))) | (spl9_5 | ~spl9_12)),
% 6.31/1.19 inference(forward_demodulation,[],[f138,f571])).
% 6.31/1.19 thf(f1398,plain,(
% 6.31/1.19 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : ((sK3 = (^[Y0 : 'type/realax/real']: ($false))) | ($true = (('const/realax/real_le' @ ('const/sets/inf' @ sK3) @ X1))) | ($true != (('const/sets/IN' @ 'type/realax/real' @ X1 @ sK3))) | ($true = (('const/realax/real_le' @ sK5 @ (sK2 @ X0 @ sK3))))) ) | ~spl9_12),
% 6.31/1.19 inference(forward_demodulation,[],[f202,f571])).
% 6.31/1.19 thf(f1446,definition,(
% 6.31/1.19 spl9_31 <=> ! [X1 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ ('const/sets/inf' @ sK3) @ X1))) | ($true != (('const/sets/IN' @ 'type/realax/real' @ X1 @ sK3))))),
% 6.31/1.19 introduced(definition,[new_symbols(definition,[spl9_31])],[avatar_definition])).
% 6.31/1.19 thf(f1447,plain,(
% 6.31/1.19 ( ! [X1 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ ('const/sets/inf' @ sK3) @ X1))) | ($true != (('const/sets/IN' @ 'type/realax/real' @ X1 @ sK3)))) ) | ~spl9_31),
% 6.31/1.19 inference(avatar_component_clause,[],[f1446])).
% 6.31/1.19 thf(f1449,definition,(
% 6.31/1.19 spl9_32 <=> ! [X0 : 'type/realax/real'] : ($true = (('const/realax/real_le' @ sK5 @ (sK2 @ X0 @ sK3))))),
% 6.31/1.19 introduced(definition,[new_symbols(definition,[spl9_32])],[avatar_definition])).
% 6.31/1.19 thf(f1450,plain,(
% 6.31/1.19 ( ! [X0 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ sK5 @ (sK2 @ X0 @ sK3))))) ) | ~spl9_32),
% 6.31/1.19 inference(avatar_component_clause,[],[f1449])).
% 6.31/1.19 thf(f1489,definition,(
% 6.31/1.19 spl9_38 <=> (sK3 = (^[Y0 : 'type/realax/real']: ($false)))),
% 6.31/1.19 introduced(definition,[new_symbols(definition,[spl9_38])],[avatar_definition])).
% 6.31/1.19 thf(f1490,plain,(
% 6.31/1.19 (sK3 != (^[Y0 : 'type/realax/real']: ($false))) | spl9_38),
% 6.31/1.19 inference(avatar_component_clause,[],[f1489])).
% 6.31/1.19 thf(f1497,plain,(
% 6.31/1.19 spl9_32 | spl9_31 | spl9_38 | ~spl9_12),
% 6.31/1.19 inference(avatar_split_clause,[],[f1398,f569,f1489,f1446,f1449])).
% 6.31/1.19 thf(f1515,plain,(
% 6.31/1.19 ~spl9_38 | spl9_5 | ~spl9_12),
% 6.31/1.19 inference(avatar_split_clause,[],[f1392,f569,f137,f1489])).
% 6.31/1.19 thf(f1524,plain,(
% 6.31/1.19 ( ! [X0 : 'type/realax/real'] : (($true != $true) | ($true != (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK3))) | ($true = (('const/realax/real_le' @ ('const/sets/inf' @ sK3) @ X0))) | ('const/sets/EMPTY' @ 'type/realax/real' = sK3)) ) | ~spl9_32),
% 6.31/1.19 inference(constrained_superposition,[],[f40,f1450])).
% 6.31/1.19 thf(f1525,plain,(
% 6.31/1.19 ( ! [X0 : 'type/realax/real'] : (($true != (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK3))) | ($true = (('const/realax/real_le' @ ('const/sets/inf' @ sK3) @ X0))) | ('const/sets/EMPTY' @ 'type/realax/real' = sK3)) ) | ~spl9_32),
% 6.31/1.20 inference(trivial_inequality_removal,[],[f1524])).
% 6.31/1.20 thf(f1528,plain,(
% 6.31/1.20 ( ! [X0 : 'type/realax/real'] : ((sK3 = (^[Y0 : 'type/realax/real']: ($false))) | ($true != (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK3))) | ($true = (('const/realax/real_le' @ ('const/sets/inf' @ sK3) @ X0)))) ) | (~spl9_12 | ~spl9_32)),
% 6.31/1.20 inference(forward_demodulation,[],[f1525,f571])).
% 6.31/1.20 thf(f1531,plain,(
% 6.31/1.20 ( ! [X0 : 'type/realax/real'] : (($true != (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK3))) | ($true = (('const/realax/real_le' @ ('const/sets/inf' @ sK3) @ X0)))) ) | (~spl9_12 | ~spl9_32 | spl9_38)),
% 6.31/1.20 inference(forward_subsumption_resolution,[],[f1528,f1490])).
% 6.31/1.20 thf(f1534,plain,(
% 6.31/1.20 spl9_31 | ~spl9_12 | ~spl9_32 | spl9_38),
% 6.31/1.20 inference(avatar_split_clause,[],[f1531,f1489,f1449,f569,f1446])).
% 6.31/1.20 thf(f1536,plain,(
% 6.31/1.20 ($true = $false) | ~spl9_27),
% 6.31/1.20 inference(constrained_superposition,[],[f1376,f104])).
% 6.31/1.20 thf(f1543,plain,(
% 6.31/1.20 $false | ~spl9_27),
% 6.31/1.20 inference(trivial_inequality_removal,[],[f1536])).
% 6.31/1.20 thf(f1544,plain,(
% 6.31/1.20 ~spl9_27),
% 6.31/1.20 inference(avatar_contradiction_clause,[],[f1543])).
% 6.31/1.20 thf(f1590,plain,(
% 6.31/1.20 ( ! [X0 : ('type/realax/real' > $o),X1 : 'type/realax/real'] : (($true != $true) | ($true = (('const/realax/real_le' @ ('const/sets/inf' @ sK3) @ ('const/sets/inf' @ X0)))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK2 @ X1 @ X0) @ X0))) | ('const/sets/EMPTY' @ 'type/realax/real' = X0) | ($true != (('const/sets/IN' @ 'type/realax/real' @ (sK1 @ ('const/sets/inf' @ sK3) @ X0) @ sK3)))) ) | ~spl9_31),
% 6.31/1.20 inference(constrained_superposition,[],[f43,f1447])).
% 6.31/1.20 thf(f1593,plain,(
% 6.31/1.20 ( ! [X0 : ('type/realax/real' > $o),X1 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ ('const/sets/inf' @ sK3) @ ('const/sets/inf' @ X0)))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK2 @ X1 @ X0) @ X0))) | ('const/sets/EMPTY' @ 'type/realax/real' = X0) | ($true != (('const/sets/IN' @ 'type/realax/real' @ (sK1 @ ('const/sets/inf' @ sK3) @ X0) @ sK3)))) ) | ~spl9_31),
% 6.31/1.20 inference(trivial_inequality_removal,[],[f1590])).
% 6.31/1.20 thf(f1606,plain,(
% 6.31/1.20 ( ! [X0 : ('type/realax/real' > $o),X1 : 'type/realax/real'] : (($true != (('const/sets/IN' @ 'type/realax/real' @ (sK1 @ ('const/sets/inf' @ sK3) @ X0) @ sK3))) | ($true = (('const/realax/real_le' @ ('const/sets/inf' @ sK3) @ ('const/sets/inf' @ X0)))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK2 @ X1 @ X0) @ X0))) | ((^[Y0 : 'type/realax/real']: ($false)) = X0)) ) | (~spl9_12 | ~spl9_31)),
% 6.31/1.20 inference(forward_demodulation,[],[f1593,f571])).
% 6.31/1.20 thf(f1694,plain,(
% 6.31/1.20 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : (($true = $false) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK1 @ X1 @ sK4) @ sK4))) | ($true = (('const/realax/real_le' @ X1 @ ('const/sets/inf' @ sK4)))) | ('const/sets/EMPTY' @ 'type/realax/real' = sK4) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK2 @ X0 @ sK4) @ sK3)))) )),
% 6.31/1.20 inference(constrained_superposition,[],[f41,f1244])).
% 6.31/1.20 thf(f1707,plain,(
% 6.31/1.20 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : (($true = (('const/sets/IN' @ 'type/realax/real' @ (sK1 @ X1 @ sK4) @ sK4))) | ($true = (('const/realax/real_le' @ X1 @ ('const/sets/inf' @ sK4)))) | ('const/sets/EMPTY' @ 'type/realax/real' = sK4) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK2 @ X0 @ sK4) @ sK3)))) )),
% 6.31/1.20 inference(trivial_inequality_removal,[],[f1694])).
% 6.31/1.20 thf(f1725,plain,(
% 6.31/1.20 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : (($true = (('const/sets/IN' @ 'type/realax/real' @ (sK1 @ X1 @ sK4) @ sK4))) | ($true = (('const/realax/real_le' @ X1 @ ('const/sets/inf' @ sK4)))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK2 @ X0 @ sK4) @ sK3)))) )),
% 6.31/1.20 inference(forward_subsumption_resolution,[],[f1707,f45])).
% 6.31/1.20 thf(f1735,definition,(
% 6.31/1.20 spl9_39 <=> ! [X0 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ X0 @ ('const/sets/inf' @ sK4)))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK1 @ X0 @ sK4) @ sK3))))),
% 6.31/1.20 introduced(definition,[new_symbols(definition,[spl9_39])],[avatar_definition])).
% 6.31/1.20 thf(f1736,plain,(
% 6.31/1.20 ( ! [X0 : 'type/realax/real'] : (($true = (('const/sets/IN' @ 'type/realax/real' @ (sK1 @ X0 @ sK4) @ sK3))) | ($true = (('const/realax/real_le' @ X0 @ ('const/sets/inf' @ sK4))))) ) | ~spl9_39),
% 6.31/1.20 inference(avatar_component_clause,[],[f1735])).
% 6.31/1.20 thf(f1738,definition,(
% 6.31/1.20 spl9_40 <=> ! [X1 : 'type/realax/real'] : ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK2 @ X1 @ sK4) @ sK4)))),
% 6.31/1.20 introduced(definition,[new_symbols(definition,[spl9_40])],[avatar_definition])).
% 6.31/1.20 thf(f1739,plain,(
% 6.31/1.20 ( ! [X1 : 'type/realax/real'] : (($true = (('const/sets/IN' @ 'type/realax/real' @ (sK2 @ X1 @ sK4) @ sK4)))) ) | ~spl9_40),
% 6.31/1.20 inference(avatar_component_clause,[],[f1738])).
% 6.31/1.20 thf(f1743,definition,(
% 6.31/1.20 spl9_41 <=> ! [X0 : 'type/realax/real'] : ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK2 @ X0 @ sK4) @ sK3)))),
% 6.31/1.20 introduced(definition,[new_symbols(definition,[spl9_41])],[avatar_definition])).
% 6.31/1.20 thf(f1744,plain,(
% 6.31/1.20 ( ! [X0 : 'type/realax/real'] : (($true = (('const/sets/IN' @ 'type/realax/real' @ (sK2 @ X0 @ sK4) @ sK3)))) ) | ~spl9_41),
% 6.31/1.20 inference(avatar_component_clause,[],[f1743])).
% 6.31/1.20 thf(f1750,definition,(
% 6.31/1.20 spl9_43 <=> ! [X1 : 'type/realax/real'] : (($true = (('const/sets/IN' @ 'type/realax/real' @ (sK1 @ X1 @ sK4) @ sK4))) | ($true = (('const/realax/real_le' @ X1 @ ('const/sets/inf' @ sK4)))))),
% 6.31/1.20 introduced(definition,[new_symbols(definition,[spl9_43])],[avatar_definition])).
% 6.31/1.20 thf(f1751,plain,(
% 6.31/1.20 ( ! [X1 : 'type/realax/real'] : (($true = (('const/sets/IN' @ 'type/realax/real' @ (sK1 @ X1 @ sK4) @ sK4))) | ($true = (('const/realax/real_le' @ X1 @ ('const/sets/inf' @ sK4))))) ) | ~spl9_43),
% 6.31/1.20 inference(avatar_component_clause,[],[f1750])).
% 6.31/1.20 thf(f1752,plain,(
% 6.31/1.20 spl9_41 | spl9_43),
% 6.31/1.20 inference(avatar_split_clause,[],[f1725,f1750,f1743])).
% 6.31/1.20 thf(f1894,plain,(
% 6.31/1.20 ( ! [X0 : 'type/realax/real'] : (($true = $false) | ($true = ((sK3 @ (sK2 @ X0 @ sK4))))) ) | ~spl9_41),
% 6.31/1.20 inference(constrained_superposition,[],[f75,f1744])).
% 6.31/1.20 thf(f1896,plain,(
% 6.31/1.20 ( ! [X0 : 'type/realax/real'] : (($true != $true) | ($true = (('const/realax/real_le' @ sK5 @ (sK2 @ X0 @ sK4))))) ) | ~spl9_41),
% 6.31/1.20 inference(constrained_superposition,[],[f47,f1744])).
% 6.31/1.20 thf(f1897,plain,(
% 6.31/1.20 ( ! [X0 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ sK5 @ (sK2 @ X0 @ sK4))))) ) | ~spl9_41),
% 6.31/1.20 inference(trivial_inequality_removal,[],[f1896])).
% 6.31/1.20 thf(f1899,plain,(
% 6.31/1.20 ( ! [X0 : 'type/realax/real'] : (($true = ((sK3 @ (sK2 @ X0 @ sK4))))) ) | ~spl9_41),
% 6.31/1.20 inference(trivial_inequality_removal,[],[f1894])).
% 6.31/1.20 thf(f2124,plain,(
% 6.31/1.20 ( ! [X0 : 'type/realax/real'] : (($true != $true) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK1 @ X0 @ sK4) @ sK4))) | ($true = (('const/realax/real_le' @ X0 @ ('const/sets/inf' @ sK4)))) | ('const/sets/EMPTY' @ 'type/realax/real' = sK4)) ) | ~spl9_41),
% 6.31/1.20 inference(constrained_superposition,[],[f42,f1897])).
% 6.31/1.20 thf(f2129,plain,(
% 6.31/1.20 ( ! [X0 : 'type/realax/real'] : (($true = (('const/sets/IN' @ 'type/realax/real' @ (sK1 @ X0 @ sK4) @ sK4))) | ($true = (('const/realax/real_le' @ X0 @ ('const/sets/inf' @ sK4)))) | ('const/sets/EMPTY' @ 'type/realax/real' = sK4)) ) | ~spl9_41),
% 6.31/1.20 inference(trivial_inequality_removal,[],[f2124])).
% 6.31/1.20 thf(f2133,plain,(
% 6.31/1.20 ( ! [X0 : 'type/realax/real'] : (($true = (('const/sets/IN' @ 'type/realax/real' @ (sK1 @ X0 @ sK4) @ sK4))) | ($true = (('const/realax/real_le' @ X0 @ ('const/sets/inf' @ sK4))))) ) | ~spl9_41),
% 6.31/1.20 inference(forward_subsumption_resolution,[],[f2129,f45])).
% 6.31/1.20 thf(f2134,plain,(
% 6.31/1.20 spl9_43 | ~spl9_41),
% 6.31/1.20 inference(avatar_split_clause,[],[f2133,f1743,f1750])).
% 6.31/1.20 thf(f4161,plain,(
% 6.31/1.20 ( ! [X0 : 'type/realax/real'] : (($true != $true) | ($true = (('const/realax/real_le' @ ('const/sets/inf' @ sK3) @ ('const/sets/inf' @ sK4)))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK2 @ X0 @ sK4) @ sK4))) | (sK4 = (^[Y0 : 'type/realax/real']: ($false))) | ($true = (('const/realax/real_le' @ ('const/sets/inf' @ sK3) @ ('const/sets/inf' @ sK4))))) ) | (~spl9_12 | ~spl9_31 | ~spl9_39)),
% 6.31/1.20 inference(constrained_superposition,[],[f1606,f1736])).
% 6.31/1.20 thf(f4162,plain,(
% 6.31/1.20 ( ! [X0 : 'type/realax/real'] : (($true != $true) | ($true = (('const/realax/real_le' @ ('const/sets/inf' @ sK3) @ ('const/sets/inf' @ sK4)))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK2 @ X0 @ sK4) @ sK4))) | (sK4 = (^[Y0 : 'type/realax/real']: ($false)))) ) | (~spl9_12 | ~spl9_31 | ~spl9_39)),
% 6.31/1.20 inference(duplicate_literal_removal,[],[f4161])).
% 6.31/1.20 thf(f4163,plain,(
% 6.31/1.20 ( ! [X0 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ ('const/sets/inf' @ sK3) @ ('const/sets/inf' @ sK4)))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK2 @ X0 @ sK4) @ sK4))) | (sK4 = (^[Y0 : 'type/realax/real']: ($false)))) ) | (~spl9_12 | ~spl9_31 | ~spl9_39)),
% 6.31/1.20 inference(trivial_inequality_removal,[],[f4162])).
% 6.31/1.20 thf(f4179,plain,(
% 6.31/1.20 ( ! [X0 : 'type/realax/real'] : (($true = (('const/sets/IN' @ 'type/realax/real' @ (sK2 @ X0 @ sK4) @ sK4))) | (sK4 = (^[Y0 : 'type/realax/real']: ($false)))) ) | (~spl9_12 | ~spl9_31 | ~spl9_39)),
% 6.31/1.20 inference(forward_subsumption_resolution,[],[f4163,f48])).
% 6.31/1.20 thf(f4182,definition,(
% 6.31/1.20 spl9_62 <=> (sK4 = (^[Y0 : 'type/realax/real']: ($false)))),
% 6.31/1.20 introduced(definition,[new_symbols(definition,[spl9_62])],[avatar_definition])).
% 6.31/1.20 thf(f4184,plain,(
% 6.31/1.20 (sK4 = (^[Y0 : 'type/realax/real']: ($false))) | ~spl9_62),
% 6.31/1.20 inference(avatar_component_clause,[],[f4182])).
% 6.31/1.20 thf(f4185,plain,(
% 6.31/1.20 spl9_62 | spl9_40 | ~spl9_12 | ~spl9_31 | ~spl9_39),
% 6.31/1.20 inference(avatar_split_clause,[],[f4179,f1735,f1446,f569,f1738,f4182])).
% 6.31/1.20 thf(f4192,plain,(
% 6.31/1.20 ( ! [X0 : ('type/realax/real' > $o),X1 : 'type/realax/real'] : (($true != $true) | ($true = (('const/realax/real_le' @ ('const/sets/inf' @ sK3) @ ('const/sets/inf' @ X0)))) | ('const/sets/EMPTY' @ 'type/realax/real' = X0) | ($false = (('const/realax/real_le' @ X1 @ (sK2 @ X1 @ X0)))) | ($true != (('const/sets/IN' @ 'type/realax/real' @ (sK1 @ ('const/sets/inf' @ sK3) @ X0) @ sK3)))) ) | ~spl9_31),
% 6.31/1.20 inference(constrained_superposition,[],[f212,f1447])).
% 6.31/1.20 thf(f4228,plain,(
% 6.31/1.20 ( ! [X0 : ('type/realax/real' > $o),X1 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ ('const/sets/inf' @ sK3) @ ('const/sets/inf' @ X0)))) | ('const/sets/EMPTY' @ 'type/realax/real' = X0) | ($false = (('const/realax/real_le' @ X1 @ (sK2 @ X1 @ X0)))) | ($true != (('const/sets/IN' @ 'type/realax/real' @ (sK1 @ ('const/sets/inf' @ sK3) @ X0) @ sK3)))) ) | ~spl9_31),
% 6.31/1.20 inference(trivial_inequality_removal,[],[f4192])).
% 6.31/1.20 thf(f4240,plain,(
% 6.31/1.20 ( ! [X0 : ('type/realax/real' > $o),X1 : 'type/realax/real'] : (($true != (('const/sets/IN' @ 'type/realax/real' @ (sK1 @ ('const/sets/inf' @ sK3) @ X0) @ sK3))) | ($true = (('const/realax/real_le' @ ('const/sets/inf' @ sK3) @ ('const/sets/inf' @ X0)))) | ($false = (('const/realax/real_le' @ X1 @ (sK2 @ X1 @ X0)))) | ((^[Y0 : 'type/realax/real']: ($false)) = X0)) ) | (~spl9_12 | ~spl9_31)),
% 6.31/1.20 inference(forward_demodulation,[],[f4228,f571])).
% 6.31/1.20 thf(f4406,plain,(
% 6.31/1.20 ( ! [X0 : 'type/realax/real'] : (($true = $false) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK2 @ X0 @ sK4) @ sK3)))) ) | ~spl9_40),
% 6.31/1.20 inference(constrained_superposition,[],[f1244,f1739])).
% 6.31/1.20 thf(f4407,plain,(
% 6.31/1.20 ( ! [X0 : 'type/realax/real'] : (($true = (('const/sets/IN' @ 'type/realax/real' @ (sK2 @ X0 @ sK4) @ sK3)))) ) | ~spl9_40),
% 6.31/1.20 inference(trivial_inequality_removal,[],[f4406])).
% 6.31/1.20 thf(f4441,plain,(
% 6.31/1.20 ( ! [X0 : 'type/realax/real'] : (($true != $true) | ($true = (('const/realax/real_le' @ ('const/sets/inf' @ sK3) @ ('const/sets/inf' @ sK4)))) | ($false = (('const/realax/real_le' @ X0 @ (sK2 @ X0 @ sK4)))) | (sK4 = (^[Y0 : 'type/realax/real']: ($false))) | ($true = (('const/realax/real_le' @ ('const/sets/inf' @ sK3) @ ('const/sets/inf' @ sK4))))) ) | (~spl9_12 | ~spl9_31 | ~spl9_39)),
% 6.31/1.20 inference(constrained_superposition,[],[f4240,f1736])).
% 6.31/1.20 thf(f4444,plain,(
% 6.31/1.20 ( ! [X0 : 'type/realax/real'] : (($true != $true) | ($true = (('const/realax/real_le' @ ('const/sets/inf' @ sK3) @ ('const/sets/inf' @ sK4)))) | ($false = (('const/realax/real_le' @ X0 @ (sK2 @ X0 @ sK4)))) | (sK4 = (^[Y0 : 'type/realax/real']: ($false)))) ) | (~spl9_12 | ~spl9_31 | ~spl9_39)),
% 6.31/1.20 inference(duplicate_literal_removal,[],[f4441])).
% 6.31/1.20 thf(f4445,plain,(
% 6.31/1.20 ( ! [X0 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ ('const/sets/inf' @ sK3) @ ('const/sets/inf' @ sK4)))) | ($false = (('const/realax/real_le' @ X0 @ (sK2 @ X0 @ sK4)))) | (sK4 = (^[Y0 : 'type/realax/real']: ($false)))) ) | (~spl9_12 | ~spl9_31 | ~spl9_39)),
% 6.31/1.20 inference(trivial_inequality_removal,[],[f4444])).
% 6.31/1.20 thf(f4466,plain,(
% 6.31/1.20 ( ! [X0 : 'type/realax/real'] : (($false = (('const/realax/real_le' @ X0 @ (sK2 @ X0 @ sK4)))) | (sK4 = (^[Y0 : 'type/realax/real']: ($false)))) ) | (~spl9_12 | ~spl9_31 | ~spl9_39)),
% 6.31/1.20 inference(forward_subsumption_resolution,[],[f4445,f48])).
% 6.31/1.20 thf(f4469,definition,(
% 6.31/1.20 spl9_64 <=> ! [X0 : 'type/realax/real'] : ($false = (('const/realax/real_le' @ X0 @ (sK2 @ X0 @ sK4))))),
% 6.31/1.20 introduced(definition,[new_symbols(definition,[spl9_64])],[avatar_definition])).
% 6.31/1.20 thf(f4470,plain,(
% 6.31/1.20 ( ! [X0 : 'type/realax/real'] : (($false = (('const/realax/real_le' @ X0 @ (sK2 @ X0 @ sK4))))) ) | ~spl9_64),
% 6.31/1.20 inference(avatar_component_clause,[],[f4469])).
% 6.31/1.20 thf(f4471,plain,(
% 6.31/1.20 spl9_62 | spl9_64 | ~spl9_12 | ~spl9_31 | ~spl9_39),
% 6.31/1.20 inference(avatar_split_clause,[],[f4466,f1735,f1446,f569,f4469,f4182])).
% 6.31/1.20 thf(f4537,plain,(
% 6.31/1.20 ($true = $false) | ($false = ((sK3 @ (sK2 @ sK5 @ sK4)))) | ~spl9_64),
% 6.31/1.20 inference(constrained_superposition,[],[f4470,f164])).
% 6.31/1.20 thf(f4593,plain,(
% 6.31/1.20 ($false = ((sK3 @ (sK2 @ sK5 @ sK4)))) | ~spl9_64),
% 6.31/1.20 inference(trivial_inequality_removal,[],[f4537])).
% 6.31/1.20 thf(f4613,plain,(
% 6.31/1.20 ($true = $false) | (~spl9_41 | ~spl9_64)),
% 6.31/1.20 inference(forward_demodulation,[],[f4593,f1899])).
% 6.31/1.20 thf(f4614,plain,(
% 6.31/1.20 $false | (~spl9_41 | ~spl9_64)),
% 6.31/1.20 inference(trivial_inequality_removal,[],[f4613])).
% 6.31/1.20 thf(f4615,plain,(
% 6.31/1.20 ~spl9_41 | ~spl9_64),
% 6.31/1.20 inference(avatar_contradiction_clause,[],[f4614])).
% 6.31/1.20 thf(f4672,plain,(
% 6.31/1.20 ('const/sets/EMPTY' @ 'type/realax/real' != (^[Y0 : 'type/realax/real']: ($false))) | ~spl9_62),
% 6.31/1.20 inference(constrained_superposition,[],[f45,f4184])).
% 6.31/1.20 thf(f4704,plain,(
% 6.31/1.20 $false | (~spl9_12 | ~spl9_62)),
% 6.31/1.20 inference(forward_subsumption_resolution,[],[f4672,f571])).
% 6.31/1.20 thf(f4705,plain,(
% 6.31/1.20 ~spl9_12 | ~spl9_62),
% 6.31/1.20 inference(avatar_contradiction_clause,[],[f4704])).
% 6.31/1.20 thf(f4708,plain,(
% 6.31/1.20 spl9_41 | ~spl9_40),
% 6.31/1.20 inference(avatar_split_clause,[],[f4407,f1738,f1743])).
% 6.31/1.20 thf(f4780,plain,(
% 6.31/1.20 ( ! [X0 : 'type/realax/real'] : (($true = $false) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK1 @ X0 @ sK4) @ sK3))) | ($true = (('const/realax/real_le' @ X0 @ ('const/sets/inf' @ sK4))))) ) | ~spl9_43),
% 6.31/1.20 inference(constrained_superposition,[],[f1244,f1751])).
% 6.31/1.20 thf(f4781,plain,(
% 6.31/1.20 ( ! [X0 : 'type/realax/real'] : (($true = (('const/sets/IN' @ 'type/realax/real' @ (sK1 @ X0 @ sK4) @ sK3))) | ($true = (('const/realax/real_le' @ X0 @ ('const/sets/inf' @ sK4))))) ) | ~spl9_43),
% 6.31/1.20 inference(trivial_inequality_removal,[],[f4780])).
% 6.31/1.20 thf(f4799,plain,(
% 6.31/1.20 spl9_39 | ~spl9_43),
% 6.31/1.20 inference(avatar_split_clause,[],[f4781,f1750,f1735])).
% 6.31/1.20 cnf(s32, plain, spl9_12, inference(sat_conversion,[],[f1184])).
% 6.31/1.20 cnf(s34, plain, ~spl9_5 | spl9_27, inference(sat_conversion,[],[f1385])).
% 6.31/1.20 cnf(s66, plain, ~spl9_12 | spl9_31 | spl9_32 | spl9_38, inference(sat_conversion,[],[f1497])).
% 6.31/1.20 cnf(s82, plain, spl9_5 | ~spl9_12 | ~spl9_38, inference(sat_conversion,[],[f1515])).
% 6.31/1.20 cnf(s84, plain, ~spl9_12 | spl9_31 | ~spl9_32 | spl9_38, inference(sat_conversion,[],[f1534])).
% 6.31/1.20 cnf(s88, plain, ~spl9_27, inference(sat_conversion,[],[f1544])).
% 6.31/1.20 cnf(s97, plain, spl9_41 | spl9_43, inference(sat_conversion,[],[f1752])).
% 6.31/1.20 cnf(s110, plain, ~spl9_41 | spl9_43, inference(sat_conversion,[],[f2134])).
% 6.31/1.20 cnf(s142, plain, ~spl9_12 | ~spl9_31 | ~spl9_39 | spl9_40 | spl9_62, inference(sat_conversion,[],[f4185])).
% 6.31/1.20 cnf(s145, plain, ~spl9_12 | ~spl9_31 | ~spl9_39 | spl9_62 | spl9_64, inference(sat_conversion,[],[f4471])).
% 6.31/1.20 cnf(s153, plain, ~spl9_41 | ~spl9_64, inference(sat_conversion,[],[f4615])).
% 6.31/1.20 cnf(s158, plain, ~spl9_12 | ~spl9_62, inference(sat_conversion,[],[f4705])).
% 6.31/1.20 cnf(s159, plain, ~spl9_40 | spl9_41, inference(sat_conversion,[],[f4708])).
% 6.31/1.20 cnf(s164, plain, spl9_39 | ~spl9_43, inference(sat_conversion,[],[f4799])).
% 6.31/1.20 cnf(s176, plain, ~spl9_5, inference(rat,[],[s34,s88])).
% 6.31/1.20 cnf(s177, plain, ~spl9_62, inference(rat,[],[s158,s32])).
% 6.31/1.20 cnf(s178, plain, ~spl9_38, inference(rat,[],[s82,s176,s32])).
% 6.31/1.20 cnf(s195, plain, spl9_31, inference(rat,[],[s66,s84,s32,s178])).
% 6.31/1.20 cnf(s199, plain, ~spl9_39, inference(rat,[],[s159,s153,s142,s145,s32,s195,s177])).
% 6.31/1.20 cnf(s200, plain, ~spl9_43, inference(rat,[],[s164,s199])).
% 6.31/1.20 cnf(s203, plain, ~spl9_41, inference(rat,[],[s110,s200])).
% 6.31/1.20 cnf(s204, plain, $false, inference(rat,[],[s97,s200,s203])).
% 6.31/1.20 thf(f4801,plain,(
% 6.31/1.20 $false),
% 6.31/1.20 inference(avatar_sat_refutation,[],[s204])).
% 6.31/1.20 % SZS output end Proof for theBenchmark
% 6.31/1.20 % (1625055)------------------------------
% 6.31/1.20 % (1625055)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.31/1.20 % (1625055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.20 % (1625055)CaDiCaL version: 2.1.3
% 6.31/1.20 % (1625055)Termination reason: Refutation
% 6.31/1.20 % (1625055)Time elapsed: 0.338 s
% 6.31/1.20 % (1625055)Peak memory usage: 15 MB
% 6.31/1.20 % (1625055)Instructions burned: 698 (million)
% 6.31/1.20 % (1625002)Success in time 0.964 s
% 6.31/1.20 % Vampire exiting
%------------------------------------------------------------------------------