%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : DAT286^1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n016.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 07:48:42 AM UTC 2026
% Result : Theorem 6.85s 1.38s
% Output : Refutation 6.85s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : DAT286^1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n016.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Tue Sep 29 18:24:50 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 Running higher-order theorem proving
% 0.08/0.24 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.22/0.35 % (724066)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.22/0.35 % (724073)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=2546868566:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.22/0.35 % (724073)Refutation not found, incomplete strategy
% 0.22/0.35 % (724073)------------------------------
% 0.22/0.35 % (724073)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.35 % (724073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.35 % (724073)CaDiCaL version: 2.1.3
% 0.22/0.35 % (724073)Termination reason: Refutation not found, incomplete strategy
% 0.22/0.35 % (724073)Time elapsed: 0.002 s
% 0.22/0.35 % (724073)Peak memory usage: 12 MB
% 0.22/0.35 % (724073)Instructions burned: 5 (million)
% 0.22/0.35 % (724073)------------------------------
% 0.22/0.35 % (724073)------------------------------
% 0.22/0.35 % (724077)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.22/0.35 % (724077)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.22/0.35 % (724071)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3355348348:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.22/0.35 % (724072)lrs+10_16_si=on:nwc=1.5:random_seed=2818536579:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.22/0.35 % (724076)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=1459922061:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.22/0.35 % (724074)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=2609452068:hsq=on:hsqr=16,1:s2a=on:i=634:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2999 on theBenchmark for (2999ds/634Mi)
% 0.22/0.35 % (724075)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=998986330:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.22/0.35 % (724077)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=919581241:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.22/0.35 % (724079)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2255271510:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.22/0.35 % (724077)Refutation not found, incomplete strategy
% 0.22/0.35 % (724077)------------------------------
% 0.22/0.35 % (724077)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.35 % (724077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.35 % (724077)CaDiCaL version: 2.1.3
% 0.22/0.35 % (724077)Termination reason: Refutation not found, incomplete strategy
% 0.22/0.35 % (724077)Time elapsed: 0.005 s
% 0.22/0.35 % (724077)Peak memory usage: 12 MB
% 0.22/0.35 % (724077)Instructions burned: 8 (million)
% 0.22/0.35 % (724079)Instruction limit reached!
% 0.22/0.35 % (724079)------------------------------
% 0.22/0.35 % (724079)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.35 % (724079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.35 % (724079)CaDiCaL version: 2.1.3
% 0.22/0.35 % (724079)Termination reason: Instruction limit
% 0.22/0.35 % (724079)Termination phase: Saturation
% 0.22/0.35 % (724079)Time elapsed: 0.001 s
% 0.22/0.35 % (724079)Peak memory usage: 12 MB
% 0.22/0.35 % (724079)Instructions burned: 2 (million)
% 0.22/0.35 % (724077)------------------------------
% 0.22/0.35 % (724077)------------------------------
% 0.22/0.35 % (724072)Instruction limit reached!
% 0.22/0.35 % (724072)------------------------------
% 0.22/0.35 % (724072)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.35 % (724072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.35 % (724072)CaDiCaL version: 2.1.3
% 0.22/0.35 % (724072)Termination reason: Instruction limit
% 0.22/0.35 % (724072)Termination phase: Saturation
% 0.22/0.35 % (724072)Time elapsed: 0.010 s
% 0.22/0.35 % (724072)Peak memory usage: 12 MB
% 0.22/0.35 % (724072)Instructions burned: 18 (million)
% 0.22/0.35 % (724075)Instruction limit reached!
% 0.77/0.37 % (724075)------------------------------
% 0.77/0.37 % (724075)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.37 % (724075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.37 % (724075)CaDiCaL version: 2.1.3
% 0.77/0.37 % (724075)Termination reason: Instruction limit
% 0.77/0.37 % (724075)Termination phase: Saturation
% 0.77/0.37 % (724075)Time elapsed: 0.015 s
% 0.77/0.37 % (724075)Peak memory usage: 12 MB
% 0.77/0.37 % (724075)Instructions burned: 25 (million)
% 0.77/0.37 % (724087)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=706827901:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.77/0.37 % (724087)Instruction limit reached!
% 0.77/0.37 % (724087)------------------------------
% 0.77/0.37 % (724087)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.37 % (724087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.37 % (724087)CaDiCaL version: 2.1.3
% 0.77/0.37 % (724087)Termination reason: Instruction limit
% 0.77/0.37 % (724087)Termination phase: Saturation
% 0.77/0.37 % (724087)Time elapsed: 0.002 s
% 0.77/0.37 % (724087)Peak memory usage: 12 MB
% 0.77/0.37 % (724087)Instructions burned: 7 (million)
% 0.77/0.37 % (724088)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.37 % (724088)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3686464371: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.37 % (724089)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=3273870035:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.77/0.37 % (724092)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=1979022824:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.77/0.37 % (724090)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.37 % (724090)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.37 % (724088)Instruction limit reached!
% 0.77/0.37 % (724088)------------------------------
% 0.77/0.37 % (724088)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.37 % (724088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.37 % (724088)CaDiCaL version: 2.1.3
% 0.77/0.37 % (724088)Termination reason: Instruction limit
% 0.77/0.37 % (724088)Termination phase: Saturation
% 0.77/0.37 % (724088)Time elapsed: 0.004 s
% 0.77/0.37 % (724088)Peak memory usage: 12 MB
% 0.77/0.37 % (724088)Instructions burned: 7 (million)
% 0.77/0.37 % (724090)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=389179729: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.37 % (724089)Instruction limit reached!
% 0.77/0.37 % (724089)------------------------------
% 0.77/0.37 % (724089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.37 % (724089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.37 % (724089)CaDiCaL version: 2.1.3
% 0.77/0.37 % (724089)Termination reason: Instruction limit
% 0.77/0.37 % (724089)Termination phase: Saturation
% 0.77/0.37 % (724089)Time elapsed: 0.009 s
% 0.77/0.37 % (724089)Peak memory usage: 12 MB
% 0.77/0.37 % (724089)Instructions burned: 13 (million)
% 0.77/0.37 % (724076)Instruction limit reached!
% 0.77/0.37 % (724076)------------------------------
% 0.77/0.37 % (724076)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.37 % (724076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.37 % (724076)CaDiCaL version: 2.1.3
% 0.77/0.37 % (724076)Termination reason: Instruction limit
% 0.77/0.37 % (724076)Termination phase: Saturation
% 0.77/0.37 % (724076)Time elapsed: 0.040 s
% 0.77/0.37 % (724076)Peak memory usage: 12 MB
% 0.77/0.37 % (724076)Instructions burned: 76 (million)
% 0.77/0.37 % (724071)Instruction limit reached!
% 0.77/0.37 % (724071)------------------------------
% 0.77/0.37 % (724071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.40 % (724071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.40 % (724071)CaDiCaL version: 2.1.3
% 0.77/0.40 % (724071)Termination reason: Instruction limit
% 0.77/0.40 % (724071)Termination phase: Saturation
% 0.77/0.40 % (724071)Time elapsed: 0.046 s
% 0.77/0.40 % (724071)Peak memory usage: 12 MB
% 0.77/0.40 % (724071)Instructions burned: 88 (million)
% 0.77/0.40 % (724096)lrs+10_1_si=on:cs=on:random_seed=696462798:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.77/0.40 % (724090)Instruction limit reached!
% 0.77/0.40 % (724090)------------------------------
% 0.77/0.40 % (724090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.40 % (724090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.40 % (724090)CaDiCaL version: 2.1.3
% 0.77/0.40 % (724090)Termination reason: Instruction limit
% 0.77/0.40 % (724090)Termination phase: Saturation
% 0.77/0.40 % (724090)Time elapsed: 0.016 s
% 0.77/0.40 % (724090)Peak memory usage: 12 MB
% 0.77/0.40 % (724090)Instructions burned: 28 (million)
% 0.77/0.40 % (724098)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 0.77/0.40 % (724096)Instruction limit reached!
% 0.77/0.40 % (724096)------------------------------
% 0.77/0.40 % (724096)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.40 % (724096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.40 % (724096)CaDiCaL version: 2.1.3
% 0.77/0.40 % (724096)Termination reason: Instruction limit
% 0.77/0.40 % (724096)Termination phase: Saturation
% 0.77/0.40 % (724096)Time elapsed: 0.005 s
% 0.77/0.40 % (724096)Peak memory usage: 12 MB
% 0.77/0.40 % (724096)Instructions burned: 9 (million)
% 0.77/0.40 % (724092)Instruction limit reached!
% 0.77/0.40 % (724092)------------------------------
% 0.77/0.40 % (724092)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.40 % (724092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.40 % (724092)CaDiCaL version: 2.1.3
% 0.77/0.40 % (724092)Termination reason: Instruction limit
% 0.77/0.40 % (724092)Termination phase: Saturation
% 0.77/0.40 % (724092)Time elapsed: 0.025 s
% 0.77/0.40 % (724092)Peak memory usage: 12 MB
% 0.77/0.40 % (724092)Instructions burned: 90 (million)
% 0.77/0.40 % (724098)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=3490131543:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.77/0.40 % (724098)Instruction limit reached!
% 0.77/0.40 % (724098)------------------------------
% 0.77/0.40 % (724098)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.40 % (724098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.40 % (724098)CaDiCaL version: 2.1.3
% 0.77/0.40 % (724098)Termination reason: Instruction limit
% 0.77/0.40 % (724098)Termination phase: Saturation
% 0.77/0.40 % (724098)Time elapsed: 0.002 s
% 0.77/0.40 % (724098)Peak memory usage: 12 MB
% 0.77/0.40 % (724098)Instructions burned: 3 (million)
% 0.77/0.40 % (724103)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=3924461183:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2999 on theBenchmark for (2999ds/14Mi)
% 0.77/0.40 % (724102)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=2283096845:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/25Mi)
% 0.77/0.40 % (724099)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=3115615024:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.77/0.40 % (724099)Refutation not found, incomplete strategy
% 0.77/0.40 % (724099)------------------------------
% 0.77/0.40 % (724099)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.77/0.40 % (724099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.77/0.40 % (724099)CaDiCaL version: 2.1.3
% 0.77/0.40 % (724099)Termination reason: Refutation not found, incomplete strategy
% 0.77/0.40 % (724099)Time elapsed: 0.001 s
% 0.77/0.40 % (724099)Peak memory usage: 12 MB
% 0.77/0.40 % (724102)Refutation not found, incomplete strategy
% 0.77/0.40 % (724102)------------------------------
% 0.77/0.40 % (724102)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.56/0.47 % (724102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.56/0.47 % (724102)CaDiCaL version: 2.1.3
% 1.56/0.47 % (724102)Termination reason: Refutation not found, incomplete strategy
% 1.56/0.47 % (724102)Time elapsed: 0.002 s
% 1.56/0.47 % (724102)Peak memory usage: 12 MB
% 1.56/0.47 % (724102)Instructions burned: 2 (million)
% 1.56/0.47 % (724099)------------------------------
% 1.56/0.47 % (724099)------------------------------
% 1.56/0.47 % (724102)------------------------------
% 1.56/0.47 % (724102)------------------------------
% 1.56/0.47 % (724103)Instruction limit reached!
% 1.56/0.47 % (724103)------------------------------
% 1.56/0.47 % (724103)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.56/0.47 % (724103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.56/0.47 % (724103)CaDiCaL version: 2.1.3
% 1.56/0.47 % (724103)Termination reason: Instruction limit
% 1.56/0.47 % (724103)Termination phase: Saturation
% 1.56/0.47 % (724103)Time elapsed: 0.008 s
% 1.56/0.47 % (724103)Peak memory usage: 12 MB
% 1.56/0.47 % (724103)Instructions burned: 26 (million)
% 1.56/0.47 % (724104)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=790380972:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/327Mi)
% 1.56/0.47 % (724106)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=2050452718:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/14Mi)
% 1.56/0.47 % (724101)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=3447108918:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 1.56/0.47 % (724101)Refutation not found, incomplete strategy
% 1.56/0.47 % (724101)------------------------------
% 1.56/0.47 % (724101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.56/0.47 % (724101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.56/0.47 % (724101)CaDiCaL version: 2.1.3
% 1.56/0.47 % (724101)Termination reason: Refutation not found, incomplete strategy
% 1.56/0.47 % (724101)Time elapsed: 0.001 s
% 1.56/0.47 % (724101)Peak memory usage: 12 MB
% 1.56/0.47 % (724101)Instructions burned: 1 (million)
% 1.56/0.47 % (724101)------------------------------
% 1.56/0.47 % (724101)------------------------------
% 1.56/0.47 % (724113)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=906534404:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.56/0.47 % (724106)Instruction limit reached!
% 1.56/0.47 % (724106)------------------------------
% 1.56/0.47 % (724106)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.56/0.47 % (724106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.56/0.47 % (724106)CaDiCaL version: 2.1.3
% 1.56/0.47 % (724106)Termination reason: Instruction limit
% 1.56/0.47 % (724106)Termination phase: Saturation
% 1.56/0.47 % (724106)Time elapsed: 0.010 s
% 1.56/0.47 % (724106)Peak memory usage: 12 MB
% 1.56/0.47 % (724106)Instructions burned: 16 (million)
% 1.56/0.47 % (724110)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=1503835047: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.56/0.47 % (724111)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=4265182306:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.56/0.47 % (724110)Instruction limit reached!
% 1.56/0.47 % (724110)------------------------------
% 1.56/0.47 % (724110)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.56/0.47 % (724110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.56/0.47 % (724110)CaDiCaL version: 2.1.3
% 1.56/0.47 % (724110)Termination reason: Instruction limit
% 1.56/0.47 % (724110)Termination phase: Saturation
% 1.56/0.47 % (724110)Time elapsed: 0.002 s
% 1.56/0.47 % (724110)Peak memory usage: 12 MB
% 1.56/0.47 % (724110)Instructions burned: 2 (million)
% 1.56/0.47 % (724113)Instruction limit reached!
% 1.56/0.47 % (724113)------------------------------
% 1.56/0.47 % (724113)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.56/0.47 % (724113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.56/0.47 % (724113)CaDiCaL version: 2.1.3
% 1.56/0.47 % (724113)Termination reason: Instruction limit
% 1.56/0.47 % (724113)Termination phase: Saturation
% 1.56/0.50 % (724113)Time elapsed: 0.007 s
% 1.56/0.50 % (724113)Peak memory usage: 12 MB
% 1.56/0.50 % (724113)Instructions burned: 27 (million)
% 1.56/0.50 % (724111)Refutation not found, incomplete strategy
% 1.56/0.50 % (724111)------------------------------
% 1.56/0.50 % (724111)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.56/0.50 % (724111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.56/0.50 % (724111)CaDiCaL version: 2.1.3
% 1.56/0.50 % (724111)Termination reason: Refutation not found, incomplete strategy
% 1.56/0.50 % (724111)Time elapsed: 0.004 s
% 1.56/0.50 % (724111)Peak memory usage: 12 MB
% 1.56/0.50 % (724111)Instructions burned: 6 (million)
% 1.56/0.50 % (724111)------------------------------
% 1.56/0.50 % (724111)------------------------------
% 1.56/0.50 % (724116)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=3245475326:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 1.56/0.50 % (724118)WARNING Broken Constraint: if sine_to_age_generality_threshold(10) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 1.56/0.50 % (724118)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 1.56/0.50 % (724122)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=2947388939:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 1.56/0.50 % (724122)Refutation not found, incomplete strategy
% 1.56/0.50 % (724122)------------------------------
% 1.56/0.50 % (724122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.56/0.50 % (724122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.56/0.50 % (724122)CaDiCaL version: 2.1.3
% 1.56/0.50 % (724122)Termination reason: Refutation not found, incomplete strategy
% 1.56/0.50 % (724122)Time elapsed: 0.002 s
% 1.56/0.50 % (724122)Peak memory usage: 12 MB
% 1.56/0.50 % (724122)Instructions burned: 5 (million)
% 1.56/0.50 % (724118)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=3960926099:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.56/0.50 % (724122)------------------------------
% 1.56/0.50 % (724122)------------------------------
% 1.56/0.50 % (724121)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 1.56/0.50 % (724121)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=335269213:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.56/0.50 % (724123)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=4146387482:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 1.56/0.50 % (724118)Instruction limit reached!
% 1.56/0.50 % (724118)------------------------------
% 1.56/0.50 % (724118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.56/0.50 % (724118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.56/0.50 % (724118)CaDiCaL version: 2.1.3
% 1.56/0.50 % (724118)Termination reason: Instruction limit
% 1.56/0.50 % (724118)Termination phase: Saturation
% 1.56/0.50 % (724118)Time elapsed: 0.009 s
% 1.56/0.50 % (724118)Peak memory usage: 12 MB
% 1.56/0.50 % (724118)Instructions burned: 14 (million)
% 1.56/0.50 % (724127)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=1504791870:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.56/0.50 % (724121)Instruction limit reached!
% 1.56/0.50 % (724121)------------------------------
% 1.56/0.50 % (724121)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.56/0.50 % (724121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.56/0.50 % (724121)CaDiCaL version: 2.1.3
% 1.56/0.50 % (724121)Termination reason: Instruction limit
% 1.56/0.50 % (724121)Termination phase: Saturation
% 1.56/0.50 % (724121)Time elapsed: 0.006 s
% 1.56/0.50 % (724121)Peak memory usage: 12 MB
% 1.56/0.50 % (724121)Instructions burned: 9 (million)
% 1.56/0.50 % (724123)Instruction limit reached!
% 1.56/0.50 % (724123)------------------------------
% 1.56/0.50 % (724123)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.56/0.54 % (724123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.56/0.54 % (724123)CaDiCaL version: 2.1.3
% 1.56/0.54 % (724123)Termination reason: Instruction limit
% 1.56/0.54 % (724123)Termination phase: Saturation
% 1.56/0.54 % (724123)Time elapsed: 0.004 s
% 1.56/0.54 % (724123)Peak memory usage: 12 MB
% 1.56/0.54 % (724123)Instructions burned: 7 (million)
% 1.56/0.54 % (724127)Instruction limit reached!
% 1.56/0.54 % (724127)------------------------------
% 1.56/0.54 % (724127)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.56/0.54 % (724127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.56/0.54 % (724127)CaDiCaL version: 2.1.3
% 1.56/0.54 % (724127)Termination reason: Instruction limit
% 1.56/0.54 % (724127)Termination phase: Saturation
% 1.56/0.54 % (724127)Time elapsed: 0.006 s
% 1.56/0.54 % (724127)Peak memory usage: 12 MB
% 1.56/0.54 % (724127)Instructions burned: 27 (million)
% 1.56/0.54 % (724134)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=1645489805:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/193Mi)
% 1.56/0.54 % (724130)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=3567775378:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 1.56/0.54 % (724116)Instruction limit reached!
% 1.56/0.54 % (724116)------------------------------
% 1.56/0.54 % (724116)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.56/0.54 % (724116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.56/0.54 % (724116)CaDiCaL version: 2.1.3
% 1.56/0.54 % (724116)Termination reason: Instruction limit
% 1.56/0.54 % (724116)Termination phase: Saturation
% 1.56/0.54 % (724116)Time elapsed: 0.036 s
% 1.56/0.54 % (724116)Peak memory usage: 12 MB
% 1.56/0.54 % (724116)Instructions burned: 60 (million)
% 1.56/0.54 % (724132)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=1248221782:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 1.56/0.54 % (724133)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=2620615441:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/143Mi)
% 1.56/0.54 % (724130)Instruction limit reached!
% 1.56/0.54 % (724130)------------------------------
% 1.56/0.54 % (724130)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.56/0.54 % (724130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.56/0.54 % (724130)CaDiCaL version: 2.1.3
% 1.56/0.54 % (724130)Termination reason: Instruction limit
% 1.56/0.54 % (724130)Termination phase: Saturation
% 1.56/0.54 % (724130)Time elapsed: 0.013 s
% 1.56/0.54 % (724130)Peak memory usage: 12 MB
% 1.56/0.54 % (724130)Instructions burned: 22 (million)
% 1.56/0.54 % (724140)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.56/0.54 % (724137)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=1379473378:i=42:hud=10:rtra=on_2998 on theBenchmark for (2998ds/42Mi)
% 1.56/0.54 % (724140)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=122298114:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2998 on theBenchmark for (2998ds/7Mi)
% 1.56/0.54 % (724140)Instruction limit reached!
% 1.56/0.54 % (724140)------------------------------
% 1.56/0.54 % (724140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.56/0.54 % (724140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.56/0.54 % (724140)CaDiCaL version: 2.1.3
% 1.56/0.54 % (724140)Termination reason: Instruction limit
% 1.56/0.54 % (724140)Termination phase: Saturation
% 1.56/0.54 % (724140)Time elapsed: 0.005 s
% 1.56/0.54 % (724140)Peak memory usage: 12 MB
% 1.56/0.54 % (724140)Instructions burned: 8 (million)
% 1.56/0.54 % (724143)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=3458535252:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/181Mi)
% 1.56/0.54 % (724134)Instruction limit reached!
% 1.56/0.54 % (724134)------------------------------
% 1.56/0.54 % (724134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.56/0.54 % (724134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.56/0.54 % (724134)CaDiCaL version: 2.1.3
% 2.24/0.60 % (724134)Termination reason: Instruction limit
% 2.24/0.60 % (724134)Termination phase: Saturation
% 2.24/0.60 % (724134)Time elapsed: 0.058 s
% 2.24/0.60 % (724134)Peak memory usage: 12 MB
% 2.24/0.60 % (724134)Instructions burned: 195 (million)
% 2.24/0.60 % (724143)Refutation not found, incomplete strategy
% 2.24/0.60 % (724143)------------------------------
% 2.24/0.60 % (724143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.24/0.60 % (724143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.24/0.60 % (724143)CaDiCaL version: 2.1.3
% 2.24/0.60 % (724143)Termination reason: Refutation not found, incomplete strategy
% 2.24/0.60 % (724143)Time elapsed: 0.001 s
% 2.24/0.60 % (724143)Peak memory usage: 12 MB
% 2.24/0.60 % (724143)------------------------------
% 2.24/0.60 % (724143)------------------------------
% 2.24/0.60 % (724145)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=745739894:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2997 on theBenchmark for (2997ds/169Mi)
% 2.24/0.60 % (724145)Refutation not found, incomplete strategy
% 2.24/0.60 % (724145)------------------------------
% 2.24/0.60 % (724145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.24/0.60 % (724145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.24/0.60 % (724145)CaDiCaL version: 2.1.3
% 2.24/0.60 % (724145)Termination reason: Refutation not found, incomplete strategy
% 2.24/0.60 % (724145)Time elapsed: 0.001 s
% 2.24/0.60 % (724145)Peak memory usage: 12 MB
% 2.24/0.60 % (724145)Instructions burned: 1 (million)
% 2.24/0.60 % (724145)------------------------------
% 2.24/0.60 % (724145)------------------------------
% 2.24/0.60 % (724146)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 2.24/0.60 % (724137)Instruction limit reached!
% 2.24/0.60 % (724137)------------------------------
% 2.24/0.60 % (724137)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.24/0.60 % (724137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.24/0.60 % (724137)CaDiCaL version: 2.1.3
% 2.24/0.60 % (724137)Termination reason: Instruction limit
% 2.24/0.60 % (724137)Termination phase: Saturation
% 2.24/0.60 % (724137)Time elapsed: 0.042 s
% 2.24/0.60 % (724137)Peak memory usage: 12 MB
% 2.24/0.60 % (724137)Instructions burned: 42 (million)
% 2.24/0.60 % (724146)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=2828322965:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2997 on theBenchmark for (2997ds/6Mi)
% 2.24/0.60 % (724133)Instruction limit reached!
% 2.24/0.60 % (724133)------------------------------
% 2.24/0.60 % (724133)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.24/0.60 % (724148)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=3742713491:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2997 on theBenchmark for (2997ds/22Mi)
% 2.24/0.60 % (724133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.24/0.60 % (724133)CaDiCaL version: 2.1.3
% 2.24/0.60 % (724133)Termination reason: Instruction limit
% 2.24/0.60 % (724133)Termination phase: Saturation
% 2.24/0.60 % (724133)Time elapsed: 0.075 s
% 2.24/0.60 % (724133)Peak memory usage: 13 MB
% 2.24/0.60 % (724133)Instructions burned: 144 (million)
% 2.24/0.60 % (724146)Instruction limit reached!
% 2.24/0.60 % (724146)------------------------------
% 2.24/0.60 % (724146)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.24/0.60 % (724146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.24/0.60 % (724146)CaDiCaL version: 2.1.3
% 2.24/0.60 % (724146)Termination reason: Instruction limit
% 2.24/0.60 % (724146)Termination phase: Saturation
% 2.24/0.60 % (724146)Time elapsed: 0.004 s
% 2.24/0.60 % (724146)Peak memory usage: 12 MB
% 2.24/0.60 % (724146)Instructions burned: 7 (million)
% 2.24/0.60 % (724148)Instruction limit reached!
% 2.24/0.60 % (724148)------------------------------
% 2.24/0.60 % (724148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.24/0.60 % (724148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.24/0.60 % (724148)CaDiCaL version: 2.1.3
% 2.24/0.60 % (724148)Termination reason: Instruction limit
% 2.24/0.60 % (724148)Termination phase: Saturation
% 2.24/0.60 % (724148)Time elapsed: 0.006 s
% 2.71/0.68 % (724148)Peak memory usage: 12 MB
% 2.71/0.68 % (724148)Instructions burned: 24 (million)
% 2.71/0.68 % (724149)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=494716733:i=19:add=on:rtra=on_2997 on theBenchmark for (2997ds/19Mi)
% 2.71/0.68 % (724149)Refutation not found, incomplete strategy
% 2.71/0.68 % (724149)------------------------------
% 2.71/0.68 % (724149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.71/0.68 % (724149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.71/0.68 % (724149)CaDiCaL version: 2.1.3
% 2.71/0.68 % (724149)Termination reason: Refutation not found, incomplete strategy
% 2.71/0.68 % (724149)Time elapsed: 0.002 s
% 2.71/0.68 % (724149)Peak memory usage: 13 MB
% 2.71/0.68 % (724149)Instructions burned: 2 (million)
% 2.71/0.68 % (724149)------------------------------
% 2.71/0.68 % (724149)------------------------------
% 2.71/0.68 % (724154)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=1568243815:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2997 on theBenchmark for (2997ds/45Mi)
% 2.71/0.68 % (724152)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=4089611780:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/316Mi)
% 2.71/0.68 % (724153)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=2564442991:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2997 on theBenchmark for (2997ds/853Mi)
% 2.71/0.68 % (724154)Instruction limit reached!
% 2.71/0.68 % (724154)------------------------------
% 2.71/0.68 % (724154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.71/0.68 % (724154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.71/0.68 % (724154)CaDiCaL version: 2.1.3
% 2.71/0.68 % (724154)Termination reason: Instruction limit
% 2.71/0.68 % (724154)Termination phase: Saturation
% 2.71/0.68 % (724154)Time elapsed: 0.015 s
% 2.71/0.68 % (724154)Peak memory usage: 13 MB
% 2.71/0.68 % (724154)Instructions burned: 47 (million)
% 2.71/0.68 % (724104)Instruction limit reached!
% 2.71/0.68 % (724104)------------------------------
% 2.71/0.68 % (724104)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.71/0.68 % (724104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.71/0.68 % (724104)CaDiCaL version: 2.1.3
% 2.71/0.68 % (724104)Termination reason: Instruction limit
% 2.71/0.68 % (724104)Termination phase: Saturation
% 2.71/0.68 % (724104)Time elapsed: 0.176 s
% 2.71/0.68 % (724104)Peak memory usage: 13 MB
% 2.71/0.68 % (724104)Instructions burned: 328 (million)
% 2.71/0.68 % (724157)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=4119374321:i=480:rtra=on_2997 on theBenchmark for (2997ds/480Mi)
% 2.71/0.68 % (724157)Refutation not found, incomplete strategy
% 2.71/0.68 % (724157)------------------------------
% 2.71/0.68 % (724157)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.71/0.68 % (724157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.71/0.68 % (724157)CaDiCaL version: 2.1.3
% 2.71/0.68 % (724157)Termination reason: Refutation not found, incomplete strategy
% 2.71/0.68 % (724157)Time elapsed: 0.001 s
% 2.71/0.68 % (724157)Peak memory usage: 12 MB
% 2.71/0.68 % (724157)Instructions burned: 1 (million)
% 2.71/0.68 % (724157)------------------------------
% 2.71/0.68 % (724157)------------------------------
% 2.71/0.68 % (724160)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=1259490163:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2997 on theBenchmark for (2997ds/21Mi)
% 2.71/0.68 % (724160)Instruction limit reached!
% 2.71/0.68 % (724160)------------------------------
% 2.71/0.68 % (724160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.71/0.68 % (724160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.71/0.68 % (724160)CaDiCaL version: 2.1.3
% 2.71/0.68 % (724160)Termination reason: Instruction limit
% 2.71/0.68 % (724160)Termination phase: Saturation
% 2.71/0.68 % (724160)Time elapsed: 0.007 s
% 2.71/0.68 % (724160)Peak memory usage: 12 MB
% 2.92/0.72 % (724160)Instructions burned: 25 (million)
% 2.92/0.72 % (724162)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 2.92/0.72 % (724162)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=1420257777:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/200Mi)
% 2.92/0.72 % (724165)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=3590741010:i=66:s2at=3:nm=2:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/66Mi)
% 2.92/0.72 % (724163)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=2302921740:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2997 on theBenchmark for (2997ds/13Mi)
% 2.92/0.72 % (724165)Instruction limit reached!
% 2.92/0.72 % (724165)------------------------------
% 2.92/0.72 % (724165)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.92/0.72 % (724165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.92/0.72 % (724165)CaDiCaL version: 2.1.3
% 2.92/0.72 % (724165)Termination reason: Instruction limit
% 2.92/0.72 % (724165)Termination phase: Saturation
% 2.92/0.72 % (724165)Time elapsed: 0.015 s
% 2.92/0.72 % (724165)Peak memory usage: 13 MB
% 2.92/0.72 % (724165)Instructions burned: 68 (million)
% 2.92/0.72 % (724169)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=3930763347:i=51:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/51Mi)
% 2.92/0.72 % (724163)Instruction limit reached!
% 2.92/0.72 % (724163)------------------------------
% 2.92/0.72 % (724163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.92/0.72 % (724163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.92/0.72 % (724163)CaDiCaL version: 2.1.3
% 2.92/0.72 % (724163)Termination reason: Instruction limit
% 2.92/0.72 % (724163)Termination phase: Saturation
% 2.92/0.72 % (724163)Time elapsed: 0.015 s
% 2.92/0.72 % (724163)Peak memory usage: 12 MB
% 2.92/0.72 % (724163)Instructions burned: 14 (million)
% 2.92/0.72 % (724169)Refutation not found, incomplete strategy
% 2.92/0.72 % (724169)------------------------------
% 2.92/0.72 % (724169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.92/0.72 % (724169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.92/0.72 % (724169)CaDiCaL version: 2.1.3
% 2.92/0.72 % (724169)Termination reason: Refutation not found, incomplete strategy
% 2.92/0.72 % (724169)Time elapsed: 0.0000 s
% 2.92/0.72 % (724169)Peak memory usage: 12 MB
% 2.92/0.72 % (724169)Instructions burned: 1 (million)
% 2.92/0.72 % (724169)------------------------------
% 2.92/0.72 % (724169)------------------------------
% 2.92/0.72 % (724172)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=2151052896:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2996 on theBenchmark for (2996ds/137Mi)
% 2.92/0.72 % (724172)Refutation not found, incomplete strategy
% 2.92/0.72 % (724172)------------------------------
% 2.92/0.72 % (724172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.92/0.72 % (724172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.92/0.72 % (724172)CaDiCaL version: 2.1.3
% 2.92/0.72 % (724172)Termination reason: Refutation not found, incomplete strategy
% 2.92/0.72 % (724172)Time elapsed: 0.001 s
% 2.92/0.72 % (724172)Peak memory usage: 12 MB
% 2.92/0.72 % (724172)Instructions burned: 3 (million)
% 2.92/0.72 % (724172)------------------------------
% 2.92/0.72 % (724172)------------------------------
% 2.92/0.72 % (724171)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=2855366430:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/31Mi)
% 2.92/0.72 % (724171)Refutation not found, incomplete strategy
% 2.92/0.72 % (724171)------------------------------
% 2.92/0.72 % (724171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.92/0.72 % (724171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.92/0.72 % (724171)CaDiCaL version: 2.1.3
% 2.92/0.72 % (724171)Termination reason: Refutation not found, incomplete strategy
% 2.92/0.72 % (724171)Time elapsed: 0.003 s
% 2.92/0.72 % (724171)Peak memory usage: 12 MB
% 2.92/0.72 % (724171)Instructions burned: 4 (million)
% 2.92/0.72 % (724174)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=575494628:cond=on:i=34:hud=10:nm=10:rtra=on_2996 on theBenchmark for (2996ds/34Mi)
% 2.92/0.80 % (724171)------------------------------
% 2.92/0.80 % (724171)------------------------------
% 2.92/0.80 % (724074)Instruction limit reached!
% 2.92/0.80 % (724074)------------------------------
% 2.92/0.80 % (724074)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.92/0.80 % (724074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.92/0.80 % (724074)CaDiCaL version: 2.1.3
% 2.92/0.80 % (724074)Termination reason: Instruction limit
% 2.92/0.80 % (724074)Termination phase: Saturation
% 2.92/0.80 % (724074)Time elapsed: 0.325 s
% 2.92/0.80 % (724074)Peak memory usage: 14 MB
% 2.92/0.80 % (724074)Instructions burned: 636 (million)
% 2.92/0.80 % (724174)Instruction limit reached!
% 2.92/0.80 % (724174)------------------------------
% 2.92/0.80 % (724174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.92/0.80 % (724174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.92/0.80 % (724174)CaDiCaL version: 2.1.3
% 2.92/0.80 % (724174)Termination reason: Instruction limit
% 2.92/0.80 % (724174)Termination phase: Saturation
% 2.92/0.80 % (724174)Time elapsed: 0.010 s
% 2.92/0.80 % (724174)Peak memory usage: 12 MB
% 2.92/0.80 % (724174)Instructions burned: 38 (million)
% 2.92/0.80 % (724178)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 2.92/0.80 % (724177)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=4054453408:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2996 on theBenchmark for (2996ds/67Mi)
% 2.92/0.80 % (724178)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=2542424255:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2996 on theBenchmark for (2996ds/180Mi)
% 2.92/0.80 % (724179)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=1724528473:st=2:i=246:sd=3:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/246Mi)
% 2.92/0.80 % (724177)Refutation not found, incomplete strategy
% 2.92/0.80 % (724177)------------------------------
% 2.92/0.80 % (724177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.92/0.80 % (724177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.92/0.80 % (724177)CaDiCaL version: 2.1.3
% 2.92/0.80 % (724177)Termination reason: Refutation not found, incomplete strategy
% 2.92/0.80 % (724177)Time elapsed: 0.001 s
% 2.92/0.80 % (724177)Peak memory usage: 12 MB
% 2.92/0.80 % (724177)Instructions burned: 1 (million)
% 2.92/0.80 % (724177)------------------------------
% 2.92/0.80 % (724177)------------------------------
% 2.92/0.80 % (724183)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=4166808684:cond=on:i=96:bd=all:rtra=on_2996 on theBenchmark for (2996ds/96Mi)
% 2.92/0.80 % (724162)Instruction limit reached!
% 2.92/0.80 % (724162)------------------------------
% 2.92/0.80 % (724162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.92/0.80 % (724162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.92/0.80 % (724162)CaDiCaL version: 2.1.3
% 2.92/0.80 % (724162)Termination reason: Instruction limit
% 2.92/0.80 % (724162)Termination phase: Saturation
% 2.92/0.80 % (724162)Time elapsed: 0.098 s
% 2.92/0.80 % (724162)Peak memory usage: 12 MB
% 2.92/0.80 % (724162)Instructions burned: 200 (million)
% 2.92/0.80 % (724185)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=2190568945:i=427:sd=1:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/427Mi)
% 2.92/0.80 % (724185)Refutation not found, incomplete strategy
% 2.92/0.80 % (724185)------------------------------
% 2.92/0.80 % (724185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.92/0.80 % (724185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.92/0.80 % (724185)CaDiCaL version: 2.1.3
% 2.92/0.80 % (724185)Termination reason: Refutation not found, incomplete strategy
% 2.92/0.80 % (724185)Time elapsed: 0.001 s
% 2.92/0.80 % (724185)Peak memory usage: 12 MB
% 2.92/0.80 % (724185)------------------------------
% 2.92/0.80 % (724185)------------------------------
% 2.92/0.80 % (724152)Instruction limit reached!
% 2.92/0.80 % (724152)------------------------------
% 2.92/0.80 % (724152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.92/0.80 % (724152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.92/0.80 % (724152)CaDiCaL version: 2.1.3
% 4.07/0.92 % (724152)Termination reason: Instruction limit
% 4.07/0.92 % (724152)Termination phase: Saturation
% 4.07/0.92 % (724152)Time elapsed: 0.167 s
% 4.07/0.92 % (724152)Peak memory usage: 13 MB
% 4.07/0.92 % (724152)Instructions burned: 317 (million)
% 4.07/0.92 % (724187)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=2193587695:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/874Mi)
% 4.07/0.92 % (724179)Instruction limit reached!
% 4.07/0.92 % (724179)------------------------------
% 4.07/0.92 % (724179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.07/0.92 % (724179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.07/0.92 % (724179)CaDiCaL version: 2.1.3
% 4.07/0.92 % (724179)Termination reason: Instruction limit
% 4.07/0.92 % (724179)Termination phase: Saturation
% 4.07/0.92 % (724179)Time elapsed: 0.072 s
% 4.07/0.92 % (724179)Peak memory usage: 13 MB
% 4.07/0.92 % (724179)Instructions burned: 248 (million)
% 4.07/0.92 % (724188)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=2119643545:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/515Mi)
% 4.07/0.92 % (724183)Instruction limit reached!
% 4.07/0.92 % (724183)------------------------------
% 4.07/0.92 % (724183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.07/0.92 % (724183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.07/0.92 % (724183)CaDiCaL version: 2.1.3
% 4.07/0.92 % (724183)Termination reason: Instruction limit
% 4.07/0.92 % (724183)Termination phase: Saturation
% 4.07/0.92 % (724183)Time elapsed: 0.055 s
% 4.07/0.92 % (724183)Peak memory usage: 12 MB
% 4.07/0.92 % (724183)Instructions burned: 97 (million)
% 4.07/0.92 % (724190)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=522146687:st=1.5:i=130:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/130Mi)
% 4.07/0.92 % (724190)Refutation not found, incomplete strategy
% 4.07/0.92 % (724190)------------------------------
% 4.07/0.92 % (724190)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.07/0.92 % (724190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.07/0.92 % (724190)CaDiCaL version: 2.1.3
% 4.07/0.92 % (724190)Termination reason: Refutation not found, incomplete strategy
% 4.07/0.92 % (724190)Time elapsed: 0.001 s
% 4.07/0.92 % (724190)Peak memory usage: 12 MB
% 4.07/0.92 % (724190)Instructions burned: 4 (million)
% 4.07/0.92 % (724190)------------------------------
% 4.07/0.92 % (724190)------------------------------
% 4.07/0.92 % (724188)Refutation not found, incomplete strategy
% 4.07/0.92 % (724188)------------------------------
% 4.07/0.92 % (724188)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.07/0.92 % (724188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.07/0.92 % (724188)CaDiCaL version: 2.1.3
% 4.07/0.92 % (724188)Termination reason: Refutation not found, incomplete strategy
% 4.07/0.92 % (724188)Time elapsed: 0.011 s
% 4.07/0.92 % (724188)Peak memory usage: 13 MB
% 4.07/0.92 % (724188)Instructions burned: 19 (million)
% 4.07/0.92 % (724188)------------------------------
% 4.07/0.92 % (724188)------------------------------
% 4.07/0.92 % (724178)Instruction limit reached!
% 4.07/0.92 % (724178)------------------------------
% 4.07/0.92 % (724178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.07/0.92 % (724178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.07/0.92 % (724178)CaDiCaL version: 2.1.3
% 4.07/0.92 % (724178)Termination reason: Instruction limit
% 4.07/0.92 % (724178)Termination phase: Saturation
% 4.07/0.92 % (724178)Time elapsed: 0.088 s
% 4.07/0.92 % (724178)Peak memory usage: 12 MB
% 4.07/0.92 % (724178)Instructions burned: 181 (million)
% 4.07/0.92 % (724192)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3554538022:i=44:ep=R:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/44Mi)
% 4.07/0.92 % (724194)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=2850153776:s2a=on:i=571:nm=16:rtra=on_2995 on theBenchmark for (2995ds/571Mi)
% 4.07/0.92 % (724194)Refutation not found, incomplete strategy
% 4.07/0.92 % (724194)------------------------------
% 4.07/0.92 % (724194)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.07/0.92 % (724194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.07/0.92 % (724194)CaDiCaL version: 2.1.3
% 5.51/1.05 % (724194)Termination reason: Refutation not found, incomplete strategy
% 5.51/1.05 % (724194)Time elapsed: 0.0000 s
% 5.51/1.05 % (724194)Peak memory usage: 12 MB
% 5.51/1.05 % (724194)Instructions burned: 1 (million)
% 5.51/1.05 % (724194)------------------------------
% 5.51/1.05 % (724194)------------------------------
% 5.51/1.05 % (724192)Refutation not found, incomplete strategy
% 5.51/1.05 % (724192)------------------------------
% 5.51/1.05 % (724192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.51/1.05 % (724192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.51/1.05 % (724192)CaDiCaL version: 2.1.3
% 5.51/1.05 % (724192)Termination reason: Refutation not found, incomplete strategy
% 5.51/1.05 % (724192)Time elapsed: 0.004 s
% 5.51/1.05 % (724192)Peak memory usage: 12 MB
% 5.51/1.05 % (724192)Instructions burned: 6 (million)
% 5.51/1.05 % (724192)------------------------------
% 5.51/1.05 % (724192)------------------------------
% 5.51/1.05 % (724195)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=4113231489:i=450:rtra=on:ixr=off:ntd=on_2995 on theBenchmark for (2995ds/450Mi)
% 5.51/1.05 % (724199)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=3406231775:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2995 on theBenchmark for (2995ds/65Mi)
% 5.51/1.05 % (724196)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=3849398004:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/95Mi)
% 5.51/1.05 % (724195)Refutation not found, incomplete strategy
% 5.51/1.05 % (724195)------------------------------
% 5.51/1.05 % (724195)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.51/1.05 % (724195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.51/1.05 % (724195)CaDiCaL version: 2.1.3
% 5.51/1.05 % (724195)Termination reason: Refutation not found, incomplete strategy
% 5.51/1.05 % (724195)Time elapsed: 0.002 s
% 5.51/1.05 % (724195)Peak memory usage: 12 MB
% 5.51/1.05 % (724195)Instructions burned: 2 (million)
% 5.51/1.05 % (724195)------------------------------
% 5.51/1.05 % (724195)------------------------------
% 5.51/1.05 % (724200)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=1252658401:uwa_fpi=on:avsq=on:s2a=on:cond=fast:i=105:s2at=1.5:aac=none:fgj=on:piset=and:hud=3:fsr=off:rtra=on:er=filter:rawr=on_2995 on theBenchmark for (2995ds/105Mi)
% 5.51/1.05 % (724199)Instruction limit reached!
% 5.51/1.05 % (724199)------------------------------
% 5.51/1.05 % (724199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.51/1.05 % (724199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.51/1.05 % (724199)CaDiCaL version: 2.1.3
% 5.51/1.05 % (724199)Termination reason: Instruction limit
% 5.51/1.05 % (724199)Termination phase: Saturation
% 5.51/1.05 % (724199)Time elapsed: 0.020 s
% 5.51/1.05 % (724199)Peak memory usage: 12 MB
% 5.51/1.05 % (724199)Instructions burned: 68 (million)
% 5.51/1.05 % (724204)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=1517567577:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2995 on theBenchmark for (2995ds/5755Mi)
% 5.51/1.05 % (724206)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=1199166682:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/375Mi)
% 5.51/1.05 % (724196)Instruction limit reached!
% 5.51/1.05 % (724196)------------------------------
% 5.51/1.05 % (724196)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.51/1.05 % (724196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.51/1.05 % (724196)CaDiCaL version: 2.1.3
% 5.51/1.05 % (724196)Termination reason: Instruction limit
% 5.51/1.05 % (724196)Termination phase: Saturation
% 5.51/1.05 % (724196)Time elapsed: 0.051 s
% 5.51/1.05 % (724196)Peak memory usage: 12 MB
% 5.51/1.05 % (724196)Instructions burned: 95 (million)
% 5.51/1.05 % (724200)Instruction limit reached!
% 5.51/1.05 % (724200)------------------------------
% 5.51/1.05 % (724200)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.51/1.05 % (724200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.12/1.13 % (724200)CaDiCaL version: 2.1.3
% 6.12/1.13 % (724200)Termination reason: Instruction limit
% 6.12/1.13 % (724200)Termination phase: Saturation
% 6.12/1.13 % (724200)Time elapsed: 0.055 s
% 6.12/1.13 % (724200)Peak memory usage: 12 MB
% 6.12/1.13 % (724200)Instructions burned: 105 (million)
% 6.12/1.13 % (724209)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=484369122:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2994 on theBenchmark for (2994ds/495Mi)
% 6.12/1.13 % (724210)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=2093611862:cond=on:i=34:hud=10:nm=10:rtra=on_2994 on theBenchmark for (2994ds/34Mi)
% 6.12/1.13 % (724210)Instruction limit reached!
% 6.12/1.13 % (724210)------------------------------
% 6.12/1.13 % (724210)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.12/1.13 % (724210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.12/1.13 % (724210)CaDiCaL version: 2.1.3
% 6.12/1.13 % (724210)Termination reason: Instruction limit
% 6.12/1.13 % (724210)Termination phase: Saturation
% 6.12/1.13 % (724210)Time elapsed: 0.018 s
% 6.12/1.13 % (724210)Peak memory usage: 12 MB
% 6.12/1.13 % (724210)Instructions burned: 34 (million)
% 6.12/1.13 % (724213)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=538371052:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2994 on theBenchmark for (2994ds/91Mi)
% 6.12/1.13 % (724206)Instruction limit reached!
% 6.12/1.13 % (724206)------------------------------
% 6.12/1.13 % (724206)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.12/1.13 % (724206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.12/1.13 % (724206)CaDiCaL version: 2.1.3
% 6.12/1.13 % (724206)Termination reason: Instruction limit
% 6.12/1.13 % (724206)Termination phase: Saturation
% 6.12/1.13 % (724206)Time elapsed: 0.099 s
% 6.12/1.13 % (724206)Peak memory usage: 13 MB
% 6.12/1.13 % (724206)Instructions burned: 378 (million)
% 6.12/1.13 % (724215)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=2365785987:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2993 on theBenchmark for (2993ds/66Mi)
% 6.12/1.13 % (724215)Refutation not found, incomplete strategy
% 6.12/1.13 % (724215)------------------------------
% 6.12/1.13 % (724215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.12/1.13 % (724215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.12/1.13 % (724215)CaDiCaL version: 2.1.3
% 6.12/1.13 % (724215)Termination reason: Refutation not found, incomplete strategy
% 6.12/1.13 % (724215)Time elapsed: 0.0000 s
% 6.12/1.13 % (724215)Peak memory usage: 12 MB
% 6.12/1.13 % (724215)Instructions burned: 1 (million)
% 6.12/1.13 % (724215)------------------------------
% 6.12/1.13 % (724215)------------------------------
% 6.12/1.13 % (724217)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=255978279:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2993 on theBenchmark for (2993ds/22Mi)
% 6.12/1.13 % (724217)Instruction limit reached!
% 6.12/1.13 % (724217)------------------------------
% 6.12/1.13 % (724217)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.12/1.13 % (724217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.12/1.13 % (724217)CaDiCaL version: 2.1.3
% 6.12/1.13 % (724217)Termination reason: Instruction limit
% 6.12/1.13 % (724217)Termination phase: Saturation
% 6.12/1.13 % (724217)Time elapsed: 0.007 s
% 6.12/1.13 % (724217)Peak memory usage: 12 MB
% 6.12/1.13 % (724217)Instructions burned: 25 (million)
% 6.12/1.13 % (724219)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=934151024:i=338:bd=all:ins=4:rtra=on_2993 on theBenchmark for (2993ds/338Mi)
% 6.12/1.13 % (724213)Instruction limit reached!
% 6.12/1.13 % (724213)------------------------------
% 6.12/1.13 % (724213)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.12/1.13 % (724213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.12/1.13 % (724213)CaDiCaL version: 2.1.3
% 6.12/1.13 % (724213)Termination reason: Instruction limit
% 6.12/1.13 % (724213)Termination phase: Saturation
% 6.12/1.13 % (724213)Time elapsed: 0.048 s
% 6.12/1.13 % (724213)Peak memory usage: 12 MB
% 6.12/1.13 % (724213)Instructions burned: 92 (million)
% 6.12/1.13 % (724221)lrs+10_1_sil=128000:si=on:urr=on:random_seed=2157210125:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2993 on theBenchmark for (2993ds/28Mi)
% 6.12/1.16 % (724153)Instruction limit reached!
% 6.12/1.16 % (724153)------------------------------
% 6.12/1.16 % (724153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.12/1.16 % (724153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.12/1.16 % (724153)CaDiCaL version: 2.1.3
% 6.12/1.16 % (724153)Termination reason: Instruction limit
% 6.12/1.16 % (724153)Termination phase: Saturation
% 6.12/1.16 % (724153)Time elapsed: 0.421 s
% 6.12/1.16 % (724153)Peak memory usage: 14 MB
% 6.12/1.16 % (724153)Instructions burned: 855 (million)
% 6.12/1.16 % (724221)Instruction limit reached!
% 6.12/1.16 % (724221)------------------------------
% 6.12/1.16 % (724221)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.12/1.16 % (724221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.12/1.16 % (724221)CaDiCaL version: 2.1.3
% 6.12/1.16 % (724221)Termination reason: Instruction limit
% 6.12/1.16 % (724221)Termination phase: Saturation
% 6.12/1.16 % (724221)Time elapsed: 0.017 s
% 6.12/1.16 % (724221)Peak memory usage: 12 MB
% 6.12/1.16 % (724221)Instructions burned: 29 (million)
% 6.12/1.16 % (724223)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 6.12/1.16 % (724223)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=3521458074:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2993 on theBenchmark for (2993ds/137Mi)
% 6.12/1.16 % (724224)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=2826789818:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2993 on theBenchmark for (2993ds/340Mi)
% 6.12/1.16 % (724219)Instruction limit reached!
% 6.12/1.16 % (724219)------------------------------
% 6.12/1.16 % (724219)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.12/1.16 % (724219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.12/1.16 % (724219)CaDiCaL version: 2.1.3
% 6.12/1.16 % (724219)Termination reason: Instruction limit
% 6.12/1.16 % (724219)Termination phase: Saturation
% 6.12/1.16 % (724219)Time elapsed: 0.090 s
% 6.12/1.16 % (724219)Peak memory usage: 13 MB
% 6.12/1.16 % (724219)Instructions burned: 341 (million)
% 6.12/1.16 % (724227)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=1585404362:i=227:sd=1:bd=all:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/227Mi)
% 6.12/1.16 % (724227)Refutation not found, incomplete strategy
% 6.12/1.16 % (724227)------------------------------
% 6.12/1.16 % (724227)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.12/1.16 % (724227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.12/1.16 % (724227)CaDiCaL version: 2.1.3
% 6.12/1.16 % (724227)Termination reason: Refutation not found, incomplete strategy
% 6.12/1.16 % (724227)Time elapsed: 0.0000 s
% 6.12/1.16 % (724227)Peak memory usage: 12 MB
% 6.12/1.16 % (724227)------------------------------
% 6.12/1.16 % (724227)------------------------------
% 6.12/1.16 % (724229)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 6.12/1.16 % (724229)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=3046158015:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2992 on theBenchmark for (2992ds/373Mi)
% 6.12/1.16 % (724223)Instruction limit reached!
% 6.12/1.16 % (724223)------------------------------
% 6.12/1.16 % (724223)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.12/1.16 % (724223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.12/1.16 % (724223)CaDiCaL version: 2.1.3
% 6.12/1.16 % (724223)Termination reason: Instruction limit
% 6.12/1.16 % (724223)Termination phase: Saturation
% 6.12/1.16 % (724223)Time elapsed: 0.067 s
% 6.12/1.16 % (724223)Peak memory usage: 13 MB
% 6.12/1.16 % (724223)Instructions burned: 139 (million)
% 6.12/1.16 % (724231)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=882134410:i=116:ep=RSTC:rtra=on:ntd=on_2992 on theBenchmark for (2992ds/116Mi)
% 6.12/1.16 % (724231)Refutation not found, incomplete strategy
% 6.12/1.16 % (724231)------------------------------
% 6.12/1.16 % (724231)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.12/1.19 % (724231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.12/1.19 % (724231)CaDiCaL version: 2.1.3
% 6.12/1.19 % (724231)Termination reason: Refutation not found, incomplete strategy
% 6.12/1.19 % (724231)Time elapsed: 0.002 s
% 6.12/1.19 % (724231)Peak memory usage: 12 MB
% 6.12/1.19 % (724231)Instructions burned: 1 (million)
% 6.12/1.19 % (724231)------------------------------
% 6.12/1.19 % (724231)------------------------------
% 6.12/1.19 % (724132)Instruction limit reached!
% 6.12/1.19 % (724132)------------------------------
% 6.12/1.19 % (724132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.12/1.19 % (724132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.12/1.19 % (724132)CaDiCaL version: 2.1.3
% 6.12/1.19 % (724132)Termination reason: Instruction limit
% 6.12/1.19 % (724132)Termination phase: Saturation
% 6.12/1.19 % (724132)Time elapsed: 0.640 s
% 6.12/1.19 % (724132)Peak memory usage: 14 MB
% 6.12/1.19 % (724132)Instructions burned: 1240 (million)
% 6.12/1.19 % (724233)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=873606891:i=575:rtra=on_2992 on theBenchmark for (2992ds/575Mi)
% 6.12/1.19 % (724233)Refutation not found, incomplete strategy
% 6.12/1.19 % (724233)------------------------------
% 6.12/1.19 % (724233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.12/1.19 % (724233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.12/1.19 % (724233)CaDiCaL version: 2.1.3
% 6.12/1.19 % (724233)Termination reason: Refutation not found, incomplete strategy
% 6.12/1.19 % (724233)Time elapsed: 0.001 s
% 6.12/1.19 % (724233)Peak memory usage: 12 MB
% 6.12/1.19 % (724233)Instructions burned: 1 (million)
% 6.12/1.19 % (724233)------------------------------
% 6.12/1.19 % (724233)------------------------------
% 6.12/1.19 % (724234)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=1475325909:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2991 on theBenchmark for (2991ds/270Mi)
% 6.12/1.19 % (724236)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=598652677:hsq=on:hsqr=16,1:s2a=on:i=9840:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2991 on theBenchmark for (2991ds/9840Mi)
% 6.12/1.19 % (724229)Instruction limit reached!
% 6.12/1.19 % (724229)------------------------------
% 6.12/1.19 % (724229)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.12/1.19 % (724229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.12/1.19 % (724229)CaDiCaL version: 2.1.3
% 6.12/1.19 % (724229)Termination reason: Instruction limit
% 6.12/1.19 % (724229)Termination phase: Saturation
% 6.12/1.19 % (724229)Time elapsed: 0.094 s
% 6.12/1.19 % (724229)Peak memory usage: 16 MB
% 6.12/1.19 % (724229)Instructions burned: 376 (million)
% 6.12/1.19 % (724224)Instruction limit reached!
% 6.12/1.19 % (724224)------------------------------
% 6.12/1.19 % (724224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.12/1.19 % (724224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.12/1.19 % (724224)CaDiCaL version: 2.1.3
% 6.12/1.19 % (724224)Termination reason: Instruction limit
% 6.12/1.19 % (724224)Termination phase: Saturation
% 6.12/1.19 % (724224)Time elapsed: 0.157 s
% 6.12/1.19 % (724224)Peak memory usage: 12 MB
% 6.12/1.19 % (724224)Instructions burned: 342 (million)
% 6.12/1.19 % (724239)lrs+1010_1_sil=128000:si=on:sos=all:uwa=off:nwc=1:random_seed=2078936604:i=421:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/421Mi)
% 6.12/1.19 % (724239)Refutation not found, incomplete strategy
% 6.12/1.19 % (724239)------------------------------
% 6.12/1.19 % (724239)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.12/1.19 % (724239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.12/1.19 % (724239)CaDiCaL version: 2.1.3
% 6.12/1.19 % (724239)Termination reason: Refutation not found, incomplete strategy
% 6.12/1.19 % (724239)Time elapsed: 0.0000 s
% 6.12/1.19 % (724239)Peak memory usage: 12 MB
% 6.12/1.19 % (724239)------------------------------
% 6.12/1.19 % (724239)------------------------------
% 6.12/1.19 % (724242)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=1028840347:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2991 on theBenchmark for (2991ds/31Mi)
% 6.46/1.25 % (724240)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
% 6.46/1.25 % (724242)Refutation not found, incomplete strategy
% 6.46/1.25 % (724242)------------------------------
% 6.46/1.25 % (724242)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.46/1.25 % (724242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.46/1.25 % (724242)CaDiCaL version: 2.1.3
% 6.46/1.25 % (724242)Termination reason: Refutation not found, incomplete strategy
% 6.46/1.25 % (724242)Time elapsed: 0.001 s
% 6.46/1.25 % (724242)Peak memory usage: 12 MB
% 6.46/1.25 % (724242)Instructions burned: 4 (million)
% 6.46/1.25 % (724242)------------------------------
% 6.46/1.25 % (724242)------------------------------
% 6.46/1.25 % (724240)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=2250213075:avsq=on:i=270:s2at=3:avsqr=1,16:rtra=on:ntd=on_2991 on theBenchmark for (2991ds/270Mi)
% 6.46/1.25 % (724244)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 6.46/1.25 % (724244)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
% 6.46/1.25 % (724244)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=4189096009:hsqr=1,8:i=1440:s2at=5:add=on:nm=2:rtra=on_2991 on theBenchmark for (2991ds/1440Mi)
% 6.46/1.25 % (724209)Instruction limit reached!
% 6.46/1.25 % (724209)------------------------------
% 6.46/1.25 % (724209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.46/1.25 % (724209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.46/1.25 % (724209)CaDiCaL version: 2.1.3
% 6.46/1.25 % (724209)Termination reason: Instruction limit
% 6.46/1.25 % (724209)Termination phase: Saturation
% 6.46/1.25 % (724209)Time elapsed: 0.340 s
% 6.46/1.25 % (724209)Peak memory usage: 14 MB
% 6.46/1.25 % (724209)Instructions burned: 495 (million)
% 6.46/1.25 % (724244)Refutation not found, incomplete strategy
% 6.46/1.25 % (724244)------------------------------
% 6.46/1.25 % (724244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.46/1.25 % (724244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.46/1.25 % (724244)CaDiCaL version: 2.1.3
% 6.46/1.25 % (724244)Termination reason: Refutation not found, incomplete strategy
% 6.46/1.25 % (724244)Time elapsed: 0.003 s
% 6.46/1.25 % (724244)Peak memory usage: 12 MB
% 6.46/1.25 % (724244)Instructions burned: 8 (million)
% 6.46/1.25 % (724244)------------------------------
% 6.46/1.25 % (724244)------------------------------
% 6.46/1.25 % (724187)Instruction limit reached!
% 6.46/1.25 % (724187)------------------------------
% 6.46/1.25 % (724187)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.46/1.25 % (724187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.46/1.25 % (724187)CaDiCaL version: 2.1.3
% 6.46/1.25 % (724187)Termination reason: Instruction limit
% 6.46/1.25 % (724187)Termination phase: Saturation
% 6.46/1.25 % (724187)Time elapsed: 0.468 s
% 6.46/1.25 % (724187)Peak memory usage: 14 MB
% 6.46/1.25 % (724187)Instructions burned: 875 (million)
% 6.46/1.25 % (724248)lrs+2_16:1_si=on:cbe=off:uwa=interpreted_only:random_seed=2542396165:i=111:add=on:fgj=on:rtra=on:fdi=1024_2990 on theBenchmark for (2990ds/111Mi)
% 6.46/1.25 % (724248)Refutation not found, incomplete strategy
% 6.46/1.25 % (724248)------------------------------
% 6.46/1.25 % (724248)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.46/1.25 % (724248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.46/1.25 % (724248)CaDiCaL version: 2.1.3
% 6.46/1.25 % (724248)Termination reason: Refutation not found, incomplete strategy
% 6.46/1.25 % (724248)Time elapsed: 0.004 s
% 6.46/1.25 % (724248)Peak memory usage: 12 MB
% 6.46/1.25 % (724248)Instructions burned: 13 (million)
% 6.46/1.25 % (724248)------------------------------
% 6.46/1.25 % (724248)------------------------------
% 6.46/1.25 % (724247)dis+10_2_sil=128000:si=on:random_seed=1039086208:s2a=on:i=339:av=off:rtra=on:fe=abstraction:ss=axioms:fsd=on:ntd=on_2991 on theBenchmark for (2991ds/339Mi)
% 6.85/1.33 % (724247)Refutation not found, incomplete strategy
% 6.85/1.33 % (724247)------------------------------
% 6.85/1.33 % (724247)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.85/1.33 % (724247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/1.33 % (724247)CaDiCaL version: 2.1.3
% 6.85/1.33 % (724247)Termination reason: Refutation not found, incomplete strategy
% 6.85/1.33 % (724247)Time elapsed: 0.001 s
% 6.85/1.33 % (724247)Peak memory usage: 12 MB
% 6.85/1.33 % (724247)------------------------------
% 6.85/1.33 % (724247)------------------------------
% 6.85/1.33 % (724252)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=2677238019:uwa_fpi=on:avsq=on:i=136:avsqr=1,32:hud=15:nm=0:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/136Mi)
% 6.85/1.33 % (724252)Refutation not found, incomplete strategy
% 6.85/1.33 % (724252)------------------------------
% 6.85/1.33 % (724252)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.85/1.34 % (724252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/1.34 % (724252)CaDiCaL version: 2.1.3
% 6.85/1.34 % (724252)Termination reason: Refutation not found, incomplete strategy
% 6.85/1.34 % (724252)Time elapsed: 0.0000 s
% 6.85/1.34 % (724252)Peak memory usage: 12 MB
% 6.85/1.34 % (724252)Instructions burned: 1 (million)
% 6.85/1.34 % (724252)------------------------------
% 6.85/1.34 % (724252)------------------------------
% 6.85/1.34 % (724249)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=4264954938:st=3:avsq=on:i=122:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2990 on theBenchmark for (2990ds/122Mi)
% 6.85/1.34 % (724249)Refutation not found, incomplete strategy
% 6.85/1.34 % (724249)------------------------------
% 6.85/1.34 % (724249)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.85/1.34 % (724249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/1.34 % (724249)CaDiCaL version: 2.1.3
% 6.85/1.34 % (724249)Termination reason: Refutation not found, incomplete strategy
% 6.85/1.34 % (724249)Time elapsed: 0.001 s
% 6.85/1.34 % (724249)Peak memory usage: 12 MB
% 6.85/1.34 % (724249)Instructions burned: 1 (million)
% 6.85/1.34 % (724249)------------------------------
% 6.85/1.34 % (724249)------------------------------
% 6.85/1.34 % (724253)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=565270007:hsq=on:st=2:i=232:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2990 on theBenchmark for (2990ds/232Mi)
% 6.85/1.34 % (724255)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=2731002734:i=1254:kws=precedence:bd=preordered:av=off:rtra=on_2990 on theBenchmark for (2990ds/1254Mi)
% 6.85/1.34 % (724255)Refutation not found, incomplete strategy
% 6.85/1.34 % (724255)------------------------------
% 6.85/1.34 % (724255)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.85/1.34 % (724255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/1.34 % (724255)CaDiCaL version: 2.1.3
% 6.85/1.34 % (724255)Termination reason: Refutation not found, incomplete strategy
% 6.85/1.34 % (724255)Time elapsed: 0.001 s
% 6.85/1.34 % (724255)Peak memory usage: 12 MB
% 6.85/1.34 % (724255)Instructions burned: 3 (million)
% 6.85/1.34 % (724253)Refutation not found, incomplete strategy
% 6.85/1.34 % (724253)------------------------------
% 6.85/1.34 % (724253)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.85/1.34 % (724255)------------------------------
% 6.85/1.34 % (724255)------------------------------
% 6.85/1.34 % (724253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/1.34 % (724253)CaDiCaL version: 2.1.3
% 6.85/1.34 % (724253)Termination reason: Refutation not found, incomplete strategy
% 6.85/1.34 % (724253)Time elapsed: 0.002 s
% 6.85/1.34 % (724253)Peak memory usage: 12 MB
% 6.85/1.34 % (724253)Instructions burned: 2 (million)
% 6.85/1.34 % (724253)------------------------------
% 6.85/1.34 % (724253)------------------------------
% 6.85/1.34 % (724240)Refutation not found, incomplete strategy
% 6.85/1.34 % (724240)------------------------------
% 6.85/1.34 % (724240)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.85/1.38 % (724240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/1.38 % (724240)CaDiCaL version: 2.1.3
% 6.85/1.38 % (724240)Termination reason: Refutation not found, incomplete strategy
% 6.85/1.38 % (724240)Time elapsed: 0.054 s
% 6.85/1.38 % (724240)Peak memory usage: 12 MB
% 6.85/1.38 % (724240)Instructions burned: 106 (million)
% 6.85/1.38 % (724240)------------------------------
% 6.85/1.38 % (724240)------------------------------
% 6.85/1.38 % (724257)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 6.85/1.38 % (724260)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=324964259:i=619:add=on:rtra=on_2990 on theBenchmark for (2990ds/619Mi)
% 6.85/1.38 % (724257)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=3577480612:s2a=on:i=281:add=on:rtra=on:fe=axiom:fdi=1024_2990 on theBenchmark for (2990ds/281Mi)
% 6.85/1.38 % (724260)Refutation not found, incomplete strategy
% 6.85/1.38 % (724260)------------------------------
% 6.85/1.38 % (724260)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.85/1.38 % (724260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/1.38 % (724260)CaDiCaL version: 2.1.3
% 6.85/1.38 % (724260)Termination reason: Refutation not found, incomplete strategy
% 6.85/1.38 % (724260)Time elapsed: 0.001 s
% 6.85/1.38 % (724260)Peak memory usage: 12 MB
% 6.85/1.38 % (724260)Instructions burned: 2 (million)
% 6.85/1.38 % (724260)------------------------------
% 6.85/1.38 % (724260)------------------------------
% 6.85/1.38 % (724261)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=3328394561:i=865:bs=unit_only:ins=25:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/865Mi)
% 6.85/1.38 % (724265)lrs+1010_64_sil=128000:si=on:avsql=on:uwa=off:random_seed=1680316073:hsq=on:st=3:avsq=on:i=130:avsqr=1,16:sd=1:rtra=on:ss=axioms_2990 on theBenchmark for (2990ds/130Mi)
% 6.85/1.38 % (724234)Instruction limit reached!
% 6.85/1.38 % (724234)------------------------------
% 6.85/1.38 % (724234)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.85/1.38 % (724234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/1.38 % (724234)CaDiCaL version: 2.1.3
% 6.85/1.38 % (724234)Termination reason: Instruction limit
% 6.85/1.38 % (724234)Termination phase: Saturation
% 6.85/1.38 % (724234)Time elapsed: 0.131 s
% 6.85/1.38 % (724234)Peak memory usage: 13 MB
% 6.85/1.38 % (724234)Instructions burned: 272 (million)
% 6.85/1.38 % (724265)Refutation not found, incomplete strategy
% 6.85/1.38 % (724265)------------------------------
% 6.85/1.38 % (724265)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.85/1.38 % (724265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/1.38 % (724265)CaDiCaL version: 2.1.3
% 6.85/1.38 % (724265)Termination reason: Refutation not found, incomplete strategy
% 6.85/1.38 % (724265)Time elapsed: 0.0000 s
% 6.85/1.38 % (724265)Peak memory usage: 12 MB
% 6.85/1.38 % (724265)Instructions burned: 1 (million)
% 6.85/1.38 % (724262)lrs+10_1_sil=128000:si=on:urr=on:random_seed=573163588:i=212:sd=1:rtra=on:ss=axioms:sgt=64_2990 on theBenchmark for (2990ds/212Mi)
% 6.85/1.38 % (724265)------------------------------
% 6.85/1.38 % (724265)------------------------------
% 6.85/1.38 % (724270)lrs+1010_3_sil=128000:si=on:slsq=on:random_seed=1969882976:avsq=on:i=152:avsqr=8,1:hud=5:ins=1:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/152Mi)
% 6.85/1.38 % (724268)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=3571774458:st=1.5:i=346:rtra=on:ss=axioms_2990 on theBenchmark for (2990ds/346Mi)
% 6.85/1.38 % (724268)Refutation not found, incomplete strategy
% 6.85/1.38 % (724268)------------------------------
% 6.85/1.38 % (724268)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.85/1.38 % (724268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/1.38 % (724268)CaDiCaL version: 2.1.3
% 6.85/1.38 % (724268)Termination reason: Refutation not found, incomplete strategy
% 6.85/1.38 % (724268)Time elapsed: 0.003 s
% 6.85/1.38 % (724268)Peak memory usage: 12 MB
% 6.85/1.38 % (724268)Instructions burned: 4 (million)
% 6.85/1.38 % (724268)------------------------------
% 6.85/1.38 % (724268)------------------------------
% 6.85/1.38 % (724273)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=1991742556:i=75:ep=R:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/75Mi)
% 6.85/1.38 % (724273)Refutation not found, incomplete strategy
% 6.85/1.38 % (724273)------------------------------
% 6.85/1.38 % (724273)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.85/1.38 % (724273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/1.38 % (724273)CaDiCaL version: 2.1.3
% 6.85/1.38 % (724273)Termination reason: Refutation not found, incomplete strategy
% 6.85/1.38 % (724273)Time elapsed: 0.004 s
% 6.85/1.38 % (724273)Peak memory usage: 12 MB
% 6.85/1.38 % (724273)Instructions burned: 6 (million)
% 6.85/1.38 % (724273)------------------------------
% 6.85/1.38 % (724273)------------------------------
% 6.85/1.38 % (724270)Instruction limit reached!
% 6.85/1.38 % (724270)------------------------------
% 6.85/1.38 % (724270)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.85/1.38 % (724270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/1.38 % (724270)CaDiCaL version: 2.1.3
% 6.85/1.38 % (724270)Termination reason: Instruction limit
% 6.85/1.38 % (724270)Termination phase: Saturation
% 6.85/1.38 % (724270)Time elapsed: 0.040 s
% 6.85/1.38 % (724270)Peak memory usage: 13 MB
% 6.85/1.38 % (724270)Instructions burned: 156 (million)
% 6.85/1.38 % (724276)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=2103196627:uwa_fpi=on:i=148:doe=on:bd=preordered:rtra=on:fsd=on_2989 on theBenchmark for (2989ds/148Mi)
% 6.85/1.38 % (724276)Refutation not found, incomplete strategy
% 6.85/1.38 % (724276)------------------------------
% 6.85/1.38 % (724276)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.85/1.38 % (724276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/1.38 % (724276)CaDiCaL version: 2.1.3
% 6.85/1.38 % (724276)Termination reason: Refutation not found, incomplete strategy
% 6.85/1.38 % (724276)Time elapsed: 0.002 s
% 6.85/1.38 % (724276)Peak memory usage: 12 MB
% 6.85/1.38 % (724276)Instructions burned: 5 (million)
% 6.85/1.38 % (724276)------------------------------
% 6.85/1.38 % (724276)------------------------------
% 6.85/1.38 % (724275)dis+10_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=one_side_interpreted:nwc=5:random_seed=3221141266:st=2.5:i=387:sd=2:rtra=on:ss=axioms_2989 on theBenchmark for (2989ds/387Mi)
% 6.85/1.38 % (724278)dis+1010_3_si=on:uwa=one_side_interpreted:random_seed=220462233:i=161:piset=and:rtra=on:ntd=on_2989 on theBenchmark for (2989ds/161Mi)
% 6.85/1.38 % (724262)Instruction limit reached!
% 6.85/1.38 % (724262)------------------------------
% 6.85/1.38 % (724262)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.85/1.38 % (724262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/1.38 % (724262)CaDiCaL version: 2.1.3
% 6.85/1.38 % (724262)Termination reason: Instruction limit
% 6.85/1.38 % (724262)Termination phase: Saturation
% 6.85/1.38 % (724262)Time elapsed: 0.112 s
% 6.85/1.38 % (724262)Peak memory usage: 13 MB
% 6.85/1.38 % (724262)Instructions burned: 214 (million)
% 6.85/1.38 % (724278)Instruction limit reached!
% 6.85/1.38 % (724278)------------------------------
% 6.85/1.38 % (724278)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.85/1.38 % (724278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/1.38 % (724278)CaDiCaL version: 2.1.3
% 6.85/1.38 % (724278)Termination reason: Instruction limit
% 6.85/1.38 % (724278)Termination phase: Saturation
% 6.85/1.38 % (724278)Time elapsed: 0.041 s
% 6.85/1.38 % (724278)Peak memory usage: 12 MB
% 6.85/1.38 % (724278)Instructions burned: 163 (million)
% 6.85/1.38 % (724257)Instruction limit reached!
% 6.85/1.38 % (724257)------------------------------
% 6.85/1.38 % (724257)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.85/1.38 % (724257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/1.38 % (724257)CaDiCaL version: 2.1.3
% 6.85/1.38 % (724257)Termination reason: Instruction limit
% 6.85/1.38 % (724257)Termination phase: Saturation
% 6.85/1.38 % (724257)Time elapsed: 0.134 s
% 6.85/1.38 % (724257)Peak memory usage: 13 MB
% 6.85/1.38 % (724257)Instructions burned: 282 (million)
% 6.85/1.38 % (724282)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=1034121710:i=136:add=on:ins=4:rtra=on:sup=off_2989 on theBenchmark for (2989ds/136Mi)
% 6.85/1.38 % (724282)Refutation not found, incomplete strategy
% 6.85/1.38 % (724282)------------------------------
% 6.85/1.38 % (724282)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.85/1.38 % (724282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/1.38 % (724282)CaDiCaL version: 2.1.3
% 6.85/1.38 % (724282)Termination reason: Refutation not found, incomplete strategy
% 6.85/1.38 % (724282)Time elapsed: 0.001 s
% 6.85/1.38 % (724282)Peak memory usage: 12 MB
% 6.85/1.38 % (724282)Instructions burned: 2 (million)
% 6.85/1.38 % (724282)------------------------------
% 6.85/1.38 % (724282)------------------------------
% 6.85/1.38 % (724281)lrs+10_1_sil=128000:si=on:random_seed=274546102:st=5:i=888:sd=3:bd=preordered:rtra=on:ss=axioms_2989 on theBenchmark for (2989ds/888Mi)
% 6.85/1.38 % (724285)dis+1002_5:4_to=kbo:sil=128000:cnfonf=conj_eager:si=on:sp=reverse_arity:lma=off:hi=on:nwc=20:random_seed=4258108438:s2a=on:cond=on:i=93:add=on:bd=preordered:rtra=on:er=filter_2989 on theBenchmark for (2989ds/93Mi)
% 6.85/1.38 % (724283)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=547304301:i=88:s2at=3:nm=2:rtra=on:rawr=on_2989 on theBenchmark for (2989ds/88Mi)
% 6.85/1.38 % (724285) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-724066-724285"...
% 6.85/1.38 % (724285)...printing done.
% 6.85/1.38 % (724285)Refutation found. Thanks to Tanya!
% 6.85/1.38 % SZS status Theorem for theBenchmark
% 6.85/1.38 % SZS output start Proof for theBenchmark
% 6.85/1.38 thf(type_def_5, type, 'type/ind_types/list': $tType > $tType).
% 6.85/1.38 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 6.85/1.38 thf(type_def_7, type, sK0: $tType).
% 6.85/1.38 thf(func_def_0, type, 'const/lists/APPEND': !>[X0: $tType]:(('type/ind_types/list' @ X0 > 'type/ind_types/list' @ X0 > 'type/ind_types/list' @ X0))).
% 6.85/1.38 thf(func_def_1, type, 'const/ind_types/NIL': !>[X0: $tType]:('type/ind_types/list' @ X0)).
% 6.85/1.38 thf(func_def_2, type, 'const/ind_types/CONS': !>[X0: $tType]:((X0 > 'type/ind_types/list' @ X0 > 'type/ind_types/list' @ X0))).
% 6.85/1.38 thf(func_def_4, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 6.85/1.38 thf(func_def_5, type, vIMP: ($o > $o > $o)).
% 6.85/1.38 thf(func_def_6, type, vAND: ($o > $o > $o)).
% 6.85/1.38 thf(func_def_7, type, db2: !>[X0: $tType]:(X0)).
% 6.85/1.38 thf(func_def_8, type, db0: !>[X0: $tType]:(X0)).
% 6.85/1.38 thf(func_def_9, type, db1: !>[X0: $tType]:(X0)).
% 6.85/1.38 thf(func_def_10, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 6.85/1.38 thf(func_def_13, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 6.85/1.38 thf(func_def_14, type, sK1: 'type/ind_types/list' @ sK0).
% 6.85/1.38 thf(func_def_15, type, sK2: 'type/ind_types/list' @ sK0).
% 6.85/1.38 thf(func_def_16, type, sK3: 'type/ind_types/list' @ sK0).
% 6.85/1.38 thf(func_def_17, type, vNOT: ($o > $o)).
% 6.85/1.38 thf(func_def_18, type, sK4: sK0).
% 6.85/1.38 thf(func_def_19, type, sK5: !>[X0: $tType]:((('type/ind_types/list' @ X0 > $o) > X0))).
% 6.85/1.38 thf(func_def_20, type, sK6: !>[X0: $tType]:((('type/ind_types/list' @ X0 > $o) > 'type/ind_types/list' @ X0))).
% 6.85/1.38 thf(func_def_21, type, sK7: 'type/ind_types/list' @ sK0).
% 6.85/1.38 thf(func_def_22, type, sK8: sK0).
% 6.85/1.38 thf(func_def_23, type, sK9: sK0).
% 6.85/1.38 thf(func_def_24, type, sK10: sK0).
% 6.85/1.38 thf(func_def_25, type, sK11: 'type/ind_types/list' @ sK0).
% 6.85/1.38 thf(func_def_26, type, sK12: 'type/ind_types/list' @ sK0).
% 6.85/1.38 thf(func_def_27, type, sK13: 'type/ind_types/list' @ sK0).
% 6.85/1.38 thf(f1,axiom,(
% 6.85/1.38 ! [X0 : $tType,X1 : ('type/ind_types/list' @ X0 > $o)] : (((X1 @ 'const/ind_types/NIL' @ X0) & ! [X3 : 'type/ind_types/list' @ X0,X2 : X0] : ((X1 @ X3) => (X1 @ ('const/ind_types/CONS' @ X0 @ X2 @ X3)))) => ! [X2 : 'type/ind_types/list' @ X0] : (X1 @ X2))),
% 6.85/1.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p','thm/ind_types/list_INDUCT_')).
% 6.85/1.38 thf(f2,axiom,(
% 6.85/1.38 ! [X0 : $tType,X1 : X0,X3 : 'type/ind_types/list' @ X0,X2 : 'type/ind_types/list' @ X0] : ((('const/lists/APPEND' @ X0 @ ('const/ind_types/CONS' @ X0 @ X1 @ X2) @ X3)) = (('const/ind_types/CONS' @ X0 @ X1 @ ('const/lists/APPEND' @ X0 @ X2 @ X3))))),
% 6.85/1.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p','thm/lists/APPEND_1')).
% 6.85/1.38 thf(f3,axiom,(
% 6.85/1.38 ! [X0 : $tType,X1 : 'type/ind_types/list' @ X0] : ((('const/lists/APPEND' @ X0 @ 'const/ind_types/NIL' @ X0 @ X1)) = X1)),
% 6.85/1.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p','thm/lists/APPEND_0')).
% 6.85/1.38 thf(f4,conjecture,(
% 6.85/1.38 ! [X0 : $tType,X3 : 'type/ind_types/list' @ X0,X1 : 'type/ind_types/list' @ X0,X2 : 'type/ind_types/list' @ X0] : ((('const/lists/APPEND' @ X0 @ X1 @ ('const/lists/APPEND' @ X0 @ X2 @ X3))) = (('const/lists/APPEND' @ X0 @ ('const/lists/APPEND' @ X0 @ X1 @ X2) @ X3)))),
% 6.85/1.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p','thm/lists/APPEND_ASSOC_')).
% 6.85/1.38 thf(f5,negated_conjecture,(
% 6.85/1.38 ~ ! [X0 : $tType,X3 : 'type/ind_types/list' @ X0,X1 : 'type/ind_types/list' @ X0,X2 : 'type/ind_types/list' @ X0] : ((('const/lists/APPEND' @ X0 @ X1 @ ('const/lists/APPEND' @ X0 @ X2 @ X3))) = (('const/lists/APPEND' @ X0 @ ('const/lists/APPEND' @ X0 @ X1 @ X2) @ X3)))),
% 6.85/1.38 inference(negated_conjecture,[status(cth)],[f4])).
% 6.85/1.38 thf(f6,plain,(
% 6.85/1.38 ! [X0 : $tType,X1 : ('type/ind_types/list' @ X0 > $o)] : (((X1 @ 'const/ind_types/NIL' @ X0) & ! [X2 : 'type/ind_types/list' @ X0,X3 : X0] : ((X1 @ X2) => (X1 @ ('const/ind_types/CONS' @ X0 @ X3 @ X2)))) => ! [X4 : 'type/ind_types/list' @ X0] : (X1 @ X4))),
% 6.85/1.38 inference(rectify,[],[f1])).
% 6.85/1.38 thf(f7,plain,(
% 6.85/1.38 ( ! [X0 : $tType] : ((((!! @ ('type/ind_types/list' @ X0 > $o) @ (^[Y0 : 'type/ind_types/list' @ X0 > $o]: (((!! @ X0 @ (^[Y1 : X0]: (!! @ 'type/ind_types/list' @ X0 @ (^[Y2 : 'type/ind_types/list' @ X0]: ((Y0 @ Y2) => (Y0 @ ('const/ind_types/CONS' @ X0 @ Y1 @ Y2))))))) & (Y0 @ 'const/ind_types/NIL' @ X0)) => (!! @ 'type/ind_types/list' @ X0 @ (^[Y1 : 'type/ind_types/list' @ X0]: (Y0 @ Y1))))))) = $true)) )),
% 6.85/1.38 inference(fool_elimination,[],[f6])).
% 6.85/1.38 thf(f8,plain,(
% 6.85/1.38 ( ! [X0 : $tType] : ((((!! @ 'type/ind_types/list' @ X0 @ (^[Y0 : 'type/ind_types/list' @ X0]: (('const/lists/APPEND' @ X0 @ 'const/ind_types/NIL' @ X0 @ Y0) = Y0)))) = $true)) )),
% 6.85/1.38 inference(fool_elimination,[],[f3])).
% 6.85/1.38 thf(f9,plain,(
% 6.85/1.38 ! [X0 : $tType,X1 : X0,X2 : 'type/ind_types/list' @ X0,X3 : 'type/ind_types/list' @ X0] : ((('const/lists/APPEND' @ X0 @ ('const/ind_types/CONS' @ X0 @ X1 @ X3) @ X2)) = (('const/ind_types/CONS' @ X0 @ X1 @ ('const/lists/APPEND' @ X0 @ X3 @ X2))))),
% 6.85/1.38 inference(rectify,[],[f2])).
% 6.85/1.38 thf(f10,plain,(
% 6.85/1.38 ( ! [X0 : $tType] : ((((!! @ 'type/ind_types/list' @ X0 @ (^[Y0 : 'type/ind_types/list' @ X0]: (!! @ 'type/ind_types/list' @ X0 @ (^[Y1 : 'type/ind_types/list' @ X0]: (!! @ X0 @ (^[Y2 : X0]: (('const/lists/APPEND' @ X0 @ ('const/ind_types/CONS' @ X0 @ Y2 @ Y0) @ Y1) = ('const/ind_types/CONS' @ X0 @ Y2 @ ('const/lists/APPEND' @ X0 @ Y0 @ Y1)))))))))) = $true)) )),
% 6.85/1.38 inference(fool_elimination,[],[f9])).
% 6.85/1.38 thf(f11,plain,(
% 6.85/1.38 ! [X0 : $tType] : (((!! @ ('type/ind_types/list' @ X0 > $o) @ (^[Y0 : 'type/ind_types/list' @ X0 > $o]: (((!! @ X0 @ (^[Y1 : X0]: (!! @ 'type/ind_types/list' @ X0 @ (^[Y2 : 'type/ind_types/list' @ X0]: ((Y0 @ Y2) => (Y0 @ ('const/ind_types/CONS' @ X0 @ Y1 @ Y2))))))) & (Y0 @ 'const/ind_types/NIL' @ X0)) => (!! @ 'type/ind_types/list' @ X0 @ (^[Y1 : 'type/ind_types/list' @ X0]: (Y0 @ Y1))))))) = $true)),
% 6.85/1.38 inference(closure,[],[f7])).
% 6.85/1.38 thf(f12,plain,(
% 6.85/1.38 ! [X0 : $tType] : (((!! @ 'type/ind_types/list' @ X0 @ (^[Y0 : 'type/ind_types/list' @ X0]: (('const/lists/APPEND' @ X0 @ 'const/ind_types/NIL' @ X0 @ Y0) = Y0)))) = $true)),
% 6.85/1.38 inference(closure,[],[f8])).
% 6.85/1.38 thf(f13,plain,(
% 6.85/1.38 ! [X0 : $tType] : (((!! @ 'type/ind_types/list' @ X0 @ (^[Y0 : 'type/ind_types/list' @ X0]: (!! @ 'type/ind_types/list' @ X0 @ (^[Y1 : 'type/ind_types/list' @ X0]: (!! @ X0 @ (^[Y2 : X0]: (('const/lists/APPEND' @ X0 @ ('const/ind_types/CONS' @ X0 @ Y2 @ Y0) @ Y1) = ('const/ind_types/CONS' @ X0 @ Y2 @ ('const/lists/APPEND' @ X0 @ Y0 @ Y1)))))))))) = $true)),
% 6.85/1.38 inference(closure,[],[f10])).
% 6.85/1.38 thf(f14,plain,(
% 6.85/1.38 ~ ! [X0 : $tType,X3 : 'type/ind_types/list' @ X0,X1 : 'type/ind_types/list' @ X0,X2 : 'type/ind_types/list' @ X0] : ((('const/lists/APPEND' @ X0 @ X2 @ ('const/lists/APPEND' @ X0 @ X3 @ X1))) = (('const/lists/APPEND' @ X0 @ ('const/lists/APPEND' @ X0 @ X2 @ X3) @ X1)))),
% 6.85/1.38 inference(rectify,[],[f5])).
% 6.85/1.38 thf(f15,plain,(
% 6.85/1.38 ? [X0 : $tType,X1 : 'type/ind_types/list' @ X0,X3 : 'type/ind_types/list' @ X0,X2 : 'type/ind_types/list' @ X0] : ((('const/lists/APPEND' @ X0 @ X2 @ ('const/lists/APPEND' @ X0 @ X3 @ X1))) != (('const/lists/APPEND' @ X0 @ ('const/lists/APPEND' @ X0 @ X2 @ X3) @ X1)))),
% 6.85/1.38 inference(ennf_transformation,[],[f14])).
% 6.85/1.38 thf(f16,plain,(
% 6.85/1.38 ? [X0 : $tType,X1 : 'type/ind_types/list' @ X0,X2 : 'type/ind_types/list' @ X0,X3 : 'type/ind_types/list' @ X0] : ((('const/lists/APPEND' @ X0 @ ('const/lists/APPEND' @ X0 @ X3 @ X2) @ X1)) != (('const/lists/APPEND' @ X0 @ X3 @ ('const/lists/APPEND' @ X0 @ X2 @ X1))))),
% 6.85/1.38 inference(rectify,[],[f15])).
% 6.85/1.38 thf(f17,plain,(
% 6.85/1.38 ((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ sK3 @ sK2) @ sK1)) != (('const/lists/APPEND' @ sK0 @ sK3 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1))))),
% 6.85/1.38 inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3)],[f16])).
% 6.85/1.38 thf(f18,plain,(
% 6.85/1.38 ( ! [X0 : $tType] : ((((!! @ 'type/ind_types/list' @ X0 @ (^[Y0 : 'type/ind_types/list' @ X0]: (('const/lists/APPEND' @ X0 @ 'const/ind_types/NIL' @ X0 @ Y0) = Y0)))) = $true)) )),
% 6.85/1.38 inference(cnf_transformation,[],[f12])).
% 6.85/1.38 thf(f19,plain,(
% 6.85/1.38 ( ! [X0 : $tType] : ((((!! @ ('type/ind_types/list' @ X0 > $o) @ (^[Y0 : 'type/ind_types/list' @ X0 > $o]: (((!! @ X0 @ (^[Y1 : X0]: (!! @ 'type/ind_types/list' @ X0 @ (^[Y2 : 'type/ind_types/list' @ X0]: ((Y0 @ Y2) => (Y0 @ ('const/ind_types/CONS' @ X0 @ Y1 @ Y2))))))) & (Y0 @ 'const/ind_types/NIL' @ X0)) => (!! @ 'type/ind_types/list' @ X0 @ (^[Y1 : 'type/ind_types/list' @ X0]: (Y0 @ Y1))))))) = $true)) )),
% 6.85/1.38 inference(cnf_transformation,[],[f11])).
% 6.85/1.38 thf(f20,plain,(
% 6.85/1.38 ( ! [X0 : $tType] : ((((!! @ 'type/ind_types/list' @ X0 @ (^[Y0 : 'type/ind_types/list' @ X0]: (!! @ 'type/ind_types/list' @ X0 @ (^[Y1 : 'type/ind_types/list' @ X0]: (!! @ X0 @ (^[Y2 : X0]: (('const/lists/APPEND' @ X0 @ ('const/ind_types/CONS' @ X0 @ Y2 @ Y0) @ Y1) = ('const/ind_types/CONS' @ X0 @ Y2 @ ('const/lists/APPEND' @ X0 @ Y0 @ Y1)))))))))) = $true)) )),
% 6.85/1.38 inference(cnf_transformation,[],[f13])).
% 6.85/1.38 thf(f21,plain,(
% 6.85/1.38 ((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ sK3 @ sK2) @ sK1)) != (('const/lists/APPEND' @ sK0 @ sK3 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1))))),
% 6.85/1.38 inference(cnf_transformation,[],[f17])).
% 6.85/1.38 thf(f24,plain,(
% 6.85/1.38 ( ! [X0 : $tType] : ((((!! @ ('type/ind_types/list' @ X0 > $o) @ (^[Y0 : 'type/ind_types/list' @ X0 > $o]: (((!! @ X0 @ (^[Y1 : X0]: (!! @ 'type/ind_types/list' @ X0 @ (^[Y2 : 'type/ind_types/list' @ X0]: ((Y0 @ Y2) => (Y0 @ ('const/ind_types/CONS' @ X0 @ Y1 @ Y2))))))) & (Y0 @ 'const/ind_types/NIL' @ X0)) => (!! @ 'type/ind_types/list' @ X0 @ Y0))))) = $true)) )),
% 6.85/1.38 inference(beta-eta_normalization,[],[f19])).
% 6.85/1.38 thf(f28,plain,(
% 6.85/1.38 ((((^[Y0 : 'type/ind_types/list' @ sK0 > $o]: (((!! @ sK0 @ (^[Y1 : sK0]: (!! @ 'type/ind_types/list' @ sK0 @ (^[Y2 : 'type/ind_types/list' @ sK0]: ((Y0 @ Y2) => (Y0 @ ('const/ind_types/CONS' @ sK0 @ Y1 @ Y2))))))) & (Y0 @ 'const/ind_types/NIL' @ sK0)) => (!! @ 'type/ind_types/list' @ sK0 @ Y0))) @ (^[Y0 : 'type/ind_types/list' @ sK0]: (('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ Y0 @ sK2) @ sK1) = ('const/lists/APPEND' @ sK0 @ Y0 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1)))))) = $true)),
% 6.85/1.38 inference(heuristic_instantiation,[],[f24])).
% 6.85/1.38 thf(f30,plain,(
% 6.85/1.38 (((((!! @ sK0 @ (^[Y0 : sK0]: (!! @ 'type/ind_types/list' @ sK0 @ (^[Y1 : 'type/ind_types/list' @ sK0]: ((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ Y1 @ sK2) @ sK1) = ('const/lists/APPEND' @ sK0 @ Y1 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1))) => (('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ ('const/ind_types/CONS' @ sK0 @ Y0 @ Y1) @ sK2) @ sK1) = ('const/lists/APPEND' @ sK0 @ ('const/ind_types/CONS' @ sK0 @ Y0 @ Y1) @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1)))))))) & (('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ 'const/ind_types/NIL' @ sK0 @ sK2) @ sK1) = ('const/lists/APPEND' @ sK0 @ 'const/ind_types/NIL' @ sK0 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1)))) => (!! @ 'type/ind_types/list' @ sK0 @ (^[Y0 : 'type/ind_types/list' @ sK0]: (('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ Y0 @ sK2) @ sK1) = ('const/lists/APPEND' @ sK0 @ Y0 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1))))))) = $true)),
% 6.85/1.38 inference(beta-eta_normalization,[],[f28])).
% 6.85/1.38 thf(f35,plain,(
% 6.85/1.38 ( ! [X0 : $tType,X1 : 'type/ind_types/list' @ X0] : (((((^[Y0 : 'type/ind_types/list' @ X0]: (('const/lists/APPEND' @ X0 @ 'const/ind_types/NIL' @ X0 @ Y0) = Y0)) @ X1)) = $true)) )),
% 6.85/1.38 inference(pi_proxy_clausification,[],[f18])).
% 6.85/1.38 thf(f36,plain,(
% 6.85/1.38 ( ! [X0 : $tType,X1 : 'type/ind_types/list' @ X0] : ((((('const/lists/APPEND' @ X0 @ 'const/ind_types/NIL' @ X0 @ X1) = X1)) = $true)) )),
% 6.85/1.38 inference(beta-eta_normalization,[],[f35])).
% 6.85/1.38 thf(f37,plain,(
% 6.85/1.38 ( ! [X0 : $tType,X1 : 'type/ind_types/list' @ X0] : (((((^[Y0 : 'type/ind_types/list' @ X0]: (!! @ 'type/ind_types/list' @ X0 @ (^[Y1 : 'type/ind_types/list' @ X0]: (!! @ X0 @ (^[Y2 : X0]: (('const/lists/APPEND' @ X0 @ ('const/ind_types/CONS' @ X0 @ Y2 @ Y0) @ Y1) = ('const/ind_types/CONS' @ X0 @ Y2 @ ('const/lists/APPEND' @ X0 @ Y0 @ Y1)))))))) @ X1)) = $true)) )),
% 6.85/1.38 inference(pi_proxy_clausification,[],[f20])).
% 6.85/1.38 thf(f38,plain,(
% 6.85/1.38 ( ! [X0 : $tType,X1 : 'type/ind_types/list' @ X0] : ((((!! @ 'type/ind_types/list' @ X0 @ (^[Y0 : 'type/ind_types/list' @ X0]: (!! @ X0 @ (^[Y1 : X0]: (('const/lists/APPEND' @ X0 @ ('const/ind_types/CONS' @ X0 @ Y1 @ X1) @ Y0) = ('const/ind_types/CONS' @ X0 @ Y1 @ ('const/lists/APPEND' @ X0 @ X1 @ Y0)))))))) = $true)) )),
% 6.85/1.38 inference(beta-eta_normalization,[],[f37])).
% 6.85/1.38 thf(f39,plain,(
% 6.85/1.38 ((((!! @ sK0 @ (^[Y0 : sK0]: (!! @ 'type/ind_types/list' @ sK0 @ (^[Y1 : 'type/ind_types/list' @ sK0]: ((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ Y1 @ sK2) @ sK1) = ('const/lists/APPEND' @ sK0 @ Y1 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1))) => (('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ ('const/ind_types/CONS' @ sK0 @ Y0 @ Y1) @ sK2) @ sK1) = ('const/lists/APPEND' @ sK0 @ ('const/ind_types/CONS' @ sK0 @ Y0 @ Y1) @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1)))))))) & (('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ 'const/ind_types/NIL' @ sK0 @ sK2) @ sK1) = ('const/lists/APPEND' @ sK0 @ 'const/ind_types/NIL' @ sK0 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1))))) = $false) | (((!! @ 'type/ind_types/list' @ sK0 @ (^[Y0 : 'type/ind_types/list' @ sK0]: (('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ Y0 @ sK2) @ sK1) = ('const/lists/APPEND' @ sK0 @ Y0 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1)))))) = $true)),
% 6.85/1.38 inference(imp_proxy_clausification,[],[f30])).
% 6.85/1.38 thf(f44,plain,(
% 6.85/1.38 ( ! [X0 : $tType,X1 : 'type/ind_types/list' @ X0] : (((('const/lists/APPEND' @ X0 @ 'const/ind_types/NIL' @ X0 @ X1)) = X1)) )),
% 6.85/1.38 inference(equality_proxy_clausification,[],[f36])).
% 6.85/1.38 thf(f45,plain,(
% 6.85/1.38 ( ! [X0 : $tType,X2 : 'type/ind_types/list' @ X0,X1 : 'type/ind_types/list' @ X0] : (((((^[Y0 : 'type/ind_types/list' @ X0]: (!! @ X0 @ (^[Y1 : X0]: (('const/lists/APPEND' @ X0 @ ('const/ind_types/CONS' @ X0 @ Y1 @ X1) @ Y0) = ('const/ind_types/CONS' @ X0 @ Y1 @ ('const/lists/APPEND' @ X0 @ X1 @ Y0)))))) @ X2)) = $true)) )),
% 6.85/1.38 inference(pi_proxy_clausification,[],[f38])).
% 6.85/1.38 thf(f46,plain,(
% 6.85/1.38 ( ! [X0 : $tType,X2 : 'type/ind_types/list' @ X0,X1 : 'type/ind_types/list' @ X0] : ((((!! @ X0 @ (^[Y0 : X0]: (('const/lists/APPEND' @ X0 @ ('const/ind_types/CONS' @ X0 @ Y0 @ X1) @ X2) = ('const/ind_types/CONS' @ X0 @ Y0 @ ('const/lists/APPEND' @ X0 @ X1 @ X2)))))) = $true)) )),
% 6.85/1.38 inference(beta-eta_normalization,[],[f45])).
% 6.85/1.38 thf(f47,plain,(
% 6.85/1.38 (((!! @ 'type/ind_types/list' @ sK0 @ (^[Y0 : 'type/ind_types/list' @ sK0]: (('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ Y0 @ sK2) @ sK1) = ('const/lists/APPEND' @ sK0 @ Y0 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1)))))) = $true) | (((!! @ sK0 @ (^[Y0 : sK0]: (!! @ 'type/ind_types/list' @ sK0 @ (^[Y1 : 'type/ind_types/list' @ sK0]: ((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ Y1 @ sK2) @ sK1) = ('const/lists/APPEND' @ sK0 @ Y1 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1))) => (('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ ('const/ind_types/CONS' @ sK0 @ Y0 @ Y1) @ sK2) @ sK1) = ('const/lists/APPEND' @ sK0 @ ('const/ind_types/CONS' @ sK0 @ Y0 @ Y1) @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1))))))))) = $false) | (((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ 'const/ind_types/NIL' @ sK0 @ sK2) @ sK1) = ('const/lists/APPEND' @ sK0 @ 'const/ind_types/NIL' @ sK0 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1)))) = $false)),
% 6.85/1.38 inference(and_proxy_clausification,[],[f39])).
% 6.85/1.38 thf(f58,plain,(
% 6.85/1.38 ( ! [X0 : $tType,X2 : 'type/ind_types/list' @ X0,X3 : X0,X1 : 'type/ind_types/list' @ X0] : (((((^[Y0 : X0]: (('const/lists/APPEND' @ X0 @ ('const/ind_types/CONS' @ X0 @ Y0 @ X1) @ X2) = ('const/ind_types/CONS' @ X0 @ Y0 @ ('const/lists/APPEND' @ X0 @ X1 @ X2)))) @ X3)) = $true)) )),
% 6.85/1.38 inference(pi_proxy_clausification,[],[f46])).
% 6.85/1.38 thf(f61,plain,(
% 6.85/1.38 ( ! [X0 : $tType,X2 : 'type/ind_types/list' @ X0,X3 : X0,X1 : 'type/ind_types/list' @ X0] : ((((('const/lists/APPEND' @ X0 @ ('const/ind_types/CONS' @ X0 @ X3 @ X1) @ X2) = ('const/ind_types/CONS' @ X0 @ X3 @ ('const/lists/APPEND' @ X0 @ X1 @ X2)))) = $true)) )),
% 6.85/1.38 inference(beta-eta_normalization,[],[f58])).
% 6.85/1.38 thf(f64,plain,(
% 6.85/1.38 ( ! [X1 : 'type/ind_types/list' @ sK0] : (((((^[Y0 : 'type/ind_types/list' @ sK0]: (('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ Y0 @ sK2) @ sK1) = ('const/lists/APPEND' @ sK0 @ Y0 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1)))) @ X1)) = $true) | (((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ 'const/ind_types/NIL' @ sK0 @ sK2) @ sK1) = ('const/lists/APPEND' @ sK0 @ 'const/ind_types/NIL' @ sK0 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1)))) = $false) | (((!! @ sK0 @ (^[Y0 : sK0]: (!! @ 'type/ind_types/list' @ sK0 @ (^[Y1 : 'type/ind_types/list' @ sK0]: ((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ Y1 @ sK2) @ sK1) = ('const/lists/APPEND' @ sK0 @ Y1 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1))) => (('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ ('const/ind_types/CONS' @ sK0 @ Y0 @ Y1) @ sK2) @ sK1) = ('const/lists/APPEND' @ sK0 @ ('const/ind_types/CONS' @ sK0 @ Y0 @ Y1) @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1))))))))) = $false)) )),
% 6.85/1.38 inference(pi_proxy_clausification,[],[f47])).
% 6.85/1.38 thf(f65,plain,(
% 6.85/1.38 ( ! [X1 : 'type/ind_types/list' @ sK0] : ((((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ X1 @ sK2) @ sK1) = ('const/lists/APPEND' @ sK0 @ X1 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1)))) = $true) | (((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ 'const/ind_types/NIL' @ sK0 @ sK2) @ sK1) = ('const/lists/APPEND' @ sK0 @ 'const/ind_types/NIL' @ sK0 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1)))) = $false) | (((!! @ sK0 @ (^[Y0 : sK0]: (!! @ 'type/ind_types/list' @ sK0 @ (^[Y1 : 'type/ind_types/list' @ sK0]: ((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ Y1 @ sK2) @ sK1) = ('const/lists/APPEND' @ sK0 @ Y1 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1))) => (('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ ('const/ind_types/CONS' @ sK0 @ Y0 @ Y1) @ sK2) @ sK1) = ('const/lists/APPEND' @ sK0 @ ('const/ind_types/CONS' @ sK0 @ Y0 @ Y1) @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1))))))))) = $false)) )),
% 6.85/1.38 inference(beta-eta_normalization,[],[f64])).
% 6.85/1.38 thf(f73,plain,(
% 6.85/1.38 ( ! [X0 : $tType,X2 : 'type/ind_types/list' @ X0,X3 : X0,X1 : 'type/ind_types/list' @ X0] : (((('const/lists/APPEND' @ X0 @ ('const/ind_types/CONS' @ X0 @ X3 @ X1) @ X2)) = (('const/ind_types/CONS' @ X0 @ X3 @ ('const/lists/APPEND' @ X0 @ X1 @ X2))))) )),
% 6.85/1.38 inference(equality_proxy_clausification,[],[f61])).
% 6.85/1.38 thf(f76,plain,(
% 6.85/1.38 ( ! [X1 : 'type/ind_types/list' @ sK0] : ((((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ 'const/ind_types/NIL' @ sK0 @ sK2) @ sK1) = ('const/lists/APPEND' @ sK0 @ 'const/ind_types/NIL' @ sK0 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1)))) = $false) | (((!! @ sK0 @ (^[Y0 : sK0]: (!! @ 'type/ind_types/list' @ sK0 @ (^[Y1 : 'type/ind_types/list' @ sK0]: ((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ Y1 @ sK2) @ sK1) = ('const/lists/APPEND' @ sK0 @ Y1 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1))) => (('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ ('const/ind_types/CONS' @ sK0 @ Y0 @ Y1) @ sK2) @ sK1) = ('const/lists/APPEND' @ sK0 @ ('const/ind_types/CONS' @ sK0 @ Y0 @ Y1) @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1))))))))) = $false) | ((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ X1 @ sK2) @ sK1)) = (('const/lists/APPEND' @ sK0 @ X1 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1))))) )),
% 6.85/1.38 inference(equality_proxy_clausification,[],[f65])).
% 6.85/1.38 thf(f82,plain,(
% 6.85/1.38 ( ! [X1 : 'type/ind_types/list' @ sK0] : (((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ 'const/ind_types/NIL' @ sK0 @ sK2) @ sK1)) != (('const/lists/APPEND' @ sK0 @ 'const/ind_types/NIL' @ sK0 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1)))) | (((!! @ sK0 @ (^[Y0 : sK0]: (!! @ 'type/ind_types/list' @ sK0 @ (^[Y1 : 'type/ind_types/list' @ sK0]: ((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ Y1 @ sK2) @ sK1) = ('const/lists/APPEND' @ sK0 @ Y1 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1))) => (('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ ('const/ind_types/CONS' @ sK0 @ Y0 @ Y1) @ sK2) @ sK1) = ('const/lists/APPEND' @ sK0 @ ('const/ind_types/CONS' @ sK0 @ Y0 @ Y1) @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1))))))))) = $false) | ((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ X1 @ sK2) @ sK1)) = (('const/lists/APPEND' @ sK0 @ X1 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1))))) )),
% 6.85/1.38 inference(equality_proxy_clausification,[],[f76])).
% 6.85/1.38 thf(f90,plain,(
% 6.85/1.38 ( ! [X1 : 'type/ind_types/list' @ sK0] : (((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ X1 @ sK2) @ sK1)) = (('const/lists/APPEND' @ sK0 @ X1 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1)))) | ((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ 'const/ind_types/NIL' @ sK0 @ sK2) @ sK1)) != (('const/lists/APPEND' @ sK0 @ 'const/ind_types/NIL' @ sK0 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1)))) | ((((^[Y0 : sK0]: (!! @ 'type/ind_types/list' @ sK0 @ (^[Y1 : 'type/ind_types/list' @ sK0]: ((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ Y1 @ sK2) @ sK1) = ('const/lists/APPEND' @ sK0 @ Y1 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1))) => (('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ ('const/ind_types/CONS' @ sK0 @ Y0 @ Y1) @ sK2) @ sK1) = ('const/lists/APPEND' @ sK0 @ ('const/ind_types/CONS' @ sK0 @ Y0 @ Y1) @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1))))))) @ sK9)) = $false)) )),
% 6.85/1.38 inference(sigma_proxy_clausification,[],[f82])).
% 6.85/1.38 thf(f91,plain,(
% 6.85/1.38 ( ! [X1 : 'type/ind_types/list' @ sK0] : (((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ 'const/ind_types/NIL' @ sK0 @ sK2) @ sK1)) != (('const/lists/APPEND' @ sK0 @ 'const/ind_types/NIL' @ sK0 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1)))) | ((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ X1 @ sK2) @ sK1)) = (('const/lists/APPEND' @ sK0 @ X1 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1)))) | (((!! @ 'type/ind_types/list' @ sK0 @ (^[Y0 : 'type/ind_types/list' @ sK0]: ((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ Y0 @ sK2) @ sK1) = ('const/lists/APPEND' @ sK0 @ Y0 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1))) => (('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ ('const/ind_types/CONS' @ sK0 @ sK9 @ Y0) @ sK2) @ sK1) = ('const/lists/APPEND' @ sK0 @ ('const/ind_types/CONS' @ sK0 @ sK9 @ Y0) @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1))))))) = $false)) )),
% 6.85/1.38 inference(beta-eta_normalization,[],[f90])).
% 6.85/1.38 thf(f101,plain,(
% 6.85/1.38 ( ! [X1 : 'type/ind_types/list' @ sK0] : (((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ 'const/ind_types/NIL' @ sK0 @ sK2) @ sK1)) != (('const/lists/APPEND' @ sK0 @ 'const/ind_types/NIL' @ sK0 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1)))) | ((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ X1 @ sK2) @ sK1)) = (('const/lists/APPEND' @ sK0 @ X1 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1)))) | ((((^[Y0 : 'type/ind_types/list' @ sK0]: ((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ Y0 @ sK2) @ sK1) = ('const/lists/APPEND' @ sK0 @ Y0 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1))) => (('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ ('const/ind_types/CONS' @ sK0 @ sK9 @ Y0) @ sK2) @ sK1) = ('const/lists/APPEND' @ sK0 @ ('const/ind_types/CONS' @ sK0 @ sK9 @ Y0) @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1))))) @ sK12)) = $false)) )),
% 6.85/1.38 inference(sigma_proxy_clausification,[],[f91])).
% 6.85/1.38 thf(f102,plain,(
% 6.85/1.38 ( ! [X1 : 'type/ind_types/list' @ sK0] : (((((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ sK12 @ sK2) @ sK1) = ('const/lists/APPEND' @ sK0 @ sK12 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1))) => (('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ ('const/ind_types/CONS' @ sK0 @ sK9 @ sK12) @ sK2) @ sK1) = ('const/lists/APPEND' @ sK0 @ ('const/ind_types/CONS' @ sK0 @ sK9 @ sK12) @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1))))) = $false) | ((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ 'const/ind_types/NIL' @ sK0 @ sK2) @ sK1)) != (('const/lists/APPEND' @ sK0 @ 'const/ind_types/NIL' @ sK0 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1)))) | ((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ X1 @ sK2) @ sK1)) = (('const/lists/APPEND' @ sK0 @ X1 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1))))) )),
% 6.85/1.38 inference(beta-eta_normalization,[],[f101])).
% 6.85/1.38 thf(f108,plain,(
% 6.85/1.38 ( ! [X1 : 'type/ind_types/list' @ sK0] : (((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ X1 @ sK2) @ sK1)) = (('const/lists/APPEND' @ sK0 @ X1 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1)))) | (((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ ('const/ind_types/CONS' @ sK0 @ sK9 @ sK12) @ sK2) @ sK1) = ('const/lists/APPEND' @ sK0 @ ('const/ind_types/CONS' @ sK0 @ sK9 @ sK12) @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1)))) = $false) | ((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ 'const/ind_types/NIL' @ sK0 @ sK2) @ sK1)) != (('const/lists/APPEND' @ sK0 @ 'const/ind_types/NIL' @ sK0 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1))))) )),
% 6.85/1.38 inference(imp_proxy_clausification,[],[f102])).
% 6.85/1.38 thf(f109,plain,(
% 6.85/1.38 ( ! [X1 : 'type/ind_types/list' @ sK0] : (((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ X1 @ sK2) @ sK1)) = (('const/lists/APPEND' @ sK0 @ X1 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1)))) | ((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ 'const/ind_types/NIL' @ sK0 @ sK2) @ sK1)) != (('const/lists/APPEND' @ sK0 @ 'const/ind_types/NIL' @ sK0 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1)))) | (((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ sK12 @ sK2) @ sK1) = ('const/lists/APPEND' @ sK0 @ sK12 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1)))) = $true)) )),
% 6.85/1.38 inference(imp_proxy_clausification,[],[f102])).
% 6.85/1.38 thf(f118,plain,(
% 6.85/1.38 ( ! [X1 : 'type/ind_types/list' @ sK0] : (((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ X1 @ sK2) @ sK1)) = (('const/lists/APPEND' @ sK0 @ X1 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1)))) | ((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ 'const/ind_types/NIL' @ sK0 @ sK2) @ sK1)) != (('const/lists/APPEND' @ sK0 @ 'const/ind_types/NIL' @ sK0 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1)))) | ((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ sK12 @ sK2) @ sK1)) = (('const/lists/APPEND' @ sK0 @ sK12 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1))))) )),
% 6.85/1.38 inference(equality_proxy_clausification,[],[f109])).
% 6.85/1.38 thf(f119,plain,(
% 6.85/1.38 ((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ sK12 @ sK2) @ sK1)) = (('const/lists/APPEND' @ sK0 @ sK12 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1)))) | ((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ 'const/ind_types/NIL' @ sK0 @ sK2) @ sK1)) != (('const/lists/APPEND' @ sK0 @ 'const/ind_types/NIL' @ sK0 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1))))),
% 6.85/1.38 inference(condensation,[],[f118])).
% 6.85/1.38 thf(f120,plain,(
% 6.85/1.38 ( ! [X1 : 'type/ind_types/list' @ sK0] : (((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ X1 @ sK2) @ sK1)) = (('const/lists/APPEND' @ sK0 @ X1 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1)))) | ((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ 'const/ind_types/NIL' @ sK0 @ sK2) @ sK1)) != (('const/lists/APPEND' @ sK0 @ 'const/ind_types/NIL' @ sK0 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1)))) | ((('const/lists/APPEND' @ sK0 @ ('const/ind_types/CONS' @ sK0 @ sK9 @ sK12) @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1))) != (('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ ('const/ind_types/CONS' @ sK0 @ sK9 @ sK12) @ sK2) @ sK1)))) )),
% 6.85/1.38 inference(equality_proxy_clausification,[],[f108])).
% 6.85/1.38 thf(f131,definition,(
% 6.85/1.38 spl14_1 <=> ((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ 'const/ind_types/NIL' @ sK0 @ sK2) @ sK1)) = (('const/lists/APPEND' @ sK0 @ 'const/ind_types/NIL' @ sK0 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1))))),
% 6.85/1.38 introduced(definition,[new_symbols(definition,[spl14_1])],[avatar_definition])).
% 6.85/1.38 thf(f133,plain,(
% 6.85/1.38 ((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ 'const/ind_types/NIL' @ sK0 @ sK2) @ sK1)) != (('const/lists/APPEND' @ sK0 @ 'const/ind_types/NIL' @ sK0 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1)))) | spl14_1),
% 6.85/1.38 inference(avatar_component_clause,[],[f131])).
% 6.85/1.38 thf(f135,definition,(
% 6.85/1.38 spl14_2 <=> ((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ sK12 @ sK2) @ sK1)) = (('const/lists/APPEND' @ sK0 @ sK12 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1))))),
% 6.85/1.38 introduced(definition,[new_symbols(definition,[spl14_2])],[avatar_definition])).
% 6.85/1.38 thf(f137,plain,(
% 6.85/1.38 ((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ sK12 @ sK2) @ sK1)) = (('const/lists/APPEND' @ sK0 @ sK12 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1)))) | ~spl14_2),
% 6.85/1.38 inference(avatar_component_clause,[],[f135])).
% 6.85/1.38 thf(f138,plain,(
% 6.85/1.38 ~spl14_1 | spl14_2),
% 6.85/1.38 inference(avatar_split_clause,[],[f119,f135,f131])).
% 6.85/1.38 thf(f140,definition,(
% 6.85/1.38 spl14_3 <=> ! [X1 : 'type/ind_types/list' @ sK0] : ((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ X1 @ sK2) @ sK1)) = (('const/lists/APPEND' @ sK0 @ X1 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1))))),
% 6.85/1.38 introduced(definition,[new_symbols(definition,[spl14_3])],[avatar_definition])).
% 6.85/1.38 thf(f141,plain,(
% 6.85/1.38 ( ! [X1 : 'type/ind_types/list' @ sK0] : (((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ X1 @ sK2) @ sK1)) = (('const/lists/APPEND' @ sK0 @ X1 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1))))) ) | ~spl14_3),
% 6.85/1.38 inference(avatar_component_clause,[],[f140])).
% 6.85/1.38 thf(f143,definition,(
% 6.85/1.38 spl14_4 <=> ((('const/lists/APPEND' @ sK0 @ ('const/ind_types/CONS' @ sK0 @ sK9 @ sK12) @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1))) = (('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ ('const/ind_types/CONS' @ sK0 @ sK9 @ sK12) @ sK2) @ sK1)))),
% 6.85/1.38 introduced(definition,[new_symbols(definition,[spl14_4])],[avatar_definition])).
% 6.85/1.38 thf(f145,plain,(
% 6.85/1.38 ((('const/lists/APPEND' @ sK0 @ ('const/ind_types/CONS' @ sK0 @ sK9 @ sK12) @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1))) != (('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ ('const/ind_types/CONS' @ sK0 @ sK9 @ sK12) @ sK2) @ sK1))) | spl14_4),
% 6.85/1.38 inference(avatar_component_clause,[],[f143])).
% 6.85/1.38 thf(f146,plain,(
% 6.85/1.38 spl14_3 | ~spl14_4 | ~spl14_1),
% 6.85/1.38 inference(avatar_split_clause,[],[f120,f131,f143,f140])).
% 6.85/1.38 thf(f516,plain,(
% 6.85/1.38 ((('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ 'const/ind_types/NIL' @ sK0 @ sK2) @ sK1)) != (('const/lists/APPEND' @ sK0 @ sK2 @ sK1))) | spl14_1),
% 6.85/1.38 inference(forward_demodulation,[],[f133,f44])).
% 6.85/1.38 thf(f517,plain,(
% 6.85/1.38 ((('const/lists/APPEND' @ sK0 @ sK2 @ sK1)) != (('const/lists/APPEND' @ sK0 @ sK2 @ sK1))) | spl14_1),
% 6.85/1.38 inference(forward_demodulation,[],[f516,f44])).
% 6.85/1.38 thf(f518,plain,(
% 6.85/1.38 $false | spl14_1),
% 6.85/1.38 inference(trivial_inequality_removal,[],[f517])).
% 6.85/1.38 thf(f519,plain,(
% 6.85/1.38 spl14_1),
% 6.85/1.38 inference(avatar_contradiction_clause,[],[f518])).
% 6.85/1.38 thf(f521,plain,(
% 6.85/1.38 ((('const/lists/APPEND' @ sK0 @ ('const/ind_types/CONS' @ sK0 @ sK9 @ sK12) @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1))) != (('const/lists/APPEND' @ sK0 @ ('const/ind_types/CONS' @ sK0 @ sK9 @ ('const/lists/APPEND' @ sK0 @ sK12 @ sK2)) @ sK1))) | spl14_4),
% 6.85/1.38 inference(forward_demodulation,[],[f145,f73])).
% 6.85/1.38 thf(f522,plain,(
% 6.85/1.38 ((('const/lists/APPEND' @ sK0 @ ('const/ind_types/CONS' @ sK0 @ sK9 @ sK12) @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1))) != (('const/ind_types/CONS' @ sK0 @ sK9 @ ('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ sK12 @ sK2) @ sK1)))) | spl14_4),
% 6.85/1.38 inference(forward_demodulation,[],[f521,f73])).
% 6.85/1.38 thf(f523,plain,(
% 6.85/1.38 ((('const/ind_types/CONS' @ sK0 @ sK9 @ ('const/lists/APPEND' @ sK0 @ ('const/lists/APPEND' @ sK0 @ sK12 @ sK2) @ sK1))) != (('const/ind_types/CONS' @ sK0 @ sK9 @ ('const/lists/APPEND' @ sK0 @ sK12 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1))))) | spl14_4),
% 6.85/1.38 inference(forward_demodulation,[],[f522,f73])).
% 6.85/1.38 thf(f693,plain,(
% 6.85/1.38 ((('const/ind_types/CONS' @ sK0 @ sK9 @ ('const/lists/APPEND' @ sK0 @ sK12 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1)))) != (('const/ind_types/CONS' @ sK0 @ sK9 @ ('const/lists/APPEND' @ sK0 @ sK12 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1))))) | (~spl14_2 | spl14_4)),
% 6.85/1.38 inference(forward_demodulation,[],[f523,f137])).
% 6.85/1.38 thf(f694,plain,(
% 6.85/1.38 $false | (~spl14_2 | spl14_4)),
% 6.85/1.38 inference(trivial_inequality_removal,[],[f693])).
% 6.85/1.38 thf(f695,plain,(
% 6.85/1.38 ~spl14_2 | spl14_4),
% 6.85/1.38 inference(avatar_contradiction_clause,[],[f694])).
% 6.85/1.38 thf(f713,plain,(
% 6.85/1.38 ((('const/lists/APPEND' @ sK0 @ sK3 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1))) != (('const/lists/APPEND' @ sK0 @ sK3 @ ('const/lists/APPEND' @ sK0 @ sK2 @ sK1)))) | ~spl14_3),
% 6.85/1.38 inference(backward_demodulation,[],[f21,f141])).
% 6.85/1.38 thf(f716,plain,(
% 6.85/1.38 $false | ~spl14_3),
% 6.85/1.38 inference(trivial_inequality_removal,[],[f713])).
% 6.85/1.38 thf(f717,plain,(
% 6.85/1.38 ~spl14_3),
% 6.85/1.38 inference(avatar_contradiction_clause,[],[f716])).
% 6.85/1.38 cnf(s1, plain, ~spl14_1 | spl14_2, inference(sat_conversion,[],[f138])).
% 6.85/1.38 cnf(s2, plain, ~spl14_1 | spl14_3 | ~spl14_4, inference(sat_conversion,[],[f146])).
% 6.85/1.38 cnf(s11, plain, spl14_1, inference(sat_conversion,[],[f519])).
% 6.85/1.38 cnf(s15, plain, ~spl14_2 | spl14_4, inference(sat_conversion,[],[f695])).
% 6.85/1.38 cnf(s16, plain, ~spl14_3, inference(sat_conversion,[],[f717])).
% 6.85/1.38 cnf(s17, plain, ~spl14_4, inference(rat,[],[s2,s16,s11])).
% 6.85/1.38 cnf(s18, plain, ~spl14_2, inference(rat,[],[s15,s17])).
% 6.85/1.38 cnf(s19, plain, $false, inference(rat,[],[s1,s18,s11])).
% 6.85/1.38 thf(f720,plain,(
% 6.85/1.38 $false),
% 6.85/1.38 inference(avatar_sat_refutation,[],[s19])).
% 6.85/1.38 % SZS output end Proof for theBenchmark
% 6.85/1.38 % (724285)------------------------------
% 6.85/1.38 % (724285)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.85/1.38 % (724285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/1.38 % (724285)CaDiCaL version: 2.1.3
% 6.85/1.38 % (724285)Termination reason: Refutation
% 6.85/1.38 % (724285)Time elapsed: 0.025 s
% 6.85/1.38 % (724285)Peak memory usage: 13 MB
% 6.85/1.38 % (724285)Instructions burned: 92 (million)
% 6.85/1.38 % (724066)Success in time 1.128 s
% 6.85/1.38 % Vampire exiting
%------------------------------------------------------------------------------