%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEV208^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 : n011.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:02 AM UTC 2026
% Result : Theorem 27.49s 4.44s
% Output : Refutation 27.49s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV208^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.09/0.20 % Computer : n011.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Tue Sep 29 15:21:16 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running higher-order theorem proving
% 0.09/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.77/0.41 % (213421)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.77/0.41 % (213431)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=679362632:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.77/0.41 % (213427)lrs+10_16_si=on:nwc=1.5:random_seed=802501834:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.77/0.41 % (213429)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=785908466: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.77/0.41 % (213426)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=110304349:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.77/0.41 % (213428)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=1174107574:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.77/0.41 % (213428)Instruction limit reached!
% 0.77/0.41 % (213428)------------------------------
% 0.77/0.41 % (213428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.41 % (213428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.41 % (213428)CaDiCaL version: 2.1.3
% 0.77/0.41 % (213428)Termination reason: Instruction limit
% 0.77/0.41 % (213428)Termination phase: Property scanning
% 0.77/0.41 % (213428)Time elapsed: 0.002 s
% 0.77/0.41 % (213428)Peak memory usage: 10 MB
% 0.77/0.41 % (213428)Instructions burned: 4 (million)
% 0.77/0.41 % (213432)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.77/0.41 % (213427)Instruction limit reached!
% 0.77/0.41 % (213427)------------------------------
% 0.77/0.41 % (213427)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.41 % (213427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.41 % (213432)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.77/0.41 % (213427)CaDiCaL version: 2.1.3
% 0.77/0.41 % (213427)Termination reason: Instruction limit
% 0.77/0.41 % (213427)Termination phase: Saturation
% 0.77/0.41 % (213427)Time elapsed: 0.010 s
% 0.77/0.41 % (213427)Peak memory usage: 12 MB
% 0.77/0.41 % (213427)Instructions burned: 20 (million)
% 0.77/0.41 % (213432)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=1922877987:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.77/0.41 % (213430)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=4085913350:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.77/0.41 % (213438)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2173060974:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.77/0.41 % (213438)Instruction limit reached!
% 0.77/0.41 % (213438)------------------------------
% 0.77/0.41 % (213438)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.41 % (213438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.41 % (213438)CaDiCaL version: 2.1.3
% 0.77/0.41 % (213438)Termination reason: Instruction limit
% 0.77/0.41 % (213438)Termination phase: Property scanning
% 0.77/0.41 % (213438)Time elapsed: 0.003 s
% 0.77/0.41 % (213438)Peak memory usage: 10 MB
% 0.77/0.41 % (213438)Instructions burned: 6 (million)
% 0.77/0.41 % (213431)Instruction limit reached!
% 0.77/0.41 % (213431)------------------------------
% 0.77/0.41 % (213431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.41 % (213431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.41 % (213431)CaDiCaL version: 2.1.3
% 0.77/0.41 % (213431)Termination reason: Instruction limit
% 0.77/0.41 % (213431)Termination phase: Saturation
% 0.77/0.41 % (213431)Time elapsed: 0.029 s
% 0.77/0.41 % (213431)Peak memory usage: 13 MB
% 0.77/0.41 % (213431)Instructions burned: 76 (million)
% 0.77/0.41 % (213439)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=2993063707:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.77/0.41 % (213439)Instruction limit reached!
% 0.77/0.47 % (213439)------------------------------
% 0.77/0.47 % (213439)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.47 % (213439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.47 % (213439)CaDiCaL version: 2.1.3
% 0.77/0.47 % (213439)Termination reason: Instruction limit
% 0.77/0.47 % (213439)Termination phase: Property scanning
% 0.77/0.47 % (213439)Time elapsed: 0.002 s
% 0.77/0.47 % (213439)Peak memory usage: 10 MB
% 0.77/0.47 % (213439)Instructions burned: 5 (million)
% 0.77/0.47 % (213443)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.77/0.47 % (213443)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=4272747348:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.77/0.47 % (213446)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.77/0.47 % (213446)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.77/0.47 % (213430)Instruction limit reached!
% 0.77/0.47 % (213430)------------------------------
% 0.77/0.47 % (213430)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.47 % (213430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.47 % (213430)CaDiCaL version: 2.1.3
% 0.77/0.47 % (213444)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=1360384979:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.77/0.47 % (213430)Termination reason: Instruction limit
% 0.77/0.47 % (213430)Termination phase: Saturation
% 0.77/0.47 % (213430)Time elapsed: 0.028 s
% 0.77/0.47 % (213430)Peak memory usage: 12 MB
% 0.77/0.47 % (213430)Instructions burned: 24 (million)
% 0.77/0.47 % (213443)Instruction limit reached!
% 0.77/0.47 % (213443)------------------------------
% 0.77/0.47 % (213443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.47 % (213443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.47 % (213443)CaDiCaL version: 2.1.3
% 0.77/0.47 % (213443)Termination reason: Instruction limit
% 0.77/0.47 % (213443)Termination phase: Saturation
% 0.77/0.47 % (213443)Time elapsed: 0.004 s
% 0.77/0.47 % (213443)Peak memory usage: 12 MB
% 0.77/0.47 % (213443)Instructions burned: 8 (million)
% 0.77/0.47 % (213446)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=143466005: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.77/0.47 % (213444)Instruction limit reached!
% 0.77/0.47 % (213444)------------------------------
% 0.77/0.47 % (213444)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.47 % (213444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.47 % (213444)CaDiCaL version: 2.1.3
% 0.77/0.47 % (213444)Termination reason: Instruction limit
% 0.77/0.47 % (213444)Termination phase: Saturation
% 0.77/0.47 % (213444)Time elapsed: 0.006 s
% 0.77/0.47 % (213444)Peak memory usage: 12 MB
% 0.77/0.47 % (213444)Instructions burned: 12 (million)
% 0.77/0.47 % (213426)Instruction limit reached!
% 0.77/0.47 % (213426)------------------------------
% 0.77/0.47 % (213426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.47 % (213426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.47 % (213426)CaDiCaL version: 2.1.3
% 0.77/0.47 % (213426)Termination reason: Instruction limit
% 0.77/0.47 % (213426)Termination phase: Saturation
% 0.77/0.47 % (213426)Time elapsed: 0.055 s
% 0.77/0.47 % (213426)Peak memory usage: 13 MB
% 0.77/0.47 % (213426)Instructions burned: 88 (million)
% 0.77/0.47 % (213446)Instruction limit reached!
% 0.77/0.47 % (213446)------------------------------
% 0.77/0.47 % (213446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.47 % (213446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.47 % (213446)CaDiCaL version: 2.1.3
% 0.77/0.47 % (213446)Termination reason: Instruction limit
% 0.77/0.47 % (213446)Termination phase: Saturation
% 0.77/0.47 % (213446)Time elapsed: 0.013 s
% 0.77/0.47 % (213446)Peak memory usage: 11 MB
% 1.41/0.51 % (213446)Instructions burned: 29 (million)
% 1.41/0.51 % (213449)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=1807889778:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 1.41/0.51 % (213452)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 1.41/0.51 % (213452)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=2603938032:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 1.41/0.51 % (213453)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=392951844:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 1.41/0.51 % (213452)Instruction limit reached!
% 1.41/0.51 % (213452)------------------------------
% 1.41/0.51 % (213452)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.41/0.51 % (213452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.41/0.51 % (213452)CaDiCaL version: 2.1.3
% 1.41/0.51 % (213452)Termination reason: Instruction limit
% 1.41/0.51 % (213452)Termination phase: Saturation
% 1.41/0.51 % (213452)Time elapsed: 0.003 s
% 1.41/0.51 % (213452)Peak memory usage: 11 MB
% 1.41/0.51 % (213452)Instructions burned: 7 (million)
% 1.41/0.51 % (213450)lrs+10_1_si=on:cs=on:random_seed=1276778834:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 1.41/0.51 % (213454)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=3427384233:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 1.41/0.51 % (213450)Instruction limit reached!
% 1.41/0.51 % (213450)------------------------------
% 1.41/0.51 % (213450)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.41/0.51 % (213450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.41/0.51 % (213450)CaDiCaL version: 2.1.3
% 1.41/0.51 % (213450)Termination reason: Instruction limit
% 1.41/0.51 % (213450)Termination phase: Saturation
% 1.41/0.51 % (213450)Time elapsed: 0.005 s
% 1.41/0.51 % (213450)Peak memory usage: 12 MB
% 1.41/0.51 % (213450)Instructions burned: 10 (million)
% 1.41/0.51 % (213453)Instruction limit reached!
% 1.41/0.51 % (213453)------------------------------
% 1.41/0.51 % (213453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.41/0.51 % (213453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.41/0.51 % (213453)CaDiCaL version: 2.1.3
% 1.41/0.51 % (213453)Termination reason: Instruction limit
% 1.41/0.51 % (213453)Termination phase: Saturation
% 1.41/0.51 % (213453)Time elapsed: 0.015 s
% 1.41/0.51 % (213453)Peak memory usage: 13 MB
% 1.41/0.51 % (213453)Instructions burned: 39 (million)
% 1.41/0.51 % (213458)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=2977038696:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 1.41/0.51 % (213449)Instruction limit reached!
% 1.41/0.51 % (213449)------------------------------
% 1.41/0.51 % (213449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.41/0.51 % (213449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.41/0.51 % (213449)CaDiCaL version: 2.1.3
% 1.41/0.51 % (213449)Termination reason: Instruction limit
% 1.41/0.51 % (213449)Termination phase: Saturation
% 1.41/0.51 % (213449)Time elapsed: 0.042 s
% 1.41/0.51 % (213449)Peak memory usage: 13 MB
% 1.41/0.51 % (213449)Instructions burned: 88 (million)
% 1.41/0.51 % (213458)Instruction limit reached!
% 1.41/0.51 % (213458)------------------------------
% 1.41/0.51 % (213458)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.41/0.51 % (213458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.41/0.51 % (213458)CaDiCaL version: 2.1.3
% 1.41/0.51 % (213458)Termination reason: Instruction limit
% 1.41/0.51 % (213458)Termination phase: Saturation
% 1.41/0.51 % (213458)Time elapsed: 0.014 s
% 1.41/0.51 % (213458)Peak memory usage: 12 MB
% 1.41/0.51 % (213458)Instructions burned: 26 (million)
% 1.41/0.51 % (213462)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=3143425062:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 1.41/0.51 % (213461)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=614332927:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.41/0.58 % (213464)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=952632567:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.41/0.58 % (213465)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=925300932: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)
% 1.41/0.58 % (213465)Instruction limit reached!
% 1.41/0.58 % (213465)------------------------------
% 1.41/0.58 % (213465)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.41/0.58 % (213465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.41/0.58 % (213465)CaDiCaL version: 2.1.3
% 1.41/0.58 % (213465)Termination reason: Instruction limit
% 1.41/0.58 % (213465)Termination phase: Preprocessing 3
% 1.41/0.58 % (213465)Time elapsed: 0.001 s
% 1.41/0.58 % (213465)Peak memory usage: 10 MB
% 1.41/0.58 % (213465)Instructions burned: 2 (million)
% 1.41/0.58 % (213464)Instruction limit reached!
% 1.41/0.58 % (213464)------------------------------
% 1.41/0.58 % (213464)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.41/0.58 % (213464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.41/0.58 % (213464)CaDiCaL version: 2.1.3
% 1.41/0.58 % (213464)Termination reason: Instruction limit
% 1.41/0.58 % (213464)Termination phase: Saturation
% 1.41/0.58 % (213464)Time elapsed: 0.008 s
% 1.41/0.58 % (213464)Peak memory usage: 12 MB
% 1.41/0.58 % (213464)Instructions burned: 15 (million)
% 1.41/0.58 % (213461)Instruction limit reached!
% 1.41/0.58 % (213461)------------------------------
% 1.41/0.58 % (213461)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.41/0.58 % (213461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.41/0.58 % (213461)CaDiCaL version: 2.1.3
% 1.41/0.58 % (213461)Termination reason: Instruction limit
% 1.41/0.58 % (213461)Termination phase: Saturation
% 1.41/0.58 % (213461)Time elapsed: 0.016 s
% 1.41/0.58 % (213461)Peak memory usage: 12 MB
% 1.41/0.58 % (213461)Instructions burned: 15 (million)
% 1.41/0.58 % (213470)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3819333887:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.41/0.58 % (213471)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=189922233:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.41/0.58 % (213470)Instruction limit reached!
% 1.41/0.58 % (213470)------------------------------
% 1.41/0.58 % (213470)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.41/0.58 % (213470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.41/0.58 % (213470)CaDiCaL version: 2.1.3
% 1.41/0.58 % (213470)Termination reason: Instruction limit
% 1.41/0.58 % (213470)Termination phase: Saturation
% 1.41/0.58 % (213470)Time elapsed: 0.012 s
% 1.41/0.58 % (213470)Peak memory usage: 12 MB
% 1.41/0.58 % (213470)Instructions burned: 26 (million)
% 1.41/0.58 % (213432)Instruction limit reached!
% 1.41/0.58 % (213432)------------------------------
% 1.41/0.58 % (213432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.41/0.58 % (213432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.41/0.58 % (213432)CaDiCaL version: 2.1.3
% 1.41/0.58 % (213432)Termination reason: Instruction limit
% 1.41/0.58 % (213432)Termination phase: Saturation
% 1.41/0.58 % (213432)Time elapsed: 0.148 s
% 1.41/0.58 % (213432)Peak memory usage: 13 MB
% 1.41/0.58 % (213432)Instructions burned: 158 (million)
% 1.41/0.58 % (213471)Instruction limit reached!
% 1.41/0.58 % (213471)------------------------------
% 1.41/0.58 % (213471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.41/0.58 % (213471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.41/0.58 % (213471)CaDiCaL version: 2.1.3
% 1.41/0.58 % (213471)Termination reason: Instruction limit
% 1.41/0.58 % (213471)Termination phase: Saturation
% 1.41/0.58 % (213471)Time elapsed: 0.012 s
% 1.41/0.58 % (213471)Peak memory usage: 12 MB
% 1.41/0.58 % (213471)Instructions burned: 24 (million)
% 1.41/0.58 % (213472)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=2688237695:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 1.41/0.58 % (213475)WARNING Broken Constraint: if sine_to_age_generality_threshold(10) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 2.32/0.67 % (213475)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 2.32/0.67 % (213475)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=1178538694:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 2.32/0.67 % (213477)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=3632480156:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2997 on theBenchmark for (2997ds/31Mi)
% 2.32/0.67 % (213475)Instruction limit reached!
% 2.32/0.67 % (213475)------------------------------
% 2.32/0.67 % (213475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.32/0.67 % (213475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.32/0.67 % (213475)CaDiCaL version: 2.1.3
% 2.32/0.67 % (213475)Termination reason: Instruction limit
% 2.32/0.67 % (213475)Termination phase: Saturation
% 2.32/0.67 % (213475)Time elapsed: 0.007 s
% 2.32/0.67 % (213475)Peak memory usage: 12 MB
% 2.32/0.67 % (213475)Instructions burned: 15 (million)
% 2.32/0.67 % (213476)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 2.32/0.67 % (213477)Instruction limit reached!
% 2.32/0.67 % (213477)------------------------------
% 2.32/0.67 % (213477)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.32/0.67 % (213477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.32/0.67 % (213477)CaDiCaL version: 2.1.3
% 2.32/0.67 % (213477)Termination reason: Instruction limit
% 2.32/0.67 % (213477)Termination phase: Saturation
% 2.32/0.67 % (213477)Time elapsed: 0.014 s
% 2.32/0.67 % (213477)Peak memory usage: 12 MB
% 2.32/0.67 % (213477)Instructions burned: 31 (million)
% 2.32/0.67 % (213476)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=917968123:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 2.32/0.67 % (213481)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=1817745460:i=7:hud=5:bd=preordered:rtra=on:bet=on_2997 on theBenchmark for (2997ds/7Mi)
% 2.32/0.67 % (213481)Instruction limit reached!
% 2.32/0.67 % (213481)------------------------------
% 2.32/0.67 % (213481)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.32/0.67 % (213481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.32/0.67 % (213481)CaDiCaL version: 2.1.3
% 2.32/0.67 % (213481)Termination reason: Instruction limit
% 2.32/0.67 % (213481)Termination phase: Saturation
% 2.32/0.67 % (213481)Time elapsed: 0.003 s
% 2.32/0.67 % (213481)Peak memory usage: 11 MB
% 2.32/0.67 % (213481)Instructions burned: 7 (million)
% 2.32/0.67 % (213454)Instruction limit reached!
% 2.32/0.67 % (213454)------------------------------
% 2.32/0.67 % (213454)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.32/0.67 % (213454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.32/0.67 % (213454)CaDiCaL version: 2.1.3
% 2.32/0.67 % (213454)Termination reason: Instruction limit
% 2.32/0.67 % (213454)Termination phase: Saturation
% 2.32/0.67 % (213454)Time elapsed: 0.129 s
% 2.32/0.67 % (213454)Peak memory usage: 14 MB
% 2.32/0.67 % (213454)Instructions burned: 249 (million)
% 2.32/0.67 % (213476)Instruction limit reached!
% 2.32/0.67 % (213476)------------------------------
% 2.32/0.67 % (213476)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.32/0.67 % (213476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.32/0.67 % (213476)CaDiCaL version: 2.1.3
% 2.32/0.67 % (213476)Termination reason: Instruction limit
% 2.32/0.67 % (213476)Termination phase: Saturation
% 2.32/0.67 % (213476)Time elapsed: 0.006 s
% 2.32/0.67 % (213476)Peak memory usage: 11 MB
% 2.32/0.67 % (213476)Instructions burned: 9 (million)
% 2.32/0.67 % (213482)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=2956295315:i=23:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/23Mi)
% 2.32/0.67 % (213472)Instruction limit reached!
% 2.32/0.67 % (213472)------------------------------
% 2.77/0.78 % (213472)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.77/0.78 % (213472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.77/0.78 % (213472)CaDiCaL version: 2.1.3
% 2.77/0.78 % (213472)Termination reason: Instruction limit
% 2.77/0.78 % (213472)Termination phase: Saturation
% 2.77/0.78 % (213472)Time elapsed: 0.053 s
% 2.77/0.78 % (213472)Peak memory usage: 13 MB
% 2.77/0.78 % (213472)Instructions burned: 60 (million)
% 2.77/0.78 % (213485)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=433040669:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2997 on theBenchmark for (2997ds/20Mi)
% 2.77/0.78 % (213482)Instruction limit reached!
% 2.77/0.78 % (213482)------------------------------
% 2.77/0.78 % (213482)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.77/0.78 % (213482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.77/0.78 % (213482)CaDiCaL version: 2.1.3
% 2.77/0.78 % (213482)Termination reason: Instruction limit
% 2.77/0.78 % (213482)Termination phase: Saturation
% 2.77/0.78 % (213482)Time elapsed: 0.010 s
% 2.77/0.78 % (213482)Peak memory usage: 11 MB
% 2.77/0.78 % (213482)Instructions burned: 24 (million)
% 2.77/0.78 % (213487)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=2144646055:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2997 on theBenchmark for (2997ds/143Mi)
% 2.77/0.78 % (213486)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=4138761953:i=1240:rtra=on:ixr=off_2997 on theBenchmark for (2997ds/1240Mi)
% 2.77/0.78 % (213485)Instruction limit reached!
% 2.77/0.78 % (213485)------------------------------
% 2.77/0.78 % (213485)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.77/0.78 % (213485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.77/0.78 % (213485)CaDiCaL version: 2.1.3
% 2.77/0.78 % (213485)Termination reason: Instruction limit
% 2.77/0.78 % (213485)Termination phase: Saturation
% 2.77/0.78 % (213485)Time elapsed: 0.010 s
% 2.77/0.78 % (213485)Peak memory usage: 12 MB
% 2.77/0.78 % (213485)Instructions burned: 20 (million)
% 2.77/0.78 % (213491)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=715271798:i=42:hud=10:rtra=on_2997 on theBenchmark for (2997ds/42Mi)
% 2.77/0.78 % (213494)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 2.77/0.78 % (213489)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=1850489902:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/193Mi)
% 2.77/0.78 % (213494)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1057252734:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2997 on theBenchmark for (2997ds/7Mi)
% 2.77/0.78 % (213494)Instruction limit reached!
% 2.77/0.78 % (213494)------------------------------
% 2.77/0.78 % (213494)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.77/0.78 % (213494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.77/0.78 % (213494)CaDiCaL version: 2.1.3
% 2.77/0.78 % (213494)Termination reason: Instruction limit
% 2.77/0.78 % (213494)Termination phase: Saturation
% 2.77/0.78 % (213494)Time elapsed: 0.004 s
% 2.77/0.78 % (213494)Peak memory usage: 11 MB
% 2.77/0.78 % (213494)Instructions burned: 8 (million)
% 2.77/0.78 % (213491)Instruction limit reached!
% 2.77/0.78 % (213491)------------------------------
% 2.77/0.78 % (213491)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.77/0.78 % (213491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.77/0.78 % (213491)CaDiCaL version: 2.1.3
% 2.77/0.78 % (213491)Termination reason: Instruction limit
% 2.77/0.78 % (213491)Termination phase: Saturation
% 2.77/0.78 % (213491)Time elapsed: 0.020 s
% 2.77/0.78 % (213491)Peak memory usage: 12 MB
% 2.77/0.78 % (213491)Instructions burned: 42 (million)
% 2.77/0.78 % (213498)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=1868969495:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/181Mi)
% 2.77/0.78 % (213499)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=580704823:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2996 on theBenchmark for (2996ds/169Mi)
% 3.13/0.88 % (213487)Instruction limit reached!
% 3.13/0.88 % (213487)------------------------------
% 3.13/0.88 % (213487)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.13/0.88 % (213487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.13/0.88 % (213487)CaDiCaL version: 2.1.3
% 3.13/0.88 % (213487)Termination reason: Instruction limit
% 3.13/0.88 % (213487)Termination phase: Saturation
% 3.13/0.88 % (213487)Time elapsed: 0.067 s
% 3.13/0.88 % (213487)Peak memory usage: 13 MB
% 3.13/0.88 % (213487)Instructions burned: 145 (million)
% 3.13/0.88 % (213502)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 3.13/0.88 % (213502)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=3508879250:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2996 on theBenchmark for (2996ds/6Mi)
% 3.13/0.88 % (213502)Instruction limit reached!
% 3.13/0.88 % (213502)------------------------------
% 3.13/0.88 % (213502)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.13/0.88 % (213502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.13/0.88 % (213502)CaDiCaL version: 2.1.3
% 3.13/0.88 % (213502)Termination reason: Instruction limit
% 3.13/0.88 % (213502)Termination phase: Saturation
% 3.13/0.88 % (213502)Time elapsed: 0.003 s
% 3.13/0.88 % (213502)Peak memory usage: 11 MB
% 3.13/0.88 % (213502)Instructions burned: 6 (million)
% 3.13/0.88 % (213462)Instruction limit reached!
% 3.13/0.88 % (213462)------------------------------
% 3.13/0.88 % (213462)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.13/0.88 % (213462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.13/0.88 % (213462)CaDiCaL version: 2.1.3
% 3.13/0.88 % (213462)Termination reason: Instruction limit
% 3.13/0.88 % (213462)Termination phase: Saturation
% 3.13/0.88 % (213462)Time elapsed: 0.201 s
% 3.13/0.88 % (213462)Peak memory usage: 13 MB
% 3.13/0.88 % (213462)Instructions burned: 329 (million)
% 3.13/0.88 % (213504)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=789016097:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2996 on theBenchmark for (2996ds/22Mi)
% 3.13/0.88 % (213505)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=681019584:i=19:add=on:rtra=on_2996 on theBenchmark for (2996ds/19Mi)
% 3.13/0.88 % (213504)Instruction limit reached!
% 3.13/0.88 % (213504)------------------------------
% 3.13/0.88 % (213504)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.13/0.88 % (213504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.13/0.88 % (213504)CaDiCaL version: 2.1.3
% 3.13/0.88 % (213504)Termination reason: Instruction limit
% 3.13/0.88 % (213504)Termination phase: Saturation
% 3.13/0.88 % (213504)Time elapsed: 0.011 s
% 3.13/0.88 % (213504)Peak memory usage: 12 MB
% 3.13/0.88 % (213504)Instructions burned: 22 (million)
% 3.13/0.88 % (213505)Instruction limit reached!
% 3.13/0.88 % (213505)------------------------------
% 3.13/0.88 % (213505)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.13/0.88 % (213505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.13/0.88 % (213505)CaDiCaL version: 2.1.3
% 3.13/0.88 % (213505)Termination reason: Instruction limit
% 3.13/0.88 % (213505)Termination phase: Saturation
% 3.13/0.88 % (213505)Time elapsed: 0.010 s
% 3.13/0.88 % (213505)Peak memory usage: 12 MB
% 3.13/0.88 % (213505)Instructions burned: 20 (million)
% 3.13/0.88 % (213498)Instruction limit reached!
% 3.13/0.88 % (213498)------------------------------
% 3.13/0.88 % (213498)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.13/0.88 % (213498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.13/0.88 % (213498)CaDiCaL version: 2.1.3
% 3.13/0.88 % (213498)Termination reason: Instruction limit
% 3.13/0.88 % (213498)Termination phase: Saturation
% 3.13/0.88 % (213498)Time elapsed: 0.089 s
% 3.13/0.88 % (213498)Peak memory usage: 14 MB
% 3.13/0.88 % (213498)Instructions burned: 183 (million)
% 3.13/0.88 % (213508)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=3617581009:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/316Mi)
% 3.13/0.88 % (213509)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=2481186373:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2996 on theBenchmark for (2996ds/853Mi)
% 3.73/0.99 % (213499)Instruction limit reached!
% 3.73/0.99 % (213499)------------------------------
% 3.73/0.99 % (213499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.73/0.99 % (213499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.73/0.99 % (213499)CaDiCaL version: 2.1.3
% 3.73/0.99 % (213499)Termination reason: Instruction limit
% 3.73/0.99 % (213499)Termination phase: Saturation
% 3.73/0.99 % (213499)Time elapsed: 0.090 s
% 3.73/0.99 % (213499)Peak memory usage: 13 MB
% 3.73/0.99 % (213499)Instructions burned: 170 (million)
% 3.73/0.99 % (213510)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=1170032132:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2995 on theBenchmark for (2995ds/45Mi)
% 3.73/0.99 % (213513)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=1630048280:i=480:rtra=on_2995 on theBenchmark for (2995ds/480Mi)
% 3.73/0.99 % (213510)Instruction limit reached!
% 3.73/0.99 % (213510)------------------------------
% 3.73/0.99 % (213510)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.73/0.99 % (213510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.73/0.99 % (213510)CaDiCaL version: 2.1.3
% 3.73/0.99 % (213510)Termination reason: Instruction limit
% 3.73/0.99 % (213510)Termination phase: Saturation
% 3.73/0.99 % (213510)Time elapsed: 0.024 s
% 3.73/0.99 % (213510)Peak memory usage: 12 MB
% 3.73/0.99 % (213510)Instructions burned: 46 (million)
% 3.73/0.99 % (213489)Instruction limit reached!
% 3.73/0.99 % (213489)------------------------------
% 3.73/0.99 % (213489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.73/0.99 % (213489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.73/0.99 % (213489)CaDiCaL version: 2.1.3
% 3.73/0.99 % (213489)Termination reason: Instruction limit
% 3.73/0.99 % (213489)Termination phase: Saturation
% 3.73/0.99 % (213489)Time elapsed: 0.173 s
% 3.73/0.99 % (213489)Peak memory usage: 14 MB
% 3.73/0.99 % (213489)Instructions burned: 194 (million)
% 3.73/0.99 % (213516)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=3490246358:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2995 on theBenchmark for (2995ds/21Mi)
% 3.73/0.99 % (213516)Instruction limit reached!
% 3.73/0.99 % (213516)------------------------------
% 3.73/0.99 % (213516)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.73/0.99 % (213516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.73/0.99 % (213516)CaDiCaL version: 2.1.3
% 3.73/0.99 % (213516)Termination reason: Instruction limit
% 3.73/0.99 % (213516)Termination phase: Saturation
% 3.73/0.99 % (213516)Time elapsed: 0.017 s
% 3.73/0.99 % (213516)Peak memory usage: 12 MB
% 3.73/0.99 % (213516)Instructions burned: 22 (million)
% 3.73/0.99 % (213517)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 3.73/0.99 % (213517)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=2177841647:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/200Mi)
% 3.73/0.99 % (213519)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=2004454265:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2995 on theBenchmark for (2995ds/13Mi)
% 3.73/0.99 % (213519)Instruction limit reached!
% 3.73/0.99 % (213519)------------------------------
% 3.73/0.99 % (213519)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.73/0.99 % (213519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.73/0.99 % (213519)CaDiCaL version: 2.1.3
% 3.73/0.99 % (213519)Termination reason: Instruction limit
% 3.73/0.99 % (213519)Termination phase: Saturation
% 3.73/0.99 % (213519)Time elapsed: 0.007 s
% 3.73/0.99 % (213519)Peak memory usage: 12 MB
% 3.73/0.99 % (213519)Instructions burned: 13 (million)
% 3.73/0.99 % (213429)Instruction limit reached!
% 3.73/0.99 % (213429)------------------------------
% 3.73/0.99 % (213429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.73/0.99 % (213429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.71/1.16 % (213429)CaDiCaL version: 2.1.3
% 5.71/1.16 % (213429)Termination reason: Instruction limit
% 5.71/1.16 % (213429)Termination phase: Saturation
% 5.71/1.16 % (213429)Time elapsed: 0.497 s
% 5.71/1.16 % (213429)Peak memory usage: 16 MB
% 5.71/1.16 % (213429)Instructions burned: 634 (million)
% 5.71/1.16 % (213522)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=2717941713:i=66:s2at=3:nm=2:rtra=on:rawr=on_2994 on theBenchmark for (2994ds/66Mi)
% 5.71/1.16 % (213524)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=3104896391:i=51:fsr=off:rtra=on_2994 on theBenchmark for (2994ds/51Mi)
% 5.71/1.16 % (213508)Instruction limit reached!
% 5.71/1.16 % (213508)------------------------------
% 5.71/1.16 % (213508)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.71/1.16 % (213508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.71/1.16 % (213508)CaDiCaL version: 2.1.3
% 5.71/1.16 % (213508)Termination reason: Instruction limit
% 5.71/1.16 % (213508)Termination phase: Saturation
% 5.71/1.16 % (213508)Time elapsed: 0.161 s
% 5.71/1.16 % (213508)Peak memory usage: 14 MB
% 5.71/1.16 % (213508)Instructions burned: 318 (million)
% 5.71/1.16 % (213522)Instruction limit reached!
% 5.71/1.16 % (213522)------------------------------
% 5.71/1.16 % (213522)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.71/1.16 % (213522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.71/1.16 % (213522)CaDiCaL version: 2.1.3
% 5.71/1.16 % (213522)Termination reason: Instruction limit
% 5.71/1.16 % (213522)Termination phase: Saturation
% 5.71/1.16 % (213522)Time elapsed: 0.037 s
% 5.71/1.16 % (213522)Peak memory usage: 13 MB
% 5.71/1.16 % (213522)Instructions burned: 68 (million)
% 5.71/1.16 % (213524)Instruction limit reached!
% 5.71/1.16 % (213524)------------------------------
% 5.71/1.16 % (213524)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.71/1.16 % (213524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.71/1.16 % (213524)CaDiCaL version: 2.1.3
% 5.71/1.16 % (213524)Termination reason: Instruction limit
% 5.71/1.16 % (213524)Termination phase: Saturation
% 5.71/1.16 % (213524)Time elapsed: 0.027 s
% 5.71/1.16 % (213524)Peak memory usage: 12 MB
% 5.71/1.16 % (213524)Instructions burned: 51 (million)
% 5.71/1.16 % (213526)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=2932090674:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/31Mi)
% 5.71/1.16 % (213527)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=1522560144:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2994 on theBenchmark for (2994ds/137Mi)
% 5.71/1.16 % (213528)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=3897904518:cond=on:i=34:hud=10:nm=10:rtra=on_2994 on theBenchmark for (2994ds/34Mi)
% 5.71/1.16 % (213526)Instruction limit reached!
% 5.71/1.16 % (213526)------------------------------
% 5.71/1.16 % (213526)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.71/1.16 % (213526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.71/1.16 % (213526)CaDiCaL version: 2.1.3
% 5.71/1.16 % (213526)Termination reason: Instruction limit
% 5.71/1.16 % (213526)Termination phase: Saturation
% 5.71/1.16 % (213526)Time elapsed: 0.014 s
% 5.71/1.16 % (213526)Peak memory usage: 12 MB
% 5.71/1.16 % (213526)Instructions burned: 32 (million)
% 5.71/1.16 % (213528)Instruction limit reached!
% 5.71/1.16 % (213528)------------------------------
% 5.71/1.16 % (213528)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.71/1.16 % (213528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.71/1.16 % (213528)CaDiCaL version: 2.1.3
% 5.71/1.16 % (213528)Termination reason: Instruction limit
% 5.71/1.16 % (213528)Termination phase: Saturation
% 5.71/1.16 % (213528)Time elapsed: 0.017 s
% 5.71/1.16 % (213528)Peak memory usage: 12 MB
% 5.71/1.16 % (213528)Instructions burned: 35 (million)
% 5.71/1.16 % (213517)Instruction limit reached!
% 5.71/1.16 % (213517)------------------------------
% 5.71/1.16 % (213517)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.71/1.16 % (213517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.38/1.34 % (213517)CaDiCaL version: 2.1.3
% 6.38/1.34 % (213517)Termination reason: Instruction limit
% 6.38/1.34 % (213517)Termination phase: Saturation
% 6.38/1.34 % (213517)Time elapsed: 0.129 s
% 6.38/1.34 % (213517)Peak memory usage: 13 MB
% 6.38/1.34 % (213517)Instructions burned: 201 (million)
% 6.38/1.34 % (213532)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=1080734915:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2993 on theBenchmark for (2993ds/67Mi)
% 6.38/1.34 % (213533)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 6.38/1.34 % (213533)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=1019237860:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2993 on theBenchmark for (2993ds/180Mi)
% 6.38/1.34 % (213534)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=183881041:st=2:i=246:sd=3:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/246Mi)
% 6.38/1.34 % (213532)Instruction limit reached!
% 6.38/1.34 % (213532)------------------------------
% 6.38/1.34 % (213532)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.38/1.34 % (213532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.38/1.34 % (213532)CaDiCaL version: 2.1.3
% 6.38/1.34 % (213532)Termination reason: Instruction limit
% 6.38/1.34 % (213532)Termination phase: Saturation
% 6.38/1.34 % (213532)Time elapsed: 0.034 s
% 6.38/1.34 % (213532)Peak memory usage: 13 MB
% 6.38/1.34 % (213532)Instructions burned: 69 (million)
% 6.38/1.34 % (213513)Instruction limit reached!
% 6.38/1.34 % (213513)------------------------------
% 6.38/1.34 % (213513)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.38/1.34 % (213513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.38/1.34 % (213513)CaDiCaL version: 2.1.3
% 6.38/1.34 % (213513)Termination reason: Instruction limit
% 6.38/1.34 % (213513)Termination phase: Saturation
% 6.38/1.34 % (213513)Time elapsed: 0.246 s
% 6.38/1.34 % (213513)Peak memory usage: 15 MB
% 6.38/1.34 % (213513)Instructions burned: 481 (million)
% 6.38/1.34 % (213538)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=765007346:cond=on:i=96:bd=all:rtra=on_2993 on theBenchmark for (2993ds/96Mi)
% 6.38/1.34 % (213527)Instruction limit reached!
% 6.38/1.34 % (213527)------------------------------
% 6.38/1.34 % (213527)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.38/1.34 % (213527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.38/1.34 % (213527)CaDiCaL version: 2.1.3
% 6.38/1.34 % (213527)Termination reason: Instruction limit
% 6.38/1.34 % (213527)Termination phase: Saturation
% 6.38/1.34 % (213527)Time elapsed: 0.091 s
% 6.38/1.34 % (213527)Peak memory usage: 12 MB
% 6.38/1.34 % (213527)Instructions burned: 137 (million)
% 6.38/1.34 % (213539)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=3947138142:i=427:sd=1:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/427Mi)
% 6.38/1.34 % (213541)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=1420026838:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/874Mi)
% 6.38/1.34 % (213486)Instruction limit reached!
% 6.38/1.34 % (213486)------------------------------
% 6.38/1.34 % (213486)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.38/1.34 % (213486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.38/1.34 % (213486)CaDiCaL version: 2.1.3
% 6.38/1.34 % (213486)Termination reason: Instruction limit
% 6.38/1.34 % (213486)Termination phase: Saturation
% 6.38/1.34 % (213486)Time elapsed: 0.447 s
% 6.38/1.34 % (213486)Peak memory usage: 15 MB
% 6.38/1.34 % (213486)Instructions burned: 1240 (million)
% 6.38/1.34 % (213533)Instruction limit reached!
% 6.38/1.34 % (213533)------------------------------
% 6.38/1.34 % (213533)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.38/1.34 % (213533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.38/1.34 % (213533)CaDiCaL version: 2.1.3
% 6.38/1.34 % (213533)Termination reason: Instruction limit
% 6.38/1.34 % (213533)Termination phase: Saturation
% 6.38/1.34 % (213533)Time elapsed: 0.075 s
% 6.38/1.34 % (213533)Peak memory usage: 13 MB
% 6.38/1.34 % (213533)Instructions burned: 180 (million)
% 6.38/1.34 % (213538)Instruction limit reached!
% 6.38/1.34 % (213538)------------------------------
% 6.38/1.34 % (213538)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.38/1.34 % (213538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.94/1.46 % (213538)CaDiCaL version: 2.1.3
% 6.94/1.46 % (213538)Termination reason: Instruction limit
% 6.94/1.46 % (213538)Termination phase: Saturation
% 6.94/1.46 % (213538)Time elapsed: 0.053 s
% 6.94/1.46 % (213538)Peak memory usage: 13 MB
% 6.94/1.46 % (213538)Instructions burned: 97 (million)
% 6.94/1.46 % (213544)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=490173384:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/515Mi)
% 6.94/1.46 % (213545)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=2325780084:st=1.5:i=130:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/130Mi)
% 6.94/1.46 % (213546)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=2097097138:i=44:ep=R:rtra=on:ntd=on_2992 on theBenchmark for (2992ds/44Mi)
% 6.94/1.46 % (213546)Instruction limit reached!
% 6.94/1.46 % (213546)------------------------------
% 6.94/1.46 % (213546)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.94/1.46 % (213546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.94/1.46 % (213546)CaDiCaL version: 2.1.3
% 6.94/1.46 % (213546)Termination reason: Instruction limit
% 6.94/1.46 % (213546)Termination phase: Saturation
% 6.94/1.46 % (213546)Time elapsed: 0.022 s
% 6.94/1.46 % (213546)Peak memory usage: 12 MB
% 6.94/1.46 % (213546)Instructions burned: 44 (million)
% 6.94/1.46 % (213550)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=270955286:s2a=on:i=571:nm=16:rtra=on_2992 on theBenchmark for (2992ds/571Mi)
% 6.94/1.46 % (213509)Instruction limit reached!
% 6.94/1.46 % (213509)------------------------------
% 6.94/1.46 % (213509)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.94/1.46 % (213509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.94/1.46 % (213509)CaDiCaL version: 2.1.3
% 6.94/1.46 % (213509)Termination reason: Instruction limit
% 6.94/1.46 % (213509)Termination phase: Saturation
% 6.94/1.46 % (213509)Time elapsed: 0.388 s
% 6.94/1.46 % (213509)Peak memory usage: 17 MB
% 6.94/1.46 % (213509)Instructions burned: 854 (million)
% 6.94/1.46 % (213545)Instruction limit reached!
% 6.94/1.46 % (213545)------------------------------
% 6.94/1.46 % (213545)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.94/1.46 % (213545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.94/1.46 % (213545)CaDiCaL version: 2.1.3
% 6.94/1.46 % (213545)Termination reason: Instruction limit
% 6.94/1.46 % (213545)Termination phase: Saturation
% 6.94/1.46 % (213545)Time elapsed: 0.051 s
% 6.94/1.46 % (213545)Peak memory usage: 12 MB
% 6.94/1.46 % (213545)Instructions burned: 130 (million)
% 6.94/1.46 % (213552)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=1249289510:i=450:rtra=on:ixr=off:ntd=on_2992 on theBenchmark for (2992ds/450Mi)
% 6.94/1.46 % (213553)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=4030894588:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2992 on theBenchmark for (2992ds/95Mi)
% 6.94/1.46 % (213534)Instruction limit reached!
% 6.94/1.46 % (213534)------------------------------
% 6.94/1.46 % (213534)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.94/1.46 % (213534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.94/1.46 % (213534)CaDiCaL version: 2.1.3
% 6.94/1.46 % (213534)Termination reason: Instruction limit
% 6.94/1.46 % (213534)Termination phase: Saturation
% 6.94/1.46 % (213534)Time elapsed: 0.215 s
% 6.94/1.46 % (213534)Peak memory usage: 14 MB
% 6.94/1.46 % (213534)Instructions burned: 246 (million)
% 6.94/1.46 % (213553)Instruction limit reached!
% 6.94/1.46 % (213553)------------------------------
% 6.94/1.46 % (213553)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.94/1.46 % (213553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.94/1.46 % (213553)CaDiCaL version: 2.1.3
% 6.94/1.46 % (213553)Termination reason: Instruction limit
% 6.94/1.46 % (213553)Termination phase: Saturation
% 6.94/1.46 % (213553)Time elapsed: 0.068 s
% 6.94/1.46 % (213553)Peak memory usage: 13 MB
% 6.94/1.46 % (213553)Instructions burned: 95 (million)
% 6.94/1.46 % (213556)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=1634201911:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2991 on theBenchmark for (2991ds/65Mi)
% 8.44/1.61 % (213558)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=2092044421: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_2991 on theBenchmark for (2991ds/105Mi)
% 8.44/1.61 % (213539)Instruction limit reached!
% 8.44/1.61 % (213539)------------------------------
% 8.44/1.61 % (213539)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.44/1.61 % (213539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.44/1.61 % (213539)CaDiCaL version: 2.1.3
% 8.44/1.61 % (213539)Termination reason: Instruction limit
% 8.44/1.61 % (213539)Termination phase: Saturation
% 8.44/1.61 % (213539)Time elapsed: 0.230 s
% 8.44/1.61 % (213539)Peak memory usage: 14 MB
% 8.44/1.61 % (213539)Instructions burned: 428 (million)
% 8.44/1.61 % (213556)Instruction limit reached!
% 8.44/1.61 % (213556)------------------------------
% 8.44/1.61 % (213556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.44/1.61 % (213556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.44/1.61 % (213556)CaDiCaL version: 2.1.3
% 8.44/1.61 % (213556)Termination reason: Instruction limit
% 8.44/1.61 % (213556)Termination phase: Saturation
% 8.44/1.61 % (213556)Time elapsed: 0.056 s
% 8.44/1.61 % (213556)Peak memory usage: 13 MB
% 8.44/1.61 % (213556)Instructions burned: 67 (million)
% 8.44/1.61 % (213562)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=874783656:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2990 on theBenchmark for (2990ds/5755Mi)
% 8.44/1.61 % (213558)Instruction limit reached!
% 8.44/1.61 % (213558)------------------------------
% 8.44/1.61 % (213558)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.44/1.61 % (213558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.44/1.61 % (213558)CaDiCaL version: 2.1.3
% 8.44/1.61 % (213558)Termination reason: Instruction limit
% 8.44/1.61 % (213558)Termination phase: Saturation
% 8.44/1.61 % (213558)Time elapsed: 0.055 s
% 8.44/1.61 % (213558)Peak memory usage: 13 MB
% 8.44/1.61 % (213558)Instructions burned: 106 (million)
% 8.44/1.61 % (213563)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=3334914344:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2990 on theBenchmark for (2990ds/375Mi)
% 8.44/1.61 % (213565)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=3689610344:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2990 on theBenchmark for (2990ds/495Mi)
% 8.44/1.61 % (213544)Instruction limit reached!
% 8.44/1.61 % (213544)------------------------------
% 8.44/1.61 % (213544)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.44/1.61 % (213544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.44/1.61 % (213544)CaDiCaL version: 2.1.3
% 8.44/1.61 % (213544)Termination reason: Instruction limit
% 8.44/1.61 % (213544)Termination phase: Saturation
% 8.44/1.61 % (213544)Time elapsed: 0.258 s
% 8.44/1.61 % (213544)Peak memory usage: 15 MB
% 8.44/1.61 % (213544)Instructions burned: 515 (million)
% 8.44/1.61 % (213568)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=3265257586:cond=on:i=34:hud=10:nm=10:rtra=on_2990 on theBenchmark for (2990ds/34Mi)
% 8.44/1.61 % (213568)Instruction limit reached!
% 8.44/1.61 % (213568)------------------------------
% 8.44/1.61 % (213568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.44/1.61 % (213568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.44/1.61 % (213568)CaDiCaL version: 2.1.3
% 8.44/1.61 % (213568)Termination reason: Instruction limit
% 8.44/1.61 % (213568)Termination phase: Saturation
% 8.44/1.61 % (213568)Time elapsed: 0.017 s
% 8.44/1.61 % (213568)Peak memory usage: 12 MB
% 8.44/1.61 % (213568)Instructions burned: 34 (million)
% 8.44/1.61 % (213570)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=2329811046:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2989 on theBenchmark for (2989ds/91Mi)
% 8.44/1.61 % (213550)Instruction limit reached!
% 8.44/1.61 % (213550)------------------------------
% 8.44/1.61 % (213550)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.91/1.82 % (213550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.91/1.82 % (213550)CaDiCaL version: 2.1.3
% 8.91/1.82 % (213550)Termination reason: Instruction limit
% 8.91/1.82 % (213550)Termination phase: Saturation
% 8.91/1.82 % (213550)Time elapsed: 0.290 s
% 8.91/1.82 % (213550)Peak memory usage: 18 MB
% 8.91/1.82 % (213550)Instructions burned: 572 (million)
% 8.91/1.82 % (213570)Instruction limit reached!
% 8.91/1.82 % (213570)------------------------------
% 8.91/1.82 % (213570)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.91/1.82 % (213570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.91/1.82 % (213570)CaDiCaL version: 2.1.3
% 8.91/1.82 % (213570)Termination reason: Instruction limit
% 8.91/1.82 % (213570)Termination phase: Saturation
% 8.91/1.82 % (213570)Time elapsed: 0.044 s
% 8.91/1.82 % (213570)Peak memory usage: 13 MB
% 8.91/1.82 % (213570)Instructions burned: 93 (million)
% 8.91/1.82 % (213572)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=2097478768:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2989 on theBenchmark for (2989ds/66Mi)
% 8.91/1.82 % (213573)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=1962639590:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2989 on theBenchmark for (2989ds/22Mi)
% 8.91/1.82 % (213573)Instruction limit reached!
% 8.91/1.82 % (213573)------------------------------
% 8.91/1.82 % (213573)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.91/1.82 % (213573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.91/1.82 % (213573)CaDiCaL version: 2.1.3
% 8.91/1.82 % (213573)Termination reason: Instruction limit
% 8.91/1.82 % (213573)Termination phase: Saturation
% 8.91/1.82 % (213573)Time elapsed: 0.011 s
% 8.91/1.82 % (213573)Peak memory usage: 12 MB
% 8.91/1.82 % (213573)Instructions burned: 22 (million)
% 8.91/1.82 % (213572)Instruction limit reached!
% 8.91/1.82 % (213572)------------------------------
% 8.91/1.82 % (213572)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.91/1.82 % (213572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.91/1.82 % (213572)CaDiCaL version: 2.1.3
% 8.91/1.82 % (213572)Termination reason: Instruction limit
% 8.91/1.82 % (213572)Termination phase: Saturation
% 8.91/1.82 % (213572)Time elapsed: 0.035 s
% 8.91/1.82 % (213572)Peak memory usage: 12 MB
% 8.91/1.82 % (213572)Instructions burned: 68 (million)
% 8.91/1.82 % (213576)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=2817512965:i=338:bd=all:ins=4:rtra=on_2988 on theBenchmark for (2988ds/338Mi)
% 8.91/1.82 % (213577)lrs+10_1_sil=128000:si=on:urr=on:random_seed=168388021:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2988 on theBenchmark for (2988ds/28Mi)
% 8.91/1.82 % (213552)Instruction limit reached!
% 8.91/1.82 % (213552)------------------------------
% 8.91/1.82 % (213552)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.91/1.82 % (213552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.91/1.82 % (213552)CaDiCaL version: 2.1.3
% 8.91/1.82 % (213552)Termination reason: Instruction limit
% 8.91/1.82 % (213552)Termination phase: Saturation
% 8.91/1.82 % (213552)Time elapsed: 0.354 s
% 8.91/1.82 % (213552)Peak memory usage: 14 MB
% 8.91/1.82 % (213552)Instructions burned: 450 (million)
% 8.91/1.82 % (213577)Instruction limit reached!
% 8.91/1.82 % (213577)------------------------------
% 8.91/1.82 % (213577)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.91/1.82 % (213577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.91/1.82 % (213577)CaDiCaL version: 2.1.3
% 8.91/1.82 % (213577)Termination reason: Instruction limit
% 8.91/1.82 % (213577)Termination phase: Saturation
% 8.91/1.82 % (213577)Time elapsed: 0.018 s
% 8.91/1.82 % (213577)Peak memory usage: 12 MB
% 8.91/1.82 % (213577)Instructions burned: 28 (million)
% 8.91/1.82 % (213581)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=1716331093:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2988 on theBenchmark for (2988ds/340Mi)
% 8.91/1.82 % (213580)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 8.91/1.82 % (213580)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=3627049938:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2988 on theBenchmark for (2988ds/137Mi)
% 9.91/1.99 % (213541)Instruction limit reached!
% 9.91/1.99 % (213541)------------------------------
% 9.91/1.99 % (213541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.91/1.99 % (213541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.91/1.99 % (213541)CaDiCaL version: 2.1.3
% 9.91/1.99 % (213541)Termination reason: Instruction limit
% 9.91/1.99 % (213541)Termination phase: Saturation
% 9.91/1.99 % (213541)Time elapsed: 0.506 s
% 9.91/1.99 % (213541)Peak memory usage: 15 MB
% 9.91/1.99 % (213541)Instructions burned: 874 (million)
% 9.91/1.99 % (213565)Instruction limit reached!
% 9.91/1.99 % (213565)------------------------------
% 9.91/1.99 % (213565)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.91/1.99 % (213565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.91/1.99 % (213565)CaDiCaL version: 2.1.3
% 9.91/1.99 % (213565)Termination reason: Instruction limit
% 9.91/1.99 % (213565)Termination phase: Saturation
% 9.91/1.99 % (213565)Time elapsed: 0.230 s
% 9.91/1.99 % (213565)Peak memory usage: 14 MB
% 9.91/1.99 % (213565)Instructions burned: 495 (million)
% 9.91/1.99 % (213584)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=3998567554:i=227:sd=1:bd=all:rtra=on:ss=axioms_2987 on theBenchmark for (2987ds/227Mi)
% 9.91/1.99 % (213585)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 9.91/1.99 % (213585)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=1878939492:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2987 on theBenchmark for (2987ds/373Mi)
% 9.91/1.99 % (213563)Instruction limit reached!
% 9.91/1.99 % (213563)------------------------------
% 9.91/1.99 % (213563)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.91/1.99 % (213563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.91/1.99 % (213563)CaDiCaL version: 2.1.3
% 9.91/1.99 % (213563)Termination reason: Instruction limit
% 9.91/1.99 % (213563)Termination phase: Saturation
% 9.91/1.99 % (213563)Time elapsed: 0.269 s
% 9.91/1.99 % (213563)Peak memory usage: 15 MB
% 9.91/1.99 % (213563)Instructions burned: 375 (million)
% 9.91/1.99 % (213588)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=2321251658:i=116:ep=RSTC:rtra=on:ntd=on_2987 on theBenchmark for (2987ds/116Mi)
% 9.91/1.99 % (213576)Instruction limit reached!
% 9.91/1.99 % (213576)------------------------------
% 9.91/1.99 % (213576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.91/1.99 % (213576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.91/1.99 % (213576)CaDiCaL version: 2.1.3
% 9.91/1.99 % (213576)Termination reason: Instruction limit
% 9.91/1.99 % (213576)Termination phase: Saturation
% 9.91/1.99 % (213576)Time elapsed: 0.163 s
% 9.91/1.99 % (213576)Peak memory usage: 14 MB
% 9.91/1.99 % (213576)Instructions burned: 338 (million)
% 9.91/1.99 % (213580)Instruction limit reached!
% 9.91/1.99 % (213580)------------------------------
% 9.91/1.99 % (213580)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.91/1.99 % (213580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.91/1.99 % (213580)CaDiCaL version: 2.1.3
% 9.91/1.99 % (213580)Termination reason: Instruction limit
% 9.91/1.99 % (213580)Termination phase: Saturation
% 9.91/1.99 % (213580)Time elapsed: 0.116 s
% 9.91/1.99 % (213580)Peak memory usage: 12 MB
% 9.91/1.99 % (213580)Instructions burned: 138 (million)
% 9.91/1.99 % (213590)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=841129166:i=575:rtra=on_2986 on theBenchmark for (2986ds/575Mi)
% 9.91/1.99 % (213584)Instruction limit reached!
% 9.91/1.99 % (213584)------------------------------
% 9.91/1.99 % (213584)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.91/1.99 % (213584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.91/1.99 % (213584)CaDiCaL version: 2.1.3
% 9.91/1.99 % (213584)Termination reason: Instruction limit
% 9.91/1.99 % (213584)Termination phase: Saturation
% 9.91/1.99 % (213584)Time elapsed: 0.113 s
% 9.91/1.99 % (213584)Peak memory usage: 13 MB
% 9.91/1.99 % (213584)Instructions burned: 228 (million)
% 9.91/1.99 % (213591)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=2285838219:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2986 on theBenchmark for (2986ds/270Mi)
% 13.51/2.36 % (213588)Instruction limit reached!
% 13.51/2.36 % (213588)------------------------------
% 13.51/2.36 % (213588)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.51/2.36 % (213588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.51/2.36 % (213588)CaDiCaL version: 2.1.3
% 13.51/2.36 % (213588)Termination reason: Instruction limit
% 13.51/2.36 % (213588)Termination phase: Saturation
% 13.51/2.36 % (213588)Time elapsed: 0.064 s
% 13.51/2.36 % (213588)Peak memory usage: 13 MB
% 13.51/2.36 % (213588)Instructions burned: 117 (million)
% 13.51/2.36 % (213581)Instruction limit reached!
% 13.51/2.36 % (213581)------------------------------
% 13.51/2.36 % (213581)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.51/2.36 % (213581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.51/2.36 % (213581)CaDiCaL version: 2.1.3
% 13.51/2.36 % (213581)Termination reason: Instruction limit
% 13.51/2.36 % (213581)Termination phase: Saturation
% 13.51/2.36 % (213581)Time elapsed: 0.159 s
% 13.51/2.36 % (213581)Peak memory usage: 14 MB
% 13.51/2.36 % (213581)Instructions burned: 340 (million)
% 13.51/2.36 % (213593)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=1654699976: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_2986 on theBenchmark for (2986ds/9840Mi)
% 13.51/2.36 % (213596)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.51/2.36 % (213596)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=3662818176:avsq=on:i=270:s2at=3:avsqr=1,16:rtra=on:ntd=on_2986 on theBenchmark for (2986ds/270Mi)
% 13.51/2.36 % (213595)lrs+1010_1_sil=128000:si=on:sos=all:uwa=off:nwc=1:random_seed=973002:i=421:rtra=on:ss=axioms_2986 on theBenchmark for (2986ds/421Mi)
% 13.51/2.36 % (213585)Instruction limit reached!
% 13.51/2.36 % (213585)------------------------------
% 13.51/2.36 % (213585)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.51/2.36 % (213585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.51/2.36 % (213585)CaDiCaL version: 2.1.3
% 13.51/2.36 % (213585)Termination reason: Instruction limit
% 13.51/2.36 % (213585)Termination phase: Saturation
% 13.51/2.36 % (213585)Time elapsed: 0.166 s
% 13.51/2.36 % (213585)Peak memory usage: 15 MB
% 13.51/2.36 % (213585)Instructions burned: 373 (million)
% 13.51/2.36 % (213600)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=4293102574:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2985 on theBenchmark for (2985ds/31Mi)
% 13.51/2.36 % (213600)Instruction limit reached!
% 13.51/2.36 % (213600)------------------------------
% 13.51/2.36 % (213600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.51/2.36 % (213600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.51/2.36 % (213600)CaDiCaL version: 2.1.3
% 13.51/2.36 % (213600)Termination reason: Instruction limit
% 13.51/2.36 % (213600)Termination phase: Saturation
% 13.51/2.36 % (213600)Time elapsed: 0.016 s
% 13.51/2.36 % (213600)Peak memory usage: 12 MB
% 13.51/2.36 % (213600)Instructions burned: 32 (million)
% 13.51/2.36 % (213602)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 13.51/2.36 % (213602)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
% 13.51/2.36 % (213602)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=3386798115:hsqr=1,8:i=1440:s2at=5:add=on:nm=2:rtra=on_2985 on theBenchmark for (2985ds/1440Mi)
% 13.51/2.36 % (213591)Instruction limit reached!
% 13.51/2.36 % (213591)------------------------------
% 13.51/2.36 % (213591)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.51/2.36 % (213591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.90/2.51 % (213591)CaDiCaL version: 2.1.3
% 14.90/2.51 % (213591)Termination reason: Instruction limit
% 14.90/2.51 % (213591)Termination phase: Saturation
% 14.90/2.51 % (213591)Time elapsed: 0.207 s
% 14.90/2.51 % (213591)Peak memory usage: 13 MB
% 14.90/2.51 % (213591)Instructions burned: 270 (million)
% 14.90/2.51 % (213596)Instruction limit reached!
% 14.90/2.51 % (213596)------------------------------
% 14.90/2.51 % (213596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.90/2.51 % (213596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.90/2.51 % (213596)CaDiCaL version: 2.1.3
% 14.90/2.51 % (213596)Termination reason: Instruction limit
% 14.90/2.51 % (213596)Termination phase: Saturation
% 14.90/2.51 % (213596)Time elapsed: 0.189 s
% 14.90/2.51 % (213596)Peak memory usage: 14 MB
% 14.90/2.51 % (213596)Instructions burned: 270 (million)
% 14.90/2.51 % (213604)dis+10_2_sil=128000:si=on:random_seed=3380213650:s2a=on:i=339:av=off:rtra=on:fe=abstraction:ss=axioms:fsd=on:ntd=on_2984 on theBenchmark for (2984ds/339Mi)
% 14.90/2.51 % (213605)lrs+2_16:1_si=on:cbe=off:uwa=interpreted_only:random_seed=1234438994:i=111:add=on:fgj=on:rtra=on:fdi=1024_2984 on theBenchmark for (2984ds/111Mi)
% 14.90/2.51 % (213590)Instruction limit reached!
% 14.90/2.51 % (213590)------------------------------
% 14.90/2.51 % (213590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.90/2.51 % (213590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.90/2.51 % (213590)CaDiCaL version: 2.1.3
% 14.90/2.51 % (213590)Termination reason: Instruction limit
% 14.90/2.51 % (213590)Termination phase: Saturation
% 14.90/2.51 % (213590)Time elapsed: 0.272 s
% 14.90/2.51 % (213590)Peak memory usage: 15 MB
% 14.90/2.51 % (213590)Instructions burned: 575 (million)
% 14.90/2.51 % (213608)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=3893318437:st=3:avsq=on:i=122:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2983 on theBenchmark for (2983ds/122Mi)
% 14.90/2.51 % (213595)Instruction limit reached!
% 14.90/2.51 % (213595)------------------------------
% 14.90/2.51 % (213595)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.90/2.51 % (213595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.90/2.51 % (213595)CaDiCaL version: 2.1.3
% 14.90/2.51 % (213595)Termination reason: Instruction limit
% 14.90/2.51 % (213595)Termination phase: Saturation
% 14.90/2.51 % (213595)Time elapsed: 0.250 s
% 14.90/2.51 % (213595)Peak memory usage: 14 MB
% 14.90/2.51 % (213595)Instructions burned: 423 (million)
% 14.90/2.51 % (213605)Instruction limit reached!
% 14.90/2.51 % (213605)------------------------------
% 14.90/2.51 % (213605)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.90/2.51 % (213605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.90/2.51 % (213605)CaDiCaL version: 2.1.3
% 14.90/2.51 % (213605)Termination reason: Instruction limit
% 14.90/2.51 % (213605)Termination phase: Saturation
% 14.90/2.51 % (213605)Time elapsed: 0.058 s
% 14.90/2.51 % (213605)Peak memory usage: 13 MB
% 14.90/2.51 % (213605)Instructions burned: 111 (million)
% 14.90/2.51 % (213611)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=1674827636:hsq=on:st=2:i=232:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2983 on theBenchmark for (2983ds/232Mi)
% 14.90/2.51 % (213610)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=1938519883:uwa_fpi=on:avsq=on:i=136:avsqr=1,32:hud=15:nm=0:rtra=on:ntd=on_2983 on theBenchmark for (2983ds/136Mi)
% 14.90/2.51 % (213608)Instruction limit reached!
% 14.90/2.51 % (213608)------------------------------
% 14.90/2.51 % (213608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.90/2.51 % (213608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.90/2.51 % (213608)CaDiCaL version: 2.1.3
% 14.90/2.51 % (213608)Termination reason: Instruction limit
% 14.90/2.51 % (213608)Termination phase: Saturation
% 14.90/2.51 % (213608)Time elapsed: 0.090 s
% 14.90/2.51 % (213608)Peak memory usage: 13 MB
% 14.90/2.51 % (213608)Instructions burned: 122 (million)
% 14.90/2.51 % (213604)Instruction limit reached!
% 14.90/2.51 % (213604)------------------------------
% 14.90/2.51 % (213604)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.90/2.51 % (213604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.54/2.77 % (213604)CaDiCaL version: 2.1.3
% 16.54/2.77 % (213604)Termination reason: Instruction limit
% 16.54/2.77 % (213604)Termination phase: Saturation
% 16.54/2.77 % (213604)Time elapsed: 0.154 s
% 16.54/2.77 % (213604)Peak memory usage: 13 MB
% 16.54/2.77 % (213604)Instructions burned: 340 (million)
% 16.54/2.77 % (213615)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 16.54/2.77 % (213615)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=3335285259:s2a=on:i=281:add=on:rtra=on:fe=axiom:fdi=1024_2982 on theBenchmark for (2982ds/281Mi)
% 16.54/2.77 % (213614)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=3906231868:i=1254:kws=precedence:bd=preordered:av=off:rtra=on_2982 on theBenchmark for (2982ds/1254Mi)
% 16.54/2.77 % (213610)Instruction limit reached!
% 16.54/2.77 % (213610)------------------------------
% 16.54/2.77 % (213610)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.54/2.77 % (213610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.54/2.77 % (213610)CaDiCaL version: 2.1.3
% 16.54/2.77 % (213610)Termination reason: Instruction limit
% 16.54/2.77 % (213610)Termination phase: Saturation
% 16.54/2.77 % (213610)Time elapsed: 0.089 s
% 16.54/2.77 % (213610)Peak memory usage: 13 MB
% 16.54/2.77 % (213610)Instructions burned: 136 (million)
% 16.54/2.77 % (213618)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=3914526842:i=619:add=on:rtra=on_2982 on theBenchmark for (2982ds/619Mi)
% 16.54/2.77 % (213611)Instruction limit reached!
% 16.54/2.77 % (213611)------------------------------
% 16.54/2.77 % (213611)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.54/2.77 % (213611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.54/2.77 % (213611)CaDiCaL version: 2.1.3
% 16.54/2.77 % (213611)Termination reason: Instruction limit
% 16.54/2.77 % (213611)Termination phase: Saturation
% 16.54/2.77 % (213611)Time elapsed: 0.144 s
% 16.54/2.77 % (213611)Peak memory usage: 13 MB
% 16.54/2.77 % (213611)Instructions burned: 232 (million)
% 16.54/2.77 % (213620)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=1170034378:i=865:bs=unit_only:ins=25:rtra=on:ntd=on_2981 on theBenchmark for (2981ds/865Mi)
% 16.54/2.77 % (213615)Instruction limit reached!
% 16.54/2.77 % (213615)------------------------------
% 16.54/2.77 % (213615)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.54/2.77 % (213615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.54/2.77 % (213615)CaDiCaL version: 2.1.3
% 16.54/2.77 % (213615)Termination reason: Instruction limit
% 16.54/2.77 % (213615)Termination phase: Saturation
% 16.54/2.77 % (213615)Time elapsed: 0.143 s
% 16.54/2.77 % (213615)Peak memory usage: 13 MB
% 16.54/2.77 % (213615)Instructions burned: 283 (million)
% 16.54/2.77 % (213622)lrs+10_1_sil=128000:si=on:urr=on:random_seed=2791906064:i=212:sd=1:rtra=on:ss=axioms:sgt=64_2980 on theBenchmark for (2980ds/212Mi)
% 16.54/2.77 % (213622)Instruction limit reached!
% 16.54/2.77 % (213622)------------------------------
% 16.54/2.77 % (213622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.54/2.77 % (213622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.54/2.77 % (213622)CaDiCaL version: 2.1.3
% 16.54/2.77 % (213622)Termination reason: Instruction limit
% 16.54/2.77 % (213622)Termination phase: Saturation
% 16.54/2.77 % (213622)Time elapsed: 0.102 s
% 16.54/2.77 % (213622)Peak memory usage: 14 MB
% 16.54/2.77 % (213622)Instructions burned: 213 (million)
% 16.54/2.77 % (213624)lrs+1010_64_sil=128000:si=on:avsql=on:uwa=off:random_seed=1925759259:hsq=on:st=3:avsq=on:i=130:avsqr=1,16:sd=1:rtra=on:ss=axioms_2979 on theBenchmark for (2979ds/130Mi)
% 16.54/2.77 % (213602)Instruction limit reached!
% 16.54/2.77 % (213602)------------------------------
% 16.54/2.77 % (213602)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.54/2.77 % (213602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.54/2.77 % (213602)CaDiCaL version: 2.1.3
% 16.54/2.77 % (213602)Termination reason: Instruction limit
% 16.54/2.77 % (213602)Termination phase: Saturation
% 16.54/2.77 % (213602)Time elapsed: 0.613 s
% 16.54/2.77 % (213602)Peak memory usage: 16 MB
% 18.99/3.07 % (213602)Instructions burned: 1442 (million)
% 18.99/3.07 % (213626)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=1103244077:st=1.5:i=346:rtra=on:ss=axioms_2978 on theBenchmark for (2978ds/346Mi)
% 18.99/3.07 % (213624)Instruction limit reached!
% 18.99/3.07 % (213624)------------------------------
% 18.99/3.07 % (213624)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.99/3.07 % (213624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.99/3.07 % (213624)CaDiCaL version: 2.1.3
% 18.99/3.07 % (213624)Termination reason: Instruction limit
% 18.99/3.07 % (213624)Termination phase: Saturation
% 18.99/3.07 % (213624)Time elapsed: 0.070 s
% 18.99/3.07 % (213624)Peak memory usage: 13 MB
% 18.99/3.07 % (213624)Instructions burned: 130 (million)
% 18.99/3.07 % (213628)lrs+1010_3_sil=128000:si=on:slsq=on:random_seed=3251716418:avsq=on:i=152:avsqr=8,1:hud=5:ins=1:fsr=off:rtra=on_2978 on theBenchmark for (2978ds/152Mi)
% 18.99/3.07 % (213618)Instruction limit reached!
% 18.99/3.07 % (213618)------------------------------
% 18.99/3.07 % (213618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.99/3.07 % (213618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.99/3.07 % (213618)CaDiCaL version: 2.1.3
% 18.99/3.07 % (213618)Termination reason: Instruction limit
% 18.99/3.07 % (213618)Termination phase: Saturation
% 18.99/3.07 % (213618)Time elapsed: 0.360 s
% 18.99/3.07 % (213618)Peak memory usage: 14 MB
% 18.99/3.07 % (213618)Instructions burned: 620 (million)
% 18.99/3.07 % (213630)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3680236291:i=75:ep=R:rtra=on:ntd=on_2978 on theBenchmark for (2978ds/75Mi)
% 18.99/3.07 % (213630)Instruction limit reached!
% 18.99/3.07 % (213630)------------------------------
% 18.99/3.07 % (213630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.99/3.07 % (213630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.99/3.07 % (213630)CaDiCaL version: 2.1.3
% 18.99/3.07 % (213630)Termination reason: Instruction limit
% 18.99/3.07 % (213630)Termination phase: Saturation
% 18.99/3.07 % (213630)Time elapsed: 0.037 s
% 18.99/3.07 % (213630)Peak memory usage: 13 MB
% 18.99/3.07 % (213630)Instructions burned: 76 (million)
% 18.99/3.07 % (213626)Instruction limit reached!
% 18.99/3.07 % (213626)------------------------------
% 18.99/3.07 % (213626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.99/3.07 % (213626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.99/3.07 % (213626)CaDiCaL version: 2.1.3
% 18.99/3.07 % (213626)Termination reason: Instruction limit
% 18.99/3.07 % (213626)Termination phase: Saturation
% 18.99/3.07 % (213626)Time elapsed: 0.091 s
% 18.99/3.07 % (213626)Peak memory usage: 14 MB
% 18.99/3.07 % (213626)Instructions burned: 350 (million)
% 18.99/3.07 % (213628)Instruction limit reached!
% 18.99/3.07 % (213628)------------------------------
% 18.99/3.07 % (213628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.99/3.07 % (213628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.99/3.07 % (213628)CaDiCaL version: 2.1.3
% 18.99/3.07 % (213628)Termination reason: Instruction limit
% 18.99/3.07 % (213628)Termination phase: Saturation
% 18.99/3.07 % (213628)Time elapsed: 0.071 s
% 18.99/3.07 % (213628)Peak memory usage: 14 MB
% 18.99/3.07 % (213628)Instructions burned: 153 (million)
% 18.99/3.07 % (213633)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=265833706:uwa_fpi=on:i=148:doe=on:bd=preordered:rtra=on:fsd=on_2977 on theBenchmark for (2977ds/148Mi)
% 18.99/3.07 % (213632)dis+10_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=one_side_interpreted:nwc=5:random_seed=3139353832:st=2.5:i=387:sd=2:rtra=on:ss=axioms_2977 on theBenchmark for (2977ds/387Mi)
% 18.99/3.07 % (213634)dis+1010_3_si=on:uwa=one_side_interpreted:random_seed=1684933506:i=161:piset=and:rtra=on:ntd=on_2977 on theBenchmark for (2977ds/161Mi)
% 18.99/3.07 % (213633)Instruction limit reached!
% 18.99/3.07 % (213633)------------------------------
% 18.99/3.07 % (213633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.99/3.07 % (213633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.99/3.07 % (213633)CaDiCaL version: 2.1.3
% 18.99/3.07 % (213633)Termination reason: Instruction limit
% 18.99/3.07 % (213633)Termination phase: Saturation
% 18.99/3.07 % (213633)Time elapsed: 0.035 s
% 20.57/3.31 % (213633)Peak memory usage: 13 MB
% 20.57/3.31 % (213633)Instructions burned: 152 (million)
% 20.57/3.31 % (213638)lrs+10_1_sil=128000:si=on:random_seed=1735930292:st=5:i=888:sd=3:bd=preordered:rtra=on:ss=axioms_2977 on theBenchmark for (2977ds/888Mi)
% 20.57/3.31 % (213634)Instruction limit reached!
% 20.57/3.31 % (213634)------------------------------
% 20.57/3.31 % (213634)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.57/3.31 % (213634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.57/3.31 % (213634)CaDiCaL version: 2.1.3
% 20.57/3.31 % (213634)Termination reason: Instruction limit
% 20.57/3.31 % (213634)Termination phase: Saturation
% 20.57/3.31 % (213634)Time elapsed: 0.118 s
% 20.57/3.31 % (213634)Peak memory usage: 13 MB
% 20.57/3.31 % (213634)Instructions burned: 162 (million)
% 20.57/3.31 % (213640)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=2635268098:i=136:add=on:ins=4:rtra=on:sup=off_2976 on theBenchmark for (2976ds/136Mi)
% 20.57/3.31 % (213632)Instruction limit reached!
% 20.57/3.31 % (213632)------------------------------
% 20.57/3.31 % (213632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.57/3.31 % (213632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.57/3.31 % (213632)CaDiCaL version: 2.1.3
% 20.57/3.31 % (213632)Termination reason: Instruction limit
% 20.57/3.31 % (213632)Termination phase: Saturation
% 20.57/3.31 % (213632)Time elapsed: 0.185 s
% 20.57/3.31 % (213632)Peak memory usage: 14 MB
% 20.57/3.31 % (213632)Instructions burned: 388 (million)
% 20.57/3.31 % (213620)Instruction limit reached!
% 20.57/3.31 % (213620)------------------------------
% 20.57/3.31 % (213620)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.57/3.31 % (213620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.57/3.31 % (213620)CaDiCaL version: 2.1.3
% 20.57/3.31 % (213620)Termination reason: Instruction limit
% 20.57/3.31 % (213620)Termination phase: Saturation
% 20.57/3.31 % (213620)Time elapsed: 0.598 s
% 20.57/3.31 % (213620)Peak memory usage: 17 MB
% 20.57/3.31 % (213620)Instructions burned: 866 (million)
% 20.57/3.31 % (213642)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=3218183986:i=88:s2at=3:nm=2:rtra=on:rawr=on_2975 on theBenchmark for (2975ds/88Mi)
% 20.57/3.31 % (213643)dis+1002_5:4_to=kbo:sil=128000:cnfonf=conj_eager:si=on:sp=reverse_arity:lma=off:hi=on:nwc=20:random_seed=65742909:s2a=on:cond=on:i=93:add=on:bd=preordered:rtra=on:er=filter_2975 on theBenchmark for (2975ds/93Mi)
% 20.57/3.31 % (213640)Instruction limit reached!
% 20.57/3.31 % (213640)------------------------------
% 20.57/3.31 % (213640)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.57/3.31 % (213640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.57/3.31 % (213640)CaDiCaL version: 2.1.3
% 20.57/3.31 % (213640)Termination reason: Instruction limit
% 20.57/3.31 % (213640)Termination phase: Saturation
% 20.57/3.31 % (213640)Time elapsed: 0.075 s
% 20.57/3.31 % (213640)Peak memory usage: 14 MB
% 20.57/3.31 % (213640)Instructions burned: 137 (million)
% 20.57/3.31 % (213638)Instruction limit reached!
% 20.57/3.31 % (213638)------------------------------
% 20.57/3.31 % (213638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.57/3.31 % (213638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.57/3.31 % (213638)CaDiCaL version: 2.1.3
% 20.57/3.31 % (213638)Termination reason: Instruction limit
% 20.57/3.31 % (213638)Termination phase: Saturation
% 20.57/3.31 % (213638)Time elapsed: 0.205 s
% 20.57/3.31 % (213638)Peak memory usage: 16 MB
% 20.57/3.31 % (213638)Instructions burned: 890 (million)
% 20.57/3.31 % (213647)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3637490210:s2a=on:i=240:rtra=on:ntd=on_2975 on theBenchmark for (2975ds/240Mi)
% 20.57/3.31 % (213646)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=2274867576:i=2186:rtra=on:ixr=off_2975 on theBenchmark for (2975ds/2186Mi)
% 20.57/3.31 % (213642)Instruction limit reached!
% 20.57/3.31 % (213642)------------------------------
% 20.57/3.31 % (213642)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.57/3.31 % (213642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.57/3.31 % (213642)CaDiCaL version: 2.1.3
% 20.57/3.31 % (213642)Termination reason: Instruction limit
% 21.54/3.50 % (213642)Termination phase: Saturation
% 21.54/3.50 % (213642)Time elapsed: 0.076 s
% 21.54/3.50 % (213642)Peak memory usage: 13 MB
% 21.54/3.50 % (213642)Instructions burned: 88 (million)
% 21.54/3.50 % (213650)dis+10_1_to=lpo:sil=128000:tgt=ground:si=on:urr=on:cbe=off:uwa=one_side_constant:nwc=5:random_seed=3265414242:i=805:aac=none:doe=on:piset=not:bd=all:rtra=on:fe=abstraction_2974 on theBenchmark for (2974ds/805Mi)
% 21.54/3.50 % (213643)Instruction limit reached!
% 21.54/3.50 % (213643)------------------------------
% 21.54/3.50 % (213643)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.54/3.50 % (213643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.54/3.50 % (213643)CaDiCaL version: 2.1.3
% 21.54/3.50 % (213643)Termination reason: Instruction limit
% 21.54/3.50 % (213643)Termination phase: Saturation
% 21.54/3.50 % (213643)Time elapsed: 0.084 s
% 21.54/3.50 % (213643)Peak memory usage: 13 MB
% 21.54/3.50 % (213643)Instructions burned: 95 (million)
% 21.54/3.50 % (213647)Instruction limit reached!
% 21.54/3.50 % (213647)------------------------------
% 21.54/3.50 % (213647)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.54/3.51 % (213647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.54/3.51 % (213647)CaDiCaL version: 2.1.3
% 21.54/3.51 % (213647)Termination reason: Instruction limit
% 21.54/3.51 % (213647)Termination phase: Saturation
% 21.54/3.51 % (213647)Time elapsed: 0.064 s
% 21.54/3.51 % (213647)Peak memory usage: 14 MB
% 21.54/3.51 % (213647)Instructions burned: 243 (million)
% 21.54/3.51 % (213653)dis+10_1_sil=128000:si=on:urr=on:uwa=off:random_seed=3150030296:i=355:av=off:fsr=off:rtra=on:ixr=off_2974 on theBenchmark for (2974ds/355Mi)
% 21.54/3.51 % (213652)WARNING Broken Constraint: if avatar_split_queue_cutoffs(1) has been set then avatar_split_queue(off) is equal to on
% 21.54/3.51 % (213652)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=3319192160:st=2:s2a=on:i=391:sd=4:bd=preordered:nm=16:rtra=on:ss=axioms:rawr=on_2974 on theBenchmark for (2974ds/391Mi)
% 21.54/3.51 % (213653)Instruction limit reached!
% 21.54/3.51 % (213653)------------------------------
% 21.54/3.51 % (213653)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.54/3.51 % (213653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.54/3.51 % (213653)CaDiCaL version: 2.1.3
% 21.54/3.51 % (213653)Termination reason: Instruction limit
% 21.54/3.51 % (213653)Termination phase: Saturation
% 21.54/3.51 % (213653)Time elapsed: 0.087 s
% 21.54/3.51 % (213653)Peak memory usage: 13 MB
% 21.54/3.51 % (213653)Instructions burned: 357 (million)
% 21.54/3.51 % (213656)lrs+1010_5:1_sil=128000:si=on:uwa=interpreted_only:sac=on:slsq=on:random_seed=1505584999:lrd=on:i=314:sd=1:rtra=on:ss=axioms_2973 on theBenchmark for (2973ds/314Mi)
% 21.54/3.51 % (213656)Instruction limit reached!
% 21.54/3.51 % (213656)------------------------------
% 21.54/3.51 % (213656)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.54/3.51 % (213656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.54/3.51 % (213656)CaDiCaL version: 2.1.3
% 21.54/3.51 % (213656)Termination reason: Instruction limit
% 21.54/3.51 % (213656)Termination phase: Saturation
% 21.54/3.51 % (213656)Time elapsed: 0.079 s
% 21.54/3.51 % (213656)Peak memory usage: 14 MB
% 21.54/3.51 % (213656)Instructions burned: 315 (million)
% 21.54/3.51 % (213658)lrs+10_1_sil=128000:e2e=on:si=on:cbe=off:uwa=interpreted_only:cs=on:random_seed=2548991904:s2a=on:i=251:fsr=off:rtra=on_2972 on theBenchmark for (2972ds/251Mi)
% 21.54/3.51 % (213614)Instruction limit reached!
% 21.54/3.51 % (213614)------------------------------
% 21.54/3.51 % (213614)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.54/3.51 % (213614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.54/3.51 % (213614)CaDiCaL version: 2.1.3
% 21.54/3.51 % (213614)Termination reason: Instruction limit
% 21.54/3.51 % (213614)Termination phase: Saturation
% 21.54/3.51 % (213614)Time elapsed: 1.031 s
% 21.54/3.51 % (213614)Peak memory usage: 20 MB
% 21.54/3.51 % (213614)Instructions burned: 1254 (million)
% 21.54/3.51 % (213658)Instruction limit reached!
% 21.54/3.51 % (213658)------------------------------
% 21.54/3.51 % (213658)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.54/3.51 % (213658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.24/3.85 % (213658)CaDiCaL version: 2.1.3
% 23.24/3.85 % (213658)Termination reason: Instruction limit
% 23.24/3.85 % (213658)Termination phase: Saturation
% 23.24/3.85 % (213658)Time elapsed: 0.069 s
% 23.24/3.85 % (213658)Peak memory usage: 14 MB
% 23.24/3.85 % (213658)Instructions burned: 258 (million)
% 23.24/3.85 % (213660)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=811033098: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_2972 on theBenchmark for (2972ds/2470Mi)
% 23.24/3.85 % (213661)dis+10_6_sil=128000:si=on:sp=arity:bce=on:cbe=off:uwa=interpreted_only:slsqc=4:slsq=on:random_seed=4050962581:i=673:doe=on:fgj=on:piset=and:slsql=off:rtra=on:fdi=1024:ntd=on_2971 on theBenchmark for (2971ds/673Mi)
% 23.24/3.85 % (213652)Instruction limit reached!
% 23.24/3.85 % (213652)------------------------------
% 23.24/3.85 % (213652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.24/3.85 % (213652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.24/3.85 % (213652)CaDiCaL version: 2.1.3
% 23.24/3.85 % (213652)Termination reason: Instruction limit
% 23.24/3.85 % (213652)Termination phase: Saturation
% 23.24/3.85 % (213652)Time elapsed: 0.280 s
% 23.24/3.85 % (213652)Peak memory usage: 14 MB
% 23.24/3.85 % (213652)Instructions burned: 391 (million)
% 23.24/3.85 % (213664)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=2051160593:i=116:ep=RSTC:rtra=on:ntd=on_2971 on theBenchmark for (2971ds/116Mi)
% 23.24/3.85 % (213661)Instruction limit reached!
% 23.24/3.85 % (213661)------------------------------
% 23.24/3.85 % (213661)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.24/3.85 % (213661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.24/3.85 % (213661)CaDiCaL version: 2.1.3
% 23.24/3.85 % (213661)Termination reason: Instruction limit
% 23.24/3.85 % (213661)Termination phase: Saturation
% 23.24/3.85 % (213661)Time elapsed: 0.164 s
% 23.24/3.85 % (213661)Peak memory usage: 14 MB
% 23.24/3.85 % (213661)Instructions burned: 674 (million)
% 23.24/3.85 % (213664)Instruction limit reached!
% 23.24/3.85 % (213664)------------------------------
% 23.24/3.85 % (213664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.24/3.85 % (213664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.24/3.85 % (213664)CaDiCaL version: 2.1.3
% 23.24/3.85 % (213664)Termination reason: Instruction limit
% 23.24/3.85 % (213664)Termination phase: Saturation
% 23.24/3.85 % (213664)Time elapsed: 0.101 s
% 23.24/3.85 % (213664)Peak memory usage: 13 MB
% 23.24/3.85 % (213664)Instructions burned: 116 (million)
% 23.24/3.85 % (213668)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=130340897:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2970 on theBenchmark for (2970ds/270Mi)
% 23.24/3.85 % (213650)Instruction limit reached!
% 23.24/3.85 % (213650)------------------------------
% 23.24/3.85 % (213650)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.24/3.85 % (213650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.24/3.85 % (213650)CaDiCaL version: 2.1.3
% 23.24/3.85 % (213650)Termination reason: Instruction limit
% 23.24/3.85 % (213650)Termination phase: Saturation
% 23.24/3.85 % (213650)Time elapsed: 0.490 s
% 23.24/3.85 % (213650)Peak memory usage: 16 MB
% 23.24/3.85 % (213650)Instructions burned: 806 (million)
% 23.24/3.85 % (213669)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=1151012452: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_2970 on theBenchmark for (2970ds/30Mi)
% 23.24/3.85 % (213672)WARNING Broken Constraint: if sine_tolerance(12) has been set then sine_selection(off) is not equal to off
% 23.24/3.85 % (213672)dis+1010_128_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=hol:nwc=2:flr=on:random_seed=2859559868:st=12:uwa_fpi=on:i=39:nm=40:ins=7:rtra=on_2969 on theBenchmark for (2969ds/39Mi)
% 23.24/3.85 % (213669)Instruction limit reached!
% 23.24/3.85 % (213669)------------------------------
% 23.24/3.85 % (213669)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.24/3.85 % (213669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.94/4.06 % (213669)CaDiCaL version: 2.1.3
% 25.94/4.06 % (213669)Termination reason: Instruction limit
% 25.94/4.06 % (213669)Termination phase: Saturation
% 25.94/4.06 % (213669)Time elapsed: 0.030 s
% 25.94/4.06 % (213669)Peak memory usage: 12 MB
% 25.94/4.06 % (213669)Instructions burned: 30 (million)
% 25.94/4.06 % (213668)Instruction limit reached!
% 25.94/4.06 % (213668)------------------------------
% 25.94/4.06 % (213668)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.94/4.06 % (213668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.94/4.06 % (213668)CaDiCaL version: 2.1.3
% 25.94/4.06 % (213668)Termination reason: Instruction limit
% 25.94/4.06 % (213668)Termination phase: Saturation
% 25.94/4.06 % (213668)Time elapsed: 0.060 s
% 25.94/4.06 % (213668)Peak memory usage: 14 MB
% 25.94/4.06 % (213668)Instructions burned: 271 (million)
% 25.94/4.06 % (213672)Instruction limit reached!
% 25.94/4.06 % (213672)------------------------------
% 25.94/4.06 % (213672)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.94/4.06 % (213672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.94/4.06 % (213672)CaDiCaL version: 2.1.3
% 25.94/4.06 % (213672)Termination reason: Instruction limit
% 25.94/4.06 % (213672)Termination phase: Saturation
% 25.94/4.06 % (213672)Time elapsed: 0.026 s
% 25.94/4.06 % (213672)Peak memory usage: 12 MB
% 25.94/4.06 % (213672)Instructions burned: 41 (million)
% 25.94/4.06 % (213675)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=2783048493:i=158:av=off:rtra=on_2969 on theBenchmark for (2969ds/158Mi)
% 25.94/4.06 % (213674)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=4175903048:i=365:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2969 on theBenchmark for (2969ds/365Mi)
% 25.94/4.06 % (213676)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
% 25.94/4.06 % (213676)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=2064986740:avsq=on:i=252:s2at=3:avsqr=1,16:rtra=on:ntd=on_2969 on theBenchmark for (2969ds/252Mi)
% 25.94/4.06 % (213675)Instruction limit reached!
% 25.94/4.06 % (213675)------------------------------
% 25.94/4.06 % (213675)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.94/4.06 % (213675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.94/4.06 % (213675)CaDiCaL version: 2.1.3
% 25.94/4.06 % (213675)Termination reason: Instruction limit
% 25.94/4.06 % (213675)Termination phase: Saturation
% 25.94/4.06 % (213675)Time elapsed: 0.045 s
% 25.94/4.06 % (213675)Peak memory usage: 13 MB
% 25.94/4.06 % (213675)Instructions burned: 161 (million)
% 25.94/4.06 % (213680)lrs+10_1_cnfonf=off:si=on:sos=on:uwa=off:random_seed=2072259970:i=213:rtra=on:ss=axioms_2968 on theBenchmark for (2968ds/213Mi)
% 25.94/4.06 % (213680)Instruction limit reached!
% 25.94/4.06 % (213680)------------------------------
% 25.94/4.06 % (213680)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.94/4.06 % (213680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.94/4.06 % (213680)CaDiCaL version: 2.1.3
% 25.94/4.06 % (213680)Termination reason: Instruction limit
% 25.94/4.06 % (213680)Termination phase: Saturation
% 25.94/4.06 % (213680)Time elapsed: 0.054 s
% 25.94/4.06 % (213680)Peak memory usage: 13 MB
% 25.94/4.06 % (213680)Instructions burned: 213 (million)
% 25.94/4.06 % (213682)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=292396334:st=3:i=160:s2at=3:bd=preordered:nm=16:rtra=on:ss=axioms:ntd=on_2968 on theBenchmark for (2968ds/160Mi)
% 25.94/4.06 % (213682)Instruction limit reached!
% 25.94/4.06 % (213682)------------------------------
% 25.94/4.06 % (213682)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.94/4.06 % (213682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.94/4.06 % (213682)CaDiCaL version: 2.1.3
% 25.94/4.06 % (213682)Termination reason: Instruction limit
% 25.94/4.06 % (213682)Termination phase: Saturation
% 25.94/4.06 % (213682)Time elapsed: 0.046 s
% 25.94/4.06 % (213682)Peak memory usage: 13 MB
% 25.94/4.06 % (213682)Instructions burned: 164 (million)
% 25.94/4.06 % (213674)Instruction limit reached!
% 25.94/4.06 % (213674)------------------------------
% 25.94/4.06 % (213674)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.47/4.17 % (213674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.47/4.17 % (213674)CaDiCaL version: 2.1.3
% 26.47/4.17 % (213674)Termination reason: Instruction limit
% 26.47/4.17 % (213674)Termination phase: Saturation
% 26.47/4.17 % (213674)Time elapsed: 0.169 s
% 26.47/4.17 % (213674)Peak memory usage: 14 MB
% 26.47/4.17 % (213674)Instructions burned: 365 (million)
% 26.47/4.17 % (213684)lrs+1010_2:3_sil=128000:cnfonf=off:e2e=on:si=on:sp=unary_first:uwa=off:br=off:lftc=80:random_seed=3577348015:hsq=on:hsqr=16,1:i=763:kws=inv_frequency:piset=and:bd=all:rtra=on:ntd=on_2967 on theBenchmark for (2967ds/763Mi)
% 26.47/4.17 % (213685)WARNING Broken Constraint: if ho_split_queue_layered_arrangement(off) has been set then ho_split_queue(off) is equal to on
% 26.47/4.17 % (213685)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=150204189:i=237:hsql=off:fgj=on:piset=all_but_not_eq:bd=preordered:av=off:rtra=on:ss=axioms:sgt=4:rawr=on_2967 on theBenchmark for (2967ds/237Mi)
% 26.47/4.17 % (213676)Instruction limit reached!
% 26.47/4.17 % (213676)------------------------------
% 26.47/4.17 % (213676)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.47/4.17 % (213676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.47/4.17 % (213676)CaDiCaL version: 2.1.3
% 26.47/4.17 % (213676)Termination reason: Instruction limit
% 26.47/4.17 % (213676)Termination phase: Saturation
% 26.47/4.17 % (213676)Time elapsed: 0.235 s
% 26.47/4.17 % (213676)Peak memory usage: 14 MB
% 26.47/4.17 % (213676)Instructions burned: 252 (million)
% 26.47/4.17 % (213688)dis+1002_1_drc=ordering:cnfonf=lazy_not_gen_be_off:si=on:lma=off:cbe=off:uwa=off:random_seed=466682017:s2a=on:i=386:rtra=on:ntd=on_2966 on theBenchmark for (2966ds/386Mi)
% 26.47/4.17 % (213685)Instruction limit reached!
% 26.47/4.17 % (213685)------------------------------
% 26.47/4.17 % (213685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.47/4.17 % (213685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.47/4.17 % (213685)CaDiCaL version: 2.1.3
% 26.47/4.17 % (213685)Termination reason: Instruction limit
% 26.47/4.17 % (213685)Termination phase: Saturation
% 26.47/4.17 % (213685)Time elapsed: 0.132 s
% 26.47/4.17 % (213685)Peak memory usage: 14 MB
% 26.47/4.17 % (213685)Instructions burned: 238 (million)
% 26.47/4.17 % (213690)dis+10_128_to=lpo:sil=128000:si=on:spb=intro:uwa=off:random_seed=453494115:i=300:piset=and:nm=32:rtra=on_2965 on theBenchmark for (2965ds/300Mi)
% 26.47/4.17 % (213646)Instruction limit reached!
% 26.47/4.17 % (213646)------------------------------
% 26.47/4.17 % (213646)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.47/4.17 % (213646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.47/4.17 % (213646)CaDiCaL version: 2.1.3
% 26.47/4.17 % (213646)Termination reason: Instruction limit
% 26.47/4.17 % (213646)Termination phase: Saturation
% 26.47/4.17 % (213646)Time elapsed: 0.993 s
% 26.47/4.17 % (213646)Peak memory usage: 15 MB
% 26.47/4.17 % (213646)Instructions burned: 2188 (million)
% 26.47/4.17 % (213684)Instruction limit reached!
% 26.47/4.17 % (213684)------------------------------
% 26.47/4.17 % (213684)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.47/4.17 % (213684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.47/4.17 % (213684)CaDiCaL version: 2.1.3
% 26.47/4.17 % (213684)Termination reason: Instruction limit
% 26.47/4.17 % (213684)Termination phase: Saturation
% 26.47/4.17 % (213684)Time elapsed: 0.230 s
% 26.47/4.17 % (213684)Peak memory usage: 19 MB
% 26.47/4.17 % (213684)Instructions burned: 763 (million)
% 26.47/4.17 % (213692)dis+1010_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:urr=on:random_seed=1284489274:st=5:s2a=on:i=567:sd=2:rtra=on:ss=axioms_2965 on theBenchmark for (2965ds/567Mi)
% 26.47/4.17 % (213693)lrs+1010_1_si=on:uwa=one_side_interpreted:random_seed=2323743950:s2a=on:i=379:sd=1:rtra=on:ss=axioms:sgt=128_2965 on theBenchmark for (2965ds/379Mi)
% 26.47/4.17 % (213690)Instruction limit reached!
% 26.47/4.17 % (213690)------------------------------
% 26.47/4.17 % (213690)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.47/4.17 % (213690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.47/4.17 % (213690)CaDiCaL version: 2.1.3
% 26.47/4.17 % (213690)Termination reason: Instruction limit
% 26.47/4.17 % (213690)Termination phase: Saturation
% 27.49/4.43 % (213690)Time elapsed: 0.173 s
% 27.49/4.43 % (213690)Peak memory usage: 13 MB
% 27.49/4.43 % (213690)Instructions burned: 301 (million)
% 27.49/4.43 % (213693)Instruction limit reached!
% 27.49/4.43 % (213693)------------------------------
% 27.49/4.43 % (213693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.49/4.43 % (213693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.49/4.43 % (213693)CaDiCaL version: 2.1.3
% 27.49/4.43 % (213693)Termination reason: Instruction limit
% 27.49/4.43 % (213693)Termination phase: Saturation
% 27.49/4.43 % (213693)Time elapsed: 0.101 s
% 27.49/4.43 % (213693)Peak memory usage: 15 MB
% 27.49/4.43 % (213693)Instructions burned: 380 (million)
% 27.49/4.43 % (213697)ott+10_1_to=lpo:sil=128000:e2e=on:si=on:sos=on:uwa=off:sac=on:random_seed=1808291261:i=478:bd=all:rtra=on_2963 on theBenchmark for (2963ds/478Mi)
% 27.49/4.43 % (213562)Instruction limit reached!
% 27.49/4.43 % (213562)------------------------------
% 27.49/4.43 % (213562)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.49/4.43 % (213562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.49/4.43 % (213562)CaDiCaL version: 2.1.3
% 27.49/4.43 % (213562)Termination reason: Instruction limit
% 27.49/4.43 % (213562)Termination phase: Saturation
% 27.49/4.43 % (213562)Time elapsed: 2.650 s
% 27.49/4.43 % (213562)Peak memory usage: 32 MB
% 27.49/4.43 % (213562)Instructions burned: 5756 (million)
% 27.49/4.43 % (213696)dis+32_3_cha=on:sil=128000:drc=off:si=on:cbe=off:uwa=interpreted_only:nwc=3:random_seed=1586870954:s2a=on:i=429:s2at=5:add=on:sd=2:ep=R:bd=preordered:rtra=on:ss=included:sgt=40_2964 on theBenchmark for (2964ds/429Mi)
% 27.49/4.43 % (213700)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=2392066447:i=445:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2963 on theBenchmark for (2963ds/445Mi)
% 27.49/4.43 % (213688)Instruction limit reached!
% 27.49/4.43 % (213688)------------------------------
% 27.49/4.43 % (213688)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.49/4.43 % (213688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.49/4.43 % (213688)CaDiCaL version: 2.1.3
% 27.49/4.43 % (213688)Termination reason: Instruction limit
% 27.49/4.43 % (213688)Termination phase: Saturation
% 27.49/4.43 % (213688)Time elapsed: 0.322 s
% 27.49/4.43 % (213688)Peak memory usage: 13 MB
% 27.49/4.43 % (213688)Instructions burned: 386 (million)
% 27.49/4.43 % (213702)ott+1003_1_to=kbo:cnfonf=lazy_pi_sigma_gen:si=on:sp=weighted_frequency:spb=units:urr=on:cbe=off:random_seed=43962576:uwa_fpi=on:i=71:hud=10:rtra=on:ixr=off_2963 on theBenchmark for (2963ds/71Mi)
% 27.49/4.43 % (213697)Instruction limit reached!
% 27.49/4.43 % (213697)------------------------------
% 27.49/4.43 % (213697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.49/4.43 % (213697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.49/4.43 % (213697)CaDiCaL version: 2.1.3
% 27.49/4.43 % (213697)Termination reason: Instruction limit
% 27.49/4.43 % (213697)Termination phase: Saturation
% 27.49/4.43 % (213697)Time elapsed: 0.125 s
% 27.49/4.43 % (213697)Peak memory usage: 15 MB
% 27.49/4.43 % (213697)Instructions burned: 482 (million)
% 27.49/4.43 % (213704)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=1699124180:i=302:sd=2:bd=preordered:rtra=on:ss=axioms_2962 on theBenchmark for (2962ds/302Mi)
% 27.49/4.43 % (213692)Instruction limit reached!
% 27.49/4.43 % (213692)------------------------------
% 27.49/4.43 % (213692)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.49/4.43 % (213692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.49/4.43 % (213692)CaDiCaL version: 2.1.3
% 27.49/4.43 % (213692)Termination reason: Instruction limit
% 27.49/4.43 % (213692)Termination phase: Saturation
% 27.49/4.43 % (213692)Time elapsed: 0.254 s
% 27.49/4.43 % (213692)Peak memory usage: 15 MB
% 27.49/4.43 % (213692)Instructions burned: 568 (million)
% 27.49/4.43 % (213706)lrs+10_1_sil=128000:fde=none:cnfonf=off:si=on:uwa=off:random_seed=2494507739:s2a=on:i=4980:sd=2:bd=all:rtra=on:ss=axioms:ntd=on_2962 on theBenchmark for (2962ds/4980Mi)
% 27.49/4.43 % (213702)Instruction limit reached!
% 27.49/4.43 % (213702)------------------------------
% 27.49/4.43 % (213702)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.49/4.43 % (213702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.49/4.43 % (213702)CaDiCaL version: 2.1.3
% 27.49/4.43 % (213702)Termination reason: Instruction limit
% 27.49/4.43 % (213702)Termination phase: Saturation
% 27.49/4.43 % (213702)Time elapsed: 0.066 s
% 27.49/4.43 % (213702)Peak memory usage: 12 MB
% 27.49/4.43 % (213702)Instructions burned: 72 (million)
% 27.49/4.43 % (213704)Instruction limit reached!
% 27.49/4.43 % (213704)------------------------------
% 27.49/4.43 % (213704)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.49/4.43 % (213704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.49/4.43 % (213704)CaDiCaL version: 2.1.3
% 27.49/4.43 % (213704)Termination reason: Instruction limit
% 27.49/4.43 % (213704)Termination phase: Saturation
% 27.49/4.43 % (213704)Time elapsed: 0.073 s
% 27.49/4.43 % (213704)Peak memory usage: 14 MB
% 27.49/4.43 % (213704)Instructions burned: 306 (million)
% 27.49/4.43 % (213708)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
% 27.49/4.43 % (213708)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 27.49/4.44 % (213708)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=401662249:i=100:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2961 on theBenchmark for (2961ds/100Mi)
% 27.49/4.44 % (213709)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=3880499801:i=76:piset=equals:rtra=on:ntd=on_2961 on theBenchmark for (2961ds/76Mi)
% 27.49/4.44 % (213709)Instruction limit reached!
% 27.49/4.44 % (213709)------------------------------
% 27.49/4.44 % (213709)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.49/4.44 % (213709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.49/4.44 % (213709)CaDiCaL version: 2.1.3
% 27.49/4.44 % (213709)Termination reason: Instruction limit
% 27.49/4.44 % (213709)Termination phase: Saturation
% 27.49/4.44 % (213709)Time elapsed: 0.020 s
% 27.49/4.44 % (213709)Peak memory usage: 12 MB
% 27.49/4.44 % (213709)Instructions burned: 79 (million)
% 27.49/4.44 % (213696)Instruction limit reached!
% 27.49/4.44 % (213696)------------------------------
% 27.49/4.44 % (213696)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.49/4.44 % (213696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.49/4.44 % (213696)CaDiCaL version: 2.1.3
% 27.49/4.44 % (213696)Termination reason: Instruction limit
% 27.49/4.44 % (213696)Termination phase: Saturation
% 27.49/4.44 % (213696)Time elapsed: 0.246 s
% 27.49/4.44 % (213696)Peak memory usage: 13 MB
% 27.49/4.44 % (213696)Instructions burned: 430 (million)
% 27.49/4.44 % (213713)lrs+2_64_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_first:bsr=unit_only:cbe=off:uwa=interpreted_only:nwc=0.5:slsqc=5:sac=on:slsq=on:random_seed=1035864716:i=493:s2at=5:kws=frequency:doe=on:rtra=on:er=known_2961 on theBenchmark for (2961ds/493Mi)
% 27.49/4.44 % (213712)lrs+10_1_to=lpo:sil=128000:cnfonf=off:si=on:sp=unary_first:sos=all:spb=goal:uwa=off:random_seed=3782057548:i=289:rtra=on_2961 on theBenchmark for (2961ds/289Mi)
% 27.49/4.44 % (213708)Instruction limit reached!
% 27.49/4.44 % (213708)------------------------------
% 27.49/4.44 % (213708)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.49/4.44 % (213708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.49/4.44 % (213708)CaDiCaL version: 2.1.3
% 27.49/4.44 % (213708)Termination reason: Instruction limit
% 27.49/4.44 % (213708)Termination phase: Saturation
% 27.49/4.44 % (213708)Time elapsed: 0.047 s
% 27.49/4.44 % (213708)Peak memory usage: 12 MB
% 27.49/4.44 % (213708)Instructions burned: 101 (million)
% 27.49/4.44 % (213716)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=3134423416:cond=on:i=34:hud=10:nm=10:rtra=on_2961 on theBenchmark for (2961ds/34Mi)
% 27.49/4.44 % (213716)Instruction limit reached!
% 27.49/4.44 % (213716)------------------------------
% 27.49/4.44 % (213716)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.49/4.44 % (213716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.49/4.44 % (213716)CaDiCaL version: 2.1.3
% 27.49/4.44 % (213716)Termination reason: Instruction limit
% 27.49/4.44 % (213716)Termination phase: Saturation
% 27.49/4.44 % (213716)Time elapsed: 0.016 s
% 27.49/4.44 % (213716)Peak memory usage: 12 MB
% 27.49/4.44 % (213716)Instructions burned: 34 (million)
% 27.49/4.44 % (213700)Instruction limit reached!
% 27.49/4.44 % (213700)------------------------------
% 27.49/4.44 % (213700)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.49/4.44 % (213700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.49/4.44 % (213700)CaDiCaL version: 2.1.3
% 27.49/4.44 % (213700)Termination reason: Instruction limit
% 27.49/4.44 % (213700)Termination phase: Saturation
% 27.49/4.44 % (213700)Time elapsed: 0.281 s
% 27.49/4.44 % (213700)Peak memory usage: 15 MB
% 27.49/4.44 % (213700)Instructions burned: 445 (million)
% 27.49/4.44 % (213719)lrs+1002_1024_sil=128000:tgt=ground:e2e=on:si=on:uwa=interpreted_only:fd=off:nwc=1:random_seed=254177533:cts=off:avsq=on:i=670:avsqr=1,16:nm=16:rtra=on_2960 on theBenchmark for (2960ds/670Mi)
% 27.49/4.44 % (213718)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 27.49/4.44 % (213718)dis+1010_1_to=lpo:irw=on:plsq=on:drc=ordering:plsqc=4:cnfonf=lazy_simp:si=on:sp=reverse_frequency:sos=on:plsqr=32,1:cbe=off:uwa=off:rp=on:lwlo=on:random_seed=3738526626:i=372:add=off:piset=or:nm=10:fsr=off:rtra=on:c=on_2960 on theBenchmark for (2960ds/372Mi)
% 27.49/4.44 % (213713)Instruction limit reached!
% 27.49/4.44 % (213713)------------------------------
% 27.49/4.44 % (213713)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.49/4.44 % (213713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.49/4.44 % (213713)CaDiCaL version: 2.1.3
% 27.49/4.44 % (213713)Termination reason: Instruction limit
% 27.49/4.44 % (213713)Termination phase: Saturation
% 27.49/4.44 % (213713)Time elapsed: 0.133 s
% 27.49/4.44 % (213713)Peak memory usage: 15 MB
% 27.49/4.44 % (213713)Instructions burned: 493 (million)
% 27.49/4.44 % (213722)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=829100843:hsq=on:st=2:i=647:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2959 on theBenchmark for (2959ds/647Mi)
% 27.49/4.44 % (213660)Instruction limit reached!
% 27.49/4.44 % (213660)------------------------------
% 27.49/4.44 % (213660)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.49/4.44 % (213660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.49/4.44 % (213660)CaDiCaL version: 2.1.3
% 27.49/4.44 % (213660)Termination reason: Instruction limit
% 27.49/4.44 % (213660)Termination phase: Saturation
% 27.49/4.44 % (213660)Time elapsed: 1.267 s
% 27.49/4.44 % (213660)Peak memory usage: 18 MB
% 27.49/4.44 % (213660)Instructions burned: 2471 (million)
% 27.49/4.44 % (213724)dis+10_128_sil=128000:tgt=full:plsq=on:plsqc=3:cnfonf=off:si=on:sp=arity:spb=goal_then_units:uwa=one_side_interpreted:nwc=1.5:random_seed=952422236:i=857:add=off:kws=frequency:rtra=on:ntd=on_2959 on theBenchmark for (2959ds/857Mi)
% 27.49/4.44 % (213712)Instruction limit reached!
% 27.49/4.44 % (213712)------------------------------
% 27.49/4.44 % (213712)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.49/4.44 % (213712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.49/4.44 % (213712)CaDiCaL version: 2.1.3
% 27.49/4.44 % (213712)Termination reason: Instruction limit
% 27.49/4.44 % (213712)Termination phase: Saturation
% 27.49/4.44 % (213712)Time elapsed: 0.230 s
% 27.49/4.44 % (213712)Peak memory usage: 15 MB
% 27.49/4.44 % (213712)Instructions burned: 289 (million)
% 27.49/4.44 % (213726)dis+1010_4_anc=all_dependent:to=lpo:sil=128000:fde=unused:cnfonf=conj_eager:si=on:sp=reverse_frequency:lma=off:spb=intro:cbe=off:uwa=off:random_seed=2930311073:i=693:add=off:fsr=off:rtra=on:fe=abstraction:ntd=on_2958 on theBenchmark for (2958ds/693Mi)
% 27.49/4.44 % (213722) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-213421-213722"...
% 27.49/4.44 % (213722)...printing done.
% 27.49/4.44 % (213722)Refutation found. Thanks to Tanya!
% 27.49/4.44 % SZS status Theorem for theBenchmark
% 27.49/4.44 % SZS output start Proof for theBenchmark
% 27.49/4.44 thf(type_def_5, type, a: $tType).
% 27.49/4.44 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 27.49/4.44 thf(func_def_0, type, z: a).
% 27.49/4.44 thf(func_def_1, type, y: a).
% 27.49/4.44 thf(func_def_2, type, cP: (a > a > a)).
% 27.49/4.44 thf(func_def_3, type, w: a).
% 27.49/4.44 thf(func_def_4, type, x: a).
% 27.49/4.44 thf(func_def_5, type, c0: a).
% 27.49/4.44 thf(func_def_9, type, sP0: (a > a > (a > a > a > $o) > a > $o)).
% 27.49/4.44 thf(func_def_10, type, sP1: (a > a > a > (a > a > a > $o) > $o)).
% 27.49/4.44 thf(func_def_11, type, sK2: (a > a > a > (a > a > a > $o) > a)).
% 27.49/4.44 thf(func_def_12, type, sK3: (a > a > a > (a > a > a > $o) > a)).
% 27.49/4.44 thf(func_def_13, type, sK4: (a > a > a > (a > a > a > $o) > a)).
% 27.49/4.44 thf(func_def_14, type, sK5: (a > a > a > (a > a > a > $o) > a)).
% 27.49/4.44 thf(func_def_15, type, sK6: (a > a > a > (a > a > a > $o) > a)).
% 27.49/4.44 thf(func_def_16, type, sK7: (a > a > a > (a > a > a > $o) > a)).
% 27.49/4.44 thf(func_def_17, type, sK8: (a > a > (a > a > a > $o) > a > a)).
% 27.49/4.44 thf(func_def_18, type, sK9: (a > a > (a > a > a > $o) > a > a)).
% 27.49/4.44 thf(func_def_19, type, sK10: (a > a > (a > a > a > $o) > a > a)).
% 27.49/4.44 thf(func_def_20, type, sK11: (a > a > (a > a > a > $o) > a > a)).
% 27.49/4.44 thf(func_def_21, type, sK12: (a > a > (a > a > a > $o) > a > a)).
% 27.49/4.44 thf(func_def_22, type, sK13: (a > a > (a > a > a > $o) > a > a)).
% 27.49/4.44 thf(func_def_23, type, sK14: ((a > a > a > $o) > a)).
% 27.49/4.44 thf(func_def_24, type, sK15: ((a > a > a > $o) > a)).
% 27.49/4.44 thf(func_def_25, type, sK16: ((a > a > a > $o) > a)).
% 27.49/4.44 thf(func_def_26, type, sK17: (a > a > a > $o)).
% 27.49/4.44 thf(func_def_27, type, sK18: ((a > a > a > $o) > a)).
% 27.49/4.44 thf(func_def_28, type, sK19: ((a > a > a > $o) > a)).
% 27.49/4.44 thf(func_def_29, type, sK20: ((a > a > a > $o) > a)).
% 27.49/4.44 thf(func_def_30, type, db0: !>[X0: $tType]:(X0)).
% 27.49/4.44 thf(func_def_31, type, db1: !>[X0: $tType]:(X0)).
% 27.49/4.44 thf(func_def_32, type, db2: !>[X0: $tType]:(X0)).
% 27.49/4.44 thf(func_def_33, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 27.49/4.44 thf(f1,conjecture,(
% 27.49/4.44 (! [X0 : (a > a > a > $o)] : ((! [X3 : a,X1 : a,X2 : a] : ((((X2 = X3) & (X1 = c0)) | ((X2 = c0) & (X1 = X3)) | ? [X6 : a,X9 : a,X8 : a,X4 : a,X5 : a,X7 : a] : ((X3 = ((cP @ X8 @ X9))) & (X0 @ X5 @ X7 @ X9) & (X2 = ((cP @ X6 @ X7))) & (X0 @ X4 @ X6 @ X8) & (X1 = ((cP @ X4 @ X5))))) => (X0 @ X1 @ X2 @ X3)) & $true) => (X0 @ w @ z @ z)) & ! [X0 : (a > a > a > $o)] : ((! [X3 : a,X1 : a,X2 : a] : ((? [X5 : a,X4 : a,X8 : a,X6 : a,X9 : a,X7 : a] : ((X3 = ((cP @ X8 @ X9))) & (X0 @ X5 @ X7 @ X9) & (X1 = ((cP @ X4 @ X5))) & (X0 @ X4 @ X6 @ X8) & (X2 = ((cP @ X6 @ X7)))) | ((X2 = c0) & (X1 = X3)) | ((X2 = X3) & (X1 = c0))) => (X0 @ X1 @ X2 @ X3)) & $true) => (X0 @ x @ y @ y))) => ! [X0 : (a > a > a > $o)] : ((! [X3 : a,X1 : a,X2 : a] : ((((X2 = c0) & (X1 = X3)) | ? [X4 : a,X6 : a,X9 : a,X8 : a,X7 : a,X5 : a] : ((X0 @ X5 @ X7 @ X9) & (X1 = ((cP @ X4 @ X5))) & (X0 @ X4 @ X6 @ X8) & (X3 = ((cP @ X8 @ X9))) & (X2 = ((cP @ X6 @ X7)))) | ((X1 = c0) & (X2 = X3))) => (X0 @ X1 @ X2 @ X3)) & $true) => (X0 @ (cP @ x @ w) @ (cP @ y @ z) @ (cP @ y @ z)))),
% 27.49/4.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cS_INCL_LEM1_pme)).
% 27.49/4.44 thf(f2,negated_conjecture,(
% 27.49/4.44 ~((! [X0 : (a > a > a > $o)] : ((! [X3 : a,X1 : a,X2 : a] : ((((X2 = X3) & (X1 = c0)) | ((X2 = c0) & (X1 = X3)) | ? [X6 : a,X9 : a,X8 : a,X4 : a,X5 : a,X7 : a] : ((X3 = ((cP @ X8 @ X9))) & (X0 @ X5 @ X7 @ X9) & (X2 = ((cP @ X6 @ X7))) & (X0 @ X4 @ X6 @ X8) & (X1 = ((cP @ X4 @ X5))))) => (X0 @ X1 @ X2 @ X3)) & $true) => (X0 @ w @ z @ z)) & ! [X0 : (a > a > a > $o)] : ((! [X3 : a,X1 : a,X2 : a] : ((? [X5 : a,X4 : a,X8 : a,X6 : a,X9 : a,X7 : a] : ((X3 = ((cP @ X8 @ X9))) & (X0 @ X5 @ X7 @ X9) & (X1 = ((cP @ X4 @ X5))) & (X0 @ X4 @ X6 @ X8) & (X2 = ((cP @ X6 @ X7)))) | ((X2 = c0) & (X1 = X3)) | ((X2 = X3) & (X1 = c0))) => (X0 @ X1 @ X2 @ X3)) & $true) => (X0 @ x @ y @ y))) => ! [X0 : (a > a > a > $o)] : ((! [X3 : a,X1 : a,X2 : a] : ((((X2 = c0) & (X1 = X3)) | ? [X4 : a,X6 : a,X9 : a,X8 : a,X7 : a,X5 : a] : ((X0 @ X5 @ X7 @ X9) & (X1 = ((cP @ X4 @ X5))) & (X0 @ X4 @ X6 @ X8) & (X3 = ((cP @ X8 @ X9))) & (X2 = ((cP @ X6 @ X7)))) | ((X1 = c0) & (X2 = X3))) => (X0 @ X1 @ X2 @ X3)) & $true) => (X0 @ (cP @ x @ w) @ (cP @ y @ z) @ (cP @ y @ z))))),
% 27.49/4.44 inference(negated_conjecture,[status(cth)],[f1])).
% 27.49/4.44 thf(f3,plain,(
% 27.49/4.44 ~((! [X0 : (a > a > a > $o)] : ((! [X1 : a,X2 : a,X3 : a] : ((((X1 = X3) & (c0 = X2)) | ((c0 = X3) & (X1 = X2)) | ? [X4 : a,X5 : a,X6 : a,X7 : a,X8 : a,X9 : a] : ((((cP @ X6 @ X5)) = X1) & (X0 @ X8 @ X9 @ X5) & (((cP @ X4 @ X9)) = X3) & (X0 @ X7 @ X4 @ X6) & (((cP @ X7 @ X8)) = X2))) => (X0 @ X2 @ X3 @ X1)) & $true) => (X0 @ w @ z @ z)) & ! [X10 : (a > a > a > $o)] : ((! [X11 : a,X12 : a,X13 : a] : ((? [X14 : a,X15 : a,X16 : a,X17 : a,X18 : a,X19 : a] : ((((cP @ X16 @ X18)) = X11) & (X10 @ X14 @ X19 @ X18) & (((cP @ X15 @ X14)) = X12) & (X10 @ X15 @ X17 @ X16) & (((cP @ X17 @ X19)) = X13)) | ((c0 = X13) & (X11 = X12)) | ((X11 = X13) & (c0 = X12))) => (X10 @ X12 @ X13 @ X11)) & $true) => (X10 @ x @ y @ y))) => ! [X20 : (a > a > a > $o)] : ((! [X21 : a,X22 : a,X23 : a] : ((((c0 = X23) & (X21 = X22)) | ? [X24 : a,X25 : a,X26 : a,X27 : a,X28 : a,X29 : a] : ((X20 @ X29 @ X28 @ X26) & (((cP @ X24 @ X29)) = X22) & (X20 @ X24 @ X25 @ X27) & (((cP @ X27 @ X26)) = X21) & (((cP @ X25 @ X28)) = X23)) | ((c0 = X22) & (X21 = X23))) => (X20 @ X22 @ X23 @ X21)) & $true) => (X20 @ (cP @ x @ w) @ (cP @ y @ z) @ (cP @ y @ z))))),
% 27.49/4.44 inference(rectify,[],[f2])).
% 27.49/4.44 thf(f4,plain,(
% 27.49/4.44 ~((! [X0 : (a > a > a > $o)] : ((! [X2 : a,X3 : a,X1 : a] : ((? [X6 : a,X9 : a,X7 : a,X5 : a,X8 : a,X4 : a] : ((((cP @ X7 @ X8)) = X2) & ($true = ((X0 @ X8 @ X9 @ X5))) & ($true = ((X0 @ X7 @ X4 @ X6))) & (((cP @ X6 @ X5)) = X1) & (((cP @ X4 @ X9)) = X3)) | ((X1 = X3) & (c0 = X2)) | ((X1 = X2) & (c0 = X3))) => ($true = ((X0 @ X2 @ X3 @ X1)))) & $true) => (((X0 @ w @ z @ z)) = $true)) & ! [X10 : (a > a > a > $o)] : ((! [X12 : a,X13 : a,X11 : a] : ((((c0 = X13) & (X11 = X12)) | ? [X14 : a,X19 : a,X16 : a,X17 : a,X15 : a,X18 : a] : ((((X10 @ X15 @ X17 @ X16)) = $true) & (((cP @ X16 @ X18)) = X11) & ($true = ((X10 @ X14 @ X19 @ X18))) & (((cP @ X17 @ X19)) = X13) & (((cP @ X15 @ X14)) = X12)) | ((X11 = X13) & (c0 = X12))) => ($true = ((X10 @ X12 @ X13 @ X11)))) & $true) => ($true = ((X10 @ x @ y @ y))))) => ! [X20 : (a > a > a > $o)] : ((! [X23 : a,X21 : a,X22 : a] : ((((c0 = X23) & (X21 = X22)) | ? [X28 : a,X29 : a,X27 : a,X26 : a,X24 : a,X25 : a] : ((((cP @ X24 @ X29)) = X22) & (((X20 @ X24 @ X25 @ X27)) = $true) & (((cP @ X27 @ X26)) = X21) & (((cP @ X25 @ X28)) = X23) & (((X20 @ X29 @ X28 @ X26)) = $true)) | ((c0 = X22) & (X21 = X23))) => ($true = ((X20 @ X22 @ X23 @ X21)))) & $true) => (((X20 @ (cP @ x @ w) @ (cP @ y @ z) @ (cP @ y @ z))) = $true)))),
% 27.49/4.44 inference(fool_elimination,[],[f3])).
% 27.49/4.44 thf(f5,plain,(
% 27.49/4.44 ~((! [X0 : (a > a > a > $o)] : (! [X2 : a,X3 : a,X1 : a] : ((? [X6 : a,X9 : a,X7 : a,X5 : a,X8 : a,X4 : a] : ((((cP @ X7 @ X8)) = X2) & ($true = ((X0 @ X8 @ X9 @ X5))) & ($true = ((X0 @ X7 @ X4 @ X6))) & (((cP @ X6 @ X5)) = X1) & (((cP @ X4 @ X9)) = X3)) | ((X1 = X3) & (c0 = X2)) | ((X1 = X2) & (c0 = X3))) => ($true = ((X0 @ X2 @ X3 @ X1)))) => (((X0 @ w @ z @ z)) = $true)) & ! [X10 : (a > a > a > $o)] : (! [X12 : a,X13 : a,X11 : a] : ((((c0 = X13) & (X11 = X12)) | ? [X14 : a,X19 : a,X16 : a,X17 : a,X15 : a,X18 : a] : ((((X10 @ X15 @ X17 @ X16)) = $true) & (((cP @ X16 @ X18)) = X11) & ($true = ((X10 @ X14 @ X19 @ X18))) & (((cP @ X17 @ X19)) = X13) & (((cP @ X15 @ X14)) = X12)) | ((X11 = X13) & (c0 = X12))) => ($true = ((X10 @ X12 @ X13 @ X11)))) => ($true = ((X10 @ x @ y @ y))))) => ! [X20 : (a > a > a > $o)] : (! [X23 : a,X21 : a,X22 : a] : ((((c0 = X23) & (X21 = X22)) | ? [X28 : a,X29 : a,X27 : a,X26 : a,X24 : a,X25 : a] : ((((cP @ X24 @ X29)) = X22) & (((X20 @ X24 @ X25 @ X27)) = $true) & (((cP @ X27 @ X26)) = X21) & (((cP @ X25 @ X28)) = X23) & (((X20 @ X29 @ X28 @ X26)) = $true)) | ((c0 = X22) & (X21 = X23))) => ($true = ((X20 @ X22 @ X23 @ X21)))) => (((X20 @ (cP @ x @ w) @ (cP @ y @ z) @ (cP @ y @ z))) = $true)))),
% 27.49/4.44 inference(true_and_false_elimination,[],[f4])).
% 27.49/4.44 thf(f6,plain,(
% 27.49/4.44 ? [X20 : (a > a > a > $o)] : ((((X20 @ (cP @ x @ w) @ (cP @ y @ z) @ (cP @ y @ z))) != $true) & ! [X22 : a,X21 : a,X23 : a] : ((! [X26 : a,X27 : a,X29 : a,X24 : a,X28 : a,X25 : a] : ((((cP @ X25 @ X28)) != X23) | (((X20 @ X29 @ X28 @ X26)) != $true) | (((cP @ X24 @ X29)) != X22) | (((X20 @ X24 @ X25 @ X27)) != $true) | (((cP @ X27 @ X26)) != X21)) & ((X21 != X23) | (c0 != X22)) & ((c0 != X23) | (X21 != X22))) | ($true = ((X20 @ X22 @ X23 @ X21))))) & (! [X0 : (a > a > a > $o)] : ((((X0 @ w @ z @ z)) = $true) | ? [X2 : a,X3 : a,X1 : a] : ((? [X6 : a,X9 : a,X7 : a,X5 : a,X8 : a,X4 : a] : ((((cP @ X7 @ X8)) = X2) & ($true = ((X0 @ X8 @ X9 @ X5))) & ($true = ((X0 @ X7 @ X4 @ X6))) & (((cP @ X6 @ X5)) = X1) & (((cP @ X4 @ X9)) = X3)) | ((X1 = X3) & (c0 = X2)) | ((X1 = X2) & (c0 = X3))) & ($true != ((X0 @ X2 @ X3 @ X1))))) & ! [X10 : (a > a > a > $o)] : (? [X13 : a,X12 : a,X11 : a] : ((((c0 = X13) & (X11 = X12)) | ? [X14 : a,X19 : a,X16 : a,X17 : a,X15 : a,X18 : a] : ((((X10 @ X15 @ X17 @ X16)) = $true) & (((cP @ X16 @ X18)) = X11) & ($true = ((X10 @ X14 @ X19 @ X18))) & (((cP @ X17 @ X19)) = X13) & (((cP @ X15 @ X14)) = X12)) | ((X11 = X13) & (c0 = X12))) & ($true != ((X10 @ X12 @ X13 @ X11)))) | ($true = ((X10 @ x @ y @ y)))))),
% 27.49/4.44 inference(ennf_transformation,[],[f5])).
% 27.49/4.44 thf(f7,plain,(
% 27.49/4.44 ! [X10 : (a > a > a > $o)] : (? [X13 : a,X12 : a,X11 : a] : ((((c0 = X13) & (X11 = X12)) | ? [X14 : a,X19 : a,X16 : a,X17 : a,X15 : a,X18 : a] : ((((X10 @ X15 @ X17 @ X16)) = $true) & (((cP @ X16 @ X18)) = X11) & ($true = ((X10 @ X14 @ X19 @ X18))) & (((cP @ X17 @ X19)) = X13) & (((cP @ X15 @ X14)) = X12)) | ((X11 = X13) & (c0 = X12))) & ($true != ((X10 @ X12 @ X13 @ X11)))) | ($true = ((X10 @ x @ y @ y)))) & ? [X20 : (a > a > a > $o)] : ((((X20 @ (cP @ x @ w) @ (cP @ y @ z) @ (cP @ y @ z))) != $true) & ! [X22 : a,X21 : a,X23 : a] : ((! [X26 : a,X27 : a,X29 : a,X24 : a,X28 : a,X25 : a] : ((((cP @ X25 @ X28)) != X23) | (((X20 @ X29 @ X28 @ X26)) != $true) | (((cP @ X24 @ X29)) != X22) | (((X20 @ X24 @ X25 @ X27)) != $true) | (((cP @ X27 @ X26)) != X21)) & ((X21 != X23) | (c0 != X22)) & ((c0 != X23) | (X21 != X22))) | ($true = ((X20 @ X22 @ X23 @ X21))))) & ! [X0 : (a > a > a > $o)] : ((((X0 @ w @ z @ z)) = $true) | ? [X2 : a,X3 : a,X1 : a] : ((? [X6 : a,X9 : a,X7 : a,X5 : a,X8 : a,X4 : a] : ((((cP @ X7 @ X8)) = X2) & ($true = ((X0 @ X8 @ X9 @ X5))) & ($true = ((X0 @ X7 @ X4 @ X6))) & (((cP @ X6 @ X5)) = X1) & (((cP @ X4 @ X9)) = X3)) | ((X1 = X3) & (c0 = X2)) | ((X1 = X2) & (c0 = X3))) & ($true != ((X0 @ X2 @ X3 @ X1)))))),
% 27.49/4.44 inference(flattening,[],[f6])).
% 27.49/4.44 thf(f8,definition,(
% 27.49/4.44 ! [X2 : a,X0 : (a > a > a > $o),X1 : a,X3 : a] : (? [X6 : a,X9 : a,X7 : a,X5 : a,X8 : a,X4 : a] : ((((cP @ X7 @ X8)) = X2) & ($true = ((X0 @ X8 @ X9 @ X5))) & ($true = ((X0 @ X7 @ X4 @ X6))) & (((cP @ X6 @ X5)) = X1) & (((cP @ X4 @ X9)) = X3)) | ~ ($true = ((sP0 @ X3 @ X1 @ X0 @ X2))))),
% 27.49/4.44 introduced(definition,[new_symbols(definition,[=])],[predicate_definition_introduction])).
% 27.49/4.44 thf(f9,definition,(
% 27.49/4.44 ! [X10 : (a > a > a > $o),X11 : a,X13 : a,X12 : a] : (? [X14 : a,X19 : a,X16 : a,X17 : a,X15 : a,X18 : a] : ((((X10 @ X15 @ X17 @ X16)) = $true) & (((cP @ X16 @ X18)) = X11) & ($true = ((X10 @ X14 @ X19 @ X18))) & (((cP @ X17 @ X19)) = X13) & (((cP @ X15 @ X14)) = X12)) | ~ (((sP1 @ X12 @ X13 @ X11 @ X10)) = $true))),
% 27.49/4.44 introduced(definition,[new_symbols(definition,[=])],[predicate_definition_introduction])).
% 27.49/4.44 thf(f10,plain,(
% 27.49/4.44 ! [X10 : (a > a > a > $o)] : (? [X13 : a,X12 : a,X11 : a] : ((((c0 = X13) & (X11 = X12)) | (((sP1 @ X12 @ X13 @ X11 @ X10)) = $true) | ((X11 = X13) & (c0 = X12))) & ($true != ((X10 @ X12 @ X13 @ X11)))) | ($true = ((X10 @ x @ y @ y)))) & ? [X20 : (a > a > a > $o)] : ((((X20 @ (cP @ x @ w) @ (cP @ y @ z) @ (cP @ y @ z))) != $true) & ! [X22 : a,X21 : a,X23 : a] : ((! [X26 : a,X27 : a,X29 : a,X24 : a,X28 : a,X25 : a] : ((((cP @ X25 @ X28)) != X23) | (((X20 @ X29 @ X28 @ X26)) != $true) | (((cP @ X24 @ X29)) != X22) | (((X20 @ X24 @ X25 @ X27)) != $true) | (((cP @ X27 @ X26)) != X21)) & ((X21 != X23) | (c0 != X22)) & ((c0 != X23) | (X21 != X22))) | ($true = ((X20 @ X22 @ X23 @ X21))))) & ! [X0 : (a > a > a > $o)] : ((((X0 @ w @ z @ z)) = $true) | ? [X2 : a,X3 : a,X1 : a] : ((($true = ((sP0 @ X3 @ X1 @ X0 @ X2))) | ((X1 = X3) & (c0 = X2)) | ((X1 = X2) & (c0 = X3))) & ($true != ((X0 @ X2 @ X3 @ X1)))))),
% 27.49/4.44 inference(definition_folding,[],[f7,f9,f8])).
% 27.49/4.44 thf(f11,plain,(
% 27.49/4.44 ! [X10 : (a > a > a > $o),X11 : a,X13 : a,X12 : a] : (? [X14 : a,X19 : a,X16 : a,X17 : a,X15 : a,X18 : a] : ((((X10 @ X15 @ X17 @ X16)) = $true) & (((cP @ X16 @ X18)) = X11) & ($true = ((X10 @ X14 @ X19 @ X18))) & (((cP @ X17 @ X19)) = X13) & (((cP @ X15 @ X14)) = X12)) | (((sP1 @ X12 @ X13 @ X11 @ X10)) != $true))),
% 27.49/4.44 inference(nnf_transformation,[],[f9])).
% 27.49/4.44 thf(f12,plain,(
% 27.49/4.44 ! [X0 : (a > a > a > $o),X1 : a,X2 : a,X3 : a] : (? [X4 : a,X5 : a,X6 : a,X7 : a,X8 : a,X9 : a] : (($true = ((X0 @ X8 @ X7 @ X6))) & (((cP @ X6 @ X9)) = X1) & ($true = ((X0 @ X4 @ X5 @ X9))) & (((cP @ X7 @ X5)) = X2) & (((cP @ X8 @ X4)) = X3)) | (((sP1 @ X3 @ X2 @ X1 @ X0)) != $true))),
% 27.49/4.44 inference(rectify,[],[f11])).
% 27.49/4.44 thf(f13,plain,(
% 27.49/4.44 ! [X0 : (a > a > a > $o),X1 : a,X2 : a,X3 : a] : ((($true = ((X0 @ (sK6 @ X3 @ X2 @ X1 @ X0) @ (sK5 @ X3 @ X2 @ X1 @ X0) @ (sK4 @ X3 @ X2 @ X1 @ X0)))) & (((cP @ (sK4 @ X3 @ X2 @ X1 @ X0) @ (sK7 @ X3 @ X2 @ X1 @ X0))) = X1) & ($true = ((X0 @ (sK2 @ X3 @ X2 @ X1 @ X0) @ (sK3 @ X3 @ X2 @ X1 @ X0) @ (sK7 @ X3 @ X2 @ X1 @ X0)))) & (((cP @ (sK5 @ X3 @ X2 @ X1 @ X0) @ (sK3 @ X3 @ X2 @ X1 @ X0))) = X2) & (((cP @ (sK6 @ X3 @ X2 @ X1 @ X0) @ (sK2 @ X3 @ X2 @ X1 @ X0))) = X3)) | (((sP1 @ X3 @ X2 @ X1 @ X0)) != $true))),
% 27.49/4.44 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP,vAPP,vAPP,vAPP,vAPP,vAPP]),skolemize(X9,sK7 @ X3 @ X2 @ X1 @ X0),skolemize(X9,sK7 @ X3 @ X2 @ X1 @ X0),skolemize(X9,sK7 @ X3 @ X2 @ X1 @ X0),skolemize(X9,sK7 @ X3 @ X2 @ X1 @ X0),skolemize(X9,sK7 @ X3 @ X2 @ X1 @ X0),skolemize(X9,sK7 @ X3 @ X2 @ X1 @ X0)],[f12])).
% 27.49/4.44 thf(f14,plain,(
% 27.49/4.44 ! [X2 : a,X0 : (a > a > a > $o),X1 : a,X3 : a] : (? [X6 : a,X9 : a,X7 : a,X5 : a,X8 : a,X4 : a] : ((((cP @ X7 @ X8)) = X2) & ($true = ((X0 @ X8 @ X9 @ X5))) & ($true = ((X0 @ X7 @ X4 @ X6))) & (((cP @ X6 @ X5)) = X1) & (((cP @ X4 @ X9)) = X3)) | ($true != ((sP0 @ X3 @ X1 @ X0 @ X2))))),
% 27.49/4.44 inference(nnf_transformation,[],[f8])).
% 27.49/4.44 thf(f15,plain,(
% 27.49/4.44 ! [X0 : a,X1 : (a > a > a > $o),X2 : a,X3 : a] : (? [X4 : a,X5 : a,X6 : a,X7 : a,X8 : a,X9 : a] : ((((cP @ X6 @ X8)) = X0) & ($true = ((X1 @ X8 @ X5 @ X7))) & (((X1 @ X6 @ X9 @ X4)) = $true) & (((cP @ X4 @ X7)) = X2) & (((cP @ X9 @ X5)) = X3)) | ($true != ((sP0 @ X3 @ X2 @ X1 @ X0))))),
% 27.49/4.44 inference(rectify,[],[f14])).
% 27.49/4.44 thf(f16,plain,(
% 27.49/4.44 ! [X0 : a,X1 : (a > a > a > $o),X2 : a,X3 : a] : (((((cP @ (sK10 @ X3 @ X2 @ X1 @ X0) @ (sK12 @ X3 @ X2 @ X1 @ X0))) = X0) & ($true = ((X1 @ (sK12 @ X3 @ X2 @ X1 @ X0) @ (sK9 @ X3 @ X2 @ X1 @ X0) @ (sK11 @ X3 @ X2 @ X1 @ X0)))) & ($true = ((X1 @ (sK10 @ X3 @ X2 @ X1 @ X0) @ (sK13 @ X3 @ X2 @ X1 @ X0) @ (sK8 @ X3 @ X2 @ X1 @ X0)))) & (((cP @ (sK8 @ X3 @ X2 @ X1 @ X0) @ (sK11 @ X3 @ X2 @ X1 @ X0))) = X2) & (((cP @ (sK13 @ X3 @ X2 @ X1 @ X0) @ (sK9 @ X3 @ X2 @ X1 @ X0))) = X3)) | ($true != ((sP0 @ X3 @ X2 @ X1 @ X0))))),
% 27.49/4.44 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP,vAPP,vAPP,vAPP,vAPP,vAPP]),skolemize(X9,sK7 @ X3 @ X2 @ X1 @ X0),skolemize(X9,sK7 @ X3 @ X2 @ X1 @ X0),skolemize(X9,sK7 @ X3 @ X2 @ X1 @ X0),skolemize(X9,sK7 @ X3 @ X2 @ X1 @ X0),skolemize(X9,sK7 @ X3 @ X2 @ X1 @ X0),skolemize(X9,sK7 @ X3 @ X2 @ X1 @ X0)],[f15])).
% 27.49/4.44 thf(f17,plain,(
% 27.49/4.44 ! [X0 : (a > a > a > $o)] : (? [X1 : a,X2 : a,X3 : a] : ((((c0 = X1) & (X2 = X3)) | ($true = ((sP1 @ X2 @ X1 @ X3 @ X0))) | ((X1 = X3) & (c0 = X2))) & (((X0 @ X2 @ X1 @ X3)) != $true)) | (((X0 @ x @ y @ y)) = $true)) & ? [X4 : (a > a > a > $o)] : (($true != ((X4 @ (cP @ x @ w) @ (cP @ y @ z) @ (cP @ y @ z)))) & ! [X5 : a,X6 : a,X7 : a] : ((! [X8 : a,X9 : a,X10 : a,X11 : a,X12 : a,X13 : a] : ((((cP @ X13 @ X12)) != X7) | (((X4 @ X10 @ X12 @ X8)) != $true) | (((cP @ X11 @ X10)) != X5) | (((X4 @ X11 @ X13 @ X9)) != $true) | (((cP @ X9 @ X8)) != X6)) & ((X6 != X7) | (c0 != X5)) & ((c0 != X7) | (X5 != X6))) | (((X4 @ X5 @ X7 @ X6)) = $true))) & ! [X14 : (a > a > a > $o)] : (($true = ((X14 @ w @ z @ z))) | ? [X15 : a,X16 : a,X17 : a] : (((((sP0 @ X16 @ X17 @ X14 @ X15)) = $true) | ((X16 = X17) & (c0 = X15)) | ((X15 = X17) & (c0 = X16))) & ($true != ((X14 @ X15 @ X16 @ X17)))))),
% 27.49/4.44 inference(rectify,[],[f10])).
% 27.49/4.44 thf(f18,plain,(
% 27.49/4.44 ! [X0 : (a > a > a > $o)] : (((((c0 = ((sK14 @ X0))) & (((sK15 @ X0)) = ((sK16 @ X0)))) | ($true = ((sP1 @ (sK15 @ X0) @ (sK14 @ X0) @ (sK16 @ X0) @ X0))) | ((((sK16 @ X0)) = ((sK14 @ X0))) & (c0 = ((sK15 @ X0))))) & (((X0 @ (sK15 @ X0) @ (sK14 @ X0) @ (sK16 @ X0))) != $true)) | (((X0 @ x @ y @ y)) = $true)) & ((((sK17 @ (cP @ x @ w) @ (cP @ y @ z) @ (cP @ y @ z))) != $true) & ! [X5 : a,X6 : a,X7 : a] : ((! [X8 : a,X9 : a,X10 : a,X11 : a,X12 : a,X13 : a] : ((((cP @ X13 @ X12)) != X7) | (((sK17 @ X10 @ X12 @ X8)) != $true) | (((cP @ X11 @ X10)) != X5) | ($true != ((sK17 @ X11 @ X13 @ X9))) | (((cP @ X9 @ X8)) != X6)) & ((X6 != X7) | (c0 != X5)) & ((c0 != X7) | (X5 != X6))) | ($true = ((sK17 @ X5 @ X7 @ X6))))) & ! [X14 : (a > a > a > $o)] : (($true = ((X14 @ w @ z @ z))) | ((($true = ((sP0 @ (sK19 @ X14) @ (sK20 @ X14) @ X14 @ (sK18 @ X14)))) | ((((sK20 @ X14)) = ((sK19 @ X14))) & (c0 = ((sK18 @ X14)))) | ((((sK20 @ X14)) = ((sK18 @ X14))) & (c0 = ((sK19 @ X14))))) & (((X14 @ (sK18 @ X14) @ (sK19 @ X14) @ (sK20 @ X14))) != $true)))),
% 27.49/4.44 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP,vAPP,vAPP,sK17,vAPP,vAPP,vAPP]),skolemize(X9,sK7 @ X3 @ X2 @ X1 @ X0),skolemize(X9,sK7 @ X3 @ X2 @ X1 @ X0),skolemize(X9,sK7 @ X3 @ X2 @ X1 @ X0),skolemize(X4,sK17),skolemize(X9,sK7 @ X3 @ X2 @ X1 @ X0),skolemize(X9,sK7 @ X3 @ X2 @ X1 @ X0),skolemize(X9,sK7 @ X3 @ X2 @ X1 @ X0)],[f17])).
% 27.49/4.44 thf(f19,plain,(
% 27.49/4.44 ( ! [X2 : a,X3 : a,X0 : (a > a > a > $o),X1 : a] : ((((cP @ (sK6 @ X3 @ X2 @ X1 @ X0) @ (sK2 @ X3 @ X2 @ X1 @ X0))) = X3) | (((sP1 @ X3 @ X2 @ X1 @ X0)) != $true)) )),
% 27.49/4.44 inference(cnf_transformation,[],[f13])).
% 27.49/4.44 thf(f20,plain,(
% 27.49/4.44 ( ! [X2 : a,X3 : a,X0 : (a > a > a > $o),X1 : a] : ((((cP @ (sK5 @ X3 @ X2 @ X1 @ X0) @ (sK3 @ X3 @ X2 @ X1 @ X0))) = X2) | (((sP1 @ X3 @ X2 @ X1 @ X0)) != $true)) )),
% 27.49/4.44 inference(cnf_transformation,[],[f13])).
% 27.49/4.44 thf(f21,plain,(
% 27.49/4.44 ( ! [X2 : a,X3 : a,X0 : (a > a > a > $o),X1 : a] : (($true = ((X0 @ (sK2 @ X3 @ X2 @ X1 @ X0) @ (sK3 @ X3 @ X2 @ X1 @ X0) @ (sK7 @ X3 @ X2 @ X1 @ X0)))) | (((sP1 @ X3 @ X2 @ X1 @ X0)) != $true)) )),
% 27.49/4.44 inference(cnf_transformation,[],[f13])).
% 27.49/4.44 thf(f22,plain,(
% 27.49/4.44 ( ! [X2 : a,X3 : a,X0 : (a > a > a > $o),X1 : a] : ((((cP @ (sK4 @ X3 @ X2 @ X1 @ X0) @ (sK7 @ X3 @ X2 @ X1 @ X0))) = X1) | (((sP1 @ X3 @ X2 @ X1 @ X0)) != $true)) )),
% 27.49/4.44 inference(cnf_transformation,[],[f13])).
% 27.49/4.44 thf(f23,plain,(
% 27.49/4.44 ( ! [X2 : a,X3 : a,X0 : (a > a > a > $o),X1 : a] : (($true = ((X0 @ (sK6 @ X3 @ X2 @ X1 @ X0) @ (sK5 @ X3 @ X2 @ X1 @ X0) @ (sK4 @ X3 @ X2 @ X1 @ X0)))) | (((sP1 @ X3 @ X2 @ X1 @ X0)) != $true)) )),
% 27.49/4.44 inference(cnf_transformation,[],[f13])).
% 27.49/4.44 thf(f24,plain,(
% 27.49/4.44 ( ! [X2 : a,X3 : a,X0 : a,X1 : (a > a > a > $o)] : ((((cP @ (sK13 @ X3 @ X2 @ X1 @ X0) @ (sK9 @ X3 @ X2 @ X1 @ X0))) = X3) | ($true != ((sP0 @ X3 @ X2 @ X1 @ X0)))) )),
% 27.49/4.44 inference(cnf_transformation,[],[f16])).
% 27.49/4.44 thf(f25,plain,(
% 27.49/4.44 ( ! [X2 : a,X3 : a,X0 : a,X1 : (a > a > a > $o)] : ((((cP @ (sK8 @ X3 @ X2 @ X1 @ X0) @ (sK11 @ X3 @ X2 @ X1 @ X0))) = X2) | ($true != ((sP0 @ X3 @ X2 @ X1 @ X0)))) )),
% 27.49/4.44 inference(cnf_transformation,[],[f16])).
% 27.49/4.44 thf(f26,plain,(
% 27.49/4.44 ( ! [X2 : a,X3 : a,X0 : a,X1 : (a > a > a > $o)] : (($true = ((X1 @ (sK10 @ X3 @ X2 @ X1 @ X0) @ (sK13 @ X3 @ X2 @ X1 @ X0) @ (sK8 @ X3 @ X2 @ X1 @ X0)))) | ($true != ((sP0 @ X3 @ X2 @ X1 @ X0)))) )),
% 27.49/4.44 inference(cnf_transformation,[],[f16])).
% 27.49/4.44 thf(f27,plain,(
% 27.49/4.44 ( ! [X2 : a,X3 : a,X0 : a,X1 : (a > a > a > $o)] : (($true = ((X1 @ (sK12 @ X3 @ X2 @ X1 @ X0) @ (sK9 @ X3 @ X2 @ X1 @ X0) @ (sK11 @ X3 @ X2 @ X1 @ X0)))) | ($true != ((sP0 @ X3 @ X2 @ X1 @ X0)))) )),
% 27.49/4.44 inference(cnf_transformation,[],[f16])).
% 27.49/4.44 thf(f28,plain,(
% 27.49/4.44 ( ! [X2 : a,X3 : a,X0 : a,X1 : (a > a > a > $o)] : ((((cP @ (sK10 @ X3 @ X2 @ X1 @ X0) @ (sK12 @ X3 @ X2 @ X1 @ X0))) = X0) | ($true != ((sP0 @ X3 @ X2 @ X1 @ X0)))) )),
% 27.49/4.44 inference(cnf_transformation,[],[f16])).
% 27.49/4.44 thf(f29,plain,(
% 27.49/4.44 ( ! [X14 : (a > a > a > $o)] : ((((X14 @ (sK18 @ X14) @ (sK19 @ X14) @ (sK20 @ X14))) != $true) | ($true = ((X14 @ w @ z @ z)))) )),
% 27.49/4.44 inference(cnf_transformation,[],[f18])).
% 27.49/4.44 thf(f30,plain,(
% 27.49/4.44 ( ! [X14 : (a > a > a > $o)] : (($true = ((sP0 @ (sK19 @ X14) @ (sK20 @ X14) @ X14 @ (sK18 @ X14)))) | (c0 = ((sK18 @ X14))) | ($true = ((X14 @ w @ z @ z))) | (c0 = ((sK19 @ X14)))) )),
% 27.49/4.44 inference(cnf_transformation,[],[f18])).
% 27.49/4.44 thf(f31,plain,(
% 27.49/4.44 ( ! [X14 : (a > a > a > $o)] : (($true = ((sP0 @ (sK19 @ X14) @ (sK20 @ X14) @ X14 @ (sK18 @ X14)))) | (((sK20 @ X14)) = ((sK18 @ X14))) | ($true = ((X14 @ w @ z @ z))) | (c0 = ((sK18 @ X14)))) )),
% 27.49/4.44 inference(cnf_transformation,[],[f18])).
% 27.49/4.44 thf(f32,plain,(
% 27.49/4.44 ( ! [X14 : (a > a > a > $o)] : (($true = ((sP0 @ (sK19 @ X14) @ (sK20 @ X14) @ X14 @ (sK18 @ X14)))) | (c0 = ((sK19 @ X14))) | ($true = ((X14 @ w @ z @ z))) | (((sK20 @ X14)) = ((sK19 @ X14)))) )),
% 27.49/4.44 inference(cnf_transformation,[],[f18])).
% 27.49/4.44 thf(f33,plain,(
% 27.49/4.44 ( ! [X14 : (a > a > a > $o)] : (($true = ((sP0 @ (sK19 @ X14) @ (sK20 @ X14) @ X14 @ (sK18 @ X14)))) | (((sK20 @ X14)) = ((sK18 @ X14))) | (((sK20 @ X14)) = ((sK19 @ X14))) | ($true = ((X14 @ w @ z @ z)))) )),
% 27.49/4.44 inference(cnf_transformation,[],[f18])).
% 27.49/4.44 thf(f34,plain,(
% 27.49/4.44 ( ! [X6 : a,X7 : a,X5 : a] : ((c0 != X7) | (X5 != X6) | ($true = ((sK17 @ X5 @ X7 @ X6)))) )),
% 27.49/4.44 inference(cnf_transformation,[],[f18])).
% 27.49/4.44 thf(f35,plain,(
% 27.49/4.44 ( ! [X6 : a,X7 : a,X5 : a] : ((X6 != X7) | (c0 != X5) | ($true = ((sK17 @ X5 @ X7 @ X6)))) )),
% 27.49/4.44 inference(cnf_transformation,[],[f18])).
% 27.49/4.44 thf(f36,plain,(
% 27.49/4.44 ( ! [X10 : a,X11 : a,X8 : a,X6 : a,X9 : a,X7 : a,X5 : a,X12 : a,X13 : a] : ((((cP @ X13 @ X12)) != X7) | (((sK17 @ X10 @ X12 @ X8)) != $true) | (((cP @ X11 @ X10)) != X5) | ($true != ((sK17 @ X11 @ X13 @ X9))) | (((cP @ X9 @ X8)) != X6) | ($true = ((sK17 @ X5 @ X7 @ X6)))) )),
% 27.49/4.44 inference(cnf_transformation,[],[f18])).
% 27.49/4.44 thf(f37,plain,(
% 27.49/4.44 (((sK17 @ (cP @ x @ w) @ (cP @ y @ z) @ (cP @ y @ z))) != $true)),
% 27.49/4.44 inference(cnf_transformation,[],[f18])).
% 27.49/4.44 thf(f38,plain,(
% 27.49/4.44 ( ! [X0 : (a > a > a > $o)] : ((((X0 @ (sK15 @ X0) @ (sK14 @ X0) @ (sK16 @ X0))) != $true) | (((X0 @ x @ y @ y)) = $true)) )),
% 27.49/4.44 inference(cnf_transformation,[],[f18])).
% 27.49/4.44 thf(f39,plain,(
% 27.49/4.44 ( ! [X0 : (a > a > a > $o)] : (($true = ((sP1 @ (sK15 @ X0) @ (sK14 @ X0) @ (sK16 @ X0) @ X0))) | (c0 = ((sK15 @ X0))) | (((X0 @ x @ y @ y)) = $true) | (((sK15 @ X0)) = ((sK16 @ X0)))) )),
% 27.49/4.44 inference(cnf_transformation,[],[f18])).
% 27.49/4.44 thf(f40,plain,(
% 27.49/4.44 ( ! [X0 : (a > a > a > $o)] : (($true = ((sP1 @ (sK15 @ X0) @ (sK14 @ X0) @ (sK16 @ X0) @ X0))) | (((X0 @ x @ y @ y)) = $true) | (((sK16 @ X0)) = ((sK14 @ X0))) | (((sK15 @ X0)) = ((sK16 @ X0)))) )),
% 27.49/4.44 inference(cnf_transformation,[],[f18])).
% 27.49/4.44 thf(f41,plain,(
% 27.49/4.44 ( ! [X0 : (a > a > a > $o)] : (($true = ((sP1 @ (sK15 @ X0) @ (sK14 @ X0) @ (sK16 @ X0) @ X0))) | (c0 = ((sK14 @ X0))) | (c0 = ((sK15 @ X0))) | (((X0 @ x @ y @ y)) = $true)) )),
% 27.49/4.44 inference(cnf_transformation,[],[f18])).
% 27.49/4.44 thf(f42,plain,(
% 27.49/4.44 ( ! [X0 : (a > a > a > $o)] : (($true = ((sP1 @ (sK15 @ X0) @ (sK14 @ X0) @ (sK16 @ X0) @ X0))) | (c0 = ((sK14 @ X0))) | (((sK16 @ X0)) = ((sK14 @ X0))) | (((X0 @ x @ y @ y)) = $true)) )),
% 27.49/4.44 inference(cnf_transformation,[],[f18])).
% 27.49/4.44 thf(f45,plain,(
% 27.49/4.44 ( ! [X10 : a,X11 : a,X8 : a,X6 : a,X9 : a,X5 : a,X12 : a,X13 : a] : ((((sK17 @ X10 @ X12 @ X8)) != $true) | (((cP @ X11 @ X10)) != X5) | ($true != ((sK17 @ X11 @ X13 @ X9))) | (((cP @ X9 @ X8)) != X6) | ($true = ((sK17 @ X5 @ (cP @ X13 @ X12) @ X6)))) )),
% 27.49/4.44 inference(equality_resolution,[],[f36])).
% 27.49/4.44 thf(f46,plain,(
% 27.49/4.44 ( ! [X10 : a,X11 : a,X8 : a,X6 : a,X9 : a,X12 : a,X13 : a] : ((((sK17 @ X10 @ X12 @ X8)) != $true) | ($true != ((sK17 @ X11 @ X13 @ X9))) | (((cP @ X9 @ X8)) != X6) | ($true = ((sK17 @ (cP @ X11 @ X10) @ (cP @ X13 @ X12) @ X6)))) )),
% 27.49/4.44 inference(equality_resolution,[],[f45])).
% 27.49/4.44 thf(f47,plain,(
% 27.49/4.44 ( ! [X10 : a,X11 : a,X8 : a,X9 : a,X12 : a,X13 : a] : ((((sK17 @ (cP @ X11 @ X10) @ (cP @ X13 @ X12) @ (cP @ X9 @ X8))) = $true) | ($true != ((sK17 @ X11 @ X13 @ X9))) | (((sK17 @ X10 @ X12 @ X8)) != $true)) )),
% 27.49/4.44 inference(equality_resolution,[],[f46])).
% 27.49/4.44 thf(f48,plain,(
% 27.49/4.44 ( ! [X7 : a,X5 : a] : ((c0 != X5) | ($true = ((sK17 @ X5 @ X7 @ X7)))) )),
% 27.49/4.44 inference(equality_resolution,[],[f35])).
% 27.49/4.44 thf(f49,plain,(
% 27.49/4.44 ( ! [X7 : a] : (($true = ((sK17 @ c0 @ X7 @ X7)))) )),
% 27.49/4.44 inference(equality_resolution,[],[f48])).
% 27.49/4.44 thf(f50,plain,(
% 27.49/4.44 ( ! [X6 : a,X5 : a] : ((X5 != X6) | ($true = ((sK17 @ X5 @ c0 @ X6)))) )),
% 27.49/4.44 inference(equality_resolution,[],[f34])).
% 27.49/4.44 thf(f51,plain,(
% 27.49/4.44 ( ! [X6 : a] : ((((sK17 @ X6 @ c0 @ X6)) = $true)) )),
% 27.49/4.44 inference(equality_resolution,[],[f50])).
% 27.49/4.44 thf(f54,plain,(
% 27.49/4.44 ($true != ((sK17 @ w @ z @ z))) | ($true != ((sK17 @ x @ y @ y))) | ($true != $true)),
% 27.49/4.44 inference(superposition,[],[f37,f47])).
% 27.49/4.44 thf(f55,plain,(
% 27.49/4.44 ($true != ((sK17 @ w @ z @ z))) | ($true != ((sK17 @ x @ y @ y)))),
% 27.49/4.44 inference(trivial_inequality_removal,[],[f54])).
% 27.49/4.44 thf(f57,definition,(
% 27.49/4.44 spl21_1 <=> ($true = ((sK17 @ x @ y @ y)))),
% 27.49/4.44 introduced(definition,[new_symbols(definition,[spl21_1])],[avatar_definition])).
% 27.49/4.44 thf(f59,plain,(
% 27.49/4.44 ($true != ((sK17 @ x @ y @ y))) | spl21_1),
% 27.49/4.44 inference(avatar_component_clause,[],[f57])).
% 27.49/4.44 thf(f61,definition,(
% 27.49/4.44 spl21_2 <=> ($true = ((sK17 @ w @ z @ z)))),
% 27.49/4.44 introduced(definition,[new_symbols(definition,[spl21_2])],[avatar_definition])).
% 27.49/4.44 thf(f63,plain,(
% 27.49/4.44 ($true != ((sK17 @ w @ z @ z))) | spl21_2),
% 27.49/4.44 inference(avatar_component_clause,[],[f61])).
% 27.49/4.44 thf(f64,plain,(
% 27.49/4.44 ~spl21_1 | ~spl21_2),
% 27.49/4.44 inference(avatar_split_clause,[],[f55,f61,f57])).
% 27.49/4.44 thf(f66,plain,(
% 27.49/4.44 ( ! [X2 : a,X3 : a,X0 : a,X1 : a,X6 : a,X7 : a,X4 : (a > a > a > $o),X5 : a] : (($true != ((sK17 @ X2 @ (sK9 @ X0 @ X3 @ X4 @ X5) @ X7))) | ($true != ((sP0 @ X0 @ X3 @ X4 @ X5))) | (((sK17 @ (cP @ X1 @ X2) @ X0 @ (cP @ X6 @ X7))) = $true) | ($true != ((sK17 @ X1 @ (sK13 @ X0 @ X3 @ X4 @ X5) @ X6)))) )),
% 27.49/4.44 inference(superposition,[],[f47,f24])).
% 27.49/4.44 thf(f90,plain,(
% 27.49/4.44 ( ! [X2 : a,X3 : (a > a > a > $o),X0 : a,X1 : a,X6 : a,X7 : a,X4 : a,X5 : a] : (($true != ((sK17 @ (sK6 @ X0 @ X1 @ X2 @ X3) @ X4 @ X6))) | ($true = ((sK17 @ X0 @ (cP @ X4 @ X5) @ (cP @ X6 @ X7)))) | ($true != ((sP1 @ X0 @ X1 @ X2 @ X3))) | ($true != ((sK17 @ (sK2 @ X0 @ X1 @ X2 @ X3) @ X5 @ X7)))) )),
% 27.49/4.44 inference(superposition,[],[f47,f19])).
% 27.49/4.44 thf(f137,plain,(
% 27.49/4.44 ( ! [X2 : a,X3 : a,X0 : a,X1 : a,X4 : a] : (($true != $true) | (((sK17 @ X3 @ (sK13 @ X0 @ X1 @ sK17 @ X2) @ X4)) != $true) | ($true = ((sK17 @ (cP @ X3 @ (sK12 @ X0 @ X1 @ sK17 @ X2)) @ X0 @ (cP @ X4 @ (sK11 @ X0 @ X1 @ sK17 @ X2))))) | ($true != ((sP0 @ X0 @ X1 @ sK17 @ X2))) | ($true != ((sP0 @ X0 @ X1 @ sK17 @ X2)))) )),
% 27.49/4.44 inference(superposition,[],[f66,f27])).
% 27.49/4.44 thf(f138,plain,(
% 27.49/4.44 ( ! [X2 : a,X3 : a,X0 : a,X1 : a,X4 : a] : (($true = ((sK17 @ (cP @ X3 @ (sK12 @ X0 @ X1 @ sK17 @ X2)) @ X0 @ (cP @ X4 @ (sK11 @ X0 @ X1 @ sK17 @ X2))))) | ($true != ((sP0 @ X0 @ X1 @ sK17 @ X2))) | ($true != $true) | (((sK17 @ X3 @ (sK13 @ X0 @ X1 @ sK17 @ X2) @ X4)) != $true)) )),
% 27.49/4.44 inference(duplicate_literal_removal,[],[f137])).
% 27.49/4.44 thf(f139,plain,(
% 27.49/4.44 ( ! [X2 : a,X3 : a,X0 : a,X1 : a,X4 : a] : (($true = ((sK17 @ (cP @ X3 @ (sK12 @ X0 @ X1 @ sK17 @ X2)) @ X0 @ (cP @ X4 @ (sK11 @ X0 @ X1 @ sK17 @ X2))))) | (((sK17 @ X3 @ (sK13 @ X0 @ X1 @ sK17 @ X2) @ X4)) != $true) | ($true != ((sP0 @ X0 @ X1 @ sK17 @ X2)))) )),
% 27.49/4.44 inference(trivial_inequality_removal,[],[f138])).
% 27.49/4.44 thf(f201,plain,(
% 27.49/4.44 ( ! [X2 : a,X3 : a,X0 : a,X1 : a,X4 : a] : (($true != ((sP1 @ X0 @ X1 @ X2 @ sK17))) | ($true != ((sK17 @ (sK2 @ X0 @ X1 @ X2 @ sK17) @ X3 @ X4))) | (((sK17 @ X0 @ (cP @ (sK5 @ X0 @ X1 @ X2 @ sK17) @ X3) @ (cP @ (sK4 @ X0 @ X1 @ X2 @ sK17) @ X4))) = $true) | ($true != $true) | ($true != ((sP1 @ X0 @ X1 @ X2 @ sK17)))) )),
% 27.49/4.44 inference(superposition,[],[f90,f23])).
% 27.49/4.44 thf(f204,plain,(
% 27.49/4.44 ( ! [X2 : a,X3 : a,X0 : a,X1 : a,X4 : a] : (($true != ((sP1 @ X0 @ X1 @ X2 @ sK17))) | ($true != $true) | ($true != ((sK17 @ (sK2 @ X0 @ X1 @ X2 @ sK17) @ X3 @ X4))) | (((sK17 @ X0 @ (cP @ (sK5 @ X0 @ X1 @ X2 @ sK17) @ X3) @ (cP @ (sK4 @ X0 @ X1 @ X2 @ sK17) @ X4))) = $true)) )),
% 27.49/4.44 inference(duplicate_literal_removal,[],[f201])).
% 27.49/4.44 thf(f205,plain,(
% 27.49/4.44 ( ! [X2 : a,X3 : a,X0 : a,X1 : a,X4 : a] : ((((sK17 @ X0 @ (cP @ (sK5 @ X0 @ X1 @ X2 @ sK17) @ X3) @ (cP @ (sK4 @ X0 @ X1 @ X2 @ sK17) @ X4))) = $true) | ($true != ((sK17 @ (sK2 @ X0 @ X1 @ X2 @ sK17) @ X3 @ X4))) | ($true != ((sP1 @ X0 @ X1 @ X2 @ sK17)))) )),
% 27.49/4.44 inference(trivial_inequality_removal,[],[f204])).
% 27.49/4.44 thf(f579,plain,(
% 27.49/4.44 ( ! [X2 : a,X3 : a,X0 : a,X1 : a] : ((((sK17 @ (cP @ X1 @ (sK12 @ X2 @ X0 @ sK17 @ X3)) @ X2 @ X0)) = $true) | (((sP0 @ X2 @ X0 @ sK17 @ X3)) != $true) | (((sP0 @ X2 @ X0 @ sK17 @ X3)) != $true) | ($true != ((sK17 @ X1 @ (sK13 @ X2 @ X0 @ sK17 @ X3) @ (sK8 @ X2 @ X0 @ sK17 @ X3))))) )),
% 27.49/4.44 inference(superposition,[],[f139,f25])).
% 27.49/4.44 thf(f587,plain,(
% 27.49/4.44 ( ! [X2 : a,X3 : a,X0 : a,X1 : a] : (($true != ((sK17 @ X1 @ (sK13 @ X2 @ X0 @ sK17 @ X3) @ (sK8 @ X2 @ X0 @ sK17 @ X3)))) | (((sK17 @ (cP @ X1 @ (sK12 @ X2 @ X0 @ sK17 @ X3)) @ X2 @ X0)) = $true) | (((sP0 @ X2 @ X0 @ sK17 @ X3)) != $true)) )),
% 27.49/4.44 inference(duplicate_literal_removal,[],[f579])).
% 27.49/4.44 thf(f647,plain,(
% 27.49/4.44 ( ! [X2 : a,X3 : a,X0 : a,X1 : a] : (($true != ((sP1 @ X1 @ X2 @ X0 @ sK17))) | ($true != ((sP1 @ X1 @ X2 @ X0 @ sK17))) | (((sK17 @ (sK2 @ X1 @ X2 @ X0 @ sK17) @ X3 @ (sK7 @ X1 @ X2 @ X0 @ sK17))) != $true) | ($true = ((sK17 @ X1 @ (cP @ (sK5 @ X1 @ X2 @ X0 @ sK17) @ X3) @ X0)))) )),
% 27.49/4.44 inference(superposition,[],[f205,f22])).
% 27.49/4.44 thf(f656,plain,(
% 27.49/4.44 ( ! [X2 : a,X3 : a,X0 : a,X1 : a] : ((((sK17 @ (sK2 @ X1 @ X2 @ X0 @ sK17) @ X3 @ (sK7 @ X1 @ X2 @ X0 @ sK17))) != $true) | ($true = ((sK17 @ X1 @ (cP @ (sK5 @ X1 @ X2 @ X0 @ sK17) @ X3) @ X0))) | ($true != ((sP1 @ X1 @ X2 @ X0 @ sK17)))) )),
% 27.49/4.44 inference(duplicate_literal_removal,[],[f647])).
% 27.49/4.44 thf(f719,plain,(
% 27.49/4.44 ( ! [X2 : a,X0 : a,X1 : a] : (($true != ((sP0 @ X0 @ X1 @ sK17 @ X2))) | ($true != $true) | ($true != ((sP0 @ X0 @ X1 @ sK17 @ X2))) | (((sK17 @ (cP @ (sK10 @ X0 @ X1 @ sK17 @ X2) @ (sK12 @ X0 @ X1 @ sK17 @ X2)) @ X0 @ X1)) = $true)) )),
% 27.49/4.44 inference(superposition,[],[f587,f26])).
% 27.49/4.44 thf(f720,plain,(
% 27.49/4.44 ( ! [X2 : a,X0 : a,X1 : a] : (($true != $true) | (((sK17 @ (cP @ (sK10 @ X0 @ X1 @ sK17 @ X2) @ (sK12 @ X0 @ X1 @ sK17 @ X2)) @ X0 @ X1)) = $true) | ($true != ((sP0 @ X0 @ X1 @ sK17 @ X2)))) )),
% 27.49/4.44 inference(duplicate_literal_removal,[],[f719])).
% 27.49/4.44 thf(f721,plain,(
% 27.49/4.44 ( ! [X2 : a,X0 : a,X1 : a] : ((((sK17 @ (cP @ (sK10 @ X0 @ X1 @ sK17 @ X2) @ (sK12 @ X0 @ X1 @ sK17 @ X2)) @ X0 @ X1)) = $true) | ($true != ((sP0 @ X0 @ X1 @ sK17 @ X2)))) )),
% 27.49/4.44 inference(trivial_inequality_removal,[],[f720])).
% 27.49/4.44 thf(f722,plain,(
% 27.49/4.44 ( ! [X2 : a,X0 : a,X1 : a] : ((((sP0 @ X1 @ X2 @ sK17 @ X0)) != $true) | ($true = ((sK17 @ X0 @ X1 @ X2))) | (((sP0 @ X1 @ X2 @ sK17 @ X0)) != $true)) )),
% 27.49/4.44 inference(superposition,[],[f721,f28])).
% 27.49/4.44 thf(f767,plain,(
% 27.49/4.44 ( ! [X2 : a,X0 : a,X1 : a] : ((((sP0 @ X1 @ X2 @ sK17 @ X0)) != $true) | ($true = ((sK17 @ X0 @ X1 @ X2)))) )),
% 27.49/4.44 inference(duplicate_literal_removal,[],[f722])).
% 27.49/4.44 thf(f772,plain,(
% 27.49/4.44 (((sK20 @ sK17)) = ((sK19 @ sK17))) | (((sK20 @ sK17)) = ((sK18 @ sK17))) | ($true = ((sK17 @ w @ z @ z))) | ($true = ((sK17 @ (sK18 @ sK17) @ (sK19 @ sK17) @ (sK20 @ sK17)))) | ($true != $true)),
% 27.49/4.44 inference(superposition,[],[f767,f33])).
% 27.49/4.44 thf(f773,plain,(
% 27.49/4.44 (((sK20 @ sK17)) = ((sK19 @ sK17))) | ($true = ((sK17 @ (sK18 @ sK17) @ (sK19 @ sK17) @ (sK20 @ sK17)))) | ($true = ((sK17 @ w @ z @ z))) | (c0 = ((sK19 @ sK17))) | ($true != $true)),
% 27.49/4.44 inference(superposition,[],[f767,f32])).
% 27.49/4.44 thf(f774,plain,(
% 27.49/4.44 ($true = ((sK17 @ w @ z @ z))) | ($true = ((sK17 @ (sK18 @ sK17) @ (sK19 @ sK17) @ (sK20 @ sK17)))) | ($true != $true) | (((sK20 @ sK17)) = ((sK18 @ sK17))) | (c0 = ((sK18 @ sK17)))),
% 27.49/4.44 inference(superposition,[],[f767,f31])).
% 27.49/4.44 thf(f775,plain,(
% 27.49/4.44 ($true != $true) | (c0 = ((sK19 @ sK17))) | ($true = ((sK17 @ (sK18 @ sK17) @ (sK19 @ sK17) @ (sK20 @ sK17)))) | (c0 = ((sK18 @ sK17))) | ($true = ((sK17 @ w @ z @ z)))),
% 27.49/4.44 inference(superposition,[],[f767,f30])).
% 27.49/4.44 thf(f776,plain,(
% 27.49/4.44 ($true = ((sK17 @ w @ z @ z))) | ($true = ((sK17 @ (sK18 @ sK17) @ (sK19 @ sK17) @ (sK20 @ sK17)))) | (((sK20 @ sK17)) = ((sK18 @ sK17))) | (((sK20 @ sK17)) = ((sK19 @ sK17)))),
% 27.49/4.44 inference(trivial_inequality_removal,[],[f772])).
% 27.49/4.44 thf(f777,plain,(
% 27.49/4.44 (c0 = ((sK18 @ sK17))) | (((sK20 @ sK17)) = ((sK18 @ sK17))) | ($true = ((sK17 @ (sK18 @ sK17) @ (sK19 @ sK17) @ (sK20 @ sK17)))) | ($true = ((sK17 @ w @ z @ z)))),
% 27.49/4.44 inference(trivial_inequality_removal,[],[f774])).
% 27.49/4.44 thf(f778,plain,(
% 27.49/4.44 (((sK20 @ sK17)) = ((sK19 @ sK17))) | (c0 = ((sK19 @ sK17))) | ($true = ((sK17 @ w @ z @ z))) | ($true = ((sK17 @ (sK18 @ sK17) @ (sK19 @ sK17) @ (sK20 @ sK17))))),
% 27.49/4.44 inference(trivial_inequality_removal,[],[f773])).
% 27.49/4.44 thf(f779,plain,(
% 27.49/4.44 ($true = ((sK17 @ w @ z @ z))) | (c0 = ((sK19 @ sK17))) | (c0 = ((sK18 @ sK17))) | ($true = ((sK17 @ (sK18 @ sK17) @ (sK19 @ sK17) @ (sK20 @ sK17))))),
% 27.49/4.44 inference(trivial_inequality_removal,[],[f775])).
% 27.49/4.44 thf(f780,plain,(
% 27.49/4.44 ($true = ((sK17 @ w @ z @ z))) | (((sK20 @ sK17)) = ((sK19 @ sK17))) | (((sK20 @ sK17)) = ((sK18 @ sK17)))),
% 27.49/4.44 inference(forward_subsumption_resolution,[],[f776,f29])).
% 27.49/4.44 thf(f781,plain,(
% 27.49/4.44 ($true = ((sK17 @ w @ z @ z))) | (((sK20 @ sK17)) = ((sK18 @ sK17))) | (c0 = ((sK18 @ sK17)))),
% 27.49/4.44 inference(forward_subsumption_resolution,[],[f777,f29])).
% 27.49/4.44 thf(f782,plain,(
% 27.49/4.44 ($true = ((sK17 @ w @ z @ z))) | (((sK20 @ sK17)) = ((sK19 @ sK17))) | (c0 = ((sK19 @ sK17)))),
% 27.49/4.44 inference(forward_subsumption_resolution,[],[f778,f29])).
% 27.49/4.44 thf(f783,plain,(
% 27.49/4.44 (c0 = ((sK19 @ sK17))) | (c0 = ((sK18 @ sK17))) | ($true = ((sK17 @ w @ z @ z)))),
% 27.49/4.44 inference(forward_subsumption_resolution,[],[f779,f29])).
% 27.49/4.44 thf(f785,definition,(
% 27.49/4.44 spl21_3 <=> (((sK20 @ sK17)) = ((sK18 @ sK17)))),
% 27.49/4.44 introduced(definition,[new_symbols(definition,[spl21_3])],[avatar_definition])).
% 27.49/4.44 thf(f787,plain,(
% 27.49/4.44 (((sK20 @ sK17)) = ((sK18 @ sK17))) | ~spl21_3),
% 27.49/4.44 inference(avatar_component_clause,[],[f785])).
% 27.49/4.44 thf(f789,definition,(
% 27.49/4.44 spl21_4 <=> (((sK20 @ sK17)) = ((sK19 @ sK17)))),
% 27.49/4.44 introduced(definition,[new_symbols(definition,[spl21_4])],[avatar_definition])).
% 27.49/4.44 thf(f791,plain,(
% 27.49/4.44 (((sK20 @ sK17)) = ((sK19 @ sK17))) | ~spl21_4),
% 27.49/4.44 inference(avatar_component_clause,[],[f789])).
% 27.49/4.44 thf(f792,plain,(
% 27.49/4.44 spl21_3 | spl21_2 | spl21_4),
% 27.49/4.44 inference(avatar_split_clause,[],[f780,f789,f61,f785])).
% 27.49/4.44 thf(f794,definition,(
% 27.49/4.44 spl21_5 <=> (c0 = ((sK18 @ sK17)))),
% 27.49/4.44 introduced(definition,[new_symbols(definition,[spl21_5])],[avatar_definition])).
% 27.49/4.44 thf(f796,plain,(
% 27.49/4.44 (c0 = ((sK18 @ sK17))) | ~spl21_5),
% 27.49/4.44 inference(avatar_component_clause,[],[f794])).
% 27.49/4.44 thf(f797,plain,(
% 27.49/4.44 spl21_5 | spl21_3 | spl21_2),
% 27.49/4.44 inference(avatar_split_clause,[],[f781,f61,f785,f794])).
% 27.49/4.44 thf(f799,definition,(
% 27.49/4.44 spl21_6 <=> (c0 = ((sK19 @ sK17)))),
% 27.49/4.44 introduced(definition,[new_symbols(definition,[spl21_6])],[avatar_definition])).
% 27.49/4.44 thf(f801,plain,(
% 27.49/4.44 (c0 = ((sK19 @ sK17))) | ~spl21_6),
% 27.49/4.44 inference(avatar_component_clause,[],[f799])).
% 27.49/4.44 thf(f802,plain,(
% 27.49/4.44 spl21_4 | spl21_2 | spl21_6),
% 27.49/4.44 inference(avatar_split_clause,[],[f782,f799,f61,f789])).
% 27.49/4.44 thf(f803,plain,(
% 27.49/4.44 spl21_6 | spl21_2 | spl21_5),
% 27.49/4.44 inference(avatar_split_clause,[],[f783,f794,f61,f799])).
% 27.49/4.44 thf(f830,plain,(
% 27.49/4.44 ($true = ((sK17 @ w @ z @ z))) | ($true != ((sK17 @ (sK18 @ sK17) @ (sK19 @ sK17) @ (sK19 @ sK17)))) | ~spl21_4),
% 27.49/4.44 inference(superposition,[],[f29,f791])).
% 27.49/4.44 thf(f837,plain,(
% 27.49/4.44 ($true != ((sK17 @ c0 @ (sK19 @ sK17) @ (sK19 @ sK17)))) | ($true = ((sK17 @ w @ z @ z))) | (~spl21_4 | ~spl21_5)),
% 27.49/4.44 inference(forward_demodulation,[],[f830,f796])).
% 27.49/4.44 thf(f838,plain,(
% 27.49/4.44 ($true = ((sK17 @ w @ z @ z))) | (~spl21_4 | ~spl21_5)),
% 27.49/4.44 inference(forward_subsumption_resolution,[],[f837,f49])).
% 27.49/4.44 thf(f839,plain,(
% 27.49/4.44 spl21_2 | ~spl21_4 | ~spl21_5),
% 27.49/4.44 inference(avatar_split_clause,[],[f838,f794,f789,f61])).
% 27.49/4.44 thf(f878,plain,(
% 27.49/4.44 ( ! [X2 : a,X0 : a,X1 : a] : (($true != $true) | ($true != ((sP1 @ X0 @ X1 @ X2 @ sK17))) | ($true != ((sP1 @ X0 @ X1 @ X2 @ sK17))) | ($true = ((sK17 @ X0 @ (cP @ (sK5 @ X0 @ X1 @ X2 @ sK17) @ (sK3 @ X0 @ X1 @ X2 @ sK17)) @ X2)))) )),
% 27.49/4.44 inference(superposition,[],[f656,f21])).
% 27.49/4.44 thf(f879,plain,(
% 27.49/4.44 ( ! [X2 : a,X0 : a,X1 : a] : (($true = ((sK17 @ X0 @ (cP @ (sK5 @ X0 @ X1 @ X2 @ sK17) @ (sK3 @ X0 @ X1 @ X2 @ sK17)) @ X2))) | ($true != ((sP1 @ X0 @ X1 @ X2 @ sK17))) | ($true != $true)) )),
% 27.49/4.44 inference(duplicate_literal_removal,[],[f878])).
% 27.49/4.44 thf(f880,plain,(
% 27.49/4.44 ( ! [X2 : a,X0 : a,X1 : a] : (($true = ((sK17 @ X0 @ (cP @ (sK5 @ X0 @ X1 @ X2 @ sK17) @ (sK3 @ X0 @ X1 @ X2 @ sK17)) @ X2))) | ($true != ((sP1 @ X0 @ X1 @ X2 @ sK17)))) )),
% 27.49/4.44 inference(trivial_inequality_removal,[],[f879])).
% 27.49/4.44 thf(f951,plain,(
% 27.49/4.44 ( ! [X2 : a,X0 : a,X1 : a] : ((((sK17 @ X1 @ X0 @ X2)) = $true) | ($true != ((sP1 @ X1 @ X0 @ X2 @ sK17))) | ($true != ((sP1 @ X1 @ X0 @ X2 @ sK17)))) )),
% 27.49/4.44 inference(superposition,[],[f880,f20])).
% 27.49/4.44 thf(f995,plain,(
% 27.49/4.44 ( ! [X2 : a,X0 : a,X1 : a] : (($true != ((sP1 @ X1 @ X0 @ X2 @ sK17))) | (((sK17 @ X1 @ X0 @ X2)) = $true)) )),
% 27.49/4.44 inference(duplicate_literal_removal,[],[f951])).
% 27.49/4.44 thf(f1003,plain,(
% 27.49/4.44 ($true != $true) | ($true = ((sK17 @ x @ y @ y))) | (((sK16 @ sK17)) = ((sK15 @ sK17))) | ($true = ((sK17 @ (sK15 @ sK17) @ (sK14 @ sK17) @ (sK16 @ sK17)))) | (((sK16 @ sK17)) = ((sK14 @ sK17)))),
% 27.49/4.44 inference(superposition,[],[f995,f40])).
% 27.49/4.44 thf(f1004,plain,(
% 27.49/4.44 (c0 = ((sK14 @ sK17))) | ($true != $true) | ($true = ((sK17 @ x @ y @ y))) | ($true = ((sK17 @ (sK15 @ sK17) @ (sK14 @ sK17) @ (sK16 @ sK17)))) | (((sK16 @ sK17)) = ((sK14 @ sK17)))),
% 27.49/4.44 inference(superposition,[],[f995,f42])).
% 27.49/4.44 thf(f1005,plain,(
% 27.49/4.44 (c0 = ((sK15 @ sK17))) | ($true != $true) | (((sK16 @ sK17)) = ((sK15 @ sK17))) | ($true = ((sK17 @ x @ y @ y))) | ($true = ((sK17 @ (sK15 @ sK17) @ (sK14 @ sK17) @ (sK16 @ sK17))))),
% 27.49/4.44 inference(superposition,[],[f995,f39])).
% 27.49/4.44 thf(f1006,plain,(
% 27.49/4.44 (c0 = ((sK15 @ sK17))) | (c0 = ((sK14 @ sK17))) | ($true = ((sK17 @ x @ y @ y))) | ($true != $true) | ($true = ((sK17 @ (sK15 @ sK17) @ (sK14 @ sK17) @ (sK16 @ sK17))))),
% 27.49/4.44 inference(superposition,[],[f995,f41])).
% 27.49/4.44 thf(f1007,plain,(
% 27.49/4.44 (c0 = ((sK15 @ sK17))) | ($true = ((sK17 @ (sK15 @ sK17) @ (sK14 @ sK17) @ (sK16 @ sK17)))) | ($true = ((sK17 @ x @ y @ y))) | (c0 = ((sK14 @ sK17)))),
% 27.49/4.44 inference(trivial_inequality_removal,[],[f1006])).
% 27.49/4.44 thf(f1008,plain,(
% 27.49/4.44 ($true = ((sK17 @ (sK15 @ sK17) @ (sK14 @ sK17) @ (sK16 @ sK17)))) | (((sK16 @ sK17)) = ((sK15 @ sK17))) | ($true = ((sK17 @ x @ y @ y))) | (c0 = ((sK15 @ sK17)))),
% 27.49/4.44 inference(trivial_inequality_removal,[],[f1005])).
% 27.49/4.44 thf(f1009,plain,(
% 27.49/4.44 ($true = ((sK17 @ (sK15 @ sK17) @ (sK14 @ sK17) @ (sK16 @ sK17)))) | (c0 = ((sK14 @ sK17))) | (((sK16 @ sK17)) = ((sK14 @ sK17))) | ($true = ((sK17 @ x @ y @ y)))),
% 27.49/4.44 inference(trivial_inequality_removal,[],[f1004])).
% 27.49/4.44 thf(f1010,plain,(
% 27.49/4.44 (((sK16 @ sK17)) = ((sK14 @ sK17))) | ($true = ((sK17 @ (sK15 @ sK17) @ (sK14 @ sK17) @ (sK16 @ sK17)))) | ($true = ((sK17 @ x @ y @ y))) | (((sK16 @ sK17)) = ((sK15 @ sK17)))),
% 27.49/4.44 inference(trivial_inequality_removal,[],[f1003])).
% 27.49/4.44 thf(f1011,plain,(
% 27.49/4.44 (c0 = ((sK14 @ sK17))) | (c0 = ((sK15 @ sK17))) | ($true = ((sK17 @ x @ y @ y)))),
% 27.49/4.44 inference(forward_subsumption_resolution,[],[f1007,f38])).
% 27.49/4.44 thf(f1013,plain,(
% 27.49/4.44 (c0 = ((sK14 @ sK17))) | (((sK16 @ sK17)) = ((sK14 @ sK17))) | ($true = ((sK17 @ x @ y @ y)))),
% 27.49/4.44 inference(forward_subsumption_resolution,[],[f1009,f38])).
% 27.49/4.44 thf(f1014,plain,(
% 27.49/4.44 (((sK16 @ sK17)) = ((sK15 @ sK17))) | (((sK16 @ sK17)) = ((sK14 @ sK17))) | ($true = ((sK17 @ x @ y @ y)))),
% 27.49/4.44 inference(forward_subsumption_resolution,[],[f1010,f38])).
% 27.49/4.44 thf(f1017,definition,(
% 27.49/4.44 spl21_10 <=> (c0 = ((sK15 @ sK17)))),
% 27.49/4.44 introduced(definition,[new_symbols(definition,[spl21_10])],[avatar_definition])).
% 27.49/4.44 thf(f1019,plain,(
% 27.49/4.44 (c0 = ((sK15 @ sK17))) | ~spl21_10),
% 27.49/4.44 inference(avatar_component_clause,[],[f1017])).
% 27.49/4.44 thf(f1021,definition,(
% 27.49/4.44 spl21_11 <=> (((sK16 @ sK17)) = ((sK15 @ sK17)))),
% 27.49/4.44 introduced(definition,[new_symbols(definition,[spl21_11])],[avatar_definition])).
% 27.49/4.44 thf(f1023,plain,(
% 27.49/4.44 (((sK16 @ sK17)) = ((sK15 @ sK17))) | ~spl21_11),
% 27.49/4.44 inference(avatar_component_clause,[],[f1021])).
% 27.49/4.44 thf(f1032,definition,(
% 27.49/4.44 spl21_13 <=> (c0 = ((sK14 @ sK17)))),
% 27.49/4.44 introduced(definition,[new_symbols(definition,[spl21_13])],[avatar_definition])).
% 27.49/4.44 thf(f1034,plain,(
% 27.49/4.44 (c0 = ((sK14 @ sK17))) | ~spl21_13),
% 27.49/4.44 inference(avatar_component_clause,[],[f1032])).
% 27.49/4.44 thf(f1037,definition,(
% 27.49/4.44 spl21_14 <=> (((sK16 @ sK17)) = ((sK14 @ sK17)))),
% 27.49/4.44 introduced(definition,[new_symbols(definition,[spl21_14])],[avatar_definition])).
% 27.49/4.44 thf(f1039,plain,(
% 27.49/4.44 (((sK16 @ sK17)) = ((sK14 @ sK17))) | ~spl21_14),
% 27.49/4.44 inference(avatar_component_clause,[],[f1037])).
% 27.49/4.44 thf(f1393,plain,(
% 27.49/4.44 ($true = ((sK17 @ w @ z @ z))) | ($true != ((sK17 @ (sK18 @ sK17) @ (sK19 @ sK17) @ (sK18 @ sK17)))) | ~spl21_3),
% 27.49/4.44 inference(superposition,[],[f29,f787])).
% 27.49/4.44 thf(f1400,plain,(
% 27.49/4.44 ($true != ((sK17 @ (sK18 @ sK17) @ (sK19 @ sK17) @ (sK18 @ sK17)))) | (spl21_2 | ~spl21_3)),
% 27.49/4.44 inference(forward_subsumption_resolution,[],[f1393,f63])).
% 27.49/4.44 thf(f1401,plain,(
% 27.49/4.44 ($true != ((sK17 @ (sK18 @ sK17) @ c0 @ (sK18 @ sK17)))) | (spl21_2 | ~spl21_3 | ~spl21_6)),
% 27.49/4.44 inference(forward_demodulation,[],[f1400,f801])).
% 27.49/4.44 thf(f1402,plain,(
% 27.49/4.44 $false | (spl21_2 | ~spl21_3 | ~spl21_6)),
% 27.49/4.44 inference(forward_subsumption_resolution,[],[f1401,f51])).
% 27.49/4.44 thf(f1403,plain,(
% 27.49/4.44 spl21_2 | ~spl21_3 | ~spl21_6),
% 27.49/4.44 inference(avatar_contradiction_clause,[],[f1402])).
% 27.49/4.44 thf(f1449,plain,(
% 27.49/4.44 ($true != ((sK17 @ (sK15 @ sK17) @ (sK16 @ sK17) @ (sK16 @ sK17)))) | ($true = ((sK17 @ x @ y @ y))) | ~spl21_14),
% 27.49/4.44 inference(superposition,[],[f38,f1039])).
% 27.49/4.44 thf(f1454,plain,(
% 27.49/4.44 ($true != ((sK17 @ (sK15 @ sK17) @ (sK16 @ sK17) @ (sK16 @ sK17)))) | (spl21_1 | ~spl21_14)),
% 27.49/4.44 inference(forward_subsumption_resolution,[],[f1449,f59])).
% 27.49/4.44 thf(f1455,plain,(
% 27.49/4.44 ($true != ((sK17 @ c0 @ (sK16 @ sK17) @ (sK16 @ sK17)))) | (spl21_1 | ~spl21_10 | ~spl21_14)),
% 27.49/4.44 inference(forward_demodulation,[],[f1454,f1019])).
% 27.49/4.44 thf(f1456,plain,(
% 27.49/4.44 $false | (spl21_1 | ~spl21_10 | ~spl21_14)),
% 27.49/4.44 inference(forward_subsumption_resolution,[],[f1455,f49])).
% 27.49/4.44 thf(f1457,plain,(
% 27.49/4.44 spl21_1 | ~spl21_10 | ~spl21_14),
% 27.49/4.44 inference(avatar_contradiction_clause,[],[f1456])).
% 27.49/4.44 thf(f1458,plain,(
% 27.49/4.44 (c0 = ((sK14 @ sK17))) | (c0 = ((sK15 @ sK17))) | spl21_1),
% 27.49/4.44 inference(forward_subsumption_resolution,[],[f1011,f59])).
% 27.49/4.44 thf(f1459,plain,(
% 27.49/4.44 (((sK16 @ sK17)) = ((sK14 @ sK17))) | (((sK16 @ sK17)) = ((sK15 @ sK17))) | spl21_1),
% 27.49/4.44 inference(forward_subsumption_resolution,[],[f1014,f59])).
% 27.49/4.44 thf(f1460,plain,(
% 27.49/4.44 (c0 = ((sK14 @ sK17))) | (((sK16 @ sK17)) = ((sK14 @ sK17))) | spl21_1),
% 27.49/4.44 inference(forward_subsumption_resolution,[],[f1013,f59])).
% 27.49/4.44 thf(f1461,plain,(
% 27.49/4.44 ($true = ((sK17 @ x @ y @ y))) | (((sK16 @ sK17)) = ((sK15 @ sK17))) | (c0 = ((sK15 @ sK17)))),
% 27.49/4.44 inference(forward_subsumption_resolution,[],[f1008,f38])).
% 27.49/4.44 thf(f1462,plain,(
% 27.49/4.44 spl21_13 | spl21_10 | spl21_1),
% 27.49/4.44 inference(avatar_split_clause,[],[f1458,f57,f1017,f1032])).
% 27.49/4.44 thf(f1463,plain,(
% 27.49/4.44 spl21_14 | spl21_11 | spl21_1),
% 27.49/4.44 inference(avatar_split_clause,[],[f1459,f57,f1021,f1037])).
% 27.49/4.44 thf(f1464,plain,(
% 27.49/4.44 spl21_14 | spl21_13 | spl21_1),
% 27.49/4.44 inference(avatar_split_clause,[],[f1460,f57,f1032,f1037])).
% 27.49/4.44 thf(f1465,plain,(
% 27.49/4.44 (c0 = ((sK15 @ sK17))) | (((sK16 @ sK17)) = ((sK15 @ sK17))) | spl21_1),
% 27.49/4.44 inference(forward_subsumption_resolution,[],[f1461,f59])).
% 27.49/4.44 thf(f1466,plain,(
% 27.49/4.44 spl21_11 | spl21_10 | spl21_1),
% 27.49/4.44 inference(avatar_split_clause,[],[f1465,f57,f1017,f1021])).
% 27.49/4.44 thf(f1534,plain,(
% 27.49/4.44 ($true = ((sK17 @ x @ y @ y))) | ($true != ((sK17 @ (sK16 @ sK17) @ (sK14 @ sK17) @ (sK16 @ sK17)))) | ~spl21_11),
% 27.49/4.44 inference(superposition,[],[f38,f1023])).
% 27.49/4.44 thf(f1539,plain,(
% 27.49/4.44 ($true != ((sK17 @ (sK16 @ sK17) @ (sK14 @ sK17) @ (sK16 @ sK17)))) | (spl21_1 | ~spl21_11)),
% 27.49/4.44 inference(forward_subsumption_resolution,[],[f1534,f59])).
% 27.49/4.44 thf(f1540,plain,(
% 27.49/4.44 ($true != ((sK17 @ (sK16 @ sK17) @ c0 @ (sK16 @ sK17)))) | (spl21_1 | ~spl21_11 | ~spl21_13)),
% 27.49/4.44 inference(forward_demodulation,[],[f1539,f1034])).
% 27.49/4.44 thf(f1541,plain,(
% 27.49/4.44 $false | (spl21_1 | ~spl21_11 | ~spl21_13)),
% 27.49/4.44 inference(forward_subsumption_resolution,[],[f1540,f51])).
% 27.49/4.44 thf(f1542,plain,(
% 27.49/4.44 spl21_1 | ~spl21_11 | ~spl21_13),
% 27.49/4.44 inference(avatar_contradiction_clause,[],[f1541])).
% 27.49/4.44 cnf(s1, plain, ~spl21_1 | ~spl21_2, inference(sat_conversion,[],[f64])).
% 27.49/4.44 cnf(s2, plain, spl21_2 | spl21_3 | spl21_4, inference(sat_conversion,[],[f792])).
% 27.49/4.44 cnf(s3, plain, spl21_2 | spl21_3 | spl21_5, inference(sat_conversion,[],[f797])).
% 27.49/4.44 cnf(s4, plain, spl21_2 | spl21_4 | spl21_6, inference(sat_conversion,[],[f802])).
% 27.49/4.44 cnf(s5, plain, spl21_2 | spl21_5 | spl21_6, inference(sat_conversion,[],[f803])).
% 27.49/4.44 cnf(s9, plain, spl21_2 | ~spl21_4 | ~spl21_5, inference(sat_conversion,[],[f839])).
% 27.49/4.44 cnf(s46, plain, spl21_2 | ~spl21_3 | ~spl21_6, inference(sat_conversion,[],[f1403])).
% 27.49/4.44 cnf(s58, plain, spl21_1 | ~spl21_10 | ~spl21_14, inference(sat_conversion,[],[f1457])).
% 27.49/4.44 cnf(s59, plain, spl21_1 | spl21_10 | spl21_13, inference(sat_conversion,[],[f1462])).
% 27.49/4.44 cnf(s60, plain, spl21_1 | spl21_11 | spl21_14, inference(sat_conversion,[],[f1463])).
% 27.49/4.44 cnf(s61, plain, spl21_1 | spl21_13 | spl21_14, inference(sat_conversion,[],[f1464])).
% 27.49/4.44 cnf(s62, plain, spl21_1 | spl21_10 | spl21_11, inference(sat_conversion,[],[f1466])).
% 27.49/4.44 cnf(s65, plain, spl21_1 | ~spl21_11 | ~spl21_13, inference(sat_conversion,[],[f1542])).
% 27.49/4.44 cnf(s66, plain, spl21_3 | spl21_2, inference(rat,[],[s9,s2,s3])).
% 27.49/4.44 cnf(s67, plain, spl21_6 | spl21_2, inference(rat,[],[s9,s4,s5])).
% 27.49/4.44 cnf(s68, plain, ~spl21_3 | spl21_2, inference(rat,[],[s67,s46])).
% 27.49/4.44 cnf(s69, plain, spl21_2, inference(rat,[],[s68,s66])).
% 27.49/4.44 cnf(s70, plain, spl21_10 | spl21_1, inference(rat,[],[s65,s59,s62])).
% 27.49/4.44 cnf(s71, plain, spl21_14 | spl21_1, inference(rat,[],[s65,s61,s60])).
% 27.49/4.44 cnf(s72, plain, ~spl21_10 | spl21_1, inference(rat,[],[s71,s58])).
% 27.49/4.44 cnf(s73, plain, spl21_1, inference(rat,[],[s72,s70])).
% 27.49/4.44 cnf(s74, plain, $false, inference(rat,[],[s1,s69,s73])).
% 27.49/4.44 thf(f1543,plain,(
% 27.49/4.44 $false),
% 27.49/4.44 inference(avatar_sat_refutation,[],[s74])).
% 27.49/4.44 % SZS output end Proof for theBenchmark
% 27.49/4.44 % (213722)------------------------------
% 27.49/4.44 % (213722)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.49/4.44 % (213722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.49/4.44 % (213722)CaDiCaL version: 2.1.3
% 27.49/4.44 % (213722)Termination reason: Refutation
% 27.49/4.44 % (213722)Time elapsed: 0.153 s
% 27.49/4.44 % (213722)Peak memory usage: 16 MB
% 27.49/4.44 % (213722)Instructions burned: 552 (million)
% 27.49/4.44 % (213421)Success in time 4.179 s
% 27.49/4.44 % Vampire exiting
%------------------------------------------------------------------------------