%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : PUZ087^1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n010.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:20:52 AM UTC 2026
% Result : Theorem 3.97s 0.99s
% Output : Refutation 3.97s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ087^1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.20 % Computer : n010.cluster.edu
% 0.08/0.20 % Model : x86_64 x86_64
% 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.20 % Memory : 8046.5625MB
% 0.08/0.20 % OS : Linux 6.8.0-71-generic
% 0.08/0.20 % CPULimit : 300
% 0.08/0.20 % WCLimit : 300
% 0.08/0.20 % DateTime : Tue Sep 29 13:22:19 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 Running higher-order theorem proving
% 0.08/0.25 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.22/0.36 % (2834698)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.22/0.36 % (2834703)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=2593412663:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.22/0.36 % (2834709)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.22/0.36 % (2834709)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.22/0.36 % (2834704)lrs+10_16_si=on:nwc=1.5:random_seed=442043560:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.22/0.36 % (2834705)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=4093821359:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.22/0.36 % (2834707)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=3837848686:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.22/0.36 % (2834706)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=1858998128: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.22/0.36 % (2834708)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=1008036916:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.22/0.36 % (2834709)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=3887690024:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.22/0.36 % (2834705)Instruction limit reached!
% 0.22/0.36 % (2834705)------------------------------
% 0.22/0.36 % (2834705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.36 % (2834705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.36 % (2834705)CaDiCaL version: 2.1.3
% 0.22/0.36 % (2834705)Termination reason: Instruction limit
% 0.22/0.36 % (2834705)Termination phase: shuffling
% 0.22/0.36 % (2834705)Time elapsed: 0.002 s
% 0.22/0.36 % (2834705)Peak memory usage: 9 MB
% 0.22/0.36 % (2834705)Instructions burned: 4 (million)
% 0.22/0.36 % (2834704)Instruction limit reached!
% 0.22/0.36 % (2834704)------------------------------
% 0.22/0.36 % (2834704)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.36 % (2834704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.36 % (2834704)CaDiCaL version: 2.1.3
% 0.22/0.36 % (2834704)Termination reason: Instruction limit
% 0.22/0.36 % (2834704)Termination phase: Property scanning
% 0.22/0.36 % (2834704)Time elapsed: 0.008 s
% 0.22/0.36 % (2834704)Peak memory usage: 10 MB
% 0.22/0.36 % (2834704)Instructions burned: 20 (million)
% 0.22/0.36 % (2834707)Instruction limit reached!
% 0.22/0.36 % (2834707)------------------------------
% 0.22/0.36 % (2834707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.36 % (2834707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.36 % (2834707)CaDiCaL version: 2.1.3
% 0.22/0.36 % (2834707)Termination reason: Instruction limit
% 0.22/0.36 % (2834707)Termination phase: Saturation
% 0.22/0.36 % (2834707)Time elapsed: 0.013 s
% 0.22/0.36 % (2834707)Peak memory usage: 11 MB
% 0.22/0.36 % (2834707)Instructions burned: 25 (million)
% 0.22/0.36 % (2834703)Instruction limit reached!
% 0.22/0.36 % (2834703)------------------------------
% 0.22/0.36 % (2834703)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.36 % (2834703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.36 % (2834703)CaDiCaL version: 2.1.3
% 0.22/0.36 % (2834703)Termination reason: Instruction limit
% 0.22/0.36 % (2834703)Termination phase: Saturation
% 0.22/0.36 % (2834703)Time elapsed: 0.026 s
% 0.22/0.36 % (2834703)Peak memory usage: 12 MB
% 0.22/0.36 % (2834703)Instructions burned: 101 (million)
% 0.22/0.36 % (2834721)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=666877102:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.22/0.36 % (2834721)Instruction limit reached!
% 0.22/0.36 % (2834721)------------------------------
% 0.22/0.36 % (2834721)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.38 % (2834721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.38 % (2834721)CaDiCaL version: 2.1.3
% 0.81/0.38 % (2834721)Termination reason: Instruction limit
% 0.81/0.38 % (2834721)Termination phase: shuffling
% 0.81/0.38 % (2834721)Time elapsed: 0.001 s
% 0.81/0.38 % (2834721)Peak memory usage: 9 MB
% 0.81/0.38 % (2834721)Instructions burned: 2 (million)
% 0.81/0.38 % (2834723)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=525704142:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.81/0.38 % (2834725)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=3859365017:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.81/0.38 % (2834724)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.81/0.38 % (2834723)Instruction limit reached!
% 0.81/0.38 % (2834723)------------------------------
% 0.81/0.38 % (2834723)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.38 % (2834723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.38 % (2834723)CaDiCaL version: 2.1.3
% 0.81/0.38 % (2834723)Termination reason: Instruction limit
% 0.81/0.38 % (2834723)Termination phase: Property scanning
% 0.81/0.38 % (2834723)Time elapsed: 0.003 s
% 0.81/0.38 % (2834723)Peak memory usage: 10 MB
% 0.81/0.38 % (2834723)Instructions burned: 7 (million)
% 0.81/0.38 % (2834725)Instruction limit reached!
% 0.81/0.38 % (2834725)------------------------------
% 0.81/0.38 % (2834725)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.38 % (2834725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.38 % (2834725)CaDiCaL version: 2.1.3
% 0.81/0.38 % (2834725)Termination reason: Instruction limit
% 0.81/0.38 % (2834725)Termination phase: Property scanning
% 0.81/0.38 % (2834725)Time elapsed: 0.003 s
% 0.81/0.38 % (2834725)Peak memory usage: 10 MB
% 0.81/0.38 % (2834725)Instructions burned: 14 (million)
% 0.81/0.38 % (2834724)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=151506803:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.81/0.38 % (2834708)Instruction limit reached!
% 0.81/0.38 % (2834708)------------------------------
% 0.81/0.38 % (2834708)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.38 % (2834708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.38 % (2834708)CaDiCaL version: 2.1.3
% 0.81/0.38 % (2834708)Termination reason: Instruction limit
% 0.81/0.38 % (2834708)Termination phase: Saturation
% 0.81/0.38 % (2834708)Time elapsed: 0.035 s
% 0.81/0.38 % (2834708)Peak memory usage: 12 MB
% 0.81/0.38 % (2834708)Instructions burned: 75 (million)
% 0.81/0.38 % (2834724)Instruction limit reached!
% 0.81/0.38 % (2834724)------------------------------
% 0.81/0.38 % (2834724)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.38 % (2834724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.38 % (2834724)CaDiCaL version: 2.1.3
% 0.81/0.38 % (2834724)Termination reason: Instruction limit
% 0.81/0.38 % (2834724)Termination phase: Property scanning
% 0.81/0.38 % (2834724)Time elapsed: 0.003 s
% 0.81/0.38 % (2834724)Peak memory usage: 10 MB
% 0.81/0.38 % (2834724)Instructions burned: 7 (million)
% 0.81/0.38 % (2834727)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.81/0.38 % (2834727)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.81/0.38 % (2834727)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=1347408341: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.81/0.38 % (2834734)lrs+10_1_si=on:cs=on:random_seed=38311159:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.81/0.38 % (2834734)Instruction limit reached!
% 0.81/0.38 % (2834734)------------------------------
% 0.81/0.38 % (2834734)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.38 % (2834734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.41 % (2834734)CaDiCaL version: 2.1.3
% 0.81/0.41 % (2834734)Termination reason: Instruction limit
% 0.81/0.41 % (2834734)Termination phase: Property scanning
% 0.81/0.41 % (2834734)Time elapsed: 0.005 s
% 0.81/0.41 % (2834734)Peak memory usage: 10 MB
% 0.81/0.41 % (2834734)Instructions burned: 22 (million)
% 0.81/0.41 % (2834733)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=1606059613:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.81/0.41 % (2834736)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.81/0.41 % (2834737)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=3635322767:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.81/0.41 % (2834727)Instruction limit reached!
% 0.81/0.41 % (2834727)------------------------------
% 0.81/0.41 % (2834727)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.41 % (2834727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.41 % (2834727)CaDiCaL version: 2.1.3
% 0.81/0.41 % (2834727)Termination reason: Instruction limit
% 0.81/0.41 % (2834727)Termination phase: Saturation
% 0.81/0.41 % (2834727)Time elapsed: 0.012 s
% 0.81/0.41 % (2834727)Peak memory usage: 11 MB
% 0.81/0.41 % (2834727)Instructions burned: 29 (million)
% 0.81/0.41 % (2834736)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=3576185245:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.81/0.41 % (2834747)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=609240245:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.81/0.41 % (2834736)Instruction limit reached!
% 0.81/0.41 % (2834736)------------------------------
% 0.81/0.41 % (2834736)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.41 % (2834736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.41 % (2834736)CaDiCaL version: 2.1.3
% 0.81/0.41 % (2834736)Termination reason: Instruction limit
% 0.81/0.41 % (2834736)Termination phase: Property scanning
% 0.81/0.41 % (2834736)Time elapsed: 0.003 s
% 0.81/0.41 % (2834736)Peak memory usage: 10 MB
% 0.81/0.41 % (2834736)Instructions burned: 6 (million)
% 0.81/0.41 % (2834737)Refutation not found, incomplete strategy
% 0.81/0.41 % (2834737)------------------------------
% 0.81/0.41 % (2834737)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.41 % (2834737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.41 % (2834737)CaDiCaL version: 2.1.3
% 0.81/0.41 % (2834737)Termination reason: Refutation not found, incomplete strategy
% 0.81/0.41 % (2834737)Time elapsed: 0.011 s
% 0.81/0.41 % (2834737)Peak memory usage: 12 MB
% 0.81/0.41 % (2834737)Instructions burned: 23 (million)
% 0.81/0.41 % (2834737)------------------------------
% 0.81/0.41 % (2834737)------------------------------
% 0.81/0.41 % (2834747)Refutation not found, incomplete strategy
% 0.81/0.41 % (2834747)------------------------------
% 0.81/0.41 % (2834747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.41 % (2834747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.41 % (2834747)CaDiCaL version: 2.1.3
% 0.81/0.41 % (2834747)Termination reason: Refutation not found, incomplete strategy
% 0.81/0.41 % (2834747)Time elapsed: 0.008 s
% 0.81/0.41 % (2834747)Peak memory usage: 12 MB
% 0.81/0.41 % (2834747)Instructions burned: 18 (million)
% 0.81/0.41 % (2834747)------------------------------
% 0.81/0.41 % (2834747)------------------------------
% 0.81/0.41 % (2834754)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=2814645375:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/25Mi)
% 0.81/0.41 % (2834760)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=3574778230:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2999 on theBenchmark for (2999ds/14Mi)
% 0.81/0.41 % (2834709)Instruction limit reached!
% 0.81/0.41 % (2834709)------------------------------
% 0.81/0.41 % (2834709)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.41 % (2834709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.45 % (2834709)CaDiCaL version: 2.1.3
% 0.81/0.45 % (2834709)Termination reason: Instruction limit
% 0.81/0.45 % (2834709)Termination phase: Saturation
% 0.81/0.45 % (2834709)Time elapsed: 0.075 s
% 0.81/0.45 % (2834709)Peak memory usage: 12 MB
% 0.81/0.45 % (2834709)Instructions burned: 157 (million)
% 0.81/0.45 % (2834760)Instruction limit reached!
% 0.81/0.45 % (2834760)------------------------------
% 0.81/0.45 % (2834760)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.45 % (2834760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.45 % (2834760)CaDiCaL version: 2.1.3
% 0.81/0.45 % (2834760)Termination reason: Instruction limit
% 0.81/0.45 % (2834760)Termination phase: Function definition elimination
% 0.81/0.45 % (2834760)Time elapsed: 0.005 s
% 0.81/0.45 % (2834760)Peak memory usage: 10 MB
% 0.81/0.45 % (2834760)Instructions burned: 16 (million)
% 0.81/0.45 % (2834765)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=2543852342:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/327Mi)
% 0.81/0.45 % (2834754)Instruction limit reached!
% 0.81/0.45 % (2834754)------------------------------
% 0.81/0.45 % (2834754)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.45 % (2834754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.45 % (2834754)CaDiCaL version: 2.1.3
% 0.81/0.45 % (2834754)Termination reason: Instruction limit
% 0.81/0.45 % (2834754)Termination phase: Saturation
% 0.81/0.45 % (2834754)Time elapsed: 0.013 s
% 0.81/0.45 % (2834754)Peak memory usage: 12 MB
% 0.81/0.45 % (2834754)Instructions burned: 25 (million)
% 0.81/0.45 % (2834767)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=366417606:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/14Mi)
% 0.81/0.45 % (2834778)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=1041738145:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 0.81/0.45 % (2834733)Instruction limit reached!
% 0.81/0.45 % (2834733)------------------------------
% 0.81/0.45 % (2834733)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.45 % (2834733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.45 % (2834733)CaDiCaL version: 2.1.3
% 0.81/0.45 % (2834733)Termination reason: Instruction limit
% 0.81/0.45 % (2834733)Termination phase: Saturation
% 0.81/0.45 % (2834733)Time elapsed: 0.041 s
% 0.81/0.45 % (2834733)Peak memory usage: 13 MB
% 0.81/0.45 % (2834733)Instructions burned: 86 (million)
% 0.81/0.45 % (2834767)Instruction limit reached!
% 0.81/0.45 % (2834767)------------------------------
% 0.81/0.45 % (2834767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.45 % (2834767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.45 % (2834767)CaDiCaL version: 2.1.3
% 0.81/0.45 % (2834767)Termination reason: Instruction limit
% 0.81/0.45 % (2834767)Termination phase: Function definition elimination
% 0.81/0.45 % (2834767)Time elapsed: 0.006 s
% 0.81/0.45 % (2834767)Peak memory usage: 10 MB
% 0.81/0.45 % (2834767)Instructions burned: 15 (million)
% 0.81/0.45 % (2834775)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=751062830: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.81/0.45 % (2834778)Instruction limit reached!
% 0.81/0.45 % (2834778)------------------------------
% 0.81/0.45 % (2834778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.45 % (2834778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.45 % (2834778)CaDiCaL version: 2.1.3
% 0.81/0.45 % (2834778)Termination reason: Instruction limit
% 0.81/0.45 % (2834778)Termination phase: Saturation
% 0.81/0.45 % (2834778)Time elapsed: 0.006 s
% 0.81/0.45 % (2834778)Peak memory usage: 11 MB
% 0.81/0.45 % (2834778)Instructions burned: 29 (million)
% 0.81/0.45 % (2834775)Instruction limit reached!
% 0.81/0.45 % (2834775)------------------------------
% 0.81/0.45 % (2834775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.45 % (2834775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.45 % (2834775)CaDiCaL version: 2.1.3
% 0.81/0.45 % (2834775)Termination reason: Instruction limit
% 0.81/0.45 % (2834775)Termination phase: shuffling
% 0.81/0.45 % (2834775)Time elapsed: 0.002 s
% 1.55/0.47 % (2834775)Peak memory usage: 9 MB
% 1.55/0.47 % (2834775)Instructions burned: 4 (million)
% 1.55/0.47 % (2834765)Refutation not found, incomplete strategy
% 1.55/0.47 % (2834765)------------------------------
% 1.55/0.47 % (2834765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.55/0.47 % (2834765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.55/0.47 % (2834765)CaDiCaL version: 2.1.3
% 1.55/0.47 % (2834765)Termination reason: Refutation not found, incomplete strategy
% 1.55/0.47 % (2834765)Time elapsed: 0.018 s
% 1.55/0.47 % (2834765)Peak memory usage: 12 MB
% 1.55/0.47 % (2834765)Instructions burned: 39 (million)
% 1.55/0.47 % (2834793)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 1.55/0.47 % (2834765)------------------------------
% 1.55/0.47 % (2834765)------------------------------
% 1.55/0.47 % (2834785)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=917315849:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.55/0.47 % (2834793)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=3147583298:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.55/0.47 % (2834791)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
% 1.55/0.47 % (2834791)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 1.55/0.47 % (2834793)Instruction limit reached!
% 1.55/0.47 % (2834793)------------------------------
% 1.55/0.47 % (2834793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.55/0.47 % (2834793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.55/0.47 % (2834793)CaDiCaL version: 2.1.3
% 1.55/0.47 % (2834793)Termination reason: Instruction limit
% 1.55/0.47 % (2834793)Termination phase: Property scanning
% 1.55/0.47 % (2834793)Time elapsed: 0.002 s
% 1.55/0.47 % (2834793)Peak memory usage: 10 MB
% 1.55/0.47 % (2834793)Instructions burned: 9 (million)
% 1.55/0.47 % (2834789)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=1458698275:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 1.55/0.47 % (2834791)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=584909757:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.55/0.47 % (2834785)Instruction limit reached!
% 1.55/0.47 % (2834785)------------------------------
% 1.55/0.47 % (2834785)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.55/0.47 % (2834785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.55/0.47 % (2834785)CaDiCaL version: 2.1.3
% 1.55/0.47 % (2834785)Termination reason: Instruction limit
% 1.55/0.47 % (2834785)Termination phase: Property scanning
% 1.55/0.47 % (2834785)Time elapsed: 0.009 s
% 1.55/0.47 % (2834785)Peak memory usage: 10 MB
% 1.55/0.47 % (2834785)Instructions burned: 23 (million)
% 1.55/0.47 % (2834794)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=3275108467:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 1.55/0.47 % (2834791)Instruction limit reached!
% 1.55/0.47 % (2834791)------------------------------
% 1.55/0.47 % (2834791)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.55/0.47 % (2834800)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=3991442506:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.55/0.47 % (2834791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.55/0.47 % (2834791)CaDiCaL version: 2.1.3
% 1.55/0.47 % (2834791)Termination reason: Instruction limit
% 1.55/0.47 % (2834791)Termination phase: Property scanning
% 1.55/0.47 % (2834791)Time elapsed: 0.006 s
% 1.55/0.47 % (2834791)Peak memory usage: 10 MB
% 1.55/0.47 % (2834791)Instructions burned: 15 (million)
% 1.55/0.47 % (2834798)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=3255307131:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 1.55/0.52 % (2834800)Instruction limit reached!
% 1.55/0.52 % (2834800)------------------------------
% 1.55/0.52 % (2834800)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.55/0.52 % (2834800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.55/0.52 % (2834800)CaDiCaL version: 2.1.3
% 1.55/0.52 % (2834800)Termination reason: Instruction limit
% 1.55/0.52 % (2834800)Termination phase: Saturation
% 1.55/0.52 % (2834800)Time elapsed: 0.005 s
% 1.55/0.52 % (2834800)Peak memory usage: 11 MB
% 1.55/0.52 % (2834800)Instructions burned: 24 (million)
% 1.55/0.52 % (2834798)Instruction limit reached!
% 1.55/0.52 % (2834798)------------------------------
% 1.55/0.52 % (2834798)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.55/0.52 % (2834798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.55/0.52 % (2834798)CaDiCaL version: 2.1.3
% 1.55/0.52 % (2834798)Termination reason: Instruction limit
% 1.55/0.52 % (2834798)Termination phase: Property scanning
% 1.55/0.52 % (2834798)Time elapsed: 0.003 s
% 1.55/0.52 % (2834798)Peak memory usage: 10 MB
% 1.55/0.52 % (2834798)Instructions burned: 7 (million)
% 1.55/0.52 % (2834794)Instruction limit reached!
% 1.55/0.52 % (2834794)------------------------------
% 1.55/0.52 % (2834794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.55/0.52 % (2834794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.55/0.52 % (2834794)CaDiCaL version: 2.1.3
% 1.55/0.52 % (2834794)Termination reason: Instruction limit
% 1.55/0.52 % (2834794)Termination phase: Saturation
% 1.55/0.52 % (2834794)Time elapsed: 0.016 s
% 1.55/0.52 % (2834794)Peak memory usage: 12 MB
% 1.55/0.52 % (2834794)Instructions burned: 31 (million)
% 1.55/0.52 % (2834805)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=1815556324:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 1.55/0.52 % (2834812)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=762218412:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/143Mi)
% 1.55/0.52 % (2834809)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=2222979770:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 1.55/0.52 % (2834789)Instruction limit reached!
% 1.55/0.52 % (2834789)------------------------------
% 1.55/0.52 % (2834789)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.55/0.52 % (2834789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.55/0.52 % (2834789)CaDiCaL version: 2.1.3
% 1.55/0.52 % (2834789)Termination reason: Instruction limit
% 1.55/0.52 % (2834789)Termination phase: Saturation
% 1.55/0.52 % (2834789)Time elapsed: 0.032 s
% 1.55/0.52 % (2834789)Peak memory usage: 12 MB
% 1.55/0.52 % (2834789)Instructions burned: 61 (million)
% 1.55/0.52 % (2834805)Instruction limit reached!
% 1.55/0.52 % (2834805)------------------------------
% 1.55/0.52 % (2834805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.55/0.52 % (2834805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.55/0.52 % (2834805)CaDiCaL version: 2.1.3
% 1.55/0.52 % (2834805)Termination reason: Instruction limit
% 1.55/0.52 % (2834805)Termination phase: Saturation
% 1.55/0.52 % (2834805)Time elapsed: 0.009 s
% 1.55/0.52 % (2834805)Peak memory usage: 11 MB
% 1.55/0.52 % (2834805)Instructions burned: 21 (million)
% 1.55/0.52 % (2834813)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=337251754:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/193Mi)
% 1.55/0.52 % (2834814)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=983018119:i=42:hud=10:rtra=on_2998 on theBenchmark for (2998ds/42Mi)
% 1.55/0.52 % (2834818)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.55/0.52 % (2834819)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=2623569302:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/181Mi)
% 1.55/0.52 % (2834813)Refutation not found, incomplete strategy
% 1.55/0.52 % (2834813)------------------------------
% 1.55/0.52 % (2834813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.55/0.52 % (2834818)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=4242299208:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2998 on theBenchmark for (2998ds/7Mi)
% 2.21/0.60 % (2834813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.21/0.60 % (2834813)CaDiCaL version: 2.1.3
% 2.21/0.60 % (2834813)Termination reason: Refutation not found, incomplete strategy
% 2.21/0.60 % (2834813)Time elapsed: 0.018 s
% 2.21/0.60 % (2834813)Peak memory usage: 12 MB
% 2.21/0.60 % (2834813)Instructions burned: 38 (million)
% 2.21/0.60 % (2834813)------------------------------
% 2.21/0.60 % (2834813)------------------------------
% 2.21/0.60 % (2834814)Instruction limit reached!
% 2.21/0.60 % (2834814)------------------------------
% 2.21/0.60 % (2834814)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.21/0.60 % (2834814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.21/0.60 % (2834814)CaDiCaL version: 2.1.3
% 2.21/0.60 % (2834814)Termination reason: Instruction limit
% 2.21/0.60 % (2834814)Termination phase: Saturation
% 2.21/0.60 % (2834814)Time elapsed: 0.018 s
% 2.21/0.60 % (2834814)Peak memory usage: 11 MB
% 2.21/0.60 % (2834814)Instructions burned: 42 (million)
% 2.21/0.60 % (2834818)Instruction limit reached!
% 2.21/0.60 % (2834818)------------------------------
% 2.21/0.60 % (2834818)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.21/0.60 % (2834818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.21/0.60 % (2834818)CaDiCaL version: 2.1.3
% 2.21/0.60 % (2834818)Termination reason: Instruction limit
% 2.21/0.60 % (2834818)Termination phase: Property scanning
% 2.21/0.60 % (2834818)Time elapsed: 0.005 s
% 2.21/0.60 % (2834818)Peak memory usage: 10 MB
% 2.21/0.60 % (2834818)Instructions burned: 10 (million)
% 2.21/0.60 % (2834812)Instruction limit reached!
% 2.21/0.60 % (2834812)------------------------------
% 2.21/0.60 % (2834812)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.21/0.60 % (2834812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.21/0.60 % (2834812)CaDiCaL version: 2.1.3
% 2.21/0.60 % (2834812)Termination reason: Instruction limit
% 2.21/0.60 % (2834812)Termination phase: Saturation
% 2.21/0.60 % (2834812)Time elapsed: 0.037 s
% 2.21/0.60 % (2834812)Peak memory usage: 13 MB
% 2.21/0.60 % (2834812)Instructions burned: 144 (million)
% 2.21/0.60 % (2834827)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=3530698446:i=19:add=on:rtra=on_2998 on theBenchmark for (2998ds/19Mi)
% 2.21/0.60 % (2834819)Refutation not found, incomplete strategy
% 2.21/0.60 % (2834819)------------------------------
% 2.21/0.60 % (2834819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.21/0.60 % (2834819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.21/0.60 % (2834819)CaDiCaL version: 2.1.3
% 2.21/0.60 % (2834819)Termination reason: Refutation not found, incomplete strategy
% 2.21/0.60 % (2834819)Time elapsed: 0.022 s
% 2.21/0.60 % (2834825)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 2.21/0.60 % (2834819)Peak memory usage: 12 MB
% 2.21/0.60 % (2834819)Instructions burned: 47 (million)
% 2.21/0.60 % (2834824)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=4270190667: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)
% 2.21/0.60 % (2834819)------------------------------
% 2.21/0.60 % (2834819)------------------------------
% 2.21/0.60 % (2834827)Instruction limit reached!
% 2.21/0.60 % (2834827)------------------------------
% 2.21/0.60 % (2834827)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.21/0.60 % (2834827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.21/0.60 % (2834827)CaDiCaL version: 2.1.3
% 2.21/0.60 % (2834827)Termination reason: Instruction limit
% 2.21/0.60 % (2834827)Termination phase: Property scanning
% 2.21/0.60 % (2834827)Time elapsed: 0.004 s
% 2.21/0.60 % (2834827)Peak memory usage: 10 MB
% 2.21/0.60 % (2834827)Instructions burned: 19 (million)
% 2.21/0.60 % (2834825)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=4143498509:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2998 on theBenchmark for (2998ds/6Mi)
% 2.21/0.60 % (2834826)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=2685919737:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2998 on theBenchmark for (2998ds/22Mi)
% 2.67/0.67 % (2834825)Instruction limit reached!
% 2.67/0.67 % (2834825)------------------------------
% 2.67/0.67 % (2834825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.67/0.67 % (2834825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.67/0.67 % (2834825)CaDiCaL version: 2.1.3
% 2.67/0.67 % (2834825)Termination reason: Instruction limit
% 2.67/0.67 % (2834825)Termination phase: Property scanning
% 2.67/0.67 % (2834825)Time elapsed: 0.003 s
% 2.67/0.67 % (2834825)Peak memory usage: 9 MB
% 2.67/0.67 % (2834825)Instructions burned: 7 (million)
% 2.67/0.67 % (2834824)Refutation not found, incomplete strategy
% 2.67/0.67 % (2834824)------------------------------
% 2.67/0.67 % (2834824)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.67/0.67 % (2834824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.67/0.67 % (2834824)CaDiCaL version: 2.1.3
% 2.67/0.67 % (2834824)Termination reason: Refutation not found, incomplete strategy
% 2.67/0.67 % (2834824)Time elapsed: 0.012 s
% 2.67/0.67 % (2834824)Peak memory usage: 12 MB
% 2.67/0.67 % (2834824)Instructions burned: 26 (million)
% 2.67/0.67 % (2834831)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=1586073327: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)
% 2.67/0.67 % (2834824)------------------------------
% 2.67/0.67 % (2834824)------------------------------
% 2.67/0.67 % (2834826)Instruction limit reached!
% 2.67/0.67 % (2834826)------------------------------
% 2.67/0.67 % (2834826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.67/0.67 % (2834826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.67/0.67 % (2834826)CaDiCaL version: 2.1.3
% 2.67/0.67 % (2834826)Termination reason: Instruction limit
% 2.67/0.67 % (2834826)Termination phase: Property scanning
% 2.67/0.67 % (2834826)Time elapsed: 0.010 s
% 2.67/0.67 % (2834826)Peak memory usage: 11 MB
% 2.67/0.67 % (2834826)Instructions burned: 25 (million)
% 2.67/0.67 % (2834830)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=1677939930:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/316Mi)
% 2.67/0.67 % (2834834)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=1716083588: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)
% 2.67/0.67 % (2834836)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=4200354587:i=480:rtra=on_2997 on theBenchmark for (2997ds/480Mi)
% 2.67/0.67 % (2834837)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=188075129: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)
% 2.67/0.67 % (2834836)Refutation not found, incomplete strategy
% 2.67/0.67 % (2834836)------------------------------
% 2.67/0.67 % (2834836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.67/0.67 % (2834836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.67/0.67 % (2834836)CaDiCaL version: 2.1.3
% 2.67/0.67 % (2834836)Termination reason: Refutation not found, incomplete strategy
% 2.67/0.67 % (2834836)Time elapsed: 0.009 s
% 2.67/0.67 % (2834836)Peak memory usage: 12 MB
% 2.67/0.67 % (2834836)Instructions burned: 21 (million)
% 2.67/0.67 % (2834836)------------------------------
% 2.67/0.67 % (2834836)------------------------------
% 2.67/0.67 % (2834837)Instruction limit reached!
% 2.67/0.67 % (2834837)------------------------------
% 2.67/0.67 % (2834837)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.67/0.67 % (2834837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.67/0.67 % (2834837)CaDiCaL version: 2.1.3
% 2.67/0.67 % (2834837)Termination reason: Instruction limit
% 2.67/0.67 % (2834837)Termination phase: Property scanning
% 2.67/0.67 % (2834837)Time elapsed: 0.009 s
% 2.67/0.67 % (2834837)Peak memory usage: 10 MB
% 2.67/0.67 % (2834837)Instructions burned: 21 (million)
% 2.67/0.67 % (2834834)Instruction limit reached!
% 2.67/0.67 % (2834834)------------------------------
% 3.05/0.73 % (2834834)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.05/0.73 % (2834834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.05/0.73 % (2834834)CaDiCaL version: 2.1.3
% 3.05/0.73 % (2834834)Termination reason: Instruction limit
% 3.05/0.73 % (2834834)Termination phase: Saturation
% 3.05/0.73 % (2834834)Time elapsed: 0.020 s
% 3.05/0.73 % (2834834)Peak memory usage: 12 MB
% 3.05/0.73 % (2834834)Instructions burned: 47 (million)
% 3.05/0.73 % (2834842)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 3.05/0.73 % (2834842)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=908749772:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/200Mi)
% 3.05/0.73 % (2834843)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=262714348:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2997 on theBenchmark for (2997ds/13Mi)
% 3.05/0.73 % (2834844)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=1891104784:i=66:s2at=3:nm=2:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/66Mi)
% 3.05/0.73 % (2834843)Instruction limit reached!
% 3.05/0.73 % (2834843)------------------------------
% 3.05/0.73 % (2834843)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.05/0.73 % (2834843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.05/0.73 % (2834843)CaDiCaL version: 2.1.3
% 3.05/0.73 % (2834843)Termination reason: Instruction limit
% 3.05/0.73 % (2834843)Termination phase: Property scanning
% 3.05/0.73 % (2834843)Time elapsed: 0.007 s
% 3.05/0.73 % (2834843)Peak memory usage: 10 MB
% 3.05/0.73 % (2834843)Instructions burned: 16 (million)
% 3.05/0.73 % (2834848)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=1593336467:i=51:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/51Mi)
% 3.05/0.73 % (2834844)Instruction limit reached!
% 3.05/0.73 % (2834844)------------------------------
% 3.05/0.73 % (2834844)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.05/0.73 % (2834844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.05/0.73 % (2834844)CaDiCaL version: 2.1.3
% 3.05/0.73 % (2834844)Termination reason: Instruction limit
% 3.05/0.73 % (2834844)Termination phase: Saturation
% 3.05/0.73 % (2834844)Time elapsed: 0.029 s
% 3.05/0.73 % (2834844)Peak memory usage: 12 MB
% 3.05/0.73 % (2834844)Instructions burned: 67 (million)
% 3.05/0.73 % (2834848)Refutation not found, incomplete strategy
% 3.05/0.73 % (2834848)------------------------------
% 3.05/0.73 % (2834848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.05/0.73 % (2834848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.05/0.73 % (2834848)CaDiCaL version: 2.1.3
% 3.05/0.73 % (2834848)Termination reason: Refutation not found, incomplete strategy
% 3.05/0.73 % (2834848)Time elapsed: 0.021 s
% 3.05/0.73 % (2834848)Peak memory usage: 12 MB
% 3.05/0.73 % (2834848)Instructions burned: 49 (million)
% 3.05/0.73 % (2834848)------------------------------
% 3.05/0.73 % (2834848)------------------------------
% 3.05/0.73 % (2834850)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=3262409846:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/31Mi)
% 3.05/0.73 % (2834850)Instruction limit reached!
% 3.05/0.73 % (2834850)------------------------------
% 3.05/0.73 % (2834850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.05/0.73 % (2834850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.05/0.73 % (2834850)CaDiCaL version: 2.1.3
% 3.05/0.73 % (2834850)Termination reason: Instruction limit
% 3.05/0.73 % (2834850)Termination phase: Saturation
% 3.05/0.73 % (2834850)Time elapsed: 0.013 s
% 3.05/0.73 % (2834850)Peak memory usage: 12 MB
% 3.05/0.73 % (2834850)Instructions burned: 31 (million)
% 3.05/0.73 % (2834851)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=12989671:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2996 on theBenchmark for (2996ds/137Mi)
% 3.05/0.73 % (2834706)Instruction limit reached!
% 3.05/0.73 % (2834706)------------------------------
% 3.05/0.73 % (2834706)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.05/0.73 % (2834706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.05/0.78 % (2834706)CaDiCaL version: 2.1.3
% 3.05/0.78 % (2834706)Termination reason: Instruction limit
% 3.05/0.78 % (2834706)Termination phase: Saturation
% 3.05/0.78 % (2834706)Time elapsed: 0.318 s
% 3.05/0.78 % (2834706)Peak memory usage: 15 MB
% 3.05/0.78 % (2834706)Instructions burned: 635 (million)
% 3.05/0.78 % (2834853)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=1190428662:cond=on:i=34:hud=10:nm=10:rtra=on_2996 on theBenchmark for (2996ds/34Mi)
% 3.05/0.78 % (2834842)Instruction limit reached!
% 3.05/0.78 % (2834842)------------------------------
% 3.05/0.78 % (2834842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.05/0.78 % (2834842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.05/0.78 % (2834842)CaDiCaL version: 2.1.3
% 3.05/0.78 % (2834842)Termination reason: Instruction limit
% 3.05/0.78 % (2834842)Termination phase: Saturation
% 3.05/0.78 % (2834842)Time elapsed: 0.085 s
% 3.05/0.78 % (2834842)Peak memory usage: 12 MB
% 3.05/0.78 % (2834842)Instructions burned: 201 (million)
% 3.05/0.78 % (2834855)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=1897194654:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2996 on theBenchmark for (2996ds/67Mi)
% 3.05/0.78 % (2834853)Instruction limit reached!
% 3.05/0.78 % (2834853)------------------------------
% 3.05/0.78 % (2834853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.05/0.78 % (2834853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.05/0.78 % (2834853)CaDiCaL version: 2.1.3
% 3.05/0.78 % (2834853)Termination reason: Instruction limit
% 3.05/0.78 % (2834853)Termination phase: Saturation
% 3.05/0.78 % (2834853)Time elapsed: 0.015 s
% 3.05/0.78 % (2834853)Peak memory usage: 11 MB
% 3.05/0.78 % (2834853)Instructions burned: 36 (million)
% 3.05/0.78 % (2834857)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 3.05/0.78 % (2834857)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=1562289494:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2996 on theBenchmark for (2996ds/180Mi)
% 3.05/0.78 % (2834855)Refutation not found, incomplete strategy
% 3.05/0.78 % (2834855)------------------------------
% 3.05/0.78 % (2834855)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.05/0.78 % (2834855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.05/0.78 % (2834855)CaDiCaL version: 2.1.3
% 3.05/0.78 % (2834855)Termination reason: Refutation not found, incomplete strategy
% 3.05/0.78 % (2834855)Time elapsed: 0.021 s
% 3.05/0.78 % (2834855)Peak memory usage: 12 MB
% 3.05/0.78 % (2834855)Instructions burned: 50 (million)
% 3.05/0.78 % (2834855)------------------------------
% 3.05/0.78 % (2834855)------------------------------
% 3.05/0.78 % (2834859)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=2403076924:st=2:i=246:sd=3:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/246Mi)
% 3.05/0.78 % (2834830)Instruction limit reached!
% 3.05/0.78 % (2834830)------------------------------
% 3.05/0.78 % (2834830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.05/0.78 % (2834830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.05/0.78 % (2834830)CaDiCaL version: 2.1.3
% 3.05/0.78 % (2834830)Termination reason: Instruction limit
% 3.05/0.78 % (2834830)Termination phase: Saturation
% 3.05/0.78 % (2834830)Time elapsed: 0.170 s
% 3.05/0.78 % (2834830)Peak memory usage: 15 MB
% 3.05/0.78 % (2834830)Instructions burned: 316 (million)
% 3.05/0.78 % (2834861)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=636830196:cond=on:i=96:bd=all:rtra=on_2996 on theBenchmark for (2996ds/96Mi)
% 3.05/0.78 % (2834859)Refutation not found, incomplete strategy
% 3.05/0.78 % (2834859)------------------------------
% 3.05/0.78 % (2834859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.05/0.78 % (2834859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.05/0.78 % (2834859)CaDiCaL version: 2.1.3
% 3.05/0.78 % (2834859)Termination reason: Refutation not found, incomplete strategy
% 3.05/0.78 % (2834859)Time elapsed: 0.017 s
% 3.05/0.78 % (2834859)Peak memory usage: 12 MB
% 3.05/0.78 % (2834859)Instructions burned: 36 (million)
% 3.05/0.78 % (2834851)Instruction limit reached!
% 3.05/0.78 % (2834851)------------------------------
% 3.05/0.78 % (2834851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.65/0.84 % (2834851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.65/0.84 % (2834851)CaDiCaL version: 2.1.3
% 3.65/0.84 % (2834851)Termination reason: Instruction limit
% 3.65/0.84 % (2834851)Termination phase: Saturation
% 3.65/0.84 % (2834851)Time elapsed: 0.070 s
% 3.65/0.84 % (2834851)Peak memory usage: 13 MB
% 3.65/0.84 % (2834851)Instructions burned: 137 (million)
% 3.65/0.84 % (2834859)------------------------------
% 3.65/0.84 % (2834859)------------------------------
% 3.65/0.84 % (2834863)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=3753186535:i=427:sd=1:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/427Mi)
% 3.65/0.84 % (2834865)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=4221315485:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/874Mi)
% 3.65/0.84 % (2834866)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=2539715126:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/515Mi)
% 3.65/0.84 % (2834863)Refutation not found, incomplete strategy
% 3.65/0.84 % (2834863)------------------------------
% 3.65/0.84 % (2834863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.65/0.84 % (2834863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.65/0.84 % (2834863)CaDiCaL version: 2.1.3
% 3.65/0.84 % (2834863)Termination reason: Refutation not found, incomplete strategy
% 3.65/0.84 % (2834863)Time elapsed: 0.008 s
% 3.65/0.84 % (2834863)Peak memory usage: 12 MB
% 3.65/0.84 % (2834863)Instructions burned: 17 (million)
% 3.65/0.84 % (2834863)------------------------------
% 3.65/0.84 % (2834863)------------------------------
% 3.65/0.84 % (2834865)Refutation not found, incomplete strategy
% 3.65/0.84 % (2834865)------------------------------
% 3.65/0.84 % (2834865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.65/0.84 % (2834865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.65/0.84 % (2834865)CaDiCaL version: 2.1.3
% 3.65/0.84 % (2834865)Termination reason: Refutation not found, incomplete strategy
% 3.65/0.84 % (2834865)Time elapsed: 0.018 s
% 3.65/0.84 % (2834865)Peak memory usage: 12 MB
% 3.65/0.84 % (2834865)Instructions burned: 38 (million)
% 3.65/0.84 % (2834865)------------------------------
% 3.65/0.84 % (2834865)------------------------------
% 3.65/0.84 % (2834870)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=2850031290:st=1.5:i=130:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/130Mi)
% 3.65/0.84 % (2834861)Instruction limit reached!
% 3.65/0.84 % (2834861)------------------------------
% 3.65/0.84 % (2834861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.65/0.84 % (2834861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.65/0.84 % (2834861)CaDiCaL version: 2.1.3
% 3.65/0.84 % (2834861)Termination reason: Instruction limit
% 3.65/0.84 % (2834861)Termination phase: Saturation
% 3.65/0.84 % (2834861)Time elapsed: 0.045 s
% 3.65/0.84 % (2834861)Peak memory usage: 13 MB
% 3.65/0.84 % (2834861)Instructions burned: 97 (million)
% 3.65/0.84 % (2834857)Instruction limit reached!
% 3.65/0.84 % (2834857)------------------------------
% 3.65/0.84 % (2834857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.65/0.84 % (2834857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.65/0.84 % (2834857)CaDiCaL version: 2.1.3
% 3.65/0.84 % (2834857)Termination reason: Instruction limit
% 3.65/0.84 % (2834857)Termination phase: Saturation
% 3.65/0.84 % (2834857)Time elapsed: 0.084 s
% 3.65/0.84 % (2834857)Peak memory usage: 13 MB
% 3.65/0.84 % (2834857)Instructions burned: 181 (million)
% 3.65/0.84 % (2834871)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=1614538819:i=44:ep=R:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/44Mi)
% 3.65/0.84 % (2834831)Instruction limit reached!
% 3.65/0.84 % (2834831)------------------------------
% 3.65/0.84 % (2834831)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.65/0.84 % (2834873)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=2736907257:s2a=on:i=571:nm=16:rtra=on_2995 on theBenchmark for (2995ds/571Mi)
% 3.65/0.84 % (2834831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.65/0.84 % (2834831)CaDiCaL version: 2.1.3
% 3.65/0.84 % (2834831)Termination reason: Instruction limit
% 3.65/0.84 % (2834831)Termination phase: Saturation
% 3.97/0.94 % (2834831)Time elapsed: 0.245 s
% 3.97/0.94 % (2834831)Peak memory usage: 17 MB
% 3.97/0.94 % (2834831)Instructions burned: 855 (million)
% 3.97/0.94 % (2834870)Refutation not found, incomplete strategy
% 3.97/0.94 % (2834870)------------------------------
% 3.97/0.94 % (2834870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.97/0.94 % (2834870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.97/0.94 % (2834870)CaDiCaL version: 2.1.3
% 3.97/0.94 % (2834870)Termination reason: Refutation not found, incomplete strategy
% 3.97/0.94 % (2834870)Time elapsed: 0.024 s
% 3.97/0.94 % (2834870)Peak memory usage: 12 MB
% 3.97/0.94 % (2834870)Instructions burned: 48 (million)
% 3.97/0.94 % (2834870)------------------------------
% 3.97/0.94 % (2834870)------------------------------
% 3.97/0.94 % (2834874)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=3315363008:i=450:rtra=on:ixr=off:ntd=on_2995 on theBenchmark for (2995ds/450Mi)
% 3.97/0.94 % (2834877)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=2107999524:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/95Mi)
% 3.97/0.94 % (2834873)Refutation not found, incomplete strategy
% 3.97/0.94 % (2834873)------------------------------
% 3.97/0.94 % (2834873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.97/0.94 % (2834873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.97/0.94 % (2834873)CaDiCaL version: 2.1.3
% 3.97/0.94 % (2834873)Termination reason: Refutation not found, incomplete strategy
% 3.97/0.94 % (2834873)Time elapsed: 0.010 s
% 3.97/0.94 % (2834873)Peak memory usage: 12 MB
% 3.97/0.94 % (2834873)Instructions burned: 22 (million)
% 3.97/0.94 % (2834873)------------------------------
% 3.97/0.94 % (2834873)------------------------------
% 3.97/0.94 % (2834871)Instruction limit reached!
% 3.97/0.94 % (2834871)------------------------------
% 3.97/0.94 % (2834871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.97/0.94 % (2834871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.97/0.94 % (2834871)CaDiCaL version: 2.1.3
% 3.97/0.94 % (2834871)Termination reason: Instruction limit
% 3.97/0.94 % (2834871)Termination phase: Saturation
% 3.97/0.94 % (2834871)Time elapsed: 0.019 s
% 3.97/0.94 % (2834871)Peak memory usage: 12 MB
% 3.97/0.94 % (2834871)Instructions burned: 46 (million)
% 3.97/0.94 % (2834878)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=40790110:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2995 on theBenchmark for (2995ds/65Mi)
% 3.97/0.94 % (2834881)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=2695288441: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_2995 on theBenchmark for (2995ds/105Mi)
% 3.97/0.94 % (2834877)Instruction limit reached!
% 3.97/0.94 % (2834877)------------------------------
% 3.97/0.94 % (2834877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.97/0.94 % (2834877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.97/0.94 % (2834877)CaDiCaL version: 2.1.3
% 3.97/0.94 % (2834877)Termination reason: Instruction limit
% 3.97/0.94 % (2834877)Termination phase: Saturation
% 3.97/0.94 % (2834877)Time elapsed: 0.024 s
% 3.97/0.94 % (2834877)Peak memory usage: 12 MB
% 3.97/0.94 % (2834877)Instructions burned: 100 (million)
% 3.97/0.94 % (2834882)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=3743735217:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2995 on theBenchmark for (2995ds/5755Mi)
% 3.97/0.94 % (2834886)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=4236703517:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/375Mi)
% 3.97/0.94 % (2834882)Refutation not found, incomplete strategy
% 3.97/0.94 % (2834882)------------------------------
% 3.97/0.94 % (2834882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.97/0.94 % (2834882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.97/0.94 % (2834882)CaDiCaL version: 2.1.3
% 3.97/0.99 % (2834882)Termination reason: Refutation not found, incomplete strategy
% 3.97/0.99 % (2834882)Time elapsed: 0.013 s
% 3.97/0.99 % (2834882)Peak memory usage: 13 MB
% 3.97/0.99 % (2834882)Instructions burned: 28 (million)
% 3.97/0.99 % (2834882)------------------------------
% 3.97/0.99 % (2834882)------------------------------
% 3.97/0.99 % (2834886)Refutation not found, incomplete strategy
% 3.97/0.99 % (2834886)------------------------------
% 3.97/0.99 % (2834886)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.97/0.99 % (2834886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.97/0.99 % (2834886)CaDiCaL version: 2.1.3
% 3.97/0.99 % (2834886)Termination reason: Refutation not found, incomplete strategy
% 3.97/0.99 % (2834886)Time elapsed: 0.008 s
% 3.97/0.99 % (2834886)Peak memory usage: 12 MB
% 3.97/0.99 % (2834886)Instructions burned: 32 (million)
% 3.97/0.99 % (2834886)------------------------------
% 3.97/0.99 % (2834886)------------------------------
% 3.97/0.99 % (2834878)Instruction limit reached!
% 3.97/0.99 % (2834878)------------------------------
% 3.97/0.99 % (2834878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.97/0.99 % (2834878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.97/0.99 % (2834878)CaDiCaL version: 2.1.3
% 3.97/0.99 % (2834878)Termination reason: Instruction limit
% 3.97/0.99 % (2834878)Termination phase: Saturation
% 3.97/0.99 % (2834878)Time elapsed: 0.030 s
% 3.97/0.99 % (2834878)Peak memory usage: 12 MB
% 3.97/0.99 % (2834878)Instructions burned: 65 (million)
% 3.97/0.99 % (2834889)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=554030892:cond=on:i=34:hud=10:nm=10:rtra=on_2994 on theBenchmark for (2994ds/34Mi)
% 3.97/0.99 % (2834888)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=2339117819:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2994 on theBenchmark for (2994ds/495Mi)
% 3.97/0.99 % (2834889)Instruction limit reached!
% 3.97/0.99 % (2834889)------------------------------
% 3.97/0.99 % (2834889)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.97/0.99 % (2834889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.97/0.99 % (2834889)CaDiCaL version: 2.1.3
% 3.97/0.99 % (2834889)Termination reason: Instruction limit
% 3.97/0.99 % (2834889)Termination phase: Saturation
% 3.97/0.99 % (2834889)Time elapsed: 0.008 s
% 3.97/0.99 % (2834889)Peak memory usage: 11 MB
% 3.97/0.99 % (2834889)Instructions burned: 37 (million)
% 3.97/0.99 % (2834890)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=3289466846:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2994 on theBenchmark for (2994ds/91Mi)
% 3.97/0.99 % (2834881)Instruction limit reached!
% 3.97/0.99 % (2834881)------------------------------
% 3.97/0.99 % (2834881)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.97/0.99 % (2834881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.97/0.99 % (2834881)CaDiCaL version: 2.1.3
% 3.97/0.99 % (2834881)Termination reason: Instruction limit
% 3.97/0.99 % (2834881)Termination phase: Saturation
% 3.97/0.99 % (2834881)Time elapsed: 0.049 s
% 3.97/0.99 % (2834881)Peak memory usage: 13 MB
% 3.97/0.99 % (2834881)Instructions burned: 105 (million)
% 3.97/0.99 % (2834893)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=1532255410:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2994 on theBenchmark for (2994ds/66Mi)
% 3.97/0.99 % (2834893)Refutation not found, incomplete strategy
% 3.97/0.99 % (2834893)------------------------------
% 3.97/0.99 % (2834893)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.97/0.99 % (2834893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.97/0.99 % (2834893)CaDiCaL version: 2.1.3
% 3.97/0.99 % (2834893)Termination reason: Refutation not found, incomplete strategy
% 3.97/0.99 % (2834893)Time elapsed: 0.005 s
% 3.97/0.99 % (2834893)Peak memory usage: 12 MB
% 3.97/0.99 % (2834893)Instructions burned: 24 (million)
% 3.97/0.99 % (2834893)------------------------------
% 3.97/0.99 % (2834893)------------------------------
% 3.97/0.99 % (2834895)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=2533014532:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2994 on theBenchmark for (2994ds/22Mi)
% 3.97/0.99 % (2834897)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=244962081:i=338:bd=all:ins=4:rtra=on_2994 on theBenchmark for (2994ds/338Mi)
% 3.97/0.99 % (2834895)Instruction limit reached!
% 3.97/0.99 % (2834895)------------------------------
% 3.97/0.99 % (2834895)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.97/0.99 % (2834895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.97/0.99 % (2834895)CaDiCaL version: 2.1.3
% 3.97/0.99 % (2834895)Termination reason: Instruction limit
% 3.97/0.99 % (2834895)Termination phase: Property scanning
% 3.97/0.99 % (2834895)Time elapsed: 0.009 s
% 3.97/0.99 % (2834895)Peak memory usage: 10 MB
% 3.97/0.99 % (2834895)Instructions burned: 23 (million)
% 3.97/0.99 % (2834890)Instruction limit reached!
% 3.97/0.99 % (2834890)------------------------------
% 3.97/0.99 % (2834890)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.97/0.99 % (2834890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.97/0.99 % (2834890)CaDiCaL version: 2.1.3
% 3.97/0.99 % (2834890)Termination reason: Instruction limit
% 3.97/0.99 % (2834890)Termination phase: Saturation
% 3.97/0.99 % (2834890)Time elapsed: 0.042 s
% 3.97/0.99 % (2834890)Peak memory usage: 12 MB
% 3.97/0.99 % (2834890)Instructions burned: 91 (million)
% 3.97/0.99 % (2834900)lrs+10_1_sil=128000:si=on:urr=on:random_seed=3963974948:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2994 on theBenchmark for (2994ds/28Mi)
% 3.97/0.99 % (2834901)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 3.97/0.99 % (2834901)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=1948987603:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2994 on theBenchmark for (2994ds/137Mi)
% 3.97/0.99 % (2834900)Instruction limit reached!
% 3.97/0.99 % (2834900)------------------------------
% 3.97/0.99 % (2834900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.97/0.99 % (2834900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.97/0.99 % (2834900)CaDiCaL version: 2.1.3
% 3.97/0.99 % (2834900)Termination reason: Instruction limit
% 3.97/0.99 % (2834900)Termination phase: Saturation
% 3.97/0.99 % (2834900)Time elapsed: 0.011 s
% 3.97/0.99 % (2834900)Peak memory usage: 11 MB
% 3.97/0.99 % (2834900)Instructions burned: 28 (million)
% 3.97/0.99 % (2834904)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=2252935533:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2993 on theBenchmark for (2993ds/340Mi)
% 3.97/0.99 % (2834866)Instruction limit reached!
% 3.97/0.99 % (2834866)------------------------------
% 3.97/0.99 % (2834866)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.97/0.99 % (2834866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.97/0.99 % (2834866)CaDiCaL version: 2.1.3
% 3.97/0.99 % (2834866)Termination reason: Instruction limit
% 3.97/0.99 % (2834866)Termination phase: Saturation
% 3.97/0.99 % (2834866)Time elapsed: 0.224 s
% 3.97/0.99 % (2834866)Peak memory usage: 13 MB
% 3.97/0.99 % (2834866)Instructions burned: 517 (million)
% 3.97/0.99 % (2834901)Instruction limit reached!
% 3.97/0.99 % (2834901)------------------------------
% 3.97/0.99 % (2834901)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.97/0.99 % (2834901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.97/0.99 % (2834901)CaDiCaL version: 2.1.3
% 3.97/0.99 % (2834901)Termination reason: Instruction limit
% 3.97/0.99 % (2834901)Termination phase: Saturation
% 3.97/0.99 % (2834901)Time elapsed: 0.064 s
% 3.97/0.99 % (2834901)Peak memory usage: 13 MB
% 3.97/0.99 % (2834901)Instructions burned: 139 (million)
% 3.97/0.99 % (2834906)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=3444382806:i=227:sd=1:bd=all:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/227Mi)
% 3.97/0.99 % (2834906)Refutation not found, incomplete strategy
% 3.97/0.99 % (2834906)------------------------------
% 3.97/0.99 % (2834906)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.97/0.99 % (2834906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.97/0.99 % (2834906)CaDiCaL version: 2.1.3
% 3.97/0.99 % (2834906)Termination reason: Refutation not found, incomplete strategy
% 3.97/0.99 % (2834906)Time elapsed: 0.008 s
% 3.97/0.99 % (2834906)Peak memory usage: 12 MB
% 3.97/0.99 % (2834906)Instructions burned: 18 (million)
% 3.97/0.99 % (2834906)------------------------------
% 3.97/0.99 % (2834906)------------------------------
% 3.97/0.99 % (2834907)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 3.97/0.99 % (2834907)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=3807859795:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/373Mi)
% 3.97/0.99 % (2834874)Instruction limit reached!
% 3.97/0.99 % (2834874)------------------------------
% 3.97/0.99 % (2834874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.97/0.99 % (2834874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.97/0.99 % (2834874)CaDiCaL version: 2.1.3
% 3.97/0.99 % (2834874)Termination reason: Instruction limit
% 3.97/0.99 % (2834874)Termination phase: Saturation
% 3.97/0.99 % (2834874)Time elapsed: 0.209 s
% 3.97/0.99 % (2834874)Peak memory usage: 13 MB
% 3.97/0.99 % (2834874)Instructions burned: 451 (million)
% 3.97/0.99 % (2834909)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=3386845125:i=116:ep=RSTC:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/116Mi)
% 3.97/0.99 % (2834911)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=3119718557:i=575:rtra=on_2993 on theBenchmark for (2993ds/575Mi)
% 3.97/0.99 % (2834904) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2834698-2834904"...
% 3.97/0.99 % (2834904)...printing done.
% 3.97/0.99 % (2834904)Refutation found. Thanks to Tanya!
% 3.97/0.99 % SZS status Theorem for theBenchmark
% 3.97/0.99 % SZS output start Proof for theBenchmark
% 3.97/0.99 thf(type_def_5, type, mu: $tType).
% 3.97/0.99 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 3.97/0.99 thf(func_def_0, type, meq_ind: (mu > mu > $i > $o)).
% 3.97/0.99 thf(func_def_1, type, meq_prop: (($i > $o) > ($i > $o) > $i > $o)).
% 3.97/0.99 thf(func_def_3, type, mnot: (($i > $o) > $i > $o)).
% 3.97/0.99 thf(func_def_4, type, mor: (($i > $o) > ($i > $o) > $i > $o)).
% 3.97/0.99 thf(func_def_5, type, mand: (($i > $o) > ($i > $o) > $i > $o)).
% 3.97/0.99 thf(func_def_6, type, mimplies: (($i > $o) > ($i > $o) > $i > $o)).
% 3.97/0.99 thf(func_def_7, type, mimplied: (($i > $o) > ($i > $o) > $i > $o)).
% 3.97/0.99 thf(func_def_8, type, mequiv: (($i > $o) > ($i > $o) > $i > $o)).
% 3.97/0.99 thf(func_def_9, type, mxor: (($i > $o) > ($i > $o) > $i > $o)).
% 3.97/0.99 thf(func_def_10, type, mforall_ind: ((mu > $i > $o) > $i > $o)).
% 3.97/0.99 thf(func_def_11, type, mforall_prop: ((($i > $o) > $i > $o) > $i > $o)).
% 3.97/0.99 thf(func_def_12, type, mexists_ind: ((mu > $i > $o) > $i > $o)).
% 3.97/0.99 thf(func_def_13, type, mexists_prop: ((($i > $o) > $i > $o) > $i > $o)).
% 3.97/0.99 thf(func_def_14, type, mtrue: ($i > $o)).
% 3.97/0.99 thf(func_def_15, type, mfalse: ($i > $o)).
% 3.97/0.99 thf(func_def_16, type, mbox: (($i > $i > $o) > ($i > $o) > $i > $o)).
% 3.97/0.99 thf(func_def_17, type, mdia: (($i > $i > $o) > ($i > $o) > $i > $o)).
% 3.97/0.99 thf(func_def_18, type, mreflexive: (($i > $i > $o) > $o)).
% 3.97/0.99 thf(func_def_19, type, msymmetric: (($i > $i > $o) > $o)).
% 3.97/0.99 thf(func_def_20, type, mserial: (($i > $i > $o) > $o)).
% 3.97/0.99 thf(func_def_21, type, mtransitive: (($i > $i > $o) > $o)).
% 3.97/0.99 thf(func_def_22, type, meuclidean: (($i > $i > $o) > $o)).
% 3.97/0.99 thf(func_def_23, type, mpartially_functional: (($i > $i > $o) > $o)).
% 3.97/0.99 thf(func_def_24, type, mfunctional: (($i > $i > $o) > $o)).
% 3.97/0.99 thf(func_def_25, type, mweakly_dense: (($i > $i > $o) > $o)).
% 3.97/0.99 thf(func_def_26, type, mweakly_connected: (($i > $i > $o) > $o)).
% 3.97/0.99 thf(func_def_27, type, mweakly_directed: (($i > $i > $o) > $o)).
% 3.97/0.99 thf(func_def_28, type, mvalid: (($i > $o) > $o)).
% 3.97/0.99 thf(func_def_29, type, minvalid: (($i > $o) > $o)).
% 3.97/0.99 thf(func_def_30, type, msatisfiable: (($i > $o) > $o)).
% 3.97/0.99 thf(func_def_31, type, mcountersatisfiable: (($i > $o) > $o)).
% 3.97/0.99 thf(func_def_32, type, a: ($i > $i > $o)).
% 3.97/0.99 thf(func_def_33, type, b: ($i > $i > $o)).
% 3.97/0.99 thf(func_def_34, type, c: ($i > $i > $o)).
% 3.97/0.99 thf(func_def_35, type, fool: ($i > $i > $o)).
% 3.97/0.99 thf(func_def_36, type, ws: (($i > $i > $o) > $i > $o)).
% 3.97/0.99 thf(func_def_37, type, db2: !>[X0: $tType]:(X0)).
% 3.97/0.99 thf(func_def_38, type, db0: !>[X0: $tType]:(X0)).
% 3.97/0.99 thf(func_def_39, type, db1: !>[X0: $tType]:(X0)).
% 3.97/0.99 thf(func_def_40, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 3.97/0.99 thf(func_def_41, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 3.97/0.99 thf(func_def_44, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 3.97/0.99 thf(func_def_45, type, vOR: ($o > $o > $o)).
% 3.97/0.99 thf(func_def_46, type, vNOT: ($o > $o)).
% 3.97/0.99 thf(func_def_47, type, db3: !>[X0: $tType]:(X0)).
% 3.97/0.99 thf(func_def_48, type, vIMP: ($o > $o > $o)).
% 3.97/0.99 thf(func_def_49, type, vAND: ($o > $o > $o)).
% 3.97/0.99 thf(func_def_50, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 3.97/0.99 thf(func_def_51, type, db4: !>[X0: $tType]:(X0)).
% 3.97/0.99 thf(func_def_52, type, sF0: $o).
% 3.97/0.99 thf(func_def_53, type, sF1: $o).
% 3.97/0.99 thf(func_def_54, type, sK2: ($i > $i)).
% 3.97/0.99 thf(func_def_55, type, sK3: ($i > $i)).
% 3.97/0.99 thf(func_def_56, type, sK4: ($i > ($i > $o) > $i)).
% 3.97/0.99 thf(f3,axiom,(
% 3.97/0.99 (mnot = (^[X0 : ($i > $o), X1 : $i] : (~(X0 @ X1))))),
% 3.97/0.99 file('/export/starexec/sandbox2/benchmark/Axioms/LCL013^0.ax',mnot)).
% 3.97/0.99 thf(f4,axiom,(
% 3.97/0.99 ((^[X0 : ($i > $o), X1 : ($i > $o), X2 : $i] : ((X0 @ X2) | (X1 @ X2))) = mor)),
% 3.97/0.99 file('/export/starexec/sandbox2/benchmark/Axioms/LCL013^0.ax',mor)).
% 3.97/0.99 thf(f6,axiom,(
% 3.97/0.99 ((^[X0 : ($i > $o), X1 : ($i > $o)] : ((mor @ (mnot @ X0) @ X1))) = mimplies)),
% 3.97/0.99 file('/export/starexec/sandbox2/benchmark/Axioms/LCL013^0.ax',mimplies)).
% 3.97/0.99 thf(f11,axiom,(
% 3.97/0.99 (mforall_prop = (^[X0 : (($i > $o) > $i > $o), X1 : $i] : (! [X2 : ($i > $o)] : (X0 @ X2 @ X1))))),
% 3.97/0.99 file('/export/starexec/sandbox2/benchmark/Axioms/LCL013^0.ax',mforall_prop)).
% 3.97/0.99 thf(f16,axiom,(
% 3.97/0.99 (mbox = (^[X0 : ($i > $i > $o), X1 : ($i > $o), X2 : $i] : (! [X3 : $i] : (~(X0 @ X2 @ X3) | (X1 @ X3)))))),
% 3.97/0.99 file('/export/starexec/sandbox2/benchmark/Axioms/LCL013^0.ax',mbox)).
% 3.97/0.99 thf(f28,axiom,(
% 3.97/0.99 ((^[X0 : ($i > $o)] : (! [X1 : $i] : (X0 @ X1))) = mvalid)),
% 3.97/0.99 file('/export/starexec/sandbox2/benchmark/Axioms/LCL013^0.ax',mvalid)).
% 3.97/0.99 thf(f32,axiom,(
% 3.97/0.99 (mvalid @ (mbox @ fool @ (mor @ (ws @ a) @ (mor @ (ws @ b) @ (ws @ c)))))),
% 3.97/0.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_1)).
% 3.97/0.99 thf(f39,axiom,(
% 3.97/0.99 (mvalid @ (mbox @ fool @ (mimplies @ (mnot @ (ws @ a)) @ (mbox @ b @ (mnot @ (ws @ a))))))),
% 3.97/0.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_3_a_b)).
% 3.97/0.99 thf(f43,axiom,(
% 3.97/0.99 (mvalid @ (mbox @ fool @ (mimplies @ (mnot @ (ws @ c)) @ (mbox @ a @ (mnot @ (ws @ c))))))),
% 3.97/0.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_3_c_a)).
% 3.97/0.99 thf(f44,axiom,(
% 3.97/0.99 (mvalid @ (mbox @ fool @ (mimplies @ (mnot @ (ws @ c)) @ (mbox @ b @ (mnot @ (ws @ c))))))),
% 3.97/0.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_3_c_b)).
% 3.97/0.99 thf(f45,axiom,(
% 3.97/0.99 (mvalid @ (mforall_prop @ (^[X0 : ($i > $o)] : ((mimplies @ (mbox @ fool @ X0) @ X0)))))),
% 3.97/0.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t_axiom_for_fool)).
% 3.97/0.99 thf(f62,axiom,(
% 3.97/0.99 (mvalid @ (mnot @ (mbox @ a @ (ws @ a))))),
% 3.97/0.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_4)).
% 3.97/0.99 thf(f63,axiom,(
% 3.97/0.99 (mvalid @ (mnot @ (mbox @ b @ (ws @ b))))),
% 3.97/0.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_5)).
% 3.97/0.99 thf(f64,conjecture,(
% 3.97/0.99 (mvalid @ (mbox @ c @ (ws @ c)))),
% 3.97/0.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj)).
% 3.97/0.99 thf(f65,negated_conjecture,(
% 3.97/0.99 ~(mvalid @ (mbox @ c @ (ws @ c)))),
% 3.97/0.99 inference(negated_conjecture,[status(cth)],[f64])).
% 3.97/0.99 thf(f76,plain,(
% 3.97/0.99 (mbox = (^[X0 : ($i > $i > $o), X1 : ($i > $o), X2 : $i] : (! [X3 : $i] : (~(X0 @ X2 @ X3) | (X1 @ X3)))))),
% 3.97/0.99 inference(rectify,[],[f16])).
% 3.97/0.99 thf(f77,plain,(
% 3.97/0.99 (mbox = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (Y0 @ Y2 @ Y3)))))))))))),
% 3.97/0.99 inference(fool_elimination,[],[f76])).
% 3.97/0.99 thf(f78,plain,(
% 3.97/0.99 ~(mvalid @ (mbox @ c @ (ws @ c)))),
% 3.97/0.99 inference(rectify,[],[f65])).
% 3.97/0.99 thf(f79,plain,(
% 3.97/0.99 ($true = ((~ (mvalid @ (mbox @ c @ (ws @ c))))))),
% 3.97/0.99 inference(fool_elimination,[],[f78])).
% 3.97/0.99 thf(f84,plain,(
% 3.97/0.99 (mvalid @ (mbox @ fool @ (mimplies @ (mnot @ (ws @ c)) @ (mbox @ b @ (mnot @ (ws @ c))))))),
% 3.97/0.99 inference(rectify,[],[f44])).
% 3.97/0.99 thf(f85,plain,(
% 3.97/0.99 (((mvalid @ (mbox @ fool @ (mimplies @ (mnot @ (ws @ c)) @ (mbox @ b @ (mnot @ (ws @ c))))))) = $true)),
% 3.97/0.99 inference(fool_elimination,[],[f84])).
% 3.97/0.99 thf(f93,plain,(
% 3.97/0.99 (mvalid @ (mnot @ (mbox @ b @ (ws @ b))))),
% 3.97/0.99 inference(rectify,[],[f63])).
% 3.97/0.99 thf(f94,plain,(
% 3.97/0.99 (((mvalid @ (mnot @ (mbox @ b @ (ws @ b))))) = $true)),
% 3.97/0.99 inference(fool_elimination,[],[f93])).
% 3.97/0.99 thf(f97,plain,(
% 3.97/0.99 ((^[X0 : ($i > $o), X1 : ($i > $o), X2 : $i] : ((X0 @ X2) | (X1 @ X2))) = mor)),
% 3.97/0.99 inference(rectify,[],[f4])).
% 3.97/0.99 thf(f98,plain,(
% 3.97/0.99 (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (Y0 @ Y2))))))))),
% 3.97/0.99 inference(fool_elimination,[],[f97])).
% 3.97/0.99 thf(f101,plain,(
% 3.97/0.99 (mvalid @ (mbox @ fool @ (mimplies @ (mnot @ (ws @ c)) @ (mbox @ a @ (mnot @ (ws @ c))))))),
% 3.97/0.99 inference(rectify,[],[f43])).
% 3.97/0.99 thf(f102,plain,(
% 3.97/0.99 (((mvalid @ (mbox @ fool @ (mimplies @ (mnot @ (ws @ c)) @ (mbox @ a @ (mnot @ (ws @ c))))))) = $true)),
% 3.97/0.99 inference(fool_elimination,[],[f101])).
% 3.97/0.99 thf(f103,plain,(
% 3.97/0.99 (mvalid @ (mbox @ fool @ (mimplies @ (mnot @ (ws @ a)) @ (mbox @ b @ (mnot @ (ws @ a))))))),
% 3.97/0.99 inference(rectify,[],[f39])).
% 3.97/0.99 thf(f104,plain,(
% 3.97/0.99 (((mvalid @ (mbox @ fool @ (mimplies @ (mnot @ (ws @ a)) @ (mbox @ b @ (mnot @ (ws @ a))))))) = $true)),
% 3.97/0.99 inference(fool_elimination,[],[f103])).
% 3.97/0.99 thf(f107,plain,(
% 3.97/0.99 (mvalid @ (mbox @ fool @ (mor @ (ws @ a) @ (mor @ (ws @ b) @ (ws @ c)))))),
% 3.97/0.99 inference(rectify,[],[f32])).
% 3.97/0.99 thf(f108,plain,(
% 3.97/0.99 (((mvalid @ (mbox @ fool @ (mor @ (ws @ a) @ (mor @ (ws @ b) @ (ws @ c)))))) = $true)),
% 3.97/0.99 inference(fool_elimination,[],[f107])).
% 3.97/0.99 thf(f112,plain,(
% 3.97/0.99 (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mor @ (mnot @ Y0) @ Y1)))))),
% 3.97/0.99 inference(fool_elimination,[],[f6])).
% 3.97/0.99 thf(f117,plain,(
% 3.97/0.99 (mnot = (^[X0 : ($i > $o), X1 : $i] : (~(X0 @ X1))))),
% 3.97/0.99 inference(rectify,[],[f3])).
% 3.97/0.99 thf(f118,plain,(
% 3.97/0.99 (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1))))))),
% 3.97/0.99 inference(fool_elimination,[],[f117])).
% 3.97/0.99 thf(f121,plain,(
% 3.97/0.99 (mforall_prop = (^[X0 : (($i > $o) > $i > $o), X1 : $i] : (! [X2 : ($i > $o)] : (X0 @ X2 @ X1))))),
% 3.97/0.99 inference(rectify,[],[f11])).
% 3.97/0.99 thf(f122,plain,(
% 3.97/0.99 (mforall_prop = (^[Y0 : ($i > $o) > $i > $o]: ((^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: (Y0 @ Y2 @ Y1)))))))),
% 3.97/0.99 inference(fool_elimination,[],[f121])).
% 3.97/0.99 thf(f166,plain,(
% 3.97/0.99 (mvalid @ (mnot @ (mbox @ a @ (ws @ a))))),
% 3.97/0.99 inference(rectify,[],[f62])).
% 3.97/0.99 thf(f167,plain,(
% 3.97/0.99 (((mvalid @ (mnot @ (mbox @ a @ (ws @ a))))) = $true)),
% 3.97/0.99 inference(fool_elimination,[],[f166])).
% 3.97/0.99 thf(f174,plain,(
% 3.97/0.99 (mvalid @ (mforall_prop @ (^[X0 : ($i > $o)] : ((mimplies @ (mbox @ fool @ X0) @ X0)))))),
% 3.97/0.99 inference(rectify,[],[f45])).
% 3.97/0.99 thf(f175,plain,(
% 3.97/0.99 ($true = ((mvalid @ (mforall_prop @ (^[Y0 : $i > $o]: (mimplies @ (mbox @ fool @ Y0) @ Y0))))))),
% 3.97/0.99 inference(fool_elimination,[],[f174])).
% 3.97/0.99 thf(f176,plain,(
% 3.97/0.99 ((^[X0 : ($i > $o)] : (! [X1 : $i] : (X0 @ X1))) = mvalid)),
% 3.97/0.99 inference(rectify,[],[f28])).
% 3.97/0.99 thf(f177,plain,(
% 3.97/0.99 (mvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))),
% 3.97/0.99 inference(fool_elimination,[],[f176])).
% 3.97/0.99 thf(f189,plain,(
% 3.97/0.99 (((mvalid @ (mbox @ fool @ (mor @ (ws @ a) @ (mor @ (ws @ b) @ (ws @ c)))))) = $true)),
% 3.97/0.99 inference(cnf_transformation,[],[f108])).
% 3.97/0.99 thf(f190,plain,(
% 3.97/0.99 ($true = ((mvalid @ (mforall_prop @ (^[Y0 : $i > $o]: (mimplies @ (mbox @ fool @ Y0) @ Y0))))))),
% 3.97/0.99 inference(cnf_transformation,[],[f175])).
% 3.97/0.99 thf(f191,plain,(
% 3.97/0.99 (((mvalid @ (mnot @ (mbox @ a @ (ws @ a))))) = $true)),
% 3.97/0.99 inference(cnf_transformation,[],[f167])).
% 3.97/0.99 thf(f198,plain,(
% 3.97/0.99 (mvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))),
% 3.97/0.99 inference(cnf_transformation,[],[f177])).
% 3.97/0.99 thf(f199,plain,(
% 3.97/0.99 (((mvalid @ (mbox @ fool @ (mimplies @ (mnot @ (ws @ a)) @ (mbox @ b @ (mnot @ (ws @ a))))))) = $true)),
% 3.97/0.99 inference(cnf_transformation,[],[f104])).
% 3.97/0.99 thf(f200,plain,(
% 3.97/0.99 (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mor @ (mnot @ Y0) @ Y1)))))),
% 3.97/0.99 inference(cnf_transformation,[],[f112])).
% 3.97/0.99 thf(f203,plain,(
% 3.97/0.99 (mforall_prop = (^[Y0 : ($i > $o) > $i > $o]: ((^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: (Y0 @ Y2 @ Y1)))))))),
% 3.97/0.99 inference(cnf_transformation,[],[f122])).
% 3.97/0.99 thf(f205,plain,(
% 3.97/0.99 (((mvalid @ (mbox @ fool @ (mimplies @ (mnot @ (ws @ c)) @ (mbox @ a @ (mnot @ (ws @ c))))))) = $true)),
% 3.97/0.99 inference(cnf_transformation,[],[f102])).
% 3.97/0.99 thf(f209,plain,(
% 3.97/0.99 (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (Y0 @ Y2))))))))),
% 3.97/0.99 inference(cnf_transformation,[],[f98])).
% 3.97/0.99 thf(f214,plain,(
% 3.97/0.99 ($true = ((~ (mvalid @ (mbox @ c @ (ws @ c))))))),
% 3.97/0.99 inference(cnf_transformation,[],[f79])).
% 3.97/0.99 thf(f217,plain,(
% 3.97/0.99 (((mvalid @ (mbox @ fool @ (mimplies @ (mnot @ (ws @ c)) @ (mbox @ b @ (mnot @ (ws @ c))))))) = $true)),
% 3.97/0.99 inference(cnf_transformation,[],[f85])).
% 3.97/0.99 thf(f232,plain,(
% 3.97/0.99 (mbox = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (Y0 @ Y2 @ Y3)))))))))))),
% 3.97/0.99 inference(cnf_transformation,[],[f77])).
% 3.97/0.99 thf(f236,plain,(
% 3.97/0.99 (((mvalid @ (mnot @ (mbox @ b @ (ws @ b))))) = $true)),
% 3.97/0.99 inference(cnf_transformation,[],[f94])).
% 3.97/0.99 thf(f241,plain,(
% 3.97/0.99 (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1))))))),
% 3.97/0.99 inference(cnf_transformation,[],[f118])).
% 3.97/0.99 thf(f249,definition,(
% 3.97/0.99 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 3.97/0.99 introduced(theory,[fool_exhaustiveness_axiom])).
% 3.97/0.99 thf(f251,plain,(
% 3.97/0.99 (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y3 @ Y4) | (Y2 @ Y4))))))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (~ (Y2 @ Y3))))) @ Y0) @ Y1)))))),
% 3.97/0.99 inference(definition_unfolding,[],[f200,f209,f241])).
% 3.97/0.99 thf(f259,plain,(
% 3.97/0.99 ($true = (((^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))) @ ((^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (Y0 @ Y2 @ Y3)))))))))) @ fool @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (Y0 @ Y2))))))) @ (ws @ a) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (Y0 @ Y2))))))) @ (ws @ b) @ (ws @ c)))))))),
% 3.97/0.99 inference(definition_unfolding,[],[f189,f198,f232,f209,f209])).
% 3.97/0.99 thf(f260,plain,(
% 3.97/0.99 ($true = (((^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))) @ ((^[Y0 : ($i > $o) > $i > $o]: ((^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: (Y0 @ Y2 @ Y1)))))) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i > $o]: ((^[Y5 : $i]: ((Y4 @ Y5) | (Y3 @ Y5))))))) @ ((^[Y3 : $i > $o]: ((^[Y4 : $i]: (~ (Y3 @ Y4))))) @ Y1) @ Y2)))) @ ((^[Y1 : $i > $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((Y2 @ Y4) | (~ (Y1 @ Y3 @ Y4)))))))))) @ fool @ Y0) @ Y0))))))),
% 3.97/0.99 inference(definition_unfolding,[],[f190,f198,f203,f251,f232])).
% 3.97/0.99 thf(f261,plain,(
% 3.97/0.99 ($true = (((^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1))))) @ ((^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (Y0 @ Y2 @ Y3)))))))))) @ a @ (ws @ a))))))),
% 3.97/0.99 inference(definition_unfolding,[],[f191,f198,f241,f232])).
% 3.97/0.99 thf(f267,plain,(
% 3.97/0.99 ($true = (((^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))) @ ((^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (Y0 @ Y2 @ Y3)))))))))) @ fool @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y3 @ Y4) | (Y2 @ Y4))))))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (~ (Y2 @ Y3))))) @ Y0) @ Y1)))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1))))) @ (ws @ a)) @ ((^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (Y0 @ Y2 @ Y3)))))))))) @ b @ ((^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1))))) @ (ws @ a))))))))),
% 3.97/0.99 inference(definition_unfolding,[],[f199,f198,f232,f251,f241,f232,f241])).
% 3.97/0.99 thf(f268,plain,(
% 3.97/0.99 ($true = (((^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))) @ ((^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (Y0 @ Y2 @ Y3)))))))))) @ fool @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y3 @ Y4) | (Y2 @ Y4))))))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (~ (Y2 @ Y3))))) @ Y0) @ Y1)))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1))))) @ (ws @ c)) @ ((^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (Y0 @ Y2 @ Y3)))))))))) @ a @ ((^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1))))) @ (ws @ c))))))))),
% 3.97/0.99 inference(definition_unfolding,[],[f205,f198,f232,f251,f241,f232,f241])).
% 3.97/0.99 thf(f271,plain,(
% 3.97/0.99 ($true = ((~ ((^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))) @ ((^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (Y0 @ Y2 @ Y3)))))))))) @ c @ (ws @ c))))))),
% 3.97/0.99 inference(definition_unfolding,[],[f214,f198,f232])).
% 3.97/0.99 thf(f274,plain,(
% 3.97/0.99 ($true = (((^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))) @ ((^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (Y0 @ Y2 @ Y3)))))))))) @ fool @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y3 @ Y4) | (Y2 @ Y4))))))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (~ (Y2 @ Y3))))) @ Y0) @ Y1)))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1))))) @ (ws @ c)) @ ((^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (Y0 @ Y2 @ Y3)))))))))) @ b @ ((^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1))))) @ (ws @ c))))))))),
% 3.97/0.99 inference(definition_unfolding,[],[f217,f198,f232,f251,f241,f232,f241])).
% 3.97/0.99 thf(f285,plain,(
% 3.97/0.99 ((((^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1))))) @ ((^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (Y0 @ Y2 @ Y3)))))))))) @ b @ (ws @ b))))) = $true)),
% 3.97/0.99 inference(definition_unfolding,[],[f236,f198,f241,f232])).
% 3.97/0.99 thf(f292,definition,(
% 3.97/0.99 (sF0 = (((^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))) @ ((^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (Y0 @ Y2 @ Y3)))))))))) @ c @ (ws @ c)))))),
% 3.97/0.99 introduced(definition,[new_symbols(definition,[sF0])],[function_definition])).
% 3.97/0.99 thf(f293,definition,(
% 3.97/0.99 (sF1 = ((~ sF0)))),
% 3.97/0.99 introduced(definition,[new_symbols(definition,[sF1])],[function_definition])).
% 3.97/0.99 thf(f294,plain,(
% 3.97/0.99 (((~ sF0)) = sF1)),
% 3.97/0.99 inference(reorient_equations,[],[f293])).
% 3.97/0.99 thf(f295,plain,(
% 3.97/0.99 ($true = sF1)),
% 3.97/0.99 inference(definition_folding,[],[f271,f294,f292])).
% 3.97/0.99 thf(f304,plain,(
% 3.97/0.99 ($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((!! @ $i @ (^[Y2 : $i]: ((~ (ws @ a @ Y2)) | (~ (b @ Y1 @ Y2))))) | (~ (~ (ws @ a @ Y1)))) | (~ (fool @ Y0 @ Y1)))))))))),
% 3.97/0.99 inference(beta-eta_normalization,[],[f267])).
% 3.97/0.99 thf(f305,plain,(
% 3.97/0.99 ($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((!! @ $i @ (^[Y2 : $i]: ((~ (ws @ a @ Y2)) | (~ (b @ Y1 @ Y2))))) | (ws @ a @ Y1)) | (~ (fool @ Y0 @ Y1)))))))))),
% 3.97/0.99 inference(boolean_simplification,[],[f304])).
% 3.97/0.99 thf(f310,plain,(
% 3.97/0.99 (((!! @ $i @ (^[Y0 : $i]: (~ (!! @ $i @ (^[Y1 : $i]: ((ws @ a @ Y1) | (~ (a @ Y0 @ Y1))))))))) = $true)),
% 3.97/0.99 inference(beta-eta_normalization,[],[f261])).
% 3.97/0.99 thf(f313,plain,(
% 3.97/0.99 ($true = ((!! @ $i @ (^[Y0 : $i]: (~ (!! @ $i @ (^[Y1 : $i]: ((ws @ b @ Y1) | (~ (b @ Y0 @ Y1))))))))))),
% 3.97/0.99 inference(beta-eta_normalization,[],[f285])).
% 3.97/0.99 thf(f318,plain,(
% 3.97/0.99 (sF0 = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((ws @ c @ Y1) | (~ (c @ Y0 @ Y1)))))))))),
% 3.97/0.99 inference(beta-eta_normalization,[],[f292])).
% 3.97/0.99 thf(f320,plain,(
% 3.97/0.99 ($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((ws @ c @ Y1) | (ws @ b @ Y1)) | (ws @ a @ Y1)) | (~ (fool @ Y0 @ Y1)))))))))),
% 3.97/0.99 inference(beta-eta_normalization,[],[f259])).
% 3.97/0.99 thf(f330,plain,(
% 3.97/0.99 ($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((!! @ $i @ (^[Y2 : $i]: ((~ (ws @ c @ Y2)) | (~ (a @ Y1 @ Y2))))) | (~ (~ (ws @ c @ Y1)))) | (~ (fool @ Y0 @ Y1)))))))))),
% 3.97/0.99 inference(beta-eta_normalization,[],[f268])).
% 3.97/0.99 thf(f331,plain,(
% 3.97/0.99 ($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((!! @ $i @ (^[Y2 : $i]: ((~ (ws @ c @ Y2)) | (~ (a @ Y1 @ Y2))))) | (ws @ c @ Y1)) | (~ (fool @ Y0 @ Y1)))))))))),
% 3.97/0.99 inference(boolean_simplification,[],[f330])).
% 3.97/0.99 thf(f337,plain,(
% 3.97/0.99 ($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: ((Y1 @ Y0) | (~ (!! @ $i @ (^[Y2 : $i]: ((Y1 @ Y2) | (~ (fool @ Y0 @ Y2)))))))))))))),
% 3.97/0.99 inference(beta-eta_normalization,[],[f260])).
% 3.97/0.99 thf(f339,plain,(
% 3.97/0.99 ($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((!! @ $i @ (^[Y2 : $i]: ((~ (ws @ c @ Y2)) | (~ (b @ Y1 @ Y2))))) | (~ (~ (ws @ c @ Y1)))) | (~ (fool @ Y0 @ Y1)))))))))),
% 3.97/0.99 inference(beta-eta_normalization,[],[f274])).
% 3.97/0.99 thf(f340,plain,(
% 3.97/0.99 ($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((!! @ $i @ (^[Y2 : $i]: ((~ (ws @ c @ Y2)) | (~ (b @ Y1 @ Y2))))) | (ws @ c @ Y1)) | (~ (fool @ Y0 @ Y1)))))))))),
% 3.97/0.99 inference(boolean_simplification,[],[f339])).
% 3.97/0.99 thf(f349,plain,(
% 3.97/0.99 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: (~ (!! @ $i @ (^[Y1 : $i]: ((ws @ a @ Y1) | (~ (a @ Y0 @ Y1))))))) @ X1)))) )),
% 3.97/0.99 inference(pi_proxy_clausification,[],[f310])).
% 3.97/0.99 thf(f350,plain,(
% 3.97/0.99 ( ! [X1 : $i] : (($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((ws @ a @ Y0) | (~ (a @ X1 @ Y0))))))))) )),
% 3.97/0.99 inference(beta-eta_normalization,[],[f349])).
% 3.97/0.99 thf(f351,plain,(
% 3.97/0.99 ( ! [X1 : $i] : (($false = ((!! @ $i @ (^[Y0 : $i]: ((ws @ a @ Y0) | (~ (a @ X1 @ Y0)))))))) )),
% 3.97/0.99 inference(not_proxy_clausification,[],[f350])).
% 3.97/0.99 thf(f356,plain,(
% 3.97/0.99 ( ! [X1 : $i] : (((((^[Y0 : $i]: ((ws @ a @ Y0) | (~ (a @ X1 @ Y0)))) @ (sK2 @ X1))) = $false)) )),
% 3.97/0.99 inference(sigma_proxy_clausification,[],[f351])).
% 3.97/0.99 thf(f360,plain,(
% 3.97/0.99 ( ! [X1 : $i] : (($false = (((ws @ a @ (sK2 @ X1)) | (~ (a @ X1 @ (sK2 @ X1))))))) )),
% 3.97/0.99 inference(beta-eta_normalization,[],[f356])).
% 3.97/0.99 thf(f361,plain,(
% 3.97/0.99 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: (~ (!! @ $i @ (^[Y1 : $i]: ((ws @ b @ Y1) | (~ (b @ Y0 @ Y1))))))) @ X1)))) )),
% 3.97/0.99 inference(pi_proxy_clausification,[],[f313])).
% 3.97/0.99 thf(f362,plain,(
% 3.97/0.99 ( ! [X1 : $i] : ((((~ (!! @ $i @ (^[Y0 : $i]: ((ws @ b @ Y0) | (~ (b @ X1 @ Y0))))))) = $true)) )),
% 3.97/0.99 inference(beta-eta_normalization,[],[f361])).
% 3.97/0.99 thf(f363,plain,(
% 3.97/0.99 ( ! [X1 : $i] : (($false = ((!! @ $i @ (^[Y0 : $i]: ((ws @ b @ Y0) | (~ (b @ X1 @ Y0)))))))) )),
% 3.97/0.99 inference(not_proxy_clausification,[],[f362])).
% 3.97/0.99 thf(f368,plain,(
% 3.97/0.99 ( ! [X1 : $i] : (((((^[Y0 : $i]: ((ws @ b @ Y0) | (~ (b @ X1 @ Y0)))) @ (sK3 @ X1))) = $false)) )),
% 3.97/0.99 inference(sigma_proxy_clausification,[],[f363])).
% 3.97/0.99 thf(f370,plain,(
% 3.97/0.99 ( ! [X1 : $i] : (($false = (((ws @ b @ (sK3 @ X1)) | (~ (b @ X1 @ (sK3 @ X1))))))) )),
% 3.97/0.99 inference(beta-eta_normalization,[],[f368])).
% 3.97/0.99 thf(f374,plain,(
% 3.97/0.99 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: ((Y1 @ Y0) | (~ (!! @ $i @ (^[Y2 : $i]: ((Y1 @ Y2) | (~ (fool @ Y0 @ Y2)))))))))) @ X1)))) )),
% 3.97/0.99 inference(pi_proxy_clausification,[],[f337])).
% 3.97/0.99 thf(f375,plain,(
% 3.97/0.99 ( ! [X1 : $i] : ((((!! @ ($i > $o) @ (^[Y0 : $i > $o]: ((Y0 @ X1) | (~ (!! @ $i @ (^[Y1 : $i]: ((Y0 @ Y1) | (~ (fool @ X1 @ Y1)))))))))) = $true)) )),
% 3.97/0.99 inference(beta-eta_normalization,[],[f374])).
% 3.97/0.99 thf(f376,plain,(
% 3.97/0.99 ( ! [X2 : ($i > $o),X1 : $i] : (((((^[Y0 : $i > $o]: ((Y0 @ X1) | (~ (!! @ $i @ (^[Y1 : $i]: ((Y0 @ Y1) | (~ (fool @ X1 @ Y1)))))))) @ X2)) = $true)) )),
% 3.97/0.99 inference(pi_proxy_clausification,[],[f375])).
% 3.97/0.99 thf(f377,plain,(
% 3.97/0.99 ( ! [X2 : ($i > $o),X1 : $i] : (((((X2 @ X1) | (~ (!! @ $i @ (^[Y0 : $i]: ((X2 @ Y0) | (~ (fool @ X1 @ Y0)))))))) = $true)) )),
% 3.97/0.99 inference(beta-eta_normalization,[],[f376])).
% 3.97/0.99 thf(f379,plain,(
% 3.97/0.99 ( ! [X0 : ($i > $o),X1 : $i] : (($false = ((!! @ $i @ (^[Y0 : $i]: ((X0 @ Y0) | (~ (fool @ X1 @ Y0))))))) | ($true = (((X0 @ X1) | (~ $true))))) )),
% 3.97/0.99 inference(constrained_superposition,[],[f377,f249])).
% 3.97/0.99 thf(f382,plain,(
% 3.97/0.99 ( ! [X0 : ($i > $o),X1 : $i] : (($true = (((X0 @ X1) | $false))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((X0 @ Y0) | (~ (fool @ X1 @ Y0)))))))) )),
% 3.97/0.99 inference(boolean_simplification,[],[f379])).
% 3.97/0.99 thf(f383,plain,(
% 3.97/0.99 ( ! [X0 : ($i > $o),X1 : $i] : (($false = ((!! @ $i @ (^[Y0 : $i]: ((X0 @ Y0) | (~ (fool @ X1 @ Y0))))))) | (((X0 @ X1)) = $true)) )),
% 3.97/0.99 inference(boolean_simplification,[],[f382])).
% 3.97/0.99 thf(f386,plain,(
% 3.97/0.99 ( ! [X1 : $i] : (((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((((ws @ c @ Y1) | (ws @ b @ Y1)) | (ws @ a @ Y1)) | (~ (fool @ Y0 @ Y1)))))) @ X1)) = $true)) )),
% 3.97/0.99 inference(pi_proxy_clausification,[],[f320])).
% 3.97/0.99 thf(f387,plain,(
% 3.97/0.99 ( ! [X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: ((((ws @ c @ Y0) | (ws @ b @ Y0)) | (ws @ a @ Y0)) | (~ (fool @ X1 @ Y0)))))))) )),
% 3.97/0.99 inference(beta-eta_normalization,[],[f386])).
% 3.97/0.99 thf(f388,plain,(
% 3.97/0.99 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((((ws @ c @ Y0) | (ws @ b @ Y0)) | (ws @ a @ Y0)) | (~ (fool @ X1 @ Y0)))) @ X2)))) )),
% 3.97/0.99 inference(pi_proxy_clausification,[],[f387])).
% 3.97/0.99 thf(f389,plain,(
% 3.97/0.99 ( ! [X2 : $i,X1 : $i] : (($true = (((((ws @ c @ X2) | (ws @ b @ X2)) | (ws @ a @ X2)) | (~ (fool @ X1 @ X2)))))) )),
% 3.97/0.99 inference(beta-eta_normalization,[],[f388])).
% 3.97/0.99 thf(f408,plain,(
% 3.97/0.99 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((!! @ $i @ (^[Y2 : $i]: ((~ (ws @ a @ Y2)) | (~ (b @ Y1 @ Y2))))) | (ws @ a @ Y1)) | (~ (fool @ Y0 @ Y1)))))) @ X1)))) )),
% 3.97/0.99 inference(pi_proxy_clausification,[],[f305])).
% 3.97/0.99 thf(f409,plain,(
% 3.97/0.99 ( ! [X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: (((!! @ $i @ (^[Y1 : $i]: ((~ (ws @ a @ Y1)) | (~ (b @ Y0 @ Y1))))) | (ws @ a @ Y0)) | (~ (fool @ X1 @ Y0)))))))) )),
% 3.97/0.99 inference(beta-eta_normalization,[],[f408])).
% 3.97/0.99 thf(f410,plain,(
% 3.97/0.99 ( ! [X2 : $i,X1 : $i] : (((((^[Y0 : $i]: (((!! @ $i @ (^[Y1 : $i]: ((~ (ws @ a @ Y1)) | (~ (b @ Y0 @ Y1))))) | (ws @ a @ Y0)) | (~ (fool @ X1 @ Y0)))) @ X2)) = $true)) )),
% 3.97/0.99 inference(pi_proxy_clausification,[],[f409])).
% 3.97/0.99 thf(f411,plain,(
% 3.97/0.99 ( ! [X2 : $i,X1 : $i] : ((((((!! @ $i @ (^[Y0 : $i]: ((~ (ws @ a @ Y0)) | (~ (b @ X2 @ Y0))))) | (ws @ a @ X2)) | (~ (fool @ X1 @ X2)))) = $true)) )),
% 3.97/0.99 inference(beta-eta_normalization,[],[f410])).
% 3.97/0.99 thf(f449,plain,(
% 3.97/0.99 (((~ sF0)) = $true)),
% 3.97/0.99 inference(forward_demodulation,[],[f294,f295])).
% 3.97/0.99 thf(f487,plain,(
% 3.97/0.99 ( ! [X0 : ($i > $o),X1 : $i] : ((((X0 @ X1)) = $true) | ($false = (((^[Y0 : $i]: ((X0 @ Y0) | (~ (fool @ X1 @ Y0)))) @ (sK4 @ X1 @ X0))))) )),
% 3.97/0.99 inference(sigma_proxy_clausification,[],[f383])).
% 3.97/0.99 thf(f490,plain,(
% 3.97/0.99 ( ! [X0 : ($i > $o),X1 : $i] : (($false = (((X0 @ (sK4 @ X1 @ X0)) | (~ (fool @ X1 @ (sK4 @ X1 @ X0)))))) | (((X0 @ X1)) = $true)) )),
% 3.97/0.99 inference(beta-eta_normalization,[],[f487])).
% 3.97/0.99 thf(f512,plain,(
% 3.97/0.99 ($false = sF0)),
% 3.97/0.99 inference(not_proxy_clausification,[],[f449])).
% 3.97/0.99 thf(f534,plain,(
% 3.97/0.99 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((!! @ $i @ (^[Y2 : $i]: ((~ (ws @ c @ Y2)) | (~ (a @ Y1 @ Y2))))) | (ws @ c @ Y1)) | (~ (fool @ Y0 @ Y1)))))) @ X1)))) )),
% 3.97/0.99 inference(pi_proxy_clausification,[],[f331])).
% 3.97/0.99 thf(f535,plain,(
% 3.97/0.99 ( ! [X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: (((!! @ $i @ (^[Y1 : $i]: ((~ (ws @ c @ Y1)) | (~ (a @ Y0 @ Y1))))) | (ws @ c @ Y0)) | (~ (fool @ X1 @ Y0)))))))) )),
% 3.97/0.99 inference(beta-eta_normalization,[],[f534])).
% 3.97/0.99 thf(f536,plain,(
% 3.97/0.99 ( ! [X2 : $i,X1 : $i] : (((((^[Y0 : $i]: (((!! @ $i @ (^[Y1 : $i]: ((~ (ws @ c @ Y1)) | (~ (a @ Y0 @ Y1))))) | (ws @ c @ Y0)) | (~ (fool @ X1 @ Y0)))) @ X2)) = $true)) )),
% 3.97/0.99 inference(pi_proxy_clausification,[],[f535])).
% 3.97/0.99 thf(f537,plain,(
% 3.97/0.99 ( ! [X2 : $i,X1 : $i] : (($true = ((((!! @ $i @ (^[Y0 : $i]: ((~ (ws @ c @ Y0)) | (~ (a @ X2 @ Y0))))) | (ws @ c @ X2)) | (~ (fool @ X1 @ X2)))))) )),
% 3.97/0.99 inference(beta-eta_normalization,[],[f536])).
% 3.97/0.99 thf(f557,plain,(
% 3.97/0.99 ($false = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((ws @ c @ Y1) | (~ (c @ Y0 @ Y1)))))))))),
% 3.97/0.99 inference(backward_demodulation,[],[f318,f512])).
% 3.97/0.99 thf(f561,plain,(
% 3.97/0.99 ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((ws @ c @ Y1) | (~ (c @ Y0 @ Y1)))))) @ sK5)))),
% 3.97/0.99 inference(sigma_proxy_clausification,[],[f557])).
% 3.97/0.99 thf(f563,plain,(
% 3.97/0.99 ($false = ((!! @ $i @ (^[Y0 : $i]: ((ws @ c @ Y0) | (~ (c @ sK5 @ Y0)))))))),
% 3.97/0.99 inference(beta-eta_normalization,[],[f561])).
% 3.97/0.99 thf(f565,plain,(
% 3.97/0.99 ($false = (((^[Y0 : $i]: ((ws @ c @ Y0) | (~ (c @ sK5 @ Y0)))) @ sK6)))),
% 3.97/0.99 inference(sigma_proxy_clausification,[],[f563])).
% 3.97/0.99 thf(f568,plain,(
% 3.97/0.99 ($false = (((ws @ c @ sK6) | (~ (c @ sK5 @ sK6)))))),
% 3.97/0.99 inference(beta-eta_normalization,[],[f565])).
% 3.97/0.99 thf(f628,plain,(
% 3.97/0.99 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (((!! @ $i @ (^[Y2 : $i]: ((~ (ws @ c @ Y2)) | (~ (b @ Y1 @ Y2))))) | (ws @ c @ Y1)) | (~ (fool @ Y0 @ Y1)))))) @ X1)))) )),
% 3.97/0.99 inference(pi_proxy_clausification,[],[f340])).
% 3.97/0.99 thf(f629,plain,(
% 3.97/0.99 ( ! [X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: (((!! @ $i @ (^[Y1 : $i]: ((~ (ws @ c @ Y1)) | (~ (b @ Y0 @ Y1))))) | (ws @ c @ Y0)) | (~ (fool @ X1 @ Y0)))))))) )),
% 3.97/0.99 inference(beta-eta_normalization,[],[f628])).
% 3.97/0.99 thf(f630,plain,(
% 3.97/0.99 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: (((!! @ $i @ (^[Y1 : $i]: ((~ (ws @ c @ Y1)) | (~ (b @ Y0 @ Y1))))) | (ws @ c @ Y0)) | (~ (fool @ X1 @ Y0)))) @ X2)))) )),
% 3.97/0.99 inference(pi_proxy_clausification,[],[f629])).
% 3.97/0.99 thf(f631,plain,(
% 3.97/0.99 ( ! [X2 : $i,X1 : $i] : (($true = ((((!! @ $i @ (^[Y0 : $i]: ((~ (ws @ c @ Y0)) | (~ (b @ X2 @ Y0))))) | (ws @ c @ X2)) | (~ (fool @ X1 @ X2)))))) )),
% 3.97/0.99 inference(beta-eta_normalization,[],[f630])).
% 3.97/0.99 thf(f660,plain,(
% 3.97/0.99 ($false = ((~ (c @ sK5 @ sK6))))),
% 3.97/0.99 inference(or_proxy_clausification,[],[f568])).
% 3.97/0.99 thf(f708,plain,(
% 3.97/0.99 ($false = (((ws @ c @ sK6) | $false)))),
% 3.97/0.99 inference(backward_demodulation,[],[f568,f660])).
% 3.97/0.99 thf(f713,plain,(
% 3.97/0.99 (((ws @ c @ sK6)) = $false)),
% 3.97/0.99 inference(boolean_simplification,[],[f708])).
% 3.97/0.99 thf(f776,plain,(
% 3.97/0.99 ( ! [X0 : $i] : (($true = ((((!! @ $i @ (^[Y0 : $i]: ((~ (ws @ c @ Y0)) | (~ (a @ sK6 @ Y0))))) | $false) | (~ (fool @ X0 @ sK6)))))) )),
% 3.97/0.99 inference(constrained_superposition,[],[f537,f713])).
% 3.97/0.99 thf(f782,plain,(
% 3.97/0.99 ( ! [X0 : $i] : (($true = (((!! @ $i @ (^[Y0 : $i]: ((~ (ws @ c @ Y0)) | (~ (a @ sK6 @ Y0))))) | (~ (fool @ X0 @ sK6)))))) )),
% 3.97/0.99 inference(boolean_simplification,[],[f776])).
% 3.97/0.99 thf(f817,plain,(
% 3.97/0.99 ( ! [X0 : ($i > $o),X1 : $i] : (($false = ((X0 @ (sK4 @ X1 @ X0)))) | (((X0 @ X1)) = $true)) )),
% 3.97/0.99 inference(or_proxy_clausification,[],[f490])).
% 3.97/0.99 thf(f905,plain,(
% 3.97/0.99 ( ! [X1 : $i] : (($false = ((~ (a @ X1 @ (sK2 @ X1)))))) )),
% 3.97/0.99 inference(or_proxy_clausification,[],[f360])).
% 3.97/0.99 thf(f918,plain,(
% 3.97/0.99 ( ! [X1 : $i] : (($false = (((ws @ a @ (sK2 @ X1)) | $false)))) )),
% 3.97/0.99 inference(backward_demodulation,[],[f360,f905])).
% 3.97/0.99 thf(f919,plain,(
% 3.97/0.99 ( ! [X1 : $i] : (($true = ((a @ X1 @ (sK2 @ X1))))) )),
% 3.97/0.99 inference(not_proxy_clausification,[],[f905])).
% 3.97/0.99 thf(f923,plain,(
% 3.97/0.99 ( ! [X1 : $i] : (($false = ((ws @ a @ (sK2 @ X1))))) )),
% 3.97/0.99 inference(boolean_simplification,[],[f918])).
% 3.97/0.99 thf(f933,plain,(
% 3.97/0.99 ( ! [X0 : $i,X1 : $i] : (($true = ((((!! @ $i @ (^[Y0 : $i]: ((~ (ws @ a @ Y0)) | (~ (b @ (sK2 @ X0) @ Y0))))) | $false) | (~ (fool @ X1 @ (sK2 @ X0))))))) )),
% 3.97/0.99 inference(constrained_superposition,[],[f411,f923])).
% 3.97/0.99 thf(f935,plain,(
% 3.97/0.99 ( ! [X0 : $i,X1 : $i] : (($true = (((!! @ $i @ (^[Y0 : $i]: ((~ (ws @ a @ Y0)) | (~ (b @ (sK2 @ X0) @ Y0))))) | (~ (fool @ X1 @ (sK2 @ X0))))))) )),
% 3.97/0.99 inference(boolean_simplification,[],[f933])).
% 3.97/0.99 thf(f1001,plain,(
% 3.97/0.99 ( ! [X0 : $i] : (((($false | (~ $false))) = $false) | ($true = ((fool @ X0 @ X0))) | ($true = ((fool @ X0 @ X0)))) )),
% 3.97/0.99 inference(constrained_superposition,[],[f490,f817])).
% 3.97/0.99 thf(f1016,plain,(
% 3.97/0.99 ( ! [X0 : $i] : (($true = ((fool @ X0 @ X0))) | ((($false | (~ $false))) = $false)) )),
% 3.97/0.99 inference(duplicate_literal_removal,[],[f1001])).
% 3.97/0.99 thf(f1017,plain,(
% 3.97/0.99 ( ! [X0 : $i] : (($true = $false) | ($true = ((fool @ X0 @ X0)))) )),
% 3.97/0.99 inference(boolean_simplification,[],[f1016])).
% 3.97/0.99 thf(f1018,plain,(
% 3.97/0.99 ( ! [X0 : $i] : (($true = ((fool @ X0 @ X0)))) )),
% 3.97/0.99 inference(trivial_inequality_removal,[],[f1017])).
% 3.97/0.99 thf(f1088,plain,(
% 3.97/0.99 ( ! [X0 : $i] : (($true = ((((!! @ $i @ (^[Y0 : $i]: ((~ (ws @ c @ Y0)) | (~ (b @ X0 @ Y0))))) | (ws @ c @ X0)) | (~ $true))))) )),
% 3.97/0.99 inference(constrained_superposition,[],[f631,f1018])).
% 3.97/0.99 thf(f1090,plain,(
% 3.97/0.99 ( ! [X0 : $i] : (($true = (((!! @ $i @ (^[Y0 : $i]: ((~ (ws @ a @ Y0)) | (~ (b @ (sK2 @ X0) @ Y0))))) | (~ $true))))) )),
% 3.97/0.99 inference(constrained_superposition,[],[f935,f1018])).
% 3.97/0.99 thf(f1092,plain,(
% 3.97/0.99 ($true = (((!! @ $i @ (^[Y0 : $i]: ((~ (ws @ c @ Y0)) | (~ (a @ sK6 @ Y0))))) | (~ $true))))),
% 3.97/0.99 inference(constrained_superposition,[],[f782,f1018])).
% 3.97/0.99 thf(f1101,plain,(
% 3.97/0.99 ( ! [X0 : $i] : (($true = ((((!! @ $i @ (^[Y0 : $i]: ((~ (ws @ c @ Y0)) | (~ (b @ X0 @ Y0))))) | (ws @ c @ X0)) | $false)))) )),
% 3.97/0.99 inference(boolean_simplification,[],[f1088])).
% 3.97/0.99 thf(f1102,plain,(
% 3.97/0.99 ( ! [X0 : $i] : (($true = (((!! @ $i @ (^[Y0 : $i]: ((~ (ws @ c @ Y0)) | (~ (b @ X0 @ Y0))))) | (ws @ c @ X0))))) )),
% 3.97/0.99 inference(boolean_simplification,[],[f1101])).
% 3.97/0.99 thf(f1116,plain,(
% 3.97/0.99 ($true = (((!! @ $i @ (^[Y0 : $i]: ((~ (ws @ c @ Y0)) | (~ (a @ sK6 @ Y0))))) | $false)))),
% 3.97/0.99 inference(boolean_simplification,[],[f1092])).
% 3.97/0.99 thf(f1117,plain,(
% 3.97/0.99 (((!! @ $i @ (^[Y0 : $i]: ((~ (ws @ c @ Y0)) | (~ (a @ sK6 @ Y0)))))) = $true)),
% 3.97/0.99 inference(boolean_simplification,[],[f1116])).
% 3.97/0.99 thf(f1120,plain,(
% 3.97/0.99 ( ! [X0 : $i] : (($true = (((!! @ $i @ (^[Y0 : $i]: ((~ (ws @ a @ Y0)) | (~ (b @ (sK2 @ X0) @ Y0))))) | $false)))) )),
% 3.97/0.99 inference(boolean_simplification,[],[f1090])).
% 3.97/0.99 thf(f1121,plain,(
% 3.97/0.99 ( ! [X0 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (ws @ a @ Y0)) | (~ (b @ (sK2 @ X0) @ Y0)))))))) )),
% 3.97/0.99 inference(boolean_simplification,[],[f1120])).
% 3.97/0.99 thf(f1131,plain,(
% 3.97/0.99 ( ! [X1 : $i] : (((((^[Y0 : $i]: ((~ (ws @ c @ Y0)) | (~ (a @ sK6 @ Y0)))) @ X1)) = $true)) )),
% 3.97/0.99 inference(pi_proxy_clausification,[],[f1117])).
% 3.97/0.99 thf(f1133,plain,(
% 3.97/0.99 ( ! [X1 : $i] : (((((~ (ws @ c @ X1)) | (~ (a @ sK6 @ X1)))) = $true)) )),
% 3.97/0.99 inference(beta-eta_normalization,[],[f1131])).
% 3.97/0.99 thf(f1135,plain,(
% 3.97/0.99 ( ! [X0 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (ws @ a @ Y0)) | (~ (b @ (sK2 @ X0) @ Y0)))) @ X1)))) )),
% 3.97/0.99 inference(pi_proxy_clausification,[],[f1121])).
% 3.97/0.99 thf(f1137,plain,(
% 3.97/0.99 ( ! [X0 : $i,X1 : $i] : (($true = (((~ (ws @ a @ X1)) | (~ (b @ (sK2 @ X0) @ X1)))))) )),
% 3.97/0.99 inference(beta-eta_normalization,[],[f1135])).
% 3.97/0.99 thf(f1320,plain,(
% 3.97/0.99 ($true = (((~ (ws @ c @ (sK2 @ sK6))) | (~ $true))))),
% 3.97/0.99 inference(constrained_superposition,[],[f1133,f919])).
% 3.97/0.99 thf(f1329,plain,(
% 3.97/0.99 ($true = (((~ (ws @ c @ (sK2 @ sK6))) | $false)))),
% 3.97/0.99 inference(boolean_simplification,[],[f1320])).
% 3.97/0.99 thf(f1330,plain,(
% 3.97/0.99 ($true = ((~ (ws @ c @ (sK2 @ sK6)))))),
% 3.97/0.99 inference(boolean_simplification,[],[f1329])).
% 3.97/0.99 thf(f1341,plain,(
% 3.97/0.99 ($false = ((ws @ c @ (sK2 @ sK6))))),
% 3.97/0.99 inference(not_proxy_clausification,[],[f1330])).
% 3.97/0.99 thf(f1358,plain,(
% 3.97/0.99 ((((!! @ $i @ (^[Y0 : $i]: ((~ (ws @ c @ Y0)) | (~ (b @ (sK2 @ sK6) @ Y0))))) | $false)) = $true)),
% 3.97/0.99 inference(constrained_superposition,[],[f1102,f1341])).
% 3.97/0.99 thf(f1363,plain,(
% 3.97/0.99 ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (ws @ c @ Y0)) | (~ (b @ (sK2 @ sK6) @ Y0)))))))),
% 3.97/0.99 inference(boolean_simplification,[],[f1358])).
% 3.97/0.99 thf(f1385,plain,(
% 3.97/0.99 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (ws @ c @ Y0)) | (~ (b @ (sK2 @ sK6) @ Y0)))) @ X1)))) )),
% 3.97/0.99 inference(pi_proxy_clausification,[],[f1363])).
% 3.97/0.99 thf(f1386,plain,(
% 3.97/0.99 ( ! [X1 : $i] : (($true = (((~ (ws @ c @ X1)) | (~ (b @ (sK2 @ sK6) @ X1)))))) )),
% 3.97/0.99 inference(beta-eta_normalization,[],[f1385])).
% 3.97/0.99 thf(f1389,plain,(
% 3.97/0.99 ( ! [X1 : $i] : (($false = ((~ (b @ X1 @ (sK3 @ X1)))))) )),
% 3.97/0.99 inference(or_proxy_clausification,[],[f370])).
% 3.97/0.99 thf(f1402,plain,(
% 3.97/0.99 ( ! [X1 : $i] : (((((ws @ b @ (sK3 @ X1)) | $false)) = $false)) )),
% 3.97/0.99 inference(backward_demodulation,[],[f370,f1389])).
% 3.97/0.99 thf(f1403,plain,(
% 3.97/0.99 ( ! [X1 : $i] : (($true = ((b @ X1 @ (sK3 @ X1))))) )),
% 3.97/0.99 inference(not_proxy_clausification,[],[f1389])).
% 3.97/0.99 thf(f1410,plain,(
% 3.97/0.99 ( ! [X1 : $i] : ((((ws @ b @ (sK3 @ X1))) = $false)) )),
% 3.97/0.99 inference(boolean_simplification,[],[f1402])).
% 3.97/0.99 thf(f1548,plain,(
% 3.97/0.99 ( ! [X0 : $i] : (($true = (((~ (ws @ a @ (sK3 @ (sK2 @ X0)))) | (~ $true))))) )),
% 3.97/0.99 inference(constrained_superposition,[],[f1137,f1403])).
% 3.97/0.99 thf(f1567,plain,(
% 3.97/0.99 ( ! [X0 : $i] : (($true = (((~ (ws @ a @ (sK3 @ (sK2 @ X0)))) | $false)))) )),
% 3.97/0.99 inference(boolean_simplification,[],[f1548])).
% 3.97/0.99 thf(f1568,plain,(
% 3.97/0.99 ( ! [X0 : $i] : ((((~ (ws @ a @ (sK3 @ (sK2 @ X0))))) = $true)) )),
% 3.97/0.99 inference(boolean_simplification,[],[f1567])).
% 3.97/0.99 thf(f1569,plain,(
% 3.97/0.99 ( ! [X0 : $i] : (($false = ((ws @ a @ (sK3 @ (sK2 @ X0)))))) )),
% 3.97/0.99 inference(not_proxy_clausification,[],[f1568])).
% 3.97/0.99 thf(f1757,plain,(
% 3.97/0.99 ($true = (((~ (ws @ c @ (sK3 @ (sK2 @ sK6)))) | (~ $true))))),
% 3.97/0.99 inference(constrained_superposition,[],[f1386,f1403])).
% 3.97/0.99 thf(f1775,plain,(
% 3.97/0.99 ($true = (((~ (ws @ c @ (sK3 @ (sK2 @ sK6)))) | $false)))),
% 3.97/0.99 inference(boolean_simplification,[],[f1757])).
% 3.97/0.99 thf(f1776,plain,(
% 3.97/0.99 ($true = ((~ (ws @ c @ (sK3 @ (sK2 @ sK6))))))),
% 3.97/0.99 inference(boolean_simplification,[],[f1775])).
% 3.97/0.99 thf(f1784,plain,(
% 3.97/0.99 ($false = ((ws @ c @ (sK3 @ (sK2 @ sK6)))))),
% 3.97/0.99 inference(not_proxy_clausification,[],[f1776])).
% 3.97/0.99 thf(f1800,plain,(
% 3.97/0.99 ( ! [X0 : $i] : (((((($false | (ws @ b @ (sK3 @ (sK2 @ sK6)))) | (ws @ a @ (sK3 @ (sK2 @ sK6)))) | (~ (fool @ X0 @ (sK3 @ (sK2 @ sK6)))))) = $true)) )),
% 3.97/0.99 inference(constrained_superposition,[],[f389,f1784])).
% 3.97/0.99 thf(f1812,plain,(
% 3.97/0.99 ( ! [X0 : $i] : ((((((ws @ b @ (sK3 @ (sK2 @ sK6))) | (ws @ a @ (sK3 @ (sK2 @ sK6)))) | (~ (fool @ X0 @ (sK3 @ (sK2 @ sK6)))))) = $true)) )),
% 3.97/0.99 inference(boolean_simplification,[],[f1800])).
% 3.97/0.99 thf(f1825,plain,(
% 3.97/0.99 ( ! [X0 : $i] : ((((($false | (ws @ a @ (sK3 @ (sK2 @ sK6)))) | (~ (fool @ X0 @ (sK3 @ (sK2 @ sK6)))))) = $true)) )),
% 3.97/0.99 inference(forward_demodulation,[],[f1812,f1410])).
% 3.97/0.99 thf(f1826,plain,(
% 3.97/0.99 ( ! [X0 : $i] : (((((ws @ a @ (sK3 @ (sK2 @ sK6))) | (~ (fool @ X0 @ (sK3 @ (sK2 @ sK6)))))) = $true)) )),
% 3.97/0.99 inference(boolean_simplification,[],[f1825])).
% 3.97/0.99 thf(f1827,plain,(
% 3.97/0.99 ( ! [X0 : $i] : (((($false | (~ (fool @ X0 @ (sK3 @ (sK2 @ sK6)))))) = $true)) )),
% 3.97/0.99 inference(forward_demodulation,[],[f1826,f1569])).
% 3.97/0.99 thf(f1828,plain,(
% 3.97/0.99 ( ! [X0 : $i] : ((((~ (fool @ X0 @ (sK3 @ (sK2 @ sK6))))) = $true)) )),
% 3.97/0.99 inference(boolean_simplification,[],[f1827])).
% 3.97/0.99 thf(f1845,plain,(
% 3.97/0.99 ($true = ((~ $true)))),
% 3.97/0.99 inference(constrained_superposition,[],[f1828,f1018])).
% 3.97/0.99 thf(f1850,plain,(
% 3.97/0.99 ($true = $false)),
% 3.97/0.99 inference(boolean_simplification,[],[f1845])).
% 3.97/0.99 thf(f1851,plain,(
% 3.97/0.99 $false),
% 3.97/0.99 inference(trivial_inequality_removal,[],[f1850])).
% 3.97/0.99 % SZS output end Proof for theBenchmark
% 3.97/0.99 % (2834904)------------------------------
% 3.97/0.99 % (2834904)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.97/0.99 % (2834904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.97/0.99 % (2834904)CaDiCaL version: 2.1.3
% 3.97/0.99 % (2834904)Termination reason: Refutation
% 3.97/0.99 % (2834904)Time elapsed: 0.099 s
% 3.97/0.99 % (2834904)Peak memory usage: 13 MB
% 3.97/0.99 % (2834904)Instructions burned: 198 (million)
% 3.97/0.99 % (2834698)Success in time 0.727 s
% 3.97/0.99 % Vampire exiting
%------------------------------------------------------------------------------