%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYO544^1 : TPTP v9.3.1. Released v5.2.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:48:23 AM UTC 2026
% Result : Theorem 4.04s 0.97s
% Output : Refutation 4.04s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYO544^1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.18 % Computer : n018.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Tue Sep 29 17:16:27 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.21 Running higher-order theorem proving
% 0.09/0.23 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.21/0.35 % (370608)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.21/0.35 % (370617)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=1743510324:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.21/0.35 % (370619)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.21/0.35 % (370619)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.21/0.35 % (370617)Instruction limit reached!
% 0.21/0.35 % (370617)------------------------------
% 0.21/0.35 % (370617)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.35 % (370617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.35 % (370617)CaDiCaL version: 2.1.3
% 0.21/0.35 % (370617)Termination reason: Instruction limit
% 0.21/0.35 % (370617)Termination phase: Saturation
% 0.21/0.35 % (370617)Time elapsed: 0.007 s
% 0.21/0.35 % (370617)Peak memory usage: 12 MB
% 0.21/0.35 % (370617)Instructions burned: 26 (million)
% 0.21/0.35 % (370613)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3110790549:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.21/0.35 % (370614)lrs+10_16_si=on:nwc=1.5:random_seed=749128439:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.21/0.35 % (370618)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=1331693420:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.21/0.35 % (370615)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=1133825270:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.21/0.35 % (370616)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=3652012992: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.21/0.35 % (370619)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=1952115856:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.21/0.35 % (370615)Instruction limit reached!
% 0.21/0.35 % (370615)------------------------------
% 0.21/0.35 % (370615)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.35 % (370615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.35 % (370615)CaDiCaL version: 2.1.3
% 0.21/0.35 % (370615)Termination reason: Instruction limit
% 0.21/0.35 % (370615)Termination phase: Saturation
% 0.21/0.35 % (370615)Time elapsed: 0.002 s
% 0.21/0.35 % (370615)Peak memory usage: 11 MB
% 0.21/0.35 % (370615)Instructions burned: 3 (million)
% 0.21/0.35 % (370613)Refutation not found, incomplete strategy
% 0.21/0.35 % (370613)------------------------------
% 0.21/0.35 % (370613)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.35 % (370613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.35 % (370613)CaDiCaL version: 2.1.3
% 0.21/0.35 % (370613)Termination reason: Refutation not found, incomplete strategy
% 0.21/0.35 % (370613)Time elapsed: 0.005 s
% 0.21/0.35 % (370613)Peak memory usage: 12 MB
% 0.21/0.35 % (370613)Instructions burned: 9 (million)
% 0.21/0.35 % (370613)------------------------------
% 0.21/0.35 % (370613)------------------------------
% 0.21/0.35 % (370614)Instruction limit reached!
% 0.21/0.35 % (370614)------------------------------
% 0.21/0.35 % (370614)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.35 % (370614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.35 % (370614)CaDiCaL version: 2.1.3
% 0.21/0.35 % (370614)Termination reason: Instruction limit
% 0.21/0.35 % (370614)Termination phase: Saturation
% 0.21/0.35 % (370614)Time elapsed: 0.009 s
% 0.21/0.35 % (370614)Peak memory usage: 12 MB
% 0.21/0.35 % (370614)Instructions burned: 18 (million)
% 0.21/0.35 % (370625)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3914383122:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.21/0.35 % (370625)Instruction limit reached!
% 0.21/0.35 % (370625)------------------------------
% 0.21/0.35 % (370625)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.37 % (370625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.37 % (370625)CaDiCaL version: 2.1.3
% 0.75/0.37 % (370625)Termination reason: Instruction limit
% 0.75/0.37 % (370625)Termination phase: Saturation
% 0.75/0.37 % (370625)Time elapsed: 0.002 s
% 0.75/0.37 % (370625)Peak memory usage: 11 MB
% 0.75/0.37 % (370625)Instructions burned: 3 (million)
% 0.75/0.37 % (370628)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=3582710839:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.75/0.37 % (370629)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.75/0.37 % (370628)Instruction limit reached!
% 0.75/0.37 % (370628)------------------------------
% 0.75/0.37 % (370628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.37 % (370628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.37 % (370628)CaDiCaL version: 2.1.3
% 0.75/0.37 % (370628)Termination reason: Instruction limit
% 0.75/0.37 % (370628)Termination phase: Saturation
% 0.75/0.37 % (370628)Time elapsed: 0.003 s
% 0.75/0.37 % (370628)Peak memory usage: 11 MB
% 0.75/0.37 % (370628)Instructions burned: 5 (million)
% 0.75/0.37 % (370629)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2736252419:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.75/0.37 % (370630)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=1802735822:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.75/0.37 % (370629)Instruction limit reached!
% 0.75/0.37 % (370629)------------------------------
% 0.75/0.37 % (370629)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.37 % (370629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.37 % (370629)CaDiCaL version: 2.1.3
% 0.75/0.37 % (370629)Termination reason: Instruction limit
% 0.75/0.37 % (370629)Termination phase: Saturation
% 0.75/0.37 % (370629)Time elapsed: 0.004 s
% 0.75/0.37 % (370629)Peak memory usage: 12 MB
% 0.75/0.37 % (370629)Instructions burned: 8 (million)
% 0.75/0.37 % (370632)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.75/0.37 % (370632)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.75/0.37 % (370630)Instruction limit reached!
% 0.75/0.37 % (370630)------------------------------
% 0.75/0.37 % (370630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.37 % (370630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.37 % (370630)CaDiCaL version: 2.1.3
% 0.75/0.37 % (370630)Termination reason: Instruction limit
% 0.75/0.37 % (370630)Termination phase: Saturation
% 0.75/0.37 % (370630)Time elapsed: 0.007 s
% 0.75/0.37 % (370630)Peak memory usage: 12 MB
% 0.75/0.37 % (370630)Instructions burned: 13 (million)
% 0.75/0.37 % (370618)Instruction limit reached!
% 0.75/0.37 % (370618)------------------------------
% 0.75/0.37 % (370618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.37 % (370618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.37 % (370618)CaDiCaL version: 2.1.3
% 0.75/0.37 % (370618)Termination reason: Instruction limit
% 0.75/0.37 % (370618)Termination phase: Saturation
% 0.75/0.37 % (370618)Time elapsed: 0.037 s
% 0.75/0.37 % (370618)Peak memory usage: 12 MB
% 0.75/0.37 % (370618)Instructions burned: 76 (million)
% 0.75/0.37 % (370632)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=3540127165: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.75/0.37 % (370634)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=3090824407:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.75/0.37 % (370637)lrs+10_1_si=on:cs=on:random_seed=3276929376:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.75/0.37 % (370638)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.75/0.39 % (370637)Instruction limit reached!
% 0.75/0.39 % (370637)------------------------------
% 0.75/0.39 % (370637)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.39 % (370637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.39 % (370637)CaDiCaL version: 2.1.3
% 0.75/0.39 % (370637)Termination reason: Instruction limit
% 0.75/0.39 % (370637)Termination phase: Saturation
% 0.75/0.39 % (370637)Time elapsed: 0.004 s
% 0.75/0.39 % (370637)Peak memory usage: 12 MB
% 0.75/0.39 % (370637)Instructions burned: 8 (million)
% 0.75/0.39 % (370632)Instruction limit reached!
% 0.75/0.39 % (370632)------------------------------
% 0.75/0.39 % (370632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.39 % (370632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.39 % (370632)CaDiCaL version: 2.1.3
% 0.75/0.39 % (370632)Termination reason: Instruction limit
% 0.75/0.39 % (370632)Termination phase: Saturation
% 0.75/0.39 % (370632)Time elapsed: 0.013 s
% 0.75/0.39 % (370632)Peak memory usage: 12 MB
% 0.75/0.39 % (370632)Instructions burned: 28 (million)
% 0.75/0.39 % (370638)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=3927731319:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.75/0.39 % (370639)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=2624942911:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.75/0.39 % (370638)Instruction limit reached!
% 0.75/0.39 % (370638)------------------------------
% 0.75/0.39 % (370638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.39 % (370638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.39 % (370638)CaDiCaL version: 2.1.3
% 0.75/0.39 % (370638)Termination reason: Instruction limit
% 0.75/0.39 % (370638)Termination phase: Saturation
% 0.75/0.39 % (370638)Time elapsed: 0.002 s
% 0.75/0.39 % (370638)Peak memory usage: 11 MB
% 0.75/0.39 % (370638)Instructions burned: 3 (million)
% 0.75/0.39 % (370639)Refutation not found, incomplete strategy
% 0.75/0.39 % (370639)------------------------------
% 0.75/0.39 % (370639)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.39 % (370639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.39 % (370639)CaDiCaL version: 2.1.3
% 0.75/0.39 % (370639)Termination reason: Refutation not found, incomplete strategy
% 0.75/0.39 % (370639)Time elapsed: 0.002 s
% 0.75/0.39 % (370639)Peak memory usage: 12 MB
% 0.75/0.39 % (370639)Instructions burned: 3 (million)
% 0.75/0.39 % (370639)------------------------------
% 0.75/0.39 % (370639)------------------------------
% 0.75/0.39 % (370647)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=2009635716:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2999 on theBenchmark for (2999ds/14Mi)
% 0.75/0.39 % (370647)Refutation not found, incomplete strategy
% 0.75/0.39 % (370647)------------------------------
% 0.75/0.39 % (370647)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.39 % (370643)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=152251698:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.75/0.39 % (370647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.39 % (370647)CaDiCaL version: 2.1.3
% 0.75/0.39 % (370647)Termination reason: Refutation not found, incomplete strategy
% 0.75/0.39 % (370647)Time elapsed: 0.003 s
% 0.75/0.39 % (370647)Peak memory usage: 12 MB
% 0.75/0.39 % (370647)Instructions burned: 9 (million)
% 0.75/0.39 % (370647)------------------------------
% 0.75/0.39 % (370647)------------------------------
% 0.75/0.39 % (370644)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=908527942:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/25Mi)
% 0.75/0.39 % (370643)Refutation not found, incomplete strategy
% 0.75/0.39 % (370643)------------------------------
% 0.75/0.39 % (370643)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.39 % (370643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.39 % (370643)CaDiCaL version: 2.1.3
% 0.75/0.39 % (370643)Termination reason: Refutation not found, incomplete strategy
% 0.75/0.42 % (370643)Time elapsed: 0.003 s
% 0.75/0.42 % (370643)Peak memory usage: 12 MB
% 0.75/0.42 % (370643)Instructions burned: 6 (million)
% 0.75/0.42 % (370643)------------------------------
% 0.75/0.42 % (370643)------------------------------
% 0.75/0.42 % (370648)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=4227531555:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/327Mi)
% 0.75/0.42 % (370651)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=1466869770:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 0.75/0.42 % (370619)Instruction limit reached!
% 0.75/0.42 % (370619)------------------------------
% 0.75/0.42 % (370619)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.42 % (370619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.42 % (370619)CaDiCaL version: 2.1.3
% 0.75/0.42 % (370619)Termination reason: Instruction limit
% 0.75/0.42 % (370619)Termination phase: Saturation
% 0.75/0.42 % (370619)Time elapsed: 0.082 s
% 0.75/0.42 % (370619)Peak memory usage: 13 MB
% 0.75/0.42 % (370619)Instructions burned: 165 (million)
% 0.75/0.42 % (370648)Refutation not found, incomplete strategy
% 0.75/0.42 % (370648)------------------------------
% 0.75/0.42 % (370648)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.42 % (370648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.42 % (370648)CaDiCaL version: 2.1.3
% 0.75/0.42 % (370648)Termination reason: Refutation not found, incomplete strategy
% 0.75/0.42 % (370648)Time elapsed: 0.006 s
% 0.75/0.42 % (370648)Peak memory usage: 12 MB
% 0.75/0.42 % (370648)Instructions burned: 10 (million)
% 0.75/0.42 % (370648)------------------------------
% 0.75/0.42 % (370648)------------------------------
% 0.75/0.42 % (370644)Instruction limit reached!
% 0.75/0.42 % (370644)------------------------------
% 0.75/0.42 % (370644)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.42 % (370644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.42 % (370644)CaDiCaL version: 2.1.3
% 0.75/0.42 % (370644)Termination reason: Instruction limit
% 0.75/0.42 % (370644)Termination phase: Saturation
% 0.75/0.42 % (370644)Time elapsed: 0.014 s
% 0.75/0.42 % (370644)Peak memory usage: 12 MB
% 0.75/0.42 % (370644)Instructions burned: 25 (million)
% 0.75/0.42 % (370651)Instruction limit reached!
% 0.75/0.42 % (370651)------------------------------
% 0.75/0.42 % (370651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.42 % (370651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.42 % (370651)CaDiCaL version: 2.1.3
% 0.75/0.42 % (370651)Termination reason: Instruction limit
% 0.75/0.42 % (370651)Termination phase: Saturation
% 0.75/0.42 % (370651)Time elapsed: 0.006 s
% 0.75/0.42 % (370651)Peak memory usage: 12 MB
% 0.75/0.42 % (370651)Instructions burned: 14 (million)
% 0.75/0.42 % (370634)Instruction limit reached!
% 0.75/0.42 % (370634)------------------------------
% 0.75/0.42 % (370634)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.42 % (370634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.42 % (370634)CaDiCaL version: 2.1.3
% 0.75/0.42 % (370634)Termination reason: Instruction limit
% 0.75/0.42 % (370634)Termination phase: Saturation
% 0.75/0.42 % (370634)Time elapsed: 0.046 s
% 0.75/0.42 % (370634)Peak memory usage: 13 MB
% 0.75/0.42 % (370634)Instructions burned: 92 (million)
% 0.75/0.42 % (370656)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=1240415836:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 0.75/0.42 % (370654)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=2260548974: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.75/0.42 % (370656)Refutation not found, incomplete strategy
% 0.75/0.42 % (370656)------------------------------
% 0.75/0.42 % (370656)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.42 % (370656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.42 % (370656)CaDiCaL version: 2.1.3
% 0.75/0.42 % (370656)Termination reason: Refutation not found, incomplete strategy
% 0.75/0.42 % (370656)Time elapsed: 0.005 s
% 0.75/0.42 % (370656)Peak memory usage: 12 MB
% 0.75/0.42 % (370656)Instructions burned: 17 (million)
% 0.75/0.45 % (370656)------------------------------
% 0.75/0.45 % (370656)------------------------------
% 0.75/0.45 % (370654)Instruction limit reached!
% 0.75/0.45 % (370654)------------------------------
% 0.75/0.45 % (370654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.45 % (370654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.45 % (370654)CaDiCaL version: 2.1.3
% 0.75/0.45 % (370654)Termination reason: Instruction limit
% 0.75/0.45 % (370654)Termination phase: Property scanning
% 0.75/0.45 % (370654)Time elapsed: 0.002 s
% 0.75/0.45 % (370654)Peak memory usage: 11 MB
% 0.75/0.45 % (370654)Instructions burned: 3 (million)
% 0.75/0.45 % (370659)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
% 0.75/0.45 % (370659)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 0.75/0.45 % (370657)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=3890634316:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 0.75/0.45 % (370660)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 0.75/0.45 % (370658)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=909856676:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 0.75/0.45 % (370659)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=3824696919:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 0.75/0.45 % (370660)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=1681447264:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 0.75/0.45 % (370663)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=1004570210:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 0.75/0.45 % (370660)Instruction limit reached!
% 0.75/0.45 % (370660)------------------------------
% 0.75/0.45 % (370660)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.45 % (370660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.45 % (370660)CaDiCaL version: 2.1.3
% 0.75/0.45 % (370660)Termination reason: Instruction limit
% 0.75/0.45 % (370660)Termination phase: Saturation
% 0.75/0.45 % (370660)Time elapsed: 0.005 s
% 0.75/0.45 % (370660)Peak memory usage: 12 MB
% 0.75/0.45 % (370660)Instructions burned: 10 (million)
% 0.75/0.45 % (370659)Instruction limit reached!
% 0.75/0.45 % (370659)------------------------------
% 0.75/0.45 % (370659)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.45 % (370659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.45 % (370659)CaDiCaL version: 2.1.3
% 0.75/0.45 % (370659)Termination reason: Instruction limit
% 0.75/0.45 % (370659)Termination phase: Saturation
% 0.75/0.45 % (370659)Time elapsed: 0.008 s
% 0.75/0.45 % (370659)Peak memory usage: 12 MB
% 0.75/0.45 % (370659)Instructions burned: 15 (million)
% 0.75/0.45 % (370657)Instruction limit reached!
% 0.75/0.45 % (370657)------------------------------
% 0.75/0.45 % (370657)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.45 % (370657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.45 % (370657)CaDiCaL version: 2.1.3
% 0.75/0.45 % (370657)Termination reason: Instruction limit
% 0.75/0.45 % (370657)Termination phase: Saturation
% 0.75/0.45 % (370657)Time elapsed: 0.012 s
% 0.75/0.45 % (370657)Peak memory usage: 11 MB
% 0.75/0.45 % (370657)Instructions burned: 24 (million)
% 0.75/0.45 % (370664)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=4021531416:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 0.75/0.45 % (370663)Instruction limit reached!
% 0.75/0.45 % (370663)------------------------------
% 0.75/0.45 % (370663)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.45 % (370663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.45 % (370663)CaDiCaL version: 2.1.3
% 1.54/0.47 % (370663)Termination reason: Instruction limit
% 1.54/0.47 % (370663)Termination phase: Saturation
% 1.54/0.47 % (370663)Time elapsed: 0.009 s
% 1.54/0.47 % (370663)Peak memory usage: 12 MB
% 1.54/0.47 % (370663)Instructions burned: 35 (million)
% 1.54/0.47 % (370664)Instruction limit reached!
% 1.54/0.47 % (370664)------------------------------
% 1.54/0.47 % (370664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.47 % (370664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.47 % (370664)CaDiCaL version: 2.1.3
% 1.54/0.47 % (370664)Termination reason: Instruction limit
% 1.54/0.47 % (370664)Termination phase: Saturation
% 1.54/0.47 % (370664)Time elapsed: 0.004 s
% 1.54/0.47 % (370664)Peak memory usage: 12 MB
% 1.54/0.47 % (370664)Instructions burned: 8 (million)
% 1.54/0.47 % (370674)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=3893640450:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/143Mi)
% 1.54/0.47 % (370670)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=2889693037:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.54/0.47 % (370671)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=3110917278:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 1.54/0.47 % (370672)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=3975229524:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 1.54/0.47 % (370658)Instruction limit reached!
% 1.54/0.47 % (370658)------------------------------
% 1.54/0.47 % (370658)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.47 % (370658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.47 % (370658)CaDiCaL version: 2.1.3
% 1.54/0.47 % (370658)Termination reason: Instruction limit
% 1.54/0.47 % (370658)Termination phase: Saturation
% 1.54/0.47 % (370658)Time elapsed: 0.031 s
% 1.54/0.47 % (370658)Peak memory usage: 12 MB
% 1.54/0.47 % (370658)Instructions burned: 60 (million)
% 1.54/0.47 % (370675)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=2602609372:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/193Mi)
% 1.54/0.47 % (370670)Instruction limit reached!
% 1.54/0.47 % (370670)------------------------------
% 1.54/0.47 % (370670)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.47 % (370670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.47 % (370670)CaDiCaL version: 2.1.3
% 1.54/0.47 % (370670)Termination reason: Instruction limit
% 1.54/0.47 % (370670)Termination phase: Saturation
% 1.54/0.47 % (370670)Time elapsed: 0.011 s
% 1.54/0.47 % (370670)Peak memory usage: 11 MB
% 1.54/0.47 % (370670)Instructions burned: 25 (million)
% 1.54/0.47 % (370671)Instruction limit reached!
% 1.54/0.47 % (370671)------------------------------
% 1.54/0.47 % (370671)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.47 % (370671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.47 % (370671)CaDiCaL version: 2.1.3
% 1.54/0.47 % (370671)Termination reason: Instruction limit
% 1.54/0.47 % (370671)Termination phase: Saturation
% 1.54/0.47 % (370671)Time elapsed: 0.011 s
% 1.54/0.47 % (370671)Peak memory usage: 12 MB
% 1.54/0.47 % (370671)Instructions burned: 20 (million)
% 1.54/0.47 % (370675)Refutation not found, incomplete strategy
% 1.54/0.47 % (370675)------------------------------
% 1.54/0.47 % (370675)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.47 % (370675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.47 % (370675)CaDiCaL version: 2.1.3
% 1.54/0.47 % (370675)Termination reason: Refutation not found, incomplete strategy
% 1.54/0.47 % (370675)Time elapsed: 0.006 s
% 1.54/0.47 % (370675)Peak memory usage: 12 MB
% 1.54/0.47 % (370675)Instructions burned: 10 (million)
% 1.54/0.47 % (370672)Refutation not found, incomplete strategy
% 1.54/0.47 % (370672)------------------------------
% 1.54/0.47 % (370672)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.47 % (370672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.47 % (370672)CaDiCaL version: 2.1.3
% 1.54/0.47 % (370672)Termination reason: Refutation not found, incomplete strategy
% 1.54/0.47 % (370672)Time elapsed: 0.013 s
% 1.54/0.47 % (370672)Peak memory usage: 12 MB
% 1.54/0.47 % (370672)Instructions burned: 25 (million)
% 1.54/0.50 % (370675)------------------------------
% 1.54/0.50 % (370675)------------------------------
% 1.54/0.50 % (370672)------------------------------
% 1.54/0.50 % (370672)------------------------------
% 1.54/0.50 % (370680)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3142142626:i=42:hud=10:rtra=on_2998 on theBenchmark for (2998ds/42Mi)
% 1.54/0.50 % (370682)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.54/0.50 % (370682)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1319432816:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2998 on theBenchmark for (2998ds/7Mi)
% 1.54/0.50 % (370685)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 1.54/0.50 % (370683)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=3375149249:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/181Mi)
% 1.54/0.50 % (370682)Instruction limit reached!
% 1.54/0.50 % (370682)------------------------------
% 1.54/0.50 % (370682)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.50 % (370682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.50 % (370682)CaDiCaL version: 2.1.3
% 1.54/0.50 % (370682)Termination reason: Instruction limit
% 1.54/0.50 % (370682)Termination phase: Saturation
% 1.54/0.50 % (370682)Time elapsed: 0.004 s
% 1.54/0.50 % (370682)Peak memory usage: 12 MB
% 1.54/0.50 % (370682)Instructions burned: 7 (million)
% 1.54/0.50 % (370684)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=801727639:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/169Mi)
% 1.54/0.50 % (370685)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=2126270971:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2998 on theBenchmark for (2998ds/6Mi)
% 1.54/0.50 % (370674)Instruction limit reached!
% 1.54/0.50 % (370674)------------------------------
% 1.54/0.50 % (370674)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.50 % (370674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.50 % (370674)CaDiCaL version: 2.1.3
% 1.54/0.50 % (370674)Termination reason: Instruction limit
% 1.54/0.50 % (370674)Termination phase: Saturation
% 1.54/0.50 % (370674)Time elapsed: 0.039 s
% 1.54/0.50 % (370674)Peak memory usage: 13 MB
% 1.54/0.50 % (370674)Instructions burned: 144 (million)
% 1.54/0.50 % (370683)Refutation not found, incomplete strategy
% 1.54/0.50 % (370683)------------------------------
% 1.54/0.50 % (370683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.50 % (370683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.50 % (370683)CaDiCaL version: 2.1.3
% 1.54/0.50 % (370683)Termination reason: Refutation not found, incomplete strategy
% 1.54/0.50 % (370683)Time elapsed: 0.004 s
% 1.54/0.50 % (370683)Peak memory usage: 12 MB
% 1.54/0.50 % (370683)Instructions burned: 5 (million)
% 1.54/0.50 % (370683)------------------------------
% 1.54/0.50 % (370683)------------------------------
% 1.54/0.50 % (370685)Instruction limit reached!
% 1.54/0.50 % (370685)------------------------------
% 1.54/0.50 % (370685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.50 % (370685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.50 % (370685)CaDiCaL version: 2.1.3
% 1.54/0.50 % (370685)Termination reason: Instruction limit
% 1.54/0.50 % (370685)Termination phase: Saturation
% 1.54/0.50 % (370685)Time elapsed: 0.003 s
% 1.54/0.50 % (370685)Peak memory usage: 11 MB
% 1.54/0.50 % (370685)Instructions burned: 6 (million)
% 1.54/0.50 % (370684)Refutation not found, incomplete strategy
% 1.54/0.50 % (370684)------------------------------
% 1.54/0.50 % (370684)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.50 % (370684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.50 % (370684)CaDiCaL version: 2.1.3
% 1.54/0.50 % (370684)Termination reason: Refutation not found, incomplete strategy
% 1.54/0.50 % (370684)Time elapsed: 0.004 s
% 1.54/0.50 % (370684)Peak memory usage: 12 MB
% 1.54/0.50 % (370684)Instructions burned: 6 (million)
% 1.54/0.53 % (370684)------------------------------
% 1.54/0.53 % (370684)------------------------------
% 1.54/0.53 % (370680)Instruction limit reached!
% 1.54/0.53 % (370680)------------------------------
% 1.54/0.53 % (370680)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.53 % (370680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.53 % (370680)CaDiCaL version: 2.1.3
% 1.54/0.53 % (370680)Termination reason: Instruction limit
% 1.54/0.53 % (370680)Termination phase: Saturation
% 1.54/0.53 % (370680)Time elapsed: 0.021 s
% 1.54/0.53 % (370680)Peak memory usage: 12 MB
% 1.54/0.53 % (370680)Instructions burned: 44 (million)
% 1.54/0.53 % (370692)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=3084615707:i=19:add=on:rtra=on_2997 on theBenchmark for (2997ds/19Mi)
% 1.54/0.53 % (370692)Refutation not found, incomplete strategy
% 1.54/0.53 % (370692)------------------------------
% 1.54/0.53 % (370692)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.53 % (370692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.53 % (370692)CaDiCaL version: 2.1.3
% 1.54/0.53 % (370692)Termination reason: Refutation not found, incomplete strategy
% 1.54/0.53 % (370692)Time elapsed: 0.005 s
% 1.54/0.53 % (370692)Peak memory usage: 13 MB
% 1.54/0.53 % (370692)Instructions burned: 19 (million)
% 1.54/0.53 % (370692)------------------------------
% 1.54/0.53 % (370692)------------------------------
% 1.54/0.53 % (370689)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=1709076737:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2997 on theBenchmark for (2997ds/22Mi)
% 1.54/0.53 % (370693)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=2578690052:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/316Mi)
% 1.54/0.53 % (370694)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=4175429302:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2997 on theBenchmark for (2997ds/853Mi)
% 1.54/0.53 % (370695)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=2958066640:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2997 on theBenchmark for (2997ds/45Mi)
% 1.54/0.53 % (370699)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=2816975334:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2997 on theBenchmark for (2997ds/21Mi)
% 1.54/0.53 % (370696)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=771256281:i=480:rtra=on_2997 on theBenchmark for (2997ds/480Mi)
% 1.54/0.53 % (370689)Instruction limit reached!
% 1.54/0.53 % (370689)------------------------------
% 1.54/0.53 % (370689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.53 % (370689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.53 % (370689)CaDiCaL version: 2.1.3
% 1.54/0.53 % (370689)Termination reason: Instruction limit
% 1.54/0.53 % (370689)Termination phase: Saturation
% 1.54/0.53 % (370689)Time elapsed: 0.011 s
% 1.54/0.53 % (370689)Peak memory usage: 12 MB
% 1.54/0.53 % (370689)Instructions burned: 23 (million)
% 1.54/0.53 % (370696)Refutation not found, incomplete strategy
% 1.54/0.53 % (370696)------------------------------
% 1.54/0.53 % (370696)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.53 % (370696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.54/0.53 % (370696)CaDiCaL version: 2.1.3
% 1.54/0.53 % (370696)Termination reason: Refutation not found, incomplete strategy
% 1.54/0.53 % (370696)Time elapsed: 0.002 s
% 1.54/0.53 % (370696)Peak memory usage: 12 MB
% 1.54/0.53 % (370696)Instructions burned: 2 (million)
% 1.54/0.53 % (370696)------------------------------
% 1.54/0.53 % (370696)------------------------------
% 1.54/0.53 % (370695)Refutation not found, incomplete strategy
% 1.54/0.53 % (370695)------------------------------
% 1.54/0.53 % (370695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.54/0.53 % (370695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.24/0.57 % (370695)CaDiCaL version: 2.1.3
% 2.24/0.57 % (370695)Termination reason: Refutation not found, incomplete strategy
% 2.24/0.57 % (370695)Time elapsed: 0.006 s
% 2.24/0.57 % (370695)Peak memory usage: 12 MB
% 2.24/0.57 % (370695)Instructions burned: 9 (million)
% 2.24/0.57 % (370695)------------------------------
% 2.24/0.57 % (370695)------------------------------
% 2.24/0.57 % (370699)Instruction limit reached!
% 2.24/0.57 % (370699)------------------------------
% 2.24/0.57 % (370699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.24/0.57 % (370699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.24/0.57 % (370699)CaDiCaL version: 2.1.3
% 2.24/0.57 % (370699)Termination reason: Instruction limit
% 2.24/0.57 % (370699)Termination phase: Saturation
% 2.24/0.57 % (370699)Time elapsed: 0.006 s
% 2.24/0.57 % (370699)Peak memory usage: 12 MB
% 2.24/0.57 % (370699)Instructions burned: 24 (million)
% 2.24/0.57 % (370705)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 2.24/0.57 % (370708)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=2353682677:i=51:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/51Mi)
% 2.24/0.57 % (370708)Refutation not found, incomplete strategy
% 2.24/0.57 % (370708)------------------------------
% 2.24/0.57 % (370708)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.24/0.57 % (370708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.24/0.57 % (370708)CaDiCaL version: 2.1.3
% 2.24/0.57 % (370708)Termination reason: Refutation not found, incomplete strategy
% 2.24/0.57 % (370708)Time elapsed: 0.001 s
% 2.24/0.57 % (370708)Peak memory usage: 12 MB
% 2.24/0.57 % (370708)Instructions burned: 6 (million)
% 2.24/0.57 % (370708)------------------------------
% 2.24/0.57 % (370708)------------------------------
% 2.24/0.57 % (370705)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=2398643854:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/200Mi)
% 2.24/0.57 % (370706)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=3123885950:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2997 on theBenchmark for (2997ds/13Mi)
% 2.24/0.57 % (370705)Refutation not found, incomplete strategy
% 2.24/0.57 % (370705)------------------------------
% 2.24/0.57 % (370705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.24/0.57 % (370705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.24/0.57 % (370705)CaDiCaL version: 2.1.3
% 2.24/0.57 % (370705)Termination reason: Refutation not found, incomplete strategy
% 2.24/0.57 % (370705)Time elapsed: 0.004 s
% 2.24/0.57 % (370705)Peak memory usage: 12 MB
% 2.24/0.57 % (370705)Instructions burned: 8 (million)
% 2.24/0.57 % (370707)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=1754278577:i=66:s2at=3:nm=2:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/66Mi)
% 2.24/0.57 % (370705)------------------------------
% 2.24/0.57 % (370705)------------------------------
% 2.24/0.57 % (370693)Refutation not found, incomplete strategy
% 2.24/0.57 % (370693)------------------------------
% 2.24/0.57 % (370693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.24/0.57 % (370693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.24/0.57 % (370693)CaDiCaL version: 2.1.3
% 2.24/0.57 % (370693)Termination reason: Refutation not found, incomplete strategy
% 2.24/0.57 % (370693)Time elapsed: 0.032 s
% 2.24/0.57 % (370693)Peak memory usage: 13 MB
% 2.24/0.57 % (370693)Instructions burned: 63 (million)
% 2.24/0.57 % (370693)------------------------------
% 2.24/0.57 % (370693)------------------------------
% 2.24/0.57 % (370710)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=2747287701:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/31Mi)
% 2.24/0.57 % (370706)Instruction limit reached!
% 2.24/0.57 % (370706)------------------------------
% 2.24/0.57 % (370706)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.24/0.57 % (370706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.24/0.57 % (370706)CaDiCaL version: 2.1.3
% 2.24/0.57 % (370706)Termination reason: Instruction limit
% 2.24/0.57 % (370706)Termination phase: Saturation
% 2.24/0.57 % (370706)Time elapsed: 0.008 s
% 2.24/0.57 % (370706)Peak memory usage: 12 MB
% 2.24/0.57 % (370706)Instructions burned: 15 (million)
% 2.24/0.61 % (370707)Refutation not found, incomplete strategy
% 2.24/0.61 % (370707)------------------------------
% 2.24/0.61 % (370707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.24/0.61 % (370707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.24/0.61 % (370707)CaDiCaL version: 2.1.3
% 2.24/0.61 % (370707)Termination reason: Refutation not found, incomplete strategy
% 2.24/0.61 % (370707)Time elapsed: 0.006 s
% 2.24/0.61 % (370707)Peak memory usage: 13 MB
% 2.24/0.61 % (370707)Instructions burned: 10 (million)
% 2.24/0.61 % (370707)------------------------------
% 2.24/0.61 % (370707)------------------------------
% 2.24/0.61 % (370710)Refutation not found, incomplete strategy
% 2.24/0.61 % (370710)------------------------------
% 2.24/0.61 % (370710)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.24/0.61 % (370710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.24/0.61 % (370710)CaDiCaL version: 2.1.3
% 2.24/0.61 % (370710)Termination reason: Refutation not found, incomplete strategy
% 2.24/0.61 % (370710)Time elapsed: 0.004 s
% 2.24/0.61 % (370710)Peak memory usage: 12 MB
% 2.24/0.61 % (370710)Instructions burned: 16 (million)
% 2.24/0.61 % (370710)------------------------------
% 2.24/0.61 % (370710)------------------------------
% 2.24/0.61 % (370714)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=367503099:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2997 on theBenchmark for (2997ds/137Mi)
% 2.24/0.61 % (370719)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=1236134110:st=2:i=246:sd=3:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/246Mi)
% 2.24/0.61 % (370718)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 2.24/0.61 % (370716)dis+10_2_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_pi_sigma_gen:si=on:sp=occurrence:plsqr=5,1:bsr=on:plsql=on:random_seed=2220949080:cond=on:i=34:hud=10:nm=10:rtra=on_2997 on theBenchmark for (2997ds/34Mi)
% 2.24/0.61 % (370719)Refutation not found, incomplete strategy
% 2.24/0.61 % (370719)------------------------------
% 2.24/0.61 % (370719)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.24/0.61 % (370719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.24/0.61 % (370719)CaDiCaL version: 2.1.3
% 2.24/0.61 % (370719)Termination reason: Refutation not found, incomplete strategy
% 2.24/0.61 % (370719)Time elapsed: 0.003 s
% 2.24/0.61 % (370719)Peak memory usage: 12 MB
% 2.24/0.61 % (370719)Instructions burned: 9 (million)
% 2.24/0.61 % (370719)------------------------------
% 2.24/0.61 % (370719)------------------------------
% 2.24/0.61 % (370717)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=522034465:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2997 on theBenchmark for (2997ds/67Mi)
% 2.24/0.61 % (370714)Refutation not found, incomplete strategy
% 2.24/0.61 % (370714)------------------------------
% 2.24/0.61 % (370714)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.24/0.61 % (370714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.24/0.61 % (370714)CaDiCaL version: 2.1.3
% 2.24/0.61 % (370714)Termination reason: Refutation not found, incomplete strategy
% 2.24/0.61 % (370714)Time elapsed: 0.005 s
% 2.24/0.61 % (370714)Peak memory usage: 12 MB
% 2.24/0.61 % (370714)Instructions burned: 8 (million)
% 2.24/0.61 % (370714)------------------------------
% 2.24/0.61 % (370714)------------------------------
% 2.24/0.61 % (370718)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=949520677:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2997 on theBenchmark for (2997ds/180Mi)
% 2.24/0.61 % (370717)Refutation not found, incomplete strategy
% 2.24/0.61 % (370717)------------------------------
% 2.24/0.61 % (370717)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.24/0.61 % (370717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.24/0.61 % (370717)CaDiCaL version: 2.1.3
% 2.24/0.61 % (370717)Termination reason: Refutation not found, incomplete strategy
% 2.24/0.61 % (370717)Time elapsed: 0.003 s
% 2.24/0.61 % (370717)Peak memory usage: 12 MB
% 2.24/0.61 % (370717)Instructions burned: 6 (million)
% 2.24/0.61 % (370717)------------------------------
% 2.24/0.61 % (370717)------------------------------
% 2.24/0.61 % (370723)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=3582657278:cond=on:i=96:bd=all:rtra=on_2997 on theBenchmark for (2997ds/96Mi)
% 2.79/0.73 % (370716)Instruction limit reached!
% 2.79/0.73 % (370716)------------------------------
% 2.79/0.73 % (370716)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.79/0.73 % (370716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.79/0.73 % (370716)CaDiCaL version: 2.1.3
% 2.79/0.73 % (370716)Termination reason: Instruction limit
% 2.79/0.73 % (370716)Termination phase: Saturation
% 2.79/0.73 % (370716)Time elapsed: 0.016 s
% 2.79/0.73 % (370716)Peak memory usage: 12 MB
% 2.79/0.73 % (370716)Instructions burned: 34 (million)
% 2.79/0.73 % (370726)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=517639475:i=427:sd=1:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/427Mi)
% 2.79/0.73 % (370726)Refutation not found, incomplete strategy
% 2.79/0.73 % (370726)------------------------------
% 2.79/0.73 % (370726)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.79/0.73 % (370726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.79/0.73 % (370726)CaDiCaL version: 2.1.3
% 2.79/0.73 % (370726)Termination reason: Refutation not found, incomplete strategy
% 2.79/0.73 % (370726)Time elapsed: 0.002 s
% 2.79/0.73 % (370726)Peak memory usage: 12 MB
% 2.79/0.73 % (370726)Instructions burned: 2 (million)
% 2.79/0.73 % (370726)------------------------------
% 2.79/0.73 % (370726)------------------------------
% 2.79/0.73 % (370727)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=31588142:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/874Mi)
% 2.79/0.73 % (370727)Refutation not found, incomplete strategy
% 2.79/0.73 % (370727)------------------------------
% 2.79/0.73 % (370727)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.79/0.73 % (370727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.79/0.73 % (370727)CaDiCaL version: 2.1.3
% 2.79/0.73 % (370727)Termination reason: Refutation not found, incomplete strategy
% 2.79/0.73 % (370727)Time elapsed: 0.006 s
% 2.79/0.73 % (370727)Peak memory usage: 12 MB
% 2.79/0.73 % (370727)Instructions burned: 10 (million)
% 2.79/0.73 % (370727)------------------------------
% 2.79/0.73 % (370727)------------------------------
% 2.79/0.73 % (370729)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=3390244632:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/515Mi)
% 2.79/0.73 % (370723)Instruction limit reached!
% 2.79/0.73 % (370723)------------------------------
% 2.79/0.73 % (370723)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.79/0.73 % (370723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.79/0.73 % (370723)CaDiCaL version: 2.1.3
% 2.79/0.73 % (370723)Termination reason: Instruction limit
% 2.79/0.73 % (370723)Termination phase: Saturation
% 2.79/0.73 % (370723)Time elapsed: 0.024 s
% 2.79/0.73 % (370723)Peak memory usage: 12 MB
% 2.79/0.73 % (370723)Instructions burned: 96 (million)
% 2.79/0.73 % (370731)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=1886834882:st=1.5:i=130:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/130Mi)
% 2.79/0.73 % (370735)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=3654100253:s2a=on:i=571:nm=16:rtra=on_2996 on theBenchmark for (2996ds/571Mi)
% 2.79/0.73 % (370735)Refutation not found, incomplete strategy
% 2.79/0.73 % (370735)------------------------------
% 2.79/0.73 % (370735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.79/0.73 % (370735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.79/0.73 % (370735)CaDiCaL version: 2.1.3
% 2.79/0.73 % (370735)Termination reason: Refutation not found, incomplete strategy
% 2.79/0.73 % (370735)Time elapsed: 0.001 s
% 2.79/0.73 % (370735)Peak memory usage: 12 MB
% 2.79/0.73 % (370735)Instructions burned: 3 (million)
% 2.79/0.73 % (370735)------------------------------
% 2.79/0.73 % (370735)------------------------------
% 2.79/0.73 % (370731)Refutation not found, incomplete strategy
% 2.79/0.73 % (370731)------------------------------
% 2.79/0.73 % (370731)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.79/0.73 % (370731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.79/0.73 % (370731)CaDiCaL version: 2.1.3
% 2.79/0.73 % (370731)Termination reason: Refutation not found, incomplete strategy
% 2.79/0.73 % (370731)Time elapsed: 0.005 s
% 2.79/0.77 % (370731)Peak memory usage: 12 MB
% 2.79/0.77 % (370731)Instructions burned: 8 (million)
% 2.79/0.77 % (370731)------------------------------
% 2.79/0.77 % (370731)------------------------------
% 2.79/0.77 % (370733)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=2665083329:i=44:ep=R:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/44Mi)
% 2.79/0.77 % (370616)Instruction limit reached!
% 2.79/0.77 % (370616)------------------------------
% 2.79/0.77 % (370616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.79/0.77 % (370616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.79/0.77 % (370616)CaDiCaL version: 2.1.3
% 2.79/0.77 % (370616)Termination reason: Instruction limit
% 2.79/0.77 % (370616)Termination phase: Saturation
% 2.79/0.77 % (370616)Time elapsed: 0.300 s
% 2.79/0.77 % (370616)Peak memory usage: 14 MB
% 2.79/0.77 % (370616)Instructions burned: 635 (million)
% 2.79/0.77 % (370733)Refutation not found, incomplete strategy
% 2.79/0.77 % (370733)------------------------------
% 2.79/0.77 % (370733)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.79/0.77 % (370733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.79/0.77 % (370733)CaDiCaL version: 2.1.3
% 2.79/0.77 % (370733)Termination reason: Refutation not found, incomplete strategy
% 2.79/0.77 % (370733)Time elapsed: 0.009 s
% 2.79/0.77 % (370733)Peak memory usage: 12 MB
% 2.79/0.77 % (370733)Instructions burned: 17 (million)
% 2.79/0.77 % (370733)------------------------------
% 2.79/0.77 % (370733)------------------------------
% 2.79/0.77 % (370738)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=2435018244:i=450:rtra=on:ixr=off:ntd=on_2996 on theBenchmark for (2996ds/450Mi)
% 2.79/0.77 % (370739)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=1338102655:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/95Mi)
% 2.79/0.77 % (370738)Refutation not found, incomplete strategy
% 2.79/0.77 % (370738)------------------------------
% 2.79/0.77 % (370738)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.79/0.77 % (370738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.79/0.77 % (370738)CaDiCaL version: 2.1.3
% 2.79/0.77 % (370738)Termination reason: Refutation not found, incomplete strategy
% 2.79/0.77 % (370738)Time elapsed: 0.004 s
% 2.79/0.77 % (370738)Peak memory usage: 12 MB
% 2.79/0.77 % (370738)Instructions burned: 7 (million)
% 2.79/0.77 % (370738)------------------------------
% 2.79/0.77 % (370738)------------------------------
% 2.79/0.77 % (370741)lrs+1003_1_sil=128000:drc=off:cnfonf=lazy_pi_sigma_gen:si=on:uwa=one_side_interpreted:fd=off:rp=on:sac=on:random_seed=2625215198:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2996 on theBenchmark for (2996ds/65Mi)
% 2.79/0.77 % (370742)dis+1010_2:1_slsqr=2,1:to=lpo:plsq=on:cnfonf=lazy_pi_sigma_gen:si=on:sp=reverse_arity:acc=on:uwa=hol:fd=preordered:s2agt=16:flr=on:pe=on:slsq=on:random_seed=1374920999:uwa_fpi=on:avsq=on:s2a=on:cond=fast:i=105:s2at=1.5:aac=none:fgj=on:piset=and:hud=3:fsr=off:rtra=on:er=filter:rawr=on_2996 on theBenchmark for (2996ds/105Mi)
% 2.79/0.77 % (370718)Instruction limit reached!
% 2.79/0.77 % (370718)------------------------------
% 2.79/0.77 % (370718)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.79/0.77 % (370718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.79/0.77 % (370718)CaDiCaL version: 2.1.3
% 2.79/0.77 % (370718)Termination reason: Instruction limit
% 2.79/0.77 % (370718)Termination phase: Saturation
% 2.79/0.77 % (370718)Time elapsed: 0.082 s
% 2.79/0.77 % (370718)Peak memory usage: 14 MB
% 2.79/0.77 % (370718)Instructions burned: 182 (million)
% 2.79/0.77 % (370741)Refutation not found, incomplete strategy
% 2.79/0.77 % (370741)------------------------------
% 2.79/0.77 % (370741)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.79/0.77 % (370741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.79/0.77 % (370741)CaDiCaL version: 2.1.3
% 2.79/0.77 % (370741)Termination reason: Refutation not found, incomplete strategy
% 2.79/0.77 % (370741)Time elapsed: 0.012 s
% 2.79/0.77 % (370741)Peak memory usage: 12 MB
% 2.79/0.77 % (370741)Instructions burned: 24 (million)
% 2.79/0.77 % (370741)------------------------------
% 2.79/0.77 % (370741)------------------------------
% 2.79/0.77 % (370745)dis+10_4:1_sfv=off:to=kbo:fde=unused:cnfonf=off:sas=cadical:e2e=on:si=on:sp=occurrence:acc=on:uwa=off:fd=preordered:foolp=on:random_seed=2294077163:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2996 on theBenchmark for (2996ds/5755Mi)
% 3.53/0.85 % (370748)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=4021400044:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/375Mi)
% 3.53/0.85 % (370749)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=2282086988:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2996 on theBenchmark for (2996ds/495Mi)
% 3.53/0.85 % (370739)Instruction limit reached!
% 3.53/0.85 % (370739)------------------------------
% 3.53/0.85 % (370739)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.53/0.85 % (370739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.53/0.85 % (370739)CaDiCaL version: 2.1.3
% 3.53/0.85 % (370739)Termination reason: Instruction limit
% 3.53/0.85 % (370739)Termination phase: Saturation
% 3.53/0.85 % (370739)Time elapsed: 0.053 s
% 3.53/0.85 % (370739)Peak memory usage: 12 MB
% 3.53/0.85 % (370739)Instructions burned: 97 (million)
% 3.53/0.85 % (370742)Instruction limit reached!
% 3.53/0.85 % (370742)------------------------------
% 3.53/0.85 % (370742)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.53/0.85 % (370742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.53/0.85 % (370742)CaDiCaL version: 2.1.3
% 3.53/0.85 % (370742)Termination reason: Instruction limit
% 3.53/0.85 % (370742)Termination phase: Saturation
% 3.53/0.85 % (370742)Time elapsed: 0.049 s
% 3.53/0.85 % (370742)Peak memory usage: 13 MB
% 3.53/0.85 % (370742)Instructions burned: 107 (million)
% 3.53/0.85 % (370753)dis+10_2_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_pi_sigma_gen:si=on:sp=occurrence:plsqr=5,1:bsr=on:plsql=on:random_seed=2012686991:cond=on:i=34:hud=10:nm=10:rtra=on_2995 on theBenchmark for (2995ds/34Mi)
% 3.53/0.85 % (370754)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=1815890794:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2995 on theBenchmark for (2995ds/91Mi)
% 3.53/0.85 % (370753)Instruction limit reached!
% 3.53/0.85 % (370753)------------------------------
% 3.53/0.85 % (370753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.53/0.85 % (370753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.53/0.85 % (370753)CaDiCaL version: 2.1.3
% 3.53/0.85 % (370753)Termination reason: Instruction limit
% 3.53/0.85 % (370753)Termination phase: Saturation
% 3.53/0.85 % (370753)Time elapsed: 0.017 s
% 3.53/0.85 % (370753)Peak memory usage: 12 MB
% 3.53/0.85 % (370753)Instructions burned: 35 (million)
% 3.53/0.85 % (370757)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=4216436579:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2995 on theBenchmark for (2995ds/66Mi)
% 3.53/0.85 % (370757)Refutation not found, incomplete strategy
% 3.53/0.85 % (370757)------------------------------
% 3.53/0.85 % (370757)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.53/0.85 % (370757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.53/0.85 % (370757)CaDiCaL version: 2.1.3
% 3.53/0.85 % (370757)Termination reason: Refutation not found, incomplete strategy
% 3.53/0.85 % (370757)Time elapsed: 0.002 s
% 3.53/0.85 % (370757)Peak memory usage: 12 MB
% 3.53/0.85 % (370757)Instructions burned: 3 (million)
% 3.53/0.85 % (370757)------------------------------
% 3.53/0.85 % (370757)------------------------------
% 3.53/0.85 % (370754)Instruction limit reached!
% 3.53/0.85 % (370754)------------------------------
% 3.53/0.85 % (370754)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.53/0.85 % (370754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.53/0.85 % (370754)CaDiCaL version: 2.1.3
% 3.53/0.85 % (370754)Termination reason: Instruction limit
% 3.53/0.85 % (370754)Termination phase: Saturation
% 3.53/0.85 % (370754)Time elapsed: 0.047 s
% 3.53/0.85 % (370754)Peak memory usage: 12 MB
% 3.53/0.85 % (370754)Instructions burned: 92 (million)
% 3.53/0.85 % (370759)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=1363765025:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2995 on theBenchmark for (2995ds/22Mi)
% 3.53/0.85 % (370759)Instruction limit reached!
% 3.53/0.85 % (370759)------------------------------
% 3.53/0.89 % (370759)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.53/0.89 % (370759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.53/0.89 % (370759)CaDiCaL version: 2.1.3
% 3.53/0.89 % (370759)Termination reason: Instruction limit
% 3.53/0.89 % (370759)Termination phase: Saturation
% 3.53/0.89 % (370759)Time elapsed: 0.012 s
% 3.53/0.89 % (370759)Peak memory usage: 12 MB
% 3.53/0.89 % (370759)Instructions burned: 23 (million)
% 3.53/0.89 % (370748)Instruction limit reached!
% 3.53/0.89 % (370748)------------------------------
% 3.53/0.89 % (370748)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.53/0.89 % (370748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.53/0.89 % (370748)CaDiCaL version: 2.1.3
% 3.53/0.89 % (370748)Termination reason: Instruction limit
% 3.53/0.89 % (370748)Termination phase: Saturation
% 3.53/0.89 % (370748)Time elapsed: 0.114 s
% 3.53/0.89 % (370748)Peak memory usage: 14 MB
% 3.53/0.89 % (370748)Instructions burned: 376 (million)
% 3.53/0.89 % (370760)lrs+21_16_anc=none:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:sas=cadical:si=on:plsqr=32,1:uwa=interpreted_only:foolp=on:nwc=3:random_seed=2044332881:i=338:bd=all:ins=4:rtra=on_2995 on theBenchmark for (2995ds/338Mi)
% 3.53/0.89 % (370763)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 3.53/0.89 % (370763)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=3665944954:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2995 on theBenchmark for (2995ds/137Mi)
% 3.53/0.89 % (370763)Refutation not found, incomplete strategy
% 3.53/0.89 % (370763)------------------------------
% 3.53/0.89 % (370763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.53/0.89 % (370763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.53/0.89 % (370763)CaDiCaL version: 2.1.3
% 3.53/0.89 % (370763)Termination reason: Refutation not found, incomplete strategy
% 3.53/0.89 % (370763)Time elapsed: 0.004 s
% 3.53/0.89 % (370763)Peak memory usage: 12 MB
% 3.53/0.89 % (370763)Instructions burned: 16 (million)
% 3.53/0.89 % (370763)------------------------------
% 3.53/0.89 % (370763)------------------------------
% 3.53/0.89 % (370762)lrs+10_1_sil=128000:si=on:urr=on:random_seed=820615409:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2995 on theBenchmark for (2995ds/28Mi)
% 3.53/0.89 % (370760)Refutation not found, incomplete strategy
% 3.53/0.89 % (370760)------------------------------
% 3.53/0.89 % (370760)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.53/0.89 % (370760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.53/0.89 % (370760)CaDiCaL version: 2.1.3
% 3.53/0.89 % (370760)Termination reason: Refutation not found, incomplete strategy
% 3.53/0.89 % (370760)Time elapsed: 0.019 s
% 3.53/0.89 % (370760)Peak memory usage: 13 MB
% 3.53/0.89 % (370760)Instructions burned: 37 (million)
% 3.53/0.89 % (370760)------------------------------
% 3.53/0.89 % (370760)------------------------------
% 3.53/0.89 % (370762)Instruction limit reached!
% 3.53/0.89 % (370762)------------------------------
% 3.53/0.89 % (370762)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.53/0.89 % (370762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.53/0.89 % (370762)CaDiCaL version: 2.1.3
% 3.53/0.89 % (370762)Termination reason: Instruction limit
% 3.53/0.89 % (370762)Termination phase: Saturation
% 3.53/0.89 % (370762)Time elapsed: 0.015 s
% 3.53/0.89 % (370762)Peak memory usage: 12 MB
% 3.53/0.89 % (370762)Instructions burned: 28 (million)
% 3.53/0.89 % (370766)dis+10_32_sil=128000:tgt=ground:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=32,1:uwa=one_side_interpreted:nwc=1:random_seed=1063182730:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2994 on theBenchmark for (2994ds/340Mi)
% 3.53/0.89 % (370768)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=2500347347:i=227:sd=1:bd=all:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/227Mi)
% 3.53/0.89 % (370768)Refutation not found, incomplete strategy
% 3.53/0.89 % (370768)------------------------------
% 3.53/0.89 % (370768)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.53/0.89 % (370768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.53/0.89 % (370768)CaDiCaL version: 2.1.3
% 4.04/0.94 % (370768)Termination reason: Refutation not found, incomplete strategy
% 4.04/0.94 % (370768)Time elapsed: 0.002 s
% 4.04/0.94 % (370768)Peak memory usage: 12 MB
% 4.04/0.94 % (370768)Instructions burned: 2 (million)
% 4.04/0.94 % (370768)------------------------------
% 4.04/0.94 % (370768)------------------------------
% 4.04/0.94 % (370769)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 4.04/0.94 % (370769)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=2890174352:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/373Mi)
% 4.04/0.94 % (370729)Instruction limit reached!
% 4.04/0.94 % (370729)------------------------------
% 4.04/0.94 % (370729)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.04/0.94 % (370729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.04/0.94 % (370729)CaDiCaL version: 2.1.3
% 4.04/0.94 % (370729)Termination reason: Instruction limit
% 4.04/0.94 % (370729)Termination phase: Saturation
% 4.04/0.94 % (370729)Time elapsed: 0.239 s
% 4.04/0.94 % (370729)Peak memory usage: 15 MB
% 4.04/0.94 % (370729)Instructions burned: 515 (million)
% 4.04/0.94 % (370772)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=2823501094:i=116:ep=RSTC:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/116Mi)
% 4.04/0.94 % (370772)Refutation not found, incomplete strategy
% 4.04/0.94 % (370772)------------------------------
% 4.04/0.94 % (370772)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.04/0.94 % (370772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.04/0.94 % (370772)CaDiCaL version: 2.1.3
% 4.04/0.94 % (370772)Termination reason: Refutation not found, incomplete strategy
% 4.04/0.94 % (370772)Time elapsed: 0.003 s
% 4.04/0.94 % (370772)Peak memory usage: 12 MB
% 4.04/0.94 % (370772)Instructions burned: 6 (million)
% 4.04/0.94 % (370772)------------------------------
% 4.04/0.94 % (370772)------------------------------
% 4.04/0.94 % (370775)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=2588513741:i=575:rtra=on_2994 on theBenchmark for (2994ds/575Mi)
% 4.04/0.94 % (370775)Refutation not found, incomplete strategy
% 4.04/0.94 % (370775)------------------------------
% 4.04/0.94 % (370775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.04/0.94 % (370775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.04/0.94 % (370775)CaDiCaL version: 2.1.3
% 4.04/0.94 % (370775)Termination reason: Refutation not found, incomplete strategy
% 4.04/0.94 % (370775)Time elapsed: 0.003 s
% 4.04/0.94 % (370775)Peak memory usage: 12 MB
% 4.04/0.94 % (370775)Instructions burned: 6 (million)
% 4.04/0.94 % (370775)------------------------------
% 4.04/0.94 % (370775)------------------------------
% 4.04/0.94 % (370776)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=96760931:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2994 on theBenchmark for (2994ds/270Mi)
% 4.04/0.94 % (370779)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=559128009:hsq=on:hsqr=16,1:s2a=on:i=9840:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2994 on theBenchmark for (2994ds/9840Mi)
% 4.04/0.94 % (370694)Instruction limit reached!
% 4.04/0.94 % (370694)------------------------------
% 4.04/0.94 % (370694)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.04/0.94 % (370694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.04/0.94 % (370694)CaDiCaL version: 2.1.3
% 4.04/0.94 % (370694)Termination reason: Instruction limit
% 4.04/0.94 % (370694)Termination phase: Saturation
% 4.04/0.94 % (370694)Time elapsed: 0.378 s
% 4.04/0.94 % (370694)Peak memory usage: 14 MB
% 4.04/0.94 % (370694)Instructions burned: 853 (million)
% 4.04/0.94 % (370749)Instruction limit reached!
% 4.04/0.94 % (370749)------------------------------
% 4.04/0.94 % (370749)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.04/0.94 % (370749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.04/0.94 % (370749)CaDiCaL version: 2.1.3
% 4.04/0.94 % (370749)Termination reason: Instruction limit
% 4.04/0.94 % (370749)Termination phase: Saturation
% 4.04/0.94 % (370749)Time elapsed: 0.225 s
% 4.04/0.97 % (370749)Peak memory usage: 14 MB
% 4.04/0.97 % (370749)Instructions burned: 497 (million)
% 4.04/0.97 % (370781)lrs+1010_1_sil=128000:si=on:sos=all:uwa=off:nwc=1:random_seed=600248855:i=421:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/421Mi)
% 4.04/0.97 % (370766)Instruction limit reached!
% 4.04/0.97 % (370766)------------------------------
% 4.04/0.97 % (370766)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.04/0.97 % (370766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.04/0.97 % (370766)CaDiCaL version: 2.1.3
% 4.04/0.97 % (370766)Termination reason: Instruction limit
% 4.04/0.97 % (370766)Termination phase: Saturation
% 4.04/0.97 % (370766)Time elapsed: 0.100 s
% 4.04/0.97 % (370766)Peak memory usage: 13 MB
% 4.04/0.97 % (370766)Instructions burned: 343 (million)
% 4.04/0.97 % (370781)Refutation not found, incomplete strategy
% 4.04/0.97 % (370781)------------------------------
% 4.04/0.97 % (370781)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.04/0.97 % (370781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.04/0.97 % (370781)CaDiCaL version: 2.1.3
% 4.04/0.97 % (370781)Termination reason: Refutation not found, incomplete strategy
% 4.04/0.97 % (370781)Time elapsed: 0.002 s
% 4.04/0.97 % (370781)Peak memory usage: 12 MB
% 4.04/0.97 % (370781)Instructions burned: 2 (million)
% 4.04/0.97 % (370781)------------------------------
% 4.04/0.97 % (370781)------------------------------
% 4.04/0.97 % (370782)WARNING Broken Constraint: if sine_to_age_tolerance(3) 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
% 4.04/0.97 % (370782)lrs+10_40_sil=128000:tgt=full:cnfonf=off:si=on:sp=reverse_frequency:spb=goal_then_units:uwa=off:fd=preordered:nwc=1:random_seed=632710045:avsq=on:i=270:s2at=3:avsqr=1,16:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/270Mi)
% 4.04/0.97 % (370784)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=3477213967:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/31Mi)
% 4.04/0.97 % (370782)Refutation not found, incomplete strategy
% 4.04/0.97 % (370782)------------------------------
% 4.04/0.97 % (370782)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.04/0.97 % (370782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.04/0.97 % (370782)CaDiCaL version: 2.1.3
% 4.04/0.97 % (370782)Termination reason: Refutation not found, incomplete strategy
% 4.04/0.97 % (370782)Time elapsed: 0.005 s
% 4.04/0.97 % (370782)Peak memory usage: 12 MB
% 4.04/0.97 % (370782)Instructions burned: 8 (million)
% 4.04/0.97 % (370782)------------------------------
% 4.04/0.97 % (370782)------------------------------
% 4.04/0.97 % (370784)Refutation not found, incomplete strategy
% 4.04/0.97 % (370784)------------------------------
% 4.04/0.97 % (370784)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.04/0.97 % (370784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.04/0.97 % (370784)CaDiCaL version: 2.1.3
% 4.04/0.97 % (370784)Termination reason: Refutation not found, incomplete strategy
% 4.04/0.97 % (370784)Time elapsed: 0.004 s
% 4.04/0.97 % (370784)Peak memory usage: 12 MB
% 4.04/0.97 % (370784)Instructions burned: 16 (million)
% 4.04/0.97 % (370784)------------------------------
% 4.04/0.97 % (370784)------------------------------
% 4.04/0.97 % (370785)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 4.04/0.97 % (370785)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
% 4.04/0.97 % (370785)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=4086062347:hsqr=1,8:i=1440:s2at=5:add=on:nm=2:rtra=on_2993 on theBenchmark for (2993ds/1440Mi)
% 4.04/0.97 % (370789)lrs+2_16:1_si=on:cbe=off:uwa=interpreted_only:random_seed=1393730817:i=111:add=on:fgj=on:rtra=on:fdi=1024_2993 on theBenchmark for (2993ds/111Mi)
% 4.04/0.97 % (370789)Refutation not found, incomplete strategy
% 4.04/0.97 % (370789)------------------------------
% 4.04/0.97 % (370789)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.04/0.97 % (370789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.04/0.97 % (370789)CaDiCaL version: 2.1.3
% 4.04/0.97 % (370789)Termination reason: Refutation not found, incomplete strategy
% 4.04/0.97 % (370789)Time elapsed: 0.002 s
% 4.04/0.97 % (370789)Peak memory usage: 12 MB
% 4.04/0.97 % (370789)Instructions burned: 8 (million)
% 4.04/0.97 % (370789)------------------------------
% 4.04/0.97 % (370789)------------------------------
% 4.04/0.97 % (370788)dis+10_2_sil=128000:si=on:random_seed=3671179162:s2a=on:i=339:av=off:rtra=on:fe=abstraction:ss=axioms:fsd=on:ntd=on_2993 on theBenchmark for (2993ds/339Mi)
% 4.04/0.97 % (370788)Refutation not found, incomplete strategy
% 4.04/0.97 % (370788)------------------------------
% 4.04/0.97 % (370788)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.04/0.97 % (370788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.04/0.97 % (370788)CaDiCaL version: 2.1.3
% 4.04/0.97 % (370788)Termination reason: Refutation not found, incomplete strategy
% 4.04/0.97 % (370788)Time elapsed: 0.002 s
% 4.04/0.97 % (370788)Peak memory usage: 12 MB
% 4.04/0.97 % (370788)Instructions burned: 3 (million)
% 4.04/0.97 % (370788)------------------------------
% 4.04/0.97 % (370788)------------------------------
% 4.04/0.97 % (370792)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=2419889945:st=3:avsq=on:i=122:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2993 on theBenchmark for (2993ds/122Mi)
% 4.04/0.97 % (370792)Refutation not found, incomplete strategy
% 4.04/0.97 % (370792)------------------------------
% 4.04/0.97 % (370792)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.04/0.97 % (370792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.04/0.97 % (370792)CaDiCaL version: 2.1.3
% 4.04/0.97 % (370792)Termination reason: Refutation not found, incomplete strategy
% 4.04/0.97 % (370792)Time elapsed: 0.002 s
% 4.04/0.97 % (370792)Peak memory usage: 12 MB
% 4.04/0.97 % (370792)Instructions burned: 6 (million)
% 4.04/0.97 % (370792)------------------------------
% 4.04/0.97 % (370792)------------------------------
% 4.04/0.97 % (370796)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=3751701300:hsq=on:st=2:i=232:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2993 on theBenchmark for (2993ds/232Mi)
% 4.04/0.97 % (370794)dis+1010_3:2_anc=all_dependent:sil=128000:si=on:sos=on:lma=off:spb=goal_then_units:bce=on:fd=off:random_seed=3840538105:uwa_fpi=on:avsq=on:i=136:avsqr=1,32:hud=15:nm=0:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/136Mi)
% 4.04/0.97 % (370794)Refutation not found, incomplete strategy
% 4.04/0.97 % (370794)------------------------------
% 4.04/0.97 % (370794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.04/0.97 % (370794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.04/0.97 % (370794)CaDiCaL version: 2.1.3
% 4.04/0.97 % (370794)Termination reason: Refutation not found, incomplete strategy
% 4.04/0.97 % (370794)Time elapsed: 0.003 s
% 4.04/0.97 % (370794)Peak memory usage: 12 MB
% 4.04/0.97 % (370794)Instructions burned: 6 (million)
% 4.04/0.97 % (370794)------------------------------
% 4.04/0.97 % (370794)------------------------------
% 4.04/0.97 % (370769)Instruction limit reached!
% 4.04/0.97 % (370769)------------------------------
% 4.04/0.97 % (370769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.04/0.97 % (370769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.04/0.97 % (370769)CaDiCaL version: 2.1.3
% 4.04/0.97 % (370769)Termination reason: Instruction limit
% 4.04/0.97 % (370769)Termination phase: Saturation
% 4.04/0.97 % (370769)Time elapsed: 0.159 s
% 4.04/0.97 % (370769)Peak memory usage: 15 MB
% 4.04/0.97 % (370769)Instructions burned: 374 (million)
% 4.04/0.97 % (370776)Instruction limit reached!
% 4.04/0.97 % (370776)------------------------------
% 4.04/0.97 % (370776)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.04/0.97 % (370776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.04/0.97 % (370776)CaDiCaL version: 2.1.3
% 4.04/0.97 % (370776)Termination reason: Instruction limit
% 4.04/0.97 % (370776)Termination phase: Saturation
% 4.04/0.97 % (370776)Time elapsed: 0.126 s
% 4.04/0.97 % (370776)Peak memory usage: 13 MB
% 4.04/0.97 % (370776)Instructions burned: 272 (million)
% 4.04/0.97 % (370799)lrs+1010_8:1_sil=128000:tgt=ground:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:sos=on:plsqr=256,1:uwa=off:random_seed=1004377432:i=1254:kws=precedence:bd=preordered:av=off:rtra=on_2993 on theBenchmark for (2993ds/1254Mi)
% 4.04/0.97 % (370785) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-370608-370785"...
% 4.04/0.97 % (370800)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 4.04/0.97 % (370800)dis+1002_5:4_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_simp:si=on:plsqr=878,253:plsql=on:uwa=interpreted_only:lwlo=on:random_seed=2256916751:s2a=on:i=281:add=on:rtra=on:fe=axiom:fdi=1024_2992 on theBenchmark for (2992ds/281Mi)
% 4.04/0.97 % (370801)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=3821944799:i=619:add=on:rtra=on_2992 on theBenchmark for (2992ds/619Mi)
% 4.04/0.97 % (370785)...printing done.
% 4.04/0.97 % (370785)Refutation found. Thanks to Tanya!
% 4.04/0.97 % SZS status Theorem for theBenchmark
% 4.04/0.97 % SZS output start Proof for theBenchmark
% 4.04/0.97 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 4.04/0.97 thf(func_def_0, type, eps: (($i > $o) > $i)).
% 4.04/0.97 thf(func_def_2, type, case: (($o > $o) > $i > $i > $i > $i > $i)).
% 4.04/0.97 thf(func_def_3, type, vNOT: ($o > $o)).
% 4.04/0.97 thf(func_def_4, type, f0: ($o > $o)).
% 4.04/0.97 thf(func_def_5, type, f1: ($o > $o)).
% 4.04/0.97 thf(func_def_6, type, f2: ($o > $o)).
% 4.04/0.97 thf(func_def_7, type, f3: ($o > $o)).
% 4.04/0.97 thf(func_def_10, type, vOR: ($o > $o > $o)).
% 4.04/0.97 thf(func_def_11, type, vAND: ($o > $o > $o)).
% 4.04/0.97 thf(func_def_12, type, db5: !>[X0: $tType]:(X0)).
% 4.04/0.97 thf(func_def_13, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 4.04/0.97 thf(func_def_14, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 4.04/0.97 thf(func_def_15, type, db4: !>[X0: $tType]:(X0)).
% 4.04/0.97 thf(func_def_16, type, db0: !>[X0: $tType]:(X0)).
% 4.04/0.97 thf(func_def_17, type, db2: !>[X0: $tType]:(X0)).
% 4.04/0.97 thf(func_def_18, type, db1: !>[X0: $tType]:(X0)).
% 4.04/0.97 thf(func_def_19, type, db3: !>[X0: $tType]:(X0)).
% 4.04/0.97 thf(func_def_29, type, sK9: $o).
% 4.04/0.97 thf(func_def_30, type, sK10: $o).
% 4.04/0.97 thf(func_def_31, type, sK11: $o).
% 4.04/0.97 thf(func_def_32, type, sK12: $o).
% 4.04/0.97 thf(func_def_33, type, sK13: $o).
% 4.04/0.97 thf(func_def_34, type, sK14: $o).
% 4.04/0.97 thf(func_def_35, type, sK15: $o).
% 4.04/0.97 thf(func_def_36, type, sK16: $o).
% 4.04/0.97 thf(func_def_37, type, sK17: $o).
% 4.04/0.97 thf(func_def_38, type, sK18: $o).
% 4.04/0.97 thf(func_def_39, type, sK19: $o).
% 4.04/0.97 thf(func_def_40, type, sK20: $o).
% 4.04/0.97 thf(func_def_41, type, sK21: $o).
% 4.04/0.97 thf(func_def_42, type, sK22: $o).
% 4.04/0.97 thf(func_def_43, type, sK23: $o).
% 4.04/0.97 thf(func_def_44, type, sK24: $o).
% 4.04/0.97 thf(func_def_45, type, sK25: $o).
% 4.04/0.97 thf(func_def_46, type, sK26: $o).
% 4.04/0.97 thf(func_def_47, type, sK27: $o).
% 4.04/0.97 thf(func_def_48, type, sK28: $o).
% 4.04/0.97 thf(func_def_49, type, sK29: $o).
% 4.04/0.97 thf(func_def_50, type, sK30: $o).
% 4.04/0.97 thf(func_def_51, type, sK31: $o).
% 4.04/0.97 thf(func_def_52, type, sK32: $o).
% 4.04/0.97 thf(func_def_53, type, sK33: $o).
% 4.04/0.97 thf(func_def_54, type, sK34: $o).
% 4.04/0.97 thf(func_def_55, type, sK35: $o).
% 4.04/0.97 thf(func_def_56, type, sK36: $o).
% 4.04/0.97 thf(func_def_57, type, sK37: $o).
% 4.04/0.97 thf(func_def_58, type, sK38: $o).
% 4.04/0.97 thf(func_def_59, type, sK39: $o).
% 4.04/0.97 thf(f1,axiom,(
% 4.04/0.97 ! [X0 : ($i > $o)] : (? [X1 : $i] : (X0 @ X1) => (X0 @ (eps @ X0)))),
% 4.04/0.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',choiceax)).
% 4.04/0.97 thf(f2,axiom,(
% 4.04/0.97 (case = (^[X0 : ($o > $o), X1 : $i, X2 : $i, X3 : $i, X4 : $i] : ((eps @ (^[X5 : $i] : (((X0 = ~) & (X5 = X2)) | ((X5 = X4) & (X0 = (^[X6 : $o] : ($true)))) | ((X5 = X3) & (X0 = (^[X6 : $o] : (X6)))) | ((X5 = X1) & (X0 = (^[X6 : $o] : ($false))))))))))),
% 4.04/0.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',caseood)).
% 4.04/0.97 thf(f3,axiom,(
% 4.04/0.97 (((f0 @ $false)) = $false)),
% 4.04/0.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f0f)).
% 4.04/0.97 thf(f4,axiom,(
% 4.04/0.97 (((f0 @ $true)) = $false)),
% 4.04/0.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f0t)).
% 4.04/0.97 thf(f5,axiom,(
% 4.04/0.97 (((f1 @ $false)) = $true)),
% 4.04/0.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f1f)).
% 4.04/0.97 thf(f6,axiom,(
% 4.04/0.97 ($false = ((f1 @ $true)))),
% 4.04/0.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f1t)).
% 4.04/0.97 thf(f7,axiom,(
% 4.04/0.97 (((f2 @ $false)) = $false)),
% 4.04/0.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f2f)).
% 4.04/0.97 thf(f8,axiom,(
% 4.04/0.97 (((f2 @ $true)) = $true)),
% 4.04/0.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f2t)).
% 4.04/0.97 thf(f9,axiom,(
% 4.04/0.97 (((f3 @ $false)) = $true)),
% 4.04/0.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f3f)).
% 4.04/0.97 thf(f10,axiom,(
% 4.04/0.97 (((f3 @ $true)) = $true)),
% 4.04/0.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f3t)).
% 4.04/0.97 thf(f11,conjecture,(
% 4.04/0.97 ! [X2 : $i,X0 : $i,X1 : $i,X3 : $i] : ((((case @ f2 @ X0 @ X1 @ X2 @ X3)) = X2) & (((case @ f3 @ X0 @ X1 @ X2 @ X3)) = X3) & (((case @ f0 @ X0 @ X1 @ X2 @ X3)) = X0) & (((case @ f1 @ X0 @ X1 @ X2 @ X3)) = X1))),
% 4.04/0.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj)).
% 4.04/0.97 thf(f12,negated_conjecture,(
% 4.04/0.97 ~ ! [X2 : $i,X0 : $i,X1 : $i,X3 : $i] : ((((case @ f2 @ X0 @ X1 @ X2 @ X3)) = X2) & (((case @ f3 @ X0 @ X1 @ X2 @ X3)) = X3) & (((case @ f0 @ X0 @ X1 @ X2 @ X3)) = X0) & (((case @ f1 @ X0 @ X1 @ X2 @ X3)) = X1))),
% 4.04/0.97 inference(negated_conjecture,[status(cth)],[f11])).
% 4.04/0.97 thf(f13,plain,(
% 4.04/0.97 ! [X0 : ($i > $o)] : (? [X1 : $i] : (X0 @ X1) => (X0 @ (eps @ X0)))),
% 4.04/0.97 inference(rectify,[],[f1])).
% 4.04/0.97 thf(f14,plain,(
% 4.04/0.97 ! [X0 : ($i > $o)] : (? [X1 : $i] : (((X0 @ X1)) = $true) => (((X0 @ (eps @ X0))) = $true))),
% 4.04/0.97 inference(fool_elimination,[],[f13])).
% 4.04/0.97 thf(f15,plain,(
% 4.04/0.97 ($false = ((f1 @ $true)))),
% 4.04/0.97 inference(rectify,[],[f6])).
% 4.04/0.97 thf(f16,plain,(
% 4.04/0.97 ($false = ((f1 @ $true)))),
% 4.04/0.97 inference(fool_elimination,[],[f15])).
% 4.04/0.97 thf(f17,plain,(
% 4.04/0.97 (((f1 @ $false)) = $true)),
% 4.04/0.97 inference(rectify,[],[f5])).
% 4.04/0.97 thf(f18,plain,(
% 4.04/0.97 ($true = ((f1 @ $false)))),
% 4.04/0.97 inference(fool_elimination,[],[f17])).
% 4.04/0.97 thf(f19,plain,(
% 4.04/0.97 (((f3 @ $false)) = $true)),
% 4.04/0.97 inference(rectify,[],[f9])).
% 4.04/0.97 thf(f20,plain,(
% 4.04/0.97 (((f3 @ $false)) = $true)),
% 4.04/0.97 inference(fool_elimination,[],[f19])).
% 4.04/0.97 thf(f21,plain,(
% 4.04/0.97 (((f2 @ $true)) = $true)),
% 4.04/0.97 inference(rectify,[],[f8])).
% 4.04/0.97 thf(f22,plain,(
% 4.04/0.97 (((f2 @ $true)) = $true)),
% 4.04/0.97 inference(fool_elimination,[],[f21])).
% 4.04/0.97 thf(f23,plain,(
% 4.04/0.97 (((f0 @ $false)) = $false)),
% 4.04/0.97 inference(rectify,[],[f3])).
% 4.04/0.97 thf(f24,plain,(
% 4.04/0.97 ($false = ((f0 @ $false)))),
% 4.04/0.97 inference(fool_elimination,[],[f23])).
% 4.04/0.97 thf(f25,plain,(
% 4.04/0.97 (((f0 @ $true)) = $false)),
% 4.04/0.97 inference(rectify,[],[f4])).
% 4.04/0.97 thf(f26,plain,(
% 4.04/0.97 ($false = ((f0 @ $true)))),
% 4.04/0.97 inference(fool_elimination,[],[f25])).
% 4.04/0.97 thf(f27,plain,(
% 4.04/0.97 (((f3 @ $true)) = $true)),
% 4.04/0.97 inference(rectify,[],[f10])).
% 4.04/0.97 thf(f28,plain,(
% 4.04/0.97 (((f3 @ $true)) = $true)),
% 4.04/0.97 inference(fool_elimination,[],[f27])).
% 4.04/0.97 thf(f29,plain,(
% 4.04/0.97 (((f2 @ $false)) = $false)),
% 4.04/0.97 inference(rectify,[],[f7])).
% 4.04/0.97 thf(f30,plain,(
% 4.04/0.97 ($false = ((f2 @ $false)))),
% 4.04/0.97 inference(fool_elimination,[],[f29])).
% 4.04/0.97 thf(f31,plain,(
% 4.04/0.97 (case = (^[X0 : ($o > $o), X1 : $i, X2 : $i, X3 : $i, X4 : $i] : ((eps @ (^[X5 : $i] : (((X0 = ~) & (X5 = X2)) | ((X5 = X4) & (X0 = (^[X6 : $o] : ($true)))) | ((X5 = X3) & (X0 = (^[X7 : $o] : (X7)))) | ((X5 = X1) & (X0 = (^[X8 : $o] : ($false))))))))))),
% 4.04/0.97 inference(rectify,[],[f2])).
% 4.04/0.97 thf(f32,plain,(
% 4.04/0.97 (case = (^[Y0 : $o > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (eps @ (^[Y5 : $i]: (((((Y0 = (^[Y6 : $o]: ($false))) & (Y1 = Y5)) | ((Y0 = (^[Y6 : $o]: (Y6))) & (Y3 = Y5))) | ((Y0 = (^[Y6 : $o]: ($true))) & (Y4 = Y5))) | ((Y2 = Y5) & (~ = Y0)))))))))))))))),
% 4.04/0.97 inference(fool_elimination,[],[f31])).
% 4.04/0.97 thf(f33,plain,(
% 4.04/0.97 ~ ! [X0 : $i,X3 : $i,X1 : $i,X2 : $i] : ((((case @ f1 @ X1 @ X2 @ X0 @ X3)) = X2) & (((case @ f0 @ X1 @ X2 @ X0 @ X3)) = X1) & (((case @ f3 @ X1 @ X2 @ X0 @ X3)) = X3) & (((case @ f2 @ X1 @ X2 @ X0 @ X3)) = X0))),
% 4.04/0.97 inference(rectify,[],[f12])).
% 4.04/0.97 thf(f34,plain,(
% 4.04/0.97 ! [X0 : ($i > $o)] : ((((X0 @ (eps @ X0))) = $true) | ! [X1 : $i] : (((X0 @ X1)) != $true))),
% 4.04/0.97 inference(ennf_transformation,[],[f14])).
% 4.04/0.97 thf(f35,plain,(
% 4.04/0.97 ? [X1 : $i,X0 : $i,X3 : $i,X2 : $i] : ((((case @ f3 @ X1 @ X2 @ X0 @ X3)) != X3) | (((case @ f1 @ X1 @ X2 @ X0 @ X3)) != X2) | (((case @ f2 @ X1 @ X2 @ X0 @ X3)) != X0) | (((case @ f0 @ X1 @ X2 @ X0 @ X3)) != X1))),
% 4.04/0.97 inference(ennf_transformation,[],[f33])).
% 4.04/0.97 thf(f36,plain,(
% 4.04/0.97 ? [X0 : $i,X1 : $i,X2 : $i,X3 : $i] : ((((case @ f3 @ X0 @ X3 @ X1 @ X2)) != X2) | (((case @ f1 @ X0 @ X3 @ X1 @ X2)) != X3) | (((case @ f2 @ X0 @ X3 @ X1 @ X2)) != X1) | (((case @ f0 @ X0 @ X3 @ X1 @ X2)) != X0))),
% 4.04/0.97 inference(rectify,[],[f35])).
% 4.04/0.97 thf(f37,plain,(
% 4.04/0.97 (sK2 != ((case @ f3 @ sK0 @ sK3 @ sK1 @ sK2))) | (sK3 != ((case @ f1 @ sK0 @ sK3 @ sK1 @ sK2))) | (((case @ f2 @ sK0 @ sK3 @ sK1 @ sK2)) != sK1) | (sK0 != ((case @ f0 @ sK0 @ sK3 @ sK1 @ sK2)))),
% 4.04/0.97 inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3)],[f36])).
% 4.04/0.97 thf(f38,plain,(
% 4.04/0.97 (sK2 != ((case @ f3 @ sK0 @ sK3 @ sK1 @ sK2))) | (sK3 != ((case @ f1 @ sK0 @ sK3 @ sK1 @ sK2))) | (((case @ f2 @ sK0 @ sK3 @ sK1 @ sK2)) != sK1) | (sK0 != ((case @ f0 @ sK0 @ sK3 @ sK1 @ sK2)))),
% 4.04/0.97 inference(cnf_transformation,[],[f37])).
% 4.04/0.97 thf(f39,plain,(
% 4.04/0.97 (((f3 @ $true)) = $true)),
% 4.04/0.97 inference(cnf_transformation,[],[f28])).
% 4.04/0.97 thf(f40,plain,(
% 4.04/0.97 (((f2 @ $true)) = $true)),
% 4.04/0.97 inference(cnf_transformation,[],[f22])).
% 4.04/0.97 thf(f41,plain,(
% 4.04/0.97 ($false = ((f0 @ $true)))),
% 4.04/0.97 inference(cnf_transformation,[],[f26])).
% 4.04/0.97 thf(f42,plain,(
% 4.04/0.97 ($false = ((f0 @ $false)))),
% 4.04/0.97 inference(cnf_transformation,[],[f24])).
% 4.04/0.97 thf(f43,plain,(
% 4.04/0.97 ( ! [X0 : ($i > $o),X1 : $i] : ((((X0 @ (eps @ X0))) = $true) | (((X0 @ X1)) != $true)) )),
% 4.04/0.97 inference(cnf_transformation,[],[f34])).
% 4.04/0.97 thf(f44,plain,(
% 4.04/0.97 (case = (^[Y0 : $o > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (eps @ (^[Y5 : $i]: (((((Y0 = (^[Y6 : $o]: ($false))) & (Y1 = Y5)) | ((Y0 = (^[Y6 : $o]: (Y6))) & (Y3 = Y5))) | ((Y0 = (^[Y6 : $o]: ($true))) & (Y4 = Y5))) | ((Y2 = Y5) & (~ = Y0)))))))))))))))),
% 4.04/0.97 inference(cnf_transformation,[],[f32])).
% 4.04/0.97 thf(f45,plain,(
% 4.04/0.97 ($true = ((f1 @ $false)))),
% 4.04/0.97 inference(cnf_transformation,[],[f18])).
% 4.04/0.97 thf(f46,plain,(
% 4.04/0.97 (((f3 @ $false)) = $true)),
% 4.04/0.97 inference(cnf_transformation,[],[f20])).
% 4.04/0.97 thf(f47,plain,(
% 4.04/0.97 ($false = ((f1 @ $true)))),
% 4.04/0.97 inference(cnf_transformation,[],[f16])).
% 4.04/0.97 thf(f48,plain,(
% 4.04/0.97 ($false = ((f2 @ $false)))),
% 4.04/0.97 inference(cnf_transformation,[],[f30])).
% 4.04/0.97 thf(f50,definition,(
% 4.04/0.97 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 4.04/0.97 introduced(theory,[fool_exhaustiveness_axiom])).
% 4.04/0.97 thf(f51,plain,(
% 4.04/0.97 (sK2 != (((^[Y0 : $o > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (eps @ (^[Y5 : $i]: (((((Y0 = (^[Y6 : $o]: ($false))) & (Y1 = Y5)) | ((Y0 = (^[Y6 : $o]: (Y6))) & (Y3 = Y5))) | ((Y0 = (^[Y6 : $o]: ($true))) & (Y4 = Y5))) | ((Y2 = Y5) & (~ = Y0)))))))))))))) @ f3 @ sK0 @ sK3 @ sK1 @ sK2))) | (sK3 != (((^[Y0 : $o > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (eps @ (^[Y5 : $i]: (((((Y0 = (^[Y6 : $o]: ($false))) & (Y1 = Y5)) | ((Y0 = (^[Y6 : $o]: (Y6))) & (Y3 = Y5))) | ((Y0 = (^[Y6 : $o]: ($true))) & (Y4 = Y5))) | ((Y2 = Y5) & (~ = Y0)))))))))))))) @ f1 @ sK0 @ sK3 @ sK1 @ sK2))) | ((((^[Y0 : $o > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (eps @ (^[Y5 : $i]: (((((Y0 = (^[Y6 : $o]: ($false))) & (Y1 = Y5)) | ((Y0 = (^[Y6 : $o]: (Y6))) & (Y3 = Y5))) | ((Y0 = (^[Y6 : $o]: ($true))) & (Y4 = Y5))) | ((Y2 = Y5) & (~ = Y0)))))))))))))) @ f2 @ sK0 @ sK3 @ sK1 @ sK2)) != sK1) | ((((^[Y0 : $o > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (eps @ (^[Y5 : $i]: (((((Y0 = (^[Y6 : $o]: ($false))) & (Y1 = Y5)) | ((Y0 = (^[Y6 : $o]: (Y6))) & (Y3 = Y5))) | ((Y0 = (^[Y6 : $o]: ($true))) & (Y4 = Y5))) | ((Y2 = Y5) & (~ = Y0)))))))))))))) @ f0 @ sK0 @ sK3 @ sK1 @ sK2)) != sK0)),
% 4.04/0.97 inference(definition_unfolding,[],[f38,f44,f44,f44,f44])).
% 4.04/0.97 thf(f52,definition,(
% 4.04/0.97 (sF4 = (((^[Y0 : $o > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (eps @ (^[Y5 : $i]: (((((Y0 = (^[Y6 : $o]: ($false))) & (Y1 = Y5)) | ((Y0 = (^[Y6 : $o]: (Y6))) & (Y3 = Y5))) | ((Y0 = (^[Y6 : $o]: ($true))) & (Y4 = Y5))) | ((Y2 = Y5) & (~ = Y0)))))))))))))) @ f3 @ sK0 @ sK3 @ sK1 @ sK2)))),
% 4.04/0.97 introduced(definition,[new_symbols(definition,[sF4])],[function_definition])).
% 4.04/0.97 thf(f53,definition,(
% 4.04/0.97 (sF5 = (((^[Y0 : $o > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (eps @ (^[Y5 : $i]: (((((Y0 = (^[Y6 : $o]: ($false))) & (Y1 = Y5)) | ((Y0 = (^[Y6 : $o]: (Y6))) & (Y3 = Y5))) | ((Y0 = (^[Y6 : $o]: ($true))) & (Y4 = Y5))) | ((Y2 = Y5) & (~ = Y0)))))))))))))) @ f1 @ sK0 @ sK3 @ sK1 @ sK2)))),
% 4.04/0.97 introduced(definition,[new_symbols(definition,[sF5])],[function_definition])).
% 4.04/0.97 thf(f54,plain,(
% 4.04/0.97 ((((^[Y0 : $o > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (eps @ (^[Y5 : $i]: (((((Y0 = (^[Y6 : $o]: ($false))) & (Y1 = Y5)) | ((Y0 = (^[Y6 : $o]: (Y6))) & (Y3 = Y5))) | ((Y0 = (^[Y6 : $o]: ($true))) & (Y4 = Y5))) | ((Y2 = Y5) & (~ = Y0)))))))))))))) @ f1 @ sK0 @ sK3 @ sK1 @ sK2)) = sF5)),
% 4.04/0.97 inference(reorient_equations,[],[f53])).
% 4.04/0.97 thf(f55,definition,(
% 4.04/0.97 (sF6 = (((^[Y0 : $o > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (eps @ (^[Y5 : $i]: (((((Y0 = (^[Y6 : $o]: ($false))) & (Y1 = Y5)) | ((Y0 = (^[Y6 : $o]: (Y6))) & (Y3 = Y5))) | ((Y0 = (^[Y6 : $o]: ($true))) & (Y4 = Y5))) | ((Y2 = Y5) & (~ = Y0)))))))))))))) @ f2 @ sK0 @ sK3 @ sK1 @ sK2)))),
% 4.04/0.97 introduced(definition,[new_symbols(definition,[sF6])],[function_definition])).
% 4.04/0.97 thf(f56,plain,(
% 4.04/0.97 ((((^[Y0 : $o > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (eps @ (^[Y5 : $i]: (((((Y0 = (^[Y6 : $o]: ($false))) & (Y1 = Y5)) | ((Y0 = (^[Y6 : $o]: (Y6))) & (Y3 = Y5))) | ((Y0 = (^[Y6 : $o]: ($true))) & (Y4 = Y5))) | ((Y2 = Y5) & (~ = Y0)))))))))))))) @ f2 @ sK0 @ sK3 @ sK1 @ sK2)) = sF6)),
% 4.04/0.97 inference(reorient_equations,[],[f55])).
% 4.04/0.97 thf(f57,definition,(
% 4.04/0.97 (sF7 = (((^[Y0 : $o > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (eps @ (^[Y5 : $i]: (((((Y0 = (^[Y6 : $o]: ($false))) & (Y1 = Y5)) | ((Y0 = (^[Y6 : $o]: (Y6))) & (Y3 = Y5))) | ((Y0 = (^[Y6 : $o]: ($true))) & (Y4 = Y5))) | ((Y2 = Y5) & (~ = Y0)))))))))))))) @ f0 @ sK0 @ sK3 @ sK1 @ sK2)))),
% 4.04/0.97 introduced(definition,[new_symbols(definition,[sF7])],[function_definition])).
% 4.04/0.97 thf(f58,plain,(
% 4.04/0.97 ((((^[Y0 : $o > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (eps @ (^[Y5 : $i]: (((((Y0 = (^[Y6 : $o]: ($false))) & (Y1 = Y5)) | ((Y0 = (^[Y6 : $o]: (Y6))) & (Y3 = Y5))) | ((Y0 = (^[Y6 : $o]: ($true))) & (Y4 = Y5))) | ((Y2 = Y5) & (~ = Y0)))))))))))))) @ f0 @ sK0 @ sK3 @ sK1 @ sK2)) = sF7)),
% 4.04/0.97 inference(reorient_equations,[],[f57])).
% 4.04/0.97 thf(f59,plain,(
% 4.04/0.97 (sK3 != sF5) | (sF6 != sK1) | (sK2 != sF4) | (sK0 != sF7)),
% 4.04/0.97 inference(definition_folding,[],[f51,f58,f56,f54,f52])).
% 4.04/0.97 thf(f60,plain,(
% 4.04/0.97 (sF4 = ((eps @ (^[Y0 : $i]: (((((f3 = (^[Y1 : $o]: ($false))) & (sK0 = Y0)) | ((f3 = (^[Y1 : $o]: (Y1))) & (sK1 = Y0))) | ((f3 = (^[Y1 : $o]: ($true))) & (sK2 = Y0))) | ((sK3 = Y0) & (~ = f3)))))))),
% 4.04/0.97 inference(beta-eta_normalization,[],[f52])).
% 4.04/0.97 thf(f61,plain,(
% 4.04/0.97 (sF7 = ((eps @ (^[Y0 : $i]: (((((f0 = (^[Y1 : $o]: ($false))) & (sK0 = Y0)) | ((f0 = (^[Y1 : $o]: (Y1))) & (sK1 = Y0))) | ((f0 = (^[Y1 : $o]: ($true))) & (sK2 = Y0))) | ((sK3 = Y0) & (~ = f0)))))))),
% 4.04/0.97 inference(beta-eta_normalization,[],[f58])).
% 4.04/0.97 thf(f62,plain,(
% 4.04/0.97 (((eps @ (^[Y0 : $i]: (((((f1 = (^[Y1 : $o]: ($false))) & (sK0 = Y0)) | ((f1 = (^[Y1 : $o]: (Y1))) & (sK1 = Y0))) | ((f1 = (^[Y1 : $o]: ($true))) & (sK2 = Y0))) | ((sK3 = Y0) & (~ = f1)))))) = sF5)),
% 4.04/0.97 inference(beta-eta_normalization,[],[f54])).
% 4.04/0.97 thf(f63,plain,(
% 4.04/0.97 (sF6 = ((eps @ (^[Y0 : $i]: (((((f2 = (^[Y1 : $o]: ($false))) & (sK0 = Y0)) | ((f2 = (^[Y1 : $o]: (Y1))) & (sK1 = Y0))) | ((f2 = (^[Y1 : $o]: ($true))) & (sK2 = Y0))) | ((sK3 = Y0) & (~ = f2)))))))),
% 4.04/0.97 inference(beta-eta_normalization,[],[f56])).
% 4.04/0.97 thf(f65,definition,(
% 4.04/0.97 spl8_1 <=> (sK0 = sF7)),
% 4.04/0.97 introduced(definition,[new_symbols(definition,[spl8_1])],[avatar_definition])).
% 4.04/0.97 thf(f69,definition,(
% 4.04/0.97 spl8_2 <=> (sF6 = sK1)),
% 4.04/0.97 introduced(definition,[new_symbols(definition,[spl8_2])],[avatar_definition])).
% 4.04/0.97 thf(f73,definition,(
% 4.04/0.97 spl8_3 <=> (sK2 = sF4)),
% 4.04/0.97 introduced(definition,[new_symbols(definition,[spl8_3])],[avatar_definition])).
% 4.04/0.97 thf(f77,definition,(
% 4.04/0.97 spl8_4 <=> (sK3 = sF5)),
% 4.04/0.97 introduced(definition,[new_symbols(definition,[spl8_4])],[avatar_definition])).
% 4.04/0.97 thf(f80,plain,(
% 4.04/0.97 ~spl8_1 | ~spl8_2 | ~spl8_3 | ~spl8_4),
% 4.04/0.97 inference(avatar_split_clause,[],[f59,f77,f73,f69,f65])).
% 4.04/0.97 thf(f88,plain,(
% 4.04/0.97 ( ! [X0 : $o] : (($false = X0) | (((f3 @ X0)) = X0)) )),
% 4.04/0.97 inference(constrained_superposition,[],[f39,f50])).
% 4.04/0.97 thf(f89,plain,(
% 4.04/0.97 ( ! [X0 : $o] : (($false = X0) | ($false = X0) | (((f3 @ X0)) = $true)) )),
% 4.04/0.97 inference(iff_proxy_clausification,[],[f88])).
% 4.04/0.97 thf(f91,plain,(
% 4.04/0.97 ( ! [X0 : $o] : ((((f3 @ X0)) = $true) | ($false = X0)) )),
% 4.04/0.97 inference(duplicate_literal_removal,[],[f89])).
% 4.04/0.97 thf(f96,plain,(
% 4.04/0.97 ( ! [X0 : $o] : (($false = ((f0 @ X0))) | ($false = X0)) )),
% 4.04/0.97 inference(constrained_superposition,[],[f41,f50])).
% 4.04/0.97 thf(f110,plain,(
% 4.04/0.97 ( ! [X0 : $i] : (($true != (((^[Y0 : $i]: (((((f3 = (^[Y1 : $o]: ($false))) & (sK0 = Y0)) | ((f3 = (^[Y1 : $o]: (Y1))) & (sK1 = Y0))) | ((f3 = (^[Y1 : $o]: ($true))) & (sK2 = Y0))) | ((sK3 = Y0) & (~ = f3)))) @ X0))) | ((((^[Y0 : $i]: (((((f3 = (^[Y1 : $o]: ($false))) & (sK0 = Y0)) | ((f3 = (^[Y1 : $o]: (Y1))) & (sK1 = Y0))) | ((f3 = (^[Y1 : $o]: ($true))) & (sK2 = Y0))) | ((sK3 = Y0) & (~ = f3)))) @ sF4)) = $true)) )),
% 4.04/0.97 inference(constrained_superposition,[],[f43,f60])).
% 4.04/0.97 thf(f111,plain,(
% 4.04/0.97 ( ! [X0 : $i] : (($true = ((((((f3 = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((f3 = (^[Y0 : $o]: (Y0))) & (sK1 = sF4))) | ((f3 = (^[Y0 : $o]: ($true))) & (sK2 = sF4))) | ((sK3 = sF4) & (~ = f3))))) | (((((((f3 = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((f3 = (^[Y0 : $o]: (Y0))) & (sK1 = X0))) | ((f3 = (^[Y0 : $o]: ($true))) & (sK2 = X0))) | ((sK3 = X0) & (~ = f3)))) != $true)) )),
% 4.04/0.97 inference(beta-eta_normalization,[],[f110])).
% 4.04/0.97 thf(f112,plain,(
% 4.04/0.97 ( ! [X0 : $i] : (((((sK3 = sF4) & (~ = f3))) = $true) | ($true = (((((f3 = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((f3 = (^[Y0 : $o]: (Y0))) & (sK1 = sF4))) | ((f3 = (^[Y0 : $o]: ($true))) & (sK2 = sF4))))) | (((((((f3 = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((f3 = (^[Y0 : $o]: (Y0))) & (sK1 = X0))) | ((f3 = (^[Y0 : $o]: ($true))) & (sK2 = X0))) | ((sK3 = X0) & (~ = f3)))) != $true)) )),
% 4.04/0.97 inference(or_proxy_clausification,[],[f111])).
% 4.04/0.97 thf(f113,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((((~ = f3)) = $true) | (((((((f3 = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((f3 = (^[Y0 : $o]: (Y0))) & (sK1 = X0))) | ((f3 = (^[Y0 : $o]: ($true))) & (sK2 = X0))) | ((sK3 = X0) & (~ = f3)))) != $true) | ($true = (((((f3 = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((f3 = (^[Y0 : $o]: (Y0))) & (sK1 = sF4))) | ((f3 = (^[Y0 : $o]: ($true))) & (sK2 = sF4)))))) )),
% 4.04/0.97 inference(and_proxy_clausification,[],[f112])).
% 4.04/0.97 thf(f286,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((((((((f3 = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((f3 = (^[Y0 : $o]: (Y0))) & (sK1 = X0))) | ((f3 = (^[Y0 : $o]: ($true))) & (sK2 = X0))) | ((sK3 = X0) & (~ = f3)))) != $true) | (~ = f3) | ($true = (((((f3 = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((f3 = (^[Y0 : $o]: (Y0))) & (sK1 = sF4))) | ((f3 = (^[Y0 : $o]: ($true))) & (sK2 = sF4)))))) )),
% 4.04/0.97 inference(equality_proxy_clausification,[],[f113])).
% 4.04/0.97 thf(f288,plain,(
% 4.04/0.97 ( ! [X0 : $i] : (($true = (((((f3 = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((f3 = (^[Y0 : $o]: (Y0))) & (sK1 = sF4))) | ((f3 = (^[Y0 : $o]: ($true))) & (sK2 = sF4))))) | ($false = (((((f3 = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((f3 = (^[Y0 : $o]: (Y0))) & (sK1 = X0))) | ((f3 = (^[Y0 : $o]: ($true))) & (sK2 = X0))))) | (~ = f3)) )),
% 4.04/0.97 inference(or_proxy_clausification,[],[f286])).
% 4.04/0.97 thf(f289,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((((((f3 = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((f3 = (^[Y0 : $o]: (Y0))) & (sK1 = sF4)))) = $true) | (~ = f3) | ($false = (((((f3 = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((f3 = (^[Y0 : $o]: (Y0))) & (sK1 = X0))) | ((f3 = (^[Y0 : $o]: ($true))) & (sK2 = X0))))) | ((((f3 = (^[Y0 : $o]: ($true))) & (sK2 = sF4))) = $true)) )),
% 4.04/0.97 inference(or_proxy_clausification,[],[f288])).
% 4.04/0.97 thf(f290,plain,(
% 4.04/0.97 ( ! [X0 : $i] : (((((f3 = (^[Y0 : $o]: ($false))) & (sK0 = sF4))) = $true) | ((((f3 = (^[Y0 : $o]: (Y0))) & (sK1 = sF4))) = $true) | (~ = f3) | ((((f3 = (^[Y0 : $o]: ($true))) & (sK2 = sF4))) = $true) | ($false = (((((f3 = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((f3 = (^[Y0 : $o]: (Y0))) & (sK1 = X0))) | ((f3 = (^[Y0 : $o]: ($true))) & (sK2 = X0)))))) )),
% 4.04/0.97 inference(or_proxy_clausification,[],[f289])).
% 4.04/0.97 thf(f292,plain,(
% 4.04/0.97 ( ! [X0 : $i] : (($false = (((((f3 = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((f3 = (^[Y0 : $o]: (Y0))) & (sK1 = X0))) | ((f3 = (^[Y0 : $o]: ($true))) & (sK2 = X0))))) | ($true = ((f3 = (^[Y0 : $o]: ($false))))) | ((((f3 = (^[Y0 : $o]: ($true))) & (sK2 = sF4))) = $true) | ((((f3 = (^[Y0 : $o]: (Y0))) & (sK1 = sF4))) = $true) | (~ = f3)) )),
% 4.04/0.97 inference(and_proxy_clausification,[],[f290])).
% 4.04/0.97 thf(f293,plain,(
% 4.04/0.97 ( ! [X0 : $i] : (($true = ((f3 = (^[Y0 : $o]: ($false))))) | ($false = (((f3 = (^[Y0 : $o]: ($true))) & (sK2 = X0)))) | ((((f3 = (^[Y0 : $o]: (Y0))) & (sK1 = sF4))) = $true) | ((((f3 = (^[Y0 : $o]: ($true))) & (sK2 = sF4))) = $true) | (~ = f3)) )),
% 4.04/0.97 inference(or_proxy_clausification,[],[f292])).
% 4.04/0.97 thf(f342,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((f3 = (^[Y0 : $o]: ($false))) | (~ = f3) | ($false = (((f3 = (^[Y0 : $o]: ($true))) & (sK2 = X0)))) | ((((f3 = (^[Y0 : $o]: ($true))) & (sK2 = sF4))) = $true) | ((((f3 = (^[Y0 : $o]: (Y0))) & (sK1 = sF4))) = $true)) )),
% 4.04/0.97 inference(equality_proxy_clausification,[],[f293])).
% 4.04/0.97 thf(f343,plain,(
% 4.04/0.97 ( ! [X0 : $i] : (((((f3 = (^[Y0 : $o]: ($true))) & (sK2 = sF4))) = $true) | ($false = ((f3 = (^[Y0 : $o]: ($true))))) | ((((f3 = (^[Y0 : $o]: (Y0))) & (sK1 = sF4))) = $true) | (~ = f3) | (f3 = (^[Y0 : $o]: ($false))) | ($false = ((sK2 = X0)))) )),
% 4.04/0.97 inference(and_proxy_clausification,[],[f342])).
% 4.04/0.97 thf(f344,plain,(
% 4.04/0.97 ( ! [X0 : $i] : (((((f3 = (^[Y0 : $o]: (Y0))) & (sK1 = sF4))) = $true) | ($false = ((f3 = (^[Y0 : $o]: ($true))))) | (((sK2 = sF4)) = $true) | (~ = f3) | ($false = ((sK2 = X0))) | (f3 = (^[Y0 : $o]: ($false)))) )),
% 4.04/0.97 inference(and_proxy_clausification,[],[f343])).
% 4.04/0.97 thf(f356,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((~ = f3) | ($false = ((sK2 = X0))) | (((f3 = (^[Y0 : $o]: (Y0)))) = $true) | (f3 = (^[Y0 : $o]: ($false))) | (((sK2 = sF4)) = $true) | ($false = ((f3 = (^[Y0 : $o]: ($true)))))) )),
% 4.04/0.97 inference(and_proxy_clausification,[],[f344])).
% 4.04/0.97 thf(f357,plain,(
% 4.04/0.97 ( ! [X0 : $i] : (($false = ((f3 = (^[Y0 : $o]: ($true))))) | (sK2 != X0) | (((sK2 = sF4)) = $true) | (f3 = (^[Y0 : $o]: ($false))) | (((f3 = (^[Y0 : $o]: (Y0)))) = $true) | (~ = f3)) )),
% 4.04/0.97 inference(equality_proxy_clausification,[],[f356])).
% 4.04/0.97 thf(f358,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((f3 != (^[Y0 : $o]: ($true))) | (f3 = (^[Y0 : $o]: ($false))) | (sK2 != X0) | (~ = f3) | (((sK2 = sF4)) = $true) | (((f3 = (^[Y0 : $o]: (Y0)))) = $true)) )),
% 4.04/0.97 inference(equality_proxy_clausification,[],[f357])).
% 4.04/0.97 thf(f359,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((~ = f3) | (((f3 = (^[Y0 : $o]: (Y0)))) = $true) | (sK2 != X0) | (f3 != (^[Y0 : $o]: ($true))) | (f3 = (^[Y0 : $o]: ($false))) | (sK2 = sF4)) )),
% 4.04/0.97 inference(equality_proxy_clausification,[],[f358])).
% 4.04/0.97 thf(f360,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((sK2 = sF4) | (f3 = (^[Y0 : $o]: (Y0))) | (~ = f3) | (sK2 != X0) | (f3 != (^[Y0 : $o]: ($true))) | (f3 = (^[Y0 : $o]: ($false)))) )),
% 4.04/0.97 inference(equality_proxy_clausification,[],[f359])).
% 4.04/0.97 thf(f471,definition,(
% 4.04/0.97 spl8_5 <=> (f3 = (^[Y0 : $o]: (Y0)))),
% 4.04/0.97 introduced(definition,[new_symbols(definition,[spl8_5])],[avatar_definition])).
% 4.04/0.97 thf(f473,plain,(
% 4.04/0.97 (f3 = (^[Y0 : $o]: (Y0))) | ~spl8_5),
% 4.04/0.97 inference(avatar_component_clause,[],[f471])).
% 4.04/0.97 thf(f475,definition,(
% 4.04/0.97 spl8_6 <=> (f3 = (^[Y0 : $o]: ($false)))),
% 4.04/0.97 introduced(definition,[new_symbols(definition,[spl8_6])],[avatar_definition])).
% 4.04/0.97 thf(f476,plain,(
% 4.04/0.97 (f3 = (^[Y0 : $o]: ($false))) | ~spl8_6),
% 4.04/0.97 inference(avatar_component_clause,[],[f475])).
% 4.04/0.97 thf(f477,plain,(
% 4.04/0.97 (f3 != (^[Y0 : $o]: ($false))) | spl8_6),
% 4.04/0.97 inference(avatar_component_clause,[],[f475])).
% 4.04/0.97 thf(f479,definition,(
% 4.04/0.97 spl8_7 <=> ! [X0 : $i] : (sK0 != X0)),
% 4.04/0.97 introduced(definition,[new_symbols(definition,[spl8_7])],[avatar_definition])).
% 4.04/0.97 thf(f480,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((sK0 != X0)) ) | ~spl8_7),
% 4.04/0.97 inference(avatar_component_clause,[],[f479])).
% 4.04/0.97 thf(f490,definition,(
% 4.04/0.97 spl8_10 <=> (f3 = (^[Y0 : $o]: ($true)))),
% 4.04/0.97 introduced(definition,[new_symbols(definition,[spl8_10])],[avatar_definition])).
% 4.04/0.97 thf(f491,plain,(
% 4.04/0.97 (f3 != (^[Y0 : $o]: ($true))) | spl8_10),
% 4.04/0.97 inference(avatar_component_clause,[],[f490])).
% 4.04/0.97 thf(f492,plain,(
% 4.04/0.97 (f3 = (^[Y0 : $o]: ($true))) | ~spl8_10),
% 4.04/0.97 inference(avatar_component_clause,[],[f490])).
% 4.04/0.97 thf(f502,definition,(
% 4.04/0.97 spl8_12 <=> ! [X0 : $i] : (sK1 != X0)),
% 4.04/0.97 introduced(definition,[new_symbols(definition,[spl8_12])],[avatar_definition])).
% 4.04/0.97 thf(f503,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((sK1 != X0)) ) | ~spl8_12),
% 4.04/0.97 inference(avatar_component_clause,[],[f502])).
% 4.04/0.97 thf(f509,definition,(
% 4.04/0.97 spl8_13 <=> ! [X0 : $i] : (sK2 != X0)),
% 4.04/0.97 introduced(definition,[new_symbols(definition,[spl8_13])],[avatar_definition])).
% 4.04/0.97 thf(f510,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((sK2 != X0)) ) | ~spl8_13),
% 4.04/0.97 inference(avatar_component_clause,[],[f509])).
% 4.04/0.97 thf(f516,definition,(
% 4.04/0.97 spl8_14 <=> (~ = f3)),
% 4.04/0.97 introduced(definition,[new_symbols(definition,[spl8_14])],[avatar_definition])).
% 4.04/0.97 thf(f517,plain,(
% 4.04/0.97 (~ = f3) | ~spl8_14),
% 4.04/0.97 inference(avatar_component_clause,[],[f516])).
% 4.04/0.97 thf(f520,definition,(
% 4.04/0.97 spl8_15 <=> ! [X0 : $i] : (sK3 != X0)),
% 4.04/0.97 introduced(definition,[new_symbols(definition,[spl8_15])],[avatar_definition])).
% 4.04/0.97 thf(f521,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((sK3 != X0)) ) | ~spl8_15),
% 4.04/0.97 inference(avatar_component_clause,[],[f520])).
% 4.04/0.97 thf(f532,plain,(
% 4.04/0.97 spl8_14 | spl8_13 | spl8_5 | spl8_3 | spl8_6 | ~spl8_10),
% 4.04/0.97 inference(avatar_split_clause,[],[f360,f490,f475,f73,f471,f509,f516])).
% 4.04/0.97 thf(f556,plain,(
% 4.04/0.97 ( ! [X0 : $i] : (((((^[Y0 : $i]: (((((f0 = (^[Y1 : $o]: ($false))) & (sK0 = Y0)) | ((f0 = (^[Y1 : $o]: (Y1))) & (sK1 = Y0))) | ((f0 = (^[Y1 : $o]: ($true))) & (sK2 = Y0))) | ((sK3 = Y0) & (~ = f0)))) @ sF7)) = $true) | ($true != (((^[Y0 : $i]: (((((f0 = (^[Y1 : $o]: ($false))) & (sK0 = Y0)) | ((f0 = (^[Y1 : $o]: (Y1))) & (sK1 = Y0))) | ((f0 = (^[Y1 : $o]: ($true))) & (sK2 = Y0))) | ((sK3 = Y0) & (~ = f0)))) @ X0)))) )),
% 4.04/0.97 inference(constrained_superposition,[],[f43,f61])).
% 4.04/0.97 thf(f557,plain,(
% 4.04/0.97 ( ! [X0 : $i] : (($true != ((((((f0 = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((f0 = (^[Y0 : $o]: (Y0))) & (sK1 = X0))) | ((f0 = (^[Y0 : $o]: ($true))) & (sK2 = X0))) | ((sK3 = X0) & (~ = f0))))) | (((((((f0 = (^[Y0 : $o]: ($false))) & (sK0 = sF7)) | ((f0 = (^[Y0 : $o]: (Y0))) & (sK1 = sF7))) | ((f0 = (^[Y0 : $o]: ($true))) & (sK2 = sF7))) | ((sK3 = sF7) & (~ = f0)))) = $true)) )),
% 4.04/0.97 inference(beta-eta_normalization,[],[f556])).
% 4.04/0.97 thf(f559,plain,(
% 4.04/0.97 ( ! [X0 : $i] : (($false = (((((f0 = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((f0 = (^[Y0 : $o]: (Y0))) & (sK1 = X0))) | ((f0 = (^[Y0 : $o]: ($true))) & (sK2 = X0))))) | (((((((f0 = (^[Y0 : $o]: ($false))) & (sK0 = sF7)) | ((f0 = (^[Y0 : $o]: (Y0))) & (sK1 = sF7))) | ((f0 = (^[Y0 : $o]: ($true))) & (sK2 = sF7))) | ((sK3 = sF7) & (~ = f0)))) = $true)) )),
% 4.04/0.97 inference(or_proxy_clausification,[],[f557])).
% 4.04/0.97 thf(f561,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((((((((f0 = (^[Y0 : $o]: ($false))) & (sK0 = sF7)) | ((f0 = (^[Y0 : $o]: (Y0))) & (sK1 = sF7))) | ((f0 = (^[Y0 : $o]: ($true))) & (sK2 = sF7))) | ((sK3 = sF7) & (~ = f0)))) = $true) | (((((f0 = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((f0 = (^[Y0 : $o]: (Y0))) & (sK1 = X0)))) = $false)) )),
% 4.04/0.97 inference(or_proxy_clausification,[],[f559])).
% 4.04/0.97 thf(f562,plain,(
% 4.04/0.97 ( ! [X0 : $i] : (($true = (((((f0 = (^[Y0 : $o]: ($false))) & (sK0 = sF7)) | ((f0 = (^[Y0 : $o]: (Y0))) & (sK1 = sF7))) | ((f0 = (^[Y0 : $o]: ($true))) & (sK2 = sF7))))) | (((((f0 = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((f0 = (^[Y0 : $o]: (Y0))) & (sK1 = X0)))) = $false) | ($true = (((sK3 = sF7) & (~ = f0))))) )),
% 4.04/0.97 inference(or_proxy_clausification,[],[f561])).
% 4.04/0.97 thf(f563,plain,(
% 4.04/0.97 ( ! [X0 : $i] : (((((f0 = (^[Y0 : $o]: ($true))) & (sK2 = sF7))) = $true) | ($true = (((sK3 = sF7) & (~ = f0)))) | (((((f0 = (^[Y0 : $o]: ($false))) & (sK0 = sF7)) | ((f0 = (^[Y0 : $o]: (Y0))) & (sK1 = sF7)))) = $true) | (((((f0 = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((f0 = (^[Y0 : $o]: (Y0))) & (sK1 = X0)))) = $false)) )),
% 4.04/0.97 inference(or_proxy_clausification,[],[f562])).
% 4.04/0.97 thf(f565,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((((((f0 = (^[Y0 : $o]: ($false))) & (sK0 = sF7)) | ((f0 = (^[Y0 : $o]: (Y0))) & (sK1 = sF7)))) = $true) | (((f0 = (^[Y0 : $o]: ($true)))) = $true) | (((((f0 = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((f0 = (^[Y0 : $o]: (Y0))) & (sK1 = X0)))) = $false) | ($true = (((sK3 = sF7) & (~ = f0))))) )),
% 4.04/0.97 inference(and_proxy_clausification,[],[f563])).
% 4.04/0.97 thf(f566,plain,(
% 4.04/0.97 ( ! [X0 : $i] : (((((f0 = (^[Y0 : $o]: (Y0))) & (sK1 = sF7))) = $true) | ($true = (((sK3 = sF7) & (~ = f0)))) | (((f0 = (^[Y0 : $o]: ($true)))) = $true) | ($true = (((f0 = (^[Y0 : $o]: ($false))) & (sK0 = sF7)))) | (((((f0 = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((f0 = (^[Y0 : $o]: (Y0))) & (sK1 = X0)))) = $false)) )),
% 4.04/0.97 inference(or_proxy_clausification,[],[f565])).
% 4.04/0.97 thf(f568,plain,(
% 4.04/0.97 ( ! [X0 : $i] : (($true = (((f0 = (^[Y0 : $o]: ($false))) & (sK0 = sF7)))) | (((f0 = (^[Y0 : $o]: ($true)))) = $true) | ($true = (((sK3 = sF7) & (~ = f0)))) | (((f0 = (^[Y0 : $o]: (Y0)))) = $true) | (((((f0 = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((f0 = (^[Y0 : $o]: (Y0))) & (sK1 = X0)))) = $false)) )),
% 4.04/0.97 inference(and_proxy_clausification,[],[f566])).
% 4.04/0.97 thf(f569,plain,(
% 4.04/0.97 ( ! [X0 : $i] : (($true = ((sK0 = sF7))) | ($true = (((sK3 = sF7) & (~ = f0)))) | (((f0 = (^[Y0 : $o]: (Y0)))) = $true) | (((((f0 = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((f0 = (^[Y0 : $o]: (Y0))) & (sK1 = X0)))) = $false) | (((f0 = (^[Y0 : $o]: ($true)))) = $true)) )),
% 4.04/0.97 inference(and_proxy_clausification,[],[f568])).
% 4.04/0.97 thf(f597,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((sK0 = sF7) | (((f0 = (^[Y0 : $o]: ($true)))) = $true) | (((((f0 = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((f0 = (^[Y0 : $o]: (Y0))) & (sK1 = X0)))) = $false) | ($true = (((sK3 = sF7) & (~ = f0)))) | (((f0 = (^[Y0 : $o]: (Y0)))) = $true)) )),
% 4.04/0.97 inference(equality_proxy_clausification,[],[f569])).
% 4.04/0.97 thf(f598,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((((((f0 = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((f0 = (^[Y0 : $o]: (Y0))) & (sK1 = X0)))) = $false) | ($true = (((sK3 = sF7) & (~ = f0)))) | (sK0 = sF7) | (((f0 = (^[Y0 : $o]: (Y0)))) = $true) | (f0 = (^[Y0 : $o]: ($true)))) )),
% 4.04/0.97 inference(equality_proxy_clausification,[],[f597])).
% 4.04/0.97 thf(f600,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((((f0 = (^[Y0 : $o]: (Y0)))) = $true) | ($true = (((sK3 = sF7) & (~ = f0)))) | ($false = (((f0 = (^[Y0 : $o]: ($false))) & (sK0 = X0)))) | (sK0 = sF7) | (f0 = (^[Y0 : $o]: ($true)))) )),
% 4.04/0.97 inference(or_proxy_clausification,[],[f598])).
% 4.04/0.97 thf(f601,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((f0 = (^[Y0 : $o]: (Y0))) | (sK0 = sF7) | (f0 = (^[Y0 : $o]: ($true))) | ($true = (((sK3 = sF7) & (~ = f0)))) | ($false = (((f0 = (^[Y0 : $o]: ($false))) & (sK0 = X0))))) )),
% 4.04/0.97 inference(equality_proxy_clausification,[],[f600])).
% 4.04/0.97 thf(f602,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((f0 = (^[Y0 : $o]: ($true))) | (f0 = (^[Y0 : $o]: (Y0))) | ($false = (((f0 = (^[Y0 : $o]: ($false))) & (sK0 = X0)))) | ($true = ((~ = f0))) | (sK0 = sF7)) )),
% 4.04/0.97 inference(and_proxy_clausification,[],[f601])).
% 4.04/0.97 thf(f608,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((sK0 = sF7) | ($false = ((sK0 = X0))) | (f0 = (^[Y0 : $o]: ($true))) | ($false = ((f0 = (^[Y0 : $o]: ($false))))) | ($true = ((~ = f0))) | (f0 = (^[Y0 : $o]: (Y0)))) )),
% 4.04/0.97 inference(and_proxy_clausification,[],[f602])).
% 4.04/0.97 thf(f609,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((sK0 != X0) | ($false = ((f0 = (^[Y0 : $o]: ($false))))) | (f0 = (^[Y0 : $o]: (Y0))) | (sK0 = sF7) | (f0 = (^[Y0 : $o]: ($true))) | ($true = ((~ = f0)))) )),
% 4.04/0.97 inference(equality_proxy_clausification,[],[f608])).
% 4.04/0.97 thf(f610,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((f0 = (^[Y0 : $o]: ($true))) | (f0 != (^[Y0 : $o]: ($false))) | (sK0 = sF7) | (f0 = (^[Y0 : $o]: (Y0))) | (sK0 != X0) | ($true = ((~ = f0)))) )),
% 4.04/0.97 inference(equality_proxy_clausification,[],[f609])).
% 4.04/0.97 thf(f611,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((f0 = (^[Y0 : $o]: ($true))) | (~ = f0) | (sK0 != X0) | (f0 = (^[Y0 : $o]: (Y0))) | (f0 != (^[Y0 : $o]: ($false))) | (sK0 = sF7)) )),
% 4.04/0.97 inference(equality_proxy_clausification,[],[f610])).
% 4.04/0.97 thf(f961,definition,(
% 4.04/0.97 spl8_18 <=> (f0 = (^[Y0 : $o]: ($false)))),
% 4.04/0.97 introduced(definition,[new_symbols(definition,[spl8_18])],[avatar_definition])).
% 4.04/0.97 thf(f962,plain,(
% 4.04/0.97 (f0 != (^[Y0 : $o]: ($false))) | spl8_18),
% 4.04/0.97 inference(avatar_component_clause,[],[f961])).
% 4.04/0.97 thf(f963,plain,(
% 4.04/0.97 (f0 = (^[Y0 : $o]: ($false))) | ~spl8_18),
% 4.04/0.97 inference(avatar_component_clause,[],[f961])).
% 4.04/0.97 thf(f973,definition,(
% 4.04/0.97 spl8_21 <=> (f0 = (^[Y0 : $o]: (Y0)))),
% 4.04/0.97 introduced(definition,[new_symbols(definition,[spl8_21])],[avatar_definition])).
% 4.04/0.97 thf(f974,plain,(
% 4.04/0.97 (f0 = (^[Y0 : $o]: (Y0))) | ~spl8_21),
% 4.04/0.97 inference(avatar_component_clause,[],[f973])).
% 4.04/0.97 thf(f975,plain,(
% 4.04/0.97 (f0 != (^[Y0 : $o]: (Y0))) | spl8_21),
% 4.04/0.97 inference(avatar_component_clause,[],[f973])).
% 4.04/0.97 thf(f1133,plain,(
% 4.04/0.97 (sK3 != sK3) | ~spl8_15),
% 4.04/0.97 inference(imitation,[],[f521])).
% 4.04/0.97 thf(f1136,plain,(
% 4.04/0.97 $false | ~spl8_15),
% 4.04/0.97 inference(trivial_inequality_removal,[],[f1133])).
% 4.04/0.97 thf(f1137,plain,(
% 4.04/0.97 ~spl8_15),
% 4.04/0.97 inference(avatar_contradiction_clause,[],[f1136])).
% 4.04/0.97 thf(f1140,plain,(
% 4.04/0.97 ( ! [X0 : $i] : (((((^[Y0 : $i]: (((((f1 = (^[Y1 : $o]: ($false))) & (sK0 = Y0)) | ((f1 = (^[Y1 : $o]: (Y1))) & (sK1 = Y0))) | ((f1 = (^[Y1 : $o]: ($true))) & (sK2 = Y0))) | ((sK3 = Y0) & (~ = f1)))) @ X0)) != $true) | ($true = (((^[Y0 : $i]: (((((f1 = (^[Y1 : $o]: ($false))) & (sK0 = Y0)) | ((f1 = (^[Y1 : $o]: (Y1))) & (sK1 = Y0))) | ((f1 = (^[Y1 : $o]: ($true))) & (sK2 = Y0))) | ((sK3 = Y0) & (~ = f1)))) @ sF5)))) )),
% 4.04/0.97 inference(constrained_superposition,[],[f43,f62])).
% 4.04/0.97 thf(f1141,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((((((((f1 = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((f1 = (^[Y0 : $o]: (Y0))) & (sK1 = X0))) | ((f1 = (^[Y0 : $o]: ($true))) & (sK2 = X0))) | ((sK3 = X0) & (~ = f1)))) != $true) | ($true = ((((((f1 = (^[Y0 : $o]: ($false))) & (sK0 = sF5)) | ((f1 = (^[Y0 : $o]: (Y0))) & (sK1 = sF5))) | ((f1 = (^[Y0 : $o]: ($true))) & (sK2 = sF5))) | ((sK3 = sF5) & (~ = f1)))))) )),
% 4.04/0.97 inference(beta-eta_normalization,[],[f1140])).
% 4.04/0.97 thf(f1142,plain,(
% 4.04/0.97 ( ! [X0 : $i] : (($true = ((((((f1 = (^[Y0 : $o]: ($false))) & (sK0 = sF5)) | ((f1 = (^[Y0 : $o]: (Y0))) & (sK1 = sF5))) | ((f1 = (^[Y0 : $o]: ($true))) & (sK2 = sF5))) | ((sK3 = sF5) & (~ = f1))))) | ($false = (((sK3 = X0) & (~ = f1))))) )),
% 4.04/0.97 inference(or_proxy_clausification,[],[f1141])).
% 4.04/0.97 thf(f1388,plain,(
% 4.04/0.97 ( ! [X0 : $i] : (($true = (((sK3 = sF5) & (~ = f1)))) | ((((((f1 = (^[Y0 : $o]: ($false))) & (sK0 = sF5)) | ((f1 = (^[Y0 : $o]: (Y0))) & (sK1 = sF5))) | ((f1 = (^[Y0 : $o]: ($true))) & (sK2 = sF5)))) = $true) | ($false = (((sK3 = X0) & (~ = f1))))) )),
% 4.04/0.97 inference(or_proxy_clausification,[],[f1142])).
% 4.04/0.97 thf(f1390,plain,(
% 4.04/0.97 ( ! [X0 : $i] : (($true = ((sK3 = sF5))) | ($false = (((sK3 = X0) & (~ = f1)))) | ((((((f1 = (^[Y0 : $o]: ($false))) & (sK0 = sF5)) | ((f1 = (^[Y0 : $o]: (Y0))) & (sK1 = sF5))) | ((f1 = (^[Y0 : $o]: ($true))) & (sK2 = sF5)))) = $true)) )),
% 4.04/0.97 inference(and_proxy_clausification,[],[f1388])).
% 4.04/0.97 thf(f1391,plain,(
% 4.04/0.97 ( ! [X0 : $i] : (((((((f1 = (^[Y0 : $o]: ($false))) & (sK0 = sF5)) | ((f1 = (^[Y0 : $o]: (Y0))) & (sK1 = sF5))) | ((f1 = (^[Y0 : $o]: ($true))) & (sK2 = sF5)))) = $true) | (sK3 = sF5) | ($false = (((sK3 = X0) & (~ = f1))))) )),
% 4.04/0.97 inference(equality_proxy_clausification,[],[f1390])).
% 4.04/0.97 thf(f1392,plain,(
% 4.04/0.97 ( ! [X0 : $i] : (($true = ((((f1 = (^[Y0 : $o]: ($false))) & (sK0 = sF5)) | ((f1 = (^[Y0 : $o]: (Y0))) & (sK1 = sF5))))) | ($true = (((f1 = (^[Y0 : $o]: ($true))) & (sK2 = sF5)))) | (sK3 = sF5) | ($false = (((sK3 = X0) & (~ = f1))))) )),
% 4.04/0.97 inference(or_proxy_clausification,[],[f1391])).
% 4.04/0.97 thf(f1393,plain,(
% 4.04/0.97 ( ! [X0 : $i] : (($true = (((f1 = (^[Y0 : $o]: (Y0))) & (sK1 = sF5)))) | ($true = (((f1 = (^[Y0 : $o]: ($true))) & (sK2 = sF5)))) | ($true = (((f1 = (^[Y0 : $o]: ($false))) & (sK0 = sF5)))) | (sK3 = sF5) | ($false = (((sK3 = X0) & (~ = f1))))) )),
% 4.04/0.97 inference(or_proxy_clausification,[],[f1392])).
% 4.04/0.97 thf(f1395,plain,(
% 4.04/0.97 ( ! [X0 : $i] : (($true = (((f1 = (^[Y0 : $o]: ($false))) & (sK0 = sF5)))) | (sK3 = sF5) | ($true = (((f1 = (^[Y0 : $o]: ($true))) & (sK2 = sF5)))) | ($false = (((sK3 = X0) & (~ = f1)))) | ($true = ((f1 = (^[Y0 : $o]: (Y0)))))) )),
% 4.04/0.97 inference(and_proxy_clausification,[],[f1393])).
% 4.04/0.97 thf(f1397,plain,(
% 4.04/0.97 ( ! [X0 : $i] : (($true = ((f1 = (^[Y0 : $o]: ($false))))) | ($true = (((f1 = (^[Y0 : $o]: ($true))) & (sK2 = sF5)))) | ($false = (((sK3 = X0) & (~ = f1)))) | (sK3 = sF5) | ($true = ((f1 = (^[Y0 : $o]: (Y0)))))) )),
% 4.04/0.97 inference(and_proxy_clausification,[],[f1395])).
% 4.04/0.97 thf(f1398,plain,(
% 4.04/0.97 ( ! [X0 : $i] : (($true = (((f1 = (^[Y0 : $o]: ($true))) & (sK2 = sF5)))) | (sK3 = sF5) | ($true = ((f1 = (^[Y0 : $o]: (Y0))))) | ($false = (((sK3 = X0) & (~ = f1)))) | (f1 = (^[Y0 : $o]: ($false)))) )),
% 4.04/0.97 inference(equality_proxy_clausification,[],[f1397])).
% 4.04/0.97 thf(f1400,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((f1 = (^[Y0 : $o]: ($false))) | (sK3 = sF5) | ($true = ((f1 = (^[Y0 : $o]: (Y0))))) | ($true = ((f1 = (^[Y0 : $o]: ($true))))) | ($false = (((sK3 = X0) & (~ = f1))))) )),
% 4.04/0.97 inference(and_proxy_clausification,[],[f1398])).
% 4.04/0.97 thf(f1401,plain,(
% 4.04/0.97 ( ! [X0 : $i] : (($false = (((sK3 = X0) & (~ = f1)))) | ($true = ((f1 = (^[Y0 : $o]: ($true))))) | (sK3 = sF5) | (f1 = (^[Y0 : $o]: ($false))) | (f1 = (^[Y0 : $o]: (Y0)))) )),
% 4.04/0.97 inference(equality_proxy_clausification,[],[f1400])).
% 4.04/0.97 thf(f1402,plain,(
% 4.04/0.97 ( ! [X0 : $i] : (($false = ((sK3 = X0))) | ($false = ((~ = f1))) | (f1 = (^[Y0 : $o]: (Y0))) | ($true = ((f1 = (^[Y0 : $o]: ($true))))) | (f1 = (^[Y0 : $o]: ($false))) | (sK3 = sF5)) )),
% 4.04/0.97 inference(and_proxy_clausification,[],[f1401])).
% 4.04/0.97 thf(f1403,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((f1 = (^[Y0 : $o]: ($false))) | ($true = ((f1 = (^[Y0 : $o]: ($true))))) | (sK3 = sF5) | ($false = ((~ = f1))) | (sK3 != X0) | (f1 = (^[Y0 : $o]: (Y0)))) )),
% 4.04/0.97 inference(equality_proxy_clausification,[],[f1402])).
% 4.04/0.97 thf(f1404,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((sK3 = sF5) | (f1 = (^[Y0 : $o]: (Y0))) | (sK3 != X0) | (f1 = (^[Y0 : $o]: ($false))) | ($false = ((~ = f1))) | (f1 = (^[Y0 : $o]: ($true)))) )),
% 4.04/0.97 inference(equality_proxy_clausification,[],[f1403])).
% 4.04/0.97 thf(f1405,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((f1 = (^[Y0 : $o]: ($true))) | (sK3 != X0) | (sK3 = sF5) | (~ != f1) | (f1 = (^[Y0 : $o]: ($false))) | (f1 = (^[Y0 : $o]: (Y0)))) )),
% 4.04/0.97 inference(equality_proxy_clausification,[],[f1404])).
% 4.04/0.97 thf(f1496,definition,(
% 4.04/0.97 spl8_33 <=> (f1 = (^[Y0 : $o]: (Y0)))),
% 4.04/0.97 introduced(definition,[new_symbols(definition,[spl8_33])],[avatar_definition])).
% 4.04/0.97 thf(f1498,plain,(
% 4.04/0.97 (f1 = (^[Y0 : $o]: (Y0))) | ~spl8_33),
% 4.04/0.97 inference(avatar_component_clause,[],[f1496])).
% 4.04/0.97 thf(f1500,definition,(
% 4.04/0.97 spl8_34 <=> (f1 = (^[Y0 : $o]: ($false)))),
% 4.04/0.97 introduced(definition,[new_symbols(definition,[spl8_34])],[avatar_definition])).
% 4.04/0.97 thf(f1501,plain,(
% 4.04/0.97 (f1 = (^[Y0 : $o]: ($false))) | ~spl8_34),
% 4.04/0.97 inference(avatar_component_clause,[],[f1500])).
% 4.04/0.97 thf(f1508,definition,(
% 4.04/0.97 spl8_36 <=> (f1 = (^[Y0 : $o]: ($true)))),
% 4.04/0.97 introduced(definition,[new_symbols(definition,[spl8_36])],[avatar_definition])).
% 4.04/0.97 thf(f1510,plain,(
% 4.04/0.97 (f1 = (^[Y0 : $o]: ($true))) | ~spl8_36),
% 4.04/0.97 inference(avatar_component_clause,[],[f1508])).
% 4.04/0.97 thf(f1524,definition,(
% 4.04/0.97 spl8_39 <=> (~ = f1)),
% 4.04/0.97 introduced(definition,[new_symbols(definition,[spl8_39])],[avatar_definition])).
% 4.04/0.97 thf(f1525,plain,(
% 4.04/0.97 (~ != f1) | spl8_39),
% 4.04/0.97 inference(avatar_component_clause,[],[f1524])).
% 4.04/0.97 thf(f1526,plain,(
% 4.04/0.97 (~ = f1) | ~spl8_39),
% 4.04/0.97 inference(avatar_component_clause,[],[f1524])).
% 4.04/0.97 thf(f1547,plain,(
% 4.04/0.97 ~spl8_39 | spl8_4 | spl8_33 | spl8_15 | spl8_36 | spl8_34),
% 4.04/0.97 inference(avatar_split_clause,[],[f1405,f1500,f1508,f520,f1496,f77,f1524])).
% 4.04/0.97 thf(f1567,plain,(
% 4.04/0.97 ( ! [X0 : $i] : (($true != (((^[Y0 : $i]: (((((f2 = (^[Y1 : $o]: ($false))) & (sK0 = Y0)) | ((f2 = (^[Y1 : $o]: (Y1))) & (sK1 = Y0))) | ((f2 = (^[Y1 : $o]: ($true))) & (sK2 = Y0))) | ((sK3 = Y0) & (~ = f2)))) @ X0))) | ((((^[Y0 : $i]: (((((f2 = (^[Y1 : $o]: ($false))) & (sK0 = Y0)) | ((f2 = (^[Y1 : $o]: (Y1))) & (sK1 = Y0))) | ((f2 = (^[Y1 : $o]: ($true))) & (sK2 = Y0))) | ((sK3 = Y0) & (~ = f2)))) @ sF6)) = $true)) )),
% 4.04/0.97 inference(constrained_superposition,[],[f43,f63])).
% 4.04/0.97 thf(f1568,plain,(
% 4.04/0.97 ( ! [X0 : $i] : (($true = ((((((f2 = (^[Y0 : $o]: ($false))) & (sK0 = sF6)) | ((f2 = (^[Y0 : $o]: (Y0))) & (sK1 = sF6))) | ((f2 = (^[Y0 : $o]: ($true))) & (sK2 = sF6))) | ((sK3 = sF6) & (~ = f2))))) | ($true != ((((((f2 = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((f2 = (^[Y0 : $o]: (Y0))) & (sK1 = X0))) | ((f2 = (^[Y0 : $o]: ($true))) & (sK2 = X0))) | ((sK3 = X0) & (~ = f2)))))) )),
% 4.04/0.97 inference(beta-eta_normalization,[],[f1567])).
% 4.04/0.97 thf(f1569,plain,(
% 4.04/0.97 ( ! [X0 : $i] : (((((sK3 = sF6) & (~ = f2))) = $true) | ((((((f2 = (^[Y0 : $o]: ($false))) & (sK0 = sF6)) | ((f2 = (^[Y0 : $o]: (Y0))) & (sK1 = sF6))) | ((f2 = (^[Y0 : $o]: ($true))) & (sK2 = sF6)))) = $true) | ($true != ((((((f2 = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((f2 = (^[Y0 : $o]: (Y0))) & (sK1 = X0))) | ((f2 = (^[Y0 : $o]: ($true))) & (sK2 = X0))) | ((sK3 = X0) & (~ = f2)))))) )),
% 4.04/0.97 inference(or_proxy_clausification,[],[f1568])).
% 4.04/0.97 thf(f1570,plain,(
% 4.04/0.97 ( ! [X0 : $i] : (($true != ((((((f2 = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((f2 = (^[Y0 : $o]: (Y0))) & (sK1 = X0))) | ((f2 = (^[Y0 : $o]: ($true))) & (sK2 = X0))) | ((sK3 = X0) & (~ = f2))))) | ((((((f2 = (^[Y0 : $o]: ($false))) & (sK0 = sF6)) | ((f2 = (^[Y0 : $o]: (Y0))) & (sK1 = sF6))) | ((f2 = (^[Y0 : $o]: ($true))) & (sK2 = sF6)))) = $true) | ($true = ((~ = f2)))) )),
% 4.04/0.97 inference(and_proxy_clausification,[],[f1569])).
% 4.04/0.97 thf(f1767,plain,(
% 4.04/0.97 ( ! [X0 : $i] : (((((((f2 = (^[Y0 : $o]: ($false))) & (sK0 = sF6)) | ((f2 = (^[Y0 : $o]: (Y0))) & (sK1 = sF6))) | ((f2 = (^[Y0 : $o]: ($true))) & (sK2 = sF6)))) = $true) | ($true = ((~ = f2))) | ($false = (((((f2 = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((f2 = (^[Y0 : $o]: (Y0))) & (sK1 = X0))) | ((f2 = (^[Y0 : $o]: ($true))) & (sK2 = X0)))))) )),
% 4.04/0.97 inference(or_proxy_clausification,[],[f1570])).
% 4.04/0.97 thf(f1768,plain,(
% 4.04/0.97 ( ! [X0 : $i] : (($true = (((f2 = (^[Y0 : $o]: ($true))) & (sK2 = sF6)))) | ($true = ((((f2 = (^[Y0 : $o]: ($false))) & (sK0 = sF6)) | ((f2 = (^[Y0 : $o]: (Y0))) & (sK1 = sF6))))) | ($false = (((((f2 = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((f2 = (^[Y0 : $o]: (Y0))) & (sK1 = X0))) | ((f2 = (^[Y0 : $o]: ($true))) & (sK2 = X0))))) | ($true = ((~ = f2)))) )),
% 4.04/0.97 inference(or_proxy_clausification,[],[f1767])).
% 4.04/0.97 thf(f1770,plain,(
% 4.04/0.97 ( ! [X0 : $i] : (($true = ((f2 = (^[Y0 : $o]: ($true))))) | ($true = ((((f2 = (^[Y0 : $o]: ($false))) & (sK0 = sF6)) | ((f2 = (^[Y0 : $o]: (Y0))) & (sK1 = sF6))))) | ($true = ((~ = f2))) | ($false = (((((f2 = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((f2 = (^[Y0 : $o]: (Y0))) & (sK1 = X0))) | ((f2 = (^[Y0 : $o]: ($true))) & (sK2 = X0)))))) )),
% 4.04/0.97 inference(and_proxy_clausification,[],[f1768])).
% 4.04/0.97 thf(f1771,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((f2 = (^[Y0 : $o]: ($true))) | ($true = ((((f2 = (^[Y0 : $o]: ($false))) & (sK0 = sF6)) | ((f2 = (^[Y0 : $o]: (Y0))) & (sK1 = sF6))))) | ($true = ((~ = f2))) | ($false = (((((f2 = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((f2 = (^[Y0 : $o]: (Y0))) & (sK1 = X0))) | ((f2 = (^[Y0 : $o]: ($true))) & (sK2 = X0)))))) )),
% 4.04/0.97 inference(equality_proxy_clausification,[],[f1770])).
% 4.04/0.97 thf(f1772,plain,(
% 4.04/0.97 ( ! [X0 : $i] : (((((f2 = (^[Y0 : $o]: ($false))) & (sK0 = sF6))) = $true) | ($false = (((((f2 = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((f2 = (^[Y0 : $o]: (Y0))) & (sK1 = X0))) | ((f2 = (^[Y0 : $o]: ($true))) & (sK2 = X0))))) | ($true = ((~ = f2))) | ((((f2 = (^[Y0 : $o]: (Y0))) & (sK1 = sF6))) = $true) | (f2 = (^[Y0 : $o]: ($true)))) )),
% 4.04/0.97 inference(or_proxy_clausification,[],[f1771])).
% 4.04/0.97 thf(f1774,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((f2 = (^[Y0 : $o]: ($true))) | ($true = ((~ = f2))) | ((((f2 = (^[Y0 : $o]: (Y0))) & (sK1 = sF6))) = $true) | ($false = (((((f2 = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((f2 = (^[Y0 : $o]: (Y0))) & (sK1 = X0))) | ((f2 = (^[Y0 : $o]: ($true))) & (sK2 = X0))))) | ($true = ((f2 = (^[Y0 : $o]: ($false)))))) )),
% 4.04/0.97 inference(and_proxy_clausification,[],[f1772])).
% 4.04/0.97 thf(f1775,plain,(
% 4.04/0.97 ( ! [X0 : $i] : (($false = (((((f2 = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((f2 = (^[Y0 : $o]: (Y0))) & (sK1 = X0))) | ((f2 = (^[Y0 : $o]: ($true))) & (sK2 = X0))))) | (~ = f2) | (f2 = (^[Y0 : $o]: ($true))) | ((((f2 = (^[Y0 : $o]: (Y0))) & (sK1 = sF6))) = $true) | ($true = ((f2 = (^[Y0 : $o]: ($false)))))) )),
% 4.04/0.97 inference(equality_proxy_clausification,[],[f1774])).
% 4.04/0.97 thf(f1777,plain,(
% 4.04/0.97 ( ! [X0 : $i] : (($true = ((f2 = (^[Y0 : $o]: ($false))))) | (~ = f2) | ($false = ((((f2 = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((f2 = (^[Y0 : $o]: (Y0))) & (sK1 = X0))))) | (f2 = (^[Y0 : $o]: ($true))) | ((((f2 = (^[Y0 : $o]: (Y0))) & (sK1 = sF6))) = $true)) )),
% 4.04/0.97 inference(or_proxy_clausification,[],[f1775])).
% 4.04/0.97 thf(f1778,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((f2 = (^[Y0 : $o]: ($true))) | ((((f2 = (^[Y0 : $o]: (Y0))) & (sK1 = sF6))) = $true) | ($false = ((((f2 = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((f2 = (^[Y0 : $o]: (Y0))) & (sK1 = X0))))) | (f2 = (^[Y0 : $o]: ($false))) | (~ = f2)) )),
% 4.04/0.97 inference(equality_proxy_clausification,[],[f1777])).
% 4.04/0.97 thf(f1779,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((~ = f2) | (f2 = (^[Y0 : $o]: ($false))) | (f2 = (^[Y0 : $o]: ($true))) | ($false = ((((f2 = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((f2 = (^[Y0 : $o]: (Y0))) & (sK1 = X0))))) | (((sK1 = sF6)) = $true)) )),
% 4.04/0.97 inference(and_proxy_clausification,[],[f1778])).
% 4.04/0.97 thf(f1791,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((((sK1 = sF6)) = $true) | (~ = f2) | (f2 = (^[Y0 : $o]: ($false))) | ($false = (((f2 = (^[Y0 : $o]: (Y0))) & (sK1 = X0)))) | (f2 = (^[Y0 : $o]: ($true)))) )),
% 4.04/0.97 inference(or_proxy_clausification,[],[f1779])).
% 4.04/0.97 thf(f1797,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((sF6 = sK1) | (f2 = (^[Y0 : $o]: ($true))) | ($false = (((f2 = (^[Y0 : $o]: (Y0))) & (sK1 = X0)))) | (f2 = (^[Y0 : $o]: ($false))) | (~ = f2)) )),
% 4.04/0.97 inference(equality_proxy_clausification,[],[f1791])).
% 4.04/0.97 thf(f1798,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((sF6 = sK1) | ($false = ((f2 = (^[Y0 : $o]: (Y0))))) | ($false = ((sK1 = X0))) | (~ = f2) | (f2 = (^[Y0 : $o]: ($false))) | (f2 = (^[Y0 : $o]: ($true)))) )),
% 4.04/0.97 inference(and_proxy_clausification,[],[f1797])).
% 4.04/0.97 thf(f1799,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((f2 = (^[Y0 : $o]: ($false))) | (f2 = (^[Y0 : $o]: ($true))) | (sF6 = sK1) | (f2 != (^[Y0 : $o]: (Y0))) | ($false = ((sK1 = X0))) | (~ = f2)) )),
% 4.04/0.97 inference(equality_proxy_clausification,[],[f1798])).
% 4.04/0.97 thf(f1800,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((f2 = (^[Y0 : $o]: ($true))) | (sF6 = sK1) | (f2 != (^[Y0 : $o]: (Y0))) | (f2 = (^[Y0 : $o]: ($false))) | (sK1 != X0) | (~ = f2)) )),
% 4.04/0.97 inference(equality_proxy_clausification,[],[f1799])).
% 4.04/0.97 thf(f1997,definition,(
% 4.04/0.97 spl8_41 <=> (f2 = (^[Y0 : $o]: ($true)))),
% 4.04/0.97 introduced(definition,[new_symbols(definition,[spl8_41])],[avatar_definition])).
% 4.04/0.97 thf(f1998,plain,(
% 4.04/0.97 (f2 != (^[Y0 : $o]: ($true))) | spl8_41),
% 4.04/0.97 inference(avatar_component_clause,[],[f1997])).
% 4.04/0.97 thf(f1999,plain,(
% 4.04/0.97 (f2 = (^[Y0 : $o]: ($true))) | ~spl8_41),
% 4.04/0.97 inference(avatar_component_clause,[],[f1997])).
% 4.04/0.97 thf(f2005,definition,(
% 4.04/0.97 spl8_43 <=> (f2 = (^[Y0 : $o]: (Y0)))),
% 4.04/0.97 introduced(definition,[new_symbols(definition,[spl8_43])],[avatar_definition])).
% 4.04/0.97 thf(f2006,plain,(
% 4.04/0.97 (f2 != (^[Y0 : $o]: (Y0))) | spl8_43),
% 4.04/0.97 inference(avatar_component_clause,[],[f2005])).
% 4.04/0.97 thf(f2007,plain,(
% 4.04/0.97 (f2 = (^[Y0 : $o]: (Y0))) | ~spl8_43),
% 4.04/0.97 inference(avatar_component_clause,[],[f2005])).
% 4.04/0.97 thf(f2038,definition,(
% 4.04/0.97 spl8_46 <=> (f2 = f3)),
% 4.04/0.97 introduced(definition,[new_symbols(definition,[spl8_46])],[avatar_definition])).
% 4.04/0.97 thf(f2040,plain,(
% 4.04/0.97 (f2 = f3) | ~spl8_46),
% 4.04/0.97 inference(avatar_component_clause,[],[f2038])).
% 4.04/0.97 thf(f2178,plain,(
% 4.04/0.97 ( ! [X1 : $o] : ((((~ X1)) = ((f3 @ X1)))) ) | ~spl8_14),
% 4.04/0.97 inference(argument_congruence,[],[f517])).
% 4.04/0.97 thf(f2179,plain,(
% 4.04/0.97 ( ! [X1 : $o] : (($false = ((f3 @ X1))) | (((~ X1)) = $true)) ) | ~spl8_14),
% 4.04/0.97 inference(iff_proxy_clausification,[],[f2178])).
% 4.04/0.97 thf(f2182,plain,(
% 4.04/0.97 ( ! [X1 : $o] : (($false = ((f3 @ X1))) | ($false = X1)) ) | ~spl8_14),
% 4.04/0.97 inference(not_proxy_clausification,[],[f2179])).
% 4.04/0.97 thf(f2215,plain,(
% 4.04/0.97 ( ! [X1 : $o] : ((((f2 @ X1)) = ((f3 @ X1)))) ) | ~spl8_46),
% 4.04/0.97 inference(argument_congruence,[],[f2040])).
% 4.04/0.97 thf(f2216,plain,(
% 4.04/0.97 ( ! [X1 : $o] : (($true = ((f2 @ X1))) | ($false = ((f3 @ X1)))) ) | ~spl8_46),
% 4.04/0.97 inference(iff_proxy_clausification,[],[f2215])).
% 4.04/0.97 thf(f2405,plain,(
% 4.04/0.97 ( ! [X1 : $o] : (((((^[Y0 : $o]: ($true)) @ X1)) = ((f2 @ X1)))) ) | ~spl8_41),
% 4.04/0.97 inference(argument_congruence,[],[f1999])).
% 4.04/0.97 thf(f2407,plain,(
% 4.04/0.97 ( ! [X1 : $o] : (($false = (((^[Y0 : $o]: ($true)) @ X1))) | ($true = ((f2 @ X1)))) ) | ~spl8_41),
% 4.04/0.97 inference(iff_proxy_clausification,[],[f2405])).
% 4.04/0.97 thf(f2408,plain,(
% 4.04/0.97 ( ! [X1 : $o] : (($true = ((f2 @ X1))) | ($false = $true)) ) | ~spl8_41),
% 4.04/0.97 inference(beta-eta_normalization,[],[f2407])).
% 4.04/0.97 thf(f2409,plain,(
% 4.04/0.97 ( ! [X1 : $o] : (($true = ((f2 @ X1)))) ) | ~spl8_41),
% 4.04/0.97 inference(trivial_inequality_removal,[],[f2408])).
% 4.04/0.97 thf(f2411,plain,(
% 4.04/0.97 ($false = $true) | ~spl8_41),
% 4.04/0.97 inference(constrained_superposition,[],[f2409,f48])).
% 4.04/0.97 thf(f2415,plain,(
% 4.04/0.97 $false | ~spl8_41),
% 4.04/0.97 inference(trivial_inequality_removal,[],[f2411])).
% 4.04/0.97 thf(f2416,plain,(
% 4.04/0.97 ~spl8_41),
% 4.04/0.97 inference(avatar_contradiction_clause,[],[f2415])).
% 4.04/0.97 thf(f2551,plain,(
% 4.04/0.97 ((((^[Y0 : $o]: (Y0)) @ sK21)) != ((f2 @ sK21))) | spl8_43),
% 4.04/0.97 inference(negative_extensionality,[],[f2006])).
% 4.04/0.97 thf(f2552,plain,(
% 4.04/0.97 ($true = ((f2 @ sK21))) | ((((^[Y0 : $o]: (Y0)) @ sK21)) = $true) | spl8_43),
% 4.04/0.97 inference(xor_proxy_clausification,[],[f2551])).
% 4.04/0.97 thf(f2553,plain,(
% 4.04/0.97 ($false = ((f2 @ sK21))) | ($false = (((^[Y0 : $o]: (Y0)) @ sK21))) | spl8_43),
% 4.04/0.97 inference(xor_proxy_clausification,[],[f2551])).
% 4.04/0.97 thf(f2554,plain,(
% 4.04/0.97 ($false = sK21) | ($false = ((f2 @ sK21))) | spl8_43),
% 4.04/0.97 inference(beta-eta_normalization,[],[f2553])).
% 4.04/0.97 thf(f2555,plain,(
% 4.04/0.97 ($true = ((f2 @ sK21))) | (sK21 = $true) | spl8_43),
% 4.04/0.97 inference(beta-eta_normalization,[],[f2552])).
% 4.04/0.97 thf(f2557,definition,(
% 4.04/0.97 spl8_68 <=> ($false = ((f2 @ sK21)))),
% 4.04/0.97 introduced(definition,[new_symbols(definition,[spl8_68])],[avatar_definition])).
% 4.04/0.97 thf(f2559,plain,(
% 4.04/0.97 ($false = ((f2 @ sK21))) | ~spl8_68),
% 4.04/0.97 inference(avatar_component_clause,[],[f2557])).
% 4.04/0.97 thf(f2561,definition,(
% 4.04/0.97 spl8_69 <=> ($false = sK21)),
% 4.04/0.97 introduced(definition,[new_symbols(definition,[spl8_69])],[avatar_definition])).
% 4.04/0.97 thf(f2562,plain,(
% 4.04/0.97 ($false != sK21) | spl8_69),
% 4.04/0.97 inference(avatar_component_clause,[],[f2561])).
% 4.04/0.97 thf(f2563,plain,(
% 4.04/0.97 ($false = sK21) | ~spl8_69),
% 4.04/0.97 inference(avatar_component_clause,[],[f2561])).
% 4.04/0.97 thf(f2564,plain,(
% 4.04/0.97 spl8_68 | spl8_69 | spl8_43),
% 4.04/0.97 inference(avatar_split_clause,[],[f2554,f2005,f2561,f2557])).
% 4.04/0.97 thf(f2566,definition,(
% 4.04/0.97 spl8_70 <=> ($true = ((f2 @ sK21)))),
% 4.04/0.97 introduced(definition,[new_symbols(definition,[spl8_70])],[avatar_definition])).
% 4.04/0.97 thf(f2568,plain,(
% 4.04/0.97 ($true = ((f2 @ sK21))) | ~spl8_70),
% 4.04/0.97 inference(avatar_component_clause,[],[f2566])).
% 4.04/0.97 thf(f2570,definition,(
% 4.04/0.97 spl8_71 <=> (sK21 = $true)),
% 4.04/0.97 introduced(definition,[new_symbols(definition,[spl8_71])],[avatar_definition])).
% 4.04/0.97 thf(f2571,plain,(
% 4.04/0.97 (sK21 != $true) | spl8_71),
% 4.04/0.97 inference(avatar_component_clause,[],[f2570])).
% 4.04/0.97 thf(f2572,plain,(
% 4.04/0.97 (sK21 = $true) | ~spl8_71),
% 4.04/0.97 inference(avatar_component_clause,[],[f2570])).
% 4.04/0.97 thf(f2573,plain,(
% 4.04/0.97 spl8_70 | spl8_71 | spl8_43),
% 4.04/0.97 inference(avatar_split_clause,[],[f2555,f2005,f2570,f2566])).
% 4.04/0.97 thf(f2576,plain,(
% 4.04/0.97 ($false = $true) | (~spl8_69 | ~spl8_71)),
% 4.04/0.97 inference(forward_demodulation,[],[f2572,f2563])).
% 4.04/0.97 thf(f2577,plain,(
% 4.04/0.97 $false | (~spl8_69 | ~spl8_71)),
% 4.04/0.97 inference(trivial_inequality_removal,[],[f2576])).
% 4.04/0.97 thf(f2578,plain,(
% 4.04/0.97 ~spl8_69 | ~spl8_71),
% 4.04/0.97 inference(avatar_contradiction_clause,[],[f2577])).
% 4.04/0.97 thf(f2579,plain,(
% 4.04/0.97 (((f2 @ $false)) = $true) | (~spl8_69 | ~spl8_70)),
% 4.04/0.97 inference(forward_demodulation,[],[f2568,f2563])).
% 4.04/0.97 thf(f2581,plain,(
% 4.04/0.97 ($false = $true) | (~spl8_69 | ~spl8_70)),
% 4.04/0.97 inference(forward_demodulation,[],[f2579,f48])).
% 4.04/0.97 thf(f2582,plain,(
% 4.04/0.97 $false | (~spl8_69 | ~spl8_70)),
% 4.04/0.97 inference(trivial_inequality_removal,[],[f2581])).
% 4.04/0.97 thf(f2583,plain,(
% 4.04/0.97 ~spl8_69 | ~spl8_70),
% 4.04/0.97 inference(avatar_contradiction_clause,[],[f2582])).
% 4.04/0.97 thf(f2589,plain,(
% 4.04/0.97 (((f2 @ $true)) = $false) | (~spl8_68 | ~spl8_71)),
% 4.04/0.97 inference(forward_demodulation,[],[f2559,f2572])).
% 4.04/0.97 thf(f2590,plain,(
% 4.04/0.97 ($false = $true) | (~spl8_68 | ~spl8_71)),
% 4.04/0.97 inference(forward_demodulation,[],[f2589,f40])).
% 4.04/0.97 thf(f2591,plain,(
% 4.04/0.97 $false | (~spl8_68 | ~spl8_71)),
% 4.04/0.97 inference(trivial_inequality_removal,[],[f2590])).
% 4.04/0.97 thf(f2592,plain,(
% 4.04/0.97 ~spl8_68 | ~spl8_71),
% 4.04/0.97 inference(avatar_contradiction_clause,[],[f2591])).
% 4.04/0.97 thf(f2593,plain,(
% 4.04/0.97 ($true != $true) | ($false = sK21) | spl8_71),
% 4.04/0.97 inference(constrained_superposition,[],[f2571,f50])).
% 4.04/0.97 thf(f2594,plain,(
% 4.04/0.97 ($false = sK21) | spl8_71),
% 4.04/0.97 inference(trivial_inequality_removal,[],[f2593])).
% 4.04/0.97 thf(f2595,plain,(
% 4.04/0.97 $false | (spl8_69 | spl8_71)),
% 4.04/0.97 inference(forward_subsumption_resolution,[],[f2594,f2562])).
% 4.04/0.97 thf(f2596,plain,(
% 4.04/0.97 spl8_69 | spl8_71),
% 4.04/0.97 inference(avatar_contradiction_clause,[],[f2595])).
% 4.04/0.97 thf(f2634,plain,(
% 4.04/0.97 ((((^[Y0 : $o]: ($false)) @ sK23)) != ((f0 @ sK23))) | spl8_18),
% 4.04/0.97 inference(negative_extensionality,[],[f962])).
% 4.04/0.97 thf(f2635,plain,(
% 4.04/0.97 ((((^[Y0 : $o]: ($false)) @ sK23)) = $true) | ($true = ((f0 @ sK23))) | spl8_18),
% 4.04/0.97 inference(xor_proxy_clausification,[],[f2634])).
% 4.04/0.97 thf(f2638,plain,(
% 4.04/0.97 ($false = $true) | ($true = ((f0 @ sK23))) | spl8_18),
% 4.04/0.97 inference(beta-eta_normalization,[],[f2635])).
% 4.04/0.97 thf(f2639,plain,(
% 4.04/0.97 ($true = ((f0 @ sK23))) | spl8_18),
% 4.04/0.97 inference(trivial_inequality_removal,[],[f2638])).
% 4.04/0.97 thf(f2693,plain,(
% 4.04/0.97 ($false = sK23) | ($false = $true) | spl8_18),
% 4.04/0.97 inference(constrained_superposition,[],[f96,f2639])).
% 4.04/0.97 thf(f2694,plain,(
% 4.04/0.97 ($false = sK23) | spl8_18),
% 4.04/0.97 inference(trivial_inequality_removal,[],[f2693])).
% 4.04/0.97 thf(f2699,plain,(
% 4.04/0.97 ($true = ((f0 @ $false))) | spl8_18),
% 4.04/0.97 inference(constrained_superposition,[],[f2639,f2694])).
% 4.04/0.97 thf(f2701,plain,(
% 4.04/0.97 ($false = $true) | spl8_18),
% 4.04/0.97 inference(forward_demodulation,[],[f2699,f42])).
% 4.04/0.97 thf(f2702,plain,(
% 4.04/0.97 $false | spl8_18),
% 4.04/0.97 inference(trivial_inequality_removal,[],[f2701])).
% 4.04/0.97 thf(f2703,plain,(
% 4.04/0.97 spl8_18),
% 4.04/0.97 inference(avatar_contradiction_clause,[],[f2702])).
% 4.04/0.97 thf(f2791,definition,(
% 4.04/0.97 spl8_76 <=> (f0 = f2)),
% 4.04/0.97 introduced(definition,[new_symbols(definition,[spl8_76])],[avatar_definition])).
% 4.04/0.97 thf(f2793,plain,(
% 4.04/0.97 (f0 = f2) | ~spl8_76),
% 4.04/0.97 inference(avatar_component_clause,[],[f2791])).
% 4.04/0.97 thf(f2867,plain,(
% 4.04/0.97 ( ! [X1 : $o] : ((((f0 @ X1)) = (((^[Y0 : $o]: ($false)) @ X1)))) ) | ~spl8_18),
% 4.04/0.97 inference(argument_congruence,[],[f963])).
% 4.04/0.97 thf(f2869,plain,(
% 4.04/0.97 ( ! [X1 : $o] : ((((f0 @ X1)) = $false) | ($true = (((^[Y0 : $o]: ($false)) @ X1)))) ) | ~spl8_18),
% 4.04/0.97 inference(iff_proxy_clausification,[],[f2867])).
% 4.04/0.97 thf(f2870,plain,(
% 4.04/0.97 ( ! [X1 : $o] : (($false = $true) | (((f0 @ X1)) = $false)) ) | ~spl8_18),
% 4.04/0.97 inference(beta-eta_normalization,[],[f2869])).
% 4.04/0.97 thf(f2871,plain,(
% 4.04/0.97 ( ! [X1 : $o] : ((((f0 @ X1)) = $false)) ) | ~spl8_18),
% 4.04/0.97 inference(trivial_inequality_removal,[],[f2870])).
% 4.04/0.97 thf(f2876,plain,(
% 4.04/0.97 ( ! [X1 : $o] : ((((f0 @ X1)) = (((^[Y0 : $o]: (Y0)) @ X1)))) ) | ~spl8_21),
% 4.04/0.97 inference(argument_congruence,[],[f974])).
% 4.04/0.97 thf(f2877,plain,(
% 4.04/0.97 ( ! [X1 : $o] : ((((f0 @ X1)) = $true) | ($false = (((^[Y0 : $o]: (Y0)) @ X1)))) ) | ~spl8_21),
% 4.04/0.97 inference(iff_proxy_clausification,[],[f2876])).
% 4.04/0.97 thf(f2880,plain,(
% 4.04/0.97 ( ! [X1 : $o] : ((((f0 @ X1)) = $true) | ($false = X1)) ) | ~spl8_21),
% 4.04/0.97 inference(beta-eta_normalization,[],[f2877])).
% 4.04/0.97 thf(f2881,plain,(
% 4.04/0.97 ( ! [X1 : $o] : (($false = X1) | ($false = $true)) ) | (~spl8_18 | ~spl8_21)),
% 4.04/0.97 inference(forward_demodulation,[],[f2880,f2871])).
% 4.04/0.97 thf(f2882,plain,(
% 4.04/0.97 ( ! [X1 : $o] : (($false = X1)) ) | (~spl8_18 | ~spl8_21)),
% 4.04/0.97 inference(trivial_inequality_removal,[],[f2881])).
% 4.04/0.97 thf(f2909,plain,(
% 4.04/0.97 ( ! [X0 : ($i > $o),X1 : $i] : ((((X0 @ X1)) != $true) | ($false = $true)) ) | (~spl8_18 | ~spl8_21)),
% 4.04/0.97 inference(constrained_superposition,[],[f43,f2882])).
% 4.04/0.97 thf(f2969,plain,(
% 4.04/0.97 ( ! [X0 : ($i > $o),X1 : $i] : ((((X0 @ X1)) != $true)) ) | (~spl8_18 | ~spl8_21)),
% 4.04/0.97 inference(trivial_inequality_removal,[],[f2909])).
% 4.04/0.97 thf(f3003,plain,(
% 4.04/0.97 ( ! [X0 : ($i > $o),X1 : $i] : ((((X0 @ X1)) != $false)) ) | (~spl8_18 | ~spl8_21)),
% 4.04/0.97 inference(forward_demodulation,[],[f2969,f2882])).
% 4.04/0.97 thf(f3015,plain,(
% 4.04/0.97 $false | (~spl8_18 | ~spl8_21)),
% 4.04/0.97 inference(forward_subsumption_resolution,[],[f3003,f2882])).
% 4.04/0.97 thf(f3016,plain,(
% 4.04/0.97 ~spl8_18 | ~spl8_21),
% 4.04/0.97 inference(avatar_contradiction_clause,[],[f3015])).
% 4.04/0.97 thf(f3037,plain,(
% 4.04/0.97 ($false = $true) | ($false = $true) | ~spl8_14),
% 4.04/0.97 inference(constrained_superposition,[],[f39,f2182])).
% 4.04/0.97 thf(f3060,plain,(
% 4.04/0.97 ($false = $true) | ~spl8_14),
% 4.04/0.97 inference(duplicate_literal_removal,[],[f3037])).
% 4.04/0.97 thf(f3061,plain,(
% 4.04/0.97 $false | ~spl8_14),
% 4.04/0.97 inference(trivial_inequality_removal,[],[f3060])).
% 4.04/0.97 thf(f3062,plain,(
% 4.04/0.97 ~spl8_14),
% 4.04/0.97 inference(avatar_contradiction_clause,[],[f3061])).
% 4.04/0.97 thf(f3104,plain,(
% 4.04/0.97 (sK1 != sK1) | ~spl8_12),
% 4.04/0.97 inference(imitation,[],[f503])).
% 4.04/0.97 thf(f3107,plain,(
% 4.04/0.97 $false | ~spl8_12),
% 4.04/0.97 inference(trivial_inequality_removal,[],[f3104])).
% 4.04/0.97 thf(f3108,plain,(
% 4.04/0.97 ~spl8_12),
% 4.04/0.97 inference(avatar_contradiction_clause,[],[f3107])).
% 4.04/0.97 thf(f3229,plain,(
% 4.04/0.97 (((~ sK29)) != ((f1 @ sK29))) | spl8_39),
% 4.04/0.97 inference(negative_extensionality,[],[f1525])).
% 4.04/0.97 thf(f3230,plain,(
% 4.04/0.97 (((~ sK29)) = $true) | ($true = ((f1 @ sK29))) | spl8_39),
% 4.04/0.97 inference(xor_proxy_clausification,[],[f3229])).
% 4.04/0.97 thf(f3231,plain,(
% 4.04/0.97 ($false = ((~ sK29))) | ($false = ((f1 @ sK29))) | spl8_39),
% 4.04/0.97 inference(xor_proxy_clausification,[],[f3229])).
% 4.04/0.97 thf(f3232,plain,(
% 4.04/0.97 ($false = ((f1 @ sK29))) | ($true = sK29) | spl8_39),
% 4.04/0.97 inference(not_proxy_clausification,[],[f3231])).
% 4.04/0.97 thf(f3233,plain,(
% 4.04/0.97 ($false = sK29) | ($true = ((f1 @ sK29))) | spl8_39),
% 4.04/0.97 inference(not_proxy_clausification,[],[f3230])).
% 4.04/0.97 thf(f3235,definition,(
% 4.04/0.97 spl8_83 <=> ($false = ((f1 @ sK29)))),
% 4.04/0.97 introduced(definition,[new_symbols(definition,[spl8_83])],[avatar_definition])).
% 4.04/0.97 thf(f3237,plain,(
% 4.04/0.97 ($false = ((f1 @ sK29))) | ~spl8_83),
% 4.04/0.97 inference(avatar_component_clause,[],[f3235])).
% 4.04/0.97 thf(f3239,definition,(
% 4.04/0.97 spl8_84 <=> ($true = sK29)),
% 4.04/0.97 introduced(definition,[new_symbols(definition,[spl8_84])],[avatar_definition])).
% 4.04/0.97 thf(f3240,plain,(
% 4.04/0.97 ($true != sK29) | spl8_84),
% 4.04/0.97 inference(avatar_component_clause,[],[f3239])).
% 4.04/0.97 thf(f3241,plain,(
% 4.04/0.97 ($true = sK29) | ~spl8_84),
% 4.04/0.97 inference(avatar_component_clause,[],[f3239])).
% 4.04/0.97 thf(f3242,plain,(
% 4.04/0.97 spl8_83 | spl8_84 | spl8_39),
% 4.04/0.97 inference(avatar_split_clause,[],[f3232,f1524,f3239,f3235])).
% 4.04/0.97 thf(f3244,definition,(
% 4.04/0.97 spl8_85 <=> ($true = ((f1 @ sK29)))),
% 4.04/0.97 introduced(definition,[new_symbols(definition,[spl8_85])],[avatar_definition])).
% 4.04/0.97 thf(f3246,plain,(
% 4.04/0.97 ($true = ((f1 @ sK29))) | ~spl8_85),
% 4.04/0.97 inference(avatar_component_clause,[],[f3244])).
% 4.04/0.97 thf(f3248,definition,(
% 4.04/0.97 spl8_86 <=> ($false = sK29)),
% 4.04/0.97 introduced(definition,[new_symbols(definition,[spl8_86])],[avatar_definition])).
% 4.04/0.97 thf(f3250,plain,(
% 4.04/0.97 ($false = sK29) | ~spl8_86),
% 4.04/0.97 inference(avatar_component_clause,[],[f3248])).
% 4.04/0.97 thf(f3251,plain,(
% 4.04/0.97 spl8_85 | spl8_86 | spl8_39),
% 4.04/0.97 inference(avatar_split_clause,[],[f3233,f1524,f3248,f3244])).
% 4.04/0.97 thf(f3269,plain,(
% 4.04/0.97 ($true = ((f1 @ $true))) | (~spl8_84 | ~spl8_85)),
% 4.04/0.97 inference(forward_demodulation,[],[f3246,f3241])).
% 4.04/0.97 thf(f3270,plain,(
% 4.04/0.97 ($false = $true) | (~spl8_84 | ~spl8_85)),
% 4.04/0.97 inference(forward_demodulation,[],[f3269,f47])).
% 4.04/0.97 thf(f3271,plain,(
% 4.04/0.97 $false | (~spl8_84 | ~spl8_85)),
% 4.04/0.97 inference(trivial_inequality_removal,[],[f3270])).
% 4.04/0.97 thf(f3272,plain,(
% 4.04/0.97 ~spl8_84 | ~spl8_85),
% 4.04/0.97 inference(avatar_contradiction_clause,[],[f3271])).
% 4.04/0.97 thf(f3273,plain,(
% 4.04/0.97 ($false = sK29) | ($true != $true) | spl8_84),
% 4.04/0.97 inference(constrained_superposition,[],[f3240,f50])).
% 4.04/0.97 thf(f3274,plain,(
% 4.04/0.97 ($false = sK29) | spl8_84),
% 4.04/0.97 inference(trivial_inequality_removal,[],[f3273])).
% 4.04/0.97 thf(f3275,plain,(
% 4.04/0.97 spl8_86 | spl8_84),
% 4.04/0.97 inference(avatar_split_clause,[],[f3274,f3239,f3248])).
% 4.04/0.97 thf(f3278,plain,(
% 4.04/0.97 ($false = ((f1 @ $false))) | (~spl8_83 | ~spl8_86)),
% 4.04/0.97 inference(forward_demodulation,[],[f3237,f3250])).
% 4.04/0.97 thf(f3279,plain,(
% 4.04/0.97 ($false = $true) | (~spl8_83 | ~spl8_86)),
% 4.04/0.97 inference(forward_demodulation,[],[f3278,f45])).
% 4.04/0.97 thf(f3280,plain,(
% 4.04/0.97 $false | (~spl8_83 | ~spl8_86)),
% 4.04/0.97 inference(trivial_inequality_removal,[],[f3279])).
% 4.04/0.97 thf(f3281,plain,(
% 4.04/0.97 ~spl8_83 | ~spl8_86),
% 4.04/0.97 inference(avatar_contradiction_clause,[],[f3280])).
% 4.04/0.97 thf(f3283,plain,(
% 4.04/0.97 ($false = $true) | (~spl8_84 | ~spl8_86)),
% 4.04/0.97 inference(forward_demodulation,[],[f3241,f3250])).
% 4.04/0.97 thf(f3284,plain,(
% 4.04/0.97 $false | (~spl8_84 | ~spl8_86)),
% 4.04/0.97 inference(trivial_inequality_removal,[],[f3283])).
% 4.04/0.97 thf(f3285,plain,(
% 4.04/0.97 ~spl8_84 | ~spl8_86),
% 4.04/0.97 inference(avatar_contradiction_clause,[],[f3284])).
% 4.04/0.97 thf(f3295,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((sF6 = sK1) | (~ = f2) | (sK1 != X0) | (f2 != (^[Y0 : $o]: (Y0))) | (f2 = (^[Y0 : $o]: ($false)))) ) | spl8_41),
% 4.04/0.97 inference(forward_subsumption_resolution,[],[f1800,f1998])).
% 4.04/0.97 thf(f3379,plain,(
% 4.04/0.97 ( ! [X1 : $o] : (((((^[Y0 : $o]: ($true)) @ X1)) = ((f1 @ X1)))) ) | ~spl8_36),
% 4.04/0.97 inference(argument_congruence,[],[f1510])).
% 4.04/0.97 thf(f3381,plain,(
% 4.04/0.97 ( ! [X1 : $o] : (($false = (((^[Y0 : $o]: ($true)) @ X1))) | (((f1 @ X1)) = $true)) ) | ~spl8_36),
% 4.04/0.97 inference(iff_proxy_clausification,[],[f3379])).
% 4.04/0.97 thf(f3382,plain,(
% 4.04/0.97 ( ! [X1 : $o] : (($false = $true) | (((f1 @ X1)) = $true)) ) | ~spl8_36),
% 4.04/0.97 inference(beta-eta_normalization,[],[f3381])).
% 4.04/0.97 thf(f3383,plain,(
% 4.04/0.97 ( ! [X1 : $o] : ((((f1 @ X1)) = $true)) ) | ~spl8_36),
% 4.04/0.97 inference(trivial_inequality_removal,[],[f3382])).
% 4.04/0.97 thf(f3390,plain,(
% 4.04/0.97 ($false = $true) | ~spl8_36),
% 4.04/0.97 inference(constrained_superposition,[],[f3383,f47])).
% 4.04/0.97 thf(f3402,plain,(
% 4.04/0.97 $false | ~spl8_36),
% 4.04/0.97 inference(trivial_inequality_removal,[],[f3390])).
% 4.04/0.97 thf(f3403,plain,(
% 4.04/0.97 ~spl8_36),
% 4.04/0.97 inference(avatar_contradiction_clause,[],[f3402])).
% 4.04/0.97 thf(f3416,plain,(
% 4.04/0.97 (f0 = f1) | (~spl8_18 | ~spl8_34)),
% 4.04/0.97 inference(forward_demodulation,[],[f1501,f963])).
% 4.04/0.97 thf(f3425,definition,(
% 4.04/0.97 spl8_91 <=> (f0 = f1)),
% 4.04/0.97 introduced(definition,[new_symbols(definition,[spl8_91])],[avatar_definition])).
% 4.04/0.97 thf(f3426,plain,(
% 4.04/0.97 (f0 != f1) | spl8_91),
% 4.04/0.97 inference(avatar_component_clause,[],[f3425])).
% 4.04/0.97 thf(f3427,plain,(
% 4.04/0.97 (f0 = f1) | ~spl8_91),
% 4.04/0.97 inference(avatar_component_clause,[],[f3425])).
% 4.04/0.97 thf(f3440,plain,(
% 4.04/0.97 $false | ~spl8_7),
% 4.04/0.97 inference(equality_resolution,[],[f480])).
% 4.04/0.97 thf(f3443,plain,(
% 4.04/0.97 ~spl8_7),
% 4.04/0.97 inference(avatar_contradiction_clause,[],[f3440])).
% 4.04/0.97 thf(f3453,plain,(
% 4.04/0.97 spl8_91 | ~spl8_18 | ~spl8_34),
% 4.04/0.97 inference(avatar_split_clause,[],[f3416,f1500,f961,f3425])).
% 4.04/0.97 thf(f3454,plain,(
% 4.04/0.97 ( ! [X1 : $o] : ((((f0 @ X1)) = ((f1 @ X1)))) ) | ~spl8_91),
% 4.04/0.97 inference(argument_congruence,[],[f3427])).
% 4.04/0.97 thf(f3456,plain,(
% 4.04/0.97 ( ! [X1 : $o] : (($false = ((f1 @ X1))) | (((f0 @ X1)) = $true)) ) | ~spl8_91),
% 4.04/0.97 inference(iff_proxy_clausification,[],[f3454])).
% 4.04/0.97 thf(f3458,plain,(
% 4.04/0.97 ( ! [X1 : $o] : (($false = ((f1 @ X1))) | ($false = $true)) ) | (~spl8_18 | ~spl8_91)),
% 4.04/0.97 inference(forward_demodulation,[],[f3456,f2871])).
% 4.04/0.97 thf(f3459,plain,(
% 4.04/0.97 ( ! [X1 : $o] : (($false = ((f1 @ X1)))) ) | (~spl8_18 | ~spl8_91)),
% 4.04/0.97 inference(trivial_inequality_removal,[],[f3458])).
% 4.04/0.97 thf(f3461,plain,(
% 4.04/0.97 ($false = $true) | (~spl8_18 | ~spl8_91)),
% 4.04/0.97 inference(constrained_superposition,[],[f3459,f45])).
% 4.04/0.97 thf(f3466,plain,(
% 4.04/0.97 $false | (~spl8_18 | ~spl8_91)),
% 4.04/0.97 inference(trivial_inequality_removal,[],[f3461])).
% 4.04/0.97 thf(f3467,plain,(
% 4.04/0.97 ~spl8_18 | ~spl8_91),
% 4.04/0.97 inference(avatar_contradiction_clause,[],[f3466])).
% 4.04/0.97 thf(f3477,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((sK0 != X0) | (~ = f0) | (f0 != (^[Y0 : $o]: ($false))) | (f0 = (^[Y0 : $o]: ($true))) | (sK0 = sF7)) ) | spl8_21),
% 4.04/0.97 inference(forward_subsumption_resolution,[],[f611,f975])).
% 4.04/0.97 thf(f3488,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((sK0 != X0) | (f0 = (^[Y0 : $o]: ($true))) | (~ = f0) | (sK0 = sF7)) ) | (~spl8_18 | spl8_21)),
% 4.04/0.97 inference(forward_subsumption_resolution,[],[f3477,f963])).
% 4.04/0.97 thf(f3611,plain,(
% 4.04/0.97 ($false = ((f3 @ $false))) | ($false = $true) | ~spl8_46),
% 4.04/0.97 inference(constrained_superposition,[],[f2216,f48])).
% 4.04/0.97 thf(f3623,plain,(
% 4.04/0.97 ($false = ((f3 @ $false))) | ~spl8_46),
% 4.04/0.97 inference(trivial_inequality_removal,[],[f3611])).
% 4.04/0.97 thf(f3629,plain,(
% 4.04/0.97 ($false = $true) | ~spl8_46),
% 4.04/0.97 inference(forward_demodulation,[],[f3623,f46])).
% 4.04/0.97 thf(f3630,plain,(
% 4.04/0.97 $false | ~spl8_46),
% 4.04/0.97 inference(trivial_inequality_removal,[],[f3629])).
% 4.04/0.97 thf(f3631,plain,(
% 4.04/0.97 ~spl8_46),
% 4.04/0.97 inference(avatar_contradiction_clause,[],[f3630])).
% 4.04/0.97 thf(f3638,plain,(
% 4.04/0.97 (f2 = f3) | (~spl8_5 | ~spl8_43)),
% 4.04/0.97 inference(forward_demodulation,[],[f473,f2007])).
% 4.04/0.97 thf(f3640,plain,(
% 4.04/0.97 spl8_46 | ~spl8_5 | ~spl8_43),
% 4.04/0.97 inference(avatar_split_clause,[],[f3638,f2005,f471,f2038])).
% 4.04/0.97 thf(f3673,definition,(
% 4.04/0.97 spl8_96 <=> ($false = ((f3 @ sK35)))),
% 4.04/0.97 introduced(definition,[new_symbols(definition,[spl8_96])],[avatar_definition])).
% 4.04/0.97 thf(f3674,plain,(
% 4.04/0.97 ($false != ((f3 @ sK35))) | spl8_96),
% 4.04/0.97 inference(avatar_component_clause,[],[f3673])).
% 4.04/0.97 thf(f3675,plain,(
% 4.04/0.97 ($false = ((f3 @ sK35))) | ~spl8_96),
% 4.04/0.97 inference(avatar_component_clause,[],[f3673])).
% 4.04/0.97 thf(f3721,plain,(
% 4.04/0.97 ((((^[Y0 : $o]: ($true)) @ sK37)) != ((f3 @ sK37))) | spl8_10),
% 4.04/0.97 inference(negative_extensionality,[],[f491])).
% 4.04/0.97 thf(f3723,plain,(
% 4.04/0.97 ($false = ((f3 @ sK37))) | ($false = (((^[Y0 : $o]: ($true)) @ sK37))) | spl8_10),
% 4.04/0.97 inference(xor_proxy_clausification,[],[f3721])).
% 4.04/0.97 thf(f3724,plain,(
% 4.04/0.97 ($false = ((f3 @ sK37))) | ($false = $true) | spl8_10),
% 4.04/0.97 inference(beta-eta_normalization,[],[f3723])).
% 4.04/0.97 thf(f3725,plain,(
% 4.04/0.97 ($false = ((f3 @ sK37))) | spl8_10),
% 4.04/0.97 inference(trivial_inequality_removal,[],[f3724])).
% 4.04/0.97 thf(f3764,plain,(
% 4.04/0.97 ($false = sK35) | ($false = $true) | ~spl8_96),
% 4.04/0.97 inference(constrained_superposition,[],[f91,f3675])).
% 4.04/0.97 thf(f3765,plain,(
% 4.04/0.97 ($false = sK35) | ~spl8_96),
% 4.04/0.97 inference(trivial_inequality_removal,[],[f3764])).
% 4.04/0.97 thf(f3771,plain,(
% 4.04/0.97 ($false = ((f3 @ $false))) | ~spl8_96),
% 4.04/0.97 inference(constrained_superposition,[],[f3675,f3765])).
% 4.04/0.97 thf(f3773,plain,(
% 4.04/0.97 ($false = $true) | ~spl8_96),
% 4.04/0.97 inference(forward_demodulation,[],[f3771,f46])).
% 4.04/0.97 thf(f3774,plain,(
% 4.04/0.97 $false | ~spl8_96),
% 4.04/0.97 inference(trivial_inequality_removal,[],[f3773])).
% 4.04/0.97 thf(f3775,plain,(
% 4.04/0.97 ~spl8_96),
% 4.04/0.97 inference(avatar_contradiction_clause,[],[f3774])).
% 4.04/0.97 thf(f3799,plain,(
% 4.04/0.97 ($false = $true) | ($false = sK37) | spl8_10),
% 4.04/0.97 inference(constrained_superposition,[],[f91,f3725])).
% 4.04/0.97 thf(f3801,plain,(
% 4.04/0.97 ($false = sK37) | spl8_10),
% 4.04/0.97 inference(trivial_inequality_removal,[],[f3799])).
% 4.04/0.97 thf(f3806,plain,(
% 4.04/0.97 ($false = ((f3 @ $false))) | spl8_10),
% 4.04/0.97 inference(constrained_superposition,[],[f3725,f3801])).
% 4.04/0.97 thf(f3808,plain,(
% 4.04/0.97 ($false = $true) | spl8_10),
% 4.04/0.97 inference(forward_demodulation,[],[f3806,f46])).
% 4.04/0.97 thf(f3809,plain,(
% 4.04/0.97 $false | spl8_10),
% 4.04/0.97 inference(trivial_inequality_removal,[],[f3808])).
% 4.04/0.97 thf(f3810,plain,(
% 4.04/0.97 spl8_10),
% 4.04/0.97 inference(avatar_contradiction_clause,[],[f3809])).
% 4.04/0.97 thf(f3820,plain,(
% 4.04/0.97 (f0 = f3) | (~spl8_6 | ~spl8_18)),
% 4.04/0.97 inference(forward_demodulation,[],[f476,f963])).
% 4.04/0.97 thf(f3885,definition,(
% 4.04/0.97 spl8_101 <=> (f1 = f2)),
% 4.04/0.97 introduced(definition,[new_symbols(definition,[spl8_101])],[avatar_definition])).
% 4.04/0.97 thf(f3886,plain,(
% 4.04/0.97 (f1 = f2) | ~spl8_101),
% 4.04/0.97 inference(avatar_component_clause,[],[f3885])).
% 4.04/0.97 thf(f3887,plain,(
% 4.04/0.97 (f1 != f2) | spl8_101),
% 4.04/0.97 inference(avatar_component_clause,[],[f3885])).
% 4.04/0.97 thf(f3933,plain,(
% 4.04/0.97 (f1 = f2) | (~spl8_33 | ~spl8_43)),
% 4.04/0.97 inference(forward_demodulation,[],[f1498,f2007])).
% 4.04/0.97 thf(f3937,plain,(
% 4.04/0.97 spl8_101 | ~spl8_33 | ~spl8_43),
% 4.04/0.97 inference(avatar_split_clause,[],[f3933,f2005,f1496,f3885])).
% 4.04/0.97 thf(f3951,plain,(
% 4.04/0.97 ( ! [X1 : $o] : ((((f1 @ X1)) = ((f2 @ X1)))) ) | ~spl8_101),
% 4.04/0.97 inference(argument_congruence,[],[f3886])).
% 4.04/0.97 thf(f3954,plain,(
% 4.04/0.97 ( ! [X1 : $o] : (($false = ((f2 @ X1))) | (((f1 @ X1)) = $true)) ) | ~spl8_101),
% 4.04/0.97 inference(iff_proxy_clausification,[],[f3951])).
% 4.04/0.97 thf(f3956,plain,(
% 4.04/0.97 ( ! [X1 : $o] : ((((f0 @ X1)) = ((f3 @ X1)))) ) | (~spl8_6 | ~spl8_18)),
% 4.04/0.97 inference(argument_congruence,[],[f3820])).
% 4.04/0.97 thf(f3958,plain,(
% 4.04/0.97 ( ! [X1 : $o] : ((((f0 @ X1)) = $true) | ($false = ((f3 @ X1)))) ) | (~spl8_6 | ~spl8_18)),
% 4.04/0.97 inference(iff_proxy_clausification,[],[f3956])).
% 4.04/0.97 thf(f3960,plain,(
% 4.04/0.97 ( ! [X1 : $o] : (($false = ((f3 @ X1))) | ($false = $true)) ) | (~spl8_6 | ~spl8_18)),
% 4.04/0.97 inference(forward_demodulation,[],[f3958,f2871])).
% 4.04/0.97 thf(f3961,plain,(
% 4.04/0.97 ( ! [X1 : $o] : (($false = ((f3 @ X1)))) ) | (~spl8_6 | ~spl8_18)),
% 4.04/0.97 inference(trivial_inequality_removal,[],[f3960])).
% 4.04/0.97 thf(f3976,plain,(
% 4.04/0.97 ($false != $false) | (~spl8_6 | ~spl8_18 | spl8_96)),
% 4.04/0.97 inference(constrained_superposition,[],[f3674,f3961])).
% 4.04/0.97 thf(f4000,plain,(
% 4.04/0.97 $false | (~spl8_6 | ~spl8_18 | spl8_96)),
% 4.04/0.97 inference(trivial_inequality_removal,[],[f3976])).
% 4.04/0.97 thf(f4001,plain,(
% 4.04/0.97 ~spl8_6 | ~spl8_18 | spl8_96),
% 4.04/0.97 inference(avatar_contradiction_clause,[],[f4000])).
% 4.04/0.97 thf(f4004,plain,(
% 4.04/0.97 (f0 != f3) | (spl8_6 | ~spl8_18)),
% 4.04/0.97 inference(forward_demodulation,[],[f477,f963])).
% 4.04/0.97 thf(f4031,plain,(
% 4.04/0.97 ($true = ((f1 @ $true))) | ($false = $true) | ~spl8_101),
% 4.04/0.97 inference(constrained_superposition,[],[f40,f3954])).
% 4.04/0.97 thf(f4054,plain,(
% 4.04/0.97 ($true = ((f1 @ $true))) | ~spl8_101),
% 4.04/0.97 inference(trivial_inequality_removal,[],[f4031])).
% 4.04/0.97 thf(f4076,plain,(
% 4.04/0.97 ($false = $true) | ~spl8_101),
% 4.04/0.97 inference(forward_demodulation,[],[f4054,f47])).
% 4.04/0.97 thf(f4077,plain,(
% 4.04/0.97 $false | ~spl8_101),
% 4.04/0.97 inference(trivial_inequality_removal,[],[f4076])).
% 4.04/0.97 thf(f4078,plain,(
% 4.04/0.97 ~spl8_101),
% 4.04/0.97 inference(avatar_contradiction_clause,[],[f4077])).
% 4.04/0.97 thf(f4165,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((sK1 != X0) | (~ = f2) | (sF6 = sK1) | (f2 = (^[Y0 : $o]: ($false)))) ) | (spl8_41 | ~spl8_43)),
% 4.04/0.97 inference(forward_subsumption_resolution,[],[f3295,f2007])).
% 4.04/0.97 thf(f4178,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((sK1 != X0) | (f2 = (^[Y0 : $o]: ($false))) | (f1 = f2) | (sF6 = sK1)) ) | (~spl8_39 | spl8_41 | ~spl8_43)),
% 4.04/0.97 inference(forward_demodulation,[],[f4165,f1526])).
% 4.04/0.97 thf(f4188,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((f1 = f2) | (f0 = f2) | (sF6 = sK1) | (sK1 != X0)) ) | (~spl8_18 | ~spl8_39 | spl8_41 | ~spl8_43)),
% 4.04/0.97 inference(forward_demodulation,[],[f4178,f963])).
% 4.04/0.97 thf(f4275,plain,(
% 4.04/0.97 ( ! [X1 : $o] : ((((f0 @ X1)) = ((f2 @ X1)))) ) | ~spl8_76),
% 4.04/0.97 inference(argument_congruence,[],[f2793])).
% 4.04/0.97 thf(f4277,plain,(
% 4.04/0.97 ( ! [X1 : $o] : ((((f0 @ X1)) = $true) | ($false = ((f2 @ X1)))) ) | ~spl8_76),
% 4.04/0.97 inference(iff_proxy_clausification,[],[f4275])).
% 4.04/0.97 thf(f4279,plain,(
% 4.04/0.97 ( ! [X1 : $o] : (($false = $true) | ($false = ((f2 @ X1)))) ) | (~spl8_18 | ~spl8_76)),
% 4.04/0.97 inference(forward_demodulation,[],[f4277,f2871])).
% 4.04/0.97 thf(f4280,plain,(
% 4.04/0.97 ( ! [X1 : $o] : (($false = ((f2 @ X1)))) ) | (~spl8_18 | ~spl8_76)),
% 4.04/0.97 inference(trivial_inequality_removal,[],[f4279])).
% 4.04/0.97 thf(f4295,plain,(
% 4.04/0.97 ($false = $true) | (~spl8_18 | ~spl8_76)),
% 4.04/0.97 inference(constrained_superposition,[],[f4280,f40])).
% 4.04/0.97 thf(f4340,plain,(
% 4.04/0.97 $false | (~spl8_18 | ~spl8_76)),
% 4.04/0.97 inference(trivial_inequality_removal,[],[f4295])).
% 4.04/0.97 thf(f4341,plain,(
% 4.04/0.97 ~spl8_18 | ~spl8_76),
% 4.04/0.97 inference(avatar_contradiction_clause,[],[f4340])).
% 4.04/0.97 thf(f4350,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((f0 = f2) | (sK1 != X0) | (sF6 = sK1)) ) | (~spl8_18 | ~spl8_39 | spl8_41 | ~spl8_43 | spl8_101)),
% 4.04/0.97 inference(forward_subsumption_resolution,[],[f4188,f3887])).
% 4.04/0.97 thf(f4361,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((~ = f0) | (sK0 != X0) | (f0 = f3) | (sK0 = sF7)) ) | (~spl8_10 | ~spl8_18 | spl8_21)),
% 4.04/0.97 inference(forward_demodulation,[],[f3488,f492])).
% 4.04/0.97 thf(f4372,plain,(
% 4.04/0.97 spl8_2 | spl8_12 | spl8_76 | ~spl8_18 | ~spl8_39 | spl8_41 | ~spl8_43 | spl8_101),
% 4.04/0.97 inference(avatar_split_clause,[],[f4350,f3885,f2005,f1997,f1524,f961,f2791,f502,f69])).
% 4.04/0.97 thf(f4384,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((sK0 != X0) | (sK0 = sF7) | (~ = f0)) ) | (spl8_6 | ~spl8_10 | ~spl8_18 | spl8_21)),
% 4.04/0.97 inference(forward_subsumption_resolution,[],[f4361,f4004])).
% 4.04/0.97 thf(f4400,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((f0 = f1) | (sK0 != X0) | (sK0 = sF7)) ) | (spl8_6 | ~spl8_10 | ~spl8_18 | spl8_21 | ~spl8_39)),
% 4.04/0.97 inference(forward_demodulation,[],[f4384,f1526])).
% 4.04/0.97 thf(f4410,plain,(
% 4.04/0.97 ( ! [X0 : $i] : ((sK0 != X0) | (sK0 = sF7)) ) | (spl8_6 | ~spl8_10 | ~spl8_18 | spl8_21 | ~spl8_39 | spl8_91)),
% 4.04/0.97 inference(forward_subsumption_resolution,[],[f4400,f3426])).
% 4.04/0.97 thf(f4415,plain,(
% 4.04/0.97 spl8_1 | spl8_7 | spl8_6 | ~spl8_10 | ~spl8_18 | spl8_21 | ~spl8_39 | spl8_91),
% 4.04/0.97 inference(avatar_split_clause,[],[f4410,f3425,f1524,f973,f961,f490,f475,f479,f65])).
% 4.04/0.97 thf(f4450,plain,(
% 4.04/0.97 (sK2 != sK2) | ~spl8_13),
% 4.04/0.97 inference(imitation,[],[f510])).
% 4.04/0.97 thf(f4453,plain,(
% 4.04/0.97 $false | ~spl8_13),
% 4.04/0.97 inference(trivial_inequality_removal,[],[f4450])).
% 4.04/0.97 thf(f4454,plain,(
% 4.04/0.97 ~spl8_13),
% 4.04/0.97 inference(avatar_contradiction_clause,[],[f4453])).
% 4.04/0.97 cnf(s1, plain, ~spl8_1 | ~spl8_2 | ~spl8_3 | ~spl8_4, inference(sat_conversion,[],[f80])).
% 4.04/0.97 cnf(s24, plain, spl8_3 | spl8_5 | spl8_6 | ~spl8_10 | spl8_13 | spl8_14, inference(sat_conversion,[],[f532])).
% 4.04/0.97 cnf(s91, plain, ~spl8_15, inference(sat_conversion,[],[f1137])).
% 4.04/0.97 cnf(s117, plain, spl8_4 | spl8_15 | spl8_33 | spl8_34 | spl8_36 | ~spl8_39, inference(sat_conversion,[],[f1547])).
% 4.04/0.97 cnf(s211, plain, ~spl8_41, inference(sat_conversion,[],[f2416])).
% 4.04/0.97 cnf(s223, plain, spl8_43 | spl8_68 | spl8_69, inference(sat_conversion,[],[f2564])).
% 4.04/0.97 cnf(s224, plain, spl8_43 | spl8_70 | spl8_71, inference(sat_conversion,[],[f2573])).
% 4.04/0.97 cnf(s225, plain, ~spl8_69 | ~spl8_71, inference(sat_conversion,[],[f2578])).
% 4.04/0.97 cnf(s226, plain, ~spl8_69 | ~spl8_70, inference(sat_conversion,[],[f2583])).
% 4.04/0.97 cnf(s227, plain, ~spl8_68 | ~spl8_71, inference(sat_conversion,[],[f2592])).
% 4.04/0.97 cnf(s228, plain, spl8_69 | spl8_71, inference(sat_conversion,[],[f2596])).
% 4.04/0.97 cnf(s236, plain, spl8_18, inference(sat_conversion,[],[f2703])).
% 4.04/0.97 cnf(s281, plain, ~spl8_18 | ~spl8_21, inference(sat_conversion,[],[f3016])).
% 4.04/0.97 cnf(s283, plain, ~spl8_14, inference(sat_conversion,[],[f3062])).
% 4.04/0.97 cnf(s291, plain, ~spl8_12, inference(sat_conversion,[],[f3108])).
% 4.04/0.97 cnf(s310, plain, spl8_39 | spl8_83 | spl8_84, inference(sat_conversion,[],[f3242])).
% 4.04/0.97 cnf(s311, plain, spl8_39 | spl8_85 | spl8_86, inference(sat_conversion,[],[f3251])).
% 4.04/0.97 cnf(s313, plain, ~spl8_84 | ~spl8_85, inference(sat_conversion,[],[f3272])).
% 4.04/0.97 cnf(s314, plain, spl8_84 | spl8_86, inference(sat_conversion,[],[f3275])).
% 4.04/0.97 cnf(s315, plain, ~spl8_83 | ~spl8_86, inference(sat_conversion,[],[f3281])).
% 4.04/0.97 cnf(s316, plain, ~spl8_84 | ~spl8_86, inference(sat_conversion,[],[f3285])).
% 4.04/0.97 cnf(s334, plain, ~spl8_36, inference(sat_conversion,[],[f3403])).
% 4.04/0.97 cnf(s345, plain, ~spl8_7, inference(sat_conversion,[],[f3443])).
% 4.04/0.97 cnf(s348, plain, ~spl8_18 | ~spl8_34 | spl8_91, inference(sat_conversion,[],[f3453])).
% 4.04/0.97 cnf(s350, plain, ~spl8_18 | ~spl8_91, inference(sat_conversion,[],[f3467])).
% 4.04/0.97 cnf(s362, plain, ~spl8_46, inference(sat_conversion,[],[f3631])).
% 4.04/0.97 cnf(s365, plain, ~spl8_5 | ~spl8_43 | spl8_46, inference(sat_conversion,[],[f3640])).
% 4.04/0.97 cnf(s374, plain, ~spl8_96, inference(sat_conversion,[],[f3775])).
% 4.04/0.97 cnf(s375, plain, spl8_10, inference(sat_conversion,[],[f3810])).
% 4.04/0.97 cnf(s402, plain, ~spl8_33 | ~spl8_43 | spl8_101, inference(sat_conversion,[],[f3937])).
% 4.04/0.97 cnf(s420, plain, ~spl8_6 | ~spl8_18 | spl8_96, inference(sat_conversion,[],[f4001])).
% 4.04/0.97 cnf(s425, plain, ~spl8_101, inference(sat_conversion,[],[f4078])).
% 4.04/0.97 cnf(s473, plain, ~spl8_18 | ~spl8_76, inference(sat_conversion,[],[f4341])).
% 4.04/0.97 cnf(s475, plain, spl8_2 | spl8_12 | ~spl8_18 | ~spl8_39 | spl8_41 | ~spl8_43 | spl8_76 | spl8_101, inference(sat_conversion,[],[f4372])).
% 4.04/0.97 cnf(s490, plain, spl8_1 | spl8_6 | spl8_7 | ~spl8_10 | ~spl8_18 | spl8_21 | ~spl8_39 | spl8_91, inference(sat_conversion,[],[f4415])).
% 4.04/0.97 cnf(s502, plain, ~spl8_13, inference(sat_conversion,[],[f4454])).
% 4.04/0.97 cnf(s503, plain, ~spl8_33 | ~spl8_43, inference(rat,[],[s402,s425])).
% 4.04/0.97 cnf(s525, plain, ~spl8_76, inference(rat,[],[s473,s236])).
% 4.04/0.97 cnf(s527, plain, ~spl8_6, inference(rat,[],[s420,s374,s236])).
% 4.04/0.97 cnf(s528, plain, ~spl8_91, inference(rat,[],[s350,s236])).
% 4.04/0.97 cnf(s529, plain, ~spl8_34, inference(rat,[],[s348,s528,s236])).
% 4.04/0.97 cnf(s530, plain, ~spl8_21, inference(rat,[],[s281,s236])).
% 4.04/0.97 cnf(s560, plain, spl8_4 | spl8_15 | spl8_33 | ~spl8_39, inference(rat,[],[s117,s334,s529])).
% 4.04/0.97 cnf(s595, plain, spl8_3 | spl8_5, inference(rat,[],[s24,s283,s502,s375,s527])).
% 4.04/0.97 cnf(s603, plain, ~spl8_69 | spl8_43, inference(rat,[],[s224,s225,s226])).
% 4.04/0.97 cnf(s604, plain, spl8_43, inference(rat,[],[s227,s223,s228,s603])).
% 4.04/0.97 cnf(s605, plain, ~spl8_33, inference(rat,[],[s503,s604])).
% 4.04/0.97 cnf(s606, plain, ~spl8_5, inference(rat,[],[s365,s362,s604])).
% 4.04/0.97 cnf(s607, plain, spl8_3, inference(rat,[],[s595,s606])).
% 4.04/0.97 cnf(s608, plain, ~spl8_84 | spl8_39, inference(rat,[],[s311,s313,s316])).
% 4.04/0.97 cnf(s609, plain, spl8_39, inference(rat,[],[s315,s310,s314,s608])).
% 4.04/0.97 cnf(s610, plain, spl8_2, inference(rat,[],[s475,s425,s525,s609,s211,s236,s291,s604])).
% 4.04/0.97 cnf(s614, plain, spl8_1, inference(rat,[],[s490,s528,s527,s530,s236,s375,s345,s609])).
% 4.04/0.97 cnf(s615, plain, spl8_4, inference(rat,[],[s560,s605,s91,s609])).
% 4.04/0.97 cnf(s616, plain, $false, inference(rat,[],[s1,s610,s607,s614,s615])).
% 4.04/0.97 thf(f4455,plain,(
% 4.04/0.97 $false),
% 4.04/0.97 inference(avatar_sat_refutation,[],[s616])).
% 4.04/0.97 % SZS output end Proof for theBenchmark
% 4.04/0.97 % (370785)------------------------------
% 4.04/0.97 % (370785)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.04/0.97 % (370785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.04/0.97 % (370785)CaDiCaL version: 2.1.3
% 4.04/0.97 % (370785)Termination reason: Refutation
% 4.04/0.97 % (370785)Time elapsed: 0.080 s
% 4.04/0.97 % (370785)Peak memory usage: 14 MB
% 4.04/0.97 % (370785)Instructions burned: 156 (million)
% 4.04/0.97 % (370608)Success in time 0.733 s
% 4.04/0.97 % Vampire exiting
%------------------------------------------------------------------------------