%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP149^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n013.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:33 AM UTC 2026
% Result : Theorem 0.51s 0.44s
% Output : Refutation 0.51s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP149^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n013.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Tue Sep 29 20:01:33 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.20/0.28 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.51/0.41 % (2589288)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.51/0.41 % (2589298)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=1106470469:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.51/0.41 % (2589299)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.51/0.41 % (2589299)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.51/0.41 % (2589293)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=1240089015:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.51/0.41 % (2589295)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=4186223828:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.51/0.41 % (2589297)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=2996420918:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.51/0.41 % (2589296)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=1807038091: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.51/0.41 % (2589299)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=555719137:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.51/0.41 % (2589295)Instruction limit reached!
% 0.51/0.41 % (2589295)------------------------------
% 0.51/0.41 % (2589295)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.51/0.41 % (2589295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.51/0.41 % (2589295)CaDiCaL version: 2.1.3
% 0.51/0.41 % (2589295)Termination reason: Instruction limit
% 0.51/0.41 % (2589295)Termination phase: shuffling
% 0.51/0.41 % (2589295)Time elapsed: 0.002 s
% 0.51/0.41 % (2589295)Peak memory usage: 10 MB
% 0.51/0.41 % (2589295)Instructions burned: 3 (million)
% 0.51/0.41 % (2589294)lrs+10_16_si=on:nwc=1.5:random_seed=1380290288:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.51/0.41 % (2589297)Instruction limit reached!
% 0.51/0.41 % (2589297)------------------------------
% 0.51/0.41 % (2589297)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.51/0.41 % (2589297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.51/0.41 % (2589297)CaDiCaL version: 2.1.3
% 0.51/0.41 % (2589297)Termination reason: Instruction limit
% 0.51/0.41 % (2589297)Termination phase: Property scanning
% 0.51/0.41 % (2589297)Time elapsed: 0.011 s
% 0.51/0.41 % (2589297)Peak memory usage: 10 MB
% 0.51/0.41 % (2589297)Instructions burned: 26 (million)
% 0.51/0.41 % (2589298)Instruction limit reached!
% 0.51/0.41 % (2589298)------------------------------
% 0.51/0.41 % (2589298)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.51/0.41 % (2589298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.51/0.41 % (2589298)CaDiCaL version: 2.1.3
% 0.51/0.41 % (2589298)Termination reason: Instruction limit
% 0.51/0.41 % (2589298)Termination phase: Function definition elimination
% 0.51/0.41 % (2589298)Time elapsed: 0.019 s
% 0.51/0.41 % (2589298)Peak memory usage: 11 MB
% 0.51/0.41 % (2589298)Instructions burned: 79 (million)
% 0.51/0.41 % (2589294)Instruction limit reached!
% 0.51/0.41 % (2589294)------------------------------
% 0.51/0.41 % (2589294)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.51/0.41 % (2589294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.51/0.41 % (2589294)CaDiCaL version: 2.1.3
% 0.51/0.41 % (2589294)Termination reason: Instruction limit
% 0.51/0.41 % (2589294)Termination phase: shuffling
% 0.51/0.41 % (2589294)Time elapsed: 0.008 s
% 0.51/0.41 % (2589294)Peak memory usage: 10 MB
% 0.51/0.41 % (2589294)Instructions burned: 18 (million)
% 0.51/0.41 % (2589306)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3644379367:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.51/0.41 % (2589308)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=3649734948:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.51/0.44 % (2589308)Instruction limit reached!
% 0.51/0.44 % (2589308)------------------------------
% 0.51/0.44 % (2589308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.51/0.44 % (2589308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.51/0.44 % (2589308)CaDiCaL version: 2.1.3
% 0.51/0.44 % (2589308)Termination reason: Instruction limit
% 0.51/0.44 % (2589308)Termination phase: shuffling
% 0.51/0.44 % (2589308)Time elapsed: 0.001 s
% 0.51/0.44 % (2589308)Peak memory usage: 10 MB
% 0.51/0.44 % (2589308)Instructions burned: 6 (million)
% 0.51/0.44 % (2589306)Instruction limit reached!
% 0.51/0.44 % (2589306)------------------------------
% 0.51/0.44 % (2589306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.51/0.44 % (2589306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.51/0.44 % (2589306)CaDiCaL version: 2.1.3
% 0.51/0.44 % (2589306)Termination reason: Instruction limit
% 0.51/0.44 % (2589306)Termination phase: shuffling
% 0.51/0.44 % (2589306)Time elapsed: 0.002 s
% 0.51/0.44 % (2589306)Peak memory usage: 10 MB
% 0.51/0.44 % (2589306)Instructions burned: 2 (million)
% 0.51/0.44 % (2589309)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.51/0.44 % (2589309)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1417583667:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.51/0.44 % (2589310)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=3379865532:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.51/0.44 % (2589313)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.51/0.44 % (2589313)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.51/0.44 % (2589309)Instruction limit reached!
% 0.51/0.44 % (2589309)------------------------------
% 0.51/0.44 % (2589309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.51/0.44 % (2589309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.51/0.44 % (2589309)CaDiCaL version: 2.1.3
% 0.51/0.44 % (2589309)Termination reason: Instruction limit
% 0.51/0.44 % (2589309)Termination phase: shuffling
% 0.51/0.44 % (2589309)Time elapsed: 0.004 s
% 0.51/0.44 % (2589309)Peak memory usage: 10 MB
% 0.51/0.44 % (2589309)Instructions burned: 9 (million)
% 0.51/0.44 % (2589313)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=981680811: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.51/0.44 % (2589293)Instruction limit reached!
% 0.51/0.44 % (2589293)------------------------------
% 0.51/0.44 % (2589293)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.51/0.44 % (2589293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.51/0.44 % (2589293)CaDiCaL version: 2.1.3
% 0.51/0.44 % (2589293)Termination reason: Instruction limit
% 0.51/0.44 % (2589293)Termination phase: Property scanning
% 0.51/0.44 % (2589293)Time elapsed: 0.039 s
% 0.51/0.44 % (2589293)Peak memory usage: 12 MB
% 0.51/0.44 % (2589293)Instructions burned: 89 (million)
% 0.51/0.44 % (2589310)Instruction limit reached!
% 0.51/0.44 % (2589310)------------------------------
% 0.51/0.44 % (2589310)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.51/0.44 % (2589310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.51/0.44 % (2589310)CaDiCaL version: 2.1.3
% 0.51/0.44 % (2589310)Termination reason: Instruction limit
% 0.51/0.44 % (2589310)Termination phase: shuffling
% 0.51/0.44 % (2589310)Time elapsed: 0.006 s
% 0.51/0.44 % (2589310)Peak memory usage: 10 MB
% 0.51/0.44 % (2589310)Instructions burned: 14 (million)
% 0.51/0.44 % (2589313)Instruction limit reached!
% 0.51/0.44 % (2589313)------------------------------
% 0.51/0.44 % (2589313)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.51/0.44 % (2589313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.51/0.44 % (2589313)CaDiCaL version: 2.1.3
% 0.51/0.44 % (2589313)Termination reason: Instruction limit
% 0.51/0.44 % (2589313)Termination phase: shuffling
% 0.51/0.44 % (2589313)Time elapsed: 0.007 s
% 0.51/0.44 % (2589313)Peak memory usage: 10 MB
% 0.51/0.44 % (2589313)Instructions burned: 32 (million)
% 0.51/0.44 % (2589314)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=2174698817:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.51/0.44 % (2589319)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.51/0.44 % (2589321)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=2098417776:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.51/0.44 % (2589318)lrs+10_1_si=on:cs=on:random_seed=571451573:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.51/0.44 % (2589320)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=4202176955:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.51/0.44 % (2589319)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=2632548457:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.51/0.44 % (2589318)Instruction limit reached!
% 0.51/0.44 % (2589318)------------------------------
% 0.51/0.44 % (2589318)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.51/0.44 % (2589318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.51/0.44 % (2589318)CaDiCaL version: 2.1.3
% 0.51/0.44 % (2589318)Termination reason: Instruction limit
% 0.51/0.44 % (2589318)Termination phase: shuffling
% 0.51/0.44 % (2589318)Time elapsed: 0.004 s
% 0.51/0.44 % (2589318)Peak memory usage: 10 MB
% 0.51/0.44 % (2589318)Instructions burned: 9 (million)
% 0.51/0.44 % (2589319)Instruction limit reached!
% 0.51/0.44 % (2589319)------------------------------
% 0.51/0.44 % (2589319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.51/0.44 % (2589319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.51/0.44 % (2589319)CaDiCaL version: 2.1.3
% 0.51/0.44 % (2589319)Termination reason: Instruction limit
% 0.51/0.44 % (2589319)Termination phase: shuffling
% 0.51/0.44 % (2589319)Time elapsed: 0.002 s
% 0.51/0.44 % (2589319)Peak memory usage: 10 MB
% 0.51/0.44 % (2589319)Instructions burned: 4 (million)
% 0.51/0.44 % (2589299)Instruction limit reached!
% 0.51/0.44 % (2589299)------------------------------
% 0.51/0.44 % (2589299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.51/0.44 % (2589299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.51/0.44 % (2589299)CaDiCaL version: 2.1.3
% 0.51/0.44 % (2589299)Termination reason: Instruction limit
% 0.51/0.44 % (2589299)Termination phase: Saturation
% 0.51/0.44 % (2589299)Time elapsed: 0.069 s
% 0.51/0.44 % (2589299)Peak memory usage: 13 MB
% 0.51/0.44 % (2589299)Instructions burned: 159 (million)
% 0.51/0.44 % (2589320)Instruction limit reached!
% 0.51/0.44 % (2589320)------------------------------
% 0.51/0.44 % (2589320)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.51/0.44 % (2589320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.51/0.44 % (2589320)CaDiCaL version: 2.1.3
% 0.51/0.44 % (2589320)Termination reason: Instruction limit
% 0.51/0.44 % (2589320)Termination phase: SInE selection
% 0.51/0.44 % (2589320)Time elapsed: 0.017 s
% 0.51/0.44 % (2589320)Peak memory usage: 11 MB
% 0.51/0.44 % (2589320)Instructions burned: 38 (million)
% 0.51/0.44 % (2589327)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=1790284602:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 0.51/0.44 % (2589328)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=1943339063:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 0.51/0.44 % (2589314)Instruction limit reached!
% 0.51/0.44 % (2589314)------------------------------
% 0.51/0.44 % (2589314)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.51/0.44 % (2589314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.51/0.44 % (2589314)CaDiCaL version: 2.1.3
% 0.51/0.44 % (2589314)Termination reason: Instruction limit
% 0.51/0.44 % (2589314)Termination phase: Property scanning
% 0.51/0.44 % (2589314)Time elapsed: 0.036 s
% 0.51/0.44 % (2589314)Peak memory usage: 11 MB
% 0.51/0.44 % (2589314)Instructions burned: 87 (million)
% 0.51/0.44 % (2589328)Instruction limit reached!
% 0.51/0.44 % (2589328)------------------------------
% 0.51/0.44 % (2589328)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.51/0.44 % (2589328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.51/0.44 % (2589328)CaDiCaL version: 2.1.3
% 0.51/0.44 % (2589328)Termination reason: Instruction limit
% 0.51/0.44 % (2589328)Termination phase: shuffling
% 0.51/0.44 % (2589328)Time elapsed: 0.006 s
% 0.51/0.44 % (2589328)Peak memory usage: 10 MB
% 0.51/0.44 % (2589328)Instructions burned: 14 (million)
% 0.51/0.44 % (2589327)Instruction limit reached!
% 0.51/0.44 % (2589327)------------------------------
% 0.51/0.44 % (2589327)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.51/0.44 % (2589327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.51/0.44 % (2589327)CaDiCaL version: 2.1.3
% 0.51/0.44 % (2589327)Termination reason: Instruction limit
% 0.51/0.44 % (2589327)Termination phase: Property scanning
% 0.51/0.44 % (2589327)Time elapsed: 0.011 s
% 0.51/0.44 % (2589327)Peak memory usage: 10 MB
% 0.51/0.44 % (2589329)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=1472955077:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 0.51/0.44 % (2589327)Instructions burned: 25 (million)
% 0.51/0.44 % (2589330)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=221599704:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 0.51/0.44 % (2589296) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2589288-2589296"...
% 0.51/0.44 % (2589333)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=3251487521: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.51/0.44 % (2589330)Instruction limit reached!
% 0.51/0.44 % (2589330)------------------------------
% 0.51/0.44 % (2589330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.51/0.44 % (2589296)...printing done.
% 0.51/0.44 % (2589330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.51/0.44 % (2589330)CaDiCaL version: 2.1.3
% 0.51/0.44 % (2589330)Termination reason: Instruction limit
% 0.51/0.44 % (2589330)Termination phase: shuffling
% 0.51/0.44 % (2589330)Time elapsed: 0.006 s
% 0.51/0.44 % (2589330)Peak memory usage: 10 MB
% 0.51/0.44 % (2589330)Instructions burned: 14 (million)
% 0.51/0.44 % (2589296)Refutation found. Thanks to Tanya!
% 0.51/0.44 % SZS status Theorem for theBenchmark
% 0.51/0.44 % SZS output start Proof for theBenchmark
% 0.51/0.44 thf(type_def_5, type, bounde7994401a_real: $tType).
% 0.51/0.44 thf(type_def_6, type, set_set_real: $tType).
% 0.51/0.44 thf(type_def_7, type, set_set_a: $tType).
% 0.51/0.44 thf(type_def_8, type, set_real: $tType).
% 0.51/0.44 thf(type_def_9, type, set_a: $tType).
% 0.51/0.44 thf(type_def_10, type, real: $tType).
% 0.51/0.44 thf(type_def_11, type, a: $tType).
% 0.51/0.44 thf(type_def_12, type, sTfun: ($tType * $tType) > $tType).
% 0.51/0.44 thf(func_def_0, type, elemen1140313242l_real: (real > real > set_real)).
% 0.51/0.44 thf(func_def_1, type, elemen49976720ball_a: (a > real > set_a)).
% 0.51/0.44 thf(func_def_2, type, auto_l612940ivl0_a: ((a > a) > set_a > a > set_real)).
% 0.51/0.44 thf(func_def_3, type, minus_minus_real: (real > real > real)).
% 0.51/0.44 thf(func_def_4, type, minus_minus_set_real: (set_real > set_real > set_real)).
% 0.51/0.44 thf(func_def_5, type, minus_minus_set_a: (set_a > set_a > set_a)).
% 0.51/0.44 thf(func_def_6, type, minus_minus_a: (a > a > a)).
% 0.51/0.44 thf(func_def_7, type, uminus_uminus_a_a: ((a > a) > a > a)).
% 0.51/0.44 thf(func_def_8, type, uminus_uminus_real: (real > real)).
% 0.51/0.44 thf(func_def_9, type, uminus773214379t_real: (set_real > set_real)).
% 0.51/0.44 thf(func_def_10, type, uminus_uminus_set_a: (set_a > set_a)).
% 0.51/0.44 thf(func_def_11, type, uminus_uminus_a: (a > a)).
% 0.51/0.44 thf(func_def_12, type, zero_zero_real: real).
% 0.51/0.44 thf(func_def_13, type, zero_zero_a: a).
% 0.51/0.44 thf(func_def_14, type, initia826609931terval: (set_real > $o)).
% 0.51/0.44 thf(func_def_15, type, inner_4346926r_real: (real > real > real)).
% 0.51/0.44 thf(func_def_16, type, inner_1173012732nner_a: (a > a > real)).
% 0.51/0.44 thf(func_def_17, type, auto_l630715367iant_a: ((a > a) > set_a > set_a > $o)).
% 0.51/0.44 thf(func_def_18, type, line_c1152468841ment_a: (a > a > set_a)).
% 0.51/0.44 thf(func_def_19, type, line_open_segment_a: (a > a > set_a)).
% 0.51/0.44 thf(func_def_20, type, oDE_au1996717075pped_a: ((a > a) > set_a > a > set_a > $o)).
% 0.51/0.44 thf(func_def_21, type, ord_less_real: (real > real > $o)).
% 0.51/0.44 thf(func_def_22, type, ord_less_set_real: (set_real > set_real > $o)).
% 0.51/0.44 thf(func_def_23, type, ord_le861030508t_real: (set_set_real > set_set_real > $o)).
% 0.51/0.44 thf(func_def_24, type, ord_less_set_set_a: (set_set_a > set_set_a > $o)).
% 0.51/0.44 thf(func_def_25, type, ord_less_set_a: (set_a > set_a > $o)).
% 0.51/0.44 thf(func_def_26, type, ord_less_a: (a > a > $o)).
% 0.51/0.44 thf(func_def_27, type, ord_less_eq_real: (real > real > $o)).
% 0.51/0.44 thf(func_def_28, type, ord_less_eq_set_real: (set_real > set_real > $o)).
% 0.51/0.44 thf(func_def_29, type, ord_le1733505144t_real: (set_set_real > set_set_real > $o)).
% 0.51/0.44 thf(func_def_30, type, ord_le318720350_set_a: (set_set_a > set_set_a > $o)).
% 0.51/0.44 thf(func_def_31, type, ord_less_eq_set_a: (set_a > set_a > $o)).
% 0.51/0.44 thf(func_def_32, type, ord_less_eq_a: (a > a > $o)).
% 0.51/0.44 thf(func_def_33, type, top_top_set_real: set_real).
% 0.51/0.44 thf(func_def_34, type, top_top_set_a: set_a).
% 0.51/0.44 thf(func_def_35, type, period720806154rbit_a: ((a > a) > set_a > a > $o)).
% 0.51/0.44 thf(func_def_36, type, period1305449585riod_a: ((a > a) > set_a > a > real)).
% 0.51/0.44 thf(func_def_37, type, period138238489rbit_a: ((a > a) > set_a > a > $o)).
% 0.51/0.44 thf(func_def_38, type, poinca659159244_rot_a: (a > a)).
% 0.51/0.44 thf(func_def_39, type, poinca522724647ment_a: ((a > a) > set_a > a > a > $o)).
% 0.51/0.44 thf(func_def_40, type, reacha1191408304tion_a: ((a > a) > set_a > (a > real) > (a > bounde7994401a_real) > set_a > $o)).
% 0.51/0.44 thf(func_def_41, type, real_V1934908667t_real: (real > real > real)).
% 0.51/0.44 thf(func_def_42, type, real_V1514887919dist_a: (a > a > real)).
% 0.51/0.44 thf(func_def_43, type, collect_real: ((real > $o) > set_real)).
% 0.51/0.44 thf(func_def_44, type, collect_set_real: ((set_real > $o) > set_set_real)).
% 0.51/0.44 thf(func_def_45, type, collect_set_a: ((set_a > $o) > set_set_a)).
% 0.51/0.44 thf(func_def_46, type, collect_a: ((a > $o) > set_a)).
% 0.51/0.44 thf(func_def_47, type, set_or656347191t_real: (real > real > set_real)).
% 0.51/0.44 thf(func_def_48, type, set_or1619725421t_real: (set_real > set_real > set_set_real)).
% 0.51/0.44 thf(func_def_49, type, set_or2094724627_set_a: (set_a > set_a > set_set_a)).
% 0.51/0.44 thf(func_def_50, type, set_or411607219Most_a: (a > a > set_a)).
% 0.51/0.44 thf(func_def_51, type, member_real: (real > set_real > $o)).
% 0.51/0.44 thf(func_def_52, type, member_set_real: (set_real > set_set_real > $o)).
% 0.51/0.44 thf(func_def_53, type, member_set_a: (set_a > set_set_a > $o)).
% 0.51/0.44 thf(func_def_54, type, member_a: (a > set_a > $o)).
% 0.51/0.44 thf(func_def_55, type, x: set_a).
% 0.51/0.44 thf(func_def_56, type, a2: a).
% 0.51/0.44 thf(func_def_57, type, b: a).
% 0.51/0.44 thf(func_def_58, type, d: real).
% 0.51/0.44 thf(func_def_59, type, f: (a > a)).
% 0.51/0.44 thf(func_def_60, type, s: a).
% 0.51/0.44 thf(func_def_61, type, thesis: $o).
% 0.51/0.44 thf(func_def_62, type, x2: a).
% 0.51/0.44 thf(func_def_63, type, z: a).
% 0.51/0.44 thf(func_def_67, type, vAND: ($o > $o > $o)).
% 0.51/0.44 thf(func_def_68, type, db1: !>[X0: $tType]:(X0)).
% 0.51/0.44 thf(func_def_69, type, db0: !>[X0: $tType]:(X0)).
% 0.51/0.44 thf(func_def_70, type, vNOT: ($o > $o)).
% 0.51/0.44 thf(func_def_71, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 0.51/0.44 thf(func_def_72, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 0.51/0.44 thf(func_def_73, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 0.51/0.44 thf(func_def_74, type, vIMP: ($o > $o > $o)).
% 0.51/0.44 thf(func_def_75, type, db2: !>[X0: $tType]:(X0)).
% 0.51/0.44 thf(func_def_76, type, vOR: ($o > $o > $o)).
% 0.51/0.44 thf(func_def_77, type, sP0: ((real > real > $o) > real > real > $o)).
% 0.51/0.44 thf(func_def_78, type, sK1: a).
% 0.51/0.44 thf(func_def_79, type, sK2: ((real > real > $o) > real > real > real)).
% 0.51/0.44 thf(func_def_80, type, sK3: (real > (real > real > $o) > real > real > real)).
% 0.51/0.44 thf(func_def_81, type, sK4: (real > (real > real > $o) > real > real > real)).
% 0.51/0.44 thf(func_def_82, type, sK5: ((real > real > $o) > real)).
% 0.51/0.44 thf(func_def_83, type, sK6: ((real > real > $o) > real)).
% 0.51/0.44 thf(func_def_84, type, sK7: ((real > real > $o) > real)).
% 0.51/0.44 thf(func_def_85, type, sK8: real).
% 0.51/0.44 thf(func_def_86, type, sK9: (a > a)).
% 0.51/0.44 thf(func_def_87, type, sK10: (a > a)).
% 0.51/0.44 thf(func_def_88, type, sK11: ((a > $o) > (a > $o) > a)).
% 0.51/0.44 thf(func_def_89, type, sK12: (a > a > a)).
% 0.51/0.44 thf(func_def_90, type, sK13: (set_a > a)).
% 0.51/0.44 thf(func_def_91, type, sK14: (set_real > set_real > real)).
% 0.51/0.44 thf(func_def_92, type, sK15: (real > real > a)).
% 0.51/0.44 thf(func_def_93, type, sK16: (real > real > a)).
% 0.51/0.44 thf(func_def_94, type, sK17: a).
% 0.51/0.44 thf(func_def_95, type, sK18: (a > real)).
% 0.51/0.44 thf(func_def_96, type, sK19: (a > real)).
% 0.51/0.44 thf(func_def_97, type, sK20: (a > real)).
% 0.51/0.44 thf(func_def_98, type, sK21: ((real > $o) > (real > $o) > real)).
% 0.51/0.44 thf(func_def_99, type, sK22: (a > real)).
% 0.51/0.44 thf(func_def_100, type, sK23: (a > real)).
% 0.51/0.44 thf(func_def_101, type, sK24: (a > real)).
% 0.51/0.44 thf(func_def_102, type, sK25: (set_a > set_a > a)).
% 0.51/0.44 thf(func_def_103, type, sK26: (a > a)).
% 0.51/0.44 thf(func_def_104, type, sK27: (a > real > a)).
% 0.51/0.44 thf(func_def_105, type, sK28: (set_a > a)).
% 0.51/0.44 thf(func_def_106, type, sK29: (real > real > a)).
% 0.51/0.44 thf(func_def_107, type, sK30: (set_real > set_real > real)).
% 0.51/0.44 thf(func_def_108, type, sK31: ((real > $o) > (real > $o) > real)).
% 0.51/0.44 thf(func_def_109, type, sK32: (real > real)).
% 0.51/0.44 thf(func_def_110, type, sK33: (set_a > set_a > a)).
% 0.51/0.44 thf(func_def_111, type, sK34: ((a > $o) > (a > $o) > a)).
% 0.51/0.44 thf(f1,axiom,(
% 0.51/0.44 (ord_less_real @ zero_zero_real @ d)),
% 0.51/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_d_I1_J)).
% 0.51/0.44 thf(f2,axiom,(
% 0.51/0.44 (member_a @ s @ (elemen49976720ball_a @ x2 @ d))),
% 0.51/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1__092_060open_062s_A_092_060in_062_Acball_Ax_Ad_092_060close_062)).
% 0.51/0.44 thf(f6,axiom,(
% 0.51/0.44 ! [X0 : a] : ((member_a @ X0 @ (elemen49976720ball_a @ x2 @ d)) => (ord_less_eq_real @ (inner_1173012732nner_a @ (f @ s) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))) @ (inner_1173012732nner_a @ (f @ X0) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b)))))),
% 0.51/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_5__092_060open_062_092_060forall_062x_092_060in_062cball_Ax_Ad_O_Af_As_A_092_060bullet_062_Arot_A_Ia_A_N_Ab_J_A_092_060le_062_Af_Ax_A_092_060bullet_062_Arot_A_Ia_A_N_Ab_J_092_060close_062)).
% 0.51/0.44 thf(f9,axiom,(
% 0.51/0.44 ! [X0 : a] : ((member_a @ X0 @ (elemen49976720ball_a @ x2 @ d)) => ((((f @ X0)) != zero_zero_a) & (ord_less_real @ zero_zero_real @ (inner_1173012732nner_a @ (f @ X0) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b)))) & (member_a @ X0 @ x)))),
% 0.51/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_8_d_I2_J)).
% 0.51/0.44 thf(f353,conjecture,(
% 0.51/0.44 ? [X0 : real] : ((ord_less_real @ zero_zero_real @ X0) & ? [X1 : real] : ((ord_less_real @ zero_zero_real @ X1) & ! [X2 : a] : ((member_a @ X2 @ (elemen49976720ball_a @ x2 @ X0)) => (ord_less_eq_real @ X1 @ (inner_1173012732nner_a @ (f @ X2) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b)))))))),
% 0.51/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0)).
% 0.51/0.44 thf(f354,negated_conjecture,(
% 0.51/0.44 ~ ? [X0 : real] : ((ord_less_real @ zero_zero_real @ X0) & ? [X1 : real] : ((ord_less_real @ zero_zero_real @ X1) & ! [X2 : a] : ((member_a @ X2 @ (elemen49976720ball_a @ x2 @ X0)) => (ord_less_eq_real @ X1 @ (inner_1173012732nner_a @ (f @ X2) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b)))))))),
% 0.51/0.44 inference(negated_conjecture,[status(cth)],[f353])).
% 0.51/0.44 thf(f438,plain,(
% 0.51/0.44 (member_a @ s @ (elemen49976720ball_a @ x2 @ d))),
% 0.51/0.44 inference(rectify,[],[f2])).
% 0.51/0.44 thf(f439,plain,(
% 0.51/0.44 (((member_a @ s @ (elemen49976720ball_a @ x2 @ d))) = $true)),
% 0.51/0.44 inference(fool_elimination,[],[f438])).
% 0.51/0.44 thf(f450,plain,(
% 0.51/0.44 ! [X0 : a] : ((member_a @ X0 @ (elemen49976720ball_a @ x2 @ d)) => (ord_less_eq_real @ (inner_1173012732nner_a @ (f @ s) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))) @ (inner_1173012732nner_a @ (f @ X0) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b)))))),
% 0.51/0.44 inference(rectify,[],[f6])).
% 0.51/0.44 thf(f451,plain,(
% 0.51/0.44 ! [X0 : a] : ((((member_a @ X0 @ (elemen49976720ball_a @ x2 @ d))) = $true) => (((ord_less_eq_real @ (inner_1173012732nner_a @ (f @ s) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))) @ (inner_1173012732nner_a @ (f @ X0) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))))) = $true))),
% 0.51/0.44 inference(fool_elimination,[],[f450])).
% 0.51/0.44 thf(f541,plain,(
% 0.51/0.44 ~ ? [X0 : real] : ((ord_less_real @ zero_zero_real @ X0) & ? [X1 : real] : ((ord_less_real @ zero_zero_real @ X1) & ! [X2 : a] : ((member_a @ X2 @ (elemen49976720ball_a @ x2 @ X0)) => (ord_less_eq_real @ X1 @ (inner_1173012732nner_a @ (f @ X2) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b)))))))),
% 0.51/0.44 inference(rectify,[],[f354])).
% 0.51/0.44 thf(f542,plain,(
% 0.51/0.44 ~ ? [X0 : real] : ((((ord_less_real @ zero_zero_real @ X0)) = $true) & ? [X1 : real] : ((((ord_less_real @ zero_zero_real @ X1)) = $true) & ! [X2 : a] : ((((member_a @ X2 @ (elemen49976720ball_a @ x2 @ X0))) = $true) => (((ord_less_eq_real @ X1 @ (inner_1173012732nner_a @ (f @ X2) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))))) = $true))))),
% 0.51/0.44 inference(fool_elimination,[],[f541])).
% 0.51/0.44 thf(f647,plain,(
% 0.51/0.44 ! [X0 : a] : ((member_a @ X0 @ (elemen49976720ball_a @ x2 @ d)) => ((((f @ X0)) != zero_zero_a) & (ord_less_real @ zero_zero_real @ (inner_1173012732nner_a @ (f @ X0) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b)))) & (member_a @ X0 @ x)))),
% 0.51/0.44 inference(rectify,[],[f9])).
% 0.51/0.44 thf(f648,plain,(
% 0.51/0.44 ! [X0 : a] : ((((member_a @ X0 @ (elemen49976720ball_a @ x2 @ d))) = $true) => ((((member_a @ X0 @ x)) = $true) & (((ord_less_real @ zero_zero_real @ (inner_1173012732nner_a @ (f @ X0) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))))) = $true) & (((f @ X0)) != zero_zero_a)))),
% 0.51/0.44 inference(fool_elimination,[],[f647])).
% 0.51/0.44 thf(f670,plain,(
% 0.51/0.44 (ord_less_real @ zero_zero_real @ d)),
% 0.51/0.44 inference(rectify,[],[f1])).
% 0.51/0.44 thf(f671,plain,(
% 0.51/0.44 (((ord_less_real @ zero_zero_real @ d)) = $true)),
% 0.51/0.44 inference(fool_elimination,[],[f670])).
% 0.51/0.44 thf(f1046,plain,(
% 0.51/0.44 ! [X0 : real] : (! [X1 : real] : ((((ord_less_real @ zero_zero_real @ X1)) != $true) | ? [X2 : a] : ((((ord_less_eq_real @ X1 @ (inner_1173012732nner_a @ (f @ X2) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))))) != $true) & (((member_a @ X2 @ (elemen49976720ball_a @ x2 @ X0))) = $true))) | (((ord_less_real @ zero_zero_real @ X0)) != $true))),
% 0.51/0.44 inference(ennf_transformation,[],[f542])).
% 0.51/0.44 thf(f1051,plain,(
% 0.51/0.44 ! [X0 : a] : (((((member_a @ X0 @ x)) = $true) & (((ord_less_real @ zero_zero_real @ (inner_1173012732nner_a @ (f @ X0) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))))) = $true) & (((f @ X0)) != zero_zero_a)) | (((member_a @ X0 @ (elemen49976720ball_a @ x2 @ d))) != $true))),
% 0.51/0.44 inference(ennf_transformation,[],[f648])).
% 0.51/0.44 thf(f1087,plain,(
% 0.51/0.44 ! [X0 : a] : ((((member_a @ X0 @ (elemen49976720ball_a @ x2 @ d))) != $true) | (((ord_less_eq_real @ (inner_1173012732nner_a @ (f @ s) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))) @ (inner_1173012732nner_a @ (f @ X0) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))))) = $true))),
% 0.51/0.44 inference(ennf_transformation,[],[f451])).
% 0.51/0.44 thf(f1309,plain,(
% 0.51/0.44 ! [X0 : real] : (! [X1 : real] : ((((ord_less_real @ zero_zero_real @ X1)) != $true) | ((((ord_less_eq_real @ X1 @ (inner_1173012732nner_a @ (f @ (sK29 @ X1 @ X0)) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))))) != $true) & ($true = ((member_a @ (sK29 @ X1 @ X0) @ (elemen49976720ball_a @ x2 @ X0)))))) | (((ord_less_real @ zero_zero_real @ X0)) != $true))),
% 0.51/0.44 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP]),skolemize(X6,sK4 @ X4 @ X2 @ X1 @ X0)],[f1046])).
% 0.51/0.44 thf(f1490,plain,(
% 0.51/0.44 (((ord_less_real @ zero_zero_real @ d)) = $true)),
% 0.51/0.44 inference(cnf_transformation,[],[f671])).
% 0.51/0.44 thf(f1576,plain,(
% 0.51/0.44 (((member_a @ s @ (elemen49976720ball_a @ x2 @ d))) = $true)),
% 0.51/0.44 inference(cnf_transformation,[],[f439])).
% 0.51/0.44 thf(f1622,plain,(
% 0.51/0.44 ( ! [X0 : a] : ((((ord_less_real @ zero_zero_real @ (inner_1173012732nner_a @ (f @ X0) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))))) = $true) | (((member_a @ X0 @ (elemen49976720ball_a @ x2 @ d))) != $true)) )),
% 0.51/0.44 inference(cnf_transformation,[],[f1051])).
% 0.51/0.44 thf(f1746,plain,(
% 0.51/0.44 ( ! [X0 : real,X1 : real] : (($true = ((member_a @ (sK29 @ X1 @ X0) @ (elemen49976720ball_a @ x2 @ X0)))) | (((ord_less_real @ zero_zero_real @ X0)) != $true) | (((ord_less_real @ zero_zero_real @ X1)) != $true)) )),
% 0.51/0.44 inference(cnf_transformation,[],[f1309])).
% 0.51/0.44 thf(f1747,plain,(
% 0.51/0.44 ( ! [X0 : real,X1 : real] : ((((ord_less_eq_real @ X1 @ (inner_1173012732nner_a @ (f @ (sK29 @ X1 @ X0)) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))))) != $true) | (((ord_less_real @ zero_zero_real @ X0)) != $true) | (((ord_less_real @ zero_zero_real @ X1)) != $true)) )),
% 0.51/0.44 inference(cnf_transformation,[],[f1309])).
% 0.51/0.44 thf(f1877,plain,(
% 0.51/0.44 ( ! [X0 : a] : ((((ord_less_eq_real @ (inner_1173012732nner_a @ (f @ s) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))) @ (inner_1173012732nner_a @ (f @ X0) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))))) = $true) | (((member_a @ X0 @ (elemen49976720ball_a @ x2 @ d))) != $true)) )),
% 0.51/0.44 inference(cnf_transformation,[],[f1087])).
% 0.51/0.44 thf(f2056,definition,(
% 0.51/0.44 spl35_3 <=> (((ord_less_real @ zero_zero_real @ d)) = $true)),
% 0.51/0.44 introduced(definition,[new_symbols(definition,[spl35_3])],[avatar_definition])).
% 0.51/0.44 thf(f2059,plain,(
% 0.51/0.44 spl35_3),
% 0.51/0.44 inference(avatar_split_clause,[],[f1490,f2056])).
% 0.51/0.44 thf(f2066,definition,(
% 0.51/0.44 spl35_5 <=> (((member_a @ s @ (elemen49976720ball_a @ x2 @ d))) = $true)),
% 0.51/0.44 introduced(definition,[new_symbols(definition,[spl35_5])],[avatar_definition])).
% 0.51/0.44 thf(f2068,plain,(
% 0.51/0.44 (((member_a @ s @ (elemen49976720ball_a @ x2 @ d))) = $true) | ~spl35_5),
% 0.51/0.44 inference(avatar_component_clause,[],[f2066])).
% 0.51/0.44 thf(f2069,plain,(
% 0.51/0.44 spl35_5),
% 0.51/0.44 inference(avatar_split_clause,[],[f1576,f2066])).
% 0.51/0.44 thf(f2574,plain,(
% 0.51/0.44 ( ! [X0 : real] : (($true != ((ord_less_real @ zero_zero_real @ (inner_1173012732nner_a @ (f @ s) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b)))))) | ($true != $true) | (((ord_less_real @ zero_zero_real @ X0)) != $true) | ($true != ((member_a @ (sK29 @ (inner_1173012732nner_a @ (f @ s) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))) @ X0) @ (elemen49976720ball_a @ x2 @ d))))) )),
% 0.51/0.44 inference(superposition,[],[f1747,f1877])).
% 0.51/0.44 thf(f2578,plain,(
% 0.51/0.44 ( ! [X0 : real] : ((((ord_less_real @ zero_zero_real @ X0)) != $true) | ($true != ((member_a @ (sK29 @ (inner_1173012732nner_a @ (f @ s) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))) @ X0) @ (elemen49976720ball_a @ x2 @ d)))) | ($true != ((ord_less_real @ zero_zero_real @ (inner_1173012732nner_a @ (f @ s) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))))))) )),
% 0.51/0.44 inference(trivial_inequality_removal,[],[f2574])).
% 0.51/0.44 thf(f2583,definition,(
% 0.51/0.44 spl35_71 <=> ($true = ((ord_less_real @ zero_zero_real @ (inner_1173012732nner_a @ (f @ s) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))))))),
% 0.51/0.44 introduced(definition,[new_symbols(definition,[spl35_71])],[avatar_definition])).
% 0.51/0.44 thf(f2585,plain,(
% 0.51/0.44 ($true != ((ord_less_real @ zero_zero_real @ (inner_1173012732nner_a @ (f @ s) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b)))))) | spl35_71),
% 0.51/0.44 inference(avatar_component_clause,[],[f2583])).
% 0.51/0.44 thf(f2587,definition,(
% 0.51/0.44 spl35_72 <=> ! [X0 : real] : ((((ord_less_real @ zero_zero_real @ X0)) != $true) | ($true != ((member_a @ (sK29 @ (inner_1173012732nner_a @ (f @ s) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))) @ X0) @ (elemen49976720ball_a @ x2 @ d)))))),
% 0.51/0.44 introduced(definition,[new_symbols(definition,[spl35_72])],[avatar_definition])).
% 0.51/0.44 thf(f2588,plain,(
% 0.51/0.44 ( ! [X0 : real] : (($true != ((member_a @ (sK29 @ (inner_1173012732nner_a @ (f @ s) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b))) @ X0) @ (elemen49976720ball_a @ x2 @ d)))) | (((ord_less_real @ zero_zero_real @ X0)) != $true)) ) | ~spl35_72),
% 0.51/0.44 inference(avatar_component_clause,[],[f2587])).
% 0.51/0.44 thf(f2589,plain,(
% 0.51/0.44 ~spl35_71 | spl35_72),
% 0.51/0.44 inference(avatar_split_clause,[],[f2578,f2587,f2583])).
% 0.51/0.44 thf(f2678,plain,(
% 0.51/0.44 ($true != $true) | (((member_a @ s @ (elemen49976720ball_a @ x2 @ d))) != $true) | spl35_71),
% 0.51/0.44 inference(superposition,[],[f2585,f1622])).
% 0.51/0.44 thf(f2683,plain,(
% 0.51/0.44 (((member_a @ s @ (elemen49976720ball_a @ x2 @ d))) != $true) | spl35_71),
% 0.51/0.44 inference(trivial_inequality_removal,[],[f2678])).
% 0.51/0.44 thf(f2688,plain,(
% 0.51/0.44 $false | (~spl35_5 | spl35_71)),
% 0.51/0.44 inference(forward_subsumption_resolution,[],[f2683,f2068])).
% 0.51/0.44 thf(f2689,plain,(
% 0.51/0.44 ~spl35_5 | spl35_71),
% 0.51/0.44 inference(avatar_contradiction_clause,[],[f2688])).
% 0.51/0.44 thf(f2719,plain,(
% 0.51/0.44 ($true != $true) | ($true != ((ord_less_real @ zero_zero_real @ (inner_1173012732nner_a @ (f @ s) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b)))))) | (((ord_less_real @ zero_zero_real @ d)) != $true) | (((ord_less_real @ zero_zero_real @ d)) != $true) | ~spl35_72),
% 0.51/0.44 inference(superposition,[],[f2588,f1746])).
% 0.51/0.44 thf(f2725,plain,(
% 0.51/0.44 (((ord_less_real @ zero_zero_real @ d)) != $true) | ($true != ((ord_less_real @ zero_zero_real @ (inner_1173012732nner_a @ (f @ s) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b)))))) | ($true != $true) | ~spl35_72),
% 0.51/0.44 inference(duplicate_literal_removal,[],[f2719])).
% 0.51/0.44 thf(f2726,plain,(
% 0.51/0.44 (((ord_less_real @ zero_zero_real @ d)) != $true) | ($true != ((ord_less_real @ zero_zero_real @ (inner_1173012732nner_a @ (f @ s) @ (poinca659159244_rot_a @ (minus_minus_a @ a2 @ b)))))) | ~spl35_72),
% 0.51/0.44 inference(trivial_inequality_removal,[],[f2725])).
% 0.51/0.44 thf(f2728,plain,(
% 0.51/0.44 ~spl35_3 | ~spl35_71 | ~spl35_72),
% 0.51/0.44 inference(avatar_split_clause,[],[f2726,f2587,f2583,f2056])).
% 0.51/0.44 cnf(s3, plain, spl35_3, inference(sat_conversion,[],[f2059])).
% 0.51/0.44 cnf(s5, plain, spl35_5, inference(sat_conversion,[],[f2069])).
% 0.51/0.44 cnf(s90, plain, ~spl35_71 | spl35_72, inference(sat_conversion,[],[f2589])).
% 0.51/0.44 cnf(s95, plain, ~spl35_5 | spl35_71, inference(sat_conversion,[],[f2689])).
% 0.51/0.44 cnf(s100, plain, ~spl35_3 | ~spl35_71 | ~spl35_72, inference(sat_conversion,[],[f2728])).
% 0.51/0.44 cnf(s105, plain, spl35_71, inference(rat,[],[s95,s5])).
% 0.51/0.44 cnf(s108, plain, spl35_72, inference(rat,[],[s90,s105])).
% 0.51/0.44 cnf(s109, plain, ~spl35_3, inference(rat,[],[s100,s105,s108])).
% 0.51/0.44 cnf(s110, plain, $false, inference(rat,[],[s3,s109])).
% 0.51/0.44 thf(f2733,plain,(
% 0.51/0.44 $false),
% 0.51/0.44 inference(avatar_sat_refutation,[],[s110])).
% 0.51/0.44 % SZS output end Proof for theBenchmark
% 0.51/0.44 % (2589296)------------------------------
% 0.51/0.44 % (2589296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.51/0.44 % (2589296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.51/0.44 % (2589296)CaDiCaL version: 2.1.3
% 0.51/0.44 % (2589296)Termination reason: Refutation
% 0.51/0.44 % (2589296)Time elapsed: 0.099 s
% 0.51/0.44 % (2589296)Peak memory usage: 15 MB
% 0.51/0.44 % (2589296)Instructions burned: 197 (million)
% 0.51/0.44 % (2589288)Success in time 0.15 s
% 0.51/0.44 % Vampire exiting
%------------------------------------------------------------------------------