%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ITP149^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:10:53 AM UTC 2026
% Result : Theorem 186.48s 26.66s
% Output : Refutation 186.48s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP149^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 % Computer : n011.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Tue Sep 29 20:02:13 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 Running first-order model finding
% 0.09/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
% 5.55/1.07 % (570907)Will run a generic schedule for satisfiability detection.
% 5.55/1.07 % (570912)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1249019217_2999 on theBenchmark for (2999ds/0Mi)
% 5.55/1.07 % (570913)% WARNING: option uhcvi not known.
% 5.55/1.07 % (570913)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=867440861:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 5.55/1.07 % (570914)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3175116889:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 5.55/1.07 % (570915)dis+10_1_sil=32000:sp=arity:random_seed=2925850587:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 5.55/1.07 % (570916)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2110176715:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 5.55/1.07 % (570917)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=725197521:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 5.55/1.07 % (570918)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1966743669:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 5.55/1.07 % Exception at run slice level
% 5.55/1.07 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 5.55/1.07 % (570913)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 5.55/1.07 % (570916)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 5.55/1.07 % (570926)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3634923128:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 5.55/1.07 % (570913)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 5.55/1.07 % (570915)Instruction limit reached!
% 5.55/1.07 % (570915)------------------------------
% 5.55/1.07 % (570915)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.55/1.07 % (570915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.55/1.07 % (570915)CaDiCaL version: 2.1.3
% 5.55/1.07 % (570915)Termination reason: Instruction limit
% 5.55/1.07 % (570915)Termination phase: Saturation
% 5.55/1.07 % (570915)Time elapsed: 0.042 s
% 5.55/1.07 % (570915)Peak memory usage: 12 MB
% 5.55/1.07 % (570915)Instructions burned: 103 (million)
% 5.55/1.07 % Exception at run slice level
% 5.55/1.07 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 5.55/1.07 % (570916)Instruction limit reached!
% 5.55/1.07 % (570916)------------------------------
% 5.55/1.07 % (570916)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.55/1.07 % (570916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.55/1.07 % (570916)CaDiCaL version: 2.1.3
% 5.55/1.07 % (570916)Termination reason: Instruction limit
% 5.55/1.07 % (570916)Termination phase: Saturation
% 5.55/1.07 % (570916)Time elapsed: 0.050 s
% 5.55/1.07 % (570916)Peak memory usage: 12 MB
% 5.55/1.07 % (570916)Instructions burned: 121 (million)
% 5.55/1.07 % (570917)Instruction limit reached!
% 5.55/1.07 % (570917)------------------------------
% 5.55/1.07 % (570917)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.55/1.07 % (570917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.55/1.07 % (570917)CaDiCaL version: 2.1.3
% 5.55/1.07 % (570917)Termination reason: Instruction limit
% 5.55/1.07 % (570917)Termination phase: Saturation
% 5.55/1.07 % (570917)Time elapsed: 0.055 s
% 5.55/1.07 % (570917)Peak memory usage: 12 MB
% 5.55/1.07 % (570917)Instructions burned: 133 (million)
% 5.55/1.07 % (570929)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=1282087878:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 5.55/1.07 % (570928)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1707670945:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 5.55/1.07 % (570929)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 5.55/1.07 % (570918)Instruction limit reached!
% 5.55/1.07 % (570918)------------------------------
% 5.55/1.07 % (570918)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.55/1.07 % (570918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.55/1.07 % (570918)CaDiCaL version: 2.1.3
% 17.05/2.88 % (570918)Termination reason: Instruction limit
% 17.05/2.88 % (570918)Termination phase: Saturation
% 17.05/2.88 % (570918)Time elapsed: 0.068 s
% 17.05/2.88 % (570918)Peak memory usage: 13 MB
% 17.05/2.88 % (570918)Instructions burned: 161 (million)
% 17.05/2.88 % (570930)ott-21_1_sil=16000:fs=off:random_seed=1813659595:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 17.05/2.88 % (570932)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2091961298:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 17.05/2.88 % (570929)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 17.05/2.88 % (570935)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1828180877:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 17.05/2.88 % (570928)Instruction limit reached!
% 17.05/2.88 % (570928)------------------------------
% 17.05/2.88 % (570928)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.05/2.88 % (570928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.05/2.88 % (570928)CaDiCaL version: 2.1.3
% 17.05/2.88 % (570928)Termination reason: Instruction limit
% 17.05/2.88 % (570928)Termination phase: Saturation
% 17.05/2.88 % (570928)Time elapsed: 0.055 s
% 17.05/2.88 % (570928)Peak memory usage: 12 MB
% 17.05/2.88 % (570928)Instructions burned: 132 (million)
% 17.05/2.88 % Exception at run slice level
% 17.05/2.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 17.05/2.88 % (570938)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3918133559:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 17.05/2.88 % (570930)Instruction limit reached!
% 17.05/2.88 % (570930)------------------------------
% 17.05/2.88 % (570930)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.05/2.88 % (570930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.05/2.88 % (570930)CaDiCaL version: 2.1.3
% 17.05/2.88 % (570930)Termination reason: Instruction limit
% 17.05/2.88 % (570930)Termination phase: Saturation
% 17.05/2.88 % (570930)Time elapsed: 0.077 s
% 17.05/2.88 % (570930)Peak memory usage: 14 MB
% 17.05/2.88 % (570930)Instructions burned: 184 (million)
% 17.05/2.88 % (570939)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2172185381:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 17.05/2.88 % (570942)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=542703254: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)
% 17.05/2.88 % (570942)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 17.05/2.88 % (570929)Instruction limit reached!
% 17.05/2.88 % (570929)------------------------------
% 17.05/2.88 % (570929)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.05/2.88 % (570929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.05/2.88 % (570929)CaDiCaL version: 2.1.3
% 17.05/2.88 % (570929)Termination reason: Instruction limit
% 17.05/2.88 % (570929)Termination phase: Saturation
% 17.05/2.88 % (570929)Time elapsed: 0.135 s
% 17.05/2.88 % (570929)Peak memory usage: 15 MB
% 17.05/2.88 % (570929)Instructions burned: 685 (million)
% 17.05/2.88 % Exception at run slice level
% 17.05/2.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 17.05/2.88 % (570944)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2131202201:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 17.05/2.88 % (570944)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 17.05/2.88 % (570945)fmb+10_1_sil=64000:random_seed=296088070:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi)
% 17.05/2.88 % (570945)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 17.05/2.88 % Exception at run slice level
% 17.05/2.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 17.05/2.88 % (570948)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=861092874:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi)
% 17.05/2.88 % Exception at run slice level
% 17.05/2.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 17.05/2.88 % (570932)Instruction limit reached!
% 17.05/2.88 % (570932)------------------------------
% 44.34/6.56 % (570932)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.34/6.56 % (570932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.34/6.56 % (570932)CaDiCaL version: 2.1.3
% 44.34/6.56 % (570932)Termination reason: Instruction limit
% 44.34/6.56 % (570932)Termination phase: Saturation
% 44.34/6.56 % (570932)Time elapsed: 0.247 s
% 44.34/6.56 % (570932)Peak memory usage: 14 MB
% 44.34/6.56 % (570932)Instructions burned: 478 (million)
% 44.34/6.56 % (570950)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2020708833:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi)
% 44.34/6.56 % (570951)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=869020026:i=5131_2996 on theBenchmark for (2996ds/5131Mi)
% 44.34/6.56 % (570951)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 44.34/6.56 % Exception at run slice level
% 44.34/6.56 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 44.34/6.56 % (570954)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3794560282:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 44.34/6.56 % (570954)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 44.34/6.56 % (570954)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 44.34/6.56 % (570944)Instruction limit reached!
% 44.34/6.56 % (570944)------------------------------
% 44.34/6.56 % (570944)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.34/6.56 % (570944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.34/6.56 % (570944)CaDiCaL version: 2.1.3
% 44.34/6.56 % (570944)Termination reason: Instruction limit
% 44.34/6.56 % (570944)Termination phase: Saturation
% 44.34/6.56 % (570944)Time elapsed: 0.231 s
% 44.34/6.56 % (570944)Peak memory usage: 17 MB
% 44.34/6.56 % (570944)Instructions burned: 882 (million)
% 44.34/6.56 % (570956)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2544342478:i=6324_2995 on theBenchmark for (2995ds/6324Mi)
% 44.34/6.56 % Exception at run slice level
% 44.34/6.56 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 44.34/6.56 % (570958)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1076888534:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi)
% 44.34/6.56 % (570942)Instruction limit reached!
% 44.34/6.56 % (570942)------------------------------
% 44.34/6.56 % (570942)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.34/6.56 % (570942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.34/6.56 % (570942)CaDiCaL version: 2.1.3
% 44.34/6.56 % (570942)Termination reason: Instruction limit
% 44.34/6.56 % (570942)Termination phase: Saturation
% 44.34/6.56 % (570942)Time elapsed: 0.316 s
% 44.34/6.56 % (570942)Peak memory usage: 17 MB
% 44.34/6.56 % (570942)Instructions burned: 693 (million)
% 44.34/6.56 % Exception at run slice level
% 44.34/6.56 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 44.34/6.56 % (570960)ott-2_1_sil=16000:newcnf=on:random_seed=3128997356:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi)
% 44.34/6.56 % (570961)ott+10_1_sil=32000:tgt=ground:random_seed=179635945:i=5114:av=off_2994 on theBenchmark for (2994ds/5114Mi)
% 44.34/6.56 % (570960)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 44.34/6.56 % (570938)Instruction limit reached!
% 44.34/6.56 % (570938)------------------------------
% 44.34/6.56 % (570938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.34/6.56 % (570938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.34/6.56 % (570938)CaDiCaL version: 2.1.3
% 44.34/6.56 % (570938)Termination reason: Instruction limit
% 44.34/6.56 % (570938)Termination phase: Saturation
% 44.34/6.56 % (570938)Time elapsed: 0.567 s
% 44.34/6.56 % (570938)Peak memory usage: 18 MB
% 44.34/6.56 % (570938)Instructions burned: 1181 (million)
% 44.34/6.56 % (570964)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2512009506:i=54282_2992 on theBenchmark for (2992ds/54282Mi)
% 44.34/6.56 % Exception at run slice level
% 44.34/6.56 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 44.34/6.56 % (570966)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3863507655:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi)
% 94.72/13.65 % (570966)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 94.72/13.65 % (570960)Instruction limit reached!
% 94.72/13.65 % (570960)------------------------------
% 94.72/13.65 % (570960)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.72/13.65 % (570960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.72/13.65 % (570960)CaDiCaL version: 2.1.3
% 94.72/13.65 % (570960)Termination reason: Instruction limit
% 94.72/13.65 % (570960)Termination phase: Saturation
% 94.72/13.65 % (570960)Time elapsed: 0.419 s
% 94.72/13.65 % (570960)Peak memory usage: 16 MB
% 94.72/13.65 % (570960)Instructions burned: 871 (million)
% 94.72/13.65 % (570968)dis+21_1_sil=32000:sas=cadical:random_seed=1885407721:i=3773:amm=off_2990 on theBenchmark for (2990ds/3773Mi)
% 94.72/13.65 % (570954)Instruction limit reached!
% 94.72/13.65 % (570954)------------------------------
% 94.72/13.65 % (570954)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.72/13.65 % (570954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.72/13.65 % (570954)CaDiCaL version: 2.1.3
% 94.72/13.65 % (570954)Termination reason: Instruction limit
% 94.72/13.65 % (570954)Termination phase: Saturation
% 94.72/13.65 % (570954)Time elapsed: 0.667 s
% 94.72/13.65 % (570954)Peak memory usage: 16 MB
% 94.72/13.65 % (570954)Instructions burned: 1475 (million)
% 94.72/13.65 % (570970)ott+11_1_sil=16000:gs=on:random_seed=2290788656:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi)
% 94.72/13.65 % (570970)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 94.72/13.65 % (570961)Instruction limit reached!
% 94.72/13.65 % (570961)------------------------------
% 94.72/13.65 % (570961)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.72/13.65 % (570961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.72/13.65 % (570961)CaDiCaL version: 2.1.3
% 94.72/13.65 % (570961)Termination reason: Instruction limit
% 94.72/13.65 % (570961)Termination phase: Saturation
% 94.72/13.65 % (570961)Time elapsed: 1.311 s
% 94.72/13.65 % (570961)Peak memory usage: 32 MB
% 94.72/13.65 % (570961)Instructions burned: 5115 (million)
% 94.72/13.65 % (570972)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3724552069:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi)
% 94.72/13.65 % Exception at run slice level
% 94.72/13.65 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 94.72/13.65 % (570974)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2948517938:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2980 on theBenchmark for (2980ds/4591Mi)
% 94.72/13.65 % (570970)Instruction limit reached!
% 94.72/13.65 % (570970)------------------------------
% 94.72/13.65 % (570970)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.72/13.65 % (570970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.72/13.65 % (570970)CaDiCaL version: 2.1.3
% 94.72/13.65 % (570970)Termination reason: Instruction limit
% 94.72/13.65 % (570970)Termination phase: Saturation
% 94.72/13.65 % (570970)Time elapsed: 1.040 s
% 94.72/13.65 % (570970)Peak memory usage: 18 MB
% 94.72/13.65 % (570970)Instructions burned: 2252 (million)
% 94.72/13.65 % (570999)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1427297922:i=29340_2978 on theBenchmark for (2978ds/29340Mi)
% 94.72/13.65 % (570966)Instruction limit reached!
% 94.72/13.65 % (570966)------------------------------
% 94.72/13.65 % (570966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.72/13.65 % (570966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.72/13.65 % (570966)CaDiCaL version: 2.1.3
% 94.72/13.65 % (570966)Termination reason: Instruction limit
% 94.72/13.65 % (570966)Termination phase: Saturation
% 94.72/13.65 % (570966)Time elapsed: 1.706 s
% 94.72/13.65 % (570966)Peak memory usage: 24 MB
% 94.72/13.65 % (570966)Instructions burned: 3512 (million)
% 94.72/13.65 % (571118)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1793320644:i=5211_2974 on theBenchmark for (2974ds/5211Mi)
% 94.72/13.65 % (570974)Instruction limit reached!
% 94.72/13.65 % (570974)------------------------------
% 94.72/13.65 % (570974)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.72/13.65 % (570974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.19/17.22 % (570974)CaDiCaL version: 2.1.3
% 120.19/17.22 % (570974)Termination reason: Instruction limit
% 120.19/17.22 % (570974)Termination phase: Saturation
% 120.19/17.22 % (570974)Time elapsed: 0.729 s
% 120.19/17.22 % (570974)Peak memory usage: 17 MB
% 120.19/17.22 % (570974)Instructions burned: 4592 (million)
% 120.19/17.22 % (571145)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=155868466:i=5497:nm=2_2973 on theBenchmark for (2973ds/5497Mi)
% 120.19/17.22 % Exception at run slice level
% 120.19/17.22 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 120.19/17.22 % (571155)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3530163838:fmbsr=2:i=46332_2973 on theBenchmark for (2973ds/46332Mi)
% 120.19/17.22 % Exception at run slice level
% 120.19/17.22 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 120.19/17.22 % (571177)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2515644473:i=14071_2972 on theBenchmark for (2972ds/14071Mi)
% 120.19/17.22 % Exception at run slice level
% 120.19/17.22 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 120.19/17.22 % (571192)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1031547914:i=22565:add=on:rawr=on_2972 on theBenchmark for (2972ds/22565Mi)
% 120.19/17.22 % (570968)Instruction limit reached!
% 120.19/17.22 % (570968)------------------------------
% 120.19/17.22 % (570968)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 120.19/17.22 % (570968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.19/17.22 % (570968)CaDiCaL version: 2.1.3
% 120.19/17.22 % (570968)Termination reason: Instruction limit
% 120.19/17.22 % (570968)Termination phase: Saturation
% 120.19/17.22 % (570968)Time elapsed: 1.845 s
% 120.19/17.22 % (570968)Peak memory usage: 25 MB
% 120.19/17.22 % (570968)Instructions burned: 3773 (million)
% 120.19/17.22 % (571197)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1208314607:i=8173:av=off_2971 on theBenchmark for (2971ds/8173Mi)
% 120.19/17.22 % (570951)Instruction limit reached!
% 120.19/17.22 % (570951)------------------------------
% 120.19/17.22 % (570951)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 120.19/17.22 % (570951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.19/17.22 % (570951)CaDiCaL version: 2.1.3
% 120.19/17.22 % (570951)Termination reason: Instruction limit
% 120.19/17.22 % (570951)Termination phase: Saturation
% 120.19/17.22 % (570951)Time elapsed: 2.485 s
% 120.19/17.22 % (570951)Peak memory usage: 27 MB
% 120.19/17.22 % (570951)Instructions burned: 5132 (million)
% 120.19/17.22 % (571199)dis+10_16:1_sil=16000:random_seed=1995801175:i=9155:fsr=off_2971 on theBenchmark for (2971ds/9155Mi)
% 120.19/17.22 % (571118)Instruction limit reached!
% 120.19/17.22 % (571118)------------------------------
% 120.19/17.22 % (571118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 120.19/17.22 % (571118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.19/17.22 % (571118)CaDiCaL version: 2.1.3
% 120.19/17.22 % (571118)Termination reason: Instruction limit
% 120.19/17.22 % (571118)Termination phase: Saturation
% 120.19/17.22 % (571118)Time elapsed: 2.461 s
% 120.19/17.22 % (571118)Peak memory usage: 35 MB
% 120.19/17.22 % (571118)Instructions burned: 5213 (million)
% 120.19/17.22 % (571354)ott-3_8_sil=64000:random_seed=3585766702:i=20139:bs=on_2949 on theBenchmark for (2949ds/20139Mi)
% 120.19/17.22 % (571192)Instruction limit reached!
% 120.19/17.22 % (571192)------------------------------
% 120.19/17.22 % (571192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 120.19/17.22 % (571192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.19/17.22 % (571192)CaDiCaL version: 2.1.3
% 120.19/17.22 % (571192)Termination reason: Instruction limit
% 120.19/17.22 % (571192)Termination phase: Saturation
% 120.19/17.22 % (571192)Time elapsed: 3.473 s
% 120.19/17.22 % (571192)Peak memory usage: 16 MB
% 120.19/17.22 % (571192)Instructions burned: 22570 (million)
% 120.19/17.22 % (571356)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2567036247:fmbsr=2:i=32576_2937 on theBenchmark for (2937ds/32576Mi)
% 120.19/17.22 % Exception at run slice level
% 120.19/17.22 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 120.19/17.22 % (571358)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=781346183:i=11404_2936 on theBenchmark for (2936ds/11404Mi)
% 128.09/18.38 % (571197)Instruction limit reached!
% 128.09/18.38 % (571197)------------------------------
% 128.09/18.38 % (571197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.09/18.38 % (571197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.09/18.38 % (571197)CaDiCaL version: 2.1.3
% 128.09/18.38 % (571197)Termination reason: Instruction limit
% 128.09/18.38 % (571197)Termination phase: Saturation
% 128.09/18.38 % (571197)Time elapsed: 4.034 s
% 128.09/18.38 % (571197)Peak memory usage: 42 MB
% 128.09/18.38 % (571197)Instructions burned: 8174 (million)
% 128.09/18.38 % (571360)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=423904037:i=14134_2931 on theBenchmark for (2931ds/14134Mi)
% 128.09/18.38 % (571360)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 128.09/18.38 % (571199)Instruction limit reached!
% 128.09/18.38 % (571199)------------------------------
% 128.09/18.38 % (571199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.09/18.38 % (571199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.09/18.38 % (571199)CaDiCaL version: 2.1.3
% 128.09/18.38 % (571199)Termination reason: Instruction limit
% 128.09/18.38 % (571199)Termination phase: Saturation
% 128.09/18.38 % (571199)Time elapsed: 4.183 s
% 128.09/18.38 % (571199)Peak memory usage: 35 MB
% 128.09/18.38 % (571199)Instructions burned: 9156 (million)
% 128.09/18.38 % (571362)dis+33_16_sil=32000:sac=on:random_seed=2490716244:i=15851:nm=0_2929 on theBenchmark for (2929ds/15851Mi)
% 128.09/18.38 % (571358)Instruction limit reached!
% 128.09/18.38 % (571358)------------------------------
% 128.09/18.38 % (571358)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.09/18.38 % (571358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.09/18.38 % (571358)CaDiCaL version: 2.1.3
% 128.09/18.38 % (571358)Termination reason: Instruction limit
% 128.09/18.38 % (571358)Termination phase: Saturation
% 128.09/18.38 % (571358)Time elapsed: 2.964 s
% 128.09/18.38 % (571358)Peak memory usage: 61 MB
% 128.09/18.38 % (571358)Instructions burned: 11405 (million)
% 128.09/18.38 % (571364)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1871487773:avsq=on:i=17627:add=on:amm=off_2907 on theBenchmark for (2907ds/17627Mi)
% 128.09/18.38 % (571364)Instruction limit reached!
% 128.09/18.38 % (571364)------------------------------
% 128.09/18.38 % (571364)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.09/18.38 % (571364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.09/18.38 % (571364)CaDiCaL version: 2.1.3
% 128.09/18.38 % (571364)Termination reason: Instruction limit
% 128.09/18.38 % (571364)Termination phase: Saturation
% 128.09/18.38 % (571364)Time elapsed: 2.643 s
% 128.09/18.38 % (571364)Peak memory usage: 16 MB
% 128.09/18.38 % (571364)Instructions burned: 17633 (million)
% 128.09/18.38 % (571366)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=927465092:s2a=on:i=53295_2880 on theBenchmark for (2880ds/53295Mi)
% 128.09/18.38 % (571354)Instruction limit reached!
% 128.09/18.38 % (571354)------------------------------
% 128.09/18.38 % (571354)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.09/18.38 % (571354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.09/18.38 % (571354)CaDiCaL version: 2.1.3
% 128.09/18.38 % (571354)Termination reason: Instruction limit
% 128.09/18.38 % (571354)Termination phase: Saturation
% 128.09/18.38 % (571354)Time elapsed: 7.142 s
% 128.09/18.38 % (571354)Peak memory usage: 30 MB
% 128.09/18.38 % (571354)Instructions burned: 20139 (million)
% 128.09/18.38 % (571368)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=4041195706:i=26857:ins=20_2878 on theBenchmark for (2878ds/26857Mi)
% 128.09/18.38 % Exception at run slice level
% 128.09/18.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 128.09/18.38 % (571370)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3211949538:i=28120:bs=on:fsr=off_2877 on theBenchmark for (2877ds/28120Mi)
% 128.09/18.38 % (571362)Instruction limit reached!
% 128.09/18.38 % (571362)------------------------------
% 128.09/18.38 % (571362)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.09/18.38 % (571362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.09/18.38 % (571362)CaDiCaL version: 2.1.3
% 128.09/18.38 % (571362)Termination reason: Instruction limit
% 128.09/18.38 % (571362)Termination phase: Saturation
% 128.09/18.38 % (571362)Time elapsed: 6.313 s
% 152.83/21.97 % (571362)Peak memory usage: 24 MB
% 152.83/21.97 % (571362)Instructions burned: 15853 (million)
% 152.83/21.97 % (571372)fmb+10_1_sil=256000:fmbss=7:random_seed=4285009439:fmbsr=1.6:i=182295_2865 on theBenchmark for (2865ds/182295Mi)
% 152.83/21.97 % Exception at run slice level
% 152.83/21.97 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 152.83/21.97 % (571374)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=108361013:i=44625:gsp=on_2865 on theBenchmark for (2865ds/44625Mi)
% 152.83/21.97 % (571374)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 152.83/21.97 % (571374)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 152.83/21.97 % Exception at run slice level
% 152.83/21.97 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 152.83/21.97 % (571376)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1332531705:i=160505_2864 on theBenchmark for (2864ds/160505Mi)
% 152.83/21.97 % Exception at run slice level
% 152.83/21.97 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 152.83/21.97 % (571378)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=4087032316:fmbsr=1.3:i=225729_2863 on theBenchmark for (2863ds/225729Mi)
% 152.83/21.97 % Exception at run slice level
% 152.83/21.97 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 152.83/21.97 % (571380)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1920048280:fmbsr=2:i=185024:ins=7_2863 on theBenchmark for (2863ds/185024Mi)
% 152.83/21.97 % Exception at run slice level
% 152.83/21.97 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 152.83/21.97 % (571382)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=802209467:rtra=on_2862 on theBenchmark for (2862ds/0Mi)
% 152.83/21.97 % Exception at run slice level
% 152.83/21.97 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 152.83/21.97 % (571384)% WARNING: option uhcvi not known.
% 152.83/21.97 % (571384)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2088116828:i=271062:add=off:rtra=on:rawr=on_2862 on theBenchmark for (2862ds/271062Mi)
% 152.83/21.97 % (571384)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 152.83/21.97 % (571384)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 152.83/21.97 % (571360)Instruction limit reached!
% 152.83/21.97 % (571360)------------------------------
% 152.83/21.97 % (571360)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 152.83/21.97 % (571360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.83/21.97 % (571360)CaDiCaL version: 2.1.3
% 152.83/21.97 % (571360)Termination reason: Instruction limit
% 152.83/21.97 % (571360)Termination phase: Saturation
% 152.83/21.97 % (571360)Time elapsed: 6.975 s
% 152.83/21.97 % (571360)Peak memory usage: 63 MB
% 152.83/21.97 % (571360)Instructions burned: 14134 (million)
% 152.83/21.97 % (571386)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=233075762:i=176048:add=on:rtra=on:rawr=on_2861 on theBenchmark for (2861ds/176048Mi)
% 152.83/21.97 % (570999)Instruction limit reached!
% 152.83/21.97 % (570999)------------------------------
% 152.83/21.97 % (570999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 152.83/21.97 % (570999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.83/21.97 % (570999)CaDiCaL version: 2.1.3
% 152.83/21.97 % (570999)Termination reason: Instruction limit
% 152.83/21.97 % (570999)Termination phase: Saturation
% 152.83/21.97 % (570999)Time elapsed: 14.668 s
% 152.83/21.97 % (570999)Peak memory usage: 51 MB
% 152.83/21.97 % (570999)Instructions burned: 29342 (million)
% 152.83/21.97 % (571388)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2601814027:i=206:fgj=on:rtra=on_2831 on theBenchmark for (2831ds/206Mi)
% 152.83/21.97 % (571388)Instruction limit reached!
% 152.83/21.97 % (571388)------------------------------
% 152.83/21.97 % (571388)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 152.83/21.97 % (571388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.83/21.97 % (571388)CaDiCaL version: 2.1.3
% 152.83/21.97 % (571388)Termination reason: Instruction limit
% 152.83/21.97 % (571388)Termination phase: Saturation
% 152.83/21.97 % (571388)Time elapsed: 0.100 s
% 169.96/24.21 % (571388)Peak memory usage: 14 MB
% 169.96/24.21 % (571388)Instructions burned: 207 (million)
% 169.96/24.21 % (571392)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=4011612324:i=232:rtra=on_2830 on theBenchmark for (2830ds/232Mi)
% 169.96/24.21 % (571392)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 169.96/24.21 % (571392)Instruction limit reached!
% 169.96/24.21 % (571392)------------------------------
% 169.96/24.21 % (571392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.96/24.21 % (571392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.96/24.21 % (571392)CaDiCaL version: 2.1.3
% 169.96/24.21 % (571392)Termination reason: Instruction limit
% 169.96/24.21 % (571392)Termination phase: Saturation
% 169.96/24.21 % (571392)Time elapsed: 0.107 s
% 169.96/24.21 % (571392)Peak memory usage: 14 MB
% 169.96/24.21 % (571392)Instructions burned: 233 (million)
% 169.96/24.21 % (571412)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1113583345:i=262:rtra=on_2828 on theBenchmark for (2828ds/262Mi)
% 169.96/24.21 % (571412)Instruction limit reached!
% 169.96/24.21 % (571412)------------------------------
% 169.96/24.21 % (571412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.96/24.21 % (571412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.96/24.21 % (571412)CaDiCaL version: 2.1.3
% 169.96/24.21 % (571412)Termination reason: Instruction limit
% 169.96/24.21 % (571412)Termination phase: Saturation
% 169.96/24.21 % (571412)Time elapsed: 0.122 s
% 169.96/24.21 % (571412)Peak memory usage: 14 MB
% 169.96/24.21 % (571412)Instructions burned: 262 (million)
% 169.96/24.21 % (571457)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1833329289:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2827 on theBenchmark for (2827ds/318Mi)
% 169.96/24.21 % (571457)Instruction limit reached!
% 169.96/24.21 % (571457)------------------------------
% 169.96/24.21 % (571457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.96/24.21 % (571457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.96/24.21 % (571457)CaDiCaL version: 2.1.3
% 169.96/24.21 % (571457)Termination reason: Instruction limit
% 169.96/24.21 % (571457)Termination phase: Saturation
% 169.96/24.21 % (571457)Time elapsed: 0.156 s
% 169.96/24.21 % (571457)Peak memory usage: 15 MB
% 169.96/24.21 % (571457)Instructions burned: 319 (million)
% 169.96/24.21 % (571521)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1359030772:i=1428:nm=2:rtra=on_2825 on theBenchmark for (2825ds/1428Mi)
% 169.96/24.21 % Exception at run slice level
% 169.96/24.21 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 169.96/24.21 % (571530)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=777037401:i=262:bd=preordered:rtra=on:fsd=on_2825 on theBenchmark for (2825ds/262Mi)
% 169.96/24.21 % (571530)Instruction limit reached!
% 169.96/24.21 % (571530)------------------------------
% 169.96/24.21 % (571530)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.96/24.21 % (571530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.96/24.21 % (571530)CaDiCaL version: 2.1.3
% 169.96/24.21 % (571530)Termination reason: Instruction limit
% 169.96/24.21 % (571530)Termination phase: Saturation
% 169.96/24.21 % (571530)Time elapsed: 0.118 s
% 169.96/24.21 % (571530)Peak memory usage: 14 MB
% 169.96/24.21 % (571530)Instructions burned: 262 (million)
% 169.96/24.21 % (571532)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:si=on:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=558955104:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2823 on theBenchmark for (2823ds/1368Mi)
% 169.96/24.21 % (571532)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 169.96/24.21 % (571532)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 169.96/24.21 % (571532)Instruction limit reached!
% 169.96/24.21 % (571532)------------------------------
% 169.96/24.21 % (571532)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.96/24.21 % (571532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.96/24.21 % (571532)CaDiCaL version: 2.1.3
% 169.96/24.21 % (571532)Termination reason: Instruction limit
% 169.96/24.21 % (571532)Termination phase: Saturation
% 169.96/24.21 % (571532)Time elapsed: 0.470 s
% 169.96/24.21 % (571532)Peak memory usage: 15 MB
% 169.96/24.21 % (571532)Instructions burned: 1370 (million)
% 169.96/24.21 % (571612)ott-21_1_sil=16000:si=on:fs=off:random_seed=2096161399:i=360:av=off:fsr=off:rtra=on_2818 on theBenchmark for (2818ds/360Mi)
% 186.48/26.66 % (571612)Instruction limit reached!
% 186.48/26.66 % (571612)------------------------------
% 186.48/26.66 % (571612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 186.48/26.66 % (571612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.48/26.66 % (571612)CaDiCaL version: 2.1.3
% 186.48/26.66 % (571612)Termination reason: Instruction limit
% 186.48/26.66 % (571612)Termination phase: Saturation
% 186.48/26.66 % (571612)Time elapsed: 0.198 s
% 186.48/26.66 % (571612)Peak memory usage: 15 MB
% 186.48/26.66 % (571612)Instructions burned: 360 (million)
% 186.48/26.66 % (571657)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=756443057:i=954:bd=all:rtra=on_2816 on theBenchmark for (2816ds/954Mi)
% 186.48/26.66 % (571657)Instruction limit reached!
% 186.48/26.66 % (571657)------------------------------
% 186.48/26.66 % (571657)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 186.48/26.66 % (571657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.48/26.66 % (571657)CaDiCaL version: 2.1.3
% 186.48/26.66 % (571657)Termination reason: Instruction limit
% 186.48/26.66 % (571657)Termination phase: Saturation
% 186.48/26.66 % (571657)Time elapsed: 0.522 s
% 186.48/26.66 % (571657)Peak memory usage: 15 MB
% 186.48/26.66 % (571657)Instructions burned: 956 (million)
% 186.48/26.66 % (571772)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=4013612369:fmbsr=1.3:i=1730:ins=25:rtra=on_2811 on theBenchmark for (2811ds/1730Mi)
% 186.48/26.66 % Exception at run slice level
% 186.48/26.66 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 186.48/26.66 % (571792)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=904345540:i=2358:rtra=on_2810 on theBenchmark for (2810ds/2358Mi)
% 186.48/26.66 % (571792)Instruction limit reached!
% 186.48/26.66 % (571792)------------------------------
% 186.48/26.66 % (571792)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 186.48/26.66 % (571792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.48/26.66 % (571792)CaDiCaL version: 2.1.3
% 186.48/26.66 % (571792)Termination reason: Instruction limit
% 186.48/26.66 % (571792)Termination phase: Saturation
% 186.48/26.66 % (571792)Time elapsed: 1.178 s
% 186.48/26.66 % (571792)Peak memory usage: 23 MB
% 186.48/26.66 % (571792)Instructions burned: 2358 (million)
% 186.48/26.66 % (571873)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3737852401:i=1778:ins=1:rtra=on_2798 on theBenchmark for (2798ds/1778Mi)
% 186.48/26.66 % Exception at run slice level
% 186.48/26.66 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 186.48/26.66 % (571875)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:si=on:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=4266857025:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2797 on theBenchmark for (2797ds/1384Mi)
% 186.48/26.66 % (571875)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 186.48/26.66 % (571875)Instruction limit reached!
% 186.48/26.66 % (571875)------------------------------
% 186.48/26.66 % (571875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 186.48/26.66 % (571875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.48/26.66 % (571875)CaDiCaL version: 2.1.3
% 186.48/26.66 % (571875)Termination reason: Instruction limit
% 186.48/26.66 % (571875)Termination phase: Saturation
% 186.48/26.66 % (571875)Time elapsed: 0.615 s
% 186.48/26.66 % (571875)Peak memory usage: 18 MB
% 186.48/26.66 % (571875)Instructions burned: 1385 (million)
% 186.48/26.66 % (571877)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2830258706:i=1758:kws=inv_precedence:fsr=off:rtra=on_2791 on theBenchmark for (2791ds/1758Mi)
% 186.48/26.66 % (571877)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 186.48/26.66 % (571877)Instruction limit reached!
% 186.48/26.66 % (571877)------------------------------
% 186.48/26.66 % (571877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 186.48/26.66 % (571877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.48/26.66 % (571877)CaDiCaL version: 2.1.3
% 186.48/26.66 % (571877)Termination reason: Instruction limit
% 186.48/26.66 % (571877)Termination phase: Saturation
% 186.48/26.66 % (571877)Time elapsed: 0.856 s
% 186.48/26.66 % (571877)Peak memory usage: 23 MB
% 186.48/26.66 % (571877)Instructions burned: 1759 (million)
% 186.48/26.66 % (571879)fmb+10_1_sil=64000:si=on:random_seed=1103848305:i=44122:nm=2:rtra=on:gsp=on_2782 on theBenchmark for (2782ds/44122Mi)
% 186.48/26.66 % (571879)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 186.48/26.66 % Exception at run slice level
% 186.48/26.66 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 186.48/26.66 % (571881)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3121647534:i=19030:nm=5:rtra=on_2782 on theBenchmark for (2782ds/19030Mi)
% 186.48/26.66 % Exception at run slice level
% 186.48/26.66 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 186.48/26.66 % (571883)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=1287003016:fmbsr=1.7:i=1840:rtra=on_2781 on theBenchmark for (2781ds/1840Mi)
% 186.48/26.66 % Exception at run slice level
% 186.48/26.66 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 186.48/26.66 % (571885)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3907935077:i=10262:rtra=on_2780 on theBenchmark for (2780ds/10262Mi)
% 186.48/26.66 % (571885)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 186.48/26.66 % (571370)Instruction limit reached!
% 186.48/26.66 % (571370)------------------------------
% 186.48/26.66 % (571370)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 186.48/26.66 % (571370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.48/26.66 % (571370)CaDiCaL version: 2.1.3
% 186.48/26.66 % (571370)Termination reason: Instruction limit
% 186.48/26.66 % (571370)Termination phase: Saturation
% 186.48/26.66 % (571370)Time elapsed: 10.432 s
% 186.48/26.66 % (571370)Peak memory usage: 27 MB
% 186.48/26.66 % (571370)Instructions burned: 28120 (million)
% 186.48/26.66 % (571887)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2345501681:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2772 on theBenchmark for (2772ds/2944Mi)
% 186.48/26.66 % (571887)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 186.48/26.66 % (571887)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 186.48/26.66 % (571366)Instruction limit reached!
% 186.48/26.66 % (571366)------------------------------
% 186.48/26.66 % (571366)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 186.48/26.66 % (571366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.48/26.66 % (571366)CaDiCaL version: 2.1.3
% 186.48/26.66 % (571366)Termination reason: Instruction limit
% 186.48/26.66 % (571366)Termination phase: Saturation
% 186.48/26.66 % (571366)Time elapsed: 11.468 s
% 186.48/26.66 % (571366)Peak memory usage: 59 MB
% 186.48/26.66 % (571366)Instructions burned: 53300 (million)
% 186.48/26.66 % (571889)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=1598760337:i=12648:rtra=on_2765 on theBenchmark for (2765ds/12648Mi)
% 186.48/26.66 % Exception at run slice level
% 186.48/26.66 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 186.48/26.66 % (571891)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=3378001801:fmbsr=2.30978:i=4348:rtra=on_2765 on theBenchmark for (2765ds/4348Mi)
% 186.48/26.66 % Exception at run slice level
% 186.48/26.66 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 186.48/26.66 % (571893)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=233164247:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2764 on theBenchmark for (2764ds/1738Mi)
% 186.48/26.66 % (571893)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 186.48/26.66 % (571887)Instruction limit reached!
% 186.48/26.66 % (571887)------------------------------
% 186.48/26.66 % (571887)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 186.48/26.66 % (571887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.48/26.66 % (571887)CaDiCaL version: 2.1.3
% 186.48/26.66 % (571887)Termination reason: Instruction limit
% 186.48/26.66 % (571887)Termination phase: Saturation
% 186.48/26.66 % (571887)Time elapsed: 1.227 s
% 186.48/26.66 % (571887)Peak memory usage: 17 MB
% 186.48/26.66 % (571887)Instructions burned: 2947 (million)
% 186.48/26.66 % (571895)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=3062282879:i=10228:av=off:rtra=on_2760 on theBenchmark for (2760ds/10228Mi)
% 186.48/26.66 % (571893)Instruction limit reached!
% 186.48/26.66 % (571893)------------------------------
% 186.48/26.66 % (571893)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 186.48/26.66 % (571893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.48/26.66 % (571893)CaDiCaL version: 2.1.3
% 186.48/26.66 % (571893)Termination reason: Instruction limit
% 186.48/26.66 % (571893)Termination phase: Saturation
% 186.48/26.66 % (571893)Time elapsed: 0.461 s
% 186.48/26.66 % (571893)Peak memory usage: 16 MB
% 186.48/26.66 % (571893)Instructions burned: 1739 (million)
% 186.48/26.66 % (571897)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=3153389699:i=108564:rtra=on_2760 on theBenchmark for (2760ds/108564Mi)
% 186.48/26.66 % Exception at run slice level
% 186.48/26.66 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 186.48/26.66 % (571899)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=2664029109:i=7024:aac=none:rtra=on_2759 on theBenchmark for (2759ds/7024Mi)
% 186.48/26.66 % (571899)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 186.48/26.66 % (570914)Instruction limit reached!
% 186.48/26.66 % (570914)------------------------------
% 186.48/26.66 % (570914)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 186.48/26.66 % (570914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.48/26.66 % (570914)CaDiCaL version: 2.1.3
% 186.48/26.66 % (570914)Termination reason: Instruction limit
% 186.48/26.66 % (570914)Termination phase: Saturation
% 186.48/26.66 % (570914)Time elapsed: 24.851 s
% 186.48/26.66 % (570914)Peak memory usage: 17 MB
% 186.48/26.66 % (570914)Instructions burned: 88025 (million)
% 186.48/26.66 % (571901)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=2507322339:i=7546:rtra=on:amm=off_2750 on theBenchmark for (2750ds/7546Mi)
% 186.48/26.66 % (571899)Instruction limit reached!
% 186.48/26.66 % (571899)------------------------------
% 186.48/26.66 % (571899)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 186.48/26.66 % (571899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.48/26.66 % (571899)CaDiCaL version: 2.1.3
% 186.48/26.66 % (571899)Termination reason: Instruction limit
% 186.48/26.66 % (571899)Termination phase: Saturation
% 186.48/26.66 % (571899)Time elapsed: 1.833 s
% 186.48/26.66 % (571899)Peak memory usage: 32 MB
% 186.48/26.66 % (571899)Instructions burned: 7024 (million)
% 186.48/26.66 % (571903)ott+11_1_sil=16000:si=on:gs=on:random_seed=3661823090:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2741 on theBenchmark for (2741ds/4502Mi)
% 186.48/26.66 % (571903)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 186.48/26.66 % (571903) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-570907-571903"...
% 186.48/26.66 % (571903)...printing done.
% 186.48/26.66 % (571903)Refutation found. Thanks to Tanya!
% 186.48/26.66 % SZS status Theorem for theBenchmark
% 186.48/26.66 % SZS output start Proof for theBenchmark
% 186.48/26.66 thf(type_def_5, type, bounde7994401a_real: $tType).
% 186.48/26.66 thf(type_def_6, type, set_set_real: $tType).
% 186.48/26.66 thf(type_def_7, type, set_set_a: $tType).
% 186.48/26.66 thf(type_def_8, type, set_real: $tType).
% 186.48/26.66 thf(type_def_9, type, set_a: $tType).
% 186.48/26.66 thf(type_def_10, type, real: $tType).
% 186.48/26.66 thf(type_def_11, type, a: $tType).
% 186.48/26.66 thf(type_def_12, type, sTfun: ($tType * $tType) > $tType).
% 186.48/26.66 thf(func_def_0, type, elemen1140313242l_real: (real > real > set_real)).
% 186.48/26.66 thf(func_def_1, type, elemen49976720ball_a: (a > real > set_a)).
% 186.48/26.66 thf(func_def_2, type, auto_l612940ivl0_a: ((a > a) > set_a > a > set_real)).
% 186.48/26.66 thf(func_def_3, type, minus_minus_real: (real > real > real)).
% 186.48/26.66 thf(func_def_4, type, minus_minus_set_real: (set_real > set_real > set_real)).
% 186.48/26.66 thf(func_def_5, type, minus_minus_set_a: (set_a > set_a > set_a)).
% 186.48/26.66 thf(func_def_6, type, minus_minus_a: (a > a > a)).
% 186.48/26.66 thf(func_def_7, type, uminus_uminus_a_a: ((a > a) > a > a)).
% 186.48/26.66 thf(func_def_8, type, uminus_uminus_real: (real > real)).
% 186.48/26.66 thf(func_def_9, type, uminus773214379t_real: (set_real > set_real)).
% 186.48/26.66 thf(func_def_10, type, uminus_uminus_set_a: (set_a > set_a)).
% 186.48/26.66 thf(func_def_11, type, uminus_uminus_a: (a > a)).
% 186.48/26.66 thf(func_def_12, type, zero_zero_real: real).
% 186.48/26.66 thf(func_def_13, type, zero_zero_a: a).
% 186.48/26.66 thf(func_def_14, type, initia826609931terval: (set_real > $o)).
% 186.48/26.66 thf(func_def_15, type, inner_4346926r_real: (real > real > real)).
% 186.48/26.66 thf(func_def_16, type, inner_1173012732nner_a: (a > a > real)).
% 186.48/26.66 thf(func_def_17, type, auto_l630715367iant_a: ((a > a) > set_a > set_a > $o)).
% 186.48/26.66 thf(func_def_18, type, line_c1152468841ment_a: (a > a > set_a)).
% 186.48/26.66 thf(func_def_19, type, line_open_segment_a: (a > a > set_a)).
% 186.48/26.66 thf(func_def_20, type, oDE_au1996717075pped_a: ((a > a) > set_a > a > set_a > $o)).
% 186.48/26.66 thf(func_def_21, type, ord_less_real: (real > real > $o)).
% 186.48/26.66 thf(func_def_22, type, ord_less_set_real: (set_real > set_real > $o)).
% 186.48/26.66 thf(func_def_23, type, ord_le861030508t_real: (set_set_real > set_set_real > $o)).
% 186.48/26.66 thf(func_def_24, type, ord_less_set_set_a: (set_set_a > set_set_a > $o)).
% 186.48/26.66 thf(func_def_25, type, ord_less_set_a: (set_a > set_a > $o)).
% 186.48/26.66 thf(func_def_26, type, ord_less_a: (a > a > $o)).
% 186.48/26.66 thf(func_def_27, type, ord_less_eq_real: (real > real > $o)).
% 186.48/26.66 thf(func_def_28, type, ord_less_eq_set_real: (set_real > set_real > $o)).
% 186.48/26.66 thf(func_def_29, type, ord_le1733505144t_real: (set_set_real > set_set_real > $o)).
% 186.48/26.66 thf(func_def_30, type, ord_le318720350_set_a: (set_set_a > set_set_a > $o)).
% 186.48/26.66 thf(func_def_31, type, ord_less_eq_set_a: (set_a > set_a > $o)).
% 186.48/26.66 thf(func_def_32, type, ord_less_eq_a: (a > a > $o)).
% 186.48/26.66 thf(func_def_33, type, top_top_set_real: set_real).
% 186.48/26.66 thf(func_def_34, type, top_top_set_a: set_a).
% 186.48/26.66 thf(func_def_35, type, period720806154rbit_a: ((a > a) > set_a > a > $o)).
% 186.48/26.66 thf(func_def_36, type, period1305449585riod_a: ((a > a) > set_a > a > real)).
% 186.48/26.66 thf(func_def_37, type, period138238489rbit_a: ((a > a) > set_a > a > $o)).
% 186.48/26.66 thf(func_def_38, type, poinca659159244_rot_a: (a > a)).
% 186.48/26.66 thf(func_def_39, type, poinca522724647ment_a: ((a > a) > set_a > a > a > $o)).
% 186.48/26.66 thf(func_def_40, type, reacha1191408304tion_a: ((a > a) > set_a > (a > real) > (a > bounde7994401a_real) > set_a > $o)).
% 186.48/26.66 thf(func_def_41, type, real_V1934908667t_real: (real > real > real)).
% 186.48/26.66 thf(func_def_42, type, real_V1514887919dist_a: (a > a > real)).
% 186.48/26.66 thf(func_def_43, type, collect_real: ((real > $o) > set_real)).
% 186.48/26.66 thf(func_def_44, type, collect_set_real: ((set_real > $o) > set_set_real)).
% 186.48/26.66 thf(func_def_45, type, collect_set_a: ((set_a > $o) > set_set_a)).
% 186.48/26.66 thf(func_def_46, type, collect_a: ((a > $o) > set_a)).
% 186.48/26.66 thf(func_def_47, type, set_or656347191t_real: (real > real > set_real)).
% 186.48/26.66 thf(func_def_48, type, set_or1619725421t_real: (set_real > set_real > set_set_real)).
% 186.48/26.66 thf(func_def_49, type, set_or2094724627_set_a: (set_a > set_a > set_set_a)).
% 186.48/26.66 thf(func_def_50, type, set_or411607219Most_a: (a > a > set_a)).
% 186.48/26.66 thf(func_def_51, type, member_real: (real > set_real > $o)).
% 186.48/26.66 thf(func_def_52, type, member_set_real: (set_real > set_set_real > $o)).
% 186.48/26.66 thf(func_def_53, type, member_set_a: (set_a > set_set_a > $o)).
% 186.48/26.66 thf(func_def_54, type, member_a: (a > set_a > $o)).
% 186.48/26.66 thf(func_def_55, type, x: set_a).
% 186.48/26.66 thf(func_def_56, type, a2: a).
% 186.48/26.66 thf(func_def_57, type, b: a).
% 186.48/26.66 thf(func_def_58, type, d: real).
% 186.48/26.66 thf(func_def_59, type, f: (a > a)).
% 186.48/26.66 thf(func_def_60, type, s: a).
% 186.48/26.66 thf(func_def_61, type, thesis: $o).
% 186.48/26.66 thf(func_def_62, type, x2: a).
% 186.48/26.66 thf(func_def_63, type, z: a).
% 186.48/26.66 thf(func_def_67, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 186.48/26.66 thf(func_def_68, type, vAND: ($o > $o > $o)).
% 186.48/26.66 thf(func_def_69, type, vNOT: ($o > $o)).
% 186.48/26.66 thf(func_def_70, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 186.48/26.66 thf(func_def_71, type, vIMP: ($o > $o > $o)).
% 186.48/26.66 thf(func_def_72, type, db0: !>[X0: $tType]:(X0)).
% 186.48/26.66 thf(func_def_73, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 186.48/26.66 thf(func_def_74, type, vOR: ($o > $o > $o)).
% 186.48/26.66 thf(func_def_75, type, db1: !>[X0: $tType]:(X0)).
% 186.48/26.66 thf(func_def_76, type, db2: !>[X0: $tType]:(X0)).
% 186.48/26.66 thf(func_def_77, type, sP0: (real > (real > real > $o) > real > $o)).
% 186.48/26.66 thf(func_def_78, type, sP1: ((real > real > $o) > $o)).
% 186.48/26.66 thf(func_def_79, type, sP2: (real > real > (real > real > $o) > $o)).
% 186.48/26.66 thf(func_def_80, type, sP3: (a > $o)).
% 186.48/26.66 thf(func_def_81, type, sP4: (a > $o)).
% 186.48/26.66 thf(func_def_82, type, sP5: (real > real > $o)).
% 186.48/26.66 thf(func_def_83, type, sP6: (a > $o)).
% 186.48/26.66 thf(func_def_84, type, sP7: (a > a > $o)).
% 186.48/26.66 thf(func_def_85, type, sP8: (a > a > $o)).
% 186.48/26.66 thf(func_def_86, type, sP9: (a > $o)).
% 186.48/26.66 thf(func_def_87, type, sK10: (a > real)).
% 186.48/26.66 thf(func_def_88, type, sK11: (set_a > set_a > a)).
% 186.48/26.66 thf(func_def_89, type, sK12: (real > real > (real > real > $o) > real)).
% 186.48/26.66 thf(func_def_90, type, sK13: ((real > real > $o) > real)).
% 186.48/26.66 thf(func_def_91, type, sK14: ((real > real > $o) > real)).
% 186.48/26.66 thf(func_def_92, type, sK15: ((real > real > $o) > real)).
% 186.48/26.66 thf(func_def_93, type, sK16: (real > (real > real > $o) > real > real)).
% 186.48/26.66 thf(func_def_94, type, sK17: (real > (real > real > $o) > real > real)).
% 186.48/26.66 thf(func_def_95, type, sK18: ((a > $o) > (a > $o) > a)).
% 186.48/26.66 thf(func_def_96, type, sK19: (a > real)).
% 186.48/26.66 thf(func_def_97, type, sK20: real).
% 186.48/26.66 thf(func_def_98, type, sK21: (a > a)).
% 186.48/26.66 thf(func_def_99, type, sK22: (a > a)).
% 186.48/26.66 thf(func_def_100, type, sK23: (real > real > a)).
% 186.48/26.66 thf(func_def_101, type, sK24: (real > real > a)).
% 186.48/26.66 thf(func_def_102, type, sK25: ((real > $o) > (real > $o) > real)).
% 186.48/26.66 thf(func_def_103, type, sK26: a).
% 186.48/26.66 thf(func_def_104, type, sK27: (a > real)).
% 186.48/26.66 thf(func_def_105, type, sK28: (a > real)).
% 186.48/26.66 thf(func_def_106, type, sK29: a).
% 186.48/26.66 thf(func_def_107, type, sK30: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_108, type, sK31: (a > real)).
% 186.48/26.66 thf(func_def_109, type, sK32: (a > real)).
% 186.48/26.66 thf(func_def_110, type, sK33: (set_a > set_a > a)).
% 186.48/26.66 thf(func_def_111, type, sK34: (a > real > a)).
% 186.48/26.66 thf(func_def_112, type, sK35: (real > real > a)).
% 186.48/26.66 thf(func_def_113, type, sK36: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_114, type, sK37: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_115, type, sK38: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_116, type, sK39: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_117, type, sK40: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_118, type, sK41: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_119, type, sK42: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_120, type, sK43: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_121, type, sK44: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_122, type, sK45: (a > a)).
% 186.48/26.66 thf(func_def_123, type, sK46: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_124, type, sK47: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_125, type, sK48: ((a > $o) > (a > $o) > a)).
% 186.48/26.66 thf(func_def_126, type, db3: !>[X0: $tType]:(X0)).
% 186.48/26.66 thf(func_def_127, type, sK49: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_128, type, sK50: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_129, type, sK51: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_130, type, sK52: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_131, type, sK53: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_132, type, sK54: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_133, type, sK55: (real > real)).
% 186.48/26.66 thf(func_def_134, type, sK56: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_135, type, sK57: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_136, type, sK58: (real > real > real > real > real)).
% 186.48/26.66 thf(func_def_137, type, sK59: (real > real > real > real > real)).
% 186.48/26.66 thf(func_def_138, type, sK60: (real > real > real > real > real)).
% 186.48/26.66 thf(func_def_139, type, sK61: (real > real > real > real > real)).
% 186.48/26.66 thf(func_def_140, type, sK62: (real > real > real > real > real)).
% 186.48/26.66 thf(func_def_141, type, sK63: (real > real > real > real > real)).
% 186.48/26.66 thf(func_def_142, type, sK64: (real > real > real > real > real)).
% 186.48/26.66 thf(func_def_143, type, sK65: ((real > $o) > (real > $o) > real)).
% 186.48/26.66 thf(func_def_144, type, sK66: ((real > $o) > (real > $o) > real)).
% 186.48/26.66 thf(func_def_145, type, sK67: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_146, type, sK68: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_147, type, sK69: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_148, type, sK70: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_149, type, sK71: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_150, type, sK72: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_151, type, sK73: (a > a > a)).
% 186.48/26.66 thf(func_def_152, type, sK74: (real > real > real > real > real)).
% 186.48/26.66 thf(func_def_153, type, sK75: (real > real > real > real > real)).
% 186.48/26.66 thf(func_def_154, type, sK76: (set_a > a)).
% 186.48/26.66 thf(func_def_155, type, sK77: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_156, type, sK78: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_157, type, sK79: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_158, type, sK80: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_159, type, sK81: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_160, type, sK82: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_161, type, sK83: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_162, type, sK84: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_163, type, sK85: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_164, type, sK86: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_165, type, sK87: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_166, type, sK88: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_167, type, sK89: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_168, type, sK90: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_169, type, sK91: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_170, type, sK92: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_171, type, sK93: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_172, type, sK94: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_173, type, sK95: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_174, type, sK96: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_175, type, sK97: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_176, type, sK98: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_177, type, sK99: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_178, type, sK100: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_179, type, sK101: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_180, type, sK102: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_181, type, sK103: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_182, type, sK104: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_183, type, sK105: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_184, type, sK106: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_185, type, sK107: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_186, type, sK108: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_187, type, sK109: (set_real > set_real > real)).
% 186.48/26.66 thf(func_def_188, type, sK110: (set_a > a)).
% 186.48/26.66 thf(f1,axiom,(
% 186.48/26.66 (ord_less_real @ zero_zero_real @ d)),
% 186.48/26.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_d_I1_J)).
% 186.48/26.66 thf(f9,axiom,(
% 186.48/26.66 ! [X0 : a] : ((member_a @ X0 @ (elemen49976720ball_a @ x2 @ d)) => ((ord_less_real @ zero_zero_real @ (inner_1173012732nner_a @ (f @ X0) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b)))) & (((f @ X0)) != zero_zero_a) & (member_a @ X0 @ x)))),
% 186.48/26.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_8_d_I2_J)).
% 186.48/26.66 thf(f12,axiom,(
% 186.48/26.66 ~ ! [X0 : a] : ((member_a @ X0 @ (elemen49976720ball_a @ x2 @ d)) => ~ ! [X1 : a] : ((member_a @ X1 @ (elemen49976720ball_a @ x2 @ d)) => (ord_less_eq_real @ (inner_1173012732nner_a @ (f @ X0) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))) @ (inner_1173012732nner_a @ (f @ X1) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))))))),
% 186.48/26.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_11__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062s_O_A_092_060lbrakk_062s_A_092_060in_062_Acball_Ax_Ad_059_A_092_060forall_062x_092_060in_062cball_Ax_Ad_O_Af_As_A_092_060bullet_062_Arot_A_Ia_A_N_Ab_J_A_092_060le_062_Af_Ax_A_092_060bullet_062_Arot_A_Ia_A_N_Ab_J_092_060rbrakk_062_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062)).
% 186.48/26.66 thf(f23,axiom,(
% 186.48/26.66 ! [X0 : a] : (((inner_1173012732nner_a @ zero_zero_a @ X0)) = zero_zero_real)),
% 186.48/26.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_22_inner__zero__left)).
% 186.48/26.66 thf(f46,axiom,(
% 186.48/26.66 ! [X0 : real] : (((minus_minus_real @ X0 @ zero_zero_real)) = X0)),
% 186.48/26.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_45_diff__0__right)).
% 186.48/26.66 thf(f86,axiom,(
% 186.48/26.66 ! [X2 : real,X1 : real,X0 : real] : ((ord_less_eq_real @ X0 @ X1) => (ord_less_eq_real @ (minus_minus_real @ X2 @ X1) @ (minus_minus_real @ X2 @ X0)))),
% 186.48/26.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_85_diff__left__mono)).
% 186.48/26.66 thf(f102,axiom,(
% 186.48/26.66 ! [X0 : a,X2 : real,X3 : real,X1 : a] : ((member_a @ X0 @ (elemen49976720ball_a @ X1 @ X2)) => ((ord_less_eq_real @ X2 @ X3) => (member_a @ X0 @ (elemen49976720ball_a @ X1 @ X3))))),
% 186.48/26.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_101_mem__cball__leI)).
% 186.48/26.66 thf(f107,axiom,(
% 186.48/26.66 ! [X0 : a] : (ord_less_eq_real @ zero_zero_real @ (inner_1173012732nner_a @ X0 @ X0))),
% 186.48/26.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_106_inner__ge__zero)).
% 186.48/26.66 thf(f125,axiom,(
% 186.48/26.66 ((^[X0 : real, X1 : real] : ((ord_less_eq_real @ X0 @ X1) & ~(ord_less_eq_real @ X1 @ X0))) = ord_less_real)),
% 186.48/26.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_124_eucl__less__le__not__le)).
% 186.48/26.66 thf(f247,axiom,(
% 186.48/26.66 ! [X0 : real,X1 : real] : ((X0 = X1) | ~(ord_less_eq_real @ X0 @ X1) | ~(ord_less_eq_real @ X1 @ X0))),
% 186.48/26.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_246_verit__la__disequality)).
% 186.48/26.66 thf(f283,axiom,(
% 186.48/26.66 ! [X1 : real,X0 : real] : (~(ord_less_eq_real @ X0 @ X1) = ((ord_less_real @ X1 @ X0)))),
% 186.48/26.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_282_verit__comp__simplify1_I3_J)).
% 186.48/26.66 thf(f353,conjecture,(
% 186.48/26.66 ? [X0 : real] : ((ord_less_real @ zero_zero_real @ X0) & ? [X1 : real] : (! [X2 : a] : ((member_a @ X2 @ (elemen49976720ball_a @ x2 @ X0)) => (ord_less_eq_real @ X1 @ (inner_1173012732nner_a @ (f @ X2) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))))) & (ord_less_real @ zero_zero_real @ X1)))),
% 186.48/26.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0)).
% 186.48/26.66 thf(f354,negated_conjecture,(
% 186.48/26.66 ~ ? [X0 : real] : ((ord_less_real @ zero_zero_real @ X0) & ? [X1 : real] : (! [X2 : a] : ((member_a @ X2 @ (elemen49976720ball_a @ x2 @ X0)) => (ord_less_eq_real @ X1 @ (inner_1173012732nner_a @ (f @ X2) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))))) & (ord_less_real @ zero_zero_real @ X1)))),
% 186.48/26.66 inference(negated_conjecture,[status(cth)],[f353])).
% 186.48/26.66 thf(f400,plain,(
% 186.48/26.66 (ord_less_real @ zero_zero_real @ d)),
% 186.48/26.66 inference(rectify,[],[f1])).
% 186.48/26.66 thf(f401,plain,(
% 186.48/26.66 (((ord_less_real @ zero_zero_real @ d)) = $true)),
% 186.48/26.66 inference(fool_elimination,[],[f400])).
% 186.48/26.66 thf(f406,plain,(
% 186.48/26.66 ! [X0 : a] : (ord_less_eq_real @ zero_zero_real @ (inner_1173012732nner_a @ X0 @ X0))),
% 186.48/26.66 inference(rectify,[],[f107])).
% 186.48/26.66 thf(f407,plain,(
% 186.48/26.66 ! [X0 : a] : (((ord_less_eq_real @ zero_zero_real @ (inner_1173012732nner_a @ X0 @ X0))) = $true)),
% 186.48/26.66 inference(fool_elimination,[],[f406])).
% 186.48/26.66 thf(f499,plain,(
% 186.48/26.66 ! [X0 : a,X1 : real,X2 : real,X3 : a] : ((member_a @ X0 @ (elemen49976720ball_a @ X3 @ X1)) => ((ord_less_eq_real @ X1 @ X2) => (member_a @ X0 @ (elemen49976720ball_a @ X3 @ X2))))),
% 186.48/26.66 inference(rectify,[],[f102])).
% 186.48/26.66 thf(f500,plain,(
% 186.48/26.66 ! [X0 : a,X1 : real,X3 : a,X2 : real] : (($true = ((member_a @ X0 @ (elemen49976720ball_a @ X3 @ X1)))) => (($true = ((ord_less_eq_real @ X1 @ X2))) => ($true = ((member_a @ X0 @ (elemen49976720ball_a @ X3 @ X2))))))),
% 186.48/26.66 inference(fool_elimination,[],[f499])).
% 186.48/26.66 thf(f560,plain,(
% 186.48/26.66 ((^[X0 : real, X1 : real] : ((ord_less_eq_real @ X0 @ X1) & ~(ord_less_eq_real @ X1 @ X0))) = ord_less_real)),
% 186.48/26.66 inference(rectify,[],[f125])).
% 186.48/26.66 thf(f561,plain,(
% 186.48/26.66 (ord_less_real = (^[Y0 : real]: ((^[Y1 : real]: ((~ (ord_less_eq_real @ Y1 @ Y0)) & (ord_less_eq_real @ Y0 @ Y1))))))),
% 186.48/26.66 inference(fool_elimination,[],[f560])).
% 186.48/26.66 thf(f580,plain,(
% 186.48/26.66 ~ ? [X0 : real] : ((ord_less_real @ zero_zero_real @ X0) & ? [X1 : real] : (! [X2 : a] : ((member_a @ X2 @ (elemen49976720ball_a @ x2 @ X0)) => (ord_less_eq_real @ X1 @ (inner_1173012732nner_a @ (f @ X2) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))))) & (ord_less_real @ zero_zero_real @ X1)))),
% 186.48/26.66 inference(rectify,[],[f354])).
% 186.48/26.66 thf(f581,plain,(
% 186.48/26.66 ~ ? [X0 : real] : (? [X1 : real] : ((((ord_less_real @ zero_zero_real @ X1)) = $true) & ! [X2 : a] : ((((member_a @ X2 @ (elemen49976720ball_a @ x2 @ X0))) = $true) => (((ord_less_eq_real @ X1 @ (inner_1173012732nner_a @ (f @ X2) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))))) = $true))) & (((ord_less_real @ zero_zero_real @ X0)) = $true))),
% 186.48/26.66 inference(fool_elimination,[],[f580])).
% 186.48/26.66 thf(f610,plain,(
% 186.48/26.66 ! [X0 : a] : ((member_a @ X0 @ (elemen49976720ball_a @ x2 @ d)) => ((ord_less_real @ zero_zero_real @ (inner_1173012732nner_a @ (f @ X0) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b)))) & (((f @ X0)) != zero_zero_a) & (member_a @ X0 @ x)))),
% 186.48/26.66 inference(rectify,[],[f9])).
% 186.48/26.66 thf(f611,plain,(
% 186.48/26.66 ! [X0 : a] : ((((member_a @ X0 @ (elemen49976720ball_a @ x2 @ d))) = $true) => ((((member_a @ X0 @ x)) = $true) & (((f @ X0)) != zero_zero_a) & (((ord_less_real @ zero_zero_real @ (inner_1173012732nner_a @ (f @ X0) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))))) = $true)))),
% 186.48/26.66 inference(fool_elimination,[],[f610])).
% 186.48/26.66 thf(f736,plain,(
% 186.48/26.66 ~ ! [X0 : a] : ((member_a @ X0 @ (elemen49976720ball_a @ x2 @ d)) => ~ ! [X1 : a] : ((member_a @ X1 @ (elemen49976720ball_a @ x2 @ d)) => (ord_less_eq_real @ (inner_1173012732nner_a @ (f @ X0) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))) @ (inner_1173012732nner_a @ (f @ X1) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))))))),
% 186.48/26.66 inference(rectify,[],[f12])).
% 186.48/26.66 thf(f737,plain,(
% 186.48/26.66 ~ ! [X0 : a] : ((((member_a @ X0 @ (elemen49976720ball_a @ x2 @ d))) = $true) => ~ ! [X1 : a] : ((((member_a @ X1 @ (elemen49976720ball_a @ x2 @ d))) = $true) => (((ord_less_eq_real @ (inner_1173012732nner_a @ (f @ X0) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))) @ (inner_1173012732nner_a @ (f @ X1) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))))) = $true)))),
% 186.48/26.66 inference(fool_elimination,[],[f736])).
% 186.48/26.66 thf(f738,plain,(
% 186.48/26.66 ! [X0 : real,X1 : real,X2 : real] : ((ord_less_eq_real @ X2 @ X1) => (ord_less_eq_real @ (minus_minus_real @ X0 @ X1) @ (minus_minus_real @ X0 @ X2)))),
% 186.48/26.66 inference(rectify,[],[f86])).
% 186.48/26.66 thf(f739,plain,(
% 186.48/26.66 ! [X2 : real,X1 : real,X0 : real] : (($true = ((ord_less_eq_real @ X2 @ X1))) => (((ord_less_eq_real @ (minus_minus_real @ X0 @ X1) @ (minus_minus_real @ X0 @ X2))) = $true))),
% 186.48/26.66 inference(fool_elimination,[],[f738])).
% 186.48/26.66 thf(f758,plain,(
% 186.48/26.66 ! [X0 : real,X1 : real] : ((X0 = X1) | ~(ord_less_eq_real @ X0 @ X1) | ~(ord_less_eq_real @ X1 @ X0))),
% 186.48/26.66 inference(rectify,[],[f247])).
% 186.48/26.66 thf(f759,plain,(
% 186.48/26.66 ! [X0 : real,X1 : real] : ((X0 = X1) | ~ (((ord_less_eq_real @ X0 @ X1)) = $true) | ~ (((ord_less_eq_real @ X1 @ X0)) = $true))),
% 186.48/26.66 inference(fool_elimination,[],[f758])).
% 186.48/26.66 thf(f823,plain,(
% 186.48/26.66 ! [X0 : real,X1 : real] : (~(ord_less_eq_real @ X1 @ X0) = ((ord_less_real @ X0 @ X1)))),
% 186.48/26.66 inference(rectify,[],[f283])).
% 186.48/26.66 thf(f824,plain,(
% 186.48/26.66 ! [X1 : real,X0 : real] : (((ord_less_real @ X0 @ X1)) = ((~ (ord_less_eq_real @ X1 @ X0))))),
% 186.48/26.66 inference(fool_elimination,[],[f823])).
% 186.48/26.66 thf(f872,plain,(
% 186.48/26.66 ! [X0 : real,X1 : real] : ((((ord_less_eq_real @ X1 @ X0)) != $true) | (X0 = X1) | (((ord_less_eq_real @ X0 @ X1)) != $true))),
% 186.48/26.66 inference(flattening,[],[f759])).
% 186.48/26.66 thf(f981,plain,(
% 186.48/26.66 ! [X0 : a] : ((((member_a @ X0 @ (elemen49976720ball_a @ x2 @ d))) != $true) | ((((member_a @ X0 @ x)) = $true) & (((f @ X0)) != zero_zero_a) & (((ord_less_real @ zero_zero_real @ (inner_1173012732nner_a @ (f @ X0) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))))) = $true)))),
% 186.48/26.66 inference(ennf_transformation,[],[f611])).
% 186.48/26.66 thf(f983,plain,(
% 186.48/26.66 ! [X0 : a,X1 : real,X3 : a,X2 : real] : ((($true = ((member_a @ X0 @ (elemen49976720ball_a @ X3 @ X2)))) | ($true != ((ord_less_eq_real @ X1 @ X2)))) | ($true != ((member_a @ X0 @ (elemen49976720ball_a @ X3 @ X1)))))),
% 186.48/26.66 inference(ennf_transformation,[],[f500])).
% 186.48/26.66 thf(f984,plain,(
% 186.48/26.66 ! [X0 : a,X2 : real,X3 : a,X1 : real] : (($true = ((member_a @ X0 @ (elemen49976720ball_a @ X3 @ X2)))) | ($true != ((member_a @ X0 @ (elemen49976720ball_a @ X3 @ X1)))) | ($true != ((ord_less_eq_real @ X1 @ X2))))),
% 186.48/26.66 inference(flattening,[],[f983])).
% 186.48/26.66 thf(f1013,plain,(
% 186.48/26.66 ? [X0 : a] : ((((member_a @ X0 @ (elemen49976720ball_a @ x2 @ d))) = $true) & ! [X1 : a] : ((((ord_less_eq_real @ (inner_1173012732nner_a @ (f @ X0) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))) @ (inner_1173012732nner_a @ (f @ X1) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))))) = $true) | (((member_a @ X1 @ (elemen49976720ball_a @ x2 @ d))) != $true)))),
% 186.48/26.66 inference(ennf_transformation,[],[f737])).
% 186.48/26.66 thf(f1031,plain,(
% 186.48/26.66 ! [X0 : real] : ((((ord_less_real @ zero_zero_real @ X0)) != $true) | ! [X1 : real] : (? [X2 : a] : ((((member_a @ X2 @ (elemen49976720ball_a @ x2 @ X0))) = $true) & (((ord_less_eq_real @ X1 @ (inner_1173012732nner_a @ (f @ X2) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))))) != $true)) | (((ord_less_real @ zero_zero_real @ X1)) != $true)))),
% 186.48/26.66 inference(ennf_transformation,[],[f581])).
% 186.48/26.66 thf(f1083,plain,(
% 186.48/26.66 ! [X1 : real,X2 : real,X0 : real] : (($true != ((ord_less_eq_real @ X2 @ X1))) | (((ord_less_eq_real @ (minus_minus_real @ X0 @ X1) @ (minus_minus_real @ X0 @ X2))) = $true))),
% 186.48/26.66 inference(ennf_transformation,[],[f739])).
% 186.48/26.66 thf(f1111,definition,(
% 186.48/26.66 ! [X0 : a] : (((((member_a @ X0 @ x)) = $true) & (((f @ X0)) != zero_zero_a) & (((ord_less_real @ zero_zero_real @ (inner_1173012732nner_a @ (f @ X0) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))))) = $true)) | ~ ($true = ((sP4 @ X0))))),
% 186.48/26.66 introduced(definition,[new_symbols(definition,[=])],[predicate_definition_introduction])).
% 186.48/26.66 thf(f1112,plain,(
% 186.48/26.66 ! [X0 : a] : ((((member_a @ X0 @ (elemen49976720ball_a @ x2 @ d))) != $true) | ($true = ((sP4 @ X0))))),
% 186.48/26.66 inference(definition_folding,[],[f981,f1111])).
% 186.48/26.66 thf(f1174,plain,(
% 186.48/26.66 ! [X0 : a] : (((((member_a @ X0 @ x)) = $true) & (((f @ X0)) != zero_zero_a) & (((ord_less_real @ zero_zero_real @ (inner_1173012732nner_a @ (f @ X0) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))))) = $true)) | ($true != ((sP4 @ X0))))),
% 186.48/26.66 inference(nnf_transformation,[],[f1111])).
% 186.48/26.66 thf(f1189,plain,(
% 186.48/26.66 ! [X0 : real,X1 : real] : (((ord_less_real @ X1 @ X0)) = ((~ (ord_less_eq_real @ X0 @ X1))))),
% 186.48/26.66 inference(rectify,[],[f824])).
% 186.48/26.66 thf(f1204,plain,(
% 186.48/26.66 ($true = ((member_a @ sK26 @ (elemen49976720ball_a @ x2 @ d)))) & ! [X1 : a] : (($true = ((ord_less_eq_real @ (inner_1173012732nner_a @ (f @ sK26) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))) @ (inner_1173012732nner_a @ (f @ X1) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b)))))) | (((member_a @ X1 @ (elemen49976720ball_a @ x2 @ d))) != $true))),
% 186.48/26.66 inference(skolemize,[status(esa),new_symbols(skolem,[sK26]),skolemize(X0,sK26)],[f1013])).
% 186.48/26.66 thf(f1232,plain,(
% 186.48/26.66 ! [X0 : real,X1 : real,X2 : real] : ((((ord_less_eq_real @ X1 @ X0)) != $true) | ($true = ((ord_less_eq_real @ (minus_minus_real @ X2 @ X0) @ (minus_minus_real @ X2 @ X1)))))),
% 186.48/26.66 inference(rectify,[],[f1083])).
% 186.48/26.66 thf(f1236,plain,(
% 186.48/26.66 ! [X0 : a,X1 : real,X2 : a,X3 : real] : (($true = ((member_a @ X0 @ (elemen49976720ball_a @ X2 @ X1)))) | ($true != ((member_a @ X0 @ (elemen49976720ball_a @ X2 @ X3)))) | ($true != ((ord_less_eq_real @ X3 @ X1))))),
% 186.48/26.66 inference(rectify,[],[f984])).
% 186.48/26.66 thf(f1285,plain,(
% 186.48/26.66 ! [X0 : real] : ((((ord_less_real @ zero_zero_real @ X0)) != $true) | ! [X1 : real] : ((($true = ((member_a @ (sK35 @ X1 @ X0) @ (elemen49976720ball_a @ x2 @ X0)))) & ($true != ((ord_less_eq_real @ X1 @ (inner_1173012732nner_a @ (f @ (sK35 @ X1 @ X0)) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))))))) | (((ord_less_real @ zero_zero_real @ X1)) != $true)))),
% 186.48/26.66 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP]),skolemize(X1,sK10 @ X0)],[f1031])).
% 186.48/26.66 thf(f1309,plain,(
% 186.48/26.66 (ord_less_real = (^[Y0 : real]: ((^[Y1 : real]: ((~ (ord_less_eq_real @ Y1 @ Y0)) & (ord_less_eq_real @ Y0 @ Y1))))))),
% 186.48/26.66 inference(cnf_transformation,[],[f561])).
% 186.48/26.66 thf(f1318,plain,(
% 186.48/26.66 ( ! [X0 : real] : ((((minus_minus_real @ X0 @ zero_zero_real)) = X0)) )),
% 186.48/26.66 inference(cnf_transformation,[],[f46])).
% 186.48/26.66 thf(f1422,plain,(
% 186.48/26.66 ( ! [X0 : a] : ((((ord_less_real @ zero_zero_real @ (inner_1173012732nner_a @ (f @ X0) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))))) = $true) | ($true != ((sP4 @ X0)))) )),
% 186.48/26.66 inference(cnf_transformation,[],[f1174])).
% 186.48/26.66 thf(f1425,plain,(
% 186.48/26.66 ( ! [X0 : a] : ((((member_a @ X0 @ (elemen49976720ball_a @ x2 @ d))) != $true) | ($true = ((sP4 @ X0)))) )),
% 186.48/26.66 inference(cnf_transformation,[],[f1112])).
% 186.48/26.66 thf(f1457,plain,(
% 186.48/26.66 ( ! [X0 : real,X1 : real] : ((((ord_less_real @ X1 @ X0)) = ((~ (ord_less_eq_real @ X0 @ X1))))) )),
% 186.48/26.66 inference(cnf_transformation,[],[f1189])).
% 186.48/26.66 thf(f1488,plain,(
% 186.48/26.66 ( ! [X1 : a] : ((((member_a @ X1 @ (elemen49976720ball_a @ x2 @ d))) != $true) | ($true = ((ord_less_eq_real @ (inner_1173012732nner_a @ (f @ sK26) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))) @ (inner_1173012732nner_a @ (f @ X1) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))))))) )),
% 186.48/26.66 inference(cnf_transformation,[],[f1204])).
% 186.48/26.66 thf(f1489,plain,(
% 186.48/26.66 ($true = ((member_a @ sK26 @ (elemen49976720ball_a @ x2 @ d))))),
% 186.48/26.66 inference(cnf_transformation,[],[f1204])).
% 186.48/26.66 thf(f1553,plain,(
% 186.48/26.66 ( ! [X2 : real,X0 : real,X1 : real] : ((((ord_less_eq_real @ X1 @ X0)) != $true) | ($true = ((ord_less_eq_real @ (minus_minus_real @ X2 @ X0) @ (minus_minus_real @ X2 @ X1))))) )),
% 186.48/26.66 inference(cnf_transformation,[],[f1232])).
% 186.48/26.66 thf(f1559,plain,(
% 186.48/26.66 ( ! [X2 : a,X3 : real,X0 : a,X1 : real] : (($true != ((member_a @ X0 @ (elemen49976720ball_a @ X2 @ X3)))) | ($true != ((ord_less_eq_real @ X3 @ X1))) | ($true = ((member_a @ X0 @ (elemen49976720ball_a @ X2 @ X1))))) )),
% 186.48/26.66 inference(cnf_transformation,[],[f1236])).
% 186.48/26.66 thf(f1612,plain,(
% 186.48/26.66 ( ! [X0 : a] : ((zero_zero_real = ((inner_1173012732nner_a @ zero_zero_a @ X0)))) )),
% 186.48/26.66 inference(cnf_transformation,[],[f23])).
% 186.48/26.66 thf(f1624,plain,(
% 186.48/26.66 ( ! [X0 : real,X1 : real] : ((((ord_less_eq_real @ X1 @ X0)) != $true) | (((ord_less_eq_real @ X0 @ X1)) != $true) | (X0 = X1)) )),
% 186.48/26.66 inference(cnf_transformation,[],[f872])).
% 186.48/26.66 thf(f1652,plain,(
% 186.48/26.66 ( ! [X0 : a] : ((((ord_less_eq_real @ zero_zero_real @ (inner_1173012732nner_a @ X0 @ X0))) = $true)) )),
% 186.48/26.66 inference(cnf_transformation,[],[f407])).
% 186.48/26.66 thf(f1655,plain,(
% 186.48/26.66 (((ord_less_real @ zero_zero_real @ d)) = $true)),
% 186.48/26.66 inference(cnf_transformation,[],[f401])).
% 186.48/26.66 thf(f1680,plain,(
% 186.48/26.66 ( ! [X0 : real,X1 : real] : ((((ord_less_real @ zero_zero_real @ X0)) != $true) | ($true != ((ord_less_eq_real @ X1 @ (inner_1173012732nner_a @ (f @ (sK35 @ X1 @ X0)) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b)))))) | (((ord_less_real @ zero_zero_real @ X1)) != $true)) )),
% 186.48/26.66 inference(cnf_transformation,[],[f1285])).
% 186.48/26.66 thf(f1681,plain,(
% 186.48/26.66 ( ! [X0 : real,X1 : real] : ((((ord_less_real @ zero_zero_real @ X0)) != $true) | ($true = ((member_a @ (sK35 @ X1 @ X0) @ (elemen49976720ball_a @ x2 @ X0)))) | (((ord_less_real @ zero_zero_real @ X1)) != $true)) )),
% 186.48/26.66 inference(cnf_transformation,[],[f1285])).
% 186.48/26.66 thf(f1706,definition,(
% 186.48/26.66 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 186.48/26.66 introduced(theory,[fool_exhaustiveness_axiom])).
% 186.48/26.66 thf(f1755,plain,(
% 186.48/26.66 ( ! [X0 : a] : (($true = (((^[Y0 : real]: ((^[Y1 : real]: ((~ (ord_less_eq_real @ Y1 @ Y0)) & (ord_less_eq_real @ Y0 @ Y1))))) @ zero_zero_real @ (inner_1173012732nner_a @ (f @ X0) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b)))))) | ($true != ((sP4 @ X0)))) )),
% 186.48/26.66 inference(definition_unfolding,[],[f1422,f1309])).
% 186.48/26.66 thf(f1767,plain,(
% 186.48/26.66 ( ! [X0 : real,X1 : real] : (((((^[Y0 : real]: ((^[Y1 : real]: ((~ (ord_less_eq_real @ Y1 @ Y0)) & (ord_less_eq_real @ Y0 @ Y1))))) @ X1 @ X0)) = ((~ (ord_less_eq_real @ X0 @ X1))))) )),
% 186.48/26.66 inference(definition_unfolding,[],[f1457,f1309])).
% 186.48/26.66 thf(f1858,plain,(
% 186.48/26.66 ($true = (((^[Y0 : real]: ((^[Y1 : real]: ((~ (ord_less_eq_real @ Y1 @ Y0)) & (ord_less_eq_real @ Y0 @ Y1))))) @ zero_zero_real @ d)))),
% 186.48/26.66 inference(definition_unfolding,[],[f1655,f1309])).
% 186.48/26.66 thf(f1869,plain,(
% 186.48/26.66 ( ! [X0 : real,X1 : real] : (((((^[Y0 : real]: ((^[Y1 : real]: ((~ (ord_less_eq_real @ Y1 @ Y0)) & (ord_less_eq_real @ Y0 @ Y1))))) @ zero_zero_real @ X1)) != $true) | ($true = ((member_a @ (sK35 @ X1 @ X0) @ (elemen49976720ball_a @ x2 @ X0)))) | ($true != (((^[Y0 : real]: ((^[Y1 : real]: ((~ (ord_less_eq_real @ Y1 @ Y0)) & (ord_less_eq_real @ Y0 @ Y1))))) @ zero_zero_real @ X0)))) )),
% 186.48/26.66 inference(definition_unfolding,[],[f1681,f1309,f1309])).
% 186.48/26.66 thf(f1870,plain,(
% 186.48/26.66 ( ! [X0 : real,X1 : real] : (((((^[Y0 : real]: ((^[Y1 : real]: ((~ (ord_less_eq_real @ Y1 @ Y0)) & (ord_less_eq_real @ Y0 @ Y1))))) @ zero_zero_real @ X1)) != $true) | ($true != ((ord_less_eq_real @ X1 @ (inner_1173012732nner_a @ (f @ (sK35 @ X1 @ X0)) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b)))))) | ($true != (((^[Y0 : real]: ((^[Y1 : real]: ((~ (ord_less_eq_real @ Y1 @ Y0)) & (ord_less_eq_real @ Y0 @ Y1))))) @ zero_zero_real @ X0)))) )),
% 186.48/26.66 inference(definition_unfolding,[],[f1680,f1309,f1309])).
% 186.48/26.66 thf(f2010,plain,(
% 186.48/26.66 ( ! [X0 : a] : (($true != ((sP4 @ X0))) | ($true = (((~ (ord_less_eq_real @ (inner_1173012732nner_a @ (f @ X0) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))) @ zero_zero_real)) & (ord_less_eq_real @ zero_zero_real @ (inner_1173012732nner_a @ (f @ X0) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b)))))))) )),
% 186.48/26.66 inference(beta-eta_normalization,[],[f1755])).
% 186.48/26.66 thf(f2011,plain,(
% 186.48/26.66 ( ! [X0 : a] : (($true != ((sP4 @ X0))) | ($true = ((ord_less_eq_real @ zero_zero_real @ (inner_1173012732nner_a @ (f @ X0) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))))))) )),
% 186.48/26.66 inference(and_proxy_clausification,[],[f2010])).
% 186.48/26.66 thf(f2012,plain,(
% 186.48/26.66 ( ! [X0 : a] : (($true = ((~ (ord_less_eq_real @ (inner_1173012732nner_a @ (f @ X0) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))) @ zero_zero_real)))) | ($true != ((sP4 @ X0)))) )),
% 186.48/26.66 inference(and_proxy_clausification,[],[f2010])).
% 186.48/26.66 thf(f2013,plain,(
% 186.48/26.66 ( ! [X0 : a] : (($true != ((sP4 @ X0))) | ($false = ((ord_less_eq_real @ (inner_1173012732nner_a @ (f @ X0) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))) @ zero_zero_real)))) )),
% 186.48/26.66 inference(not_proxy_clausification,[],[f2012])).
% 186.48/26.66 thf(f2736,plain,(
% 186.48/26.66 ( ! [X0 : real,X1 : real] : (($true != (((~ (ord_less_eq_real @ X0 @ zero_zero_real)) & (ord_less_eq_real @ zero_zero_real @ X0)))) | ($true != (((~ (ord_less_eq_real @ X1 @ zero_zero_real)) & (ord_less_eq_real @ zero_zero_real @ X1)))) | ($true = ((member_a @ (sK35 @ X1 @ X0) @ (elemen49976720ball_a @ x2 @ X0))))) )),
% 186.48/26.66 inference(beta-eta_normalization,[],[f1869])).
% 186.48/26.66 thf(f2737,plain,(
% 186.48/26.66 ( ! [X0 : real,X1 : real] : ((((~ (ord_less_eq_real @ X0 @ zero_zero_real))) = $false) | ($true != (((~ (ord_less_eq_real @ X1 @ zero_zero_real)) & (ord_less_eq_real @ zero_zero_real @ X1)))) | ($true = ((member_a @ (sK35 @ X1 @ X0) @ (elemen49976720ball_a @ x2 @ X0)))) | (((ord_less_eq_real @ zero_zero_real @ X0)) = $false)) )),
% 186.48/26.66 inference(and_proxy_clausification,[],[f2736])).
% 186.48/26.66 thf(f2738,plain,(
% 186.48/26.66 ( ! [X0 : real,X1 : real] : (($true = ((member_a @ (sK35 @ X1 @ X0) @ (elemen49976720ball_a @ x2 @ X0)))) | (((ord_less_eq_real @ zero_zero_real @ X0)) = $false) | ($true != (((~ (ord_less_eq_real @ X1 @ zero_zero_real)) & (ord_less_eq_real @ zero_zero_real @ X1)))) | (((ord_less_eq_real @ X0 @ zero_zero_real)) = $true)) )),
% 186.48/26.66 inference(not_proxy_clausification,[],[f2737])).
% 186.48/26.66 thf(f2739,plain,(
% 186.48/26.66 ( ! [X0 : real,X1 : real] : (($false = ((~ (ord_less_eq_real @ X1 @ zero_zero_real)))) | ($true = ((member_a @ (sK35 @ X1 @ X0) @ (elemen49976720ball_a @ x2 @ X0)))) | (((ord_less_eq_real @ zero_zero_real @ X1)) = $false) | (((ord_less_eq_real @ zero_zero_real @ X0)) = $false) | (((ord_less_eq_real @ X0 @ zero_zero_real)) = $true)) )),
% 186.48/26.66 inference(and_proxy_clausification,[],[f2738])).
% 186.48/26.66 thf(f2740,plain,(
% 186.48/26.66 ( ! [X0 : real,X1 : real] : (($true = ((member_a @ (sK35 @ X1 @ X0) @ (elemen49976720ball_a @ x2 @ X0)))) | (((ord_less_eq_real @ zero_zero_real @ X0)) = $false) | ($true = ((ord_less_eq_real @ X1 @ zero_zero_real))) | (((ord_less_eq_real @ zero_zero_real @ X1)) = $false) | (((ord_less_eq_real @ X0 @ zero_zero_real)) = $true)) )),
% 186.48/26.66 inference(not_proxy_clausification,[],[f2739])).
% 186.48/26.66 thf(f2966,plain,(
% 186.48/26.66 ( ! [X0 : real,X1 : real] : (($true = (((^[Y0 : real]: ((^[Y1 : real]: ((~ (ord_less_eq_real @ Y1 @ Y0)) & (ord_less_eq_real @ Y0 @ Y1))))) @ X1 @ X0))) | ($false = ((~ (ord_less_eq_real @ X0 @ X1))))) )),
% 186.48/26.66 inference(iff_proxy_clausification,[],[f1767])).
% 186.48/26.66 thf(f2972,plain,(
% 186.48/26.66 ( ! [X0 : real,X1 : real] : (($true = (((^[Y0 : real]: ((^[Y1 : real]: ((~ (ord_less_eq_real @ Y1 @ Y0)) & (ord_less_eq_real @ Y0 @ Y1))))) @ X1 @ X0))) | (((ord_less_eq_real @ X0 @ X1)) = $true)) )),
% 186.48/26.66 inference(not_proxy_clausification,[],[f2966])).
% 186.48/26.66 thf(f2973,plain,(
% 186.48/26.66 ( ! [X0 : real,X1 : real] : ((((ord_less_eq_real @ X0 @ X1)) = $true) | ((((~ (ord_less_eq_real @ X0 @ X1)) & (ord_less_eq_real @ X1 @ X0))) = $true)) )),
% 186.48/26.66 inference(beta-eta_normalization,[],[f2972])).
% 186.48/26.66 thf(f2974,plain,(
% 186.48/26.66 ( ! [X0 : real,X1 : real] : ((((ord_less_eq_real @ X1 @ X0)) = $true) | (((ord_less_eq_real @ X0 @ X1)) = $true)) )),
% 186.48/26.66 inference(and_proxy_clausification,[],[f2973])).
% 186.48/26.66 thf(f3245,plain,(
% 186.48/26.66 ( ! [X0 : real,X1 : real] : (($true != (((~ (ord_less_eq_real @ X1 @ zero_zero_real)) & (ord_less_eq_real @ zero_zero_real @ X1)))) | ($true != (((~ (ord_less_eq_real @ X0 @ zero_zero_real)) & (ord_less_eq_real @ zero_zero_real @ X0)))) | ($true != ((ord_less_eq_real @ X1 @ (inner_1173012732nner_a @ (f @ (sK35 @ X1 @ X0)) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))))))) )),
% 186.48/26.66 inference(beta-eta_normalization,[],[f1870])).
% 186.48/26.66 thf(f3246,plain,(
% 186.48/26.66 ( ! [X0 : real,X1 : real] : ((((ord_less_eq_real @ zero_zero_real @ X1)) = $false) | ($true != ((ord_less_eq_real @ X1 @ (inner_1173012732nner_a @ (f @ (sK35 @ X1 @ X0)) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b)))))) | ($false = ((~ (ord_less_eq_real @ X1 @ zero_zero_real)))) | ($true != (((~ (ord_less_eq_real @ X0 @ zero_zero_real)) & (ord_less_eq_real @ zero_zero_real @ X0))))) )),
% 186.48/26.66 inference(and_proxy_clausification,[],[f3245])).
% 186.48/26.66 thf(f3247,plain,(
% 186.48/26.66 ( ! [X0 : real,X1 : real] : (($true != ((ord_less_eq_real @ X1 @ (inner_1173012732nner_a @ (f @ (sK35 @ X1 @ X0)) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b)))))) | ($true = ((ord_less_eq_real @ X1 @ zero_zero_real))) | ($true != (((~ (ord_less_eq_real @ X0 @ zero_zero_real)) & (ord_less_eq_real @ zero_zero_real @ X0)))) | (((ord_less_eq_real @ zero_zero_real @ X1)) = $false)) )),
% 186.48/26.66 inference(not_proxy_clausification,[],[f3246])).
% 186.48/26.66 thf(f3248,plain,(
% 186.48/26.66 ( ! [X0 : real,X1 : real] : ((((ord_less_eq_real @ zero_zero_real @ X0)) = $false) | ($true != ((ord_less_eq_real @ X1 @ (inner_1173012732nner_a @ (f @ (sK35 @ X1 @ X0)) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b)))))) | (((ord_less_eq_real @ zero_zero_real @ X1)) = $false) | ($true = ((ord_less_eq_real @ X1 @ zero_zero_real))) | (((~ (ord_less_eq_real @ X0 @ zero_zero_real))) = $false)) )),
% 186.48/26.66 inference(and_proxy_clausification,[],[f3247])).
% 186.48/26.66 thf(f3249,plain,(
% 186.48/26.66 ( ! [X0 : real,X1 : real] : ((((ord_less_eq_real @ X0 @ zero_zero_real)) = $true) | ($true = ((ord_less_eq_real @ X1 @ zero_zero_real))) | (((ord_less_eq_real @ zero_zero_real @ X1)) = $false) | ($true != ((ord_less_eq_real @ X1 @ (inner_1173012732nner_a @ (f @ (sK35 @ X1 @ X0)) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b)))))) | (((ord_less_eq_real @ zero_zero_real @ X0)) = $false)) )),
% 186.48/26.66 inference(not_proxy_clausification,[],[f3248])).
% 186.48/26.66 thf(f3793,plain,(
% 186.48/26.66 ($true = (((~ (ord_less_eq_real @ d @ zero_zero_real)) & (ord_less_eq_real @ zero_zero_real @ d))))),
% 186.48/26.66 inference(beta-eta_normalization,[],[f1858])).
% 186.48/26.66 thf(f3795,plain,(
% 186.48/26.66 ($true = ((~ (ord_less_eq_real @ d @ zero_zero_real))))),
% 186.48/26.66 inference(and_proxy_clausification,[],[f3793])).
% 186.48/26.66 thf(f3796,plain,(
% 186.48/26.66 (((ord_less_eq_real @ d @ zero_zero_real)) = $false)),
% 186.48/26.66 inference(not_proxy_clausification,[],[f3795])).
% 186.48/26.66 thf(f3973,plain,(
% 186.48/26.66 ( ! [X0 : real,X1 : real] : ((((ord_less_eq_real @ X0 @ zero_zero_real)) = $true) | ($true = $false) | (((ord_less_eq_real @ zero_zero_real @ X0)) = $false) | ($true = ((ord_less_eq_real @ X1 @ zero_zero_real))) | ($true != ((ord_less_eq_real @ X1 @ (inner_1173012732nner_a @ (f @ (sK35 @ X1 @ X0)) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))))))) )),
% 186.48/26.66 inference(forward_subsumption_demodulation,[],[f3249,f2974])).
% 186.48/26.66 thf(f3974,plain,(
% 186.48/26.66 ( ! [X0 : real,X1 : real] : ((((ord_less_eq_real @ X0 @ zero_zero_real)) = $true) | ($true != ((ord_less_eq_real @ X1 @ (inner_1173012732nner_a @ (f @ (sK35 @ X1 @ X0)) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b)))))) | (((ord_less_eq_real @ zero_zero_real @ X0)) = $false) | ($true = ((ord_less_eq_real @ X1 @ zero_zero_real)))) )),
% 186.48/26.66 inference(trivial_inequality_removal,[],[f3973])).
% 186.48/26.66 thf(f4000,plain,(
% 186.48/26.66 ( ! [X0 : real,X1 : real] : (($true = ((ord_less_eq_real @ X1 @ zero_zero_real))) | (((ord_less_eq_real @ X0 @ zero_zero_real)) = $true) | ($true = $false) | ($true != ((ord_less_eq_real @ X1 @ (inner_1173012732nner_a @ (f @ (sK35 @ X1 @ X0)) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))))))) )),
% 186.48/26.66 inference(forward_subsumption_demodulation,[],[f3974,f2974])).
% 186.48/26.66 thf(f4001,plain,(
% 186.48/26.66 ( ! [X0 : real,X1 : real] : (($true != ((ord_less_eq_real @ X1 @ (inner_1173012732nner_a @ (f @ (sK35 @ X1 @ X0)) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b)))))) | ($true = ((ord_less_eq_real @ X1 @ zero_zero_real))) | (((ord_less_eq_real @ X0 @ zero_zero_real)) = $true)) )),
% 186.48/26.66 inference(trivial_inequality_removal,[],[f4000])).
% 186.48/26.66 thf(f4007,definition,(
% 186.48/26.66 spl111_7 <=> ($true = ((ord_less_eq_real @ zero_zero_real @ zero_zero_real)))),
% 186.48/26.66 introduced(definition,[new_symbols(definition,[spl111_7])],[avatar_definition])).
% 186.48/26.66 thf(f4009,plain,(
% 186.48/26.66 ($true = ((ord_less_eq_real @ zero_zero_real @ zero_zero_real))) | ~spl111_7),
% 186.48/26.66 inference(avatar_component_clause,[],[f4007])).
% 186.48/26.66 thf(f4058,plain,(
% 186.48/26.66 ($true = ((ord_less_eq_real @ zero_zero_real @ zero_zero_real)))),
% 186.48/26.66 inference(constrained_superposition,[],[f1652,f1612])).
% 186.48/26.66 thf(f4093,plain,(
% 186.48/26.66 ($true != $true) | (((sP4 @ sK26)) = $true)),
% 186.48/26.66 inference(constrained_superposition,[],[f1425,f1489])).
% 186.48/26.66 thf(f4095,plain,(
% 186.48/26.66 (((sP4 @ sK26)) = $true)),
% 186.48/26.66 inference(trivial_inequality_removal,[],[f4093])).
% 186.48/26.66 thf(f4295,plain,(
% 186.48/26.66 ( ! [X0 : real] : (($true != $true) | ($true = ((ord_less_eq_real @ (minus_minus_real @ X0 @ zero_zero_real) @ (minus_minus_real @ X0 @ zero_zero_real))))) ) | ~spl111_7),
% 186.48/26.66 inference(constrained_superposition,[],[f1553,f4009])).
% 186.48/26.66 thf(f4304,plain,(
% 186.48/26.66 ( ! [X0 : real] : (($true = ((ord_less_eq_real @ (minus_minus_real @ X0 @ zero_zero_real) @ (minus_minus_real @ X0 @ zero_zero_real))))) ) | ~spl111_7),
% 186.48/26.66 inference(trivial_inequality_removal,[],[f4295])).
% 186.48/26.66 thf(f4308,plain,(
% 186.48/26.66 ( ! [X0 : real] : (($true = ((ord_less_eq_real @ X0 @ X0)))) ) | ~spl111_7),
% 186.48/26.66 inference(forward_demodulation,[],[f4304,f1318])).
% 186.48/26.66 thf(f4566,plain,(
% 186.48/26.66 ( ! [X2 : real,X0 : real,X1 : real] : ((((ord_less_eq_real @ X0 @ zero_zero_real)) = $true) | ($true != $true) | (((ord_less_eq_real @ zero_zero_real @ X1)) = $false) | (((ord_less_eq_real @ zero_zero_real @ X0)) = $false) | ($true = ((ord_less_eq_real @ X1 @ zero_zero_real))) | ($true = ((member_a @ (sK35 @ X0 @ X1) @ (elemen49976720ball_a @ x2 @ X2)))) | ($true != ((ord_less_eq_real @ X1 @ X2)))) )),
% 186.48/26.66 inference(constrained_superposition,[],[f1559,f2740])).
% 186.48/26.66 thf(f4569,plain,(
% 186.48/26.66 ( ! [X2 : real,X0 : real,X1 : real] : (($true != ((ord_less_eq_real @ X1 @ X2))) | (((ord_less_eq_real @ X0 @ zero_zero_real)) = $true) | ($true = ((member_a @ (sK35 @ X0 @ X1) @ (elemen49976720ball_a @ x2 @ X2)))) | (((ord_less_eq_real @ zero_zero_real @ X0)) = $false) | (((ord_less_eq_real @ zero_zero_real @ X1)) = $false) | ($true = ((ord_less_eq_real @ X1 @ zero_zero_real)))) )),
% 186.48/26.66 inference(trivial_inequality_removal,[],[f4566])).
% 186.48/26.66 thf(f4573,plain,(
% 186.48/26.66 ( ! [X2 : real,X0 : real,X1 : real] : (($true = ((ord_less_eq_real @ X1 @ zero_zero_real))) | ($true = $false) | (((ord_less_eq_real @ zero_zero_real @ X0)) = $false) | ($true != ((ord_less_eq_real @ X1 @ X2))) | ($true = ((member_a @ (sK35 @ X0 @ X1) @ (elemen49976720ball_a @ x2 @ X2)))) | (((ord_less_eq_real @ X0 @ zero_zero_real)) = $true)) )),
% 186.48/26.66 inference(forward_subsumption_demodulation,[],[f4569,f2974])).
% 186.48/26.66 thf(f4574,plain,(
% 186.48/26.66 ( ! [X2 : real,X0 : real,X1 : real] : (($true = ((ord_less_eq_real @ X1 @ zero_zero_real))) | ($true = ((member_a @ (sK35 @ X0 @ X1) @ (elemen49976720ball_a @ x2 @ X2)))) | (((ord_less_eq_real @ X0 @ zero_zero_real)) = $true) | ($true != ((ord_less_eq_real @ X1 @ X2))) | (((ord_less_eq_real @ zero_zero_real @ X0)) = $false)) )),
% 186.48/26.66 inference(trivial_inequality_removal,[],[f4573])).
% 186.48/26.66 thf(f4575,plain,(
% 186.48/26.66 ( ! [X2 : real,X0 : real,X1 : real] : ((((ord_less_eq_real @ X0 @ zero_zero_real)) = $true) | ($true = $false) | ($true != ((ord_less_eq_real @ X1 @ X2))) | ($true = ((member_a @ (sK35 @ X0 @ X1) @ (elemen49976720ball_a @ x2 @ X2)))) | ($true = ((ord_less_eq_real @ X1 @ zero_zero_real)))) )),
% 186.48/26.66 inference(forward_subsumption_demodulation,[],[f4574,f2974])).
% 186.48/26.66 thf(f4576,plain,(
% 186.48/26.66 ( ! [X2 : real,X0 : real,X1 : real] : (($true != ((ord_less_eq_real @ X1 @ X2))) | ($true = ((ord_less_eq_real @ X1 @ zero_zero_real))) | (((ord_less_eq_real @ X0 @ zero_zero_real)) = $true) | ($true = ((member_a @ (sK35 @ X0 @ X1) @ (elemen49976720ball_a @ x2 @ X2))))) )),
% 186.48/26.66 inference(trivial_inequality_removal,[],[f4575])).
% 186.48/26.66 thf(f4578,plain,(
% 186.48/26.66 ( ! [X0 : real,X1 : real] : (($true = ((ord_less_eq_real @ X1 @ zero_zero_real))) | ($true = ((member_a @ (sK35 @ X1 @ X0) @ (elemen49976720ball_a @ x2 @ X0)))) | ($true != $true) | (((ord_less_eq_real @ X0 @ zero_zero_real)) = $true)) ) | ~spl111_7),
% 186.48/26.66 inference(constrained_superposition,[],[f4576,f4308])).
% 186.48/26.66 thf(f4589,plain,(
% 186.48/26.66 ( ! [X0 : real,X1 : real] : (($true = ((member_a @ (sK35 @ X1 @ X0) @ (elemen49976720ball_a @ x2 @ X0)))) | ($true = ((ord_less_eq_real @ X1 @ zero_zero_real))) | (((ord_less_eq_real @ X0 @ zero_zero_real)) = $true)) ) | ~spl111_7),
% 186.48/26.66 inference(trivial_inequality_removal,[],[f4578])).
% 186.48/26.66 thf(f4647,plain,(
% 186.48/26.66 ( ! [X0 : real] : ((((ord_less_eq_real @ d @ zero_zero_real)) = $true) | ($true != $true) | (((ord_less_eq_real @ X0 @ zero_zero_real)) = $true) | ($true = ((ord_less_eq_real @ (inner_1173012732nner_a @ (f @ sK26) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))) @ (inner_1173012732nner_a @ (f @ (sK35 @ X0 @ d)) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))))))) ) | ~spl111_7),
% 186.48/26.66 inference(constrained_superposition,[],[f1488,f4589])).
% 186.48/26.66 thf(f4654,plain,(
% 186.48/26.66 ( ! [X0 : real] : ((((ord_less_eq_real @ d @ zero_zero_real)) = $true) | (((ord_less_eq_real @ X0 @ zero_zero_real)) = $true) | ($true = ((ord_less_eq_real @ (inner_1173012732nner_a @ (f @ sK26) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))) @ (inner_1173012732nner_a @ (f @ (sK35 @ X0 @ d)) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))))))) ) | ~spl111_7),
% 186.48/26.67 inference(trivial_inequality_removal,[],[f4647])).
% 186.48/26.67 thf(f4658,plain,(
% 186.48/26.67 ( ! [X0 : real] : (($true = $false) | ($true = ((ord_less_eq_real @ (inner_1173012732nner_a @ (f @ sK26) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))) @ (inner_1173012732nner_a @ (f @ (sK35 @ X0 @ d)) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b)))))) | (((ord_less_eq_real @ X0 @ zero_zero_real)) = $true)) ) | ~spl111_7),
% 186.48/26.67 inference(forward_demodulation,[],[f4654,f3796])).
% 186.48/26.67 thf(f4659,plain,(
% 186.48/26.67 ( ! [X0 : real] : (($true = ((ord_less_eq_real @ (inner_1173012732nner_a @ (f @ sK26) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))) @ (inner_1173012732nner_a @ (f @ (sK35 @ X0 @ d)) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b)))))) | (((ord_less_eq_real @ X0 @ zero_zero_real)) = $true)) ) | ~spl111_7),
% 186.48/26.67 inference(trivial_inequality_removal,[],[f4658])).
% 186.48/26.67 thf(f4819,plain,(
% 186.48/26.67 ($true = ((ord_less_eq_real @ (inner_1173012732nner_a @ (f @ sK26) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))) @ zero_zero_real))) | ($true = ((ord_less_eq_real @ (inner_1173012732nner_a @ (f @ sK26) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))) @ zero_zero_real))) | (((ord_less_eq_real @ d @ zero_zero_real)) = $true) | ($true != $true) | ~spl111_7),
% 186.48/26.67 inference(constrained_superposition,[],[f4001,f4659])).
% 186.48/26.67 thf(f4822,plain,(
% 186.48/26.67 (((ord_less_eq_real @ d @ zero_zero_real)) = $true) | ($true != $true) | ($true = ((ord_less_eq_real @ (inner_1173012732nner_a @ (f @ sK26) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))) @ zero_zero_real))) | ~spl111_7),
% 186.48/26.67 inference(duplicate_literal_removal,[],[f4819])).
% 186.48/26.67 thf(f4823,plain,(
% 186.48/26.67 ($true = ((ord_less_eq_real @ (inner_1173012732nner_a @ (f @ sK26) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))) @ zero_zero_real))) | (((ord_less_eq_real @ d @ zero_zero_real)) = $true) | ~spl111_7),
% 186.48/26.67 inference(trivial_inequality_removal,[],[f4822])).
% 186.48/26.67 thf(f4843,definition,(
% 186.48/26.67 spl111_11 <=> ($true = ((ord_less_eq_real @ (inner_1173012732nner_a @ (f @ sK26) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))) @ zero_zero_real)))),
% 186.48/26.67 introduced(definition,[new_symbols(definition,[spl111_11])],[avatar_definition])).
% 186.48/26.67 thf(f4845,plain,(
% 186.48/26.67 ($true = ((ord_less_eq_real @ (inner_1173012732nner_a @ (f @ sK26) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))) @ zero_zero_real))) | ~spl111_11),
% 186.48/26.67 inference(avatar_component_clause,[],[f4843])).
% 186.48/26.67 thf(f4860,plain,(
% 186.48/26.67 ($true = ((ord_less_eq_real @ (inner_1173012732nner_a @ (f @ sK26) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))) @ zero_zero_real))) | ($true = $false) | ~spl111_7),
% 186.48/26.67 inference(forward_demodulation,[],[f4823,f3796])).
% 186.48/26.67 thf(f4861,plain,(
% 186.48/26.67 ($true = ((ord_less_eq_real @ (inner_1173012732nner_a @ (f @ sK26) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))) @ zero_zero_real))) | ~spl111_7),
% 186.48/26.67 inference(trivial_inequality_removal,[],[f4860])).
% 186.48/26.67 thf(f4877,plain,(
% 186.48/26.67 spl111_11 | ~spl111_7),
% 186.48/26.67 inference(avatar_split_clause,[],[f4861,f4007,f4843])).
% 186.48/26.67 thf(f4892,plain,(
% 186.48/26.67 spl111_7),
% 186.48/26.67 inference(avatar_split_clause,[],[f4058,f4007])).
% 186.48/26.67 thf(f4904,plain,(
% 186.48/26.67 (zero_zero_real = ((inner_1173012732nner_a @ (f @ sK26) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))))) | ($true != ((ord_less_eq_real @ zero_zero_real @ (inner_1173012732nner_a @ (f @ sK26) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b)))))) | ($true != $true) | ~spl111_11),
% 186.48/26.67 inference(constrained_superposition,[],[f1624,f4845])).
% 186.48/26.67 thf(f4915,plain,(
% 186.48/26.67 (zero_zero_real = ((inner_1173012732nner_a @ (f @ sK26) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))))) | ($true != ((ord_less_eq_real @ zero_zero_real @ (inner_1173012732nner_a @ (f @ sK26) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b)))))) | ~spl111_11),
% 186.48/26.67 inference(trivial_inequality_removal,[],[f4904])).
% 186.48/26.67 thf(f4920,definition,(
% 186.48/26.67 spl111_21 <=> ($true = ((ord_less_eq_real @ zero_zero_real @ (inner_1173012732nner_a @ (f @ sK26) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))))))),
% 186.48/26.67 introduced(definition,[new_symbols(definition,[spl111_21])],[avatar_definition])).
% 186.48/26.67 thf(f4922,plain,(
% 186.48/26.67 ($true != ((ord_less_eq_real @ zero_zero_real @ (inner_1173012732nner_a @ (f @ sK26) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b)))))) | spl111_21),
% 186.48/26.67 inference(avatar_component_clause,[],[f4920])).
% 186.48/26.67 thf(f4924,definition,(
% 186.48/26.67 spl111_22 <=> (zero_zero_real = ((inner_1173012732nner_a @ (f @ sK26) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b)))))),
% 186.48/26.67 introduced(definition,[new_symbols(definition,[spl111_22])],[avatar_definition])).
% 186.48/26.67 thf(f4926,plain,(
% 186.48/26.67 (zero_zero_real = ((inner_1173012732nner_a @ (f @ sK26) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))))) | ~spl111_22),
% 186.48/26.67 inference(avatar_component_clause,[],[f4924])).
% 186.48/26.67 thf(f4927,plain,(
% 186.48/26.67 ~spl111_21 | spl111_22 | ~spl111_11),
% 186.48/26.67 inference(avatar_split_clause,[],[f4915,f4843,f4924,f4920])).
% 186.48/26.67 thf(f4970,plain,(
% 186.48/26.67 (((ord_less_eq_real @ zero_zero_real @ (inner_1173012732nner_a @ (f @ sK26) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))))) = $false) | ($true != $true) | spl111_21),
% 186.48/26.67 inference(constrained_superposition,[],[f4922,f1706])).
% 186.48/26.67 thf(f4972,plain,(
% 186.48/26.67 (((ord_less_eq_real @ zero_zero_real @ (inner_1173012732nner_a @ (f @ sK26) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))))) = $false) | spl111_21),
% 186.48/26.67 inference(trivial_inequality_removal,[],[f4970])).
% 186.48/26.67 thf(f9315,plain,(
% 186.48/26.67 ($true != $true) | ($true = ((ord_less_eq_real @ zero_zero_real @ (inner_1173012732nner_a @ (f @ sK26) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))))))),
% 186.48/26.67 inference(constrained_superposition,[],[f2011,f4095])).
% 186.48/26.67 thf(f9320,plain,(
% 186.48/26.67 ($true = ((ord_less_eq_real @ zero_zero_real @ (inner_1173012732nner_a @ (f @ sK26) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))))))),
% 186.48/26.67 inference(trivial_inequality_removal,[],[f9315])).
% 186.48/26.67 thf(f9322,plain,(
% 186.48/26.67 ($true = $false) | spl111_21),
% 186.48/26.67 inference(forward_demodulation,[],[f9320,f4972])).
% 186.48/26.67 thf(f9323,plain,(
% 186.48/26.67 $false | spl111_21),
% 186.48/26.67 inference(trivial_inequality_removal,[],[f9322])).
% 186.48/26.67 thf(f9324,plain,(
% 186.48/26.67 spl111_21),
% 186.48/26.67 inference(avatar_contradiction_clause,[],[f9323])).
% 186.48/26.67 thf(f9333,plain,(
% 186.48/26.67 ($false = ((ord_less_eq_real @ (inner_1173012732nner_a @ (f @ sK26) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))) @ zero_zero_real))) | ($true != $true)),
% 186.48/26.67 inference(constrained_superposition,[],[f2013,f4095])).
% 186.48/26.67 thf(f9337,plain,(
% 186.48/26.67 ($false = ((ord_less_eq_real @ (inner_1173012732nner_a @ (f @ sK26) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))) @ zero_zero_real)))),
% 186.48/26.67 inference(trivial_inequality_removal,[],[f9333])).
% 186.48/26.67 thf(f9340,plain,(
% 186.48/26.67 ($false = ((ord_less_eq_real @ zero_zero_real @ zero_zero_real))) | ~spl111_22),
% 186.48/26.67 inference(forward_demodulation,[],[f9337,f4926])).
% 186.48/26.67 thf(f9341,plain,(
% 186.48/26.67 ($true = $false) | (~spl111_7 | ~spl111_22)),
% 186.48/26.67 inference(forward_demodulation,[],[f9340,f4308])).
% 186.48/26.67 thf(f9342,plain,(
% 186.48/26.67 $false | (~spl111_7 | ~spl111_22)),
% 186.48/26.67 inference(trivial_inequality_removal,[],[f9341])).
% 186.48/26.67 thf(f9343,plain,(
% 186.48/26.67 ~spl111_7 | ~spl111_22),
% 186.48/26.67 inference(avatar_contradiction_clause,[],[f9342])).
% 186.48/26.67 cnf(s815, plain, ~spl111_7 | spl111_11, inference(sat_conversion,[],[f4877])).
% 186.48/26.67 cnf(s829, plain, spl111_7, inference(sat_conversion,[],[f4892])).
% 186.48/26.67 cnf(s847, plain, ~spl111_11 | ~spl111_21 | spl111_22, inference(sat_conversion,[],[f4927])).
% 186.48/26.67 cnf(s1841, plain, spl111_21, inference(sat_conversion,[],[f9324])).
% 186.48/26.67 cnf(s1850, plain, ~spl111_7 | ~spl111_22, inference(sat_conversion,[],[f9343])).
% 186.48/26.67 cnf(s1853, plain, ~spl111_11 | spl111_22, inference(rat,[],[s847,s1841])).
% 186.48/26.67 cnf(s1854, plain, ~spl111_22, inference(rat,[],[s1850,s829])).
% 186.48/26.67 cnf(s1855, plain, ~spl111_11, inference(rat,[],[s1853,s1854])).
% 186.48/26.67 cnf(s1856, plain, $false, inference(rat,[],[s815,s1855,s829])).
% 186.48/26.67 thf(f9344,plain,(
% 186.48/26.67 $false),
% 186.48/26.67 inference(avatar_sat_refutation,[],[s1856])).
% 186.48/26.67 % SZS output end Proof for theBenchmark
% 186.48/26.67 % (571903)------------------------------
% 186.48/26.67 % (571903)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 186.48/26.67 % (571903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.48/26.67 % (571903)CaDiCaL version: 2.1.3
% 186.48/26.67 % (571903)Termination reason: Refutation
% 186.48/26.67 % (571903)Time elapsed: 0.540 s
% 186.48/26.67 % (571903)Peak memory usage: 19 MB
% 186.48/26.67 % (571903)Instructions burned: 2113 (million)
% 186.48/26.67 % (570907)Success in time 26.429 s
% 186.48/26.67 % Vampire exiting
%------------------------------------------------------------------------------