%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP021^3 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n018.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:07:55 AM UTC 2026
% Result : Theorem 3.63s 1.03s
% Output : Refutation 3.63s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP021^3 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 % Computer : n018.cluster.edu
% 0.08/0.23 % Model : x86_64 x86_64
% 0.08/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.23 % Memory : 8046.5625MB
% 0.08/0.23 % OS : Linux 6.8.0-71-generic
% 0.08/0.23 % CPULimit : 300
% 0.08/0.23 % WCLimit : 300
% 0.08/0.23 % DateTime : Tue Sep 29 19:36:26 UTC 2026
% 0.08/0.24 % CPUTime :
% 0.08/0.24 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.29 Running higher-order theorem proving
% 0.24/0.30 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.84/0.47 % (535688)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.84/0.47 % (535697)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=2504859932:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.84/0.47 % (535694)lrs+10_16_si=on:nwc=1.5:random_seed=1076670270:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.84/0.47 % (535699)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.84/0.47 % (535699)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.84/0.47 % (535697)Instruction limit reached!
% 0.84/0.47 % (535697)------------------------------
% 0.84/0.47 % (535697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.84/0.47 % (535697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.84/0.47 % (535697)CaDiCaL version: 2.1.3
% 0.84/0.47 % (535697)Termination reason: Instruction limit
% 0.84/0.47 % (535697)Termination phase: Saturation
% 0.84/0.47 % (535697)Time elapsed: 0.013 s
% 0.84/0.47 % (535697)Peak memory usage: 12 MB
% 0.84/0.47 % (535695)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=211492772:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.84/0.47 % (535697)Instructions burned: 26 (million)
% 0.84/0.47 % (535693)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3184428221:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.84/0.47 % (535694)Instruction limit reached!
% 0.84/0.47 % (535694)------------------------------
% 0.84/0.47 % (535694)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.84/0.47 % (535694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.84/0.47 % (535694)CaDiCaL version: 2.1.3
% 0.84/0.47 % (535694)Termination reason: Instruction limit
% 0.84/0.47 % (535694)Termination phase: Saturation
% 0.84/0.47 % (535694)Time elapsed: 0.010 s
% 0.84/0.47 % (535694)Peak memory usage: 12 MB
% 0.84/0.47 % (535694)Instructions burned: 18 (million)
% 0.84/0.47 % (535698)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=431075953:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.84/0.47 % (535699)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=1079785339:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.84/0.47 % (535696)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=2086156517: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.84/0.47 % (535695)Instruction limit reached!
% 0.84/0.47 % (535695)------------------------------
% 0.84/0.47 % (535695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.84/0.47 % (535695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.84/0.47 % (535695)CaDiCaL version: 2.1.3
% 0.84/0.47 % (535695)Termination reason: Instruction limit
% 0.84/0.47 % (535695)Termination phase: Preprocessing 3
% 0.84/0.47 % (535695)Time elapsed: 0.004 s
% 0.84/0.47 % (535695)Peak memory usage: 10 MB
% 0.84/0.47 % (535695)Instructions burned: 3 (million)
% 0.84/0.47 % (535705)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3874423043:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.84/0.47 % (535705)Instruction limit reached!
% 0.84/0.47 % (535705)------------------------------
% 0.84/0.47 % (535705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.84/0.47 % (535705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.84/0.47 % (535705)CaDiCaL version: 2.1.3
% 0.84/0.47 % (535705)Termination reason: Instruction limit
% 0.84/0.47 % (535705)Termination phase: Preprocessing 3
% 0.84/0.47 % (535705)Time elapsed: 0.002 s
% 0.84/0.47 % (535705)Peak memory usage: 10 MB
% 0.84/0.47 % (535705)Instructions burned: 3 (million)
% 0.84/0.47 % (535708)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=2579082579:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.84/0.47 % (535708)Instruction limit reached!
% 1.24/0.54 % (535708)------------------------------
% 1.24/0.54 % (535708)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.24/0.54 % (535708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.24/0.54 % (535708)CaDiCaL version: 2.1.3
% 1.24/0.54 % (535708)Termination reason: Instruction limit
% 1.24/0.54 % (535708)Termination phase: Property scanning
% 1.24/0.54 % (535708)Time elapsed: 0.003 s
% 1.24/0.54 % (535708)Peak memory usage: 10 MB
% 1.24/0.54 % (535708)Instructions burned: 5 (million)
% 1.24/0.54 % (535709)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.24/0.54 % (535709)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=381044019:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 1.24/0.54 % (535711)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=3849703176:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 1.24/0.54 % (535713)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
% 1.24/0.54 % (535713)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.24/0.54 % (535709)Instruction limit reached!
% 1.24/0.54 % (535709)------------------------------
% 1.24/0.54 % (535709)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.24/0.54 % (535711)Instruction limit reached!
% 1.24/0.54 % (535711)------------------------------
% 1.24/0.54 % (535711)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.24/0.54 % (535709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.24/0.54 % (535709)CaDiCaL version: 2.1.3
% 1.24/0.54 % (535709)Termination reason: Instruction limit
% 1.24/0.54 % (535709)Termination phase: Property scanning
% 1.24/0.54 % (535711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.24/0.54 % (535709)Time elapsed: 0.006 s
% 1.24/0.54 % (535709)Peak memory usage: 10 MB
% 1.24/0.54 % (535709)Instructions burned: 8 (million)
% 1.24/0.54 % (535711)CaDiCaL version: 2.1.3
% 1.24/0.54 % (535711)Termination reason: Instruction limit
% 1.24/0.54 % (535711)Termination phase: Property scanning
% 1.24/0.54 % (535711)Time elapsed: 0.006 s
% 1.24/0.54 % (535711)Peak memory usage: 11 MB
% 1.24/0.54 % (535711)Instructions burned: 12 (million)
% 1.24/0.54 % (535713)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=2182209671:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 1.24/0.54 % (535713)Instruction limit reached!
% 1.24/0.54 % (535713)------------------------------
% 1.24/0.54 % (535713)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.24/0.54 % (535713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.24/0.54 % (535713)CaDiCaL version: 2.1.3
% 1.24/0.54 % (535713)Termination reason: Instruction limit
% 1.24/0.54 % (535713)Termination phase: Saturation
% 1.24/0.54 % (535713)Time elapsed: 0.015 s
% 1.24/0.54 % (535713)Peak memory usage: 12 MB
% 1.24/0.54 % (535713)Instructions burned: 29 (million)
% 1.24/0.54 % (535717)lrs+10_1_si=on:cs=on:random_seed=3227110507:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 1.24/0.54 % (535717)Instruction limit reached!
% 1.24/0.54 % (535717)------------------------------
% 1.24/0.54 % (535717)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.24/0.54 % (535717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.24/0.54 % (535717)CaDiCaL version: 2.1.3
% 1.24/0.54 % (535717)Termination reason: Instruction limit
% 1.24/0.54 % (535717)Termination phase: Function definition elimination
% 1.24/0.54 % (535717)Time elapsed: 0.004 s
% 1.24/0.54 % (535717)Peak memory usage: 11 MB
% 1.24/0.54 % (535717)Instructions burned: 8 (million)
% 1.24/0.54 % (535716)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=954688446:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 1.24/0.54 % (535720)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 1.96/0.62 % (535698)Instruction limit reached!
% 1.96/0.62 % (535698)------------------------------
% 1.96/0.62 % (535698)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.96/0.62 % (535698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.96/0.62 % (535698)CaDiCaL version: 2.1.3
% 1.96/0.62 % (535698)Termination reason: Instruction limit
% 1.96/0.62 % (535698)Termination phase: Saturation
% 1.96/0.62 % (535698)Time elapsed: 0.078 s
% 1.96/0.62 % (535698)Peak memory usage: 12 MB
% 1.96/0.62 % (535698)Instructions burned: 75 (million)
% 1.96/0.62 % (535693)Instruction limit reached!
% 1.96/0.62 % (535693)------------------------------
% 1.96/0.62 % (535693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.96/0.62 % (535693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.96/0.62 % (535693)CaDiCaL version: 2.1.3
% 1.96/0.62 % (535693)Termination reason: Instruction limit
% 1.96/0.62 % (535693)Termination phase: Saturation
% 1.96/0.62 % (535693)Time elapsed: 0.081 s
% 1.96/0.62 % (535693)Peak memory usage: 12 MB
% 1.96/0.62 % (535693)Instructions burned: 88 (million)
% 1.96/0.62 % (535720)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=2292803122:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 1.96/0.62 % (535721)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=3095556350:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 1.96/0.62 % (535720)Instruction limit reached!
% 1.96/0.62 % (535720)------------------------------
% 1.96/0.62 % (535720)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.96/0.62 % (535720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.96/0.62 % (535720)CaDiCaL version: 2.1.3
% 1.96/0.62 % (535720)Termination reason: Instruction limit
% 1.96/0.62 % (535720)Termination phase: Property scanning
% 1.96/0.62 % (535720)Time elapsed: 0.004 s
% 1.96/0.62 % (535720)Peak memory usage: 10 MB
% 1.96/0.62 % (535720)Instructions burned: 6 (million)
% 1.96/0.62 % (535721)Instruction limit reached!
% 1.96/0.62 % (535721)------------------------------
% 1.96/0.62 % (535721)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.96/0.62 % (535721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.96/0.62 % (535721)CaDiCaL version: 2.1.3
% 1.96/0.62 % (535721)Termination reason: Instruction limit
% 1.96/0.62 % (535721)Termination phase: Saturation
% 1.96/0.62 % (535721)Time elapsed: 0.019 s
% 1.96/0.62 % (535721)Peak memory usage: 13 MB
% 1.96/0.62 % (535721)Instructions burned: 39 (million)
% 1.96/0.62 % (535727)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=2256776066:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.96/0.62 % (535723)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=2831849982:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 1.96/0.62 % (535725)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=739956525:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 1.96/0.62 % (535727)Instruction limit reached!
% 1.96/0.62 % (535727)------------------------------
% 1.96/0.62 % (535727)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.96/0.62 % (535727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.96/0.62 % (535727)CaDiCaL version: 2.1.3
% 1.96/0.62 % (535727)Termination reason: Instruction limit
% 1.96/0.62 % (535727)Termination phase: Saturation
% 1.96/0.62 % (535727)Time elapsed: 0.013 s
% 1.96/0.62 % (535727)Peak memory usage: 11 MB
% 1.96/0.62 % (535727)Instructions burned: 15 (million)
% 1.96/0.62 % (535728)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=3364819838:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 1.96/0.62 % (535716)Refutation not found, incomplete strategy
% 1.96/0.62 % (535716)------------------------------
% 1.96/0.62 % (535716)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.96/0.62 % (535716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.96/0.62 % (535716)CaDiCaL version: 2.1.3
% 1.96/0.62 % (535716)Termination reason: Refutation not found, incomplete strategy
% 2.54/0.70 % (535716)Time elapsed: 0.048 s
% 2.54/0.70 % (535716)Peak memory usage: 12 MB
% 2.54/0.70 % (535716)Instructions burned: 53 (million)
% 2.54/0.70 % (535716)------------------------------
% 2.54/0.70 % (535716)------------------------------
% 2.54/0.70 % (535725)Instruction limit reached!
% 2.54/0.70 % (535725)------------------------------
% 2.54/0.70 % (535725)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.54/0.70 % (535725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.54/0.70 % (535725)CaDiCaL version: 2.1.3
% 2.54/0.70 % (535725)Termination reason: Instruction limit
% 2.54/0.70 % (535725)Termination phase: Saturation
% 2.54/0.70 % (535725)Time elapsed: 0.024 s
% 2.54/0.70 % (535725)Peak memory usage: 12 MB
% 2.54/0.70 % (535725)Instructions burned: 25 (million)
% 2.54/0.70 % (535699)Instruction limit reached!
% 2.54/0.70 % (535699)------------------------------
% 2.54/0.70 % (535699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.54/0.70 % (535699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.54/0.70 % (535699)CaDiCaL version: 2.1.3
% 2.54/0.70 % (535699)Termination reason: Instruction limit
% 2.54/0.70 % (535699)Termination phase: Saturation
% 2.54/0.70 % (535699)Time elapsed: 0.149 s
% 2.54/0.70 % (535699)Peak memory usage: 13 MB
% 2.54/0.70 % (535699)Instructions burned: 158 (million)
% 2.54/0.70 % (535732)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=526570800:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 2.54/0.70 % (535734)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=2270718984: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)
% 2.54/0.70 % (535734)Instruction limit reached!
% 2.54/0.70 % (535734)------------------------------
% 2.54/0.70 % (535734)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.54/0.70 % (535734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.54/0.70 % (535734)CaDiCaL version: 2.1.3
% 2.54/0.70 % (535734)Termination reason: Instruction limit
% 2.54/0.70 % (535734)Termination phase: SInE selection
% 2.54/0.70 % (535734)Time elapsed: 0.002 s
% 2.54/0.70 % (535734)Peak memory usage: 10 MB
% 2.54/0.70 % (535734)Instructions burned: 2 (million)
% 2.54/0.70 % (535732)Instruction limit reached!
% 2.54/0.70 % (535732)------------------------------
% 2.54/0.70 % (535732)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.54/0.70 % (535732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.54/0.70 % (535732)CaDiCaL version: 2.1.3
% 2.54/0.70 % (535732)Termination reason: Instruction limit
% 2.54/0.70 % (535732)Termination phase: Saturation
% 2.54/0.70 % (535732)Time elapsed: 0.013 s
% 2.54/0.70 % (535732)Peak memory usage: 12 MB
% 2.54/0.70 % (535732)Instructions burned: 14 (million)
% 2.54/0.70 % (535735)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=4093880574:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 2.54/0.70 % (535736)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=2438406777:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 2.54/0.70 % (535740)WARNING Broken Constraint: if sine_to_age_generality_threshold(10) 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
% 2.54/0.70 % (535740)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 2.54/0.70 % (535739)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=1575647114:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 2.54/0.70 % (535740)ott+21_1_to=kbo:sil=128000:cnfonf=lazy_gen:bsd=on:si=on:sp=const_frequency:lma=off:uwa=off:foolp=on:s2agt=10:lwlo=on:random_seed=2640138118:i=14:add=off:nm=40:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 2.54/0.70 % (535735)Instruction limit reached!
% 2.54/0.70 % (535735)------------------------------
% 2.54/0.70 % (535735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.54/0.70 % (535735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.54/0.70 % (535735)CaDiCaL version: 2.1.3
% 2.54/0.70 % (535735)Termination reason: Instruction limit
% 3.04/0.81 % (535735)Termination phase: Saturation
% 3.04/0.81 % (535735)Time elapsed: 0.024 s
% 3.04/0.81 % (535735)Peak memory usage: 11 MB
% 3.04/0.81 % (535735)Instructions burned: 26 (million)
% 3.04/0.81 % (535740)Instruction limit reached!
% 3.04/0.81 % (535740)------------------------------
% 3.04/0.81 % (535740)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.81 % (535740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.81 % (535740)CaDiCaL version: 2.1.3
% 3.04/0.81 % (535740)Termination reason: Instruction limit
% 3.04/0.81 % (535740)Termination phase: Saturation
% 3.04/0.81 % (535740)Time elapsed: 0.011 s
% 3.04/0.81 % (535740)Peak memory usage: 11 MB
% 3.04/0.81 % (535740)Instructions burned: 14 (million)
% 3.04/0.81 % (535736)Instruction limit reached!
% 3.04/0.81 % (535736)------------------------------
% 3.04/0.81 % (535736)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.81 % (535736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.81 % (535736)CaDiCaL version: 2.1.3
% 3.04/0.81 % (535736)Termination reason: Instruction limit
% 3.04/0.81 % (535736)Termination phase: Saturation
% 3.04/0.81 % (535736)Time elapsed: 0.021 s
% 3.04/0.81 % (535736)Peak memory usage: 12 MB
% 3.04/0.81 % (535736)Instructions burned: 24 (million)
% 3.04/0.81 % (535745)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 3.04/0.81 % (535745)lrs+1010_4:1_slsqr=8,1:to=kbo:cha=on:drc=off:si=on:sp=arity:lcm=predicate:uwa=off:fd=preordered:gs=on:nwc=5:s2agt=32:slsqc=1:kmz=on:updr=off:chr=on:pe=on:slsq=on:random_seed=736103642:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2997 on theBenchmark for (2997ds/8Mi)
% 3.04/0.81 % (535746)dis+1004_50_to=lpo:drc=off:fde=unused:cnfonf=lazy_not_gen_be_off:si=on:sp=reverse_arity:spb=units:cbe=off:foolp=on:random_seed=16012553:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2997 on theBenchmark for (2997ds/31Mi)
% 3.04/0.81 % (535747)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=4062601536:i=7:hud=5:bd=preordered:rtra=on:bet=on_2997 on theBenchmark for (2997ds/7Mi)
% 3.04/0.81 % (535745)Instruction limit reached!
% 3.04/0.81 % (535745)------------------------------
% 3.04/0.81 % (535745)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.81 % (535745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.81 % (535745)CaDiCaL version: 2.1.3
% 3.04/0.81 % (535745)Termination reason: Instruction limit
% 3.04/0.81 % (535745)Termination phase: Property scanning
% 3.04/0.81 % (535745)Time elapsed: 0.008 s
% 3.04/0.81 % (535745)Peak memory usage: 10 MB
% 3.04/0.81 % (535745)Instructions burned: 8 (million)
% 3.04/0.81 % (535747)Instruction limit reached!
% 3.04/0.81 % (535747)------------------------------
% 3.04/0.81 % (535747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.81 % (535747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.81 % (535747)CaDiCaL version: 2.1.3
% 3.04/0.81 % (535747)Termination reason: Instruction limit
% 3.04/0.81 % (535747)Termination phase: Function definition elimination
% 3.04/0.81 % (535747)Time elapsed: 0.007 s
% 3.04/0.81 % (535747)Peak memory usage: 10 MB
% 3.04/0.81 % (535747)Instructions burned: 8 (million)
% 3.04/0.81 % (535739)Instruction limit reached!
% 3.04/0.81 % (535739)------------------------------
% 3.04/0.81 % (535739)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.81 % (535739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.81 % (535739)CaDiCaL version: 2.1.3
% 3.04/0.81 % (535739)Termination reason: Instruction limit
% 3.04/0.81 % (535739)Termination phase: Saturation
% 3.04/0.81 % (535739)Time elapsed: 0.060 s
% 3.04/0.81 % (535739)Peak memory usage: 12 MB
% 3.04/0.81 % (535739)Instructions burned: 60 (million)
% 3.04/0.81 % (535746)Instruction limit reached!
% 3.04/0.81 % (535746)------------------------------
% 3.04/0.81 % (535746)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.81 % (535746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.81 % (535746)CaDiCaL version: 2.1.3
% 3.04/0.81 % (535746)Termination reason: Instruction limit
% 3.04/0.81 % (535746)Termination phase: Saturation
% 3.04/0.81 % (535746)Time elapsed: 0.028 s
% 3.04/0.81 % (535746)Peak memory usage: 12 MB
% 3.04/0.81 % (535746)Instructions burned: 31 (million)
% 3.04/0.81 % (535728)Instruction limit reached!
% 3.04/0.81 % (535728)------------------------------
% 3.04/0.81 % (535728)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.63/0.93 % (535728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.63/0.93 % (535728)CaDiCaL version: 2.1.3
% 3.63/0.93 % (535728)Termination reason: Instruction limit
% 3.63/0.93 % (535728)Termination phase: Saturation
% 3.63/0.93 % (535728)Time elapsed: 0.145 s
% 3.63/0.93 % (535728)Peak memory usage: 13 MB
% 3.63/0.93 % (535728)Instructions burned: 327 (million)
% 3.63/0.93 % (535753)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=3118825423:i=1240:rtra=on:ixr=off_2997 on theBenchmark for (2997ds/1240Mi)
% 3.63/0.93 % (535751)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=2661074765:i=23:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/23Mi)
% 3.63/0.93 % (535752)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=3772623755:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2997 on theBenchmark for (2997ds/20Mi)
% 3.63/0.93 % (535751)Instruction limit reached!
% 3.63/0.93 % (535751)------------------------------
% 3.63/0.93 % (535751)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.63/0.93 % (535751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.63/0.93 % (535751)CaDiCaL version: 2.1.3
% 3.63/0.93 % (535751)Termination reason: Instruction limit
% 3.63/0.93 % (535751)Termination phase: Saturation
% 3.63/0.93 % (535751)Time elapsed: 0.019 s
% 3.63/0.93 % (535751)Peak memory usage: 11 MB
% 3.63/0.93 % (535751)Instructions burned: 23 (million)
% 3.63/0.93 % (535752)Instruction limit reached!
% 3.63/0.93 % (535752)------------------------------
% 3.63/0.93 % (535752)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.63/0.93 % (535752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.63/0.93 % (535752)CaDiCaL version: 2.1.3
% 3.63/0.93 % (535752)Termination reason: Instruction limit
% 3.63/0.93 % (535752)Termination phase: Saturation
% 3.63/0.93 % (535752)Time elapsed: 0.019 s
% 3.63/0.93 % (535752)Peak memory usage: 12 MB
% 3.63/0.93 % (535752)Instructions burned: 20 (million)
% 3.63/0.93 % (535754)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=56220170:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2997 on theBenchmark for (2997ds/143Mi)
% 3.63/0.93 % (535755)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=992510004:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/193Mi)
% 3.63/0.93 % (535760)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 3.63/0.93 % (535760)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3070807223:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2996 on theBenchmark for (2996ds/7Mi)
% 3.63/0.93 % (535760)Instruction limit reached!
% 3.63/0.93 % (535760)------------------------------
% 3.63/0.93 % (535760)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.63/0.93 % (535760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.63/0.93 % (535760)CaDiCaL version: 2.1.3
% 3.63/0.93 % (535760)Termination reason: Instruction limit
% 3.63/0.93 % (535760)Termination phase: Property scanning
% 3.63/0.93 % (535760)Time elapsed: 0.003 s
% 3.63/0.93 % (535760)Peak memory usage: 10 MB
% 3.63/0.93 % (535760)Instructions burned: 7 (million)
% 3.63/0.93 % (535723)Instruction limit reached!
% 3.63/0.93 % (535723)------------------------------
% 3.63/0.93 % (535723)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.63/0.93 % (535723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.63/0.93 % (535723)CaDiCaL version: 2.1.3
% 3.63/0.93 % (535723)Termination reason: Instruction limit
% 3.63/0.93 % (535723)Termination phase: Saturation
% 3.63/0.93 % (535723)Time elapsed: 0.210 s
% 3.63/0.93 % (535723)Peak memory usage: 12 MB
% 3.63/0.93 % (535723)Instructions burned: 249 (million)
% 3.63/0.93 % (535759)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=318636175:i=42:hud=10:rtra=on_2996 on theBenchmark for (2996ds/42Mi)
% 3.63/0.93 % (535764)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=2255195238:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/181Mi)
% 3.63/0.93 % (535766)dis+10_8_sil=128000:plsq=on:plsqc=1:si=on:sp=unary_first:sos=on:lma=off:plsqr=64,1:uwa=interpreted_only:foolp=on:random_seed=1413733995:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2996 on theBenchmark for (2996ds/169Mi)
% 3.63/1.03 % (535759)Instruction limit reached!
% 3.63/1.03 % (535759)------------------------------
% 3.63/1.03 % (535759)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.63/1.03 % (535759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.63/1.03 % (535759)CaDiCaL version: 2.1.3
% 3.63/1.03 % (535759)Termination reason: Instruction limit
% 3.63/1.03 % (535759)Termination phase: Saturation
% 3.63/1.03 % (535759)Time elapsed: 0.039 s
% 3.63/1.03 % (535759)Peak memory usage: 12 MB
% 3.63/1.03 % (535759)Instructions burned: 43 (million)
% 3.63/1.03 % (535769)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 3.63/1.03 % (535769)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=2223312390:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2996 on theBenchmark for (2996ds/6Mi)
% 3.63/1.03 % (535769)Instruction limit reached!
% 3.63/1.03 % (535769)------------------------------
% 3.63/1.03 % (535769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.63/1.03 % (535769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.63/1.03 % (535769)CaDiCaL version: 2.1.3
% 3.63/1.03 % (535769)Termination reason: Instruction limit
% 3.63/1.03 % (535769)Termination phase: SInE selection
% 3.63/1.03 % (535769)Time elapsed: 0.003 s
% 3.63/1.03 % (535769)Peak memory usage: 10 MB
% 3.63/1.03 % (535769)Instructions burned: 6 (million)
% 3.63/1.03 % (535771)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=4091932350:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2995 on theBenchmark for (2995ds/22Mi)
% 3.63/1.03 % (535771)Instruction limit reached!
% 3.63/1.03 % (535771)------------------------------
% 3.63/1.03 % (535771)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.63/1.03 % (535771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.63/1.03 % (535771)CaDiCaL version: 2.1.3
% 3.63/1.03 % (535771)Termination reason: Instruction limit
% 3.63/1.03 % (535771)Termination phase: Saturation
% 3.63/1.03 % (535771)Time elapsed: 0.012 s
% 3.63/1.03 % (535771)Peak memory usage: 12 MB
% 3.63/1.03 % (535771)Instructions burned: 24 (million)
% 3.63/1.03 % (535764)Instruction limit reached!
% 3.63/1.03 % (535764)------------------------------
% 3.63/1.03 % (535764)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.63/1.03 % (535764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.63/1.03 % (535764)CaDiCaL version: 2.1.3
% 3.63/1.03 % (535764)Termination reason: Instruction limit
% 3.63/1.03 % (535764)Termination phase: Saturation
% 3.63/1.03 % (535764)Time elapsed: 0.089 s
% 3.63/1.03 % (535764)Peak memory usage: 12 MB
% 3.63/1.03 % (535764)Instructions burned: 182 (million)
% 3.63/1.03 % (535754)Instruction limit reached!
% 3.63/1.03 % (535754)------------------------------
% 3.63/1.03 % (535754)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.63/1.03 % (535754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.63/1.03 % (535754)CaDiCaL version: 2.1.3
% 3.63/1.03 % (535754)Termination reason: Instruction limit
% 3.63/1.03 % (535754)Termination phase: Saturation
% 3.63/1.03 % (535754)Time elapsed: 0.129 s
% 3.63/1.03 % (535754)Peak memory usage: 13 MB
% 3.63/1.03 % (535754)Instructions burned: 144 (million)
% 3.63/1.03 % (535773)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=1074332696:i=19:add=on:rtra=on_2995 on theBenchmark for (2995ds/19Mi)
% 3.63/1.03 % (535773)Instruction limit reached!
% 3.63/1.03 % (535773)------------------------------
% 3.63/1.03 % (535773)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.63/1.03 % (535773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.63/1.03 % (535773)CaDiCaL version: 2.1.3
% 3.63/1.03 % (535773)Termination reason: Instruction limit
% 3.63/1.03 % (535773)Termination phase: Saturation
% 3.63/1.03 % (535773)Time elapsed: 0.011 s
% 3.63/1.03 % (535773)Peak memory usage: 12 MB
% 3.63/1.03 % (535773)Instructions burned: 19 (million)
% 3.63/1.03 % (535774)ott+10_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:lma=off:plsqr=128,1:urr=ec_only:uwa=off:rp=on:nwc=20:br=off:random_seed=3105150673:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/316Mi)
% 3.63/1.03 % (535775)dis+1004_4:1_slsqr=1,2:to=lpo:plsq=on:fde=unused:e2e=on:si=on:spb=goal_then_units:acc=on:urr=on:uwa=off:fd=preordered:s2agt=16:slsqc=1:slsq=on:random_seed=1294545903:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2995 on theBenchmark for (2995ds/853Mi)
% 3.63/1.03 % (535755)Instruction limit reached!
% 3.63/1.03 % (535755)------------------------------
% 3.63/1.03 % (535755)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.63/1.03 % (535755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.63/1.03 % (535755)CaDiCaL version: 2.1.3
% 3.63/1.03 % (535755)Termination reason: Instruction limit
% 3.63/1.03 % (535755)Termination phase: Saturation
% 3.63/1.03 % (535755)Time elapsed: 0.165 s
% 3.63/1.03 % (535755)Peak memory usage: 12 MB
% 3.63/1.03 % (535755)Instructions burned: 194 (million)
% 3.63/1.03 % (535777)dis+1003_3:4_to=kbo:plsq=on:prc=on:sims=off:e2e=on:si=on:spb=intro:acc=on:urr=on:uwa=off:foolp=on:s2agt=32:slsqc=3:slsq=on:random_seed=2046501069:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2995 on theBenchmark for (2995ds/45Mi)
% 3.63/1.03 % (535780)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=2012001355:i=480:rtra=on_2994 on theBenchmark for (2994ds/480Mi)
% 3.63/1.03 % (535777)Instruction limit reached!
% 3.63/1.03 % (535777)------------------------------
% 3.63/1.03 % (535777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.63/1.03 % (535777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.63/1.03 % (535777)CaDiCaL version: 2.1.3
% 3.63/1.03 % (535777)Termination reason: Instruction limit
% 3.63/1.03 % (535777)Termination phase: Saturation
% 3.63/1.03 % (535777)Time elapsed: 0.041 s
% 3.63/1.03 % (535777)Peak memory usage: 13 MB
% 3.63/1.03 % (535777)Instructions burned: 45 (million)
% 3.63/1.03 % (535766)Instruction limit reached!
% 3.63/1.03 % (535766)------------------------------
% 3.63/1.03 % (535766)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.63/1.03 % (535766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.63/1.03 % (535766)CaDiCaL version: 2.1.3
% 3.63/1.03 % (535766)Termination reason: Instruction limit
% 3.63/1.03 % (535766)Termination phase: Saturation
% 3.63/1.03 % (535766)Time elapsed: 0.161 s
% 3.63/1.03 % (535766)Peak memory usage: 13 MB
% 3.63/1.03 % (535766)Instructions burned: 170 (million)
% 3.63/1.03 % (535696)Instruction limit reached!
% 3.63/1.03 % (535696)------------------------------
% 3.63/1.03 % (535696)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.63/1.03 % (535696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.63/1.03 % (535696)CaDiCaL version: 2.1.3
% 3.63/1.03 % (535696)Termination reason: Instruction limit
% 3.63/1.03 % (535696)Termination phase: Saturation
% 3.63/1.03 % (535696)Time elapsed: 0.538 s
% 3.63/1.03 % (535696)Peak memory usage: 14 MB
% 3.63/1.03 % (535696)Instructions burned: 634 (million)
% 3.63/1.03 % (535784)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 3.63/1.03 % (535784)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=3849486593:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/200Mi)
% 3.63/1.03 % (535783)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=2439624104:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2994 on theBenchmark for (2994ds/21Mi)
% 3.63/1.03 % (535783)Instruction limit reached!
% 3.63/1.03 % (535783)------------------------------
% 3.63/1.03 % (535783)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.63/1.03 % (535783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.63/1.03 % (535783)CaDiCaL version: 2.1.3
% 3.63/1.03 % (535783)Termination reason: Instruction limit
% 3.63/1.03 % (535783)Termination phase: Saturation
% 3.63/1.03 % (535783)Time elapsed: 0.016 s
% 3.63/1.03 % (535783)Peak memory usage: 12 MB
% 3.63/1.03 % (535783)Instructions burned: 21 (million)
% 3.63/1.03 % (535785)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=3199102466:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2994 on theBenchmark for (2994ds/13Mi)
% 3.63/1.03 % (535785)Instruction limit reached!
% 3.63/1.03 % (535785)------------------------------
% 3.63/1.03 % (535785)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.63/1.03 % (535785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.63/1.03 % (535785)CaDiCaL version: 2.1.3
% 3.63/1.03 % (535785)Termination reason: Instruction limit
% 3.63/1.03 % (535785)Termination phase: Saturation
% 3.63/1.03 % (535785)Time elapsed: 0.012 s
% 3.63/1.03 % (535785)Peak memory usage: 11 MB
% 3.63/1.03 % (535785)Instructions burned: 13 (million)
% 3.63/1.03 % (535788)lrs+1010_1_anc=none:slsqr=1,2:sil=128000:cnfonf=conj_eager:sas=cadical:si=on:hi=on:uwa=one_side_interpreted:rp=on:nwc=2:slsqc=3:slsq=on:random_seed=2126789496:i=66:s2at=3:nm=2:rtra=on:rawr=on_2994 on theBenchmark for (2994ds/66Mi)
% 3.63/1.03 % (535790)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=2247513637:i=51:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/51Mi)
% 3.63/1.03 % (535788)Instruction limit reached!
% 3.63/1.03 % (535788)------------------------------
% 3.63/1.03 % (535788)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.63/1.03 % (535788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.63/1.03 % (535788)CaDiCaL version: 2.1.3
% 3.63/1.03 % (535788)Termination reason: Instruction limit
% 3.63/1.03 % (535788)Termination phase: Saturation
% 3.63/1.03 % (535788)Time elapsed: 0.029 s
% 3.63/1.03 % (535788)Peak memory usage: 12 MB
% 3.63/1.03 % (535788)Instructions burned: 66 (million)
% 3.63/1.03 % (535790)Instruction limit reached!
% 3.63/1.03 % (535790)------------------------------
% 3.63/1.03 % (535790)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.63/1.03 % (535790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.63/1.03 % (535790)CaDiCaL version: 2.1.3
% 3.63/1.03 % (535790)Termination reason: Instruction limit
% 3.63/1.03 % (535790)Termination phase: Saturation
% 3.63/1.03 % (535790)Time elapsed: 0.031 s
% 3.63/1.03 % (535790)Peak memory usage: 12 MB
% 3.63/1.03 % (535790)Instructions burned: 51 (million)
% 3.63/1.03 % (535793)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=680029944:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/31Mi)
% 3.63/1.03 % (535795)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=719444530:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2993 on theBenchmark for (2993ds/137Mi)
% 3.63/1.03 % (535775) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-535688-535775"...
% 3.63/1.03 % (535753) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-535688-535753"...
% 3.63/1.03 % (535793)Refutation not found, incomplete strategy
% 3.63/1.03 % (535793)------------------------------
% 3.63/1.03 % (535793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.63/1.03 % (535793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.63/1.03 % (535793)CaDiCaL version: 2.1.3
% 3.63/1.03 % (535793)Termination reason: Refutation not found, incomplete strategy
% 3.63/1.03 % (535793)Time elapsed: 0.021 s
% 3.63/1.03 % (535793)Peak memory usage: 12 MB
% 3.63/1.03 % (535793)Instructions burned: 24 (million)
% 3.63/1.03 % (535793)------------------------------
% 3.63/1.03 % (535793)------------------------------
% 3.63/1.03 % (535775)...printing done.
% 3.63/1.03 % (535753)...printing done.
% 3.63/1.03 % (535753)Refutation found. Thanks to Tanya!
% 3.63/1.03 % SZS status Theorem for theBenchmark
% 3.63/1.03 % SZS output start Proof for theBenchmark
% 3.63/1.03 thf(type_def_5, type, tyop_2Eextreal_2Eextreal: $tType).
% 3.63/1.03 thf(type_def_6, type, tyop_2Emin_2Ebool: $tType).
% 3.63/1.03 thf(type_def_7, type, tyop_2Emin_2Efun: ($tType * $tType) > $tType).
% 3.63/1.03 thf(type_def_8, type, sTfun: ($tType * $tType) > $tType).
% 3.63/1.03 thf(func_def_0, type, c_2Ebool_2E_21: !>[X0: $tType]:(((X0 > $o) > $o))).
% 3.63/1.03 thf(func_def_1, type, c_2Ebool_2E_2F_5C: ($o > $o > $o)).
% 3.63/1.03 thf(func_def_2, type, c_2Emin_2E_3D: !>[X0: $tType]:((X0 > X0 > $o))).
% 3.63/1.03 thf(func_def_3, type, c_2Emin_2E_3D_3D_3E: ($o > $o > $o)).
% 3.63/1.03 thf(func_def_4, type, c_2Ebool_2E_3F: !>[X0: $tType]:(((X0 > $o) > $o))).
% 3.63/1.03 thf(func_def_5, type, c_2Ebool_2ECOND: !>[X0: $tType]:(($o > X0 > X0 > X0))).
% 3.63/1.03 thf(func_def_6, type, c_2Ebool_2EF: $o).
% 3.63/1.03 thf(func_def_7, type, c_2Ebool_2ET: $o).
% 3.63/1.03 thf(func_def_8, type, c_2Ebool_2E_5C_2F: ($o > $o > $o)).
% 3.63/1.03 thf(func_def_9, type, c_2Eextreal_2Eextreal__le: (tyop_2Eextreal_2Eextreal > tyop_2Eextreal_2Eextreal > $o)).
% 3.63/1.03 thf(func_def_10, type, c_2Eextreal_2Eextreal__max: (tyop_2Eextreal_2Eextreal > tyop_2Eextreal_2Eextreal > tyop_2Eextreal_2Eextreal)).
% 3.63/1.03 thf(func_def_11, type, c_2Ebool_2E_7E: ($o > $o)).
% 3.63/1.03 thf(func_def_13, type, vNOT: ($o > $o)).
% 3.63/1.03 thf(func_def_14, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 3.63/1.03 thf(func_def_15, type, vIFF: ($o > $o > $o)).
% 3.63/1.03 thf(func_def_16, type, db1: !>[X0: $tType]:(X0)).
% 3.63/1.03 thf(func_def_17, type, db0: !>[X0: $tType]:(X0)).
% 3.63/1.03 thf(func_def_18, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 3.63/1.03 thf(func_def_21, type, vIMP: ($o > $o > $o)).
% 3.63/1.03 thf(func_def_22, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 3.63/1.03 thf(func_def_23, type, vAND: ($o > $o > $o)).
% 3.63/1.03 thf(func_def_24, type, db2: !>[X0: $tType]:(X0)).
% 3.63/1.03 thf(func_def_25, type, vOR: ($o > $o > $o)).
% 3.63/1.03 thf(func_def_26, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 3.63/1.03 thf(func_def_27, type, sK0: tyop_2Eextreal_2Eextreal).
% 3.63/1.03 thf(func_def_28, type, sK1: tyop_2Eextreal_2Eextreal).
% 3.63/1.03 thf(func_def_29, type, sK2: tyop_2Eextreal_2Eextreal).
% 3.63/1.03 thf(func_def_31, type, sK4: !>[X0: $tType]:(((X0 > $o) > X0))).
% 3.63/1.03 thf(func_def_32, type, sK5: !>[X0: $tType]:(((X0 > $o) > X0))).
% 3.63/1.03 thf(f8,axiom,(
% 3.63/1.03 c_2Ebool_2ET),
% 3.63/1.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ebool_2ETRUTH)).
% 3.63/1.03 thf(f15,axiom,(
% 3.63/1.03 (c_2Ebool_2ET <=> (~ c_2Ebool_2EF)) & ((~ c_2Ebool_2ET) <=> c_2Ebool_2EF) & ! [X0 : $o] : (X0 <=> (~ (~ X0)))),
% 3.63/1.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ebool_2ENOT__CLAUSES)).
% 3.63/1.03 thf(f18,axiom,(
% 3.63/1.03 ! [X0 : $tType,X1 : X0,X2 : X0] : ((((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2EF @ X1 @ X2)) = X2) & (((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2ET @ X1 @ X2)) = X1))),
% 3.63/1.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ebool_2ECOND__CLAUSES)).
% 3.63/1.03 thf(f22,axiom,(
% 3.63/1.03 ! [X0 : tyop_2Eextreal_2Eextreal,X2 : tyop_2Eextreal_2Eextreal,X1 : tyop_2Eextreal_2Eextreal] : (((c_2Eextreal_2Eextreal__le @ X0 @ X1) & (c_2Eextreal_2Eextreal__le @ X1 @ X2)) => (c_2Eextreal_2Eextreal__le @ X0 @ X2))),
% 3.63/1.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Eextreal_2Ele__trans)).
% 3.63/1.03 thf(f23,axiom,(
% 3.63/1.03 ! [X0 : tyop_2Eextreal_2Eextreal,X1 : tyop_2Eextreal_2Eextreal] : ((c_2Eextreal_2Eextreal__le @ X1 @ X0) | (c_2Eextreal_2Eextreal__le @ X0 @ X1))),
% 3.63/1.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Eextreal_2Ele__total)).
% 3.63/1.03 thf(f24,axiom,(
% 3.63/1.03 ! [X0 : tyop_2Eextreal_2Eextreal,X1 : tyop_2Eextreal_2Eextreal] : (((c_2Eextreal_2Eextreal__max @ X0 @ X1)) = ((c_2Ebool_2ECOND @ tyop_2Eextreal_2Eextreal @ (c_2Eextreal_2Eextreal__le @ X0 @ X1) @ X1 @ X0)))),
% 3.63/1.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Eextreal_2Eextreal__max__def)).
% 3.63/1.03 thf(f35,conjecture,(
% 3.63/1.03 ! [X0 : tyop_2Eextreal_2Eextreal,X2 : tyop_2Eextreal_2Eextreal,X1 : tyop_2Eextreal_2Eextreal] : (((c_2Eextreal_2Eextreal__le @ X2 @ X0) & (c_2Eextreal_2Eextreal__le @ X1 @ X0)) <=> (c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ X1 @ X2) @ X0))),
% 3.63/1.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Eextreal_2Emax__le)).
% 3.63/1.03 thf(f36,negated_conjecture,(
% 3.63/1.03 ~ ! [X0 : tyop_2Eextreal_2Eextreal,X2 : tyop_2Eextreal_2Eextreal,X1 : tyop_2Eextreal_2Eextreal] : (((c_2Eextreal_2Eextreal__le @ X2 @ X0) & (c_2Eextreal_2Eextreal__le @ X1 @ X0)) <=> (c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ X1 @ X2) @ X0))),
% 3.63/1.03 inference(negated_conjecture,[status(cth)],[f35])).
% 3.63/1.03 thf(f41,plain,(
% 3.63/1.03 ! [X0 : tyop_2Eextreal_2Eextreal,X1 : tyop_2Eextreal_2Eextreal,X2 : tyop_2Eextreal_2Eextreal] : (((c_2Eextreal_2Eextreal__le @ X0 @ X2) & (c_2Eextreal_2Eextreal__le @ X2 @ X1)) => (c_2Eextreal_2Eextreal__le @ X0 @ X1))),
% 3.63/1.03 inference(rectify,[],[f22])).
% 3.63/1.03 thf(f42,plain,(
% 3.63/1.03 (((!! @ tyop_2Eextreal_2Eextreal @ (^[Y0 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y1 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y2 : tyop_2Eextreal_2Eextreal]: (((c_2Eextreal_2Eextreal__le @ Y0 @ Y1) & (c_2Eextreal_2Eextreal__le @ Y2 @ Y0)) => (c_2Eextreal_2Eextreal__le @ Y2 @ Y1))))))))) = $true)),
% 3.63/1.03 inference(fool_elimination,[],[f41])).
% 3.63/1.03 thf(f43,plain,(
% 3.63/1.03 (c_2Ebool_2ET <=> (~ c_2Ebool_2EF)) & ((~ c_2Ebool_2ET) <=> c_2Ebool_2EF) & ! [X0 : $o] : (X0 <=> (~ (~ X0)))),
% 3.63/1.03 inference(rectify,[],[f15])).
% 3.63/1.03 thf(f44,plain,(
% 3.63/1.03 (((((!! @ $o @ (^[Y0 : $o]: (Y0 = (~ (~ Y0))))) & ((~ c_2Ebool_2ET) = c_2Ebool_2EF)) & (c_2Ebool_2ET = (~ c_2Ebool_2EF)))) = $true)),
% 3.63/1.03 inference(fool_elimination,[],[f43])).
% 3.63/1.03 thf(f57,plain,(
% 3.63/1.03 ~ ! [X0 : tyop_2Eextreal_2Eextreal,X1 : tyop_2Eextreal_2Eextreal,X2 : tyop_2Eextreal_2Eextreal] : (((c_2Eextreal_2Eextreal__le @ X1 @ X0) & (c_2Eextreal_2Eextreal__le @ X2 @ X0)) <=> (c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ X2 @ X1) @ X0))),
% 3.63/1.03 inference(rectify,[],[f36])).
% 3.63/1.03 thf(f58,plain,(
% 3.63/1.03 ($true = ((~ (!! @ tyop_2Eextreal_2Eextreal @ (^[Y0 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y1 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y2 : tyop_2Eextreal_2Eextreal]: (((c_2Eextreal_2Eextreal__le @ Y0 @ Y2) & (c_2Eextreal_2Eextreal__le @ Y1 @ Y2)) = (c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ Y0 @ Y1) @ Y2)))))))))))),
% 3.63/1.03 inference(fool_elimination,[],[f57])).
% 3.63/1.03 thf(f71,plain,(
% 3.63/1.03 ($true = ((!! @ tyop_2Eextreal_2Eextreal @ (^[Y0 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y1 : tyop_2Eextreal_2Eextreal]: ((c_2Eextreal_2Eextreal__max @ Y1 @ Y0) = (c_2Ebool_2ECOND @ tyop_2Eextreal_2Eextreal @ (c_2Eextreal_2Eextreal__le @ Y1 @ Y0) @ Y0 @ Y1))))))))),
% 3.63/1.03 inference(fool_elimination,[],[f24])).
% 3.63/1.03 thf(f72,plain,(
% 3.63/1.03 c_2Ebool_2ET),
% 3.63/1.03 inference(rectify,[],[f8])).
% 3.63/1.03 thf(f73,plain,(
% 3.63/1.03 (c_2Ebool_2ET = $true)),
% 3.63/1.03 inference(fool_elimination,[],[f72])).
% 3.63/1.03 thf(f80,plain,(
% 3.63/1.03 ( ! [X0 : $tType] : ((((!! @ X0 @ (^[Y0 : X0]: (!! @ X0 @ (^[Y1 : X0]: (((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2ET @ Y1 @ Y0) = Y1) & ((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2EF @ Y1 @ Y0) = Y0))))))) = $true)) )),
% 3.63/1.03 inference(fool_elimination,[],[f18])).
% 3.63/1.03 thf(f81,plain,(
% 3.63/1.03 ! [X0 : tyop_2Eextreal_2Eextreal,X1 : tyop_2Eextreal_2Eextreal] : ((c_2Eextreal_2Eextreal__le @ X1 @ X0) | (c_2Eextreal_2Eextreal__le @ X0 @ X1))),
% 3.63/1.03 inference(rectify,[],[f23])).
% 3.63/1.03 thf(f82,plain,(
% 3.63/1.03 ($true = ((!! @ tyop_2Eextreal_2Eextreal @ (^[Y0 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y1 : tyop_2Eextreal_2Eextreal]: ((c_2Eextreal_2Eextreal__le @ Y1 @ Y0) | (c_2Eextreal_2Eextreal__le @ Y0 @ Y1))))))))),
% 3.63/1.03 inference(fool_elimination,[],[f81])).
% 3.63/1.03 thf(f108,plain,(
% 3.63/1.03 ! [X0 : $tType] : (((!! @ X0 @ (^[Y0 : X0]: (!! @ X0 @ (^[Y1 : X0]: (((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2ET @ Y1 @ Y0) = Y1) & ((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2EF @ Y1 @ Y0) = Y0))))))) = $true)),
% 3.63/1.03 inference(closure,[],[f80])).
% 3.63/1.03 thf(f111,plain,(
% 3.63/1.03 (((((!! @ $o @ (^[Y0 : $o]: (Y0 = (~ (~ Y0))))) & ((~ c_2Ebool_2ET) = c_2Ebool_2EF)) & (c_2Ebool_2ET = (~ c_2Ebool_2EF)))) = $true)),
% 3.63/1.03 inference(cnf_transformation,[],[f44])).
% 3.63/1.03 thf(f123,plain,(
% 3.63/1.03 ( ! [X0 : $tType] : ((((!! @ X0 @ (^[Y0 : X0]: (!! @ X0 @ (^[Y1 : X0]: (((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2ET @ Y1 @ Y0) = Y1) & ((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2EF @ Y1 @ Y0) = Y0))))))) = $true)) )),
% 3.63/1.03 inference(cnf_transformation,[],[f108])).
% 3.63/1.03 thf(f131,plain,(
% 3.63/1.03 ($true = ((!! @ tyop_2Eextreal_2Eextreal @ (^[Y0 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y1 : tyop_2Eextreal_2Eextreal]: ((c_2Eextreal_2Eextreal__le @ Y1 @ Y0) | (c_2Eextreal_2Eextreal__le @ Y0 @ Y1))))))))),
% 3.63/1.03 inference(cnf_transformation,[],[f82])).
% 3.63/1.03 thf(f132,plain,(
% 3.63/1.03 ($true = ((!! @ tyop_2Eextreal_2Eextreal @ (^[Y0 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y1 : tyop_2Eextreal_2Eextreal]: ((c_2Eextreal_2Eextreal__max @ Y1 @ Y0) = (c_2Ebool_2ECOND @ tyop_2Eextreal_2Eextreal @ (c_2Eextreal_2Eextreal__le @ Y1 @ Y0) @ Y0 @ Y1))))))))),
% 3.63/1.03 inference(cnf_transformation,[],[f71])).
% 3.63/1.03 thf(f134,plain,(
% 3.63/1.03 (((!! @ tyop_2Eextreal_2Eextreal @ (^[Y0 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y1 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y2 : tyop_2Eextreal_2Eextreal]: (((c_2Eextreal_2Eextreal__le @ Y0 @ Y1) & (c_2Eextreal_2Eextreal__le @ Y2 @ Y0)) => (c_2Eextreal_2Eextreal__le @ Y2 @ Y1))))))))) = $true)),
% 3.63/1.03 inference(cnf_transformation,[],[f42])).
% 3.63/1.03 thf(f137,plain,(
% 3.63/1.03 ($true = ((~ (!! @ tyop_2Eextreal_2Eextreal @ (^[Y0 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y1 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y2 : tyop_2Eextreal_2Eextreal]: (((c_2Eextreal_2Eextreal__le @ Y0 @ Y2) & (c_2Eextreal_2Eextreal__le @ Y1 @ Y2)) = (c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ Y0 @ Y1) @ Y2)))))))))))),
% 3.63/1.03 inference(cnf_transformation,[],[f58])).
% 3.63/1.03 thf(f142,plain,(
% 3.63/1.03 (c_2Ebool_2ET = $true)),
% 3.63/1.03 inference(cnf_transformation,[],[f73])).
% 3.63/1.03 thf(f146,definition,(
% 3.63/1.03 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 3.63/1.03 introduced(theory,[fool_exhaustiveness_axiom])).
% 3.63/1.03 thf(f147,plain,(
% 3.63/1.03 (((((!! @ $o @ (^[Y0 : $o]: (Y0 = (~ (~ Y0))))) & ((~ $true) = c_2Ebool_2EF)) & ($true = (~ c_2Ebool_2EF)))) = $true)),
% 3.63/1.03 inference(definition_unfolding,[],[f111,f142,f142])).
% 3.63/1.03 thf(f149,plain,(
% 3.63/1.03 ( ! [X0 : $tType] : ((((!! @ X0 @ (^[Y0 : X0]: (!! @ X0 @ (^[Y1 : X0]: (((c_2Ebool_2ECOND @ X0 @ $true @ Y1 @ Y0) = Y1) & ((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2EF @ Y1 @ Y0) = Y0))))))) = $true)) )),
% 3.63/1.03 inference(definition_unfolding,[],[f123,f142])).
% 3.63/1.03 thf(f153,plain,(
% 3.63/1.03 (((((!! @ $o @ (^[Y0 : $o]: (Y0 = (~ (~ Y0))))) & ((~ $true) = c_2Ebool_2EF)) & (~ c_2Ebool_2EF))) = $true)),
% 3.63/1.03 inference(boolean_simplification,[],[f147])).
% 3.63/1.03 thf(f154,plain,(
% 3.63/1.03 (((((!! @ $o @ (^[Y0 : $o]: (Y0 = (~ (~ Y0))))) & ($false = c_2Ebool_2EF)) & (~ c_2Ebool_2EF))) = $true)),
% 3.63/1.03 inference(boolean_simplification,[],[f153])).
% 3.63/1.03 thf(f155,plain,(
% 3.63/1.03 ($true = ((((!! @ $o @ (^[Y0 : $o]: (Y0 = (~ (~ Y0))))) & (~ c_2Ebool_2EF)) & (~ c_2Ebool_2EF))))),
% 3.63/1.03 inference(boolean_simplification,[],[f154])).
% 3.63/1.03 thf(f156,plain,(
% 3.63/1.03 ($true = ((((!! @ $o @ (^[Y0 : $o]: (Y0 = Y0))) & (~ c_2Ebool_2EF)) & (~ c_2Ebool_2EF))))),
% 3.63/1.03 inference(boolean_simplification,[],[f155])).
% 3.63/1.03 thf(f157,plain,(
% 3.63/1.03 (((((!! @ $o @ (^[Y0 : $o]: ($true))) & (~ c_2Ebool_2EF)) & (~ c_2Ebool_2EF))) = $true)),
% 3.63/1.03 inference(boolean_simplification,[],[f156])).
% 3.63/1.03 thf(f173,plain,(
% 3.63/1.03 (((!! @ tyop_2Eextreal_2Eextreal @ (^[Y0 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y1 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y2 : tyop_2Eextreal_2Eextreal]: (((c_2Eextreal_2Eextreal__le @ Y0 @ Y2) & (c_2Eextreal_2Eextreal__le @ Y1 @ Y2)) = (c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ Y0 @ Y1) @ Y2))))))))) = $false)),
% 3.63/1.03 inference(not_proxy_clausification,[],[f137])).
% 3.63/1.03 thf(f174,plain,(
% 3.63/1.03 (((~ c_2Ebool_2EF)) = $true)),
% 3.63/1.03 inference(and_proxy_clausification,[],[f157])).
% 3.63/1.03 thf(f178,plain,(
% 3.63/1.03 (c_2Ebool_2EF = $false)),
% 3.63/1.03 inference(not_proxy_clausification,[],[f174])).
% 3.63/1.03 thf(f180,plain,(
% 3.63/1.03 ($false = (((^[Y0 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y1 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y2 : tyop_2Eextreal_2Eextreal]: (((c_2Eextreal_2Eextreal__le @ Y0 @ Y2) & (c_2Eextreal_2Eextreal__le @ Y1 @ Y2)) = (c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ Y0 @ Y1) @ Y2))))))) @ sK0)))),
% 3.63/1.03 inference(sigma_proxy_clausification,[],[f173])).
% 3.63/1.03 thf(f181,plain,(
% 3.63/1.03 (((!! @ tyop_2Eextreal_2Eextreal @ (^[Y0 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y1 : tyop_2Eextreal_2Eextreal]: (((c_2Eextreal_2Eextreal__le @ sK0 @ Y1) & (c_2Eextreal_2Eextreal__le @ Y0 @ Y1)) = (c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ sK0 @ Y0) @ Y1))))))) = $false)),
% 3.63/1.03 inference(beta-eta_normalization,[],[f180])).
% 3.63/1.03 thf(f182,plain,(
% 3.63/1.03 ((((^[Y0 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y1 : tyop_2Eextreal_2Eextreal]: (((c_2Eextreal_2Eextreal__le @ sK0 @ Y1) & (c_2Eextreal_2Eextreal__le @ Y0 @ Y1)) = (c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ sK0 @ Y0) @ Y1))))) @ sK1)) = $false)),
% 3.63/1.03 inference(sigma_proxy_clausification,[],[f181])).
% 3.63/1.03 thf(f183,plain,(
% 3.63/1.03 (((!! @ tyop_2Eextreal_2Eextreal @ (^[Y0 : tyop_2Eextreal_2Eextreal]: (((c_2Eextreal_2Eextreal__le @ sK0 @ Y0) & (c_2Eextreal_2Eextreal__le @ sK1 @ Y0)) = (c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ sK0 @ sK1) @ Y0))))) = $false)),
% 3.63/1.03 inference(beta-eta_normalization,[],[f182])).
% 3.63/1.03 thf(f184,plain,(
% 3.63/1.03 ($false = (((^[Y0 : tyop_2Eextreal_2Eextreal]: (((c_2Eextreal_2Eextreal__le @ sK0 @ Y0) & (c_2Eextreal_2Eextreal__le @ sK1 @ Y0)) = (c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ sK0 @ sK1) @ Y0))) @ sK2)))),
% 3.63/1.03 inference(sigma_proxy_clausification,[],[f183])).
% 3.63/1.03 thf(f185,plain,(
% 3.63/1.03 (((((c_2Eextreal_2Eextreal__le @ sK0 @ sK2) & (c_2Eextreal_2Eextreal__le @ sK1 @ sK2)) = (c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ sK0 @ sK1) @ sK2))) = $false)),
% 3.63/1.03 inference(beta-eta_normalization,[],[f184])).
% 3.63/1.03 thf(f202,plain,(
% 3.63/1.03 ($false = ((((c_2Eextreal_2Eextreal__le @ sK0 @ sK2) & $true) = (c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ sK0 @ sK1) @ sK2)))) | (((c_2Eextreal_2Eextreal__le @ sK1 @ sK2)) = $false)),
% 3.63/1.03 inference(superposition,[],[f185,f146])).
% 3.63/1.03 thf(f203,plain,(
% 3.63/1.03 (((($true & (c_2Eextreal_2Eextreal__le @ sK1 @ sK2)) = (c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ sK0 @ sK1) @ sK2))) = $false) | (((c_2Eextreal_2Eextreal__le @ sK0 @ sK2)) = $false)),
% 3.63/1.03 inference(superposition,[],[f185,f146])).
% 3.63/1.03 thf(f206,plain,(
% 3.63/1.03 ((((c_2Eextreal_2Eextreal__le @ sK1 @ sK2) = (c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ sK0 @ sK1) @ sK2))) = $false) | (((c_2Eextreal_2Eextreal__le @ sK0 @ sK2)) = $false)),
% 3.63/1.03 inference(boolean_simplification,[],[f203])).
% 3.63/1.03 thf(f210,plain,(
% 3.63/1.03 ((((c_2Eextreal_2Eextreal__le @ sK0 @ sK2) = (c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ sK0 @ sK1) @ sK2))) = $false) | (((c_2Eextreal_2Eextreal__le @ sK1 @ sK2)) = $false)),
% 3.63/1.03 inference(boolean_simplification,[],[f202])).
% 3.63/1.03 thf(f212,definition,(
% 3.63/1.03 spl3_1 <=> (((c_2Eextreal_2Eextreal__le @ sK0 @ sK2)) = $false)),
% 3.63/1.03 introduced(definition,[new_symbols(definition,[spl3_1])],[avatar_definition])).
% 3.63/1.03 thf(f213,plain,(
% 3.63/1.03 (((c_2Eextreal_2Eextreal__le @ sK0 @ sK2)) != $false) | spl3_1),
% 3.63/1.03 inference(avatar_component_clause,[],[f212])).
% 3.63/1.03 thf(f214,plain,(
% 3.63/1.03 (((c_2Eextreal_2Eextreal__le @ sK0 @ sK2)) = $false) | ~spl3_1),
% 3.63/1.03 inference(avatar_component_clause,[],[f212])).
% 3.63/1.03 thf(f216,definition,(
% 3.63/1.03 spl3_2 <=> ((((c_2Eextreal_2Eextreal__le @ sK1 @ sK2) = (c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ sK0 @ sK1) @ sK2))) = $false)),
% 3.63/1.03 introduced(definition,[new_symbols(definition,[spl3_2])],[avatar_definition])).
% 3.63/1.03 thf(f218,plain,(
% 3.63/1.03 ((((c_2Eextreal_2Eextreal__le @ sK1 @ sK2) = (c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ sK0 @ sK1) @ sK2))) = $false) | ~spl3_2),
% 3.63/1.03 inference(avatar_component_clause,[],[f216])).
% 3.63/1.03 thf(f219,plain,(
% 3.63/1.03 spl3_1 | spl3_2),
% 3.63/1.03 inference(avatar_split_clause,[],[f206,f216,f212])).
% 3.63/1.03 thf(f223,definition,(
% 3.63/1.03 spl3_3 <=> ((((c_2Eextreal_2Eextreal__le @ sK0 @ sK2) = (c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ sK0 @ sK1) @ sK2))) = $false)),
% 3.63/1.03 introduced(definition,[new_symbols(definition,[spl3_3])],[avatar_definition])).
% 3.63/1.03 thf(f225,plain,(
% 3.63/1.03 ((((c_2Eextreal_2Eextreal__le @ sK0 @ sK2) = (c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ sK0 @ sK1) @ sK2))) = $false) | ~spl3_3),
% 3.63/1.03 inference(avatar_component_clause,[],[f223])).
% 3.63/1.03 thf(f227,definition,(
% 3.63/1.03 spl3_4 <=> (((c_2Eextreal_2Eextreal__le @ sK1 @ sK2)) = $false)),
% 3.63/1.03 introduced(definition,[new_symbols(definition,[spl3_4])],[avatar_definition])).
% 3.63/1.03 thf(f229,plain,(
% 3.63/1.03 (((c_2Eextreal_2Eextreal__le @ sK1 @ sK2)) = $false) | ~spl3_4),
% 3.63/1.03 inference(avatar_component_clause,[],[f227])).
% 3.63/1.03 thf(f230,plain,(
% 3.63/1.03 spl3_3 | spl3_4),
% 3.63/1.03 inference(avatar_split_clause,[],[f210,f227,f223])).
% 3.63/1.03 thf(f232,definition,(
% 3.63/1.03 spl3_5 <=> ($false = ((c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ sK0 @ sK1) @ sK2)))),
% 3.63/1.03 introduced(definition,[new_symbols(definition,[spl3_5])],[avatar_definition])).
% 3.63/1.03 thf(f233,plain,(
% 3.63/1.03 ($false != ((c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ sK0 @ sK1) @ sK2))) | spl3_5),
% 3.63/1.03 inference(avatar_component_clause,[],[f232])).
% 3.63/1.03 thf(f234,plain,(
% 3.63/1.03 ($false = ((c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ sK0 @ sK1) @ sK2))) | ~spl3_5),
% 3.63/1.03 inference(avatar_component_clause,[],[f232])).
% 3.63/1.03 thf(f414,plain,(
% 3.63/1.03 ( ! [X1 : tyop_2Eextreal_2Eextreal] : (($true = (((^[Y0 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y1 : tyop_2Eextreal_2Eextreal]: ((c_2Eextreal_2Eextreal__le @ Y1 @ Y0) | (c_2Eextreal_2Eextreal__le @ Y0 @ Y1))))) @ X1)))) )),
% 3.63/1.03 inference(pi_proxy_clausification,[],[f131])).
% 3.63/1.03 thf(f417,plain,(
% 3.63/1.03 ( ! [X1 : tyop_2Eextreal_2Eextreal] : ((((!! @ tyop_2Eextreal_2Eextreal @ (^[Y0 : tyop_2Eextreal_2Eextreal]: ((c_2Eextreal_2Eextreal__le @ Y0 @ X1) | (c_2Eextreal_2Eextreal__le @ X1 @ Y0))))) = $true)) )),
% 3.63/1.03 inference(beta-eta_normalization,[],[f414])).
% 3.63/1.03 thf(f418,plain,(
% 3.63/1.03 ( ! [X2 : tyop_2Eextreal_2Eextreal,X1 : tyop_2Eextreal_2Eextreal] : (($true = (((^[Y0 : tyop_2Eextreal_2Eextreal]: ((c_2Eextreal_2Eextreal__le @ Y0 @ X1) | (c_2Eextreal_2Eextreal__le @ X1 @ Y0))) @ X2)))) )),
% 3.63/1.03 inference(pi_proxy_clausification,[],[f417])).
% 3.63/1.03 thf(f420,plain,(
% 3.63/1.03 ( ! [X2 : tyop_2Eextreal_2Eextreal,X1 : tyop_2Eextreal_2Eextreal] : (($true = (((c_2Eextreal_2Eextreal__le @ X2 @ X1) | (c_2Eextreal_2Eextreal__le @ X1 @ X2))))) )),
% 3.63/1.03 inference(beta-eta_normalization,[],[f418])).
% 3.63/1.03 thf(f422,plain,(
% 3.63/1.03 ( ! [X2 : tyop_2Eextreal_2Eextreal,X1 : tyop_2Eextreal_2Eextreal] : (($true = ((c_2Eextreal_2Eextreal__le @ X2 @ X1))) | (((c_2Eextreal_2Eextreal__le @ X1 @ X2)) = $true)) )),
% 3.63/1.03 inference(or_proxy_clausification,[],[f420])).
% 3.63/1.03 thf(f524,plain,(
% 3.63/1.03 ( ! [X1 : tyop_2Eextreal_2Eextreal] : (((((^[Y0 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y1 : tyop_2Eextreal_2Eextreal]: ((c_2Eextreal_2Eextreal__max @ Y1 @ Y0) = (c_2Ebool_2ECOND @ tyop_2Eextreal_2Eextreal @ (c_2Eextreal_2Eextreal__le @ Y1 @ Y0) @ Y0 @ Y1))))) @ X1)) = $true)) )),
% 3.63/1.03 inference(pi_proxy_clausification,[],[f132])).
% 3.63/1.03 thf(f526,plain,(
% 3.63/1.03 ( ! [X1 : tyop_2Eextreal_2Eextreal] : ((((!! @ tyop_2Eextreal_2Eextreal @ (^[Y0 : tyop_2Eextreal_2Eextreal]: ((c_2Eextreal_2Eextreal__max @ Y0 @ X1) = (c_2Ebool_2ECOND @ tyop_2Eextreal_2Eextreal @ (c_2Eextreal_2Eextreal__le @ Y0 @ X1) @ X1 @ Y0))))) = $true)) )),
% 3.63/1.03 inference(beta-eta_normalization,[],[f524])).
% 3.63/1.03 thf(f531,plain,(
% 3.63/1.03 ( ! [X2 : tyop_2Eextreal_2Eextreal,X1 : tyop_2Eextreal_2Eextreal] : (($true = (((^[Y0 : tyop_2Eextreal_2Eextreal]: ((c_2Eextreal_2Eextreal__max @ Y0 @ X1) = (c_2Ebool_2ECOND @ tyop_2Eextreal_2Eextreal @ (c_2Eextreal_2Eextreal__le @ Y0 @ X1) @ X1 @ Y0))) @ X2)))) )),
% 3.63/1.03 inference(pi_proxy_clausification,[],[f526])).
% 3.63/1.03 thf(f534,plain,(
% 3.63/1.03 ( ! [X2 : tyop_2Eextreal_2Eextreal,X1 : tyop_2Eextreal_2Eextreal] : (((((c_2Eextreal_2Eextreal__max @ X2 @ X1) = (c_2Ebool_2ECOND @ tyop_2Eextreal_2Eextreal @ (c_2Eextreal_2Eextreal__le @ X2 @ X1) @ X1 @ X2))) = $true)) )),
% 3.63/1.03 inference(beta-eta_normalization,[],[f531])).
% 3.63/1.03 thf(f535,plain,(
% 3.63/1.03 ( ! [X2 : tyop_2Eextreal_2Eextreal,X1 : tyop_2Eextreal_2Eextreal] : ((((c_2Ebool_2ECOND @ tyop_2Eextreal_2Eextreal @ (c_2Eextreal_2Eextreal__le @ X2 @ X1) @ X1 @ X2)) = ((c_2Eextreal_2Eextreal__max @ X2 @ X1)))) )),
% 3.63/1.03 inference(equality_proxy_clausification,[],[f534])).
% 3.63/1.03 thf(f543,plain,(
% 3.63/1.03 ( ! [X0 : tyop_2Eextreal_2Eextreal,X1 : tyop_2Eextreal_2Eextreal] : ((((c_2Eextreal_2Eextreal__le @ X0 @ X1)) = $false) | (((c_2Eextreal_2Eextreal__max @ X0 @ X1)) = ((c_2Ebool_2ECOND @ tyop_2Eextreal_2Eextreal @ $true @ X1 @ X0)))) )),
% 3.63/1.03 inference(superposition,[],[f535,f146])).
% 3.63/1.03 thf(f676,plain,(
% 3.63/1.03 ( ! [X1 : tyop_2Eextreal_2Eextreal] : (($true = (((^[Y0 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y1 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y2 : tyop_2Eextreal_2Eextreal]: (((c_2Eextreal_2Eextreal__le @ Y0 @ Y1) & (c_2Eextreal_2Eextreal__le @ Y2 @ Y0)) => (c_2Eextreal_2Eextreal__le @ Y2 @ Y1))))))) @ X1)))) )),
% 3.63/1.03 inference(pi_proxy_clausification,[],[f134])).
% 3.63/1.03 thf(f679,plain,(
% 3.63/1.03 ( ! [X1 : tyop_2Eextreal_2Eextreal] : (($true = ((!! @ tyop_2Eextreal_2Eextreal @ (^[Y0 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y1 : tyop_2Eextreal_2Eextreal]: (((c_2Eextreal_2Eextreal__le @ X1 @ Y0) & (c_2Eextreal_2Eextreal__le @ Y1 @ X1)) => (c_2Eextreal_2Eextreal__le @ Y1 @ Y0))))))))) )),
% 3.63/1.03 inference(beta-eta_normalization,[],[f676])).
% 3.63/1.03 thf(f692,plain,(
% 3.63/1.03 ( ! [X2 : tyop_2Eextreal_2Eextreal,X1 : tyop_2Eextreal_2Eextreal] : (((((^[Y0 : tyop_2Eextreal_2Eextreal]: (!! @ tyop_2Eextreal_2Eextreal @ (^[Y1 : tyop_2Eextreal_2Eextreal]: (((c_2Eextreal_2Eextreal__le @ X1 @ Y0) & (c_2Eextreal_2Eextreal__le @ Y1 @ X1)) => (c_2Eextreal_2Eextreal__le @ Y1 @ Y0))))) @ X2)) = $true)) )),
% 3.63/1.03 inference(pi_proxy_clausification,[],[f679])).
% 3.63/1.03 thf(f695,plain,(
% 3.63/1.03 ( ! [X2 : tyop_2Eextreal_2Eextreal,X1 : tyop_2Eextreal_2Eextreal] : ((((!! @ tyop_2Eextreal_2Eextreal @ (^[Y0 : tyop_2Eextreal_2Eextreal]: (((c_2Eextreal_2Eextreal__le @ X1 @ X2) & (c_2Eextreal_2Eextreal__le @ Y0 @ X1)) => (c_2Eextreal_2Eextreal__le @ Y0 @ X2))))) = $true)) )),
% 3.63/1.03 inference(beta-eta_normalization,[],[f692])).
% 3.63/1.03 thf(f696,plain,(
% 3.63/1.03 ( ! [X2 : tyop_2Eextreal_2Eextreal,X3 : tyop_2Eextreal_2Eextreal,X1 : tyop_2Eextreal_2Eextreal] : (($true = (((^[Y0 : tyop_2Eextreal_2Eextreal]: (((c_2Eextreal_2Eextreal__le @ X1 @ X2) & (c_2Eextreal_2Eextreal__le @ Y0 @ X1)) => (c_2Eextreal_2Eextreal__le @ Y0 @ X2))) @ X3)))) )),
% 3.63/1.03 inference(pi_proxy_clausification,[],[f695])).
% 3.63/1.03 thf(f698,plain,(
% 3.63/1.03 ( ! [X2 : tyop_2Eextreal_2Eextreal,X3 : tyop_2Eextreal_2Eextreal,X1 : tyop_2Eextreal_2Eextreal] : (($true = ((((c_2Eextreal_2Eextreal__le @ X1 @ X2) & (c_2Eextreal_2Eextreal__le @ X3 @ X1)) => (c_2Eextreal_2Eextreal__le @ X3 @ X2))))) )),
% 3.63/1.03 inference(beta-eta_normalization,[],[f696])).
% 3.63/1.03 thf(f700,plain,(
% 3.63/1.03 ( ! [X2 : tyop_2Eextreal_2Eextreal,X3 : tyop_2Eextreal_2Eextreal,X1 : tyop_2Eextreal_2Eextreal] : (((((c_2Eextreal_2Eextreal__le @ X1 @ X2) & (c_2Eextreal_2Eextreal__le @ X3 @ X1))) = $false) | ($true = ((c_2Eextreal_2Eextreal__le @ X3 @ X2)))) )),
% 3.63/1.03 inference(imp_proxy_clausification,[],[f698])).
% 3.63/1.03 thf(f701,plain,(
% 3.63/1.03 ( ! [X2 : tyop_2Eextreal_2Eextreal,X3 : tyop_2Eextreal_2Eextreal,X1 : tyop_2Eextreal_2Eextreal] : (($true = ((c_2Eextreal_2Eextreal__le @ X3 @ X2))) | (((c_2Eextreal_2Eextreal__le @ X1 @ X2)) = $false) | (((c_2Eextreal_2Eextreal__le @ X3 @ X1)) = $false)) )),
% 3.63/1.03 inference(and_proxy_clausification,[],[f700])).
% 3.63/1.03 thf(f722,plain,(
% 3.63/1.03 ( ! [X0 : tyop_2Eextreal_2Eextreal] : ((((c_2Eextreal_2Eextreal__le @ sK1 @ X0)) = $false) | (((c_2Eextreal_2Eextreal__le @ X0 @ sK2)) = $false) | ($false = ((((c_2Eextreal_2Eextreal__le @ sK0 @ sK2) & $true) = (c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ sK0 @ sK1) @ sK2))))) )),
% 3.63/1.03 inference(superposition,[],[f185,f701])).
% 3.63/1.03 thf(f728,plain,(
% 3.63/1.03 ( ! [X0 : tyop_2Eextreal_2Eextreal] : ((((c_2Eextreal_2Eextreal__le @ sK1 @ X0)) = $false) | ((((c_2Eextreal_2Eextreal__le @ sK0 @ sK2) = (c_2Eextreal_2Eextreal__le @ (c_2Eextreal_2Eextreal__max @ sK0 @ sK1) @ sK2))) = $false) | (((c_2Eextreal_2Eextreal__le @ X0 @ sK2)) = $false)) )),
% 3.63/1.03 inference(boolean_simplification,[],[f722])).
% 3.63/1.03 thf(f949,plain,(
% 3.63/1.03 ( ! [X0 : $tType,X1 : X0] : (((((^[Y0 : X0]: (!! @ X0 @ (^[Y1 : X0]: (((c_2Ebool_2ECOND @ X0 @ $true @ Y1 @ Y0) = Y1) & ((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2EF @ Y1 @ Y0) = Y0))))) @ X1)) = $true)) )),
% 3.63/1.03 inference(pi_proxy_clausification,[],[f149])).
% 3.63/1.03 thf(f951,plain,(
% 3.63/1.03 ( ! [X0 : $tType,X1 : X0] : (($true = ((!! @ X0 @ (^[Y0 : X0]: (((c_2Ebool_2ECOND @ X0 @ $true @ Y0 @ X1) = Y0) & ((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2EF @ Y0 @ X1) = X1))))))) )),
% 3.63/1.03 inference(beta-eta_normalization,[],[f949])).
% 3.63/1.03 thf(f971,plain,(
% 3.63/1.03 ( ! [X0 : $tType,X2 : X0,X1 : X0] : (((((^[Y0 : X0]: (((c_2Ebool_2ECOND @ X0 @ $true @ Y0 @ X1) = Y0) & ((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2EF @ Y0 @ X1) = X1))) @ X2)) = $true)) )),
% 3.63/1.03 inference(pi_proxy_clausification,[],[f951])).
% 3.63/1.03 thf(f973,plain,(
% 3.63/1.03 ( ! [X0 : $tType,X2 : X0,X1 : X0] : (($true = ((((c_2Ebool_2ECOND @ X0 @ $true @ X2 @ X1) = X2) & ((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2EF @ X2 @ X1) = X1))))) )),
% 3.63/1.03 inference(beta-eta_normalization,[],[f971])).
% 3.63/1.03 thf(f975,plain,(
% 3.63/1.03 ( ! [X0 : $tType,X2 : X0,X1 : X0] : ((((((c_2Ebool_2ECOND @ X0 @ $true @ X2 @ X1) = X2) & ((c_2Ebool_2ECOND @ X0 @ $false @ X2 @ X1) = X1))) = $true)) )),
% 3.63/1.03 inference(forward_demodulation,[],[f973,f178])).
% 3.63/1.03 thf(f976,plain,(
% 3.63/1.03 ( ! [X0 : $tType,X2 : X0,X1 : X0] : (($true = (((c_2Ebool_2ECOND @ X0 @ $false @ X2 @ X1) = X1)))) )),
% 3.63/1.03 inference(and_proxy_clausification,[],[f975])).
% 3.63/1.03 thf(f977,plain,(
% 3.63/1.03 ( ! [X0 : $tType,X2 : X0,X1 : X0] : (((((c_2Ebool_2ECOND @ X0 @ $true @ X2 @ X1) = X2)) = $true)) )),
% 3.63/1.03 inference(and_proxy_clausification,[],[f975])).
% 3.63/1.03 thf(f978,plain,(
% 3.63/1.03 ( ! [X0 : $tType,X2 : X0,X1 : X0] : ((((c_2Ebool_2ECOND @ X0 @ $false @ X2 @ X1)) = X1)) )),
% 3.63/1.03 inference(equality_proxy_clausification,[],[f976])).
% 3.63/1.03 thf(f979,plain,(
% 3.63/1.03 ( ! [X0 : $tType,X2 : X0,X1 : X0] : ((((c_2Ebool_2ECOND @ X0 @ $true @ X2 @ X1)) = X2)) )),
% 3.63/1.03 inference(equality_proxy_clausification,[],[f977])).
% 3.63/1.03 thf(f4334,definition,(
% 3.63/1.03 spl3_73 <=> ! [X0 : tyop_2Eextreal_2Eextreal] : ((((c_2Eextreal_2Eextreal__le @ X0 @ sK2)) = $false) | (((c_2Eextreal_2Eextreal__le @ sK0 @ X0)) = $false))),
% 3.63/1.03 introduced(definition,[new_symbols(definition,[spl3_73])],[avatar_definition])).
% 3.63/1.03 thf(f4335,plain,(
% 3.63/1.03 ( ! [X0 : tyop_2Eextreal_2Eextreal] : ((((c_2Eextreal_2Eextreal__le @ sK0 @ X0)) = $false) | (((c_2Eextreal_2Eextreal__le @ X0 @ sK2)) = $false)) ) | ~spl3_73),
% 3.63/1.03 inference(avatar_component_clause,[],[f4334])).
% 3.63/1.03 thf(f4345,definition,(
% 3.63/1.03 spl3_75 <=> ! [X0 : tyop_2Eextreal_2Eextreal] : ((((c_2Eextreal_2Eextreal__le @ sK1 @ X0)) = $false) | (((c_2Eextreal_2Eextreal__le @ X0 @ sK2)) = $false))),
% 3.63/1.03 introduced(definition,[new_symbols(definition,[spl3_75])],[avatar_definition])).
% 3.63/1.03 thf(f4346,plain,(
% 3.63/1.03 ( ! [X0 : tyop_2Eextreal_2Eextreal] : ((((c_2Eextreal_2Eextreal__le @ sK1 @ X0)) = $false) | (((c_2Eextreal_2Eextreal__le @ X0 @ sK2)) = $false)) ) | ~spl3_75),
% 3.63/1.03 inference(avatar_component_clause,[],[f4345])).
% 3.63/1.03 thf(f4347,plain,(
% 3.63/1.03 spl3_3 | spl3_75),
% 3.63/1.03 inference(avatar_split_clause,[],[f728,f4345,f223])).
% 3.63/1.03 thf(f4382,plain,(
% 3.63/1.03 ( ! [X0 : tyop_2Eextreal_2Eextreal] : ((((c_2Eextreal_2Eextreal__le @ X0 @ sK2)) = $false) | ($true = $false) | (((c_2Eextreal_2Eextreal__le @ sK0 @ X0)) = $false)) ) | ~spl3_1),
% 3.63/1.03 inference(superposition,[],[f214,f701])).
% 3.63/1.03 thf(f4389,plain,(
% 3.63/1.03 ( ! [X0 : tyop_2Eextreal_2Eextreal] : ((((c_2Eextreal_2Eextreal__le @ X0 @ sK2)) = $false) | (((c_2Eextreal_2Eextreal__le @ sK0 @ X0)) = $false)) ) | ~spl3_1),
% 3.63/1.03 inference(trivial_inequality_removal,[],[f4382])).
% 3.63/1.03 thf(f4397,plain,(
% 3.63/1.03 spl3_73 | ~spl3_1),
% 3.63/1.03 inference(avatar_split_clause,[],[f4389,f212,f4334])).
% 3.63/1.03 thf(f4407,plain,(
% 3.63/1.03 (((((c_2Eextreal_2Eextreal__le @ sK0 @ sK2) & (c_2Eextreal_2Eextreal__le @ sK1 @ sK2)) = $false)) = $false) | ~spl3_5),
% 3.63/1.03 inference(superposition,[],[f185,f234])).
% 3.63/1.03 thf(f4415,plain,(
% 3.63/1.03 (((~ ((c_2Eextreal_2Eextreal__le @ sK0 @ sK2) & (c_2Eextreal_2Eextreal__le @ sK1 @ sK2)))) = $false) | ~spl3_5),
% 3.63/1.03 inference(boolean_simplification,[],[f4407])).
% 3.63/1.03 thf(f4420,plain,(
% 3.63/1.03 (((~ ($false & (c_2Eextreal_2Eextreal__le @ sK1 @ sK2)))) = $false) | (~spl3_1 | ~spl3_5)),
% 3.63/1.03 inference(forward_demodulation,[],[f4415,f214])).
% 3.63/1.03 thf(f4421,plain,(
% 3.63/1.03 ($false = ((~ $false))) | (~spl3_1 | ~spl3_5)),
% 3.63/1.03 inference(boolean_simplification,[],[f4420])).
% 3.63/1.03 thf(f4422,plain,(
% 3.63/1.03 ($true = $false) | (~spl3_1 | ~spl3_5)),
% 3.63/1.03 inference(boolean_simplification,[],[f4421])).
% 3.63/1.03 thf(f4423,plain,(
% 3.63/1.03 $false | (~spl3_1 | ~spl3_5)),
% 3.63/1.03 inference(trivial_inequality_removal,[],[f4422])).
% 3.63/1.03 thf(f4424,plain,(
% 3.63/1.03 ~spl3_1 | ~spl3_5),
% 3.63/1.03 inference(avatar_contradiction_clause,[],[f4423])).
% 3.63/1.03 thf(f4496,plain,(
% 3.63/1.03 ( ! [X0 : tyop_2Eextreal_2Eextreal] : (($true = $false) | (((c_2Eextreal_2Eextreal__le @ X0 @ sK2)) = $false) | ($true = ((c_2Eextreal_2Eextreal__le @ X0 @ sK1)))) ) | ~spl3_75),
% 3.63/1.03 inference(superposition,[],[f4346,f422])).
% 3.63/1.03 thf(f4510,plain,(
% 3.63/1.03 ( ! [X0 : tyop_2Eextreal_2Eextreal] : (($true = ((c_2Eextreal_2Eextreal__le @ X0 @ sK1))) | (((c_2Eextreal_2Eextreal__le @ X0 @ sK2)) = $false)) ) | ~spl3_75),
% 3.63/1.03 inference(trivial_inequality_removal,[],[f4496])).
% 3.63/1.03 thf(f4624,plain,(
% 3.63/1.03 ( ! [X0 : tyop_2Eextreal_2Eextreal] : ((((c_2Ebool_2ECOND @ tyop_2Eextreal_2Eextreal @ $true @ sK1 @ X0)) = ((c_2Eextreal_2Eextreal__max @ X0 @ sK1))) | (((c_2Eextreal_2Eextreal__le @ X0 @ sK2)) = $false)) ) | ~spl3_75),
% 3.63/1.03 inference(superposition,[],[f535,f4510])).
% 3.63/1.03 thf(f4629,plain,(
% 3.63/1.03 ( ! [X0 : tyop_2Eextreal_2Eextreal] : ((((c_2Eextreal_2Eextreal__max @ X0 @ sK1)) = sK1) | (((c_2Eextreal_2Eextreal__le @ X0 @ sK2)) = $false)) ) | ~spl3_75),
% 3.63/1.03 inference(forward_demodulation,[],[f4624,f979])).
% 3.63/1.03 thf(f4852,plain,(
% 3.63/1.03 (((c_2Eextreal_2Eextreal__le @ sK0 @ sK2)) = $false) | (((c_2Eextreal_2Eextreal__le @ sK1 @ sK2)) != $false) | (spl3_5 | ~spl3_75)),
% 3.63/1.03 inference(superposition,[],[f233,f4629])).
% 3.63/1.03 thf(f4864,plain,(
% 3.63/1.03 (((c_2Eextreal_2Eextreal__le @ sK0 @ sK2)) = $false) | (~spl3_4 | spl3_5 | ~spl3_75)),
% 3.63/1.03 inference(forward_subsumption_resolution,[],[f4852,f229])).
% 3.63/1.03 thf(f4875,plain,(
% 3.63/1.03 $false | (spl3_1 | ~spl3_4 | spl3_5 | ~spl3_75)),
% 3.63/1.03 inference(forward_subsumption_resolution,[],[f4864,f213])).
% 3.63/1.03 thf(f4876,plain,(
% 3.63/1.03 spl3_1 | ~spl3_4 | spl3_5 | ~spl3_75),
% 3.63/1.03 inference(avatar_contradiction_clause,[],[f4875])).
% 3.63/1.03 thf(f5062,definition,(
% 3.63/1.03 spl3_92 <=> (((c_2Eextreal_2Eextreal__le @ sK0 @ sK1)) = $false)),
% 3.63/1.03 introduced(definition,[new_symbols(definition,[spl3_92])],[avatar_definition])).
% 3.63/1.03 thf(f5063,plain,(
% 3.63/1.03 (((c_2Eextreal_2Eextreal__le @ sK0 @ sK1)) = $false) | ~spl3_92),
% 3.63/1.03 inference(avatar_component_clause,[],[f5062])).
% 3.63/1.03 thf(f5064,plain,(
% 3.63/1.03 (((c_2Eextreal_2Eextreal__le @ sK0 @ sK1)) != $false) | spl3_92),
% 3.63/1.03 inference(avatar_component_clause,[],[f5062])).
% 3.63/1.03 thf(f5122,plain,(
% 3.63/1.03 ( ! [X0 : tyop_2Eextreal_2Eextreal,X1 : tyop_2Eextreal_2Eextreal] : ((((c_2Eextreal_2Eextreal__max @ X0 @ X1)) = X1) | (((c_2Eextreal_2Eextreal__le @ X0 @ X1)) = $false)) )),
% 3.63/1.03 inference(forward_demodulation,[],[f543,f979])).
% 3.63/1.03 thf(f5294,plain,(
% 3.63/1.03 (((c_2Eextreal_2Eextreal__max @ sK0 @ sK1)) = ((c_2Ebool_2ECOND @ tyop_2Eextreal_2Eextreal @ $false @ sK1 @ sK0))) | ~spl3_92),
% 3.63/1.03 inference(superposition,[],[f535,f5063])).
% 3.63/1.03 thf(f5301,plain,(
% 3.63/1.03 (((c_2Eextreal_2Eextreal__max @ sK0 @ sK1)) = sK0) | ~spl3_92),
% 3.63/1.03 inference(forward_demodulation,[],[f5294,f978])).
% 3.63/1.03 thf(f5305,plain,(
% 3.63/1.03 (((c_2Eextreal_2Eextreal__le @ sK0 @ sK2)) = $false) | (~spl3_5 | ~spl3_92)),
% 3.63/1.03 inference(superposition,[],[f234,f5301])).
% 3.63/1.03 thf(f5324,plain,(
% 3.63/1.03 $false | (spl3_1 | ~spl3_5 | ~spl3_92)),
% 3.63/1.03 inference(forward_subsumption_resolution,[],[f5305,f213])).
% 3.63/1.03 thf(f5325,plain,(
% 3.63/1.03 spl3_1 | ~spl3_5 | ~spl3_92),
% 3.63/1.03 inference(avatar_contradiction_clause,[],[f5324])).
% 3.63/1.03 thf(f5339,plain,(
% 3.63/1.03 ((((c_2Eextreal_2Eextreal__le @ sK0 @ sK2) = (c_2Eextreal_2Eextreal__le @ sK0 @ sK2))) = $false) | (~spl3_3 | ~spl3_92)),
% 3.63/1.03 inference(forward_demodulation,[],[f225,f5301])).
% 3.63/1.03 thf(f5340,plain,(
% 3.63/1.03 ($true = $false) | (~spl3_3 | ~spl3_92)),
% 3.63/1.03 inference(boolean_simplification,[],[f5339])).
% 3.63/1.03 thf(f5341,plain,(
% 3.63/1.03 $false | (~spl3_3 | ~spl3_92)),
% 3.63/1.03 inference(trivial_inequality_removal,[],[f5340])).
% 3.63/1.03 thf(f5342,plain,(
% 3.63/1.03 ~spl3_3 | ~spl3_92),
% 3.63/1.03 inference(avatar_contradiction_clause,[],[f5341])).
% 3.63/1.03 thf(f5352,plain,(
% 3.63/1.03 (((c_2Eextreal_2Eextreal__le @ sK0 @ sK2)) != $false) | (spl3_5 | ~spl3_92)),
% 3.63/1.03 inference(forward_demodulation,[],[f233,f5301])).
% 3.63/1.03 thf(f5365,plain,(
% 3.63/1.03 ~spl3_1 | spl3_5 | ~spl3_92),
% 3.63/1.03 inference(avatar_split_clause,[],[f5352,f5062,f232,f212])).
% 3.63/1.03 thf(f5402,plain,(
% 3.63/1.03 (((c_2Eextreal_2Eextreal__le @ sK0 @ sK1)) = $false) | (((c_2Eextreal_2Eextreal__le @ sK1 @ sK2)) != $false) | spl3_5),
% 3.63/1.03 inference(superposition,[],[f233,f5122])).
% 3.63/1.03 thf(f5435,plain,(
% 3.63/1.03 ((((c_2Eextreal_2Eextreal__le @ sK1 @ sK2) = (c_2Eextreal_2Eextreal__le @ sK1 @ sK2))) = $false) | (((c_2Eextreal_2Eextreal__le @ sK0 @ sK1)) = $false) | ~spl3_2),
% 3.63/1.03 inference(superposition,[],[f218,f5122])).
% 3.63/1.03 thf(f5445,plain,(
% 3.63/1.03 ($true = $false) | (((c_2Eextreal_2Eextreal__le @ sK0 @ sK1)) = $false) | ~spl3_2),
% 3.63/1.03 inference(boolean_simplification,[],[f5435])).
% 3.63/1.03 thf(f5446,plain,(
% 3.63/1.03 (((c_2Eextreal_2Eextreal__le @ sK0 @ sK1)) = $false) | ~spl3_2),
% 3.63/1.03 inference(trivial_inequality_removal,[],[f5445])).
% 3.63/1.03 thf(f5455,plain,(
% 3.63/1.03 spl3_92 | ~spl3_2),
% 3.63/1.03 inference(avatar_split_clause,[],[f5446,f216,f5062])).
% 3.63/1.03 thf(f5653,plain,(
% 3.63/1.03 ($false != $false) | (((c_2Eextreal_2Eextreal__le @ sK1 @ sK2)) = $false) | (~spl3_73 | spl3_92)),
% 3.63/1.03 inference(superposition,[],[f5064,f4335])).
% 3.63/1.03 thf(f5657,plain,(
% 3.63/1.03 (((c_2Eextreal_2Eextreal__le @ sK1 @ sK2)) = $false) | (~spl3_73 | spl3_92)),
% 3.63/1.03 inference(trivial_inequality_removal,[],[f5653])).
% 3.63/1.03 thf(f5668,plain,(
% 3.63/1.03 spl3_4 | ~spl3_73 | spl3_92),
% 3.63/1.03 inference(avatar_split_clause,[],[f5657,f5062,f4334,f227])).
% 3.63/1.03 thf(f5669,plain,(
% 3.63/1.03 (((c_2Eextreal_2Eextreal__le @ sK1 @ sK2)) != $false) | (spl3_5 | spl3_92)),
% 3.63/1.03 inference(forward_subsumption_resolution,[],[f5402,f5064])).
% 3.63/1.03 thf(f5711,plain,(
% 3.63/1.03 $false | (~spl3_4 | spl3_5 | spl3_92)),
% 3.63/1.03 inference(forward_subsumption_resolution,[],[f5669,f229])).
% 3.63/1.03 thf(f5712,plain,(
% 3.63/1.03 ~spl3_4 | spl3_5 | spl3_92),
% 3.63/1.03 inference(avatar_contradiction_clause,[],[f5711])).
% 3.63/1.03 cnf(s1, plain, spl3_1 | spl3_2, inference(sat_conversion,[],[f219])).
% 3.63/1.03 cnf(s2, plain, spl3_3 | spl3_4, inference(sat_conversion,[],[f230])).
% 3.63/1.03 cnf(s77, plain, spl3_3 | spl3_75, inference(sat_conversion,[],[f4347])).
% 3.63/1.03 cnf(s85, plain, ~spl3_1 | spl3_73, inference(sat_conversion,[],[f4397])).
% 3.63/1.03 cnf(s92, plain, ~spl3_1 | ~spl3_5, inference(sat_conversion,[],[f4424])).
% 3.63/1.03 cnf(s116, plain, spl3_1 | ~spl3_4 | spl3_5 | ~spl3_75, inference(sat_conversion,[],[f4876])).
% 3.63/1.03 cnf(s150, plain, spl3_1 | ~spl3_5 | ~spl3_92, inference(sat_conversion,[],[f5325])).
% 3.63/1.03 cnf(s153, plain, ~spl3_3 | ~spl3_92, inference(sat_conversion,[],[f5342])).
% 3.63/1.03 cnf(s167, plain, ~spl3_1 | spl3_5 | ~spl3_92, inference(sat_conversion,[],[f5365])).
% 3.63/1.03 cnf(s177, plain, ~spl3_2 | spl3_92, inference(sat_conversion,[],[f5455])).
% 3.63/1.03 cnf(s192, plain, spl3_4 | ~spl3_73 | spl3_92, inference(sat_conversion,[],[f5668])).
% 3.63/1.03 cnf(s208, plain, ~spl3_4 | spl3_5 | spl3_92, inference(sat_conversion,[],[f5712])).
% 3.63/1.03 cnf(s233, plain, spl3_1, inference(rat,[],[s116,s2,s77,s150,s153,s177,s1])).
% 3.63/1.03 cnf(s234, plain, ~spl3_5, inference(rat,[],[s92,s233])).
% 3.63/1.03 cnf(s235, plain, spl3_73, inference(rat,[],[s85,s233])).
% 3.63/1.03 cnf(s237, plain, ~spl3_92, inference(rat,[],[s167,s233,s234])).
% 3.63/1.03 cnf(s242, plain, ~spl3_4, inference(rat,[],[s208,s234,s237])).
% 3.63/1.03 cnf(s243, plain, $false, inference(rat,[],[s192,s235,s242,s237])).
% 3.63/1.03 thf(f5722,plain,(
% 3.63/1.03 $false),
% 3.63/1.03 inference(avatar_sat_refutation,[],[s243])).
% 3.63/1.03 % SZS output end Proof for theBenchmark
% 3.63/1.03 % (535753)------------------------------
% 3.63/1.03 % (535753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.63/1.03 % (535753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.63/1.03 % (535753)CaDiCaL version: 2.1.3
% 3.63/1.03 % (535753)Termination reason: Refutation
% 3.63/1.03 % (535753)Time elapsed: 0.404 s
% 3.63/1.03 % (535753)Peak memory usage: 15 MB
% 3.63/1.03 % (535753)Instructions burned: 493 (million)
% 3.63/1.04 % (535688)Success in time 0.717 s
% 3.63/1.04 % Vampire exiting
%------------------------------------------------------------------------------