%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP111^2 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n003.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:08:23 AM UTC 2026
% Result : Theorem 0.50s 0.44s
% Output : Refutation 0.50s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP111^2 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n003.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Tue Sep 29 19:56:59 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running higher-order theorem proving
% 0.21/0.27 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.50/0.41 % (2982334)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.50/0.41 % (2982343)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=3376821441:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.50/0.41 % (2982345)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.50/0.41 % (2982345)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.50/0.41 % (2982343)Instruction limit reached!
% 0.50/0.41 % (2982343)------------------------------
% 0.50/0.41 % (2982343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.41 % (2982343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.41 % (2982343)CaDiCaL version: 2.1.3
% 0.50/0.41 % (2982343)Termination reason: Instruction limit
% 0.50/0.41 % (2982343)Termination phase: Unused predicate definition removal
% 0.50/0.41 % (2982343)Time elapsed: 0.007 s
% 0.50/0.41 % (2982343)Peak memory usage: 10 MB
% 0.50/0.41 % (2982341)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=4023007034:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.50/0.41 % (2982340)lrs+10_16_si=on:nwc=1.5:random_seed=2166310936:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.50/0.41 % (2982339)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=2175480383:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.50/0.41 % (2982343)Instructions burned: 28 (million)
% 0.50/0.41 % (2982342)dis+1002_4:1_sfv=off:to=lpo:plsq=on:fde=none:e2e=on:si=on:spb=non_intro:acc=on:uwa=off:fd=preordered:foolp=on:s2agt=32:slsqc=1:slsq=on:random_seed=341802282:hsq=on:hsqr=16,1:s2a=on:i=634:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2999 on theBenchmark for (2999ds/634Mi)
% 0.50/0.41 % (2982344)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=760771188:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.50/0.41 % (2982345)dis+1002_8_to=kbo:sil=128000:tgt=full:drc=off:si=on:sp=const_max:lma=off:spb=non_intro:cbe=off:uwa=interpreted_only:random_seed=2058659196:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.50/0.41 % (2982341)Instruction limit reached!
% 0.50/0.41 % (2982341)------------------------------
% 0.50/0.41 % (2982341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.41 % (2982341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.41 % (2982341)CaDiCaL version: 2.1.3
% 0.50/0.41 % (2982341)Termination reason: Instruction limit
% 0.50/0.41 % (2982341)Termination phase: shuffling
% 0.50/0.41 % (2982341)Time elapsed: 0.002 s
% 0.50/0.41 % (2982341)Peak memory usage: 10 MB
% 0.50/0.41 % (2982341)Instructions burned: 4 (million)
% 0.50/0.41 % (2982352)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3470865730:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.50/0.41 % (2982352)Instruction limit reached!
% 0.50/0.41 % (2982352)------------------------------
% 0.50/0.41 % (2982352)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.41 % (2982352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.41 % (2982352)CaDiCaL version: 2.1.3
% 0.50/0.41 % (2982352)Termination reason: Instruction limit
% 0.50/0.41 % (2982352)Termination phase: shuffling
% 0.50/0.41 % (2982352)Time elapsed: 0.001 s
% 0.50/0.41 % (2982352)Peak memory usage: 10 MB
% 0.50/0.41 % (2982352)Instructions burned: 2 (million)
% 0.50/0.41 % (2982340)Instruction limit reached!
% 0.50/0.41 % (2982340)------------------------------
% 0.50/0.41 % (2982340)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.41 % (2982340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.41 % (2982340)CaDiCaL version: 2.1.3
% 0.50/0.41 % (2982340)Termination reason: Instruction limit
% 0.50/0.41 % (2982340)Termination phase: Property scanning
% 0.50/0.41 % (2982340)Time elapsed: 0.018 s
% 0.50/0.41 % (2982340)Peak memory usage: 10 MB
% 0.50/0.41 % (2982340)Instructions burned: 20 (million)
% 0.50/0.41 % (2982356)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.50/0.44 % (2982356)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1579068935:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.50/0.44 % (2982354)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=3178205343:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.50/0.44 % (2982356)Instruction limit reached!
% 0.50/0.44 % (2982356)------------------------------
% 0.50/0.44 % (2982356)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.44 % (2982356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.44 % (2982356)CaDiCaL version: 2.1.3
% 0.50/0.44 % (2982356)Termination reason: Instruction limit
% 0.50/0.44 % (2982356)Termination phase: shuffling
% 0.50/0.44 % (2982356)Time elapsed: 0.002 s
% 0.50/0.44 % (2982356)Peak memory usage: 10 MB
% 0.50/0.44 % (2982356)Instructions burned: 7 (million)
% 0.50/0.44 % (2982354)Instruction limit reached!
% 0.50/0.44 % (2982354)------------------------------
% 0.50/0.44 % (2982354)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.44 % (2982354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.44 % (2982354)CaDiCaL version: 2.1.3
% 0.50/0.44 % (2982354)Termination reason: Instruction limit
% 0.50/0.44 % (2982354)Termination phase: shuffling
% 0.50/0.44 % (2982354)Time elapsed: 0.006 s
% 0.50/0.44 % (2982354)Peak memory usage: 10 MB
% 0.50/0.44 % (2982354)Instructions burned: 5 (million)
% 0.50/0.44 % (2982360)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.50/0.44 % (2982360)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.50/0.44 % (2982344)Instruction limit reached!
% 0.50/0.44 % (2982344)------------------------------
% 0.50/0.44 % (2982344)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.44 % (2982344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.44 % (2982344)CaDiCaL version: 2.1.3
% 0.50/0.44 % (2982344)Termination reason: Instruction limit
% 0.50/0.44 % (2982344)Termination phase: Property scanning
% 0.50/0.44 % (2982344)Time elapsed: 0.035 s
% 0.50/0.44 % (2982344)Peak memory usage: 12 MB
% 0.50/0.44 % (2982344)Instructions burned: 76 (million)
% 0.50/0.44 % (2982360)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=3749456965:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 0.50/0.44 % (2982339)Instruction limit reached!
% 0.50/0.44 % (2982339)------------------------------
% 0.50/0.44 % (2982339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.44 % (2982339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.44 % (2982339)CaDiCaL version: 2.1.3
% 0.50/0.44 % (2982339)Termination reason: Instruction limit
% 0.50/0.44 % (2982339)Termination phase: Saturation
% 0.50/0.44 % (2982339)Time elapsed: 0.042 s
% 0.50/0.44 % (2982339)Peak memory usage: 13 MB
% 0.50/0.44 % (2982339)Instructions burned: 89 (million)
% 0.50/0.44 % (2982360)Instruction limit reached!
% 0.50/0.44 % (2982360)------------------------------
% 0.50/0.44 % (2982360)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.44 % (2982360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.44 % (2982360)CaDiCaL version: 2.1.3
% 0.50/0.44 % (2982360)Termination reason: Instruction limit
% 0.50/0.44 % (2982360)Termination phase: shuffling
% 0.50/0.44 % (2982360)Time elapsed: 0.006 s
% 0.50/0.44 % (2982360)Peak memory usage: 10 MB
% 0.50/0.44 % (2982360)Instructions burned: 28 (million)
% 0.50/0.44 % (2982357)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=3657877757:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.50/0.44 % (2982357)Instruction limit reached!
% 0.50/0.44 % (2982357)------------------------------
% 0.50/0.44 % (2982357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.44 % (2982357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.44 % (2982357)CaDiCaL version: 2.1.3
% 0.50/0.44 % (2982357)Termination reason: Instruction limit
% 0.50/0.44 % (2982357)Termination phase: shuffling
% 0.50/0.44 % (2982357)Time elapsed: 0.006 s
% 0.50/0.44 % (2982357)Peak memory usage: 10 MB
% 0.50/0.44 % (2982357)Instructions burned: 13 (million)
% 0.50/0.44 % (2982361)lrs+1002_64_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:sp=occurrence:lma=off:plsqr=32,1:uwa=interpreted_only:random_seed=641821084:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.50/0.44 % (2982366)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=732077233:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.50/0.44 % (2982362)lrs+10_1_si=on:cs=on:random_seed=458794333:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.50/0.44 % (2982364)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 0.50/0.44 % (2982362)Instruction limit reached!
% 0.50/0.44 % (2982362)------------------------------
% 0.50/0.44 % (2982362)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.44 % (2982362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.44 % (2982362)CaDiCaL version: 2.1.3
% 0.50/0.44 % (2982362)Termination reason: Instruction limit
% 0.50/0.44 % (2982362)Termination phase: shuffling
% 0.50/0.44 % (2982362)Time elapsed: 0.005 s
% 0.50/0.44 % (2982362)Peak memory usage: 10 MB
% 0.50/0.44 % (2982362)Instructions burned: 10 (million)
% 0.50/0.44 % (2982364)ott+1002_20_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:plsqr=1,32:bce=on:uwa=interpreted_only:foolp=on:random_seed=2679532820:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.50/0.44 % (2982366)Instruction limit reached!
% 0.50/0.44 % (2982366)------------------------------
% 0.50/0.44 % (2982366)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.44 % (2982366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.44 % (2982366)CaDiCaL version: 2.1.3
% 0.50/0.44 % (2982366)Termination reason: Instruction limit
% 0.50/0.44 % (2982366)Termination phase: Property scanning
% 0.50/0.44 % (2982366)Time elapsed: 0.010 s
% 0.50/0.44 % (2982366)Peak memory usage: 11 MB
% 0.50/0.44 % (2982366)Instructions burned: 42 (million)
% 0.50/0.44 % (2982364)Instruction limit reached!
% 0.50/0.44 % (2982364)------------------------------
% 0.50/0.44 % (2982364)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.44 % (2982364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.44 % (2982364)CaDiCaL version: 2.1.3
% 0.50/0.44 % (2982364)Termination reason: Instruction limit
% 0.50/0.44 % (2982364)Termination phase: shuffling
% 0.50/0.44 % (2982364)Time elapsed: 0.003 s
% 0.50/0.44 % (2982364)Peak memory usage: 10 MB
% 0.50/0.44 % (2982364)Instructions burned: 7 (million)
% 0.50/0.44 % (2982367)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=3289083041:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 0.50/0.44 % (2982373)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=2911431227:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 0.50/0.44 % (2982371)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=1597317829:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 0.50/0.44 % (2982373)Instruction limit reached!
% 0.50/0.44 % (2982373)------------------------------
% 0.50/0.44 % (2982373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.44 % (2982373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.44 % (2982373)CaDiCaL version: 2.1.3
% 0.50/0.44 % (2982373)Termination reason: Instruction limit
% 0.50/0.44 % (2982373)Termination phase: Property scanning
% 0.50/0.44 % (2982373)Time elapsed: 0.004 s
% 0.50/0.44 % (2982373)Peak memory usage: 10 MB
% 0.50/0.44 % (2982373)Instructions burned: 17 (million)
% 0.50/0.44 % (2982345)Instruction limit reached!
% 0.50/0.44 % (2982345)------------------------------
% 0.50/0.44 % (2982345)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.44 % (2982345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.44 % (2982345)CaDiCaL version: 2.1.3
% 0.50/0.44 % (2982345)Termination reason: Instruction limit
% 0.50/0.44 % (2982345)Termination phase: Saturation
% 0.50/0.44 % (2982345)Time elapsed: 0.079 s
% 0.50/0.44 % (2982345)Peak memory usage: 14 MB
% 0.50/0.44 % (2982345)Instructions burned: 158 (million)
% 0.50/0.44 % (2982374)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=3954188746:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 0.50/0.44 % (2982361)Instruction limit reached!
% 0.50/0.44 % (2982361)------------------------------
% 0.50/0.44 % (2982361)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.44 % (2982361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.44 % (2982361)CaDiCaL version: 2.1.3
% 0.50/0.44 % (2982361)Termination reason: Instruction limit
% 0.50/0.44 % (2982361)Termination phase: Property scanning
% 0.50/0.44 % (2982361)Time elapsed: 0.036 s
% 0.50/0.44 % (2982361)Peak memory usage: 11 MB
% 0.50/0.44 % (2982361)Instructions burned: 86 (million)
% 0.50/0.44 % (2982378)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=875873217:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 0.50/0.44 % (2982371)Instruction limit reached!
% 0.50/0.44 % (2982371)------------------------------
% 0.50/0.44 % (2982371)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.44 % (2982371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.44 % (2982371)CaDiCaL version: 2.1.3
% 0.50/0.44 % (2982371)Termination reason: Instruction limit
% 0.50/0.44 % (2982371)Termination phase: SInE selection
% 0.50/0.44 % (2982371)Time elapsed: 0.012 s
% 0.50/0.44 % (2982371)Peak memory usage: 11 MB
% 0.50/0.44 % (2982371)Instructions burned: 25 (million)
% 0.50/0.44 % (2982378)Instruction limit reached!
% 0.50/0.44 % (2982378)------------------------------
% 0.50/0.44 % (2982378)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.44 % (2982378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.44 % (2982378)CaDiCaL version: 2.1.3
% 0.50/0.44 % (2982378)Termination reason: Instruction limit
% 0.50/0.44 % (2982378)Termination phase: Property scanning
% 0.50/0.44 % (2982378)Time elapsed: 0.004 s
% 0.50/0.44 % (2982378)Peak memory usage: 10 MB
% 0.50/0.44 % (2982378)Instructions burned: 18 (million)
% 0.50/0.44 % (2982379)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=3019198335:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2998 on theBenchmark for (2998ds/2Mi)
% 0.50/0.44 % (2982342) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2982334-2982342"...
% 0.50/0.44 % (2982367)Refutation not found, incomplete strategy
% 0.50/0.44 % (2982367)------------------------------
% 0.50/0.44 % (2982367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.44 % (2982367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.44 % (2982367)CaDiCaL version: 2.1.3
% 0.50/0.44 % (2982367)Termination reason: Refutation not found, incomplete strategy
% 0.50/0.44 % (2982367)Time elapsed: 0.030 s
% 0.50/0.44 % (2982367)Peak memory usage: 13 MB
% 0.50/0.44 % (2982367)Instructions burned: 61 (million)
% 0.50/0.44 % (2982379)Instruction limit reached!
% 0.50/0.44 % (2982379)------------------------------
% 0.50/0.44 % (2982379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.44 % (2982379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.44 % (2982379)CaDiCaL version: 2.1.3
% 0.50/0.44 % (2982379)Termination reason: Instruction limit
% 0.50/0.44 % (2982379)Termination phase: shuffling
% 0.50/0.44 % (2982379)Time elapsed: 0.003 s
% 0.50/0.44 % (2982379)Peak memory usage: 10 MB
% 0.50/0.44 % (2982379)Instructions burned: 5 (million)
% 0.50/0.44 % (2982384)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=4169621762:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 0.50/0.44 % (2982367)------------------------------
% 0.50/0.44 % (2982367)------------------------------
% 0.50/0.44 % (2982382)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=2651099417:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 0.50/0.44 % (2982342)...printing done.
% 0.50/0.44 % (2982342)Refutation found. Thanks to Tanya!
% 0.50/0.44 % SZS status Theorem for theBenchmark
% 0.50/0.44 % SZS output start Proof for theBenchmark
% 0.50/0.44 thf(type_def_5, type, extended_ereal: $tType).
% 0.50/0.44 thf(type_def_6, type, real: $tType).
% 0.50/0.44 thf(type_def_7, type, set: $tType > $tType).
% 0.50/0.44 thf(type_def_8, type, a: $tType).
% 0.50/0.44 thf(type_def_9, type, sTfun: ($tType * $tType) > $tType).
% 0.50/0.44 thf(func_def_0, type, real_V2090557954_space: !>[X0: $tType]:($o)).
% 0.50/0.44 thf(func_def_1, type, type: !>[X0: $tType]:($o)).
% 0.50/0.44 thf(func_def_2, type, idom: !>[X0: $tType]:($o)).
% 0.50/0.44 thf(func_def_3, type, ring: !>[X0: $tType]:($o)).
% 0.50/0.44 thf(func_def_4, type, zero: !>[X0: $tType]:($o)).
% 0.50/0.44 thf(func_def_5, type, field: !>[X0: $tType]:($o)).
% 0.50/0.44 thf(func_def_6, type, uminus: !>[X0: $tType]:($o)).
% 0.50/0.44 thf(func_def_7, type, ord: !>[X0: $tType]:($o)).
% 0.50/0.44 thf(func_def_8, type, order: !>[X0: $tType]:($o)).
% 0.50/0.44 thf(func_def_9, type, mult_zero: !>[X0: $tType]:($o)).
% 0.50/0.44 thf(func_def_10, type, group_add: !>[X0: $tType]:($o)).
% 0.50/0.44 thf(func_def_11, type, no_bot: !>[X0: $tType]:($o)).
% 0.50/0.44 thf(func_def_12, type, no_top: !>[X0: $tType]:($o)).
% 0.50/0.44 thf(func_def_13, type, linorder: !>[X0: $tType]:($o)).
% 0.50/0.44 thf(func_def_14, type, preorder: !>[X0: $tType]:($o)).
% 0.50/0.44 thf(func_def_15, type, wellorder: !>[X0: $tType]:($o)).
% 0.50/0.44 thf(func_def_16, type, division_ring: !>[X0: $tType]:($o)).
% 0.50/0.44 thf(func_def_17, type, semidom_divide: !>[X0: $tType]:($o)).
% 0.50/0.44 thf(func_def_18, type, semigroup_mult: !>[X0: $tType]:($o)).
% 0.50/0.44 thf(func_def_19, type, dense_order: !>[X0: $tType]:($o)).
% 0.50/0.44 thf(func_def_20, type, linordered_idom: !>[X0: $tType]:($o)).
% 0.50/0.44 thf(func_def_21, type, linordered_ring: !>[X0: $tType]:($o)).
% 0.50/0.44 thf(func_def_22, type, linordered_field: !>[X0: $tType]:($o)).
% 0.50/0.44 thf(func_def_23, type, ab_semigroup_mult: !>[X0: $tType]:($o)).
% 0.50/0.44 thf(func_def_24, type, boolean_algebra: !>[X0: $tType]:($o)).
% 0.50/0.44 thf(func_def_25, type, ordered_ab_group_add: !>[X0: $tType]:($o)).
% 0.50/0.44 thf(func_def_26, type, topological_t0_space: !>[X0: $tType]:($o)).
% 0.50/0.44 thf(func_def_27, type, topological_t1_space: !>[X0: $tType]:($o)).
% 0.50/0.44 thf(func_def_28, type, linord581940658strict: !>[X0: $tType]:($o)).
% 0.50/0.44 thf(func_def_29, type, linord219039673up_add: !>[X0: $tType]:($o)).
% 0.50/0.44 thf(func_def_30, type, semiri1193490041visors: !>[X0: $tType]:($o)).
% 0.50/0.44 thf(func_def_31, type, linord20386208strict: !>[X0: $tType]:($o)).
% 0.50/0.44 thf(func_def_32, type, linord1659791738miring: !>[X0: $tType]:($o)).
% 0.50/0.44 thf(func_def_33, type, topolo2133971006pology: !>[X0: $tType]:($o)).
% 0.50/0.44 thf(func_def_34, type, topolo503727757_space: !>[X0: $tType]:($o)).
% 0.50/0.44 thf(func_def_35, type, canoni770627133id_add: !>[X0: $tType]:($o)).
% 0.50/0.44 thf(func_def_36, type, linord893533164strict: !>[X0: $tType]:($o)).
% 0.50/0.44 thf(func_def_37, type, semiri1923998003cancel: !>[X0: $tType]:($o)).
% 0.50/0.44 thf(func_def_38, type, euclid24285859cancel: !>[X0: $tType]:($o)).
% 0.50/0.44 thf(func_def_39, type, euclid191655569cancel: !>[X0: $tType]:($o)).
% 0.50/0.44 thf(func_def_40, type, condit1656338222tinuum: !>[X0: $tType]:($o)).
% 0.50/0.44 thf(func_def_41, type, extend1396239628finity: !>[X0: $tType]:(X0)).
% 0.50/0.44 thf(func_def_42, type, extended_MInfty: extended_ereal).
% 0.50/0.44 thf(func_def_43, type, extended_PInfty: extended_ereal).
% 0.50/0.44 thf(func_def_44, type, extended_rec_ereal: !>[X0: $tType]:(((real > X0) > X0 > X0 > extended_ereal > X0))).
% 0.50/0.44 thf(func_def_45, type, times_times: !>[X0: $tType]:((X0 > X0 > X0))).
% 0.50/0.44 thf(func_def_46, type, uminus_uminus: !>[X0: $tType]:((X0 > X0))).
% 0.50/0.44 thf(func_def_47, type, zero_zero: !>[X0: $tType]:(X0)).
% 0.50/0.44 thf(func_def_48, type, lower_582600101lsc_at: !>[X0: $tType, X1: $tType]:((X0 > (X0 > X1) > $o))).
% 0.50/0.44 thf(func_def_49, type, ord_less: !>[X0: $tType]:((X0 > X0 > $o))).
% 0.50/0.44 thf(func_def_50, type, divide_divide: !>[X0: $tType]:((X0 > X0 > X0))).
% 0.50/0.44 thf(func_def_51, type, collect: !>[X0: $tType]:(((X0 > $o) > set @ X0))).
% 0.50/0.44 thf(func_def_52, type, topolo1751647064n_open: !>[X0: $tType]:((set @ X0 > $o))).
% 0.50/0.44 thf(func_def_53, type, member: !>[X0: $tType]:((X0 > set @ X0 > $o))).
% 0.50/0.44 thf(func_def_54, type, f: (a > extended_ereal)).
% 0.50/0.44 thf(func_def_55, type, x0: a).
% 0.50/0.44 thf(func_def_59, type, db1: !>[X0: $tType]:(X0)).
% 0.50/0.44 thf(func_def_60, type, db0: !>[X0: $tType]:(X0)).
% 0.50/0.44 thf(func_def_61, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 0.50/0.44 thf(func_def_62, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 0.50/0.44 thf(func_def_63, type, vAND: ($o > $o > $o)).
% 0.50/0.44 thf(func_def_64, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 0.50/0.44 thf(func_def_65, type, vIMP: ($o > $o > $o)).
% 0.50/0.44 thf(func_def_66, type, vNOT: ($o > $o)).
% 0.50/0.44 thf(func_def_67, type, db2: !>[X0: $tType]:(X0)).
% 0.50/0.44 thf(func_def_68, type, sP0: (extended_ereal > extended_ereal > $o)).
% 0.50/0.44 thf(func_def_69, type, sP1: (extended_ereal > extended_ereal > $o)).
% 0.50/0.44 thf(func_def_70, type, sK2: !>[X0: $tType]:((X0 > X0))).
% 0.50/0.44 thf(func_def_71, type, sK3: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0))).
% 0.50/0.44 thf(func_def_72, type, sK4: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 0.50/0.44 thf(func_def_73, type, sK5: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 0.50/0.44 thf(func_def_74, type, sK6: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 0.50/0.44 thf(func_def_75, type, sK7: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 0.50/0.44 thf(func_def_76, type, sK8: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 0.50/0.44 thf(func_def_77, type, sK9: !>[X0: $tType, X1: $tType]:(((X0 > X1) > (X0 > X1) > X0))).
% 0.50/0.44 thf(func_def_78, type, sK10: extended_ereal).
% 0.50/0.44 thf(func_def_79, type, sK11: (set @ a > a)).
% 0.50/0.44 thf(func_def_80, type, sK12: (extended_ereal > set @ a)).
% 0.50/0.44 thf(func_def_81, type, sK13: !>[X0: $tType]:((X0 > X0 > set @ X0))).
% 0.50/0.44 thf(func_def_82, type, sK14: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 0.50/0.44 thf(func_def_83, type, sK15: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 0.50/0.44 thf(func_def_84, type, sK16: !>[X0: $tType]:((X0 > X0))).
% 0.50/0.44 thf(func_def_85, type, sK17: !>[X0: $tType]:((X0 > X0 > set @ X0))).
% 0.50/0.44 thf(func_def_86, type, sK18: !>[X0: $tType]:((X0 > X0))).
% 0.50/0.44 thf(func_def_87, type, sK19: !>[X0: $tType]:((X0 > X0))).
% 0.50/0.44 thf(func_def_88, type, sK20: !>[X0: $tType]:((X0 > X0))).
% 0.50/0.44 thf(func_def_89, type, sK21: (extended_ereal > set @ a)).
% 0.50/0.44 thf(func_def_90, type, sK22: extended_ereal).
% 0.50/0.44 thf(func_def_91, type, sK23: (set @ a > a)).
% 0.50/0.44 thf(func_def_92, type, sK24: !>[X0: $tType]:((X0 > X0 > set @ X0))).
% 0.50/0.44 thf(func_def_93, type, sK25: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 0.50/0.44 thf(func_def_94, type, sK26: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 0.50/0.44 thf(func_def_95, type, sK27: !>[X0: $tType]:((X0 > (X0 > $o) > (X0 > $o) > X0))).
% 0.50/0.44 thf(func_def_96, type, sK28: !>[X0: $tType]:((X0 > (X0 > $o) > (X0 > $o) > X0))).
% 0.50/0.44 thf(func_def_97, type, sK29: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > (X0 > $o) > (X0 > $o) > X0))).
% 0.50/0.44 thf(func_def_98, type, sK30: !>[X0: $tType, X1: $tType]:((X1 > X0))).
% 0.50/0.44 thf(func_def_99, type, sK31: !>[X0: $tType]:((X0 > (X0 > $o) > (X0 > $o) > X0))).
% 0.50/0.44 thf(func_def_100, type, sK32: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > (X0 > $o) > (X0 > $o) > X0))).
% 0.50/0.44 thf(func_def_101, type, sK33: !>[X0: $tType]:((X0 > (X0 > $o) > (X0 > $o) > X0))).
% 0.50/0.44 thf(func_def_102, type, sK34: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 0.50/0.44 thf(func_def_103, type, sK35: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 0.50/0.44 thf(func_def_104, type, sK36: !>[X0: $tType, X1: $tType]:((X0 > X1))).
% 0.50/0.44 thf(func_def_105, type, sK37: (extended_ereal > set @ a)).
% 0.50/0.44 thf(func_def_106, type, sK38: extended_ereal).
% 0.50/0.44 thf(func_def_107, type, sK39: (set @ a > a)).
% 0.50/0.44 thf(func_def_108, type, sK40: !>[X0: $tType]:((X0 > X0 > set @ X0))).
% 0.50/0.44 thf(func_def_109, type, sK41: !>[X0: $tType]:((X0 > X0))).
% 0.50/0.44 thf(func_def_110, type, sK42: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 0.50/0.44 thf(func_def_111, type, sK43: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 0.50/0.44 thf(func_def_112, type, sK44: !>[X0: $tType]:((X0 > (X0 > $o) > (X0 > $o) > X0))).
% 0.50/0.44 thf(func_def_113, type, sK45: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > (X0 > $o) > (X0 > $o) > X0))).
% 0.50/0.44 thf(func_def_114, type, sK46: !>[X0: $tType]:((X0 > (X0 > $o) > (X0 > $o) > X0))).
% 0.50/0.44 thf(func_def_115, type, sK47: !>[X0: $tType]:((X0 > X0))).
% 0.50/0.44 thf(func_def_116, type, sK48: !>[X0: $tType]:((X0 > X0 > X0))).
% 0.50/0.44 thf(func_def_117, type, sK49: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > (X0 > $o) > (X0 > $o) > X0))).
% 0.50/0.44 thf(func_def_118, type, sK50: !>[X0: $tType]:((X0 > (X0 > $o) > (X0 > $o) > X0))).
% 0.50/0.44 thf(func_def_119, type, sK51: !>[X0: $tType]:((X0 > (X0 > $o) > (X0 > $o) > X0))).
% 0.50/0.44 thf(func_def_120, type, sK52: !>[X0: $tType]:((X0 > X0))).
% 0.50/0.44 thf(func_def_121, type, sK53: !>[X0: $tType]:((X0 > X0))).
% 0.50/0.44 thf(func_def_122, type, sK54: !>[X0: $tType]:((X0 > X0 > X0))).
% 0.50/0.44 thf(func_def_123, type, sK55: !>[X0: $tType]:((X0 > X0))).
% 0.50/0.44 thf(func_def_124, type, sK56: !>[X0: $tType]:((X0 > X0))).
% 0.50/0.44 thf(func_def_125, type, sK57: !>[X0: $tType]:(((X0 > $o) > X0))).
% 0.50/0.44 thf(func_def_126, type, sK58: extended_ereal).
% 0.50/0.44 thf(func_def_127, type, sK59: (set @ a > a)).
% 0.50/0.44 thf(func_def_128, type, sK60: (extended_ereal > set @ a)).
% 0.50/0.44 thf(func_def_129, type, sK61: !>[X0: $tType]:((X0 > X0))).
% 0.50/0.44 thf(func_def_130, type, sK62: !>[X0: $tType]:((X0 > X0))).
% 0.50/0.44 thf(f1,axiom,(
% 0.50/0.44 (((f @ x0)) = extend1396239628finity @ extended_ereal) => (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = ! [X2 : extended_ereal] : ((ord_less @ extended_ereal @ X2 @ (f @ x0)) => ? [X3 : set @ a] : ((topolo1751647064n_open @ a @ X3) & ! [X4 : a] : ((member @ a @ X4 @ X3) => (ord_less @ extended_ereal @ X2 @ (f @ X4))) & (member @ a @ x0 @ X3))))),
% 0.50/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0__092_060open_062f_Ax0_A_061_A_092_060infinity_062_A_092_060Longrightarrow_062_Alsc__at_Ax0_Af_A_061_A_I_092_060forall_062C_060f_Ax0_O_A_092_060exists_062T_O_Aopen_AT_A_092_060and_062_Ax0_A_092_060in_062_AT_A_092_060and_062_A_I_092_060forall_062y_092_060in_062T_O_AC_A_060_Af_Ay_J_J_092_060close_062)).
% 0.50/0.44 thf(f2,axiom,(
% 0.50/0.44 (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) => (! [X0 : extended_ereal] : ((ord_less @ extended_ereal @ X0 @ (f @ x0)) => ? [X1 : set @ a] : (! [X2 : a] : ((member @ a @ X2 @ X1) => (ord_less @ extended_ereal @ X0 @ (f @ X2))) & (topolo1751647064n_open @ a @ X1) & (member @ a @ x0 @ X1))) = ((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)))),
% 0.50/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1__092_060open_062f_Ax0_A_061_A_N_A_092_060infinity_062_A_092_060Longrightarrow_062_Alsc__at_Ax0_Af_A_061_A_I_092_060forall_062C_060f_Ax0_O_A_092_060exists_062T_O_Aopen_AT_A_092_060and_062_Ax0_A_092_060in_062_AT_A_092_060and_062_A_I_092_060forall_062y_092_060in_062T_O_AC_A_060_Af_Ay_J_J_092_060close_062)).
% 0.50/0.44 thf(f3,axiom,(
% 0.50/0.44 (((f @ x0)) != ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) => ((((f @ x0)) != extend1396239628finity @ extended_ereal) => (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = ! [X0 : extended_ereal] : ((ord_less @ extended_ereal @ X0 @ (f @ x0)) => ? [X1 : set @ a] : ((member @ a @ x0 @ X1) & ! [X2 : a] : ((member @ a @ X2 @ X1) => (ord_less @ extended_ereal @ X0 @ (f @ X2))) & (topolo1751647064n_open @ a @ X1)))))),
% 0.50/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2__092_060open_062_092_060lbrakk_062f_Ax0_A_092_060noteq_062_A_N_A_092_060infinity_062_059_Af_Ax0_A_092_060noteq_062_A_092_060infinity_062_092_060rbrakk_062_A_092_060Longrightarrow_062_Alsc__at_Ax0_Af_A_061_A_I_092_060forall_062C_060f_Ax0_O_A_092_060exists_062T_O_Aopen_AT_A_092_060and_062_Ax0_A_092_060in_062_AT_A_092_060and_062_A_I_092_060forall_062y_092_060in_062T_O_AC_A_060_Af_Ay_J_J_092_060close_062)).
% 0.50/0.44 thf(f298,conjecture,(
% 0.50/0.44 (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) != ~ ! [X0 : extended_ereal] : ((ord_less @ extended_ereal @ X0 @ (f @ x0)) => ? [X1 : set @ a] : (! [X2 : a] : ((member @ a @ X2 @ X1) => (ord_less @ extended_ereal @ X0 @ (f @ X2))) & (member @ a @ x0 @ X1) & (topolo1751647064n_open @ a @ X1))))),
% 0.50/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0)).
% 0.50/0.44 thf(f299,negated_conjecture,(
% 0.50/0.44 ~ (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) != ~ ! [X0 : extended_ereal] : ((ord_less @ extended_ereal @ X0 @ (f @ x0)) => ? [X1 : set @ a] : (! [X2 : a] : ((member @ a @ X2 @ X1) => (ord_less @ extended_ereal @ X0 @ (f @ X2))) & (member @ a @ x0 @ X1) & (topolo1751647064n_open @ a @ X1))))),
% 0.50/0.44 inference(negated_conjecture,[status(cth)],[f298])).
% 0.50/0.44 thf(f332,plain,(
% 0.50/0.44 (((f @ x0)) = extend1396239628finity @ extended_ereal) => (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = ! [X0 : extended_ereal] : ((ord_less @ extended_ereal @ X0 @ (f @ x0)) => ? [X1 : set @ a] : ((topolo1751647064n_open @ a @ X1) & ! [X2 : a] : ((member @ a @ X2 @ X1) => (ord_less @ extended_ereal @ X0 @ (f @ X2))) & (member @ a @ x0 @ X1))))),
% 0.50/0.44 inference(rectify,[],[f1])).
% 0.50/0.44 thf(f333,plain,(
% 0.50/0.44 (((f @ x0)) = extend1396239628finity @ extended_ereal) => (! [X0 : extended_ereal] : ((((ord_less @ extended_ereal @ X0 @ (f @ x0))) = $true) => ? [X1 : set @ a] : ((((topolo1751647064n_open @ a @ X1)) = $true) & (((member @ a @ x0 @ X1)) = $true) & ! [X2 : a] : ((((member @ a @ X2 @ X1)) = $true) => (((ord_less @ extended_ereal @ X0 @ (f @ X2))) = $true)))) <=> (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true))),
% 0.50/0.44 inference(fool_elimination,[],[f332])).
% 0.50/0.44 thf(f352,plain,(
% 0.50/0.44 ~ (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) != ~ ! [X0 : extended_ereal] : ((ord_less @ extended_ereal @ X0 @ (f @ x0)) => ? [X1 : set @ a] : (! [X2 : a] : ((member @ a @ X2 @ X1) => (ord_less @ extended_ereal @ X0 @ (f @ X2))) & (member @ a @ x0 @ X1) & (topolo1751647064n_open @ a @ X1))))),
% 0.50/0.44 inference(rectify,[],[f299])).
% 0.50/0.44 thf(f353,plain,(
% 0.50/0.44 ~(~ ! [X0 : extended_ereal] : ((((ord_less @ extended_ereal @ X0 @ (f @ x0))) = $true) => ? [X1 : set @ a] : ((((member @ a @ x0 @ X1)) = $true) & ! [X2 : a] : ((((member @ a @ X2 @ X1)) = $true) => (((ord_less @ extended_ereal @ X0 @ (f @ X2))) = $true)) & (((topolo1751647064n_open @ a @ X1)) = $true))) <~> (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true))),
% 0.50/0.44 inference(fool_elimination,[],[f352])).
% 0.50/0.44 thf(f667,plain,(
% 0.50/0.44 (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) => (! [X0 : extended_ereal] : ((ord_less @ extended_ereal @ X0 @ (f @ x0)) => ? [X1 : set @ a] : (! [X2 : a] : ((member @ a @ X2 @ X1) => (ord_less @ extended_ereal @ X0 @ (f @ X2))) & (topolo1751647064n_open @ a @ X1) & (member @ a @ x0 @ X1))) = ((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)))),
% 0.50/0.44 inference(rectify,[],[f2])).
% 0.50/0.44 thf(f668,plain,(
% 0.50/0.44 (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) => (! [X0 : extended_ereal] : ((((ord_less @ extended_ereal @ X0 @ (f @ x0))) = $true) => ? [X1 : set @ a] : (! [X2 : a] : ((((member @ a @ X2 @ X1)) = $true) => (((ord_less @ extended_ereal @ X0 @ (f @ X2))) = $true)) & (((topolo1751647064n_open @ a @ X1)) = $true) & (((member @ a @ x0 @ X1)) = $true))) <=> (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true))),
% 0.50/0.44 inference(fool_elimination,[],[f667])).
% 0.50/0.44 thf(f786,plain,(
% 0.50/0.44 (((f @ x0)) != ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) => ((((f @ x0)) != extend1396239628finity @ extended_ereal) => (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = ! [X0 : extended_ereal] : ((ord_less @ extended_ereal @ X0 @ (f @ x0)) => ? [X1 : set @ a] : ((member @ a @ x0 @ X1) & ! [X2 : a] : ((member @ a @ X2 @ X1) => (ord_less @ extended_ereal @ X0 @ (f @ X2))) & (topolo1751647064n_open @ a @ X1)))))),
% 0.50/0.44 inference(rectify,[],[f3])).
% 0.50/0.44 thf(f787,plain,(
% 0.50/0.44 (((f @ x0)) != ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) => ((((f @ x0)) != extend1396239628finity @ extended_ereal) => (! [X0 : extended_ereal] : ((((ord_less @ extended_ereal @ X0 @ (f @ x0))) = $true) => ? [X1 : set @ a] : ((((topolo1751647064n_open @ a @ X1)) = $true) & (((member @ a @ x0 @ X1)) = $true) & ! [X2 : a] : ((((member @ a @ X2 @ X1)) = $true) => (((ord_less @ extended_ereal @ X0 @ (f @ X2))) = $true)))) <=> (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true)))),
% 0.50/0.44 inference(fool_elimination,[],[f786])).
% 0.50/0.44 thf(f871,plain,(
% 0.50/0.44 ((! [X0 : extended_ereal] : (? [X1 : set @ a] : (! [X2 : a] : ((((ord_less @ extended_ereal @ X0 @ (f @ X2))) = $true) | (((member @ a @ X2 @ X1)) != $true)) & (((topolo1751647064n_open @ a @ X1)) = $true) & (((member @ a @ x0 @ X1)) = $true)) | (((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true)) <=> (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true)) | (((f @ x0)) = extend1396239628finity @ extended_ereal)) | (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal)))),
% 0.50/0.44 inference(ennf_transformation,[],[f787])).
% 0.50/0.44 thf(f872,plain,(
% 0.50/0.44 (! [X0 : extended_ereal] : (? [X1 : set @ a] : (! [X2 : a] : ((((ord_less @ extended_ereal @ X0 @ (f @ X2))) = $true) | (((member @ a @ X2 @ X1)) != $true)) & (((topolo1751647064n_open @ a @ X1)) = $true) & (((member @ a @ x0 @ X1)) = $true)) | (((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true)) <=> (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true)) | (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | (((f @ x0)) = extend1396239628finity @ extended_ereal)),
% 0.50/0.44 inference(flattening,[],[f871])).
% 0.50/0.44 thf(f1125,plain,(
% 0.50/0.44 ? [X0 : extended_ereal] : ((((ord_less @ extended_ereal @ X0 @ (f @ x0))) = $true) & ! [X1 : set @ a] : ((((member @ a @ x0 @ X1)) != $true) | (((topolo1751647064n_open @ a @ X1)) != $true) | ? [X2 : a] : ((((member @ a @ X2 @ X1)) = $true) & (((ord_less @ extended_ereal @ X0 @ (f @ X2))) != $true)))) <=> (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true)),
% 0.50/0.44 inference(ennf_transformation,[],[f353])).
% 0.50/0.44 thf(f1127,plain,(
% 0.50/0.44 (! [X0 : extended_ereal] : (? [X1 : set @ a] : ((((member @ a @ x0 @ X1)) = $true) & ! [X2 : a] : ((((ord_less @ extended_ereal @ X0 @ (f @ X2))) = $true) | (((member @ a @ X2 @ X1)) != $true)) & (((topolo1751647064n_open @ a @ X1)) = $true)) | (((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true)) <=> (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true)) | (((f @ x0)) != ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal)))),
% 0.50/0.44 inference(ennf_transformation,[],[f668])).
% 0.50/0.44 thf(f1130,plain,(
% 0.50/0.44 ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) <=> ! [X0 : extended_ereal] : ((((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true) | ? [X1 : set @ a] : ((((member @ a @ x0 @ X1)) = $true) & (((topolo1751647064n_open @ a @ X1)) = $true) & ! [X2 : a] : ((((ord_less @ extended_ereal @ X0 @ (f @ X2))) = $true) | (((member @ a @ X2 @ X1)) != $true))))) | (((f @ x0)) != extend1396239628finity @ extended_ereal)),
% 0.50/0.44 inference(ennf_transformation,[],[f333])).
% 0.50/0.44 thf(f1182,plain,(
% 0.50/0.44 (? [X0 : extended_ereal] : ((((ord_less @ extended_ereal @ X0 @ (f @ x0))) = $true) & ! [X1 : set @ a] : ((((member @ a @ x0 @ X1)) != $true) | (((topolo1751647064n_open @ a @ X1)) != $true) | ? [X2 : a] : ((((member @ a @ X2 @ X1)) = $true) & (((ord_less @ extended_ereal @ X0 @ (f @ X2))) != $true)))) | (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) != $true)) & ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | ! [X0 : extended_ereal] : ((((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true) | ? [X1 : set @ a] : ((((member @ a @ x0 @ X1)) = $true) & (((topolo1751647064n_open @ a @ X1)) = $true) & ! [X2 : a] : ((((member @ a @ X2 @ X1)) != $true) | (((ord_less @ extended_ereal @ X0 @ (f @ X2))) = $true)))))),
% 0.50/0.44 inference(nnf_transformation,[],[f1125])).
% 0.50/0.44 thf(f1183,plain,(
% 0.50/0.44 (? [X0 : extended_ereal] : ((((ord_less @ extended_ereal @ X0 @ (f @ x0))) = $true) & ! [X1 : set @ a] : ((((member @ a @ x0 @ X1)) != $true) | (((topolo1751647064n_open @ a @ X1)) != $true) | ? [X2 : a] : ((((member @ a @ X2 @ X1)) = $true) & (((ord_less @ extended_ereal @ X0 @ (f @ X2))) != $true)))) | (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) != $true)) & ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | ! [X3 : extended_ereal] : (($true != ((ord_less @ extended_ereal @ X3 @ (f @ x0)))) | ? [X4 : set @ a] : ((((member @ a @ x0 @ X4)) = $true) & ($true = ((topolo1751647064n_open @ a @ X4))) & ! [X5 : a] : ((((member @ a @ X5 @ X4)) != $true) | (((ord_less @ extended_ereal @ X3 @ (f @ X5))) = $true)))))),
% 0.50/0.44 inference(rectify,[],[f1182])).
% 0.50/0.44 thf(f1184,plain,(
% 0.50/0.44 ((($true = ((ord_less @ extended_ereal @ sK10 @ (f @ x0)))) & ! [X1 : set @ a] : ((((member @ a @ x0 @ X1)) != $true) | (((topolo1751647064n_open @ a @ X1)) != $true) | ((((member @ a @ (sK11 @ X1) @ X1)) = $true) & (((ord_less @ extended_ereal @ sK10 @ (f @ (sK11 @ X1)))) != $true)))) | (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) != $true)) & ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | ! [X3 : extended_ereal] : (($true != ((ord_less @ extended_ereal @ X3 @ (f @ x0)))) | ((((member @ a @ x0 @ (sK12 @ X3))) = $true) & ($true = ((topolo1751647064n_open @ a @ (sK12 @ X3)))) & ! [X5 : a] : (($true != ((member @ a @ X5 @ (sK12 @ X3)))) | (((ord_less @ extended_ereal @ X3 @ (f @ X5))) = $true)))))),
% 0.50/0.44 inference(skolemize,[status(esa),new_symbols(skolem,[sK10,vAPP,vAPP]),skolemize(X0,sK10),skolemize(X2,sK2 @ X0 @ X1),skolemize(X2,sK2 @ X0 @ X1)],[f1183])).
% 0.50/0.44 thf(f1227,plain,(
% 0.50/0.44 ((! [X0 : extended_ereal] : (? [X1 : set @ a] : (! [X2 : a] : ((((ord_less @ extended_ereal @ X0 @ (f @ X2))) = $true) | (((member @ a @ X2 @ X1)) != $true)) & (((topolo1751647064n_open @ a @ X1)) = $true) & (((member @ a @ x0 @ X1)) = $true)) | (((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true)) | (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) != $true)) & ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | ? [X0 : extended_ereal] : (! [X1 : set @ a] : (? [X2 : a] : ((((ord_less @ extended_ereal @ X0 @ (f @ X2))) != $true) & (((member @ a @ X2 @ X1)) = $true)) | (((topolo1751647064n_open @ a @ X1)) != $true) | (((member @ a @ x0 @ X1)) != $true)) & (((ord_less @ extended_ereal @ X0 @ (f @ x0))) = $true)))) | (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | (((f @ x0)) = extend1396239628finity @ extended_ereal)),
% 0.50/0.44 inference(nnf_transformation,[],[f872])).
% 0.50/0.44 thf(f1228,plain,(
% 0.50/0.44 ((! [X0 : extended_ereal] : (? [X1 : set @ a] : (! [X2 : a] : ((((ord_less @ extended_ereal @ X0 @ (f @ X2))) = $true) | (((member @ a @ X2 @ X1)) != $true)) & (((topolo1751647064n_open @ a @ X1)) = $true) & (((member @ a @ x0 @ X1)) = $true)) | (((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true)) | (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) != $true)) & ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | ? [X3 : extended_ereal] : (! [X4 : set @ a] : (? [X5 : a] : ((((ord_less @ extended_ereal @ X3 @ (f @ X5))) != $true) & (((member @ a @ X5 @ X4)) = $true)) | ($true != ((topolo1751647064n_open @ a @ X4))) | (((member @ a @ x0 @ X4)) != $true)) & ($true = ((ord_less @ extended_ereal @ X3 @ (f @ x0))))))) | (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | (((f @ x0)) = extend1396239628finity @ extended_ereal)),
% 0.50/0.44 inference(rectify,[],[f1227])).
% 0.50/0.44 thf(f1229,plain,(
% 0.50/0.44 ((! [X0 : extended_ereal] : ((! [X2 : a] : ((((ord_less @ extended_ereal @ X0 @ (f @ X2))) = $true) | ($true != ((member @ a @ X2 @ (sK21 @ X0))))) & ($true = ((topolo1751647064n_open @ a @ (sK21 @ X0)))) & ($true = ((member @ a @ x0 @ (sK21 @ X0))))) | (((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true)) | (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) != $true)) & ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (! [X4 : set @ a] : (((((ord_less @ extended_ereal @ sK22 @ (f @ (sK23 @ X4)))) != $true) & ($true = ((member @ a @ (sK23 @ X4) @ X4)))) | ($true != ((topolo1751647064n_open @ a @ X4))) | (((member @ a @ x0 @ X4)) != $true)) & ($true = ((ord_less @ extended_ereal @ sK22 @ (f @ x0))))))) | (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | (((f @ x0)) = extend1396239628finity @ extended_ereal)),
% 0.50/0.44 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP,sK22,vAPP]),skolemize(X2,sK2 @ X0 @ X1),skolemize(X3,sK22),skolemize(X2,sK2 @ X0 @ X1)],[f1228])).
% 0.50/0.44 thf(f1281,plain,(
% 0.50/0.44 ((! [X0 : extended_ereal] : (? [X1 : set @ a] : ((((member @ a @ x0 @ X1)) = $true) & ! [X2 : a] : ((((ord_less @ extended_ereal @ X0 @ (f @ X2))) = $true) | (((member @ a @ X2 @ X1)) != $true)) & (((topolo1751647064n_open @ a @ X1)) = $true)) | (((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true)) | (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) != $true)) & ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | ? [X0 : extended_ereal] : (! [X1 : set @ a] : ((((member @ a @ x0 @ X1)) != $true) | ? [X2 : a] : ((((ord_less @ extended_ereal @ X0 @ (f @ X2))) != $true) & (((member @ a @ X2 @ X1)) = $true)) | (((topolo1751647064n_open @ a @ X1)) != $true)) & (((ord_less @ extended_ereal @ X0 @ (f @ x0))) = $true)))) | (((f @ x0)) != ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal)))),
% 0.50/0.44 inference(nnf_transformation,[],[f1127])).
% 0.50/0.44 thf(f1282,plain,(
% 0.50/0.44 ((! [X0 : extended_ereal] : (? [X1 : set @ a] : ((((member @ a @ x0 @ X1)) = $true) & ! [X2 : a] : ((((ord_less @ extended_ereal @ X0 @ (f @ X2))) = $true) | (((member @ a @ X2 @ X1)) != $true)) & (((topolo1751647064n_open @ a @ X1)) = $true)) | (((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true)) | (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) != $true)) & ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | ? [X3 : extended_ereal] : (! [X4 : set @ a] : ((((member @ a @ x0 @ X4)) != $true) | ? [X5 : a] : ((((ord_less @ extended_ereal @ X3 @ (f @ X5))) != $true) & (((member @ a @ X5 @ X4)) = $true)) | ($true != ((topolo1751647064n_open @ a @ X4)))) & ($true = ((ord_less @ extended_ereal @ X3 @ (f @ x0))))))) | (((f @ x0)) != ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal)))),
% 0.50/0.44 inference(rectify,[],[f1281])).
% 0.50/0.44 thf(f1283,plain,(
% 0.50/0.44 ((! [X0 : extended_ereal] : (((((member @ a @ x0 @ (sK37 @ X0))) = $true) & ! [X2 : a] : ((((ord_less @ extended_ereal @ X0 @ (f @ X2))) = $true) | (((member @ a @ X2 @ (sK37 @ X0))) != $true)) & (((topolo1751647064n_open @ a @ (sK37 @ X0))) = $true)) | (((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true)) | (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) != $true)) & ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (! [X4 : set @ a] : ((((member @ a @ x0 @ X4)) != $true) | ((((ord_less @ extended_ereal @ sK38 @ (f @ (sK39 @ X4)))) != $true) & (((member @ a @ (sK39 @ X4) @ X4)) = $true)) | ($true != ((topolo1751647064n_open @ a @ X4)))) & (((ord_less @ extended_ereal @ sK38 @ (f @ x0))) = $true)))) | (((f @ x0)) != ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal)))),
% 0.50/0.44 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP,sK38,vAPP]),skolemize(X2,sK2 @ X0 @ X1),skolemize(X3,sK38),skolemize(X2,sK2 @ X0 @ X1)],[f1282])).
% 0.50/0.44 thf(f1361,plain,(
% 0.50/0.44 (((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | ? [X0 : extended_ereal] : ((((ord_less @ extended_ereal @ X0 @ (f @ x0))) = $true) & ! [X1 : set @ a] : ((((member @ a @ x0 @ X1)) != $true) | (((topolo1751647064n_open @ a @ X1)) != $true) | ? [X2 : a] : ((((ord_less @ extended_ereal @ X0 @ (f @ X2))) != $true) & (((member @ a @ X2 @ X1)) = $true))))) & (! [X0 : extended_ereal] : ((((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true) | ? [X1 : set @ a] : ((((member @ a @ x0 @ X1)) = $true) & (((topolo1751647064n_open @ a @ X1)) = $true) & ! [X2 : a] : ((((ord_less @ extended_ereal @ X0 @ (f @ X2))) = $true) | (((member @ a @ X2 @ X1)) != $true)))) | (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) != $true))) | (((f @ x0)) != extend1396239628finity @ extended_ereal)),
% 0.50/0.44 inference(nnf_transformation,[],[f1130])).
% 0.50/0.44 thf(f1362,plain,(
% 0.50/0.44 (((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | ? [X0 : extended_ereal] : ((((ord_less @ extended_ereal @ X0 @ (f @ x0))) = $true) & ! [X1 : set @ a] : ((((member @ a @ x0 @ X1)) != $true) | (((topolo1751647064n_open @ a @ X1)) != $true) | ? [X2 : a] : ((((ord_less @ extended_ereal @ X0 @ (f @ X2))) != $true) & (((member @ a @ X2 @ X1)) = $true))))) & (! [X3 : extended_ereal] : (($true != ((ord_less @ extended_ereal @ X3 @ (f @ x0)))) | ? [X4 : set @ a] : ((((member @ a @ x0 @ X4)) = $true) & ($true = ((topolo1751647064n_open @ a @ X4))) & ! [X5 : a] : ((((ord_less @ extended_ereal @ X3 @ (f @ X5))) = $true) | (((member @ a @ X5 @ X4)) != $true)))) | (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) != $true))) | (((f @ x0)) != extend1396239628finity @ extended_ereal)),
% 0.50/0.44 inference(rectify,[],[f1361])).
% 0.50/0.44 thf(f1363,plain,(
% 0.50/0.44 (((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (($true = ((ord_less @ extended_ereal @ sK58 @ (f @ x0)))) & ! [X1 : set @ a] : ((((member @ a @ x0 @ X1)) != $true) | (((topolo1751647064n_open @ a @ X1)) != $true) | ((((ord_less @ extended_ereal @ sK58 @ (f @ (sK59 @ X1)))) != $true) & ($true = ((member @ a @ (sK59 @ X1) @ X1))))))) & (! [X3 : extended_ereal] : (($true != ((ord_less @ extended_ereal @ X3 @ (f @ x0)))) | (($true = ((member @ a @ x0 @ (sK60 @ X3)))) & ($true = ((topolo1751647064n_open @ a @ (sK60 @ X3)))) & ! [X5 : a] : ((((ord_less @ extended_ereal @ X3 @ (f @ X5))) = $true) | (((member @ a @ X5 @ (sK60 @ X3))) != $true)))) | (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) != $true))) | (((f @ x0)) != extend1396239628finity @ extended_ereal)),
% 0.50/0.44 inference(skolemize,[status(esa),new_symbols(skolem,[sK58,vAPP,vAPP]),skolemize(X0,sK58),skolemize(X2,sK2 @ X0 @ X1),skolemize(X2,sK2 @ X0 @ X1)],[f1362])).
% 0.50/0.44 thf(f1489,plain,(
% 0.50/0.44 ( ! [X3 : extended_ereal,X5 : a] : (($true != ((ord_less @ extended_ereal @ X3 @ (f @ x0)))) | ($true != ((member @ a @ X5 @ (sK12 @ X3)))) | (((ord_less @ extended_ereal @ X3 @ (f @ X5))) = $true) | (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true)) )),
% 0.50/0.44 inference(cnf_transformation,[],[f1184])).
% 0.50/0.44 thf(f1490,plain,(
% 0.50/0.44 ( ! [X3 : extended_ereal] : (($true = ((topolo1751647064n_open @ a @ (sK12 @ X3)))) | (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | ($true != ((ord_less @ extended_ereal @ X3 @ (f @ x0))))) )),
% 0.50/0.44 inference(cnf_transformation,[],[f1184])).
% 0.50/0.44 thf(f1491,plain,(
% 0.50/0.44 ( ! [X3 : extended_ereal] : ((((member @ a @ x0 @ (sK12 @ X3))) = $true) | (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | ($true != ((ord_less @ extended_ereal @ X3 @ (f @ x0))))) )),
% 0.50/0.44 inference(cnf_transformation,[],[f1184])).
% 0.50/0.44 thf(f1492,plain,(
% 0.50/0.44 ( ! [X1 : set @ a] : ((((member @ a @ x0 @ X1)) != $true) | (((ord_less @ extended_ereal @ sK10 @ (f @ (sK11 @ X1)))) != $true) | (((topolo1751647064n_open @ a @ X1)) != $true) | (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) != $true)) )),
% 0.50/0.44 inference(cnf_transformation,[],[f1184])).
% 0.50/0.44 thf(f1493,plain,(
% 0.50/0.44 ( ! [X1 : set @ a] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) != $true) | (((member @ a @ (sK11 @ X1) @ X1)) = $true) | (((topolo1751647064n_open @ a @ X1)) != $true) | (((member @ a @ x0 @ X1)) != $true)) )),
% 0.50/0.44 inference(cnf_transformation,[],[f1184])).
% 0.50/0.44 thf(f1494,plain,(
% 0.50/0.44 ($true = ((ord_less @ extended_ereal @ sK10 @ (f @ x0)))) | (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) != $true)),
% 0.50/0.44 inference(cnf_transformation,[],[f1184])).
% 0.50/0.44 thf(f1589,plain,(
% 0.50/0.44 ($true = ((ord_less @ extended_ereal @ sK22 @ (f @ x0)))) | (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (((f @ x0)) = extend1396239628finity @ extended_ereal)),
% 0.50/0.44 inference(cnf_transformation,[],[f1229])).
% 0.50/0.44 thf(f1590,plain,(
% 0.50/0.44 ( ! [X4 : set @ a] : ((((f @ x0)) = extend1396239628finity @ extended_ereal) | ($true != ((topolo1751647064n_open @ a @ X4))) | (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | (((member @ a @ x0 @ X4)) != $true) | ($true = ((member @ a @ (sK23 @ X4) @ X4)))) )),
% 0.50/0.44 inference(cnf_transformation,[],[f1229])).
% 0.50/0.44 thf(f1591,plain,(
% 0.50/0.44 ( ! [X4 : set @ a] : ((((member @ a @ x0 @ X4)) != $true) | (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | (((f @ x0)) = extend1396239628finity @ extended_ereal) | (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (((ord_less @ extended_ereal @ sK22 @ (f @ (sK23 @ X4)))) != $true) | ($true != ((topolo1751647064n_open @ a @ X4)))) )),
% 0.50/0.44 inference(cnf_transformation,[],[f1229])).
% 0.50/0.44 thf(f1592,plain,(
% 0.50/0.44 ( ! [X0 : extended_ereal] : ((((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | (((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true) | ($true = ((member @ a @ x0 @ (sK21 @ X0)))) | (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) != $true) | (((f @ x0)) = extend1396239628finity @ extended_ereal)) )),
% 0.50/0.44 inference(cnf_transformation,[],[f1229])).
% 0.50/0.44 thf(f1593,plain,(
% 0.50/0.44 ( ! [X0 : extended_ereal] : ((((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true) | (((f @ x0)) = extend1396239628finity @ extended_ereal) | (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) != $true) | ($true = ((topolo1751647064n_open @ a @ (sK21 @ X0))))) )),
% 0.50/0.44 inference(cnf_transformation,[],[f1229])).
% 0.50/0.44 thf(f1594,plain,(
% 0.50/0.44 ( ! [X2 : a,X0 : extended_ereal] : ((((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true) | (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) != $true) | (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | ($true != ((member @ a @ X2 @ (sK21 @ X0)))) | (((ord_less @ extended_ereal @ X0 @ (f @ X2))) = $true) | (((f @ x0)) = extend1396239628finity @ extended_ereal)) )),
% 0.50/0.44 inference(cnf_transformation,[],[f1229])).
% 0.50/0.44 thf(f1711,plain,(
% 0.50/0.44 (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (((f @ x0)) != ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | (((ord_less @ extended_ereal @ sK38 @ (f @ x0))) = $true)),
% 0.50/0.44 inference(cnf_transformation,[],[f1283])).
% 0.50/0.44 thf(f1712,plain,(
% 0.50/0.44 ( ! [X4 : set @ a] : (($true != ((topolo1751647064n_open @ a @ X4))) | (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (((member @ a @ (sK39 @ X4) @ X4)) = $true) | (((f @ x0)) != ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | (((member @ a @ x0 @ X4)) != $true)) )),
% 0.50/0.44 inference(cnf_transformation,[],[f1283])).
% 0.50/0.44 thf(f1713,plain,(
% 0.50/0.44 ( ! [X4 : set @ a] : ((((ord_less @ extended_ereal @ sK38 @ (f @ (sK39 @ X4)))) != $true) | ($true != ((topolo1751647064n_open @ a @ X4))) | (((f @ x0)) != ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | (((member @ a @ x0 @ X4)) != $true) | (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true)) )),
% 0.50/0.44 inference(cnf_transformation,[],[f1283])).
% 0.50/0.44 thf(f1714,plain,(
% 0.50/0.44 ( ! [X0 : extended_ereal] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) != $true) | (((topolo1751647064n_open @ a @ (sK37 @ X0))) = $true) | (((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true) | (((f @ x0)) != ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal)))) )),
% 0.50/0.44 inference(cnf_transformation,[],[f1283])).
% 0.50/0.44 thf(f1715,plain,(
% 0.50/0.44 ( ! [X2 : a,X0 : extended_ereal] : ((((member @ a @ X2 @ (sK37 @ X0))) != $true) | (((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true) | (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) != $true) | (((ord_less @ extended_ereal @ X0 @ (f @ X2))) = $true) | (((f @ x0)) != ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal)))) )),
% 0.50/0.44 inference(cnf_transformation,[],[f1283])).
% 0.50/0.44 thf(f1716,plain,(
% 0.50/0.44 ( ! [X0 : extended_ereal] : ((((f @ x0)) != ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | (((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true) | (((member @ a @ x0 @ (sK37 @ X0))) = $true) | (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) != $true)) )),
% 0.50/0.44 inference(cnf_transformation,[],[f1283])).
% 0.50/0.44 thf(f1896,plain,(
% 0.50/0.44 ( ! [X3 : extended_ereal,X5 : a] : (($true != ((ord_less @ extended_ereal @ X3 @ (f @ x0)))) | (((f @ x0)) != extend1396239628finity @ extended_ereal) | (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) != $true) | (((ord_less @ extended_ereal @ X3 @ (f @ X5))) = $true) | (((member @ a @ X5 @ (sK60 @ X3))) != $true)) )),
% 0.50/0.44 inference(cnf_transformation,[],[f1363])).
% 0.50/0.44 thf(f1897,plain,(
% 0.50/0.44 ( ! [X3 : extended_ereal] : (($true != ((ord_less @ extended_ereal @ X3 @ (f @ x0)))) | ($true = ((topolo1751647064n_open @ a @ (sK60 @ X3)))) | (((f @ x0)) != extend1396239628finity @ extended_ereal) | (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) != $true)) )),
% 0.50/0.44 inference(cnf_transformation,[],[f1363])).
% 0.50/0.44 thf(f1898,plain,(
% 0.50/0.44 ( ! [X3 : extended_ereal] : ((((f @ x0)) != extend1396239628finity @ extended_ereal) | (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) != $true) | ($true = ((member @ a @ x0 @ (sK60 @ X3)))) | ($true != ((ord_less @ extended_ereal @ X3 @ (f @ x0))))) )),
% 0.50/0.44 inference(cnf_transformation,[],[f1363])).
% 0.50/0.44 thf(f1899,plain,(
% 0.50/0.44 ( ! [X1 : set @ a] : ((((topolo1751647064n_open @ a @ X1)) != $true) | (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (((f @ x0)) != extend1396239628finity @ extended_ereal) | ($true = ((member @ a @ (sK59 @ X1) @ X1))) | (((member @ a @ x0 @ X1)) != $true)) )),
% 0.50/0.44 inference(cnf_transformation,[],[f1363])).
% 0.50/0.44 thf(f1900,plain,(
% 0.50/0.44 ( ! [X1 : set @ a] : ((((f @ x0)) != extend1396239628finity @ extended_ereal) | (((ord_less @ extended_ereal @ sK58 @ (f @ (sK59 @ X1)))) != $true) | (((topolo1751647064n_open @ a @ X1)) != $true) | (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (((member @ a @ x0 @ X1)) != $true)) )),
% 0.50/0.44 inference(cnf_transformation,[],[f1363])).
% 0.50/0.44 thf(f1901,plain,(
% 0.50/0.44 (((f @ x0)) != extend1396239628finity @ extended_ereal) | ($true = ((ord_less @ extended_ereal @ sK58 @ (f @ x0)))) | (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true)),
% 0.50/0.44 inference(cnf_transformation,[],[f1363])).
% 0.50/0.44 thf(f2279,definition,(
% 0.50/0.44 spl63_5 <=> (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true)),
% 0.50/0.44 introduced(definition,[new_symbols(definition,[spl63_5])],[avatar_definition])).
% 0.50/0.44 thf(f2283,definition,(
% 0.50/0.44 spl63_6 <=> ! [X2 : a,X0 : extended_ereal] : ((((member @ a @ X2 @ (sK37 @ X0))) != $true) | (((ord_less @ extended_ereal @ X0 @ (f @ X2))) = $true) | (((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true))),
% 0.50/0.44 introduced(definition,[new_symbols(definition,[spl63_6])],[avatar_definition])).
% 0.50/0.44 thf(f2284,plain,(
% 0.50/0.44 ( ! [X2 : a,X0 : extended_ereal] : ((((member @ a @ X2 @ (sK37 @ X0))) != $true) | (((ord_less @ extended_ereal @ X0 @ (f @ X2))) = $true) | (((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true)) ) | ~spl63_6),
% 0.50/0.44 inference(avatar_component_clause,[],[f2283])).
% 0.50/0.44 thf(f2286,definition,(
% 0.50/0.44 spl63_7 <=> (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal)))),
% 0.50/0.44 introduced(definition,[new_symbols(definition,[spl63_7])],[avatar_definition])).
% 0.50/0.44 thf(f2287,plain,(
% 0.50/0.44 (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | ~spl63_7),
% 0.50/0.44 inference(avatar_component_clause,[],[f2286])).
% 0.50/0.44 thf(f2289,plain,(
% 0.50/0.44 ~spl63_5 | spl63_6 | ~spl63_7),
% 0.50/0.44 inference(avatar_split_clause,[],[f1715,f2286,f2283,f2279])).
% 0.50/0.44 thf(f2291,definition,(
% 0.50/0.44 spl63_8 <=> (((f @ x0)) = extend1396239628finity @ extended_ereal)),
% 0.50/0.44 introduced(definition,[new_symbols(definition,[spl63_8])],[avatar_definition])).
% 0.50/0.44 thf(f2292,plain,(
% 0.50/0.44 (((f @ x0)) = extend1396239628finity @ extended_ereal) | ~spl63_8),
% 0.50/0.44 inference(avatar_component_clause,[],[f2291])).
% 0.50/0.44 thf(f2295,definition,(
% 0.50/0.44 spl63_9 <=> ! [X1 : set @ a] : ((((ord_less @ extended_ereal @ sK58 @ (f @ (sK59 @ X1)))) != $true) | (((member @ a @ x0 @ X1)) != $true) | (((topolo1751647064n_open @ a @ X1)) != $true))),
% 0.50/0.44 introduced(definition,[new_symbols(definition,[spl63_9])],[avatar_definition])).
% 0.50/0.44 thf(f2296,plain,(
% 0.50/0.44 ( ! [X1 : set @ a] : ((((ord_less @ extended_ereal @ sK58 @ (f @ (sK59 @ X1)))) != $true) | (((member @ a @ x0 @ X1)) != $true) | (((topolo1751647064n_open @ a @ X1)) != $true)) ) | ~spl63_9),
% 0.50/0.44 inference(avatar_component_clause,[],[f2295])).
% 0.50/0.44 thf(f2297,plain,(
% 0.50/0.44 ~spl63_8 | spl63_9 | spl63_5),
% 0.50/0.44 inference(avatar_split_clause,[],[f1900,f2279,f2295,f2291])).
% 0.50/0.44 thf(f2299,definition,(
% 0.50/0.44 spl63_10 <=> ! [X0 : extended_ereal] : ((((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true) | (((member @ a @ x0 @ (sK37 @ X0))) = $true))),
% 0.50/0.44 introduced(definition,[new_symbols(definition,[spl63_10])],[avatar_definition])).
% 0.50/0.44 thf(f2300,plain,(
% 0.50/0.44 ( ! [X0 : extended_ereal] : ((((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true) | (((member @ a @ x0 @ (sK37 @ X0))) = $true)) ) | ~spl63_10),
% 0.50/0.44 inference(avatar_component_clause,[],[f2299])).
% 0.50/0.44 thf(f2301,plain,(
% 0.50/0.44 spl63_10 | ~spl63_7 | ~spl63_5),
% 0.50/0.44 inference(avatar_split_clause,[],[f1716,f2279,f2286,f2299])).
% 0.50/0.44 thf(f2323,definition,(
% 0.50/0.44 spl63_15 <=> ! [X3 : extended_ereal] : (($true = ((topolo1751647064n_open @ a @ (sK12 @ X3)))) | ($true != ((ord_less @ extended_ereal @ X3 @ (f @ x0)))))),
% 0.50/0.44 introduced(definition,[new_symbols(definition,[spl63_15])],[avatar_definition])).
% 0.50/0.44 thf(f2324,plain,(
% 0.50/0.44 ( ! [X3 : extended_ereal] : (($true != ((ord_less @ extended_ereal @ X3 @ (f @ x0)))) | ($true = ((topolo1751647064n_open @ a @ (sK12 @ X3))))) ) | ~spl63_15),
% 0.50/0.44 inference(avatar_component_clause,[],[f2323])).
% 0.50/0.44 thf(f2325,plain,(
% 0.50/0.44 spl63_15 | spl63_5),
% 0.50/0.44 inference(avatar_split_clause,[],[f1490,f2279,f2323])).
% 0.50/0.44 thf(f2357,definition,(
% 0.50/0.44 spl63_22 <=> ! [X5 : a,X3 : extended_ereal] : (($true != ((ord_less @ extended_ereal @ X3 @ (f @ x0)))) | (((ord_less @ extended_ereal @ X3 @ (f @ X5))) = $true) | ($true != ((member @ a @ X5 @ (sK12 @ X3)))))),
% 0.50/0.44 introduced(definition,[new_symbols(definition,[spl63_22])],[avatar_definition])).
% 0.50/0.44 thf(f2358,plain,(
% 0.50/0.44 ( ! [X3 : extended_ereal,X5 : a] : (($true != ((member @ a @ X5 @ (sK12 @ X3)))) | ($true != ((ord_less @ extended_ereal @ X3 @ (f @ x0)))) | (((ord_less @ extended_ereal @ X3 @ (f @ X5))) = $true)) ) | ~spl63_22),
% 0.50/0.44 inference(avatar_component_clause,[],[f2357])).
% 0.50/0.44 thf(f2359,plain,(
% 0.50/0.44 spl63_22 | spl63_5),
% 0.50/0.44 inference(avatar_split_clause,[],[f1489,f2279,f2357])).
% 0.50/0.44 thf(f2361,definition,(
% 0.50/0.44 spl63_23 <=> ! [X3 : extended_ereal] : (($true != ((ord_less @ extended_ereal @ X3 @ (f @ x0)))) | ($true = ((topolo1751647064n_open @ a @ (sK60 @ X3)))))),
% 0.50/0.44 introduced(definition,[new_symbols(definition,[spl63_23])],[avatar_definition])).
% 0.50/0.44 thf(f2362,plain,(
% 0.50/0.44 ( ! [X3 : extended_ereal] : (($true != ((ord_less @ extended_ereal @ X3 @ (f @ x0)))) | ($true = ((topolo1751647064n_open @ a @ (sK60 @ X3))))) ) | ~spl63_23),
% 0.50/0.44 inference(avatar_component_clause,[],[f2361])).
% 0.50/0.44 thf(f2363,plain,(
% 0.50/0.44 ~spl63_8 | ~spl63_5 | spl63_23),
% 0.50/0.44 inference(avatar_split_clause,[],[f1897,f2361,f2279,f2291])).
% 0.50/0.44 thf(f2365,definition,(
% 0.50/0.44 spl63_24 <=> ! [X2 : a,X0 : extended_ereal] : ((((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true) | (((ord_less @ extended_ereal @ X0 @ (f @ X2))) = $true) | ($true != ((member @ a @ X2 @ (sK21 @ X0)))))),
% 0.50/0.44 introduced(definition,[new_symbols(definition,[spl63_24])],[avatar_definition])).
% 0.50/0.44 thf(f2366,plain,(
% 0.50/0.44 ( ! [X2 : a,X0 : extended_ereal] : (($true != ((member @ a @ X2 @ (sK21 @ X0)))) | (((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true) | (((ord_less @ extended_ereal @ X0 @ (f @ X2))) = $true)) ) | ~spl63_24),
% 0.50/0.44 inference(avatar_component_clause,[],[f2365])).
% 0.50/0.44 thf(f2367,plain,(
% 0.50/0.44 spl63_24 | spl63_7 | ~spl63_5 | spl63_8),
% 0.50/0.44 inference(avatar_split_clause,[],[f1594,f2291,f2279,f2286,f2365])).
% 0.50/0.44 thf(f2379,definition,(
% 0.50/0.44 spl63_27 <=> ! [X1 : set @ a] : ((((member @ a @ x0 @ X1)) != $true) | (((topolo1751647064n_open @ a @ X1)) != $true) | (((ord_less @ extended_ereal @ sK10 @ (f @ (sK11 @ X1)))) != $true))),
% 0.50/0.44 introduced(definition,[new_symbols(definition,[spl63_27])],[avatar_definition])).
% 0.50/0.44 thf(f2380,plain,(
% 0.50/0.44 ( ! [X1 : set @ a] : ((((ord_less @ extended_ereal @ sK10 @ (f @ (sK11 @ X1)))) != $true) | (((member @ a @ x0 @ X1)) != $true) | (((topolo1751647064n_open @ a @ X1)) != $true)) ) | ~spl63_27),
% 0.50/0.44 inference(avatar_component_clause,[],[f2379])).
% 0.50/0.44 thf(f2381,plain,(
% 0.50/0.44 ~spl63_5 | spl63_27),
% 0.50/0.44 inference(avatar_split_clause,[],[f1492,f2379,f2279])).
% 0.50/0.44 thf(f2383,definition,(
% 0.50/0.44 spl63_28 <=> ! [X0 : extended_ereal] : ((((topolo1751647064n_open @ a @ (sK37 @ X0))) = $true) | (((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true))),
% 0.50/0.44 introduced(definition,[new_symbols(definition,[spl63_28])],[avatar_definition])).
% 0.50/0.44 thf(f2384,plain,(
% 0.50/0.44 ( ! [X0 : extended_ereal] : ((((topolo1751647064n_open @ a @ (sK37 @ X0))) = $true) | (((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true)) ) | ~spl63_28),
% 0.50/0.44 inference(avatar_component_clause,[],[f2383])).
% 0.50/0.44 thf(f2385,plain,(
% 0.50/0.44 ~spl63_7 | ~spl63_5 | spl63_28),
% 0.50/0.44 inference(avatar_split_clause,[],[f1714,f2383,f2279,f2286])).
% 0.50/0.44 thf(f2387,definition,(
% 0.50/0.44 spl63_29 <=> ($true = ((ord_less @ extended_ereal @ sK58 @ (f @ x0))))),
% 0.50/0.44 introduced(definition,[new_symbols(definition,[spl63_29])],[avatar_definition])).
% 0.50/0.44 thf(f2390,plain,(
% 0.50/0.44 spl63_29 | spl63_5 | ~spl63_8),
% 0.50/0.44 inference(avatar_split_clause,[],[f1901,f2291,f2279,f2387])).
% 0.50/0.44 thf(f2397,definition,(
% 0.50/0.44 spl63_31 <=> ($true = ((ord_less @ extended_ereal @ sK10 @ (f @ x0))))),
% 0.50/0.44 introduced(definition,[new_symbols(definition,[spl63_31])],[avatar_definition])).
% 0.50/0.44 thf(f2399,plain,(
% 0.50/0.44 ($true = ((ord_less @ extended_ereal @ sK10 @ (f @ x0)))) | ~spl63_31),
% 0.50/0.44 inference(avatar_component_clause,[],[f2397])).
% 0.50/0.44 thf(f2400,plain,(
% 0.50/0.44 spl63_31 | ~spl63_5),
% 0.50/0.44 inference(avatar_split_clause,[],[f1494,f2279,f2397])).
% 0.50/0.44 thf(f2407,definition,(
% 0.50/0.44 spl63_33 <=> ! [X0 : extended_ereal] : ((((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true) | ($true = ((member @ a @ x0 @ (sK21 @ X0)))))),
% 0.50/0.44 introduced(definition,[new_symbols(definition,[spl63_33])],[avatar_definition])).
% 0.50/0.44 thf(f2408,plain,(
% 0.50/0.44 ( ! [X0 : extended_ereal] : (($true = ((member @ a @ x0 @ (sK21 @ X0)))) | (((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true)) ) | ~spl63_33),
% 0.50/0.44 inference(avatar_component_clause,[],[f2407])).
% 0.50/0.44 thf(f2409,plain,(
% 0.50/0.44 spl63_7 | ~spl63_5 | spl63_8 | spl63_33),
% 0.50/0.44 inference(avatar_split_clause,[],[f1592,f2407,f2291,f2279,f2286])).
% 0.50/0.44 thf(f2421,definition,(
% 0.50/0.44 spl63_36 <=> ! [X4 : set @ a] : (($true != ((topolo1751647064n_open @ a @ X4))) | ($true = ((member @ a @ (sK23 @ X4) @ X4))) | (((member @ a @ x0 @ X4)) != $true))),
% 0.50/0.44 introduced(definition,[new_symbols(definition,[spl63_36])],[avatar_definition])).
% 0.50/0.44 thf(f2422,plain,(
% 0.50/0.44 ( ! [X4 : set @ a] : (($true = ((member @ a @ (sK23 @ X4) @ X4))) | ($true != ((topolo1751647064n_open @ a @ X4))) | (((member @ a @ x0 @ X4)) != $true)) ) | ~spl63_36),
% 0.50/0.44 inference(avatar_component_clause,[],[f2421])).
% 0.50/0.44 thf(f2423,plain,(
% 0.50/0.44 spl63_36 | spl63_7 | spl63_8 | spl63_5),
% 0.50/0.44 inference(avatar_split_clause,[],[f1590,f2279,f2291,f2286,f2421])).
% 0.50/0.44 thf(f2450,definition,(
% 0.50/0.44 spl63_42 <=> ! [X1 : set @ a] : ((((topolo1751647064n_open @ a @ X1)) != $true) | (((member @ a @ x0 @ X1)) != $true) | ($true = ((member @ a @ (sK59 @ X1) @ X1))))),
% 0.50/0.44 introduced(definition,[new_symbols(definition,[spl63_42])],[avatar_definition])).
% 0.50/0.44 thf(f2451,plain,(
% 0.50/0.44 ( ! [X1 : set @ a] : (($true = ((member @ a @ (sK59 @ X1) @ X1))) | (((topolo1751647064n_open @ a @ X1)) != $true) | (((member @ a @ x0 @ X1)) != $true)) ) | ~spl63_42),
% 0.50/0.44 inference(avatar_component_clause,[],[f2450])).
% 0.50/0.44 thf(f2452,plain,(
% 0.50/0.44 ~spl63_8 | spl63_42 | spl63_5),
% 0.50/0.44 inference(avatar_split_clause,[],[f1899,f2279,f2450,f2291])).
% 0.50/0.44 thf(f2466,definition,(
% 0.50/0.44 spl63_46 <=> ! [X4 : set @ a] : ((((ord_less @ extended_ereal @ sK38 @ (f @ (sK39 @ X4)))) != $true) | (((member @ a @ x0 @ X4)) != $true) | ($true != ((topolo1751647064n_open @ a @ X4))))),
% 0.50/0.44 introduced(definition,[new_symbols(definition,[spl63_46])],[avatar_definition])).
% 0.50/0.44 thf(f2467,plain,(
% 0.50/0.44 ( ! [X4 : set @ a] : ((((ord_less @ extended_ereal @ sK38 @ (f @ (sK39 @ X4)))) != $true) | ($true != ((topolo1751647064n_open @ a @ X4))) | (((member @ a @ x0 @ X4)) != $true)) ) | ~spl63_46),
% 0.50/0.44 inference(avatar_component_clause,[],[f2466])).
% 0.50/0.44 thf(f2468,plain,(
% 0.50/0.44 spl63_46 | spl63_5 | ~spl63_7),
% 0.50/0.44 inference(avatar_split_clause,[],[f1713,f2286,f2279,f2466])).
% 0.50/0.44 thf(f2480,definition,(
% 0.50/0.44 spl63_49 <=> ! [X4 : set @ a] : ((((member @ a @ x0 @ X4)) != $true) | ($true != ((topolo1751647064n_open @ a @ X4))) | (((ord_less @ extended_ereal @ sK22 @ (f @ (sK23 @ X4)))) != $true))),
% 0.50/0.44 introduced(definition,[new_symbols(definition,[spl63_49])],[avatar_definition])).
% 0.50/0.44 thf(f2481,plain,(
% 0.50/0.44 ( ! [X4 : set @ a] : ((((ord_less @ extended_ereal @ sK22 @ (f @ (sK23 @ X4)))) != $true) | (((member @ a @ x0 @ X4)) != $true) | ($true != ((topolo1751647064n_open @ a @ X4)))) ) | ~spl63_49),
% 0.50/0.44 inference(avatar_component_clause,[],[f2480])).
% 0.50/0.44 thf(f2482,plain,(
% 0.50/0.44 spl63_7 | spl63_5 | spl63_8 | spl63_49),
% 0.50/0.44 inference(avatar_split_clause,[],[f1591,f2480,f2291,f2279,f2286])).
% 0.50/0.44 thf(f2484,definition,(
% 0.50/0.44 spl63_50 <=> ! [X0 : extended_ereal] : ((((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true) | ($true = ((topolo1751647064n_open @ a @ (sK21 @ X0)))))),
% 0.50/0.44 introduced(definition,[new_symbols(definition,[spl63_50])],[avatar_definition])).
% 0.50/0.44 thf(f2485,plain,(
% 0.50/0.44 ( ! [X0 : extended_ereal] : ((((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true) | ($true = ((topolo1751647064n_open @ a @ (sK21 @ X0))))) ) | ~spl63_50),
% 0.50/0.44 inference(avatar_component_clause,[],[f2484])).
% 0.50/0.44 thf(f2486,plain,(
% 0.50/0.44 spl63_7 | spl63_8 | ~spl63_5 | spl63_50),
% 0.50/0.44 inference(avatar_split_clause,[],[f1593,f2484,f2279,f2291,f2286])).
% 0.50/0.44 thf(f2498,definition,(
% 0.50/0.44 spl63_53 <=> ! [X1 : set @ a] : ((((member @ a @ (sK11 @ X1) @ X1)) = $true) | (((member @ a @ x0 @ X1)) != $true) | (((topolo1751647064n_open @ a @ X1)) != $true))),
% 0.50/0.44 introduced(definition,[new_symbols(definition,[spl63_53])],[avatar_definition])).
% 0.50/0.44 thf(f2499,plain,(
% 0.50/0.44 ( ! [X1 : set @ a] : ((((member @ a @ (sK11 @ X1) @ X1)) = $true) | (((topolo1751647064n_open @ a @ X1)) != $true) | (((member @ a @ x0 @ X1)) != $true)) ) | ~spl63_53),
% 0.50/0.44 inference(avatar_component_clause,[],[f2498])).
% 0.50/0.44 thf(f2500,plain,(
% 0.50/0.44 spl63_53 | ~spl63_5),
% 0.50/0.44 inference(avatar_split_clause,[],[f1493,f2279,f2498])).
% 0.50/0.44 thf(f2512,definition,(
% 0.50/0.44 spl63_56 <=> ($true = ((ord_less @ extended_ereal @ sK22 @ (f @ x0))))),
% 0.50/0.44 introduced(definition,[new_symbols(definition,[spl63_56])],[avatar_definition])).
% 0.50/0.44 thf(f2515,plain,(
% 0.50/0.44 spl63_56 | spl63_7 | spl63_5 | spl63_8),
% 0.50/0.44 inference(avatar_split_clause,[],[f1589,f2291,f2279,f2286,f2512])).
% 0.50/0.44 thf(f2537,definition,(
% 0.50/0.44 spl63_61 <=> (((ord_less @ extended_ereal @ sK38 @ (f @ x0))) = $true)),
% 0.50/0.44 introduced(definition,[new_symbols(definition,[spl63_61])],[avatar_definition])).
% 0.50/0.44 thf(f2539,plain,(
% 0.50/0.44 (((ord_less @ extended_ereal @ sK38 @ (f @ x0))) = $true) | ~spl63_61),
% 0.50/0.44 inference(avatar_component_clause,[],[f2537])).
% 0.50/0.44 thf(f2540,plain,(
% 0.50/0.44 spl63_5 | spl63_61 | ~spl63_7),
% 0.50/0.44 inference(avatar_split_clause,[],[f1711,f2286,f2537,f2279])).
% 0.50/0.44 thf(f2552,definition,(
% 0.50/0.44 spl63_64 <=> ! [X3 : extended_ereal] : ((((member @ a @ x0 @ (sK12 @ X3))) = $true) | ($true != ((ord_less @ extended_ereal @ X3 @ (f @ x0)))))),
% 0.50/0.44 introduced(definition,[new_symbols(definition,[spl63_64])],[avatar_definition])).
% 0.50/0.44 thf(f2553,plain,(
% 0.50/0.44 ( ! [X3 : extended_ereal] : ((((member @ a @ x0 @ (sK12 @ X3))) = $true) | ($true != ((ord_less @ extended_ereal @ X3 @ (f @ x0))))) ) | ~spl63_64),
% 0.50/0.44 inference(avatar_component_clause,[],[f2552])).
% 0.50/0.44 thf(f2554,plain,(
% 0.50/0.44 spl63_5 | spl63_64),
% 0.50/0.44 inference(avatar_split_clause,[],[f1491,f2552,f2279])).
% 0.50/0.44 thf(f2561,definition,(
% 0.50/0.44 spl63_66 <=> ! [X5 : a,X3 : extended_ereal] : (($true != ((ord_less @ extended_ereal @ X3 @ (f @ x0)))) | (((member @ a @ X5 @ (sK60 @ X3))) != $true) | (((ord_less @ extended_ereal @ X3 @ (f @ X5))) = $true))),
% 0.50/0.44 introduced(definition,[new_symbols(definition,[spl63_66])],[avatar_definition])).
% 0.50/0.44 thf(f2562,plain,(
% 0.50/0.44 ( ! [X3 : extended_ereal,X5 : a] : ((((member @ a @ X5 @ (sK60 @ X3))) != $true) | (((ord_less @ extended_ereal @ X3 @ (f @ X5))) = $true) | ($true != ((ord_less @ extended_ereal @ X3 @ (f @ x0))))) ) | ~spl63_66),
% 0.50/0.44 inference(avatar_component_clause,[],[f2561])).
% 0.50/0.44 thf(f2563,plain,(
% 0.50/0.44 ~spl63_8 | ~spl63_5 | spl63_66),
% 0.50/0.44 inference(avatar_split_clause,[],[f1896,f2561,f2279,f2291])).
% 0.50/0.44 thf(f2565,definition,(
% 0.50/0.44 spl63_67 <=> ! [X4 : set @ a] : (($true != ((topolo1751647064n_open @ a @ X4))) | (((member @ a @ x0 @ X4)) != $true) | (((member @ a @ (sK39 @ X4) @ X4)) = $true))),
% 0.50/0.44 introduced(definition,[new_symbols(definition,[spl63_67])],[avatar_definition])).
% 0.50/0.44 thf(f2566,plain,(
% 0.50/0.44 ( ! [X4 : set @ a] : ((((member @ a @ (sK39 @ X4) @ X4)) = $true) | ($true != ((topolo1751647064n_open @ a @ X4))) | (((member @ a @ x0 @ X4)) != $true)) ) | ~spl63_67),
% 0.50/0.44 inference(avatar_component_clause,[],[f2565])).
% 0.50/0.44 thf(f2567,plain,(
% 0.50/0.44 spl63_5 | ~spl63_7 | spl63_67),
% 0.50/0.44 inference(avatar_split_clause,[],[f1712,f2565,f2286,f2279])).
% 0.50/0.44 thf(f2584,definition,(
% 0.50/0.44 spl63_71 <=> ! [X3 : extended_ereal] : (($true = ((member @ a @ x0 @ (sK60 @ X3)))) | ($true != ((ord_less @ extended_ereal @ X3 @ (f @ x0)))))),
% 0.50/0.44 introduced(definition,[new_symbols(definition,[spl63_71])],[avatar_definition])).
% 0.50/0.44 thf(f2585,plain,(
% 0.50/0.44 ( ! [X3 : extended_ereal] : (($true = ((member @ a @ x0 @ (sK60 @ X3)))) | ($true != ((ord_less @ extended_ereal @ X3 @ (f @ x0))))) ) | ~spl63_71),
% 0.50/0.44 inference(avatar_component_clause,[],[f2584])).
% 0.50/0.44 thf(f2586,plain,(
% 0.50/0.44 ~spl63_5 | spl63_71 | ~spl63_8),
% 0.50/0.44 inference(avatar_split_clause,[],[f1898,f2291,f2584,f2279])).
% 0.50/0.44 thf(f2627,plain,(
% 0.50/0.44 ( ! [X0 : extended_ereal] : (($true != ((topolo1751647064n_open @ a @ (sK12 @ X0)))) | ($true = ((ord_less @ extended_ereal @ X0 @ (f @ (sK23 @ (sK12 @ X0)))))) | ($true != $true) | (((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true) | (((member @ a @ x0 @ (sK12 @ X0))) != $true)) ) | (~spl63_22 | ~spl63_36)),
% 0.50/0.44 inference(superposition,[],[f2358,f2422])).
% 0.50/0.44 thf(f2628,plain,(
% 0.50/0.44 ( ! [X0 : extended_ereal] : (($true != ((topolo1751647064n_open @ a @ (sK12 @ X0)))) | (((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true) | ($true = ((ord_less @ extended_ereal @ X0 @ (f @ (sK23 @ (sK12 @ X0)))))) | (((member @ a @ x0 @ (sK12 @ X0))) != $true)) ) | (~spl63_22 | ~spl63_36)),
% 0.50/0.44 inference(trivial_inequality_removal,[],[f2627])).
% 0.50/0.44 thf(f2629,plain,(
% 0.50/0.44 ( ! [X0 : extended_ereal] : ((((member @ a @ x0 @ (sK12 @ X0))) != $true) | ($true = ((ord_less @ extended_ereal @ X0 @ (f @ (sK23 @ (sK12 @ X0)))))) | (((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true)) ) | (~spl63_15 | ~spl63_22 | ~spl63_36)),
% 0.50/0.44 inference(forward_subsumption_resolution,[],[f2628,f2324])).
% 0.50/0.44 thf(f2630,plain,(
% 0.50/0.44 ( ! [X0 : extended_ereal] : (($true = ((ord_less @ extended_ereal @ X0 @ (f @ (sK23 @ (sK12 @ X0)))))) | (((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true)) ) | (~spl63_15 | ~spl63_22 | ~spl63_36 | ~spl63_64)),
% 0.50/0.44 inference(forward_subsumption_resolution,[],[f2629,f2553])).
% 0.50/0.44 thf(f2631,plain,(
% 0.50/0.44 ( ! [X0 : extended_ereal] : ((((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true) | (((ord_less @ extended_ereal @ X0 @ (f @ (sK59 @ (sK12 @ X0))))) = $true) | (((member @ a @ x0 @ (sK12 @ X0))) != $true) | ($true != ((topolo1751647064n_open @ a @ (sK12 @ X0)))) | ($true != $true)) ) | (~spl63_22 | ~spl63_42)),
% 0.50/0.44 inference(superposition,[],[f2358,f2451])).
% 0.50/0.44 thf(f2632,plain,(
% 0.50/0.44 ( ! [X0 : extended_ereal] : ((((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true) | ($true != ((topolo1751647064n_open @ a @ (sK12 @ X0)))) | (((member @ a @ x0 @ (sK12 @ X0))) != $true) | (((ord_less @ extended_ereal @ X0 @ (f @ (sK59 @ (sK12 @ X0))))) = $true)) ) | (~spl63_22 | ~spl63_42)),
% 0.50/0.44 inference(trivial_inequality_removal,[],[f2631])).
% 0.50/0.44 thf(f2633,plain,(
% 0.50/0.44 ( ! [X0 : extended_ereal] : ((((member @ a @ x0 @ (sK12 @ X0))) != $true) | (((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true) | (((ord_less @ extended_ereal @ X0 @ (f @ (sK59 @ (sK12 @ X0))))) = $true)) ) | (~spl63_15 | ~spl63_22 | ~spl63_42)),
% 0.50/0.44 inference(forward_subsumption_resolution,[],[f2632,f2324])).
% 0.50/0.44 thf(f2634,plain,(
% 0.50/0.44 ( ! [X0 : extended_ereal] : ((((ord_less @ extended_ereal @ X0 @ (f @ (sK59 @ (sK12 @ X0))))) = $true) | (((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true)) ) | (~spl63_15 | ~spl63_22 | ~spl63_42 | ~spl63_64)),
% 0.50/0.44 inference(forward_subsumption_resolution,[],[f2633,f2553])).
% 0.50/0.44 thf(f2637,plain,(
% 0.50/0.44 ($true != $true) | ($true != ((topolo1751647064n_open @ a @ (sK12 @ sK22)))) | ($true != ((ord_less @ extended_ereal @ sK22 @ (f @ x0)))) | ($true != ((member @ a @ x0 @ (sK12 @ sK22)))) | (~spl63_15 | ~spl63_22 | ~spl63_36 | ~spl63_49 | ~spl63_64)),
% 0.50/0.44 inference(superposition,[],[f2481,f2630])).
% 0.50/0.44 thf(f2640,plain,(
% 0.50/0.44 ($true != ((ord_less @ extended_ereal @ sK22 @ (f @ x0)))) | ($true != ((topolo1751647064n_open @ a @ (sK12 @ sK22)))) | ($true != ((member @ a @ x0 @ (sK12 @ sK22)))) | (~spl63_15 | ~spl63_22 | ~spl63_36 | ~spl63_49 | ~spl63_64)),
% 0.50/0.44 inference(trivial_inequality_removal,[],[f2637])).
% 0.50/0.44 thf(f2641,plain,(
% 0.50/0.44 ($true != ((member @ a @ x0 @ (sK12 @ sK22)))) | ($true != ((ord_less @ extended_ereal @ sK22 @ (f @ x0)))) | (~spl63_15 | ~spl63_22 | ~spl63_36 | ~spl63_49 | ~spl63_64)),
% 0.50/0.44 inference(forward_subsumption_resolution,[],[f2640,f2324])).
% 0.50/0.44 thf(f2642,plain,(
% 0.50/0.44 ($true != ((ord_less @ extended_ereal @ sK22 @ (f @ x0)))) | (~spl63_15 | ~spl63_22 | ~spl63_36 | ~spl63_49 | ~spl63_64)),
% 0.50/0.44 inference(forward_subsumption_resolution,[],[f2641,f2553])).
% 0.50/0.44 thf(f2645,plain,(
% 0.50/0.44 ~spl63_56 | ~spl63_15 | ~spl63_22 | ~spl63_36 | ~spl63_49 | ~spl63_64),
% 0.50/0.44 inference(avatar_split_clause,[],[f2642,f2552,f2480,f2421,f2357,f2323,f2512])).
% 0.50/0.44 thf(f2648,plain,(
% 0.50/0.44 ( ! [X0 : extended_ereal] : ((((ord_less @ extended_ereal @ X0 @ (uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) != $true) | ($true = ((topolo1751647064n_open @ a @ (sK12 @ X0))))) ) | (~spl63_7 | ~spl63_15)),
% 0.50/0.44 inference(superposition,[],[f2324,f2287])).
% 0.50/0.44 thf(f2654,plain,(
% 0.50/0.44 ($true = ((ord_less @ extended_ereal @ sK38 @ (uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal)))) | (~spl63_7 | ~spl63_61)),
% 0.50/0.44 inference(forward_demodulation,[],[f2539,f2287])).
% 0.50/0.44 thf(f2656,definition,(
% 0.50/0.44 spl63_77 <=> ($true = ((ord_less @ extended_ereal @ sK38 @ (uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))))),
% 0.50/0.44 introduced(definition,[new_symbols(definition,[spl63_77])],[avatar_definition])).
% 0.50/0.44 thf(f2658,plain,(
% 0.50/0.44 ($true = ((ord_less @ extended_ereal @ sK38 @ (uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal)))) | ~spl63_77),
% 0.50/0.44 inference(avatar_component_clause,[],[f2656])).
% 0.50/0.44 thf(f2659,plain,(
% 0.50/0.44 spl63_77 | ~spl63_7 | ~spl63_61),
% 0.50/0.44 inference(avatar_split_clause,[],[f2654,f2537,f2286,f2656])).
% 0.50/0.44 thf(f2660,plain,(
% 0.50/0.44 ( ! [X0 : extended_ereal] : (($true != $true) | ($true != ((topolo1751647064n_open @ a @ (sK12 @ X0)))) | (((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true) | (((ord_less @ extended_ereal @ X0 @ (f @ (sK39 @ (sK12 @ X0))))) = $true) | (((member @ a @ x0 @ (sK12 @ X0))) != $true)) ) | (~spl63_22 | ~spl63_67)),
% 0.50/0.44 inference(superposition,[],[f2358,f2566])).
% 0.50/0.44 thf(f2661,plain,(
% 0.50/0.44 ( ! [X0 : extended_ereal] : (($true != ((topolo1751647064n_open @ a @ (sK12 @ X0)))) | (((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true) | (((member @ a @ x0 @ (sK12 @ X0))) != $true) | (((ord_less @ extended_ereal @ X0 @ (f @ (sK39 @ (sK12 @ X0))))) = $true)) ) | (~spl63_22 | ~spl63_67)),
% 0.50/0.44 inference(trivial_inequality_removal,[],[f2660])).
% 0.50/0.44 thf(f2662,plain,(
% 0.50/0.44 ( ! [X0 : extended_ereal] : ((((ord_less @ extended_ereal @ X0 @ (f @ (sK39 @ (sK12 @ X0))))) = $true) | (((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true) | (((member @ a @ x0 @ (sK12 @ X0))) != $true)) ) | (~spl63_15 | ~spl63_22 | ~spl63_67)),
% 0.50/0.44 inference(forward_subsumption_resolution,[],[f2661,f2324])).
% 0.50/0.44 thf(f2663,plain,(
% 0.50/0.44 ( ! [X0 : extended_ereal] : ((((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true) | (((ord_less @ extended_ereal @ X0 @ (f @ (sK39 @ (sK12 @ X0))))) = $true)) ) | (~spl63_15 | ~spl63_22 | ~spl63_64 | ~spl63_67)),
% 0.50/0.44 inference(forward_subsumption_resolution,[],[f2662,f2553])).
% 0.50/0.44 thf(f2664,plain,(
% 0.50/0.44 ( ! [X0 : extended_ereal] : ((((ord_less @ extended_ereal @ X0 @ (f @ (sK39 @ (sK12 @ X0))))) = $true) | (((ord_less @ extended_ereal @ X0 @ (uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) != $true)) ) | (~spl63_7 | ~spl63_15 | ~spl63_22 | ~spl63_64 | ~spl63_67)),
% 0.50/0.44 inference(forward_demodulation,[],[f2663,f2287])).
% 0.50/0.44 thf(f2740,plain,(
% 0.50/0.44 ($true != $true) | (((topolo1751647064n_open @ a @ (sK12 @ sK38))) != $true) | ($true != ((ord_less @ extended_ereal @ sK38 @ (uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal)))) | (((member @ a @ x0 @ (sK12 @ sK38))) != $true) | (~spl63_7 | ~spl63_15 | ~spl63_22 | ~spl63_46 | ~spl63_64 | ~spl63_67)),
% 0.50/0.44 inference(superposition,[],[f2467,f2664])).
% 0.50/0.44 thf(f2742,plain,(
% 0.50/0.44 (((member @ a @ x0 @ (sK12 @ sK38))) != $true) | (((topolo1751647064n_open @ a @ (sK12 @ sK38))) != $true) | ($true != ((ord_less @ extended_ereal @ sK38 @ (uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal)))) | (~spl63_7 | ~spl63_15 | ~spl63_22 | ~spl63_46 | ~spl63_64 | ~spl63_67)),
% 0.50/0.44 inference(trivial_inequality_removal,[],[f2740])).
% 0.50/0.44 thf(f2744,plain,(
% 0.50/0.44 (((member @ a @ x0 @ (sK12 @ sK38))) != $true) | ($true != ((ord_less @ extended_ereal @ sK38 @ (uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal)))) | (~spl63_7 | ~spl63_15 | ~spl63_22 | ~spl63_46 | ~spl63_64 | ~spl63_67)),
% 0.50/0.44 inference(forward_subsumption_resolution,[],[f2742,f2648])).
% 0.50/0.44 thf(f2745,plain,(
% 0.50/0.44 (((member @ a @ x0 @ (sK12 @ sK38))) != $true) | (~spl63_7 | ~spl63_15 | ~spl63_22 | ~spl63_46 | ~spl63_64 | ~spl63_67 | ~spl63_77)),
% 0.50/0.44 inference(forward_subsumption_resolution,[],[f2744,f2658])).
% 0.50/0.44 thf(f2747,definition,(
% 0.50/0.44 spl63_81 <=> (((member @ a @ x0 @ (sK12 @ sK38))) = $true)),
% 0.50/0.44 introduced(definition,[new_symbols(definition,[spl63_81])],[avatar_definition])).
% 0.50/0.44 thf(f2749,plain,(
% 0.50/0.44 (((member @ a @ x0 @ (sK12 @ sK38))) != $true) | spl63_81),
% 0.50/0.44 inference(avatar_component_clause,[],[f2747])).
% 0.50/0.44 thf(f2750,plain,(
% 0.50/0.44 ~spl63_81 | ~spl63_7 | ~spl63_15 | ~spl63_22 | ~spl63_46 | ~spl63_64 | ~spl63_67 | ~spl63_77),
% 0.50/0.44 inference(avatar_split_clause,[],[f2745,f2656,f2565,f2552,f2466,f2357,f2323,f2286,f2747])).
% 0.50/0.44 thf(f2791,plain,(
% 0.50/0.44 (((ord_less @ extended_ereal @ sK38 @ (f @ x0))) != $true) | ($true != $true) | (~spl63_64 | spl63_81)),
% 0.50/0.44 inference(superposition,[],[f2749,f2553])).
% 0.50/0.44 thf(f2792,plain,(
% 0.50/0.44 (((ord_less @ extended_ereal @ sK38 @ (f @ x0))) != $true) | (~spl63_64 | spl63_81)),
% 0.50/0.44 inference(trivial_inequality_removal,[],[f2791])).
% 0.50/0.44 thf(f2793,plain,(
% 0.50/0.44 ($true != ((ord_less @ extended_ereal @ sK38 @ (uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal)))) | (~spl63_7 | ~spl63_64 | spl63_81)),
% 0.50/0.44 inference(forward_demodulation,[],[f2792,f2287])).
% 0.50/0.44 thf(f2794,plain,(
% 0.50/0.44 $false | (~spl63_7 | ~spl63_64 | ~spl63_77 | spl63_81)),
% 0.50/0.44 inference(forward_subsumption_resolution,[],[f2793,f2658])).
% 0.50/0.44 thf(f2795,plain,(
% 0.50/0.44 ~spl63_7 | ~spl63_64 | ~spl63_77 | spl63_81),
% 0.50/0.44 inference(avatar_contradiction_clause,[],[f2794])).
% 0.50/0.44 thf(f2796,plain,(
% 0.50/0.44 ($true != ((topolo1751647064n_open @ a @ (sK12 @ sK58)))) | (((member @ a @ x0 @ (sK12 @ sK58))) != $true) | ($true != $true) | ($true != ((ord_less @ extended_ereal @ sK58 @ (f @ x0)))) | (~spl63_9 | ~spl63_15 | ~spl63_22 | ~spl63_42 | ~spl63_64)),
% 0.50/0.44 inference(superposition,[],[f2296,f2634])).
% 0.50/0.44 thf(f2798,plain,(
% 0.50/0.44 (((member @ a @ x0 @ (sK12 @ sK58))) != $true) | ($true != ((ord_less @ extended_ereal @ sK58 @ (f @ x0)))) | ($true != ((topolo1751647064n_open @ a @ (sK12 @ sK58)))) | (~spl63_9 | ~spl63_15 | ~spl63_22 | ~spl63_42 | ~spl63_64)),
% 0.50/0.44 inference(trivial_inequality_removal,[],[f2796])).
% 0.50/0.44 thf(f2800,plain,(
% 0.50/0.44 ($true != ((topolo1751647064n_open @ a @ (sK12 @ sK58)))) | ($true != ((ord_less @ extended_ereal @ sK58 @ (f @ x0)))) | (~spl63_9 | ~spl63_15 | ~spl63_22 | ~spl63_42 | ~spl63_64)),
% 0.50/0.44 inference(forward_subsumption_resolution,[],[f2798,f2553])).
% 0.50/0.44 thf(f2801,plain,(
% 0.50/0.44 ($true != ((ord_less @ extended_ereal @ sK58 @ (f @ x0)))) | (~spl63_9 | ~spl63_15 | ~spl63_22 | ~spl63_42 | ~spl63_64)),
% 0.50/0.44 inference(forward_subsumption_resolution,[],[f2800,f2324])).
% 0.50/0.44 thf(f2802,plain,(
% 0.50/0.44 ~spl63_29 | ~spl63_9 | ~spl63_15 | ~spl63_22 | ~spl63_42 | ~spl63_64),
% 0.50/0.44 inference(avatar_split_clause,[],[f2801,f2552,f2450,f2357,f2323,f2295,f2387])).
% 0.50/0.44 thf(f2816,plain,(
% 0.50/0.44 ($true = ((ord_less @ extended_ereal @ sK10 @ extend1396239628finity @ extended_ereal))) | (~spl63_8 | ~spl63_31)),
% 0.50/0.44 inference(superposition,[],[f2399,f2292])).
% 0.50/0.44 thf(f2825,definition,(
% 0.50/0.44 spl63_88 <=> ($true = ((ord_less @ extended_ereal @ sK10 @ extend1396239628finity @ extended_ereal)))),
% 0.50/0.44 introduced(definition,[new_symbols(definition,[spl63_88])],[avatar_definition])).
% 0.50/0.44 thf(f2827,plain,(
% 0.50/0.44 ($true = ((ord_less @ extended_ereal @ sK10 @ extend1396239628finity @ extended_ereal))) | ~spl63_88),
% 0.50/0.44 inference(avatar_component_clause,[],[f2825])).
% 0.50/0.45 thf(f2828,plain,(
% 0.50/0.45 spl63_88 | ~spl63_8 | ~spl63_31),
% 0.50/0.45 inference(avatar_split_clause,[],[f2816,f2397,f2291,f2825])).
% 0.50/0.45 thf(f2869,plain,(
% 0.50/0.45 ( ! [X3 : extended_ereal] : (($true != ((ord_less @ extended_ereal @ X3 @ extend1396239628finity @ extended_ereal))) | ($true = ((topolo1751647064n_open @ a @ (sK60 @ X3))))) ) | (~spl63_8 | ~spl63_23)),
% 0.50/0.45 inference(forward_demodulation,[],[f2362,f2292])).
% 0.50/0.45 thf(f2891,plain,(
% 0.50/0.45 ( ! [X3 : extended_ereal] : (($true = ((member @ a @ x0 @ (sK60 @ X3)))) | ($true != ((ord_less @ extended_ereal @ X3 @ extend1396239628finity @ extended_ereal)))) ) | (~spl63_8 | ~spl63_71)),
% 0.50/0.45 inference(forward_demodulation,[],[f2585,f2292])).
% 0.50/0.45 thf(f2893,plain,(
% 0.50/0.45 ( ! [X3 : extended_ereal,X5 : a] : ((((member @ a @ X5 @ (sK60 @ X3))) != $true) | (((ord_less @ extended_ereal @ X3 @ (f @ X5))) = $true) | ($true != ((ord_less @ extended_ereal @ X3 @ extend1396239628finity @ extended_ereal)))) ) | (~spl63_8 | ~spl63_66)),
% 0.50/0.45 inference(forward_demodulation,[],[f2562,f2292])).
% 0.50/0.45 thf(f2897,plain,(
% 0.50/0.45 ( ! [X0 : extended_ereal] : ((((member @ a @ x0 @ (sK60 @ X0))) != $true) | ($true != $true) | (((ord_less @ extended_ereal @ X0 @ (f @ (sK11 @ (sK60 @ X0))))) = $true) | ($true != ((topolo1751647064n_open @ a @ (sK60 @ X0)))) | (((ord_less @ extended_ereal @ X0 @ extend1396239628finity @ extended_ereal)) != $true)) ) | (~spl63_8 | ~spl63_53 | ~spl63_66)),
% 0.50/0.45 inference(superposition,[],[f2893,f2499])).
% 0.50/0.45 thf(f2902,plain,(
% 0.50/0.45 ( ! [X0 : extended_ereal] : ((((member @ a @ x0 @ (sK60 @ X0))) != $true) | (((ord_less @ extended_ereal @ X0 @ extend1396239628finity @ extended_ereal)) != $true) | ($true != ((topolo1751647064n_open @ a @ (sK60 @ X0)))) | (((ord_less @ extended_ereal @ X0 @ (f @ (sK11 @ (sK60 @ X0))))) = $true)) ) | (~spl63_8 | ~spl63_53 | ~spl63_66)),
% 0.50/0.45 inference(trivial_inequality_removal,[],[f2897])).
% 0.50/0.45 thf(f2906,plain,(
% 0.50/0.45 ( ! [X0 : extended_ereal] : (($true != ((topolo1751647064n_open @ a @ (sK60 @ X0)))) | (((ord_less @ extended_ereal @ X0 @ extend1396239628finity @ extended_ereal)) != $true) | (((ord_less @ extended_ereal @ X0 @ (f @ (sK11 @ (sK60 @ X0))))) = $true)) ) | (~spl63_8 | ~spl63_53 | ~spl63_66 | ~spl63_71)),
% 0.50/0.45 inference(forward_subsumption_resolution,[],[f2902,f2891])).
% 0.50/0.45 thf(f2909,plain,(
% 0.50/0.45 ( ! [X0 : extended_ereal] : ((((ord_less @ extended_ereal @ X0 @ (f @ (sK11 @ (sK60 @ X0))))) = $true) | (((ord_less @ extended_ereal @ X0 @ extend1396239628finity @ extended_ereal)) != $true)) ) | (~spl63_8 | ~spl63_23 | ~spl63_53 | ~spl63_66 | ~spl63_71)),
% 0.50/0.45 inference(forward_subsumption_resolution,[],[f2906,f2869])).
% 0.50/0.45 thf(f2910,plain,(
% 0.50/0.45 (((member @ a @ x0 @ (sK60 @ sK10))) != $true) | ($true != $true) | ($true != ((topolo1751647064n_open @ a @ (sK60 @ sK10)))) | ($true != ((ord_less @ extended_ereal @ sK10 @ extend1396239628finity @ extended_ereal))) | (~spl63_8 | ~spl63_23 | ~spl63_27 | ~spl63_53 | ~spl63_66 | ~spl63_71)),
% 0.50/0.45 inference(superposition,[],[f2380,f2909])).
% 0.50/0.45 thf(f2913,plain,(
% 0.50/0.45 (((member @ a @ x0 @ (sK60 @ sK10))) != $true) | ($true != ((ord_less @ extended_ereal @ sK10 @ extend1396239628finity @ extended_ereal))) | ($true != ((topolo1751647064n_open @ a @ (sK60 @ sK10)))) | (~spl63_8 | ~spl63_23 | ~spl63_27 | ~spl63_53 | ~spl63_66 | ~spl63_71)),
% 0.50/0.45 inference(trivial_inequality_removal,[],[f2910])).
% 0.50/0.45 thf(f2914,plain,(
% 0.50/0.45 ($true != ((topolo1751647064n_open @ a @ (sK60 @ sK10)))) | ($true != ((ord_less @ extended_ereal @ sK10 @ extend1396239628finity @ extended_ereal))) | (~spl63_8 | ~spl63_23 | ~spl63_27 | ~spl63_53 | ~spl63_66 | ~spl63_71)),
% 0.50/0.45 inference(forward_subsumption_resolution,[],[f2913,f2891])).
% 0.50/0.45 thf(f2915,plain,(
% 0.50/0.45 ($true != ((ord_less @ extended_ereal @ sK10 @ extend1396239628finity @ extended_ereal))) | (~spl63_8 | ~spl63_23 | ~spl63_27 | ~spl63_53 | ~spl63_66 | ~spl63_71)),
% 0.50/0.45 inference(forward_subsumption_resolution,[],[f2914,f2869])).
% 0.50/0.45 thf(f2916,plain,(
% 0.50/0.45 $false | (~spl63_8 | ~spl63_23 | ~spl63_27 | ~spl63_53 | ~spl63_66 | ~spl63_71 | ~spl63_88)),
% 0.50/0.45 inference(forward_subsumption_resolution,[],[f2915,f2827])).
% 0.50/0.45 thf(f2917,plain,(
% 0.50/0.45 ~spl63_8 | ~spl63_23 | ~spl63_27 | ~spl63_53 | ~spl63_66 | ~spl63_71 | ~spl63_88),
% 0.50/0.45 inference(avatar_contradiction_clause,[],[f2916])).
% 0.50/0.45 thf(f2960,plain,(
% 0.50/0.45 ( ! [X0 : extended_ereal] : (($true != ((topolo1751647064n_open @ a @ (sK21 @ X0)))) | ($true != $true) | ($true != ((member @ a @ x0 @ (sK21 @ X0)))) | ($true = ((ord_less @ extended_ereal @ X0 @ (f @ (sK11 @ (sK21 @ X0)))))) | (((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true)) ) | (~spl63_24 | ~spl63_53)),
% 0.50/0.45 inference(superposition,[],[f2366,f2499])).
% 0.50/0.45 thf(f2964,plain,(
% 0.50/0.45 ( ! [X0 : extended_ereal] : ((((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true) | ($true != ((member @ a @ x0 @ (sK21 @ X0)))) | ($true != ((topolo1751647064n_open @ a @ (sK21 @ X0)))) | ($true = ((ord_less @ extended_ereal @ X0 @ (f @ (sK11 @ (sK21 @ X0))))))) ) | (~spl63_24 | ~spl63_53)),
% 0.50/0.45 inference(trivial_inequality_removal,[],[f2960])).
% 0.50/0.45 thf(f2967,plain,(
% 0.50/0.45 ( ! [X0 : extended_ereal] : (($true != ((member @ a @ x0 @ (sK21 @ X0)))) | ($true = ((ord_less @ extended_ereal @ X0 @ (f @ (sK11 @ (sK21 @ X0)))))) | (((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true)) ) | (~spl63_24 | ~spl63_50 | ~spl63_53)),
% 0.50/0.45 inference(forward_subsumption_resolution,[],[f2964,f2485])).
% 0.50/0.45 thf(f2970,plain,(
% 0.50/0.45 ( ! [X0 : extended_ereal] : (($true = ((ord_less @ extended_ereal @ X0 @ (f @ (sK11 @ (sK21 @ X0)))))) | (((ord_less @ extended_ereal @ X0 @ (f @ x0))) != $true)) ) | (~spl63_24 | ~spl63_33 | ~spl63_50 | ~spl63_53)),
% 0.50/0.45 inference(forward_subsumption_resolution,[],[f2967,f2408])).
% 0.50/0.45 thf(f2985,plain,(
% 0.50/0.45 ($true != ((ord_less @ extended_ereal @ sK10 @ (f @ x0)))) | ($true != ((member @ a @ x0 @ (sK21 @ sK10)))) | (((topolo1751647064n_open @ a @ (sK21 @ sK10))) != $true) | ($true != $true) | (~spl63_24 | ~spl63_27 | ~spl63_33 | ~spl63_50 | ~spl63_53)),
% 0.50/0.45 inference(superposition,[],[f2380,f2970])).
% 0.50/0.45 thf(f2988,plain,(
% 0.50/0.45 ($true != ((member @ a @ x0 @ (sK21 @ sK10)))) | (((topolo1751647064n_open @ a @ (sK21 @ sK10))) != $true) | ($true != ((ord_less @ extended_ereal @ sK10 @ (f @ x0)))) | (~spl63_24 | ~spl63_27 | ~spl63_33 | ~spl63_50 | ~spl63_53)),
% 0.50/0.45 inference(trivial_inequality_removal,[],[f2985])).
% 0.50/0.45 thf(f2989,plain,(
% 0.50/0.45 ($true != ((ord_less @ extended_ereal @ sK10 @ (f @ x0)))) | (((topolo1751647064n_open @ a @ (sK21 @ sK10))) != $true) | (~spl63_24 | ~spl63_27 | ~spl63_33 | ~spl63_50 | ~spl63_53)),
% 0.50/0.45 inference(forward_subsumption_resolution,[],[f2988,f2408])).
% 0.50/0.45 thf(f2990,plain,(
% 0.50/0.45 ($true != ((ord_less @ extended_ereal @ sK10 @ (f @ x0)))) | (~spl63_24 | ~spl63_27 | ~spl63_33 | ~spl63_50 | ~spl63_53)),
% 0.50/0.45 inference(forward_subsumption_resolution,[],[f2989,f2485])).
% 0.50/0.45 thf(f2991,plain,(
% 0.50/0.45 $false | (~spl63_24 | ~spl63_27 | ~spl63_31 | ~spl63_33 | ~spl63_50 | ~spl63_53)),
% 0.50/0.45 inference(forward_subsumption_resolution,[],[f2990,f2399])).
% 0.50/0.45 thf(f2992,plain,(
% 0.50/0.45 ~spl63_24 | ~spl63_27 | ~spl63_31 | ~spl63_33 | ~spl63_50 | ~spl63_53),
% 0.50/0.45 inference(avatar_contradiction_clause,[],[f2991])).
% 0.50/0.45 thf(f2999,plain,(
% 0.50/0.45 ($true = ((ord_less @ extended_ereal @ sK10 @ (uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal)))) | (~spl63_7 | ~spl63_31)),
% 0.50/0.45 inference(superposition,[],[f2399,f2287])).
% 0.50/0.45 thf(f3004,definition,(
% 0.50/0.45 spl63_98 <=> ($true = ((ord_less @ extended_ereal @ sK10 @ (uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))))),
% 0.50/0.45 introduced(definition,[new_symbols(definition,[spl63_98])],[avatar_definition])).
% 0.50/0.45 thf(f3006,plain,(
% 0.50/0.45 ($true = ((ord_less @ extended_ereal @ sK10 @ (uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal)))) | ~spl63_98),
% 0.50/0.45 inference(avatar_component_clause,[],[f3004])).
% 0.50/0.45 thf(f3007,plain,(
% 0.50/0.45 spl63_98 | ~spl63_7 | ~spl63_31),
% 0.50/0.45 inference(avatar_split_clause,[],[f2999,f2397,f2286,f3004])).
% 0.50/0.45 thf(f3008,plain,(
% 0.50/0.45 ( ! [X0 : extended_ereal] : ((((ord_less @ extended_ereal @ X0 @ (uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) != $true) | (((topolo1751647064n_open @ a @ (sK37 @ X0))) = $true)) ) | (~spl63_7 | ~spl63_28)),
% 0.50/0.45 inference(forward_demodulation,[],[f2384,f2287])).
% 0.50/0.45 thf(f3016,plain,(
% 0.50/0.45 ( ! [X0 : extended_ereal] : ((((member @ a @ x0 @ (sK37 @ X0))) = $true) | (((ord_less @ extended_ereal @ X0 @ (uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) != $true)) ) | (~spl63_7 | ~spl63_10)),
% 0.50/0.45 inference(forward_demodulation,[],[f2300,f2287])).
% 0.50/0.45 thf(f3017,plain,(
% 0.50/0.45 ( ! [X2 : a,X0 : extended_ereal] : ((((member @ a @ X2 @ (sK37 @ X0))) != $true) | (((ord_less @ extended_ereal @ X0 @ (uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) != $true) | (((ord_less @ extended_ereal @ X0 @ (f @ X2))) = $true)) ) | (~spl63_6 | ~spl63_7)),
% 0.50/0.45 inference(forward_demodulation,[],[f2284,f2287])).
% 0.50/0.45 thf(f3021,plain,(
% 0.50/0.45 ( ! [X0 : extended_ereal] : ((((member @ a @ x0 @ (sK37 @ X0))) != $true) | (((topolo1751647064n_open @ a @ (sK37 @ X0))) != $true) | ($true != $true) | ($true = ((ord_less @ extended_ereal @ X0 @ (f @ (sK11 @ (sK37 @ X0)))))) | (((ord_less @ extended_ereal @ X0 @ (uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) != $true)) ) | (~spl63_6 | ~spl63_7 | ~spl63_53)),
% 0.50/0.45 inference(superposition,[],[f3017,f2499])).
% 0.50/0.45 thf(f3026,plain,(
% 0.50/0.45 ( ! [X0 : extended_ereal] : ((((topolo1751647064n_open @ a @ (sK37 @ X0))) != $true) | ($true = ((ord_less @ extended_ereal @ X0 @ (f @ (sK11 @ (sK37 @ X0)))))) | (((ord_less @ extended_ereal @ X0 @ (uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) != $true) | (((member @ a @ x0 @ (sK37 @ X0))) != $true)) ) | (~spl63_6 | ~spl63_7 | ~spl63_53)),
% 0.50/0.45 inference(trivial_inequality_removal,[],[f3021])).
% 0.50/0.45 thf(f3030,plain,(
% 0.50/0.45 ( ! [X0 : extended_ereal] : ((((member @ a @ x0 @ (sK37 @ X0))) != $true) | (((ord_less @ extended_ereal @ X0 @ (uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) != $true) | ($true = ((ord_less @ extended_ereal @ X0 @ (f @ (sK11 @ (sK37 @ X0))))))) ) | (~spl63_6 | ~spl63_7 | ~spl63_28 | ~spl63_53)),
% 0.50/0.45 inference(forward_subsumption_resolution,[],[f3026,f3008])).
% 0.50/0.45 thf(f3033,plain,(
% 0.50/0.45 ( ! [X0 : extended_ereal] : (($true = ((ord_less @ extended_ereal @ X0 @ (f @ (sK11 @ (sK37 @ X0)))))) | (((ord_less @ extended_ereal @ X0 @ (uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) != $true)) ) | (~spl63_6 | ~spl63_7 | ~spl63_10 | ~spl63_28 | ~spl63_53)),
% 0.50/0.45 inference(forward_subsumption_resolution,[],[f3030,f3016])).
% 0.50/0.45 thf(f3046,plain,(
% 0.50/0.45 ($true != ((member @ a @ x0 @ (sK37 @ sK10)))) | ($true != ((topolo1751647064n_open @ a @ (sK37 @ sK10)))) | ($true != ((ord_less @ extended_ereal @ sK10 @ (uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal)))) | ($true != $true) | (~spl63_6 | ~spl63_7 | ~spl63_10 | ~spl63_27 | ~spl63_28 | ~spl63_53)),
% 0.50/0.45 inference(superposition,[],[f2380,f3033])).
% 0.50/0.45 thf(f3049,plain,(
% 0.50/0.45 ($true != ((topolo1751647064n_open @ a @ (sK37 @ sK10)))) | ($true != ((member @ a @ x0 @ (sK37 @ sK10)))) | ($true != ((ord_less @ extended_ereal @ sK10 @ (uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal)))) | (~spl63_6 | ~spl63_7 | ~spl63_10 | ~spl63_27 | ~spl63_28 | ~spl63_53)),
% 0.50/0.45 inference(trivial_inequality_removal,[],[f3046])).
% 0.50/0.45 thf(f3050,plain,(
% 0.50/0.45 ($true != ((ord_less @ extended_ereal @ sK10 @ (uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal)))) | ($true != ((member @ a @ x0 @ (sK37 @ sK10)))) | (~spl63_6 | ~spl63_7 | ~spl63_10 | ~spl63_27 | ~spl63_28 | ~spl63_53)),
% 0.50/0.45 inference(forward_subsumption_resolution,[],[f3049,f3008])).
% 0.50/0.45 thf(f3051,plain,(
% 0.50/0.45 ($true != ((ord_less @ extended_ereal @ sK10 @ (uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal)))) | (~spl63_6 | ~spl63_7 | ~spl63_10 | ~spl63_27 | ~spl63_28 | ~spl63_53)),
% 0.50/0.45 inference(forward_subsumption_resolution,[],[f3050,f3016])).
% 0.50/0.45 thf(f3052,plain,(
% 0.50/0.45 $false | (~spl63_6 | ~spl63_7 | ~spl63_10 | ~spl63_27 | ~spl63_28 | ~spl63_53 | ~spl63_98)),
% 0.50/0.45 inference(forward_subsumption_resolution,[],[f3051,f3006])).
% 0.50/0.45 thf(f3053,plain,(
% 0.50/0.45 ~spl63_6 | ~spl63_7 | ~spl63_10 | ~spl63_27 | ~spl63_28 | ~spl63_53 | ~spl63_98),
% 0.50/0.45 inference(avatar_contradiction_clause,[],[f3052])).
% 0.50/0.45 cnf(s5, plain, ~spl63_5 | spl63_6 | ~spl63_7, inference(sat_conversion,[],[f2289])).
% 0.50/0.45 cnf(s6, plain, spl63_5 | ~spl63_8 | spl63_9, inference(sat_conversion,[],[f2297])).
% 0.50/0.45 cnf(s7, plain, ~spl63_5 | ~spl63_7 | spl63_10, inference(sat_conversion,[],[f2301])).
% 0.50/0.45 cnf(s12, plain, spl63_5 | spl63_15, inference(sat_conversion,[],[f2325])).
% 0.50/0.45 cnf(s19, plain, spl63_5 | spl63_22, inference(sat_conversion,[],[f2359])).
% 0.50/0.45 cnf(s20, plain, ~spl63_5 | ~spl63_8 | spl63_23, inference(sat_conversion,[],[f2363])).
% 0.50/0.45 cnf(s21, plain, ~spl63_5 | spl63_7 | spl63_8 | spl63_24, inference(sat_conversion,[],[f2367])).
% 0.50/0.45 cnf(s24, plain, ~spl63_5 | spl63_27, inference(sat_conversion,[],[f2381])).
% 0.50/0.45 cnf(s25, plain, ~spl63_5 | ~spl63_7 | spl63_28, inference(sat_conversion,[],[f2385])).
% 0.50/0.45 cnf(s26, plain, spl63_5 | ~spl63_8 | spl63_29, inference(sat_conversion,[],[f2390])).
% 0.50/0.45 cnf(s28, plain, ~spl63_5 | spl63_31, inference(sat_conversion,[],[f2400])).
% 0.50/0.45 cnf(s30, plain, ~spl63_5 | spl63_7 | spl63_8 | spl63_33, inference(sat_conversion,[],[f2409])).
% 0.50/0.45 cnf(s33, plain, spl63_5 | spl63_7 | spl63_8 | spl63_36, inference(sat_conversion,[],[f2423])).
% 0.50/0.45 cnf(s39, plain, spl63_5 | ~spl63_8 | spl63_42, inference(sat_conversion,[],[f2452])).
% 0.50/0.45 cnf(s42, plain, spl63_5 | ~spl63_7 | spl63_46, inference(sat_conversion,[],[f2468])).
% 0.50/0.45 cnf(s45, plain, spl63_5 | spl63_7 | spl63_8 | spl63_49, inference(sat_conversion,[],[f2482])).
% 0.50/0.45 cnf(s46, plain, ~spl63_5 | spl63_7 | spl63_8 | spl63_50, inference(sat_conversion,[],[f2486])).
% 0.50/0.45 cnf(s50, plain, ~spl63_5 | spl63_53, inference(sat_conversion,[],[f2500])).
% 0.50/0.45 cnf(s53, plain, spl63_5 | spl63_7 | spl63_8 | spl63_56, inference(sat_conversion,[],[f2515])).
% 0.50/0.45 cnf(s58, plain, spl63_5 | ~spl63_7 | spl63_61, inference(sat_conversion,[],[f2540])).
% 0.50/0.45 cnf(s61, plain, spl63_5 | spl63_64, inference(sat_conversion,[],[f2554])).
% 0.50/0.45 cnf(s63, plain, ~spl63_5 | ~spl63_8 | spl63_66, inference(sat_conversion,[],[f2563])).
% 0.50/0.45 cnf(s64, plain, spl63_5 | ~spl63_7 | spl63_67, inference(sat_conversion,[],[f2567])).
% 0.50/0.45 cnf(s68, plain, ~spl63_5 | ~spl63_8 | spl63_71, inference(sat_conversion,[],[f2586])).
% 0.50/0.45 cnf(s75, plain, ~spl63_15 | ~spl63_22 | ~spl63_36 | ~spl63_49 | ~spl63_56 | ~spl63_64, inference(sat_conversion,[],[f2645])).
% 0.50/0.45 cnf(s77, plain, ~spl63_7 | ~spl63_61 | spl63_77, inference(sat_conversion,[],[f2659])).
% 0.50/0.45 cnf(s80, plain, ~spl63_7 | ~spl63_15 | ~spl63_22 | ~spl63_46 | ~spl63_64 | ~spl63_67 | ~spl63_77 | ~spl63_81, inference(sat_conversion,[],[f2750])).
% 0.50/0.45 cnf(s84, plain, ~spl63_7 | ~spl63_64 | ~spl63_77 | spl63_81, inference(sat_conversion,[],[f2795])).
% 0.50/0.45 cnf(s85, plain, ~spl63_9 | ~spl63_15 | ~spl63_22 | ~spl63_29 | ~spl63_42 | ~spl63_64, inference(sat_conversion,[],[f2802])).
% 0.50/0.45 cnf(s88, plain, ~spl63_8 | ~spl63_31 | spl63_88, inference(sat_conversion,[],[f2828])).
% 0.50/0.45 cnf(s96, plain, ~spl63_8 | ~spl63_23 | ~spl63_27 | ~spl63_53 | ~spl63_66 | ~spl63_71 | ~spl63_88, inference(sat_conversion,[],[f2917])).
% 0.50/0.45 cnf(s102, plain, ~spl63_24 | ~spl63_27 | ~spl63_31 | ~spl63_33 | ~spl63_50 | ~spl63_53, inference(sat_conversion,[],[f2992])).
% 0.50/0.45 cnf(s105, plain, ~spl63_7 | ~spl63_31 | spl63_98, inference(sat_conversion,[],[f3007])).
% 0.50/0.45 cnf(s108, plain, ~spl63_6 | ~spl63_7 | ~spl63_10 | ~spl63_27 | ~spl63_28 | ~spl63_53 | ~spl63_98, inference(sat_conversion,[],[f3053])).
% 0.50/0.45 cnf(s109, plain, spl63_8 | spl63_7 | spl63_5, inference(rat,[],[s75,s33,s45,s53,s61,s19,s12])).
% 0.50/0.45 cnf(s110, plain, ~spl63_8 | spl63_5, inference(rat,[],[s85,s6,s26,s39,s61,s19,s12])).
% 0.50/0.45 cnf(s111, plain, spl63_5, inference(rat,[],[s80,s84,s77,s42,s58,s64,s109,s110,s12,s19,s61])).
% 0.50/0.45 cnf(s112, plain, spl63_53, inference(rat,[],[s50,s111])).
% 0.50/0.45 cnf(s113, plain, spl63_31, inference(rat,[],[s28,s111])).
% 0.50/0.45 cnf(s114, plain, spl63_27, inference(rat,[],[s24,s111])).
% 0.50/0.45 cnf(s115, plain, spl63_8 | spl63_7, inference(rat,[],[s102,s30,s46,s21,s111,s112,s114,s113])).
% 0.50/0.45 cnf(s116, plain, ~spl63_8, inference(rat,[],[s96,s88,s20,s63,s68,s114,s112,s113,s111])).
% 0.50/0.45 cnf(s117, plain, spl63_7, inference(rat,[],[s115,s116])).
% 0.50/0.45 cnf(s118, plain, spl63_28, inference(rat,[],[s25,s111,s117])).
% 0.50/0.45 cnf(s119, plain, spl63_10, inference(rat,[],[s7,s111,s117])).
% 0.50/0.45 cnf(s120, plain, spl63_6, inference(rat,[],[s5,s111,s117])).
% 0.50/0.45 cnf(s121, plain, spl63_98, inference(rat,[],[s105,s113,s117])).
% 0.50/0.45 cnf(s122, plain, $false, inference(rat,[],[s108,s121,s112,s117,s114,s120,s118,s119])).
% 0.50/0.45 thf(f3054,plain,(
% 0.50/0.45 $false),
% 0.50/0.45 inference(avatar_sat_refutation,[],[s122])).
% 0.50/0.45 % SZS output end Proof for theBenchmark
% 0.50/0.45 % (2982342)------------------------------
% 0.50/0.45 % (2982342)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.50/0.45 % (2982342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/0.45 % (2982342)CaDiCaL version: 2.1.3
% 0.50/0.45 % (2982342)Termination reason: Refutation
% 0.50/0.45 % (2982342)Time elapsed: 0.106 s
% 0.50/0.45 % (2982342)Peak memory usage: 15 MB
% 0.50/0.45 % (2982342)Instructions burned: 211 (million)
% 0.50/0.45 % (2982334)Success in time 0.162 s
% 0.50/0.45 % Vampire exiting
%------------------------------------------------------------------------------