%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : PHI007^4 : TPTP v9.3.1. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:20:18 AM UTC 2026
% Result : ContradictoryAxioms 6.96s 1.30s
% Output : Refutation 6.96s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PHI007^4 : TPTP v9.3.1. Released v6.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.05/0.18 % Computer : n013.cluster.edu
% 0.05/0.18 % Model : x86_64 x86_64
% 0.05/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.05/0.18 % Memory : 8046.5625MB
% 0.05/0.18 % OS : Linux 6.8.0-71-generic
% 0.05/0.18 % CPULimit : 300
% 0.05/0.18 % WCLimit : 300
% 0.05/0.18 % DateTime : Tue Sep 29 13:19:22 UTC 2026
% 0.05/0.18 % CPUTime :
% 0.05/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.05/0.22 Running higher-order theorem proving
% 0.05/0.23 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.20/0.35 % (2085120)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.20/0.35 % (2085127)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=2049107842:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.20/0.35 % (2085127)Instruction limit reached!
% 0.20/0.35 % (2085127)------------------------------
% 0.20/0.35 % (2085127)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.35 % (2085127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.35 % (2085127)CaDiCaL version: 2.1.3
% 0.20/0.35 % (2085127)Termination reason: Instruction limit
% 0.20/0.35 % (2085127)Termination phase: Preprocessing 2
% 0.20/0.35 % (2085127)Time elapsed: 0.001 s
% 0.20/0.35 % (2085127)Peak memory usage: 10 MB
% 0.20/0.35 % (2085127)Instructions burned: 3 (million)
% 0.20/0.35 % (2085131)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.20/0.35 % (2085131)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.20/0.35 % (2085125)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=2617330933:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.20/0.35 % (2085126)lrs+10_16_si=on:nwc=1.5:random_seed=2755637468:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.20/0.35 % (2085130)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=3734670218:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.20/0.35 % (2085129)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=2137212457:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.20/0.35 % (2085128)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=3295238750: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.20/0.35 % (2085131)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=2840340316:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.20/0.35 % (2085133)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2672769165:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.20/0.35 % (2085133)Instruction limit reached!
% 0.20/0.35 % (2085133)------------------------------
% 0.20/0.35 % (2085133)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.35 % (2085133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.35 % (2085133)CaDiCaL version: 2.1.3
% 0.20/0.35 % (2085133)Termination reason: Instruction limit
% 0.20/0.35 % (2085133)Termination phase: Preprocessing 3
% 0.20/0.35 % (2085133)Time elapsed: 0.001 s
% 0.20/0.35 % (2085133)Peak memory usage: 10 MB
% 0.20/0.35 % (2085133)Instructions burned: 4 (million)
% 0.20/0.35 % (2085126)Instruction limit reached!
% 0.20/0.35 % (2085126)------------------------------
% 0.20/0.35 % (2085126)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.35 % (2085126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.35 % (2085126)CaDiCaL version: 2.1.3
% 0.20/0.35 % (2085126)Termination reason: Instruction limit
% 0.20/0.35 % (2085126)Termination phase: Saturation
% 0.20/0.35 % (2085126)Time elapsed: 0.009 s
% 0.20/0.35 % (2085126)Peak memory usage: 12 MB
% 0.20/0.35 % (2085126)Instructions burned: 18 (million)
% 0.20/0.35 % (2085129)Instruction limit reached!
% 0.20/0.35 % (2085129)------------------------------
% 0.20/0.35 % (2085129)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.35 % (2085129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.35 % (2085129)CaDiCaL version: 2.1.3
% 0.20/0.35 % (2085129)Termination reason: Instruction limit
% 0.20/0.35 % (2085129)Termination phase: Saturation
% 0.20/0.35 % (2085129)Time elapsed: 0.015 s
% 0.20/0.35 % (2085129)Peak memory usage: 12 MB
% 0.20/0.35 % (2085129)Instructions burned: 25 (million)
% 0.20/0.35 % (2085141)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=823249305:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.80/0.37 % (2085141)Instruction limit reached!
% 0.80/0.37 % (2085141)------------------------------
% 0.80/0.37 % (2085141)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.80/0.37 % (2085141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.80/0.37 % (2085141)CaDiCaL version: 2.1.3
% 0.80/0.37 % (2085141)Termination reason: Instruction limit
% 0.80/0.37 % (2085141)Termination phase: Saturation
% 0.80/0.37 % (2085141)Time elapsed: 0.002 s
% 0.80/0.37 % (2085141)Peak memory usage: 10 MB
% 0.80/0.37 % (2085141)Instructions burned: 8 (million)
% 0.80/0.37 % (2085142)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.80/0.37 % (2085145)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.80/0.37 % (2085145)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.80/0.37 % (2085142)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3990581973:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.80/0.37 % (2085145)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=4028447018: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.80/0.37 % (2085142)Instruction limit reached!
% 0.80/0.37 % (2085142)------------------------------
% 0.80/0.37 % (2085142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.80/0.37 % (2085142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.80/0.37 % (2085142)CaDiCaL version: 2.1.3
% 0.80/0.37 % (2085142)Termination reason: Instruction limit
% 0.80/0.37 % (2085142)Termination phase: Property scanning
% 0.80/0.37 % (2085142)Time elapsed: 0.003 s
% 0.80/0.37 % (2085142)Peak memory usage: 10 MB
% 0.80/0.37 % (2085142)Instructions burned: 7 (million)
% 0.80/0.37 % (2085143)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=2239546150:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.80/0.37 % (2085145)Instruction limit reached!
% 0.80/0.37 % (2085145)------------------------------
% 0.80/0.37 % (2085145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.80/0.37 % (2085145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.80/0.37 % (2085145)CaDiCaL version: 2.1.3
% 0.80/0.37 % (2085145)Termination reason: Instruction limit
% 0.80/0.37 % (2085145)Termination phase: Saturation
% 0.80/0.37 % (2085145)Time elapsed: 0.007 s
% 0.80/0.37 % (2085145)Peak memory usage: 11 MB
% 0.80/0.37 % (2085145)Instructions burned: 30 (million)
% 0.80/0.37 % (2085143)Instruction limit reached!
% 0.80/0.37 % (2085143)------------------------------
% 0.80/0.37 % (2085143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.80/0.37 % (2085143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.80/0.37 % (2085143)CaDiCaL version: 2.1.3
% 0.80/0.37 % (2085143)Termination reason: Instruction limit
% 0.80/0.37 % (2085143)Termination phase: Saturation
% 0.80/0.37 % (2085143)Time elapsed: 0.006 s
% 0.80/0.37 % (2085143)Peak memory usage: 12 MB
% 0.80/0.37 % (2085143)Instructions burned: 12 (million)
% 0.80/0.37 % (2085130)Instruction limit reached!
% 0.80/0.37 % (2085130)------------------------------
% 0.80/0.37 % (2085130)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.80/0.37 % (2085130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.80/0.37 % (2085130)CaDiCaL version: 2.1.3
% 0.80/0.37 % (2085130)Termination reason: Instruction limit
% 0.80/0.37 % (2085130)Termination phase: Saturation
% 0.80/0.37 % (2085130)Time elapsed: 0.041 s
% 0.80/0.37 % (2085130)Peak memory usage: 12 MB
% 0.80/0.37 % (2085130)Instructions burned: 75 (million)
% 0.80/0.37 % (2085150)lrs+10_1_si=on:cs=on:random_seed=2709161566:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.80/0.37 % (2085125)Instruction limit reached!
% 0.80/0.37 % (2085125)------------------------------
% 0.80/0.37 % (2085125)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.80/0.37 % (2085125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.80/0.39 % (2085125)CaDiCaL version: 2.1.3
% 0.80/0.39 % (2085125)Termination reason: Instruction limit
% 0.80/0.39 % (2085125)Termination phase: Saturation
% 0.80/0.39 % (2085125)Time elapsed: 0.048 s
% 0.80/0.39 % (2085125)Peak memory usage: 13 MB
% 0.80/0.39 % (2085125)Instructions burned: 88 (million)
% 0.80/0.39 % (2085150)Instruction limit reached!
% 0.80/0.39 % (2085150)------------------------------
% 0.80/0.39 % (2085150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.80/0.39 % (2085150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.80/0.39 % (2085150)CaDiCaL version: 2.1.3
% 0.80/0.39 % (2085150)Termination reason: Instruction limit
% 0.80/0.39 % (2085150)Termination phase: Saturation
% 0.80/0.39 % (2085150)Time elapsed: 0.003 s
% 0.80/0.39 % (2085150)Peak memory usage: 11 MB
% 0.80/0.39 % (2085150)Instructions burned: 13 (million)
% 0.80/0.39 % (2085148)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=2963961650:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.80/0.39 % (2085151)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.80/0.39 % (2085152)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=191617216:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.80/0.39 % (2085151)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=4053212460:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.80/0.39 % (2085151)Instruction limit reached!
% 0.80/0.39 % (2085151)------------------------------
% 0.80/0.39 % (2085151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.80/0.39 % (2085151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.80/0.39 % (2085151)CaDiCaL version: 2.1.3
% 0.80/0.39 % (2085151)Termination reason: Instruction limit
% 0.80/0.39 % (2085151)Termination phase: Property scanning
% 0.80/0.39 % (2085151)Time elapsed: 0.002 s
% 0.80/0.39 % (2085151)Peak memory usage: 9 MB
% 0.80/0.39 % (2085151)Instructions burned: 4 (million)
% 0.80/0.39 % (2085152)Refutation not found, incomplete strategy
% 0.80/0.39 % (2085152)------------------------------
% 0.80/0.39 % (2085152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.80/0.39 % (2085152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.80/0.39 % (2085152)CaDiCaL version: 2.1.3
% 0.80/0.39 % (2085152)Termination reason: Refutation not found, incomplete strategy
% 0.80/0.39 % (2085152)Time elapsed: 0.002 s
% 0.80/0.39 % (2085152)Peak memory usage: 11 MB
% 0.80/0.39 % (2085152)Instructions burned: 4 (million)
% 0.80/0.39 % (2085156)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=3042570403:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/25Mi)
% 0.80/0.39 % (2085152)------------------------------
% 0.80/0.39 % (2085152)------------------------------
% 0.80/0.39 % (2085156)Refutation not found, incomplete strategy
% 0.80/0.39 % (2085156)------------------------------
% 0.80/0.39 % (2085156)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.80/0.39 % (2085156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.80/0.39 % (2085156)CaDiCaL version: 2.1.3
% 0.80/0.39 % (2085156)Termination reason: Refutation not found, incomplete strategy
% 0.80/0.39 % (2085156)Time elapsed: 0.001 s
% 0.80/0.39 % (2085156)Peak memory usage: 11 MB
% 0.80/0.39 % (2085156)Instructions burned: 4 (million)
% 0.80/0.39 % (2085156)------------------------------
% 0.80/0.39 % (2085156)------------------------------
% 0.80/0.39 % (2085154)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=3444554540:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.80/0.39 % (2085154)Refutation not found, incomplete strategy
% 0.80/0.39 % (2085154)------------------------------
% 0.80/0.39 % (2085154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.80/0.39 % (2085154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.80/0.39 % (2085154)CaDiCaL version: 2.1.3
% 0.80/0.39 % (2085154)Termination reason: Refutation not found, incomplete strategy
% 0.80/0.39 % (2085154)Time elapsed: 0.003 s
% 0.80/0.43 % (2085154)Peak memory usage: 11 MB
% 0.80/0.43 % (2085154)Instructions burned: 4 (million)
% 0.80/0.43 % (2085154)------------------------------
% 0.80/0.43 % (2085154)------------------------------
% 0.80/0.43 % (2085162)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=3120827637:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/14Mi)
% 0.80/0.43 % (2085162)Instruction limit reached!
% 0.80/0.43 % (2085162)------------------------------
% 0.80/0.43 % (2085162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.80/0.43 % (2085162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.80/0.43 % (2085162)CaDiCaL version: 2.1.3
% 0.80/0.43 % (2085162)Termination reason: Instruction limit
% 0.80/0.43 % (2085162)Termination phase: Saturation
% 0.80/0.43 % (2085162)Time elapsed: 0.004 s
% 0.80/0.43 % (2085162)Peak memory usage: 12 MB
% 0.80/0.43 % (2085162)Instructions burned: 14 (million)
% 0.80/0.43 % (2085160)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=1519898528:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2999 on theBenchmark for (2999ds/14Mi)
% 0.80/0.43 % (2085161)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=2132541197:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/327Mi)
% 0.80/0.43 % (2085131)Instruction limit reached!
% 0.80/0.43 % (2085131)------------------------------
% 0.80/0.43 % (2085131)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.80/0.43 % (2085131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.80/0.43 % (2085131)CaDiCaL version: 2.1.3
% 0.80/0.43 % (2085131)Termination reason: Instruction limit
% 0.80/0.43 % (2085131)Termination phase: Saturation
% 0.80/0.43 % (2085131)Time elapsed: 0.082 s
% 0.80/0.43 % (2085131)Peak memory usage: 13 MB
% 0.80/0.43 % (2085131)Instructions burned: 158 (million)
% 0.80/0.43 % (2085161)Refutation not found, incomplete strategy
% 0.80/0.43 % (2085161)------------------------------
% 0.80/0.43 % (2085161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.80/0.43 % (2085161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.80/0.43 % (2085161)CaDiCaL version: 2.1.3
% 0.80/0.43 % (2085161)Termination reason: Refutation not found, incomplete strategy
% 0.80/0.43 % (2085161)Time elapsed: 0.003 s
% 0.80/0.43 % (2085161)Peak memory usage: 12 MB
% 0.80/0.43 % (2085161)Instructions burned: 5 (million)
% 0.80/0.43 % (2085161)------------------------------
% 0.80/0.43 % (2085161)------------------------------
% 0.80/0.43 % (2085160)Instruction limit reached!
% 0.80/0.43 % (2085160)------------------------------
% 0.80/0.43 % (2085160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.80/0.43 % (2085160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.80/0.43 % (2085160)CaDiCaL version: 2.1.3
% 0.80/0.43 % (2085160)Termination reason: Instruction limit
% 0.80/0.43 % (2085160)Termination phase: Saturation
% 0.80/0.43 % (2085160)Time elapsed: 0.007 s
% 0.80/0.43 % (2085160)Peak memory usage: 12 MB
% 0.80/0.43 % (2085160)Instructions burned: 14 (million)
% 0.80/0.43 % (2085166)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=2245258921:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 0.80/0.43 % (2085164)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=3555554683: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.80/0.43 % (2085164)Instruction limit reached!
% 0.80/0.43 % (2085164)------------------------------
% 0.80/0.43 % (2085164)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.80/0.43 % (2085164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.80/0.43 % (2085164)CaDiCaL version: 2.1.3
% 0.80/0.43 % (2085164)Termination reason: Instruction limit
% 0.80/0.43 % (2085164)Termination phase: SInE selection
% 0.80/0.43 % (2085164)Time elapsed: 0.002 s
% 0.80/0.43 % (2085164)Peak memory usage: 10 MB
% 0.80/0.43 % (2085164)Instructions burned: 4 (million)
% 0.80/0.43 % (2085148)Instruction limit reached!
% 0.80/0.43 % (2085148)------------------------------
% 0.80/0.43 % (2085148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.80/0.43 % (2085148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.80/0.43 % (2085148)CaDiCaL version: 2.1.3
% 0.80/0.43 % (2085148)Termination reason: Instruction limit
% 0.80/0.46 % (2085148)Termination phase: Saturation
% 0.80/0.46 % (2085148)Time elapsed: 0.045 s
% 0.80/0.46 % (2085148)Peak memory usage: 12 MB
% 0.80/0.46 % (2085148)Instructions burned: 87 (million)
% 0.80/0.46 % (2085166)Instruction limit reached!
% 0.80/0.46 % (2085166)------------------------------
% 0.80/0.46 % (2085166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.80/0.46 % (2085166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.80/0.46 % (2085166)CaDiCaL version: 2.1.3
% 0.80/0.46 % (2085166)Termination reason: Instruction limit
% 0.80/0.46 % (2085166)Termination phase: Saturation
% 0.80/0.46 % (2085166)Time elapsed: 0.007 s
% 0.80/0.46 % (2085166)Peak memory usage: 12 MB
% 0.80/0.46 % (2085166)Instructions burned: 27 (million)
% 0.80/0.46 % (2085169)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=893112054:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 0.80/0.46 % (2085171)WARNING Broken Constraint: if sine_to_age_generality_threshold(10) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.80/0.46 % (2085171)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 0.80/0.46 % (2085170)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=3720640688:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 0.80/0.46 % (2085171)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=1264015065:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 0.80/0.46 % (2085174)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 0.80/0.46 % (2085176)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=2799485668:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 0.80/0.46 % (2085176)Instruction limit reached!
% 0.80/0.46 % (2085176)------------------------------
% 0.80/0.46 % (2085176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.80/0.46 % (2085176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.80/0.46 % (2085176)CaDiCaL version: 2.1.3
% 0.80/0.46 % (2085176)Termination reason: Instruction limit
% 0.80/0.46 % (2085176)Termination phase: Property scanning
% 0.80/0.46 % (2085176)Time elapsed: 0.002 s
% 0.80/0.46 % (2085176)Peak memory usage: 10 MB
% 0.80/0.46 % (2085176)Instructions burned: 8 (million)
% 0.80/0.46 % (2085174)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=1296169733:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 0.80/0.46 % (2085169)Instruction limit reached!
% 0.80/0.46 % (2085169)------------------------------
% 0.80/0.46 % (2085169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.80/0.46 % (2085169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.80/0.46 % (2085169)CaDiCaL version: 2.1.3
% 0.80/0.46 % (2085169)Termination reason: Instruction limit
% 0.80/0.46 % (2085169)Termination phase: Saturation
% 0.80/0.46 % (2085169)Time elapsed: 0.012 s
% 0.80/0.46 % (2085169)Peak memory usage: 11 MB
% 0.80/0.46 % (2085169)Instructions burned: 23 (million)
% 0.80/0.46 % (2085171)Instruction limit reached!
% 0.80/0.46 % (2085171)------------------------------
% 0.80/0.46 % (2085171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.80/0.46 % (2085171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.80/0.46 % (2085171)CaDiCaL version: 2.1.3
% 0.80/0.46 % (2085171)Termination reason: Instruction limit
% 0.80/0.46 % (2085171)Termination phase: Saturation
% 0.80/0.46 % (2085171)Time elapsed: 0.007 s
% 0.80/0.46 % (2085171)Peak memory usage: 12 MB
% 0.80/0.46 % (2085171)Instructions burned: 15 (million)
% 0.80/0.46 % (2085175)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=247845451:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 0.80/0.46 % (2085174)Instruction limit reached!
% 0.80/0.46 % (2085174)------------------------------
% 0.80/0.46 % (2085174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.55/0.49 % (2085174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.55/0.49 % (2085174)CaDiCaL version: 2.1.3
% 1.55/0.49 % (2085174)Termination reason: Instruction limit
% 1.55/0.49 % (2085174)Termination phase: Property scanning
% 1.55/0.49 % (2085174)Time elapsed: 0.004 s
% 1.55/0.49 % (2085174)Peak memory usage: 11 MB
% 1.55/0.49 % (2085174)Instructions burned: 8 (million)
% 1.55/0.49 % (2085181)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=2512309780:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.55/0.49 % (2085181)Instruction limit reached!
% 1.55/0.49 % (2085181)------------------------------
% 1.55/0.49 % (2085181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.55/0.49 % (2085181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.55/0.49 % (2085181)CaDiCaL version: 2.1.3
% 1.55/0.49 % (2085181)Termination reason: Instruction limit
% 1.55/0.49 % (2085181)Termination phase: Saturation
% 1.55/0.49 % (2085181)Time elapsed: 0.005 s
% 1.55/0.49 % (2085181)Peak memory usage: 11 MB
% 1.55/0.49 % (2085181)Instructions burned: 24 (million)
% 1.55/0.49 % (2085175)Instruction limit reached!
% 1.55/0.49 % (2085175)------------------------------
% 1.55/0.49 % (2085175)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.55/0.49 % (2085175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.55/0.49 % (2085175)CaDiCaL version: 2.1.3
% 1.55/0.49 % (2085175)Termination reason: Instruction limit
% 1.55/0.49 % (2085175)Termination phase: Saturation
% 1.55/0.49 % (2085175)Time elapsed: 0.016 s
% 1.55/0.49 % (2085175)Peak memory usage: 12 MB
% 1.55/0.49 % (2085175)Instructions burned: 31 (million)
% 1.55/0.49 % (2085183)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=320635487:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 1.55/0.49 % (2085185)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=1070965306:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 1.55/0.49 % (2085186)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=3507295432:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/143Mi)
% 1.55/0.49 % (2085188)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=3415602086:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/193Mi)
% 1.55/0.49 % (2085188)Refutation not found, incomplete strategy
% 1.55/0.49 % (2085188)------------------------------
% 1.55/0.49 % (2085188)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.55/0.49 % (2085188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.55/0.49 % (2085188)CaDiCaL version: 2.1.3
% 1.55/0.49 % (2085188)Termination reason: Refutation not found, incomplete strategy
% 1.55/0.49 % (2085188)Time elapsed: 0.001 s
% 1.55/0.49 % (2085188)Peak memory usage: 11 MB
% 1.55/0.49 % (2085188)Instructions burned: 5 (million)
% 1.55/0.49 % (2085188)------------------------------
% 1.55/0.49 % (2085188)------------------------------
% 1.55/0.49 % (2085170)Instruction limit reached!
% 1.55/0.49 % (2085170)------------------------------
% 1.55/0.49 % (2085170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.55/0.49 % (2085170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.55/0.49 % (2085170)CaDiCaL version: 2.1.3
% 1.55/0.49 % (2085170)Termination reason: Instruction limit
% 1.55/0.49 % (2085170)Termination phase: Saturation
% 1.55/0.49 % (2085170)Time elapsed: 0.035 s
% 1.55/0.49 % (2085170)Peak memory usage: 12 MB
% 1.55/0.49 % (2085170)Instructions burned: 61 (million)
% 1.55/0.49 % (2085183)Instruction limit reached!
% 1.55/0.49 % (2085183)------------------------------
% 1.55/0.49 % (2085183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.55/0.49 % (2085183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.55/0.49 % (2085183)CaDiCaL version: 2.1.3
% 1.55/0.49 % (2085183)Termination reason: Instruction limit
% 1.55/0.49 % (2085183)Termination phase: Saturation
% 1.55/0.49 % (2085183)Time elapsed: 0.011 s
% 1.55/0.49 % (2085183)Peak memory usage: 12 MB
% 1.55/0.49 % (2085183)Instructions burned: 21 (million)
% 1.55/0.49 % (2085194)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.49 % (2085194)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=816927195:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2998 on theBenchmark for (2998ds/7Mi)
% 1.55/0.56 % (2085190)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3974820724:i=42:hud=10:rtra=on_2998 on theBenchmark for (2998ds/42Mi)
% 1.55/0.56 % (2085194)Instruction limit reached!
% 1.55/0.56 % (2085194)------------------------------
% 1.55/0.56 % (2085194)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.55/0.56 % (2085194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.55/0.56 % (2085194)CaDiCaL version: 2.1.3
% 1.55/0.56 % (2085194)Termination reason: Instruction limit
% 1.55/0.56 % (2085194)Termination phase: Function definition elimination
% 1.55/0.56 % (2085194)Time elapsed: 0.001 s
% 1.55/0.56 % (2085194)Peak memory usage: 10 MB
% 1.55/0.56 % (2085194)Instructions burned: 7 (million)
% 1.55/0.56 % (2085195)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=4029263438:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/181Mi)
% 1.55/0.56 % (2085199)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 1.55/0.56 % (2085195)Refutation not found, incomplete strategy
% 1.55/0.56 % (2085195)------------------------------
% 1.55/0.56 % (2085195)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.55/0.56 % (2085195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.55/0.56 % (2085195)CaDiCaL version: 2.1.3
% 1.55/0.56 % (2085195)Termination reason: Refutation not found, incomplete strategy
% 1.55/0.56 % (2085195)Time elapsed: 0.002 s
% 1.55/0.56 % (2085195)Peak memory usage: 11 MB
% 1.55/0.56 % (2085195)Instructions burned: 4 (million)
% 1.55/0.56 % (2085195)------------------------------
% 1.55/0.56 % (2085195)------------------------------
% 1.55/0.56 % (2085199)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=533229400:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2998 on theBenchmark for (2998ds/6Mi)
% 1.55/0.56 % (2085196)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=447131431:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/169Mi)
% 1.55/0.56 % (2085199)Instruction limit reached!
% 1.55/0.56 % (2085199)------------------------------
% 1.55/0.56 % (2085199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.55/0.56 % (2085199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.55/0.56 % (2085199)CaDiCaL version: 2.1.3
% 1.55/0.56 % (2085199)Termination reason: Instruction limit
% 1.55/0.56 % (2085199)Termination phase: Saturation
% 1.55/0.56 % (2085199)Time elapsed: 0.003 s
% 1.55/0.56 % (2085199)Peak memory usage: 11 MB
% 1.55/0.56 % (2085199)Instructions burned: 14 (million)
% 1.55/0.56 % (2085196)Refutation not found, incomplete strategy
% 1.55/0.56 % (2085196)------------------------------
% 1.55/0.56 % (2085196)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.55/0.56 % (2085196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.55/0.56 % (2085196)CaDiCaL version: 2.1.3
% 1.55/0.56 % (2085196)Termination reason: Refutation not found, incomplete strategy
% 1.55/0.56 % (2085196)Time elapsed: 0.002 s
% 1.55/0.56 % (2085196)Peak memory usage: 11 MB
% 1.55/0.56 % (2085196)Instructions burned: 4 (million)
% 1.55/0.56 % (2085196)------------------------------
% 1.55/0.56 % (2085196)------------------------------
% 1.55/0.56 % (2085190)Instruction limit reached!
% 1.55/0.56 % (2085190)------------------------------
% 1.55/0.56 % (2085190)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.55/0.56 % (2085190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.55/0.56 % (2085190)CaDiCaL version: 2.1.3
% 1.55/0.56 % (2085190)Termination reason: Instruction limit
% 1.55/0.56 % (2085190)Termination phase: Saturation
% 1.55/0.56 % (2085190)Time elapsed: 0.023 s
% 1.55/0.56 % (2085190)Peak memory usage: 12 MB
% 1.55/0.56 % (2085190)Instructions burned: 44 (million)
% 1.55/0.56 % (2085204)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=1880465593:i=19:add=on:rtra=on_2997 on theBenchmark for (2997ds/19Mi)
% 1.55/0.56 % (2085204)Refutation not found, incomplete strategy
% 2.24/0.62 % (2085204)------------------------------
% 2.24/0.62 % (2085204)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.24/0.62 % (2085204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.24/0.62 % (2085204)CaDiCaL version: 2.1.3
% 2.24/0.62 % (2085204)Termination reason: Refutation not found, incomplete strategy
% 2.24/0.62 % (2085204)Time elapsed: 0.004 s
% 2.24/0.62 % (2085204)Peak memory usage: 13 MB
% 2.24/0.62 % (2085204)Instructions burned: 14 (million)
% 2.24/0.62 % (2085202)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=1733498101:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2998 on theBenchmark for (2998ds/22Mi)
% 2.24/0.62 % (2085204)------------------------------
% 2.24/0.62 % (2085204)------------------------------
% 2.24/0.62 % (2085205)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=813141806:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/316Mi)
% 2.24/0.62 % (2085209)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=1270383445: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.24/0.62 % (2085202)Instruction limit reached!
% 2.24/0.62 % (2085202)------------------------------
% 2.24/0.62 % (2085202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.24/0.62 % (2085202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.24/0.62 % (2085202)CaDiCaL version: 2.1.3
% 2.24/0.62 % (2085202)Termination reason: Instruction limit
% 2.24/0.62 % (2085202)Termination phase: Saturation
% 2.24/0.62 % (2085202)Time elapsed: 0.011 s
% 2.24/0.62 % (2085202)Peak memory usage: 12 MB
% 2.24/0.62 % (2085202)Instructions burned: 24 (million)
% 2.24/0.62 % (2085206)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=3164406645: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.24/0.62 % (2085209)Instruction limit reached!
% 2.24/0.62 % (2085209)------------------------------
% 2.24/0.62 % (2085209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.24/0.62 % (2085209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.24/0.62 % (2085209)CaDiCaL version: 2.1.3
% 2.24/0.62 % (2085209)Termination reason: Instruction limit
% 2.24/0.62 % (2085209)Termination phase: Saturation
% 2.24/0.62 % (2085209)Time elapsed: 0.013 s
% 2.24/0.62 % (2085209)Peak memory usage: 13 MB
% 2.24/0.62 % (2085209)Instructions burned: 45 (million)
% 2.24/0.62 % (2085186)Instruction limit reached!
% 2.24/0.62 % (2085186)------------------------------
% 2.24/0.62 % (2085186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.24/0.62 % (2085186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.24/0.62 % (2085186)CaDiCaL version: 2.1.3
% 2.24/0.62 % (2085186)Termination reason: Instruction limit
% 2.24/0.62 % (2085186)Termination phase: Saturation
% 2.24/0.62 % (2085186)Time elapsed: 0.075 s
% 2.24/0.62 % (2085186)Peak memory usage: 13 MB
% 2.24/0.62 % (2085186)Instructions burned: 143 (million)
% 2.24/0.62 % (2085212)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=3055115440:i=480:rtra=on_2997 on theBenchmark for (2997ds/480Mi)
% 2.24/0.62 % (2085214)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=2176897226: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.24/0.62 % (2085212)Refutation not found, incomplete strategy
% 2.24/0.62 % (2085212)------------------------------
% 2.24/0.62 % (2085212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.24/0.62 % (2085212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.24/0.62 % (2085212)CaDiCaL version: 2.1.3
% 2.24/0.62 % (2085212)Termination reason: Refutation not found, incomplete strategy
% 2.24/0.62 % (2085212)Time elapsed: 0.005 s
% 2.24/0.62 % (2085212)Peak memory usage: 12 MB
% 2.24/0.62 % (2085212)Instructions burned: 9 (million)
% 2.24/0.62 % (2085212)------------------------------
% 2.24/0.62 % (2085212)------------------------------
% 2.73/0.65 % (2085214)Instruction limit reached!
% 2.73/0.65 % (2085214)------------------------------
% 2.73/0.65 % (2085214)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.73/0.65 % (2085214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.73/0.65 % (2085214)CaDiCaL version: 2.1.3
% 2.73/0.65 % (2085214)Termination reason: Instruction limit
% 2.73/0.65 % (2085214)Termination phase: Saturation
% 2.73/0.65 % (2085214)Time elapsed: 0.006 s
% 2.73/0.65 % (2085214)Peak memory usage: 12 MB
% 2.73/0.65 % (2085214)Instructions burned: 22 (million)
% 2.73/0.65 % (2085216)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 2.73/0.65 % (2085216)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=1853170178:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/200Mi)
% 2.73/0.65 % (2085219)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=75030564:i=66:s2at=3:nm=2:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/66Mi)
% 2.73/0.65 % (2085128)Instruction limit reached!
% 2.73/0.65 % (2085128)------------------------------
% 2.73/0.65 % (2085128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.73/0.65 % (2085128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.73/0.65 % (2085128)CaDiCaL version: 2.1.3
% 2.73/0.65 % (2085128)Termination reason: Instruction limit
% 2.73/0.65 % (2085128)Termination phase: Saturation
% 2.73/0.65 % (2085128)Time elapsed: 0.235 s
% 2.73/0.65 % (2085128)Peak memory usage: 13 MB
% 2.73/0.65 % (2085128)Instructions burned: 635 (million)
% 2.73/0.65 % (2085218)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=3134321544:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2997 on theBenchmark for (2997ds/13Mi)
% 2.73/0.65 % (2085218)Instruction limit reached!
% 2.73/0.65 % (2085218)------------------------------
% 2.73/0.65 % (2085218)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.73/0.65 % (2085218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.73/0.65 % (2085218)CaDiCaL version: 2.1.3
% 2.73/0.65 % (2085218)Termination reason: Instruction limit
% 2.73/0.65 % (2085218)Termination phase: Saturation
% 2.73/0.65 % (2085218)Time elapsed: 0.008 s
% 2.73/0.65 % (2085218)Peak memory usage: 12 MB
% 2.73/0.65 % (2085218)Instructions burned: 14 (million)
% 2.73/0.65 % (2085219)Instruction limit reached!
% 2.73/0.65 % (2085219)------------------------------
% 2.73/0.65 % (2085219)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.73/0.65 % (2085219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.73/0.65 % (2085219)CaDiCaL version: 2.1.3
% 2.73/0.65 % (2085219)Termination reason: Instruction limit
% 2.73/0.65 % (2085219)Termination phase: Saturation
% 2.73/0.65 % (2085219)Time elapsed: 0.018 s
% 2.73/0.65 % (2085219)Peak memory usage: 13 MB
% 2.73/0.65 % (2085219)Instructions burned: 68 (million)
% 2.73/0.65 % (2085222)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=3992527919:i=51:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/51Mi)
% 2.73/0.65 % (2085222)Refutation not found, incomplete strategy
% 2.73/0.65 % (2085222)------------------------------
% 2.73/0.65 % (2085222)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.73/0.65 % (2085222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.73/0.65 % (2085222)CaDiCaL version: 2.1.3
% 2.73/0.65 % (2085222)Termination reason: Refutation not found, incomplete strategy
% 2.73/0.65 % (2085222)Time elapsed: 0.006 s
% 2.73/0.65 % (2085222)Peak memory usage: 12 MB
% 2.73/0.65 % (2085222)Instructions burned: 12 (million)
% 2.73/0.65 % (2085222)------------------------------
% 2.73/0.65 % (2085222)------------------------------
% 2.73/0.65 % (2085224)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=1973253949:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/31Mi)
% 2.73/0.65 % (2085225)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=2835746920:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2997 on theBenchmark for (2997ds/137Mi)
% 2.73/0.65 % (2085224)Instruction limit reached!
% 2.73/0.65 % (2085224)------------------------------
% 2.73/0.65 % (2085224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.12/0.70 % (2085224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.12/0.70 % (2085224)CaDiCaL version: 2.1.3
% 3.12/0.70 % (2085224)Termination reason: Instruction limit
% 3.12/0.70 % (2085224)Termination phase: Saturation
% 3.12/0.70 % (2085224)Time elapsed: 0.015 s
% 3.12/0.70 % (2085224)Peak memory usage: 12 MB
% 3.12/0.70 % (2085224)Instructions burned: 31 (million)
% 3.12/0.70 % (2085227)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=378888170:cond=on:i=34:hud=10:nm=10:rtra=on_2997 on theBenchmark for (2997ds/34Mi)
% 3.12/0.70 % (2085216)Instruction limit reached!
% 3.12/0.70 % (2085216)------------------------------
% 3.12/0.70 % (2085216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.12/0.70 % (2085216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.12/0.70 % (2085216)CaDiCaL version: 2.1.3
% 3.12/0.70 % (2085216)Termination reason: Instruction limit
% 3.12/0.70 % (2085216)Termination phase: Saturation
% 3.12/0.70 % (2085216)Time elapsed: 0.063 s
% 3.12/0.70 % (2085216)Peak memory usage: 13 MB
% 3.12/0.70 % (2085216)Instructions burned: 204 (million)
% 3.12/0.70 % (2085230)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=2898096274:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2996 on theBenchmark for (2996ds/67Mi)
% 3.12/0.70 % (2085227)Instruction limit reached!
% 3.12/0.70 % (2085227)------------------------------
% 3.12/0.70 % (2085227)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.12/0.70 % (2085227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.12/0.70 % (2085227)CaDiCaL version: 2.1.3
% 3.12/0.70 % (2085227)Termination reason: Instruction limit
% 3.12/0.70 % (2085227)Termination phase: Saturation
% 3.12/0.70 % (2085227)Time elapsed: 0.019 s
% 3.12/0.70 % (2085227)Peak memory usage: 12 MB
% 3.12/0.70 % (2085227)Instructions burned: 35 (million)
% 3.12/0.70 % (2085232)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 3.12/0.70 % (2085232)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=30708099:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2996 on theBenchmark for (2996ds/180Mi)
% 3.12/0.70 % (2085230)Refutation not found, incomplete strategy
% 3.12/0.70 % (2085230)------------------------------
% 3.12/0.70 % (2085230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.12/0.70 % (2085230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.12/0.70 % (2085230)CaDiCaL version: 2.1.3
% 3.12/0.70 % (2085230)Termination reason: Refutation not found, incomplete strategy
% 3.12/0.70 % (2085230)Time elapsed: 0.006 s
% 3.12/0.70 % (2085230)Peak memory usage: 12 MB
% 3.12/0.70 % (2085230)Instructions burned: 11 (million)
% 3.12/0.70 % (2085230)------------------------------
% 3.12/0.70 % (2085230)------------------------------
% 3.12/0.70 % (2085234)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=2127256499:st=2:i=246:sd=3:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/246Mi)
% 3.12/0.70 % (2085234)Refutation not found, incomplete strategy
% 3.12/0.70 % (2085234)------------------------------
% 3.12/0.70 % (2085234)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.12/0.70 % (2085234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.12/0.70 % (2085234)CaDiCaL version: 2.1.3
% 3.12/0.70 % (2085234)Termination reason: Refutation not found, incomplete strategy
% 3.12/0.70 % (2085234)Time elapsed: 0.002 s
% 3.12/0.70 % (2085234)Peak memory usage: 11 MB
% 3.12/0.70 % (2085234)Instructions burned: 4 (million)
% 3.12/0.70 % (2085234)------------------------------
% 3.12/0.70 % (2085234)------------------------------
% 3.12/0.70 % (2085236)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=2874160456:cond=on:i=96:bd=all:rtra=on_2996 on theBenchmark for (2996ds/96Mi)
% 3.12/0.70 % (2085239)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=3800895923:i=427:sd=1:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/427Mi)
% 3.12/0.70 % (2085239)Refutation not found, incomplete strategy
% 3.12/0.70 % (2085239)------------------------------
% 3.12/0.70 % (2085239)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.12/0.70 % (2085239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.12/0.70 % (2085239)CaDiCaL version: 2.1.3
% 3.12/0.78 % (2085239)Termination reason: Refutation not found, incomplete strategy
% 3.12/0.78 % (2085239)Time elapsed: 0.002 s
% 3.12/0.78 % (2085239)Peak memory usage: 11 MB
% 3.12/0.78 % (2085239)Instructions burned: 4 (million)
% 3.12/0.78 % (2085239)------------------------------
% 3.12/0.78 % (2085239)------------------------------
% 3.12/0.78 % (2085225)Instruction limit reached!
% 3.12/0.78 % (2085225)------------------------------
% 3.12/0.78 % (2085225)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.12/0.78 % (2085225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.12/0.78 % (2085225)CaDiCaL version: 2.1.3
% 3.12/0.78 % (2085225)Termination reason: Instruction limit
% 3.12/0.78 % (2085225)Termination phase: Saturation
% 3.12/0.78 % (2085225)Time elapsed: 0.075 s
% 3.12/0.78 % (2085225)Peak memory usage: 13 MB
% 3.12/0.78 % (2085225)Instructions burned: 138 (million)
% 3.12/0.78 % (2085232)Instruction limit reached!
% 3.12/0.78 % (2085232)------------------------------
% 3.12/0.78 % (2085232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.12/0.78 % (2085232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.12/0.78 % (2085232)CaDiCaL version: 2.1.3
% 3.12/0.78 % (2085232)Termination reason: Instruction limit
% 3.12/0.78 % (2085232)Termination phase: Saturation
% 3.12/0.78 % (2085232)Time elapsed: 0.043 s
% 3.12/0.78 % (2085232)Peak memory usage: 13 MB
% 3.12/0.78 % (2085232)Instructions burned: 183 (million)
% 3.12/0.78 % (2085205)Instruction limit reached!
% 3.12/0.78 % (2085205)------------------------------
% 3.12/0.78 % (2085205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.12/0.78 % (2085205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.12/0.78 % (2085205)CaDiCaL version: 2.1.3
% 3.12/0.78 % (2085205)Termination reason: Instruction limit
% 3.12/0.78 % (2085205)Termination phase: Saturation
% 3.12/0.78 % (2085205)Time elapsed: 0.166 s
% 3.12/0.78 % (2085205)Peak memory usage: 15 MB
% 3.12/0.78 % (2085205)Instructions burned: 317 (million)
% 3.12/0.78 % (2085243)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=2917105831:st=1.5:i=130:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/130Mi)
% 3.12/0.78 % (2085241)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=3998968500:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/874Mi)
% 3.12/0.78 % (2085242)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=3818861592:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/515Mi)
% 3.12/0.78 % (2085241)Refutation not found, incomplete strategy
% 3.12/0.78 % (2085241)------------------------------
% 3.12/0.78 % (2085241)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.12/0.78 % (2085241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.12/0.78 % (2085241)CaDiCaL version: 2.1.3
% 3.12/0.78 % (2085241)Termination reason: Refutation not found, incomplete strategy
% 3.12/0.78 % (2085241)Time elapsed: 0.003 s
% 3.12/0.78 % (2085241)Peak memory usage: 11 MB
% 3.12/0.78 % (2085241)Instructions burned: 5 (million)
% 3.12/0.78 % (2085242)Refutation not found, incomplete strategy
% 3.12/0.78 % (2085242)------------------------------
% 3.12/0.78 % (2085242)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.12/0.78 % (2085242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.12/0.78 % (2085242)CaDiCaL version: 2.1.3
% 3.12/0.78 % (2085242)Termination reason: Refutation not found, incomplete strategy
% 3.12/0.78 % (2085242)Time elapsed: 0.003 s
% 3.12/0.78 % (2085242)Peak memory usage: 12 MB
% 3.12/0.78 % (2085242)Instructions burned: 5 (million)
% 3.12/0.78 % (2085241)------------------------------
% 3.12/0.78 % (2085241)------------------------------
% 3.12/0.78 % (2085236)Instruction limit reached!
% 3.12/0.78 % (2085236)------------------------------
% 3.12/0.78 % (2085236)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.12/0.78 % (2085236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.12/0.78 % (2085236)CaDiCaL version: 2.1.3
% 3.12/0.78 % (2085236)Termination reason: Instruction limit
% 3.12/0.78 % (2085236)Termination phase: Saturation
% 3.12/0.78 % (2085236)Time elapsed: 0.045 s
% 3.12/0.78 % (2085236)Peak memory usage: 12 MB
% 3.12/0.78 % (2085236)Instructions burned: 97 (million)
% 3.12/0.78 % (2085242)------------------------------
% 3.12/0.78 % (2085242)------------------------------
% 3.12/0.78 % (2085244)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3155877910:i=44:ep=R:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/44Mi)
% 3.68/0.84 % (2085248)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=1582904352:s2a=on:i=571:nm=16:rtra=on_2995 on theBenchmark for (2995ds/571Mi)
% 3.68/0.84 % (2085249)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=198321365:i=450:rtra=on:ixr=off:ntd=on_2995 on theBenchmark for (2995ds/450Mi)
% 3.68/0.84 % (2085250)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=3729228004:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/95Mi)
% 3.68/0.84 % (2085243)Instruction limit reached!
% 3.68/0.84 % (2085243)------------------------------
% 3.68/0.84 % (2085243)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.68/0.84 % (2085243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.68/0.84 % (2085248)Refutation not found, incomplete strategy
% 3.68/0.84 % (2085248)------------------------------
% 3.68/0.84 % (2085248)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.68/0.84 % (2085243)CaDiCaL version: 2.1.3
% 3.68/0.84 % (2085243)Termination reason: Instruction limit
% 3.68/0.84 % (2085243)Termination phase: Saturation
% 3.68/0.84 % (2085243)Time elapsed: 0.035 s
% 3.68/0.84 % (2085248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.68/0.84 % (2085243)Peak memory usage: 12 MB
% 3.68/0.84 % (2085243)Instructions burned: 130 (million)
% 3.68/0.84 % (2085248)CaDiCaL version: 2.1.3
% 3.68/0.84 % (2085248)Termination reason: Refutation not found, incomplete strategy
% 3.68/0.84 % (2085248)Time elapsed: 0.005 s
% 3.68/0.84 % (2085248)Peak memory usage: 12 MB
% 3.68/0.84 % (2085248)Instructions burned: 9 (million)
% 3.68/0.84 % (2085248)------------------------------
% 3.68/0.84 % (2085248)------------------------------
% 3.68/0.84 % (2085244)Instruction limit reached!
% 3.68/0.84 % (2085244)------------------------------
% 3.68/0.84 % (2085244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.68/0.84 % (2085244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.68/0.84 % (2085244)CaDiCaL version: 2.1.3
% 3.68/0.84 % (2085244)Termination reason: Instruction limit
% 3.68/0.84 % (2085244)Termination phase: Saturation
% 3.68/0.84 % (2085244)Time elapsed: 0.023 s
% 3.68/0.84 % (2085244)Peak memory usage: 12 MB
% 3.68/0.84 % (2085244)Instructions burned: 45 (million)
% 3.68/0.84 % (2085255)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=1390199670:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2995 on theBenchmark for (2995ds/65Mi)
% 3.68/0.84 % (2085256)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=1229857782: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.68/0.84 % (2085257)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=386862315: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.68/0.84 % (2085257)Refutation not found, incomplete strategy
% 3.68/0.84 % (2085257)------------------------------
% 3.68/0.84 % (2085257)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.68/0.84 % (2085257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.68/0.84 % (2085257)CaDiCaL version: 2.1.3
% 3.68/0.84 % (2085257)Termination reason: Refutation not found, incomplete strategy
% 3.68/0.84 % (2085257)Time elapsed: 0.003 s
% 3.68/0.84 % (2085257)Peak memory usage: 12 MB
% 3.68/0.84 % (2085257)Instructions burned: 4 (million)
% 3.68/0.84 % (2085257)------------------------------
% 3.68/0.84 % (2085257)------------------------------
% 3.68/0.84 % (2085255)Instruction limit reached!
% 3.68/0.84 % (2085255)------------------------------
% 3.68/0.84 % (2085255)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.68/0.84 % (2085255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.68/0.84 % (2085255)CaDiCaL version: 2.1.3
% 3.68/0.84 % (2085255)Termination reason: Instruction limit
% 4.35/0.92 % (2085255)Termination phase: Saturation
% 4.35/0.92 % (2085255)Time elapsed: 0.017 s
% 4.35/0.92 % (2085255)Peak memory usage: 12 MB
% 4.35/0.92 % (2085255)Instructions burned: 68 (million)
% 4.35/0.92 % (2085262)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=1836171832:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2995 on theBenchmark for (2995ds/495Mi)
% 4.35/0.92 % (2085261)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=4141455820:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/375Mi)
% 4.35/0.92 % (2085261)Refutation not found, incomplete strategy
% 4.35/0.92 % (2085261)------------------------------
% 4.35/0.92 % (2085261)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.35/0.92 % (2085261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.35/0.92 % (2085261)CaDiCaL version: 2.1.3
% 4.35/0.92 % (2085261)Termination reason: Refutation not found, incomplete strategy
% 4.35/0.92 % (2085261)Time elapsed: 0.002 s
% 4.35/0.92 % (2085261)Peak memory usage: 11 MB
% 4.35/0.92 % (2085261)Instructions burned: 4 (million)
% 4.35/0.92 % (2085250)Instruction limit reached!
% 4.35/0.92 % (2085250)------------------------------
% 4.35/0.92 % (2085250)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.35/0.92 % (2085250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.35/0.92 % (2085250)CaDiCaL version: 2.1.3
% 4.35/0.92 % (2085250)Termination reason: Instruction limit
% 4.35/0.92 % (2085250)Termination phase: Saturation
% 4.35/0.92 % (2085250)Time elapsed: 0.052 s
% 4.35/0.92 % (2085250)Peak memory usage: 13 MB
% 4.35/0.92 % (2085250)Instructions burned: 97 (million)
% 4.35/0.92 % (2085261)------------------------------
% 4.35/0.92 % (2085261)------------------------------
% 4.35/0.92 % (2085265)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=2711890192:cond=on:i=34:hud=10:nm=10:rtra=on_2995 on theBenchmark for (2995ds/34Mi)
% 4.35/0.92 % (2085266)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=1210221796:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2995 on theBenchmark for (2995ds/91Mi)
% 4.35/0.92 % (2085256)Instruction limit reached!
% 4.35/0.92 % (2085256)------------------------------
% 4.35/0.92 % (2085256)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.35/0.92 % (2085256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.35/0.92 % (2085256)CaDiCaL version: 2.1.3
% 4.35/0.92 % (2085256)Termination reason: Instruction limit
% 4.35/0.92 % (2085256)Termination phase: Saturation
% 4.35/0.92 % (2085256)Time elapsed: 0.056 s
% 4.35/0.92 % (2085256)Peak memory usage: 13 MB
% 4.35/0.92 % (2085256)Instructions burned: 106 (million)
% 4.35/0.92 % (2085265)Instruction limit reached!
% 4.35/0.92 % (2085265)------------------------------
% 4.35/0.92 % (2085265)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.35/0.92 % (2085265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.35/0.92 % (2085265)CaDiCaL version: 2.1.3
% 4.35/0.92 % (2085265)Termination reason: Instruction limit
% 4.35/0.92 % (2085265)Termination phase: Saturation
% 4.35/0.92 % (2085265)Time elapsed: 0.019 s
% 4.35/0.92 % (2085265)Peak memory usage: 12 MB
% 4.35/0.92 % (2085265)Instructions burned: 36 (million)
% 4.35/0.92 % (2085269)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=85266276: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)
% 4.35/0.92 % (2085269)Refutation not found, incomplete strategy
% 4.35/0.92 % (2085269)------------------------------
% 4.35/0.92 % (2085269)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.35/0.92 % (2085269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.35/0.92 % (2085269)CaDiCaL version: 2.1.3
% 4.35/0.92 % (2085269)Termination reason: Refutation not found, incomplete strategy
% 4.35/0.92 % (2085269)Time elapsed: 0.002 s
% 4.35/0.92 % (2085269)Peak memory usage: 11 MB
% 4.35/0.92 % (2085269)Instructions burned: 4 (million)
% 4.35/0.92 % (2085269)------------------------------
% 4.35/0.92 % (2085269)------------------------------
% 4.35/0.92 % (2085270)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=2694347882:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2994 on theBenchmark for (2994ds/22Mi)
% 4.35/0.92 % (2085206)Instruction limit reached!
% 4.35/1.00 % (2085206)------------------------------
% 4.35/1.00 % (2085206)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.35/1.00 % (2085206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.35/1.00 % (2085206)CaDiCaL version: 2.1.3
% 4.35/1.00 % (2085206)Termination reason: Instruction limit
% 4.35/1.00 % (2085206)Termination phase: Saturation
% 4.35/1.00 % (2085206)Time elapsed: 0.305 s
% 4.35/1.00 % (2085206)Peak memory usage: 14 MB
% 4.35/1.00 % (2085206)Instructions burned: 853 (million)
% 4.35/1.00 % (2085266)Instruction limit reached!
% 4.35/1.00 % (2085266)------------------------------
% 4.35/1.00 % (2085266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.35/1.00 % (2085266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.35/1.00 % (2085266)CaDiCaL version: 2.1.3
% 4.35/1.00 % (2085266)Termination reason: Instruction limit
% 4.35/1.00 % (2085266)Termination phase: Saturation
% 4.35/1.00 % (2085266)Time elapsed: 0.046 s
% 4.35/1.00 % (2085266)Peak memory usage: 13 MB
% 4.35/1.00 % (2085266)Instructions burned: 92 (million)
% 4.35/1.00 % (2085270)Instruction limit reached!
% 4.35/1.00 % (2085270)------------------------------
% 4.35/1.00 % (2085270)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.35/1.00 % (2085270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.35/1.00 % (2085270)CaDiCaL version: 2.1.3
% 4.35/1.00 % (2085270)Termination reason: Instruction limit
% 4.35/1.00 % (2085270)Termination phase: Saturation
% 4.35/1.00 % (2085270)Time elapsed: 0.011 s
% 4.35/1.00 % (2085270)Peak memory usage: 12 MB
% 4.35/1.00 % (2085270)Instructions burned: 22 (million)
% 4.35/1.00 % (2085272)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=1858575381:i=338:bd=all:ins=4:rtra=on_2994 on theBenchmark for (2994ds/338Mi)
% 4.35/1.00 % (2085274)lrs+10_1_sil=128000:si=on:urr=on:random_seed=1569415392:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2994 on theBenchmark for (2994ds/28Mi)
% 4.35/1.00 % (2085274)Refutation not found, incomplete strategy
% 4.35/1.00 % (2085274)------------------------------
% 4.35/1.00 % (2085274)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.35/1.00 % (2085274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.35/1.00 % (2085274)CaDiCaL version: 2.1.3
% 4.35/1.00 % (2085274)Termination reason: Refutation not found, incomplete strategy
% 4.35/1.00 % (2085274)Time elapsed: 0.002 s
% 4.35/1.00 % (2085274)Peak memory usage: 11 MB
% 4.35/1.00 % (2085274)Instructions burned: 4 (million)
% 4.35/1.00 % (2085274)------------------------------
% 4.35/1.00 % (2085274)------------------------------
% 4.35/1.00 % (2085275)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 4.35/1.00 % (2085275)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=2027522537: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)
% 4.35/1.00 % (2085276)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=772685386:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2994 on theBenchmark for (2994ds/340Mi)
% 4.35/1.00 % (2085279)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=3436624572:i=227:sd=1:bd=all:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/227Mi)
% 4.35/1.00 % (2085279)Refutation not found, incomplete strategy
% 4.35/1.00 % (2085279)------------------------------
% 4.35/1.00 % (2085279)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.35/1.00 % (2085279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.35/1.00 % (2085279)CaDiCaL version: 2.1.3
% 4.35/1.00 % (2085279)Termination reason: Refutation not found, incomplete strategy
% 4.35/1.00 % (2085279)Time elapsed: 0.002 s
% 4.35/1.00 % (2085279)Peak memory usage: 11 MB
% 4.35/1.00 % (2085279)Instructions burned: 4 (million)
% 4.35/1.00 % (2085279)------------------------------
% 4.35/1.00 % (2085279)------------------------------
% 4.35/1.00 % (2085283)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 4.35/1.00 % (2085283)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=2986610329:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/373Mi)
% 5.57/1.05 % (2085262)Instruction limit reached!
% 5.57/1.05 % (2085262)------------------------------
% 5.57/1.05 % (2085262)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.57/1.05 % (2085262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.57/1.05 % (2085262)CaDiCaL version: 2.1.3
% 5.57/1.05 % (2085262)Termination reason: Instruction limit
% 5.57/1.05 % (2085262)Termination phase: Saturation
% 5.57/1.05 % (2085262)Time elapsed: 0.132 s
% 5.57/1.05 % (2085262)Peak memory usage: 16 MB
% 5.57/1.05 % (2085262)Instructions burned: 498 (million)
% 5.57/1.05 % (2085285)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=4108089881:i=116:ep=RSTC:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/116Mi)
% 5.57/1.05 % (2085275)Instruction limit reached!
% 5.57/1.05 % (2085275)------------------------------
% 5.57/1.05 % (2085275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.57/1.05 % (2085275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.57/1.05 % (2085275)CaDiCaL version: 2.1.3
% 5.57/1.05 % (2085275)Termination reason: Instruction limit
% 5.57/1.05 % (2085275)Termination phase: Saturation
% 5.57/1.05 % (2085275)Time elapsed: 0.070 s
% 5.57/1.05 % (2085275)Peak memory usage: 13 MB
% 5.57/1.05 % (2085275)Instructions burned: 138 (million)
% 5.57/1.05 % (2085249)Instruction limit reached!
% 5.57/1.05 % (2085249)------------------------------
% 5.57/1.05 % (2085249)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.57/1.05 % (2085249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.57/1.05 % (2085249)CaDiCaL version: 2.1.3
% 5.57/1.05 % (2085249)Termination reason: Instruction limit
% 5.57/1.05 % (2085249)Termination phase: Saturation
% 5.57/1.05 % (2085249)Time elapsed: 0.220 s
% 5.57/1.05 % (2085249)Peak memory usage: 13 MB
% 5.57/1.05 % (2085249)Instructions burned: 451 (million)
% 5.57/1.05 % (2085285)Instruction limit reached!
% 5.57/1.05 % (2085285)------------------------------
% 5.57/1.05 % (2085285)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.57/1.05 % (2085285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.57/1.05 % (2085285)CaDiCaL version: 2.1.3
% 5.57/1.05 % (2085285)Termination reason: Instruction limit
% 5.57/1.05 % (2085285)Termination phase: Saturation
% 5.57/1.05 % (2085285)Time elapsed: 0.032 s
% 5.57/1.05 % (2085285)Peak memory usage: 12 MB
% 5.57/1.05 % (2085285)Instructions burned: 117 (million)
% 5.57/1.05 % (2085287)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=3843397739:i=575:rtra=on_2993 on theBenchmark for (2993ds/575Mi)
% 5.57/1.05 % (2085288)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=2966565141:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2993 on theBenchmark for (2993ds/270Mi)
% 5.57/1.05 % (2085287)Refutation not found, incomplete strategy
% 5.57/1.05 % (2085287)------------------------------
% 5.57/1.05 % (2085287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.57/1.05 % (2085287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.57/1.05 % (2085287)CaDiCaL version: 2.1.3
% 5.57/1.05 % (2085287)Termination reason: Refutation not found, incomplete strategy
% 5.57/1.05 % (2085287)Time elapsed: 0.006 s
% 5.57/1.05 % (2085287)Peak memory usage: 12 MB
% 5.57/1.05 % (2085287)Instructions burned: 12 (million)
% 5.57/1.05 % (2085287)------------------------------
% 5.57/1.05 % (2085287)------------------------------
% 5.57/1.05 % (2085289)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=3592704865:hsq=on:hsqr=16,1:s2a=on:i=9840:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2993 on theBenchmark for (2993ds/9840Mi)
% 5.57/1.05 % (2085292)lrs+1010_1_sil=128000:si=on:sos=all:uwa=off:nwc=1:random_seed=1330603536:i=421:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/421Mi)
% 5.57/1.05 % (2085292)Refutation not found, incomplete strategy
% 5.57/1.05 % (2085292)------------------------------
% 5.57/1.05 % (2085292)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.57/1.05 % (2085292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.57/1.09 % (2085292)CaDiCaL version: 2.1.3
% 5.57/1.09 % (2085292)Termination reason: Refutation not found, incomplete strategy
% 5.57/1.09 % (2085292)Time elapsed: 0.002 s
% 5.57/1.09 % (2085292)Peak memory usage: 11 MB
% 5.57/1.09 % (2085292)Instructions burned: 4 (million)
% 5.57/1.09 % (2085292)------------------------------
% 5.57/1.09 % (2085292)------------------------------
% 5.57/1.09 % (2085295)WARNING Broken Constraint: if sine_to_age_tolerance(3) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 5.57/1.09 % (2085295)lrs+10_40_sil=128000:tgt=full:cnfonf=off:si=on:sp=reverse_frequency:spb=goal_then_units:uwa=off:fd=preordered:nwc=1:random_seed=555977688:avsq=on:i=270:s2at=3:avsqr=1,16:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/270Mi)
% 5.57/1.09 % (2085272)Instruction limit reached!
% 5.57/1.09 % (2085272)------------------------------
% 5.57/1.09 % (2085272)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.57/1.09 % (2085272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.57/1.09 % (2085272)CaDiCaL version: 2.1.3
% 5.57/1.09 % (2085272)Termination reason: Instruction limit
% 5.57/1.09 % (2085272)Termination phase: Saturation
% 5.57/1.09 % (2085272)Time elapsed: 0.162 s
% 5.57/1.09 % (2085272)Peak memory usage: 14 MB
% 5.57/1.09 % (2085272)Instructions burned: 338 (million)
% 5.57/1.09 % (2085288)Instruction limit reached!
% 5.57/1.09 % (2085288)------------------------------
% 5.57/1.09 % (2085288)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.57/1.09 % (2085288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.57/1.09 % (2085288)CaDiCaL version: 2.1.3
% 5.57/1.09 % (2085288)Termination reason: Instruction limit
% 5.57/1.09 % (2085288)Termination phase: Saturation
% 5.57/1.09 % (2085288)Time elapsed: 0.069 s
% 5.57/1.09 % (2085288)Peak memory usage: 14 MB
% 5.57/1.09 % (2085288)Instructions burned: 274 (million)
% 5.57/1.09 % (2085297)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=3414722525:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2992 on theBenchmark for (2992ds/31Mi)
% 5.57/1.09 % (2085298)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 5.57/1.09 % (2085298)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
% 5.57/1.09 % (2085298)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=2229825117:hsqr=1,8:i=1440:s2at=5:add=on:nm=2:rtra=on_2992 on theBenchmark for (2992ds/1440Mi)
% 5.57/1.09 % (2085276)Instruction limit reached!
% 5.57/1.09 % (2085276)------------------------------
% 5.57/1.09 % (2085276)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.57/1.09 % (2085276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.57/1.09 % (2085276)CaDiCaL version: 2.1.3
% 5.57/1.09 % (2085276)Termination reason: Instruction limit
% 5.57/1.09 % (2085276)Termination phase: Saturation
% 5.57/1.09 % (2085276)Time elapsed: 0.174 s
% 5.57/1.09 % (2085276)Peak memory usage: 15 MB
% 5.57/1.09 % (2085276)Instructions burned: 341 (million)
% 5.57/1.09 % (2085297)Instruction limit reached!
% 5.57/1.09 % (2085297)------------------------------
% 5.57/1.09 % (2085297)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.57/1.09 % (2085297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.57/1.09 % (2085297)CaDiCaL version: 2.1.3
% 5.57/1.09 % (2085297)Termination reason: Instruction limit
% 5.57/1.09 % (2085297)Termination phase: Saturation
% 5.57/1.09 % (2085297)Time elapsed: 0.016 s
% 5.57/1.09 % (2085297)Peak memory usage: 12 MB
% 5.57/1.09 % (2085297)Instructions burned: 32 (million)
% 5.57/1.09 % (2085301)dis+10_2_sil=128000:si=on:random_seed=2062158318:s2a=on:i=339:av=off:rtra=on:fe=abstraction:ss=axioms:fsd=on:ntd=on_2992 on theBenchmark for (2992ds/339Mi)
% 5.57/1.09 % (2085301)Refutation not found, incomplete strategy
% 5.57/1.09 % (2085301)------------------------------
% 5.57/1.09 % (2085301)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.57/1.09 % (2085301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.57/1.09 % (2085301)CaDiCaL version: 2.1.3
% 6.32/1.26 % (2085301)Termination reason: Refutation not found, incomplete strategy
% 6.32/1.26 % (2085301)Time elapsed: 0.003 s
% 6.32/1.26 % (2085301)Peak memory usage: 11 MB
% 6.32/1.26 % (2085301)Instructions burned: 4 (million)
% 6.32/1.26 % (2085301)------------------------------
% 6.32/1.26 % (2085301)------------------------------
% 6.32/1.26 % (2085302)lrs+2_16:1_si=on:cbe=off:uwa=interpreted_only:random_seed=861212635:i=111:add=on:fgj=on:rtra=on:fdi=1024_2992 on theBenchmark for (2992ds/111Mi)
% 6.32/1.26 % (2085185)Instruction limit reached!
% 6.32/1.26 % (2085185)------------------------------
% 6.32/1.26 % (2085185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.32/1.26 % (2085185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.32/1.26 % (2085185)CaDiCaL version: 2.1.3
% 6.32/1.26 % (2085185)Termination reason: Instruction limit
% 6.32/1.26 % (2085185)Termination phase: Saturation
% 6.32/1.26 % (2085185)Time elapsed: 0.603 s
% 6.32/1.26 % (2085185)Peak memory usage: 15 MB
% 6.32/1.26 % (2085185)Instructions burned: 1242 (million)
% 6.32/1.26 % (2085283)Instruction limit reached!
% 6.32/1.26 % (2085283)------------------------------
% 6.32/1.26 % (2085283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.32/1.26 % (2085283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.32/1.26 % (2085283)CaDiCaL version: 2.1.3
% 6.32/1.26 % (2085283)Termination reason: Instruction limit
% 6.32/1.26 % (2085283)Termination phase: Saturation
% 6.32/1.26 % (2085283)Time elapsed: 0.176 s
% 6.32/1.26 % (2085283)Peak memory usage: 15 MB
% 6.32/1.26 % (2085283)Instructions burned: 373 (million)
% 6.32/1.26 % (2085304)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=1179959835:st=3:avsq=on:i=122:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2992 on theBenchmark for (2992ds/122Mi)
% 6.32/1.26 % (2085304)Refutation not found, incomplete strategy
% 6.32/1.26 % (2085304)------------------------------
% 6.32/1.26 % (2085304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.32/1.26 % (2085304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.32/1.26 % (2085304)CaDiCaL version: 2.1.3
% 6.32/1.26 % (2085304)Termination reason: Refutation not found, incomplete strategy
% 6.32/1.26 % (2085304)Time elapsed: 0.003 s
% 6.32/1.26 % (2085304)Peak memory usage: 12 MB
% 6.32/1.26 % (2085304)Instructions burned: 4 (million)
% 6.32/1.26 % (2085304)------------------------------
% 6.32/1.26 % (2085304)------------------------------
% 6.32/1.26 % (2085306)dis+1010_3:2_anc=all_dependent:sil=128000:si=on:sos=on:lma=off:spb=goal_then_units:bce=on:fd=off:random_seed=3092525448:uwa_fpi=on:avsq=on:i=136:avsqr=1,32:hud=15:nm=0:rtra=on:ntd=on_2992 on theBenchmark for (2992ds/136Mi)
% 6.32/1.26 % (2085307)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=3101069479:hsq=on:st=2:i=232:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2992 on theBenchmark for (2992ds/232Mi)
% 6.32/1.26 % (2085307)Refutation not found, incomplete strategy
% 6.32/1.26 % (2085307)------------------------------
% 6.32/1.26 % (2085307)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.32/1.26 % (2085307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.32/1.26 % (2085307)CaDiCaL version: 2.1.3
% 6.32/1.26 % (2085307)Termination reason: Refutation not found, incomplete strategy
% 6.32/1.26 % (2085307)Time elapsed: 0.002 s
% 6.32/1.26 % (2085307)Peak memory usage: 12 MB
% 6.32/1.26 % (2085307)Instructions burned: 4 (million)
% 6.32/1.26 % (2085307)------------------------------
% 6.32/1.26 % (2085307)------------------------------
% 6.32/1.26 % (2085306)Refutation not found, incomplete strategy
% 6.32/1.26 % (2085306)------------------------------
% 6.32/1.26 % (2085306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.32/1.26 % (2085306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.32/1.26 % (2085306)CaDiCaL version: 2.1.3
% 6.32/1.26 % (2085306)Termination reason: Refutation not found, incomplete strategy
% 6.32/1.26 % (2085306)Time elapsed: 0.006 s
% 6.32/1.26 % (2085306)Peak memory usage: 12 MB
% 6.32/1.26 % (2085306)Instructions burned: 11 (million)
% 6.32/1.26 % (2085306)------------------------------
% 6.32/1.26 % (2085306)------------------------------
% 6.32/1.26 % (2085309)lrs+1010_8:1_sil=128000:tgt=ground:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:sos=on:plsqr=256,1:uwa=off:random_seed=2502182025:i=1254:kws=precedence:bd=preordered:av=off:rtra=on_2992 on theBenchmark for (2992ds/1254Mi)
% 6.96/1.30 % (2085312)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 6.96/1.30 % (2085309)Refutation not found, incomplete strategy
% 6.96/1.30 % (2085309)------------------------------
% 6.96/1.30 % (2085309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.96/1.30 % (2085309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.30 % (2085309)CaDiCaL version: 2.1.3
% 6.96/1.30 % (2085309)Termination reason: Refutation not found, incomplete strategy
% 6.96/1.30 % (2085309)Time elapsed: 0.007 s
% 6.96/1.30 % (2085309)Peak memory usage: 12 MB
% 6.96/1.30 % (2085309)Instructions burned: 14 (million)
% 6.96/1.30 % (2085309)------------------------------
% 6.96/1.30 % (2085309)------------------------------
% 6.96/1.30 % (2085312)dis+1002_5:4_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_simp:si=on:plsqr=878,253:plsql=on:uwa=interpreted_only:lwlo=on:random_seed=3223846210:s2a=on:i=281:add=on:rtra=on:fe=axiom:fdi=1024_2992 on theBenchmark for (2992ds/281Mi)
% 6.96/1.30 % (2085313)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=5073342:i=619:add=on:rtra=on_2991 on theBenchmark for (2991ds/619Mi)
% 6.96/1.30 % (2085302)Instruction limit reached!
% 6.96/1.30 % (2085302)------------------------------
% 6.96/1.30 % (2085302)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.96/1.30 % (2085302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.30 % (2085302)CaDiCaL version: 2.1.3
% 6.96/1.30 % (2085302)Termination reason: Instruction limit
% 6.96/1.30 % (2085302)Termination phase: Saturation
% 6.96/1.30 % (2085302)Time elapsed: 0.058 s
% 6.96/1.30 % (2085302)Peak memory usage: 12 MB
% 6.96/1.30 % (2085302)Instructions burned: 112 (million)
% 6.96/1.30 % (2085313)Refutation not found, incomplete strategy
% 6.96/1.30 % (2085313)------------------------------
% 6.96/1.30 % (2085313)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.96/1.30 % (2085313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.30 % (2085313)CaDiCaL version: 2.1.3
% 6.96/1.30 % (2085313)Termination reason: Refutation not found, incomplete strategy
% 6.96/1.30 % (2085313)Time elapsed: 0.007 s
% 6.96/1.30 % (2085313)Peak memory usage: 12 MB
% 6.96/1.30 % (2085313)Instructions burned: 14 (million)
% 6.96/1.30 % (2085313)------------------------------
% 6.96/1.30 % (2085313)------------------------------
% 6.96/1.30 % (2085315)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=2132922757:i=865:bs=unit_only:ins=25:rtra=on:ntd=on_2991 on theBenchmark for (2991ds/865Mi)
% 6.96/1.30 % (2085295)Instruction limit reached!
% 6.96/1.30 % (2085295)------------------------------
% 6.96/1.30 % (2085295)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.96/1.30 % (2085295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.30 % (2085295)CaDiCaL version: 2.1.3
% 6.96/1.30 % (2085295)Termination reason: Instruction limit
% 6.96/1.30 % (2085295)Termination phase: Saturation
% 6.96/1.30 % (2085295)Time elapsed: 0.136 s
% 6.96/1.30 % (2085295)Peak memory usage: 13 MB
% 6.96/1.30 % (2085295)Instructions burned: 271 (million)
% 6.96/1.30 % (2085318)lrs+10_1_sil=128000:si=on:urr=on:random_seed=79478409:i=212:sd=1:rtra=on:ss=axioms:sgt=64_2991 on theBenchmark for (2991ds/212Mi)
% 6.96/1.30 % (2085319)lrs+1010_64_sil=128000:si=on:avsql=on:uwa=off:random_seed=499757819:hsq=on:st=3:avsq=on:i=130:avsqr=1,16:sd=1:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/130Mi)
% 6.96/1.30 % (2085318)Refutation not found, incomplete strategy
% 6.96/1.30 % (2085318)------------------------------
% 6.96/1.30 % (2085318)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.96/1.30 % (2085318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.30 % (2085318)CaDiCaL version: 2.1.3
% 6.96/1.30 % (2085318)Termination reason: Refutation not found, incomplete strategy
% 6.96/1.30 % (2085318)Time elapsed: 0.002 s
% 6.96/1.30 % (2085318)Peak memory usage: 11 MB
% 6.96/1.30 % (2085318)Instructions burned: 4 (million)
% 6.96/1.30 % (2085318)------------------------------
% 6.96/1.30 % (2085318)------------------------------
% 6.96/1.30 % (2085319)Refutation not found, incomplete strategy
% 6.96/1.30 % (2085319)------------------------------
% 6.96/1.30 % (2085319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.96/1.30 % (2085319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.30 % (2085319)CaDiCaL version: 2.1.3
% 6.96/1.30 % (2085319)Termination reason: Refutation not found, incomplete strategy
% 6.96/1.30 % (2085319)Time elapsed: 0.002 s
% 6.96/1.30 % (2085319)Peak memory usage: 11 MB
% 6.96/1.30 % (2085319)Instructions burned: 4 (million)
% 6.96/1.30 % (2085319)------------------------------
% 6.96/1.30 % (2085319)------------------------------
% 6.96/1.30 % (2085321)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=1059745427:st=1.5:i=346:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/346Mi)
% 6.96/1.30 % (2085324)lrs+1010_3_sil=128000:si=on:slsq=on:random_seed=2048227349:avsq=on:i=152:avsqr=8,1:hud=5:ins=1:fsr=off:rtra=on_2991 on theBenchmark for (2991ds/152Mi)
% 6.96/1.30 % (2085325)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3429883404:i=75:ep=R:rtra=on:ntd=on_2991 on theBenchmark for (2991ds/75Mi)
% 6.96/1.30 % (2085325)Instruction limit reached!
% 6.96/1.30 % (2085325)------------------------------
% 6.96/1.30 % (2085325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.96/1.30 % (2085325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.30 % (2085325)CaDiCaL version: 2.1.3
% 6.96/1.30 % (2085325)Termination reason: Instruction limit
% 6.96/1.30 % (2085325)Termination phase: Saturation
% 6.96/1.30 % (2085325)Time elapsed: 0.039 s
% 6.96/1.30 % (2085325)Peak memory usage: 12 MB
% 6.96/1.30 % (2085325)Instructions burned: 75 (million)
% 6.96/1.30 % (2085329)dis+10_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=one_side_interpreted:nwc=5:random_seed=591659271:st=2.5:i=387:sd=2:rtra=on:ss=axioms_2990 on theBenchmark for (2990ds/387Mi)
% 6.96/1.30 % (2085324)Instruction limit reached!
% 6.96/1.30 % (2085324)------------------------------
% 6.96/1.30 % (2085324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.96/1.30 % (2085324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.30 % (2085324)CaDiCaL version: 2.1.3
% 6.96/1.30 % (2085324)Termination reason: Instruction limit
% 6.96/1.30 % (2085324)Termination phase: Saturation
% 6.96/1.30 % (2085324)Time elapsed: 0.073 s
% 6.96/1.30 % (2085324)Peak memory usage: 13 MB
% 6.96/1.30 % (2085324)Instructions burned: 152 (million)
% 6.96/1.30 % (2085331)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=4238742252:uwa_fpi=on:i=148:doe=on:bd=preordered:rtra=on:fsd=on_2990 on theBenchmark for (2990ds/148Mi)
% 6.96/1.30 % (2085312)Instruction limit reached!
% 6.96/1.30 % (2085312)------------------------------
% 6.96/1.30 % (2085312)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.96/1.30 % (2085312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.30 % (2085312)CaDiCaL version: 2.1.3
% 6.96/1.30 % (2085312)Termination reason: Instruction limit
% 6.96/1.30 % (2085312)Termination phase: Saturation
% 6.96/1.30 % (2085312)Time elapsed: 0.144 s
% 6.96/1.30 % (2085312)Peak memory usage: 13 MB
% 6.96/1.30 % (2085312)Instructions burned: 282 (million)
% 6.96/1.30 % (2085333)dis+1010_3_si=on:uwa=one_side_interpreted:random_seed=1985411821:i=161:piset=and:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/161Mi)
% 6.96/1.30 % (2085321)Instruction limit reached!
% 6.96/1.30 % (2085321)------------------------------
% 6.96/1.30 % (2085321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.96/1.30 % (2085321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.30 % (2085321)CaDiCaL version: 2.1.3
% 6.96/1.30 % (2085321)Termination reason: Instruction limit
% 6.96/1.30 % (2085321)Termination phase: Saturation
% 6.96/1.30 % (2085321)Time elapsed: 0.146 s
% 6.96/1.30 % (2085321)Peak memory usage: 13 MB
% 6.96/1.30 % (2085321)Instructions burned: 347 (million)
% 6.96/1.30 % (2085298)Instruction limit reached!
% 6.96/1.30 % (2085298)------------------------------
% 6.96/1.30 % (2085298)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.96/1.30 % (2085298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.30 % (2085298)CaDiCaL version: 2.1.3
% 6.96/1.30 % (2085298)Termination reason: Instruction limit
% 6.96/1.30 % (2085298)Termination phase: Saturation
% 6.96/1.30 % (2085298)Time elapsed: 0.280 s
% 6.96/1.30 % (2085298)Peak memory usage: 13 MB
% 6.96/1.30 % (2085298)Instructions burned: 1445 (million)
% 6.96/1.30 % (2085335)lrs+10_1_sil=128000:si=on:random_seed=2999602230:st=5:i=888:sd=3:bd=preordered:rtra=on:ss=axioms_2989 on theBenchmark for (2989ds/888Mi)
% 6.96/1.30 % (2085335)Refutation not found, incomplete strategy
% 6.96/1.30 % (2085335)------------------------------
% 6.96/1.30 % (2085335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.96/1.30 % (2085335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.30 % (2085335)CaDiCaL version: 2.1.3
% 6.96/1.30 % (2085335)Termination reason: Refutation not found, incomplete strategy
% 6.96/1.30 % (2085335)Time elapsed: 0.002 s
% 6.96/1.30 % (2085335)Peak memory usage: 12 MB
% 6.96/1.30 % (2085335)Instructions burned: 4 (million)
% 6.96/1.30 % (2085335)------------------------------
% 6.96/1.30 % (2085335)------------------------------
% 6.96/1.30 % (2085336)ott-1003_1_sil=128000:plsq=on:plsqc=1:si=on:sp=weighted_frequency:lma=off:plsqr=1,32:urr=on:cbe=off:random_seed=1288019224:i=136:add=on:ins=4:rtra=on:sup=off_2989 on theBenchmark for (2989ds/136Mi)
% 6.96/1.30 % (2085331)Instruction limit reached!
% 6.96/1.30 % (2085331)------------------------------
% 6.96/1.30 % (2085331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.96/1.30 % (2085331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.30 % (2085331)CaDiCaL version: 2.1.3
% 6.96/1.30 % (2085331)Termination reason: Instruction limit
% 6.96/1.30 % (2085331)Termination phase: Saturation
% 6.96/1.30 % (2085331)Time elapsed: 0.078 s
% 6.96/1.30 % (2085331)Peak memory usage: 13 MB
% 6.96/1.30 % (2085331)Instructions burned: 157 (million)
% 6.96/1.30 % (2085339)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=2277839167:i=88:s2at=3:nm=2:rtra=on:rawr=on_2989 on theBenchmark for (2989ds/88Mi)
% 6.96/1.30 % (2085336) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2085120-2085336"...
% 6.96/1.30 % (2085340)dis+1002_5:4_to=kbo:sil=128000:cnfonf=conj_eager:si=on:sp=reverse_arity:lma=off:hi=on:nwc=20:random_seed=501329612:s2a=on:cond=on:i=93:add=on:bd=preordered:rtra=on:er=filter_2989 on theBenchmark for (2989ds/93Mi)
% 6.96/1.30 % (2085336)...printing done.
% 6.96/1.30 % (2085336)Refutation found. Thanks to Tanya!
% 6.96/1.30 % SZS status ContradictoryAxioms for theBenchmark
% 6.96/1.30 % SZS output start Proof for theBenchmark
% 6.96/1.30 thf(type_def_5, type, set_set_set_nat: $tType).
% 6.96/1.30 thf(type_def_6, type, set_set_nat: $tType).
% 6.96/1.30 thf(type_def_7, type, qML_mu: $tType).
% 6.96/1.30 thf(type_def_8, type, set_nat: $tType).
% 6.96/1.30 thf(type_def_9, type, qML_i: $tType).
% 6.96/1.30 thf(type_def_10, type, nat: $tType).
% 6.96/1.30 thf(type_def_11, type, sTfun: ($tType * $tType) > $tType).
% 6.96/1.30 thf(func_def_0, type, equiv_2129914667vp_nat: ((nat > nat > $o) > $o)).
% 6.96/1.30 thf(func_def_1, type, equiv_235907809et_nat: ((set_nat > set_nat > $o) > $o)).
% 6.96/1.30 thf(func_def_2, type, inconsistency_G: (qML_mu > qML_i > $o)).
% 6.96/1.30 thf(func_def_3, type, incons1905966852QML_mu: (qML_mu > qML_i > $o)).
% 6.96/1.30 thf(func_def_4, type, inconsistency_P: ((qML_mu > qML_i > $o) > qML_i > $o)).
% 6.96/1.30 thf(func_def_5, type, incons1389517216QML_mu: ((qML_mu > qML_i > $o) > qML_mu > qML_i > $o)).
% 6.96/1.30 thf(func_def_6, type, ord_less_eq_set_nat: (set_nat > set_nat > $o)).
% 6.96/1.30 thf(func_def_7, type, ord_le1613022364et_nat: (set_set_nat > set_set_nat > $o)).
% 6.96/1.30 thf(func_def_8, type, qML_r: (qML_i > qML_i > $o)).
% 6.96/1.30 thf(func_def_9, type, dvd_dvd_nat: (nat > nat > $o)).
% 6.96/1.30 thf(func_def_10, type, ball_nat: (set_nat > (nat > $o) > $o)).
% 6.96/1.30 thf(func_def_11, type, ball_set_nat: (set_set_nat > (set_nat > $o) > $o)).
% 6.96/1.30 thf(func_def_12, type, collect_nat: ((nat > $o) > set_nat)).
% 6.96/1.30 thf(func_def_13, type, collect_set_nat: ((set_nat > $o) > set_set_nat)).
% 6.96/1.30 thf(func_def_14, type, collect_set_set_nat: ((set_set_nat > $o) > set_set_set_nat)).
% 6.96/1.30 thf(func_def_15, type, set_greaterThan_nat: ((nat > nat > $o) > nat > set_nat)).
% 6.96/1.30 thf(func_def_16, type, member_nat: (nat > set_nat > $o)).
% 6.96/1.30 thf(func_def_17, type, member_set_nat: (set_nat > set_set_nat > $o)).
% 6.96/1.30 thf(func_def_18, type, member_set_set_nat: (set_set_nat > set_set_set_nat > $o)).
% 6.96/1.30 thf(func_def_22, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 6.96/1.30 thf(func_def_23, type, vAND: ($o > $o > $o)).
% 6.96/1.31 thf(func_def_24, type, db0: !>[X0: $tType]:(X0)).
% 6.96/1.31 thf(func_def_25, type, db1: !>[X0: $tType]:(X0)).
% 6.96/1.31 thf(func_def_26, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 6.96/1.31 thf(func_def_27, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 6.96/1.31 thf(func_def_28, type, vNOT: ($o > $o)).
% 6.96/1.31 thf(func_def_29, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 6.96/1.31 thf(func_def_30, type, vIMP: ($o > $o > $o)).
% 6.96/1.31 thf(func_def_31, type, db2: !>[X0: $tType]:(X0)).
% 6.96/1.31 thf(func_def_32, type, db5: !>[X0: $tType]:(X0)).
% 6.96/1.31 thf(func_def_33, type, sK0: (set_set_nat > set_set_nat > set_nat)).
% 6.96/1.31 thf(func_def_34, type, sK1: ((qML_mu > qML_i > $o) > qML_i > (qML_mu > qML_i > $o) > qML_i)).
% 6.96/1.31 thf(func_def_35, type, sK2: ((qML_mu > qML_i > $o) > qML_i > (qML_mu > qML_i > $o) > qML_mu)).
% 6.96/1.31 thf(func_def_36, type, sK3: ((set_nat > set_nat > $o) > set_set_nat)).
% 6.96/1.31 thf(func_def_37, type, sK4: ((nat > nat > $o) > set_nat)).
% 6.96/1.31 thf(func_def_38, type, sK5: (set_nat > set_nat > nat)).
% 6.96/1.31 thf(func_def_39, type, sK6: ((nat > nat > $o) > nat)).
% 6.96/1.31 thf(func_def_40, type, sK7: ((nat > nat > $o) > nat)).
% 6.96/1.31 thf(func_def_41, type, sK8: ((nat > nat > $o) > nat)).
% 6.96/1.31 thf(func_def_42, type, sK9: ((nat > nat > $o) > nat)).
% 6.96/1.31 thf(func_def_43, type, db4: !>[X0: $tType]:(X0)).
% 6.96/1.31 thf(func_def_44, type, db3: !>[X0: $tType]:(X0)).
% 6.96/1.31 thf(func_def_45, type, sK10: ((nat > nat > $o) > nat)).
% 6.96/1.31 thf(func_def_46, type, sK11: ((nat > nat > $o) > nat)).
% 6.96/1.31 thf(func_def_47, type, sK12: ((qML_mu > qML_i > $o) > qML_i > qML_mu > qML_i > $o)).
% 6.96/1.31 thf(func_def_48, type, sK13: ((qML_mu > qML_i > $o) > qML_i > qML_mu)).
% 6.96/1.31 thf(func_def_49, type, sK14: ((qML_mu > qML_i > $o) > qML_i > qML_i)).
% 6.96/1.31 thf(func_def_50, type, sK15: ((qML_mu > qML_i > $o) > qML_i > qML_mu)).
% 6.96/1.31 thf(func_def_51, type, sK16: ((qML_mu > qML_i > $o) > qML_i > qML_mu)).
% 6.96/1.31 thf(func_def_52, type, sK17: ((qML_mu > qML_i > $o) > qML_i > qML_mu > qML_i > $o)).
% 6.96/1.31 thf(func_def_53, type, sK18: ((qML_mu > qML_i > $o) > qML_i > qML_mu)).
% 6.96/1.31 thf(func_def_54, type, sK19: ((qML_mu > qML_i > $o) > qML_i > qML_i)).
% 6.96/1.31 thf(func_def_55, type, sK20: ((qML_mu > qML_i > $o) > qML_i > qML_mu)).
% 6.96/1.31 thf(func_def_56, type, sK21: ((qML_mu > qML_i > $o) > qML_i > qML_mu)).
% 6.96/1.31 thf(func_def_57, type, sK22: ((qML_mu > qML_i > $o) > qML_i > qML_mu > qML_i > $o)).
% 6.96/1.31 thf(func_def_58, type, sK23: ((qML_mu > qML_i > $o) > qML_i > qML_mu)).
% 6.96/1.31 thf(func_def_59, type, sK24: ((qML_mu > qML_i > $o) > qML_i > qML_i)).
% 6.96/1.31 thf(func_def_60, type, sK25: ((qML_mu > qML_i > $o) > qML_i > qML_mu)).
% 6.96/1.31 thf(func_def_61, type, sK26: ((qML_mu > qML_i > $o) > qML_i > qML_mu)).
% 6.96/1.31 thf(func_def_62, type, sK27: ((qML_mu > qML_i > $o) > qML_i > qML_mu > qML_i > $o)).
% 6.96/1.31 thf(func_def_63, type, sK28: ((qML_mu > qML_i > $o) > qML_i > qML_mu)).
% 6.96/1.31 thf(func_def_64, type, sK29: ((qML_mu > qML_i > $o) > qML_i > qML_i)).
% 6.96/1.31 thf(func_def_65, type, sK30: ((qML_mu > qML_i > $o) > qML_i > qML_mu)).
% 6.96/1.31 thf(f1,axiom,(
% 6.96/1.31 ! [X0 : qML_i,X1 : (qML_mu > qML_i > $o),X2 : (qML_mu > qML_i > $o)] : ((! [X3 : qML_i] : ((qML_r @ X0 @ X3) => ! [X4 : qML_mu] : ((X1 @ X4 @ X3) => (X2 @ X4 @ X3))) & (inconsistency_P @ X1 @ X0)) => (inconsistency_P @ X2 @ X0))),
% 6.96/1.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_A2)).
% 6.96/1.31 thf(f2,axiom,(
% 6.96/1.31 ! [X0 : qML_i] : (inconsistency_P @ incons1905966852QML_mu @ X0)),
% 6.96/1.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1_A5)).
% 6.96/1.31 thf(f3,axiom,(
% 6.96/1.31 ((^[X0 : qML_mu, X1 : qML_i] : (! [X2 : (qML_mu > qML_i > $o)] : ((inconsistency_P @ X2 @ X1) => (X2 @ X0 @ X1)))) = inconsistency_G)),
% 6.96/1.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2_G__def)).
% 6.96/1.31 thf(f4,axiom,(
% 6.96/1.31 ! [X0 : qML_i,X1 : (qML_mu > qML_i > $o)] : ((inconsistency_P @ (^[X2 : qML_mu, X3 : qML_i] : (~(X1 @ X2 @ X3))) @ X0) => ~(inconsistency_P @ X1 @ X0))),
% 6.96/1.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3_A1a)).
% 6.96/1.31 thf(f5,axiom,(
% 6.96/1.31 ! [X0 : qML_i] : (inconsistency_P @ inconsistency_G @ X0)),
% 6.96/1.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4_A3)).
% 6.96/1.31 thf(f9,axiom,(
% 6.96/1.31 ! [X1 : qML_i,X0 : qML_i] : ((qML_r @ X0 @ X1) => (qML_r @ X1 @ X0))),
% 6.96/1.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_8_QML__S5_Osym)).
% 6.96/1.31 thf(f11,axiom,(
% 6.96/1.31 (incons1905966852QML_mu = (^[X0 : qML_mu, X1 : qML_i] : (! [X2 : (qML_mu > qML_i > $o)] : ((incons1389517216QML_mu @ X2 @ X0 @ X1) => ! [X3 : qML_i] : ((qML_r @ X1 @ X3) => ? [X4 : qML_mu] : (X2 @ X4 @ X3))))))),
% 6.96/1.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_10_NE__def)).
% 6.96/1.31 thf(f12,axiom,(
% 6.96/1.31 ((^[X0 : (qML_mu > qML_i > $o), X1 : qML_mu, X2 : qML_i] : (! [X3 : (qML_mu > qML_i > $o)] : ((X3 @ X1 @ X2) => ! [X4 : qML_i] : ((qML_r @ X2 @ X4) => ! [X5 : qML_mu] : ((X0 @ X5 @ X4) => (X3 @ X5 @ X4)))))) = incons1389517216QML_mu)),
% 6.96/1.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_11_ess__def)).
% 6.96/1.31 thf(f31,plain,(
% 6.96/1.31 ! [X0 : qML_i,X1 : (qML_mu > qML_i > $o)] : ((inconsistency_P @ (^[X2 : qML_mu, X3 : qML_i] : (~(X1 @ X2 @ X3))) @ X0) => ~(inconsistency_P @ X1 @ X0))),
% 6.96/1.31 inference(rectify,[],[f4])).
% 6.96/1.31 thf(f32,plain,(
% 6.96/1.31 ! [X0 : qML_i,X1 : (qML_mu > qML_i > $o)] : (($true = ((inconsistency_P @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (~ (X1 @ Y0 @ Y1))))) @ X0))) => ~ (((inconsistency_P @ X1 @ X0)) = $true))),
% 6.96/1.31 inference(fool_elimination,[],[f31])).
% 6.96/1.31 thf(f33,plain,(
% 6.96/1.31 ! [X0 : qML_i] : (inconsistency_P @ inconsistency_G @ X0)),
% 6.96/1.31 inference(rectify,[],[f5])).
% 6.96/1.31 thf(f34,plain,(
% 6.96/1.31 ! [X0 : qML_i] : (((inconsistency_P @ inconsistency_G @ X0)) = $true)),
% 6.96/1.31 inference(fool_elimination,[],[f33])).
% 6.96/1.31 thf(f37,plain,(
% 6.96/1.31 ! [X0 : qML_i,X1 : qML_i] : ((qML_r @ X1 @ X0) => (qML_r @ X0 @ X1))),
% 6.96/1.31 inference(rectify,[],[f9])).
% 6.96/1.31 thf(f38,plain,(
% 6.96/1.31 ! [X0 : qML_i,X1 : qML_i] : ((((qML_r @ X1 @ X0)) = $true) => (((qML_r @ X0 @ X1)) = $true))),
% 6.96/1.31 inference(fool_elimination,[],[f37])).
% 6.96/1.31 thf(f45,plain,(
% 6.96/1.31 ! [X0 : qML_i,X1 : (qML_mu > qML_i > $o),X2 : (qML_mu > qML_i > $o)] : ((! [X3 : qML_i] : ((qML_r @ X0 @ X3) => ! [X4 : qML_mu] : ((X1 @ X4 @ X3) => (X2 @ X4 @ X3))) & (inconsistency_P @ X1 @ X0)) => (inconsistency_P @ X2 @ X0))),
% 6.96/1.31 inference(rectify,[],[f1])).
% 6.96/1.31 thf(f46,plain,(
% 6.96/1.31 ! [X2 : (qML_mu > qML_i > $o),X0 : qML_i,X1 : (qML_mu > qML_i > $o)] : (((((inconsistency_P @ X1 @ X0)) = $true) & ! [X3 : qML_i] : ((((qML_r @ X0 @ X3)) = $true) => ! [X4 : qML_mu] : ((((X1 @ X4 @ X3)) = $true) => (((X2 @ X4 @ X3)) = $true)))) => (((inconsistency_P @ X2 @ X0)) = $true))),
% 6.96/1.31 inference(fool_elimination,[],[f45])).
% 6.96/1.31 thf(f47,plain,(
% 6.96/1.31 ((^[X0 : (qML_mu > qML_i > $o), X1 : qML_mu, X2 : qML_i] : (! [X3 : (qML_mu > qML_i > $o)] : ((X3 @ X1 @ X2) => ! [X4 : qML_i] : ((qML_r @ X2 @ X4) => ! [X5 : qML_mu] : ((X0 @ X5 @ X4) => (X3 @ X5 @ X4)))))) = incons1389517216QML_mu)),
% 6.96/1.31 inference(rectify,[],[f12])).
% 6.96/1.31 thf(f48,plain,(
% 6.96/1.31 (incons1389517216QML_mu = (^[Y0 : qML_mu > qML_i > $o]: ((^[Y1 : qML_mu]: ((^[Y2 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((Y3 @ Y1 @ Y2) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y2 @ Y4) => (!! @ qML_mu @ (^[Y5 : qML_mu]: ((Y0 @ Y5 @ Y4) => (Y3 @ Y5 @ Y4))))))))))))))))),
% 6.96/1.31 inference(fool_elimination,[],[f47])).
% 6.96/1.31 thf(f49,plain,(
% 6.96/1.31 ! [X0 : qML_i] : (inconsistency_P @ incons1905966852QML_mu @ X0)),
% 6.96/1.31 inference(rectify,[],[f2])).
% 6.96/1.31 thf(f50,plain,(
% 6.96/1.31 ! [X0 : qML_i] : (((inconsistency_P @ incons1905966852QML_mu @ X0)) = $true)),
% 6.96/1.31 inference(fool_elimination,[],[f49])).
% 6.96/1.31 thf(f63,plain,(
% 6.96/1.31 (incons1905966852QML_mu = (^[X0 : qML_mu, X1 : qML_i] : (! [X2 : (qML_mu > qML_i > $o)] : ((incons1389517216QML_mu @ X2 @ X0 @ X1) => ! [X3 : qML_i] : ((qML_r @ X1 @ X3) => ? [X4 : qML_mu] : (X2 @ X4 @ X3))))))),
% 6.96/1.31 inference(rectify,[],[f11])).
% 6.96/1.31 thf(f64,plain,(
% 6.96/1.31 (incons1905966852QML_mu = (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((incons1389517216QML_mu @ Y2 @ Y0 @ Y1) => (!! @ qML_i @ (^[Y3 : qML_i]: ((qML_r @ Y1 @ Y3) => (?? @ qML_mu @ (^[Y4 : qML_mu]: (Y2 @ Y4 @ Y3)))))))))))))),
% 6.96/1.31 inference(fool_elimination,[],[f63])).
% 6.96/1.31 thf(f73,plain,(
% 6.96/1.31 ((^[X0 : qML_mu, X1 : qML_i] : (! [X2 : (qML_mu > qML_i > $o)] : ((inconsistency_P @ X2 @ X1) => (X2 @ X0 @ X1)))) = inconsistency_G)),
% 6.96/1.31 inference(rectify,[],[f3])).
% 6.96/1.31 thf(f74,plain,(
% 6.96/1.31 (inconsistency_G = (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y2 @ Y1) => (Y2 @ Y0 @ Y1))))))))),
% 6.96/1.31 inference(fool_elimination,[],[f73])).
% 6.96/1.31 thf(f77,plain,(
% 6.96/1.31 ! [X0 : qML_i,X1 : (qML_mu > qML_i > $o)] : (($true = ((inconsistency_P @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (~ (X1 @ Y0 @ Y1))))) @ X0))) => (((inconsistency_P @ X1 @ X0)) != $true))),
% 6.96/1.31 inference(flattening,[],[f32])).
% 6.96/1.31 thf(f85,plain,(
% 6.96/1.31 ! [X1 : (qML_mu > qML_i > $o),X0 : qML_i] : (($true != ((inconsistency_P @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (~ (X1 @ Y0 @ Y1))))) @ X0))) | (((inconsistency_P @ X1 @ X0)) != $true))),
% 6.96/1.31 inference(ennf_transformation,[],[f77])).
% 6.96/1.31 thf(f86,plain,(
% 6.96/1.31 ! [X2 : (qML_mu > qML_i > $o),X0 : qML_i,X1 : (qML_mu > qML_i > $o)] : ((((inconsistency_P @ X2 @ X0)) = $true) | ((((inconsistency_P @ X1 @ X0)) != $true) | ? [X3 : qML_i] : (? [X4 : qML_mu] : ((((X1 @ X4 @ X3)) = $true) & (((X2 @ X4 @ X3)) != $true)) & (((qML_r @ X0 @ X3)) = $true))))),
% 6.96/1.31 inference(ennf_transformation,[],[f46])).
% 6.96/1.31 thf(f87,plain,(
% 6.96/1.31 ! [X1 : (qML_mu > qML_i > $o),X0 : qML_i,X2 : (qML_mu > qML_i > $o)] : ((((inconsistency_P @ X2 @ X0)) = $true) | (((inconsistency_P @ X1 @ X0)) != $true) | ? [X3 : qML_i] : (? [X4 : qML_mu] : ((((X1 @ X4 @ X3)) = $true) & (((X2 @ X4 @ X3)) != $true)) & (((qML_r @ X0 @ X3)) = $true)))),
% 6.96/1.31 inference(flattening,[],[f86])).
% 6.96/1.31 thf(f88,plain,(
% 6.96/1.31 ! [X1 : qML_i,X0 : qML_i] : ((((qML_r @ X0 @ X1)) = $true) | (((qML_r @ X1 @ X0)) != $true))),
% 6.96/1.31 inference(ennf_transformation,[],[f38])).
% 6.96/1.31 thf(f96,plain,(
% 6.96/1.31 ! [X0 : qML_i,X1 : qML_i] : ((((qML_r @ X1 @ X0)) = $true) | (((qML_r @ X0 @ X1)) != $true))),
% 6.96/1.31 inference(rectify,[],[f88])).
% 6.96/1.31 thf(f100,plain,(
% 6.96/1.31 ! [X0 : (qML_mu > qML_i > $o),X1 : qML_i,X2 : (qML_mu > qML_i > $o)] : ((((inconsistency_P @ X2 @ X1)) = $true) | (((inconsistency_P @ X0 @ X1)) != $true) | ? [X3 : qML_i] : (? [X4 : qML_mu] : ((((X0 @ X4 @ X3)) = $true) & (((X2 @ X4 @ X3)) != $true)) & (((qML_r @ X1 @ X3)) = $true)))),
% 6.96/1.31 inference(rectify,[],[f87])).
% 6.96/1.31 thf(f101,plain,(
% 6.96/1.31 ! [X0 : (qML_mu > qML_i > $o),X1 : qML_i,X2 : (qML_mu > qML_i > $o)] : ((((inconsistency_P @ X2 @ X1)) = $true) | (((inconsistency_P @ X0 @ X1)) != $true) | (((((X0 @ (sK2 @ X2 @ X1 @ X0) @ (sK1 @ X2 @ X1 @ X0))) = $true) & ($true != ((X2 @ (sK2 @ X2 @ X1 @ X0) @ (sK1 @ X2 @ X1 @ X0))))) & (((qML_r @ X1 @ (sK1 @ X2 @ X1 @ X0))) = $true)))),
% 6.96/1.31 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP,vAPP]),skolemize(X2,sK0 @ X1 @ X0),skolemize(X2,sK0 @ X1 @ X0)],[f100])).
% 6.96/1.31 thf(f107,plain,(
% 6.96/1.31 ! [X0 : (qML_mu > qML_i > $o),X1 : qML_i] : (($true != ((inconsistency_P @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (~ (X0 @ Y0 @ Y1))))) @ X1))) | (((inconsistency_P @ X0 @ X1)) != $true))),
% 6.96/1.31 inference(rectify,[],[f85])).
% 6.96/1.31 thf(f111,plain,(
% 6.96/1.31 ( ! [X0 : qML_i,X1 : qML_i] : ((((qML_r @ X0 @ X1)) != $true) | (((qML_r @ X1 @ X0)) = $true)) )),
% 6.96/1.31 inference(cnf_transformation,[],[f96])).
% 6.96/1.31 thf(f117,plain,(
% 6.96/1.31 (incons1389517216QML_mu = (^[Y0 : qML_mu > qML_i > $o]: ((^[Y1 : qML_mu]: ((^[Y2 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((Y3 @ Y1 @ Y2) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y2 @ Y4) => (!! @ qML_mu @ (^[Y5 : qML_mu]: ((Y0 @ Y5 @ Y4) => (Y3 @ Y5 @ Y4))))))))))))))))),
% 6.96/1.31 inference(cnf_transformation,[],[f48])).
% 6.96/1.31 thf(f118,plain,(
% 6.96/1.31 (incons1905966852QML_mu = (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((incons1389517216QML_mu @ Y2 @ Y0 @ Y1) => (!! @ qML_i @ (^[Y3 : qML_i]: ((qML_r @ Y1 @ Y3) => (?? @ qML_mu @ (^[Y4 : qML_mu]: (Y2 @ Y4 @ Y3)))))))))))))),
% 6.96/1.31 inference(cnf_transformation,[],[f64])).
% 6.96/1.31 thf(f122,plain,(
% 6.96/1.31 ( ! [X0 : qML_i] : ((((inconsistency_P @ incons1905966852QML_mu @ X0)) = $true)) )),
% 6.96/1.31 inference(cnf_transformation,[],[f50])).
% 6.96/1.31 thf(f124,plain,(
% 6.96/1.31 ( ! [X2 : (qML_mu > qML_i > $o),X0 : (qML_mu > qML_i > $o),X1 : qML_i] : ((((inconsistency_P @ X0 @ X1)) != $true) | (((inconsistency_P @ X2 @ X1)) = $true) | (((qML_r @ X1 @ (sK1 @ X2 @ X1 @ X0))) = $true)) )),
% 6.96/1.31 inference(cnf_transformation,[],[f101])).
% 6.96/1.31 thf(f126,plain,(
% 6.96/1.31 ( ! [X2 : (qML_mu > qML_i > $o),X0 : (qML_mu > qML_i > $o),X1 : qML_i] : ((((inconsistency_P @ X0 @ X1)) != $true) | (((inconsistency_P @ X2 @ X1)) = $true) | (((X0 @ (sK2 @ X2 @ X1 @ X0) @ (sK1 @ X2 @ X1 @ X0))) = $true)) )),
% 6.96/1.31 inference(cnf_transformation,[],[f101])).
% 6.96/1.31 thf(f132,plain,(
% 6.96/1.31 ( ! [X0 : (qML_mu > qML_i > $o),X1 : qML_i] : (($true != ((inconsistency_P @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (~ (X0 @ Y0 @ Y1))))) @ X1))) | (((inconsistency_P @ X0 @ X1)) != $true)) )),
% 6.96/1.31 inference(cnf_transformation,[],[f107])).
% 6.96/1.31 thf(f135,plain,(
% 6.96/1.31 (inconsistency_G = (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y2 @ Y1) => (Y2 @ Y0 @ Y1))))))))),
% 6.96/1.31 inference(cnf_transformation,[],[f74])).
% 6.96/1.31 thf(f136,plain,(
% 6.96/1.31 ( ! [X0 : qML_i] : ((((inconsistency_P @ inconsistency_G @ X0)) = $true)) )),
% 6.96/1.31 inference(cnf_transformation,[],[f34])).
% 6.96/1.31 thf(f140,definition,(
% 6.96/1.31 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 6.96/1.31 introduced(theory,[fool_exhaustiveness_axiom])).
% 6.96/1.31 thf(f141,plain,(
% 6.96/1.31 (incons1905966852QML_mu = (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: (((^[Y3 : qML_mu > qML_i > $o]: ((^[Y4 : qML_mu]: ((^[Y5 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y6 : qML_mu > qML_i > $o]: ((Y6 @ Y4 @ Y5) => (!! @ qML_i @ (^[Y7 : qML_i]: ((qML_r @ Y5 @ Y7) => (!! @ qML_mu @ (^[Y8 : qML_mu]: ((Y3 @ Y8 @ Y7) => (Y6 @ Y8 @ Y7))))))))))))))) @ Y2 @ Y0 @ Y1) => (!! @ qML_i @ (^[Y3 : qML_i]: ((qML_r @ Y1 @ Y3) => (?? @ qML_mu @ (^[Y4 : qML_mu]: (Y2 @ Y4 @ Y3)))))))))))))),
% 6.96/1.31 inference(definition_unfolding,[],[f118,f117])).
% 6.96/1.31 thf(f144,plain,(
% 6.96/1.31 ( ! [X0 : qML_i] : (($true = ((inconsistency_P @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: (((^[Y3 : qML_mu > qML_i > $o]: ((^[Y4 : qML_mu]: ((^[Y5 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y6 : qML_mu > qML_i > $o]: ((Y6 @ Y4 @ Y5) => (!! @ qML_i @ (^[Y7 : qML_i]: ((qML_r @ Y5 @ Y7) => (!! @ qML_mu @ (^[Y8 : qML_mu]: ((Y3 @ Y8 @ Y7) => (Y6 @ Y8 @ Y7))))))))))))))) @ Y2 @ Y0 @ Y1) => (!! @ qML_i @ (^[Y3 : qML_i]: ((qML_r @ Y1 @ Y3) => (?? @ qML_mu @ (^[Y4 : qML_mu]: (Y2 @ Y4 @ Y3)))))))))))) @ X0)))) )),
% 6.96/1.31 inference(definition_unfolding,[],[f122,f141])).
% 6.96/1.31 thf(f147,plain,(
% 6.96/1.31 ( ! [X0 : qML_i] : (($true = ((inconsistency_P @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y2 @ Y1) => (Y2 @ Y0 @ Y1))))))) @ X0)))) )),
% 6.96/1.31 inference(definition_unfolding,[],[f136,f135])).
% 6.96/1.31 thf(f189,plain,(
% 6.96/1.31 ( ! [X0 : qML_i] : ((((inconsistency_P @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((Y3 @ Y0 @ Y1) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y1 @ Y4) => (!! @ qML_mu @ (^[Y5 : qML_mu]: ((Y2 @ Y5 @ Y4) => (Y3 @ Y5 @ Y4)))))))))) => (!! @ qML_i @ (^[Y3 : qML_i]: ((qML_r @ Y1 @ Y3) => (?? @ qML_mu @ (^[Y4 : qML_mu]: (Y2 @ Y4 @ Y3)))))))))))) @ X0)) = $true)) )),
% 6.96/1.31 inference(beta-eta_normalization,[],[f144])).
% 6.96/1.31 thf(f379,plain,(
% 6.96/1.31 ( ! [X0 : qML_i] : ((((inconsistency_P @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (~ ((^[Y2 : qML_mu]: ((^[Y3 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y4 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y4 @ Y3) => (Y4 @ Y2 @ Y3))))))) @ Y0 @ Y1))))) @ X0)) != $true)) )),
% 6.96/1.31 inference(unit_resulting_resolution,[],[f132,f147])).
% 6.96/1.31 thf(f381,plain,(
% 6.96/1.31 ( ! [X0 : qML_i] : ((((inconsistency_P @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y2 @ Y1) => (Y2 @ Y0 @ Y1)))))))) @ X0)) != $true)) )),
% 6.96/1.31 inference(beta-eta_normalization,[],[f379])).
% 6.96/1.31 thf(f414,plain,(
% 6.96/1.31 ( ! [X0 : qML_i] : (((((^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((Y3 @ Y0 @ Y1) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y1 @ Y4) => (!! @ qML_mu @ (^[Y5 : qML_mu]: ((Y2 @ Y5 @ Y4) => (Y3 @ Y5 @ Y4)))))))))) => (!! @ qML_i @ (^[Y3 : qML_i]: ((qML_r @ Y1 @ Y3) => (?? @ qML_mu @ (^[Y4 : qML_mu]: (Y2 @ Y4 @ Y3)))))))))))) @ (sK2 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y2 @ Y1) => (Y2 @ Y0 @ Y1)))))))) @ X0 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((Y3 @ Y0 @ Y1) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y1 @ Y4) => (!! @ qML_mu @ (^[Y5 : qML_mu]: ((Y2 @ Y5 @ Y4) => (Y3 @ Y5 @ Y4)))))))))) => (!! @ qML_i @ (^[Y3 : qML_i]: ((qML_r @ Y1 @ Y3) => (?? @ qML_mu @ (^[Y4 : qML_mu]: (Y2 @ Y4 @ Y3))))))))))))) @ (sK1 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y2 @ Y1) => (Y2 @ Y0 @ Y1)))))))) @ X0 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((Y3 @ Y0 @ Y1) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y1 @ Y4) => (!! @ qML_mu @ (^[Y5 : qML_mu]: ((Y2 @ Y5 @ Y4) => (Y3 @ Y5 @ Y4)))))))))) => (!! @ qML_i @ (^[Y3 : qML_i]: ((qML_r @ Y1 @ Y3) => (?? @ qML_mu @ (^[Y4 : qML_mu]: (Y2 @ Y4 @ Y3))))))))))))))) = $true)) )),
% 6.96/1.31 inference(unit_resulting_resolution,[],[f126,f381,f189])).
% 6.96/1.31 thf(f415,plain,(
% 6.96/1.31 ( ! [X0 : qML_i] : ((((qML_r @ X0 @ (sK1 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y2 @ Y1) => (Y2 @ Y0 @ Y1)))))))) @ X0 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((Y3 @ Y0 @ Y1) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y1 @ Y4) => (!! @ qML_mu @ (^[Y5 : qML_mu]: ((Y2 @ Y5 @ Y4) => (Y3 @ Y5 @ Y4)))))))))) => (!! @ qML_i @ (^[Y3 : qML_i]: ((qML_r @ Y1 @ Y3) => (?? @ qML_mu @ (^[Y4 : qML_mu]: (Y2 @ Y4 @ Y3))))))))))))))) = $true)) )),
% 6.96/1.31 inference(unit_resulting_resolution,[],[f124,f381,f189])).
% 6.96/1.31 thf(f416,plain,(
% 6.96/1.31 ( ! [X0 : qML_i] : ((((!! @ (qML_mu > qML_i > $o) @ (^[Y0 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y1 : qML_mu > qML_i > $o]: ((Y1 @ (sK2 @ (^[Y2 : qML_mu]: ((^[Y3 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y4 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y4 @ Y3) => (Y4 @ Y2 @ Y3)))))))) @ X0 @ (^[Y2 : qML_mu]: ((^[Y3 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y4 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y5 : qML_mu > qML_i > $o]: ((Y5 @ Y2 @ Y3) => (!! @ qML_i @ (^[Y6 : qML_i]: ((qML_r @ Y3 @ Y6) => (!! @ qML_mu @ (^[Y7 : qML_mu]: ((Y4 @ Y7 @ Y6) => (Y5 @ Y7 @ Y6)))))))))) => (!! @ qML_i @ (^[Y5 : qML_i]: ((qML_r @ Y3 @ Y5) => (?? @ qML_mu @ (^[Y6 : qML_mu]: (Y4 @ Y6 @ Y5))))))))))))) @ (sK1 @ (^[Y2 : qML_mu]: ((^[Y3 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y4 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y4 @ Y3) => (Y4 @ Y2 @ Y3)))))))) @ X0 @ (^[Y2 : qML_mu]: ((^[Y3 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y4 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y5 : qML_mu > qML_i > $o]: ((Y5 @ Y2 @ Y3) => (!! @ qML_i @ (^[Y6 : qML_i]: ((qML_r @ Y3 @ Y6) => (!! @ qML_mu @ (^[Y7 : qML_mu]: ((Y4 @ Y7 @ Y6) => (Y5 @ Y7 @ Y6)))))))))) => (!! @ qML_i @ (^[Y5 : qML_i]: ((qML_r @ Y3 @ Y5) => (?? @ qML_mu @ (^[Y6 : qML_mu]: (Y4 @ Y6 @ Y5)))))))))))))) => (!! @ qML_i @ (^[Y2 : qML_i]: ((qML_r @ (sK1 @ (^[Y3 : qML_mu]: ((^[Y4 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y5 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y5 @ Y4) => (Y5 @ Y3 @ Y4)))))))) @ X0 @ (^[Y3 : qML_mu]: ((^[Y4 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y5 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y6 : qML_mu > qML_i > $o]: ((Y6 @ Y3 @ Y4) => (!! @ qML_i @ (^[Y7 : qML_i]: ((qML_r @ Y4 @ Y7) => (!! @ qML_mu @ (^[Y8 : qML_mu]: ((Y5 @ Y8 @ Y7) => (Y6 @ Y8 @ Y7)))))))))) => (!! @ qML_i @ (^[Y6 : qML_i]: ((qML_r @ Y4 @ Y6) => (?? @ qML_mu @ (^[Y7 : qML_mu]: (Y5 @ Y7 @ Y6))))))))))))) @ Y2) => (!! @ qML_mu @ (^[Y3 : qML_mu]: ((Y0 @ Y3 @ Y2) => (Y1 @ Y3 @ Y2)))))))))) => (!! @ qML_i @ (^[Y1 : qML_i]: ((qML_r @ (sK1 @ (^[Y2 : qML_mu]: ((^[Y3 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y4 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y4 @ Y3) => (Y4 @ Y2 @ Y3)))))))) @ X0 @ (^[Y2 : qML_mu]: ((^[Y3 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y4 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y5 : qML_mu > qML_i > $o]: ((Y5 @ Y2 @ Y3) => (!! @ qML_i @ (^[Y6 : qML_i]: ((qML_r @ Y3 @ Y6) => (!! @ qML_mu @ (^[Y7 : qML_mu]: ((Y4 @ Y7 @ Y6) => (Y5 @ Y7 @ Y6)))))))))) => (!! @ qML_i @ (^[Y5 : qML_i]: ((qML_r @ Y3 @ Y5) => (?? @ qML_mu @ (^[Y6 : qML_mu]: (Y4 @ Y6 @ Y5))))))))))))) @ Y1) => (?? @ qML_mu @ (^[Y2 : qML_mu]: (Y0 @ Y2 @ Y1)))))))))) = $true)) )),
% 6.96/1.31 inference(beta-eta_normalization,[],[f414])).
% 6.96/1.31 thf(f417,plain,(
% 6.96/1.31 ( ! [X0 : qML_i,X1 : (qML_mu > qML_i > $o)] : (($true = (((^[Y0 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y1 : qML_mu > qML_i > $o]: ((Y1 @ (sK2 @ (^[Y2 : qML_mu]: ((^[Y3 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y4 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y4 @ Y3) => (Y4 @ Y2 @ Y3)))))))) @ X0 @ (^[Y2 : qML_mu]: ((^[Y3 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y4 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y5 : qML_mu > qML_i > $o]: ((Y5 @ Y2 @ Y3) => (!! @ qML_i @ (^[Y6 : qML_i]: ((qML_r @ Y3 @ Y6) => (!! @ qML_mu @ (^[Y7 : qML_mu]: ((Y4 @ Y7 @ Y6) => (Y5 @ Y7 @ Y6)))))))))) => (!! @ qML_i @ (^[Y5 : qML_i]: ((qML_r @ Y3 @ Y5) => (?? @ qML_mu @ (^[Y6 : qML_mu]: (Y4 @ Y6 @ Y5))))))))))))) @ (sK1 @ (^[Y2 : qML_mu]: ((^[Y3 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y4 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y4 @ Y3) => (Y4 @ Y2 @ Y3)))))))) @ X0 @ (^[Y2 : qML_mu]: ((^[Y3 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y4 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y5 : qML_mu > qML_i > $o]: ((Y5 @ Y2 @ Y3) => (!! @ qML_i @ (^[Y6 : qML_i]: ((qML_r @ Y3 @ Y6) => (!! @ qML_mu @ (^[Y7 : qML_mu]: ((Y4 @ Y7 @ Y6) => (Y5 @ Y7 @ Y6)))))))))) => (!! @ qML_i @ (^[Y5 : qML_i]: ((qML_r @ Y3 @ Y5) => (?? @ qML_mu @ (^[Y6 : qML_mu]: (Y4 @ Y6 @ Y5)))))))))))))) => (!! @ qML_i @ (^[Y2 : qML_i]: ((qML_r @ (sK1 @ (^[Y3 : qML_mu]: ((^[Y4 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y5 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y5 @ Y4) => (Y5 @ Y3 @ Y4)))))))) @ X0 @ (^[Y3 : qML_mu]: ((^[Y4 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y5 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y6 : qML_mu > qML_i > $o]: ((Y6 @ Y3 @ Y4) => (!! @ qML_i @ (^[Y7 : qML_i]: ((qML_r @ Y4 @ Y7) => (!! @ qML_mu @ (^[Y8 : qML_mu]: ((Y5 @ Y8 @ Y7) => (Y6 @ Y8 @ Y7)))))))))) => (!! @ qML_i @ (^[Y6 : qML_i]: ((qML_r @ Y4 @ Y6) => (?? @ qML_mu @ (^[Y7 : qML_mu]: (Y5 @ Y7 @ Y6))))))))))))) @ Y2) => (!! @ qML_mu @ (^[Y3 : qML_mu]: ((Y0 @ Y3 @ Y2) => (Y1 @ Y3 @ Y2)))))))))) => (!! @ qML_i @ (^[Y1 : qML_i]: ((qML_r @ (sK1 @ (^[Y2 : qML_mu]: ((^[Y3 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y4 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y4 @ Y3) => (Y4 @ Y2 @ Y3)))))))) @ X0 @ (^[Y2 : qML_mu]: ((^[Y3 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y4 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y5 : qML_mu > qML_i > $o]: ((Y5 @ Y2 @ Y3) => (!! @ qML_i @ (^[Y6 : qML_i]: ((qML_r @ Y3 @ Y6) => (!! @ qML_mu @ (^[Y7 : qML_mu]: ((Y4 @ Y7 @ Y6) => (Y5 @ Y7 @ Y6)))))))))) => (!! @ qML_i @ (^[Y5 : qML_i]: ((qML_r @ Y3 @ Y5) => (?? @ qML_mu @ (^[Y6 : qML_mu]: (Y4 @ Y6 @ Y5))))))))))))) @ Y1) => (?? @ qML_mu @ (^[Y2 : qML_mu]: (Y0 @ Y2 @ Y1)))))))) @ X1)))) )),
% 6.96/1.31 inference(pi_proxy_clausification,[],[f416])).
% 6.96/1.31 thf(f418,plain,(
% 6.96/1.31 ( ! [X0 : qML_i,X1 : (qML_mu > qML_i > $o)] : (((((!! @ (qML_mu > qML_i > $o) @ (^[Y0 : qML_mu > qML_i > $o]: ((Y0 @ (sK2 @ (^[Y1 : qML_mu]: ((^[Y2 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y3 @ Y2) => (Y3 @ Y1 @ Y2)))))))) @ X0 @ (^[Y1 : qML_mu]: ((^[Y2 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y4 : qML_mu > qML_i > $o]: ((Y4 @ Y1 @ Y2) => (!! @ qML_i @ (^[Y5 : qML_i]: ((qML_r @ Y2 @ Y5) => (!! @ qML_mu @ (^[Y6 : qML_mu]: ((Y3 @ Y6 @ Y5) => (Y4 @ Y6 @ Y5)))))))))) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y2 @ Y4) => (?? @ qML_mu @ (^[Y5 : qML_mu]: (Y3 @ Y5 @ Y4))))))))))))) @ (sK1 @ (^[Y1 : qML_mu]: ((^[Y2 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y3 @ Y2) => (Y3 @ Y1 @ Y2)))))))) @ X0 @ (^[Y1 : qML_mu]: ((^[Y2 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y4 : qML_mu > qML_i > $o]: ((Y4 @ Y1 @ Y2) => (!! @ qML_i @ (^[Y5 : qML_i]: ((qML_r @ Y2 @ Y5) => (!! @ qML_mu @ (^[Y6 : qML_mu]: ((Y3 @ Y6 @ Y5) => (Y4 @ Y6 @ Y5)))))))))) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y2 @ Y4) => (?? @ qML_mu @ (^[Y5 : qML_mu]: (Y3 @ Y5 @ Y4)))))))))))))) => (!! @ qML_i @ (^[Y1 : qML_i]: ((qML_r @ (sK1 @ (^[Y2 : qML_mu]: ((^[Y3 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y4 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y4 @ Y3) => (Y4 @ Y2 @ Y3)))))))) @ X0 @ (^[Y2 : qML_mu]: ((^[Y3 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y4 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y5 : qML_mu > qML_i > $o]: ((Y5 @ Y2 @ Y3) => (!! @ qML_i @ (^[Y6 : qML_i]: ((qML_r @ Y3 @ Y6) => (!! @ qML_mu @ (^[Y7 : qML_mu]: ((Y4 @ Y7 @ Y6) => (Y5 @ Y7 @ Y6)))))))))) => (!! @ qML_i @ (^[Y5 : qML_i]: ((qML_r @ Y3 @ Y5) => (?? @ qML_mu @ (^[Y6 : qML_mu]: (Y4 @ Y6 @ Y5))))))))))))) @ Y1) => (!! @ qML_mu @ (^[Y2 : qML_mu]: ((X1 @ Y2 @ Y1) => (Y0 @ Y2 @ Y1)))))))))) => (!! @ qML_i @ (^[Y0 : qML_i]: ((qML_r @ (sK1 @ (^[Y1 : qML_mu]: ((^[Y2 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y3 @ Y2) => (Y3 @ Y1 @ Y2)))))))) @ X0 @ (^[Y1 : qML_mu]: ((^[Y2 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y4 : qML_mu > qML_i > $o]: ((Y4 @ Y1 @ Y2) => (!! @ qML_i @ (^[Y5 : qML_i]: ((qML_r @ Y2 @ Y5) => (!! @ qML_mu @ (^[Y6 : qML_mu]: ((Y3 @ Y6 @ Y5) => (Y4 @ Y6 @ Y5)))))))))) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y2 @ Y4) => (?? @ qML_mu @ (^[Y5 : qML_mu]: (Y3 @ Y5 @ Y4))))))))))))) @ Y0) => (?? @ qML_mu @ (^[Y1 : qML_mu]: (X1 @ Y1 @ Y0)))))))) = $true)) )),
% 6.96/1.31 inference(beta-eta_normalization,[],[f417])).
% 6.96/1.31 thf(f419,plain,(
% 6.96/1.31 ( ! [X0 : qML_i,X1 : (qML_mu > qML_i > $o)] : (($false = ((!! @ (qML_mu > qML_i > $o) @ (^[Y0 : qML_mu > qML_i > $o]: ((Y0 @ (sK2 @ (^[Y1 : qML_mu]: ((^[Y2 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y3 @ Y2) => (Y3 @ Y1 @ Y2)))))))) @ X0 @ (^[Y1 : qML_mu]: ((^[Y2 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y4 : qML_mu > qML_i > $o]: ((Y4 @ Y1 @ Y2) => (!! @ qML_i @ (^[Y5 : qML_i]: ((qML_r @ Y2 @ Y5) => (!! @ qML_mu @ (^[Y6 : qML_mu]: ((Y3 @ Y6 @ Y5) => (Y4 @ Y6 @ Y5)))))))))) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y2 @ Y4) => (?? @ qML_mu @ (^[Y5 : qML_mu]: (Y3 @ Y5 @ Y4))))))))))))) @ (sK1 @ (^[Y1 : qML_mu]: ((^[Y2 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y3 @ Y2) => (Y3 @ Y1 @ Y2)))))))) @ X0 @ (^[Y1 : qML_mu]: ((^[Y2 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y4 : qML_mu > qML_i > $o]: ((Y4 @ Y1 @ Y2) => (!! @ qML_i @ (^[Y5 : qML_i]: ((qML_r @ Y2 @ Y5) => (!! @ qML_mu @ (^[Y6 : qML_mu]: ((Y3 @ Y6 @ Y5) => (Y4 @ Y6 @ Y5)))))))))) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y2 @ Y4) => (?? @ qML_mu @ (^[Y5 : qML_mu]: (Y3 @ Y5 @ Y4)))))))))))))) => (!! @ qML_i @ (^[Y1 : qML_i]: ((qML_r @ (sK1 @ (^[Y2 : qML_mu]: ((^[Y3 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y4 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y4 @ Y3) => (Y4 @ Y2 @ Y3)))))))) @ X0 @ (^[Y2 : qML_mu]: ((^[Y3 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y4 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y5 : qML_mu > qML_i > $o]: ((Y5 @ Y2 @ Y3) => (!! @ qML_i @ (^[Y6 : qML_i]: ((qML_r @ Y3 @ Y6) => (!! @ qML_mu @ (^[Y7 : qML_mu]: ((Y4 @ Y7 @ Y6) => (Y5 @ Y7 @ Y6)))))))))) => (!! @ qML_i @ (^[Y5 : qML_i]: ((qML_r @ Y3 @ Y5) => (?? @ qML_mu @ (^[Y6 : qML_mu]: (Y4 @ Y6 @ Y5))))))))))))) @ Y1) => (!! @ qML_mu @ (^[Y2 : qML_mu]: ((X1 @ Y2 @ Y1) => (Y0 @ Y2 @ Y1)))))))))))) | (((!! @ qML_i @ (^[Y0 : qML_i]: ((qML_r @ (sK1 @ (^[Y1 : qML_mu]: ((^[Y2 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y3 @ Y2) => (Y3 @ Y1 @ Y2)))))))) @ X0 @ (^[Y1 : qML_mu]: ((^[Y2 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y4 : qML_mu > qML_i > $o]: ((Y4 @ Y1 @ Y2) => (!! @ qML_i @ (^[Y5 : qML_i]: ((qML_r @ Y2 @ Y5) => (!! @ qML_mu @ (^[Y6 : qML_mu]: ((Y3 @ Y6 @ Y5) => (Y4 @ Y6 @ Y5)))))))))) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y2 @ Y4) => (?? @ qML_mu @ (^[Y5 : qML_mu]: (Y3 @ Y5 @ Y4))))))))))))) @ Y0) => (?? @ qML_mu @ (^[Y1 : qML_mu]: (X1 @ Y1 @ Y0))))))) = $true)) )),
% 6.96/1.31 inference(imp_proxy_clausification,[],[f418])).
% 6.96/1.31 thf(f420,plain,(
% 6.96/1.31 ( ! [X0 : qML_i,X1 : (qML_mu > qML_i > $o)] : ((((!! @ qML_i @ (^[Y0 : qML_i]: ((qML_r @ (sK1 @ (^[Y1 : qML_mu]: ((^[Y2 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y3 @ Y2) => (Y3 @ Y1 @ Y2)))))))) @ X0 @ (^[Y1 : qML_mu]: ((^[Y2 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y4 : qML_mu > qML_i > $o]: ((Y4 @ Y1 @ Y2) => (!! @ qML_i @ (^[Y5 : qML_i]: ((qML_r @ Y2 @ Y5) => (!! @ qML_mu @ (^[Y6 : qML_mu]: ((Y3 @ Y6 @ Y5) => (Y4 @ Y6 @ Y5)))))))))) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y2 @ Y4) => (?? @ qML_mu @ (^[Y5 : qML_mu]: (Y3 @ Y5 @ Y4))))))))))))) @ Y0) => (?? @ qML_mu @ (^[Y1 : qML_mu]: (X1 @ Y1 @ Y0))))))) = $true) | ($false = (((^[Y0 : qML_mu > qML_i > $o]: ((Y0 @ (sK2 @ (^[Y1 : qML_mu]: ((^[Y2 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y3 @ Y2) => (Y3 @ Y1 @ Y2)))))))) @ X0 @ (^[Y1 : qML_mu]: ((^[Y2 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y4 : qML_mu > qML_i > $o]: ((Y4 @ Y1 @ Y2) => (!! @ qML_i @ (^[Y5 : qML_i]: ((qML_r @ Y2 @ Y5) => (!! @ qML_mu @ (^[Y6 : qML_mu]: ((Y3 @ Y6 @ Y5) => (Y4 @ Y6 @ Y5)))))))))) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y2 @ Y4) => (?? @ qML_mu @ (^[Y5 : qML_mu]: (Y3 @ Y5 @ Y4))))))))))))) @ (sK1 @ (^[Y1 : qML_mu]: ((^[Y2 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y3 @ Y2) => (Y3 @ Y1 @ Y2)))))))) @ X0 @ (^[Y1 : qML_mu]: ((^[Y2 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y4 : qML_mu > qML_i > $o]: ((Y4 @ Y1 @ Y2) => (!! @ qML_i @ (^[Y5 : qML_i]: ((qML_r @ Y2 @ Y5) => (!! @ qML_mu @ (^[Y6 : qML_mu]: ((Y3 @ Y6 @ Y5) => (Y4 @ Y6 @ Y5)))))))))) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y2 @ Y4) => (?? @ qML_mu @ (^[Y5 : qML_mu]: (Y3 @ Y5 @ Y4)))))))))))))) => (!! @ qML_i @ (^[Y1 : qML_i]: ((qML_r @ (sK1 @ (^[Y2 : qML_mu]: ((^[Y3 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y4 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y4 @ Y3) => (Y4 @ Y2 @ Y3)))))))) @ X0 @ (^[Y2 : qML_mu]: ((^[Y3 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y4 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y5 : qML_mu > qML_i > $o]: ((Y5 @ Y2 @ Y3) => (!! @ qML_i @ (^[Y6 : qML_i]: ((qML_r @ Y3 @ Y6) => (!! @ qML_mu @ (^[Y7 : qML_mu]: ((Y4 @ Y7 @ Y6) => (Y5 @ Y7 @ Y6)))))))))) => (!! @ qML_i @ (^[Y5 : qML_i]: ((qML_r @ Y3 @ Y5) => (?? @ qML_mu @ (^[Y6 : qML_mu]: (Y4 @ Y6 @ Y5))))))))))))) @ Y1) => (!! @ qML_mu @ (^[Y2 : qML_mu]: ((X1 @ Y2 @ Y1) => (Y0 @ Y2 @ Y1))))))))) @ (sK12 @ X1 @ X0))))) )),
% 6.96/1.31 inference(sigma_proxy_clausification,[],[f419])).
% 6.96/1.31 thf(f421,plain,(
% 6.96/1.31 ( ! [X2 : qML_i,X0 : qML_i,X1 : (qML_mu > qML_i > $o)] : (($false = (((^[Y0 : qML_mu > qML_i > $o]: ((Y0 @ (sK2 @ (^[Y1 : qML_mu]: ((^[Y2 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y3 @ Y2) => (Y3 @ Y1 @ Y2)))))))) @ X0 @ (^[Y1 : qML_mu]: ((^[Y2 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y4 : qML_mu > qML_i > $o]: ((Y4 @ Y1 @ Y2) => (!! @ qML_i @ (^[Y5 : qML_i]: ((qML_r @ Y2 @ Y5) => (!! @ qML_mu @ (^[Y6 : qML_mu]: ((Y3 @ Y6 @ Y5) => (Y4 @ Y6 @ Y5)))))))))) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y2 @ Y4) => (?? @ qML_mu @ (^[Y5 : qML_mu]: (Y3 @ Y5 @ Y4))))))))))))) @ (sK1 @ (^[Y1 : qML_mu]: ((^[Y2 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y3 @ Y2) => (Y3 @ Y1 @ Y2)))))))) @ X0 @ (^[Y1 : qML_mu]: ((^[Y2 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y4 : qML_mu > qML_i > $o]: ((Y4 @ Y1 @ Y2) => (!! @ qML_i @ (^[Y5 : qML_i]: ((qML_r @ Y2 @ Y5) => (!! @ qML_mu @ (^[Y6 : qML_mu]: ((Y3 @ Y6 @ Y5) => (Y4 @ Y6 @ Y5)))))))))) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y2 @ Y4) => (?? @ qML_mu @ (^[Y5 : qML_mu]: (Y3 @ Y5 @ Y4)))))))))))))) => (!! @ qML_i @ (^[Y1 : qML_i]: ((qML_r @ (sK1 @ (^[Y2 : qML_mu]: ((^[Y3 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y4 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y4 @ Y3) => (Y4 @ Y2 @ Y3)))))))) @ X0 @ (^[Y2 : qML_mu]: ((^[Y3 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y4 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y5 : qML_mu > qML_i > $o]: ((Y5 @ Y2 @ Y3) => (!! @ qML_i @ (^[Y6 : qML_i]: ((qML_r @ Y3 @ Y6) => (!! @ qML_mu @ (^[Y7 : qML_mu]: ((Y4 @ Y7 @ Y6) => (Y5 @ Y7 @ Y6)))))))))) => (!! @ qML_i @ (^[Y5 : qML_i]: ((qML_r @ Y3 @ Y5) => (?? @ qML_mu @ (^[Y6 : qML_mu]: (Y4 @ Y6 @ Y5))))))))))))) @ Y1) => (!! @ qML_mu @ (^[Y2 : qML_mu]: ((X1 @ Y2 @ Y1) => (Y0 @ Y2 @ Y1))))))))) @ (sK12 @ X1 @ X0)))) | ((((^[Y0 : qML_i]: ((qML_r @ (sK1 @ (^[Y1 : qML_mu]: ((^[Y2 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y3 @ Y2) => (Y3 @ Y1 @ Y2)))))))) @ X0 @ (^[Y1 : qML_mu]: ((^[Y2 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y4 : qML_mu > qML_i > $o]: ((Y4 @ Y1 @ Y2) => (!! @ qML_i @ (^[Y5 : qML_i]: ((qML_r @ Y2 @ Y5) => (!! @ qML_mu @ (^[Y6 : qML_mu]: ((Y3 @ Y6 @ Y5) => (Y4 @ Y6 @ Y5)))))))))) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y2 @ Y4) => (?? @ qML_mu @ (^[Y5 : qML_mu]: (Y3 @ Y5 @ Y4))))))))))))) @ Y0) => (?? @ qML_mu @ (^[Y1 : qML_mu]: (X1 @ Y1 @ Y0))))) @ X2)) = $true)) )),
% 6.96/1.31 inference(pi_proxy_clausification,[],[f420])).
% 6.96/1.31 thf(f422,plain,(
% 6.96/1.31 ( ! [X2 : qML_i,X0 : qML_i,X1 : (qML_mu > qML_i > $o)] : (((((sK12 @ X1 @ X0 @ (sK2 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y2 @ Y1) => (Y2 @ Y0 @ Y1)))))))) @ X0 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((Y3 @ Y0 @ Y1) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y1 @ Y4) => (!! @ qML_mu @ (^[Y5 : qML_mu]: ((Y2 @ Y5 @ Y4) => (Y3 @ Y5 @ Y4)))))))))) => (!! @ qML_i @ (^[Y3 : qML_i]: ((qML_r @ Y1 @ Y3) => (?? @ qML_mu @ (^[Y4 : qML_mu]: (Y2 @ Y4 @ Y3))))))))))))) @ (sK1 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y2 @ Y1) => (Y2 @ Y0 @ Y1)))))))) @ X0 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((Y3 @ Y0 @ Y1) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y1 @ Y4) => (!! @ qML_mu @ (^[Y5 : qML_mu]: ((Y2 @ Y5 @ Y4) => (Y3 @ Y5 @ Y4)))))))))) => (!! @ qML_i @ (^[Y3 : qML_i]: ((qML_r @ Y1 @ Y3) => (?? @ qML_mu @ (^[Y4 : qML_mu]: (Y2 @ Y4 @ Y3)))))))))))))) => (!! @ qML_i @ (^[Y0 : qML_i]: ((qML_r @ (sK1 @ (^[Y1 : qML_mu]: ((^[Y2 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y3 @ Y2) => (Y3 @ Y1 @ Y2)))))))) @ X0 @ (^[Y1 : qML_mu]: ((^[Y2 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y4 : qML_mu > qML_i > $o]: ((Y4 @ Y1 @ Y2) => (!! @ qML_i @ (^[Y5 : qML_i]: ((qML_r @ Y2 @ Y5) => (!! @ qML_mu @ (^[Y6 : qML_mu]: ((Y3 @ Y6 @ Y5) => (Y4 @ Y6 @ Y5)))))))))) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y2 @ Y4) => (?? @ qML_mu @ (^[Y5 : qML_mu]: (Y3 @ Y5 @ Y4))))))))))))) @ Y0) => (!! @ qML_mu @ (^[Y1 : qML_mu]: ((X1 @ Y1 @ Y0) => (sK12 @ X1 @ X0 @ Y1 @ Y0))))))))) = $false) | ((((qML_r @ (sK1 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y2 @ Y1) => (Y2 @ Y0 @ Y1)))))))) @ X0 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((Y3 @ Y0 @ Y1) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y1 @ Y4) => (!! @ qML_mu @ (^[Y5 : qML_mu]: ((Y2 @ Y5 @ Y4) => (Y3 @ Y5 @ Y4)))))))))) => (!! @ qML_i @ (^[Y3 : qML_i]: ((qML_r @ Y1 @ Y3) => (?? @ qML_mu @ (^[Y4 : qML_mu]: (Y2 @ Y4 @ Y3))))))))))))) @ X2) => (?? @ qML_mu @ (^[Y0 : qML_mu]: (X1 @ Y0 @ X2))))) = $true)) )),
% 6.96/1.31 inference(beta-eta_normalization,[],[f421])).
% 6.96/1.31 thf(f423,plain,(
% 6.96/1.31 ( ! [X2 : qML_i,X0 : qML_i,X1 : (qML_mu > qML_i > $o)] : ((((!! @ qML_i @ (^[Y0 : qML_i]: ((qML_r @ (sK1 @ (^[Y1 : qML_mu]: ((^[Y2 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y3 @ Y2) => (Y3 @ Y1 @ Y2)))))))) @ X0 @ (^[Y1 : qML_mu]: ((^[Y2 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y4 : qML_mu > qML_i > $o]: ((Y4 @ Y1 @ Y2) => (!! @ qML_i @ (^[Y5 : qML_i]: ((qML_r @ Y2 @ Y5) => (!! @ qML_mu @ (^[Y6 : qML_mu]: ((Y3 @ Y6 @ Y5) => (Y4 @ Y6 @ Y5)))))))))) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y2 @ Y4) => (?? @ qML_mu @ (^[Y5 : qML_mu]: (Y3 @ Y5 @ Y4))))))))))))) @ Y0) => (!! @ qML_mu @ (^[Y1 : qML_mu]: ((X1 @ Y1 @ Y0) => (sK12 @ X1 @ X0 @ Y1 @ Y0)))))))) = $false) | ((((qML_r @ (sK1 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y2 @ Y1) => (Y2 @ Y0 @ Y1)))))))) @ X0 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((Y3 @ Y0 @ Y1) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y1 @ Y4) => (!! @ qML_mu @ (^[Y5 : qML_mu]: ((Y2 @ Y5 @ Y4) => (Y3 @ Y5 @ Y4)))))))))) => (!! @ qML_i @ (^[Y3 : qML_i]: ((qML_r @ Y1 @ Y3) => (?? @ qML_mu @ (^[Y4 : qML_mu]: (Y2 @ Y4 @ Y3))))))))))))) @ X2) => (?? @ qML_mu @ (^[Y0 : qML_mu]: (X1 @ Y0 @ X2))))) = $true)) )),
% 6.96/1.31 inference(imp_proxy_clausification,[],[f422])).
% 6.96/1.31 thf(f428,plain,(
% 6.96/1.31 ( ! [X2 : qML_i,X0 : qML_i,X1 : (qML_mu > qML_i > $o)] : (((((qML_r @ (sK1 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y2 @ Y1) => (Y2 @ Y0 @ Y1)))))))) @ X0 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((Y3 @ Y0 @ Y1) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y1 @ Y4) => (!! @ qML_mu @ (^[Y5 : qML_mu]: ((Y2 @ Y5 @ Y4) => (Y3 @ Y5 @ Y4)))))))))) => (!! @ qML_i @ (^[Y3 : qML_i]: ((qML_r @ Y1 @ Y3) => (?? @ qML_mu @ (^[Y4 : qML_mu]: (Y2 @ Y4 @ Y3))))))))))))) @ X2) => (?? @ qML_mu @ (^[Y0 : qML_mu]: (X1 @ Y0 @ X2))))) = $true) | ((((^[Y0 : qML_i]: ((qML_r @ (sK1 @ (^[Y1 : qML_mu]: ((^[Y2 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y3 @ Y2) => (Y3 @ Y1 @ Y2)))))))) @ X0 @ (^[Y1 : qML_mu]: ((^[Y2 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y4 : qML_mu > qML_i > $o]: ((Y4 @ Y1 @ Y2) => (!! @ qML_i @ (^[Y5 : qML_i]: ((qML_r @ Y2 @ Y5) => (!! @ qML_mu @ (^[Y6 : qML_mu]: ((Y3 @ Y6 @ Y5) => (Y4 @ Y6 @ Y5)))))))))) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y2 @ Y4) => (?? @ qML_mu @ (^[Y5 : qML_mu]: (Y3 @ Y5 @ Y4))))))))))))) @ Y0) => (!! @ qML_mu @ (^[Y1 : qML_mu]: ((X1 @ Y1 @ Y0) => (sK12 @ X1 @ X0 @ Y1 @ Y0)))))) @ (sK14 @ X1 @ X0))) = $false)) )),
% 6.96/1.31 inference(sigma_proxy_clausification,[],[f423])).
% 6.96/1.31 thf(f429,plain,(
% 6.96/1.31 ( ! [X2 : qML_i,X0 : qML_i,X1 : (qML_mu > qML_i > $o)] : (((((^[Y0 : qML_i]: ((qML_r @ (sK1 @ (^[Y1 : qML_mu]: ((^[Y2 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y3 @ Y2) => (Y3 @ Y1 @ Y2)))))))) @ X0 @ (^[Y1 : qML_mu]: ((^[Y2 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y4 : qML_mu > qML_i > $o]: ((Y4 @ Y1 @ Y2) => (!! @ qML_i @ (^[Y5 : qML_i]: ((qML_r @ Y2 @ Y5) => (!! @ qML_mu @ (^[Y6 : qML_mu]: ((Y3 @ Y6 @ Y5) => (Y4 @ Y6 @ Y5)))))))))) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y2 @ Y4) => (?? @ qML_mu @ (^[Y5 : qML_mu]: (Y3 @ Y5 @ Y4))))))))))))) @ Y0) => (!! @ qML_mu @ (^[Y1 : qML_mu]: ((X1 @ Y1 @ Y0) => (sK12 @ X1 @ X0 @ Y1 @ Y0)))))) @ (sK14 @ X1 @ X0))) = $false) | ($true = ((?? @ qML_mu @ (^[Y0 : qML_mu]: (X1 @ Y0 @ X2))))) | (((qML_r @ (sK1 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y2 @ Y1) => (Y2 @ Y0 @ Y1)))))))) @ X0 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((Y3 @ Y0 @ Y1) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y1 @ Y4) => (!! @ qML_mu @ (^[Y5 : qML_mu]: ((Y2 @ Y5 @ Y4) => (Y3 @ Y5 @ Y4)))))))))) => (!! @ qML_i @ (^[Y3 : qML_i]: ((qML_r @ Y1 @ Y3) => (?? @ qML_mu @ (^[Y4 : qML_mu]: (Y2 @ Y4 @ Y3))))))))))))) @ X2)) = $false)) )),
% 6.96/1.31 inference(imp_proxy_clausification,[],[f428])).
% 6.96/1.31 thf(f430,plain,(
% 6.96/1.31 ( ! [X2 : qML_i,X0 : qML_i,X1 : (qML_mu > qML_i > $o)] : (($true = (((^[Y0 : qML_mu]: (X1 @ Y0 @ X2)) @ (sK15 @ X1 @ X2)))) | (((qML_r @ (sK1 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y2 @ Y1) => (Y2 @ Y0 @ Y1)))))))) @ X0 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((Y3 @ Y0 @ Y1) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y1 @ Y4) => (!! @ qML_mu @ (^[Y5 : qML_mu]: ((Y2 @ Y5 @ Y4) => (Y3 @ Y5 @ Y4)))))))))) => (!! @ qML_i @ (^[Y3 : qML_i]: ((qML_r @ Y1 @ Y3) => (?? @ qML_mu @ (^[Y4 : qML_mu]: (Y2 @ Y4 @ Y3))))))))))))) @ X2)) = $false) | ((((^[Y0 : qML_i]: ((qML_r @ (sK1 @ (^[Y1 : qML_mu]: ((^[Y2 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y3 @ Y2) => (Y3 @ Y1 @ Y2)))))))) @ X0 @ (^[Y1 : qML_mu]: ((^[Y2 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y4 : qML_mu > qML_i > $o]: ((Y4 @ Y1 @ Y2) => (!! @ qML_i @ (^[Y5 : qML_i]: ((qML_r @ Y2 @ Y5) => (!! @ qML_mu @ (^[Y6 : qML_mu]: ((Y3 @ Y6 @ Y5) => (Y4 @ Y6 @ Y5)))))))))) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y2 @ Y4) => (?? @ qML_mu @ (^[Y5 : qML_mu]: (Y3 @ Y5 @ Y4))))))))))))) @ Y0) => (!! @ qML_mu @ (^[Y1 : qML_mu]: ((X1 @ Y1 @ Y0) => (sK12 @ X1 @ X0 @ Y1 @ Y0)))))) @ (sK14 @ X1 @ X0))) = $false)) )),
% 6.96/1.31 inference(sigma_proxy_clausification,[],[f429])).
% 6.96/1.31 thf(f431,plain,(
% 6.96/1.31 ( ! [X2 : qML_i,X0 : qML_i,X1 : (qML_mu > qML_i > $o)] : (($true = ((X1 @ (sK15 @ X1 @ X2) @ X2))) | (((qML_r @ (sK1 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y2 @ Y1) => (Y2 @ Y0 @ Y1)))))))) @ X0 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((Y3 @ Y0 @ Y1) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y1 @ Y4) => (!! @ qML_mu @ (^[Y5 : qML_mu]: ((Y2 @ Y5 @ Y4) => (Y3 @ Y5 @ Y4)))))))))) => (!! @ qML_i @ (^[Y3 : qML_i]: ((qML_r @ Y1 @ Y3) => (?? @ qML_mu @ (^[Y4 : qML_mu]: (Y2 @ Y4 @ Y3))))))))))))) @ X2)) = $false) | ($false = (((qML_r @ (sK1 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y2 @ Y1) => (Y2 @ Y0 @ Y1)))))))) @ X0 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((Y3 @ Y0 @ Y1) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y1 @ Y4) => (!! @ qML_mu @ (^[Y5 : qML_mu]: ((Y2 @ Y5 @ Y4) => (Y3 @ Y5 @ Y4)))))))))) => (!! @ qML_i @ (^[Y3 : qML_i]: ((qML_r @ Y1 @ Y3) => (?? @ qML_mu @ (^[Y4 : qML_mu]: (Y2 @ Y4 @ Y3))))))))))))) @ (sK14 @ X1 @ X0)) => (!! @ qML_mu @ (^[Y0 : qML_mu]: ((X1 @ Y0 @ (sK14 @ X1 @ X0)) => (sK12 @ X1 @ X0 @ Y0 @ (sK14 @ X1 @ X0))))))))) )),
% 6.96/1.31 inference(beta-eta_normalization,[],[f430])).
% 6.96/1.31 thf(f432,plain,(
% 6.96/1.31 ( ! [X2 : qML_i,X0 : qML_i,X1 : (qML_mu > qML_i > $o)] : ((((qML_r @ (sK1 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y2 @ Y1) => (Y2 @ Y0 @ Y1)))))))) @ X0 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((Y3 @ Y0 @ Y1) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y1 @ Y4) => (!! @ qML_mu @ (^[Y5 : qML_mu]: ((Y2 @ Y5 @ Y4) => (Y3 @ Y5 @ Y4)))))))))) => (!! @ qML_i @ (^[Y3 : qML_i]: ((qML_r @ Y1 @ Y3) => (?? @ qML_mu @ (^[Y4 : qML_mu]: (Y2 @ Y4 @ Y3))))))))))))) @ X2)) = $false) | ($false = ((!! @ qML_mu @ (^[Y0 : qML_mu]: ((X1 @ Y0 @ (sK14 @ X1 @ X0)) => (sK12 @ X1 @ X0 @ Y0 @ (sK14 @ X1 @ X0))))))) | ($true = ((X1 @ (sK15 @ X1 @ X2) @ X2)))) )),
% 6.96/1.31 inference(imp_proxy_clausification,[],[f431])).
% 6.96/1.31 thf(f434,plain,(
% 6.96/1.31 ( ! [X2 : qML_i,X0 : qML_i,X1 : (qML_mu > qML_i > $o)] : (($true = ((X1 @ (sK15 @ X1 @ X2) @ X2))) | ((((^[Y0 : qML_mu]: ((X1 @ Y0 @ (sK14 @ X1 @ X0)) => (sK12 @ X1 @ X0 @ Y0 @ (sK14 @ X1 @ X0)))) @ (sK16 @ X1 @ X0))) = $false) | (((qML_r @ (sK1 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y2 @ Y1) => (Y2 @ Y0 @ Y1)))))))) @ X0 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((Y3 @ Y0 @ Y1) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y1 @ Y4) => (!! @ qML_mu @ (^[Y5 : qML_mu]: ((Y2 @ Y5 @ Y4) => (Y3 @ Y5 @ Y4)))))))))) => (!! @ qML_i @ (^[Y3 : qML_i]: ((qML_r @ Y1 @ Y3) => (?? @ qML_mu @ (^[Y4 : qML_mu]: (Y2 @ Y4 @ Y3))))))))))))) @ X2)) = $false)) )),
% 6.96/1.31 inference(sigma_proxy_clausification,[],[f432])).
% 6.96/1.31 thf(f435,plain,(
% 6.96/1.31 ( ! [X2 : qML_i,X0 : qML_i,X1 : (qML_mu > qML_i > $o)] : (($false = (((X1 @ (sK16 @ X1 @ X0) @ (sK14 @ X1 @ X0)) => (sK12 @ X1 @ X0 @ (sK16 @ X1 @ X0) @ (sK14 @ X1 @ X0))))) | ($true = ((X1 @ (sK15 @ X1 @ X2) @ X2))) | (((qML_r @ (sK1 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y2 @ Y1) => (Y2 @ Y0 @ Y1)))))))) @ X0 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((Y3 @ Y0 @ Y1) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y1 @ Y4) => (!! @ qML_mu @ (^[Y5 : qML_mu]: ((Y2 @ Y5 @ Y4) => (Y3 @ Y5 @ Y4)))))))))) => (!! @ qML_i @ (^[Y3 : qML_i]: ((qML_r @ Y1 @ Y3) => (?? @ qML_mu @ (^[Y4 : qML_mu]: (Y2 @ Y4 @ Y3))))))))))))) @ X2)) = $false)) )),
% 6.96/1.31 inference(beta-eta_normalization,[],[f434])).
% 6.96/1.31 thf(f437,plain,(
% 6.96/1.31 ( ! [X2 : qML_i,X0 : qML_i,X1 : (qML_mu > qML_i > $o)] : (($true = ((X1 @ (sK15 @ X1 @ X2) @ X2))) | (((qML_r @ (sK1 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y2 @ Y1) => (Y2 @ Y0 @ Y1)))))))) @ X0 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((Y3 @ Y0 @ Y1) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y1 @ Y4) => (!! @ qML_mu @ (^[Y5 : qML_mu]: ((Y2 @ Y5 @ Y4) => (Y3 @ Y5 @ Y4)))))))))) => (!! @ qML_i @ (^[Y3 : qML_i]: ((qML_r @ Y1 @ Y3) => (?? @ qML_mu @ (^[Y4 : qML_mu]: (Y2 @ Y4 @ Y3))))))))))))) @ X2)) = $false) | (((X1 @ (sK16 @ X1 @ X0) @ (sK14 @ X1 @ X0))) = $true)) )),
% 6.96/1.31 inference(imp_proxy_clausification,[],[f435])).
% 6.96/1.31 thf(f449,plain,(
% 6.96/1.31 ( ! [X2 : qML_i,X0 : (qML_mu > qML_i > $o),X1 : qML_i] : ((((qML_r @ (sK1 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y2 @ Y1) => (Y2 @ Y0 @ Y1)))))))) @ X2 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((Y3 @ Y0 @ Y1) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y1 @ Y4) => (!! @ qML_mu @ (^[Y5 : qML_mu]: ((Y2 @ Y5 @ Y4) => (Y3 @ Y5 @ Y4)))))))))) => (!! @ qML_i @ (^[Y3 : qML_i]: ((qML_r @ Y1 @ Y3) => (?? @ qML_mu @ (^[Y4 : qML_mu]: (Y2 @ Y4 @ Y3))))))))))))) @ X1)) = $false) | ($false != ((X0 @ (sK15 @ X0 @ X1) @ X1))) | (((qML_r @ (sK1 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y2 @ Y1) => (Y2 @ Y0 @ Y1)))))))) @ X2 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((Y3 @ Y0 @ Y1) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y1 @ Y4) => (!! @ qML_mu @ (^[Y5 : qML_mu]: ((Y2 @ Y5 @ Y4) => (Y3 @ Y5 @ Y4)))))))))) => (!! @ qML_i @ (^[Y3 : qML_i]: ((qML_r @ Y1 @ Y3) => (?? @ qML_mu @ (^[Y4 : qML_mu]: (Y2 @ Y4 @ Y3))))))))))))) @ X1)) != $true) | (((X0 @ (sK16 @ X0 @ X2) @ (sK14 @ X0 @ X2))) = $true)) )),
% 6.96/1.31 inference(equality_factoring,[],[f437])).
% 6.96/1.31 thf(f460,plain,(
% 6.96/1.31 ( ! [X2 : qML_i,X0 : (qML_mu > qML_i > $o),X1 : qML_i] : (($false != ((X0 @ (sK15 @ X0 @ X1) @ X1))) | (((qML_r @ (sK1 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y2 @ Y1) => (Y2 @ Y0 @ Y1)))))))) @ X2 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((Y3 @ Y0 @ Y1) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y1 @ Y4) => (!! @ qML_mu @ (^[Y5 : qML_mu]: ((Y2 @ Y5 @ Y4) => (Y3 @ Y5 @ Y4)))))))))) => (!! @ qML_i @ (^[Y3 : qML_i]: ((qML_r @ Y1 @ Y3) => (?? @ qML_mu @ (^[Y4 : qML_mu]: (Y2 @ Y4 @ Y3))))))))))))) @ X1)) = $false) | (((X0 @ (sK16 @ X0 @ X2) @ (sK14 @ X0 @ X2))) = $true)) )),
% 6.96/1.31 inference(forward_subsumption_resolution,[],[f449,f140])).
% 6.96/1.31 thf(f467,plain,(
% 6.96/1.31 ( ! [X0 : qML_i,X1 : qML_i] : (($false = ((qML_r @ (sK1 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y2 @ Y1) => (Y2 @ Y0 @ Y1)))))))) @ X0 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((Y3 @ Y0 @ Y1) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y1 @ Y4) => (!! @ qML_mu @ (^[Y5 : qML_mu]: ((Y2 @ Y5 @ Y4) => (Y3 @ Y5 @ Y4)))))))))) => (!! @ qML_i @ (^[Y3 : qML_i]: ((qML_r @ Y1 @ Y3) => (?? @ qML_mu @ (^[Y4 : qML_mu]: (Y2 @ Y4 @ Y3))))))))))))) @ X1))) | ($true = (((^[Y0 : qML_mu]: ((^[Y1 : qML_i]: ($false)))) @ (sK16 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: ($false)))) @ X0) @ (sK14 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: ($false)))) @ X0))))) )),
% 6.96/1.31 inference(equality_resolution,[],[f460])).
% 6.96/1.31 thf(f468,plain,(
% 6.96/1.31 ( ! [X0 : qML_i,X1 : qML_i] : (($false = $true) | ($false = ((qML_r @ (sK1 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y2 @ Y1) => (Y2 @ Y0 @ Y1)))))))) @ X0 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((Y3 @ Y0 @ Y1) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y1 @ Y4) => (!! @ qML_mu @ (^[Y5 : qML_mu]: ((Y2 @ Y5 @ Y4) => (Y3 @ Y5 @ Y4)))))))))) => (!! @ qML_i @ (^[Y3 : qML_i]: ((qML_r @ Y1 @ Y3) => (?? @ qML_mu @ (^[Y4 : qML_mu]: (Y2 @ Y4 @ Y3))))))))))))) @ X1)))) )),
% 6.96/1.31 inference(beta-eta_normalization,[],[f467])).
% 6.96/1.31 thf(f469,plain,(
% 6.96/1.31 ( ! [X0 : qML_i,X1 : qML_i] : (($false = ((qML_r @ (sK1 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y2 @ Y1) => (Y2 @ Y0 @ Y1)))))))) @ X0 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((Y3 @ Y0 @ Y1) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y1 @ Y4) => (!! @ qML_mu @ (^[Y5 : qML_mu]: ((Y2 @ Y5 @ Y4) => (Y3 @ Y5 @ Y4)))))))))) => (!! @ qML_i @ (^[Y3 : qML_i]: ((qML_r @ Y1 @ Y3) => (?? @ qML_mu @ (^[Y4 : qML_mu]: (Y2 @ Y4 @ Y3))))))))))))) @ X1)))) )),
% 6.96/1.31 inference(trivial_inequality_removal,[],[f468])).
% 6.96/1.31 thf(f699,plain,(
% 6.96/1.31 ( ! [X0 : qML_i] : ((((qML_r @ (sK1 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (~ (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((inconsistency_P @ Y2 @ Y1) => (Y2 @ Y0 @ Y1)))))))) @ X0 @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((!! @ (qML_mu > qML_i > $o) @ (^[Y3 : qML_mu > qML_i > $o]: ((Y3 @ Y0 @ Y1) => (!! @ qML_i @ (^[Y4 : qML_i]: ((qML_r @ Y1 @ Y4) => (!! @ qML_mu @ (^[Y5 : qML_mu]: ((Y2 @ Y5 @ Y4) => (Y3 @ Y5 @ Y4)))))))))) => (!! @ qML_i @ (^[Y3 : qML_i]: ((qML_r @ Y1 @ Y3) => (?? @ qML_mu @ (^[Y4 : qML_mu]: (Y2 @ Y4 @ Y3))))))))))))) @ X0)) = $true)) )),
% 6.96/1.31 inference(unit_resulting_resolution,[],[f111,f415])).
% 6.96/1.31 thf(f700,plain,(
% 6.96/1.31 ($false = $true)),
% 6.96/1.31 inference(forward_demodulation,[],[f699,f469])).
% 6.96/1.31 thf(f701,plain,(
% 6.96/1.31 $false),
% 6.96/1.31 inference(trivial_inequality_removal,[],[f700])).
% 6.96/1.31 % SZS output end Proof for theBenchmark
% 6.96/1.31 % (2085336)------------------------------
% 6.96/1.31 % (2085336)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.96/1.31 % (2085336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.31 % (2085336)CaDiCaL version: 2.1.3
% 6.96/1.31 % (2085336)Termination reason: Refutation
% 6.96/1.31 % (2085336)Time elapsed: 0.033 s
% 6.96/1.31 % (2085336)Peak memory usage: 13 MB
% 6.96/1.31 % (2085336)Instructions burned: 138 (million)
% 6.96/1.31 % (2085120)Success in time 1.063 s
% 6.96/1.31 % Vampire exiting
%------------------------------------------------------------------------------