%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG253^1 : TPTP v9.3.1. Bugfixed v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 07:45:12 AM UTC 2026
% Result : Theorem 12.48s 2.21s
% Output : Refutation 12.48s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : ALG253^1 : TPTP v9.3.1. Bugfixed v5.2.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.25/0.27 % Computer : n017.cluster.edu
% 0.25/0.27 % Model : x86_64 x86_64
% 0.25/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.25/0.27 % Memory : 8046.5625MB
% 0.25/0.27 % OS : Linux 6.8.0-71-generic
% 0.25/0.27 % CPULimit : 300
% 0.25/0.27 % WCLimit : 300
% 0.25/0.27 % DateTime : Tue Sep 29 17:28:07 UTC 2026
% 0.25/0.27 % CPUTime :
% 0.25/0.28 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.25/0.32 Running higher-order theorem proving
% 0.25/0.36 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.81/0.56 % (641789)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.81/0.56 % (641795)lrs+10_16_si=on:nwc=1.5:random_seed=1790654905:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.81/0.56 % (641794)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=433326282:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.81/0.56 % (641795)Instruction limit reached!
% 0.81/0.56 % (641795)------------------------------
% 0.81/0.56 % (641795)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.56 % (641795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.56 % (641795)CaDiCaL version: 2.1.3
% 0.81/0.56 % (641795)Termination reason: Instruction limit
% 0.81/0.56 % (641795)Termination phase: shuffling
% 0.81/0.56 % (641795)Time elapsed: 0.009 s
% 0.81/0.56 % (641795)Peak memory usage: 10 MB
% 0.81/0.56 % (641795)Instructions burned: 20 (million)
% 0.81/0.56 % (641800)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.81/0.56 % (641800)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.81/0.56 % (641796)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=191842044:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.81/0.56 % (641798)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=3669337063:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.81/0.56 % (641800)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=2026568267:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.81/0.56 % (641797)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=2456664089:hsq=on:hsqr=16,1:s2a=on:i=634:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2999 on theBenchmark for (2999ds/634Mi)
% 0.81/0.56 % (641799)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=1159584256:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.81/0.56 % (641796)Instruction limit reached!
% 0.81/0.56 % (641796)------------------------------
% 0.81/0.56 % (641796)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.56 % (641796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.56 % (641796)CaDiCaL version: 2.1.3
% 0.81/0.56 % (641796)Termination reason: Instruction limit
% 0.81/0.56 % (641796)Termination phase: shuffling
% 0.81/0.56 % (641796)Time elapsed: 0.003 s
% 0.81/0.56 % (641796)Peak memory usage: 10 MB
% 0.81/0.56 % (641796)Instructions burned: 3 (million)
% 0.81/0.56 % (641798)Instruction limit reached!
% 0.81/0.56 % (641798)------------------------------
% 0.81/0.56 % (641798)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.56 % (641798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.56 % (641798)CaDiCaL version: 2.1.3
% 0.81/0.56 % (641798)Termination reason: Instruction limit
% 0.81/0.56 % (641798)Termination phase: Preprocessing 2
% 0.81/0.56 % (641798)Time elapsed: 0.020 s
% 0.81/0.56 % (641798)Peak memory usage: 10 MB
% 0.81/0.56 % (641798)Instructions burned: 24 (million)
% 0.81/0.56 % (641809)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=4028565576:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.81/0.56 % (641809)Instruction limit reached!
% 0.81/0.56 % (641809)------------------------------
% 0.81/0.56 % (641809)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.56 % (641809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.56 % (641809)CaDiCaL version: 2.1.3
% 0.81/0.56 % (641809)Termination reason: Instruction limit
% 0.81/0.56 % (641809)Termination phase: shuffling
% 0.81/0.56 % (641809)Time elapsed: 0.003 s
% 0.81/0.56 % (641809)Peak memory usage: 10 MB
% 0.81/0.56 % (641809)Instructions burned: 7 (million)
% 0.81/0.56 % (641803)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=909241630:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.81/0.56 % (641803)Instruction limit reached!
% 1.53/0.61 % (641803)------------------------------
% 1.53/0.61 % (641803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.53/0.61 % (641803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.53/0.61 % (641803)CaDiCaL version: 2.1.3
% 1.53/0.61 % (641803)Termination reason: Instruction limit
% 1.53/0.61 % (641803)Termination phase: shuffling
% 1.53/0.61 % (641803)Time elapsed: 0.003 s
% 1.53/0.61 % (641803)Peak memory usage: 10 MB
% 1.53/0.61 % (641803)Instructions burned: 3 (million)
% 1.53/0.61 % (641813)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=2333921417:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 1.53/0.61 % (641811)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.53/0.61 % (641813)Instruction limit reached!
% 1.53/0.61 % (641813)------------------------------
% 1.53/0.61 % (641813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.53/0.61 % (641813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.53/0.61 % (641813)CaDiCaL version: 2.1.3
% 1.53/0.61 % (641813)Termination reason: Instruction limit
% 1.53/0.61 % (641813)Termination phase: shuffling
% 1.53/0.61 % (641813)Time elapsed: 0.006 s
% 1.53/0.61 % (641813)Peak memory usage: 10 MB
% 1.53/0.61 % (641813)Instructions burned: 13 (million)
% 1.53/0.61 % (641794)Instruction limit reached!
% 1.53/0.61 % (641794)------------------------------
% 1.53/0.61 % (641794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.53/0.61 % (641794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.53/0.61 % (641794)CaDiCaL version: 2.1.3
% 1.53/0.61 % (641794)Termination reason: Instruction limit
% 1.53/0.61 % (641794)Termination phase: Function definition elimination
% 1.53/0.61 % (641794)Time elapsed: 0.064 s
% 1.53/0.61 % (641794)Peak memory usage: 12 MB
% 1.53/0.61 % (641794)Instructions burned: 87 (million)
% 1.53/0.61 % (641811)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3585946979:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 1.53/0.61 % (641814)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.53/0.61 % (641814)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.53/0.61 % (641811)Instruction limit reached!
% 1.53/0.61 % (641811)------------------------------
% 1.53/0.61 % (641811)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.53/0.61 % (641811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.53/0.61 % (641811)CaDiCaL version: 2.1.3
% 1.53/0.61 % (641811)Termination reason: Instruction limit
% 1.53/0.61 % (641811)Termination phase: shuffling
% 1.53/0.61 % (641811)Time elapsed: 0.006 s
% 1.53/0.61 % (641811)Peak memory usage: 10 MB
% 1.53/0.61 % (641811)Instructions burned: 7 (million)
% 1.53/0.61 % (641814)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=1759937864:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 1.53/0.61 % (641799)Instruction limit reached!
% 1.53/0.61 % (641799)------------------------------
% 1.53/0.61 % (641799)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.53/0.61 % (641799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.53/0.61 % (641799)CaDiCaL version: 2.1.3
% 1.53/0.61 % (641799)Termination reason: Instruction limit
% 1.53/0.61 % (641799)Termination phase: Property scanning
% 1.53/0.61 % (641799)Time elapsed: 0.063 s
% 1.53/0.61 % (641799)Peak memory usage: 12 MB
% 1.53/0.61 % (641799)Instructions burned: 76 (million)
% 1.53/0.61 % (641816)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=3997479226:i=86:piset=equals:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/86Mi)
% 1.53/0.61 % (641819)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.53/0.61 % (641819)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=2158283389:i=2:add=on:rtra=on_2998 on theBenchmark for (2998ds/2Mi)
% 1.89/0.66 % (641817)lrs+10_1_si=on:cs=on:random_seed=713871522:i=8:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.89/0.66 % (641819)Instruction limit reached!
% 1.89/0.66 % (641819)------------------------------
% 1.89/0.66 % (641819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.89/0.66 % (641819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.89/0.66 % (641819)CaDiCaL version: 2.1.3
% 1.89/0.66 % (641819)Termination reason: Instruction limit
% 1.89/0.66 % (641819)Termination phase: shuffling
% 1.89/0.66 % (641819)Time elapsed: 0.002 s
% 1.89/0.66 % (641819)Peak memory usage: 10 MB
% 1.89/0.66 % (641819)Instructions burned: 4 (million)
% 1.89/0.66 % (641814)Instruction limit reached!
% 1.89/0.66 % (641814)------------------------------
% 1.89/0.66 % (641814)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.89/0.66 % (641814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.89/0.66 % (641814)CaDiCaL version: 2.1.3
% 1.89/0.66 % (641814)Termination reason: Instruction limit
% 1.89/0.66 % (641814)Termination phase: Property scanning
% 1.89/0.66 % (641814)Time elapsed: 0.024 s
% 1.89/0.66 % (641814)Peak memory usage: 10 MB
% 1.89/0.66 % (641814)Instructions burned: 29 (million)
% 1.89/0.66 % (641817)Instruction limit reached!
% 1.89/0.66 % (641817)------------------------------
% 1.89/0.66 % (641817)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.89/0.66 % (641817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.89/0.66 % (641817)CaDiCaL version: 2.1.3
% 1.89/0.66 % (641817)Termination reason: Instruction limit
% 1.89/0.66 % (641817)Termination phase: shuffling
% 1.89/0.66 % (641817)Time elapsed: 0.007 s
% 1.89/0.66 % (641817)Peak memory usage: 10 MB
% 1.89/0.66 % (641817)Instructions burned: 8 (million)
% 1.89/0.66 % (641821)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=1380279384:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/38Mi)
% 1.89/0.66 % (641816)Instruction limit reached!
% 1.89/0.66 % (641816)------------------------------
% 1.89/0.66 % (641816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.89/0.66 % (641816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.89/0.66 % (641816)CaDiCaL version: 2.1.3
% 1.89/0.66 % (641816)Termination reason: Instruction limit
% 1.89/0.66 % (641816)Termination phase: Saturation
% 1.89/0.66 % (641816)Time elapsed: 0.036 s
% 1.89/0.66 % (641816)Peak memory usage: 12 MB
% 1.89/0.66 % (641816)Instructions burned: 87 (million)
% 1.89/0.66 % (641825)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=3373973953:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 1.89/0.66 % (641826)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=3043022748:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 1.89/0.66 % (641821)Refutation not found, incomplete strategy
% 1.89/0.66 % (641821)------------------------------
% 1.89/0.66 % (641821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.89/0.66 % (641821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.89/0.66 % (641821)CaDiCaL version: 2.1.3
% 1.89/0.66 % (641821)Termination reason: Refutation not found, incomplete strategy
% 1.89/0.66 % (641821)Time elapsed: 0.025 s
% 1.89/0.66 % (641821)Peak memory usage: 12 MB
% 1.89/0.66 % (641821)Instructions burned: 27 (million)
% 1.89/0.66 % (641821)------------------------------
% 1.89/0.66 % (641821)------------------------------
% 1.89/0.66 % (641827)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=1505352371:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.89/0.66 % (641800)Instruction limit reached!
% 1.89/0.66 % (641800)------------------------------
% 1.89/0.66 % (641800)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.89/0.66 % (641800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.89/0.66 % (641800)CaDiCaL version: 2.1.3
% 1.89/0.66 % (641800)Termination reason: Instruction limit
% 1.89/0.66 % (641800)Termination phase: Saturation
% 1.89/0.66 % (641800)Time elapsed: 0.126 s
% 1.89/0.66 % (641800)Peak memory usage: 13 MB
% 1.89/0.66 % (641800)Instructions burned: 157 (million)
% 2.25/0.73 % (641825)Refutation not found, incomplete strategy
% 2.25/0.73 % (641825)------------------------------
% 2.25/0.73 % (641825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.25/0.73 % (641825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.25/0.73 % (641825)CaDiCaL version: 2.1.3
% 2.25/0.73 % (641825)Termination reason: Refutation not found, incomplete strategy
% 2.25/0.73 % (641825)Time elapsed: 0.022 s
% 2.25/0.73 % (641825)Peak memory usage: 12 MB
% 2.25/0.73 % (641825)Instructions burned: 51 (million)
% 2.25/0.73 % (641829)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=3499281497:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 2.25/0.73 % (641825)------------------------------
% 2.25/0.73 % (641825)------------------------------
% 2.25/0.73 % (641827)Instruction limit reached!
% 2.25/0.73 % (641827)------------------------------
% 2.25/0.73 % (641827)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.25/0.73 % (641827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.25/0.73 % (641827)CaDiCaL version: 2.1.3
% 2.25/0.73 % (641827)Termination reason: Instruction limit
% 2.25/0.73 % (641827)Termination phase: shuffling
% 2.25/0.73 % (641827)Time elapsed: 0.012 s
% 2.25/0.73 % (641827)Peak memory usage: 10 MB
% 2.25/0.73 % (641827)Instructions burned: 15 (million)
% 2.25/0.73 % (641826)Instruction limit reached!
% 2.25/0.73 % (641826)------------------------------
% 2.25/0.73 % (641826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.25/0.73 % (641826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.25/0.73 % (641826)CaDiCaL version: 2.1.3
% 2.25/0.73 % (641826)Termination reason: Instruction limit
% 2.25/0.73 % (641826)Termination phase: Naming
% 2.25/0.73 % (641826)Time elapsed: 0.023 s
% 2.25/0.73 % (641826)Peak memory usage: 11 MB
% 2.25/0.73 % (641826)Instructions burned: 26 (million)
% 2.25/0.73 % (641836)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=531074986:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 2.25/0.73 % (641833)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=166214163:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 2.25/0.73 % (641834)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=2677406651:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2998 on theBenchmark for (2998ds/2Mi)
% 2.25/0.73 % (641834)Instruction limit reached!
% 2.25/0.73 % (641834)------------------------------
% 2.25/0.73 % (641834)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.25/0.73 % (641834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.25/0.73 % (641834)CaDiCaL version: 2.1.3
% 2.25/0.73 % (641834)Termination reason: Instruction limit
% 2.25/0.73 % (641834)Termination phase: shuffling
% 2.25/0.73 % (641834)Time elapsed: 0.003 s
% 2.25/0.73 % (641834)Peak memory usage: 10 MB
% 2.25/0.73 % (641834)Instructions burned: 3 (million)
% 2.25/0.73 % (641836)Instruction limit reached!
% 2.25/0.73 % (641836)------------------------------
% 2.25/0.73 % (641836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.25/0.73 % (641836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.25/0.73 % (641836)CaDiCaL version: 2.1.3
% 2.25/0.73 % (641836)Termination reason: Instruction limit
% 2.25/0.73 % (641836)Termination phase: Property scanning
% 2.25/0.73 % (641836)Time elapsed: 0.012 s
% 2.25/0.73 % (641836)Peak memory usage: 10 MB
% 2.25/0.73 % (641836)Instructions burned: 27 (million)
% 2.25/0.73 % (641837)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=110786562:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 2.25/0.73 % (641833)Instruction limit reached!
% 2.25/0.73 % (641833)------------------------------
% 2.25/0.73 % (641833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.25/0.73 % (641833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.25/0.73 % (641833)CaDiCaL version: 2.1.3
% 2.25/0.73 % (641833)Termination reason: Instruction limit
% 2.25/0.73 % (641833)Termination phase: shuffling
% 2.25/0.73 % (641833)Time elapsed: 0.012 s
% 2.25/0.73 % (641833)Peak memory usage: 10 MB
% 2.25/0.73 % (641833)Instructions burned: 15 (million)
% 2.25/0.73 % (641838)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=3390279197:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 2.76/0.81 % (641843)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 2.76/0.81 % (641843)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=1897217093:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2997 on theBenchmark for (2997ds/8Mi)
% 2.76/0.81 % (641837)Instruction limit reached!
% 2.76/0.81 % (641837)------------------------------
% 2.76/0.81 % (641837)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.76/0.81 % (641837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.76/0.81 % (641837)CaDiCaL version: 2.1.3
% 2.76/0.81 % (641837)Termination reason: Instruction limit
% 2.76/0.81 % (641837)Termination phase: Property scanning
% 2.76/0.81 % (641837)Time elapsed: 0.019 s
% 2.76/0.81 % (641837)Peak memory usage: 10 MB
% 2.76/0.81 % (641837)Instructions burned: 23 (million)
% 2.76/0.81 % (641843)Instruction limit reached!
% 2.76/0.81 % (641843)------------------------------
% 2.76/0.81 % (641843)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.76/0.81 % (641843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.76/0.81 % (641843)CaDiCaL version: 2.1.3
% 2.76/0.81 % (641843)Termination reason: Instruction limit
% 2.76/0.81 % (641843)Termination phase: shuffling
% 2.76/0.81 % (641843)Time elapsed: 0.004 s
% 2.76/0.81 % (641843)Peak memory usage: 10 MB
% 2.76/0.81 % (641843)Instructions burned: 9 (million)
% 2.76/0.81 % (641842)WARNING Broken Constraint: if sine_to_age_generality_threshold(10) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 2.76/0.81 % (641842)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 2.76/0.81 % (641842)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=3875571208:i=14:add=off:nm=40:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 2.76/0.81 % (641845)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=3250482203:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2997 on theBenchmark for (2997ds/31Mi)
% 2.76/0.81 % (641842)Instruction limit reached!
% 2.76/0.81 % (641842)------------------------------
% 2.76/0.81 % (641842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.76/0.81 % (641842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.76/0.81 % (641842)CaDiCaL version: 2.1.3
% 2.76/0.81 % (641842)Termination reason: Instruction limit
% 2.76/0.81 % (641842)Termination phase: shuffling
% 2.76/0.81 % (641842)Time elapsed: 0.012 s
% 2.76/0.81 % (641842)Peak memory usage: 10 MB
% 2.76/0.81 % (641842)Instructions burned: 14 (million)
% 2.76/0.81 % (641848)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=1220858835:i=7:hud=5:bd=preordered:rtra=on:bet=on_2997 on theBenchmark for (2997ds/7Mi)
% 2.76/0.81 % (641848)Instruction limit reached!
% 2.76/0.81 % (641848)------------------------------
% 2.76/0.81 % (641848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.76/0.81 % (641848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.76/0.81 % (641848)CaDiCaL version: 2.1.3
% 2.76/0.81 % (641848)Termination reason: Instruction limit
% 2.76/0.81 % (641848)Termination phase: shuffling
% 2.76/0.81 % (641848)Time elapsed: 0.005 s
% 2.76/0.81 % (641848)Peak memory usage: 10 MB
% 2.76/0.81 % (641848)Instructions burned: 9 (million)
% 2.76/0.81 % (641849)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=1529292706:i=23:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/23Mi)
% 2.76/0.81 % (641838)Instruction limit reached!
% 2.76/0.81 % (641838)------------------------------
% 2.76/0.81 % (641838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.76/0.81 % (641838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.76/0.81 % (641838)CaDiCaL version: 2.1.3
% 2.76/0.81 % (641838)Termination reason: Instruction limit
% 2.76/0.81 % (641838)Termination phase: Property scanning
% 3.10/0.95 % (641838)Time elapsed: 0.051 s
% 3.10/0.95 % (641838)Peak memory usage: 12 MB
% 3.10/0.95 % (641838)Instructions burned: 60 (million)
% 3.10/0.95 % (641845)Instruction limit reached!
% 3.10/0.95 % (641845)------------------------------
% 3.10/0.95 % (641845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.10/0.95 % (641845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.10/0.95 % (641845)CaDiCaL version: 2.1.3
% 3.10/0.95 % (641845)Termination reason: Instruction limit
% 3.10/0.95 % (641845)Termination phase: Property scanning
% 3.10/0.95 % (641845)Time elapsed: 0.025 s
% 3.10/0.95 % (641845)Peak memory usage: 10 MB
% 3.10/0.95 % (641845)Instructions burned: 31 (million)
% 3.10/0.95 % (641854)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=1755304222:i=1240:rtra=on:ixr=off_2997 on theBenchmark for (2997ds/1240Mi)
% 3.10/0.95 % (641852)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=3245807318:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2997 on theBenchmark for (2997ds/20Mi)
% 3.10/0.95 % (641849)Instruction limit reached!
% 3.10/0.95 % (641849)------------------------------
% 3.10/0.95 % (641849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.10/0.95 % (641849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.10/0.95 % (641849)CaDiCaL version: 2.1.3
% 3.10/0.95 % (641849)Termination reason: Instruction limit
% 3.10/0.95 % (641849)Termination phase: Property scanning
% 3.10/0.95 % (641849)Time elapsed: 0.019 s
% 3.10/0.95 % (641849)Peak memory usage: 10 MB
% 3.10/0.95 % (641849)Instructions burned: 23 (million)
% 3.10/0.95 % (641857)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=222121979:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/193Mi)
% 3.10/0.95 % (641852)Instruction limit reached!
% 3.10/0.95 % (641852)------------------------------
% 3.10/0.95 % (641852)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.10/0.95 % (641852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.10/0.95 % (641852)CaDiCaL version: 2.1.3
% 3.10/0.95 % (641852)Termination reason: Instruction limit
% 3.10/0.95 % (641852)Termination phase: shuffling
% 3.10/0.95 % (641852)Time elapsed: 0.017 s
% 3.10/0.95 % (641852)Peak memory usage: 10 MB
% 3.10/0.95 % (641852)Instructions burned: 20 (million)
% 3.10/0.95 % (641856)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=1138089152:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2997 on theBenchmark for (2997ds/143Mi)
% 3.10/0.95 % (641857)Refutation not found, incomplete strategy
% 3.10/0.95 % (641857)------------------------------
% 3.10/0.95 % (641857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.10/0.95 % (641857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.10/0.95 % (641857)CaDiCaL version: 2.1.3
% 3.10/0.95 % (641857)Termination reason: Refutation not found, incomplete strategy
% 3.10/0.95 % (641857)Time elapsed: 0.027 s
% 3.10/0.95 % (641857)Peak memory usage: 13 MB
% 3.10/0.95 % (641857)Instructions burned: 64 (million)
% 3.10/0.95 % (641857)------------------------------
% 3.10/0.95 % (641857)------------------------------
% 3.10/0.95 % (641860)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=188421825:i=42:hud=10:rtra=on_2997 on theBenchmark for (2997ds/42Mi)
% 3.10/0.95 % (641862)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 3.10/0.95 % (641862)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=40604192:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2996 on theBenchmark for (2996ds/7Mi)
% 3.10/0.95 % (641864)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=3762235117:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/181Mi)
% 3.10/0.95 % (641862)Instruction limit reached!
% 3.10/0.95 % (641862)------------------------------
% 3.10/0.95 % (641862)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.10/0.95 % (641862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.10/0.95 % (641862)CaDiCaL version: 2.1.3
% 3.10/0.95 % (641862)Termination reason: Instruction limit
% 3.10/0.95 % (641862)Termination phase: shuffling
% 3.10/0.95 % (641862)Time elapsed: 0.007 s
% 3.10/0.95 % (641862)Peak memory usage: 10 MB
% 3.10/0.95 % (641862)Instructions burned: 8 (million)
% 4.70/1.09 % (641860)Instruction limit reached!
% 4.70/1.09 % (641860)------------------------------
% 4.70/1.09 % (641860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.70/1.09 % (641860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.70/1.09 % (641860)CaDiCaL version: 2.1.3
% 4.70/1.09 % (641860)Termination reason: Instruction limit
% 4.70/1.09 % (641860)Termination phase: Property scanning
% 4.70/1.09 % (641860)Time elapsed: 0.035 s
% 4.70/1.09 % (641860)Peak memory usage: 11 MB
% 4.70/1.09 % (641860)Instructions burned: 42 (million)
% 4.70/1.09 % (641864)Refutation not found, incomplete strategy
% 4.70/1.09 % (641864)------------------------------
% 4.70/1.09 % (641864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.70/1.09 % (641864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.70/1.09 % (641864)CaDiCaL version: 2.1.3
% 4.70/1.09 % (641864)Termination reason: Refutation not found, incomplete strategy
% 4.70/1.09 % (641864)Time elapsed: 0.028 s
% 4.70/1.09 % (641864)Peak memory usage: 13 MB
% 4.70/1.09 % (641864)Instructions burned: 53 (million)
% 4.70/1.09 % (641864)------------------------------
% 4.70/1.09 % (641864)------------------------------
% 4.70/1.09 % (641869)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 4.70/1.09 % (641868)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=337337663:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2996 on theBenchmark for (2996ds/169Mi)
% 4.70/1.09 % (641869)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=774773222:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2996 on theBenchmark for (2996ds/6Mi)
% 4.70/1.09 % (641869)Instruction limit reached!
% 4.70/1.09 % (641869)------------------------------
% 4.70/1.09 % (641869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.70/1.09 % (641869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.70/1.09 % (641869)CaDiCaL version: 2.1.3
% 4.70/1.09 % (641869)Termination reason: Instruction limit
% 4.70/1.09 % (641869)Termination phase: shuffling
% 4.70/1.09 % (641869)Time elapsed: 0.003 s
% 4.70/1.09 % (641869)Peak memory usage: 10 MB
% 4.70/1.09 % (641869)Instructions burned: 7 (million)
% 4.70/1.09 % (641870)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=1181782537:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2996 on theBenchmark for (2996ds/22Mi)
% 4.70/1.09 % (641873)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=366560908:i=19:add=on:rtra=on_2996 on theBenchmark for (2996ds/19Mi)
% 4.70/1.09 % (641870)Instruction limit reached!
% 4.70/1.09 % (641870)------------------------------
% 4.70/1.09 % (641870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.70/1.09 % (641870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.70/1.09 % (641870)CaDiCaL version: 2.1.3
% 4.70/1.09 % (641870)Termination reason: Instruction limit
% 4.70/1.09 % (641870)Termination phase: Property scanning
% 4.70/1.09 % (641870)Time elapsed: 0.011 s
% 4.70/1.09 % (641870)Peak memory usage: 10 MB
% 4.70/1.09 % (641870)Instructions burned: 23 (million)
% 4.70/1.09 % (641873)Instruction limit reached!
% 4.70/1.09 % (641873)------------------------------
% 4.70/1.09 % (641873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.70/1.09 % (641873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.70/1.09 % (641873)CaDiCaL version: 2.1.3
% 4.70/1.09 % (641873)Termination reason: Instruction limit
% 4.70/1.09 % (641873)Termination phase: shuffling
% 4.70/1.09 % (641873)Time elapsed: 0.008 s
% 4.70/1.09 % (641873)Peak memory usage: 10 MB
% 4.70/1.09 % (641873)Instructions burned: 19 (million)
% 4.70/1.09 % (641856)Instruction limit reached!
% 4.70/1.09 % (641856)------------------------------
% 4.70/1.09 % (641856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.70/1.09 % (641856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.70/1.09 % (641856)CaDiCaL version: 2.1.3
% 4.70/1.09 % (641856)Termination reason: Instruction limit
% 4.70/1.09 % (641856)Termination phase: Saturation
% 4.70/1.09 % (641856)Time elapsed: 0.115 s
% 4.70/1.09 % (641856)Peak memory usage: 13 MB
% 4.70/1.09 % (641856)Instructions burned: 143 (million)
% 5.39/1.21 % (641877)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=207029515:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2995 on theBenchmark for (2995ds/853Mi)
% 5.39/1.21 % (641876)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=2679635872:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/316Mi)
% 5.39/1.21 % (641878)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=4179684360:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2995 on theBenchmark for (2995ds/45Mi)
% 5.39/1.21 % (641829)Instruction limit reached!
% 5.39/1.21 % (641829)------------------------------
% 5.39/1.21 % (641829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.39/1.21 % (641829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.39/1.21 % (641829)CaDiCaL version: 2.1.3
% 5.39/1.21 % (641829)Termination reason: Instruction limit
% 5.39/1.21 % (641829)Termination phase: Saturation
% 5.39/1.21 % (641829)Time elapsed: 0.282 s
% 5.39/1.21 % (641829)Peak memory usage: 15 MB
% 5.39/1.21 % (641829)Instructions burned: 328 (million)
% 5.39/1.21 % (641878)Instruction limit reached!
% 5.39/1.21 % (641878)------------------------------
% 5.39/1.21 % (641878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.39/1.21 % (641878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.39/1.21 % (641878)CaDiCaL version: 2.1.3
% 5.39/1.21 % (641878)Termination reason: Instruction limit
% 5.39/1.21 % (641878)Termination phase: Preprocessing 3
% 5.39/1.21 % (641878)Time elapsed: 0.024 s
% 5.39/1.21 % (641878)Peak memory usage: 12 MB
% 5.39/1.21 % (641878)Instructions burned: 45 (million)
% 5.39/1.21 % (641883)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=827064048:i=480:rtra=on_2995 on theBenchmark for (2995ds/480Mi)
% 5.39/1.21 % (641884)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=2177767658:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2995 on theBenchmark for (2995ds/21Mi)
% 5.39/1.21 % (641884)Instruction limit reached!
% 5.39/1.21 % (641884)------------------------------
% 5.39/1.21 % (641884)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.39/1.21 % (641884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.39/1.21 % (641884)CaDiCaL version: 2.1.3
% 5.39/1.21 % (641884)Termination reason: Instruction limit
% 5.39/1.21 % (641884)Termination phase: Property scanning
% 5.39/1.21 % (641884)Time elapsed: 0.018 s
% 5.39/1.21 % (641884)Peak memory usage: 10 MB
% 5.39/1.21 % (641884)Instructions burned: 21 (million)
% 5.39/1.21 % (641868)Instruction limit reached!
% 5.39/1.21 % (641868)------------------------------
% 5.39/1.21 % (641868)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.39/1.21 % (641868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.39/1.21 % (641868)CaDiCaL version: 2.1.3
% 5.39/1.21 % (641868)Termination reason: Instruction limit
% 5.39/1.21 % (641868)Termination phase: Saturation
% 5.39/1.21 % (641868)Time elapsed: 0.147 s
% 5.39/1.21 % (641868)Peak memory usage: 13 MB
% 5.39/1.21 % (641868)Instructions burned: 170 (million)
% 5.39/1.21 % (641888)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 5.39/1.21 % (641888)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=1832867969:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/200Mi)
% 5.39/1.21 % (641889)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=1001183187:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2994 on theBenchmark for (2994ds/13Mi)
% 5.39/1.21 % (641889)Instruction limit reached!
% 5.39/1.21 % (641889)------------------------------
% 5.39/1.21 % (641889)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.39/1.21 % (641889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.39/1.21 % (641889)CaDiCaL version: 2.1.3
% 5.39/1.21 % (641889)Termination reason: Instruction limit
% 5.39/1.21 % (641889)Termination phase: shuffling
% 6.17/1.37 % (641889)Time elapsed: 0.012 s
% 6.17/1.37 % (641889)Peak memory usage: 10 MB
% 6.17/1.37 % (641889)Instructions burned: 13 (million)
% 6.17/1.37 % (641797)Instruction limit reached!
% 6.17/1.37 % (641797)------------------------------
% 6.17/1.37 % (641797)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.17/1.37 % (641797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.17/1.37 % (641797)CaDiCaL version: 2.1.3
% 6.17/1.37 % (641797)Termination reason: Instruction limit
% 6.17/1.37 % (641797)Termination phase: Saturation
% 6.17/1.37 % (641797)Time elapsed: 0.551 s
% 6.17/1.37 % (641797)Peak memory usage: 19 MB
% 6.17/1.37 % (641797)Instructions burned: 635 (million)
% 6.17/1.37 % (641892)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=2033425274:i=66:s2at=3:nm=2:rtra=on:rawr=on_2994 on theBenchmark for (2994ds/66Mi)
% 6.17/1.37 % (641883)Refutation not found, incomplete strategy
% 6.17/1.37 % (641883)------------------------------
% 6.17/1.37 % (641883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.17/1.37 % (641883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.17/1.37 % (641883)CaDiCaL version: 2.1.3
% 6.17/1.37 % (641883)Termination reason: Refutation not found, incomplete strategy
% 6.17/1.37 % (641883)Time elapsed: 0.141 s
% 6.17/1.37 % (641883)Peak memory usage: 15 MB
% 6.17/1.37 % (641883)Instructions burned: 161 (million)
% 6.17/1.37 % (641883)------------------------------
% 6.17/1.37 % (641883)------------------------------
% 6.17/1.37 % (641893)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=4261682889:i=51:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/51Mi)
% 6.17/1.37 % (641892)Instruction limit reached!
% 6.17/1.37 % (641892)------------------------------
% 6.17/1.37 % (641892)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.17/1.37 % (641892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.17/1.37 % (641892)CaDiCaL version: 2.1.3
% 6.17/1.37 % (641892)Termination reason: Instruction limit
% 6.17/1.37 % (641892)Termination phase: Property scanning
% 6.17/1.37 % (641892)Time elapsed: 0.060 s
% 6.17/1.37 % (641892)Peak memory usage: 10 MB
% 6.17/1.37 % (641892)Instructions burned: 66 (million)
% 6.17/1.37 % (641896)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=341991459:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/31Mi)
% 6.17/1.37 % (641893)Instruction limit reached!
% 6.17/1.37 % (641893)------------------------------
% 6.17/1.37 % (641893)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.17/1.37 % (641893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.17/1.37 % (641893)CaDiCaL version: 2.1.3
% 6.17/1.37 % (641893)Termination reason: Instruction limit
% 6.17/1.37 % (641893)Termination phase: Property scanning
% 6.17/1.37 % (641893)Time elapsed: 0.045 s
% 6.17/1.37 % (641893)Peak memory usage: 11 MB
% 6.17/1.37 % (641893)Instructions burned: 51 (million)
% 6.17/1.37 % (641876)Instruction limit reached!
% 6.17/1.37 % (641876)------------------------------
% 6.17/1.37 % (641876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.17/1.37 % (641876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.17/1.37 % (641876)CaDiCaL version: 2.1.3
% 6.17/1.37 % (641876)Termination reason: Instruction limit
% 6.17/1.37 % (641876)Termination phase: Saturation
% 6.17/1.37 % (641876)Time elapsed: 0.248 s
% 6.17/1.37 % (641876)Peak memory usage: 14 MB
% 6.17/1.37 % (641876)Instructions burned: 316 (million)
% 6.17/1.37 % (641896)Instruction limit reached!
% 6.17/1.37 % (641896)------------------------------
% 6.17/1.37 % (641896)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.17/1.37 % (641896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.17/1.37 % (641896)CaDiCaL version: 2.1.3
% 6.17/1.37 % (641896)Termination reason: Instruction limit
% 6.17/1.37 % (641896)Termination phase: Property scanning
% 6.17/1.37 % (641896)Time elapsed: 0.016 s
% 6.17/1.37 % (641896)Peak memory usage: 10 MB
% 6.17/1.37 % (641896)Instructions burned: 33 (million)
% 6.17/1.37 % (641888)Instruction limit reached!
% 6.17/1.37 % (641888)------------------------------
% 6.17/1.37 % (641888)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.17/1.37 % (641888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.94/1.55 % (641888)CaDiCaL version: 2.1.3
% 6.94/1.55 % (641888)Termination reason: Instruction limit
% 6.94/1.55 % (641888)Termination phase: Saturation
% 6.94/1.55 % (641888)Time elapsed: 0.158 s
% 6.94/1.55 % (641888)Peak memory usage: 14 MB
% 6.94/1.55 % (641888)Instructions burned: 202 (million)
% 6.94/1.55 % (641898)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=1879092763:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2993 on theBenchmark for (2993ds/137Mi)
% 6.94/1.55 % (641900)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=692765575:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2993 on theBenchmark for (2993ds/67Mi)
% 6.94/1.55 % (641901)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 6.94/1.55 % (641899)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=2557188925:cond=on:i=34:hud=10:nm=10:rtra=on_2993 on theBenchmark for (2993ds/34Mi)
% 6.94/1.55 % (641901)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=2281908145:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2993 on theBenchmark for (2993ds/180Mi)
% 6.94/1.55 % (641903)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=1130907111:st=2:i=246:sd=3:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/246Mi)
% 6.94/1.55 % (641900)Instruction limit reached!
% 6.94/1.55 % (641900)------------------------------
% 6.94/1.55 % (641900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.94/1.55 % (641900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.94/1.55 % (641900)CaDiCaL version: 2.1.3
% 6.94/1.55 % (641900)Termination reason: Instruction limit
% 6.94/1.55 % (641900)Termination phase: Property scanning
% 6.94/1.55 % (641900)Time elapsed: 0.031 s
% 6.94/1.55 % (641900)Peak memory usage: 11 MB
% 6.94/1.55 % (641900)Instructions burned: 69 (million)
% 6.94/1.55 % (641899)Instruction limit reached!
% 6.94/1.55 % (641899)------------------------------
% 6.94/1.55 % (641899)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.94/1.55 % (641899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.94/1.55 % (641899)CaDiCaL version: 2.1.3
% 6.94/1.55 % (641899)Termination reason: Instruction limit
% 6.94/1.55 % (641899)Termination phase: Property scanning
% 6.94/1.55 % (641899)Time elapsed: 0.029 s
% 6.94/1.55 % (641899)Peak memory usage: 10 MB
% 6.94/1.55 % (641899)Instructions burned: 35 (million)
% 6.94/1.55 % (641908)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=1129890914:cond=on:i=96:bd=all:rtra=on_2992 on theBenchmark for (2992ds/96Mi)
% 6.94/1.55 % (641909)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=54333548:i=427:sd=1:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/427Mi)
% 6.94/1.55 % (641898)Instruction limit reached!
% 6.94/1.55 % (641898)------------------------------
% 6.94/1.55 % (641898)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.94/1.55 % (641898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.94/1.55 % (641898)CaDiCaL version: 2.1.3
% 6.94/1.55 % (641898)Termination reason: Instruction limit
% 6.94/1.55 % (641898)Termination phase: Saturation
% 6.94/1.55 % (641898)Time elapsed: 0.111 s
% 6.94/1.55 % (641898)Peak memory usage: 14 MB
% 6.94/1.55 % (641898)Instructions burned: 138 (million)
% 6.94/1.55 % (641909)Refutation not found, incomplete strategy
% 6.94/1.55 % (641909)------------------------------
% 6.94/1.55 % (641909)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.94/1.55 % (641909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.94/1.55 % (641909)CaDiCaL version: 2.1.3
% 6.94/1.55 % (641909)Termination reason: Refutation not found, incomplete strategy
% 6.94/1.55 % (641909)Time elapsed: 0.039 s
% 6.94/1.55 % (641909)Peak memory usage: 13 MB
% 6.94/1.55 % (641909)Instructions burned: 47 (million)
% 6.94/1.55 % (641909)------------------------------
% 6.94/1.55 % (641909)------------------------------
% 6.94/1.55 % (641877)Instruction limit reached!
% 6.94/1.55 % (641877)------------------------------
% 6.94/1.55 % (641877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.94/1.55 % (641877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.94/1.55 % (641877)CaDiCaL version: 2.1.3
% 6.94/1.55 % (641877)Termination reason: Instruction limit
% 6.94/1.72 % (641877)Termination phase: Saturation
% 6.94/1.72 % (641877)Time elapsed: 0.399 s
% 6.94/1.72 % (641877)Peak memory usage: 20 MB
% 6.94/1.72 % (641877)Instructions burned: 855 (million)
% 6.94/1.72 % (641912)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=2680445754:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/874Mi)
% 6.94/1.72 % (641908)Instruction limit reached!
% 6.94/1.72 % (641908)------------------------------
% 6.94/1.72 % (641908)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.94/1.72 % (641908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.94/1.72 % (641908)CaDiCaL version: 2.1.3
% 6.94/1.72 % (641908)Termination reason: Instruction limit
% 6.94/1.72 % (641908)Termination phase: Saturation
% 6.94/1.72 % (641908)Time elapsed: 0.075 s
% 6.94/1.72 % (641908)Peak memory usage: 12 MB
% 6.94/1.72 % (641908)Instructions burned: 96 (million)
% 6.94/1.72 % (641914)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=3532904200:st=1.5:i=130:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/130Mi)
% 6.94/1.72 % (641913)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=691845174:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/515Mi)
% 6.94/1.73 % (641901)Instruction limit reached!
% 6.94/1.73 % (641901)------------------------------
% 6.94/1.73 % (641901)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.94/1.73 % (641901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.94/1.73 % (641901)CaDiCaL version: 2.1.3
% 6.94/1.73 % (641901)Termination reason: Instruction limit
% 6.94/1.73 % (641901)Termination phase: Saturation
% 6.94/1.73 % (641901)Time elapsed: 0.148 s
% 6.94/1.73 % (641901)Peak memory usage: 13 MB
% 6.94/1.73 % (641901)Instructions burned: 180 (million)
% 6.94/1.73 % (641916)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=4278379543:i=44:ep=R:rtra=on:ntd=on_2991 on theBenchmark for (2991ds/44Mi)
% 6.94/1.73 % (641919)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=4204808818:s2a=on:i=571:nm=16:rtra=on_2991 on theBenchmark for (2991ds/571Mi)
% 6.94/1.73 % (641914)Instruction limit reached!
% 6.94/1.73 % (641914)------------------------------
% 6.94/1.73 % (641914)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.94/1.73 % (641914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.94/1.73 % (641914)CaDiCaL version: 2.1.3
% 6.94/1.73 % (641914)Termination reason: Instruction limit
% 6.94/1.73 % (641914)Termination phase: Saturation
% 6.94/1.73 % (641914)Time elapsed: 0.059 s
% 6.94/1.73 % (641914)Peak memory usage: 13 MB
% 6.94/1.73 % (641914)Instructions burned: 131 (million)
% 6.94/1.73 % (641916)Instruction limit reached!
% 6.94/1.73 % (641916)------------------------------
% 6.94/1.73 % (641916)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.94/1.73 % (641916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.94/1.73 % (641916)CaDiCaL version: 2.1.3
% 6.94/1.73 % (641916)Termination reason: Instruction limit
% 6.94/1.73 % (641916)Termination phase: Property scanning
% 6.94/1.73 % (641916)Time elapsed: 0.036 s
% 6.94/1.73 % (641916)Peak memory usage: 11 MB
% 6.94/1.73 % (641916)Instructions burned: 44 (million)
% 6.94/1.73 % (641922)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=1643981731:i=450:rtra=on:ixr=off:ntd=on_2990 on theBenchmark for (2990ds/450Mi)
% 6.94/1.73 % (641923)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=3186570122:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/95Mi)
% 6.94/1.73 % (641903)Instruction limit reached!
% 6.94/1.73 % (641903)------------------------------
% 6.94/1.73 % (641903)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.94/1.73 % (641903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.94/1.73 % (641903)CaDiCaL version: 2.1.3
% 6.94/1.73 % (641903)Termination reason: Instruction limit
% 6.94/1.73 % (641903)Termination phase: Saturation
% 6.94/1.73 % (641903)Time elapsed: 0.219 s
% 6.94/1.73 % (641903)Peak memory usage: 15 MB
% 6.94/1.73 % (641903)Instructions burned: 246 (million)
% 6.94/1.73 % (641926)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=599471817:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2990 on theBenchmark for (2990ds/65Mi)
% 9.11/1.90 % (641926)Instruction limit reached!
% 9.11/1.90 % (641926)------------------------------
% 9.11/1.90 % (641926)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.11/1.90 % (641926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.11/1.90 % (641926)CaDiCaL version: 2.1.3
% 9.11/1.90 % (641926)Termination reason: Instruction limit
% 9.11/1.90 % (641926)Termination phase: Property scanning
% 9.11/1.90 % (641926)Time elapsed: 0.035 s
% 9.11/1.90 % (641926)Peak memory usage: 11 MB
% 9.11/1.90 % (641926)Instructions burned: 65 (million)
% 9.11/1.90 % (641923)Instruction limit reached!
% 9.11/1.90 % (641923)------------------------------
% 9.11/1.90 % (641923)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.11/1.90 % (641923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.11/1.90 % (641923)CaDiCaL version: 2.1.3
% 9.11/1.90 % (641923)Termination reason: Instruction limit
% 9.11/1.90 % (641923)Termination phase: Saturation
% 9.11/1.90 % (641923)Time elapsed: 0.076 s
% 9.11/1.90 % (641923)Peak memory usage: 12 MB
% 9.11/1.90 % (641923)Instructions burned: 96 (million)
% 9.11/1.90 % (641928)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=3163644512: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_2989 on theBenchmark for (2989ds/105Mi)
% 9.11/1.90 % (641929)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=4064637159:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2989 on theBenchmark for (2989ds/5755Mi)
% 9.11/1.90 % (641929)Refutation not found, incomplete strategy
% 9.11/1.90 % (641929)------------------------------
% 9.11/1.90 % (641929)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.11/1.90 % (641929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.11/1.90 % (641929)CaDiCaL version: 2.1.3
% 9.11/1.90 % (641929)Termination reason: Refutation not found, incomplete strategy
% 9.11/1.90 % (641929)Time elapsed: 0.029 s
% 9.11/1.90 % (641929)Peak memory usage: 13 MB
% 9.11/1.90 % (641929)Instructions burned: 29 (million)
% 9.11/1.90 % (641929)------------------------------
% 9.11/1.90 % (641929)------------------------------
% 9.11/1.90 % (641928)Instruction limit reached!
% 9.11/1.90 % (641928)------------------------------
% 9.11/1.90 % (641928)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.11/1.90 % (641928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.11/1.90 % (641928)CaDiCaL version: 2.1.3
% 9.11/1.90 % (641928)Termination reason: Instruction limit
% 9.11/1.90 % (641928)Termination phase: Saturation
% 9.11/1.90 % (641928)Time elapsed: 0.054 s
% 9.11/1.90 % (641928)Peak memory usage: 12 MB
% 9.11/1.90 % (641928)Instructions burned: 106 (million)
% 9.11/1.90 % (641933)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=716868501:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2988 on theBenchmark for (2988ds/495Mi)
% 9.11/1.90 % (641932)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=781702630:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2989 on theBenchmark for (2989ds/375Mi)
% 9.11/1.90 % (641922)Instruction limit reached!
% 9.11/1.90 % (641922)------------------------------
% 9.11/1.90 % (641922)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.11/1.90 % (641922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.11/1.90 % (641922)CaDiCaL version: 2.1.3
% 9.11/1.90 % (641922)Termination reason: Instruction limit
% 9.11/1.90 % (641922)Termination phase: Saturation
% 9.11/1.90 % (641922)Time elapsed: 0.202 s
% 9.11/1.90 % (641922)Peak memory usage: 18 MB
% 9.11/1.90 % (641922)Instructions burned: 450 (million)
% 9.11/1.90 % (641936)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=4159576094:cond=on:i=34:hud=10:nm=10:rtra=on_2988 on theBenchmark for (2988ds/34Mi)
% 9.11/1.90 % (641936)Instruction limit reached!
% 9.11/1.90 % (641936)------------------------------
% 9.11/1.90 % (641936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.11/1.90 % (641936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.11/1.99 % (641936)CaDiCaL version: 2.1.3
% 9.11/1.99 % (641936)Termination reason: Instruction limit
% 9.11/1.99 % (641936)Termination phase: Property scanning
% 9.11/1.99 % (641936)Time elapsed: 0.016 s
% 9.11/1.99 % (641936)Peak memory usage: 10 MB
% 9.11/1.99 % (641936)Instructions burned: 35 (million)
% 9.11/1.99 % (641938)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=2230825933:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2988 on theBenchmark for (2988ds/91Mi)
% 9.11/1.99 % (641938)Instruction limit reached!
% 9.11/1.99 % (641938)------------------------------
% 9.11/1.99 % (641938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.11/1.99 % (641938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.11/1.99 % (641938)CaDiCaL version: 2.1.3
% 9.11/1.99 % (641938)Termination reason: Instruction limit
% 9.11/1.99 % (641938)Termination phase: Property scanning
% 9.11/1.99 % (641938)Time elapsed: 0.053 s
% 9.11/1.99 % (641938)Peak memory usage: 11 MB
% 9.11/1.99 % (641938)Instructions burned: 91 (million)
% 9.11/1.99 % (641940)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=2513295406:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2987 on theBenchmark for (2987ds/66Mi)
% 9.11/1.99 % (641940)Refutation not found, incomplete strategy
% 9.11/1.99 % (641940)------------------------------
% 9.11/1.99 % (641940)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.11/1.99 % (641940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.11/1.99 % (641940)CaDiCaL version: 2.1.3
% 9.11/1.99 % (641940)Termination reason: Refutation not found, incomplete strategy
% 9.11/1.99 % (641940)Time elapsed: 0.020 s
% 9.11/1.99 % (641940)Peak memory usage: 13 MB
% 9.11/1.99 % (641940)Instructions burned: 29 (million)
% 9.11/1.99 % (641940)------------------------------
% 9.11/1.99 % (641940)------------------------------
% 9.11/1.99 % (641913)Instruction limit reached!
% 9.11/1.99 % (641913)------------------------------
% 9.11/1.99 % (641913)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.11/1.99 % (641913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.11/1.99 % (641913)CaDiCaL version: 2.1.3
% 9.11/1.99 % (641913)Termination reason: Instruction limit
% 9.11/1.99 % (641913)Termination phase: Saturation
% 9.11/1.99 % (641913)Time elapsed: 0.443 s
% 9.11/1.99 % (641913)Peak memory usage: 16 MB
% 9.11/1.99 % (641913)Instructions burned: 515 (million)
% 9.11/1.99 % (641854)Instruction limit reached!
% 9.11/1.99 % (641854)------------------------------
% 9.11/1.99 % (641854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.11/1.99 % (641854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.11/1.99 % (641854)CaDiCaL version: 2.1.3
% 9.11/1.99 % (641854)Termination reason: Instruction limit
% 9.11/1.99 % (641854)Termination phase: Saturation
% 9.11/1.99 % (641854)Time elapsed: 1.028 s
% 9.11/1.99 % (641854)Peak memory usage: 20 MB
% 9.11/1.99 % (641854)Instructions burned: 1240 (million)
% 9.11/1.99 % (641942)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=2656081835:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2987 on theBenchmark for (2987ds/22Mi)
% 9.11/1.99 % (641932)Instruction limit reached!
% 9.11/1.99 % (641932)------------------------------
% 9.11/1.99 % (641932)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.11/1.99 % (641932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.11/1.99 % (641932)CaDiCaL version: 2.1.3
% 9.11/1.99 % (641932)Termination reason: Instruction limit
% 9.11/1.99 % (641932)Termination phase: Saturation
% 9.11/1.99 % (641932)Time elapsed: 0.202 s
% 9.11/1.99 % (641932)Peak memory usage: 14 MB
% 9.11/1.99 % (641932)Instructions burned: 376 (million)
% 9.11/1.99 % (641943)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=335849383:i=338:bd=all:ins=4:rtra=on_2986 on theBenchmark for (2986ds/338Mi)
% 9.11/1.99 % (641942)Instruction limit reached!
% 9.11/1.99 % (641942)------------------------------
% 9.11/1.99 % (641942)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.11/1.99 % (641942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.11/1.99 % (641942)CaDiCaL version: 2.1.3
% 9.11/1.99 % (641942)Termination reason: Instruction limit
% 9.11/1.99 % (641942)Termination phase: Property scanning
% 11.68/2.09 % (641942)Time elapsed: 0.019 s
% 11.68/2.09 % (641942)Peak memory usage: 10 MB
% 11.68/2.09 % (641942)Instructions burned: 22 (million)
% 11.68/2.09 % (641944)lrs+10_1_sil=128000:si=on:urr=on:random_seed=863641931:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2986 on theBenchmark for (2986ds/28Mi)
% 11.68/2.09 % (641946)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 11.68/2.09 % (641946)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=4091406085:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2986 on theBenchmark for (2986ds/137Mi)
% 11.68/2.09 % (641948)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=3420798731:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2986 on theBenchmark for (2986ds/340Mi)
% 11.68/2.09 % (641944)Instruction limit reached!
% 11.68/2.09 % (641944)------------------------------
% 11.68/2.09 % (641944)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.68/2.09 % (641944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.68/2.09 % (641944)CaDiCaL version: 2.1.3
% 11.68/2.09 % (641944)Termination reason: Instruction limit
% 11.68/2.09 % (641944)Termination phase: Property scanning
% 11.68/2.09 % (641944)Time elapsed: 0.023 s
% 11.68/2.09 % (641944)Peak memory usage: 10 MB
% 11.68/2.09 % (641944)Instructions burned: 28 (million)
% 11.68/2.09 % (641919)Instruction limit reached!
% 11.68/2.09 % (641919)------------------------------
% 11.68/2.09 % (641919)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.68/2.09 % (641919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.68/2.09 % (641919)CaDiCaL version: 2.1.3
% 11.68/2.09 % (641919)Termination reason: Instruction limit
% 11.68/2.09 % (641919)Termination phase: Saturation
% 11.68/2.09 % (641919)Time elapsed: 0.490 s
% 11.68/2.09 % (641919)Peak memory usage: 17 MB
% 11.68/2.09 % (641919)Instructions burned: 572 (million)
% 11.68/2.09 % (641952)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=816774179:i=227:sd=1:bd=all:rtra=on:ss=axioms_2986 on theBenchmark for (2986ds/227Mi)
% 11.68/2.09 % (641954)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 11.68/2.09 % (641954)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=4249404721:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2985 on theBenchmark for (2985ds/373Mi)
% 11.68/2.09 % (641952)Refutation not found, incomplete strategy
% 11.68/2.09 % (641952)------------------------------
% 11.68/2.09 % (641952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.68/2.09 % (641952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.68/2.09 % (641952)CaDiCaL version: 2.1.3
% 11.68/2.09 % (641952)Termination reason: Refutation not found, incomplete strategy
% 11.68/2.09 % (641952)Time elapsed: 0.042 s
% 11.68/2.09 % (641952)Peak memory usage: 12 MB
% 11.68/2.09 % (641952)Instructions burned: 51 (million)
% 11.68/2.09 % (641952)------------------------------
% 11.68/2.09 % (641952)------------------------------
% 11.68/2.09 % (641946)Instruction limit reached!
% 11.68/2.09 % (641946)------------------------------
% 11.68/2.09 % (641946)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.68/2.09 % (641946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.68/2.09 % (641946)CaDiCaL version: 2.1.3
% 11.68/2.09 % (641946)Termination reason: Instruction limit
% 11.68/2.09 % (641946)Termination phase: Saturation
% 11.68/2.09 % (641946)Time elapsed: 0.106 s
% 11.68/2.09 % (641946)Peak memory usage: 13 MB
% 11.68/2.09 % (641946)Instructions burned: 138 (million)
% 11.68/2.09 % (641958)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=4139050319:i=116:ep=RSTC:rtra=on:ntd=on_2985 on theBenchmark for (2985ds/116Mi)
% 11.68/2.09 % (641959)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=3299846004:i=575:rtra=on_2985 on theBenchmark for (2985ds/575Mi)
% 11.68/2.09 % (641943)Instruction limit reached!
% 11.68/2.09 % (641943)------------------------------
% 11.68/2.09 % (641943)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.68/2.09 % (641943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.48/2.21 % (641943)CaDiCaL version: 2.1.3
% 12.48/2.21 % (641943)Termination reason: Instruction limit
% 12.48/2.21 % (641943)Termination phase: Saturation
% 12.48/2.21 % (641943)Time elapsed: 0.191 s
% 12.48/2.21 % (641943)Peak memory usage: 15 MB
% 12.48/2.21 % (641943)Instructions burned: 339 (million)
% 12.48/2.21 % (641948)Instruction limit reached!
% 12.48/2.21 % (641948)------------------------------
% 12.48/2.21 % (641948)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.48/2.21 % (641948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.48/2.21 % (641948)CaDiCaL version: 2.1.3
% 12.48/2.21 % (641948)Termination reason: Instruction limit
% 12.48/2.21 % (641948)Termination phase: Saturation
% 12.48/2.21 % (641948)Time elapsed: 0.167 s
% 12.48/2.21 % (641948)Peak memory usage: 15 MB
% 12.48/2.21 % (641948)Instructions burned: 341 (million)
% 12.48/2.21 % (641962)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=1190232344:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2984 on theBenchmark for (2984ds/270Mi)
% 12.48/2.21 % (641958)Instruction limit reached!
% 12.48/2.21 % (641958)------------------------------
% 12.48/2.21 % (641958)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.48/2.21 % (641958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.48/2.21 % (641958)CaDiCaL version: 2.1.3
% 12.48/2.21 % (641958)Termination reason: Instruction limit
% 12.48/2.21 % (641958)Termination phase: Property scanning
% 12.48/2.21 % (641958)Time elapsed: 0.071 s
% 12.48/2.21 % (641958)Peak memory usage: 13 MB
% 12.48/2.21 % (641958)Instructions burned: 116 (million)
% 12.48/2.21 % (641912)Instruction limit reached!
% 12.48/2.21 % (641912)------------------------------
% 12.48/2.21 % (641912)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.48/2.21 % (641912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.48/2.21 % (641912)CaDiCaL version: 2.1.3
% 12.48/2.21 % (641912)Termination reason: Instruction limit
% 12.48/2.21 % (641912)Termination phase: Saturation
% 12.48/2.21 % (641912)Time elapsed: 0.713 s
% 12.48/2.21 % (641912)Peak memory usage: 18 MB
% 12.48/2.21 % (641912)Instructions burned: 874 (million)
% 12.48/2.21 % (641933)Instruction limit reached!
% 12.48/2.21 % (641933)------------------------------
% 12.48/2.21 % (641933)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.48/2.21 % (641933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.48/2.21 % (641933)CaDiCaL version: 2.1.3
% 12.48/2.21 % (641933)Termination reason: Instruction limit
% 12.48/2.21 % (641933)Termination phase: Saturation
% 12.48/2.21 % (641933)Time elapsed: 0.438 s
% 12.48/2.21 % (641933)Peak memory usage: 18 MB
% 12.48/2.21 % (641933)Instructions burned: 495 (million)
% 12.48/2.21 % (641963)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=1721215938: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_2984 on theBenchmark for (2984ds/9840Mi)
% 12.48/2.21 % (641966)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
% 12.48/2.21 % (641966)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=3120774443:avsq=on:i=270:s2at=3:avsqr=1,16:rtra=on:ntd=on_2984 on theBenchmark for (2984ds/270Mi)
% 12.48/2.21 % (641965)lrs+1010_1_sil=128000:si=on:sos=all:uwa=off:nwc=1:random_seed=3826602598:i=421:rtra=on:ss=axioms_2984 on theBenchmark for (2984ds/421Mi)
% 12.48/2.21 % (641967)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=758747731:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2984 on theBenchmark for (2984ds/31Mi)
% 12.48/2.21 % (641959)Refutation not found, incomplete strategy
% 12.48/2.21 % (641959)------------------------------
% 12.48/2.21 % (641959)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.48/2.21 % (641959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.48/2.21 % (641959)CaDiCaL version: 2.1.3
% 12.48/2.21 % (641959)Termination reason: Refutation not found, incomplete strategy
% 12.48/2.21 % (641959)Time elapsed: 0.103 s
% 12.48/2.21 % (641959)Peak memory usage: 14 MB
% 12.48/2.21 % (641959)Instructions burned: 128 (million)
% 12.48/2.21 % (641959)------------------------------
% 12.48/2.21 % (641959)------------------------------
% 12.48/2.21 % (641965)Refutation not found, incomplete strategy
% 12.48/2.21 % (641965)------------------------------
% 12.48/2.21 % (641965)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.48/2.21 % (641965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.48/2.21 % (641965)CaDiCaL version: 2.1.3
% 12.48/2.21 % (641965)Termination reason: Refutation not found, incomplete strategy
% 12.48/2.21 % (641965)Time elapsed: 0.039 s
% 12.48/2.21 % (641965)Peak memory usage: 12 MB
% 12.48/2.21 % (641965)Instructions burned: 47 (million)
% 12.48/2.21 % (641965)------------------------------
% 12.48/2.21 % (641965)------------------------------
% 12.48/2.21 % (641967)Instruction limit reached!
% 12.48/2.21 % (641967)------------------------------
% 12.48/2.21 % (641967)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.48/2.21 % (641967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.48/2.21 % (641967)CaDiCaL version: 2.1.3
% 12.48/2.21 % (641967)Termination reason: Instruction limit
% 12.48/2.21 % (641967)Termination phase: Property scanning
% 12.48/2.21 % (641967)Time elapsed: 0.028 s
% 12.48/2.21 % (641967)Peak memory usage: 10 MB
% 12.48/2.21 % (641967)Instructions burned: 34 (million)
% 12.48/2.21 % (641972)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 12.48/2.21 % (641972)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
% 12.48/2.21 % (641972)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=2366738766:hsqr=1,8:i=1440:s2at=5:add=on:nm=2:rtra=on_2983 on theBenchmark for (2983ds/1440Mi)
% 12.48/2.21 % (641974)lrs+2_16:1_si=on:cbe=off:uwa=interpreted_only:random_seed=3744749014:i=111:add=on:fgj=on:rtra=on:fdi=1024_2983 on theBenchmark for (2983ds/111Mi)
% 12.48/2.21 % (641973)dis+10_2_sil=128000:si=on:random_seed=106814988:s2a=on:i=339:av=off:rtra=on:fe=abstraction:ss=axioms:fsd=on:ntd=on_2983 on theBenchmark for (2983ds/339Mi)
% 12.48/2.21 % (641966)Refutation not found, incomplete strategy
% 12.48/2.21 % (641966)------------------------------
% 12.48/2.21 % (641966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.48/2.21 % (641966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.48/2.21 % (641966)CaDiCaL version: 2.1.3
% 12.48/2.21 % (641966)Termination reason: Refutation not found, incomplete strategy
% 12.48/2.21 % (641966)Time elapsed: 0.091 s
% 12.48/2.21 % (641966)Peak memory usage: 14 MB
% 12.48/2.21 % (641966)Instructions burned: 218 (million)
% 12.48/2.21 % (641966)------------------------------
% 12.48/2.21 % (641966)------------------------------
% 12.48/2.21 % (641978)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=1375821167:st=3:avsq=on:i=122:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2983 on theBenchmark for (2983ds/122Mi)
% 12.48/2.21 % (641962)Instruction limit reached!
% 12.48/2.21 % (641962)------------------------------
% 12.48/2.21 % (641962)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.48/2.21 % (641962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.48/2.21 % (641962)CaDiCaL version: 2.1.3
% 12.48/2.21 % (641962)Termination reason: Instruction limit
% 12.48/2.21 % (641962)Termination phase: Saturation
% 12.48/2.21 % (641962)Time elapsed: 0.161 s
% 12.48/2.21 % (641962)Peak memory usage: 13 MB
% 12.48/2.21 % (641962)Instructions burned: 270 (million)
% 12.48/2.21 % (641973)Refutation not found, incomplete strategy
% 12.48/2.21 % (641973)------------------------------
% 12.48/2.21 % (641973)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.48/2.21 % (641973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.48/2.21 % (641973)CaDiCaL version: 2.1.3
% 12.48/2.21 % (641973)Termination reason: Refutation not found, incomplete strategy
% 12.48/2.21 % (641973)Time elapsed: 0.053 s
% 12.48/2.21 % (641973)Peak memory usage: 13 MB
% 12.48/2.21 % (641973)Instructions burned: 66 (million)
% 12.48/2.21 % (641973)------------------------------
% 12.48/2.21 % (641973)------------------------------
% 12.48/2.21 % (641954)Instruction limit reached!
% 12.48/2.21 % (641954)------------------------------
% 12.48/2.21 % (641954)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.48/2.21 % (641954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.48/2.21 % (641954)CaDiCaL version: 2.1.3
% 12.48/2.21 % (641954)Termination reason: Instruction limit
% 12.48/2.21 % (641954)Termination phase: Saturation
% 12.48/2.21 % (641954)Time elapsed: 0.306 s
% 12.48/2.21 % (641954)Peak memory usage: 12 MB
% 12.48/2.21 % (641954)Instructions burned: 374 (million)
% 12.48/2.21 % (641981)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=3030001992:hsq=on:st=2:i=232:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2982 on theBenchmark for (2982ds/232Mi)
% 12.48/2.21 % (641980)dis+1010_3:2_anc=all_dependent:sil=128000:si=on:sos=on:lma=off:spb=goal_then_units:bce=on:fd=off:random_seed=960498685:uwa_fpi=on:avsq=on:i=136:avsqr=1,32:hud=15:nm=0:rtra=on:ntd=on_2982 on theBenchmark for (2982ds/136Mi)
% 12.48/2.21 % (641974)Instruction limit reached!
% 12.48/2.21 % (641974)------------------------------
% 12.48/2.21 % (641974)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.48/2.21 % (641974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.48/2.21 % (641974)CaDiCaL version: 2.1.3
% 12.48/2.21 % (641974)Termination reason: Instruction limit
% 12.48/2.21 % (641974)Termination phase: Saturation
% 12.48/2.21 % (641974)Time elapsed: 0.089 s
% 12.48/2.21 % (641974)Peak memory usage: 12 MB
% 12.48/2.21 % (641974)Instructions burned: 111 (million)
% 12.48/2.21 % (641978)Instruction limit reached!
% 12.48/2.21 % (641978)------------------------------
% 12.48/2.21 % (641978)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.48/2.21 % (641978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.48/2.21 % (641978)CaDiCaL version: 2.1.3
% 12.48/2.21 % (641978)Termination reason: Instruction limit
% 12.48/2.21 % (641978)Termination phase: Saturation
% 12.48/2.21 % (641978)Time elapsed: 0.060 s
% 12.48/2.21 % (641978)Peak memory usage: 13 MB
% 12.48/2.21 % (641978)Instructions burned: 123 (million)
% 12.48/2.21 % (641982)lrs+1010_8:1_sil=128000:tgt=ground:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:sos=on:plsqr=256,1:uwa=off:random_seed=150688750:i=1254:kws=precedence:bd=preordered:av=off:rtra=on_2982 on theBenchmark for (2982ds/1254Mi)
% 12.48/2.21 % (641985)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 12.48/2.21 % (641985)dis+1002_5:4_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_simp:si=on:plsqr=878,253:plsql=on:uwa=interpreted_only:lwlo=on:random_seed=1411387496:s2a=on:i=281:add=on:rtra=on:fe=axiom:fdi=1024_2982 on theBenchmark for (2982ds/281Mi)
% 12.48/2.21 % (641986)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=1842210232:i=619:add=on:rtra=on_2982 on theBenchmark for (2982ds/619Mi)
% 12.48/2.21 % (641981) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-641789-641981"...
% 12.48/2.21 % (641981)...printing done.
% 12.48/2.21 % (641981)Refutation found. Thanks to Tanya!
% 12.48/2.21 % SZS status Theorem for theBenchmark
% 12.48/2.21 % SZS output start Proof for theBenchmark
% 12.48/2.21 thf(type_def_5, type, term: $tType).
% 12.48/2.21 thf(type_def_6, type, subst: $tType).
% 12.48/2.21 thf(type_def_7, type, sTfun: ($tType * $tType) > $tType).
% 12.48/2.21 thf(func_def_0, type, one: term).
% 12.48/2.21 thf(func_def_1, type, ap: (term > term > term)).
% 12.48/2.21 thf(func_def_2, type, lam: (term > term)).
% 12.48/2.21 thf(func_def_3, type, sub: (term > subst > term)).
% 12.48/2.21 thf(func_def_4, type, id: subst).
% 12.48/2.21 thf(func_def_5, type, sh: subst).
% 12.48/2.21 thf(func_def_6, type, push: (term > subst > subst)).
% 12.48/2.21 thf(func_def_7, type, comp: (subst > subst > subst)).
% 12.48/2.21 thf(func_def_8, type, var: (term > $o)).
% 12.48/2.21 thf(func_def_9, type, pushprop_lem1v2: $o).
% 12.48/2.21 thf(func_def_10, type, pushprop_lem1_gthm: $o).
% 12.48/2.21 thf(func_def_11, type, axmap: $o).
% 12.48/2.21 thf(func_def_12, type, pushprop_lem0_gthm: $o).
% 12.48/2.21 thf(func_def_13, type, shinj: $o).
% 12.48/2.21 thf(func_def_14, type, hoasinduction_lem1v2: $o).
% 12.48/2.21 thf(func_def_15, type, hoasinduction_lem1v2_gthm: $o).
% 12.48/2.21 thf(func_def_16, type, hoasap: (subst > term > subst > term > term)).
% 12.48/2.21 thf(func_def_17, type, induction2lem: $o).
% 12.48/2.21 thf(func_def_18, type, hoasinduction_lem3v2_f: $o).
% 12.48/2.21 thf(func_def_19, type, axvarshift: $o).
% 12.48/2.21 thf(func_def_20, type, hoasapinj2: $o).
% 12.48/2.21 thf(func_def_21, type, hoasapnotvar_gthm: $o).
% 12.48/2.21 thf(func_def_22, type, hoasapinj1: $o).
% 12.48/2.21 thf(func_def_23, type, ulamvar1: $o).
% 12.48/2.21 thf(func_def_24, type, induction2lem_lthm: $o).
% 12.48/2.21 thf(func_def_25, type, hoasinduction_lem3v2_gthm: $o).
% 12.48/2.21 thf(func_def_26, type, apnotvar: $o).
% 12.48/2.21 thf(func_def_27, type, pushprop_lthm_orig: $o).
% 12.48/2.21 thf(func_def_28, type, hoasinduction_lem3v2_f_lthm: $o).
% 12.48/2.21 thf(func_def_29, type, hoasinduction_lthm: $o).
% 12.48/2.21 thf(func_def_30, type, hoasinduction_no_psi_cond_lthm: $o).
% 12.48/2.21 thf(func_def_31, type, hoaslaminj: $o).
% 12.48/2.21 thf(func_def_32, type, hoasinduction_lem3aaa: $o).
% 12.48/2.21 thf(func_def_33, type, induction2lem_gthm: $o).
% 12.48/2.21 thf(func_def_34, type, hoasinduction_lem3aa_lthm: $o).
% 12.48/2.21 thf(func_def_35, type, hoasinduction_lem3: $o).
% 12.48/2.21 thf(func_def_36, type, hoasinduction_lem2: $o).
% 12.48/2.21 thf(func_def_37, type, termmset_lthm: $o).
% 12.48/2.21 thf(func_def_38, type, hoasinduction_lem1: $o).
% 12.48/2.21 thf(func_def_39, type, hoaslamnotap_lthm: $o).
% 12.48/2.21 thf(func_def_40, type, pushprop_lem1v2_lthm: $o).
% 12.48/2.21 thf(func_def_41, type, hoasapnotvar: $o).
% 12.48/2.21 thf(func_def_42, type, hoasinduction_lem0: $o).
% 12.48/2.21 thf(func_def_43, type, hoasinduction: $o).
% 12.48/2.21 thf(func_def_44, type, hoasinduction_gthm: $o).
% 12.48/2.21 thf(func_def_45, type, axapp: $o).
% 12.48/2.21 thf(func_def_46, type, hoaslamnotvar_lthm: $o).
% 12.48/2.21 thf(func_def_47, type, pushprop_lem3v2_lthm: $o).
% 12.48/2.21 thf(func_def_48, type, hoasinduction_lem3b_lthm: $o).
% 12.48/2.21 thf(func_def_49, type, ulamvarind: $o).
% 12.48/2.21 thf(func_def_50, type, induction: $o).
% 12.48/2.21 thf(func_def_51, type, hoasinduction_lem3a_lthm: $o).
% 12.48/2.21 thf(func_def_52, type, termmset_gthm: $o).
% 12.48/2.21 thf(func_def_53, type, hoasinduction_lem3aa: $o).
% 12.48/2.21 thf(func_def_54, type, pushprop_lem1v2_gthm: $o).
% 12.48/2.21 thf(func_def_55, type, hoaslamnotap_gthm: $o).
% 12.48/2.21 thf(func_def_56, type, hoaslamnotvar_gthm: $o).
% 12.48/2.21 thf(func_def_57, type, hoasinduction_lem3b_gthm: $o).
% 12.48/2.21 thf(func_def_58, type, pushprop_lem2v2: $o).
% 12.48/2.21 thf(func_def_59, type, hoasinduction_lem3a_gthm: $o).
% 12.48/2.21 thf(func_def_60, type, axclos: $o).
% 12.48/2.21 thf(func_def_61, type, axassoc: $o).
% 12.48/2.21 thf(func_def_62, type, hoasinduction_lem2v2: $o).
% 12.48/2.21 thf(func_def_63, type, pushprop_lthm: $o).
% 12.48/2.21 thf(func_def_64, type, apinj2: $o).
% 12.48/2.21 thf(func_def_65, type, apinj1: $o).
% 12.48/2.21 thf(func_def_66, type, hoasapinj2_lthm: $o).
% 12.48/2.21 thf(func_def_67, type, hoasinduction_lem3v2a: $o).
% 12.48/2.21 thf(func_def_68, type, hoasapinj1_lthm: $o).
% 12.48/2.21 thf(func_def_69, type, hoaslaminj_lthm: $o).
% 12.48/2.21 thf(func_def_70, type, axvarcons: $o).
% 12.48/2.21 thf(func_def_71, type, hoaslam: (subst > (subst > term > term) > term)).
% 12.48/2.21 thf(func_def_72, type, axscons: $o).
% 12.48/2.21 thf(func_def_73, type, hoasinduction_lem2v2_gthm: $o).
% 12.48/2.21 thf(func_def_74, type, axidr: $o).
% 12.48/2.21 thf(func_def_75, type, pushprop_lem1: $o).
% 12.48/2.21 thf(func_def_76, type, laminj: $o).
% 12.48/2.21 thf(func_def_77, type, hoasinduction_lem3_lthm: $o).
% 12.48/2.21 thf(func_def_78, type, pushprop_lem0: $o).
% 12.48/2.21 thf(func_def_79, type, pushprop_gthm: $o).
% 12.48/2.21 thf(func_def_80, type, axabs: $o).
% 12.48/2.21 thf(func_def_81, type, hoasinduction_lem3v2a_lthm: $o).
% 12.48/2.21 thf(func_def_82, type, hoasinduction_lem2_lthm: $o).
% 12.48/2.21 thf(func_def_83, type, hoasapinj2_gthm: $o).
% 12.48/2.21 thf(func_def_84, type, hoasinduction_p_and_p_prime: ((subst > term > subst > $o) > (term > $o) > $o)).
% 12.48/2.21 thf(func_def_85, type, hoasinduction_lem1_lthm: $o).
% 12.48/2.21 thf(func_def_86, type, lamnotap: $o).
% 12.48/2.21 thf(func_def_87, type, hoasapinj1_gthm: $o).
% 12.48/2.21 thf(func_def_88, type, hoaslamnotvar: $o).
% 12.48/2.21 thf(func_def_89, type, axidl: $o).
% 12.48/2.21 thf(func_def_90, type, hoaslaminj_gthm: $o).
% 12.48/2.21 thf(func_def_91, type, induction2_lthm: $o).
% 12.48/2.21 thf(func_def_92, type, hoasinduction_lem0_lthm: $o).
% 12.48/2.21 thf(func_def_93, type, substmonoid_lthm: $o).
% 12.48/2.21 thf(func_def_94, type, pushprop: $o).
% 12.48/2.21 thf(func_def_95, type, hoasinduction_lem3_gthm: $o).
% 12.48/2.21 thf(func_def_96, type, hoasinduction_lem2_gthm: $o).
% 12.48/2.21 thf(func_def_97, type, hoasinduction_lem3b: $o).
% 12.48/2.21 thf(func_def_98, type, substmonoid: $o).
% 12.48/2.21 thf(func_def_99, type, lamnotvar: $o).
% 12.48/2.21 thf(func_def_100, type, hoasinduction_lem3a: $o).
% 12.48/2.21 thf(func_def_101, type, hoasinduction_lem1_gthm: $o).
% 12.48/2.21 thf(func_def_102, type, hoasinduction_no_psi_cond: $o).
% 12.48/2.21 thf(func_def_103, type, induction2_gthm: $o).
% 12.48/2.21 thf(func_def_104, type, pushprop_lem2v2_lthm: $o).
% 12.48/2.21 thf(func_def_105, type, hoasvar: (subst > term > subst > $o)).
% 12.48/2.21 thf(func_def_106, type, hoaslamnotap: $o).
% 12.48/2.21 thf(func_def_107, type, substmonoid_gthm: $o).
% 12.48/2.21 thf(func_def_108, type, ulamvarsh: $o).
% 12.48/2.21 thf(func_def_109, type, induction2: $o).
% 12.48/2.21 thf(func_def_110, type, pushprop_lem3v2: $o).
% 12.48/2.21 thf(func_def_111, type, pushprop_lem2v2_gthm: $o).
% 12.48/2.21 thf(func_def_112, type, pushprop_lem1_lthm: $o).
% 12.48/2.21 thf(func_def_113, type, hoasinduction_lem3v2: $o).
% 12.48/2.21 thf(func_def_114, type, axshiftcons: $o).
% 12.48/2.21 thf(func_def_115, type, termmset: $o).
% 12.48/2.21 thf(func_def_116, type, pushprop_lem0_lthm: $o).
% 12.48/2.21 thf(func_def_117, type, hoasapnotvar_lthm: $o).
% 12.48/2.21 thf(func_def_118, type, hoasinduction_lem3v2_lthm: $o).
% 12.48/2.21 thf(func_def_119, type, pushprop_p_and_p_prime: (term > subst > (term > $o) > (term > $o) > $o)).
% 12.48/2.21 thf(func_def_120, type, axvarid: $o).
% 12.48/2.21 thf(func_def_121, type, hoasinduction_lthm_3: $o).
% 12.48/2.21 thf(func_def_125, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 12.48/2.21 thf(func_def_126, type, vIFF: ($o > $o > $o)).
% 12.48/2.21 thf(func_def_127, type, db2: !>[X0: $tType]:(X0)).
% 12.48/2.21 thf(func_def_128, type, db0: !>[X0: $tType]:(X0)).
% 12.48/2.21 thf(func_def_129, type, db1: !>[X0: $tType]:(X0)).
% 12.48/2.21 thf(func_def_130, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 12.48/2.21 thf(func_def_131, type, db4: !>[X0: $tType]:(X0)).
% 12.48/2.21 thf(func_def_132, type, db3: !>[X0: $tType]:(X0)).
% 12.48/2.21 thf(func_def_133, type, sP0: ((subst > term > subst > $o) > $o)).
% 12.48/2.21 thf(func_def_134, type, sP1: $o).
% 12.48/2.21 thf(func_def_135, type, sP2: $o).
% 12.48/2.21 thf(func_def_136, type, sP3: ((term > $o) > $o)).
% 12.48/2.21 thf(func_def_137, type, sP4: ((term > $o) > $o)).
% 12.48/2.21 thf(func_def_138, type, sP5: $o).
% 12.48/2.21 thf(func_def_139, type, sP6: ((term > $o) > $o)).
% 12.48/2.21 thf(func_def_140, type, sP7: $o).
% 12.48/2.21 thf(func_def_141, type, sP8: ((subst > term > subst > $o) > $o)).
% 12.48/2.21 thf(func_def_142, type, sP9: ((subst > term > subst > $o) > $o)).
% 12.48/2.21 thf(func_def_143, type, sP10: $o).
% 12.48/2.21 thf(func_def_144, type, sK11: term).
% 12.48/2.21 thf(func_def_145, type, sK12: term).
% 12.48/2.21 thf(func_def_146, type, sK13: (subst > term > term)).
% 12.48/2.21 thf(func_def_147, type, sK14: (subst > term > term)).
% 12.48/2.21 thf(func_def_148, type, sK15: term).
% 12.48/2.21 thf(func_def_149, type, sK16: subst).
% 12.48/2.21 thf(func_def_150, type, sK17: ((subst > term > term) > subst)).
% 12.48/2.21 thf(func_def_151, type, sK18: ((subst > term > term) > subst)).
% 12.48/2.21 thf(func_def_152, type, sK19: ((subst > term > term) > term)).
% 12.48/2.21 thf(func_def_153, type, sK20: ((subst > term > term) > term)).
% 12.48/2.21 thf(func_def_154, type, sK21: ((subst > term > term) > subst)).
% 12.48/2.21 thf(func_def_155, type, sK22: ((subst > term > term) > subst)).
% 12.48/2.21 thf(func_def_156, type, sK23: term).
% 12.48/2.21 thf(func_def_157, type, sK24: term).
% 12.48/2.21 thf(func_def_158, type, sK25: ((term > $o) > term)).
% 12.48/2.21 thf(func_def_159, type, sK26: (term > $o)).
% 12.48/2.21 thf(func_def_160, type, sK27: term).
% 12.48/2.21 thf(func_def_161, type, sK28: (subst > term > subst > $o)).
% 12.48/2.21 thf(func_def_162, type, sK29: term).
% 12.48/2.21 thf(func_def_163, type, sK30: term).
% 12.48/2.21 thf(func_def_164, type, sK31: ((subst > term > subst > $o) > subst)).
% 12.48/2.21 thf(func_def_165, type, sK32: ((subst > term > subst > $o) > subst)).
% 12.48/2.21 thf(func_def_166, type, sK33: ((subst > term > subst > $o) > subst)).
% 12.48/2.21 thf(func_def_167, type, sK34: ((subst > term > subst > $o) > term)).
% 12.48/2.21 thf(func_def_168, type, sK35: ((subst > term > subst > $o) > subst)).
% 12.48/2.21 thf(func_def_169, type, sK36: ((subst > term > subst > $o) > term)).
% 12.48/2.21 thf(func_def_170, type, sK37: ((subst > term > subst > $o) > subst)).
% 12.48/2.21 thf(func_def_171, type, sK38: ((subst > term > subst > $o) > subst)).
% 12.48/2.21 thf(func_def_172, type, sK39: ((subst > term > subst > $o) > term)).
% 12.48/2.21 thf(func_def_173, type, sK40: ((subst > term > subst > $o) > term)).
% 12.48/2.21 thf(func_def_174, type, sK41: term).
% 12.48/2.21 thf(func_def_175, type, sK42: term).
% 12.48/2.21 thf(func_def_176, type, sK43: ((subst > term > term) > term)).
% 12.48/2.21 thf(func_def_177, type, sK44: ((subst > term > term) > subst)).
% 12.48/2.21 thf(func_def_178, type, sK45: ((subst > term > term) > subst)).
% 12.48/2.21 thf(func_def_179, type, sK46: (subst > term > term)).
% 12.48/2.21 thf(func_def_180, type, sK47: term).
% 12.48/2.21 thf(func_def_181, type, sK48: term).
% 12.48/2.21 thf(func_def_182, type, sK49: (subst > term > term)).
% 12.48/2.21 thf(func_def_183, type, sK50: ((subst > term > term) > term)).
% 12.48/2.21 thf(func_def_184, type, sK51: ((subst > term > term) > subst)).
% 12.48/2.21 thf(func_def_185, type, sK52: ((subst > term > term) > subst)).
% 12.48/2.21 thf(func_def_186, type, sK53: subst).
% 12.48/2.21 thf(func_def_187, type, sK54: subst).
% 12.48/2.21 thf(func_def_188, type, sK55: subst).
% 12.48/2.21 thf(func_def_189, type, sK56: subst).
% 12.48/2.21 thf(func_def_190, type, sK57: subst).
% 12.48/2.21 thf(func_def_191, type, sK58: (subst > term > subst > $o)).
% 12.48/2.21 thf(func_def_192, type, sK59: term).
% 12.48/2.21 thf(func_def_193, type, sK60: ((subst > term > subst > $o) > subst)).
% 12.48/2.21 thf(func_def_194, type, sK61: ((subst > term > subst > $o) > term)).
% 12.48/2.21 thf(func_def_195, type, sK62: ((subst > term > subst > $o) > subst)).
% 12.48/2.21 thf(func_def_196, type, sK63: ((subst > term > subst > $o) > subst)).
% 12.48/2.21 thf(func_def_197, type, sK64: ((subst > term > subst > $o) > subst)).
% 12.48/2.21 thf(func_def_198, type, sK65: ((subst > term > subst > $o) > subst)).
% 12.48/2.21 thf(func_def_199, type, sK66: ((subst > term > subst > $o) > subst)).
% 12.48/2.21 thf(func_def_200, type, sK67: ((subst > term > subst > $o) > term)).
% 12.48/2.21 thf(func_def_201, type, sK68: ((subst > term > subst > $o) > term)).
% 12.48/2.21 thf(func_def_202, type, sK69: subst).
% 12.48/2.21 thf(func_def_203, type, sK70: subst).
% 12.48/2.21 thf(func_def_204, type, sK71: subst).
% 12.48/2.21 thf(func_def_205, type, sK72: term).
% 12.48/2.21 thf(func_def_206, type, sK73: term).
% 12.48/2.21 thf(func_def_207, type, sK74: term).
% 12.48/2.21 thf(func_def_208, type, sK75: subst).
% 12.48/2.21 thf(func_def_209, type, sK76: term).
% 12.48/2.21 thf(func_def_210, type, sK77: ((term > $o) > term)).
% 12.48/2.21 thf(func_def_211, type, sK78: ((term > $o) > term)).
% 12.48/2.21 thf(func_def_212, type, sK79: (term > $o)).
% 12.48/2.21 thf(func_def_213, type, sK80: term).
% 12.48/2.21 thf(func_def_214, type, sK81: ((term > $o) > term)).
% 12.48/2.21 thf(func_def_215, type, sK82: ((term > $o) > term)).
% 12.48/2.21 thf(func_def_216, type, sK83: (term > $o)).
% 12.48/2.21 thf(func_def_217, type, sK84: (term > term)).
% 12.48/2.21 thf(func_def_218, type, sK85: term).
% 12.48/2.21 thf(func_def_219, type, sK86: ((term > $o) > term)).
% 12.48/2.21 thf(func_def_220, type, sK87: ((term > $o) > term)).
% 12.48/2.21 thf(func_def_221, type, sK88: ((term > $o) > term)).
% 12.48/2.21 thf(func_def_222, type, sK89: ((term > $o) > term)).
% 12.48/2.21 thf(func_def_223, type, sK90: term).
% 12.48/2.21 thf(func_def_224, type, sK91: term).
% 12.48/2.21 thf(func_def_225, type, sK92: term).
% 12.48/2.21 thf(func_def_226, type, sK93: term).
% 12.48/2.21 thf(func_def_227, type, sK94: term).
% 12.48/2.21 thf(func_def_228, type, sK95: subst).
% 12.48/2.21 thf(func_def_229, type, sK96: subst).
% 12.48/2.21 thf(func_def_230, type, sK97: term).
% 12.48/2.21 thf(func_def_231, type, sK98: term).
% 12.48/2.21 thf(func_def_232, type, sK99: subst).
% 12.48/2.21 thf(func_def_233, type, sK100: subst).
% 12.48/2.21 thf(func_def_234, type, sK101: term).
% 12.48/2.21 thf(func_def_235, type, sK102: term).
% 12.48/2.21 thf(func_def_236, type, sK103: term).
% 12.48/2.21 thf(func_def_237, type, sK104: term).
% 12.48/2.21 thf(func_def_238, type, sK105: term).
% 12.48/2.21 thf(func_def_239, type, sK106: term).
% 12.48/2.21 thf(func_def_240, type, sK107: term).
% 12.48/2.21 thf(func_def_241, type, sK108: term).
% 12.48/2.21 thf(func_def_242, type, sK109: term).
% 12.48/2.21 thf(func_def_243, type, sK110: term).
% 12.48/2.21 thf(func_def_244, type, sK111: subst).
% 12.48/2.21 thf(func_def_245, type, sK112: term).
% 12.48/2.21 thf(func_def_246, type, sK113: subst).
% 12.48/2.21 thf(func_def_247, type, sK114: term).
% 12.48/2.21 thf(func_def_248, type, sK115: subst).
% 12.48/2.21 thf(func_def_249, type, sK116: (term > $o)).
% 12.48/2.21 thf(func_def_250, type, sK117: (term > term)).
% 12.48/2.21 thf(func_def_251, type, sK118: subst).
% 12.48/2.21 thf(func_def_252, type, sK119: term).
% 12.48/2.21 thf(func_def_253, type, sK120: ((term > $o) > term)).
% 12.48/2.21 thf(func_def_254, type, sK121: (subst > (term > $o) > term)).
% 12.48/2.21 thf(func_def_255, type, sK122: ((term > $o) > term)).
% 12.48/2.21 thf(func_def_256, type, sK123: ((term > $o) > term)).
% 12.48/2.21 thf(func_def_257, type, sK124: subst).
% 12.48/2.21 thf(func_def_258, type, sK125: subst).
% 12.48/2.21 thf(func_def_259, type, sK126: term).
% 12.48/2.21 thf(func_def_260, type, sK127: (subst > term > subst > $o)).
% 12.48/2.21 thf(func_def_261, type, sK128: term).
% 12.48/2.21 thf(func_def_262, type, sK129: ((subst > term > subst > $o) > subst)).
% 12.48/2.21 thf(func_def_263, type, sK130: ((subst > term > subst > $o) > term)).
% 12.48/2.21 thf(func_def_264, type, sK131: ((subst > term > subst > $o) > subst)).
% 12.48/2.21 thf(func_def_265, type, sK132: ((subst > term > subst > $o) > subst)).
% 12.48/2.21 thf(func_def_266, type, sK133: ((subst > term > subst > $o) > term)).
% 12.48/2.21 thf(func_def_267, type, sK134: ((subst > term > subst > $o) > subst)).
% 12.48/2.21 thf(func_def_268, type, sK135: ((subst > term > subst > $o) > subst)).
% 12.48/2.21 thf(func_def_269, type, sK136: ((subst > term > subst > $o) > term)).
% 12.48/2.21 thf(func_def_270, type, sK137: ((subst > term > subst > $o) > subst)).
% 12.48/2.21 thf(func_def_271, type, sK138: ((subst > term > term) > subst)).
% 12.48/2.21 thf(func_def_272, type, sK139: ((subst > term > term) > subst)).
% 12.48/2.21 thf(func_def_273, type, sK140: ((subst > term > term) > term)).
% 12.48/2.21 thf(func_def_274, type, sK141: ((subst > term > term) > (subst > term > subst > $o) > term)).
% 12.48/2.21 thf(func_def_275, type, sK142: ((subst > term > subst > $o) > subst > term > term)).
% 12.48/2.21 thf(func_def_276, type, sK143: ((subst > term > subst > $o) > term)).
% 12.48/2.21 thf(func_def_277, type, sK144: ((subst > term > subst > $o) > term)).
% 12.48/2.21 thf(func_def_278, type, sK145: term).
% 12.48/2.21 thf(func_def_279, type, sK146: term).
% 12.48/2.21 thf(func_def_280, type, sK147: term).
% 12.48/2.21 thf(func_def_281, type, sK148: term).
% 12.48/2.21 thf(func_def_282, type, sK149: term).
% 12.48/2.21 thf(func_def_283, type, sK150: term).
% 12.48/2.21 thf(func_def_284, type, sK151: subst).
% 12.48/2.21 thf(func_def_285, type, sK152: term).
% 12.48/2.21 thf(func_def_286, type, sK153: term).
% 12.48/2.21 thf(func_def_287, type, sK154: subst).
% 12.48/2.21 thf(func_def_288, type, sK155: subst).
% 12.48/2.21 thf(func_def_289, type, sK156: term).
% 12.48/2.21 thf(func_def_290, type, sK157: term).
% 12.48/2.21 thf(func_def_291, type, sK158: (term > $o)).
% 12.48/2.21 thf(func_def_292, type, sK159: subst).
% 12.48/2.21 thf(func_def_293, type, sK160: term).
% 12.48/2.21 thf(func_def_294, type, sK161: (subst > (term > $o) > term)).
% 12.48/2.21 thf(f3,axiom,(
% 12.48/2.21 (! [X0 : term] : (((sub @ X0 @ id)) = X0) = axvarid)),
% 12.48/2.21 file('/export/starexec/sandbox/benchmark/Axioms/ALG003^0.ax',axvarid)).
% 12.48/2.21 thf(f43,axiom,(
% 12.48/2.21 (! [X0 : (term > $o)] : (! [X1 : term,X2 : term] : ((X0 @ X1) => ((X0 @ X2) => (X0 @ (ap @ X1 @ X2)))) => (! [X1 : term] : (! [X2 : term] : ((X0 @ X2) => (X0 @ (sub @ X1 @ (push @ X2 @ id)))) => (X0 @ (lam @ X1))) => ! [X1 : term,X3 : subst] : (! [X2 : term] : ((var @ X2) => (X0 @ (sub @ X2 @ X3))) => (X0 @ (sub @ X1 @ X3))))) = induction2lem)),
% 12.48/2.21 file('/export/starexec/sandbox/benchmark/Axioms/ALG003^0.ax',induction2lem)).
% 12.48/2.21 thf(f46,axiom,(
% 12.48/2.21 (! [X0 : (term > $o)] : (! [X1 : term] : ((var @ X1) => (X0 @ X1)) => (! [X2 : term,X1 : term] : ((X0 @ X1) => ((X0 @ X2) => (X0 @ (ap @ X1 @ X2)))) => (! [X1 : term] : (! [X2 : term] : ((X0 @ X2) => (X0 @ (sub @ X1 @ (push @ X2 @ id)))) => (X0 @ (lam @ X1))) => ! [X1 : term] : (X0 @ X1)))) = induction2)),
% 12.48/2.21 file('/export/starexec/sandbox/benchmark/Axioms/ALG003^0.ax',induction2)).
% 12.48/2.21 thf(f47,axiom,(
% 12.48/2.21 (induction2_gthm = axapp => (axvarcons => (axvarid => (axabs => (axclos => (axidl => (axshiftcons => (axassoc => (axmap => (axidr => (axvarshift => (axscons => (ulamvar1 => (ulamvarsh => (ulamvarind => (apinj1 => (apinj2 => (laminj => (shinj => (lamnotap => (apnotvar => (lamnotvar => (induction => (pushprop => (induction2lem => induction2)))))))))))))))))))))))))),
% 12.48/2.21 file('/export/starexec/sandbox/benchmark/Axioms/ALG003^0.ax',induction2_gthm)).
% 12.48/2.21 thf(f114,conjecture,(
% 12.48/2.21 induction2_gthm),
% 12.48/2.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm)).
% 12.48/2.21 thf(f115,negated_conjecture,(
% 12.48/2.21 ~induction2_gthm),
% 12.48/2.21 inference(negated_conjecture,[status(cth)],[f114])).
% 12.48/2.21 thf(f116,plain,(
% 12.48/2.21 ! [X0 : term] : (((sub @ X0 @ id)) = X0) <=> (axvarid = $true)),
% 12.48/2.21 inference(fool_elimination,[],[f3])).
% 12.48/2.21 thf(f141,plain,(
% 12.48/2.21 ~induction2_gthm),
% 12.48/2.21 inference(rectify,[],[f115])).
% 12.48/2.21 thf(f142,plain,(
% 12.48/2.21 ~ (induction2_gthm = $true)),
% 12.48/2.21 inference(fool_elimination,[],[f141])).
% 12.48/2.21 thf(f158,plain,(
% 12.48/2.21 (induction2_gthm = axapp => (axvarcons => (axvarid => (axabs => (axclos => (axidl => (axshiftcons => (axassoc => (axmap => (axidr => (axvarshift => (axscons => (ulamvar1 => (ulamvarsh => (ulamvarind => (apinj1 => (apinj2 => (laminj => (shinj => (lamnotap => (apnotvar => (lamnotvar => (induction => (pushprop => (induction2lem => induction2)))))))))))))))))))))))))),
% 12.48/2.22 inference(rectify,[],[f47])).
% 12.48/2.22 thf(f159,plain,(
% 12.48/2.22 (induction2_gthm = $true) <=> ((axapp = $true) => ((axvarcons = $true) => ((axvarid = $true) => ((axabs = $true) => ((axclos = $true) => ((axidl = $true) => ((axshiftcons = $true) => ((axassoc = $true) => ((axmap = $true) => ((axidr = $true) => ((axvarshift = $true) => ((axscons = $true) => ((ulamvar1 = $true) => ((ulamvarsh = $true) => ((ulamvarind = $true) => ((apinj1 = $true) => ((apinj2 = $true) => ((laminj = $true) => ((shinj = $true) => ((lamnotap = $true) => ((apnotvar = $true) => ((lamnotvar = $true) => ((induction = $true) => ((pushprop = $true) => ((induction2lem = $true) => (induction2 = $true))))))))))))))))))))))))))),
% 12.48/2.22 inference(fool_elimination,[],[f158])).
% 12.48/2.22 thf(f182,plain,(
% 12.48/2.22 (! [X0 : (term > $o)] : (! [X1 : term,X2 : term] : ((X0 @ X1) => ((X0 @ X2) => (X0 @ (ap @ X1 @ X2)))) => (! [X3 : term] : (! [X4 : term] : ((X0 @ X4) => (X0 @ (sub @ X3 @ (push @ X4 @ id)))) => (X0 @ (lam @ X3))) => ! [X5 : term,X6 : subst] : (! [X7 : term] : ((var @ X7) => (X0 @ (sub @ X7 @ X6))) => (X0 @ (sub @ X5 @ X6))))) = induction2lem)),
% 12.48/2.22 inference(rectify,[],[f43])).
% 12.48/2.22 thf(f183,plain,(
% 12.48/2.22 (induction2lem = $true) <=> ! [X0 : (term > $o)] : (! [X1 : term,X2 : term] : ((((X0 @ X1)) = $true) => ((((X0 @ X2)) = $true) => (((X0 @ (ap @ X1 @ X2))) = $true))) => (! [X3 : term] : (! [X4 : term] : ((((X0 @ X4)) = $true) => ($true = ((X0 @ (sub @ X3 @ (push @ X4 @ id)))))) => (((X0 @ (lam @ X3))) = $true)) => ! [X5 : term,X6 : subst] : (! [X7 : term] : (($true = ((var @ X7))) => ($true = ((X0 @ (sub @ X7 @ X6))))) => ($true = ((X0 @ (sub @ X5 @ X6)))))))),
% 12.48/2.22 inference(fool_elimination,[],[f182])).
% 12.48/2.22 thf(f184,plain,(
% 12.48/2.22 (! [X0 : (term > $o)] : (! [X1 : term] : ((var @ X1) => (X0 @ X1)) => (! [X2 : term,X3 : term] : ((X0 @ X3) => ((X0 @ X2) => (X0 @ (ap @ X3 @ X2)))) => (! [X4 : term] : (! [X5 : term] : ((X0 @ X5) => (X0 @ (sub @ X4 @ (push @ X5 @ id)))) => (X0 @ (lam @ X4))) => ! [X6 : term] : (X0 @ X6)))) = induction2)),
% 12.48/2.22 inference(rectify,[],[f46])).
% 12.48/2.22 thf(f185,plain,(
% 12.48/2.22 (induction2 = $true) <=> ! [X0 : (term > $o)] : (! [X1 : term] : ((((var @ X1)) = $true) => (((X0 @ X1)) = $true)) => (! [X3 : term,X2 : term] : (($true = ((X0 @ X3))) => ((((X0 @ X2)) = $true) => ($true = ((X0 @ (ap @ X3 @ X2)))))) => (! [X4 : term] : (! [X5 : term] : (($true = ((X0 @ X5))) => ($true = ((X0 @ (sub @ X4 @ (push @ X5 @ id)))))) => ($true = ((X0 @ (lam @ X4))))) => ! [X6 : term] : ($true = ((X0 @ X6))))))),
% 12.48/2.22 inference(fool_elimination,[],[f184])).
% 12.48/2.22 thf(f320,plain,(
% 12.48/2.22 (induction2_gthm != $true)),
% 12.48/2.22 inference(flattening,[],[f142])).
% 12.48/2.22 thf(f327,plain,(
% 12.48/2.22 (induction2lem = $true) <=> ! [X0 : (term > $o)] : ((! [X6 : subst,X5 : term] : (($true = ((X0 @ (sub @ X5 @ X6)))) | ? [X7 : term] : (($true != ((X0 @ (sub @ X7 @ X6)))) & ($true = ((var @ X7))))) | ? [X3 : term] : (! [X4 : term] : (($true = ((X0 @ (sub @ X3 @ (push @ X4 @ id))))) | (((X0 @ X4)) != $true)) & (((X0 @ (lam @ X3))) != $true))) | ? [X1 : term,X2 : term] : (((((X0 @ (ap @ X1 @ X2))) != $true) & (((X0 @ X2)) = $true)) & (((X0 @ X1)) = $true)))),
% 12.48/2.22 inference(ennf_transformation,[],[f183])).
% 12.48/2.22 thf(f328,plain,(
% 12.48/2.22 ! [X0 : (term > $o)] : (? [X1 : term,X2 : term] : ((((X0 @ (ap @ X1 @ X2))) != $true) & (((X0 @ X2)) = $true) & (((X0 @ X1)) = $true)) | ? [X3 : term] : (! [X4 : term] : (($true = ((X0 @ (sub @ X3 @ (push @ X4 @ id))))) | (((X0 @ X4)) != $true)) & (((X0 @ (lam @ X3))) != $true)) | ! [X6 : subst,X5 : term] : (($true = ((X0 @ (sub @ X5 @ X6)))) | ? [X7 : term] : (($true != ((X0 @ (sub @ X7 @ X6)))) & ($true = ((var @ X7)))))) <=> (induction2lem = $true)),
% 12.48/2.22 inference(flattening,[],[f327])).
% 12.48/2.22 thf(f337,plain,(
% 12.48/2.22 (induction2_gthm = $true) <=> ((((((((((((((((((((((((((induction2 = $true) | (induction2lem != $true)) | (pushprop != $true)) | (induction != $true)) | (lamnotvar != $true)) | (apnotvar != $true)) | (lamnotap != $true)) | (shinj != $true)) | (laminj != $true)) | (apinj2 != $true)) | (apinj1 != $true)) | (ulamvarind != $true)) | (ulamvarsh != $true)) | (ulamvar1 != $true)) | (axscons != $true)) | (axvarshift != $true)) | (axidr != $true)) | (axmap != $true)) | (axassoc != $true)) | (axshiftcons != $true)) | (axidl != $true)) | (axclos != $true)) | (axabs != $true)) | (axvarid != $true)) | (axvarcons != $true)) | (axapp != $true))),
% 12.48/2.22 inference(ennf_transformation,[],[f159])).
% 12.48/2.22 thf(f338,plain,(
% 12.48/2.22 ((apinj2 != $true) | (lamnotap != $true) | (laminj != $true) | (axassoc != $true) | (axvarcons != $true) | (axscons != $true) | (axidl != $true) | (induction2 = $true) | (ulamvar1 != $true) | (axmap != $true) | (axapp != $true) | (induction2lem != $true) | (apnotvar != $true) | (axabs != $true) | (axidr != $true) | (induction != $true) | (shinj != $true) | (axclos != $true) | (axvarid != $true) | (pushprop != $true) | (ulamvarind != $true) | (apinj1 != $true) | (ulamvarsh != $true) | (axshiftcons != $true) | (axvarshift != $true) | (lamnotvar != $true)) <=> (induction2_gthm = $true)),
% 12.48/2.22 inference(flattening,[],[f337])).
% 12.48/2.22 thf(f354,plain,(
% 12.48/2.22 (induction2 = $true) <=> ! [X0 : (term > $o)] : (((! [X6 : term] : ($true = ((X0 @ X6))) | ? [X4 : term] : (! [X5 : term] : (($true != ((X0 @ X5))) | ($true = ((X0 @ (sub @ X4 @ (push @ X5 @ id)))))) & ($true != ((X0 @ (lam @ X4)))))) | ? [X3 : term,X2 : term] : ((($true != ((X0 @ (ap @ X3 @ X2)))) & (((X0 @ X2)) = $true)) & ($true = ((X0 @ X3))))) | ? [X1 : term] : ((((X0 @ X1)) != $true) & (((var @ X1)) = $true)))),
% 12.48/2.22 inference(ennf_transformation,[],[f185])).
% 12.48/2.22 thf(f355,plain,(
% 12.48/2.22 (induction2 = $true) <=> ! [X0 : (term > $o)] : (? [X4 : term] : (! [X5 : term] : (($true != ((X0 @ X5))) | ($true = ((X0 @ (sub @ X4 @ (push @ X5 @ id)))))) & ($true != ((X0 @ (lam @ X4))))) | ? [X3 : term,X2 : term] : (($true = ((X0 @ X3))) & (((X0 @ X2)) = $true) & ($true != ((X0 @ (ap @ X3 @ X2))))) | ! [X6 : term] : ($true = ((X0 @ X6))) | ? [X1 : term] : ((((X0 @ X1)) != $true) & (((var @ X1)) = $true)))),
% 12.48/2.22 inference(flattening,[],[f354])).
% 12.48/2.22 thf(f363,definition,(
% 12.48/2.22 ! [X0 : (term > $o)] : (($true = ((sP4 @ X0))) <=> ? [X3 : term,X2 : term] : (($true = ((X0 @ X3))) & (((X0 @ X2)) = $true) & ($true != ((X0 @ (ap @ X3 @ X2))))))),
% 12.48/2.22 introduced(definition,[new_symbols(definition,[=])],[predicate_definition_introduction])).
% 12.48/2.22 thf(f364,definition,(
% 12.48/2.22 ($true = sP5) <=> ! [X0 : (term > $o)] : (? [X4 : term] : (! [X5 : term] : (($true != ((X0 @ X5))) | ($true = ((X0 @ (sub @ X4 @ (push @ X5 @ id)))))) & ($true != ((X0 @ (lam @ X4))))) | ($true = ((sP4 @ X0))) | ! [X6 : term] : ($true = ((X0 @ X6))) | ? [X1 : term] : ((((X0 @ X1)) != $true) & (((var @ X1)) = $true)))),
% 12.48/2.22 introduced(definition,[new_symbols(definition,[=])],[predicate_definition_introduction])).
% 12.48/2.22 thf(f365,plain,(
% 12.48/2.22 (induction2 = $true) <=> ($true = sP5)),
% 12.48/2.22 inference(definition_folding,[],[f355,f364,f363])).
% 12.48/2.22 thf(f366,definition,(
% 12.48/2.22 ! [X0 : (term > $o)] : ((((sP6 @ X0)) = $true) <=> ? [X1 : term,X2 : term] : ((((X0 @ (ap @ X1 @ X2))) != $true) & (((X0 @ X2)) = $true) & (((X0 @ X1)) = $true)))),
% 12.48/2.22 introduced(definition,[new_symbols(definition,[=])],[predicate_definition_introduction])).
% 12.48/2.22 thf(f367,definition,(
% 12.48/2.22 ($true = sP7) <=> ! [X0 : (term > $o)] : ((((sP6 @ X0)) = $true) | ? [X3 : term] : (! [X4 : term] : (($true = ((X0 @ (sub @ X3 @ (push @ X4 @ id))))) | (((X0 @ X4)) != $true)) & (((X0 @ (lam @ X3))) != $true)) | ! [X6 : subst,X5 : term] : (($true = ((X0 @ (sub @ X5 @ X6)))) | ? [X7 : term] : (($true != ((X0 @ (sub @ X7 @ X6)))) & ($true = ((var @ X7))))))),
% 12.48/2.22 introduced(definition,[new_symbols(definition,[=])],[predicate_definition_introduction])).
% 12.48/2.22 thf(f368,plain,(
% 12.48/2.22 ($true = sP7) <=> (induction2lem = $true)),
% 12.48/2.22 inference(definition_folding,[],[f328,f367,f366])).
% 12.48/2.22 thf(f395,plain,(
% 12.48/2.22 (((apinj2 != $true) | (lamnotap != $true) | (laminj != $true) | (axassoc != $true) | (axvarcons != $true) | (axscons != $true) | (axidl != $true) | (induction2 = $true) | (ulamvar1 != $true) | (axmap != $true) | (axapp != $true) | (induction2lem != $true) | (apnotvar != $true) | (axabs != $true) | (axidr != $true) | (induction != $true) | (shinj != $true) | (axclos != $true) | (axvarid != $true) | (pushprop != $true) | (ulamvarind != $true) | (apinj1 != $true) | (ulamvarsh != $true) | (axshiftcons != $true) | (axvarshift != $true) | (lamnotvar != $true)) | (induction2_gthm != $true)) & ((induction2_gthm = $true) | ((apinj2 = $true) & (lamnotap = $true) & (laminj = $true) & (axassoc = $true) & (axvarcons = $true) & (axscons = $true) & (axidl = $true) & (induction2 != $true) & (ulamvar1 = $true) & (axmap = $true) & (axapp = $true) & (induction2lem = $true) & (apnotvar = $true) & (axabs = $true) & (axidr = $true) & (induction = $true) & (shinj = $true) & (axclos = $true) & (axvarid = $true) & (pushprop = $true) & (ulamvarind = $true) & (apinj1 = $true) & (ulamvarsh = $true) & (axshiftcons = $true) & (axvarshift = $true) & (lamnotvar = $true)))),
% 12.48/2.22 inference(nnf_transformation,[],[f338])).
% 12.48/2.22 thf(f396,plain,(
% 12.48/2.22 ((apinj2 != $true) | (lamnotap != $true) | (laminj != $true) | (axassoc != $true) | (axvarcons != $true) | (axscons != $true) | (axidl != $true) | (induction2 = $true) | (ulamvar1 != $true) | (axmap != $true) | (axapp != $true) | (induction2lem != $true) | (apnotvar != $true) | (axabs != $true) | (axidr != $true) | (induction != $true) | (shinj != $true) | (axclos != $true) | (axvarid != $true) | (pushprop != $true) | (ulamvarind != $true) | (apinj1 != $true) | (ulamvarsh != $true) | (axshiftcons != $true) | (axvarshift != $true) | (lamnotvar != $true) | (induction2_gthm != $true)) & ((induction2_gthm = $true) | ((apinj2 = $true) & (lamnotap = $true) & (laminj = $true) & (axassoc = $true) & (axvarcons = $true) & (axscons = $true) & (axidl = $true) & (induction2 != $true) & (ulamvar1 = $true) & (axmap = $true) & (axapp = $true) & (induction2lem = $true) & (apnotvar = $true) & (axabs = $true) & (axidr = $true) & (induction = $true) & (shinj = $true) & (axclos = $true) & (axvarid = $true) & (pushprop = $true) & (ulamvarind = $true) & (apinj1 = $true) & (ulamvarsh = $true) & (axshiftcons = $true) & (axvarshift = $true) & (lamnotvar = $true)))),
% 12.48/2.22 inference(flattening,[],[f395])).
% 12.48/2.22 thf(f427,plain,(
% 12.48/2.22 (($true = sP5) | ? [X0 : (term > $o)] : (! [X4 : term] : (? [X5 : term] : (($true = ((X0 @ X5))) & ($true != ((X0 @ (sub @ X4 @ (push @ X5 @ id)))))) | ($true = ((X0 @ (lam @ X4))))) & ($true != ((sP4 @ X0))) & ? [X6 : term] : ($true != ((X0 @ X6))) & ! [X1 : term] : ((((X0 @ X1)) = $true) | (((var @ X1)) != $true)))) & (! [X0 : (term > $o)] : (? [X4 : term] : (! [X5 : term] : (($true != ((X0 @ X5))) | ($true = ((X0 @ (sub @ X4 @ (push @ X5 @ id)))))) & ($true != ((X0 @ (lam @ X4))))) | ($true = ((sP4 @ X0))) | ! [X6 : term] : ($true = ((X0 @ X6))) | ? [X1 : term] : ((((X0 @ X1)) != $true) & (((var @ X1)) = $true))) | ($true != sP5))),
% 12.48/2.22 inference(nnf_transformation,[],[f364])).
% 12.48/2.22 thf(f428,plain,(
% 12.48/2.22 (($true = sP5) | ? [X0 : (term > $o)] : (! [X1 : term] : (? [X2 : term] : ((((X0 @ X2)) = $true) & (((X0 @ (sub @ X1 @ (push @ X2 @ id)))) != $true)) | (((X0 @ (lam @ X1))) = $true)) & ($true != ((sP4 @ X0))) & ? [X3 : term] : ($true != ((X0 @ X3))) & ! [X4 : term] : ((((X0 @ X4)) = $true) | (((var @ X4)) != $true)))) & (! [X5 : (term > $o)] : (? [X6 : term] : (! [X7 : term] : (($true != ((X5 @ X7))) | ($true = ((X5 @ (sub @ X6 @ (push @ X7 @ id)))))) & ($true != ((X5 @ (lam @ X6))))) | ($true = ((sP4 @ X5))) | ! [X8 : term] : ($true = ((X5 @ X8))) | ? [X9 : term] : (($true != ((X5 @ X9))) & ($true = ((var @ X9))))) | ($true != sP5))),
% 12.48/2.22 inference(rectify,[],[f427])).
% 12.48/2.22 thf(f429,plain,(
% 12.48/2.22 (($true = sP5) | (! [X1 : term] : ((($true = ((sK83 @ (sK84 @ X1)))) & ($true != ((sK83 @ (sub @ X1 @ (push @ (sK84 @ X1) @ id)))))) | ($true = ((sK83 @ (lam @ X1))))) & ($true != ((sP4 @ sK83))) & ($true != ((sK83 @ sK85))) & ! [X4 : term] : (($true = ((sK83 @ X4))) | (((var @ X4)) != $true)))) & (! [X5 : (term > $o)] : ((! [X7 : term] : (($true != ((X5 @ X7))) | ($true = ((X5 @ (sub @ (sK86 @ X5) @ (push @ X7 @ id)))))) & ($true != ((X5 @ (lam @ (sK86 @ X5)))))) | ($true = ((sP4 @ X5))) | ! [X8 : term] : ($true = ((X5 @ X8))) | (($true != ((X5 @ (sK87 @ X5)))) & ($true = ((var @ (sK87 @ X5)))))) | ($true != sP5))),
% 12.48/2.22 inference(skolemize,[status(esa),new_symbols(skolem,[sK83,vAPP,sK85,vAPP,vAPP]),skolemize(X0,sK83),skolemize(X17,sK22 @ X14),skolemize(X3,sK85),skolemize(X17,sK22 @ X14),skolemize(X17,sK22 @ X14)],[f428])).
% 12.48/2.22 thf(f430,plain,(
% 12.48/2.22 ! [X0 : (term > $o)] : ((($true = ((sP4 @ X0))) | ! [X3 : term,X2 : term] : (($true != ((X0 @ X3))) | (((X0 @ X2)) != $true) | ($true = ((X0 @ (ap @ X3 @ X2)))))) & (? [X3 : term,X2 : term] : (($true = ((X0 @ X3))) & (((X0 @ X2)) = $true) & ($true != ((X0 @ (ap @ X3 @ X2))))) | ($true != ((sP4 @ X0)))))),
% 12.48/2.22 inference(nnf_transformation,[],[f363])).
% 12.48/2.22 thf(f431,plain,(
% 12.48/2.22 ! [X0 : (term > $o)] : ((($true = ((sP4 @ X0))) | ! [X1 : term,X2 : term] : ((((X0 @ X1)) != $true) | (((X0 @ X2)) != $true) | (((X0 @ (ap @ X1 @ X2))) = $true))) & (? [X3 : term,X4 : term] : (($true = ((X0 @ X3))) & (((X0 @ X4)) = $true) & ($true != ((X0 @ (ap @ X3 @ X4))))) | ($true != ((sP4 @ X0)))))),
% 12.48/2.22 inference(rectify,[],[f430])).
% 12.48/2.22 thf(f432,plain,(
% 12.48/2.22 ! [X0 : (term > $o)] : ((($true = ((sP4 @ X0))) | ! [X1 : term,X2 : term] : ((((X0 @ X1)) != $true) | (((X0 @ X2)) != $true) | (((X0 @ (ap @ X1 @ X2))) = $true))) & ((($true = ((X0 @ (sK88 @ X0)))) & ($true = ((X0 @ (sK89 @ X0)))) & ($true != ((X0 @ (ap @ (sK88 @ X0) @ (sK89 @ X0)))))) | ($true != ((sP4 @ X0)))))),
% 12.48/2.22 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP,vAPP]),skolemize(X17,sK22 @ X14),skolemize(X17,sK22 @ X14)],[f431])).
% 12.48/2.22 thf(f433,plain,(
% 12.48/2.22 ((induction2 = $true) | ($true != sP5)) & (($true = sP5) | (induction2 != $true))),
% 12.48/2.22 inference(nnf_transformation,[],[f365])).
% 12.48/2.22 thf(f437,plain,(
% 12.48/2.22 (! [X0 : term] : (((sub @ X0 @ id)) = X0) | (axvarid != $true)) & ((axvarid = $true) | ? [X0 : term] : (((sub @ X0 @ id)) != X0))),
% 12.48/2.22 inference(nnf_transformation,[],[f116])).
% 12.48/2.22 thf(f438,plain,(
% 12.48/2.22 (! [X0 : term] : (((sub @ X0 @ id)) = X0) | (axvarid != $true)) & ((axvarid = $true) | ? [X1 : term] : (((sub @ X1 @ id)) != X1))),
% 12.48/2.22 inference(rectify,[],[f437])).
% 12.48/2.22 thf(f439,plain,(
% 12.48/2.22 (! [X0 : term] : (((sub @ X0 @ id)) = X0) | (axvarid != $true)) & ((axvarid = $true) | (((sub @ sK94 @ id)) != sK94))),
% 12.48/2.22 inference(skolemize,[status(esa),new_symbols(skolem,[sK94]),skolemize(X1,sK94)],[f438])).
% 12.48/2.22 thf(f468,plain,(
% 12.48/2.22 (($true = sP7) | ? [X0 : (term > $o)] : ((((sP6 @ X0)) != $true) & ! [X3 : term] : (? [X4 : term] : (($true != ((X0 @ (sub @ X3 @ (push @ X4 @ id))))) & (((X0 @ X4)) = $true)) | (((X0 @ (lam @ X3))) = $true)) & ? [X6 : subst,X5 : term] : (($true != ((X0 @ (sub @ X5 @ X6)))) & ! [X7 : term] : (($true = ((X0 @ (sub @ X7 @ X6)))) | ($true != ((var @ X7))))))) & (! [X0 : (term > $o)] : ((((sP6 @ X0)) = $true) | ? [X3 : term] : (! [X4 : term] : (($true = ((X0 @ (sub @ X3 @ (push @ X4 @ id))))) | (((X0 @ X4)) != $true)) & (((X0 @ (lam @ X3))) != $true)) | ! [X6 : subst,X5 : term] : (($true = ((X0 @ (sub @ X5 @ X6)))) | ? [X7 : term] : (($true != ((X0 @ (sub @ X7 @ X6)))) & ($true = ((var @ X7)))))) | ($true != sP7))),
% 12.48/2.22 inference(nnf_transformation,[],[f367])).
% 12.48/2.22 thf(f469,plain,(
% 12.48/2.22 (($true = sP7) | ? [X0 : (term > $o)] : ((((sP6 @ X0)) != $true) & ! [X1 : term] : (? [X2 : term] : ((((X0 @ (sub @ X1 @ (push @ X2 @ id)))) != $true) & (((X0 @ X2)) = $true)) | (((X0 @ (lam @ X1))) = $true)) & ? [X3 : subst,X4 : term] : ((((X0 @ (sub @ X4 @ X3))) != $true) & ! [X5 : term] : (($true = ((X0 @ (sub @ X5 @ X3)))) | (((var @ X5)) != $true))))) & (! [X6 : (term > $o)] : (($true = ((sP6 @ X6))) | ? [X7 : term] : (! [X8 : term] : (($true = ((X6 @ (sub @ X7 @ (push @ X8 @ id))))) | ($true != ((X6 @ X8)))) & ($true != ((X6 @ (lam @ X7))))) | ! [X9 : subst,X10 : term] : (($true = ((X6 @ (sub @ X10 @ X9)))) | ? [X11 : term] : (($true != ((X6 @ (sub @ X11 @ X9)))) & (((var @ X11)) = $true)))) | ($true != sP7))),
% 12.48/2.22 inference(rectify,[],[f468])).
% 12.48/2.22 thf(f470,plain,(
% 12.48/2.22 (($true = sP7) | (($true != ((sP6 @ sK116))) & ! [X1 : term] : ((($true != ((sK116 @ (sub @ X1 @ (push @ (sK117 @ X1) @ id))))) & ($true = ((sK116 @ (sK117 @ X1))))) | (((sK116 @ (lam @ X1))) = $true)) & (($true != ((sK116 @ (sub @ sK119 @ sK118)))) & ! [X5 : term] : ((((sK116 @ (sub @ X5 @ sK118))) = $true) | (((var @ X5)) != $true))))) & (! [X6 : (term > $o)] : (($true = ((sP6 @ X6))) | (! [X8 : term] : ((((X6 @ (sub @ (sK120 @ X6) @ (push @ X8 @ id)))) = $true) | ($true != ((X6 @ X8)))) & (((X6 @ (lam @ (sK120 @ X6)))) != $true)) | ! [X9 : subst,X10 : term] : (($true = ((X6 @ (sub @ X10 @ X9)))) | (($true != ((X6 @ (sub @ (sK121 @ X9 @ X6) @ X9)))) & ($true = ((var @ (sK121 @ X9 @ X6))))))) | ($true != sP7))),
% 12.48/2.22 inference(skolemize,[status(esa),new_symbols(skolem,[sK116,vAPP,sK118,sK119,vAPP,vAPP]),skolemize(X0,sK116),skolemize(X17,sK22 @ X14),skolemize(X3,sK118),skolemize(X4,sK119),skolemize(X17,sK22 @ X14),skolemize(X17,sK22 @ X14)],[f469])).
% 12.48/2.22 thf(f471,plain,(
% 12.48/2.22 ! [X0 : (term > $o)] : (((((sP6 @ X0)) = $true) | ! [X1 : term,X2 : term] : ((((X0 @ (ap @ X1 @ X2))) = $true) | (((X0 @ X2)) != $true) | (((X0 @ X1)) != $true))) & (? [X1 : term,X2 : term] : ((((X0 @ (ap @ X1 @ X2))) != $true) & (((X0 @ X2)) = $true) & (((X0 @ X1)) = $true)) | (((sP6 @ X0)) != $true)))),
% 12.48/2.22 inference(nnf_transformation,[],[f366])).
% 12.48/2.22 thf(f472,plain,(
% 12.48/2.22 ! [X0 : (term > $o)] : (((((sP6 @ X0)) = $true) | ! [X1 : term,X2 : term] : ((((X0 @ (ap @ X1 @ X2))) = $true) | (((X0 @ X2)) != $true) | (((X0 @ X1)) != $true))) & (? [X3 : term,X4 : term] : (($true != ((X0 @ (ap @ X3 @ X4)))) & (((X0 @ X4)) = $true) & ($true = ((X0 @ X3)))) | (((sP6 @ X0)) != $true)))),
% 12.48/2.22 inference(rectify,[],[f471])).
% 12.48/2.22 thf(f473,plain,(
% 12.48/2.22 ! [X0 : (term > $o)] : (((((sP6 @ X0)) = $true) | ! [X1 : term,X2 : term] : ((((X0 @ (ap @ X1 @ X2))) = $true) | (((X0 @ X2)) != $true) | (((X0 @ X1)) != $true))) & ((($true != ((X0 @ (ap @ (sK122 @ X0) @ (sK123 @ X0))))) & ($true = ((X0 @ (sK123 @ X0)))) & ($true = ((X0 @ (sK122 @ X0))))) | (((sP6 @ X0)) != $true)))),
% 12.48/2.22 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP,vAPP]),skolemize(X17,sK22 @ X14),skolemize(X17,sK22 @ X14)],[f472])).
% 12.48/2.22 thf(f474,plain,(
% 12.48/2.22 (($true = sP7) | (induction2lem != $true)) & ((induction2lem = $true) | ($true != sP7))),
% 12.48/2.22 inference(nnf_transformation,[],[f368])).
% 12.48/2.22 thf(f550,plain,(
% 12.48/2.22 (induction2_gthm = $true) | (axvarid = $true)),
% 12.48/2.22 inference(cnf_transformation,[],[f396])).
% 12.48/2.22 thf(f557,plain,(
% 12.48/2.22 (induction2_gthm = $true) | (induction2lem = $true)),
% 12.48/2.22 inference(cnf_transformation,[],[f396])).
% 12.48/2.22 thf(f561,plain,(
% 12.48/2.22 (induction2_gthm = $true) | (induction2 != $true)),
% 12.48/2.22 inference(cnf_transformation,[],[f396])).
% 12.48/2.22 thf(f619,plain,(
% 12.48/2.22 ( ! [X4 : term] : (($true = ((sK83 @ X4))) | ($true = sP5) | (((var @ X4)) != $true)) )),
% 12.48/2.22 inference(cnf_transformation,[],[f429])).
% 12.48/2.22 thf(f620,plain,(
% 12.48/2.22 ($true != ((sK83 @ sK85))) | ($true = sP5)),
% 12.48/2.22 inference(cnf_transformation,[],[f429])).
% 12.48/2.22 thf(f621,plain,(
% 12.48/2.22 ($true != ((sP4 @ sK83))) | ($true = sP5)),
% 12.48/2.22 inference(cnf_transformation,[],[f429])).
% 12.48/2.22 thf(f622,plain,(
% 12.48/2.22 ( ! [X1 : term] : (($true = ((sK83 @ (lam @ X1)))) | ($true != ((sK83 @ (sub @ X1 @ (push @ (sK84 @ X1) @ id))))) | ($true = sP5)) )),
% 12.48/2.22 inference(cnf_transformation,[],[f429])).
% 12.48/2.22 thf(f623,plain,(
% 12.48/2.22 ( ! [X1 : term] : (($true = ((sK83 @ (sK84 @ X1)))) | ($true = ((sK83 @ (lam @ X1)))) | ($true = sP5)) )),
% 12.48/2.22 inference(cnf_transformation,[],[f429])).
% 12.48/2.22 thf(f627,plain,(
% 12.48/2.22 ( ! [X2 : term,X0 : (term > $o),X1 : term] : ((((X0 @ (ap @ X1 @ X2))) = $true) | (((X0 @ X1)) != $true) | (((X0 @ X2)) != $true) | ($true = ((sP4 @ X0)))) )),
% 12.48/2.22 inference(cnf_transformation,[],[f432])).
% 12.48/2.22 thf(f629,plain,(
% 12.48/2.22 ($true != sP5) | (induction2 = $true)),
% 12.48/2.22 inference(cnf_transformation,[],[f433])).
% 12.48/2.22 thf(f634,plain,(
% 12.48/2.22 ( ! [X0 : term] : ((axvarid != $true) | (((sub @ X0 @ id)) = X0)) )),
% 12.48/2.22 inference(cnf_transformation,[],[f439])).
% 12.48/2.22 thf(f658,plain,(
% 12.48/2.22 ( ! [X10 : term,X6 : (term > $o),X9 : subst] : ((((X6 @ (lam @ (sK120 @ X6)))) != $true) | ($true = ((X6 @ (sub @ X10 @ X9)))) | ($true != sP7) | ($true = ((sP6 @ X6))) | ($true = ((var @ (sK121 @ X9 @ X6))))) )),
% 12.48/2.22 inference(cnf_transformation,[],[f470])).
% 12.48/2.22 thf(f659,plain,(
% 12.48/2.22 ( ! [X10 : term,X6 : (term > $o),X9 : subst] : ((((X6 @ (lam @ (sK120 @ X6)))) != $true) | ($true = ((X6 @ (sub @ X10 @ X9)))) | ($true != ((X6 @ (sub @ (sK121 @ X9 @ X6) @ X9)))) | ($true != sP7) | ($true = ((sP6 @ X6)))) )),
% 12.48/2.22 inference(cnf_transformation,[],[f470])).
% 12.48/2.22 thf(f660,plain,(
% 12.48/2.22 ( ! [X10 : term,X8 : term,X6 : (term > $o),X9 : subst] : (($true != sP7) | ($true = ((X6 @ (sub @ X10 @ X9)))) | ($true = ((var @ (sK121 @ X9 @ X6)))) | ($true = ((sP6 @ X6))) | ($true != ((X6 @ X8))) | (((X6 @ (sub @ (sK120 @ X6) @ (push @ X8 @ id)))) = $true)) )),
% 12.48/2.22 inference(cnf_transformation,[],[f470])).
% 12.48/2.22 thf(f661,plain,(
% 12.48/2.22 ( ! [X10 : term,X8 : term,X6 : (term > $o),X9 : subst] : (($true != ((X6 @ X8))) | ($true != ((X6 @ (sub @ (sK121 @ X9 @ X6) @ X9)))) | ($true = ((sP6 @ X6))) | (((X6 @ (sub @ (sK120 @ X6) @ (push @ X8 @ id)))) = $true) | ($true != sP7) | ($true = ((X6 @ (sub @ X10 @ X9))))) )),
% 12.48/2.22 inference(cnf_transformation,[],[f470])).
% 12.48/2.22 thf(f667,plain,(
% 12.48/2.22 ( ! [X0 : (term > $o)] : (($true = ((X0 @ (sK122 @ X0)))) | (((sP6 @ X0)) != $true)) )),
% 12.48/2.22 inference(cnf_transformation,[],[f473])).
% 12.48/2.22 thf(f668,plain,(
% 12.48/2.22 ( ! [X0 : (term > $o)] : (($true = ((X0 @ (sK123 @ X0)))) | (((sP6 @ X0)) != $true)) )),
% 12.48/2.22 inference(cnf_transformation,[],[f473])).
% 12.48/2.22 thf(f669,plain,(
% 12.48/2.22 ( ! [X0 : (term > $o)] : (($true != ((X0 @ (ap @ (sK122 @ X0) @ (sK123 @ X0))))) | (((sP6 @ X0)) != $true)) )),
% 12.48/2.22 inference(cnf_transformation,[],[f473])).
% 12.48/2.22 thf(f672,plain,(
% 12.48/2.22 ($true = sP7) | (induction2lem != $true)),
% 12.48/2.22 inference(cnf_transformation,[],[f474])).
% 12.48/2.22 thf(f703,plain,(
% 12.48/2.22 (induction2_gthm != $true)),
% 12.48/2.22 inference(cnf_transformation,[],[f320])).
% 12.48/2.22 thf(f769,definition,(
% 12.48/2.22 spl162_9 <=> ! [X7 : term] : (((sub @ X7 @ id)) = X7)),
% 12.48/2.22 introduced(definition,[new_symbols(definition,[spl162_9])],[avatar_definition])).
% 12.48/2.22 thf(f770,plain,(
% 12.48/2.22 ( ! [X7 : term] : ((((sub @ X7 @ id)) = X7)) ) | ~spl162_9),
% 12.48/2.22 inference(avatar_component_clause,[],[f769])).
% 12.48/2.22 thf(f777,definition,(
% 12.48/2.22 spl162_11 <=> (induction2_gthm = $true)),
% 12.48/2.22 introduced(definition,[new_symbols(definition,[spl162_11])],[avatar_definition])).
% 12.48/2.22 thf(f812,definition,(
% 12.48/2.22 spl162_19 <=> ($true = sP5)),
% 12.48/2.22 introduced(definition,[new_symbols(definition,[spl162_19])],[avatar_definition])).
% 12.48/2.22 thf(f816,definition,(
% 12.48/2.22 spl162_20 <=> ! [X1 : term] : (($true = ((sK83 @ (sK84 @ X1)))) | ($true = ((sK83 @ (lam @ X1)))))),
% 12.48/2.22 introduced(definition,[new_symbols(definition,[spl162_20])],[avatar_definition])).
% 12.48/2.22 thf(f817,plain,(
% 12.48/2.22 ( ! [X1 : term] : (($true = ((sK83 @ (sK84 @ X1)))) | ($true = ((sK83 @ (lam @ X1))))) ) | ~spl162_20),
% 12.48/2.22 inference(avatar_component_clause,[],[f816])).
% 12.48/2.22 thf(f818,plain,(
% 12.48/2.22 spl162_19 | spl162_20),
% 12.48/2.22 inference(avatar_split_clause,[],[f623,f816,f812])).
% 12.48/2.22 thf(f883,definition,(
% 12.48/2.22 spl162_35 <=> ($true = sP7)),
% 12.48/2.22 introduced(definition,[new_symbols(definition,[spl162_35])],[avatar_definition])).
% 12.48/2.22 thf(f887,definition,(
% 12.48/2.22 spl162_36 <=> ! [X6 : (term > $o),X9 : subst,X10 : term] : ((((X6 @ (lam @ (sK120 @ X6)))) != $true) | ($true = ((sP6 @ X6))) | ($true != ((X6 @ (sub @ (sK121 @ X9 @ X6) @ X9)))) | ($true = ((X6 @ (sub @ X10 @ X9)))))),
% 12.48/2.22 introduced(definition,[new_symbols(definition,[spl162_36])],[avatar_definition])).
% 12.48/2.22 thf(f888,plain,(
% 12.48/2.22 ( ! [X10 : term,X6 : (term > $o),X9 : subst] : (($true != ((X6 @ (sub @ (sK121 @ X9 @ X6) @ X9)))) | (((X6 @ (lam @ (sK120 @ X6)))) != $true) | ($true = ((sP6 @ X6))) | ($true = ((X6 @ (sub @ X10 @ X9))))) ) | ~spl162_36),
% 12.48/2.22 inference(avatar_component_clause,[],[f887])).
% 12.48/2.22 thf(f889,plain,(
% 12.48/2.22 ~spl162_35 | spl162_36),
% 12.48/2.22 inference(avatar_split_clause,[],[f659,f887,f883])).
% 12.48/2.22 thf(f936,definition,(
% 12.48/2.22 spl162_47 <=> (induction2lem = $true)),
% 12.48/2.22 introduced(definition,[new_symbols(definition,[spl162_47])],[avatar_definition])).
% 12.48/2.22 thf(f939,plain,(
% 12.48/2.22 spl162_11 | spl162_47),
% 12.48/2.22 inference(avatar_split_clause,[],[f557,f936,f777])).
% 12.48/2.22 thf(f1051,definition,(
% 12.48/2.22 spl162_74 <=> ! [X4 : term] : (($true = ((sK83 @ X4))) | (((var @ X4)) != $true))),
% 12.48/2.22 introduced(definition,[new_symbols(definition,[spl162_74])],[avatar_definition])).
% 12.48/2.22 thf(f1052,plain,(
% 12.48/2.22 ( ! [X4 : term] : (($true = ((sK83 @ X4))) | (((var @ X4)) != $true)) ) | ~spl162_74),
% 12.48/2.22 inference(avatar_component_clause,[],[f1051])).
% 12.48/2.22 thf(f1053,plain,(
% 12.48/2.22 spl162_74 | spl162_19),
% 12.48/2.22 inference(avatar_split_clause,[],[f619,f812,f1051])).
% 12.48/2.22 thf(f1060,definition,(
% 12.48/2.22 spl162_76 <=> (induction2 = $true)),
% 12.48/2.22 introduced(definition,[new_symbols(definition,[spl162_76])],[avatar_definition])).
% 12.48/2.22 thf(f1063,plain,(
% 12.48/2.22 spl162_76 | ~spl162_19),
% 12.48/2.22 inference(avatar_split_clause,[],[f629,f812,f1060])).
% 12.48/2.22 thf(f1224,definition,(
% 12.48/2.22 spl162_113 <=> ! [X9 : subst,X10 : term,X6 : (term > $o),X8 : term] : (($true = ((X6 @ (sub @ X10 @ X9)))) | (((X6 @ (sub @ (sK120 @ X6) @ (push @ X8 @ id)))) = $true) | ($true != ((X6 @ X8))) | ($true = ((sP6 @ X6))) | ($true = ((var @ (sK121 @ X9 @ X6)))))),
% 12.48/2.22 introduced(definition,[new_symbols(definition,[spl162_113])],[avatar_definition])).
% 12.48/2.22 thf(f1225,plain,(
% 12.48/2.22 ( ! [X10 : term,X8 : term,X6 : (term > $o),X9 : subst] : ((((X6 @ (sub @ (sK120 @ X6) @ (push @ X8 @ id)))) = $true) | ($true = ((var @ (sK121 @ X9 @ X6)))) | ($true = ((sP6 @ X6))) | ($true = ((X6 @ (sub @ X10 @ X9)))) | ($true != ((X6 @ X8)))) ) | ~spl162_113),
% 12.48/2.22 inference(avatar_component_clause,[],[f1224])).
% 12.48/2.22 thf(f1226,plain,(
% 12.48/2.22 ~spl162_35 | spl162_113),
% 12.48/2.22 inference(avatar_split_clause,[],[f660,f1224,f883])).
% 12.48/2.22 thf(f1248,definition,(
% 12.48/2.22 spl162_118 <=> ! [X9 : subst,X10 : term,X6 : (term > $o),X8 : term] : (($true != ((X6 @ X8))) | ($true = ((X6 @ (sub @ X10 @ X9)))) | (((X6 @ (sub @ (sK120 @ X6) @ (push @ X8 @ id)))) = $true) | ($true = ((sP6 @ X6))) | ($true != ((X6 @ (sub @ (sK121 @ X9 @ X6) @ X9)))))),
% 12.48/2.22 introduced(definition,[new_symbols(definition,[spl162_118])],[avatar_definition])).
% 12.48/2.22 thf(f1249,plain,(
% 12.48/2.22 ( ! [X10 : term,X8 : term,X6 : (term > $o),X9 : subst] : ((((X6 @ (sub @ (sK120 @ X6) @ (push @ X8 @ id)))) = $true) | ($true = ((sP6 @ X6))) | ($true != ((X6 @ (sub @ (sK121 @ X9 @ X6) @ X9)))) | ($true != ((X6 @ X8))) | ($true = ((X6 @ (sub @ X10 @ X9))))) ) | ~spl162_118),
% 12.48/2.22 inference(avatar_component_clause,[],[f1248])).
% 12.48/2.22 thf(f1250,plain,(
% 12.48/2.22 ~spl162_35 | spl162_118),
% 12.48/2.22 inference(avatar_split_clause,[],[f661,f1248,f883])).
% 12.48/2.22 thf(f1256,plain,(
% 12.48/2.22 spl162_11 | ~spl162_76),
% 12.48/2.22 inference(avatar_split_clause,[],[f561,f1060,f777])).
% 12.48/2.22 thf(f1295,definition,(
% 12.48/2.22 spl162_128 <=> ! [X1 : term] : (($true = ((sK83 @ (lam @ X1)))) | ($true != ((sK83 @ (sub @ X1 @ (push @ (sK84 @ X1) @ id))))))),
% 12.48/2.22 introduced(definition,[new_symbols(definition,[spl162_128])],[avatar_definition])).
% 12.48/2.22 thf(f1296,plain,(
% 12.48/2.22 ( ! [X1 : term] : (($true != ((sK83 @ (sub @ X1 @ (push @ (sK84 @ X1) @ id))))) | ($true = ((sK83 @ (lam @ X1))))) ) | ~spl162_128),
% 12.48/2.22 inference(avatar_component_clause,[],[f1295])).
% 12.48/2.22 thf(f1297,plain,(
% 12.48/2.22 spl162_19 | spl162_128),
% 12.48/2.22 inference(avatar_split_clause,[],[f622,f1295,f812])).
% 12.48/2.22 thf(f1318,definition,(
% 12.48/2.22 spl162_133 <=> (axvarid = $true)),
% 12.48/2.22 introduced(definition,[new_symbols(definition,[spl162_133])],[avatar_definition])).
% 12.48/2.22 thf(f1321,plain,(
% 12.48/2.22 spl162_11 | spl162_133),
% 12.48/2.22 inference(avatar_split_clause,[],[f550,f1318,f777])).
% 12.48/2.22 thf(f1360,definition,(
% 12.48/2.22 spl162_141 <=> ($true = ((sK83 @ sK85)))),
% 12.48/2.22 introduced(definition,[new_symbols(definition,[spl162_141])],[avatar_definition])).
% 12.48/2.22 thf(f1362,plain,(
% 12.48/2.22 ($true != ((sK83 @ sK85))) | spl162_141),
% 12.48/2.22 inference(avatar_component_clause,[],[f1360])).
% 12.48/2.22 thf(f1363,plain,(
% 12.48/2.22 ~spl162_141 | spl162_19),
% 12.48/2.22 inference(avatar_split_clause,[],[f620,f812,f1360])).
% 12.48/2.22 thf(f1390,definition,(
% 12.48/2.22 spl162_148 <=> ($true = ((sP4 @ sK83)))),
% 12.48/2.22 introduced(definition,[new_symbols(definition,[spl162_148])],[avatar_definition])).
% 12.48/2.22 thf(f1392,plain,(
% 12.48/2.22 ($true != ((sP4 @ sK83))) | spl162_148),
% 12.48/2.22 inference(avatar_component_clause,[],[f1390])).
% 12.48/2.22 thf(f1393,plain,(
% 12.48/2.22 ~spl162_148 | spl162_19),
% 12.48/2.22 inference(avatar_split_clause,[],[f621,f812,f1390])).
% 12.48/2.22 thf(f1407,plain,(
% 12.48/2.22 spl162_35 | ~spl162_47),
% 12.48/2.22 inference(avatar_split_clause,[],[f672,f936,f883])).
% 12.48/2.22 thf(f1444,definition,(
% 12.48/2.22 spl162_158 <=> ! [X6 : (term > $o),X9 : subst,X10 : term] : ((((X6 @ (lam @ (sK120 @ X6)))) != $true) | ($true = ((var @ (sK121 @ X9 @ X6)))) | ($true = ((sP6 @ X6))) | ($true = ((X6 @ (sub @ X10 @ X9)))))),
% 12.48/2.22 introduced(definition,[new_symbols(definition,[spl162_158])],[avatar_definition])).
% 12.48/2.22 thf(f1445,plain,(
% 12.48/2.22 ( ! [X10 : term,X6 : (term > $o),X9 : subst] : (($true = ((var @ (sK121 @ X9 @ X6)))) | ($true = ((X6 @ (sub @ X10 @ X9)))) | ($true = ((sP6 @ X6))) | (((X6 @ (lam @ (sK120 @ X6)))) != $true)) ) | ~spl162_158),
% 12.48/2.22 inference(avatar_component_clause,[],[f1444])).
% 12.48/2.22 thf(f1446,plain,(
% 12.48/2.22 spl162_158 | ~spl162_35),
% 12.48/2.22 inference(avatar_split_clause,[],[f658,f883,f1444])).
% 12.48/2.22 thf(f1469,plain,(
% 12.48/2.22 spl162_9 | ~spl162_133),
% 12.48/2.22 inference(avatar_split_clause,[],[f634,f1318,f769])).
% 12.48/2.22 thf(f1489,plain,(
% 12.48/2.22 ~spl162_11),
% 12.48/2.22 inference(avatar_split_clause,[],[f703,f777])).
% 12.48/2.22 thf(f1746,plain,(
% 12.48/2.22 ( ! [X0 : (term > $o)] : ((((sP6 @ X0)) != $true) | ($true = ((sP4 @ X0))) | ($true != ((X0 @ (sK122 @ X0)))) | ($true != ((X0 @ (sK123 @ X0)))) | ($true != $true)) )),
% 12.48/2.22 inference(superposition,[],[f669,f627])).
% 12.48/2.22 thf(f1747,plain,(
% 12.48/2.22 ( ! [X0 : (term > $o)] : (($true != ((X0 @ (sK122 @ X0)))) | (((sP6 @ X0)) != $true) | ($true != ((X0 @ (sK123 @ X0)))) | ($true = ((sP4 @ X0)))) )),
% 12.48/2.22 inference(trivial_inequality_removal,[],[f1746])).
% 12.48/2.22 thf(f1750,plain,(
% 12.48/2.22 ( ! [X0 : (term > $o)] : (($true = ((sP4 @ X0))) | ($true != ((X0 @ (sK123 @ X0)))) | (((sP6 @ X0)) != $true)) )),
% 12.48/2.22 inference(forward_subsumption_resolution,[],[f1747,f667])).
% 12.48/2.22 thf(f1757,plain,(
% 12.48/2.22 ( ! [X0 : (term > $o)] : (($true = ((sP4 @ X0))) | (((sP6 @ X0)) != $true)) )),
% 12.48/2.22 inference(forward_subsumption_resolution,[],[f1750,f668])).
% 12.48/2.22 thf(f1838,plain,(
% 12.48/2.22 ($true != ((sP6 @ sK83))) | ($true != $true) | spl162_148),
% 12.48/2.22 inference(superposition,[],[f1392,f1757])).
% 12.48/2.22 thf(f1840,plain,(
% 12.48/2.22 ($true != ((sP6 @ sK83))) | spl162_148),
% 12.48/2.22 inference(trivial_inequality_removal,[],[f1838])).
% 12.48/2.22 thf(f2185,plain,(
% 12.48/2.22 ( ! [X0 : subst,X1 : term] : (($true != $true) | ($true != ((var @ (sub @ (sK121 @ X0 @ sK83) @ X0)))) | ($true != ((sK83 @ (lam @ (sK120 @ sK83))))) | ($true = ((sK83 @ (sub @ X1 @ X0)))) | ($true = ((sP6 @ sK83)))) ) | (~spl162_36 | ~spl162_74)),
% 12.48/2.22 inference(superposition,[],[f888,f1052])).
% 12.48/2.22 thf(f2191,plain,(
% 12.48/2.22 ( ! [X0 : subst,X1 : term] : (($true != ((sK83 @ (lam @ (sK120 @ sK83))))) | ($true != ((var @ (sub @ (sK121 @ X0 @ sK83) @ X0)))) | ($true = ((sP6 @ sK83))) | ($true = ((sK83 @ (sub @ X1 @ X0))))) ) | (~spl162_36 | ~spl162_74)),
% 12.48/2.22 inference(trivial_inequality_removal,[],[f2185])).
% 12.48/2.22 thf(f2193,plain,(
% 12.48/2.22 ( ! [X0 : subst,X1 : term] : (($true != ((var @ (sub @ (sK121 @ X0 @ sK83) @ X0)))) | ($true != ((sK83 @ (lam @ (sK120 @ sK83))))) | ($true = ((sK83 @ (sub @ X1 @ X0))))) ) | (~spl162_36 | ~spl162_74 | spl162_148)),
% 12.48/2.22 inference(forward_subsumption_resolution,[],[f2191,f1840])).
% 12.48/2.22 thf(f2198,definition,(
% 12.48/2.22 spl162_199 <=> ($true = ((sK83 @ (lam @ (sK120 @ sK83)))))),
% 12.48/2.22 introduced(definition,[new_symbols(definition,[spl162_199])],[avatar_definition])).
% 12.48/2.22 thf(f2202,definition,(
% 12.48/2.22 spl162_200 <=> ! [X0 : subst,X1 : term] : (($true != ((var @ (sub @ (sK121 @ X0 @ sK83) @ X0)))) | ($true = ((sK83 @ (sub @ X1 @ X0)))))),
% 12.48/2.22 introduced(definition,[new_symbols(definition,[spl162_200])],[avatar_definition])).
% 12.48/2.22 thf(f2203,plain,(
% 12.48/2.22 ( ! [X0 : subst,X1 : term] : (($true != ((var @ (sub @ (sK121 @ X0 @ sK83) @ X0)))) | ($true = ((sK83 @ (sub @ X1 @ X0))))) ) | ~spl162_200),
% 12.48/2.22 inference(avatar_component_clause,[],[f2202])).
% 12.48/2.22 thf(f2204,plain,(
% 12.48/2.22 ~spl162_199 | spl162_200 | ~spl162_36 | ~spl162_74 | spl162_148),
% 12.48/2.22 inference(avatar_split_clause,[],[f2193,f1390,f1051,f887,f2202,f2198])).
% 12.48/2.22 thf(f2273,plain,(
% 12.48/2.22 ( ! [X0 : subst,X1 : term] : (($true = ((sK83 @ (sub @ X1 @ X0)))) | ($true = ((var @ (sK121 @ X0 @ sK83)))) | ($true != ((sK83 @ (sK84 @ (sK120 @ sK83))))) | ($true = ((sP6 @ sK83))) | ($true != $true) | ($true = ((sK83 @ (lam @ (sK120 @ sK83)))))) ) | (~spl162_113 | ~spl162_128)),
% 12.48/2.22 inference(superposition,[],[f1296,f1225])).
% 12.48/2.22 thf(f2276,plain,(
% 12.48/2.22 ( ! [X0 : subst,X1 : term] : (($true = ((sP6 @ sK83))) | ($true = ((sK83 @ (lam @ (sK120 @ sK83))))) | ($true = ((var @ (sK121 @ X0 @ sK83)))) | ($true != ((sK83 @ (sK84 @ (sK120 @ sK83))))) | ($true = ((sK83 @ (sub @ X1 @ X0))))) ) | (~spl162_113 | ~spl162_128)),
% 12.48/2.22 inference(trivial_inequality_removal,[],[f2273])).
% 12.48/2.22 thf(f2279,plain,(
% 12.48/2.22 ( ! [X0 : subst,X1 : term] : (($true = ((sK83 @ (lam @ (sK120 @ sK83))))) | ($true = ((sP6 @ sK83))) | ($true = ((sK83 @ (sub @ X1 @ X0)))) | ($true = ((var @ (sK121 @ X0 @ sK83))))) ) | (~spl162_20 | ~spl162_113 | ~spl162_128)),
% 12.48/2.22 inference(forward_subsumption_resolution,[],[f2276,f817])).
% 12.48/2.22 thf(f2280,plain,(
% 12.48/2.22 ( ! [X0 : subst,X1 : term] : (($true = ((sP6 @ sK83))) | ($true = ((var @ (sK121 @ X0 @ sK83)))) | ($true = ((sK83 @ (sub @ X1 @ X0))))) ) | (~spl162_20 | ~spl162_113 | ~spl162_128 | ~spl162_158)),
% 12.48/2.22 inference(forward_subsumption_resolution,[],[f2279,f1445])).
% 12.48/2.22 thf(f2281,plain,(
% 12.48/2.22 ( ! [X0 : subst,X1 : term] : (($true = ((var @ (sK121 @ X0 @ sK83)))) | ($true = ((sK83 @ (sub @ X1 @ X0))))) ) | (~spl162_20 | ~spl162_113 | ~spl162_128 | spl162_148 | ~spl162_158)),
% 12.48/2.22 inference(forward_subsumption_resolution,[],[f2280,f1840])).
% 12.48/2.22 thf(f2282,plain,(
% 12.48/2.22 ( ! [X0 : subst,X1 : term] : (($true = ((sK83 @ (lam @ (sK120 @ sK83))))) | ($true != ((sK83 @ (sK84 @ (sK120 @ sK83))))) | ($true != $true) | ($true = ((sK83 @ (sub @ X1 @ X0)))) | ($true = ((sP6 @ sK83))) | ($true != ((sK83 @ (sub @ (sK121 @ X0 @ sK83) @ X0))))) ) | (~spl162_118 | ~spl162_128)),
% 12.48/2.22 inference(superposition,[],[f1296,f1249])).
% 12.48/2.22 thf(f2287,plain,(
% 12.48/2.22 ( ! [X0 : subst,X1 : term] : (($true = ((sP6 @ sK83))) | ($true != ((sK83 @ (sK84 @ (sK120 @ sK83))))) | ($true = ((sK83 @ (sub @ X1 @ X0)))) | ($true != ((sK83 @ (sub @ (sK121 @ X0 @ sK83) @ X0)))) | ($true = ((sK83 @ (lam @ (sK120 @ sK83)))))) ) | (~spl162_118 | ~spl162_128)),
% 12.48/2.22 inference(trivial_inequality_removal,[],[f2282])).
% 12.48/2.22 thf(f2288,plain,(
% 12.48/2.22 ( ! [X0 : subst,X1 : term] : (($true = ((sP6 @ sK83))) | ($true = ((sK83 @ (sub @ X1 @ X0)))) | ($true != ((sK83 @ (sK84 @ (sK120 @ sK83))))) | ($true != ((sK83 @ (sub @ (sK121 @ X0 @ sK83) @ X0))))) ) | (~spl162_36 | ~spl162_118 | ~spl162_128)),
% 12.48/2.22 inference(forward_subsumption_resolution,[],[f2287,f888])).
% 12.48/2.22 thf(f2289,plain,(
% 12.48/2.22 ( ! [X0 : subst,X1 : term] : (($true != ((sK83 @ (sub @ (sK121 @ X0 @ sK83) @ X0)))) | ($true != ((sK83 @ (sK84 @ (sK120 @ sK83))))) | ($true = ((sK83 @ (sub @ X1 @ X0))))) ) | (~spl162_36 | ~spl162_118 | ~spl162_128 | spl162_148)),
% 12.48/2.22 inference(forward_subsumption_resolution,[],[f2288,f1840])).
% 12.48/2.22 thf(f2291,definition,(
% 12.48/2.22 spl162_203 <=> ($true = ((sK83 @ (sK84 @ (sK120 @ sK83)))))),
% 12.48/2.22 introduced(definition,[new_symbols(definition,[spl162_203])],[avatar_definition])).
% 12.48/2.22 thf(f2293,plain,(
% 12.48/2.22 ($true != ((sK83 @ (sK84 @ (sK120 @ sK83))))) | spl162_203),
% 12.48/2.22 inference(avatar_component_clause,[],[f2291])).
% 12.48/2.22 thf(f2295,definition,(
% 12.48/2.22 spl162_204 <=> ! [X0 : subst,X1 : term] : (($true != ((sK83 @ (sub @ (sK121 @ X0 @ sK83) @ X0)))) | ($true = ((sK83 @ (sub @ X1 @ X0)))))),
% 12.48/2.22 introduced(definition,[new_symbols(definition,[spl162_204])],[avatar_definition])).
% 12.48/2.22 thf(f2296,plain,(
% 12.48/2.22 ( ! [X0 : subst,X1 : term] : (($true != ((sK83 @ (sub @ (sK121 @ X0 @ sK83) @ X0)))) | ($true = ((sK83 @ (sub @ X1 @ X0))))) ) | ~spl162_204),
% 12.48/2.22 inference(avatar_component_clause,[],[f2295])).
% 12.48/2.22 thf(f2297,plain,(
% 12.48/2.22 ~spl162_203 | spl162_204 | ~spl162_36 | ~spl162_118 | ~spl162_128 | spl162_148),
% 12.48/2.22 inference(avatar_split_clause,[],[f2289,f1390,f1295,f1248,f887,f2295,f2291])).
% 12.48/2.22 thf(f2298,plain,(
% 12.48/2.22 ($true = ((sK83 @ (lam @ (sK120 @ sK83))))) | ($true != $true) | (~spl162_20 | spl162_203)),
% 12.48/2.22 inference(superposition,[],[f2293,f817])).
% 12.48/2.22 thf(f2300,plain,(
% 12.48/2.22 ($true = ((sK83 @ (lam @ (sK120 @ sK83))))) | (~spl162_20 | spl162_203)),
% 12.48/2.22 inference(trivial_inequality_removal,[],[f2298])).
% 12.48/2.22 thf(f2304,plain,(
% 12.48/2.22 spl162_199 | ~spl162_20 | spl162_203),
% 12.48/2.22 inference(avatar_split_clause,[],[f2300,f2291,f816,f2198])).
% 12.48/2.22 thf(f2305,plain,(
% 12.48/2.22 ( ! [X0 : term] : ((((sK83 @ (sub @ X0 @ id))) = $true) | ($true != ((var @ (sK121 @ id @ sK83))))) ) | (~spl162_9 | ~spl162_200)),
% 12.48/2.22 inference(superposition,[],[f2203,f770])).
% 12.48/2.22 thf(f2316,plain,(
% 12.48/2.22 ( ! [X0 : term] : ((((sK83 @ (sub @ X0 @ id))) = $true)) ) | (~spl162_9 | ~spl162_20 | ~spl162_113 | ~spl162_128 | spl162_148 | ~spl162_158 | ~spl162_200)),
% 12.48/2.22 inference(forward_subsumption_resolution,[],[f2305,f2281])).
% 12.48/2.22 thf(f2319,plain,(
% 12.48/2.22 ( ! [X0 : term] : (($true = ((sK83 @ X0)))) ) | (~spl162_9 | ~spl162_20 | ~spl162_113 | ~spl162_128 | spl162_148 | ~spl162_158 | ~spl162_200)),
% 12.48/2.22 inference(forward_demodulation,[],[f2316,f770])).
% 12.48/2.22 thf(f2327,plain,(
% 12.48/2.22 ($true != $true) | (~spl162_9 | ~spl162_20 | ~spl162_113 | ~spl162_128 | spl162_141 | spl162_148 | ~spl162_158 | ~spl162_200)),
% 12.48/2.22 inference(superposition,[],[f1362,f2319])).
% 12.48/2.22 thf(f2339,plain,(
% 12.48/2.22 $false | (~spl162_9 | ~spl162_20 | ~spl162_113 | ~spl162_128 | spl162_141 | spl162_148 | ~spl162_158 | ~spl162_200)),
% 12.48/2.22 inference(trivial_inequality_removal,[],[f2327])).
% 12.48/2.22 thf(f2340,plain,(
% 12.48/2.22 ~spl162_9 | ~spl162_20 | ~spl162_113 | ~spl162_128 | spl162_141 | spl162_148 | ~spl162_158 | ~spl162_200),
% 12.48/2.22 inference(avatar_contradiction_clause,[],[f2339])).
% 12.48/2.22 thf(f2393,plain,(
% 12.48/2.22 ( ! [X0 : subst,X1 : term] : (($true != $true) | ($true = ((sK83 @ (sub @ X1 @ X0)))) | ($true != ((var @ (sub @ (sK121 @ X0 @ sK83) @ X0))))) ) | (~spl162_74 | ~spl162_204)),
% 12.48/2.22 inference(superposition,[],[f2296,f1052])).
% 12.48/2.22 thf(f2395,plain,(
% 12.48/2.22 ( ! [X0 : subst,X1 : term] : (($true != ((var @ (sub @ (sK121 @ X0 @ sK83) @ X0)))) | ($true = ((sK83 @ (sub @ X1 @ X0))))) ) | (~spl162_74 | ~spl162_204)),
% 12.48/2.22 inference(trivial_inequality_removal,[],[f2393])).
% 12.48/2.22 thf(f2398,plain,(
% 12.48/2.22 spl162_200 | ~spl162_74 | ~spl162_204),
% 12.48/2.22 inference(avatar_split_clause,[],[f2395,f2295,f1051,f2202])).
% 12.48/2.22 cnf(s10, plain, spl162_19 | spl162_20, inference(sat_conversion,[],[f818])).
% 12.48/2.22 cnf(s21, plain, ~spl162_35 | spl162_36, inference(sat_conversion,[],[f889])).
% 12.48/2.22 cnf(s29, plain, spl162_11 | spl162_47, inference(sat_conversion,[],[f939])).
% 12.48/2.22 cnf(s48, plain, spl162_19 | spl162_74, inference(sat_conversion,[],[f1053])).
% 12.48/2.22 cnf(s51, plain, ~spl162_19 | spl162_76, inference(sat_conversion,[],[f1063])).
% 12.48/2.22 cnf(s84, plain, ~spl162_35 | spl162_113, inference(sat_conversion,[],[f1226])).
% 12.48/2.22 cnf(s91, plain, ~spl162_35 | spl162_118, inference(sat_conversion,[],[f1250])).
% 12.48/2.22 cnf(s93, plain, spl162_11 | ~spl162_76, inference(sat_conversion,[],[f1256])).
% 12.48/2.22 cnf(s104, plain, spl162_19 | spl162_128, inference(sat_conversion,[],[f1297])).
% 12.48/2.22 cnf(s110, plain, spl162_11 | spl162_133, inference(sat_conversion,[],[f1321])).
% 12.48/2.22 cnf(s123, plain, spl162_19 | ~spl162_141, inference(sat_conversion,[],[f1363])).
% 12.48/2.22 cnf(s130, plain, spl162_19 | ~spl162_148, inference(sat_conversion,[],[f1393])).
% 12.48/2.22 cnf(s134, plain, spl162_35 | ~spl162_47, inference(sat_conversion,[],[f1407])).
% 12.48/2.22 cnf(s146, plain, ~spl162_35 | spl162_158, inference(sat_conversion,[],[f1446])).
% 12.48/2.22 cnf(s152, plain, spl162_9 | ~spl162_133, inference(sat_conversion,[],[f1469])).
% 12.48/2.22 cnf(s159, plain, ~spl162_11, inference(sat_conversion,[],[f1489])).
% 12.48/2.22 cnf(s208, plain, ~spl162_36 | ~spl162_74 | spl162_148 | ~spl162_199 | spl162_200, inference(sat_conversion,[],[f2204])).
% 12.48/2.22 cnf(s210, plain, ~spl162_36 | ~spl162_118 | ~spl162_128 | spl162_148 | ~spl162_203 | spl162_204, inference(sat_conversion,[],[f2297])).
% 12.48/2.22 cnf(s212, plain, ~spl162_20 | spl162_199 | spl162_203, inference(sat_conversion,[],[f2304])).
% 12.48/2.22 cnf(s213, plain, ~spl162_9 | ~spl162_20 | ~spl162_113 | ~spl162_128 | spl162_141 | spl162_148 | ~spl162_158 | ~spl162_200, inference(sat_conversion,[],[f2340])).
% 12.48/2.22 cnf(s216, plain, ~spl162_74 | spl162_200 | ~spl162_204, inference(sat_conversion,[],[f2398])).
% 12.48/2.22 cnf(s235, plain, spl162_133, inference(rat,[],[s110,s159])).
% 12.48/2.22 cnf(s236, plain, spl162_9, inference(rat,[],[s152,s235])).
% 12.48/2.22 cnf(s244, plain, ~spl162_76, inference(rat,[],[s93,s159])).
% 12.48/2.22 cnf(s258, plain, ~spl162_19, inference(rat,[],[s51,s244])).
% 12.48/2.22 cnf(s259, plain, ~spl162_148, inference(rat,[],[s130,s258])).
% 12.48/2.22 cnf(s260, plain, ~spl162_141, inference(rat,[],[s123,s258])).
% 12.48/2.22 cnf(s261, plain, spl162_128, inference(rat,[],[s104,s258])).
% 12.48/2.22 cnf(s268, plain, spl162_74, inference(rat,[],[s48,s258])).
% 12.48/2.22 cnf(s277, plain, spl162_47, inference(rat,[],[s29,s159])).
% 12.48/2.22 cnf(s278, plain, spl162_35, inference(rat,[],[s134,s277])).
% 12.48/2.22 cnf(s279, plain, spl162_158, inference(rat,[],[s146,s278])).
% 12.48/2.22 cnf(s280, plain, spl162_118, inference(rat,[],[s91,s278])).
% 12.48/2.22 cnf(s281, plain, spl162_113, inference(rat,[],[s84,s278])).
% 12.48/2.22 cnf(s287, plain, spl162_36, inference(rat,[],[s21,s278])).
% 12.48/2.22 cnf(s293, plain, spl162_20, inference(rat,[],[s10,s258])).
% 12.48/2.22 cnf(s294, plain, ~spl162_200, inference(rat,[],[s213,s281,s279,s259,s260,s261,s236,s293])).
% 12.48/2.22 cnf(s295, plain, ~spl162_204, inference(rat,[],[s216,s268,s294])).
% 12.48/2.22 cnf(s296, plain, ~spl162_199, inference(rat,[],[s208,s287,s268,s259,s294])).
% 12.48/2.22 cnf(s297, plain, ~spl162_203, inference(rat,[],[s210,s287,s280,s259,s261,s295])).
% 12.48/2.22 cnf(s298, plain, $false, inference(rat,[],[s212,s293,s297,s296])).
% 12.48/2.22 thf(f2409,plain,(
% 12.48/2.22 $false),
% 12.48/2.22 inference(avatar_sat_refutation,[],[s298])).
% 12.48/2.22 % SZS output end Proof for theBenchmark
% 12.48/2.22 % (641981)------------------------------
% 12.48/2.22 % (641981)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.48/2.22 % (641981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.48/2.22 % (641981)CaDiCaL version: 2.1.3
% 12.48/2.22 % (641981)Termination reason: Refutation
% 12.48/2.22 % (641981)Time elapsed: 0.091 s
% 12.48/2.22 % (641981)Peak memory usage: 15 MB
% 12.48/2.22 % (641981)Instructions burned: 175 (million)
% 12.48/2.22 % (641789)Success in time 1.833 s
% 12.48/2.22 % Vampire exiting
%------------------------------------------------------------------------------