%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEV319^6 : TPTP v9.3.1. Released v5.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:38:15 AM UTC 2026
% Result : Theorem 13.96s 2.43s
% Output : Refutation 13.96s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEV319^6 : TPTP v9.3.1. Released v5.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.17 % Computer : n001.cluster.edu
% 0.09/0.17 % Model : x86_64 x86_64
% 0.09/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.17 % Memory : 8046.5625MB
% 0.09/0.17 % OS : Linux 6.8.0-71-generic
% 0.09/0.17 % CPULimit : 300
% 0.09/0.17 % WCLimit : 300
% 0.09/0.17 % DateTime : Tue Sep 29 15:42:36 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.21 Running higher-order theorem proving
% 0.09/0.22 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
% 1.16/0.46 % (1391918)Detected a higher-order problem, will run a greedy HOL sequence.
% 1.16/0.46 % (1391940)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=548540151: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)
% 1.16/0.46 % (1391938)lrs+10_16_si=on:nwc=1.5:random_seed=3207757997:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 1.16/0.46 % (1391937)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3478922303:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 1.16/0.46 % (1391939)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=1170043794:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 1.16/0.46 % (1391941)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=3384984671:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 1.16/0.46 % (1391943)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 1.16/0.46 % (1391943)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
% 1.16/0.46 % (1391939)Instruction limit reached!
% 1.16/0.46 % (1391939)------------------------------
% 1.16/0.46 % (1391939)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.46 % (1391939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.46 % (1391939)CaDiCaL version: 2.1.3
% 1.16/0.46 % (1391939)Termination reason: Instruction limit
% 1.16/0.46 % (1391939)Termination phase: Saturation
% 1.16/0.46 % (1391939)Time elapsed: 0.005 s
% 1.16/0.46 % (1391939)Peak memory usage: 12 MB
% 1.16/0.46 % (1391939)Instructions burned: 3 (million)
% 1.16/0.46 % (1391942)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=1798258846:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 1.16/0.46 % (1391943)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=521669158:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 1.16/0.46 % (1391938)Instruction limit reached!
% 1.16/0.46 % (1391938)------------------------------
% 1.16/0.46 % (1391938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.46 % (1391938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.46 % (1391938)CaDiCaL version: 2.1.3
% 1.16/0.46 % (1391938)Termination reason: Instruction limit
% 1.16/0.46 % (1391938)Termination phase: Saturation
% 1.16/0.46 % (1391938)Time elapsed: 0.019 s
% 1.16/0.46 % (1391938)Peak memory usage: 12 MB
% 1.16/0.46 % (1391938)Instructions burned: 18 (million)
% 1.16/0.46 % (1391941)Instruction limit reached!
% 1.16/0.46 % (1391941)------------------------------
% 1.16/0.46 % (1391941)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.46 % (1391941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.46 % (1391941)CaDiCaL version: 2.1.3
% 1.16/0.46 % (1391941)Termination reason: Instruction limit
% 1.16/0.46 % (1391941)Termination phase: Saturation
% 1.16/0.46 % (1391941)Time elapsed: 0.025 s
% 1.16/0.46 % (1391941)Peak memory usage: 12 MB
% 1.16/0.46 % (1391941)Instructions burned: 25 (million)
% 1.16/0.46 % (1391951)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3474161020:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 1.16/0.46 % (1391951)Instruction limit reached!
% 1.16/0.46 % (1391951)------------------------------
% 1.16/0.46 % (1391951)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.46 % (1391951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.46 % (1391951)CaDiCaL version: 2.1.3
% 1.16/0.46 % (1391951)Termination reason: Instruction limit
% 1.16/0.46 % (1391951)Termination phase: Saturation
% 1.16/0.46 % (1391951)Time elapsed: 0.003 s
% 1.16/0.46 % (1391951)Peak memory usage: 12 MB
% 1.16/0.46 % (1391951)Instructions burned: 2 (million)
% 1.16/0.46 % (1391952)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=1416668772:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 1.16/0.52 % (1391953)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.16/0.52 % (1391953)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3498455876:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 1.16/0.52 % (1391952)Instruction limit reached!
% 1.16/0.52 % (1391952)------------------------------
% 1.16/0.52 % (1391952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.52 % (1391952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.52 % (1391952)CaDiCaL version: 2.1.3
% 1.16/0.52 % (1391952)Termination reason: Instruction limit
% 1.16/0.52 % (1391952)Termination phase: Saturation
% 1.16/0.52 % (1391952)Time elapsed: 0.007 s
% 1.16/0.52 % (1391952)Peak memory usage: 12 MB
% 1.16/0.52 % (1391952)Instructions burned: 5 (million)
% 1.16/0.52 % (1391953)Instruction limit reached!
% 1.16/0.52 % (1391953)------------------------------
% 1.16/0.52 % (1391953)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.52 % (1391953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.52 % (1391953)CaDiCaL version: 2.1.3
% 1.16/0.52 % (1391953)Termination reason: Instruction limit
% 1.16/0.52 % (1391953)Termination phase: Saturation
% 1.16/0.52 % (1391953)Time elapsed: 0.008 s
% 1.16/0.52 % (1391953)Peak memory usage: 12 MB
% 1.16/0.52 % (1391953)Instructions burned: 7 (million)
% 1.16/0.52 % (1391955)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=1080749780:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 1.16/0.52 % (1391942)Instruction limit reached!
% 1.16/0.52 % (1391942)------------------------------
% 1.16/0.52 % (1391942)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.52 % (1391942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.52 % (1391942)CaDiCaL version: 2.1.3
% 1.16/0.52 % (1391942)Termination reason: Instruction limit
% 1.16/0.52 % (1391942)Termination phase: Saturation
% 1.16/0.52 % (1391942)Time elapsed: 0.072 s
% 1.16/0.52 % (1391942)Peak memory usage: 13 MB
% 1.16/0.52 % (1391942)Instructions burned: 75 (million)
% 1.16/0.52 % (1391937)Instruction limit reached!
% 1.16/0.52 % (1391937)------------------------------
% 1.16/0.52 % (1391937)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.52 % (1391937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.52 % (1391937)CaDiCaL version: 2.1.3
% 1.16/0.52 % (1391937)Termination reason: Instruction limit
% 1.16/0.52 % (1391937)Termination phase: Saturation
% 1.16/0.52 % (1391937)Time elapsed: 0.082 s
% 1.16/0.52 % (1391937)Peak memory usage: 12 MB
% 1.16/0.52 % (1391937)Instructions burned: 88 (million)
% 1.16/0.52 % (1391958)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
% 1.16/0.52 % (1391958)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.16/0.52 % (1391958)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=4014156490:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2998 on theBenchmark for (2998ds/28Mi)
% 1.16/0.52 % (1391955)Instruction limit reached!
% 1.16/0.52 % (1391955)------------------------------
% 1.16/0.52 % (1391955)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.52 % (1391955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.52 % (1391955)CaDiCaL version: 2.1.3
% 1.16/0.52 % (1391955)Termination reason: Instruction limit
% 1.16/0.52 % (1391955)Termination phase: Saturation
% 1.16/0.52 % (1391955)Time elapsed: 0.017 s
% 1.16/0.52 % (1391955)Peak memory usage: 12 MB
% 1.16/0.52 % (1391955)Instructions burned: 15 (million)
% 1.16/0.52 % (1391959)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=3595058635:i=86:piset=equals:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/86Mi)
% 1.16/0.52 % (1391962)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 1.97/0.57 % (1391962)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=557204685:i=2:add=on:rtra=on_2998 on theBenchmark for (2998ds/2Mi)
% 1.97/0.57 % (1391962)Instruction limit reached!
% 1.97/0.57 % (1391962)------------------------------
% 1.97/0.57 % (1391962)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.97/0.57 % (1391962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.97/0.57 % (1391962)CaDiCaL version: 2.1.3
% 1.97/0.57 % (1391962)Termination reason: Instruction limit
% 1.97/0.57 % (1391962)Termination phase: Saturation
% 1.97/0.57 % (1391962)Time elapsed: 0.003 s
% 1.97/0.57 % (1391962)Peak memory usage: 11 MB
% 1.97/0.57 % (1391962)Instructions burned: 2 (million)
% 1.97/0.57 % (1391958)Instruction limit reached!
% 1.97/0.57 % (1391958)------------------------------
% 1.97/0.57 % (1391958)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.97/0.57 % (1391961)lrs+10_1_si=on:cs=on:random_seed=3494233425:i=8:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.97/0.57 % (1391958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.97/0.57 % (1391958)CaDiCaL version: 2.1.3
% 1.97/0.57 % (1391958)Termination reason: Instruction limit
% 1.97/0.57 % (1391958)Termination phase: Saturation
% 1.97/0.57 % (1391958)Time elapsed: 0.026 s
% 1.97/0.57 % (1391958)Peak memory usage: 12 MB
% 1.97/0.57 % (1391958)Instructions burned: 28 (million)
% 1.97/0.57 % (1391964)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=2652977605:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/38Mi)
% 1.97/0.57 % (1391961)Instruction limit reached!
% 1.97/0.57 % (1391961)------------------------------
% 1.97/0.57 % (1391961)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.97/0.57 % (1391961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.97/0.57 % (1391961)CaDiCaL version: 2.1.3
% 1.97/0.57 % (1391961)Termination reason: Instruction limit
% 1.97/0.57 % (1391961)Termination phase: Saturation
% 1.97/0.57 % (1391961)Time elapsed: 0.018 s
% 1.97/0.57 % (1391961)Peak memory usage: 12 MB
% 1.97/0.57 % (1391961)Instructions burned: 8 (million)
% 1.97/0.57 % (1391968)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=1937235989:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 1.97/0.57 % (1391943)Instruction limit reached!
% 1.97/0.57 % (1391943)------------------------------
% 1.97/0.57 % (1391943)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.97/0.57 % (1391943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.97/0.57 % (1391943)CaDiCaL version: 2.1.3
% 1.97/0.57 % (1391943)Termination reason: Instruction limit
% 1.97/0.57 % (1391943)Termination phase: Saturation
% 1.97/0.57 % (1391943)Time elapsed: 0.144 s
% 1.97/0.57 % (1391943)Peak memory usage: 12 MB
% 1.97/0.57 % (1391943)Instructions burned: 157 (million)
% 1.97/0.57 % (1391969)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=2794883122:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 1.97/0.57 % (1391964)Instruction limit reached!
% 1.97/0.57 % (1391964)------------------------------
% 1.97/0.57 % (1391964)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.97/0.57 % (1391964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.97/0.57 % (1391964)CaDiCaL version: 2.1.3
% 1.97/0.57 % (1391964)Termination reason: Instruction limit
% 1.97/0.57 % (1391964)Termination phase: Saturation
% 1.97/0.57 % (1391964)Time elapsed: 0.036 s
% 1.97/0.57 % (1391964)Peak memory usage: 12 MB
% 1.97/0.57 % (1391964)Instructions burned: 39 (million)
% 1.97/0.57 % (1391971)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=114163895:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.97/0.57 % (1391940)Instruction limit reached!
% 1.97/0.57 % (1391940)------------------------------
% 1.97/0.57 % (1391940)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.97/0.57 % (1391940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.97/0.57 % (1391940)CaDiCaL version: 2.1.3
% 1.97/0.57 % (1391940)Termination reason: Instruction limit
% 1.97/0.57 % (1391940)Termination phase: Saturation
% 1.97/0.57 % (1391940)Time elapsed: 0.187 s
% 1.97/0.65 % (1391940)Peak memory usage: 12 MB
% 1.97/0.65 % (1391940)Instructions burned: 634 (million)
% 1.97/0.65 % (1391959)Instruction limit reached!
% 1.97/0.65 % (1391959)------------------------------
% 1.97/0.65 % (1391959)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.97/0.65 % (1391959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.97/0.65 % (1391959)CaDiCaL version: 2.1.3
% 1.97/0.65 % (1391959)Termination reason: Instruction limit
% 1.97/0.65 % (1391959)Termination phase: Saturation
% 1.97/0.65 % (1391959)Time elapsed: 0.079 s
% 1.97/0.65 % (1391959)Peak memory usage: 12 MB
% 1.97/0.65 % (1391959)Instructions burned: 86 (million)
% 1.97/0.65 % (1391973)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=2917797224:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/327Mi)
% 1.97/0.65 % (1391969)Instruction limit reached!
% 1.97/0.65 % (1391969)------------------------------
% 1.97/0.65 % (1391969)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.97/0.65 % (1391969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.97/0.65 % (1391969)CaDiCaL version: 2.1.3
% 1.97/0.65 % (1391969)Termination reason: Instruction limit
% 1.97/0.65 % (1391969)Termination phase: Saturation
% 1.97/0.65 % (1391969)Time elapsed: 0.025 s
% 1.97/0.65 % (1391969)Peak memory usage: 12 MB
% 1.97/0.65 % (1391969)Instructions burned: 25 (million)
% 1.97/0.65 % (1391971)Instruction limit reached!
% 1.97/0.65 % (1391971)------------------------------
% 1.97/0.65 % (1391971)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.97/0.65 % (1391971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.97/0.65 % (1391971)CaDiCaL version: 2.1.3
% 1.97/0.65 % (1391971)Termination reason: Instruction limit
% 1.97/0.65 % (1391971)Termination phase: Saturation
% 1.97/0.65 % (1391971)Time elapsed: 0.017 s
% 1.97/0.65 % (1391971)Peak memory usage: 12 MB
% 1.97/0.65 % (1391971)Instructions burned: 14 (million)
% 1.97/0.65 % (1391975)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=199201021:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2997 on theBenchmark for (2997ds/14Mi)
% 1.97/0.65 % (1391975)Instruction limit reached!
% 1.97/0.65 % (1391975)------------------------------
% 1.97/0.65 % (1391975)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.97/0.65 % (1391975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.97/0.65 % (1391975)CaDiCaL version: 2.1.3
% 1.97/0.65 % (1391975)Termination reason: Instruction limit
% 1.97/0.65 % (1391975)Termination phase: Saturation
% 1.97/0.65 % (1391975)Time elapsed: 0.015 s
% 1.97/0.65 % (1391975)Peak memory usage: 12 MB
% 1.97/0.65 % (1391975)Instructions burned: 14 (million)
% 1.97/0.65 % (1391978)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3268429163:i=26:ep=R:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/26Mi)
% 1.97/0.65 % (1391980)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=3826091598:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2997 on theBenchmark for (2997ds/23Mi)
% 1.97/0.65 % (1391981)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=1119072037:cond=on:i=60:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/60Mi)
% 1.97/0.65 % (1391977)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=972209422:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2997 on theBenchmark for (2997ds/2Mi)
% 1.97/0.65 % (1391977)Instruction limit reached!
% 1.97/0.65 % (1391977)------------------------------
% 1.97/0.65 % (1391977)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.97/0.65 % (1391977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.97/0.65 % (1391977)CaDiCaL version: 2.1.3
% 1.97/0.65 % (1391977)Termination reason: Instruction limit
% 1.97/0.65 % (1391977)Termination phase: Saturation
% 1.97/0.65 % (1391977)Time elapsed: 0.003 s
% 1.97/0.65 % (1391977)Peak memory usage: 12 MB
% 1.97/0.65 % (1391977)Instructions burned: 4 (million)
% 1.97/0.65 % (1391983)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.97/0.65 % (1391983)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 3.07/0.77 % (1391978)Instruction limit reached!
% 3.07/0.77 % (1391978)------------------------------
% 3.07/0.77 % (1391978)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.07/0.77 % (1391978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.07/0.77 % (1391978)CaDiCaL version: 2.1.3
% 3.07/0.77 % (1391978)Termination reason: Instruction limit
% 3.07/0.77 % (1391978)Termination phase: Saturation
% 3.07/0.77 % (1391978)Time elapsed: 0.026 s
% 3.07/0.77 % (1391978)Peak memory usage: 11 MB
% 3.07/0.77 % (1391978)Instructions burned: 27 (million)
% 3.07/0.77 % (1391980)Instruction limit reached!
% 3.07/0.77 % (1391980)------------------------------
% 3.07/0.77 % (1391980)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.07/0.77 % (1391980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.07/0.77 % (1391980)CaDiCaL version: 2.1.3
% 3.07/0.77 % (1391980)Termination reason: Instruction limit
% 3.07/0.77 % (1391980)Termination phase: Saturation
% 3.07/0.77 % (1391980)Time elapsed: 0.024 s
% 3.07/0.77 % (1391980)Peak memory usage: 11 MB
% 3.07/0.77 % (1391980)Instructions burned: 23 (million)
% 3.07/0.77 % (1391983)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=190878975:i=14:add=off:nm=40:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 3.07/0.77 % (1391988)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 3.07/0.77 % (1391988)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=3489561643:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2997 on theBenchmark for (2997ds/8Mi)
% 3.07/0.77 % (1391988)Instruction limit reached!
% 3.07/0.77 % (1391988)------------------------------
% 3.07/0.77 % (1391988)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.07/0.77 % (1391988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.07/0.77 % (1391988)CaDiCaL version: 2.1.3
% 3.07/0.77 % (1391988)Termination reason: Instruction limit
% 3.07/0.77 % (1391988)Termination phase: Saturation
% 3.07/0.77 % (1391988)Time elapsed: 0.005 s
% 3.07/0.77 % (1391988)Peak memory usage: 12 MB
% 3.07/0.77 % (1391988)Instructions burned: 8 (million)
% 3.07/0.77 % (1391983)Instruction limit reached!
% 3.07/0.77 % (1391983)------------------------------
% 3.07/0.77 % (1391983)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.07/0.77 % (1391983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.07/0.77 % (1391983)CaDiCaL version: 2.1.3
% 3.07/0.77 % (1391983)Termination reason: Instruction limit
% 3.07/0.77 % (1391983)Termination phase: Saturation
% 3.07/0.77 % (1391983)Time elapsed: 0.016 s
% 3.07/0.77 % (1391983)Peak memory usage: 12 MB
% 3.07/0.77 % (1391983)Instructions burned: 14 (million)
% 3.07/0.77 % (1391989)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=4044700847:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2997 on theBenchmark for (2997ds/31Mi)
% 3.07/0.77 % (1391993)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=1105039890:i=23:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/23Mi)
% 3.07/0.77 % (1391990)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=2019236929:i=7:hud=5:bd=preordered:rtra=on:bet=on_2997 on theBenchmark for (2997ds/7Mi)
% 3.07/0.77 % (1391981)Instruction limit reached!
% 3.07/0.77 % (1391981)------------------------------
% 3.07/0.77 % (1391981)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.07/0.77 % (1391981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.07/0.77 % (1391981)CaDiCaL version: 2.1.3
% 3.07/0.77 % (1391981)Termination reason: Instruction limit
% 3.07/0.77 % (1391981)Termination phase: Saturation
% 3.07/0.77 % (1391981)Time elapsed: 0.057 s
% 3.07/0.77 % (1391981)Peak memory usage: 12 MB
% 3.07/0.77 % (1391981)Instructions burned: 60 (million)
% 3.07/0.77 % (1391990)Instruction limit reached!
% 3.07/0.77 % (1391990)------------------------------
% 3.07/0.77 % (1391990)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.07/0.77 % (1391990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.07/0.77 % (1391990)CaDiCaL version: 2.1.3
% 3.62/0.85 % (1391990)Termination reason: Instruction limit
% 3.62/0.85 % (1391990)Termination phase: Saturation
% 3.62/0.85 % (1391990)Time elapsed: 0.008 s
% 3.62/0.85 % (1391990)Peak memory usage: 12 MB
% 3.62/0.85 % (1391990)Instructions burned: 8 (million)
% 3.62/0.85 % (1391993)Instruction limit reached!
% 3.62/0.85 % (1391993)------------------------------
% 3.62/0.85 % (1391993)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.62/0.85 % (1391993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.62/0.85 % (1391993)CaDiCaL version: 2.1.3
% 3.62/0.85 % (1391993)Termination reason: Instruction limit
% 3.62/0.85 % (1391993)Termination phase: Saturation
% 3.62/0.85 % (1391993)Time elapsed: 0.010 s
% 3.62/0.85 % (1391993)Peak memory usage: 11 MB
% 3.62/0.85 % (1391993)Instructions burned: 24 (million)
% 3.62/0.85 % (1391994)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=2745399818:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2996 on theBenchmark for (2996ds/20Mi)
% 3.62/0.85 % (1391989)Instruction limit reached!
% 3.62/0.85 % (1391989)------------------------------
% 3.62/0.85 % (1391989)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.62/0.85 % (1391989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.62/0.85 % (1391989)CaDiCaL version: 2.1.3
% 3.62/0.85 % (1391989)Termination reason: Instruction limit
% 3.62/0.85 % (1391989)Termination phase: Saturation
% 3.62/0.85 % (1391989)Time elapsed: 0.029 s
% 3.62/0.85 % (1391989)Peak memory usage: 12 MB
% 3.62/0.85 % (1391989)Instructions burned: 31 (million)
% 3.62/0.85 % (1391998)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=3053756822:i=1240:rtra=on:ixr=off_2996 on theBenchmark for (2996ds/1240Mi)
% 3.62/0.85 % (1391999)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=2987952934:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2996 on theBenchmark for (2996ds/143Mi)
% 3.62/0.85 % (1392000)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=973403813:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/193Mi)
% 3.62/0.85 % (1392002)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2655546797:i=42:hud=10:rtra=on_2996 on theBenchmark for (2996ds/42Mi)
% 3.62/0.85 % (1391994)Instruction limit reached!
% 3.62/0.85 % (1391994)------------------------------
% 3.62/0.85 % (1391994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.62/0.85 % (1391994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.62/0.85 % (1391994)CaDiCaL version: 2.1.3
% 3.62/0.85 % (1391994)Termination reason: Instruction limit
% 3.62/0.85 % (1391994)Termination phase: Saturation
% 3.62/0.85 % (1391994)Time elapsed: 0.032 s
% 3.62/0.85 % (1391994)Peak memory usage: 12 MB
% 3.62/0.85 % (1391994)Instructions burned: 20 (million)
% 3.62/0.85 % (1392002)Instruction limit reached!
% 3.62/0.85 % (1392002)------------------------------
% 3.62/0.85 % (1392002)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.62/0.85 % (1392002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.62/0.85 % (1392002)CaDiCaL version: 2.1.3
% 3.62/0.85 % (1392002)Termination reason: Instruction limit
% 3.62/0.85 % (1392002)Termination phase: Saturation
% 3.62/0.85 % (1392002)Time elapsed: 0.021 s
% 3.62/0.85 % (1392002)Peak memory usage: 12 MB
% 3.62/0.85 % (1392002)Instructions burned: 43 (million)
% 3.62/0.85 % (1392008)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=4095122149:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/181Mi)
% 3.62/0.85 % (1392007)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 3.62/0.85 % (1391968)Instruction limit reached!
% 3.62/0.85 % (1391968)------------------------------
% 3.62/0.85 % (1391968)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.62/0.85 % (1391968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.62/0.85 % (1391968)CaDiCaL version: 2.1.3
% 3.62/0.85 % (1391968)Termination reason: Instruction limit
% 3.62/0.85 % (1391968)Termination phase: Saturation
% 3.62/0.85 % (1391968)Time elapsed: 0.218 s
% 3.62/0.85 % (1391968)Peak memory usage: 13 MB
% 3.62/0.85 % (1391968)Instructions burned: 249 (million)
% 3.62/0.85 % (1392007)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2500019758:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2996 on theBenchmark for (2996ds/7Mi)
% 4.08/1.06 % (1392007)Instruction limit reached!
% 4.08/1.06 % (1392007)------------------------------
% 4.08/1.06 % (1392007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.08/1.06 % (1392007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.08/1.06 % (1392007)CaDiCaL version: 2.1.3
% 4.08/1.06 % (1392007)Termination reason: Instruction limit
% 4.08/1.06 % (1392007)Termination phase: Saturation
% 4.08/1.06 % (1392007)Time elapsed: 0.008 s
% 4.08/1.06 % (1392007)Peak memory usage: 12 MB
% 4.08/1.06 % (1392007)Instructions burned: 7 (million)
% 4.08/1.06 % (1392011)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=2827287885:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2995 on theBenchmark for (2995ds/169Mi)
% 4.08/1.06 % (1392012)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 4.08/1.06 % (1392012)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=3991326839:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2995 on theBenchmark for (2995ds/6Mi)
% 4.08/1.06 % (1392012)Instruction limit reached!
% 4.08/1.06 % (1392012)------------------------------
% 4.08/1.06 % (1392012)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.08/1.06 % (1392012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.08/1.06 % (1392012)CaDiCaL version: 2.1.3
% 4.08/1.06 % (1392012)Termination reason: Instruction limit
% 4.08/1.06 % (1392012)Termination phase: Saturation
% 4.08/1.06 % (1392012)Time elapsed: 0.008 s
% 4.08/1.06 % (1392012)Peak memory usage: 12 MB
% 4.08/1.06 % (1392012)Instructions burned: 7 (million)
% 4.08/1.06 % (1391999)Instruction limit reached!
% 4.08/1.06 % (1391999)------------------------------
% 4.08/1.06 % (1391999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.08/1.06 % (1391999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.08/1.06 % (1391999)CaDiCaL version: 2.1.3
% 4.08/1.06 % (1391999)Termination reason: Instruction limit
% 4.08/1.06 % (1391999)Termination phase: Saturation
% 4.08/1.06 % (1391999)Time elapsed: 0.130 s
% 4.08/1.06 % (1391999)Peak memory usage: 12 MB
% 4.08/1.06 % (1391999)Instructions burned: 144 (million)
% 4.08/1.06 % (1392015)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=856097500:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2995 on theBenchmark for (2995ds/22Mi)
% 4.08/1.06 % (1391973)Instruction limit reached!
% 4.08/1.06 % (1391973)------------------------------
% 4.08/1.06 % (1391973)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.08/1.06 % (1391973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.08/1.06 % (1391973)CaDiCaL version: 2.1.3
% 4.08/1.06 % (1391973)Termination reason: Instruction limit
% 4.08/1.06 % (1391973)Termination phase: Saturation
% 4.08/1.06 % (1391973)Time elapsed: 0.280 s
% 4.08/1.06 % (1391973)Peak memory usage: 13 MB
% 4.08/1.06 % (1391973)Instructions burned: 328 (million)
% 4.08/1.06 % (1392011)Instruction limit reached!
% 4.08/1.06 % (1392011)------------------------------
% 4.08/1.06 % (1392011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.08/1.06 % (1392011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.08/1.06 % (1392011)CaDiCaL version: 2.1.3
% 4.08/1.06 % (1392011)Termination reason: Instruction limit
% 4.08/1.06 % (1392011)Termination phase: Saturation
% 4.08/1.06 % (1392011)Time elapsed: 0.077 s
% 4.08/1.06 % (1392011)Peak memory usage: 13 MB
% 4.08/1.06 % (1392011)Instructions burned: 170 (million)
% 4.08/1.06 % (1392015)Instruction limit reached!
% 4.08/1.06 % (1392015)------------------------------
% 4.08/1.06 % (1392015)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.08/1.06 % (1392015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.08/1.06 % (1392015)CaDiCaL version: 2.1.3
% 4.08/1.06 % (1392015)Termination reason: Instruction limit
% 4.08/1.06 % (1392015)Termination phase: Saturation
% 4.08/1.06 % (1392015)Time elapsed: 0.022 s
% 4.08/1.06 % (1392015)Peak memory usage: 12 MB
% 4.08/1.06 % (1392015)Instructions burned: 22 (million)
% 4.08/1.06 % (1392016)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=4294174143:i=19:add=on:rtra=on_2994 on theBenchmark for (2994ds/19Mi)
% 6.30/1.25 % (1392000)Instruction limit reached!
% 6.30/1.25 % (1392000)------------------------------
% 6.30/1.25 % (1392000)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.30/1.25 % (1392000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.30/1.25 % (1392000)CaDiCaL version: 2.1.3
% 6.30/1.25 % (1392000)Termination reason: Instruction limit
% 6.30/1.25 % (1392000)Termination phase: Saturation
% 6.30/1.25 % (1392000)Time elapsed: 0.173 s
% 6.30/1.25 % (1392000)Peak memory usage: 13 MB
% 6.30/1.25 % (1392000)Instructions burned: 194 (million)
% 6.30/1.25 % (1392018)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=3131652907:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/316Mi)
% 6.30/1.25 % (1392019)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=2310611985:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2994 on theBenchmark for (2994ds/853Mi)
% 6.30/1.25 % (1392016)Instruction limit reached!
% 6.30/1.25 % (1392016)------------------------------
% 6.30/1.25 % (1392016)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.30/1.25 % (1392016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.30/1.25 % (1392016)CaDiCaL version: 2.1.3
% 6.30/1.25 % (1392016)Termination reason: Instruction limit
% 6.30/1.25 % (1392016)Termination phase: Saturation
% 6.30/1.25 % (1392016)Time elapsed: 0.021 s
% 6.30/1.25 % (1392016)Peak memory usage: 12 MB
% 6.30/1.25 % (1392016)Instructions burned: 19 (million)
% 6.30/1.25 % (1392020)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=3097097855:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2994 on theBenchmark for (2994ds/45Mi)
% 6.30/1.25 % (1392008)Instruction limit reached!
% 6.30/1.25 % (1392008)------------------------------
% 6.30/1.25 % (1392008)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.30/1.25 % (1392008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.30/1.25 % (1392008)CaDiCaL version: 2.1.3
% 6.30/1.25 % (1392008)Termination reason: Instruction limit
% 6.30/1.25 % (1392008)Termination phase: Saturation
% 6.30/1.25 % (1392008)Time elapsed: 0.161 s
% 6.30/1.25 % (1392008)Peak memory usage: 13 MB
% 6.30/1.25 % (1392008)Instructions burned: 181 (million)
% 6.30/1.25 % (1392022)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=3894933491:i=480:rtra=on_2994 on theBenchmark for (2994ds/480Mi)
% 6.30/1.25 % (1392025)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=1991842752:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2994 on theBenchmark for (2994ds/21Mi)
% 6.30/1.25 % (1392028)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 6.30/1.25 % (1392028)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=27403964:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/200Mi)
% 6.30/1.25 % (1392020)Instruction limit reached!
% 6.30/1.25 % (1392020)------------------------------
% 6.30/1.25 % (1392020)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.30/1.25 % (1392020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.30/1.25 % (1392020)CaDiCaL version: 2.1.3
% 6.30/1.25 % (1392020)Termination reason: Instruction limit
% 6.30/1.25 % (1392020)Termination phase: Saturation
% 6.30/1.25 % (1392020)Time elapsed: 0.045 s
% 6.30/1.25 % (1392020)Peak memory usage: 12 MB
% 6.30/1.25 % (1392020)Instructions burned: 45 (million)
% 6.30/1.25 % (1392025)Instruction limit reached!
% 6.30/1.25 % (1392025)------------------------------
% 6.30/1.25 % (1392025)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.30/1.25 % (1392025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.30/1.25 % (1392025)CaDiCaL version: 2.1.3
% 6.30/1.25 % (1392025)Termination reason: Instruction limit
% 6.30/1.25 % (1392025)Termination phase: Saturation
% 6.30/1.25 % (1392025)Time elapsed: 0.022 s
% 7.97/1.52 % (1392025)Peak memory usage: 12 MB
% 7.97/1.52 % (1392025)Instructions burned: 21 (million)
% 7.97/1.52 % (1392031)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=3699010487:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2993 on theBenchmark for (2993ds/13Mi)
% 7.97/1.52 % (1392032)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=3767293543:i=66:s2at=3:nm=2:rtra=on:rawr=on_2993 on theBenchmark for (2993ds/66Mi)
% 7.97/1.52 % (1392031)Instruction limit reached!
% 7.97/1.52 % (1392031)------------------------------
% 7.97/1.52 % (1392031)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.97/1.52 % (1392031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.97/1.52 % (1392031)CaDiCaL version: 2.1.3
% 7.97/1.52 % (1392031)Termination reason: Instruction limit
% 7.97/1.52 % (1392031)Termination phase: Saturation
% 7.97/1.52 % (1392031)Time elapsed: 0.014 s
% 7.97/1.52 % (1392031)Peak memory usage: 12 MB
% 7.97/1.52 % (1392031)Instructions burned: 13 (million)
% 7.97/1.52 % (1392035)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=2547633023:i=51:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/51Mi)
% 7.97/1.52 % (1392032)Instruction limit reached!
% 7.97/1.52 % (1392032)------------------------------
% 7.97/1.52 % (1392032)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.97/1.52 % (1392032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.97/1.52 % (1392032)CaDiCaL version: 2.1.3
% 7.97/1.52 % (1392032)Termination reason: Instruction limit
% 7.97/1.52 % (1392032)Termination phase: Saturation
% 7.97/1.52 % (1392032)Time elapsed: 0.066 s
% 7.97/1.52 % (1392032)Peak memory usage: 13 MB
% 7.97/1.52 % (1392032)Instructions burned: 66 (million)
% 7.97/1.52 % (1392035)Instruction limit reached!
% 7.97/1.52 % (1392035)------------------------------
% 7.97/1.52 % (1392035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.97/1.52 % (1392035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.97/1.52 % (1392035)CaDiCaL version: 2.1.3
% 7.97/1.52 % (1392035)Termination reason: Instruction limit
% 7.97/1.52 % (1392035)Termination phase: Saturation
% 7.97/1.52 % (1392035)Time elapsed: 0.048 s
% 7.97/1.52 % (1392035)Peak memory usage: 12 MB
% 7.97/1.52 % (1392035)Instructions burned: 51 (million)
% 7.97/1.52 % (1392037)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=2433687887:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2992 on theBenchmark for (2992ds/31Mi)
% 7.97/1.52 % (1392038)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=3807560430:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2992 on theBenchmark for (2992ds/137Mi)
% 7.97/1.52 % (1392028)Instruction limit reached!
% 7.97/1.52 % (1392028)------------------------------
% 7.97/1.52 % (1392028)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.97/1.52 % (1392028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.97/1.52 % (1392028)CaDiCaL version: 2.1.3
% 7.97/1.52 % (1392028)Termination reason: Instruction limit
% 7.97/1.52 % (1392028)Termination phase: Saturation
% 7.97/1.52 % (1392028)Time elapsed: 0.172 s
% 7.97/1.52 % (1392028)Peak memory usage: 12 MB
% 7.97/1.52 % (1392028)Instructions burned: 200 (million)
% 7.97/1.52 % (1392037)Instruction limit reached!
% 7.97/1.52 % (1392037)------------------------------
% 7.97/1.52 % (1392037)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.97/1.52 % (1392037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.97/1.52 % (1392037)CaDiCaL version: 2.1.3
% 7.97/1.52 % (1392037)Termination reason: Instruction limit
% 7.97/1.52 % (1392037)Termination phase: Saturation
% 7.97/1.52 % (1392037)Time elapsed: 0.032 s
% 7.97/1.52 % (1392037)Peak memory usage: 12 MB
% 7.97/1.52 % (1392037)Instructions burned: 32 (million)
% 7.97/1.52 % (1392041)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=2344093930:cond=on:i=34:hud=10:nm=10:rtra=on_2992 on theBenchmark for (2992ds/34Mi)
% 7.97/1.52 % (1392042)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=136685441:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2992 on theBenchmark for (2992ds/67Mi)
% 7.97/1.52 % (1392018)Instruction limit reached!
% 7.97/1.52 % (1392018)------------------------------
% 7.97/1.52 % (1392018)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.30/1.70 % (1392018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.30/1.70 % (1392018)CaDiCaL version: 2.1.3
% 8.30/1.70 % (1392018)Termination reason: Instruction limit
% 8.30/1.70 % (1392018)Termination phase: Saturation
% 8.30/1.70 % (1392018)Time elapsed: 0.282 s
% 8.30/1.70 % (1392018)Peak memory usage: 14 MB
% 8.30/1.70 % (1392018)Instructions burned: 316 (million)
% 8.30/1.70 % (1392041)Instruction limit reached!
% 8.30/1.70 % (1392041)------------------------------
% 8.30/1.70 % (1392041)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.30/1.70 % (1392041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.30/1.70 % (1392041)CaDiCaL version: 2.1.3
% 8.30/1.70 % (1392041)Termination reason: Instruction limit
% 8.30/1.70 % (1392041)Termination phase: Saturation
% 8.30/1.70 % (1392041)Time elapsed: 0.034 s
% 8.30/1.70 % (1392041)Peak memory usage: 12 MB
% 8.30/1.70 % (1392041)Instructions burned: 34 (million)
% 8.30/1.70 % (1392045)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 8.73/1.70 % (1392045)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=3818459185:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2991 on theBenchmark for (2991ds/180Mi)
% 8.73/1.70 % (1392038)Instruction limit reached!
% 8.73/1.70 % (1392038)------------------------------
% 8.73/1.70 % (1392038)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.73/1.70 % (1392038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.73/1.70 % (1392038)CaDiCaL version: 2.1.3
% 8.73/1.70 % (1392038)Termination reason: Instruction limit
% 8.73/1.70 % (1392038)Termination phase: Saturation
% 8.73/1.70 % (1392038)Time elapsed: 0.086 s
% 8.73/1.70 % (1392038)Peak memory usage: 12 MB
% 8.73/1.70 % (1392038)Instructions burned: 137 (million)
% 8.73/1.70 % (1392042)Instruction limit reached!
% 8.73/1.70 % (1392042)------------------------------
% 8.73/1.70 % (1392042)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.73/1.70 % (1392042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.73/1.70 % (1392042)CaDiCaL version: 2.1.3
% 8.73/1.70 % (1392042)Termination reason: Instruction limit
% 8.73/1.70 % (1392042)Termination phase: Saturation
% 8.73/1.70 % (1392042)Time elapsed: 0.066 s
% 8.73/1.70 % (1392042)Peak memory usage: 12 MB
% 8.73/1.70 % (1392042)Instructions burned: 67 (million)
% 8.73/1.70 % (1392046)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=2674678884:st=2:i=246:sd=3:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/246Mi)
% 8.73/1.70 % (1392048)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=855129974:cond=on:i=96:bd=all:rtra=on_2991 on theBenchmark for (2991ds/96Mi)
% 8.73/1.70 % (1392049)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=3361981748:i=427:sd=1:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/427Mi)
% 8.73/1.70 % (1392022)Instruction limit reached!
% 8.73/1.70 % (1392022)------------------------------
% 8.73/1.70 % (1392022)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.73/1.70 % (1392022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.73/1.70 % (1392022)CaDiCaL version: 2.1.3
% 8.73/1.70 % (1392022)Termination reason: Instruction limit
% 8.73/1.70 % (1392022)Termination phase: Saturation
% 8.73/1.70 % (1392022)Time elapsed: 0.410 s
% 8.73/1.70 % (1392022)Peak memory usage: 13 MB
% 8.73/1.70 % (1392022)Instructions burned: 480 (million)
% 8.73/1.70 % (1392048)Instruction limit reached!
% 8.73/1.70 % (1392048)------------------------------
% 8.73/1.70 % (1392048)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.73/1.70 % (1392048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.73/1.70 % (1392048)CaDiCaL version: 2.1.3
% 8.73/1.70 % (1392048)Termination reason: Instruction limit
% 8.73/1.70 % (1392048)Termination phase: Saturation
% 8.73/1.70 % (1392048)Time elapsed: 0.090 s
% 8.73/1.70 % (1392048)Peak memory usage: 12 MB
% 8.73/1.70 % (1392048)Instructions burned: 96 (million)
% 8.73/1.70 % (1392045)Instruction limit reached!
% 8.73/1.70 % (1392045)------------------------------
% 8.73/1.70 % (1392045)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.73/1.70 % (1392045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.73/1.70 % (1392045)CaDiCaL version: 2.1.3
% 9.29/1.87 % (1392045)Termination reason: Instruction limit
% 9.29/1.87 % (1392045)Termination phase: Saturation
% 9.29/1.87 % (1392045)Time elapsed: 0.153 s
% 9.29/1.87 % (1392045)Peak memory usage: 13 MB
% 9.29/1.87 % (1392045)Instructions burned: 181 (million)
% 9.29/1.87 % (1392053)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=2253330092:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2990 on theBenchmark for (2990ds/874Mi)
% 9.29/1.87 % (1392054)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=1423501242:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2990 on theBenchmark for (2990ds/515Mi)
% 9.29/1.87 % (1392056)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=3053522449:st=1.5:i=130:rtra=on:ss=axioms_2989 on theBenchmark for (2989ds/130Mi)
% 9.29/1.87 % (1392046)Instruction limit reached!
% 9.29/1.87 % (1392046)------------------------------
% 9.29/1.87 % (1392046)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.29/1.87 % (1392046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.29/1.87 % (1392046)CaDiCaL version: 2.1.3
% 9.29/1.87 % (1392046)Termination reason: Instruction limit
% 9.29/1.87 % (1392046)Termination phase: Saturation
% 9.29/1.87 % (1392046)Time elapsed: 0.218 s
% 9.29/1.87 % (1392046)Peak memory usage: 12 MB
% 9.29/1.87 % (1392046)Instructions burned: 246 (million)
% 9.29/1.87 % (1392049)Instruction limit reached!
% 9.29/1.87 % (1392049)------------------------------
% 9.29/1.87 % (1392049)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.29/1.87 % (1392049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.29/1.87 % (1392049)CaDiCaL version: 2.1.3
% 9.29/1.87 % (1392049)Termination reason: Instruction limit
% 9.29/1.87 % (1392049)Termination phase: Saturation
% 9.29/1.87 % (1392049)Time elapsed: 0.205 s
% 9.29/1.87 % (1392049)Peak memory usage: 14 MB
% 9.29/1.87 % (1392049)Instructions burned: 429 (million)
% 9.29/1.87 % (1392060)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=3801968415:s2a=on:i=571:nm=16:rtra=on_2988 on theBenchmark for (2988ds/571Mi)
% 9.29/1.87 % (1392059)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=155697277:i=44:ep=R:rtra=on:ntd=on_2988 on theBenchmark for (2988ds/44Mi)
% 9.29/1.87 % (1392059)Instruction limit reached!
% 9.29/1.87 % (1392059)------------------------------
% 9.29/1.87 % (1392059)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.29/1.87 % (1392059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.29/1.87 % (1392059)CaDiCaL version: 2.1.3
% 9.29/1.87 % (1392059)Termination reason: Instruction limit
% 9.29/1.87 % (1392059)Termination phase: Saturation
% 9.29/1.87 % (1392059)Time elapsed: 0.042 s
% 9.29/1.87 % (1392059)Peak memory usage: 12 MB
% 9.29/1.87 % (1392059)Instructions burned: 45 (million)
% 9.29/1.87 % (1392056)Instruction limit reached!
% 9.29/1.87 % (1392056)------------------------------
% 9.29/1.87 % (1392056)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.29/1.87 % (1392056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.29/1.87 % (1392056)CaDiCaL version: 2.1.3
% 9.29/1.87 % (1392056)Termination reason: Instruction limit
% 9.29/1.87 % (1392056)Termination phase: Saturation
% 9.29/1.87 % (1392056)Time elapsed: 0.129 s
% 9.29/1.87 % (1392056)Peak memory usage: 12 MB
% 9.29/1.87 % (1392056)Instructions burned: 131 (million)
% 9.29/1.87 % (1392064)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=1125270128:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2988 on theBenchmark for (2988ds/95Mi)
% 9.29/1.87 % (1392063)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=654754959:i=450:rtra=on:ixr=off:ntd=on_2988 on theBenchmark for (2988ds/450Mi)
% 9.29/1.87 % (1392019)Instruction limit reached!
% 9.29/1.87 % (1392019)------------------------------
% 9.29/1.87 % (1392019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.29/1.87 % (1392019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.29/1.87 % (1392019)CaDiCaL version: 2.1.3
% 9.29/1.87 % (1392019)Termination reason: Instruction limit
% 9.29/1.87 % (1392019)Termination phase: Saturation
% 9.29/1.87 % (1392019)Time elapsed: 0.700 s
% 9.29/1.87 % (1392019)Peak memory usage: 15 MB
% 9.29/1.87 % (1392019)Instructions burned: 853 (million)
% 9.29/1.87 % (1392067)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=1658081807:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2987 on theBenchmark for (2987ds/65Mi)
% 12.74/2.12 % (1392064)Instruction limit reached!
% 12.74/2.12 % (1392064)------------------------------
% 12.74/2.12 % (1392064)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.74/2.12 % (1392064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.74/2.12 % (1392064)CaDiCaL version: 2.1.3
% 12.74/2.12 % (1392064)Termination reason: Instruction limit
% 12.74/2.12 % (1392064)Termination phase: Saturation
% 12.74/2.12 % (1392064)Time elapsed: 0.093 s
% 12.74/2.12 % (1392064)Peak memory usage: 12 MB
% 12.74/2.12 % (1392064)Instructions burned: 95 (million)
% 12.74/2.12 % (1392069)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=231451551: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_2986 on theBenchmark for (2986ds/105Mi)
% 12.74/2.12 % (1392067)Instruction limit reached!
% 12.74/2.12 % (1392067)------------------------------
% 12.74/2.12 % (1392067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.74/2.12 % (1392067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.74/2.12 % (1392067)CaDiCaL version: 2.1.3
% 12.74/2.12 % (1392067)Termination reason: Instruction limit
% 12.74/2.12 % (1392067)Termination phase: Saturation
% 12.74/2.12 % (1392067)Time elapsed: 0.061 s
% 12.74/2.12 % (1392067)Peak memory usage: 12 MB
% 12.74/2.12 % (1392067)Instructions burned: 66 (million)
% 12.74/2.12 % (1392060)Instruction limit reached!
% 12.74/2.12 % (1392060)------------------------------
% 12.74/2.12 % (1392060)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.74/2.12 % (1392060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.74/2.12 % (1392060)CaDiCaL version: 2.1.3
% 12.74/2.12 % (1392060)Termination reason: Instruction limit
% 12.74/2.12 % (1392060)Termination phase: Saturation
% 12.74/2.12 % (1392060)Time elapsed: 0.243 s
% 12.74/2.12 % (1392060)Peak memory usage: 14 MB
% 12.74/2.12 % (1392060)Instructions burned: 571 (million)
% 12.74/2.12 % (1392071)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=2277538000:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2986 on theBenchmark for (2986ds/5755Mi)
% 12.74/2.12 % (1391998)Instruction limit reached!
% 12.74/2.12 % (1391998)------------------------------
% 12.74/2.12 % (1391998)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.74/2.12 % (1391998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.74/2.12 % (1391998)CaDiCaL version: 2.1.3
% 12.74/2.12 % (1391998)Termination reason: Instruction limit
% 12.74/2.12 % (1391998)Termination phase: Saturation
% 12.74/2.12 % (1391998)Time elapsed: 1.025 s
% 12.74/2.12 % (1391998)Peak memory usage: 14 MB
% 12.74/2.12 % (1391998)Instructions burned: 1240 (million)
% 12.74/2.12 % (1392074)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=3358147632:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2986 on theBenchmark for (2986ds/495Mi)
% 12.74/2.12 % (1392072)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=1001043497:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2986 on theBenchmark for (2986ds/375Mi)
% 12.74/2.12 % (1392069)Instruction limit reached!
% 12.74/2.12 % (1392069)------------------------------
% 12.74/2.12 % (1392069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.74/2.12 % (1392069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.74/2.12 % (1392069)CaDiCaL version: 2.1.3
% 12.74/2.12 % (1392069)Termination reason: Instruction limit
% 12.74/2.12 % (1392069)Termination phase: Saturation
% 12.74/2.12 % (1392069)Time elapsed: 0.094 s
% 12.74/2.12 % (1392069)Peak memory usage: 13 MB
% 12.74/2.12 % (1392069)Instructions burned: 105 (million)
% 12.74/2.12 % (1392054)Instruction limit reached!
% 12.74/2.12 % (1392054)------------------------------
% 12.74/2.12 % (1392054)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.74/2.12 % (1392054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.74/2.12 % (1392054)CaDiCaL version: 2.1.3
% 12.74/2.12 % (1392054)Termination reason: Instruction limit
% 13.38/2.27 % (1392054)Termination phase: Saturation
% 13.38/2.27 % (1392054)Time elapsed: 0.446 s
% 13.38/2.27 % (1392054)Peak memory usage: 14 MB
% 13.38/2.27 % (1392054)Instructions burned: 516 (million)
% 13.38/2.27 % (1392077)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=3301311550:cond=on:i=34:hud=10:nm=10:rtra=on_2985 on theBenchmark for (2985ds/34Mi)
% 13.38/2.27 % (1392078)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=3733840828:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2985 on theBenchmark for (2985ds/91Mi)
% 13.38/2.27 % (1392077)Instruction limit reached!
% 13.38/2.27 % (1392077)------------------------------
% 13.38/2.27 % (1392077)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.38/2.27 % (1392077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.38/2.27 % (1392077)CaDiCaL version: 2.1.3
% 13.38/2.27 % (1392077)Termination reason: Instruction limit
% 13.38/2.27 % (1392077)Termination phase: Saturation
% 13.38/2.27 % (1392077)Time elapsed: 0.034 s
% 13.38/2.27 % (1392077)Peak memory usage: 12 MB
% 13.38/2.27 % (1392077)Instructions burned: 34 (million)
% 13.38/2.27 % (1392081)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=1318975799:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2984 on theBenchmark for (2984ds/66Mi)
% 13.38/2.27 % (1392078)Instruction limit reached!
% 13.38/2.27 % (1392078)------------------------------
% 13.38/2.27 % (1392078)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.38/2.27 % (1392078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.38/2.27 % (1392078)CaDiCaL version: 2.1.3
% 13.38/2.27 % (1392078)Termination reason: Instruction limit
% 13.38/2.27 % (1392078)Termination phase: Saturation
% 13.38/2.27 % (1392078)Time elapsed: 0.082 s
% 13.38/2.27 % (1392078)Peak memory usage: 12 MB
% 13.38/2.27 % (1392078)Instructions burned: 91 (million)
% 13.38/2.27 % (1392063)Instruction limit reached!
% 13.38/2.27 % (1392063)------------------------------
% 13.38/2.27 % (1392063)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.38/2.27 % (1392063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.38/2.27 % (1392063)CaDiCaL version: 2.1.3
% 13.38/2.27 % (1392063)Termination reason: Instruction limit
% 13.38/2.27 % (1392063)Termination phase: Saturation
% 13.38/2.27 % (1392063)Time elapsed: 0.373 s
% 13.38/2.27 % (1392063)Peak memory usage: 13 MB
% 13.38/2.27 % (1392063)Instructions burned: 451 (million)
% 13.38/2.27 % (1392081)Instruction limit reached!
% 13.38/2.27 % (1392081)------------------------------
% 13.38/2.27 % (1392081)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.38/2.27 % (1392081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.38/2.27 % (1392081)CaDiCaL version: 2.1.3
% 13.38/2.27 % (1392081)Termination reason: Instruction limit
% 13.38/2.27 % (1392081)Termination phase: Saturation
% 13.38/2.27 % (1392081)Time elapsed: 0.063 s
% 13.38/2.27 % (1392081)Peak memory usage: 12 MB
% 13.38/2.27 % (1392081)Instructions burned: 66 (million)
% 13.38/2.27 % (1392083)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=641268061:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2984 on theBenchmark for (2984ds/22Mi)
% 13.38/2.27 % (1392084)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=544814301:i=338:bd=all:ins=4:rtra=on_2984 on theBenchmark for (2984ds/338Mi)
% 13.38/2.27 % (1392074)Instruction limit reached!
% 13.38/2.27 % (1392074)------------------------------
% 13.38/2.27 % (1392074)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.38/2.27 % (1392074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.38/2.27 % (1392074)CaDiCaL version: 2.1.3
% 13.38/2.27 % (1392074)Termination reason: Instruction limit
% 13.38/2.27 % (1392074)Termination phase: Saturation
% 13.38/2.27 % (1392074)Time elapsed: 0.229 s
% 13.38/2.27 % (1392074)Peak memory usage: 15 MB
% 13.38/2.27 % (1392074)Instructions burned: 497 (million)
% 13.38/2.27 % (1392083)Instruction limit reached!
% 13.38/2.27 % (1392083)------------------------------
% 13.38/2.27 % (1392083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.38/2.27 % (1392083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.38/2.27 % (1392083)CaDiCaL version: 2.1.3
% 13.38/2.27 % (1392083)Termination reason: Instruction limit
% 13.96/2.43 % (1392083)Termination phase: Saturation
% 13.96/2.43 % (1392083)Time elapsed: 0.021 s
% 13.96/2.43 % (1392083)Peak memory usage: 12 MB
% 13.96/2.43 % (1392083)Instructions burned: 23 (million)
% 13.96/2.43 % (1392085)lrs+10_1_sil=128000:si=on:urr=on:random_seed=2363774966:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2983 on theBenchmark for (2983ds/28Mi)
% 13.96/2.43 % (1392088)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 13.96/2.43 % (1392088)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=4071965854:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2983 on theBenchmark for (2983ds/137Mi)
% 13.96/2.43 % (1392085)Instruction limit reached!
% 13.96/2.43 % (1392085)------------------------------
% 13.96/2.43 % (1392085)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.96/2.43 % (1392085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.96/2.43 % (1392085)CaDiCaL version: 2.1.3
% 13.96/2.43 % (1392085)Termination reason: Instruction limit
% 13.96/2.43 % (1392085)Termination phase: Saturation
% 13.96/2.43 % (1392085)Time elapsed: 0.029 s
% 13.96/2.43 % (1392085)Peak memory usage: 12 MB
% 13.96/2.43 % (1392085)Instructions burned: 29 (million)
% 13.96/2.43 % (1392089)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=902482959:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2983 on theBenchmark for (2983ds/340Mi)
% 13.96/2.43 % (1392093)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=3389808912:i=227:sd=1:bd=all:rtra=on:ss=axioms_2983 on theBenchmark for (2983ds/227Mi)
% 13.96/2.43 % (1392088)Instruction limit reached!
% 13.96/2.43 % (1392088)------------------------------
% 13.96/2.43 % (1392088)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.96/2.43 % (1392088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.96/2.43 % (1392088)CaDiCaL version: 2.1.3
% 13.96/2.43 % (1392088)Termination reason: Instruction limit
% 13.96/2.43 % (1392088)Termination phase: Saturation
% 13.96/2.43 % (1392088)Time elapsed: 0.065 s
% 13.96/2.43 % (1392088)Peak memory usage: 12 MB
% 13.96/2.43 % (1392088)Instructions burned: 138 (million)
% 13.96/2.43 % (1392095)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 13.96/2.43 % (1392095)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=1271630154:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2982 on theBenchmark for (2982ds/373Mi)
% 13.96/2.43 % (1392053)Instruction limit reached!
% 13.96/2.43 % (1392053)------------------------------
% 13.96/2.43 % (1392053)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.96/2.43 % (1392053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.96/2.43 % (1392053)CaDiCaL version: 2.1.3
% 13.96/2.43 % (1392053)Termination reason: Instruction limit
% 13.96/2.43 % (1392053)Termination phase: Saturation
% 13.96/2.43 % (1392053)Time elapsed: 0.726 s
% 13.96/2.43 % (1392053)Peak memory usage: 14 MB
% 13.96/2.43 % (1392053)Instructions burned: 875 (million)
% 13.96/2.43 % (1392072)Instruction limit reached!
% 13.96/2.43 % (1392072)------------------------------
% 13.96/2.43 % (1392072)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.96/2.43 % (1392072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.96/2.43 % (1392072)CaDiCaL version: 2.1.3
% 13.96/2.43 % (1392072)Termination reason: Instruction limit
% 13.96/2.43 % (1392072)Termination phase: Saturation
% 13.96/2.43 % (1392072)Time elapsed: 0.361 s
% 13.96/2.43 % (1392072)Peak memory usage: 13 MB
% 13.96/2.43 % (1392072)Instructions burned: 375 (million)
% 13.96/2.43 % (1392097)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=346613834:i=116:ep=RSTC:rtra=on:ntd=on_2982 on theBenchmark for (2982ds/116Mi)
% 13.96/2.43 % (1392098)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=262336183:i=575:rtra=on_2982 on theBenchmark for (2982ds/575Mi)
% 13.96/2.43 % (1392097)Instruction limit reached!
% 13.96/2.43 % (1392097)------------------------------
% 13.96/2.43 % (1392097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.96/2.43 % (1392097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.96/2.43 % (1392097)CaDiCaL version: 2.1.3
% 13.96/2.43 % (1392097)Termination reason: Instruction limit
% 13.96/2.43 % (1392097)Termination phase: Saturation
% 13.96/2.43 % (1392097)Time elapsed: 0.101 s
% 13.96/2.43 % (1392097)Peak memory usage: 12 MB
% 13.96/2.43 % (1392097)Instructions burned: 116 (million)
% 13.96/2.43 % (1392095)Instruction limit reached!
% 13.96/2.43 % (1392095)------------------------------
% 13.96/2.43 % (1392095)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.96/2.43 % (1392095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.96/2.43 % (1392095)CaDiCaL version: 2.1.3
% 13.96/2.43 % (1392095)Termination reason: Instruction limit
% 13.96/2.43 % (1392095)Termination phase: Saturation
% 13.96/2.43 % (1392095)Time elapsed: 0.166 s
% 13.96/2.43 % (1392095)Peak memory usage: 14 MB
% 13.96/2.43 % (1392095)Instructions burned: 375 (million)
% 13.96/2.43 % (1392101)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=4220826792:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2981 on theBenchmark for (2981ds/270Mi)
% 13.96/2.43 % (1392102)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=3640127078: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_2980 on theBenchmark for (2980ds/9840Mi)
% 13.96/2.43 % (1392084)Instruction limit reached!
% 13.96/2.43 % (1392084)------------------------------
% 13.96/2.43 % (1392084)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.96/2.43 % (1392084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.96/2.43 % (1392084)CaDiCaL version: 2.1.3
% 13.96/2.43 % (1392084)Termination reason: Instruction limit
% 13.96/2.43 % (1392084)Termination phase: Saturation
% 13.96/2.43 % (1392084)Time elapsed: 0.307 s
% 13.96/2.43 % (1392084)Peak memory usage: 15 MB
% 13.96/2.43 % (1392084)Instructions burned: 339 (million)
% 13.96/2.43 % (1392093)Instruction limit reached!
% 13.96/2.43 % (1392093)------------------------------
% 13.96/2.43 % (1392093)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.96/2.43 % (1392093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.96/2.43 % (1392093)CaDiCaL version: 2.1.3
% 13.96/2.43 % (1392093)Termination reason: Instruction limit
% 13.96/2.43 % (1392093)Termination phase: Saturation
% 13.96/2.43 % (1392093)Time elapsed: 0.228 s
% 13.96/2.43 % (1392093)Peak memory usage: 13 MB
% 13.96/2.43 % (1392093)Instructions burned: 227 (million)
% 13.96/2.43 % (1392106)WARNING Broken Constraint: if sine_to_age_tolerance(3) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 13.96/2.43 % (1392105)lrs+1010_1_sil=128000:si=on:sos=all:uwa=off:nwc=1:random_seed=2780830651:i=421:rtra=on:ss=axioms_2980 on theBenchmark for (2980ds/421Mi)
% 13.96/2.43 % (1392106)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=118350062:avsq=on:i=270:s2at=3:avsqr=1,16:rtra=on:ntd=on_2980 on theBenchmark for (2980ds/270Mi)
% 13.96/2.43 % (1392089)Instruction limit reached!
% 13.96/2.43 % (1392089)------------------------------
% 13.96/2.43 % (1392089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.96/2.43 % (1392089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.96/2.43 % (1392089)CaDiCaL version: 2.1.3
% 13.96/2.43 % (1392089)Termination reason: Instruction limit
% 13.96/2.43 % (1392089)Termination phase: Saturation
% 13.96/2.43 % (1392089)Time elapsed: 0.300 s
% 13.96/2.43 % (1392089)Peak memory usage: 14 MB
% 13.96/2.43 % (1392089)Instructions burned: 341 (million)
% 13.96/2.43 % (1392109)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=2673774408:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2980 on theBenchmark for (2980ds/31Mi)
% 13.96/2.43 % (1392109)Instruction limit reached!
% 13.96/2.43 % (1392109)------------------------------
% 13.96/2.43 % (1392109)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.96/2.43 % (1392109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.96/2.43 % (1392109)CaDiCaL version: 2.1.3
% 13.96/2.43 % (1392109)Termination reason: Instruction limit
% 13.96/2.43 % (1392109)Termination phase: Saturation
% 13.96/2.43 % (1392109)Time elapsed: 0.030 s
% 13.96/2.43 % (1392109)Peak memory usage: 12 MB
% 13.96/2.43 % (1392109)Instructions burned: 31 (million)
% 13.96/2.43 % (1392111)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 13.96/2.43 % (1392111)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 13.96/2.43 % (1392111)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=3317503158:hsqr=1,8:i=1440:s2at=5:add=on:nm=2:rtra=on_2979 on theBenchmark for (2979ds/1440Mi)
% 13.96/2.43 % (1392101)Instruction limit reached!
% 13.96/2.43 % (1392101)------------------------------
% 13.96/2.43 % (1392101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.96/2.43 % (1392101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.96/2.43 % (1392101)CaDiCaL version: 2.1.3
% 13.96/2.43 % (1392101)Termination reason: Instruction limit
% 13.96/2.43 % (1392101)Termination phase: Saturation
% 13.96/2.43 % (1392101)Time elapsed: 0.234 s
% 13.96/2.43 % (1392101)Peak memory usage: 13 MB
% 13.96/2.43 % (1392101)Instructions burned: 270 (million)
% 13.96/2.43 % (1392113)dis+10_2_sil=128000:si=on:random_seed=4060736857:s2a=on:i=339:av=off:rtra=on:fe=abstraction:ss=axioms:fsd=on:ntd=on_2978 on theBenchmark for (2978ds/339Mi)
% 13.96/2.43 % (1392106) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1391918-1392106"...
% 13.96/2.43 % (1392106)...printing done.
% 13.96/2.43 % (1392106)Refutation found. Thanks to Tanya!
% 13.96/2.43 % SZS status Theorem for theBenchmark
% 13.96/2.43 % SZS output start Proof for theBenchmark
% 13.96/2.43 thf(type_def_5, type, a: $tType).
% 13.96/2.43 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 13.96/2.43 thf(func_def_0, type, cLQ: (a > a > $o)).
% 13.96/2.43 thf(func_def_4, type, sK0: ((a > $o) > a)).
% 13.96/2.43 thf(func_def_5, type, sK1: (a > (a > $o) > a)).
% 13.96/2.43 thf(func_def_6, type, sK2: (a > a)).
% 13.96/2.43 thf(func_def_7, type, sF3: (a > a > $o)).
% 13.96/2.43 thf(func_def_8, type, sF4: ((a > $o) > a > a)).
% 13.96/2.43 thf(func_def_9, type, sF5: (a > (a > $o) > $o)).
% 13.96/2.43 thf(func_def_10, type, sF6: ((a > $o) > a)).
% 13.96/2.43 thf(func_def_11, type, sF7: (a > (a > $o) > $o)).
% 13.96/2.43 thf(func_def_12, type, sF8: (a > (a > $o) > $o)).
% 13.96/2.43 thf(func_def_13, type, sF9: ((a > $o) > a > $o)).
% 13.96/2.43 thf(func_def_14, type, sF10: (a > (a > $o) > $o)).
% 13.96/2.43 thf(func_def_15, type, sF11: (a > a)).
% 13.96/2.43 thf(func_def_16, type, sF12: (a > a > $o)).
% 13.96/2.43 thf(func_def_17, type, sF13: (a > $o)).
% 13.96/2.43 thf(func_def_18, type, sF14: (a > $o)).
% 13.96/2.43 thf(func_def_19, type, vNOT: ($o > $o)).
% 13.96/2.43 thf(func_def_20, type, db0: !>[X0: $tType]:(X0)).
% 13.96/2.43 thf(func_def_21, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 13.96/2.43 thf(f1,conjecture,(
% 13.96/2.43 ! [X0 : ((a > $o) > a)] : ((! [X4 : (a > $o)] : (! [X3 : a] : ((X4 @ X3) => (cLQ @ X3 @ (X0 @ X4))) & ! [X5 : a] : (! [X6 : a] : ((X4 @ X6) => (cLQ @ X6 @ X5)) => (cLQ @ (X0 @ X4) @ X5))) & ! [X2 : a,X3 : a,X1 : a] : (((cLQ @ X2 @ X3) & (cLQ @ X1 @ X2)) => (cLQ @ X1 @ X3))) => ! [X7 : (a > a)] : (! [X1 : a,X2 : a] : ((cLQ @ X1 @ X2) => (cLQ @ (X7 @ X1) @ (X7 @ X2))) => ? [X8 : a] : ((cLQ @ (X7 @ X8) @ X8) & (cLQ @ X8 @ (X7 @ X8)))))),
% 13.96/2.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p',cTHM145L1_pme)).
% 13.96/2.43 thf(f2,negated_conjecture,(
% 13.96/2.43 ~ ! [X0 : ((a > $o) > a)] : ((! [X4 : (a > $o)] : (! [X3 : a] : ((X4 @ X3) => (cLQ @ X3 @ (X0 @ X4))) & ! [X5 : a] : (! [X6 : a] : ((X4 @ X6) => (cLQ @ X6 @ X5)) => (cLQ @ (X0 @ X4) @ X5))) & ! [X2 : a,X3 : a,X1 : a] : (((cLQ @ X2 @ X3) & (cLQ @ X1 @ X2)) => (cLQ @ X1 @ X3))) => ! [X7 : (a > a)] : (! [X1 : a,X2 : a] : ((cLQ @ X1 @ X2) => (cLQ @ (X7 @ X1) @ (X7 @ X2))) => ? [X8 : a] : ((cLQ @ (X7 @ X8) @ X8) & (cLQ @ X8 @ (X7 @ X8)))))),
% 13.96/2.43 inference(negated_conjecture,[status(cth)],[f1])).
% 13.96/2.43 thf(f3,plain,(
% 13.96/2.43 ~ ! [X0 : ((a > $o) > a)] : ((! [X1 : (a > $o)] : (! [X2 : a] : ((X1 @ X2) => (cLQ @ X2 @ (X0 @ X1))) & ! [X3 : a] : (! [X4 : a] : ((X1 @ X4) => (cLQ @ X4 @ X3)) => (cLQ @ (X0 @ X1) @ X3))) & ! [X5 : a,X6 : a,X7 : a] : (((cLQ @ X5 @ X6) & (cLQ @ X7 @ X5)) => (cLQ @ X7 @ X6))) => ! [X8 : (a > a)] : (! [X9 : a,X10 : a] : ((cLQ @ X9 @ X10) => (cLQ @ (X8 @ X9) @ (X8 @ X10))) => ? [X11 : a] : ((cLQ @ (X8 @ X11) @ X11) & (cLQ @ X11 @ (X8 @ X11)))))),
% 13.96/2.43 inference(rectify,[],[f2])).
% 13.96/2.43 thf(f4,plain,(
% 13.96/2.43 ~ ! [X0 : ((a > $o) > a)] : ((! [X1 : (a > $o)] : (! [X2 : a] : ((((X1 @ X2)) = $true) => (((cLQ @ X2 @ (X0 @ X1))) = $true)) & ! [X3 : a] : (! [X4 : a] : (($true = ((X1 @ X4))) => ($true = ((cLQ @ X4 @ X3)))) => (((cLQ @ (X0 @ X1) @ X3)) = $true))) & ! [X7 : a,X6 : a,X5 : a] : ((($true = ((cLQ @ X7 @ X5))) & ($true = ((cLQ @ X5 @ X6)))) => ($true = ((cLQ @ X7 @ X6))))) => ! [X8 : (a > a)] : (! [X10 : a,X9 : a] : ((((cLQ @ X9 @ X10)) = $true) => ($true = ((cLQ @ (X8 @ X9) @ (X8 @ X10))))) => ? [X11 : a] : (($true = ((cLQ @ (X8 @ X11) @ X11))) & (((cLQ @ X11 @ (X8 @ X11))) = $true))))),
% 13.96/2.43 inference(fool_elimination,[],[f3])).
% 13.96/2.43 thf(f5,plain,(
% 13.96/2.43 ? [X0 : ((a > $o) > a)] : (? [X8 : (a > a)] : (! [X9 : a,X10 : a] : (($true = ((cLQ @ (X8 @ X9) @ (X8 @ X10)))) | (((cLQ @ X9 @ X10)) != $true)) & ! [X11 : a] : (($true != ((cLQ @ (X8 @ X11) @ X11))) | (((cLQ @ X11 @ (X8 @ X11))) != $true))) & (! [X1 : (a > $o)] : (! [X3 : a] : (? [X4 : a] : (($true = ((X1 @ X4))) & ($true != ((cLQ @ X4 @ X3)))) | (((cLQ @ (X0 @ X1) @ X3)) = $true)) & ! [X2 : a] : ((((cLQ @ X2 @ (X0 @ X1))) = $true) | (((X1 @ X2)) != $true))) & ! [X7 : a,X6 : a,X5 : a] : (($true = ((cLQ @ X7 @ X6))) | (($true != ((cLQ @ X7 @ X5))) | ($true != ((cLQ @ X5 @ X6)))))))),
% 13.96/2.43 inference(ennf_transformation,[],[f4])).
% 13.96/2.43 thf(f6,plain,(
% 13.96/2.43 ? [X0 : ((a > $o) > a)] : (! [X7 : a,X5 : a,X6 : a] : (($true != ((cLQ @ X5 @ X6))) | ($true = ((cLQ @ X7 @ X6))) | ($true != ((cLQ @ X7 @ X5)))) & ! [X1 : (a > $o)] : (! [X3 : a] : (? [X4 : a] : (($true = ((X1 @ X4))) & ($true != ((cLQ @ X4 @ X3)))) | (((cLQ @ (X0 @ X1) @ X3)) = $true)) & ! [X2 : a] : ((((cLQ @ X2 @ (X0 @ X1))) = $true) | (((X1 @ X2)) != $true))) & ? [X8 : (a > a)] : (! [X9 : a,X10 : a] : (($true = ((cLQ @ (X8 @ X9) @ (X8 @ X10)))) | (((cLQ @ X9 @ X10)) != $true)) & ! [X11 : a] : (($true != ((cLQ @ (X8 @ X11) @ X11))) | (((cLQ @ X11 @ (X8 @ X11))) != $true))))),
% 13.96/2.43 inference(flattening,[],[f5])).
% 13.96/2.43 thf(f7,plain,(
% 13.96/2.43 ? [X0 : ((a > $o) > a)] : (! [X1 : a,X2 : a,X3 : a] : ((((cLQ @ X2 @ X3)) != $true) | (((cLQ @ X1 @ X3)) = $true) | (((cLQ @ X1 @ X2)) != $true)) & ! [X4 : (a > $o)] : (! [X5 : a] : (? [X6 : a] : ((((X4 @ X6)) = $true) & (((cLQ @ X6 @ X5)) != $true)) | (((cLQ @ (X0 @ X4) @ X5)) = $true)) & ! [X7 : a] : ((((cLQ @ X7 @ (X0 @ X4))) = $true) | ($true != ((X4 @ X7))))) & ? [X8 : (a > a)] : (! [X9 : a,X10 : a] : (($true = ((cLQ @ (X8 @ X9) @ (X8 @ X10)))) | (((cLQ @ X9 @ X10)) != $true)) & ! [X11 : a] : (($true != ((cLQ @ (X8 @ X11) @ X11))) | (((cLQ @ X11 @ (X8 @ X11))) != $true))))),
% 13.96/2.43 inference(rectify,[],[f6])).
% 13.96/2.43 thf(f8,plain,(
% 13.96/2.43 ! [X1 : a,X2 : a,X3 : a] : ((((cLQ @ X2 @ X3)) != $true) | (((cLQ @ X1 @ X3)) = $true) | (((cLQ @ X1 @ X2)) != $true)) & ! [X4 : (a > $o)] : (! [X5 : a] : (((((X4 @ (sK1 @ X5 @ X4))) = $true) & (((cLQ @ (sK1 @ X5 @ X4) @ X5)) != $true)) | (((cLQ @ (sK0 @ X4) @ X5)) = $true)) & ! [X7 : a] : ((((cLQ @ X7 @ (sK0 @ X4))) = $true) | ($true != ((X4 @ X7))))) & (! [X9 : a,X10 : a] : (($true = ((cLQ @ (sK2 @ X9) @ (sK2 @ X10)))) | (((cLQ @ X9 @ X10)) != $true)) & ! [X11 : a] : ((((cLQ @ (sK2 @ X11) @ X11)) != $true) | (((cLQ @ X11 @ (sK2 @ X11))) != $true)))),
% 13.96/2.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK0,vAPP,sK2]),skolemize(X0,sK0),skolemize(X6,sK1 @ X5 @ X4),skolemize(X8,sK2)],[f7])).
% 13.96/2.43 thf(f9,plain,(
% 13.96/2.43 ( ! [X11 : a] : ((((cLQ @ (sK2 @ X11) @ X11)) != $true) | (((cLQ @ X11 @ (sK2 @ X11))) != $true)) )),
% 13.96/2.43 inference(cnf_transformation,[],[f8])).
% 13.96/2.43 thf(f10,plain,(
% 13.96/2.43 ( ! [X10 : a,X9 : a] : (($true = ((cLQ @ (sK2 @ X9) @ (sK2 @ X10)))) | (((cLQ @ X9 @ X10)) != $true)) )),
% 13.96/2.43 inference(cnf_transformation,[],[f8])).
% 13.96/2.43 thf(f11,plain,(
% 13.96/2.43 ( ! [X7 : a,X4 : (a > $o)] : ((((cLQ @ X7 @ (sK0 @ X4))) = $true) | ($true != ((X4 @ X7)))) )),
% 13.96/2.43 inference(cnf_transformation,[],[f8])).
% 13.96/2.43 thf(f12,plain,(
% 13.96/2.43 ( ! [X4 : (a > $o),X5 : a] : ((((cLQ @ (sK1 @ X5 @ X4) @ X5)) != $true) | (((cLQ @ (sK0 @ X4) @ X5)) = $true)) )),
% 13.96/2.43 inference(cnf_transformation,[],[f8])).
% 13.96/2.43 thf(f13,plain,(
% 13.96/2.43 ( ! [X4 : (a > $o),X5 : a] : ((((X4 @ (sK1 @ X5 @ X4))) = $true) | (((cLQ @ (sK0 @ X4) @ X5)) = $true)) )),
% 13.96/2.43 inference(cnf_transformation,[],[f8])).
% 13.96/2.43 thf(f14,plain,(
% 13.96/2.43 ( ! [X2 : a,X3 : a,X1 : a] : ((((cLQ @ X2 @ X3)) != $true) | (((cLQ @ X1 @ X3)) = $true) | (((cLQ @ X1 @ X2)) != $true)) )),
% 13.96/2.43 inference(cnf_transformation,[],[f8])).
% 13.96/2.43 thf(f17,definition,(
% 13.96/2.43 ( ! [X2 : a,X3 : a] : ((((sF3 @ X3 @ X2)) = ((cLQ @ X2 @ X3)))) )),
% 13.96/2.43 introduced(definition,[new_symbols(definition,[sF3])],[function_definition])).
% 13.96/2.43 thf(f18,plain,(
% 13.96/2.43 ( ! [X2 : a,X3 : a] : ((((cLQ @ X2 @ X3)) = ((sF3 @ X3 @ X2)))) )),
% 13.96/2.43 inference(reorient_equations,[],[f17])).
% 13.96/2.43 thf(f19,plain,(
% 13.96/2.43 ( ! [X2 : a,X3 : a,X1 : a] : (($true != ((sF3 @ X2 @ X1))) | (((sF3 @ X3 @ X2)) != $true) | (((sF3 @ X3 @ X1)) = $true)) )),
% 13.96/2.43 inference(definition_folding,[],[f14,f18,f18,f18])).
% 13.96/2.43 thf(f20,definition,(
% 13.96/2.43 ( ! [X4 : (a > $o),X5 : a] : ((((sF4 @ X4 @ X5)) = ((sK1 @ X5 @ X4)))) )),
% 13.96/2.43 introduced(definition,[new_symbols(definition,[sF4])],[function_definition])).
% 13.96/2.43 thf(f21,plain,(
% 13.96/2.43 ( ! [X4 : (a > $o),X5 : a] : ((((sK1 @ X5 @ X4)) = ((sF4 @ X4 @ X5)))) )),
% 13.96/2.43 inference(reorient_equations,[],[f20])).
% 13.96/2.43 thf(f22,definition,(
% 13.96/2.43 ( ! [X4 : (a > $o),X5 : a] : ((((sF5 @ X5 @ X4)) = ((X4 @ (sF4 @ X4 @ X5))))) )),
% 13.96/2.43 introduced(definition,[new_symbols(definition,[sF5])],[function_definition])).
% 13.96/2.43 thf(f23,definition,(
% 13.96/2.43 ( ! [X4 : (a > $o)] : ((((sF6 @ X4)) = ((sK0 @ X4)))) )),
% 13.96/2.43 introduced(definition,[new_symbols(definition,[sF6])],[function_definition])).
% 13.96/2.43 thf(f24,definition,(
% 13.96/2.43 ( ! [X4 : (a > $o),X5 : a] : ((((sF7 @ X5 @ X4)) = ((cLQ @ (sF6 @ X4) @ X5)))) )),
% 13.96/2.43 introduced(definition,[new_symbols(definition,[sF7])],[function_definition])).
% 13.96/2.43 thf(f25,plain,(
% 13.96/2.43 ( ! [X4 : (a > $o),X5 : a] : ((((cLQ @ (sF6 @ X4) @ X5)) = ((sF7 @ X5 @ X4)))) )),
% 13.96/2.43 inference(reorient_equations,[],[f24])).
% 13.96/2.43 thf(f26,plain,(
% 13.96/2.43 ( ! [X4 : (a > $o),X5 : a] : ((((sF7 @ X5 @ X4)) = $true) | (((sF5 @ X5 @ X4)) = $true)) )),
% 13.96/2.43 inference(definition_folding,[],[f13,f25,f23,f22,f21])).
% 13.96/2.43 thf(f27,definition,(
% 13.96/2.43 ( ! [X4 : (a > $o),X5 : a] : ((((sF8 @ X5 @ X4)) = ((cLQ @ (sF4 @ X4 @ X5) @ X5)))) )),
% 13.96/2.43 introduced(definition,[new_symbols(definition,[sF8])],[function_definition])).
% 13.96/2.43 thf(f28,plain,(
% 13.96/2.43 ( ! [X4 : (a > $o),X5 : a] : ((((sF8 @ X5 @ X4)) != $true) | (((sF7 @ X5 @ X4)) = $true)) )),
% 13.96/2.43 inference(definition_folding,[],[f12,f25,f23,f27,f21])).
% 13.96/2.43 thf(f29,definition,(
% 13.96/2.43 ( ! [X7 : a,X4 : (a > $o)] : ((((sF9 @ X4 @ X7)) = ((cLQ @ X7 @ (sF6 @ X4))))) )),
% 13.96/2.43 introduced(definition,[new_symbols(definition,[sF9])],[function_definition])).
% 13.96/2.43 thf(f30,definition,(
% 13.96/2.43 ( ! [X7 : a,X4 : (a > $o)] : ((((sF10 @ X7 @ X4)) = ((X4 @ X7)))) )),
% 13.96/2.43 introduced(definition,[new_symbols(definition,[sF10])],[function_definition])).
% 13.96/2.43 thf(f31,plain,(
% 13.96/2.43 ( ! [X7 : a,X4 : (a > $o)] : (($true != ((sF10 @ X7 @ X4))) | (((sF9 @ X4 @ X7)) = $true)) )),
% 13.96/2.43 inference(definition_folding,[],[f11,f30,f29,f23])).
% 13.96/2.43 thf(f32,definition,(
% 13.96/2.43 ( ! [X9 : a] : ((((sF11 @ X9)) = ((sK2 @ X9)))) )),
% 13.96/2.43 introduced(definition,[new_symbols(definition,[sF11])],[function_definition])).
% 13.96/2.43 thf(f33,definition,(
% 13.96/2.43 ( ! [X10 : a,X9 : a] : ((((sF12 @ X10 @ X9)) = ((cLQ @ (sF11 @ X9) @ (sF11 @ X10))))) )),
% 13.96/2.43 introduced(definition,[new_symbols(definition,[sF12])],[function_definition])).
% 13.96/2.43 thf(f34,plain,(
% 13.96/2.43 ( ! [X10 : a,X9 : a] : (($true != ((sF3 @ X10 @ X9))) | (((sF12 @ X10 @ X9)) = $true)) )),
% 13.96/2.43 inference(definition_folding,[],[f10,f18,f33,f32,f32])).
% 13.96/2.43 thf(f35,definition,(
% 13.96/2.43 ( ! [X11 : a] : ((((sF13 @ X11)) = ((cLQ @ (sF11 @ X11) @ X11)))) )),
% 13.96/2.43 introduced(definition,[new_symbols(definition,[sF13])],[function_definition])).
% 13.96/2.43 thf(f36,plain,(
% 13.96/2.43 ( ! [X11 : a] : ((((cLQ @ (sF11 @ X11) @ X11)) = ((sF13 @ X11)))) )),
% 13.96/2.43 inference(reorient_equations,[],[f35])).
% 13.96/2.43 thf(f37,definition,(
% 13.96/2.43 ( ! [X11 : a] : ((((sF14 @ X11)) = ((cLQ @ X11 @ (sF11 @ X11))))) )),
% 13.96/2.43 introduced(definition,[new_symbols(definition,[sF14])],[function_definition])).
% 13.96/2.43 thf(f38,plain,(
% 13.96/2.43 ( ! [X11 : a] : (($true != ((sF14 @ X11))) | ($true != ((sF13 @ X11)))) )),
% 13.96/2.43 inference(definition_folding,[],[f9,f37,f32,f36,f32])).
% 13.96/2.43 thf(f53,plain,(
% 13.96/2.43 ( ! [X0 : a,X1 : a] : (($true != ((cLQ @ X0 @ X1))) | ($true = ((sF12 @ X1 @ X0)))) )),
% 13.96/2.43 inference(superposition,[],[f34,f18])).
% 13.96/2.44 thf(f56,plain,(
% 13.96/2.44 ( ! [X0 : a] : ((((sF14 @ X0)) != $true) | ($true = ((sF12 @ (sF11 @ X0) @ X0)))) )),
% 13.96/2.44 inference(superposition,[],[f53,f37])).
% 13.96/2.44 thf(f58,plain,(
% 13.96/2.44 ( ! [X0 : (a > $o)] : ((((sF13 @ (sF6 @ X0))) = ((sF9 @ X0 @ (sF11 @ (sF6 @ X0)))))) )),
% 13.96/2.44 inference(superposition,[],[f29,f36])).
% 13.96/2.44 thf(f61,plain,(
% 13.96/2.44 ( ! [X0 : (a > $o),X1 : a] : (($true != ((sF9 @ X0 @ X1))) | (((sF12 @ (sF6 @ X0) @ X1)) = $true)) )),
% 13.96/2.44 inference(superposition,[],[f53,f29])).
% 13.96/2.44 thf(f63,plain,(
% 13.96/2.44 ( ! [X0 : a] : ((((sF12 @ (sF11 @ X0) @ X0)) = ((sF14 @ (sF11 @ X0))))) )),
% 13.96/2.44 inference(superposition,[],[f33,f37])).
% 13.96/2.44 thf(f69,plain,(
% 13.96/2.44 ( ! [X0 : a,X1 : a] : ((((sF3 @ (sF11 @ X0) @ (sF11 @ X1))) = ((sF12 @ X0 @ X1)))) )),
% 13.96/2.44 inference(superposition,[],[f18,f33])).
% 13.96/2.44 thf(f80,plain,(
% 13.96/2.44 ( ! [X0 : (a > $o),X1 : a] : ((((X0 @ X1)) != $true) | ($true = ((sF9 @ X0 @ X1)))) )),
% 13.96/2.44 inference(superposition,[],[f31,f30])).
% 13.96/2.44 thf(f113,plain,(
% 13.96/2.44 ( ! [X0 : a] : (($true = ((sF12 @ (sF11 @ (sF4 @ sF14 @ X0)) @ (sF4 @ sF14 @ X0)))) | ($true != ((sF5 @ X0 @ sF14)))) )),
% 13.96/2.44 inference(superposition,[],[f56,f22])).
% 13.96/2.44 thf(f128,plain,(
% 13.96/2.44 ( ! [X0 : a] : (($true != ((sF5 @ X0 @ sF14))) | (((sF14 @ (sF11 @ (sF4 @ sF14 @ X0)))) = $true)) )),
% 13.96/2.44 inference(forward_demodulation,[],[f113,f63])).
% 13.96/2.44 thf(f136,plain,(
% 13.96/2.44 ( ! [X0 : (a > $o)] : ((((sF14 @ (sF6 @ X0))) = ((sF7 @ (sF11 @ (sF6 @ X0)) @ X0)))) )),
% 13.96/2.44 inference(superposition,[],[f37,f25])).
% 13.96/2.44 thf(f202,plain,(
% 13.96/2.44 ( ! [X2 : a,X0 : a,X1 : a] : (($true != ((sF3 @ X2 @ X1))) | (((sF3 @ X2 @ X0)) = $true) | ($true != ((cLQ @ X0 @ X1)))) )),
% 13.96/2.44 inference(superposition,[],[f19,f18])).
% 13.96/2.44 thf(f430,plain,(
% 13.96/2.44 ( ! [X0 : a,X1 : (a > $o)] : ((((sF3 @ X0 @ (sF4 @ X1 @ X0))) = ((sF8 @ X0 @ X1)))) )),
% 13.96/2.44 inference(superposition,[],[f27,f18])).
% 13.96/2.44 thf(f436,plain,(
% 13.96/2.44 ( ! [X0 : (a > $o)] : (($true = ((sF5 @ (sF11 @ (sF6 @ X0)) @ X0))) | (((sF14 @ (sF6 @ X0))) = $true)) )),
% 13.96/2.44 inference(superposition,[],[f136,f26])).
% 13.96/2.44 thf(f645,plain,(
% 13.96/2.44 ( ! [X2 : a,X0 : a,X1 : a] : (($true != ((cLQ @ X2 @ X0))) | ($true != ((cLQ @ X0 @ X1))) | ($true = ((sF3 @ X1 @ X2)))) )),
% 13.96/2.44 inference(superposition,[],[f202,f18])).
% 13.96/2.44 thf(f730,plain,(
% 13.96/2.44 ( ! [X0 : a,X1 : a] : (($true != ((cLQ @ (sF11 @ X0) @ X1))) | (((sF3 @ X1 @ X0)) = $true) | (((sF14 @ X0)) != $true)) )),
% 13.96/2.44 inference(superposition,[],[f645,f37])).
% 13.96/2.44 thf(f740,plain,(
% 13.96/2.44 ( ! [X0 : a,X1 : a] : (($true != ((sF12 @ X0 @ X1))) | (((sF3 @ (sF11 @ X0) @ X1)) = $true) | (((sF14 @ X1)) != $true)) )),
% 13.96/2.44 inference(superposition,[],[f730,f33])).
% 13.96/2.44 thf(f1379,plain,(
% 13.96/2.44 ($true != $true) | (((sF14 @ (sF6 @ sF14))) = $true) | (((sF14 @ (sF11 @ (sF4 @ sF14 @ (sF11 @ (sF6 @ sF14)))))) = $true)),
% 13.96/2.44 inference(superposition,[],[f128,f436])).
% 13.96/2.44 thf(f1380,plain,(
% 13.96/2.44 (((sF14 @ (sF11 @ (sF4 @ sF14 @ (sF11 @ (sF6 @ sF14)))))) = $true) | (((sF14 @ (sF6 @ sF14))) = $true)),
% 13.96/2.44 inference(trivial_inequality_removal,[],[f1379])).
% 13.96/2.44 thf(f1382,definition,(
% 13.96/2.44 spl15_10 <=> (((sF14 @ (sF6 @ sF14))) = $true)),
% 13.96/2.44 introduced(definition,[new_symbols(definition,[spl15_10])],[avatar_definition])).
% 13.96/2.44 thf(f1383,plain,(
% 13.96/2.44 (((sF14 @ (sF6 @ sF14))) != $true) | spl15_10),
% 13.96/2.44 inference(avatar_component_clause,[],[f1382])).
% 13.96/2.44 thf(f1384,plain,(
% 13.96/2.44 (((sF14 @ (sF6 @ sF14))) = $true) | ~spl15_10),
% 13.96/2.44 inference(avatar_component_clause,[],[f1382])).
% 13.96/2.44 thf(f1386,definition,(
% 13.96/2.44 spl15_11 <=> (((sF14 @ (sF11 @ (sF4 @ sF14 @ (sF11 @ (sF6 @ sF14)))))) = $true)),
% 13.96/2.44 introduced(definition,[new_symbols(definition,[spl15_11])],[avatar_definition])).
% 13.96/2.44 thf(f1388,plain,(
% 13.96/2.44 (((sF14 @ (sF11 @ (sF4 @ sF14 @ (sF11 @ (sF6 @ sF14)))))) = $true) | ~spl15_11),
% 13.96/2.44 inference(avatar_component_clause,[],[f1386])).
% 13.96/2.44 thf(f1389,plain,(
% 13.96/2.44 spl15_10 | spl15_11),
% 13.96/2.44 inference(avatar_split_clause,[],[f1380,f1386,f1382])).
% 13.96/2.44 thf(f1393,plain,(
% 13.96/2.44 ($true != $true) | (((sF12 @ (sF11 @ (sF6 @ sF14)) @ (sF6 @ sF14))) = $true) | ~spl15_10),
% 13.96/2.44 inference(superposition,[],[f56,f1384])).
% 13.96/2.44 thf(f1394,plain,(
% 13.96/2.44 ($true != ((sF13 @ (sF6 @ sF14)))) | ($true != $true) | ~spl15_10),
% 13.96/2.44 inference(superposition,[],[f38,f1384])).
% 13.96/2.44 thf(f1401,plain,(
% 13.96/2.44 (((sF12 @ (sF11 @ (sF6 @ sF14)) @ (sF6 @ sF14))) = $true) | ~spl15_10),
% 13.96/2.44 inference(trivial_inequality_removal,[],[f1393])).
% 13.96/2.44 thf(f1403,plain,(
% 13.96/2.44 ($true != ((sF13 @ (sF6 @ sF14)))) | ~spl15_10),
% 13.96/2.44 inference(trivial_inequality_removal,[],[f1394])).
% 13.96/2.44 thf(f1405,plain,(
% 13.96/2.44 (((sF14 @ (sF11 @ (sF6 @ sF14)))) = $true) | ~spl15_10),
% 13.96/2.44 inference(forward_demodulation,[],[f1401,f63])).
% 13.96/2.44 thf(f1415,plain,(
% 13.96/2.44 ($true = ((sF9 @ sF14 @ (sF11 @ (sF6 @ sF14))))) | ($true != $true) | ~spl15_10),
% 13.96/2.44 inference(superposition,[],[f80,f1405])).
% 13.96/2.44 thf(f1421,plain,(
% 13.96/2.44 ($true = ((sF9 @ sF14 @ (sF11 @ (sF6 @ sF14))))) | ~spl15_10),
% 13.96/2.44 inference(trivial_inequality_removal,[],[f1415])).
% 13.96/2.44 thf(f1428,plain,(
% 13.96/2.44 ($true = ((sF13 @ (sF6 @ sF14)))) | ~spl15_10),
% 13.96/2.44 inference(forward_demodulation,[],[f1421,f58])).
% 13.96/2.44 thf(f1430,plain,(
% 13.96/2.44 $false | ~spl15_10),
% 13.96/2.44 inference(forward_subsumption_resolution,[],[f1428,f1403])).
% 13.96/2.44 thf(f1431,plain,(
% 13.96/2.44 ~spl15_10),
% 13.96/2.44 inference(avatar_contradiction_clause,[],[f1430])).
% 13.96/2.44 thf(f1475,plain,(
% 13.96/2.44 ($true != $true) | (((sF9 @ sF14 @ (sF11 @ (sF4 @ sF14 @ (sF11 @ (sF6 @ sF14)))))) = $true) | ~spl15_11),
% 13.96/2.44 inference(superposition,[],[f80,f1388])).
% 13.96/2.44 thf(f1482,plain,(
% 13.96/2.44 (((sF9 @ sF14 @ (sF11 @ (sF4 @ sF14 @ (sF11 @ (sF6 @ sF14)))))) = $true) | ~spl15_11),
% 13.96/2.44 inference(trivial_inequality_removal,[],[f1475])).
% 13.96/2.44 thf(f1490,definition,(
% 13.96/2.44 spl15_12 <=> (((sF5 @ (sF11 @ (sF6 @ sF14)) @ sF14)) = $true)),
% 13.96/2.44 introduced(definition,[new_symbols(definition,[spl15_12])],[avatar_definition])).
% 13.96/2.44 thf(f1491,plain,(
% 13.96/2.44 (((sF5 @ (sF11 @ (sF6 @ sF14)) @ sF14)) = $true) | ~spl15_12),
% 13.96/2.44 inference(avatar_component_clause,[],[f1490])).
% 13.96/2.44 thf(f1492,plain,(
% 13.96/2.44 (((sF5 @ (sF11 @ (sF6 @ sF14)) @ sF14)) != $true) | spl15_12),
% 13.96/2.44 inference(avatar_component_clause,[],[f1490])).
% 13.96/2.44 thf(f1498,plain,(
% 13.96/2.44 ($true != $true) | (((sF14 @ (sF6 @ sF14))) = $true) | spl15_12),
% 13.96/2.44 inference(superposition,[],[f1492,f436])).
% 13.96/2.44 thf(f1499,plain,(
% 13.96/2.44 (((sF14 @ (sF6 @ sF14))) = $true) | spl15_12),
% 13.96/2.44 inference(trivial_inequality_removal,[],[f1498])).
% 13.96/2.44 thf(f1500,plain,(
% 13.96/2.44 $false | (spl15_10 | spl15_12)),
% 13.96/2.44 inference(forward_subsumption_resolution,[],[f1499,f1383])).
% 13.96/2.44 thf(f1501,plain,(
% 13.96/2.44 spl15_10 | spl15_12),
% 13.96/2.44 inference(avatar_contradiction_clause,[],[f1500])).
% 13.96/2.44 thf(f1881,plain,(
% 13.96/2.44 (((sF12 @ (sF6 @ sF14) @ (sF11 @ (sF4 @ sF14 @ (sF11 @ (sF6 @ sF14)))))) = $true) | ($true != $true) | ~spl15_11),
% 13.96/2.44 inference(superposition,[],[f61,f1482])).
% 13.96/2.44 thf(f1885,plain,(
% 13.96/2.44 (((sF12 @ (sF6 @ sF14) @ (sF11 @ (sF4 @ sF14 @ (sF11 @ (sF6 @ sF14)))))) = $true) | ~spl15_11),
% 13.96/2.44 inference(trivial_inequality_removal,[],[f1881])).
% 13.96/2.44 thf(f2412,plain,(
% 13.96/2.44 ($true = ((sF3 @ (sF11 @ (sF6 @ sF14)) @ (sF11 @ (sF4 @ sF14 @ (sF11 @ (sF6 @ sF14))))))) | ($true != $true) | (((sF14 @ (sF11 @ (sF4 @ sF14 @ (sF11 @ (sF6 @ sF14)))))) != $true) | ~spl15_11),
% 13.96/2.44 inference(superposition,[],[f740,f1885])).
% 13.96/2.44 thf(f2418,plain,(
% 13.96/2.44 (((sF14 @ (sF11 @ (sF4 @ sF14 @ (sF11 @ (sF6 @ sF14)))))) != $true) | ($true = ((sF3 @ (sF11 @ (sF6 @ sF14)) @ (sF11 @ (sF4 @ sF14 @ (sF11 @ (sF6 @ sF14))))))) | ~spl15_11),
% 13.96/2.44 inference(trivial_inequality_removal,[],[f2412])).
% 13.96/2.44 thf(f2422,plain,(
% 13.96/2.44 ($true = ((sF3 @ (sF11 @ (sF6 @ sF14)) @ (sF11 @ (sF4 @ sF14 @ (sF11 @ (sF6 @ sF14))))))) | ~spl15_11),
% 13.96/2.44 inference(forward_subsumption_resolution,[],[f2418,f1388])).
% 13.96/2.44 thf(f2424,plain,(
% 13.96/2.44 ($true = ((sF12 @ (sF6 @ sF14) @ (sF4 @ sF14 @ (sF11 @ (sF6 @ sF14)))))) | ~spl15_11),
% 13.96/2.44 inference(forward_demodulation,[],[f2422,f69])).
% 13.96/2.44 thf(f2425,plain,(
% 13.96/2.44 (((sF3 @ (sF11 @ (sF6 @ sF14)) @ (sF4 @ sF14 @ (sF11 @ (sF6 @ sF14))))) = $true) | ($true != $true) | ($true != ((sF14 @ (sF4 @ sF14 @ (sF11 @ (sF6 @ sF14)))))) | ~spl15_11),
% 13.96/2.44 inference(superposition,[],[f740,f2424])).
% 13.96/2.44 thf(f2432,plain,(
% 13.96/2.44 (((sF3 @ (sF11 @ (sF6 @ sF14)) @ (sF4 @ sF14 @ (sF11 @ (sF6 @ sF14))))) = $true) | ($true != ((sF14 @ (sF4 @ sF14 @ (sF11 @ (sF6 @ sF14)))))) | ~spl15_11),
% 13.96/2.44 inference(trivial_inequality_removal,[],[f2425])).
% 13.96/2.44 thf(f2436,plain,(
% 13.96/2.44 (((sF8 @ (sF11 @ (sF6 @ sF14)) @ sF14)) = $true) | ($true != ((sF14 @ (sF4 @ sF14 @ (sF11 @ (sF6 @ sF14)))))) | ~spl15_11),
% 13.96/2.44 inference(forward_demodulation,[],[f2432,f430])).
% 13.96/2.44 thf(f2437,plain,(
% 13.96/2.44 (((sF8 @ (sF11 @ (sF6 @ sF14)) @ sF14)) = $true) | (((sF5 @ (sF11 @ (sF6 @ sF14)) @ sF14)) != $true) | ~spl15_11),
% 13.96/2.44 inference(forward_demodulation,[],[f2436,f22])).
% 13.96/2.44 thf(f2438,plain,(
% 13.96/2.44 (((sF8 @ (sF11 @ (sF6 @ sF14)) @ sF14)) = $true) | (~spl15_11 | ~spl15_12)),
% 13.96/2.44 inference(forward_subsumption_resolution,[],[f2437,f1491])).
% 13.96/2.44 thf(f2439,plain,(
% 13.96/2.44 ($true != $true) | (((sF7 @ (sF11 @ (sF6 @ sF14)) @ sF14)) = $true) | (~spl15_11 | ~spl15_12)),
% 13.96/2.44 inference(superposition,[],[f28,f2438])).
% 13.96/2.44 thf(f2440,plain,(
% 13.96/2.44 (((sF7 @ (sF11 @ (sF6 @ sF14)) @ sF14)) = $true) | (~spl15_11 | ~spl15_12)),
% 13.96/2.44 inference(trivial_inequality_removal,[],[f2439])).
% 13.96/2.44 thf(f2441,plain,(
% 13.96/2.44 (((sF14 @ (sF6 @ sF14))) = $true) | (~spl15_11 | ~spl15_12)),
% 13.96/2.44 inference(forward_demodulation,[],[f2440,f136])).
% 13.96/2.44 thf(f2442,plain,(
% 13.96/2.44 $false | (spl15_10 | ~spl15_11 | ~spl15_12)),
% 13.96/2.44 inference(forward_subsumption_resolution,[],[f2441,f1383])).
% 13.96/2.44 thf(f2443,plain,(
% 13.96/2.44 spl15_10 | ~spl15_11 | ~spl15_12),
% 13.96/2.44 inference(avatar_contradiction_clause,[],[f2442])).
% 13.96/2.44 cnf(s6, plain, spl15_10 | spl15_11, inference(sat_conversion,[],[f1389])).
% 13.96/2.44 cnf(s7, plain, ~spl15_10, inference(sat_conversion,[],[f1431])).
% 13.96/2.44 cnf(s9, plain, spl15_10 | spl15_12, inference(sat_conversion,[],[f1501])).
% 13.96/2.44 cnf(s13, plain, spl15_10 | ~spl15_11 | ~spl15_12, inference(sat_conversion,[],[f2443])).
% 13.96/2.44 cnf(s14, plain, spl15_12, inference(rat,[],[s9,s7])).
% 13.96/2.44 cnf(s15, plain, ~spl15_11, inference(rat,[],[s13,s7,s14])).
% 13.96/2.44 cnf(s16, plain, $false, inference(rat,[],[s6,s15,s7])).
% 13.96/2.44 thf(f2444,plain,(
% 13.96/2.44 $false),
% 13.96/2.44 inference(avatar_sat_refutation,[],[s16])).
% 13.96/2.44 % SZS output end Proof for theBenchmark
% 13.96/2.44 % (1392106)------------------------------
% 13.96/2.44 % (1392106)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.96/2.44 % (1392106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.96/2.44 % (1392106)CaDiCaL version: 2.1.3
% 13.96/2.44 % (1392106)Termination reason: Refutation
% 13.96/2.44 % (1392106)Time elapsed: 0.220 s
% 13.96/2.44 % (1392106)Peak memory usage: 14 MB
% 13.96/2.44 % (1392106)Instructions burned: 233 (million)
% 13.96/2.44 % (1391918)Success in time 2.203 s
% 13.96/2.44 % Vampire exiting
%------------------------------------------------------------------------------