%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP004^2 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:07:36 AM UTC 2026
% Result : Theorem 3.42s 0.81s
% Output : Refutation 3.42s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP004^2 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.17 % Computer : n010.cluster.edu
% 0.10/0.17 % Model : x86_64 x86_64
% 0.10/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.17 % Memory : 8046.5625MB
% 0.10/0.17 % OS : Linux 6.8.0-71-generic
% 0.10/0.18 % CPULimit : 300
% 0.10/0.18 % WCLimit : 300
% 0.10/0.18 % DateTime : Tue Sep 29 19:20:48 UTC 2026
% 0.10/0.18 % CPUTime :
% 0.10/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.21 Running higher-order theorem proving
% 0.10/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.35 % (3287889)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.19/0.35 % (3287895)lrs+10_16_si=on:nwc=1.5:random_seed=332782685:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.19/0.35 % (3287895)Instruction limit reached!
% 0.19/0.35 % (3287895)------------------------------
% 0.19/0.35 % (3287895)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.35 % (3287895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.35 % (3287895)CaDiCaL version: 2.1.3
% 0.19/0.35 % (3287895)Termination reason: Instruction limit
% 0.19/0.35 % (3287895)Termination phase: Saturation
% 0.19/0.35 % (3287895)Time elapsed: 0.006 s
% 0.19/0.35 % (3287895)Peak memory usage: 12 MB
% 0.19/0.35 % (3287895)Instructions burned: 21 (million)
% 0.19/0.35 % (3287898)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=732917299:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.19/0.35 % (3287896)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=2784835346:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.19/0.36 % (3287894)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=28225077:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.19/0.36 % (3287897)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=128077349: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.19/0.36 % (3287896)Instruction limit reached!
% 0.19/0.36 % (3287896)------------------------------
% 0.19/0.36 % (3287896)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.36 % (3287896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.36 % (3287896)CaDiCaL version: 2.1.3
% 0.19/0.36 % (3287896)Termination reason: Instruction limit
% 0.19/0.36 % (3287896)Termination phase: Property scanning
% 0.19/0.36 % (3287896)Time elapsed: 0.002 s
% 0.19/0.36 % (3287896)Peak memory usage: 9 MB
% 0.19/0.36 % (3287896)Instructions burned: 4 (million)
% 0.19/0.36 % (3287900)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.19/0.36 % (3287900)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.19/0.36 % (3287899)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=92865041:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.19/0.36 % (3287900)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=2818240770:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.19/0.36 % (3287905)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=487749983:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.19/0.36 % (3287905)Instruction limit reached!
% 0.19/0.36 % (3287905)------------------------------
% 0.19/0.36 % (3287905)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.36 % (3287905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.36 % (3287905)CaDiCaL version: 2.1.3
% 0.19/0.36 % (3287905)Termination reason: Instruction limit
% 0.19/0.36 % (3287905)Termination phase: shuffling
% 0.19/0.36 % (3287905)Time elapsed: 0.0000 s
% 0.19/0.36 % (3287905)Peak memory usage: 9 MB
% 0.19/0.36 % (3287905)Instructions burned: 2 (million)
% 0.19/0.36 % (3287898)Instruction limit reached!
% 0.19/0.36 % (3287898)------------------------------
% 0.19/0.36 % (3287898)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.36 % (3287898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.36 % (3287898)CaDiCaL version: 2.1.3
% 0.19/0.36 % (3287898)Termination reason: Instruction limit
% 0.19/0.36 % (3287898)Termination phase: Saturation
% 0.19/0.36 % (3287898)Time elapsed: 0.012 s
% 0.19/0.36 % (3287898)Peak memory usage: 11 MB
% 0.19/0.36 % (3287898)Instructions burned: 25 (million)
% 0.19/0.36 % (3287911)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.93/0.38 % (3287907)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=2438816085:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.93/0.38 % (3287911)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1187569483:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.93/0.38 % (3287911)Instruction limit reached!
% 0.93/0.38 % (3287911)------------------------------
% 0.93/0.38 % (3287911)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.93/0.38 % (3287911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.93/0.38 % (3287911)CaDiCaL version: 2.1.3
% 0.93/0.38 % (3287911)Termination reason: Instruction limit
% 0.93/0.38 % (3287911)Termination phase: Saturation
% 0.93/0.38 % (3287911)Time elapsed: 0.002 s
% 0.93/0.38 % (3287911)Peak memory usage: 11 MB
% 0.93/0.38 % (3287911)Instructions burned: 9 (million)
% 0.93/0.38 % (3287907)Instruction limit reached!
% 0.93/0.38 % (3287907)------------------------------
% 0.93/0.38 % (3287907)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.93/0.38 % (3287907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.93/0.38 % (3287907)CaDiCaL version: 2.1.3
% 0.93/0.38 % (3287907)Termination reason: Instruction limit
% 0.93/0.38 % (3287907)Termination phase: Property scanning
% 0.93/0.38 % (3287907)Time elapsed: 0.003 s
% 0.93/0.38 % (3287907)Peak memory usage: 10 MB
% 0.93/0.38 % (3287907)Instructions burned: 6 (million)
% 0.93/0.38 % (3287912)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=3633693498:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.93/0.38 % (3287915)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.93/0.38 % (3287915)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.93/0.38 % (3287915)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=103144866:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 0.93/0.38 % (3287912)Instruction limit reached!
% 0.93/0.38 % (3287912)------------------------------
% 0.93/0.38 % (3287912)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.93/0.38 % (3287912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.93/0.38 % (3287912)CaDiCaL version: 2.1.3
% 0.93/0.38 % (3287912)Termination reason: Instruction limit
% 0.93/0.38 % (3287912)Termination phase: Saturation
% 0.93/0.38 % (3287912)Time elapsed: 0.006 s
% 0.93/0.38 % (3287912)Peak memory usage: 12 MB
% 0.93/0.38 % (3287912)Instructions burned: 13 (million)
% 0.93/0.38 % (3287894)Instruction limit reached!
% 0.93/0.38 % (3287894)------------------------------
% 0.93/0.38 % (3287894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.93/0.38 % (3287894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.93/0.38 % (3287894)CaDiCaL version: 2.1.3
% 0.93/0.38 % (3287894)Termination reason: Instruction limit
% 0.93/0.38 % (3287894)Termination phase: Saturation
% 0.93/0.38 % (3287894)Time elapsed: 0.042 s
% 0.93/0.38 % (3287894)Peak memory usage: 12 MB
% 0.93/0.38 % (3287894)Instructions burned: 89 (million)
% 0.93/0.38 % (3287915)Instruction limit reached!
% 0.93/0.38 % (3287915)------------------------------
% 0.93/0.38 % (3287915)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.93/0.38 % (3287915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.93/0.38 % (3287915)CaDiCaL version: 2.1.3
% 0.93/0.38 % (3287915)Termination reason: Instruction limit
% 0.93/0.38 % (3287915)Termination phase: Saturation
% 0.93/0.38 % (3287915)Time elapsed: 0.007 s
% 0.93/0.38 % (3287915)Peak memory usage: 12 MB
% 0.93/0.38 % (3287915)Instructions burned: 28 (million)
% 0.93/0.38 % (3287899)Instruction limit reached!
% 0.93/0.38 % (3287899)------------------------------
% 0.93/0.38 % (3287899)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.93/0.38 % (3287899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.93/0.38 % (3287899)CaDiCaL version: 2.1.3
% 0.93/0.38 % (3287899)Termination reason: Instruction limit
% 0.93/0.43 % (3287899)Termination phase: Saturation
% 0.93/0.43 % (3287899)Time elapsed: 0.041 s
% 0.93/0.43 % (3287899)Peak memory usage: 13 MB
% 0.93/0.43 % (3287899)Instructions burned: 76 (million)
% 0.93/0.43 % (3287916)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=1840490350:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.93/0.43 % (3287920)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 0.93/0.43 % (3287920)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=151175333:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.93/0.43 % (3287920)Instruction limit reached!
% 0.93/0.43 % (3287920)------------------------------
% 0.93/0.43 % (3287920)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.93/0.43 % (3287920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.93/0.43 % (3287920)CaDiCaL version: 2.1.3
% 0.93/0.43 % (3287920)Termination reason: Instruction limit
% 0.93/0.43 % (3287920)Termination phase: Saturation
% 0.93/0.43 % (3287920)Time elapsed: 0.003 s
% 0.93/0.43 % (3287920)Peak memory usage: 11 MB
% 0.93/0.43 % (3287920)Instructions burned: 14 (million)
% 0.93/0.43 % (3287919)lrs+10_1_si=on:cs=on:random_seed=3393756639:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.93/0.43 % (3287921)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=4167245061:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.93/0.43 % (3287919)Instruction limit reached!
% 0.93/0.43 % (3287919)------------------------------
% 0.93/0.43 % (3287919)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.93/0.43 % (3287919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.93/0.43 % (3287919)CaDiCaL version: 2.1.3
% 0.93/0.43 % (3287919)Termination reason: Instruction limit
% 0.93/0.43 % (3287919)Termination phase: Property scanning
% 0.93/0.43 % (3287919)Time elapsed: 0.004 s
% 0.93/0.43 % (3287919)Peak memory usage: 10 MB
% 0.93/0.43 % (3287919)Instructions burned: 10 (million)
% 0.93/0.43 % (3287926)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=519355506:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/25Mi)
% 0.93/0.43 % (3287922)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=3783095843:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.93/0.43 % (3287926)Instruction limit reached!
% 0.93/0.43 % (3287926)------------------------------
% 0.93/0.43 % (3287926)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.93/0.43 % (3287926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.93/0.43 % (3287926)CaDiCaL version: 2.1.3
% 0.93/0.43 % (3287926)Termination reason: Instruction limit
% 0.93/0.43 % (3287926)Termination phase: Saturation
% 0.93/0.43 % (3287926)Time elapsed: 0.007 s
% 0.93/0.43 % (3287926)Peak memory usage: 12 MB
% 0.93/0.43 % (3287926)Instructions burned: 27 (million)
% 0.93/0.43 % (3287921)Instruction limit reached!
% 0.93/0.43 % (3287921)------------------------------
% 0.93/0.43 % (3287921)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.93/0.43 % (3287921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.93/0.43 % (3287921)CaDiCaL version: 2.1.3
% 0.93/0.43 % (3287921)Termination reason: Instruction limit
% 0.93/0.43 % (3287921)Termination phase: Saturation
% 0.93/0.43 % (3287921)Time elapsed: 0.020 s
% 0.93/0.43 % (3287921)Peak memory usage: 12 MB
% 0.93/0.43 % (3287921)Instructions burned: 39 (million)
% 0.93/0.43 % (3287922)Refutation not found, incomplete strategy
% 0.93/0.43 % (3287922)------------------------------
% 0.93/0.43 % (3287922)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.93/0.43 % (3287922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.93/0.43 % (3287922)CaDiCaL version: 2.1.3
% 0.93/0.43 % (3287922)Termination reason: Refutation not found, incomplete strategy
% 0.93/0.43 % (3287922)Time elapsed: 0.011 s
% 0.93/0.43 % (3287922)Peak memory usage: 12 MB
% 0.93/0.43 % (3287922)Instructions burned: 10 (million)
% 0.93/0.43 % (3287922)------------------------------
% 0.93/0.43 % (3287922)------------------------------
% 0.93/0.43 % (3287928)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=355478414:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2999 on theBenchmark for (2999ds/14Mi)
% 0.93/0.48 % (3287900)Instruction limit reached!
% 0.93/0.48 % (3287900)------------------------------
% 0.93/0.48 % (3287900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.93/0.48 % (3287900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.93/0.48 % (3287900)CaDiCaL version: 2.1.3
% 0.93/0.48 % (3287900)Termination reason: Instruction limit
% 0.93/0.48 % (3287900)Termination phase: Saturation
% 0.93/0.48 % (3287900)Time elapsed: 0.085 s
% 0.93/0.48 % (3287900)Peak memory usage: 13 MB
% 0.93/0.48 % (3287900)Instructions burned: 163 (million)
% 0.93/0.48 % (3287916)Instruction limit reached!
% 0.93/0.48 % (3287916)------------------------------
% 0.93/0.48 % (3287916)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.93/0.48 % (3287916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.93/0.48 % (3287916)CaDiCaL version: 2.1.3
% 0.93/0.48 % (3287916)Termination reason: Instruction limit
% 0.93/0.48 % (3287916)Termination phase: Saturation
% 0.93/0.48 % (3287916)Time elapsed: 0.044 s
% 0.93/0.48 % (3287916)Peak memory usage: 12 MB
% 0.93/0.48 % (3287916)Instructions burned: 87 (million)
% 0.93/0.48 % (3287933)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=696007182:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2998 on theBenchmark for (2998ds/2Mi)
% 0.93/0.48 % (3287928)Instruction limit reached!
% 0.93/0.48 % (3287928)------------------------------
% 0.93/0.48 % (3287928)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.93/0.48 % (3287928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.93/0.48 % (3287928)CaDiCaL version: 2.1.3
% 0.93/0.48 % (3287928)Termination reason: Instruction limit
% 0.93/0.48 % (3287928)Termination phase: Saturation
% 0.93/0.48 % (3287928)Time elapsed: 0.011 s
% 0.93/0.48 % (3287928)Peak memory usage: 12 MB
% 0.93/0.48 % (3287928)Instructions burned: 21 (million)
% 0.93/0.48 % (3287933)Instruction limit reached!
% 0.93/0.48 % (3287933)------------------------------
% 0.93/0.48 % (3287933)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.93/0.48 % (3287933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.93/0.48 % (3287933)CaDiCaL version: 2.1.3
% 0.93/0.48 % (3287933)Termination reason: Instruction limit
% 0.93/0.48 % (3287933)Termination phase: Saturation
% 0.93/0.48 % (3287933)Time elapsed: 0.004 s
% 0.93/0.48 % (3287933)Peak memory usage: 12 MB
% 0.93/0.48 % (3287933)Instructions burned: 14 (million)
% 0.93/0.48 % (3287932)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=1026216585:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 0.93/0.48 % (3287931)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=1282801771:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 0.93/0.48 % (3287939)WARNING Broken Constraint: if sine_to_age_generality_threshold(10) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.93/0.48 % (3287939)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 0.93/0.48 % (3287932)Instruction limit reached!
% 0.93/0.48 % (3287932)------------------------------
% 0.93/0.48 % (3287932)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.93/0.48 % (3287932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.93/0.48 % (3287932)CaDiCaL version: 2.1.3
% 0.93/0.48 % (3287932)Termination reason: Instruction limit
% 0.93/0.48 % (3287932)Termination phase: Saturation
% 0.93/0.48 % (3287932)Time elapsed: 0.007 s
% 0.93/0.48 % (3287932)Peak memory usage: 12 MB
% 0.93/0.48 % (3287932)Instructions burned: 15 (million)
% 0.93/0.48 % (3287939)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=3190885445:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 0.93/0.48 % (3287936)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3603905999:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 0.93/0.48 % (3287937)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=563509015:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.72/0.56 % (3287939)Instruction limit reached!
% 1.72/0.56 % (3287939)------------------------------
% 1.72/0.56 % (3287939)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.72/0.56 % (3287939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.72/0.56 % (3287939)CaDiCaL version: 2.1.3
% 1.72/0.56 % (3287939)Termination reason: Instruction limit
% 1.72/0.56 % (3287939)Termination phase: Saturation
% 1.72/0.56 % (3287939)Time elapsed: 0.004 s
% 1.72/0.56 % (3287939)Peak memory usage: 12 MB
% 1.72/0.56 % (3287939)Instructions burned: 15 (million)
% 1.72/0.56 % (3287938)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=891688342:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 1.72/0.56 % (3287942)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 1.72/0.56 % (3287946)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=1028259862:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 1.72/0.56 % (3287937)Instruction limit reached!
% 1.72/0.56 % (3287937)------------------------------
% 1.72/0.56 % (3287937)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.72/0.56 % (3287937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.72/0.56 % (3287937)CaDiCaL version: 2.1.3
% 1.72/0.56 % (3287937)Termination reason: Instruction limit
% 1.72/0.56 % (3287937)Termination phase: Saturation
% 1.72/0.56 % (3287937)Time elapsed: 0.011 s
% 1.72/0.56 % (3287937)Peak memory usage: 11 MB
% 1.72/0.56 % (3287937)Instructions burned: 24 (million)
% 1.72/0.56 % (3287936)Instruction limit reached!
% 1.72/0.56 % (3287936)------------------------------
% 1.72/0.56 % (3287936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.72/0.56 % (3287936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.72/0.56 % (3287936)CaDiCaL version: 2.1.3
% 1.72/0.56 % (3287936)Termination reason: Instruction limit
% 1.72/0.56 % (3287936)Termination phase: Saturation
% 1.72/0.56 % (3287936)Time elapsed: 0.014 s
% 1.72/0.56 % (3287936)Peak memory usage: 12 MB
% 1.72/0.56 % (3287936)Instructions burned: 26 (million)
% 1.72/0.56 % (3287942)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=1564369926:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.72/0.56 % (3287942)Instruction limit reached!
% 1.72/0.56 % (3287942)------------------------------
% 1.72/0.56 % (3287942)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.72/0.56 % (3287942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.72/0.56 % (3287942)CaDiCaL version: 2.1.3
% 1.72/0.56 % (3287942)Termination reason: Instruction limit
% 1.72/0.56 % (3287942)Termination phase: Property scanning
% 1.72/0.56 % (3287942)Time elapsed: 0.005 s
% 1.72/0.56 % (3287942)Peak memory usage: 10 MB
% 1.72/0.56 % (3287942)Instructions burned: 9 (million)
% 1.72/0.56 % (3287946)Instruction limit reached!
% 1.72/0.56 % (3287946)------------------------------
% 1.72/0.56 % (3287946)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.72/0.56 % (3287946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.72/0.56 % (3287946)CaDiCaL version: 2.1.3
% 1.72/0.56 % (3287946)Termination reason: Instruction limit
% 1.72/0.56 % (3287946)Termination phase: Saturation
% 1.72/0.56 % (3287946)Time elapsed: 0.010 s
% 1.72/0.56 % (3287946)Peak memory usage: 12 MB
% 1.72/0.56 % (3287946)Instructions burned: 32 (million)
% 1.72/0.56 % (3287953)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=1932926993:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 1.72/0.56 % (3287949)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=934566111:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 1.72/0.56 % (3287951)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=2772214573:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.72/0.56 % (3287938)Instruction limit reached!
% 2.33/0.62 % (3287938)------------------------------
% 2.33/0.62 % (3287938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.33/0.62 % (3287938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.33/0.62 % (3287938)CaDiCaL version: 2.1.3
% 2.33/0.62 % (3287938)Termination reason: Instruction limit
% 2.33/0.62 % (3287938)Termination phase: Saturation
% 2.33/0.62 % (3287938)Time elapsed: 0.040 s
% 2.33/0.62 % (3287938)Peak memory usage: 12 MB
% 2.33/0.62 % (3287938)Instructions burned: 60 (million)
% 2.33/0.62 % (3287949)Instruction limit reached!
% 2.33/0.62 % (3287949)------------------------------
% 2.33/0.62 % (3287949)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.33/0.62 % (3287949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.33/0.62 % (3287949)CaDiCaL version: 2.1.3
% 2.33/0.62 % (3287949)Termination reason: Instruction limit
% 2.33/0.62 % (3287949)Termination phase: Property scanning
% 2.33/0.62 % (3287949)Time elapsed: 0.004 s
% 2.33/0.62 % (3287949)Peak memory usage: 10 MB
% 2.33/0.62 % (3287949)Instructions burned: 7 (million)
% 2.33/0.62 % (3287952)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=2933656796:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 2.33/0.62 % (3287951)Instruction limit reached!
% 2.33/0.62 % (3287951)------------------------------
% 2.33/0.62 % (3287951)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.33/0.62 % (3287951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.33/0.62 % (3287951)CaDiCaL version: 2.1.3
% 2.33/0.62 % (3287951)Termination reason: Instruction limit
% 2.33/0.62 % (3287951)Termination phase: Saturation
% 2.33/0.62 % (3287951)Time elapsed: 0.011 s
% 2.33/0.62 % (3287951)Peak memory usage: 11 MB
% 2.33/0.62 % (3287951)Instructions burned: 25 (million)
% 2.33/0.62 % (3287957)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=588258295:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/143Mi)
% 2.33/0.62 % (3287958)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=2434494539:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/193Mi)
% 2.33/0.62 % (3287952)Instruction limit reached!
% 2.33/0.62 % (3287952)------------------------------
% 2.33/0.62 % (3287952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.33/0.62 % (3287952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.33/0.62 % (3287952)CaDiCaL version: 2.1.3
% 2.33/0.62 % (3287952)Termination reason: Instruction limit
% 2.33/0.62 % (3287952)Termination phase: Saturation
% 2.33/0.62 % (3287952)Time elapsed: 0.017 s
% 2.33/0.62 % (3287952)Peak memory usage: 12 MB
% 2.33/0.62 % (3287952)Instructions burned: 20 (million)
% 2.33/0.62 % (3287960)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=4139466647:i=42:hud=10:rtra=on_2997 on theBenchmark for (2997ds/42Mi)
% 2.33/0.62 % (3287963)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 2.33/0.62 % (3287963)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3999643847:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2997 on theBenchmark for (2997ds/7Mi)
% 2.33/0.62 % (3287963)Instruction limit reached!
% 2.33/0.62 % (3287963)------------------------------
% 2.33/0.62 % (3287963)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.33/0.62 % (3287963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.33/0.62 % (3287963)CaDiCaL version: 2.1.3
% 2.33/0.62 % (3287963)Termination reason: Instruction limit
% 2.33/0.62 % (3287963)Termination phase: Property scanning
% 2.33/0.62 % (3287963)Time elapsed: 0.004 s
% 2.33/0.62 % (3287963)Peak memory usage: 10 MB
% 2.33/0.62 % (3287963)Instructions burned: 7 (million)
% 2.33/0.62 % (3287960)Instruction limit reached!
% 2.33/0.62 % (3287960)------------------------------
% 2.33/0.62 % (3287960)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.33/0.62 % (3287960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.33/0.62 % (3287960)CaDiCaL version: 2.1.3
% 2.33/0.62 % (3287960)Termination reason: Instruction limit
% 2.33/0.62 % (3287960)Termination phase: Saturation
% 2.33/0.62 % (3287960)Time elapsed: 0.021 s
% 2.33/0.62 % (3287960)Peak memory usage: 12 MB
% 2.33/0.62 % (3287960)Instructions burned: 43 (million)
% 2.87/0.71 % (3287966)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=626079707:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/181Mi)
% 2.87/0.71 % (3287967)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=2403064241:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2997 on theBenchmark for (2997ds/169Mi)
% 2.87/0.71 % (3287967)Refutation not found, incomplete strategy
% 2.87/0.71 % (3287967)------------------------------
% 2.87/0.71 % (3287967)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.87/0.71 % (3287967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.87/0.71 % (3287967)CaDiCaL version: 2.1.3
% 2.87/0.71 % (3287967)Termination reason: Refutation not found, incomplete strategy
% 2.87/0.71 % (3287967)Time elapsed: 0.009 s
% 2.87/0.71 % (3287967)Peak memory usage: 12 MB
% 2.87/0.71 % (3287967)Instructions burned: 16 (million)
% 2.87/0.71 % (3287967)------------------------------
% 2.87/0.71 % (3287967)------------------------------
% 2.87/0.71 % (3287957)Instruction limit reached!
% 2.87/0.71 % (3287957)------------------------------
% 2.87/0.71 % (3287957)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.87/0.71 % (3287957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.87/0.71 % (3287957)CaDiCaL version: 2.1.3
% 2.87/0.71 % (3287957)Termination reason: Instruction limit
% 2.87/0.71 % (3287957)Termination phase: Saturation
% 2.87/0.71 % (3287957)Time elapsed: 0.069 s
% 2.87/0.71 % (3287957)Peak memory usage: 12 MB
% 2.87/0.71 % (3287957)Instructions burned: 144 (million)
% 2.87/0.71 % (3287970)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 2.87/0.71 % (3287970)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=2212348781:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2997 on theBenchmark for (2997ds/6Mi)
% 2.87/0.71 % (3287970)Instruction limit reached!
% 2.87/0.71 % (3287970)------------------------------
% 2.87/0.71 % (3287970)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.87/0.71 % (3287970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.87/0.71 % (3287970)CaDiCaL version: 2.1.3
% 2.87/0.71 % (3287970)Termination reason: Instruction limit
% 2.87/0.71 % (3287970)Termination phase: SInE selection
% 2.87/0.71 % (3287970)Time elapsed: 0.003 s
% 2.87/0.71 % (3287970)Peak memory usage: 10 MB
% 2.87/0.71 % (3287970)Instructions burned: 6 (million)
% 2.87/0.71 % (3287971)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=1387197739:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2997 on theBenchmark for (2997ds/22Mi)
% 2.87/0.71 % (3287958)Instruction limit reached!
% 2.87/0.71 % (3287958)------------------------------
% 2.87/0.71 % (3287958)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.87/0.71 % (3287958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.87/0.71 % (3287958)CaDiCaL version: 2.1.3
% 2.87/0.71 % (3287958)Termination reason: Instruction limit
% 2.87/0.71 % (3287958)Termination phase: Saturation
% 2.87/0.71 % (3287958)Time elapsed: 0.097 s
% 2.87/0.71 % (3287958)Peak memory usage: 13 MB
% 2.87/0.71 % (3287958)Instructions burned: 200 (million)
% 2.87/0.71 % (3287971)Instruction limit reached!
% 2.87/0.71 % (3287971)------------------------------
% 2.87/0.71 % (3287971)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.87/0.71 % (3287971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.87/0.71 % (3287971)CaDiCaL version: 2.1.3
% 2.87/0.71 % (3287971)Termination reason: Instruction limit
% 2.87/0.71 % (3287971)Termination phase: Saturation
% 2.87/0.71 % (3287971)Time elapsed: 0.011 s
% 2.87/0.71 % (3287971)Peak memory usage: 12 MB
% 2.87/0.71 % (3287971)Instructions burned: 23 (million)
% 2.87/0.71 % (3287973)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=2564649886:i=19:add=on:rtra=on_2997 on theBenchmark for (2997ds/19Mi)
% 2.87/0.71 % (3287973)Refutation not found, incomplete strategy
% 2.87/0.71 % (3287973)------------------------------
% 2.87/0.71 % (3287973)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.87/0.71 % (3287973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.87/0.76 % (3287973)CaDiCaL version: 2.1.3
% 2.87/0.76 % (3287973)Termination reason: Refutation not found, incomplete strategy
% 2.87/0.76 % (3287973)Time elapsed: 0.007 s
% 2.87/0.76 % (3287973)Peak memory usage: 12 MB
% 2.87/0.76 % (3287973)Instructions burned: 13 (million)
% 2.87/0.76 % (3287973)------------------------------
% 2.87/0.76 % (3287973)------------------------------
% 2.87/0.76 % (3287975)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=2236523791:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/316Mi)
% 2.87/0.76 % (3287976)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=3979777708:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2996 on theBenchmark for (2996ds/853Mi)
% 2.87/0.76 % (3287978)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=4251501547:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2996 on theBenchmark for (2996ds/45Mi)
% 2.87/0.76 % (3287897)Instruction limit reached!
% 2.87/0.76 % (3287897)------------------------------
% 2.87/0.76 % (3287897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.87/0.76 % (3287897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.87/0.76 % (3287897)CaDiCaL version: 2.1.3
% 2.87/0.76 % (3287897)Termination reason: Instruction limit
% 2.87/0.76 % (3287897)Termination phase: Saturation
% 2.87/0.76 % (3287897)Time elapsed: 0.324 s
% 2.87/0.76 % (3287897)Peak memory usage: 14 MB
% 2.87/0.76 % (3287897)Instructions burned: 635 (million)
% 2.87/0.76 % (3287966)Instruction limit reached!
% 2.87/0.76 % (3287966)------------------------------
% 2.87/0.76 % (3287966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.87/0.76 % (3287966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.87/0.76 % (3287966)CaDiCaL version: 2.1.3
% 2.87/0.76 % (3287966)Termination reason: Instruction limit
% 2.87/0.76 % (3287966)Termination phase: Saturation
% 2.87/0.76 % (3287966)Time elapsed: 0.097 s
% 2.87/0.76 % (3287966)Peak memory usage: 14 MB
% 2.87/0.76 % (3287966)Instructions burned: 183 (million)
% 2.87/0.76 % (3287978)Instruction limit reached!
% 2.87/0.76 % (3287978)------------------------------
% 2.87/0.76 % (3287978)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.87/0.76 % (3287978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.87/0.76 % (3287978)CaDiCaL version: 2.1.3
% 2.87/0.76 % (3287978)Termination reason: Instruction limit
% 2.87/0.76 % (3287978)Termination phase: Saturation
% 2.87/0.76 % (3287978)Time elapsed: 0.025 s
% 2.87/0.76 % (3287978)Peak memory usage: 12 MB
% 2.87/0.76 % (3287978)Instructions burned: 45 (million)
% 2.87/0.76 % (3287983)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=2285311371:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2996 on theBenchmark for (2996ds/21Mi)
% 2.87/0.76 % (3287982)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=192105399:i=480:rtra=on_2996 on theBenchmark for (2996ds/480Mi)
% 2.87/0.76 % (3287984)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 2.87/0.76 % (3287982)Refutation not found, incomplete strategy
% 2.87/0.76 % (3287982)------------------------------
% 2.87/0.76 % (3287982)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.87/0.76 % (3287982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.87/0.76 % (3287982)CaDiCaL version: 2.1.3
% 2.87/0.76 % (3287982)Termination reason: Refutation not found, incomplete strategy
% 2.87/0.76 % (3287982)Time elapsed: 0.009 s
% 2.87/0.76 % (3287982)Peak memory usage: 12 MB
% 2.87/0.76 % (3287982)Instructions burned: 17 (million)
% 2.87/0.76 % (3287982)------------------------------
% 2.87/0.76 % (3287982)------------------------------
% 2.87/0.76 % (3287983)Instruction limit reached!
% 2.87/0.76 % (3287983)------------------------------
% 2.87/0.76 % (3287983)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.87/0.76 % (3287983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.42/0.81 % (3287983)CaDiCaL version: 2.1.3
% 3.42/0.81 % (3287983)Termination reason: Instruction limit
% 3.42/0.81 % (3287983)Termination phase: Saturation
% 3.42/0.81 % (3287984)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=1710198:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/200Mi)
% 3.42/0.81 % (3287983)Time elapsed: 0.012 s
% 3.42/0.81 % (3287983)Peak memory usage: 12 MB
% 3.42/0.81 % (3287983)Instructions burned: 23 (million)
% 3.42/0.81 % (3287987)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=3642737158:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2996 on theBenchmark for (2996ds/13Mi)
% 3.42/0.81 % (3287989)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=3810833633:i=66:s2at=3:nm=2:rtra=on:rawr=on_2996 on theBenchmark for (2996ds/66Mi)
% 3.42/0.81 % (3287987)Instruction limit reached!
% 3.42/0.81 % (3287987)------------------------------
% 3.42/0.81 % (3287987)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.42/0.81 % (3287987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.42/0.81 % (3287987)CaDiCaL version: 2.1.3
% 3.42/0.81 % (3287987)Termination reason: Instruction limit
% 3.42/0.81 % (3287987)Termination phase: Saturation
% 3.42/0.81 % (3287987)Time elapsed: 0.006 s
% 3.42/0.81 % (3287987)Peak memory usage: 12 MB
% 3.42/0.81 % (3287987)Instructions burned: 13 (million)
% 3.42/0.81 % (3287931)Instruction limit reached!
% 3.42/0.81 % (3287931)------------------------------
% 3.42/0.81 % (3287931)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.42/0.81 % (3287931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.42/0.81 % (3287931)CaDiCaL version: 2.1.3
% 3.42/0.81 % (3287931)Termination reason: Instruction limit
% 3.42/0.81 % (3287931)Termination phase: Saturation
% 3.42/0.81 % (3287931)Time elapsed: 0.280 s
% 3.42/0.81 % (3287931)Peak memory usage: 14 MB
% 3.42/0.81 % (3287931)Instructions burned: 328 (million)
% 3.42/0.81 % (3287992)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=3774330279:i=51:fsr=off:rtra=on_2995 on theBenchmark for (2995ds/51Mi)
% 3.42/0.81 % (3287993)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=3081050060:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/31Mi)
% 3.42/0.81 % (3287989)Instruction limit reached!
% 3.42/0.81 % (3287989)------------------------------
% 3.42/0.81 % (3287989)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.42/0.81 % (3287989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.42/0.81 % (3287989)CaDiCaL version: 2.1.3
% 3.42/0.81 % (3287989)Termination reason: Instruction limit
% 3.42/0.81 % (3287989)Termination phase: Saturation
% 3.42/0.81 % (3287989)Time elapsed: 0.033 s
% 3.42/0.81 % (3287989)Peak memory usage: 13 MB
% 3.42/0.81 % (3287989)Instructions burned: 67 (million)
% 3.42/0.81 % (3287993)Instruction limit reached!
% 3.42/0.81 % (3287993)------------------------------
% 3.42/0.81 % (3287993)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.42/0.81 % (3287993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.42/0.81 % (3287993)CaDiCaL version: 2.1.3
% 3.42/0.81 % (3287993)Termination reason: Instruction limit
% 3.42/0.81 % (3287993)Termination phase: Saturation
% 3.42/0.81 % (3287993)Time elapsed: 0.016 s
% 3.42/0.81 % (3287993)Peak memory usage: 12 MB
% 3.42/0.81 % (3287993)Instructions burned: 32 (million)
% 3.42/0.81 % (3287992)Instruction limit reached!
% 3.42/0.81 % (3287992)------------------------------
% 3.42/0.81 % (3287992)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.42/0.81 % (3287992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.42/0.81 % (3287992)CaDiCaL version: 2.1.3
% 3.42/0.81 % (3287992)Termination reason: Instruction limit
% 3.42/0.81 % (3287992)Termination phase: Saturation
% 3.42/0.81 % (3287992)Time elapsed: 0.026 s
% 3.42/0.81 % (3287992)Peak memory usage: 12 MB
% 3.42/0.81 % (3287992)Instructions burned: 52 (million)
% 3.42/0.81 % (3287996)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=3131581488:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2995 on theBenchmark for (2995ds/137Mi)
% 3.42/0.81 % (3287997)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=2722326272:cond=on:i=34:hud=10:nm=10:rtra=on_2995 on theBenchmark for (2995ds/34Mi)
% 3.42/0.81 % (3287998)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=3238318793:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2995 on theBenchmark for (2995ds/67Mi)
% 3.42/0.81 % (3287984)Instruction limit reached!
% 3.42/0.81 % (3287984)------------------------------
% 3.42/0.81 % (3287984)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.42/0.81 % (3287984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.42/0.81 % (3287984)CaDiCaL version: 2.1.3
% 3.42/0.81 % (3287984)Termination reason: Instruction limit
% 3.42/0.81 % (3287984)Termination phase: Saturation
% 3.42/0.81 % (3287984)Time elapsed: 0.091 s
% 3.42/0.81 % (3287984)Peak memory usage: 12 MB
% 3.42/0.81 % (3287984)Instructions burned: 202 (million)
% 3.42/0.81 % (3288002)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 3.42/0.81 % (3287997)Instruction limit reached!
% 3.42/0.81 % (3287997)------------------------------
% 3.42/0.81 % (3287997)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.42/0.81 % (3287997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.42/0.81 % (3287997)CaDiCaL version: 2.1.3
% 3.42/0.81 % (3287997)Termination reason: Instruction limit
% 3.42/0.81 % (3287997)Termination phase: Saturation
% 3.42/0.81 % (3287997)Time elapsed: 0.019 s
% 3.42/0.81 % (3287997)Peak memory usage: 12 MB
% 3.42/0.81 % (3287997)Instructions burned: 35 (million)
% 3.42/0.81 % (3287975)Instruction limit reached!
% 3.42/0.81 % (3287975)------------------------------
% 3.42/0.81 % (3287975)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.42/0.81 % (3287975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.42/0.81 % (3287975)CaDiCaL version: 2.1.3
% 3.42/0.81 % (3287975)Termination reason: Instruction limit
% 3.42/0.81 % (3287975)Termination phase: Saturation
% 3.42/0.81 % (3287975)Time elapsed: 0.169 s
% 3.42/0.81 % (3287975)Peak memory usage: 16 MB
% 3.42/0.81 % (3287975)Instructions burned: 317 (million)
% 3.42/0.81 % (3287953)Instruction limit reached!
% 3.42/0.81 % (3287953)------------------------------
% 3.42/0.81 % (3287953)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.42/0.81 % (3287953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.42/0.81 % (3287953)CaDiCaL version: 2.1.3
% 3.42/0.81 % (3287953)Termination reason: Instruction limit
% 3.42/0.81 % (3287953)Termination phase: Saturation
% 3.42/0.81 % (3287953)Time elapsed: 0.313 s
% 3.42/0.81 % (3287953)Peak memory usage: 17 MB
% 3.42/0.81 % (3287953)Instructions burned: 1244 (million)
% 3.42/0.81 % (3288002)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=1856310456:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2995 on theBenchmark for (2995ds/180Mi)
% 3.42/0.81 % (3288006)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=919444165:i=427:sd=1:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/427Mi)
% 3.42/0.81 % (3287998)Instruction limit reached!
% 3.42/0.81 % (3287998)------------------------------
% 3.42/0.81 % (3287998)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.42/0.81 % (3287998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.42/0.81 % (3287998)CaDiCaL version: 2.1.3
% 3.42/0.81 % (3287998)Termination reason: Instruction limit
% 3.42/0.81 % (3287998)Termination phase: Saturation
% 3.42/0.81 % (3287998)Time elapsed: 0.037 s
% 3.42/0.81 % (3287998)Peak memory usage: 12 MB
% 3.42/0.81 % (3287998)Instructions burned: 68 (million)
% 3.42/0.81 % (3288003)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=358007075:st=2:i=246:sd=3:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/246Mi)
% 3.42/0.81 % (3288004)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=678914101:cond=on:i=96:bd=all:rtra=on_2995 on theBenchmark for (2995ds/96Mi)
% 3.42/0.81 % (3287996)Instruction limit reached!
% 3.42/0.81 % (3287996)------------------------------
% 3.42/0.81 % (3287996)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.42/0.81 % (3287996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.42/0.81 % (3287996)CaDiCaL version: 2.1.3
% 3.42/0.81 % (3287996)Termination reason: Instruction limit
% 3.42/0.81 % (3287996)Termination phase: Saturation
% 3.42/0.81 % (3287996)Time elapsed: 0.067 s
% 3.42/0.81 % (3287996)Peak memory usage: 12 MB
% 3.42/0.81 % (3287996)Instructions burned: 137 (million)
% 3.42/0.81 % (3288008)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=1735426333:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/874Mi)
% 3.42/0.81 % (3288011)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=4289293919:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/515Mi)
% 3.42/0.81 % (3288003) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3287889-3288003"...
% 3.42/0.81 % (3288004)Instruction limit reached!
% 3.42/0.81 % (3288004)------------------------------
% 3.42/0.81 % (3288004)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.42/0.81 % (3288004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.42/0.81 % (3288004)CaDiCaL version: 2.1.3
% 3.42/0.81 % (3288004)Termination reason: Instruction limit
% 3.42/0.81 % (3288004)Termination phase: Saturation
% 3.42/0.81 % (3288004)Time elapsed: 0.049 s
% 3.42/0.81 % (3288004)Peak memory usage: 12 MB
% 3.42/0.81 % (3288004)Instructions burned: 98 (million)
% 3.42/0.81 % (3288003)...printing done.
% 3.42/0.81 % (3288003)Refutation found. Thanks to Tanya!
% 3.42/0.81 % SZS status Theorem for theBenchmark
% 3.42/0.81 % SZS output start Proof for theBenchmark
% 3.42/0.81 thf(type_def_5, type, del: $tType).
% 3.42/0.81 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 3.42/0.81 thf(func_def_0, type, bool: del).
% 3.42/0.81 thf(func_def_1, type, ind: del).
% 3.42/0.81 thf(func_def_2, type, arr: (del > del > del)).
% 3.42/0.81 thf(func_def_3, type, mem: ($i > del > $o)).
% 3.42/0.81 thf(func_def_4, type, ap: ($i > $i > $i)).
% 3.42/0.81 thf(func_def_5, type, lam: (del > ($i > $i) > $i)).
% 3.42/0.81 thf(func_def_6, type, p: ($i > $o)).
% 3.42/0.81 thf(func_def_7, type, inj__o: ($o > $i)).
% 3.42/0.81 thf(func_def_10, type, c_2Epred__set_2ESUBSET: (del > $i)).
% 3.42/0.81 thf(func_def_13, type, c_2Ebool_2EIN: (del > $i)).
% 3.42/0.81 thf(func_def_14, type, c_2Epred__set_2ECHOICE: (del > $i)).
% 3.42/0.81 thf(func_def_15, type, c_2Epred__set_2EDELETE: (del > $i)).
% 3.42/0.81 thf(func_def_16, type, c_2Epred__set_2EREST: (del > $i)).
% 3.42/0.81 thf(func_def_17, type, c_2Emin_2E_3D: (del > $i)).
% 3.42/0.81 thf(func_def_18, type, c_2Ebool_2E_21: (del > $i)).
% 3.42/0.81 thf(func_def_21, type, sK0: del).
% 3.42/0.81 thf(func_def_23, type, sK2: ($i > $i > del > $i)).
% 3.42/0.81 thf(func_def_24, type, sK3: ($i > $i > del > $i)).
% 3.42/0.81 thf(func_def_25, type, vNOT: ($o > $o)).
% 3.42/0.81 thf(f4,axiom,(
% 3.42/0.81 ! [X1 : del,X0 : del,X2 : $i] : ((mem @ X2 @ (arr @ X0 @ X1)) => ! [X3 : $i] : ((mem @ X3 @ X0) => (mem @ (ap @ X2 @ X3) @ X1)))),
% 3.42/0.81 file('/export/starexec/sandbox/benchmark/Axioms/ITP001/ITP001^2.ax',ap_tp)).
% 3.42/0.81 thf(f16,axiom,(
% 3.42/0.81 ! [X0 : del] : (mem @ (c_2Epred__set_2ECHOICE @ X0) @ (arr @ (arr @ X0 @ bool) @ X0))),
% 3.42/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Epred__set_2ECHOICE)).
% 3.42/0.81 thf(f17,axiom,(
% 3.42/0.81 ! [X0 : del] : (mem @ (c_2Epred__set_2EDELETE @ X0) @ (arr @ (arr @ X0 @ bool) @ (arr @ X0 @ (arr @ X0 @ bool))))),
% 3.42/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Epred__set_2EDELETE)).
% 3.42/0.81 thf(f23,axiom,(
% 3.42/0.81 ! [X0 : del,X1 : $i] : ((mem @ X1 @ (arr @ X0 @ bool)) => ! [X2 : $i] : ((mem @ X2 @ (arr @ X0 @ bool)) => (! [X3 : $i] : ((mem @ X3 @ X0) => ((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ X3) @ X1)) => (p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ X3) @ X2)))) <=> (p @ (ap @ (ap @ (c_2Epred__set_2ESUBSET @ X0) @ X1) @ X2)))))),
% 3.42/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_thm_2Epred__set_2ESUBSET__DEF)).
% 3.42/0.81 thf(f24,axiom,(
% 3.42/0.81 ! [X0 : del,X1 : $i] : ((mem @ X1 @ (arr @ X0 @ bool)) => ! [X2 : $i] : ((mem @ X2 @ X0) => ! [X3 : $i] : ((mem @ X3 @ X0) => ((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ X2) @ (ap @ (ap @ (c_2Epred__set_2EDELETE @ X0) @ X1) @ X3))) <=> ((X2 != X3) & (p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ X2) @ X1)))))))),
% 3.42/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2Epred__set_2EIN__DELETE)).
% 3.42/0.81 thf(f25,axiom,(
% 3.42/0.81 ! [X0 : del,X1 : $i] : ((mem @ X1 @ (arr @ X0 @ bool)) => (((ap @ (c_2Epred__set_2EREST @ X0) @ X1)) = ((ap @ (ap @ (c_2Epred__set_2EDELETE @ X0) @ X1) @ (ap @ (c_2Epred__set_2ECHOICE @ X0) @ X1)))))),
% 3.42/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_thm_2Epred__set_2EREST__DEF)).
% 3.42/0.81 thf(f26,conjecture,(
% 3.42/0.81 ! [X1 : $i,X0 : del] : ((mem @ X1 @ (arr @ X0 @ bool)) => (p @ (ap @ (ap @ (c_2Epred__set_2ESUBSET @ X0) @ (ap @ (c_2Epred__set_2EREST @ X0) @ X1)) @ X1)))),
% 3.42/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2Epred__set_2EREST__SUBSET)).
% 3.42/0.81 thf(f27,negated_conjecture,(
% 3.42/0.81 ~ ! [X1 : $i,X0 : del] : ((mem @ X1 @ (arr @ X0 @ bool)) => (p @ (ap @ (ap @ (c_2Epred__set_2ESUBSET @ X0) @ (ap @ (c_2Epred__set_2EREST @ X0) @ X1)) @ X1)))),
% 3.42/0.81 inference(negated_conjecture,[status(cth)],[f26])).
% 3.42/0.81 thf(f50,plain,(
% 3.42/0.81 ! [X0 : del,X1 : $i] : ((mem @ X1 @ (arr @ X0 @ bool)) => (((ap @ (c_2Epred__set_2EREST @ X0) @ X1)) = ((ap @ (ap @ (c_2Epred__set_2EDELETE @ X0) @ X1) @ (ap @ (c_2Epred__set_2ECHOICE @ X0) @ X1)))))),
% 3.42/0.81 inference(rectify,[],[f25])).
% 3.42/0.81 thf(f51,plain,(
% 3.42/0.81 ! [X0 : del,X1 : $i] : ((((mem @ X1 @ (arr @ X0 @ bool))) = $true) => (((ap @ (c_2Epred__set_2EREST @ X0) @ X1)) = ((ap @ (ap @ (c_2Epred__set_2EDELETE @ X0) @ X1) @ (ap @ (c_2Epred__set_2ECHOICE @ X0) @ X1)))))),
% 3.42/0.81 inference(fool_elimination,[],[f50])).
% 3.42/0.81 thf(f52,plain,(
% 3.42/0.81 ! [X0 : del] : (mem @ (c_2Epred__set_2EDELETE @ X0) @ (arr @ (arr @ X0 @ bool) @ (arr @ X0 @ (arr @ X0 @ bool))))),
% 3.42/0.81 inference(rectify,[],[f17])).
% 3.42/0.81 thf(f53,plain,(
% 3.42/0.81 ! [X0 : del] : (((mem @ (c_2Epred__set_2EDELETE @ X0) @ (arr @ (arr @ X0 @ bool) @ (arr @ X0 @ (arr @ X0 @ bool))))) = $true)),
% 3.42/0.81 inference(fool_elimination,[],[f52])).
% 3.42/0.81 thf(f64,plain,(
% 3.42/0.81 ! [X0 : del,X1 : $i] : ((mem @ X1 @ (arr @ X0 @ bool)) => ! [X2 : $i] : ((mem @ X2 @ X0) => ! [X3 : $i] : ((mem @ X3 @ X0) => ((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ X2) @ (ap @ (ap @ (c_2Epred__set_2EDELETE @ X0) @ X1) @ X3))) <=> ((X2 != X3) & (p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ X2) @ X1)))))))),
% 3.42/0.81 inference(rectify,[],[f24])).
% 3.42/0.81 thf(f65,plain,(
% 3.42/0.81 ! [X0 : del,X1 : $i] : ((((mem @ X1 @ (arr @ X0 @ bool))) = $true) => ! [X2 : $i] : ((((mem @ X2 @ X0)) = $true) => ! [X3 : $i] : ((((mem @ X3 @ X0)) = $true) => ((((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ X2) @ (ap @ (ap @ (c_2Epred__set_2EDELETE @ X0) @ X1) @ X3)))) = $true) <=> ((((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ X2) @ X1))) = $true) & (X2 != X3))))))),
% 3.42/0.81 inference(fool_elimination,[],[f64])).
% 3.42/0.81 thf(f66,plain,(
% 3.42/0.81 ! [X0 : del,X1 : del,X2 : $i] : ((mem @ X2 @ (arr @ X1 @ X0)) => ! [X3 : $i] : ((mem @ X3 @ X1) => (mem @ (ap @ X2 @ X3) @ X0)))),
% 3.42/0.81 inference(rectify,[],[f4])).
% 3.42/0.81 thf(f67,plain,(
% 3.42/0.81 ! [X0 : del,X1 : del,X2 : $i] : ((((mem @ X2 @ (arr @ X1 @ X0))) = $true) => ! [X3 : $i] : ((((mem @ X3 @ X1)) = $true) => (((mem @ (ap @ X2 @ X3) @ X0)) = $true)))),
% 3.42/0.81 inference(fool_elimination,[],[f66])).
% 3.42/0.81 thf(f68,plain,(
% 3.42/0.81 ~ ! [X0 : $i,X1 : del] : ((mem @ X0 @ (arr @ X1 @ bool)) => (p @ (ap @ (ap @ (c_2Epred__set_2ESUBSET @ X1) @ (ap @ (c_2Epred__set_2EREST @ X1) @ X0)) @ X0)))),
% 3.42/0.81 inference(rectify,[],[f27])).
% 3.42/0.81 thf(f69,plain,(
% 3.42/0.81 ~ ! [X1 : del,X0 : $i] : ((((mem @ X0 @ (arr @ X1 @ bool))) = $true) => (((p @ (ap @ (ap @ (c_2Epred__set_2ESUBSET @ X1) @ (ap @ (c_2Epred__set_2EREST @ X1) @ X0)) @ X0))) = $true))),
% 3.42/0.81 inference(fool_elimination,[],[f68])).
% 3.42/0.81 thf(f70,plain,(
% 3.42/0.81 ! [X0 : del] : (mem @ (c_2Epred__set_2ECHOICE @ X0) @ (arr @ (arr @ X0 @ bool) @ X0))),
% 3.42/0.81 inference(rectify,[],[f16])).
% 3.42/0.81 thf(f71,plain,(
% 3.42/0.81 ! [X0 : del] : (((mem @ (c_2Epred__set_2ECHOICE @ X0) @ (arr @ (arr @ X0 @ bool) @ X0))) = $true)),
% 3.42/0.81 inference(fool_elimination,[],[f70])).
% 3.42/0.81 thf(f76,plain,(
% 3.42/0.81 ! [X0 : del,X1 : $i] : ((mem @ X1 @ (arr @ X0 @ bool)) => ! [X2 : $i] : ((mem @ X2 @ (arr @ X0 @ bool)) => (! [X3 : $i] : ((mem @ X3 @ X0) => ((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ X3) @ X1)) => (p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ X3) @ X2)))) <=> (p @ (ap @ (ap @ (c_2Epred__set_2ESUBSET @ X0) @ X1) @ X2)))))),
% 3.42/0.81 inference(rectify,[],[f23])).
% 3.42/0.81 thf(f77,plain,(
% 3.42/0.81 ! [X0 : del,X1 : $i] : ((((mem @ X1 @ (arr @ X0 @ bool))) = $true) => ! [X2 : $i] : ((((mem @ X2 @ (arr @ X0 @ bool))) = $true) => (! [X3 : $i] : ((((mem @ X3 @ X0)) = $true) => ((((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ X3) @ X1))) = $true) => (((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ X3) @ X2))) = $true))) <=> (((p @ (ap @ (ap @ (c_2Epred__set_2ESUBSET @ X0) @ X1) @ X2))) = $true))))),
% 3.42/0.81 inference(fool_elimination,[],[f76])).
% 3.42/0.81 thf(f78,plain,(
% 3.42/0.81 ? [X1 : del,X0 : $i] : ((((mem @ X0 @ (arr @ X1 @ bool))) = $true) & (((p @ (ap @ (ap @ (c_2Epred__set_2ESUBSET @ X1) @ (ap @ (c_2Epred__set_2EREST @ X1) @ X0)) @ X0))) != $true))),
% 3.42/0.81 inference(ennf_transformation,[],[f69])).
% 3.42/0.81 thf(f79,plain,(
% 3.42/0.81 ! [X1 : $i,X0 : del] : ((((ap @ (c_2Epred__set_2EREST @ X0) @ X1)) = ((ap @ (ap @ (c_2Epred__set_2EDELETE @ X0) @ X1) @ (ap @ (c_2Epred__set_2ECHOICE @ X0) @ X1)))) | (((mem @ X1 @ (arr @ X0 @ bool))) != $true))),
% 3.42/0.81 inference(ennf_transformation,[],[f51])).
% 3.42/0.81 thf(f82,plain,(
% 3.42/0.81 ! [X2 : $i,X0 : del,X1 : del] : ((((mem @ X2 @ (arr @ X1 @ X0))) != $true) | ! [X3 : $i] : ((((mem @ X3 @ X1)) != $true) | (((mem @ (ap @ X2 @ X3) @ X0)) = $true)))),
% 3.42/0.81 inference(ennf_transformation,[],[f67])).
% 3.42/0.81 thf(f83,plain,(
% 3.42/0.81 ! [X0 : del,X1 : $i] : (! [X2 : $i] : ((! [X3 : $i] : (((((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ X3) @ X2))) = $true) | (((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ X3) @ X1))) != $true)) | (((mem @ X3 @ X0)) != $true)) <=> (((p @ (ap @ (ap @ (c_2Epred__set_2ESUBSET @ X0) @ X1) @ X2))) = $true)) | (((mem @ X2 @ (arr @ X0 @ bool))) != $true)) | (((mem @ X1 @ (arr @ X0 @ bool))) != $true))),
% 3.42/0.81 inference(ennf_transformation,[],[f77])).
% 3.42/0.81 thf(f84,plain,(
% 3.42/0.81 ! [X0 : del,X1 : $i] : (! [X2 : $i] : ((((mem @ X2 @ (arr @ X0 @ bool))) != $true) | ((((p @ (ap @ (ap @ (c_2Epred__set_2ESUBSET @ X0) @ X1) @ X2))) = $true) <=> ! [X3 : $i] : ((((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ X3) @ X2))) = $true) | (((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ X3) @ X1))) != $true) | (((mem @ X3 @ X0)) != $true)))) | (((mem @ X1 @ (arr @ X0 @ bool))) != $true))),
% 3.42/0.81 inference(flattening,[],[f83])).
% 3.42/0.81 thf(f85,plain,(
% 3.42/0.81 ! [X0 : del,X1 : $i] : (! [X2 : $i] : ((((mem @ X2 @ X0)) != $true) | ! [X3 : $i] : ((((mem @ X3 @ X0)) != $true) | ((((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ X2) @ (ap @ (ap @ (c_2Epred__set_2EDELETE @ X0) @ X1) @ X3)))) = $true) <=> ((((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ X2) @ X1))) = $true) & (X2 != X3))))) | (((mem @ X1 @ (arr @ X0 @ bool))) != $true))),
% 3.42/0.81 inference(ennf_transformation,[],[f65])).
% 3.42/0.81 thf(f86,plain,(
% 3.42/0.81 ! [X0 : del,X1 : $i] : (! [X2 : $i] : ((((mem @ X2 @ X0)) != $true) | ! [X3 : $i] : ((((mem @ X3 @ X0)) != $true) | (((((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ X2) @ (ap @ (ap @ (c_2Epred__set_2EDELETE @ X0) @ X1) @ X3)))) = $true) | ((((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ X2) @ X1))) != $true) | (X2 = X3))) & (((((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ X2) @ X1))) = $true) & (X2 != X3)) | (((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ X2) @ (ap @ (ap @ (c_2Epred__set_2EDELETE @ X0) @ X1) @ X3)))) != $true))))) | (((mem @ X1 @ (arr @ X0 @ bool))) != $true))),
% 3.42/0.81 inference(nnf_transformation,[],[f85])).
% 3.42/0.81 thf(f87,plain,(
% 3.42/0.81 ! [X0 : del,X1 : $i] : (! [X2 : $i] : ((((mem @ X2 @ X0)) != $true) | ! [X3 : $i] : ((((mem @ X3 @ X0)) != $true) | (((((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ X2) @ (ap @ (ap @ (c_2Epred__set_2EDELETE @ X0) @ X1) @ X3)))) = $true) | (((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ X2) @ X1))) != $true) | (X2 = X3)) & (((((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ X2) @ X1))) = $true) & (X2 != X3)) | (((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ X2) @ (ap @ (ap @ (c_2Epred__set_2EDELETE @ X0) @ X1) @ X3)))) != $true))))) | (((mem @ X1 @ (arr @ X0 @ bool))) != $true))),
% 3.42/0.81 inference(flattening,[],[f86])).
% 3.42/0.81 thf(f88,plain,(
% 3.42/0.81 ? [X0 : del,X1 : $i] : ((((mem @ X1 @ (arr @ X0 @ bool))) = $true) & (((p @ (ap @ (ap @ (c_2Epred__set_2ESUBSET @ X0) @ (ap @ (c_2Epred__set_2EREST @ X0) @ X1)) @ X1))) != $true))),
% 3.42/0.81 inference(rectify,[],[f78])).
% 3.42/0.81 thf(f89,plain,(
% 3.42/0.81 (((mem @ sK1 @ (arr @ sK0 @ bool))) = $true) & (((p @ (ap @ (ap @ (c_2Epred__set_2ESUBSET @ sK0) @ (ap @ (c_2Epred__set_2EREST @ sK0) @ sK1)) @ sK1))) != $true)),
% 3.42/0.81 inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(X1,sK1)],[f88])).
% 3.42/0.81 thf(f92,plain,(
% 3.42/0.81 ! [X0 : $i,X1 : del] : ((((ap @ (ap @ (c_2Epred__set_2EDELETE @ X1) @ X0) @ (ap @ (c_2Epred__set_2ECHOICE @ X1) @ X0))) = ((ap @ (c_2Epred__set_2EREST @ X1) @ X0))) | (((mem @ X0 @ (arr @ X1 @ bool))) != $true))),
% 3.42/0.81 inference(rectify,[],[f79])).
% 3.42/0.81 thf(f93,plain,(
% 3.42/0.81 ! [X0 : $i,X1 : del,X2 : del] : ((((mem @ X0 @ (arr @ X2 @ X1))) != $true) | ! [X3 : $i] : ((((mem @ X3 @ X2)) != $true) | ($true = ((mem @ (ap @ X0 @ X3) @ X1)))))),
% 3.42/0.81 inference(rectify,[],[f82])).
% 3.42/0.81 thf(f94,plain,(
% 3.42/0.81 ! [X0 : del,X1 : $i] : (! [X2 : $i] : ((((mem @ X2 @ (arr @ X0 @ bool))) != $true) | (((((p @ (ap @ (ap @ (c_2Epred__set_2ESUBSET @ X0) @ X1) @ X2))) = $true) | ? [X3 : $i] : ((((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ X3) @ X2))) != $true) & (((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ X3) @ X1))) = $true) & (((mem @ X3 @ X0)) = $true))) & (! [X3 : $i] : ((((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ X3) @ X2))) = $true) | (((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ X3) @ X1))) != $true) | (((mem @ X3 @ X0)) != $true)) | (((p @ (ap @ (ap @ (c_2Epred__set_2ESUBSET @ X0) @ X1) @ X2))) != $true)))) | (((mem @ X1 @ (arr @ X0 @ bool))) != $true))),
% 3.42/0.81 inference(nnf_transformation,[],[f84])).
% 3.42/0.81 thf(f95,plain,(
% 3.42/0.81 ! [X0 : del,X1 : $i] : (! [X2 : $i] : ((((mem @ X2 @ (arr @ X0 @ bool))) != $true) | (((((p @ (ap @ (ap @ (c_2Epred__set_2ESUBSET @ X0) @ X1) @ X2))) = $true) | ? [X3 : $i] : ((((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ X3) @ X2))) != $true) & (((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ X3) @ X1))) = $true) & (((mem @ X3 @ X0)) = $true))) & (! [X4 : $i] : ((((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ X4) @ X2))) = $true) | (((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ X4) @ X1))) != $true) | (((mem @ X4 @ X0)) != $true)) | (((p @ (ap @ (ap @ (c_2Epred__set_2ESUBSET @ X0) @ X1) @ X2))) != $true)))) | (((mem @ X1 @ (arr @ X0 @ bool))) != $true))),
% 3.42/0.81 inference(rectify,[],[f94])).
% 3.42/0.81 thf(f96,plain,(
% 3.42/0.81 ! [X0 : del,X1 : $i] : (! [X2 : $i] : ((((mem @ X2 @ (arr @ X0 @ bool))) != $true) | (((((p @ (ap @ (ap @ (c_2Epred__set_2ESUBSET @ X0) @ X1) @ X2))) = $true) | (($true != ((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ (sK3 @ X2 @ X1 @ X0)) @ X2)))) & (((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ (sK3 @ X2 @ X1 @ X0)) @ X1))) = $true) & (((mem @ (sK3 @ X2 @ X1 @ X0) @ X0)) = $true))) & (! [X4 : $i] : ((((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ X4) @ X2))) = $true) | (((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ X4) @ X1))) != $true) | (((mem @ X4 @ X0)) != $true)) | (((p @ (ap @ (ap @ (c_2Epred__set_2ESUBSET @ X0) @ X1) @ X2))) != $true)))) | (((mem @ X1 @ (arr @ X0 @ bool))) != $true))),
% 3.42/0.81 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP]),skolemize(X4,sK2 @ X3 @ X1 @ X0)],[f95])).
% 3.42/0.81 thf(f98,plain,(
% 3.42/0.81 ( ! [X2 : $i,X3 : $i,X0 : del,X1 : $i] : ((((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ X2) @ (ap @ (ap @ (c_2Epred__set_2EDELETE @ X0) @ X1) @ X3)))) != $true) | (((mem @ X2 @ X0)) != $true) | (((mem @ X1 @ (arr @ X0 @ bool))) != $true) | (((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ X2) @ X1))) = $true) | (((mem @ X3 @ X0)) != $true)) )),
% 3.42/0.81 inference(cnf_transformation,[],[f87])).
% 3.42/0.81 thf(f100,plain,(
% 3.42/0.81 ( ! [X0 : del] : ((((mem @ (c_2Epred__set_2ECHOICE @ X0) @ (arr @ (arr @ X0 @ bool) @ X0))) = $true)) )),
% 3.42/0.81 inference(cnf_transformation,[],[f71])).
% 3.42/0.81 thf(f101,plain,(
% 3.42/0.81 ( ! [X0 : del] : ((((mem @ (c_2Epred__set_2EDELETE @ X0) @ (arr @ (arr @ X0 @ bool) @ (arr @ X0 @ (arr @ X0 @ bool))))) = $true)) )),
% 3.42/0.81 inference(cnf_transformation,[],[f53])).
% 3.42/0.81 thf(f105,plain,(
% 3.42/0.81 (((p @ (ap @ (ap @ (c_2Epred__set_2ESUBSET @ sK0) @ (ap @ (c_2Epred__set_2EREST @ sK0) @ sK1)) @ sK1))) != $true)),
% 3.42/0.81 inference(cnf_transformation,[],[f89])).
% 3.42/0.81 thf(f106,plain,(
% 3.42/0.81 (((mem @ sK1 @ (arr @ sK0 @ bool))) = $true)),
% 3.42/0.81 inference(cnf_transformation,[],[f89])).
% 3.42/0.81 thf(f109,plain,(
% 3.42/0.81 ( ! [X0 : $i,X1 : del] : ((((ap @ (ap @ (c_2Epred__set_2EDELETE @ X1) @ X0) @ (ap @ (c_2Epred__set_2ECHOICE @ X1) @ X0))) = ((ap @ (c_2Epred__set_2EREST @ X1) @ X0))) | (((mem @ X0 @ (arr @ X1 @ bool))) != $true)) )),
% 3.42/0.81 inference(cnf_transformation,[],[f92])).
% 3.42/0.81 thf(f110,plain,(
% 3.42/0.81 ( ! [X2 : del,X3 : $i,X0 : $i,X1 : del] : (($true = ((mem @ (ap @ X0 @ X3) @ X1))) | (((mem @ X3 @ X2)) != $true) | (((mem @ X0 @ (arr @ X2 @ X1))) != $true)) )),
% 3.42/0.81 inference(cnf_transformation,[],[f93])).
% 3.42/0.81 thf(f112,plain,(
% 3.42/0.81 ( ! [X2 : $i,X0 : del,X1 : $i] : ((((mem @ (sK3 @ X2 @ X1 @ X0) @ X0)) = $true) | (((mem @ X1 @ (arr @ X0 @ bool))) != $true) | (((p @ (ap @ (ap @ (c_2Epred__set_2ESUBSET @ X0) @ X1) @ X2))) = $true) | (((mem @ X2 @ (arr @ X0 @ bool))) != $true)) )),
% 3.42/0.81 inference(cnf_transformation,[],[f96])).
% 3.42/0.81 thf(f113,plain,(
% 3.42/0.81 ( ! [X2 : $i,X0 : del,X1 : $i] : ((((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ (sK3 @ X2 @ X1 @ X0)) @ X1))) = $true) | (((mem @ X2 @ (arr @ X0 @ bool))) != $true) | (((p @ (ap @ (ap @ (c_2Epred__set_2ESUBSET @ X0) @ X1) @ X2))) = $true) | (((mem @ X1 @ (arr @ X0 @ bool))) != $true)) )),
% 3.42/0.81 inference(cnf_transformation,[],[f96])).
% 3.42/0.81 thf(f114,plain,(
% 3.42/0.81 ( ! [X2 : $i,X0 : del,X1 : $i] : (($true != ((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ (sK3 @ X2 @ X1 @ X0)) @ X2)))) | (((p @ (ap @ (ap @ (c_2Epred__set_2ESUBSET @ X0) @ X1) @ X2))) = $true) | (((mem @ X1 @ (arr @ X0 @ bool))) != $true) | (((mem @ X2 @ (arr @ X0 @ bool))) != $true)) )),
% 3.42/0.81 inference(cnf_transformation,[],[f96])).
% 3.42/0.81 thf(f116,definition,(
% 3.42/0.81 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 3.42/0.81 introduced(theory,[fool_exhaustiveness_axiom])).
% 3.42/0.81 thf(f121,plain,(
% 3.42/0.81 ($false = ((p @ (ap @ (ap @ (c_2Epred__set_2ESUBSET @ sK0) @ (ap @ (c_2Epred__set_2EREST @ sK0) @ sK1)) @ sK1)))) | ($true != $true)),
% 3.42/0.81 inference(superposition,[],[f105,f116])).
% 3.42/0.81 thf(f127,plain,(
% 3.42/0.81 ($false = ((p @ (ap @ (ap @ (c_2Epred__set_2ESUBSET @ sK0) @ (ap @ (c_2Epred__set_2EREST @ sK0) @ sK1)) @ sK1))))),
% 3.42/0.81 inference(trivial_inequality_removal,[],[f121])).
% 3.42/0.81 thf(f131,plain,(
% 3.42/0.81 ( ! [X2 : del,X3 : del,X0 : del,X1 : $i] : ((((mem @ (ap @ (c_2Epred__set_2EDELETE @ X0) @ X1) @ (arr @ X3 @ X2))) != $true) | ($true != ((mem @ (ap @ (c_2Epred__set_2ECHOICE @ X0) @ X1) @ X3))) | (((mem @ X1 @ (arr @ X0 @ bool))) != $true) | (((mem @ (ap @ (c_2Epred__set_2EREST @ X0) @ X1) @ X2)) = $true)) )),
% 3.42/0.81 inference(superposition,[],[f110,f109])).
% 3.42/0.81 thf(f147,plain,(
% 3.42/0.81 ( ! [X2 : $i,X0 : del,X1 : $i] : (($false = ((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ (sK3 @ X1 @ X2 @ X0)) @ X1)))) | (((p @ (ap @ (ap @ (c_2Epred__set_2ESUBSET @ X0) @ X2) @ X1))) = $true) | (((mem @ X1 @ (arr @ X0 @ bool))) != $true) | (((mem @ X2 @ (arr @ X0 @ bool))) != $true) | ($true != $true)) )),
% 3.42/0.81 inference(superposition,[],[f114,f116])).
% 3.42/0.81 thf(f148,plain,(
% 3.42/0.81 ( ! [X2 : $i,X0 : del,X1 : $i] : (($false = ((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ (sK3 @ X1 @ X2 @ X0)) @ X1)))) | (((mem @ X1 @ (arr @ X0 @ bool))) != $true) | (((p @ (ap @ (ap @ (c_2Epred__set_2ESUBSET @ X0) @ X2) @ X1))) = $true) | (((mem @ X2 @ (arr @ X0 @ bool))) != $true)) )),
% 3.42/0.81 inference(trivial_inequality_removal,[],[f147])).
% 3.42/0.81 thf(f151,plain,(
% 3.42/0.81 ( ! [X2 : $i,X0 : del,X1 : $i] : ((((mem @ X2 @ X0)) != $true) | ($true != ((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ X2) @ (ap @ (c_2Epred__set_2EREST @ X0) @ X1))))) | (((mem @ X1 @ (arr @ X0 @ bool))) != $true) | ($true != ((mem @ (ap @ (c_2Epred__set_2ECHOICE @ X0) @ X1) @ X0))) | (((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ X2) @ X1))) = $true) | (((mem @ X1 @ (arr @ X0 @ bool))) != $true)) )),
% 3.42/0.81 inference(superposition,[],[f98,f109])).
% 3.42/0.81 thf(f156,plain,(
% 3.42/0.81 ( ! [X2 : $i,X0 : del,X1 : $i] : (($true != ((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ X2) @ (ap @ (c_2Epred__set_2EREST @ X0) @ X1))))) | ($true != ((mem @ (ap @ (c_2Epred__set_2ECHOICE @ X0) @ X1) @ X0))) | (((mem @ X2 @ X0)) != $true) | (((mem @ X1 @ (arr @ X0 @ bool))) != $true) | (((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ X2) @ X1))) = $true)) )),
% 3.42/0.81 inference(duplicate_literal_removal,[],[f151])).
% 3.42/0.81 thf(f171,plain,(
% 3.42/0.81 ( ! [X2 : del,X3 : del,X0 : del,X1 : $i,X4 : del] : ((((mem @ (ap @ (c_2Epred__set_2EREST @ X0) @ X1) @ X3)) = $true) | ($true != ((mem @ X1 @ X4))) | ($true != $true) | ($true != ((mem @ (c_2Epred__set_2EDELETE @ X0) @ (arr @ X4 @ (arr @ X2 @ X3))))) | (((mem @ X1 @ (arr @ X0 @ bool))) != $true) | ($true != ((mem @ (ap @ (c_2Epred__set_2ECHOICE @ X0) @ X1) @ X2)))) )),
% 3.42/0.81 inference(superposition,[],[f131,f110])).
% 3.42/0.81 thf(f174,plain,(
% 3.42/0.81 ( ! [X2 : del,X3 : del,X0 : del,X1 : $i,X4 : del] : (($true != ((mem @ (c_2Epred__set_2EDELETE @ X0) @ (arr @ X4 @ (arr @ X2 @ X3))))) | ($true != ((mem @ (ap @ (c_2Epred__set_2ECHOICE @ X0) @ X1) @ X2))) | (((mem @ (ap @ (c_2Epred__set_2EREST @ X0) @ X1) @ X3)) = $true) | ($true != ((mem @ X1 @ X4))) | (((mem @ X1 @ (arr @ X0 @ bool))) != $true)) )),
% 3.42/0.81 inference(trivial_inequality_removal,[],[f171])).
% 3.42/0.81 thf(f229,plain,(
% 3.42/0.81 ( ! [X0 : del,X1 : $i] : ((((mem @ X1 @ (arr @ X0 @ bool))) != $true) | (((mem @ X1 @ (arr @ X0 @ bool))) != $true) | ($true != ((mem @ (ap @ (c_2Epred__set_2ECHOICE @ X0) @ X1) @ X0))) | ($true = ((mem @ (ap @ (c_2Epred__set_2EREST @ X0) @ X1) @ (arr @ X0 @ bool)))) | ($true != $true)) )),
% 3.42/0.81 inference(superposition,[],[f174,f101])).
% 3.42/0.81 thf(f231,plain,(
% 3.42/0.81 ( ! [X0 : del,X1 : $i] : (($true = ((mem @ (ap @ (c_2Epred__set_2EREST @ X0) @ X1) @ (arr @ X0 @ bool)))) | (((mem @ X1 @ (arr @ X0 @ bool))) != $true) | ($true != $true) | ($true != ((mem @ (ap @ (c_2Epred__set_2ECHOICE @ X0) @ X1) @ X0)))) )),
% 3.42/0.81 inference(duplicate_literal_removal,[],[f229])).
% 3.42/0.81 thf(f232,plain,(
% 3.42/0.81 ( ! [X0 : del,X1 : $i] : (($true = ((mem @ (ap @ (c_2Epred__set_2EREST @ X0) @ X1) @ (arr @ X0 @ bool)))) | ($true != ((mem @ (ap @ (c_2Epred__set_2ECHOICE @ X0) @ X1) @ X0))) | (((mem @ X1 @ (arr @ X0 @ bool))) != $true)) )),
% 3.42/0.81 inference(trivial_inequality_removal,[],[f231])).
% 3.42/0.81 thf(f259,plain,(
% 3.42/0.81 ( ! [X2 : $i,X0 : del,X1 : $i] : (($true != $true) | (((mem @ X2 @ (arr @ X0 @ bool))) != $true) | (((mem @ (ap @ (c_2Epred__set_2EREST @ X0) @ X2) @ (arr @ X0 @ bool))) != $true) | (((mem @ (sK3 @ X1 @ (ap @ (c_2Epred__set_2EREST @ X0) @ X2) @ X0) @ X0)) != $true) | (((p @ (ap @ (ap @ (c_2Epred__set_2ESUBSET @ X0) @ (ap @ (c_2Epred__set_2EREST @ X0) @ X2)) @ X1))) = $true) | (((mem @ (ap @ (c_2Epred__set_2ECHOICE @ X0) @ X2) @ X0)) != $true) | (((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ (sK3 @ X1 @ (ap @ (c_2Epred__set_2EREST @ X0) @ X2) @ X0)) @ X2))) = $true) | (((mem @ X1 @ (arr @ X0 @ bool))) != $true)) )),
% 3.42/0.81 inference(superposition,[],[f156,f113])).
% 3.42/0.81 thf(f263,plain,(
% 3.42/0.81 ( ! [X2 : $i,X0 : del,X1 : $i] : ((((p @ (ap @ (ap @ (c_2Epred__set_2ESUBSET @ X0) @ (ap @ (c_2Epred__set_2EREST @ X0) @ X2)) @ X1))) = $true) | (((mem @ (sK3 @ X1 @ (ap @ (c_2Epred__set_2EREST @ X0) @ X2) @ X0) @ X0)) != $true) | (((mem @ X1 @ (arr @ X0 @ bool))) != $true) | (((mem @ X2 @ (arr @ X0 @ bool))) != $true) | (((mem @ (ap @ (c_2Epred__set_2EREST @ X0) @ X2) @ (arr @ X0 @ bool))) != $true) | (((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ (sK3 @ X1 @ (ap @ (c_2Epred__set_2EREST @ X0) @ X2) @ X0)) @ X2))) = $true) | (((mem @ (ap @ (c_2Epred__set_2ECHOICE @ X0) @ X2) @ X0)) != $true)) )),
% 3.42/0.81 inference(trivial_inequality_removal,[],[f259])).
% 3.42/0.81 thf(f267,plain,(
% 3.42/0.81 ( ! [X2 : $i,X0 : del,X1 : $i] : ((((p @ (ap @ (ap @ (c_2Epred__set_2ESUBSET @ X0) @ (ap @ (c_2Epred__set_2EREST @ X0) @ X2)) @ X1))) = $true) | (((mem @ X2 @ (arr @ X0 @ bool))) != $true) | (((mem @ (ap @ (c_2Epred__set_2ECHOICE @ X0) @ X2) @ X0)) != $true) | (((mem @ (ap @ (c_2Epred__set_2EREST @ X0) @ X2) @ (arr @ X0 @ bool))) != $true) | (((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ (sK3 @ X1 @ (ap @ (c_2Epred__set_2EREST @ X0) @ X2) @ X0)) @ X2))) = $true) | (((mem @ X1 @ (arr @ X0 @ bool))) != $true)) )),
% 3.42/0.81 inference(forward_subsumption_resolution,[],[f263,f112])).
% 3.42/0.81 thf(f269,plain,(
% 3.42/0.81 ( ! [X2 : $i,X0 : del,X1 : $i] : ((((p @ (ap @ (ap @ (c_2Ebool_2EIN @ X0) @ (sK3 @ X1 @ (ap @ (c_2Epred__set_2EREST @ X0) @ X2) @ X0)) @ X2))) = $true) | (((mem @ X1 @ (arr @ X0 @ bool))) != $true) | (((mem @ (ap @ (c_2Epred__set_2ECHOICE @ X0) @ X2) @ X0)) != $true) | (((p @ (ap @ (ap @ (c_2Epred__set_2ESUBSET @ X0) @ (ap @ (c_2Epred__set_2EREST @ X0) @ X2)) @ X1))) = $true) | (((mem @ X2 @ (arr @ X0 @ bool))) != $true)) )),
% 3.42/0.81 inference(forward_subsumption_resolution,[],[f267,f232])).
% 3.42/0.81 thf(f376,plain,(
% 3.42/0.81 ( ! [X0 : del,X1 : $i] : (($true != ((mem @ (ap @ (c_2Epred__set_2EREST @ X0) @ X1) @ (arr @ X0 @ bool)))) | (((mem @ X1 @ (arr @ X0 @ bool))) != $true) | ($true != ((mem @ (ap @ (c_2Epred__set_2ECHOICE @ X0) @ X1) @ X0))) | (((p @ (ap @ (ap @ (c_2Epred__set_2ESUBSET @ X0) @ (ap @ (c_2Epred__set_2EREST @ X0) @ X1)) @ X1))) = $true) | (((mem @ X1 @ (arr @ X0 @ bool))) != $true) | ($false = $true) | (((mem @ X1 @ (arr @ X0 @ bool))) != $true) | (((p @ (ap @ (ap @ (c_2Epred__set_2ESUBSET @ X0) @ (ap @ (c_2Epred__set_2EREST @ X0) @ X1)) @ X1))) = $true)) )),
% 3.42/0.81 inference(superposition,[],[f148,f269])).
% 3.42/0.81 thf(f385,plain,(
% 3.42/0.81 ( ! [X0 : del,X1 : $i] : ((((mem @ X1 @ (arr @ X0 @ bool))) != $true) | (((p @ (ap @ (ap @ (c_2Epred__set_2ESUBSET @ X0) @ (ap @ (c_2Epred__set_2EREST @ X0) @ X1)) @ X1))) = $true) | ($false = $true) | ($true != ((mem @ (ap @ (c_2Epred__set_2ECHOICE @ X0) @ X1) @ X0))) | ($true != ((mem @ (ap @ (c_2Epred__set_2EREST @ X0) @ X1) @ (arr @ X0 @ bool))))) )),
% 3.42/0.81 inference(duplicate_literal_removal,[],[f376])).
% 3.42/0.81 thf(f386,plain,(
% 3.42/0.81 ( ! [X0 : del,X1 : $i] : ((((p @ (ap @ (ap @ (c_2Epred__set_2ESUBSET @ X0) @ (ap @ (c_2Epred__set_2EREST @ X0) @ X1)) @ X1))) = $true) | ($true != ((mem @ (ap @ (c_2Epred__set_2ECHOICE @ X0) @ X1) @ X0))) | ($true != ((mem @ (ap @ (c_2Epred__set_2EREST @ X0) @ X1) @ (arr @ X0 @ bool)))) | (((mem @ X1 @ (arr @ X0 @ bool))) != $true)) )),
% 3.42/0.81 inference(trivial_inequality_removal,[],[f385])).
% 3.42/0.81 thf(f402,plain,(
% 3.42/0.81 ( ! [X0 : del,X1 : $i] : ((((p @ (ap @ (ap @ (c_2Epred__set_2ESUBSET @ X0) @ (ap @ (c_2Epred__set_2EREST @ X0) @ X1)) @ X1))) = $true) | (((mem @ X1 @ (arr @ X0 @ bool))) != $true) | ($true != ((mem @ (ap @ (c_2Epred__set_2ECHOICE @ X0) @ X1) @ X0)))) )),
% 3.42/0.81 inference(forward_subsumption_resolution,[],[f386,f232])).
% 3.42/0.81 thf(f455,plain,(
% 3.42/0.81 ($false = $true) | ($true != ((mem @ (ap @ (c_2Epred__set_2ECHOICE @ sK0) @ sK1) @ sK0))) | (((mem @ sK1 @ (arr @ sK0 @ bool))) != $true)),
% 3.42/0.81 inference(superposition,[],[f127,f402])).
% 3.42/0.81 thf(f457,plain,(
% 3.42/0.81 (((mem @ sK1 @ (arr @ sK0 @ bool))) != $true) | ($true != ((mem @ (ap @ (c_2Epred__set_2ECHOICE @ sK0) @ sK1) @ sK0)))),
% 3.42/0.81 inference(trivial_inequality_removal,[],[f455])).
% 3.42/0.81 thf(f462,plain,(
% 3.42/0.81 ($true != ((mem @ (ap @ (c_2Epred__set_2ECHOICE @ sK0) @ sK1) @ sK0)))),
% 3.42/0.81 inference(forward_subsumption_resolution,[],[f457,f106])).
% 3.42/0.81 thf(f478,plain,(
% 3.42/0.81 ( ! [X0 : del] : (($true != $true) | ($true != ((mem @ (c_2Epred__set_2ECHOICE @ sK0) @ (arr @ X0 @ sK0)))) | (((mem @ sK1 @ X0)) != $true)) )),
% 3.42/0.81 inference(superposition,[],[f462,f110])).
% 3.42/0.81 thf(f481,plain,(
% 3.42/0.81 ( ! [X0 : del] : (($true != ((mem @ (c_2Epred__set_2ECHOICE @ sK0) @ (arr @ X0 @ sK0)))) | (((mem @ sK1 @ X0)) != $true)) )),
% 3.42/0.81 inference(trivial_inequality_removal,[],[f478])).
% 3.42/0.81 thf(f528,plain,(
% 3.42/0.81 (((mem @ sK1 @ (arr @ sK0 @ bool))) != $true) | ($true != $true)),
% 3.42/0.81 inference(superposition,[],[f481,f100])).
% 3.42/0.81 thf(f530,plain,(
% 3.42/0.81 (((mem @ sK1 @ (arr @ sK0 @ bool))) != $true)),
% 3.42/0.81 inference(trivial_inequality_removal,[],[f528])).
% 3.42/0.81 thf(f532,plain,(
% 3.42/0.81 $false),
% 3.42/0.81 inference(forward_subsumption_resolution,[],[f530,f106])).
% 3.42/0.81 % SZS output end Proof for theBenchmark
% 3.42/0.81 % (3288003)------------------------------
% 3.42/0.81 % (3288003)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.42/0.81 % (3288003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.42/0.81 % (3288003)CaDiCaL version: 2.1.3
% 3.42/0.81 % (3288003)Termination reason: Refutation
% 3.42/0.81 % (3288003)Time elapsed: 0.051 s
% 3.42/0.81 % (3288003)Peak memory usage: 13 MB
% 3.42/0.81 % (3288003)Instructions burned: 99 (million)
% 3.42/0.81 % (3287889)Success in time 0.572 s
% 3.42/0.81 % Vampire exiting
%------------------------------------------------------------------------------