%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEV400^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n014.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:38:34 AM UTC 2026
% Result : Theorem 13.07s 2.21s
% Output : Refutation 13.07s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV400^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n014.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Tue Sep 29 15:44:00 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 Running higher-order theorem proving
% 0.08/0.25 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.23/0.36 % (2831544)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.23/0.36 % (2831554)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=3876825693:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.23/0.36 % (2831551)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=2053426787:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.23/0.36 % (2831550)lrs+10_16_si=on:nwc=1.5:random_seed=982385541:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.23/0.36 % (2831552)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=2723968461: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.23/0.36 % (2831549)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=2642970634:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.23/0.36 % (2831551)Instruction limit reached!
% 0.23/0.36 % (2831551)------------------------------
% 0.23/0.36 % (2831551)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.23/0.36 % (2831551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.23/0.36 % (2831551)CaDiCaL version: 2.1.3
% 0.23/0.36 % (2831551)Termination reason: Instruction limit
% 0.23/0.36 % (2831551)Termination phase: Saturation
% 0.23/0.36 % (2831551)Time elapsed: 0.003 s
% 0.23/0.36 % (2831551)Peak memory usage: 12 MB
% 0.23/0.36 % (2831551)Instructions burned: 4 (million)
% 0.23/0.36 % (2831555)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.23/0.36 % (2831555)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.23/0.36 % (2831555)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=4025532420:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.23/0.36 % (2831553)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=1518244617:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.23/0.36 % (2831550)Instruction limit reached!
% 0.23/0.36 % (2831550)------------------------------
% 0.23/0.36 % (2831550)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.23/0.36 % (2831550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.23/0.36 % (2831550)CaDiCaL version: 2.1.3
% 0.23/0.36 % (2831550)Termination reason: Instruction limit
% 0.23/0.36 % (2831550)Termination phase: Saturation
% 0.23/0.36 % (2831550)Time elapsed: 0.011 s
% 0.23/0.36 % (2831550)Peak memory usage: 12 MB
% 0.23/0.36 % (2831550)Instructions burned: 18 (million)
% 0.23/0.36 % (2831553)Refutation not found, incomplete strategy
% 0.23/0.36 % (2831553)------------------------------
% 0.23/0.36 % (2831553)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.23/0.36 % (2831553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.23/0.36 % (2831553)CaDiCaL version: 2.1.3
% 0.23/0.36 % (2831553)Termination reason: Refutation not found, incomplete strategy
% 0.23/0.36 % (2831553)Time elapsed: 0.006 s
% 0.23/0.36 % (2831553)Peak memory usage: 12 MB
% 0.23/0.36 % (2831553)Instructions burned: 9 (million)
% 0.23/0.36 % (2831554)Instruction limit reached!
% 0.23/0.36 % (2831554)------------------------------
% 0.23/0.36 % (2831554)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.23/0.36 % (2831554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.23/0.36 % (2831554)CaDiCaL version: 2.1.3
% 0.23/0.36 % (2831554)Termination reason: Instruction limit
% 0.23/0.36 % (2831554)Termination phase: Saturation
% 0.23/0.36 % (2831554)Time elapsed: 0.024 s
% 0.23/0.36 % (2831554)Peak memory usage: 12 MB
% 0.23/0.36 % (2831554)Instructions burned: 77 (million)
% 0.23/0.36 % (2831553)------------------------------
% 0.23/0.36 % (2831553)------------------------------
% 0.23/0.36 % (2831555)Refutation not found, incomplete strategy
% 0.23/0.36 % (2831555)------------------------------
% 0.23/0.36 % (2831555)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.23/0.36 % (2831555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.23/0.39 % (2831555)CaDiCaL version: 2.1.3
% 0.23/0.39 % (2831555)Termination reason: Refutation not found, incomplete strategy
% 0.23/0.39 % (2831555)Time elapsed: 0.014 s
% 0.23/0.39 % (2831555)Peak memory usage: 12 MB
% 0.23/0.39 % (2831555)Instructions burned: 24 (million)
% 0.23/0.39 % (2831555)------------------------------
% 0.23/0.39 % (2831555)------------------------------
% 0.23/0.39 % (2831561)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=1861872672:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.23/0.39 % (2831565)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.23/0.39 % (2831561)Instruction limit reached!
% 0.23/0.39 % (2831561)------------------------------
% 0.23/0.39 % (2831561)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.23/0.39 % (2831561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.23/0.39 % (2831561)CaDiCaL version: 2.1.3
% 0.23/0.39 % (2831561)Termination reason: Instruction limit
% 0.23/0.39 % (2831561)Termination phase: Saturation
% 0.23/0.39 % (2831561)Time elapsed: 0.002 s
% 0.23/0.39 % (2831561)Peak memory usage: 12 MB
% 0.23/0.39 % (2831561)Instructions burned: 2 (million)
% 0.23/0.39 % (2831565)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2379033287:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.23/0.39 % (2831564)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=416453052:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.23/0.39 % (2831565)Instruction limit reached!
% 0.23/0.39 % (2831565)------------------------------
% 0.23/0.39 % (2831565)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.23/0.39 % (2831565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.23/0.39 % (2831565)CaDiCaL version: 2.1.3
% 0.23/0.39 % (2831565)Termination reason: Instruction limit
% 0.23/0.39 % (2831565)Termination phase: Saturation
% 0.23/0.39 % (2831565)Time elapsed: 0.002 s
% 0.23/0.39 % (2831565)Peak memory usage: 12 MB
% 0.23/0.39 % (2831565)Instructions burned: 7 (million)
% 0.23/0.39 % (2831564)Instruction limit reached!
% 0.23/0.39 % (2831564)------------------------------
% 0.23/0.39 % (2831564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.23/0.39 % (2831564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.23/0.39 % (2831564)CaDiCaL version: 2.1.3
% 0.23/0.39 % (2831564)Termination reason: Instruction limit
% 0.23/0.39 % (2831564)Termination phase: Saturation
% 0.23/0.39 % (2831564)Time elapsed: 0.004 s
% 0.23/0.39 % (2831564)Peak memory usage: 12 MB
% 0.23/0.39 % (2831564)Instructions burned: 5 (million)
% 0.23/0.39 % (2831566)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=1129485873:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.23/0.39 % (2831568)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.23/0.39 % (2831568)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.23/0.39 % (2831552)Refutation not found, incomplete strategy
% 0.23/0.39 % (2831552)------------------------------
% 0.23/0.39 % (2831552)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.23/0.39 % (2831552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.23/0.39 % (2831552)CaDiCaL version: 2.1.3
% 0.23/0.39 % (2831552)Termination reason: Refutation not found, incomplete strategy
% 0.23/0.39 % (2831552)Time elapsed: 0.042 s
% 0.23/0.39 % (2831552)Peak memory usage: 12 MB
% 0.23/0.39 % (2831552)Instructions burned: 79 (million)
% 0.23/0.39 % (2831549)Instruction limit reached!
% 0.23/0.39 % (2831549)------------------------------
% 0.23/0.39 % (2831549)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.23/0.39 % (2831549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.23/0.39 % (2831549)CaDiCaL version: 2.1.3
% 0.23/0.39 % (2831549)Termination reason: Instruction limit
% 0.23/0.39 % (2831549)Termination phase: Saturation
% 0.23/0.39 % (2831549)Time elapsed: 0.043 s
% 0.92/0.42 % (2831549)Peak memory usage: 12 MB
% 0.92/0.42 % (2831549)Instructions burned: 88 (million)
% 0.92/0.42 % (2831552)------------------------------
% 0.92/0.42 % (2831552)------------------------------
% 0.92/0.42 % (2831568)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=673961277: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.92/0.42 % (2831572)lrs+10_1_si=on:cs=on:random_seed=1927691024:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.92/0.42 % (2831566)Instruction limit reached!
% 0.92/0.42 % (2831566)------------------------------
% 0.92/0.42 % (2831566)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.92/0.42 % (2831566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.92/0.42 % (2831566)CaDiCaL version: 2.1.3
% 0.92/0.42 % (2831566)Termination reason: Instruction limit
% 0.92/0.42 % (2831566)Termination phase: Saturation
% 0.92/0.42 % (2831566)Time elapsed: 0.010 s
% 0.92/0.42 % (2831566)Peak memory usage: 12 MB
% 0.92/0.42 % (2831566)Instructions burned: 12 (million)
% 0.92/0.42 % (2831569)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=1741794089:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.92/0.42 % (2831572)Instruction limit reached!
% 0.92/0.42 % (2831572)------------------------------
% 0.92/0.42 % (2831572)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.92/0.42 % (2831572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.92/0.42 % (2831572)CaDiCaL version: 2.1.3
% 0.92/0.42 % (2831572)Termination reason: Instruction limit
% 0.92/0.42 % (2831572)Termination phase: Saturation
% 0.92/0.42 % (2831572)Time elapsed: 0.004 s
% 0.92/0.42 % (2831572)Peak memory usage: 12 MB
% 0.92/0.42 % (2831572)Instructions burned: 10 (million)
% 0.92/0.42 % (2831573)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.92/0.42 % (2831573)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=2168303554:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.92/0.42 % (2831573)Instruction limit reached!
% 0.92/0.42 % (2831573)------------------------------
% 0.92/0.42 % (2831573)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.92/0.42 % (2831573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.92/0.42 % (2831573)CaDiCaL version: 2.1.3
% 0.92/0.42 % (2831573)Termination reason: Instruction limit
% 0.92/0.42 % (2831573)Termination phase: Saturation
% 0.92/0.42 % (2831573)Time elapsed: 0.002 s
% 0.92/0.42 % (2831573)Peak memory usage: 12 MB
% 0.92/0.42 % (2831573)Instructions burned: 4 (million)
% 0.92/0.42 % (2831568)Instruction limit reached!
% 0.92/0.42 % (2831568)------------------------------
% 0.92/0.42 % (2831568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.92/0.42 % (2831568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.92/0.42 % (2831568)CaDiCaL version: 2.1.3
% 0.92/0.42 % (2831568)Termination reason: Instruction limit
% 0.92/0.42 % (2831568)Termination phase: Saturation
% 0.92/0.42 % (2831568)Time elapsed: 0.015 s
% 0.92/0.42 % (2831568)Peak memory usage: 12 MB
% 0.92/0.42 % (2831568)Instructions burned: 30 (million)
% 0.92/0.42 % (2831581)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=2867923809:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2999 on theBenchmark for (2999ds/14Mi)
% 0.92/0.42 % (2831575)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=1708812661:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.92/0.42 % (2831576)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=827884933:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.92/0.42 % (2831581)Instruction limit reached!
% 0.92/0.42 % (2831581)------------------------------
% 0.92/0.42 % (2831581)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.92/0.42 % (2831581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.92/0.42 % (2831581)CaDiCaL version: 2.1.3
% 0.92/0.42 % (2831581)Termination reason: Instruction limit
% 0.92/0.42 % (2831581)Termination phase: Saturation
% 0.92/0.45 % (2831581)Time elapsed: 0.005 s
% 0.92/0.45 % (2831581)Peak memory usage: 12 MB
% 0.92/0.45 % (2831581)Instructions burned: 14 (million)
% 0.92/0.45 % (2831575)Refutation not found, incomplete strategy
% 0.92/0.45 % (2831575)------------------------------
% 0.92/0.45 % (2831575)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.92/0.45 % (2831575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.92/0.45 % (2831575)CaDiCaL version: 2.1.3
% 0.92/0.45 % (2831575)Termination reason: Refutation not found, incomplete strategy
% 0.92/0.45 % (2831575)Time elapsed: 0.005 s
% 0.92/0.45 % (2831575)Peak memory usage: 12 MB
% 0.92/0.45 % (2831575)Instructions burned: 7 (million)
% 0.92/0.45 % (2831575)------------------------------
% 0.92/0.45 % (2831575)------------------------------
% 0.92/0.45 % (2831576)Refutation not found, incomplete strategy
% 0.92/0.45 % (2831576)------------------------------
% 0.92/0.45 % (2831576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.92/0.45 % (2831576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.92/0.45 % (2831576)CaDiCaL version: 2.1.3
% 0.92/0.45 % (2831576)Termination reason: Refutation not found, incomplete strategy
% 0.92/0.45 % (2831576)Time elapsed: 0.007 s
% 0.92/0.45 % (2831576)Peak memory usage: 12 MB
% 0.92/0.45 % (2831576)Instructions burned: 11 (million)
% 0.92/0.45 % (2831576)------------------------------
% 0.92/0.45 % (2831576)------------------------------
% 0.92/0.45 % (2831588)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=4221397728: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.92/0.45 % (2831585)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=3202667531:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 0.92/0.45 % (2831584)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=3814230849:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 0.92/0.45 % (2831588)Instruction limit reached!
% 0.92/0.45 % (2831588)------------------------------
% 0.92/0.45 % (2831588)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.92/0.45 % (2831588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.92/0.45 % (2831588)CaDiCaL version: 2.1.3
% 0.92/0.45 % (2831588)Termination reason: Instruction limit
% 0.92/0.45 % (2831588)Termination phase: Saturation
% 0.92/0.45 % (2831588)Time elapsed: 0.003 s
% 0.92/0.45 % (2831588)Peak memory usage: 12 MB
% 0.92/0.45 % (2831588)Instructions burned: 9 (million)
% 0.92/0.45 % (2831579)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=3008360701:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/25Mi)
% 0.92/0.45 % (2831585)Instruction limit reached!
% 0.92/0.45 % (2831585)------------------------------
% 0.92/0.45 % (2831585)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.92/0.45 % (2831585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.92/0.45 % (2831585)CaDiCaL version: 2.1.3
% 0.92/0.45 % (2831585)Termination reason: Instruction limit
% 0.92/0.45 % (2831585)Termination phase: Saturation
% 0.92/0.45 % (2831585)Time elapsed: 0.008 s
% 0.92/0.45 % (2831585)Peak memory usage: 12 MB
% 0.92/0.45 % (2831585)Instructions burned: 14 (million)
% 0.92/0.45 % (2831589)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=2581774449:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 0.92/0.45 % (2831594)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=175779167:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 0.92/0.45 % (2831579)Refutation not found, incomplete strategy
% 0.92/0.45 % (2831579)------------------------------
% 0.92/0.45 % (2831579)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.92/0.45 % (2831579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.92/0.45 % (2831579)CaDiCaL version: 2.1.3
% 0.92/0.45 % (2831579)Termination reason: Refutation not found, incomplete strategy
% 0.92/0.45 % (2831579)Time elapsed: 0.007 s
% 0.92/0.45 % (2831579)Peak memory usage: 12 MB
% 0.92/0.45 % (2831579)Instructions burned: 5 (million)
% 0.92/0.45 % (2831590)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=1522168525:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 0.92/0.49 % (2831579)------------------------------
% 0.92/0.49 % (2831579)------------------------------
% 0.92/0.49 % (2831594)Refutation not found, incomplete strategy
% 0.92/0.49 % (2831594)------------------------------
% 0.92/0.49 % (2831594)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.92/0.49 % (2831594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.92/0.49 % (2831594)CaDiCaL version: 2.1.3
% 0.92/0.49 % (2831594)Termination reason: Refutation not found, incomplete strategy
% 0.92/0.49 % (2831594)Time elapsed: 0.005 s
% 0.92/0.49 % (2831594)Peak memory usage: 12 MB
% 0.92/0.49 % (2831594)Instructions burned: 11 (million)
% 0.92/0.49 % (2831569)Instruction limit reached!
% 0.92/0.49 % (2831569)------------------------------
% 0.92/0.49 % (2831569)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.92/0.49 % (2831569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.92/0.49 % (2831569)CaDiCaL version: 2.1.3
% 0.92/0.49 % (2831569)Termination reason: Instruction limit
% 0.92/0.49 % (2831569)Termination phase: Saturation
% 0.92/0.49 % (2831569)Time elapsed: 0.047 s
% 0.92/0.49 % (2831569)Peak memory usage: 12 MB
% 0.92/0.49 % (2831569)Instructions burned: 87 (million)
% 0.92/0.49 % (2831594)------------------------------
% 0.92/0.49 % (2831594)------------------------------
% 0.92/0.49 % (2831589)Instruction limit reached!
% 0.92/0.49 % (2831589)------------------------------
% 0.92/0.49 % (2831589)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.92/0.49 % (2831589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.92/0.49 % (2831589)CaDiCaL version: 2.1.3
% 0.92/0.49 % (2831589)Termination reason: Instruction limit
% 0.92/0.49 % (2831589)Termination phase: Saturation
% 0.92/0.49 % (2831589)Time elapsed: 0.015 s
% 0.92/0.49 % (2831589)Peak memory usage: 12 MB
% 0.92/0.49 % (2831589)Instructions burned: 27 (million)
% 0.92/0.49 % (2831590)Instruction limit reached!
% 0.92/0.49 % (2831590)------------------------------
% 0.92/0.49 % (2831590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.92/0.49 % (2831590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.92/0.49 % (2831590)CaDiCaL version: 2.1.3
% 0.92/0.49 % (2831590)Termination reason: Instruction limit
% 0.92/0.49 % (2831590)Termination phase: Saturation
% 0.92/0.49 % (2831590)Time elapsed: 0.013 s
% 0.92/0.49 % (2831590)Peak memory usage: 11 MB
% 0.92/0.49 % (2831590)Instructions burned: 25 (million)
% 0.92/0.49 % (2831596)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.92/0.49 % (2831596)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 0.92/0.49 % (2831603)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=4261362449:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 0.92/0.49 % (2831601)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=1896222028:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 0.92/0.49 % (2831600)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 0.92/0.49 % (2831603)Instruction limit reached!
% 0.92/0.49 % (2831603)------------------------------
% 0.92/0.49 % (2831603)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.92/0.49 % (2831603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.92/0.49 % (2831603)CaDiCaL version: 2.1.3
% 0.92/0.49 % (2831603)Termination reason: Instruction limit
% 0.92/0.49 % (2831603)Termination phase: Saturation
% 0.92/0.49 % (2831603)Time elapsed: 0.006 s
% 0.92/0.49 % (2831603)Peak memory usage: 11 MB
% 0.92/0.49 % (2831603)Instructions burned: 25 (million)
% 0.92/0.49 % (2831596)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=59560497:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 0.92/0.49 % (2831604)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=3274117286:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 0.92/0.49 % (2831600)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=2241277345:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.56/0.54 % (2831602)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=3371550219:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 1.56/0.54 % (2831600)Instruction limit reached!
% 1.56/0.54 % (2831600)------------------------------
% 1.56/0.54 % (2831600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.56/0.54 % (2831600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.56/0.54 % (2831600)CaDiCaL version: 2.1.3
% 1.56/0.54 % (2831600)Termination reason: Instruction limit
% 1.56/0.54 % (2831600)Termination phase: Saturation
% 1.56/0.54 % (2831600)Time elapsed: 0.006 s
% 1.56/0.54 % (2831600)Peak memory usage: 12 MB
% 1.56/0.54 % (2831600)Instructions burned: 9 (million)
% 1.56/0.54 % (2831596)Instruction limit reached!
% 1.56/0.54 % (2831596)------------------------------
% 1.56/0.54 % (2831596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.56/0.54 % (2831596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.56/0.54 % (2831596)CaDiCaL version: 2.1.3
% 1.56/0.54 % (2831596)Termination reason: Instruction limit
% 1.56/0.54 % (2831596)Termination phase: Saturation
% 1.56/0.54 % (2831596)Time elapsed: 0.009 s
% 1.56/0.54 % (2831596)Peak memory usage: 12 MB
% 1.56/0.54 % (2831596)Instructions burned: 15 (million)
% 1.56/0.54 % (2831602)Instruction limit reached!
% 1.56/0.54 % (2831602)------------------------------
% 1.56/0.54 % (2831602)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.56/0.54 % (2831602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.56/0.54 % (2831602)CaDiCaL version: 2.1.3
% 1.56/0.54 % (2831602)Termination reason: Instruction limit
% 1.56/0.54 % (2831602)Termination phase: Saturation
% 1.56/0.54 % (2831602)Time elapsed: 0.005 s
% 1.56/0.54 % (2831602)Peak memory usage: 12 MB
% 1.56/0.54 % (2831602)Instructions burned: 8 (million)
% 1.56/0.54 % (2831601)Instruction limit reached!
% 1.56/0.54 % (2831601)------------------------------
% 1.56/0.54 % (2831601)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.56/0.54 % (2831601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.56/0.54 % (2831601)CaDiCaL version: 2.1.3
% 1.56/0.54 % (2831601)Termination reason: Instruction limit
% 1.56/0.54 % (2831601)Termination phase: Saturation
% 1.56/0.54 % (2831601)Time elapsed: 0.016 s
% 1.56/0.54 % (2831601)Peak memory usage: 12 MB
% 1.56/0.54 % (2831601)Instructions burned: 32 (million)
% 1.56/0.54 % (2831604)Instruction limit reached!
% 1.56/0.54 % (2831604)------------------------------
% 1.56/0.54 % (2831604)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.56/0.54 % (2831604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.56/0.54 % (2831604)CaDiCaL version: 2.1.3
% 1.56/0.54 % (2831604)Termination reason: Instruction limit
% 1.56/0.54 % (2831604)Termination phase: Saturation
% 1.56/0.54 % (2831604)Time elapsed: 0.011 s
% 1.56/0.54 % (2831604)Peak memory usage: 12 MB
% 1.56/0.54 % (2831604)Instructions burned: 21 (million)
% 1.56/0.54 % (2831607)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=3510876916:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 1.56/0.54 % (2831615)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.56/0.54 % (2831613)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=119662772:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/193Mi)
% 1.56/0.54 % (2831612)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=3160437424:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/143Mi)
% 1.56/0.54 % (2831614)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2485667568:i=42:hud=10:rtra=on_2998 on theBenchmark for (2998ds/42Mi)
% 1.56/0.54 % (2831615)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1429305274:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2998 on theBenchmark for (2998ds/7Mi)
% 1.56/0.54 % (2831616)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=1145468819:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/181Mi)
% 1.56/0.57 % (2831615)Instruction limit reached!
% 1.56/0.57 % (2831615)------------------------------
% 1.56/0.57 % (2831615)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.56/0.57 % (2831615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.56/0.57 % (2831615)CaDiCaL version: 2.1.3
% 1.56/0.57 % (2831615)Termination reason: Instruction limit
% 1.56/0.57 % (2831615)Termination phase: Saturation
% 1.56/0.57 % (2831615)Time elapsed: 0.005 s
% 1.56/0.57 % (2831615)Peak memory usage: 12 MB
% 1.56/0.57 % (2831615)Instructions burned: 9 (million)
% 1.56/0.57 % (2831613)Refutation not found, incomplete strategy
% 1.56/0.57 % (2831613)------------------------------
% 1.56/0.57 % (2831613)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.56/0.57 % (2831613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.56/0.57 % (2831613)CaDiCaL version: 2.1.3
% 1.56/0.57 % (2831613)Termination reason: Refutation not found, incomplete strategy
% 1.56/0.57 % (2831613)Time elapsed: 0.012 s
% 1.56/0.57 % (2831613)Peak memory usage: 12 MB
% 1.56/0.57 % (2831613)Instructions burned: 20 (million)
% 1.56/0.57 % (2831613)------------------------------
% 1.56/0.57 % (2831613)------------------------------
% 1.56/0.57 % (2831614)Instruction limit reached!
% 1.56/0.57 % (2831614)------------------------------
% 1.56/0.57 % (2831614)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.56/0.57 % (2831614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.56/0.57 % (2831614)CaDiCaL version: 2.1.3
% 1.56/0.57 % (2831614)Termination reason: Instruction limit
% 1.56/0.57 % (2831614)Termination phase: Saturation
% 1.56/0.57 % (2831614)Time elapsed: 0.023 s
% 1.56/0.57 % (2831614)Peak memory usage: 12 MB
% 1.56/0.57 % (2831614)Instructions burned: 44 (million)
% 1.56/0.57 % (2831623)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=1703529987:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2997 on theBenchmark for (2997ds/169Mi)
% 1.56/0.57 % (2831624)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 1.56/0.57 % (2831624)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=2492471333:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2997 on theBenchmark for (2997ds/6Mi)
% 1.56/0.57 % (2831607)Refutation not found, incomplete strategy
% 1.56/0.57 % (2831607)------------------------------
% 1.56/0.57 % (2831607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.56/0.57 % (2831607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.56/0.57 % (2831607)CaDiCaL version: 2.1.3
% 1.56/0.57 % (2831607)Termination reason: Refutation not found, incomplete strategy
% 1.56/0.57 % (2831607)Time elapsed: 0.042 s
% 1.56/0.57 % (2831607)Peak memory usage: 12 MB
% 1.56/0.57 % (2831607)Instructions burned: 85 (million)
% 1.56/0.57 % (2831607)------------------------------
% 1.56/0.57 % (2831607)------------------------------
% 1.56/0.57 % (2831624)Instruction limit reached!
% 1.56/0.57 % (2831624)------------------------------
% 1.56/0.57 % (2831624)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.56/0.57 % (2831624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.56/0.57 % (2831624)CaDiCaL version: 2.1.3
% 1.56/0.57 % (2831624)Termination reason: Instruction limit
% 1.56/0.57 % (2831624)Termination phase: Saturation
% 1.56/0.57 % (2831624)Time elapsed: 0.004 s
% 1.56/0.57 % (2831624)Peak memory usage: 12 MB
% 1.56/0.57 % (2831624)Instructions burned: 7 (million)
% 1.56/0.57 % (2831584)Instruction limit reached!
% 1.56/0.57 % (2831584)------------------------------
% 1.56/0.57 % (2831584)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.56/0.57 % (2831584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.56/0.57 % (2831584)CaDiCaL version: 2.1.3
% 1.56/0.57 % (2831584)Termination reason: Instruction limit
% 1.56/0.57 % (2831584)Termination phase: Saturation
% 1.56/0.57 % (2831584)Time elapsed: 0.113 s
% 1.56/0.57 % (2831584)Peak memory usage: 13 MB
% 1.56/0.57 % (2831584)Instructions burned: 330 (million)
% 1.56/0.57 % (2831625)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=1810438200:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2997 on theBenchmark for (2997ds/22Mi)
% 2.22/0.63 % (2831628)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=2833742821:i=19:add=on:rtra=on_2997 on theBenchmark for (2997ds/19Mi)
% 2.22/0.63 % (2831629)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=3476515794:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/316Mi)
% 2.22/0.63 % (2831625)Instruction limit reached!
% 2.22/0.63 % (2831625)------------------------------
% 2.22/0.63 % (2831625)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.22/0.63 % (2831625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.22/0.63 % (2831625)CaDiCaL version: 2.1.3
% 2.22/0.63 % (2831625)Termination reason: Instruction limit
% 2.22/0.63 % (2831625)Termination phase: Saturation
% 2.22/0.63 % (2831625)Time elapsed: 0.017 s
% 2.22/0.63 % (2831625)Peak memory usage: 12 MB
% 2.22/0.63 % (2831625)Instructions burned: 22 (million)
% 2.22/0.63 % (2831628)Instruction limit reached!
% 2.22/0.63 % (2831628)------------------------------
% 2.22/0.63 % (2831628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.22/0.63 % (2831628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.22/0.63 % (2831628)CaDiCaL version: 2.1.3
% 2.22/0.63 % (2831628)Termination reason: Instruction limit
% 2.22/0.63 % (2831628)Termination phase: Saturation
% 2.22/0.63 % (2831628)Time elapsed: 0.010 s
% 2.22/0.63 % (2831628)Peak memory usage: 12 MB
% 2.22/0.63 % (2831628)Instructions burned: 19 (million)
% 2.22/0.63 % (2831630)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=710518440: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.22/0.63 % (2831630)Refutation not found, incomplete strategy
% 2.22/0.63 % (2831630)------------------------------
% 2.22/0.63 % (2831630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.22/0.63 % (2831630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.22/0.63 % (2831630)CaDiCaL version: 2.1.3
% 2.22/0.63 % (2831630)Termination reason: Refutation not found, incomplete strategy
% 2.22/0.63 % (2831630)Time elapsed: 0.007 s
% 2.22/0.63 % (2831630)Peak memory usage: 12 MB
% 2.22/0.63 % (2831630)Instructions burned: 10 (million)
% 2.22/0.63 % (2831612)Instruction limit reached!
% 2.22/0.63 % (2831612)------------------------------
% 2.22/0.63 % (2831612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.22/0.63 % (2831612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.22/0.63 % (2831612)CaDiCaL version: 2.1.3
% 2.22/0.63 % (2831612)Termination reason: Instruction limit
% 2.22/0.63 % (2831612)Termination phase: Saturation
% 2.22/0.63 % (2831612)Time elapsed: 0.073 s
% 2.22/0.63 % (2831612)Peak memory usage: 13 MB
% 2.22/0.63 % (2831612)Instructions burned: 144 (million)
% 2.22/0.63 % (2831630)------------------------------
% 2.22/0.63 % (2831630)------------------------------
% 2.22/0.63 % (2831634)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=3416451732: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.22/0.63 % (2831635)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=4218587998:i=480:rtra=on_2997 on theBenchmark for (2997ds/480Mi)
% 2.22/0.63 % (2831637)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=704067825: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.22/0.63 % (2831634)Refutation not found, incomplete strategy
% 2.22/0.63 % (2831634)------------------------------
% 2.22/0.63 % (2831634)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.22/0.63 % (2831634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.22/0.63 % (2831634)CaDiCaL version: 2.1.3
% 2.22/0.63 % (2831634)Termination reason: Refutation not found, incomplete strategy
% 2.22/0.63 % (2831634)Time elapsed: 0.008 s
% 2.22/0.63 % (2831634)Peak memory usage: 12 MB
% 2.22/0.63 % (2831634)Instructions burned: 12 (million)
% 2.69/0.71 % (2831634)------------------------------
% 2.69/0.71 % (2831634)------------------------------
% 2.69/0.71 % (2831638)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 2.69/0.71 % (2831635)Refutation not found, incomplete strategy
% 2.69/0.71 % (2831635)------------------------------
% 2.69/0.71 % (2831635)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.71 % (2831635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.71 % (2831635)CaDiCaL version: 2.1.3
% 2.69/0.71 % (2831635)Termination reason: Refutation not found, incomplete strategy
% 2.69/0.71 % (2831635)Time elapsed: 0.007 s
% 2.69/0.71 % (2831635)Peak memory usage: 12 MB
% 2.69/0.71 % (2831635)Instructions burned: 11 (million)
% 2.69/0.71 % (2831635)------------------------------
% 2.69/0.71 % (2831635)------------------------------
% 2.69/0.71 % (2831638)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=81414903:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/200Mi)
% 2.69/0.71 % (2831637)Instruction limit reached!
% 2.69/0.71 % (2831637)------------------------------
% 2.69/0.71 % (2831637)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.71 % (2831637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.71 % (2831637)CaDiCaL version: 2.1.3
% 2.69/0.71 % (2831637)Termination reason: Instruction limit
% 2.69/0.71 % (2831637)Termination phase: Saturation
% 2.69/0.71 % (2831637)Time elapsed: 0.009 s
% 2.69/0.71 % (2831637)Peak memory usage: 12 MB
% 2.69/0.71 % (2831637)Instructions burned: 23 (million)
% 2.69/0.71 % (2831616)Instruction limit reached!
% 2.69/0.71 % (2831616)------------------------------
% 2.69/0.71 % (2831616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.71 % (2831616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.71 % (2831616)CaDiCaL version: 2.1.3
% 2.69/0.71 % (2831616)Termination reason: Instruction limit
% 2.69/0.71 % (2831616)Termination phase: Saturation
% 2.69/0.71 % (2831616)Time elapsed: 0.093 s
% 2.69/0.71 % (2831616)Peak memory usage: 13 MB
% 2.69/0.71 % (2831616)Instructions burned: 181 (million)
% 2.69/0.71 % (2831645)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=3956677261:i=51:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/51Mi)
% 2.69/0.71 % (2831642)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=3359778280:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2997 on theBenchmark for (2997ds/13Mi)
% 2.69/0.71 % (2831644)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=3251279776:i=66:s2at=3:nm=2:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/66Mi)
% 2.69/0.71 % (2831646)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=693870054:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/31Mi)
% 2.69/0.71 % (2831642)Instruction limit reached!
% 2.69/0.71 % (2831642)------------------------------
% 2.69/0.71 % (2831642)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.71 % (2831642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.71 % (2831642)CaDiCaL version: 2.1.3
% 2.69/0.71 % (2831642)Termination reason: Instruction limit
% 2.69/0.71 % (2831642)Termination phase: Saturation
% 2.69/0.71 % (2831642)Time elapsed: 0.008 s
% 2.69/0.71 % (2831642)Peak memory usage: 12 MB
% 2.69/0.71 % (2831642)Instructions burned: 13 (million)
% 2.69/0.71 % (2831623)Instruction limit reached!
% 2.69/0.71 % (2831623)------------------------------
% 2.69/0.71 % (2831623)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.71 % (2831623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.71 % (2831623)CaDiCaL version: 2.1.3
% 2.69/0.71 % (2831623)Termination reason: Instruction limit
% 2.69/0.71 % (2831623)Termination phase: Saturation
% 2.69/0.71 % (2831623)Time elapsed: 0.092 s
% 2.69/0.71 % (2831623)Peak memory usage: 13 MB
% 2.69/0.71 % (2831623)Instructions burned: 170 (million)
% 2.69/0.71 % (2831645)Instruction limit reached!
% 2.69/0.71 % (2831645)------------------------------
% 2.69/0.71 % (2831645)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.71 % (2831645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.77 % (2831645)CaDiCaL version: 2.1.3
% 2.69/0.77 % (2831645)Termination reason: Instruction limit
% 2.69/0.77 % (2831645)Termination phase: Saturation
% 2.69/0.77 % (2831645)Time elapsed: 0.015 s
% 2.69/0.77 % (2831645)Peak memory usage: 12 MB
% 2.69/0.77 % (2831645)Instructions burned: 53 (million)
% 2.69/0.77 % (2831646)Instruction limit reached!
% 2.69/0.77 % (2831646)------------------------------
% 2.69/0.77 % (2831646)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.77 % (2831646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.77 % (2831646)CaDiCaL version: 2.1.3
% 2.69/0.77 % (2831646)Termination reason: Instruction limit
% 2.69/0.77 % (2831646)Termination phase: Saturation
% 2.69/0.77 % (2831646)Time elapsed: 0.015 s
% 2.69/0.77 % (2831646)Peak memory usage: 12 MB
% 2.69/0.77 % (2831646)Instructions burned: 31 (million)
% 2.69/0.77 % (2831653)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=3976007617:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2996 on theBenchmark for (2996ds/67Mi)
% 2.69/0.77 % (2831654)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 2.69/0.77 % (2831654)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=8090414:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2996 on theBenchmark for (2996ds/180Mi)
% 2.69/0.77 % (2831644)Instruction limit reached!
% 2.69/0.77 % (2831644)------------------------------
% 2.69/0.77 % (2831644)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.77 % (2831644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.77 % (2831644)CaDiCaL version: 2.1.3
% 2.69/0.77 % (2831644)Termination reason: Instruction limit
% 2.69/0.77 % (2831644)Termination phase: Saturation
% 2.69/0.77 % (2831644)Time elapsed: 0.038 s
% 2.69/0.77 % (2831644)Peak memory usage: 13 MB
% 2.69/0.77 % (2831644)Instructions burned: 67 (million)
% 2.69/0.77 % (2831651)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=280315481:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2996 on theBenchmark for (2996ds/137Mi)
% 2.69/0.77 % (2831652)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=3909427320:cond=on:i=34:hud=10:nm=10:rtra=on_2996 on theBenchmark for (2996ds/34Mi)
% 2.69/0.77 % (2831651)Refutation not found, incomplete strategy
% 2.69/0.77 % (2831651)------------------------------
% 2.69/0.77 % (2831651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.77 % (2831651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.77 % (2831651)CaDiCaL version: 2.1.3
% 2.69/0.77 % (2831651)Termination reason: Refutation not found, incomplete strategy
% 2.69/0.77 % (2831651)Time elapsed: 0.017 s
% 2.69/0.77 % (2831651)Peak memory usage: 12 MB
% 2.69/0.77 % (2831651)Instructions burned: 10 (million)
% 2.69/0.77 % (2831651)------------------------------
% 2.69/0.77 % (2831651)------------------------------
% 2.69/0.77 % (2831658)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=1167954195:st=2:i=246:sd=3:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/246Mi)
% 2.69/0.77 % (2831638)Instruction limit reached!
% 2.69/0.77 % (2831638)------------------------------
% 2.69/0.77 % (2831638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.77 % (2831638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.77 % (2831638)CaDiCaL version: 2.1.3
% 2.69/0.77 % (2831638)Termination reason: Instruction limit
% 2.69/0.77 % (2831638)Termination phase: Saturation
% 2.69/0.77 % (2831638)Time elapsed: 0.085 s
% 2.69/0.77 % (2831638)Peak memory usage: 12 MB
% 2.69/0.77 % (2831638)Instructions burned: 202 (million)
% 2.69/0.77 % (2831658)Refutation not found, incomplete strategy
% 2.69/0.77 % (2831658)------------------------------
% 2.69/0.77 % (2831658)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.77 % (2831658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.77 % (2831658)CaDiCaL version: 2.1.3
% 2.69/0.77 % (2831658)Termination reason: Refutation not found, incomplete strategy
% 2.69/0.77 % (2831658)Time elapsed: 0.011 s
% 2.69/0.77 % (2831658)Peak memory usage: 12 MB
% 2.69/0.77 % (2831658)Instructions burned: 19 (million)
% 2.69/0.77 % (2831652)Instruction limit reached!
% 2.69/0.77 % (2831652)------------------------------
% 2.69/0.77 % (2831652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.41/0.90 % (2831652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.41/0.90 % (2831652)CaDiCaL version: 2.1.3
% 3.41/0.90 % (2831652)Termination reason: Instruction limit
% 3.41/0.90 % (2831652)Termination phase: Saturation
% 3.41/0.90 % (2831652)Time elapsed: 0.025 s
% 3.41/0.90 % (2831652)Peak memory usage: 12 MB
% 3.41/0.90 % (2831652)Instructions burned: 36 (million)
% 3.41/0.90 % (2831658)------------------------------
% 3.41/0.90 % (2831658)------------------------------
% 3.41/0.90 % (2831662)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=1041043049:i=427:sd=1:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/427Mi)
% 3.41/0.90 % (2831661)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=386855846:cond=on:i=96:bd=all:rtra=on_2996 on theBenchmark for (2996ds/96Mi)
% 3.41/0.90 % (2831653)Instruction limit reached!
% 3.41/0.90 % (2831653)------------------------------
% 3.41/0.90 % (2831653)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.41/0.90 % (2831653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.41/0.90 % (2831653)CaDiCaL version: 2.1.3
% 3.41/0.90 % (2831653)Termination reason: Instruction limit
% 3.41/0.90 % (2831653)Termination phase: Saturation
% 3.41/0.90 % (2831653)Time elapsed: 0.056 s
% 3.41/0.90 % (2831653)Peak memory usage: 12 MB
% 3.41/0.90 % (2831653)Instructions burned: 69 (million)
% 3.41/0.90 % (2831663)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=2155609676:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/874Mi)
% 3.41/0.90 % (2831629)Instruction limit reached!
% 3.41/0.90 % (2831629)------------------------------
% 3.41/0.90 % (2831629)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.41/0.90 % (2831629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.41/0.90 % (2831629)CaDiCaL version: 2.1.3
% 3.41/0.90 % (2831629)Termination reason: Instruction limit
% 3.41/0.90 % (2831629)Termination phase: Saturation
% 3.41/0.90 % (2831629)Time elapsed: 0.158 s
% 3.41/0.90 % (2831629)Peak memory usage: 13 MB
% 3.41/0.90 % (2831629)Instructions burned: 317 (million)
% 3.41/0.90 % (2831664)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=3436277727:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/515Mi)
% 3.41/0.90 % (2831667)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=1868061123:st=1.5:i=130:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/130Mi)
% 3.41/0.90 % (2831654)Instruction limit reached!
% 3.41/0.90 % (2831654)------------------------------
% 3.41/0.90 % (2831654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.41/0.90 % (2831654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.41/0.90 % (2831654)CaDiCaL version: 2.1.3
% 3.41/0.90 % (2831654)Termination reason: Instruction limit
% 3.41/0.90 % (2831654)Termination phase: Saturation
% 3.41/0.90 % (2831654)Time elapsed: 0.077 s
% 3.41/0.90 % (2831654)Peak memory usage: 13 MB
% 3.41/0.90 % (2831654)Instructions burned: 180 (million)
% 3.41/0.90 % (2831669)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=967181700:i=44:ep=R:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/44Mi)
% 3.41/0.90 % (2831661)Refutation not found, incomplete strategy
% 3.41/0.90 % (2831661)------------------------------
% 3.41/0.90 % (2831661)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.41/0.90 % (2831661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.41/0.90 % (2831661)CaDiCaL version: 2.1.3
% 3.41/0.90 % (2831661)Termination reason: Refutation not found, incomplete strategy
% 3.41/0.90 % (2831661)Time elapsed: 0.040 s
% 3.41/0.90 % (2831661)Peak memory usage: 12 MB
% 3.41/0.90 % (2831661)Instructions burned: 71 (million)
% 3.41/0.90 % (2831661)------------------------------
% 3.41/0.90 % (2831661)------------------------------
% 3.41/0.90 % (2831672)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=3785867314:s2a=on:i=571:nm=16:rtra=on_2995 on theBenchmark for (2995ds/571Mi)
% 3.41/0.90 % (2831672)Refutation not found, incomplete strategy
% 3.41/0.90 % (2831672)------------------------------
% 3.41/0.90 % (2831672)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.41/0.90 % (2831672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.41/1.01 % (2831672)CaDiCaL version: 2.1.3
% 3.41/1.01 % (2831672)Termination reason: Refutation not found, incomplete strategy
% 3.41/1.01 % (2831672)Time elapsed: 0.009 s
% 3.41/1.01 % (2831672)Peak memory usage: 12 MB
% 3.41/1.01 % (2831672)Instructions burned: 15 (million)
% 3.41/1.01 % (2831669)Instruction limit reached!
% 3.41/1.01 % (2831669)------------------------------
% 3.41/1.01 % (2831669)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.41/1.01 % (2831669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.41/1.01 % (2831669)CaDiCaL version: 2.1.3
% 3.41/1.01 % (2831669)Termination reason: Instruction limit
% 3.41/1.01 % (2831669)Termination phase: Saturation
% 3.41/1.01 % (2831669)Time elapsed: 0.023 s
% 3.41/1.01 % (2831669)Peak memory usage: 12 MB
% 3.41/1.01 % (2831669)Instructions burned: 44 (million)
% 3.41/1.01 % (2831672)------------------------------
% 3.41/1.01 % (2831672)------------------------------
% 3.41/1.01 % (2831674)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=3117337286:i=450:rtra=on:ixr=off:ntd=on_2995 on theBenchmark for (2995ds/450Mi)
% 3.41/1.01 % (2831674)Refutation not found, incomplete strategy
% 3.41/1.01 % (2831674)------------------------------
% 3.41/1.01 % (2831674)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.41/1.01 % (2831674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.41/1.01 % (2831674)CaDiCaL version: 2.1.3
% 3.41/1.01 % (2831674)Termination reason: Refutation not found, incomplete strategy
% 3.41/1.01 % (2831674)Time elapsed: 0.002 s
% 3.41/1.01 % (2831674)Peak memory usage: 12 MB
% 3.41/1.01 % (2831674)Instructions burned: 2 (million)
% 3.41/1.01 % (2831674)------------------------------
% 3.41/1.01 % (2831674)------------------------------
% 3.41/1.01 % (2831677)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=3792213824:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2995 on theBenchmark for (2995ds/65Mi)
% 3.41/1.01 % (2831676)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=2144412947:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/95Mi)
% 3.41/1.01 % (2831679)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=1123786041: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.41/1.01 % (2831667)Instruction limit reached!
% 3.41/1.01 % (2831667)------------------------------
% 3.41/1.01 % (2831667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.41/1.01 % (2831667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.41/1.01 % (2831667)CaDiCaL version: 2.1.3
% 3.41/1.01 % (2831667)Termination reason: Instruction limit
% 3.41/1.01 % (2831667)Termination phase: Saturation
% 3.41/1.01 % (2831667)Time elapsed: 0.076 s
% 3.41/1.01 % (2831667)Peak memory usage: 12 MB
% 3.41/1.01 % (2831667)Instructions burned: 130 (million)
% 3.41/1.01 % (2831677)Instruction limit reached!
% 3.41/1.01 % (2831677)------------------------------
% 3.41/1.01 % (2831677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.41/1.01 % (2831677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.41/1.01 % (2831677)CaDiCaL version: 2.1.3
% 3.41/1.01 % (2831677)Termination reason: Instruction limit
% 3.41/1.01 % (2831677)Termination phase: Saturation
% 3.41/1.01 % (2831677)Time elapsed: 0.033 s
% 3.41/1.01 % (2831677)Peak memory usage: 12 MB
% 3.41/1.01 % (2831677)Instructions burned: 65 (million)
% 3.41/1.01 % (2831662)Instruction limit reached!
% 3.41/1.01 % (2831662)------------------------------
% 3.41/1.01 % (2831662)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.41/1.01 % (2831662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.41/1.01 % (2831662)CaDiCaL version: 2.1.3
% 3.41/1.01 % (2831662)Termination reason: Instruction limit
% 3.41/1.01 % (2831662)Termination phase: Saturation
% 3.41/1.01 % (2831662)Time elapsed: 0.121 s
% 3.41/1.01 % (2831662)Peak memory usage: 14 MB
% 3.41/1.01 % (2831662)Instructions burned: 428 (million)
% 3.41/1.01 % (2831683)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=3197824318: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)
% 5.29/1.12 % (2831685)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=3446112239:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2994 on theBenchmark for (2994ds/495Mi)
% 5.29/1.12 % (2831676)Instruction limit reached!
% 5.29/1.12 % (2831676)------------------------------
% 5.29/1.12 % (2831676)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.29/1.12 % (2831676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.29/1.12 % (2831676)CaDiCaL version: 2.1.3
% 5.29/1.12 % (2831676)Termination reason: Instruction limit
% 5.29/1.12 % (2831676)Termination phase: Saturation
% 5.29/1.12 % (2831676)Time elapsed: 0.052 s
% 5.29/1.12 % (2831676)Peak memory usage: 13 MB
% 5.29/1.12 % (2831684)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=82508051:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/375Mi)
% 5.29/1.12 % (2831676)Instructions burned: 97 (million)
% 5.29/1.12 % (2831679)Instruction limit reached!
% 5.29/1.12 % (2831679)------------------------------
% 5.29/1.12 % (2831679)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.29/1.12 % (2831679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.29/1.12 % (2831679)CaDiCaL version: 2.1.3
% 5.29/1.12 % (2831679)Termination reason: Instruction limit
% 5.29/1.12 % (2831679)Termination phase: Saturation
% 5.29/1.12 % (2831679)Time elapsed: 0.051 s
% 5.29/1.12 % (2831679)Peak memory usage: 12 MB
% 5.29/1.12 % (2831679)Instructions burned: 106 (million)
% 5.29/1.12 % (2831689)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=1664375877:cond=on:i=34:hud=10:nm=10:rtra=on_2994 on theBenchmark for (2994ds/34Mi)
% 5.29/1.12 % (2831690)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=971157447:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2994 on theBenchmark for (2994ds/91Mi)
% 5.29/1.12 % (2831689)Instruction limit reached!
% 5.29/1.12 % (2831689)------------------------------
% 5.29/1.12 % (2831689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.29/1.12 % (2831689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.29/1.12 % (2831689)CaDiCaL version: 2.1.3
% 5.29/1.12 % (2831689)Termination reason: Instruction limit
% 5.29/1.12 % (2831689)Termination phase: Saturation
% 5.29/1.12 % (2831689)Time elapsed: 0.017 s
% 5.29/1.12 % (2831689)Peak memory usage: 12 MB
% 5.29/1.12 % (2831689)Instructions burned: 35 (million)
% 5.29/1.12 % (2831693)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=3187508068: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)
% 5.29/1.12 % (2831693)Instruction limit reached!
% 5.29/1.12 % (2831693)------------------------------
% 5.29/1.12 % (2831693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.29/1.12 % (2831693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.29/1.12 % (2831693)CaDiCaL version: 2.1.3
% 5.29/1.12 % (2831693)Termination reason: Instruction limit
% 5.29/1.12 % (2831693)Termination phase: Saturation
% 5.29/1.12 % (2831693)Time elapsed: 0.035 s
% 5.29/1.12 % (2831693)Peak memory usage: 12 MB
% 5.29/1.12 % (2831693)Instructions burned: 66 (million)
% 5.29/1.12 % (2831690)Instruction limit reached!
% 5.29/1.12 % (2831690)------------------------------
% 5.29/1.12 % (2831690)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.29/1.12 % (2831690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.29/1.12 % (2831690)CaDiCaL version: 2.1.3
% 5.29/1.12 % (2831690)Termination reason: Instruction limit
% 5.29/1.12 % (2831690)Termination phase: Saturation
% 5.29/1.12 % (2831690)Time elapsed: 0.072 s
% 5.29/1.12 % (2831690)Peak memory usage: 12 MB
% 5.29/1.12 % (2831690)Instructions burned: 91 (million)
% 5.29/1.12 % (2831695)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=1591663694:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2993 on theBenchmark for (2993ds/22Mi)
% 5.29/1.12 % (2831695)Instruction limit reached!
% 5.29/1.12 % (2831695)------------------------------
% 5.29/1.12 % (2831695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.29/1.12 % (2831695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.75/1.19 % (2831695)CaDiCaL version: 2.1.3
% 5.75/1.19 % (2831695)Termination reason: Instruction limit
% 5.75/1.19 % (2831695)Termination phase: Saturation
% 5.75/1.19 % (2831695)Time elapsed: 0.011 s
% 5.75/1.19 % (2831695)Peak memory usage: 12 MB
% 5.75/1.19 % (2831695)Instructions burned: 22 (million)
% 5.75/1.19 % (2831685)Instruction limit reached!
% 5.75/1.19 % (2831685)------------------------------
% 5.75/1.19 % (2831685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.75/1.19 % (2831685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.75/1.19 % (2831685)CaDiCaL version: 2.1.3
% 5.75/1.19 % (2831685)Termination reason: Instruction limit
% 5.75/1.19 % (2831685)Termination phase: Saturation
% 5.75/1.19 % (2831685)Time elapsed: 0.127 s
% 5.75/1.19 % (2831685)Peak memory usage: 14 MB
% 5.75/1.19 % (2831685)Instructions burned: 495 (million)
% 5.75/1.19 % (2831696)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=36063687:i=338:bd=all:ins=4:rtra=on_2993 on theBenchmark for (2993ds/338Mi)
% 5.75/1.19 % (2831699)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 5.75/1.19 % (2831699)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=2349005631:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2993 on theBenchmark for (2993ds/137Mi)
% 5.75/1.19 % (2831698)lrs+10_1_sil=128000:si=on:urr=on:random_seed=1676816955:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2993 on theBenchmark for (2993ds/28Mi)
% 5.75/1.19 % (2831699)Refutation not found, incomplete strategy
% 5.75/1.19 % (2831699)------------------------------
% 5.75/1.19 % (2831699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.75/1.19 % (2831699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.75/1.19 % (2831699)CaDiCaL version: 2.1.3
% 5.75/1.19 % (2831699)Termination reason: Refutation not found, incomplete strategy
% 5.75/1.19 % (2831699)Time elapsed: 0.011 s
% 5.75/1.19 % (2831699)Peak memory usage: 12 MB
% 5.75/1.19 % (2831699)Instructions burned: 44 (million)
% 5.75/1.19 % (2831699)------------------------------
% 5.75/1.19 % (2831699)------------------------------
% 5.75/1.19 % (2831703)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=843326929:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2993 on theBenchmark for (2993ds/340Mi)
% 5.75/1.19 % (2831698)Instruction limit reached!
% 5.75/1.19 % (2831698)------------------------------
% 5.75/1.19 % (2831698)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.75/1.19 % (2831698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.75/1.19 % (2831698)CaDiCaL version: 2.1.3
% 5.75/1.19 % (2831698)Termination reason: Instruction limit
% 5.75/1.19 % (2831698)Termination phase: Saturation
% 5.75/1.19 % (2831698)Time elapsed: 0.016 s
% 5.75/1.19 % (2831698)Peak memory usage: 12 MB
% 5.75/1.19 % (2831698)Instructions burned: 28 (million)
% 5.75/1.19 % (2831705)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=2110598899:i=227:sd=1:bd=all:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/227Mi)
% 5.75/1.19 % (2831684)Instruction limit reached!
% 5.75/1.19 % (2831684)------------------------------
% 5.75/1.19 % (2831684)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.75/1.19 % (2831684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.75/1.19 % (2831684)CaDiCaL version: 2.1.3
% 5.75/1.19 % (2831684)Termination reason: Instruction limit
% 5.75/1.19 % (2831684)Termination phase: Saturation
% 5.75/1.19 % (2831684)Time elapsed: 0.189 s
% 5.75/1.19 % (2831684)Peak memory usage: 13 MB
% 5.75/1.19 % (2831684)Instructions burned: 375 (million)
% 5.75/1.19 % (2831707)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 5.75/1.19 % (2831707)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=3186191473:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2992 on theBenchmark for (2992ds/373Mi)
% 5.75/1.19 % (2831703)Instruction limit reached!
% 5.75/1.19 % (2831703)------------------------------
% 5.75/1.19 % (2831703)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.75/1.19 % (2831703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.18/1.24 % (2831703)CaDiCaL version: 2.1.3
% 6.18/1.24 % (2831703)Termination reason: Instruction limit
% 6.18/1.24 % (2831703)Termination phase: Saturation
% 6.18/1.24 % (2831703)Time elapsed: 0.077 s
% 6.18/1.24 % (2831703)Peak memory usage: 12 MB
% 6.18/1.24 % (2831703)Instructions burned: 342 (million)
% 6.18/1.24 % (2831709)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=2102619081:i=116:ep=RSTC:rtra=on:ntd=on_2992 on theBenchmark for (2992ds/116Mi)
% 6.18/1.24 % (2831709)Refutation not found, incomplete strategy
% 6.18/1.24 % (2831709)------------------------------
% 6.18/1.24 % (2831709)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.18/1.24 % (2831709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.18/1.24 % (2831709)CaDiCaL version: 2.1.3
% 6.18/1.24 % (2831709)Termination reason: Refutation not found, incomplete strategy
% 6.18/1.24 % (2831709)Time elapsed: 0.001 s
% 6.18/1.24 % (2831709)Peak memory usage: 12 MB
% 6.18/1.24 % (2831709)Instructions burned: 2 (million)
% 6.18/1.24 % (2831709)------------------------------
% 6.18/1.24 % (2831709)------------------------------
% 6.18/1.24 % (2831711)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=1294094976:i=575:rtra=on_2992 on theBenchmark for (2992ds/575Mi)
% 6.18/1.24 % (2831663)Instruction limit reached!
% 6.18/1.24 % (2831663)------------------------------
% 6.18/1.24 % (2831663)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.18/1.24 % (2831663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.18/1.24 % (2831663)CaDiCaL version: 2.1.3
% 6.18/1.24 % (2831663)Termination reason: Instruction limit
% 6.18/1.24 % (2831663)Termination phase: Saturation
% 6.18/1.24 % (2831663)Time elapsed: 0.400 s
% 6.18/1.24 % (2831663)Peak memory usage: 14 MB
% 6.18/1.24 % (2831663)Instructions burned: 876 (million)
% 6.18/1.24 % (2831705)Instruction limit reached!
% 6.18/1.24 % (2831705)------------------------------
% 6.18/1.24 % (2831705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.18/1.24 % (2831705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.18/1.24 % (2831705)CaDiCaL version: 2.1.3
% 6.18/1.24 % (2831705)Termination reason: Instruction limit
% 6.18/1.24 % (2831705)Termination phase: Saturation
% 6.18/1.24 % (2831705)Time elapsed: 0.110 s
% 6.18/1.24 % (2831705)Peak memory usage: 12 MB
% 6.18/1.24 % (2831705)Instructions burned: 228 (million)
% 6.18/1.24 % (2831713)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=3637509497:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2992 on theBenchmark for (2992ds/270Mi)
% 6.18/1.24 % (2831696)Instruction limit reached!
% 6.18/1.24 % (2831696)------------------------------
% 6.18/1.24 % (2831696)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.18/1.24 % (2831696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.18/1.24 % (2831696)CaDiCaL version: 2.1.3
% 6.18/1.24 % (2831696)Termination reason: Instruction limit
% 6.18/1.24 % (2831696)Termination phase: Saturation
% 6.18/1.24 % (2831696)Time elapsed: 0.166 s
% 6.18/1.24 % (2831696)Peak memory usage: 14 MB
% 6.18/1.24 % (2831696)Instructions burned: 339 (million)
% 6.18/1.24 % (2831714)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=2159425415: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_2991 on theBenchmark for (2991ds/9840Mi)
% 6.18/1.24 % (2831716)lrs+1010_1_sil=128000:si=on:sos=all:uwa=off:nwc=1:random_seed=901747862:i=421:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/421Mi)
% 6.18/1.24 % (2831664)Instruction limit reached!
% 6.18/1.24 % (2831664)------------------------------
% 6.18/1.24 % (2831664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.18/1.24 % (2831664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.18/1.24 % (2831664)CaDiCaL version: 2.1.3
% 6.18/1.24 % (2831664)Termination reason: Instruction limit
% 6.18/1.24 % (2831664)Termination phase: Saturation
% 6.18/1.24 % (2831664)Time elapsed: 0.434 s
% 6.18/1.24 % (2831664)Peak memory usage: 14 MB
% 6.18/1.24 % (2831664)Instructions burned: 516 (million)
% 6.18/1.24 % (2831719)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
% 7.41/1.41 % (2831719)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=715745306:avsq=on:i=270:s2at=3:avsqr=1,16:rtra=on:ntd=on_2991 on theBenchmark for (2991ds/270Mi)
% 7.41/1.41 % (2831719)Refutation not found, incomplete strategy
% 7.41/1.41 % (2831719)------------------------------
% 7.41/1.41 % (2831719)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.41/1.41 % (2831719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.41/1.41 % (2831719)CaDiCaL version: 2.1.3
% 7.41/1.41 % (2831719)Termination reason: Refutation not found, incomplete strategy
% 7.41/1.41 % (2831719)Time elapsed: 0.007 s
% 7.41/1.41 % (2831719)Peak memory usage: 12 MB
% 7.41/1.41 % (2831719)Instructions burned: 11 (million)
% 7.41/1.41 % (2831719)------------------------------
% 7.41/1.41 % (2831719)------------------------------
% 7.41/1.41 % (2831721)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=2986158055:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2991 on theBenchmark for (2991ds/31Mi)
% 7.41/1.41 % (2831707)Instruction limit reached!
% 7.41/1.41 % (2831707)------------------------------
% 7.41/1.41 % (2831707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.41/1.41 % (2831707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.41/1.41 % (2831707)CaDiCaL version: 2.1.3
% 7.41/1.41 % (2831707)Termination reason: Instruction limit
% 7.41/1.41 % (2831707)Termination phase: Saturation
% 7.41/1.41 % (2831707)Time elapsed: 0.166 s
% 7.41/1.41 % (2831707)Peak memory usage: 14 MB
% 7.41/1.41 % (2831707)Instructions burned: 373 (million)
% 7.41/1.41 % (2831721)Instruction limit reached!
% 7.41/1.41 % (2831721)------------------------------
% 7.41/1.41 % (2831721)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.41/1.41 % (2831721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.41/1.41 % (2831721)CaDiCaL version: 2.1.3
% 7.41/1.41 % (2831721)Termination reason: Instruction limit
% 7.41/1.41 % (2831721)Termination phase: Saturation
% 7.41/1.41 % (2831721)Time elapsed: 0.016 s
% 7.41/1.41 % (2831721)Peak memory usage: 12 MB
% 7.41/1.41 % (2831721)Instructions burned: 32 (million)
% 7.41/1.41 % (2831714)Refutation not found, incomplete strategy
% 7.41/1.41 % (2831714)------------------------------
% 7.41/1.41 % (2831714)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.41/1.41 % (2831714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.41/1.41 % (2831714)CaDiCaL version: 2.1.3
% 7.41/1.41 % (2831714)Termination reason: Refutation not found, incomplete strategy
% 7.41/1.41 % (2831714)Time elapsed: 0.084 s
% 7.41/1.41 % (2831714)Peak memory usage: 12 MB
% 7.41/1.41 % (2831714)Instructions burned: 174 (million)
% 7.41/1.41 % (2831714)------------------------------
% 7.41/1.41 % (2831714)------------------------------
% 7.41/1.41 % (2831723)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 7.41/1.41 % (2831723)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
% 7.41/1.41 % (2831723)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=3746624834:hsqr=1,8:i=1440:s2at=5:add=on:nm=2:rtra=on_2991 on theBenchmark for (2991ds/1440Mi)
% 7.41/1.41 % (2831724)dis+10_2_sil=128000:si=on:random_seed=1985049580:s2a=on:i=339:av=off:rtra=on:fe=abstraction:ss=axioms:fsd=on:ntd=on_2990 on theBenchmark for (2990ds/339Mi)
% 7.41/1.41 % (2831723)Refutation not found, incomplete strategy
% 7.41/1.41 % (2831723)------------------------------
% 7.41/1.41 % (2831723)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.41/1.41 % (2831723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.41/1.41 % (2831723)CaDiCaL version: 2.1.3
% 7.41/1.41 % (2831723)Termination reason: Refutation not found, incomplete strategy
% 7.41/1.41 % (2831723)Time elapsed: 0.011 s
% 7.41/1.41 % (2831723)Peak memory usage: 12 MB
% 7.41/1.41 % (2831723)Instructions burned: 20 (million)
% 7.41/1.41 % (2831723)------------------------------
% 7.98/1.51 % (2831723)------------------------------
% 7.98/1.51 % (2831711)Instruction limit reached!
% 7.98/1.51 % (2831711)------------------------------
% 7.98/1.51 % (2831711)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.98/1.51 % (2831711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.98/1.51 % (2831711)CaDiCaL version: 2.1.3
% 7.98/1.51 % (2831711)Termination reason: Instruction limit
% 7.98/1.51 % (2831711)Termination phase: Saturation
% 7.98/1.51 % (2831711)Time elapsed: 0.150 s
% 7.98/1.51 % (2831711)Peak memory usage: 14 MB
% 7.98/1.51 % (2831711)Instructions burned: 580 (million)
% 7.98/1.51 % (2831725)lrs+2_16:1_si=on:cbe=off:uwa=interpreted_only:random_seed=784601023:i=111:add=on:fgj=on:rtra=on:fdi=1024_2990 on theBenchmark for (2990ds/111Mi)
% 7.98/1.51 % (2831729)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=131018251:st=3:avsq=on:i=122:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2990 on theBenchmark for (2990ds/122Mi)
% 7.98/1.51 % (2831725)Refutation not found, incomplete strategy
% 7.98/1.51 % (2831725)------------------------------
% 7.98/1.51 % (2831725)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.98/1.51 % (2831725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.98/1.51 % (2831725)CaDiCaL version: 2.1.3
% 7.98/1.51 % (2831725)Termination reason: Refutation not found, incomplete strategy
% 7.98/1.51 % (2831725)Time elapsed: 0.010 s
% 7.98/1.51 % (2831725)Peak memory usage: 12 MB
% 7.98/1.51 % (2831725)Instructions burned: 18 (million)
% 7.98/1.51 % (2831725)------------------------------
% 7.98/1.51 % (2831725)------------------------------
% 7.98/1.51 % (2831713)Instruction limit reached!
% 7.98/1.51 % (2831713)------------------------------
% 7.98/1.51 % (2831713)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.98/1.51 % (2831713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.98/1.51 % (2831713)CaDiCaL version: 2.1.3
% 7.98/1.51 % (2831713)Termination reason: Instruction limit
% 7.98/1.51 % (2831713)Termination phase: Saturation
% 7.98/1.51 % (2831713)Time elapsed: 0.131 s
% 7.98/1.51 % (2831713)Peak memory usage: 13 MB
% 7.98/1.51 % (2831713)Instructions burned: 271 (million)
% 7.98/1.51 % (2831730)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=2468908314:uwa_fpi=on:avsq=on:i=136:avsqr=1,32:hud=15:nm=0:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/136Mi)
% 7.98/1.51 % (2831732)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=3283663381:hsq=on:st=2:i=232:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2990 on theBenchmark for (2990ds/232Mi)
% 7.98/1.51 % (2831732)Refutation not found, incomplete strategy
% 7.98/1.51 % (2831732)------------------------------
% 7.98/1.51 % (2831732)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.98/1.51 % (2831732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.98/1.51 % (2831732)CaDiCaL version: 2.1.3
% 7.98/1.51 % (2831732)Termination reason: Refutation not found, incomplete strategy
% 7.98/1.51 % (2831732)Time elapsed: 0.003 s
% 7.98/1.51 % (2831732)Peak memory usage: 12 MB
% 7.98/1.51 % (2831732)Instructions burned: 5 (million)
% 7.98/1.51 % (2831732)------------------------------
% 7.98/1.51 % (2831732)------------------------------
% 7.98/1.51 % (2831734)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=2556640882:i=1254:kws=precedence:bd=preordered:av=off:rtra=on_2990 on theBenchmark for (2990ds/1254Mi)
% 7.98/1.51 % (2831729)Instruction limit reached!
% 7.98/1.51 % (2831729)------------------------------
% 7.98/1.51 % (2831729)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.98/1.51 % (2831729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.98/1.51 % (2831729)CaDiCaL version: 2.1.3
% 7.98/1.51 % (2831729)Termination reason: Instruction limit
% 7.98/1.51 % (2831729)Termination phase: Saturation
% 7.98/1.51 % (2831729)Time elapsed: 0.032 s
% 7.98/1.51 % (2831729)Peak memory usage: 12 MB
% 7.98/1.51 % (2831729)Instructions burned: 124 (million)
% 7.98/1.51 % (2831736)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 7.98/1.51 % (2831738)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=622533700:i=619:add=on:rtra=on_2990 on theBenchmark for (2990ds/619Mi)
% 8.62/1.61 % (2831736)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=3976876464:s2a=on:i=281:add=on:rtra=on:fe=axiom:fdi=1024_2990 on theBenchmark for (2990ds/281Mi)
% 8.62/1.61 % (2831730)Instruction limit reached!
% 8.62/1.61 % (2831730)------------------------------
% 8.62/1.61 % (2831730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.62/1.61 % (2831730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.62/1.61 % (2831730)CaDiCaL version: 2.1.3
% 8.62/1.61 % (2831730)Termination reason: Instruction limit
% 8.62/1.61 % (2831730)Termination phase: Saturation
% 8.62/1.61 % (2831730)Time elapsed: 0.064 s
% 8.62/1.61 % (2831730)Peak memory usage: 14 MB
% 8.62/1.61 % (2831730)Instructions burned: 137 (million)
% 8.62/1.61 % (2831738)Refutation not found, incomplete strategy
% 8.62/1.61 % (2831738)------------------------------
% 8.62/1.61 % (2831738)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.62/1.61 % (2831738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.62/1.61 % (2831738)CaDiCaL version: 2.1.3
% 8.62/1.61 % (2831738)Termination reason: Refutation not found, incomplete strategy
% 8.62/1.61 % (2831738)Time elapsed: 0.040 s
% 8.62/1.61 % (2831738)Peak memory usage: 13 MB
% 8.62/1.61 % (2831738)Instructions burned: 165 (million)
% 8.62/1.61 % (2831738)------------------------------
% 8.62/1.61 % (2831738)------------------------------
% 8.62/1.61 % (2831741)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=526817255:i=865:bs=unit_only:ins=25:rtra=on:ntd=on_2989 on theBenchmark for (2989ds/865Mi)
% 8.62/1.61 % (2831742)lrs+10_1_sil=128000:si=on:urr=on:random_seed=805881938:i=212:sd=1:rtra=on:ss=axioms:sgt=64_2989 on theBenchmark for (2989ds/212Mi)
% 8.62/1.61 % (2831724)Instruction limit reached!
% 8.62/1.61 % (2831724)------------------------------
% 8.62/1.61 % (2831724)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.62/1.61 % (2831724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.62/1.61 % (2831724)CaDiCaL version: 2.1.3
% 8.62/1.61 % (2831724)Termination reason: Instruction limit
% 8.62/1.61 % (2831724)Termination phase: Saturation
% 8.62/1.61 % (2831724)Time elapsed: 0.157 s
% 8.62/1.61 % (2831724)Peak memory usage: 12 MB
% 8.62/1.61 % (2831724)Instructions burned: 340 (million)
% 8.62/1.61 % (2831716)Instruction limit reached!
% 8.62/1.61 % (2831716)------------------------------
% 8.62/1.61 % (2831716)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.62/1.61 % (2831716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.62/1.61 % (2831716)CaDiCaL version: 2.1.3
% 8.62/1.61 % (2831716)Termination reason: Instruction limit
% 8.62/1.61 % (2831716)Termination phase: Saturation
% 8.62/1.61 % (2831716)Time elapsed: 0.256 s
% 8.62/1.61 % (2831716)Peak memory usage: 13 MB
% 8.62/1.61 % (2831716)Instructions burned: 421 (million)
% 8.62/1.61 % (2831745)lrs+1010_64_sil=128000:si=on:avsql=on:uwa=off:random_seed=2919333356:hsq=on:st=3:avsq=on:i=130:avsqr=1,16:sd=1:rtra=on:ss=axioms_2989 on theBenchmark for (2989ds/130Mi)
% 8.62/1.61 % (2831746)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=1110363992:st=1.5:i=346:rtra=on:ss=axioms_2989 on theBenchmark for (2989ds/346Mi)
% 8.62/1.61 % (2831736)Instruction limit reached!
% 8.62/1.61 % (2831736)------------------------------
% 8.62/1.61 % (2831736)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.62/1.61 % (2831736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.62/1.61 % (2831736)CaDiCaL version: 2.1.3
% 8.62/1.61 % (2831736)Termination reason: Instruction limit
% 8.62/1.61 % (2831736)Termination phase: Saturation
% 8.62/1.61 % (2831736)Time elapsed: 0.148 s
% 8.62/1.61 % (2831736)Peak memory usage: 13 MB
% 8.62/1.61 % (2831736)Instructions burned: 283 (million)
% 8.62/1.61 % (2831749)lrs+1010_3_sil=128000:si=on:slsq=on:random_seed=127120913:avsq=on:i=152:avsqr=8,1:hud=5:ins=1:fsr=off:rtra=on_2988 on theBenchmark for (2988ds/152Mi)
% 8.62/1.61 % (2831742)Instruction limit reached!
% 8.62/1.61 % (2831742)------------------------------
% 8.62/1.61 % (2831742)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.62/1.61 % (2831742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.18/1.77 % (2831742)CaDiCaL version: 2.1.3
% 9.18/1.77 % (2831742)Termination reason: Instruction limit
% 9.18/1.77 % (2831742)Termination phase: Saturation
% 9.18/1.77 % (2831742)Time elapsed: 0.106 s
% 9.18/1.77 % (2831742)Peak memory usage: 13 MB
% 9.18/1.77 % (2831742)Instructions burned: 213 (million)
% 9.18/1.77 % (2831751)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3834031125:i=75:ep=R:rtra=on:ntd=on_2988 on theBenchmark for (2988ds/75Mi)
% 9.18/1.77 % (2831745)Instruction limit reached!
% 9.18/1.77 % (2831745)------------------------------
% 9.18/1.77 % (2831745)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.18/1.77 % (2831745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.18/1.77 % (2831745)CaDiCaL version: 2.1.3
% 9.18/1.77 % (2831745)Termination reason: Instruction limit
% 9.18/1.77 % (2831745)Termination phase: Saturation
% 9.18/1.77 % (2831745)Time elapsed: 0.069 s
% 9.18/1.77 % (2831745)Peak memory usage: 12 MB
% 9.18/1.77 % (2831745)Instructions burned: 130 (million)
% 9.18/1.77 % (2831746)Refutation not found, incomplete strategy
% 9.18/1.77 % (2831746)------------------------------
% 9.18/1.77 % (2831746)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.18/1.77 % (2831746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.18/1.77 % (2831746)CaDiCaL version: 2.1.3
% 9.18/1.77 % (2831746)Termination reason: Refutation not found, incomplete strategy
% 9.18/1.77 % (2831746)Time elapsed: 0.060 s
% 9.18/1.77 % (2831746)Peak memory usage: 12 MB
% 9.18/1.77 % (2831746)Instructions burned: 89 (million)
% 9.18/1.77 % (2831746)------------------------------
% 9.18/1.77 % (2831746)------------------------------
% 9.18/1.77 % (2831753)dis+10_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=one_side_interpreted:nwc=5:random_seed=4213253732:st=2.5:i=387:sd=2:rtra=on:ss=axioms_2988 on theBenchmark for (2988ds/387Mi)
% 9.18/1.77 % (2831754)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=57831389:uwa_fpi=on:i=148:doe=on:bd=preordered:rtra=on:fsd=on_2988 on theBenchmark for (2988ds/148Mi)
% 9.18/1.77 % (2831751)Instruction limit reached!
% 9.18/1.77 % (2831751)------------------------------
% 9.18/1.77 % (2831751)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.18/1.77 % (2831751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.18/1.77 % (2831751)CaDiCaL version: 2.1.3
% 9.18/1.77 % (2831751)Termination reason: Instruction limit
% 9.18/1.77 % (2831751)Termination phase: Saturation
% 9.18/1.77 % (2831751)Time elapsed: 0.037 s
% 9.18/1.77 % (2831751)Peak memory usage: 12 MB
% 9.18/1.77 % (2831751)Instructions burned: 77 (million)
% 9.18/1.77 % (2831749)Instruction limit reached!
% 9.18/1.77 % (2831749)------------------------------
% 9.18/1.77 % (2831749)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.18/1.77 % (2831749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.18/1.77 % (2831749)CaDiCaL version: 2.1.3
% 9.18/1.77 % (2831749)Termination reason: Instruction limit
% 9.18/1.77 % (2831749)Termination phase: Saturation
% 9.18/1.77 % (2831749)Time elapsed: 0.075 s
% 9.18/1.77 % (2831749)Peak memory usage: 13 MB
% 9.18/1.77 % (2831749)Instructions burned: 152 (million)
% 9.18/1.77 % (2831757)dis+1010_3_si=on:uwa=one_side_interpreted:random_seed=1983273579:i=161:piset=and:rtra=on:ntd=on_2987 on theBenchmark for (2987ds/161Mi)
% 9.18/1.77 % (2831758)lrs+10_1_sil=128000:si=on:random_seed=1943675455:st=5:i=888:sd=3:bd=preordered:rtra=on:ss=axioms_2987 on theBenchmark for (2987ds/888Mi)
% 9.18/1.77 % (2831741)Instruction limit reached!
% 9.18/1.77 % (2831741)------------------------------
% 9.18/1.77 % (2831741)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.18/1.77 % (2831741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.18/1.77 % (2831741)CaDiCaL version: 2.1.3
% 9.18/1.77 % (2831741)Termination reason: Instruction limit
% 9.18/1.77 % (2831741)Termination phase: Saturation
% 9.18/1.77 % (2831741)Time elapsed: 0.215 s
% 9.18/1.77 % (2831741)Peak memory usage: 15 MB
% 9.18/1.77 % (2831741)Instructions burned: 868 (million)
% 9.18/1.77 % (2831761)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=1600723695:i=136:add=on:ins=4:rtra=on:sup=off_2987 on theBenchmark for (2987ds/136Mi)
% 10.01/1.86 % (2831761)Refutation not found, incomplete strategy
% 10.01/1.86 % (2831761)------------------------------
% 10.01/1.86 % (2831761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.01/1.86 % (2831761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.01/1.86 % (2831761)CaDiCaL version: 2.1.3
% 10.01/1.86 % (2831761)Termination reason: Refutation not found, incomplete strategy
% 10.01/1.86 % (2831761)Time elapsed: 0.001 s
% 10.01/1.86 % (2831761)Peak memory usage: 12 MB
% 10.01/1.86 % (2831761)Instructions burned: 2 (million)
% 10.01/1.86 % (2831761)------------------------------
% 10.01/1.86 % (2831761)------------------------------
% 10.01/1.86 % (2831763)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=3713902352:i=88:s2at=3:nm=2:rtra=on:rawr=on_2987 on theBenchmark for (2987ds/88Mi)
% 10.01/1.86 % (2831763)Instruction limit reached!
% 10.01/1.86 % (2831763)------------------------------
% 10.01/1.86 % (2831763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.01/1.86 % (2831763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.01/1.86 % (2831763)CaDiCaL version: 2.1.3
% 10.01/1.86 % (2831763)Termination reason: Instruction limit
% 10.01/1.86 % (2831763)Termination phase: Saturation
% 10.01/1.86 % (2831763)Time elapsed: 0.026 s
% 10.01/1.86 % (2831763)Peak memory usage: 13 MB
% 10.01/1.86 % (2831763)Instructions burned: 89 (million)
% 10.01/1.86 % (2831754)Instruction limit reached!
% 10.01/1.86 % (2831754)------------------------------
% 10.01/1.86 % (2831754)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.01/1.86 % (2831754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.01/1.86 % (2831754)CaDiCaL version: 2.1.3
% 10.01/1.86 % (2831754)Termination reason: Instruction limit
% 10.01/1.86 % (2831754)Termination phase: Saturation
% 10.01/1.86 % (2831754)Time elapsed: 0.094 s
% 10.01/1.86 % (2831754)Peak memory usage: 12 MB
% 10.01/1.86 % (2831754)Instructions burned: 149 (million)
% 10.01/1.86 % (2831757)Instruction limit reached!
% 10.01/1.86 % (2831757)------------------------------
% 10.01/1.86 % (2831757)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.01/1.86 % (2831757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.01/1.86 % (2831757)CaDiCaL version: 2.1.3
% 10.01/1.86 % (2831757)Termination reason: Instruction limit
% 10.01/1.86 % (2831757)Termination phase: Saturation
% 10.01/1.86 % (2831757)Time elapsed: 0.078 s
% 10.01/1.86 % (2831757)Peak memory usage: 13 MB
% 10.01/1.86 % (2831757)Instructions burned: 162 (million)
% 10.01/1.86 % (2831765)dis+1002_5:4_to=kbo:sil=128000:cnfonf=conj_eager:si=on:sp=reverse_arity:lma=off:hi=on:nwc=20:random_seed=3547367009:s2a=on:cond=on:i=93:add=on:bd=preordered:rtra=on:er=filter_2987 on theBenchmark for (2987ds/93Mi)
% 10.01/1.86 % (2831769)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=2381202513:s2a=on:i=240:rtra=on:ntd=on_2986 on theBenchmark for (2986ds/240Mi)
% 10.01/1.86 % (2831766)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=2813233859:i=2186:rtra=on:ixr=off_2986 on theBenchmark for (2986ds/2186Mi)
% 10.01/1.86 % (2831765)Instruction limit reached!
% 10.01/1.86 % (2831765)------------------------------
% 10.01/1.86 % (2831765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.01/1.86 % (2831765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.01/1.86 % (2831765)CaDiCaL version: 2.1.3
% 10.01/1.86 % (2831765)Termination reason: Instruction limit
% 10.01/1.86 % (2831765)Termination phase: Saturation
% 10.01/1.86 % (2831765)Time elapsed: 0.029 s
% 10.01/1.86 % (2831765)Peak memory usage: 12 MB
% 10.01/1.86 % (2831765)Instructions burned: 94 (million)
% 10.01/1.86 % (2831772)dis+10_1_to=lpo:sil=128000:tgt=ground:si=on:urr=on:cbe=off:uwa=one_side_constant:nwc=5:random_seed=254060407:i=805:aac=none:doe=on:piset=not:bd=all:rtra=on:fe=abstraction_2986 on theBenchmark for (2986ds/805Mi)
% 10.01/1.86 % (2831772)Refutation not found, incomplete strategy
% 10.01/1.86 % (2831772)------------------------------
% 10.01/1.86 % (2831772)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.01/1.86 % (2831772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.01/1.86 % (2831772)CaDiCaL version: 2.1.3
% 10.01/1.86 % (2831772)Termination reason: Refutation not found, incomplete strategy
% 10.65/1.95 % (2831772)Time elapsed: 0.002 s
% 10.65/1.95 % (2831772)Peak memory usage: 12 MB
% 10.65/1.95 % (2831772)Instructions burned: 6 (million)
% 10.65/1.95 % (2831772)------------------------------
% 10.65/1.95 % (2831772)------------------------------
% 10.65/1.95 % (2831774)WARNING Broken Constraint: if avatar_split_queue_cutoffs(1) has been set then avatar_split_queue(off) is equal to on
% 10.65/1.95 % (2831766)Refutation not found, incomplete strategy
% 10.65/1.95 % (2831766)------------------------------
% 10.65/1.95 % (2831766)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.65/1.95 % (2831766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.65/1.95 % (2831766)CaDiCaL version: 2.1.3
% 10.65/1.95 % (2831766)Termination reason: Refutation not found, incomplete strategy
% 10.65/1.95 % (2831766)Time elapsed: 0.038 s
% 10.65/1.95 % (2831766)Peak memory usage: 12 MB
% 10.65/1.95 % (2831766)Instructions burned: 48 (million)
% 10.65/1.95 % (2831774)dis+1002_1_to=lpo:sil=128000:cnfonf=conj_eager:si=on:sp=unary_first:spb=intro:urr=on:cbe=off:uwa=one_side_interpreted:rp=on:avsqc=1:random_seed=2563968704:st=2:s2a=on:i=391:sd=4:bd=preordered:nm=16:rtra=on:ss=axioms:rawr=on_2986 on theBenchmark for (2986ds/391Mi)
% 10.65/1.95 % (2831766)------------------------------
% 10.65/1.95 % (2831766)------------------------------
% 10.65/1.95 % (2831753)Instruction limit reached!
% 10.65/1.95 % (2831753)------------------------------
% 10.65/1.95 % (2831753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.65/1.95 % (2831753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.65/1.95 % (2831753)CaDiCaL version: 2.1.3
% 10.65/1.95 % (2831753)Termination reason: Instruction limit
% 10.65/1.95 % (2831753)Termination phase: Saturation
% 10.65/1.95 % (2831753)Time elapsed: 0.180 s
% 10.65/1.95 % (2831753)Peak memory usage: 13 MB
% 10.65/1.95 % (2831753)Instructions burned: 389 (million)
% 10.65/1.95 % (2831777)lrs+1010_5:1_sil=128000:si=on:uwa=interpreted_only:sac=on:slsq=on:random_seed=1118358626:lrd=on:i=314:sd=1:rtra=on:ss=axioms_2986 on theBenchmark for (2986ds/314Mi)
% 10.65/1.95 % (2831776)dis+10_1_sil=128000:si=on:urr=on:uwa=off:random_seed=2107403810:i=355:av=off:fsr=off:rtra=on:ixr=off_2986 on theBenchmark for (2986ds/355Mi)
% 10.65/1.95 % (2831774)Refutation not found, incomplete strategy
% 10.65/1.95 % (2831774)------------------------------
% 10.65/1.95 % (2831774)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.65/1.95 % (2831774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.65/1.95 % (2831774)CaDiCaL version: 2.1.3
% 10.65/1.95 % (2831774)Termination reason: Refutation not found, incomplete strategy
% 10.65/1.95 % (2831774)Time elapsed: 0.030 s
% 10.65/1.95 % (2831774)Peak memory usage: 12 MB
% 10.65/1.95 % (2831774)Instructions burned: 112 (million)
% 10.65/1.95 % (2831774)------------------------------
% 10.65/1.95 % (2831774)------------------------------
% 10.65/1.95 % (2831769)Instruction limit reached!
% 10.65/1.95 % (2831769)------------------------------
% 10.65/1.95 % (2831769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.65/1.95 % (2831769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.65/1.95 % (2831769)CaDiCaL version: 2.1.3
% 10.65/1.95 % (2831769)Termination reason: Instruction limit
% 10.65/1.95 % (2831769)Termination phase: Saturation
% 10.65/1.95 % (2831769)Time elapsed: 0.107 s
% 10.65/1.95 % (2831769)Peak memory usage: 13 MB
% 10.65/1.95 % (2831769)Instructions burned: 240 (million)
% 10.65/1.95 % (2831780)lrs+10_1_sil=128000:e2e=on:si=on:cbe=off:uwa=interpreted_only:cs=on:random_seed=4259233342:s2a=on:i=251:fsr=off:rtra=on_2985 on theBenchmark for (2985ds/251Mi)
% 10.65/1.95 % (2831781)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=4198154788:uwa_fpi=on:avsq=on:s2a=on:cond=fast:i=2470:s2at=1.5:aac=none:fgj=on:piset=and:hud=3:fsr=off:rtra=on:er=filter:rawr=on_2985 on theBenchmark for (2985ds/2470Mi)
% 10.65/1.95 % (2831777)Instruction limit reached!
% 10.65/1.95 % (2831777)------------------------------
% 10.65/1.95 % (2831777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.65/1.95 % (2831777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.65/1.95 % (2831777)CaDiCaL version: 2.1.3
% 10.65/1.95 % (2831777)Termination reason: Instruction limit
% 10.65/1.95 % (2831777)Termination phase: Saturation
% 10.65/1.95 % (2831777)Time elapsed: 0.122 s
% 12.79/2.15 % (2831777)Peak memory usage: 13 MB
% 12.79/2.15 % (2831777)Instructions burned: 319 (million)
% 12.79/2.15 % (2831734)Instruction limit reached!
% 12.79/2.15 % (2831734)------------------------------
% 12.79/2.15 % (2831734)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.79/2.15 % (2831734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.79/2.15 % (2831734)CaDiCaL version: 2.1.3
% 12.79/2.15 % (2831734)Termination reason: Instruction limit
% 12.79/2.15 % (2831734)Termination phase: Saturation
% 12.79/2.15 % (2831734)Time elapsed: 0.565 s
% 12.79/2.15 % (2831734)Peak memory usage: 14 MB
% 12.79/2.15 % (2831734)Instructions burned: 1255 (million)
% 12.79/2.15 % (2831784)dis+10_6_sil=128000:si=on:sp=arity:bce=on:cbe=off:uwa=interpreted_only:slsqc=4:slsq=on:random_seed=921184111:i=673:doe=on:fgj=on:piset=and:slsql=off:rtra=on:fdi=1024:ntd=on_2984 on theBenchmark for (2984ds/673Mi)
% 12.79/2.15 % (2831784)Refutation not found, incomplete strategy
% 12.79/2.15 % (2831784)------------------------------
% 12.79/2.15 % (2831784)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.79/2.15 % (2831784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.79/2.15 % (2831784)CaDiCaL version: 2.1.3
% 12.79/2.15 % (2831784)Termination reason: Refutation not found, incomplete strategy
% 12.79/2.15 % (2831784)Time elapsed: 0.005 s
% 12.79/2.15 % (2831784)Peak memory usage: 12 MB
% 12.79/2.15 % (2831784)Instructions burned: 3 (million)
% 12.79/2.15 % (2831784)------------------------------
% 12.79/2.15 % (2831784)------------------------------
% 12.79/2.15 % (2831785)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=2433269555:i=116:ep=RSTC:rtra=on:ntd=on_2984 on theBenchmark for (2984ds/116Mi)
% 12.79/2.15 % (2831785)Refutation not found, incomplete strategy
% 12.79/2.15 % (2831785)------------------------------
% 12.79/2.15 % (2831785)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.79/2.15 % (2831785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.79/2.15 % (2831785)CaDiCaL version: 2.1.3
% 12.79/2.15 % (2831785)Termination reason: Refutation not found, incomplete strategy
% 12.79/2.15 % (2831785)Time elapsed: 0.006 s
% 12.79/2.15 % (2831785)Peak memory usage: 12 MB
% 12.79/2.15 % (2831785)Instructions burned: 2 (million)
% 12.79/2.15 % (2831785)------------------------------
% 12.79/2.15 % (2831785)------------------------------
% 12.79/2.15 % (2831780)Instruction limit reached!
% 12.79/2.15 % (2831780)------------------------------
% 12.79/2.15 % (2831780)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.79/2.15 % (2831780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.79/2.15 % (2831780)CaDiCaL version: 2.1.3
% 12.79/2.15 % (2831780)Termination reason: Instruction limit
% 12.79/2.15 % (2831780)Termination phase: Saturation
% 12.79/2.15 % (2831780)Time elapsed: 0.131 s
% 12.79/2.15 % (2831780)Peak memory usage: 12 MB
% 12.79/2.15 % (2831780)Instructions burned: 255 (million)
% 12.79/2.15 % (2831790)WARNING Broken Constraint: if sine_tolerance(12) has been set then sine_selection(off) is not equal to off
% 12.79/2.15 % (2831787)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=2026779321:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2984 on theBenchmark for (2984ds/270Mi)
% 12.79/2.15 % (2831790)dis+1010_128_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=hol:nwc=2:flr=on:random_seed=3987870615:st=12:uwa_fpi=on:i=39:nm=40:ins=7:rtra=on_2984 on theBenchmark for (2984ds/39Mi)
% 12.79/2.15 % (2831790)Instruction limit reached!
% 12.79/2.15 % (2831790)------------------------------
% 12.79/2.15 % (2831790)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.79/2.15 % (2831790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.79/2.15 % (2831790)CaDiCaL version: 2.1.3
% 12.79/2.15 % (2831790)Termination reason: Instruction limit
% 12.79/2.15 % (2831790)Termination phase: Saturation
% 12.79/2.15 % (2831790)Time elapsed: 0.011 s
% 12.79/2.15 % (2831790)Peak memory usage: 12 MB
% 12.79/2.15 % (2831790)Instructions burned: 41 (million)
% 12.79/2.15 % (2831793)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=1777264156:i=365:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2984 on theBenchmark for (2984ds/365Mi)
% 12.79/2.15 % (2831789)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=101974252:hsq=on:hsqr=16,1:s2a=on:i=30:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2984 on theBenchmark for (2984ds/30Mi)
% 13.07/2.21 % (2831776)Instruction limit reached!
% 13.07/2.21 % (2831776)------------------------------
% 13.07/2.21 % (2831776)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.07/2.21 % (2831776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.07/2.21 % (2831776)CaDiCaL version: 2.1.3
% 13.07/2.21 % (2831776)Termination reason: Instruction limit
% 13.07/2.21 % (2831776)Termination phase: Saturation
% 13.07/2.21 % (2831776)Time elapsed: 0.232 s
% 13.07/2.21 % (2831776)Peak memory usage: 12 MB
% 13.07/2.21 % (2831776)Instructions burned: 356 (million)
% 13.07/2.21 % (2831789)Instruction limit reached!
% 13.07/2.21 % (2831789)------------------------------
% 13.07/2.21 % (2831789)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.07/2.21 % (2831789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.07/2.21 % (2831789)CaDiCaL version: 2.1.3
% 13.07/2.21 % (2831789)Termination reason: Instruction limit
% 13.07/2.21 % (2831789)Termination phase: Saturation
% 13.07/2.21 % (2831789)Time elapsed: 0.029 s
% 13.07/2.21 % (2831789)Peak memory usage: 12 MB
% 13.07/2.21 % (2831789)Instructions burned: 31 (million)
% 13.07/2.21 % (2831796)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=3948077398:i=158:av=off:rtra=on_2983 on theBenchmark for (2983ds/158Mi)
% 13.07/2.21 % (2831797)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
% 13.07/2.21 % (2831796)Refutation not found, incomplete strategy
% 13.07/2.21 % (2831796)------------------------------
% 13.07/2.21 % (2831796)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.07/2.21 % (2831796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.07/2.21 % (2831796)CaDiCaL version: 2.1.3
% 13.07/2.21 % (2831796)Termination reason: Refutation not found, incomplete strategy
% 13.07/2.21 % (2831796)Time elapsed: 0.006 s
% 13.07/2.21 % (2831796)Peak memory usage: 12 MB
% 13.07/2.21 % (2831796)Instructions burned: 10 (million)
% 13.07/2.21 % (2831796)------------------------------
% 13.07/2.21 % (2831796)------------------------------
% 13.07/2.21 % (2831797)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=2895978969:avsq=on:i=252:s2at=3:avsqr=1,16:rtra=on:ntd=on_2983 on theBenchmark for (2983ds/252Mi)
% 13.07/2.21 % (2831797)Refutation not found, incomplete strategy
% 13.07/2.21 % (2831797)------------------------------
% 13.07/2.21 % (2831797)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.07/2.21 % (2831797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.07/2.21 % (2831797)CaDiCaL version: 2.1.3
% 13.07/2.21 % (2831797)Termination reason: Refutation not found, incomplete strategy
% 13.07/2.21 % (2831797)Time elapsed: 0.008 s
% 13.07/2.21 % (2831797)Peak memory usage: 12 MB
% 13.07/2.21 % (2831797)Instructions burned: 11 (million)
% 13.07/2.21 % (2831797)------------------------------
% 13.07/2.21 % (2831797)------------------------------
% 13.07/2.21 % (2831758)Instruction limit reached!
% 13.07/2.21 % (2831758)------------------------------
% 13.07/2.21 % (2831758)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.07/2.21 % (2831800)lrs+10_1_cnfonf=off:si=on:sos=on:uwa=off:random_seed=1988805998:i=213:rtra=on:ss=axioms_2983 on theBenchmark for (2983ds/213Mi)
% 13.07/2.21 % (2831758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.07/2.21 % (2831758)CaDiCaL version: 2.1.3
% 13.07/2.21 % (2831758)Termination reason: Instruction limit
% 13.07/2.21 % (2831758)Termination phase: Saturation
% 13.07/2.21 % (2831758)Time elapsed: 0.429 s
% 13.07/2.21 % (2831758)Peak memory usage: 15 MB
% 13.07/2.21 % (2831758)Instructions burned: 890 (million)
% 13.07/2.21 % (2831801)dis+1010_28_sil=128000:tgt=full:plsq=on:plsqc=1:cnfonf=off:si=on:plsqr=128,1:uwa=off:slsqc=2:sac=on:slsq=on:random_seed=783452637:st=3:i=160:s2at=3:bd=preordered:nm=16:rtra=on:ss=axioms:ntd=on_2983 on theBenchmark for (2983ds/160Mi)
% 13.07/2.21 % (2831803)lrs+1010_2:3_sil=128000:cnfonf=off:e2e=on:si=on:sp=unary_first:uwa=off:br=off:lftc=80:random_seed=4143637302:hsq=on:hsqr=16,1:i=763:kws=inv_frequency:piset=and:bd=all:rtra=on:ntd=on_2983 on theBenchmark for (2983ds/763Mi)
% 13.07/2.21 % (2831787)Instruction limit reached!
% 13.07/2.21 % (2831787)------------------------------
% 13.07/2.21 % (2831787)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.07/2.21 % (2831787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.07/2.21 % (2831787)CaDiCaL version: 2.1.3
% 13.07/2.21 % (2831787)Termination reason: Instruction limit
% 13.07/2.21 % (2831787)Termination phase: Saturation
% 13.07/2.21 % (2831787)Time elapsed: 0.132 s
% 13.07/2.21 % (2831787)Peak memory usage: 13 MB
% 13.07/2.21 % (2831787)Instructions burned: 271 (million)
% 13.07/2.21 % (2831801)Refutation not found, incomplete strategy
% 13.07/2.21 % (2831801)------------------------------
% 13.07/2.21 % (2831801)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.07/2.21 % (2831801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.07/2.21 % (2831801)CaDiCaL version: 2.1.3
% 13.07/2.21 % (2831801)Termination reason: Refutation not found, incomplete strategy
% 13.07/2.21 % (2831801)Time elapsed: 0.029 s
% 13.07/2.21 % (2831801)Peak memory usage: 12 MB
% 13.07/2.21 % (2831801)Instructions burned: 50 (million)
% 13.07/2.21 % (2831801)------------------------------
% 13.07/2.21 % (2831801)------------------------------
% 13.07/2.21 % (2831806)WARNING Broken Constraint: if ho_split_queue_layered_arrangement(off) has been set then ho_split_queue(off) is equal to on
% 13.07/2.21 % (2831806)ott+1010_40_sil=128000:tgt=full:plsq=on:plsqc=5:si=on:sos=all:lma=off:plsqr=32,1:uwa=interpreted_only:random_seed=245461306:i=237:hsql=off:fgj=on:piset=all_but_not_eq:bd=preordered:av=off:rtra=on:ss=axioms:sgt=4:rawr=on_2982 on theBenchmark for (2982ds/237Mi)
% 13.07/2.21 % (2831807)dis+1002_1_drc=ordering:cnfonf=lazy_not_gen_be_off:si=on:lma=off:cbe=off:uwa=off:random_seed=3094186435:s2a=on:i=386:rtra=on:ntd=on_2982 on theBenchmark for (2982ds/386Mi)
% 13.07/2.21 % (2831793)Instruction limit reached!
% 13.07/2.21 % (2831793)------------------------------
% 13.07/2.21 % (2831793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.07/2.21 % (2831793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.07/2.21 % (2831793)CaDiCaL version: 2.1.3
% 13.07/2.21 % (2831793)Termination reason: Instruction limit
% 13.07/2.21 % (2831793)Termination phase: Saturation
% 13.07/2.21 % (2831793)Time elapsed: 0.157 s
% 13.07/2.21 % (2831793)Peak memory usage: 14 MB
% 13.07/2.21 % (2831793)Instructions burned: 365 (million)
% 13.07/2.21 % (2831800)Instruction limit reached!
% 13.07/2.21 % (2831800)------------------------------
% 13.07/2.21 % (2831800)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.07/2.21 % (2831800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.07/2.21 % (2831800)CaDiCaL version: 2.1.3
% 13.07/2.21 % (2831800)Termination reason: Instruction limit
% 13.07/2.21 % (2831800)Termination phase: Saturation
% 13.07/2.21 % (2831800)Time elapsed: 0.120 s
% 13.07/2.21 % (2831800)Peak memory usage: 13 MB
% 13.07/2.21 % (2831800)Instructions burned: 213 (million)
% 13.07/2.21 % (2831810)dis+10_128_to=lpo:sil=128000:si=on:spb=intro:uwa=off:random_seed=3039634052:i=300:piset=and:nm=32:rtra=on_2982 on theBenchmark for (2982ds/300Mi)
% 13.07/2.21 % (2831811)dis+1010_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:urr=on:random_seed=569512700:st=5:s2a=on:i=567:sd=2:rtra=on:ss=axioms_2982 on theBenchmark for (2982ds/567Mi)
% 13.07/2.21 % (2831807)Refutation not found, incomplete strategy
% 13.07/2.21 % (2831807)------------------------------
% 13.07/2.21 % (2831807)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.07/2.21 % (2831807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.07/2.21 % (2831807)CaDiCaL version: 2.1.3
% 13.07/2.21 % (2831807)Termination reason: Refutation not found, incomplete strategy
% 13.07/2.21 % (2831807)Time elapsed: 0.072 s
% 13.07/2.21 % (2831807)Peak memory usage: 12 MB
% 13.07/2.21 % (2831807)Instructions burned: 91 (million)
% 13.07/2.21 % (2831807)------------------------------
% 13.07/2.21 % (2831807)------------------------------
% 13.07/2.21 % (2831815)lrs+1010_1_si=on:uwa=one_side_interpreted:random_seed=1266248580:s2a=on:i=379:sd=1:rtra=on:ss=axioms:sgt=128_2981 on theBenchmark for (2981ds/379Mi)
% 13.07/2.21 % (2831806)Instruction limit reached!
% 13.07/2.21 % (2831806)------------------------------
% 13.07/2.21 % (2831806)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.07/2.21 % (2831806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.07/2.21 % (2831806)CaDiCaL version: 2.1.3
% 13.07/2.21 % (2831806)Termination reason: Instruction limit
% 13.07/2.21 % (2831806)Termination phase: Saturation
% 13.07/2.21 % (2831806)Time elapsed: 0.161 s
% 13.07/2.21 % (2831806)Peak memory usage: 12 MB
% 13.07/2.21 % (2831806)Instructions burned: 239 (million)
% 13.07/2.21 % (2831821)dis+32_3_cha=on:sil=128000:drc=off:si=on:cbe=off:uwa=interpreted_only:nwc=3:random_seed=187590196:s2a=on:i=429:s2at=5:add=on:sd=2:ep=R:bd=preordered:rtra=on:ss=included:sgt=40_2981 on theBenchmark for (2981ds/429Mi)
% 13.07/2.21 % (2831821)Refutation not found, incomplete strategy
% 13.07/2.21 % (2831821)------------------------------
% 13.07/2.21 % (2831821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.07/2.21 % (2831821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.07/2.21 % (2831821)CaDiCaL version: 2.1.3
% 13.07/2.21 % (2831821)Termination reason: Refutation not found, incomplete strategy
% 13.07/2.21 % (2831821)Time elapsed: 0.016 s
% 13.07/2.21 % (2831821)Peak memory usage: 12 MB
% 13.07/2.21 % (2831821)Instructions burned: 17 (million)
% 13.07/2.21 % (2831821)------------------------------
% 13.07/2.21 % (2831821)------------------------------
% 13.07/2.21 % (2831810) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2831544-2831810"...
% 13.07/2.21 % (2831810)...printing done.
% 13.07/2.21 % (2831810)Refutation found. Thanks to Tanya!
% 13.07/2.21 % SZS status Theorem for theBenchmark
% 13.07/2.21 % SZS output start Proof for theBenchmark
% 13.07/2.21 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 13.07/2.21 thf(func_def_0, type, cQ: ($i > $o)).
% 13.07/2.21 thf(func_def_1, type, cP: ($i > $o)).
% 13.07/2.21 thf(func_def_5, type, sK0: (($i > $o) > $i > $o)).
% 13.07/2.21 thf(func_def_6, type, sK1: (($i > $o) > $i)).
% 13.07/2.21 thf(func_def_7, type, sK2: (($i > $o) > $i)).
% 13.07/2.21 thf(func_def_8, type, sK3: (($i > $o) > $i)).
% 13.07/2.21 thf(func_def_9, type, vAND: ($o > $o > $o)).
% 13.07/2.21 thf(func_def_10, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 13.07/2.21 thf(func_def_11, type, db0: !>[X0: $tType]:(X0)).
% 13.07/2.21 thf(func_def_12, type, vNOT: ($o > $o)).
% 13.07/2.21 thf(func_def_13, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 13.07/2.21 thf(f1,conjecture,(
% 13.07/2.21 ? [X0 : ($i > $o)] : (! [X2 : ($i > $o)] : ((! [X1 : $i] : ((X2 @ X1) => (cP @ X1)) & ! [X1 : $i] : ((X2 @ X1) => (cQ @ X1))) => ! [X1 : $i] : ((X2 @ X1) => (X0 @ X1))) & ! [X1 : $i] : ((X0 @ X1) => (cP @ X1)) & ! [X1 : $i] : ((X0 @ X1) => (cQ @ X1)))),
% 13.07/2.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cTHM590_pme)).
% 13.07/2.21 thf(f2,negated_conjecture,(
% 13.07/2.21 ~ ? [X0 : ($i > $o)] : (! [X2 : ($i > $o)] : ((! [X1 : $i] : ((X2 @ X1) => (cP @ X1)) & ! [X1 : $i] : ((X2 @ X1) => (cQ @ X1))) => ! [X1 : $i] : ((X2 @ X1) => (X0 @ X1))) & ! [X1 : $i] : ((X0 @ X1) => (cP @ X1)) & ! [X1 : $i] : ((X0 @ X1) => (cQ @ X1)))),
% 13.07/2.21 inference(negated_conjecture,[status(cth)],[f1])).
% 13.07/2.21 thf(f3,plain,(
% 13.07/2.21 ~ ? [X0 : ($i > $o)] : (! [X1 : ($i > $o)] : ((! [X2 : $i] : ((X1 @ X2) => (cP @ X2)) & ! [X3 : $i] : ((X1 @ X3) => (cQ @ X3))) => ! [X4 : $i] : ((X1 @ X4) => (X0 @ X4))) & ! [X5 : $i] : ((X0 @ X5) => (cP @ X5)) & ! [X6 : $i] : ((X0 @ X6) => (cQ @ X6)))),
% 13.07/2.21 inference(rectify,[],[f2])).
% 13.07/2.21 thf(f4,plain,(
% 13.07/2.21 ~ ? [X0 : ($i > $o)] : (! [X1 : ($i > $o)] : ((! [X2 : $i] : ((((X1 @ X2)) = $true) => ($true = ((cP @ X2)))) & ! [X3 : $i] : ((((X1 @ X3)) = $true) => ($true = ((cQ @ X3))))) => ! [X4 : $i] : ((((X1 @ X4)) = $true) => ($true = ((X0 @ X4))))) & ! [X5 : $i] : ((((X0 @ X5)) = $true) => ($true = ((cP @ X5)))) & ! [X6 : $i] : (($true = ((X0 @ X6))) => (((cQ @ X6)) = $true)))),
% 13.07/2.21 inference(fool_elimination,[],[f3])).
% 13.07/2.21 thf(f5,plain,(
% 13.07/2.21 ! [X0 : ($i > $o)] : (? [X1 : ($i > $o)] : (? [X4 : $i] : ((((X1 @ X4)) = $true) & ($true != ((X0 @ X4)))) & (! [X2 : $i] : ((((X1 @ X2)) != $true) | ($true = ((cP @ X2)))) & ! [X3 : $i] : (($true = ((cQ @ X3))) | (((X1 @ X3)) != $true)))) | ? [X5 : $i] : ((((X0 @ X5)) = $true) & ($true != ((cP @ X5)))) | ? [X6 : $i] : ((((cQ @ X6)) != $true) & ($true = ((X0 @ X6)))))),
% 13.07/2.21 inference(ennf_transformation,[],[f4])).
% 13.07/2.21 thf(f6,plain,(
% 13.07/2.21 ! [X0 : ($i > $o)] : (? [X1 : ($i > $o)] : (! [X3 : $i] : (($true = ((cQ @ X3))) | (((X1 @ X3)) != $true)) & ! [X2 : $i] : ((((X1 @ X2)) != $true) | ($true = ((cP @ X2)))) & ? [X4 : $i] : ((((X1 @ X4)) = $true) & ($true != ((X0 @ X4))))) | ? [X5 : $i] : ((((X0 @ X5)) = $true) & ($true != ((cP @ X5)))) | ? [X6 : $i] : ((((cQ @ X6)) != $true) & ($true = ((X0 @ X6)))))),
% 13.07/2.21 inference(flattening,[],[f5])).
% 13.07/2.21 thf(f7,plain,(
% 13.07/2.21 ! [X0 : ($i > $o)] : (? [X1 : ($i > $o)] : (! [X2 : $i] : (($true = ((cQ @ X2))) | (((X1 @ X2)) != $true)) & ! [X3 : $i] : ((((X1 @ X3)) != $true) | (((cP @ X3)) = $true)) & ? [X4 : $i] : ((((X1 @ X4)) = $true) & ($true != ((X0 @ X4))))) | ? [X5 : $i] : ((((X0 @ X5)) = $true) & ($true != ((cP @ X5)))) | ? [X6 : $i] : ((((cQ @ X6)) != $true) & ($true = ((X0 @ X6)))))),
% 13.07/2.21 inference(rectify,[],[f6])).
% 13.07/2.21 thf(f8,plain,(
% 13.07/2.21 ! [X0 : ($i > $o)] : ((! [X2 : $i] : (($true = ((cQ @ X2))) | (((sK0 @ X0 @ X2)) != $true)) & ! [X3 : $i] : ((((sK0 @ X0 @ X3)) != $true) | (((cP @ X3)) = $true)) & ((((sK0 @ X0 @ (sK1 @ X0))) = $true) & (((X0 @ (sK1 @ X0))) != $true))) | ((((X0 @ (sK2 @ X0))) = $true) & (((cP @ (sK2 @ X0))) != $true)) | (($true != ((cQ @ (sK3 @ X0)))) & (((X0 @ (sK3 @ X0))) = $true)))),
% 13.07/2.21 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP,vAPP,vAPP,vAPP]),skolemize(X6,sK3 @ X0),skolemize(X6,sK3 @ X0),skolemize(X6,sK3 @ X0),skolemize(X6,sK3 @ X0)],[f7])).
% 13.07/2.21 thf(f9,plain,(
% 13.07/2.21 ( ! [X0 : ($i > $o)] : ((((cP @ (sK2 @ X0))) != $true) | (((X0 @ (sK3 @ X0))) = $true) | (((X0 @ (sK1 @ X0))) != $true)) )),
% 13.07/2.21 inference(cnf_transformation,[],[f8])).
% 13.07/2.21 thf(f10,plain,(
% 13.07/2.21 ( ! [X0 : ($i > $o)] : (($true != ((cQ @ (sK3 @ X0)))) | (((X0 @ (sK1 @ X0))) != $true) | (((cP @ (sK2 @ X0))) != $true)) )),
% 13.07/2.21 inference(cnf_transformation,[],[f8])).
% 13.07/2.21 thf(f11,plain,(
% 13.07/2.21 ( ! [X0 : ($i > $o)] : ((((X0 @ (sK1 @ X0))) != $true) | (((X0 @ (sK2 @ X0))) = $true) | (((X0 @ (sK3 @ X0))) = $true)) )),
% 13.07/2.21 inference(cnf_transformation,[],[f8])).
% 13.07/2.21 thf(f12,plain,(
% 13.07/2.21 ( ! [X0 : ($i > $o)] : (($true != ((cQ @ (sK3 @ X0)))) | (((X0 @ (sK2 @ X0))) = $true) | (((X0 @ (sK1 @ X0))) != $true)) )),
% 13.07/2.21 inference(cnf_transformation,[],[f8])).
% 13.07/2.21 thf(f13,plain,(
% 13.07/2.21 ( ! [X0 : ($i > $o)] : ((((cP @ (sK2 @ X0))) != $true) | (((sK0 @ X0 @ (sK1 @ X0))) = $true) | (((X0 @ (sK3 @ X0))) = $true)) )),
% 13.07/2.21 inference(cnf_transformation,[],[f8])).
% 13.07/2.21 thf(f14,plain,(
% 13.07/2.21 ( ! [X0 : ($i > $o)] : (($true != ((cQ @ (sK3 @ X0)))) | (((sK0 @ X0 @ (sK1 @ X0))) = $true) | (((cP @ (sK2 @ X0))) != $true)) )),
% 13.07/2.21 inference(cnf_transformation,[],[f8])).
% 13.07/2.21 thf(f15,plain,(
% 13.07/2.21 ( ! [X0 : ($i > $o)] : ((((sK0 @ X0 @ (sK1 @ X0))) = $true) | (((X0 @ (sK3 @ X0))) = $true) | (((X0 @ (sK2 @ X0))) = $true)) )),
% 13.07/2.21 inference(cnf_transformation,[],[f8])).
% 13.07/2.21 thf(f16,plain,(
% 13.07/2.21 ( ! [X0 : ($i > $o)] : (($true != ((cQ @ (sK3 @ X0)))) | (((X0 @ (sK2 @ X0))) = $true) | (((sK0 @ X0 @ (sK1 @ X0))) = $true)) )),
% 13.07/2.21 inference(cnf_transformation,[],[f8])).
% 13.07/2.21 thf(f17,plain,(
% 13.07/2.21 ( ! [X3 : $i,X0 : ($i > $o)] : ((((sK0 @ X0 @ X3)) != $true) | (((X0 @ (sK3 @ X0))) = $true) | (((cP @ X3)) = $true) | (((cP @ (sK2 @ X0))) != $true)) )),
% 13.07/2.21 inference(cnf_transformation,[],[f8])).
% 13.07/2.21 thf(f18,plain,(
% 13.07/2.21 ( ! [X3 : $i,X0 : ($i > $o)] : ((((sK0 @ X0 @ X3)) != $true) | (((cP @ X3)) = $true) | (((cP @ (sK2 @ X0))) != $true) | ($true != ((cQ @ (sK3 @ X0))))) )),
% 13.07/2.21 inference(cnf_transformation,[],[f8])).
% 13.07/2.21 thf(f19,plain,(
% 13.07/2.21 ( ! [X3 : $i,X0 : ($i > $o)] : ((((sK0 @ X0 @ X3)) != $true) | (((X0 @ (sK2 @ X0))) = $true) | (((cP @ X3)) = $true) | (((X0 @ (sK3 @ X0))) = $true)) )),
% 13.07/2.21 inference(cnf_transformation,[],[f8])).
% 13.07/2.21 thf(f20,plain,(
% 13.07/2.21 ( ! [X3 : $i,X0 : ($i > $o)] : ((((sK0 @ X0 @ X3)) != $true) | (((cP @ X3)) = $true) | (((X0 @ (sK2 @ X0))) = $true) | ($true != ((cQ @ (sK3 @ X0))))) )),
% 13.07/2.21 inference(cnf_transformation,[],[f8])).
% 13.07/2.21 thf(f21,plain,(
% 13.07/2.21 ( ! [X2 : $i,X0 : ($i > $o)] : ((((sK0 @ X0 @ X2)) != $true) | (((X0 @ (sK3 @ X0))) = $true) | ($true = ((cQ @ X2))) | (((cP @ (sK2 @ X0))) != $true)) )),
% 13.07/2.21 inference(cnf_transformation,[],[f8])).
% 13.07/2.21 thf(f22,plain,(
% 13.07/2.21 ( ! [X2 : $i,X0 : ($i > $o)] : ((((sK0 @ X0 @ X2)) != $true) | ($true != ((cQ @ (sK3 @ X0)))) | ($true = ((cQ @ X2))) | (((cP @ (sK2 @ X0))) != $true)) )),
% 13.07/2.21 inference(cnf_transformation,[],[f8])).
% 13.07/2.21 thf(f23,plain,(
% 13.07/2.21 ( ! [X2 : $i,X0 : ($i > $o)] : ((((sK0 @ X0 @ X2)) != $true) | (((X0 @ (sK3 @ X0))) = $true) | (((X0 @ (sK2 @ X0))) = $true) | ($true = ((cQ @ X2)))) )),
% 13.07/2.21 inference(cnf_transformation,[],[f8])).
% 13.07/2.21 thf(f24,plain,(
% 13.07/2.21 ( ! [X2 : $i,X0 : ($i > $o)] : ((((sK0 @ X0 @ X2)) != $true) | ($true != ((cQ @ (sK3 @ X0)))) | ($true = ((cQ @ X2))) | (((X0 @ (sK2 @ X0))) = $true)) )),
% 13.07/2.21 inference(cnf_transformation,[],[f8])).
% 13.07/2.21 thf(f26,definition,(
% 13.07/2.21 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 13.07/2.21 introduced(theory,[fool_exhaustiveness_axiom])).
% 13.07/2.21 thf(f29,plain,(
% 13.07/2.21 ( ! [X2 : ($i > $o),X1 : ($i > $o)] : (($true = (((^[Y0 : $i]: ((X2 @ Y0) & (X1 @ Y0))) @ (sK2 @ (^[Y0 : $i]: ((X2 @ Y0) & (X1 @ Y0))))))) | ($true != (((^[Y0 : $i]: ((X2 @ Y0) & (X1 @ Y0))) @ (sK1 @ (^[Y0 : $i]: ((X2 @ Y0) & (X1 @ Y0))))))) | ($true = (((^[Y0 : $i]: ((X2 @ Y0) & (X1 @ Y0))) @ (sK3 @ (^[Y0 : $i]: ((X2 @ Y0) & (X1 @ Y0)))))))) )),
% 13.07/2.21 inference(primitive_instantiation,[],[f11])).
% 13.07/2.21 thf(f33,plain,(
% 13.07/2.21 ( ! [X2 : ($i > $o),X1 : ($i > $o)] : (($true = (((X2 @ (sK3 @ (^[Y0 : $i]: ((X2 @ Y0) & (X1 @ Y0))))) & (X1 @ (sK3 @ (^[Y0 : $i]: ((X2 @ Y0) & (X1 @ Y0)))))))) | ((((X2 @ (sK1 @ (^[Y0 : $i]: ((X2 @ Y0) & (X1 @ Y0))))) & (X1 @ (sK1 @ (^[Y0 : $i]: ((X2 @ Y0) & (X1 @ Y0))))))) != $true) | ($true = (((X2 @ (sK2 @ (^[Y0 : $i]: ((X2 @ Y0) & (X1 @ Y0))))) & (X1 @ (sK2 @ (^[Y0 : $i]: ((X2 @ Y0) & (X1 @ Y0))))))))) )),
% 13.07/2.21 inference(beta-eta_normalization,[],[f29])).
% 13.07/2.21 thf(f35,plain,(
% 13.07/2.21 ( ! [X2 : ($i > $o),X1 : ($i > $o)] : ((((X2 @ (sK3 @ (^[Y0 : $i]: ((X2 @ Y0) & (X1 @ Y0)))))) = $true) | ($true = (((X2 @ (sK2 @ (^[Y0 : $i]: ((X2 @ Y0) & (X1 @ Y0))))) & (X1 @ (sK2 @ (^[Y0 : $i]: ((X2 @ Y0) & (X1 @ Y0)))))))) | ((((X2 @ (sK1 @ (^[Y0 : $i]: ((X2 @ Y0) & (X1 @ Y0))))) & (X1 @ (sK1 @ (^[Y0 : $i]: ((X2 @ Y0) & (X1 @ Y0))))))) != $true)) )),
% 13.07/2.21 inference(and_proxy_clausification,[],[f33])).
% 13.07/2.21 thf(f36,plain,(
% 13.07/2.21 ( ! [X2 : ($i > $o),X1 : ($i > $o)] : (($true = ((X1 @ (sK2 @ (^[Y0 : $i]: ((X2 @ Y0) & (X1 @ Y0))))))) | (((X2 @ (sK3 @ (^[Y0 : $i]: ((X2 @ Y0) & (X1 @ Y0)))))) = $true) | ((((X2 @ (sK1 @ (^[Y0 : $i]: ((X2 @ Y0) & (X1 @ Y0))))) & (X1 @ (sK1 @ (^[Y0 : $i]: ((X2 @ Y0) & (X1 @ Y0))))))) != $true)) )),
% 13.07/2.21 inference(and_proxy_clausification,[],[f35])).
% 13.07/2.21 thf(f39,plain,(
% 13.07/2.21 ( ! [X2 : ($i > $o),X1 : ($i > $o)] : (($false = ((X2 @ (sK1 @ (^[Y0 : $i]: ((X2 @ Y0) & (X1 @ Y0))))))) | ($false = ((X1 @ (sK1 @ (^[Y0 : $i]: ((X2 @ Y0) & (X1 @ Y0))))))) | (((X2 @ (sK3 @ (^[Y0 : $i]: ((X2 @ Y0) & (X1 @ Y0)))))) = $true) | ($true = ((X1 @ (sK2 @ (^[Y0 : $i]: ((X2 @ Y0) & (X1 @ Y0)))))))) )),
% 13.07/2.21 inference(and_proxy_clausification,[],[f36])).
% 13.07/2.21 thf(f52,plain,(
% 13.07/2.21 ( ! [X0 : ($i > $o)] : ((((cP @ (sK1 @ X0))) = $true) | (((X0 @ (sK3 @ X0))) = $true) | (((X0 @ (sK2 @ X0))) = $true) | (((X0 @ (sK3 @ X0))) = $true) | (((X0 @ (sK2 @ X0))) = $true) | ($true != $true)) )),
% 13.07/2.21 inference(superposition,[],[f19,f15])).
% 13.07/2.21 thf(f53,plain,(
% 13.07/2.21 ( ! [X0 : ($i > $o)] : ((((X0 @ (sK3 @ X0))) = $true) | ($true != $true) | (((X0 @ (sK2 @ X0))) = $true) | (((cP @ (sK1 @ X0))) = $true)) )),
% 13.07/2.21 inference(duplicate_literal_removal,[],[f52])).
% 13.07/2.21 thf(f54,plain,(
% 13.07/2.21 ( ! [X0 : ($i > $o)] : ((((cP @ (sK1 @ X0))) = $true) | (((X0 @ (sK3 @ X0))) = $true) | (((X0 @ (sK2 @ X0))) = $true)) )),
% 13.07/2.21 inference(trivial_inequality_removal,[],[f53])).
% 13.07/2.21 thf(f75,plain,(
% 13.07/2.21 ( ! [X0 : ($i > $o)] : ((((X0 @ (sK3 @ X0))) = $true) | ($true = ((cQ @ (sK1 @ X0)))) | (((X0 @ (sK3 @ X0))) = $true) | (((X0 @ (sK2 @ X0))) = $true) | (((X0 @ (sK2 @ X0))) = $true) | ($true != $true)) )),
% 13.07/2.21 inference(superposition,[],[f23,f15])).
% 13.07/2.21 thf(f76,plain,(
% 13.07/2.21 ( ! [X0 : ($i > $o)] : (($true = ((cQ @ (sK1 @ X0)))) | (((X0 @ (sK3 @ X0))) = $true) | ($true != $true) | (((X0 @ (sK2 @ X0))) = $true)) )),
% 13.07/2.21 inference(duplicate_literal_removal,[],[f75])).
% 13.07/2.21 thf(f77,plain,(
% 13.07/2.21 ( ! [X0 : ($i > $o)] : (($true = ((cQ @ (sK1 @ X0)))) | (((X0 @ (sK2 @ X0))) = $true) | (((X0 @ (sK3 @ X0))) = $true)) )),
% 13.07/2.21 inference(trivial_inequality_removal,[],[f76])).
% 13.07/2.21 thf(f100,plain,(
% 13.07/2.21 ( ! [X0 : ($i > $o)] : ((((X0 @ (sK3 @ X0))) = $true) | ($false = ((cP @ (sK2 @ X0)))) | (((sK0 @ X0 @ (sK1 @ X0))) = $true) | ($true != $true)) )),
% 13.07/2.21 inference(superposition,[],[f13,f26])).
% 13.07/2.21 thf(f103,plain,(
% 13.07/2.21 ( ! [X0 : ($i > $o),X1 : $i] : ((((cP @ (sK2 @ X0))) != $true) | ($true != ((cQ @ (sK3 @ X0)))) | (((cP @ X1)) = $true) | ($true != $true) | ($false = ((sK0 @ X0 @ X1)))) )),
% 13.07/2.21 inference(superposition,[],[f18,f26])).
% 13.07/2.21 thf(f105,plain,(
% 13.07/2.21 ( ! [X0 : ($i > $o),X1 : $i] : ((((cP @ X1)) = $true) | (((X0 @ (sK2 @ X0))) = $true) | ($false = ((sK0 @ X0 @ X1))) | ($true != $true) | ($true != ((cQ @ (sK3 @ X0))))) )),
% 13.07/2.21 inference(superposition,[],[f20,f26])).
% 13.07/2.21 thf(f119,plain,(
% 13.07/2.21 ( ! [X0 : ($i > $o)] : ((((sK0 @ X0 @ (sK1 @ X0))) = $true) | ($false = ((cP @ (sK2 @ X0)))) | (((X0 @ (sK3 @ X0))) = $true)) )),
% 13.07/2.21 inference(trivial_inequality_removal,[],[f100])).
% 13.07/2.21 thf(f122,plain,(
% 13.07/2.21 ( ! [X0 : ($i > $o),X1 : $i] : (($true != ((cQ @ (sK3 @ X0)))) | ($false = ((sK0 @ X0 @ X1))) | (((cP @ X1)) = $true) | (((X0 @ (sK2 @ X0))) = $true)) )),
% 13.07/2.21 inference(trivial_inequality_removal,[],[f105])).
% 13.07/2.21 thf(f129,plain,(
% 13.07/2.21 ( ! [X0 : ($i > $o),X1 : $i] : (($true != ((cQ @ (sK3 @ X0)))) | (((cP @ X1)) = $true) | (((cP @ (sK2 @ X0))) != $true) | ($false = ((sK0 @ X0 @ X1)))) )),
% 13.07/2.21 inference(trivial_inequality_removal,[],[f103])).
% 13.07/2.21 thf(f513,plain,(
% 13.07/2.21 ( ! [X0 : ($i > $o)] : ((((X0 @ (sK3 @ X0))) = $true) | ($false = ((cP @ (sK2 @ X0)))) | (((cP @ (sK1 @ X0))) = $true) | (((X0 @ (sK3 @ X0))) = $true) | ($true != $true) | (((cP @ (sK2 @ X0))) != $true)) )),
% 13.07/2.21 inference(superposition,[],[f17,f119])).
% 13.07/2.21 thf(f517,plain,(
% 13.07/2.21 ( ! [X0 : ($i > $o)] : (($true != $true) | (((cP @ (sK2 @ X0))) != $true) | (((X0 @ (sK3 @ X0))) = $true) | ($true = ((cQ @ (sK1 @ X0)))) | (((X0 @ (sK3 @ X0))) = $true) | ($false = ((cP @ (sK2 @ X0))))) )),
% 13.07/2.21 inference(superposition,[],[f21,f119])).
% 13.07/2.21 thf(f524,plain,(
% 13.07/2.21 ( ! [X0 : ($i > $o)] : ((((X0 @ (sK3 @ X0))) = $true) | ($false = ((cP @ (sK2 @ X0)))) | (((cP @ (sK1 @ X0))) = $true) | (((cP @ (sK2 @ X0))) != $true) | ($true != $true)) )),
% 13.07/2.21 inference(duplicate_literal_removal,[],[f513])).
% 13.07/2.21 thf(f525,plain,(
% 13.07/2.21 ( ! [X0 : ($i > $o)] : (($false = ((cP @ (sK2 @ X0)))) | (((cP @ (sK1 @ X0))) = $true) | (((X0 @ (sK3 @ X0))) = $true) | (((cP @ (sK2 @ X0))) != $true)) )),
% 13.07/2.21 inference(trivial_inequality_removal,[],[f524])).
% 13.07/2.21 thf(f526,plain,(
% 13.07/2.21 ( ! [X0 : ($i > $o)] : ((((X0 @ (sK3 @ X0))) = $true) | ($true = ((cQ @ (sK1 @ X0)))) | ($true != $true) | ($false = ((cP @ (sK2 @ X0)))) | (((cP @ (sK2 @ X0))) != $true)) )),
% 13.07/2.21 inference(duplicate_literal_removal,[],[f517])).
% 13.07/2.21 thf(f527,plain,(
% 13.07/2.21 ( ! [X0 : ($i > $o)] : (($true = ((cQ @ (sK1 @ X0)))) | (((X0 @ (sK3 @ X0))) = $true) | (((cP @ (sK2 @ X0))) != $true) | ($false = ((cP @ (sK2 @ X0))))) )),
% 13.07/2.21 inference(trivial_inequality_removal,[],[f526])).
% 13.07/2.21 thf(f534,plain,(
% 13.07/2.21 ( ! [X0 : ($i > $o)] : ((((cP @ (sK1 @ X0))) = $true) | (((X0 @ (sK3 @ X0))) = $true) | ($false = ((cP @ (sK2 @ X0))))) )),
% 13.07/2.21 inference(forward_subsumption_resolution,[],[f525,f26])).
% 13.07/2.21 thf(f535,plain,(
% 13.07/2.21 ( ! [X0 : ($i > $o)] : (($true = ((cQ @ (sK1 @ X0)))) | ($false = ((cP @ (sK2 @ X0)))) | (((X0 @ (sK3 @ X0))) = $true)) )),
% 13.07/2.21 inference(forward_subsumption_resolution,[],[f527,f26])).
% 13.07/2.21 thf(f1588,definition,(
% 13.07/2.21 spl4_11 <=> (((cQ @ (sK3 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) = $true)),
% 13.07/2.21 introduced(definition,[new_symbols(definition,[spl4_11])],[avatar_definition])).
% 13.07/2.21 thf(f1589,plain,(
% 13.07/2.21 (((cQ @ (sK3 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) != $true) | spl4_11),
% 13.07/2.21 inference(avatar_component_clause,[],[f1588])).
% 13.07/2.21 thf(f1590,plain,(
% 13.07/2.21 (((cQ @ (sK3 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) = $true) | ~spl4_11),
% 13.07/2.21 inference(avatar_component_clause,[],[f1588])).
% 13.07/2.21 thf(f1596,definition,(
% 13.07/2.21 spl4_13 <=> ($false = ((cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))))),
% 13.07/2.21 introduced(definition,[new_symbols(definition,[spl4_13])],[avatar_definition])).
% 13.07/2.21 thf(f1598,plain,(
% 13.07/2.21 ($false = ((cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | ~spl4_13),
% 13.07/2.21 inference(avatar_component_clause,[],[f1596])).
% 13.07/2.21 thf(f1608,definition,(
% 13.07/2.21 spl4_15 <=> (((cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) = $true)),
% 13.07/2.21 introduced(definition,[new_symbols(definition,[spl4_15])],[avatar_definition])).
% 13.07/2.21 thf(f1610,plain,(
% 13.07/2.21 (((cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) = $true) | ~spl4_15),
% 13.07/2.21 inference(avatar_component_clause,[],[f1608])).
% 13.07/2.21 thf(f1622,plain,(
% 13.07/2.21 ($true != $true) | ($true = ((sK0 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))) @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | ((((^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))) @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) = $true) | ~spl4_11),
% 13.07/2.21 inference(superposition,[],[f16,f1590])).
% 13.07/2.21 thf(f1624,plain,(
% 13.07/2.21 ( ! [X0 : $i] : (((((^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))) @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) = $true) | ($true != $true) | (((cP @ X0)) = $true) | ($false = ((sK0 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))) @ X0)))) ) | ~spl4_11),
% 13.07/2.21 inference(superposition,[],[f122,f1590])).
% 13.07/2.21 thf(f1640,plain,(
% 13.07/2.21 ( ! [X0 : $i] : (((((^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))) @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) = $true) | ($false = ((sK0 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))) @ X0))) | (((cP @ X0)) = $true)) ) | ~spl4_11),
% 13.07/2.21 inference(trivial_inequality_removal,[],[f1624])).
% 13.07/2.21 thf(f1641,plain,(
% 13.07/2.21 ( ! [X0 : $i] : ((((cP @ X0)) = $true) | ($true = (((cQ @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))) & (cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))))) | ($false = ((sK0 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))) @ X0)))) ) | ~spl4_11),
% 13.07/2.21 inference(beta-eta_normalization,[],[f1640])).
% 13.07/2.21 thf(f1642,plain,(
% 13.07/2.21 ( ! [X0 : $i] : ((((cP @ X0)) = $true) | (((cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) = $true) | ($false = ((sK0 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))) @ X0)))) ) | ~spl4_11),
% 13.07/2.21 inference(and_proxy_clausification,[],[f1641])).
% 13.07/2.21 thf(f1645,plain,(
% 13.07/2.21 ($true = ((sK0 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))) @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | ((((^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))) @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) = $true) | ~spl4_11),
% 13.07/2.21 inference(trivial_inequality_removal,[],[f1622])).
% 13.07/2.21 thf(f1646,plain,(
% 13.07/2.21 ($true = ((sK0 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))) @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | ($true = (((cQ @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))) & (cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))))) | ~spl4_11),
% 13.07/2.21 inference(beta-eta_normalization,[],[f1645])).
% 13.07/2.21 thf(f1647,plain,(
% 13.07/2.21 ($true = ((sK0 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))) @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | (((cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) = $true) | ~spl4_11),
% 13.07/2.21 inference(and_proxy_clausification,[],[f1646])).
% 13.07/2.21 thf(f1651,definition,(
% 13.07/2.21 spl4_16 <=> ($false = ((cQ @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))))),
% 13.07/2.21 introduced(definition,[new_symbols(definition,[spl4_16])],[avatar_definition])).
% 13.07/2.21 thf(f1653,plain,(
% 13.07/2.21 ($false = ((cQ @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | ~spl4_16),
% 13.07/2.21 inference(avatar_component_clause,[],[f1651])).
% 13.07/2.21 thf(f1655,definition,(
% 13.07/2.21 spl4_17 <=> ($false = ((cP @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))))),
% 13.07/2.21 introduced(definition,[new_symbols(definition,[spl4_17])],[avatar_definition])).
% 13.07/2.21 thf(f1657,plain,(
% 13.07/2.21 ($false = ((cP @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | ~spl4_17),
% 13.07/2.21 inference(avatar_component_clause,[],[f1655])).
% 13.07/2.21 thf(f1660,definition,(
% 13.07/2.21 spl4_18 <=> ($true = ((sK0 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))) @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))))),
% 13.07/2.21 introduced(definition,[new_symbols(definition,[spl4_18])],[avatar_definition])).
% 13.07/2.21 thf(f1662,plain,(
% 13.07/2.21 ($true = ((sK0 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))) @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | ~spl4_18),
% 13.07/2.21 inference(avatar_component_clause,[],[f1660])).
% 13.07/2.21 thf(f1672,definition,(
% 13.07/2.21 spl4_20 <=> ! [X0 : $i] : (($false = ((sK0 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))) @ X0))) | (((cP @ X0)) = $true))),
% 13.07/2.21 introduced(definition,[new_symbols(definition,[spl4_20])],[avatar_definition])).
% 13.07/2.21 thf(f1673,plain,(
% 13.07/2.21 ( ! [X0 : $i] : (($false = ((sK0 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))) @ X0))) | (((cP @ X0)) = $true)) ) | ~spl4_20),
% 13.07/2.21 inference(avatar_component_clause,[],[f1672])).
% 13.07/2.21 thf(f1675,plain,(
% 13.07/2.21 spl4_20 | spl4_15 | ~spl4_11),
% 13.07/2.21 inference(avatar_split_clause,[],[f1642,f1588,f1608,f1672])).
% 13.07/2.21 thf(f1678,plain,(
% 13.07/2.21 spl4_18 | spl4_15 | ~spl4_11),
% 13.07/2.21 inference(avatar_split_clause,[],[f1647,f1588,f1608,f1660])).
% 13.07/2.21 thf(f2482,plain,(
% 13.07/2.21 ( ! [X0 : ($i > $o)] : (($true = ((X0 @ (sK3 @ (^[Y0 : $i]: ((X0 @ Y0) & (cP @ Y0))))))) | ($false = ((X0 @ (sK1 @ (^[Y0 : $i]: ((X0 @ Y0) & (cP @ Y0))))))) | ($false = $true) | (((cP @ (sK2 @ (^[Y0 : $i]: ((X0 @ Y0) & (cP @ Y0)))))) = $true) | ((((^[Y0 : $i]: ((X0 @ Y0) & (cP @ Y0))) @ (sK2 @ (^[Y0 : $i]: ((X0 @ Y0) & (cP @ Y0)))))) = $true) | ((((^[Y0 : $i]: ((X0 @ Y0) & (cP @ Y0))) @ (sK3 @ (^[Y0 : $i]: ((X0 @ Y0) & (cP @ Y0)))))) = $true)) )),
% 13.07/2.21 inference(superposition,[],[f54,f39])).
% 13.07/2.21 thf(f2563,plain,(
% 13.07/2.21 ( ! [X0 : ($i > $o)] : ((((cP @ (sK2 @ (^[Y0 : $i]: ((X0 @ Y0) & (cP @ Y0)))))) = $true) | ((((^[Y0 : $i]: ((X0 @ Y0) & (cP @ Y0))) @ (sK2 @ (^[Y0 : $i]: ((X0 @ Y0) & (cP @ Y0)))))) = $true) | ((((^[Y0 : $i]: ((X0 @ Y0) & (cP @ Y0))) @ (sK3 @ (^[Y0 : $i]: ((X0 @ Y0) & (cP @ Y0)))))) = $true) | ($false = ((X0 @ (sK1 @ (^[Y0 : $i]: ((X0 @ Y0) & (cP @ Y0))))))) | ($true = ((X0 @ (sK3 @ (^[Y0 : $i]: ((X0 @ Y0) & (cP @ Y0)))))))) )),
% 13.07/2.21 inference(trivial_inequality_removal,[],[f2482])).
% 13.07/2.21 thf(f2564,plain,(
% 13.07/2.21 ( ! [X0 : ($i > $o)] : (((((X0 @ (sK3 @ (^[Y0 : $i]: ((X0 @ Y0) & (cP @ Y0))))) & (cP @ (sK3 @ (^[Y0 : $i]: ((X0 @ Y0) & (cP @ Y0))))))) = $true) | ($true = ((X0 @ (sK3 @ (^[Y0 : $i]: ((X0 @ Y0) & (cP @ Y0))))))) | (((cP @ (sK2 @ (^[Y0 : $i]: ((X0 @ Y0) & (cP @ Y0)))))) = $true) | ((((X0 @ (sK2 @ (^[Y0 : $i]: ((X0 @ Y0) & (cP @ Y0))))) & (cP @ (sK2 @ (^[Y0 : $i]: ((X0 @ Y0) & (cP @ Y0))))))) = $true) | ($false = ((X0 @ (sK1 @ (^[Y0 : $i]: ((X0 @ Y0) & (cP @ Y0)))))))) )),
% 13.07/2.21 inference(beta-eta_normalization,[],[f2563])).
% 13.07/2.21 thf(f2566,plain,(
% 13.07/2.21 ( ! [X0 : ($i > $o)] : (($false = ((X0 @ (sK1 @ (^[Y0 : $i]: ((X0 @ Y0) & (cP @ Y0))))))) | ((((X0 @ (sK2 @ (^[Y0 : $i]: ((X0 @ Y0) & (cP @ Y0))))) & (cP @ (sK2 @ (^[Y0 : $i]: ((X0 @ Y0) & (cP @ Y0))))))) = $true) | (((cP @ (sK2 @ (^[Y0 : $i]: ((X0 @ Y0) & (cP @ Y0)))))) = $true) | ($true = ((X0 @ (sK3 @ (^[Y0 : $i]: ((X0 @ Y0) & (cP @ Y0))))))) | ($true = ((X0 @ (sK3 @ (^[Y0 : $i]: ((X0 @ Y0) & (cP @ Y0)))))))) )),
% 13.07/2.21 inference(and_proxy_clausification,[],[f2564])).
% 13.07/2.21 thf(f2567,plain,(
% 13.07/2.21 ( ! [X0 : ($i > $o)] : (($true = ((X0 @ (sK3 @ (^[Y0 : $i]: ((X0 @ Y0) & (cP @ Y0))))))) | (((cP @ (sK2 @ (^[Y0 : $i]: ((X0 @ Y0) & (cP @ Y0)))))) = $true) | ($true = ((X0 @ (sK3 @ (^[Y0 : $i]: ((X0 @ Y0) & (cP @ Y0))))))) | ($false = ((X0 @ (sK1 @ (^[Y0 : $i]: ((X0 @ Y0) & (cP @ Y0))))))) | (((cP @ (sK2 @ (^[Y0 : $i]: ((X0 @ Y0) & (cP @ Y0)))))) = $true)) )),
% 13.07/2.21 inference(and_proxy_clausification,[],[f2566])).
% 13.07/2.21 thf(f2570,plain,(
% 13.07/2.21 ( ! [X0 : ($i > $o)] : (($false = ((X0 @ (sK1 @ (^[Y0 : $i]: ((X0 @ Y0) & (cP @ Y0))))))) | ($true = ((X0 @ (sK3 @ (^[Y0 : $i]: ((X0 @ Y0) & (cP @ Y0))))))) | (((cP @ (sK2 @ (^[Y0 : $i]: ((X0 @ Y0) & (cP @ Y0)))))) = $true)) )),
% 13.07/2.21 inference(duplicate_literal_removal,[],[f2567])).
% 13.07/2.21 thf(f3165,plain,(
% 13.07/2.21 (((cQ @ (sK3 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) = $true) | ($false = $true) | (((cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) = $true) | ($true = (((^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))) @ (sK3 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | ((((^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))) @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) = $true)),
% 13.07/2.21 inference(superposition,[],[f77,f2570])).
% 13.07/2.21 thf(f3230,plain,(
% 13.07/2.21 ($true = (((^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))) @ (sK3 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | ((((^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))) @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) = $true) | (((cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) = $true) | (((cQ @ (sK3 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) = $true)),
% 13.07/2.21 inference(trivial_inequality_removal,[],[f3165])).
% 13.07/2.21 thf(f3231,plain,(
% 13.07/2.21 (((cQ @ (sK3 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) = $true) | (((cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) = $true) | ($true = (((cQ @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))) & (cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))))) | ((((cQ @ (sK3 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))) & (cP @ (sK3 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) = $true)),
% 13.07/2.21 inference(beta-eta_normalization,[],[f3230])).
% 13.07/2.21 thf(f3232,plain,(
% 13.07/2.21 (((cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) = $true) | (((cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) = $true) | (((cQ @ (sK3 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) = $true) | ((((cQ @ (sK3 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))) & (cP @ (sK3 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) = $true)),
% 13.07/2.21 inference(and_proxy_clausification,[],[f3231])).
% 13.07/2.21 thf(f3238,plain,(
% 13.07/2.21 (((cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) = $true) | (((cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) = $true) | (((cQ @ (sK3 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) = $true) | (((cQ @ (sK3 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) = $true)),
% 13.07/2.21 inference(and_proxy_clausification,[],[f3232])).
% 13.07/2.21 thf(f3239,plain,(
% 13.07/2.21 (((cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) = $true) | (((cQ @ (sK3 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) = $true)),
% 13.07/2.21 inference(duplicate_literal_removal,[],[f3238])).
% 13.07/2.21 thf(f3376,plain,(
% 13.07/2.21 (((cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) = $true) | spl4_11),
% 13.07/2.21 inference(forward_subsumption_resolution,[],[f3239,f1589])).
% 13.07/2.21 thf(f3380,plain,(
% 13.07/2.21 spl4_15 | spl4_11),
% 13.07/2.21 inference(avatar_split_clause,[],[f3376,f1588,f1608])).
% 13.07/2.21 thf(f3383,plain,(
% 13.07/2.21 ($true != $true) | ($true = (((^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))) @ (sK3 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | ((((^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))) @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) != $true) | ~spl4_15),
% 13.07/2.21 inference(superposition,[],[f9,f1610])).
% 13.07/2.21 thf(f3391,plain,(
% 13.07/2.21 ($true = (((^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))) @ (sK3 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | ((((^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))) @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) != $true) | ~spl4_15),
% 13.07/2.21 inference(trivial_inequality_removal,[],[f3383])).
% 13.07/2.21 thf(f3392,plain,(
% 13.07/2.21 ((((cQ @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))) & (cP @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) != $true) | ((((cQ @ (sK3 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))) & (cP @ (sK3 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) = $true) | ~spl4_15),
% 13.07/2.21 inference(beta-eta_normalization,[],[f3391])).
% 13.07/2.21 thf(f3393,plain,(
% 13.07/2.21 ((((cQ @ (sK3 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))) & (cP @ (sK3 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) = $true) | ($false = ((cP @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | ($false = ((cQ @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | ~spl4_15),
% 13.07/2.21 inference(and_proxy_clausification,[],[f3392])).
% 13.07/2.21 thf(f3395,plain,(
% 13.07/2.21 (((cQ @ (sK3 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) = $true) | ($false = ((cP @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | ($false = ((cQ @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | ~spl4_15),
% 13.07/2.21 inference(and_proxy_clausification,[],[f3393])).
% 13.07/2.21 thf(f3414,plain,(
% 13.07/2.21 ($false = ((cQ @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | ($false = ((cP @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | (spl4_11 | ~spl4_15)),
% 13.07/2.21 inference(forward_subsumption_resolution,[],[f3395,f1589])).
% 13.07/2.21 thf(f3422,plain,(
% 13.07/2.21 spl4_16 | spl4_17 | spl4_11 | ~spl4_15),
% 13.07/2.21 inference(avatar_split_clause,[],[f3414,f1608,f1588,f1655,f1651])).
% 13.07/2.21 thf(f3427,plain,(
% 13.07/2.21 ($false = ((cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | ($false = $true) | ($true = (((^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))) @ (sK3 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | ~spl4_16),
% 13.07/2.21 inference(superposition,[],[f1653,f535])).
% 13.07/2.21 thf(f3435,plain,(
% 13.07/2.21 ($true = (((^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))) @ (sK3 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | ($false = ((cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | ~spl4_16),
% 13.07/2.21 inference(trivial_inequality_removal,[],[f3427])).
% 13.07/2.21 thf(f3436,plain,(
% 13.07/2.21 ($false = ((cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | ((((cQ @ (sK3 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))) & (cP @ (sK3 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) = $true) | ~spl4_16),
% 13.07/2.21 inference(beta-eta_normalization,[],[f3435])).
% 13.07/2.21 thf(f3438,plain,(
% 13.07/2.21 (((cQ @ (sK3 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) = $true) | ($false = ((cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | ~spl4_16),
% 13.07/2.21 inference(and_proxy_clausification,[],[f3436])).
% 13.07/2.21 thf(f3470,plain,(
% 13.07/2.21 ($false = ((cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | (spl4_11 | ~spl4_16)),
% 13.07/2.21 inference(forward_subsumption_resolution,[],[f3438,f1589])).
% 13.07/2.21 thf(f3476,plain,(
% 13.07/2.21 spl4_13 | spl4_11 | ~spl4_16),
% 13.07/2.21 inference(avatar_split_clause,[],[f3470,f1651,f1588,f1596])).
% 13.07/2.21 thf(f3478,plain,(
% 13.07/2.21 ($false = $true) | (~spl4_13 | ~spl4_15)),
% 13.07/2.21 inference(superposition,[],[f1598,f1610])).
% 13.07/2.21 thf(f3504,plain,(
% 13.07/2.21 $false | (~spl4_13 | ~spl4_15)),
% 13.07/2.21 inference(trivial_inequality_removal,[],[f3478])).
% 13.07/2.21 thf(f3505,plain,(
% 13.07/2.21 ~spl4_13 | ~spl4_15),
% 13.07/2.21 inference(avatar_contradiction_clause,[],[f3504])).
% 13.07/2.21 thf(f3526,plain,(
% 13.07/2.21 ($false = ((cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | ($true = (((^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))) @ (sK3 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | ($false = $true) | ~spl4_17),
% 13.07/2.21 inference(superposition,[],[f1657,f534])).
% 13.07/2.21 thf(f3565,plain,(
% 13.07/2.21 ($false = ((cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | ($true = (((^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))) @ (sK3 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | ~spl4_17),
% 13.07/2.21 inference(trivial_inequality_removal,[],[f3526])).
% 13.07/2.21 thf(f3566,plain,(
% 13.07/2.21 ((((cQ @ (sK3 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))) & (cP @ (sK3 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) = $true) | ($false = ((cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | ~spl4_17),
% 13.07/2.21 inference(beta-eta_normalization,[],[f3565])).
% 13.07/2.21 thf(f3568,plain,(
% 13.07/2.21 ($false = ((cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | (((cQ @ (sK3 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) = $true) | ~spl4_17),
% 13.07/2.21 inference(and_proxy_clausification,[],[f3566])).
% 13.07/2.21 thf(f3579,plain,(
% 13.07/2.21 (((cQ @ (sK3 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) = $true) | ($false = $true) | (~spl4_15 | ~spl4_17)),
% 13.07/2.21 inference(forward_demodulation,[],[f3568,f1610])).
% 13.07/2.21 thf(f3580,plain,(
% 13.07/2.21 (((cQ @ (sK3 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) = $true) | (~spl4_15 | ~spl4_17)),
% 13.07/2.21 inference(trivial_inequality_removal,[],[f3579])).
% 13.07/2.21 thf(f3590,plain,(
% 13.07/2.21 spl4_11 | ~spl4_15 | ~spl4_17),
% 13.07/2.21 inference(avatar_split_clause,[],[f3580,f1655,f1608,f1588])).
% 13.07/2.21 thf(f3592,plain,(
% 13.07/2.21 ($true != $true) | ((((^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))) @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) != $true) | (((cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) != $true) | ~spl4_11),
% 13.07/2.21 inference(superposition,[],[f10,f1590])).
% 13.07/2.21 thf(f3593,plain,(
% 13.07/2.21 ($true != $true) | ((((^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))) @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) != $true) | ((((^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))) @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) = $true) | ~spl4_11),
% 13.07/2.21 inference(superposition,[],[f12,f1590])).
% 13.07/2.21 thf(f3594,plain,(
% 13.07/2.21 (((cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) != $true) | ($true != $true) | ($true = ((sK0 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))) @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | ~spl4_11),
% 13.07/2.21 inference(superposition,[],[f14,f1590])).
% 13.07/2.21 thf(f3599,plain,(
% 13.07/2.21 ( ! [X0 : $i] : ((((cP @ X0)) = $true) | ($false = ((sK0 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))) @ X0))) | (((cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) != $true) | ($true != $true)) ) | ~spl4_11),
% 13.07/2.21 inference(superposition,[],[f129,f1590])).
% 13.07/2.21 thf(f3600,plain,(
% 13.07/2.21 ((((^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))) @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) != $true) | (((cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) != $true) | ~spl4_11),
% 13.07/2.21 inference(trivial_inequality_removal,[],[f3592])).
% 13.07/2.21 thf(f3601,plain,(
% 13.07/2.21 ((((cQ @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))) & (cP @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) != $true) | (((cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) != $true) | ~spl4_11),
% 13.07/2.21 inference(beta-eta_normalization,[],[f3600])).
% 13.07/2.21 thf(f3602,plain,(
% 13.07/2.21 ($false = ((cP @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | ($false = ((cQ @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | (((cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) != $true) | ~spl4_11),
% 13.07/2.21 inference(and_proxy_clausification,[],[f3601])).
% 13.07/2.21 thf(f3603,plain,(
% 13.07/2.21 ((((^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))) @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) = $true) | ((((^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))) @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) != $true) | ~spl4_11),
% 13.07/2.21 inference(trivial_inequality_removal,[],[f3593])).
% 13.07/2.21 thf(f3604,plain,(
% 13.07/2.21 ($true = (((cQ @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))) & (cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))))) | ((((cQ @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))) & (cP @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) != $true) | ~spl4_11),
% 13.07/2.21 inference(beta-eta_normalization,[],[f3603])).
% 13.07/2.21 thf(f3605,plain,(
% 13.07/2.21 (((cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) = $true) | ((((cQ @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))) & (cP @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) != $true) | ~spl4_11),
% 13.07/2.21 inference(and_proxy_clausification,[],[f3604])).
% 13.07/2.21 thf(f3608,plain,(
% 13.07/2.21 ($false = ((cQ @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | (((cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) = $true) | ($false = ((cP @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | ~spl4_11),
% 13.07/2.21 inference(and_proxy_clausification,[],[f3605])).
% 13.07/2.21 thf(f3610,plain,(
% 13.07/2.21 ( ! [X0 : $i] : ((((cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) != $true) | ($false = ((sK0 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))) @ X0))) | (((cP @ X0)) = $true)) ) | ~spl4_11),
% 13.07/2.21 inference(trivial_inequality_removal,[],[f3599])).
% 13.07/2.21 thf(f3623,plain,(
% 13.07/2.21 (((cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) != $true) | ($true = ((sK0 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))) @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | ~spl4_11),
% 13.07/2.21 inference(trivial_inequality_removal,[],[f3594])).
% 13.07/2.21 thf(f3625,plain,(
% 13.07/2.21 ( ! [X0 : $i] : ((((cP @ X0)) = $true) | ($false = ((sK0 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))) @ X0)))) ) | (~spl4_11 | ~spl4_15)),
% 13.07/2.21 inference(forward_subsumption_resolution,[],[f3610,f1610])).
% 13.07/2.21 thf(f3626,plain,(
% 13.07/2.21 ($true = ((sK0 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))) @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | (~spl4_11 | ~spl4_15)),
% 13.07/2.21 inference(forward_subsumption_resolution,[],[f3623,f1610])).
% 13.07/2.21 thf(f3628,plain,(
% 13.07/2.21 spl4_20 | ~spl4_11 | ~spl4_15),
% 13.07/2.21 inference(avatar_split_clause,[],[f3625,f1608,f1588,f1672])).
% 13.07/2.21 thf(f3629,plain,(
% 13.07/2.21 spl4_18 | ~spl4_11 | ~spl4_15),
% 13.07/2.21 inference(avatar_split_clause,[],[f3626,f1608,f1588,f1660])).
% 13.07/2.21 thf(f3835,plain,(
% 13.07/2.21 ($false = $true) | (((cP @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) = $true) | (~spl4_18 | ~spl4_20)),
% 13.07/2.21 inference(superposition,[],[f1662,f1673])).
% 13.07/2.21 thf(f3842,plain,(
% 13.07/2.21 (((cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) != $true) | (((cQ @ (sK3 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) != $true) | ($true = ((cQ @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | ($true != $true) | ~spl4_18),
% 13.07/2.21 inference(superposition,[],[f22,f1662])).
% 13.07/2.21 thf(f3844,plain,(
% 13.07/2.21 ($true != $true) | ((((^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))) @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) = $true) | (((cQ @ (sK3 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) != $true) | ($true = ((cQ @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | ~spl4_18),
% 13.07/2.21 inference(superposition,[],[f24,f1662])).
% 13.07/2.21 thf(f3871,plain,(
% 13.07/2.21 (((cQ @ (sK3 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) != $true) | ($true = ((cQ @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | (((cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) != $true) | ~spl4_18),
% 13.07/2.21 inference(trivial_inequality_removal,[],[f3842])).
% 13.07/2.21 thf(f3915,plain,(
% 13.07/2.21 (((cQ @ (sK3 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) != $true) | ($true = ((cQ @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | ((((^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))) @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) = $true) | ~spl4_18),
% 13.07/2.21 inference(trivial_inequality_removal,[],[f3844])).
% 13.07/2.21 thf(f3916,plain,(
% 13.07/2.21 (((cQ @ (sK3 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) != $true) | ($true = (((cQ @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))) & (cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))))) | ($true = ((cQ @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | ~spl4_18),
% 13.07/2.21 inference(beta-eta_normalization,[],[f3915])).
% 13.07/2.21 thf(f3917,plain,(
% 13.07/2.21 ($true = ((cQ @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | (((cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) = $true) | (((cQ @ (sK3 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) != $true) | ~spl4_18),
% 13.07/2.21 inference(and_proxy_clausification,[],[f3916])).
% 13.07/2.21 thf(f3935,plain,(
% 13.07/2.21 (((cP @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) = $true) | (~spl4_18 | ~spl4_20)),
% 13.07/2.21 inference(trivial_inequality_removal,[],[f3835])).
% 13.07/2.21 thf(f3966,plain,(
% 13.07/2.21 ($false = $true) | (~spl4_17 | ~spl4_18 | ~spl4_20)),
% 13.07/2.21 inference(forward_demodulation,[],[f3935,f1657])).
% 13.07/2.21 thf(f3967,plain,(
% 13.07/2.21 $false | (~spl4_17 | ~spl4_18 | ~spl4_20)),
% 13.07/2.21 inference(trivial_inequality_removal,[],[f3966])).
% 13.07/2.21 thf(f3968,plain,(
% 13.07/2.21 ~spl4_17 | ~spl4_18 | ~spl4_20),
% 13.07/2.21 inference(avatar_contradiction_clause,[],[f3967])).
% 13.07/2.21 thf(f3975,plain,(
% 13.07/2.21 spl4_16 | spl4_17 | spl4_15 | ~spl4_11),
% 13.07/2.21 inference(avatar_split_clause,[],[f3608,f1588,f1608,f1655,f1651])).
% 13.07/2.21 thf(f3977,plain,(
% 13.07/2.21 (((cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) != $true) | ($true = ((cQ @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | (~spl4_11 | ~spl4_18)),
% 13.07/2.21 inference(forward_subsumption_resolution,[],[f3871,f1590])).
% 13.07/2.21 thf(f3978,plain,(
% 13.07/2.21 ~spl4_15 | spl4_17 | spl4_16 | ~spl4_11),
% 13.07/2.21 inference(avatar_split_clause,[],[f3602,f1588,f1651,f1655,f1608])).
% 13.07/2.21 thf(f3979,plain,(
% 13.07/2.21 ($true = ((cQ @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | (((cP @ (sK2 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))) = $true) | (~spl4_11 | ~spl4_18)),
% 13.07/2.21 inference(forward_subsumption_resolution,[],[f3917,f1590])).
% 13.07/2.21 thf(f3987,definition,(
% 13.07/2.21 spl4_28 <=> ($true = ((cQ @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0)))))))),
% 13.07/2.21 introduced(definition,[new_symbols(definition,[spl4_28])],[avatar_definition])).
% 13.07/2.21 thf(f3989,plain,(
% 13.07/2.21 ($true = ((cQ @ (sK1 @ (^[Y0 : $i]: ((cQ @ Y0) & (cP @ Y0))))))) | ~spl4_28),
% 13.07/2.21 inference(avatar_component_clause,[],[f3987])).
% 13.07/2.21 thf(f3990,plain,(
% 13.07/2.21 spl4_28 | ~spl4_15 | ~spl4_11 | ~spl4_18),
% 13.07/2.21 inference(avatar_split_clause,[],[f3977,f1660,f1588,f1608,f3987])).
% 13.07/2.21 thf(f3991,plain,(
% 13.07/2.21 spl4_28 | spl4_15 | ~spl4_11 | ~spl4_18),
% 13.07/2.21 inference(avatar_split_clause,[],[f3979,f1660,f1588,f1608,f3987])).
% 13.07/2.21 thf(f4085,plain,(
% 13.07/2.21 ($false = $true) | (~spl4_16 | ~spl4_28)),
% 13.07/2.21 inference(forward_demodulation,[],[f3989,f1653])).
% 13.07/2.21 thf(f4086,plain,(
% 13.07/2.21 $false | (~spl4_16 | ~spl4_28)),
% 13.07/2.21 inference(trivial_inequality_removal,[],[f4085])).
% 13.07/2.21 thf(f4087,plain,(
% 13.07/2.21 ~spl4_16 | ~spl4_28),
% 13.07/2.21 inference(avatar_contradiction_clause,[],[f4086])).
% 13.07/2.21 cnf(s32, plain, ~spl4_11 | spl4_15 | spl4_20, inference(sat_conversion,[],[f1675])).
% 13.07/2.21 cnf(s35, plain, ~spl4_11 | spl4_15 | spl4_18, inference(sat_conversion,[],[f1678])).
% 13.07/2.21 cnf(s49, plain, spl4_11 | spl4_15, inference(sat_conversion,[],[f3380])).
% 13.07/2.21 cnf(s57, plain, spl4_11 | ~spl4_15 | spl4_16 | spl4_17, inference(sat_conversion,[],[f3422])).
% 13.07/2.21 cnf(s61, plain, spl4_11 | spl4_13 | ~spl4_16, inference(sat_conversion,[],[f3476])).
% 13.07/2.21 cnf(s65, plain, ~spl4_13 | ~spl4_15, inference(sat_conversion,[],[f3505])).
% 13.07/2.21 cnf(s74, plain, spl4_11 | ~spl4_15 | ~spl4_17, inference(sat_conversion,[],[f3590])).
% 13.07/2.21 cnf(s79, plain, ~spl4_11 | ~spl4_15 | spl4_20, inference(sat_conversion,[],[f3628])).
% 13.07/2.21 cnf(s80, plain, ~spl4_11 | ~spl4_15 | spl4_18, inference(sat_conversion,[],[f3629])).
% 13.07/2.21 cnf(s82, plain, ~spl4_17 | ~spl4_18 | ~spl4_20, inference(sat_conversion,[],[f3968])).
% 13.07/2.21 cnf(s84, plain, ~spl4_11 | spl4_15 | spl4_16 | spl4_17, inference(sat_conversion,[],[f3975])).
% 13.07/2.21 cnf(s85, plain, ~spl4_11 | ~spl4_15 | spl4_16 | spl4_17, inference(sat_conversion,[],[f3978])).
% 13.07/2.21 cnf(s88, plain, ~spl4_11 | ~spl4_15 | ~spl4_18 | spl4_28, inference(sat_conversion,[],[f3990])).
% 13.07/2.21 cnf(s89, plain, ~spl4_11 | spl4_15 | ~spl4_18 | spl4_28, inference(sat_conversion,[],[f3991])).
% 13.07/2.21 cnf(s92, plain, ~spl4_16 | ~spl4_28, inference(sat_conversion,[],[f4087])).
% 13.07/2.21 cnf(s93, plain, ~spl4_15 | spl4_11, inference(rat,[],[s61,s57,s65,s74])).
% 13.07/2.21 cnf(s94, plain, spl4_11, inference(rat,[],[s93,s49])).
% 13.07/2.21 cnf(s95, plain, ~spl4_15, inference(rat,[],[s92,s85,s88,s82,s79,s80,s94])).
% 13.07/2.21 cnf(s97, plain, spl4_18, inference(rat,[],[s35,s94,s95])).
% 13.07/2.21 cnf(s98, plain, spl4_20, inference(rat,[],[s32,s94,s95])).
% 13.07/2.21 cnf(s100, plain, ~spl4_17, inference(rat,[],[s82,s98,s97])).
% 13.07/2.21 cnf(s101, plain, spl4_28, inference(rat,[],[s89,s95,s94,s97])).
% 13.07/2.21 cnf(s103, plain, spl4_16, inference(rat,[],[s84,s95,s94,s100])).
% 13.07/2.21 cnf(s104, plain, $false, inference(rat,[],[s92,s101,s103])).
% 13.07/2.21 thf(f4088,plain,(
% 13.07/2.21 $false),
% 13.07/2.21 inference(avatar_sat_refutation,[],[s104])).
% 13.07/2.21 % SZS output end Proof for theBenchmark
% 13.07/2.21 % (2831810)------------------------------
% 13.07/2.21 % (2831810)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.07/2.21 % (2831810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.07/2.21 % (2831810)CaDiCaL version: 2.1.3
% 13.07/2.21 % (2831810)Termination reason: Refutation
% 13.07/2.21 % (2831810)Time elapsed: 0.143 s
% 13.07/2.21 % (2831810)Peak memory usage: 13 MB
% 13.07/2.21 % (2831810)Instructions burned: 223 (million)
% 13.07/2.21 % (2831544)Success in time 1.956 s
% 13.07/2.21 % Vampire exiting
%------------------------------------------------------------------------------