%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ITP147^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n006.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 23.63s 3.88s
% Output : Refutation 23.63s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP147^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.17 % Computer : n006.cluster.edu
% 0.10/0.17 % Model : x86_64 x86_64
% 0.10/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.17 % Memory : 8046.5625MB
% 0.10/0.17 % OS : Linux 6.8.0-71-generic
% 0.10/0.17 % CPULimit : 300
% 0.10/0.17 % WCLimit : 300
% 0.10/0.17 % DateTime : Tue Sep 29 20:00:25 UTC 2026
% 0.10/0.18 % CPUTime :
% 0.10/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.21 Running first-order model finding
% 0.10/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.14/0.97 % (1237308)Will run a generic schedule for satisfiability detection.
% 4.14/0.97 % (1237328)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1406054053:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.14/0.97 % (1237325)% WARNING: option uhcvi not known.
% 4.14/0.97 % (1237324)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2127458666_2999 on theBenchmark for (2999ds/0Mi)
% 4.14/0.97 % (1237326)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=962581728:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.14/0.97 % (1237327)dis+10_1_sil=32000:sp=arity:random_seed=334631183:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.14/0.97 % (1237329)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2956994885:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.14/0.97 % (1237328)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.14/0.97 % (1237330)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1137971243:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.14/0.97 % (1237325)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3814106548:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.14/0.97 % (1237325)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.14/0.97 % (1237328)Instruction limit reached!
% 4.14/0.97 % (1237328)------------------------------
% 4.14/0.97 % (1237328)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.14/0.97 % (1237328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.14/0.97 % (1237328)CaDiCaL version: 2.1.3
% 4.14/0.97 % (1237328)Termination reason: Instruction limit
% 4.14/0.97 % (1237328)Termination phase: Saturation
% 4.14/0.97 % (1237328)Time elapsed: 0.027 s
% 4.14/0.97 % (1237328)Peak memory usage: 13 MB
% 4.14/0.97 % (1237328)Instructions burned: 120 (million)
% 4.14/0.97 % (1237351)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1649553426:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 4.14/0.97 % Exception at run slice level
% 4.14/0.97 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.14/0.97 % (1237325)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 4.14/0.97 % (1237327)Instruction limit reached!
% 4.14/0.97 % (1237327)------------------------------
% 4.14/0.97 % (1237327)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.14/0.97 % (1237327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.14/0.97 % (1237327)CaDiCaL version: 2.1.3
% 4.14/0.97 % (1237327)Termination reason: Instruction limit
% 4.14/0.97 % (1237327)Termination phase: Saturation
% 4.14/0.97 % (1237327)Time elapsed: 0.044 s
% 4.14/0.97 % (1237327)Peak memory usage: 12 MB
% 4.14/0.97 % (1237327)Instructions burned: 103 (million)
% 4.14/0.97 % Exception at run slice level
% 4.14/0.97 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.14/0.97 % (1237358)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2223439184:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 4.14/0.97 % (1237329)Instruction limit reached!
% 4.14/0.97 % (1237329)------------------------------
% 4.14/0.97 % (1237329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.14/0.97 % (1237329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.14/0.97 % (1237329)CaDiCaL version: 2.1.3
% 4.14/0.97 % (1237329)Termination reason: Instruction limit
% 4.14/0.97 % (1237329)Termination phase: Saturation
% 4.14/0.97 % (1237329)Time elapsed: 0.057 s
% 4.14/0.97 % (1237329)Peak memory usage: 13 MB
% 4.14/0.97 % (1237329)Instructions burned: 131 (million)
% 4.14/0.97 % (1237369)ott-21_1_sil=16000:fs=off:random_seed=220786271:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 4.14/0.97 % (1237367)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=431482310:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 4.14/0.97 % (1237330)Instruction limit reached!
% 4.14/0.97 % (1237330)------------------------------
% 4.14/0.97 % (1237330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.14/0.97 % (1237330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.03/2.67 % (1237330)CaDiCaL version: 2.1.3
% 16.03/2.67 % (1237330)Termination reason: Instruction limit
% 16.03/2.67 % (1237330)Termination phase: Saturation
% 16.03/2.67 % (1237330)Time elapsed: 0.076 s
% 16.03/2.67 % (1237330)Peak memory usage: 14 MB
% 16.03/2.67 % (1237330)Instructions burned: 160 (million)
% 16.03/2.67 % (1237373)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1113256990:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi)
% 16.03/2.67 % (1237367)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 16.03/2.67 % (1237382)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1860584151:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 16.03/2.67 % (1237367)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 16.03/2.67 % (1237369)Instruction limit reached!
% 16.03/2.67 % (1237369)------------------------------
% 16.03/2.67 % (1237369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.03/2.67 % (1237369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.03/2.67 % (1237369)CaDiCaL version: 2.1.3
% 16.03/2.67 % (1237369)Termination reason: Instruction limit
% 16.03/2.67 % (1237369)Termination phase: Saturation
% 16.03/2.67 % (1237369)Time elapsed: 0.044 s
% 16.03/2.67 % (1237369)Peak memory usage: 13 MB
% 16.03/2.67 % (1237369)Instructions burned: 183 (million)
% 16.03/2.67 % (1237358)Instruction limit reached!
% 16.03/2.67 % (1237358)------------------------------
% 16.03/2.67 % (1237358)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.03/2.67 % (1237358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.03/2.67 % (1237358)CaDiCaL version: 2.1.3
% 16.03/2.67 % (1237358)Termination reason: Instruction limit
% 16.03/2.67 % (1237358)Termination phase: Saturation
% 16.03/2.67 % (1237358)Time elapsed: 0.059 s
% 16.03/2.67 % (1237358)Peak memory usage: 13 MB
% 16.03/2.67 % (1237358)Instructions burned: 132 (million)
% 16.03/2.67 % (1237390)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2220900502:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 16.03/2.67 % Exception at run slice level
% 16.03/2.67 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 16.03/2.67 % (1237393)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2524525505:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 16.03/2.67 % (1237402)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=681619048: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)
% 16.03/2.67 % (1237402)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 16.03/2.67 % Exception at run slice level
% 16.03/2.67 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 16.03/2.67 % (1237414)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2700493527:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 16.03/2.67 % (1237414)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 16.03/2.67 % (1237373)Instruction limit reached!
% 16.03/2.67 % (1237373)------------------------------
% 16.03/2.67 % (1237373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.03/2.67 % (1237373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.03/2.67 % (1237373)CaDiCaL version: 2.1.3
% 16.03/2.67 % (1237373)Termination reason: Instruction limit
% 16.03/2.67 % (1237373)Termination phase: Saturation
% 16.03/2.67 % (1237373)Time elapsed: 0.255 s
% 16.03/2.67 % (1237373)Peak memory usage: 14 MB
% 16.03/2.67 % (1237373)Instructions burned: 479 (million)
% 16.03/2.67 % (1237433)fmb+10_1_sil=64000:random_seed=993492556:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi)
% 16.03/2.67 % (1237367)Instruction limit reached!
% 16.03/2.67 % (1237367)------------------------------
% 16.03/2.67 % (1237367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.03/2.67 % (1237367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.03/2.67 % (1237367)CaDiCaL version: 2.1.3
% 16.03/2.67 % (1237367)Termination reason: Instruction limit
% 16.03/2.67 % (1237367)Termination phase: Saturation
% 16.03/2.67 % (1237367)Time elapsed: 0.312 s
% 16.03/2.67 % (1237367)Peak memory usage: 15 MB
% 16.03/2.67 % (1237367)Instructions burned: 684 (million)
% 23.63/3.87 % (1237433)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 23.63/3.87 % Exception at run slice level
% 23.63/3.87 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 23.63/3.87 % (1237463)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3120444164:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi)
% 23.63/3.87 % (1237468)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=34289494:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi)
% 23.63/3.87 % (1237390)Instruction limit reached!
% 23.63/3.87 % (1237390)------------------------------
% 23.63/3.87 % (1237390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.63/3.87 % (1237390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.63/3.87 % (1237390)CaDiCaL version: 2.1.3
% 23.63/3.87 % (1237390)Termination reason: Instruction limit
% 23.63/3.87 % (1237390)Termination phase: Saturation
% 23.63/3.87 % (1237390)Time elapsed: 0.307 s
% 23.63/3.87 % (1237390)Peak memory usage: 18 MB
% 23.63/3.87 % (1237390)Instructions burned: 1180 (million)
% 23.63/3.87 % Exception at run slice level
% 23.63/3.87 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 23.63/3.87 % (1237477)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3688249098:i=5131_2995 on theBenchmark for (2995ds/5131Mi)
% 23.63/3.87 % Exception at run slice level
% 23.63/3.87 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 23.63/3.87 % (1237477)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 23.63/3.87 % (1237478)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=805526400:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 23.63/3.87 % (1237480)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1800399178:i=6324_2995 on theBenchmark for (2995ds/6324Mi)
% 23.63/3.87 % (1237478)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 23.63/3.87 % (1237478)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 23.63/3.87 % Exception at run slice level
% 23.63/3.87 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 23.63/3.87 % (1237402)Instruction limit reached!
% 23.63/3.87 % (1237402)------------------------------
% 23.63/3.87 % (1237402)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.63/3.87 % (1237402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.63/3.87 % (1237402)CaDiCaL version: 2.1.3
% 23.63/3.87 % (1237402)Termination reason: Instruction limit
% 23.63/3.87 % (1237402)Termination phase: Saturation
% 23.63/3.87 % (1237402)Time elapsed: 0.347 s
% 23.63/3.87 % (1237402)Peak memory usage: 16 MB
% 23.63/3.87 % (1237402)Instructions burned: 692 (million)
% 23.63/3.87 % (1237483)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1641769509:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi)
% 23.63/3.87 % (1237484)ott-2_1_sil=16000:newcnf=on:random_seed=4218549419:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi)
% 23.63/3.87 % (1237484)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 23.63/3.87 % Exception at run slice level
% 23.63/3.87 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 23.63/3.87 % (1237487)ott+10_1_sil=32000:tgt=ground:random_seed=516772036:i=5114:av=off_2994 on theBenchmark for (2994ds/5114Mi)
% 23.63/3.87 % (1237414)Instruction limit reached!
% 23.63/3.87 % (1237414)------------------------------
% 23.63/3.87 % (1237414)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.63/3.87 % (1237414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.63/3.87 % (1237414)CaDiCaL version: 2.1.3
% 23.63/3.87 % (1237414)Termination reason: Instruction limit
% 23.63/3.87 % (1237414)Termination phase: Saturation
% 23.63/3.87 % (1237414)Time elapsed: 0.463 s
% 23.63/3.87 % (1237414)Peak memory usage: 16 MB
% 23.63/3.87 % (1237414)Instructions burned: 880 (million)
% 23.63/3.87 % (1237489)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3584029646:i=54282_2993 on theBenchmark for (2993ds/54282Mi)
% 23.63/3.87 % Exception at run slice level
% 23.63/3.87 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 23.63/3.87 % (1237491)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1115571188:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi)
% 23.63/3.87 % (1237491)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 23.63/3.87 % (1237484)Instruction limit reached!
% 23.63/3.87 % (1237484)------------------------------
% 23.63/3.87 % (1237484)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.63/3.87 % (1237484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.63/3.87 % (1237484)CaDiCaL version: 2.1.3
% 23.63/3.87 % (1237484)Termination reason: Instruction limit
% 23.63/3.87 % (1237484)Termination phase: Saturation
% 23.63/3.87 % (1237484)Time elapsed: 0.421 s
% 23.63/3.87 % (1237484)Peak memory usage: 16 MB
% 23.63/3.87 % (1237484)Instructions burned: 870 (million)
% 23.63/3.87 % (1237493)dis+21_1_sil=32000:sas=cadical:random_seed=1564752208:i=3773:amm=off_2990 on theBenchmark for (2990ds/3773Mi)
% 23.63/3.87 % (1237478)Instruction limit reached!
% 23.63/3.87 % (1237478)------------------------------
% 23.63/3.87 % (1237478)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.63/3.87 % (1237478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.63/3.87 % (1237478)CaDiCaL version: 2.1.3
% 23.63/3.87 % (1237478)Termination reason: Instruction limit
% 23.63/3.87 % (1237478)Termination phase: Saturation
% 23.63/3.87 % (1237478)Time elapsed: 0.656 s
% 23.63/3.87 % (1237478)Peak memory usage: 16 MB
% 23.63/3.87 % (1237478)Instructions burned: 1472 (million)
% 23.63/3.87 % (1237495)ott+11_1_sil=16000:gs=on:random_seed=3111532538:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi)
% 23.63/3.87 % (1237495)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 23.63/3.87 % (1237477)Instruction limit reached!
% 23.63/3.87 % (1237477)------------------------------
% 23.63/3.87 % (1237477)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.63/3.87 % (1237477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.63/3.87 % (1237477)CaDiCaL version: 2.1.3
% 23.63/3.87 % (1237477)Termination reason: Instruction limit
% 23.63/3.87 % (1237477)Termination phase: Saturation
% 23.63/3.87 % (1237477)Time elapsed: 1.284 s
% 23.63/3.87 % (1237477)Peak memory usage: 23 MB
% 23.63/3.87 % (1237477)Instructions burned: 5134 (million)
% 23.63/3.87 % (1237497)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=4125014487:fmbsr=1.6:i=67534_2982 on theBenchmark for (2982ds/67534Mi)
% 23.63/3.87 % Exception at run slice level
% 23.63/3.87 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 23.63/3.87 % (1237499)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1267335851:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2982 on theBenchmark for (2982ds/4591Mi)
% 23.63/3.87 % (1237495)Instruction limit reached!
% 23.63/3.87 % (1237495)------------------------------
% 23.63/3.87 % (1237495)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.63/3.87 % (1237495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.63/3.88 % (1237495)CaDiCaL version: 2.1.3
% 23.63/3.88 % (1237495)Termination reason: Instruction limit
% 23.63/3.88 % (1237495)Termination phase: Saturation
% 23.63/3.88 % (1237495)Time elapsed: 0.978 s
% 23.63/3.88 % (1237495)Peak memory usage: 17 MB
% 23.63/3.88 % (1237495)Instructions burned: 2251 (million)
% 23.63/3.88 % (1237501)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3115951460:i=29340_2978 on theBenchmark for (2978ds/29340Mi)
% 23.63/3.88 % (1237491)Instruction limit reached!
% 23.63/3.88 % (1237491)------------------------------
% 23.63/3.88 % (1237491)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.63/3.88 % (1237491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.63/3.88 % (1237491)CaDiCaL version: 2.1.3
% 23.63/3.88 % (1237491)Termination reason: Instruction limit
% 23.63/3.88 % (1237491)Termination phase: Saturation
% 23.63/3.88 % (1237491)Time elapsed: 1.664 s
% 23.63/3.88 % (1237491)Peak memory usage: 20 MB
% 23.63/3.88 % (1237491)Instructions burned: 3513 (million)
% 23.63/3.88 % (1237503)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3028179598:i=5211_2975 on theBenchmark for (2975ds/5211Mi)
% 23.63/3.88 % (1237493)Instruction limit reached!
% 23.63/3.88 % (1237493)------------------------------
% 23.63/3.88 % (1237493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.63/3.88 % (1237493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.63/3.88 % (1237493)CaDiCaL version: 2.1.3
% 23.63/3.88 % (1237493)Termination reason: Instruction limit
% 23.63/3.88 % (1237493)Termination phase: Saturation
% 23.63/3.88 % (1237493)Time elapsed: 1.814 s
% 23.63/3.88 % (1237493)Peak memory usage: 20 MB
% 23.63/3.88 % (1237493)Instructions burned: 3773 (million)
% 23.63/3.88 % (1237505)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=141335874:i=5497:nm=2_2971 on theBenchmark for (2971ds/5497Mi)
% 23.63/3.88 % Exception at run slice level
% 23.63/3.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 23.63/3.88 % (1237507)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2909121595:fmbsr=2:i=46332_2971 on theBenchmark for (2971ds/46332Mi)
% 23.63/3.88 % Exception at run slice level
% 23.63/3.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 23.63/3.88 % (1237509)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=798660338:i=14071_2970 on theBenchmark for (2970ds/14071Mi)
% 23.63/3.88 % Exception at run slice level
% 23.63/3.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 23.63/3.88 % (1237487)Instruction limit reached!
% 23.63/3.88 % (1237487)------------------------------
% 23.63/3.88 % (1237487)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.63/3.88 % (1237487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.63/3.88 % (1237487)CaDiCaL version: 2.1.3
% 23.63/3.88 % (1237487)Termination reason: Instruction limit
% 23.63/3.88 % (1237487)Termination phase: Saturation
% 23.63/3.88 % (1237487)Time elapsed: 2.383 s
% 23.63/3.88 % (1237487)Peak memory usage: 33 MB
% 23.63/3.88 % (1237487)Instructions burned: 5116 (million)
% 23.63/3.88 % (1237511)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1283636952:i=22565:add=on:rawr=on_2970 on theBenchmark for (2970ds/22565Mi)
% 23.63/3.88 % (1237512)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=933794510:i=8173:av=off_2970 on theBenchmark for (2970ds/8173Mi)
% 23.63/3.88 % (1237499)Instruction limit reached!
% 23.63/3.88 % (1237499)------------------------------
% 23.63/3.88 % (1237499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.63/3.88 % (1237499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.63/3.88 % (1237499)CaDiCaL version: 2.1.3
% 23.63/3.88 % (1237499)Termination reason: Instruction limit
% 23.63/3.88 % (1237499)Termination phase: Saturation
% 23.63/3.88 % (1237499)Time elapsed: 1.258 s
% 23.63/3.88 % (1237499)Peak memory usage: 29 MB
% 23.63/3.88 % (1237499)Instructions burned: 4595 (million)
% 23.63/3.88 % (1237515)dis+10_16:1_sil=16000:random_seed=77766939:i=9155:fsr=off_2969 on theBenchmark for (2969ds/9155Mi)
% 23.63/3.88 % (1237512) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1237308-1237512"...
% 23.63/3.88 % (1237512)...printing done.
% 23.63/3.88 % (1237512)Refutation found. Thanks to Tanya!
% 23.63/3.88 % SZS status Theorem for theBenchmark
% 23.63/3.88 % SZS output start Proof for theBenchmark
% 23.63/3.88 thf(type_def_5, type, set_real: $tType).
% 23.63/3.88 thf(type_def_6, type, set_a: $tType).
% 23.63/3.88 thf(type_def_7, type, real: $tType).
% 23.63/3.88 thf(type_def_8, type, a: $tType).
% 23.63/3.88 thf(type_def_9, type, sTfun: ($tType * $tType) > $tType).
% 23.63/3.88 thf(func_def_0, type, elemen341675809l_real: (real > real > set_real)).
% 23.63/3.88 thf(func_def_1, type, elemen154694473ball_a: (a > real > set_a)).
% 23.63/3.88 thf(func_def_2, type, auto_l612940ivl0_a: ((a > a) > set_a > a > set_real)).
% 23.63/3.88 thf(func_def_3, type, auto_ll_on_flow0_a: ((a > a) > set_a > a > real > a)).
% 23.63/3.88 thf(func_def_4, type, abs_abs_real: (real > real)).
% 23.63/3.88 thf(func_def_5, type, abs_abs_a: (a > a)).
% 23.63/3.88 thf(func_def_6, type, one_one_real: real).
% 23.63/3.88 thf(func_def_7, type, plus_plus_real: (real > real > real)).
% 23.63/3.88 thf(func_def_8, type, plus_plus_a: (a > a > a)).
% 23.63/3.88 thf(func_def_9, type, uminus_uminus_a_a: ((a > a) > a > a)).
% 23.63/3.88 thf(func_def_10, type, uminus_uminus_real: (real > real)).
% 23.63/3.88 thf(func_def_11, type, uminus_uminus_a: (a > a)).
% 23.63/3.88 thf(func_def_12, type, zero_zero_real: real).
% 23.63/3.88 thf(func_def_13, type, zero_zero_a: a).
% 23.63/3.88 thf(func_def_14, type, if_real: ($o > real > real > real)).
% 23.63/3.88 thf(func_def_15, type, initia826609931terval: (set_real > $o)).
% 23.63/3.88 thf(func_def_16, type, limit_1865182413oint_a: ((a > a) > set_a > a > a > $o)).
% 23.63/3.88 thf(func_def_17, type, limit_94460170oint_a: ((a > a) > set_a > a > a > $o)).
% 23.63/3.88 thf(func_def_18, type, line_open_segment_a: (a > a > set_a)).
% 23.63/3.88 thf(func_def_19, type, bot_bot_set_real: set_real).
% 23.63/3.88 thf(func_def_20, type, bot_bot_set_a: set_a).
% 23.63/3.88 thf(func_def_21, type, ord_less_real: (real > real > $o)).
% 23.63/3.88 thf(func_def_22, type, ord_less_a: (a > a > $o)).
% 23.63/3.88 thf(func_def_23, type, ord_less_eq_real: (real > real > $o)).
% 23.63/3.88 thf(func_def_24, type, ord_less_eq_a: (a > a > $o)).
% 23.63/3.88 thf(func_def_25, type, top_top_set_real: set_real).
% 23.63/3.88 thf(func_def_26, type, period720806154rbit_a: ((a > a) > set_a > a > $o)).
% 23.63/3.88 thf(func_def_27, type, period1305449585riod_a: ((a > a) > set_a > a > real)).
% 23.63/3.88 thf(func_def_28, type, period138238489rbit_a: ((a > a) > set_a > a > $o)).
% 23.63/3.88 thf(func_def_29, type, poinca522724647ment_a: ((a > a) > set_a > a > a > $o)).
% 23.63/3.88 thf(func_def_30, type, collect_real: ((real > $o) > set_real)).
% 23.63/3.88 thf(func_def_31, type, collect_a: ((a > $o) > set_a)).
% 23.63/3.88 thf(func_def_32, type, topolo1710226732a_real: (set_a > (a > real) > $o)).
% 23.63/3.88 thf(func_def_33, type, member_real: (real > set_real > $o)).
% 23.63/3.88 thf(func_def_34, type, member_a: (a > set_a > $o)).
% 23.63/3.88 thf(func_def_35, type, x: set_a).
% 23.63/3.88 thf(func_def_36, type, a2: a).
% 23.63/3.88 thf(func_def_37, type, b: a).
% 23.63/3.88 thf(func_def_38, type, f: (a > a)).
% 23.63/3.88 thf(func_def_39, type, p: a).
% 23.63/3.88 thf(func_def_40, type, thesisa: $o).
% 23.63/3.88 thf(func_def_41, type, x2: a).
% 23.63/3.88 thf(func_def_45, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 23.63/3.88 thf(func_def_46, type, vNOT: ($o > $o)).
% 23.63/3.88 thf(func_def_47, type, db0: !>[X0: $tType]:(X0)).
% 23.63/3.88 thf(func_def_48, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 23.63/3.88 thf(func_def_49, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 23.63/3.88 thf(func_def_50, type, vAND: ($o > $o > $o)).
% 23.63/3.88 thf(func_def_51, type, vOR: ($o > $o > $o)).
% 23.63/3.88 thf(func_def_52, type, db1: !>[X0: $tType]:(X0)).
% 23.63/3.88 thf(func_def_53, type, sK0: real).
% 23.63/3.88 thf(func_def_54, type, sK1: (a > real)).
% 23.63/3.88 thf(func_def_55, type, sK2: ((a > real) > real > a)).
% 23.63/3.88 thf(func_def_56, type, sK3: ((a > real) > real > a)).
% 23.63/3.88 thf(func_def_57, type, sK4: (real > a > a > a > real)).
% 23.63/3.88 thf(func_def_58, type, sK5: (real > a > a > a > a > real)).
% 23.63/3.88 thf(func_def_59, type, sK6: (a > a)).
% 23.63/3.88 thf(func_def_60, type, sK7: (a > a)).
% 23.63/3.88 thf(func_def_61, type, sK8: (a > a)).
% 23.63/3.88 thf(func_def_62, type, sK9: (a > a)).
% 23.63/3.88 thf(func_def_63, type, sK10: ((real > $o) > (real > $o) > real)).
% 23.63/3.88 thf(func_def_64, type, sK11: ((a > $o) > (a > $o) > a)).
% 23.63/3.88 thf(func_def_65, type, sK12: (a > real)).
% 23.63/3.88 thf(func_def_66, type, sK13: (a > real)).
% 23.63/3.88 thf(func_def_67, type, sK14: ((a > real) > real > a)).
% 23.63/3.88 thf(func_def_68, type, sK15: ((a > real) > real > a)).
% 23.63/3.88 thf(func_def_69, type, sK16: (a > real)).
% 23.63/3.88 thf(func_def_70, type, sK17: (a > real)).
% 23.63/3.88 thf(f4,axiom,(
% 23.63/3.88 ~ ! [X0 : real] : ((ord_less_real @ zero_zero_real @ X0) => ! [X1 : (a > real)] : ((topolo1710226732a_real @ (elemen154694473ball_a @ p @ X0) @ X1) => (! [X2 : a] : ((member_a @ X2 @ (elemen154694473ball_a @ p @ X0)) => (member_a @ (auto_ll_on_flow0_a @ f @ x @ X2 @ (X1 @ X2)) @ (line_open_segment_a @ a2 @ b))) => (! [X2 : a] : ((member_a @ X2 @ (elemen154694473ball_a @ p @ X0)) => (ord_less_real @ (abs_abs_real @ (X1 @ X2)) @ one_one_real)) => ((topolo1710226732a_real @ (elemen154694473ball_a @ p @ X0) @ X1) => (((X1 @ p)) != zero_zero_real))))))),
% 23.63/3.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_3__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062d_At_O_A_092_060lbrakk_0620_A_060_Ad_059_Acontinuous__on_A_Iball_Ap_Ad_J_At_059_A_092_060And_062y_O_Ay_A_092_060in_062_Aball_Ap_Ad_A_092_060Longrightarrow_062_Aflow0_Ay_A_It_Ay_J_A_092_060in_062_A_123a_060_N_N_060b_125_059_A_092_060And_062y_O_Ay_A_092_060in_062_Aball_Ap_Ad_A_092_060Longrightarrow_062_A_092_060bar_062t_Ay_092_060bar_062_A_060_A1_059_Acontinuous__on_A_Iball_Ap_Ad_J_At_059_At_Ap_A_061_A0_092_060rbrakk_062_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062)).
% 23.63/3.88 thf(f140,axiom,(
% 23.63/3.88 (abs_abs_real = (^[X0 : real] : ((if_real @ (ord_less_real @ X0 @ zero_zero_real) @ (uminus_uminus_real @ X0) @ X0))))),
% 23.63/3.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_139_abs__if)).
% 23.63/3.88 thf(f345,axiom,(
% 23.63/3.88 ! [X0 : $o] : ((X0 = $false) | (X0 = $true))),
% 23.63/3.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_If_3_1_If_001t__Real__Oreal_T)).
% 23.63/3.88 thf(f348,axiom,(
% 23.63/3.88 ! [X0 : real,X1 : (a > real)] : ((ord_less_real @ zero_zero_real @ X0) => ((topolo1710226732a_real @ (elemen154694473ball_a @ p @ X0) @ X1) => ((((X1 @ p)) = zero_zero_real) => (! [X2 : a] : ((member_a @ X2 @ (elemen154694473ball_a @ p @ X0)) => (ord_less_real @ (abs_abs_real @ (X1 @ X2)) @ one_one_real)) => (! [X2 : a] : ((member_a @ X2 @ (elemen154694473ball_a @ p @ X0)) => (member_a @ (auto_ll_on_flow0_a @ f @ x @ X2 @ (X1 @ X2)) @ (line_open_segment_a @ a2 @ b))) => thesisa)))))),
% 23.63/3.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0)).
% 23.63/3.88 thf(f349,conjecture,(
% 23.63/3.88 thesisa),
% 23.63/3.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_1)).
% 23.63/3.88 thf(f350,negated_conjecture,(
% 23.63/3.88 ~thesisa),
% 23.63/3.88 inference(negated_conjecture,[status(cth)],[f349])).
% 23.63/3.88 thf(f357,plain,(
% 23.63/3.88 ~ ! [X0 : real] : ((ord_less_real @ zero_zero_real @ X0) => ! [X1 : (a > real)] : ((topolo1710226732a_real @ (elemen154694473ball_a @ p @ X0) @ X1) => (! [X2 : a] : ((member_a @ X2 @ (elemen154694473ball_a @ p @ X0)) => (member_a @ (auto_ll_on_flow0_a @ f @ x @ X2 @ (X1 @ X2)) @ (line_open_segment_a @ a2 @ b))) => (! [X3 : a] : ((member_a @ X3 @ (elemen154694473ball_a @ p @ X0)) => (ord_less_real @ (abs_abs_real @ (X1 @ X3)) @ one_one_real)) => ((topolo1710226732a_real @ (elemen154694473ball_a @ p @ X0) @ X1) => (((X1 @ p)) != zero_zero_real))))))),
% 23.63/3.88 inference(rectify,[],[f4])).
% 23.63/3.88 thf(f358,plain,(
% 23.63/3.88 ~ ! [X0 : real] : ((((ord_less_real @ zero_zero_real @ X0)) = $true) => ! [X1 : (a > real)] : ((((topolo1710226732a_real @ (elemen154694473ball_a @ p @ X0) @ X1)) = $true) => (! [X2 : a] : ((((member_a @ X2 @ (elemen154694473ball_a @ p @ X0))) = $true) => (((member_a @ (auto_ll_on_flow0_a @ f @ x @ X2 @ (X1 @ X2)) @ (line_open_segment_a @ a2 @ b))) = $true)) => (! [X3 : a] : (($true = ((member_a @ X3 @ (elemen154694473ball_a @ p @ X0)))) => ($true = ((ord_less_real @ (abs_abs_real @ (X1 @ X3)) @ one_one_real)))) => ((((topolo1710226732a_real @ (elemen154694473ball_a @ p @ X0) @ X1)) = $true) => (zero_zero_real != ((X1 @ p))))))))),
% 23.63/3.88 inference(fool_elimination,[],[f357])).
% 23.63/3.88 thf(f528,plain,(
% 23.63/3.88 (abs_abs_real = (^[Y0 : real]: (if_real @ (ord_less_real @ Y0 @ zero_zero_real) @ (uminus_uminus_real @ Y0) @ Y0)))),
% 23.63/3.88 inference(fool_elimination,[],[f140])).
% 23.63/3.88 thf(f733,plain,(
% 23.63/3.88 ! [X0 : $o] : (($false = X0) | ($true = X0))),
% 23.63/3.88 inference(fool_elimination,[],[f345])).
% 23.63/3.88 thf(f738,plain,(
% 23.63/3.88 ! [X0 : real,X1 : (a > real)] : ((ord_less_real @ zero_zero_real @ X0) => ((topolo1710226732a_real @ (elemen154694473ball_a @ p @ X0) @ X1) => ((((X1 @ p)) = zero_zero_real) => (! [X2 : a] : ((member_a @ X2 @ (elemen154694473ball_a @ p @ X0)) => (ord_less_real @ (abs_abs_real @ (X1 @ X2)) @ one_one_real)) => (! [X3 : a] : ((member_a @ X3 @ (elemen154694473ball_a @ p @ X0)) => (member_a @ (auto_ll_on_flow0_a @ f @ x @ X3 @ (X1 @ X3)) @ (line_open_segment_a @ a2 @ b))) => thesisa)))))),
% 23.63/3.88 inference(rectify,[],[f348])).
% 23.63/3.88 thf(f739,plain,(
% 23.63/3.88 ! [X0 : real,X1 : (a > real)] : ((((ord_less_real @ zero_zero_real @ X0)) = $true) => ((((topolo1710226732a_real @ (elemen154694473ball_a @ p @ X0) @ X1)) = $true) => ((zero_zero_real = ((X1 @ p))) => (! [X2 : a] : ((((member_a @ X2 @ (elemen154694473ball_a @ p @ X0))) = $true) => (((ord_less_real @ (abs_abs_real @ (X1 @ X2)) @ one_one_real)) = $true)) => (! [X3 : a] : (($true = ((member_a @ X3 @ (elemen154694473ball_a @ p @ X0)))) => ($true = ((member_a @ (auto_ll_on_flow0_a @ f @ x @ X3 @ (X1 @ X3)) @ (line_open_segment_a @ a2 @ b))))) => (thesisa = $true))))))),
% 23.63/3.88 inference(fool_elimination,[],[f738])).
% 23.63/3.88 thf(f740,plain,(
% 23.63/3.88 ~thesisa),
% 23.63/3.88 inference(rectify,[],[f350])).
% 23.63/3.88 thf(f741,plain,(
% 23.63/3.88 ~ (thesisa = $true)),
% 23.63/3.88 inference(fool_elimination,[],[f740])).
% 23.63/3.88 thf(f754,plain,(
% 23.63/3.88 (thesisa != $true)),
% 23.63/3.88 inference(flattening,[],[f741])).
% 23.63/3.88 thf(f757,plain,(
% 23.63/3.88 ? [X0 : real] : (? [X1 : (a > real)] : (((((zero_zero_real = ((X1 @ p))) & (((topolo1710226732a_real @ (elemen154694473ball_a @ p @ X0) @ X1)) = $true)) & ! [X3 : a] : (($true = ((ord_less_real @ (abs_abs_real @ (X1 @ X3)) @ one_one_real))) | ($true != ((member_a @ X3 @ (elemen154694473ball_a @ p @ X0)))))) & ! [X2 : a] : ((((member_a @ (auto_ll_on_flow0_a @ f @ x @ X2 @ (X1 @ X2)) @ (line_open_segment_a @ a2 @ b))) = $true) | (((member_a @ X2 @ (elemen154694473ball_a @ p @ X0))) != $true))) & (((topolo1710226732a_real @ (elemen154694473ball_a @ p @ X0) @ X1)) = $true)) & (((ord_less_real @ zero_zero_real @ X0)) = $true))),
% 23.63/3.88 inference(ennf_transformation,[],[f358])).
% 23.63/3.88 thf(f758,plain,(
% 23.63/3.88 ? [X0 : real] : (? [X1 : (a > real)] : ((zero_zero_real = ((X1 @ p))) & (((topolo1710226732a_real @ (elemen154694473ball_a @ p @ X0) @ X1)) = $true) & ! [X3 : a] : (($true = ((ord_less_real @ (abs_abs_real @ (X1 @ X3)) @ one_one_real))) | ($true != ((member_a @ X3 @ (elemen154694473ball_a @ p @ X0))))) & ! [X2 : a] : ((((member_a @ (auto_ll_on_flow0_a @ f @ x @ X2 @ (X1 @ X2)) @ (line_open_segment_a @ a2 @ b))) = $true) | (((member_a @ X2 @ (elemen154694473ball_a @ p @ X0))) != $true)) & (((topolo1710226732a_real @ (elemen154694473ball_a @ p @ X0) @ X1)) = $true)) & (((ord_less_real @ zero_zero_real @ X0)) = $true))),
% 23.63/3.88 inference(flattening,[],[f757])).
% 23.63/3.88 thf(f994,plain,(
% 23.63/3.88 ! [X0 : real,X1 : (a > real)] : ((((((thesisa = $true) | ? [X3 : a] : (($true != ((member_a @ (auto_ll_on_flow0_a @ f @ x @ X3 @ (X1 @ X3)) @ (line_open_segment_a @ a2 @ b)))) & ($true = ((member_a @ X3 @ (elemen154694473ball_a @ p @ X0)))))) | ? [X2 : a] : ((((ord_less_real @ (abs_abs_real @ (X1 @ X2)) @ one_one_real)) != $true) & (((member_a @ X2 @ (elemen154694473ball_a @ p @ X0))) = $true))) | (zero_zero_real != ((X1 @ p)))) | (((topolo1710226732a_real @ (elemen154694473ball_a @ p @ X0) @ X1)) != $true)) | (((ord_less_real @ zero_zero_real @ X0)) != $true))),
% 23.63/3.88 inference(ennf_transformation,[],[f739])).
% 23.63/3.88 thf(f995,plain,(
% 23.63/3.88 ! [X0 : real,X1 : (a > real)] : ((thesisa = $true) | ? [X3 : a] : (($true != ((member_a @ (auto_ll_on_flow0_a @ f @ x @ X3 @ (X1 @ X3)) @ (line_open_segment_a @ a2 @ b)))) & ($true = ((member_a @ X3 @ (elemen154694473ball_a @ p @ X0))))) | ? [X2 : a] : ((((ord_less_real @ (abs_abs_real @ (X1 @ X2)) @ one_one_real)) != $true) & (((member_a @ X2 @ (elemen154694473ball_a @ p @ X0))) = $true)) | (zero_zero_real != ((X1 @ p))) | (((topolo1710226732a_real @ (elemen154694473ball_a @ p @ X0) @ X1)) != $true) | (((ord_less_real @ zero_zero_real @ X0)) != $true))),
% 23.63/3.88 inference(flattening,[],[f994])).
% 23.63/3.88 thf(f996,plain,(
% 23.63/3.88 ? [X0 : real] : (? [X1 : (a > real)] : ((zero_zero_real = ((X1 @ p))) & (((topolo1710226732a_real @ (elemen154694473ball_a @ p @ X0) @ X1)) = $true) & ! [X2 : a] : ((((ord_less_real @ (abs_abs_real @ (X1 @ X2)) @ one_one_real)) = $true) | (((member_a @ X2 @ (elemen154694473ball_a @ p @ X0))) != $true)) & ! [X3 : a] : (($true = ((member_a @ (auto_ll_on_flow0_a @ f @ x @ X3 @ (X1 @ X3)) @ (line_open_segment_a @ a2 @ b)))) | ($true != ((member_a @ X3 @ (elemen154694473ball_a @ p @ X0))))) & (((topolo1710226732a_real @ (elemen154694473ball_a @ p @ X0) @ X1)) = $true)) & (((ord_less_real @ zero_zero_real @ X0)) = $true))),
% 23.63/3.88 inference(rectify,[],[f758])).
% 23.63/3.88 thf(f997,plain,(
% 23.63/3.88 ((zero_zero_real = ((sK1 @ p))) & ($true = ((topolo1710226732a_real @ (elemen154694473ball_a @ p @ sK0) @ sK1))) & ! [X2 : a] : (($true = ((ord_less_real @ (abs_abs_real @ (sK1 @ X2)) @ one_one_real))) | ($true != ((member_a @ X2 @ (elemen154694473ball_a @ p @ sK0))))) & ! [X3 : a] : (($true = ((member_a @ (auto_ll_on_flow0_a @ f @ x @ X3 @ (sK1 @ X3)) @ (line_open_segment_a @ a2 @ b)))) | ($true != ((member_a @ X3 @ (elemen154694473ball_a @ p @ sK0))))) & ($true = ((topolo1710226732a_real @ (elemen154694473ball_a @ p @ sK0) @ sK1)))) & ($true = ((ord_less_real @ zero_zero_real @ sK0)))),
% 23.63/3.88 inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(X1,sK1)],[f996])).
% 23.63/3.88 thf(f1008,plain,(
% 23.63/3.88 ! [X0 : real,X1 : (a > real)] : ((thesisa = $true) | ? [X2 : a] : ((((member_a @ (auto_ll_on_flow0_a @ f @ x @ X2 @ (X1 @ X2)) @ (line_open_segment_a @ a2 @ b))) != $true) & (((member_a @ X2 @ (elemen154694473ball_a @ p @ X0))) = $true)) | ? [X3 : a] : (($true != ((ord_less_real @ (abs_abs_real @ (X1 @ X3)) @ one_one_real))) & ($true = ((member_a @ X3 @ (elemen154694473ball_a @ p @ X0))))) | (zero_zero_real != ((X1 @ p))) | (((topolo1710226732a_real @ (elemen154694473ball_a @ p @ X0) @ X1)) != $true) | (((ord_less_real @ zero_zero_real @ X0)) != $true))),
% 23.63/3.88 inference(rectify,[],[f995])).
% 23.63/3.88 thf(f1009,plain,(
% 23.63/3.88 ! [X0 : real,X1 : (a > real)] : ((thesisa = $true) | (($true != ((member_a @ (auto_ll_on_flow0_a @ f @ x @ (sK14 @ X1 @ X0) @ (X1 @ (sK14 @ X1 @ X0))) @ (line_open_segment_a @ a2 @ b)))) & ($true = ((member_a @ (sK14 @ X1 @ X0) @ (elemen154694473ball_a @ p @ X0))))) | (($true != ((ord_less_real @ (abs_abs_real @ (X1 @ (sK15 @ X1 @ X0))) @ one_one_real))) & ($true = ((member_a @ (sK15 @ X1 @ X0) @ (elemen154694473ball_a @ p @ X0))))) | (zero_zero_real != ((X1 @ p))) | (((topolo1710226732a_real @ (elemen154694473ball_a @ p @ X0) @ X1)) != $true) | (((ord_less_real @ zero_zero_real @ X0)) != $true))),
% 23.63/3.88 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP,vAPP]),skolemize(X3,sK3 @ X1 @ X0),skolemize(X3,sK3 @ X1 @ X0)],[f1008])).
% 23.63/3.88 thf(f1013,plain,(
% 23.63/3.88 ($true = ((ord_less_real @ zero_zero_real @ sK0)))),
% 23.63/3.88 inference(cnf_transformation,[],[f997])).
% 23.63/3.88 thf(f1014,plain,(
% 23.63/3.88 ($true = ((topolo1710226732a_real @ (elemen154694473ball_a @ p @ sK0) @ sK1)))),
% 23.63/3.88 inference(cnf_transformation,[],[f997])).
% 23.63/3.88 thf(f1015,plain,(
% 23.63/3.88 ( ! [X3 : a] : (($true != ((member_a @ X3 @ (elemen154694473ball_a @ p @ sK0)))) | ($true = ((member_a @ (auto_ll_on_flow0_a @ f @ x @ X3 @ (sK1 @ X3)) @ (line_open_segment_a @ a2 @ b))))) )),
% 23.63/3.88 inference(cnf_transformation,[],[f997])).
% 23.63/3.88 thf(f1016,plain,(
% 23.63/3.88 ( ! [X2 : a] : (($true = ((ord_less_real @ (abs_abs_real @ (sK1 @ X2)) @ one_one_real))) | ($true != ((member_a @ X2 @ (elemen154694473ball_a @ p @ sK0))))) )),
% 23.63/3.88 inference(cnf_transformation,[],[f997])).
% 23.63/3.88 thf(f1018,plain,(
% 23.63/3.88 (zero_zero_real = ((sK1 @ p)))),
% 23.63/3.88 inference(cnf_transformation,[],[f997])).
% 23.63/3.88 thf(f1168,plain,(
% 23.63/3.88 (abs_abs_real = (^[Y0 : real]: (if_real @ (ord_less_real @ Y0 @ zero_zero_real) @ (uminus_uminus_real @ Y0) @ Y0)))),
% 23.63/3.88 inference(cnf_transformation,[],[f528])).
% 23.63/3.88 thf(f1375,plain,(
% 23.63/3.88 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 23.63/3.88 inference(cnf_transformation,[],[f733])).
% 23.63/3.88 thf(f1378,plain,(
% 23.63/3.88 ( ! [X0 : real,X1 : (a > real)] : ((thesisa = $true) | ($true = ((member_a @ (sK14 @ X1 @ X0) @ (elemen154694473ball_a @ p @ X0)))) | ($true = ((member_a @ (sK15 @ X1 @ X0) @ (elemen154694473ball_a @ p @ X0)))) | (zero_zero_real != ((X1 @ p))) | (((topolo1710226732a_real @ (elemen154694473ball_a @ p @ X0) @ X1)) != $true) | (((ord_less_real @ zero_zero_real @ X0)) != $true)) )),
% 23.63/3.88 inference(cnf_transformation,[],[f1009])).
% 23.63/3.88 thf(f1379,plain,(
% 23.63/3.88 ( ! [X0 : real,X1 : (a > real)] : ((thesisa = $true) | ($true = ((member_a @ (sK14 @ X1 @ X0) @ (elemen154694473ball_a @ p @ X0)))) | ($true != ((ord_less_real @ (abs_abs_real @ (X1 @ (sK15 @ X1 @ X0))) @ one_one_real))) | (zero_zero_real != ((X1 @ p))) | (((topolo1710226732a_real @ (elemen154694473ball_a @ p @ X0) @ X1)) != $true) | (((ord_less_real @ zero_zero_real @ X0)) != $true)) )),
% 23.63/3.88 inference(cnf_transformation,[],[f1009])).
% 23.63/3.88 thf(f1380,plain,(
% 23.63/3.88 ( ! [X0 : real,X1 : (a > real)] : ((thesisa = $true) | ($true != ((member_a @ (auto_ll_on_flow0_a @ f @ x @ (sK14 @ X1 @ X0) @ (X1 @ (sK14 @ X1 @ X0))) @ (line_open_segment_a @ a2 @ b)))) | ($true = ((member_a @ (sK15 @ X1 @ X0) @ (elemen154694473ball_a @ p @ X0)))) | (zero_zero_real != ((X1 @ p))) | (((topolo1710226732a_real @ (elemen154694473ball_a @ p @ X0) @ X1)) != $true) | (((ord_less_real @ zero_zero_real @ X0)) != $true)) )),
% 23.63/3.88 inference(cnf_transformation,[],[f1009])).
% 23.63/3.88 thf(f1381,plain,(
% 23.63/3.88 ( ! [X0 : real,X1 : (a > real)] : ((thesisa = $true) | ($true != ((member_a @ (auto_ll_on_flow0_a @ f @ x @ (sK14 @ X1 @ X0) @ (X1 @ (sK14 @ X1 @ X0))) @ (line_open_segment_a @ a2 @ b)))) | ($true != ((ord_less_real @ (abs_abs_real @ (X1 @ (sK15 @ X1 @ X0))) @ one_one_real))) | (zero_zero_real != ((X1 @ p))) | (((topolo1710226732a_real @ (elemen154694473ball_a @ p @ X0) @ X1)) != $true) | (((ord_less_real @ zero_zero_real @ X0)) != $true)) )),
% 23.63/3.88 inference(cnf_transformation,[],[f1009])).
% 23.63/3.88 thf(f1382,plain,(
% 23.63/3.88 (thesisa != $true)),
% 23.63/3.88 inference(cnf_transformation,[],[f754])).
% 23.63/3.88 thf(f1385,plain,(
% 23.63/3.88 ( ! [X2 : a] : (($true = ((ord_less_real @ ((^[Y0 : real]: (if_real @ (ord_less_real @ Y0 @ zero_zero_real) @ (uminus_uminus_real @ Y0) @ Y0)) @ (sK1 @ X2)) @ one_one_real))) | ($true != ((member_a @ X2 @ (elemen154694473ball_a @ p @ sK0))))) )),
% 23.63/3.88 inference(definition_unfolding,[],[f1016,f1168])).
% 23.63/3.88 thf(f1414,plain,(
% 23.63/3.88 ( ! [X0 : real,X1 : (a > real)] : ((thesisa = $true) | ($true != ((member_a @ (auto_ll_on_flow0_a @ f @ x @ (sK14 @ X1 @ X0) @ (X1 @ (sK14 @ X1 @ X0))) @ (line_open_segment_a @ a2 @ b)))) | ($true != ((ord_less_real @ ((^[Y0 : real]: (if_real @ (ord_less_real @ Y0 @ zero_zero_real) @ (uminus_uminus_real @ Y0) @ Y0)) @ (X1 @ (sK15 @ X1 @ X0))) @ one_one_real))) | (zero_zero_real != ((X1 @ p))) | (((topolo1710226732a_real @ (elemen154694473ball_a @ p @ X0) @ X1)) != $true) | (((ord_less_real @ zero_zero_real @ X0)) != $true)) )),
% 23.63/3.88 inference(definition_unfolding,[],[f1381,f1168])).
% 23.63/3.88 thf(f1415,plain,(
% 23.63/3.88 ( ! [X0 : real,X1 : (a > real)] : ((thesisa = $true) | ($true = ((member_a @ (sK14 @ X1 @ X0) @ (elemen154694473ball_a @ p @ X0)))) | ($true != ((ord_less_real @ ((^[Y0 : real]: (if_real @ (ord_less_real @ Y0 @ zero_zero_real) @ (uminus_uminus_real @ Y0) @ Y0)) @ (X1 @ (sK15 @ X1 @ X0))) @ one_one_real))) | (zero_zero_real != ((X1 @ p))) | (((topolo1710226732a_real @ (elemen154694473ball_a @ p @ X0) @ X1)) != $true) | (((ord_less_real @ zero_zero_real @ X0)) != $true)) )),
% 23.63/3.88 inference(definition_unfolding,[],[f1379,f1168])).
% 23.63/3.88 thf(f1428,plain,(
% 23.63/3.88 ( ! [X0 : real,X1 : (a > real)] : ((thesisa = $true) | ($true = ((member_a @ (sK14 @ X1 @ X0) @ (elemen154694473ball_a @ p @ X0)))) | ($true != ((ord_less_real @ (if_real @ (ord_less_real @ (X1 @ (sK15 @ X1 @ X0)) @ zero_zero_real) @ (uminus_uminus_real @ (X1 @ (sK15 @ X1 @ X0))) @ (X1 @ (sK15 @ X1 @ X0))) @ one_one_real))) | (zero_zero_real != ((X1 @ p))) | (((topolo1710226732a_real @ (elemen154694473ball_a @ p @ X0) @ X1)) != $true) | (((ord_less_real @ zero_zero_real @ X0)) != $true)) )),
% 23.63/3.88 inference(beta-eta_normalization,[],[f1415])).
% 23.63/3.88 thf(f1429,plain,(
% 23.63/3.88 ( ! [X0 : real,X1 : (a > real)] : ((thesisa = $true) | ($true != ((member_a @ (auto_ll_on_flow0_a @ f @ x @ (sK14 @ X1 @ X0) @ (X1 @ (sK14 @ X1 @ X0))) @ (line_open_segment_a @ a2 @ b)))) | ($true != ((ord_less_real @ (if_real @ (ord_less_real @ (X1 @ (sK15 @ X1 @ X0)) @ zero_zero_real) @ (uminus_uminus_real @ (X1 @ (sK15 @ X1 @ X0))) @ (X1 @ (sK15 @ X1 @ X0))) @ one_one_real))) | (zero_zero_real != ((X1 @ p))) | (((topolo1710226732a_real @ (elemen154694473ball_a @ p @ X0) @ X1)) != $true) | (((ord_less_real @ zero_zero_real @ X0)) != $true)) )),
% 23.63/3.88 inference(beta-eta_normalization,[],[f1414])).
% 23.63/3.88 thf(f1988,plain,(
% 23.63/3.88 ( ! [X2 : a] : (($true != ((member_a @ X2 @ (elemen154694473ball_a @ p @ sK0)))) | ($true = ((ord_less_real @ (if_real @ (ord_less_real @ (sK1 @ X2) @ zero_zero_real) @ (uminus_uminus_real @ (sK1 @ X2)) @ (sK1 @ X2)) @ one_one_real)))) )),
% 23.63/3.88 inference(beta-eta_normalization,[],[f1385])).
% 23.63/3.88 thf(f1989,plain,(
% 23.63/3.88 ( ! [X0 : real,X1 : (a > real)] : ((((ord_less_real @ zero_zero_real @ X0)) != $true) | ($true = ((member_a @ (sK15 @ X1 @ X0) @ (elemen154694473ball_a @ p @ X0)))) | (zero_zero_real != ((X1 @ p))) | (((topolo1710226732a_real @ (elemen154694473ball_a @ p @ X0) @ X1)) != $true) | ($true = ((member_a @ (sK14 @ X1 @ X0) @ (elemen154694473ball_a @ p @ X0))))) )),
% 23.63/3.88 inference(forward_subsumption_resolution,[],[f1378,f1382])).
% 23.63/3.88 thf(f1990,plain,(
% 23.63/3.88 ( ! [X0 : real,X1 : (a > real)] : ((((ord_less_real @ zero_zero_real @ X0)) != $true) | ($true != ((ord_less_real @ (if_real @ (ord_less_real @ (X1 @ (sK15 @ X1 @ X0)) @ zero_zero_real) @ (uminus_uminus_real @ (X1 @ (sK15 @ X1 @ X0))) @ (X1 @ (sK15 @ X1 @ X0))) @ one_one_real))) | (zero_zero_real != ((X1 @ p))) | (((topolo1710226732a_real @ (elemen154694473ball_a @ p @ X0) @ X1)) != $true) | ($true = ((member_a @ (sK14 @ X1 @ X0) @ (elemen154694473ball_a @ p @ X0))))) )),
% 23.63/3.88 inference(forward_subsumption_resolution,[],[f1428,f1382])).
% 23.63/3.88 thf(f1991,plain,(
% 23.63/3.88 ( ! [X0 : real,X1 : (a > real)] : ((((ord_less_real @ zero_zero_real @ X0)) != $true) | ($true = ((member_a @ (sK15 @ X1 @ X0) @ (elemen154694473ball_a @ p @ X0)))) | (zero_zero_real != ((X1 @ p))) | (((topolo1710226732a_real @ (elemen154694473ball_a @ p @ X0) @ X1)) != $true) | ($true != ((member_a @ (auto_ll_on_flow0_a @ f @ x @ (sK14 @ X1 @ X0) @ (X1 @ (sK14 @ X1 @ X0))) @ (line_open_segment_a @ a2 @ b))))) )),
% 23.63/3.88 inference(forward_subsumption_resolution,[],[f1380,f1382])).
% 23.63/3.88 thf(f1992,plain,(
% 23.63/3.88 ( ! [X0 : real,X1 : (a > real)] : ((((ord_less_real @ zero_zero_real @ X0)) != $true) | ($true != ((ord_less_real @ (if_real @ (ord_less_real @ (X1 @ (sK15 @ X1 @ X0)) @ zero_zero_real) @ (uminus_uminus_real @ (X1 @ (sK15 @ X1 @ X0))) @ (X1 @ (sK15 @ X1 @ X0))) @ one_one_real))) | (zero_zero_real != ((X1 @ p))) | (((topolo1710226732a_real @ (elemen154694473ball_a @ p @ X0) @ X1)) != $true) | ($true != ((member_a @ (auto_ll_on_flow0_a @ f @ x @ (sK14 @ X1 @ X0) @ (X1 @ (sK14 @ X1 @ X0))) @ (line_open_segment_a @ a2 @ b))))) )),
% 23.63/3.88 inference(forward_subsumption_resolution,[],[f1429,f1382])).
% 23.63/3.88 thf(f2049,plain,(
% 23.63/3.88 ( ! [X0 : (a > real)] : (($true != $true) | ($true = ((member_a @ (sK15 @ X0 @ sK0) @ (elemen154694473ball_a @ p @ sK0)))) | (zero_zero_real != ((X0 @ p))) | ($true != ((topolo1710226732a_real @ (elemen154694473ball_a @ p @ sK0) @ X0))) | ($true = ((member_a @ (sK14 @ X0 @ sK0) @ (elemen154694473ball_a @ p @ sK0))))) )),
% 23.63/3.88 inference(constrained_superposition,[],[f1989,f1013])).
% 23.63/3.88 thf(f2050,plain,(
% 23.63/3.88 ( ! [X0 : (a > real)] : (($true != ((topolo1710226732a_real @ (elemen154694473ball_a @ p @ sK0) @ X0))) | (zero_zero_real != ((X0 @ p))) | ($true = ((member_a @ (sK15 @ X0 @ sK0) @ (elemen154694473ball_a @ p @ sK0)))) | ($true = ((member_a @ (sK14 @ X0 @ sK0) @ (elemen154694473ball_a @ p @ sK0))))) )),
% 23.63/3.88 inference(trivial_inequality_removal,[],[f2049])).
% 23.63/3.88 thf(f2059,plain,(
% 23.63/3.88 ( ! [X0 : (a > real)] : (($true != $true) | (zero_zero_real != ((X0 @ p))) | ($true = ((member_a @ (sK15 @ X0 @ sK0) @ (elemen154694473ball_a @ p @ sK0)))) | ($true = ((member_a @ (sK14 @ X0 @ sK0) @ (elemen154694473ball_a @ p @ sK0)))) | ($false = ((topolo1710226732a_real @ (elemen154694473ball_a @ p @ sK0) @ X0)))) )),
% 23.63/3.88 inference(constrained_superposition,[],[f2050,f1375])).
% 23.63/3.88 thf(f2060,plain,(
% 23.63/3.88 ( ! [X0 : (a > real)] : ((zero_zero_real != ((X0 @ p))) | ($true = ((member_a @ (sK15 @ X0 @ sK0) @ (elemen154694473ball_a @ p @ sK0)))) | ($true = ((member_a @ (sK14 @ X0 @ sK0) @ (elemen154694473ball_a @ p @ sK0)))) | ($false = ((topolo1710226732a_real @ (elemen154694473ball_a @ p @ sK0) @ X0)))) )),
% 23.63/3.88 inference(trivial_inequality_removal,[],[f2059])).
% 23.63/3.88 thf(f2067,plain,(
% 23.63/3.88 (zero_zero_real != zero_zero_real) | ($true = ((member_a @ (sK15 @ (^[Y0 : a]: (sK1 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ sK0) @ (elemen154694473ball_a @ p @ sK0)))) | ($true = ((member_a @ (sK14 @ (^[Y0 : a]: (sK1 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ sK0) @ (elemen154694473ball_a @ p @ sK0)))) | ($false = ((topolo1710226732a_real @ (elemen154694473ball_a @ p @ sK0) @ (^[Y0 : a]: (sK1 @ ((^[Y1 : a]: (Y1)) @ Y0))))))),
% 23.63/3.88 inference(constrained_superposition,[],[f2060,f1018])).
% 23.63/3.88 thf(f2077,plain,(
% 23.63/3.88 ($true = ((member_a @ (sK15 @ (^[Y0 : a]: (sK1 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ sK0) @ (elemen154694473ball_a @ p @ sK0)))) | ($true = ((member_a @ (sK14 @ (^[Y0 : a]: (sK1 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ sK0) @ (elemen154694473ball_a @ p @ sK0)))) | ($false = ((topolo1710226732a_real @ (elemen154694473ball_a @ p @ sK0) @ (^[Y0 : a]: (sK1 @ ((^[Y1 : a]: (Y1)) @ Y0))))))),
% 23.63/3.88 inference(trivial_inequality_removal,[],[f2067])).
% 23.63/3.88 thf(f2078,plain,(
% 23.63/3.88 ($true = ((member_a @ (sK15 @ sK1 @ sK0) @ (elemen154694473ball_a @ p @ sK0)))) | ($true = ((member_a @ (sK14 @ sK1 @ sK0) @ (elemen154694473ball_a @ p @ sK0)))) | ($false = ((topolo1710226732a_real @ (elemen154694473ball_a @ p @ sK0) @ sK1)))),
% 23.63/3.88 inference(beta-eta_normalization,[],[f2077])).
% 23.63/3.88 thf(f2079,plain,(
% 23.63/3.88 ($true = $false) | ($true = ((member_a @ (sK15 @ sK1 @ sK0) @ (elemen154694473ball_a @ p @ sK0)))) | ($true = ((member_a @ (sK14 @ sK1 @ sK0) @ (elemen154694473ball_a @ p @ sK0))))),
% 23.63/3.88 inference(forward_demodulation,[],[f2078,f1014])).
% 23.63/3.88 thf(f2080,plain,(
% 23.63/3.88 ($true = ((member_a @ (sK15 @ sK1 @ sK0) @ (elemen154694473ball_a @ p @ sK0)))) | ($true = ((member_a @ (sK14 @ sK1 @ sK0) @ (elemen154694473ball_a @ p @ sK0))))),
% 23.63/3.88 inference(trivial_inequality_removal,[],[f2079])).
% 23.63/3.88 thf(f2142,plain,(
% 23.63/3.88 ( ! [X0 : (a > real)] : (($true != $true) | ($true = ((member_a @ (sK15 @ X0 @ sK0) @ (elemen154694473ball_a @ p @ sK0)))) | (zero_zero_real != ((X0 @ p))) | ($true != ((topolo1710226732a_real @ (elemen154694473ball_a @ p @ sK0) @ X0))) | ($true != ((member_a @ (auto_ll_on_flow0_a @ f @ x @ (sK14 @ X0 @ sK0) @ (X0 @ (sK14 @ X0 @ sK0))) @ (line_open_segment_a @ a2 @ b))))) )),
% 23.63/3.88 inference(constrained_superposition,[],[f1991,f1013])).
% 23.63/3.88 thf(f2145,plain,(
% 23.63/3.88 ( ! [X0 : (a > real)] : (($true != ((topolo1710226732a_real @ (elemen154694473ball_a @ p @ sK0) @ X0))) | (zero_zero_real != ((X0 @ p))) | ($true = ((member_a @ (sK15 @ X0 @ sK0) @ (elemen154694473ball_a @ p @ sK0)))) | ($true != ((member_a @ (auto_ll_on_flow0_a @ f @ x @ (sK14 @ X0 @ sK0) @ (X0 @ (sK14 @ X0 @ sK0))) @ (line_open_segment_a @ a2 @ b))))) )),
% 23.63/3.88 inference(trivial_inequality_removal,[],[f2142])).
% 23.63/3.88 thf(f2256,plain,(
% 23.63/3.88 ( ! [X0 : (a > real)] : (($true != $true) | ($true != ((ord_less_real @ (if_real @ (ord_less_real @ (X0 @ (sK15 @ X0 @ sK0)) @ zero_zero_real) @ (uminus_uminus_real @ (X0 @ (sK15 @ X0 @ sK0))) @ (X0 @ (sK15 @ X0 @ sK0))) @ one_one_real))) | (zero_zero_real != ((X0 @ p))) | ($true != ((topolo1710226732a_real @ (elemen154694473ball_a @ p @ sK0) @ X0))) | ($true = ((member_a @ (sK14 @ X0 @ sK0) @ (elemen154694473ball_a @ p @ sK0))))) )),
% 23.63/3.88 inference(constrained_superposition,[],[f1990,f1013])).
% 23.63/3.88 thf(f2259,plain,(
% 23.63/3.88 ( ! [X0 : (a > real)] : (($true != ((topolo1710226732a_real @ (elemen154694473ball_a @ p @ sK0) @ X0))) | (zero_zero_real != ((X0 @ p))) | ($true != ((ord_less_real @ (if_real @ (ord_less_real @ (X0 @ (sK15 @ X0 @ sK0)) @ zero_zero_real) @ (uminus_uminus_real @ (X0 @ (sK15 @ X0 @ sK0))) @ (X0 @ (sK15 @ X0 @ sK0))) @ one_one_real))) | ($true = ((member_a @ (sK14 @ X0 @ sK0) @ (elemen154694473ball_a @ p @ sK0))))) )),
% 23.63/3.88 inference(trivial_inequality_removal,[],[f2256])).
% 23.63/3.88 thf(f2332,plain,(
% 23.63/3.88 ( ! [X0 : (a > real)] : (($true != $true) | ($true != ((ord_less_real @ (if_real @ (ord_less_real @ (X0 @ (sK15 @ X0 @ sK0)) @ zero_zero_real) @ (uminus_uminus_real @ (X0 @ (sK15 @ X0 @ sK0))) @ (X0 @ (sK15 @ X0 @ sK0))) @ one_one_real))) | (zero_zero_real != ((X0 @ p))) | ($true != ((topolo1710226732a_real @ (elemen154694473ball_a @ p @ sK0) @ X0))) | ($true != ((member_a @ (auto_ll_on_flow0_a @ f @ x @ (sK14 @ X0 @ sK0) @ (X0 @ (sK14 @ X0 @ sK0))) @ (line_open_segment_a @ a2 @ b))))) )),
% 23.63/3.88 inference(constrained_superposition,[],[f1992,f1013])).
% 23.63/3.88 thf(f2335,plain,(
% 23.63/3.88 ( ! [X0 : (a > real)] : (($true != ((topolo1710226732a_real @ (elemen154694473ball_a @ p @ sK0) @ X0))) | (zero_zero_real != ((X0 @ p))) | ($true != ((ord_less_real @ (if_real @ (ord_less_real @ (X0 @ (sK15 @ X0 @ sK0)) @ zero_zero_real) @ (uminus_uminus_real @ (X0 @ (sK15 @ X0 @ sK0))) @ (X0 @ (sK15 @ X0 @ sK0))) @ one_one_real))) | ($true != ((member_a @ (auto_ll_on_flow0_a @ f @ x @ (sK14 @ X0 @ sK0) @ (X0 @ (sK14 @ X0 @ sK0))) @ (line_open_segment_a @ a2 @ b))))) )),
% 23.63/3.88 inference(trivial_inequality_removal,[],[f2332])).
% 23.63/3.88 thf(f3578,plain,(
% 23.63/3.88 ($true != $true) | (zero_zero_real != ((sK1 @ p))) | ($true = ((member_a @ (sK15 @ sK1 @ sK0) @ (elemen154694473ball_a @ p @ sK0)))) | ($true != ((member_a @ (auto_ll_on_flow0_a @ f @ x @ (sK14 @ sK1 @ sK0) @ (sK1 @ (sK14 @ sK1 @ sK0))) @ (line_open_segment_a @ a2 @ b))))),
% 23.63/3.88 inference(constrained_superposition,[],[f2145,f1014])).
% 23.63/3.88 thf(f3579,plain,(
% 23.63/3.88 (zero_zero_real != ((sK1 @ p))) | ($true = ((member_a @ (sK15 @ sK1 @ sK0) @ (elemen154694473ball_a @ p @ sK0)))) | ($true != ((member_a @ (auto_ll_on_flow0_a @ f @ x @ (sK14 @ sK1 @ sK0) @ (sK1 @ (sK14 @ sK1 @ sK0))) @ (line_open_segment_a @ a2 @ b))))),
% 23.63/3.88 inference(trivial_inequality_removal,[],[f3578])).
% 23.63/3.88 thf(f3581,plain,(
% 23.63/3.88 ($true != ((member_a @ (auto_ll_on_flow0_a @ f @ x @ (sK14 @ sK1 @ sK0) @ (sK1 @ (sK14 @ sK1 @ sK0))) @ (line_open_segment_a @ a2 @ b)))) | ($true = ((member_a @ (sK15 @ sK1 @ sK0) @ (elemen154694473ball_a @ p @ sK0))))),
% 23.63/3.88 inference(forward_subsumption_resolution,[],[f3579,f1018])).
% 23.63/3.88 thf(f4293,plain,(
% 23.63/3.88 ($true != $true) | ($true = ((ord_less_real @ (if_real @ (ord_less_real @ (sK1 @ (sK15 @ sK1 @ sK0)) @ zero_zero_real) @ (uminus_uminus_real @ (sK1 @ (sK15 @ sK1 @ sK0))) @ (sK1 @ (sK15 @ sK1 @ sK0))) @ one_one_real))) | ($true = ((member_a @ (sK14 @ sK1 @ sK0) @ (elemen154694473ball_a @ p @ sK0))))),
% 23.63/3.88 inference(constrained_superposition,[],[f1988,f2080])).
% 23.63/3.88 thf(f4354,plain,(
% 23.63/3.88 ($true = ((ord_less_real @ (if_real @ (ord_less_real @ (sK1 @ (sK15 @ sK1 @ sK0)) @ zero_zero_real) @ (uminus_uminus_real @ (sK1 @ (sK15 @ sK1 @ sK0))) @ (sK1 @ (sK15 @ sK1 @ sK0))) @ one_one_real))) | ($true = ((member_a @ (sK14 @ sK1 @ sK0) @ (elemen154694473ball_a @ p @ sK0))))),
% 23.63/3.88 inference(trivial_inequality_removal,[],[f4293])).
% 23.63/3.88 thf(f5324,plain,(
% 23.63/3.88 ($true != $true) | (zero_zero_real != ((sK1 @ p))) | ($true != ((ord_less_real @ (if_real @ (ord_less_real @ (sK1 @ (sK15 @ sK1 @ sK0)) @ zero_zero_real) @ (uminus_uminus_real @ (sK1 @ (sK15 @ sK1 @ sK0))) @ (sK1 @ (sK15 @ sK1 @ sK0))) @ one_one_real))) | ($true = ((member_a @ (sK14 @ sK1 @ sK0) @ (elemen154694473ball_a @ p @ sK0))))),
% 23.63/3.88 inference(constrained_superposition,[],[f2259,f1014])).
% 23.63/3.88 thf(f5325,plain,(
% 23.63/3.88 (zero_zero_real != ((sK1 @ p))) | ($true != ((ord_less_real @ (if_real @ (ord_less_real @ (sK1 @ (sK15 @ sK1 @ sK0)) @ zero_zero_real) @ (uminus_uminus_real @ (sK1 @ (sK15 @ sK1 @ sK0))) @ (sK1 @ (sK15 @ sK1 @ sK0))) @ one_one_real))) | ($true = ((member_a @ (sK14 @ sK1 @ sK0) @ (elemen154694473ball_a @ p @ sK0))))),
% 23.63/3.88 inference(trivial_inequality_removal,[],[f5324])).
% 23.63/3.88 thf(f5327,plain,(
% 23.63/3.88 ($true != ((ord_less_real @ (if_real @ (ord_less_real @ (sK1 @ (sK15 @ sK1 @ sK0)) @ zero_zero_real) @ (uminus_uminus_real @ (sK1 @ (sK15 @ sK1 @ sK0))) @ (sK1 @ (sK15 @ sK1 @ sK0))) @ one_one_real))) | ($true = ((member_a @ (sK14 @ sK1 @ sK0) @ (elemen154694473ball_a @ p @ sK0))))),
% 23.63/3.88 inference(forward_subsumption_resolution,[],[f5325,f1018])).
% 23.63/3.88 thf(f5328,plain,(
% 23.63/3.88 ($true = ((member_a @ (sK14 @ sK1 @ sK0) @ (elemen154694473ball_a @ p @ sK0))))),
% 23.63/3.88 inference(forward_subsumption_resolution,[],[f5327,f4354])).
% 23.63/3.88 thf(f5330,plain,(
% 23.63/3.88 ($true != $true) | ($true = ((member_a @ (auto_ll_on_flow0_a @ f @ x @ (sK14 @ sK1 @ sK0) @ (sK1 @ (sK14 @ sK1 @ sK0))) @ (line_open_segment_a @ a2 @ b))))),
% 23.63/3.88 inference(constrained_superposition,[],[f1015,f5328])).
% 23.63/3.88 thf(f5331,plain,(
% 23.63/3.88 ($true = ((member_a @ (auto_ll_on_flow0_a @ f @ x @ (sK14 @ sK1 @ sK0) @ (sK1 @ (sK14 @ sK1 @ sK0))) @ (line_open_segment_a @ a2 @ b))))),
% 23.63/3.88 inference(trivial_inequality_removal,[],[f5330])).
% 23.63/3.88 thf(f5458,plain,(
% 23.63/3.88 ($true != $true) | ($true = ((member_a @ (sK15 @ sK1 @ sK0) @ (elemen154694473ball_a @ p @ sK0))))),
% 23.63/3.88 inference(constrained_superposition,[],[f3581,f5331])).
% 23.63/3.88 thf(f5459,plain,(
% 23.63/3.88 ($true = ((member_a @ (sK15 @ sK1 @ sK0) @ (elemen154694473ball_a @ p @ sK0))))),
% 23.63/3.88 inference(trivial_inequality_removal,[],[f5458])).
% 23.63/3.88 thf(f5568,plain,(
% 23.63/3.88 ($true != $true) | ($true = ((ord_less_real @ (if_real @ (ord_less_real @ (sK1 @ (sK15 @ sK1 @ sK0)) @ zero_zero_real) @ (uminus_uminus_real @ (sK1 @ (sK15 @ sK1 @ sK0))) @ (sK1 @ (sK15 @ sK1 @ sK0))) @ one_one_real)))),
% 23.63/3.88 inference(constrained_superposition,[],[f1988,f5459])).
% 23.63/3.88 thf(f5571,plain,(
% 23.63/3.88 ($true = ((ord_less_real @ (if_real @ (ord_less_real @ (sK1 @ (sK15 @ sK1 @ sK0)) @ zero_zero_real) @ (uminus_uminus_real @ (sK1 @ (sK15 @ sK1 @ sK0))) @ (sK1 @ (sK15 @ sK1 @ sK0))) @ one_one_real)))),
% 23.63/3.88 inference(trivial_inequality_removal,[],[f5568])).
% 23.63/3.88 thf(f6451,plain,(
% 23.63/3.88 ($true != $true) | (zero_zero_real != ((sK1 @ p))) | ($true != ((ord_less_real @ (if_real @ (ord_less_real @ (sK1 @ (sK15 @ sK1 @ sK0)) @ zero_zero_real) @ (uminus_uminus_real @ (sK1 @ (sK15 @ sK1 @ sK0))) @ (sK1 @ (sK15 @ sK1 @ sK0))) @ one_one_real))) | ($true != ((member_a @ (auto_ll_on_flow0_a @ f @ x @ (sK14 @ sK1 @ sK0) @ (sK1 @ (sK14 @ sK1 @ sK0))) @ (line_open_segment_a @ a2 @ b))))),
% 23.63/3.88 inference(constrained_superposition,[],[f2335,f1014])).
% 23.63/3.88 thf(f6452,plain,(
% 23.63/3.88 (zero_zero_real != ((sK1 @ p))) | ($true != ((ord_less_real @ (if_real @ (ord_less_real @ (sK1 @ (sK15 @ sK1 @ sK0)) @ zero_zero_real) @ (uminus_uminus_real @ (sK1 @ (sK15 @ sK1 @ sK0))) @ (sK1 @ (sK15 @ sK1 @ sK0))) @ one_one_real))) | ($true != ((member_a @ (auto_ll_on_flow0_a @ f @ x @ (sK14 @ sK1 @ sK0) @ (sK1 @ (sK14 @ sK1 @ sK0))) @ (line_open_segment_a @ a2 @ b))))),
% 23.63/3.88 inference(trivial_inequality_removal,[],[f6451])).
% 23.63/3.88 thf(f6454,plain,(
% 23.63/3.88 ($true != ((ord_less_real @ (if_real @ (ord_less_real @ (sK1 @ (sK15 @ sK1 @ sK0)) @ zero_zero_real) @ (uminus_uminus_real @ (sK1 @ (sK15 @ sK1 @ sK0))) @ (sK1 @ (sK15 @ sK1 @ sK0))) @ one_one_real))) | ($true != ((member_a @ (auto_ll_on_flow0_a @ f @ x @ (sK14 @ sK1 @ sK0) @ (sK1 @ (sK14 @ sK1 @ sK0))) @ (line_open_segment_a @ a2 @ b))))),
% 23.63/3.88 inference(forward_subsumption_resolution,[],[f6452,f1018])).
% 23.63/3.88 thf(f6455,plain,(
% 23.63/3.88 ($true != ((member_a @ (auto_ll_on_flow0_a @ f @ x @ (sK14 @ sK1 @ sK0) @ (sK1 @ (sK14 @ sK1 @ sK0))) @ (line_open_segment_a @ a2 @ b))))),
% 23.63/3.88 inference(forward_subsumption_resolution,[],[f6454,f5571])).
% 23.63/3.88 thf(f6456,plain,(
% 23.63/3.88 $false),
% 23.63/3.88 inference(forward_subsumption_resolution,[],[f6455,f5331])).
% 23.63/3.88 % SZS output end Proof for theBenchmark
% 23.63/3.88 % (1237512)------------------------------
% 23.63/3.88 % (1237512)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.63/3.88 % (1237512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.63/3.88 % (1237512)CaDiCaL version: 2.1.3
% 23.63/3.88 % (1237512)Termination reason: Refutation
% 23.63/3.88 % (1237512)Time elapsed: 0.652 s
% 23.63/3.88 % (1237512)Peak memory usage: 19 MB
% 23.63/3.88 % (1237512)Instructions burned: 1362 (million)
% 23.63/3.88 % (1237308)Success in time 3.657 s
% 23.63/3.88 % Vampire exiting
%------------------------------------------------------------------------------