%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP015^2 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n008.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:47 AM UTC 2026
% Result : Theorem 10.96s 2.40s
% Output : Refutation 10.96s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP015^2 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.25 % Computer : n008.cluster.edu
% 0.10/0.25 % Model : x86_64 x86_64
% 0.10/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.25 % Memory : 8046.5625MB
% 0.10/0.25 % OS : Linux 6.8.0-71-generic
% 0.10/0.25 % CPULimit : 300
% 0.10/0.25 % WCLimit : 300
% 0.10/0.25 % DateTime : Tue Sep 29 19:29:59 UTC 2026
% 0.10/0.25 % CPUTime :
% 0.10/0.25 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.24/0.29 Running higher-order theorem proving
% 0.24/0.31 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.98/0.50 % (3620182)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.98/0.50 % (3620188)lrs+10_16_si=on:nwc=1.5:random_seed=4101488441:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.98/0.50 % (3620191)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=485362039:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.98/0.50 % (3620187)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=452659799:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.98/0.50 % (3620188)Instruction limit reached!
% 0.98/0.50 % (3620188)------------------------------
% 0.98/0.50 % (3620188)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.98/0.50 % (3620188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.98/0.50 % (3620188)CaDiCaL version: 2.1.3
% 0.98/0.50 % (3620188)Termination reason: Instruction limit
% 0.98/0.50 % (3620188)Termination phase: Saturation
% 0.98/0.50 % (3620188)Time elapsed: 0.009 s
% 0.98/0.50 % (3620188)Peak memory usage: 11 MB
% 0.98/0.50 % (3620188)Instructions burned: 19 (million)
% 0.98/0.50 % (3620190)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=767735156: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.98/0.50 % (3620189)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=780115350:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.98/0.50 % (3620191)Instruction limit reached!
% 0.98/0.50 % (3620191)------------------------------
% 0.98/0.50 % (3620191)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.98/0.50 % (3620191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.98/0.50 % (3620191)CaDiCaL version: 2.1.3
% 0.98/0.50 % (3620191)Termination reason: Instruction limit
% 0.98/0.50 % (3620191)Termination phase: Saturation
% 0.98/0.50 % (3620191)Time elapsed: 0.012 s
% 0.98/0.50 % (3620191)Peak memory usage: 12 MB
% 0.98/0.50 % (3620191)Instructions burned: 25 (million)
% 0.98/0.50 % (3620193)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.98/0.50 % (3620193)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.98/0.50 % (3620189)Instruction limit reached!
% 0.98/0.50 % (3620189)------------------------------
% 0.98/0.50 % (3620189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.98/0.50 % (3620189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.98/0.50 % (3620189)CaDiCaL version: 2.1.3
% 0.98/0.50 % (3620189)Termination reason: Instruction limit
% 0.98/0.50 % (3620189)Termination phase: shuffling
% 0.98/0.50 % (3620189)Time elapsed: 0.003 s
% 0.98/0.50 % (3620189)Peak memory usage: 9 MB
% 0.98/0.50 % (3620189)Instructions burned: 4 (million)
% 0.98/0.50 % (3620192)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=573965351:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.98/0.50 % (3620193)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=3944673668:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.98/0.50 % (3620201)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.98/0.50 % (3620200)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=486509026:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.98/0.50 % (3620199)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2182083447:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.98/0.50 % (3620199)Instruction limit reached!
% 0.98/0.50 % (3620199)------------------------------
% 0.98/0.50 % (3620199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.98/0.50 % (3620199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.98/0.50 % (3620199)CaDiCaL version: 2.1.3
% 0.98/0.50 % (3620199)Termination reason: Instruction limit
% 0.98/0.55 % (3620199)Termination phase: shuffling
% 0.98/0.55 % (3620199)Time elapsed: 0.001 s
% 0.98/0.55 % (3620199)Peak memory usage: 9 MB
% 0.98/0.55 % (3620199)Instructions burned: 2 (million)
% 0.98/0.55 % (3620201)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3538847442:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.98/0.55 % (3620200)Instruction limit reached!
% 0.98/0.55 % (3620200)------------------------------
% 0.98/0.55 % (3620200)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.98/0.55 % (3620200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.98/0.55 % (3620200)CaDiCaL version: 2.1.3
% 0.98/0.55 % (3620200)Termination reason: Instruction limit
% 0.98/0.55 % (3620200)Termination phase: Preprocessing 1
% 0.98/0.55 % (3620200)Time elapsed: 0.003 s
% 0.98/0.55 % (3620200)Peak memory usage: 10 MB
% 0.98/0.55 % (3620200)Instructions burned: 6 (million)
% 0.98/0.55 % (3620201)Instruction limit reached!
% 0.98/0.55 % (3620201)------------------------------
% 0.98/0.55 % (3620201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.98/0.55 % (3620201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.98/0.55 % (3620201)CaDiCaL version: 2.1.3
% 0.98/0.55 % (3620201)Termination reason: Instruction limit
% 0.98/0.55 % (3620201)Termination phase: Property scanning
% 0.98/0.55 % (3620201)Time elapsed: 0.003 s
% 0.98/0.55 % (3620201)Peak memory usage: 9 MB
% 0.98/0.55 % (3620201)Instructions burned: 8 (million)
% 0.98/0.55 % (3620208)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.98/0.55 % (3620208)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.98/0.55 % (3620187)Instruction limit reached!
% 0.98/0.55 % (3620187)------------------------------
% 0.98/0.55 % (3620187)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.98/0.55 % (3620187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.98/0.55 % (3620187)CaDiCaL version: 2.1.3
% 0.98/0.55 % (3620187)Termination reason: Instruction limit
% 0.98/0.55 % (3620187)Termination phase: Saturation
% 0.98/0.55 % (3620187)Time elapsed: 0.051 s
% 0.98/0.55 % (3620187)Peak memory usage: 12 MB
% 0.98/0.55 % (3620187)Instructions burned: 88 (million)
% 0.98/0.55 % (3620208)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=56763903: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.98/0.55 % (3620208)Instruction limit reached!
% 0.98/0.55 % (3620208)------------------------------
% 0.98/0.55 % (3620208)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.98/0.55 % (3620208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.98/0.55 % (3620208)CaDiCaL version: 2.1.3
% 0.98/0.55 % (3620208)Termination reason: Instruction limit
% 0.98/0.55 % (3620208)Termination phase: Saturation
% 0.98/0.55 % (3620208)Time elapsed: 0.012 s
% 0.98/0.55 % (3620208)Peak memory usage: 11 MB
% 0.98/0.55 % (3620208)Instructions burned: 28 (million)
% 0.98/0.55 % (3620206)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=3773295457:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.98/0.55 % (3620211)lrs+10_1_si=on:cs=on:random_seed=3933300089:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.98/0.55 % (3620206)Instruction limit reached!
% 0.98/0.55 % (3620206)------------------------------
% 0.98/0.55 % (3620206)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.98/0.55 % (3620211)Instruction limit reached!
% 0.98/0.55 % (3620211)------------------------------
% 0.98/0.55 % (3620211)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.98/0.55 % (3620206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.98/0.55 % (3620211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.98/0.55 % (3620206)CaDiCaL version: 2.1.3
% 0.98/0.55 % (3620211)CaDiCaL version: 2.1.3
% 0.98/0.55 % (3620206)Termination reason: Instruction limit
% 0.98/0.55 % (3620206)Termination phase: Property scanning
% 0.98/0.55 % (3620211)Termination reason: Instruction limit
% 1.67/0.61 % (3620211)Termination phase: Preprocessing 3
% 1.67/0.61 % (3620206)Time elapsed: 0.009 s
% 1.67/0.61 % (3620211)Time elapsed: 0.004 s
% 1.67/0.61 % (3620211)Peak memory usage: 10 MB
% 1.67/0.61 % (3620206)Peak memory usage: 10 MB
% 1.67/0.61 % (3620211)Instructions burned: 9 (million)
% 1.67/0.61 % (3620206)Instructions burned: 12 (million)
% 1.67/0.61 % (3620209)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=1369392467:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 1.67/0.61 % (3620212)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.67/0.61 % (3620212)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=401843302:i=2:add=on:rtra=on_2998 on theBenchmark for (2998ds/2Mi)
% 1.67/0.61 % (3620192)Instruction limit reached!
% 1.67/0.61 % (3620192)------------------------------
% 1.67/0.61 % (3620192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.67/0.61 % (3620212)Instruction limit reached!
% 1.67/0.61 % (3620212)------------------------------
% 1.67/0.61 % (3620212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.67/0.61 % (3620192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.67/0.61 % (3620212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.67/0.61 % (3620192)CaDiCaL version: 2.1.3
% 1.67/0.61 % (3620192)Termination reason: Instruction limit
% 1.67/0.61 % (3620192)Termination phase: Saturation
% 1.67/0.61 % (3620212)CaDiCaL version: 2.1.3
% 1.67/0.61 % (3620192)Time elapsed: 0.070 s
% 1.67/0.61 % (3620212)Termination reason: Instruction limit
% 1.67/0.61 % (3620212)Termination phase: shuffling
% 1.67/0.61 % (3620212)Time elapsed: 0.002 s
% 1.67/0.61 % (3620192)Peak memory usage: 13 MB
% 1.67/0.61 % (3620212)Peak memory usage: 9 MB
% 1.67/0.61 % (3620192)Instructions burned: 76 (million)
% 1.67/0.61 % (3620212)Instructions burned: 4 (million)
% 1.67/0.61 % (3620215)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=1133250106:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/38Mi)
% 1.67/0.61 % (3620217)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=3469486860:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 1.67/0.61 % (3620220)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=879384195:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.67/0.61 % (3620219)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=725086917:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 1.67/0.61 % (3620209)Instruction limit reached!
% 1.67/0.61 % (3620209)------------------------------
% 1.67/0.61 % (3620209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.67/0.61 % (3620209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.67/0.61 % (3620209)CaDiCaL version: 2.1.3
% 1.67/0.61 % (3620209)Termination reason: Instruction limit
% 1.67/0.61 % (3620209)Termination phase: Saturation
% 1.67/0.61 % (3620209)Time elapsed: 0.048 s
% 1.67/0.61 % (3620209)Peak memory usage: 12 MB
% 1.67/0.61 % (3620209)Instructions burned: 87 (million)
% 1.67/0.61 % (3620220)Instruction limit reached!
% 1.67/0.61 % (3620220)------------------------------
% 1.67/0.61 % (3620220)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.67/0.61 % (3620220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.67/0.61 % (3620220)CaDiCaL version: 2.1.3
% 1.67/0.61 % (3620220)Termination reason: Instruction limit
% 1.67/0.61 % (3620220)Termination phase: Property scanning
% 1.67/0.61 % (3620220)Time elapsed: 0.012 s
% 1.67/0.61 % (3620220)Peak memory usage: 10 MB
% 1.67/0.61 % (3620220)Instructions burned: 15 (million)
% 1.67/0.61 % (3620217)Refutation not found, incomplete strategy
% 1.67/0.61 % (3620217)------------------------------
% 1.67/0.61 % (3620217)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.67/0.61 % (3620217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.67/0.61 % (3620217)CaDiCaL version: 2.1.3
% 1.67/0.61 % (3620217)Termination reason: Refutation not found, incomplete strategy
% 1.98/0.66 % (3620217)Time elapsed: 0.020 s
% 1.98/0.66 % (3620217)Peak memory usage: 12 MB
% 1.98/0.66 % (3620217)Instructions burned: 11 (million)
% 1.98/0.66 % (3620217)------------------------------
% 1.98/0.66 % (3620217)------------------------------
% 1.98/0.66 % (3620219)Instruction limit reached!
% 1.98/0.66 % (3620219)------------------------------
% 1.98/0.66 % (3620219)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.98/0.66 % (3620219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.98/0.66 % (3620219)CaDiCaL version: 2.1.3
% 1.98/0.66 % (3620219)Termination reason: Instruction limit
% 1.98/0.66 % (3620219)Termination phase: Saturation
% 1.98/0.66 % (3620219)Time elapsed: 0.022 s
% 1.98/0.66 % (3620219)Peak memory usage: 12 MB
% 1.98/0.66 % (3620219)Instructions burned: 25 (million)
% 1.98/0.66 % (3620225)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=3663592039:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 1.98/0.66 % (3620215)Instruction limit reached!
% 1.98/0.66 % (3620215)------------------------------
% 1.98/0.66 % (3620215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.98/0.66 % (3620215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.98/0.66 % (3620215)CaDiCaL version: 2.1.3
% 1.98/0.66 % (3620215)Termination reason: Instruction limit
% 1.98/0.66 % (3620215)Termination phase: Saturation
% 1.98/0.66 % (3620215)Time elapsed: 0.044 s
% 1.98/0.66 % (3620215)Peak memory usage: 12 MB
% 1.98/0.66 % (3620215)Instructions burned: 39 (million)
% 1.98/0.66 % (3620226)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=3083207275:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.98/0.66 % (3620226)Instruction limit reached!
% 1.98/0.66 % (3620226)------------------------------
% 1.98/0.66 % (3620226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.98/0.66 % (3620226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.98/0.66 % (3620226)CaDiCaL version: 2.1.3
% 1.98/0.66 % (3620226)Termination reason: Instruction limit
% 1.98/0.66 % (3620226)Termination phase: Property scanning
% 1.98/0.66 % (3620226)Time elapsed: 0.007 s
% 1.98/0.66 % (3620226)Peak memory usage: 10 MB
% 1.98/0.66 % (3620226)Instructions burned: 15 (million)
% 1.98/0.66 % (3620193)Instruction limit reached!
% 1.98/0.66 % (3620193)------------------------------
% 1.98/0.66 % (3620193)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.98/0.66 % (3620193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.98/0.66 % (3620193)CaDiCaL version: 2.1.3
% 1.98/0.66 % (3620193)Termination reason: Instruction limit
% 1.98/0.66 % (3620193)Termination phase: Saturation
% 1.98/0.66 % (3620193)Time elapsed: 0.152 s
% 1.98/0.66 % (3620193)Peak memory usage: 13 MB
% 1.98/0.66 % (3620193)Instructions burned: 157 (million)
% 1.98/0.66 % (3620230)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=264524928:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.98/0.66 % (3620227)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=644142297:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2998 on theBenchmark for (2998ds/2Mi)
% 1.98/0.66 % (3620227)Instruction limit reached!
% 1.98/0.66 % (3620227)------------------------------
% 1.98/0.66 % (3620227)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.98/0.66 % (3620227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.98/0.66 % (3620227)CaDiCaL version: 2.1.3
% 1.98/0.66 % (3620227)Termination reason: Instruction limit
% 1.98/0.66 % (3620227)Termination phase: Preprocessing 1
% 1.98/0.66 % (3620227)Time elapsed: 0.008 s
% 1.98/0.66 % (3620227)Peak memory usage: 10 MB
% 1.98/0.66 % (3620227)Instructions burned: 8 (million)
% 1.98/0.66 % (3620230)Instruction limit reached!
% 1.98/0.66 % (3620230)------------------------------
% 1.98/0.66 % (3620230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.98/0.66 % (3620230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.98/0.66 % (3620230)CaDiCaL version: 2.1.3
% 1.98/0.66 % (3620230)Termination reason: Instruction limit
% 1.98/0.66 % (3620230)Termination phase: Saturation
% 1.98/0.66 % (3620230)Time elapsed: 0.011 s
% 1.98/0.66 % (3620230)Peak memory usage: 11 MB
% 1.98/0.66 % (3620230)Instructions burned: 24 (million)
% 1.98/0.66 % (3620229)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3615651946:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 2.11/0.71 % (3620233)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.11/0.71 % (3620233)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 2.11/0.71 % (3620232)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=3472963853:cond=on:i=60:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/60Mi)
% 2.11/0.71 % (3620233)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=687686159:i=14:add=off:nm=40:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 2.11/0.71 % (3620236)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 2.11/0.71 % (3620229)Instruction limit reached!
% 2.11/0.71 % (3620229)------------------------------
% 2.11/0.71 % (3620229)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.11/0.71 % (3620229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.11/0.71 % (3620229)CaDiCaL version: 2.1.3
% 2.11/0.71 % (3620229)Termination reason: Instruction limit
% 2.11/0.71 % (3620229)Termination phase: Saturation
% 2.11/0.71 % (3620229)Time elapsed: 0.025 s
% 2.11/0.71 % (3620229)Peak memory usage: 12 MB
% 2.11/0.71 % (3620229)Instructions burned: 26 (million)
% 2.11/0.71 % (3620236)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=2003173299:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2997 on theBenchmark for (2997ds/8Mi)
% 2.11/0.71 % (3620237)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=2521017248:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2997 on theBenchmark for (2997ds/31Mi)
% 2.11/0.71 % (3620233)Instruction limit reached!
% 2.11/0.71 % (3620233)------------------------------
% 2.11/0.71 % (3620233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.11/0.71 % (3620233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.11/0.71 % (3620233)CaDiCaL version: 2.1.3
% 2.11/0.71 % (3620233)Termination reason: Instruction limit
% 2.11/0.71 % (3620233)Termination phase: Property scanning
% 2.11/0.71 % (3620233)Time elapsed: 0.018 s
% 2.11/0.71 % (3620233)Peak memory usage: 10 MB
% 2.11/0.71 % (3620233)Instructions burned: 15 (million)
% 2.11/0.71 % (3620236)Instruction limit reached!
% 2.11/0.71 % (3620236)------------------------------
% 2.11/0.71 % (3620236)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.11/0.71 % (3620236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.11/0.71 % (3620236)CaDiCaL version: 2.1.3
% 2.11/0.71 % (3620236)Termination reason: Instruction limit
% 2.11/0.71 % (3620236)Termination phase: Naming
% 2.11/0.71 % (3620236)Time elapsed: 0.011 s
% 2.11/0.71 % (3620236)Peak memory usage: 10 MB
% 2.11/0.71 % (3620236)Instructions burned: 9 (million)
% 2.11/0.71 % (3620232)Instruction limit reached!
% 2.11/0.71 % (3620232)------------------------------
% 2.11/0.71 % (3620232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.11/0.71 % (3620232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.11/0.71 % (3620232)CaDiCaL version: 2.1.3
% 2.11/0.71 % (3620232)Termination reason: Instruction limit
% 2.11/0.71 % (3620232)Termination phase: Saturation
% 2.11/0.71 % (3620232)Time elapsed: 0.041 s
% 2.11/0.71 % (3620232)Peak memory usage: 12 MB
% 2.11/0.71 % (3620232)Instructions burned: 61 (million)
% 2.11/0.71 % (3620244)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=424345613:i=23:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/23Mi)
% 2.11/0.71 % (3620242)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=4013387380:i=7:hud=5:bd=preordered:rtra=on:bet=on_2997 on theBenchmark for (2997ds/7Mi)
% 2.11/0.71 % (3620237)Instruction limit reached!
% 2.11/0.71 % (3620237)------------------------------
% 2.11/0.71 % (3620237)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.11/0.71 % (3620237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.11/0.79 % (3620237)CaDiCaL version: 2.1.3
% 2.11/0.79 % (3620237)Termination reason: Instruction limit
% 2.11/0.79 % (3620237)Termination phase: Saturation
% 2.11/0.79 % (3620237)Time elapsed: 0.030 s
% 2.11/0.79 % (3620237)Peak memory usage: 11 MB
% 2.11/0.79 % (3620237)Instructions burned: 33 (million)
% 2.11/0.79 % (3620242)Instruction limit reached!
% 2.11/0.79 % (3620242)------------------------------
% 2.11/0.79 % (3620242)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.11/0.79 % (3620242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.11/0.79 % (3620242)CaDiCaL version: 2.1.3
% 2.11/0.79 % (3620242)Termination reason: Instruction limit
% 2.11/0.79 % (3620242)Termination phase: Preprocessing 1
% 2.11/0.79 % (3620242)Time elapsed: 0.007 s
% 2.11/0.79 % (3620242)Peak memory usage: 10 MB
% 2.11/0.79 % (3620242)Instructions burned: 8 (million)
% 2.11/0.79 % (3620245)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=209691482:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2997 on theBenchmark for (2997ds/20Mi)
% 2.11/0.79 % (3620244)Instruction limit reached!
% 2.11/0.79 % (3620244)------------------------------
% 2.11/0.79 % (3620244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.11/0.79 % (3620244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.11/0.79 % (3620244)CaDiCaL version: 2.1.3
% 2.11/0.79 % (3620244)Termination reason: Instruction limit
% 2.11/0.79 % (3620244)Termination phase: Saturation
% 2.11/0.79 % (3620244)Time elapsed: 0.014 s
% 2.11/0.79 % (3620244)Peak memory usage: 11 MB
% 2.11/0.79 % (3620244)Instructions burned: 24 (million)
% 2.11/0.79 % (3620245)Instruction limit reached!
% 2.11/0.79 % (3620245)------------------------------
% 2.11/0.79 % (3620245)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.11/0.79 % (3620245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.11/0.79 % (3620245)CaDiCaL version: 2.1.3
% 2.11/0.79 % (3620245)Termination reason: Instruction limit
% 2.11/0.79 % (3620245)Termination phase: Saturation
% 2.11/0.79 % (3620245)Time elapsed: 0.009 s
% 2.11/0.79 % (3620245)Peak memory usage: 11 MB
% 2.11/0.79 % (3620245)Instructions burned: 20 (million)
% 2.11/0.79 % (3620246)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=3405347436:i=1240:rtra=on:ixr=off_2997 on theBenchmark for (2997ds/1240Mi)
% 2.11/0.79 % (3620253)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 2.11/0.79 % (3620253)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1503977194:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2996 on theBenchmark for (2996ds/7Mi)
% 2.11/0.79 % (3620190)Instruction limit reached!
% 2.11/0.79 % (3620190)------------------------------
% 2.11/0.79 % (3620190)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.11/0.79 % (3620190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.11/0.79 % (3620190)CaDiCaL version: 2.1.3
% 2.11/0.79 % (3620190)Termination reason: Instruction limit
% 2.11/0.79 % (3620190)Termination phase: Saturation
% 2.11/0.79 % (3620190)Time elapsed: 0.285 s
% 2.11/0.79 % (3620190)Peak memory usage: 15 MB
% 2.11/0.79 % (3620190)Instructions burned: 634 (million)
% 2.11/0.79 % (3620253)Instruction limit reached!
% 2.11/0.79 % (3620253)------------------------------
% 2.11/0.79 % (3620253)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.11/0.79 % (3620253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.11/0.79 % (3620253)CaDiCaL version: 2.1.3
% 2.11/0.79 % (3620253)Termination reason: Instruction limit
% 2.11/0.79 % (3620253)Termination phase: Property scanning
% 2.11/0.79 % (3620253)Time elapsed: 0.003 s
% 2.11/0.79 % (3620253)Peak memory usage: 9 MB
% 2.11/0.79 % (3620253)Instructions burned: 7 (million)
% 2.11/0.79 % (3620250)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=459317555:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/193Mi)
% 2.11/0.79 % (3620249)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=1306616032:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2996 on theBenchmark for (2996ds/143Mi)
% 2.11/0.79 % (3620252)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2601133678:i=42:hud=10:rtra=on_2996 on theBenchmark for (2996ds/42Mi)
% 2.46/0.88 % (3620225)Instruction limit reached!
% 2.46/0.88 % (3620225)------------------------------
% 2.46/0.88 % (3620225)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.46/0.88 % (3620225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.46/0.88 % (3620225)CaDiCaL version: 2.1.3
% 2.46/0.88 % (3620225)Termination reason: Instruction limit
% 2.46/0.88 % (3620225)Termination phase: Saturation
% 2.46/0.88 % (3620225)Time elapsed: 0.164 s
% 2.46/0.88 % (3620225)Peak memory usage: 13 MB
% 2.46/0.88 % (3620225)Instructions burned: 329 (million)
% 2.46/0.88 % (3620256)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=806551250:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/181Mi)
% 2.46/0.88 % (3620257)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=2072786551: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)
% 2.46/0.88 % (3620252)Instruction limit reached!
% 2.46/0.88 % (3620252)------------------------------
% 2.46/0.88 % (3620252)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.46/0.88 % (3620252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.46/0.88 % (3620252)CaDiCaL version: 2.1.3
% 2.46/0.88 % (3620252)Termination reason: Instruction limit
% 2.46/0.88 % (3620252)Termination phase: Saturation
% 2.46/0.88 % (3620252)Time elapsed: 0.021 s
% 2.46/0.88 % (3620252)Peak memory usage: 12 MB
% 2.46/0.88 % (3620252)Instructions burned: 42 (million)
% 2.46/0.88 % (3620261)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 2.46/0.88 % (3620261)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=3560053255:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2996 on theBenchmark for (2996ds/6Mi)
% 2.46/0.88 % (3620257)Refutation not found, incomplete strategy
% 2.46/0.88 % (3620257)------------------------------
% 2.46/0.88 % (3620257)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.46/0.88 % (3620257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.46/0.88 % (3620257)CaDiCaL version: 2.1.3
% 2.46/0.88 % (3620257)Termination reason: Refutation not found, incomplete strategy
% 2.46/0.88 % (3620257)Time elapsed: 0.012 s
% 2.46/0.88 % (3620257)Peak memory usage: 12 MB
% 2.46/0.88 % (3620257)Instructions burned: 24 (million)
% 2.46/0.88 % (3620257)------------------------------
% 2.46/0.88 % (3620257)------------------------------
% 2.46/0.88 % (3620261)Instruction limit reached!
% 2.46/0.88 % (3620261)------------------------------
% 2.46/0.88 % (3620261)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.46/0.88 % (3620261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.46/0.88 % (3620261)CaDiCaL version: 2.1.3
% 2.46/0.88 % (3620261)Termination reason: Instruction limit
% 2.46/0.88 % (3620261)Termination phase: Property scanning
% 2.46/0.88 % (3620261)Time elapsed: 0.003 s
% 2.46/0.88 % (3620261)Peak memory usage: 9 MB
% 2.46/0.88 % (3620261)Instructions burned: 7 (million)
% 2.46/0.88 % (3620264)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=3452291680:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2996 on theBenchmark for (2996ds/22Mi)
% 2.46/0.88 % (3620264)Instruction limit reached!
% 2.46/0.88 % (3620264)------------------------------
% 2.46/0.88 % (3620264)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.46/0.88 % (3620264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.46/0.88 % (3620264)CaDiCaL version: 2.1.3
% 2.46/0.88 % (3620266)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=966430293:i=19:add=on:rtra=on_2996 on theBenchmark for (2996ds/19Mi)
% 2.46/0.88 % (3620264)Termination reason: Instruction limit
% 2.46/0.88 % (3620264)Termination phase: Property scanning
% 2.46/0.88 % (3620264)Time elapsed: 0.010 s
% 2.46/0.88 % (3620264)Peak memory usage: 10 MB
% 2.46/0.88 % (3620264)Instructions burned: 22 (million)
% 2.46/0.88 % (3620267)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=578224687:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/316Mi)
% 3.21/0.92 % (3620266)Instruction limit reached!
% 3.21/0.92 % (3620266)------------------------------
% 3.21/0.92 % (3620266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.21/0.92 % (3620266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.21/0.92 % (3620266)CaDiCaL version: 2.1.3
% 3.21/0.92 % (3620266)Termination reason: Instruction limit
% 3.21/0.92 % (3620266)Termination phase: Saturation
% 3.21/0.92 % (3620266)Time elapsed: 0.009 s
% 3.21/0.92 % (3620266)Peak memory usage: 11 MB
% 3.21/0.92 % (3620266)Instructions burned: 21 (million)
% 3.21/0.92 % (3620271)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=581095194:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2996 on theBenchmark for (2996ds/853Mi)
% 3.21/0.92 % (3620272)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=2072194714:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2995 on theBenchmark for (2995ds/45Mi)
% 3.21/0.92 % (3620256)Instruction limit reached!
% 3.21/0.92 % (3620256)------------------------------
% 3.21/0.92 % (3620256)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.21/0.92 % (3620256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.21/0.92 % (3620256)CaDiCaL version: 2.1.3
% 3.21/0.92 % (3620256)Termination reason: Instruction limit
% 3.21/0.92 % (3620256)Termination phase: Saturation
% 3.21/0.92 % (3620256)Time elapsed: 0.066 s
% 3.21/0.92 % (3620256)Peak memory usage: 13 MB
% 3.21/0.92 % (3620256)Instructions burned: 181 (million)
% 3.21/0.92 % (3620275)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=3734137952:i=480:rtra=on_2995 on theBenchmark for (2995ds/480Mi)
% 3.21/0.92 % (3620275)Refutation not found, incomplete strategy
% 3.21/0.92 % (3620275)------------------------------
% 3.21/0.92 % (3620275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.21/0.92 % (3620275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.21/0.92 % (3620275)CaDiCaL version: 2.1.3
% 3.21/0.92 % (3620275)Termination reason: Refutation not found, incomplete strategy
% 3.21/0.92 % (3620275)Time elapsed: 0.007 s
% 3.21/0.92 % (3620275)Peak memory usage: 12 MB
% 3.21/0.92 % (3620275)Instructions burned: 27 (million)
% 3.21/0.92 % (3620275)------------------------------
% 3.21/0.92 % (3620275)------------------------------
% 3.21/0.92 % (3620272)Instruction limit reached!
% 3.21/0.92 % (3620272)------------------------------
% 3.21/0.92 % (3620272)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.21/0.92 % (3620272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.21/0.92 % (3620272)CaDiCaL version: 2.1.3
% 3.21/0.92 % (3620272)Termination reason: Instruction limit
% 3.21/0.92 % (3620272)Termination phase: Saturation
% 3.21/0.92 % (3620272)Time elapsed: 0.023 s
% 3.21/0.92 % (3620272)Peak memory usage: 12 MB
% 3.21/0.92 % (3620272)Instructions burned: 45 (million)
% 3.21/0.92 % (3620277)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=3081732937:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2995 on theBenchmark for (2995ds/21Mi)
% 3.21/0.92 % (3620278)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 3.21/0.92 % (3620277)Instruction limit reached!
% 3.21/0.92 % (3620277)------------------------------
% 3.21/0.92 % (3620277)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.21/0.92 % (3620277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.21/0.92 % (3620277)CaDiCaL version: 2.1.3
% 3.21/0.92 % (3620277)Termination reason: Instruction limit
% 3.21/0.92 % (3620277)Termination phase: Saturation
% 3.21/0.92 % (3620277)Time elapsed: 0.006 s
% 3.21/0.92 % (3620277)Peak memory usage: 12 MB
% 3.21/0.92 % (3620277)Instructions burned: 24 (million)
% 3.21/0.92 % (3620278)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=162460312:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/200Mi)
% 3.21/0.92 % (3620249)Instruction limit reached!
% 3.21/0.92 % (3620249)------------------------------
% 3.21/0.92 % (3620249)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.55/1.13 % (3620249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.55/1.13 % (3620249)CaDiCaL version: 2.1.3
% 4.55/1.13 % (3620249)Termination reason: Instruction limit
% 4.55/1.13 % (3620249)Termination phase: Saturation
% 4.55/1.13 % (3620249)Time elapsed: 0.137 s
% 4.55/1.13 % (3620249)Peak memory usage: 12 MB
% 4.55/1.13 % (3620249)Instructions burned: 144 (million)
% 4.55/1.13 % (3620280)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=296834407:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2995 on theBenchmark for (2995ds/13Mi)
% 4.55/1.13 % (3620280)Instruction limit reached!
% 4.55/1.13 % (3620280)------------------------------
% 4.55/1.13 % (3620280)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.55/1.13 % (3620280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.55/1.13 % (3620280)CaDiCaL version: 2.1.3
% 4.55/1.13 % (3620280)Termination reason: Instruction limit
% 4.55/1.13 % (3620280)Termination phase: Property scanning
% 4.55/1.13 % (3620280)Time elapsed: 0.007 s
% 4.55/1.13 % (3620280)Peak memory usage: 11 MB
% 4.55/1.13 % (3620280)Instructions burned: 15 (million)
% 4.55/1.13 % (3620250)Instruction limit reached!
% 4.55/1.13 % (3620250)------------------------------
% 4.55/1.13 % (3620250)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.55/1.13 % (3620250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.55/1.13 % (3620250)CaDiCaL version: 2.1.3
% 4.55/1.13 % (3620250)Termination reason: Instruction limit
% 4.55/1.13 % (3620250)Termination phase: Saturation
% 4.55/1.13 % (3620250)Time elapsed: 0.163 s
% 4.55/1.13 % (3620250)Peak memory usage: 13 MB
% 4.55/1.13 % (3620250)Instructions burned: 194 (million)
% 4.55/1.13 % (3620282)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=3928788262:i=66:s2at=3:nm=2:rtra=on:rawr=on_2995 on theBenchmark for (2995ds/66Mi)
% 4.55/1.13 % (3620284)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=3618081199:i=51:fsr=off:rtra=on_2995 on theBenchmark for (2995ds/51Mi)
% 4.55/1.13 % (3620278)Instruction limit reached!
% 4.55/1.13 % (3620278)------------------------------
% 4.55/1.13 % (3620278)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.55/1.13 % (3620278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.55/1.13 % (3620278)CaDiCaL version: 2.1.3
% 4.55/1.13 % (3620278)Termination reason: Instruction limit
% 4.55/1.13 % (3620278)Termination phase: Saturation
% 4.55/1.13 % (3620278)Time elapsed: 0.051 s
% 4.55/1.13 % (3620278)Peak memory usage: 11 MB
% 4.55/1.13 % (3620278)Instructions burned: 201 (million)
% 4.55/1.13 % (3620285)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=1352700237:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/31Mi)
% 4.55/1.13 % (3620288)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=1604190351:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2994 on theBenchmark for (2994ds/137Mi)
% 4.55/1.13 % (3620285)Instruction limit reached!
% 4.55/1.13 % (3620285)------------------------------
% 4.55/1.13 % (3620285)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.55/1.13 % (3620285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.55/1.13 % (3620285)CaDiCaL version: 2.1.3
% 4.55/1.13 % (3620285)Termination reason: Instruction limit
% 4.55/1.13 % (3620285)Termination phase: Saturation
% 4.55/1.13 % (3620285)Time elapsed: 0.014 s
% 4.55/1.13 % (3620285)Peak memory usage: 11 MB
% 4.55/1.13 % (3620285)Instructions burned: 33 (million)
% 4.55/1.13 % (3620284)Refutation not found, incomplete strategy
% 4.55/1.13 % (3620284)------------------------------
% 4.55/1.13 % (3620284)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.55/1.13 % (3620284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.55/1.13 % (3620284)CaDiCaL version: 2.1.3
% 4.55/1.13 % (3620284)Termination reason: Refutation not found, incomplete strategy
% 4.55/1.13 % (3620284)Time elapsed: 0.026 s
% 4.55/1.13 % (3620284)Peak memory usage: 12 MB
% 4.55/1.13 % (3620284)Instructions burned: 30 (million)
% 4.55/1.13 % (3620284)------------------------------
% 4.55/1.13 % (3620284)------------------------------
% 4.55/1.13 % (3620291)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=1105493126:cond=on:i=34:hud=10:nm=10:rtra=on_2994 on theBenchmark for (2994ds/34Mi)
% 5.69/1.30 % (3620282)Instruction limit reached!
% 5.69/1.30 % (3620282)------------------------------
% 5.69/1.30 % (3620282)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.69/1.30 % (3620282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.69/1.30 % (3620282)CaDiCaL version: 2.1.3
% 5.69/1.30 % (3620282)Termination reason: Instruction limit
% 5.69/1.30 % (3620282)Termination phase: Saturation
% 5.69/1.30 % (3620282)Time elapsed: 0.055 s
% 5.69/1.30 % (3620282)Peak memory usage: 13 MB
% 5.69/1.30 % (3620282)Instructions burned: 66 (million)
% 5.69/1.30 % (3620267)Instruction limit reached!
% 5.69/1.30 % (3620267)------------------------------
% 5.69/1.30 % (3620267)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.69/1.30 % (3620267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.69/1.30 % (3620267)CaDiCaL version: 2.1.3
% 5.69/1.30 % (3620267)Termination reason: Instruction limit
% 5.69/1.30 % (3620267)Termination phase: Saturation
% 5.69/1.30 % (3620267)Time elapsed: 0.171 s
% 5.69/1.30 % (3620267)Peak memory usage: 16 MB
% 5.69/1.30 % (3620267)Instructions burned: 318 (million)
% 5.69/1.30 % (3620288)Instruction limit reached!
% 5.69/1.30 % (3620288)------------------------------
% 5.69/1.30 % (3620288)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.69/1.30 % (3620288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.69/1.30 % (3620288)CaDiCaL version: 2.1.3
% 5.69/1.30 % (3620288)Termination reason: Instruction limit
% 5.69/1.30 % (3620288)Termination phase: Saturation
% 5.69/1.30 % (3620288)Time elapsed: 0.041 s
% 5.69/1.30 % (3620288)Peak memory usage: 13 MB
% 5.69/1.30 % (3620288)Instructions burned: 137 (million)
% 5.69/1.30 % (3620292)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=4227574833:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2994 on theBenchmark for (2994ds/67Mi)
% 5.69/1.30 % (3620291)Instruction limit reached!
% 5.69/1.30 % (3620291)------------------------------
% 5.69/1.30 % (3620291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.69/1.30 % (3620291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.69/1.30 % (3620291)CaDiCaL version: 2.1.3
% 5.69/1.30 % (3620291)Termination reason: Instruction limit
% 5.69/1.30 % (3620291)Termination phase: Saturation
% 5.69/1.30 % (3620291)Time elapsed: 0.017 s
% 5.69/1.30 % (3620291)Peak memory usage: 12 MB
% 5.69/1.30 % (3620291)Instructions burned: 35 (million)
% 5.69/1.30 % (3620295)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=139351261:st=2:i=246:sd=3:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/246Mi)
% 5.69/1.30 % (3620296)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=2694064051:cond=on:i=96:bd=all:rtra=on_2994 on theBenchmark for (2994ds/96Mi)
% 5.69/1.30 % (3620294)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 5.69/1.30 % (3620298)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=3475522311:i=427:sd=1:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/427Mi)
% 5.69/1.30 % (3620292)Refutation not found, incomplete strategy
% 5.69/1.30 % (3620292)------------------------------
% 5.69/1.30 % (3620292)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.69/1.30 % (3620292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.69/1.30 % (3620292)CaDiCaL version: 2.1.3
% 5.69/1.30 % (3620292)Termination reason: Refutation not found, incomplete strategy
% 5.69/1.30 % (3620292)Time elapsed: 0.023 s
% 5.69/1.30 % (3620292)Peak memory usage: 12 MB
% 5.69/1.30 % (3620292)Instructions burned: 26 (million)
% 5.69/1.30 % (3620292)------------------------------
% 5.69/1.30 % (3620292)------------------------------
% 5.69/1.30 % (3620298)Refutation not found, incomplete strategy
% 5.69/1.30 % (3620298)------------------------------
% 5.69/1.30 % (3620298)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.69/1.30 % (3620298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.69/1.30 % (3620298)CaDiCaL version: 2.1.3
% 5.69/1.30 % (3620298)Termination reason: Refutation not found, incomplete strategy
% 5.69/1.30 % (3620298)Time elapsed: 0.005 s
% 5.69/1.30 % (3620298)Peak memory usage: 12 MB
% 5.69/1.30 % (3620298)Instructions burned: 9 (million)
% 5.69/1.30 % (3620294)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=1925995378:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2994 on theBenchmark for (2994ds/180Mi)
% 5.69/1.39 % (3620298)------------------------------
% 5.69/1.39 % (3620298)------------------------------
% 5.69/1.39 % (3620304)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=2407829543:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/515Mi)
% 5.69/1.39 % (3620303)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=189609410:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/874Mi)
% 5.69/1.39 % (3620296)Instruction limit reached!
% 5.69/1.39 % (3620296)------------------------------
% 5.69/1.39 % (3620296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.69/1.39 % (3620296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.69/1.39 % (3620296)CaDiCaL version: 2.1.3
% 5.69/1.39 % (3620296)Termination reason: Instruction limit
% 5.69/1.39 % (3620296)Termination phase: Saturation
% 5.69/1.39 % (3620296)Time elapsed: 0.051 s
% 5.69/1.39 % (3620296)Peak memory usage: 13 MB
% 5.69/1.39 % (3620296)Instructions burned: 97 (million)
% 5.69/1.39 % (3620307)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=1023108352:st=1.5:i=130:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/130Mi)
% 5.69/1.39 % (3620307)Refutation not found, incomplete strategy
% 5.69/1.39 % (3620307)------------------------------
% 5.69/1.39 % (3620307)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.69/1.39 % (3620307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.69/1.39 % (3620307)CaDiCaL version: 2.1.3
% 5.69/1.39 % (3620307)Termination reason: Refutation not found, incomplete strategy
% 5.69/1.39 % (3620307)Time elapsed: 0.045 s
% 5.69/1.39 % (3620307)Peak memory usage: 12 MB
% 5.69/1.39 % (3620307)Instructions burned: 53 (million)
% 5.69/1.39 % (3620307)------------------------------
% 5.69/1.39 % (3620307)------------------------------
% 5.69/1.39 % (3620309)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3186424073:i=44:ep=R:rtra=on:ntd=on_2992 on theBenchmark for (2992ds/44Mi)
% 5.69/1.39 % (3620309)Instruction limit reached!
% 5.69/1.39 % (3620309)------------------------------
% 5.69/1.39 % (3620309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.69/1.39 % (3620309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.69/1.39 % (3620309)CaDiCaL version: 2.1.3
% 5.69/1.39 % (3620309)Termination reason: Instruction limit
% 5.69/1.39 % (3620309)Termination phase: Saturation
% 5.69/1.39 % (3620309)Time elapsed: 0.023 s
% 5.69/1.39 % (3620309)Peak memory usage: 12 MB
% 5.69/1.39 % (3620309)Instructions burned: 44 (million)
% 5.69/1.39 % (3620294)Instruction limit reached!
% 5.69/1.39 % (3620294)------------------------------
% 5.69/1.39 % (3620294)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.69/1.39 % (3620294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.69/1.39 % (3620294)CaDiCaL version: 2.1.3
% 5.69/1.39 % (3620294)Termination reason: Instruction limit
% 5.69/1.39 % (3620294)Termination phase: Saturation
% 5.69/1.39 % (3620294)Time elapsed: 0.156 s
% 5.69/1.39 % (3620294)Peak memory usage: 13 MB
% 5.69/1.39 % (3620294)Instructions burned: 181 (million)
% 5.69/1.39 % (3620311)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=797338118:s2a=on:i=571:nm=16:rtra=on_2992 on theBenchmark for (2992ds/571Mi)
% 5.69/1.39 % (3620312)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=3979783711:i=450:rtra=on:ixr=off:ntd=on_2992 on theBenchmark for (2992ds/450Mi)
% 5.69/1.39 % (3620311)Refutation not found, incomplete strategy
% 5.69/1.39 % (3620311)------------------------------
% 5.69/1.39 % (3620311)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.69/1.39 % (3620311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.69/1.39 % (3620311)CaDiCaL version: 2.1.3
% 5.69/1.39 % (3620311)Termination reason: Refutation not found, incomplete strategy
% 5.69/1.39 % (3620311)Time elapsed: 0.015 s
% 5.69/1.39 % (3620311)Peak memory usage: 12 MB
% 5.69/1.39 % (3620311)Instructions burned: 29 (million)
% 5.69/1.39 % (3620311)------------------------------
% 5.69/1.39 % (3620311)------------------------------
% 5.69/1.39 % (3620315)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=1725824281:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2992 on theBenchmark for (2992ds/95Mi)
% 6.37/1.49 % (3620295)Instruction limit reached!
% 6.37/1.49 % (3620295)------------------------------
% 6.37/1.49 % (3620295)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.37/1.49 % (3620295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.37/1.49 % (3620295)CaDiCaL version: 2.1.3
% 6.37/1.49 % (3620295)Termination reason: Instruction limit
% 6.37/1.49 % (3620295)Termination phase: Saturation
% 6.37/1.49 % (3620295)Time elapsed: 0.230 s
% 6.37/1.49 % (3620295)Peak memory usage: 13 MB
% 6.37/1.49 % (3620295)Instructions burned: 248 (million)
% 6.37/1.49 % (3620271)Instruction limit reached!
% 6.37/1.49 % (3620271)------------------------------
% 6.37/1.49 % (3620271)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.37/1.49 % (3620271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.37/1.49 % (3620271)CaDiCaL version: 2.1.3
% 6.37/1.49 % (3620271)Termination reason: Instruction limit
% 6.37/1.49 % (3620271)Termination phase: Saturation
% 6.37/1.49 % (3620271)Time elapsed: 0.442 s
% 6.37/1.49 % (3620271)Peak memory usage: 17 MB
% 6.37/1.49 % (3620271)Instructions burned: 855 (million)
% 6.37/1.49 % (3620315)Instruction limit reached!
% 6.37/1.49 % (3620315)------------------------------
% 6.37/1.49 % (3620315)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.37/1.49 % (3620315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.37/1.49 % (3620315)CaDiCaL version: 2.1.3
% 6.37/1.49 % (3620315)Termination reason: Instruction limit
% 6.37/1.49 % (3620315)Termination phase: Saturation
% 6.37/1.49 % (3620315)Time elapsed: 0.050 s
% 6.37/1.49 % (3620315)Peak memory usage: 12 MB
% 6.37/1.49 % (3620315)Instructions burned: 97 (million)
% 6.37/1.49 % (3620317)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=3152871197:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2991 on theBenchmark for (2991ds/65Mi)
% 6.37/1.49 % (3620320)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=728644618:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2991 on theBenchmark for (2991ds/5755Mi)
% 6.37/1.49 % (3620318)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=3672461758:uwa_fpi=on:avsq=on:s2a=on:cond=fast:i=105:s2at=1.5:aac=none:fgj=on:piset=and:hud=3:fsr=off:rtra=on:er=filter:rawr=on_2991 on theBenchmark for (2991ds/105Mi)
% 6.37/1.49 % (3620317)Instruction limit reached!
% 6.37/1.49 % (3620317)------------------------------
% 6.37/1.49 % (3620317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.37/1.49 % (3620317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.37/1.49 % (3620317)CaDiCaL version: 2.1.3
% 6.37/1.49 % (3620317)Termination reason: Instruction limit
% 6.37/1.49 % (3620317)Termination phase: Saturation
% 6.37/1.49 % (3620317)Time elapsed: 0.034 s
% 6.37/1.49 % (3620317)Peak memory usage: 12 MB
% 6.37/1.49 % (3620317)Instructions burned: 66 (million)
% 6.37/1.49 % (3620323)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=427642834:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/375Mi)
% 6.37/1.49 % (3620246)Instruction limit reached!
% 6.37/1.49 % (3620246)------------------------------
% 6.37/1.49 % (3620246)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.37/1.49 % (3620246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.37/1.49 % (3620246)CaDiCaL version: 2.1.3
% 6.37/1.49 % (3620246)Termination reason: Instruction limit
% 6.37/1.49 % (3620246)Termination phase: Saturation
% 6.37/1.49 % (3620246)Time elapsed: 0.640 s
% 6.37/1.49 % (3620246)Peak memory usage: 17 MB
% 6.37/1.49 % (3620246)Instructions burned: 1241 (million)
% 6.37/1.49 % (3620325)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=3855763563:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2990 on theBenchmark for (2990ds/495Mi)
% 6.37/1.49 % (3620318)Instruction limit reached!
% 6.37/1.49 % (3620318)------------------------------
% 6.37/1.49 % (3620318)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.30/1.61 % (3620318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.30/1.61 % (3620318)CaDiCaL version: 2.1.3
% 7.30/1.61 % (3620318)Termination reason: Instruction limit
% 7.30/1.61 % (3620318)Termination phase: Saturation
% 7.30/1.61 % (3620318)Time elapsed: 0.096 s
% 7.30/1.61 % (3620318)Peak memory usage: 13 MB
% 7.30/1.61 % (3620318)Instructions burned: 106 (million)
% 7.30/1.61 % (3620304)Instruction limit reached!
% 7.30/1.61 % (3620304)------------------------------
% 7.30/1.61 % (3620304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.30/1.61 % (3620304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.30/1.61 % (3620304)CaDiCaL version: 2.1.3
% 7.30/1.61 % (3620304)Termination reason: Instruction limit
% 7.30/1.61 % (3620304)Termination phase: Saturation
% 7.30/1.61 % (3620304)Time elapsed: 0.375 s
% 7.30/1.61 % (3620304)Peak memory usage: 13 MB
% 7.30/1.61 % (3620304)Instructions burned: 515 (million)
% 7.30/1.61 % (3620312)Instruction limit reached!
% 7.30/1.61 % (3620312)------------------------------
% 7.30/1.61 % (3620312)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.30/1.61 % (3620312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.30/1.61 % (3620312)CaDiCaL version: 2.1.3
% 7.30/1.61 % (3620312)Termination reason: Instruction limit
% 7.30/1.61 % (3620312)Termination phase: Saturation
% 7.30/1.61 % (3620312)Time elapsed: 0.233 s
% 7.30/1.61 % (3620312)Peak memory usage: 14 MB
% 7.30/1.61 % (3620312)Instructions burned: 450 (million)
% 7.30/1.61 % (3620327)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=2892867542:cond=on:i=34:hud=10:nm=10:rtra=on_2990 on theBenchmark for (2990ds/34Mi)
% 7.30/1.61 % (3620329)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=784585568:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2989 on theBenchmark for (2989ds/66Mi)
% 7.30/1.61 % (3620328)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=2081586432:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2990 on theBenchmark for (2990ds/91Mi)
% 7.30/1.61 % (3620329)Refutation not found, incomplete strategy
% 7.30/1.61 % (3620329)------------------------------
% 7.30/1.61 % (3620329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.30/1.61 % (3620329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.30/1.61 % (3620329)CaDiCaL version: 2.1.3
% 7.30/1.61 % (3620329)Termination reason: Refutation not found, incomplete strategy
% 7.30/1.61 % (3620329)Time elapsed: 0.011 s
% 7.30/1.61 % (3620329)Peak memory usage: 12 MB
% 7.30/1.61 % (3620329)Instructions burned: 22 (million)
% 7.30/1.61 % (3620329)------------------------------
% 7.30/1.61 % (3620329)------------------------------
% 7.30/1.61 % (3620333)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=597848111:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2989 on theBenchmark for (2989ds/22Mi)
% 7.30/1.61 % (3620327)Instruction limit reached!
% 7.30/1.61 % (3620327)------------------------------
% 7.30/1.61 % (3620327)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.30/1.61 % (3620303)Instruction limit reached!
% 7.30/1.61 % (3620303)------------------------------
% 7.30/1.61 % (3620303)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.30/1.61 % (3620327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.30/1.61 % (3620303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.30/1.61 % (3620303)CaDiCaL version: 2.1.3
% 7.30/1.61 % (3620327)CaDiCaL version: 2.1.3
% 7.30/1.61 % (3620303)Termination reason: Instruction limit
% 7.30/1.61 % (3620303)Termination phase: Saturation
% 7.30/1.61 % (3620327)Termination reason: Instruction limit
% 7.30/1.61 % (3620327)Termination phase: Saturation
% 7.30/1.61 % (3620327)Time elapsed: 0.035 s
% 7.30/1.61 % (3620303)Time elapsed: 0.426 s
% 7.30/1.61 % (3620303)Peak memory usage: 14 MB
% 7.30/1.61 % (3620327)Peak memory usage: 12 MB
% 7.30/1.61 % (3620303)Instructions burned: 875 (million)
% 7.30/1.61 % (3620327)Instructions burned: 35 (million)
% 7.30/1.61 % (3620333)Instruction limit reached!
% 7.30/1.61 % (3620333)------------------------------
% 7.30/1.61 % (3620333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.30/1.61 % (3620333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.30/1.61 % (3620333)CaDiCaL version: 2.1.3
% 7.58/1.78 % (3620333)Termination reason: Instruction limit
% 7.58/1.78 % (3620333)Termination phase: Property scanning
% 7.58/1.78 % (3620333)Time elapsed: 0.011 s
% 7.58/1.78 % (3620333)Peak memory usage: 10 MB
% 7.58/1.78 % (3620333)Instructions burned: 23 (million)
% 7.58/1.78 % (3620328)Instruction limit reached!
% 7.58/1.78 % (3620328)------------------------------
% 7.58/1.78 % (3620328)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.58/1.78 % (3620328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.58/1.78 % (3620328)CaDiCaL version: 2.1.3
% 7.58/1.78 % (3620328)Termination reason: Instruction limit
% 7.58/1.78 % (3620328)Termination phase: Saturation
% 7.58/1.78 % (3620328)Time elapsed: 0.043 s
% 7.58/1.78 % (3620328)Peak memory usage: 12 MB
% 7.58/1.78 % (3620328)Instructions burned: 91 (million)
% 7.58/1.78 % (3620335)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=3183069887:i=338:bd=all:ins=4:rtra=on_2989 on theBenchmark for (2989ds/338Mi)
% 7.58/1.78 % (3620336)lrs+10_1_sil=128000:si=on:urr=on:random_seed=528482434:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2989 on theBenchmark for (2989ds/28Mi)
% 7.58/1.78 % (3620337)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 7.58/1.78 % (3620337)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=4114241640:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2989 on theBenchmark for (2989ds/137Mi)
% 7.58/1.78 % (3620338)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=1172882660:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2989 on theBenchmark for (2989ds/340Mi)
% 7.58/1.78 % (3620336)Instruction limit reached!
% 7.58/1.78 % (3620336)------------------------------
% 7.58/1.78 % (3620336)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.58/1.78 % (3620336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.58/1.78 % (3620336)CaDiCaL version: 2.1.3
% 7.58/1.78 % (3620336)Termination reason: Instruction limit
% 7.58/1.78 % (3620336)Termination phase: Saturation
% 7.58/1.78 % (3620336)Time elapsed: 0.024 s
% 7.58/1.78 % (3620336)Peak memory usage: 11 MB
% 7.58/1.78 % (3620336)Instructions burned: 29 (million)
% 7.58/1.78 % (3620343)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=2275795173:i=227:sd=1:bd=all:rtra=on:ss=axioms_2988 on theBenchmark for (2988ds/227Mi)
% 7.58/1.78 % (3620343)Refutation not found, incomplete strategy
% 7.58/1.78 % (3620343)------------------------------
% 7.58/1.78 % (3620343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.58/1.78 % (3620343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.58/1.78 % (3620343)CaDiCaL version: 2.1.3
% 7.58/1.78 % (3620343)Termination reason: Refutation not found, incomplete strategy
% 7.58/1.78 % (3620343)Time elapsed: 0.005 s
% 7.58/1.78 % (3620343)Peak memory usage: 12 MB
% 7.58/1.78 % (3620343)Instructions burned: 9 (million)
% 7.58/1.78 % (3620343)------------------------------
% 7.58/1.78 % (3620343)------------------------------
% 7.58/1.78 % (3620345)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 7.58/1.78 % (3620345)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=2858143231:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2988 on theBenchmark for (2988ds/373Mi)
% 7.58/1.78 % (3620337)Instruction limit reached!
% 7.58/1.78 % (3620337)------------------------------
% 7.58/1.78 % (3620337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.58/1.78 % (3620337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.58/1.78 % (3620337)CaDiCaL version: 2.1.3
% 7.58/1.78 % (3620337)Termination reason: Instruction limit
% 7.58/1.78 % (3620337)Termination phase: Saturation
% 7.58/1.78 % (3620337)Time elapsed: 0.068 s
% 7.58/1.78 % (3620337)Peak memory usage: 13 MB
% 7.58/1.78 % (3620337)Instructions burned: 137 (million)
% 7.58/1.78 % (3620335)Instruction limit reached!
% 7.58/1.78 % (3620335)------------------------------
% 7.58/1.78 % (3620335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.58/1.78 % (3620335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.43/1.85 % (3620335)CaDiCaL version: 2.1.3
% 8.43/1.85 % (3620335)Termination reason: Instruction limit
% 8.43/1.85 % (3620335)Termination phase: Saturation
% 8.43/1.85 % (3620335)Time elapsed: 0.097 s
% 8.43/1.85 % (3620335)Peak memory usage: 15 MB
% 8.43/1.85 % (3620335)Instructions burned: 340 (million)
% 8.43/1.85 % (3620347)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=2538319869:i=116:ep=RSTC:rtra=on:ntd=on_2988 on theBenchmark for (2988ds/116Mi)
% 8.43/1.85 % (3620348)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=1990585169:i=575:rtra=on_2988 on theBenchmark for (2988ds/575Mi)
% 8.43/1.85 % (3620323)Instruction limit reached!
% 8.43/1.85 % (3620323)------------------------------
% 8.43/1.85 % (3620323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.43/1.85 % (3620323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.43/1.85 % (3620323)CaDiCaL version: 2.1.3
% 8.43/1.85 % (3620323)Termination reason: Instruction limit
% 8.43/1.85 % (3620323)Termination phase: Saturation
% 8.43/1.85 % (3620323)Time elapsed: 0.268 s
% 8.43/1.85 % (3620323)Peak memory usage: 13 MB
% 8.43/1.85 % (3620323)Instructions burned: 375 (million)
% 8.43/1.85 % (3620348)Refutation not found, incomplete strategy
% 8.43/1.85 % (3620348)------------------------------
% 8.43/1.85 % (3620348)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.43/1.85 % (3620348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.43/1.85 % (3620348)CaDiCaL version: 2.1.3
% 8.43/1.85 % (3620348)Termination reason: Refutation not found, incomplete strategy
% 8.43/1.85 % (3620348)Time elapsed: 0.006 s
% 8.43/1.85 % (3620348)Peak memory usage: 12 MB
% 8.43/1.85 % (3620348)Instructions burned: 24 (million)
% 8.43/1.85 % (3620348)------------------------------
% 8.43/1.85 % (3620348)------------------------------
% 8.43/1.85 % (3620352)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=351577334: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_2988 on theBenchmark for (2988ds/9840Mi)
% 8.43/1.85 % (3620351)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=3686288098:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2988 on theBenchmark for (2988ds/270Mi)
% 8.43/1.85 % (3620325)Instruction limit reached!
% 8.43/1.85 % (3620325)------------------------------
% 8.43/1.85 % (3620325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.43/1.85 % (3620325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.43/1.85 % (3620325)CaDiCaL version: 2.1.3
% 8.43/1.85 % (3620325)Termination reason: Instruction limit
% 8.43/1.85 % (3620325)Termination phase: Saturation
% 8.43/1.85 % (3620325)Time elapsed: 0.284 s
% 8.43/1.85 % (3620325)Peak memory usage: 14 MB
% 8.43/1.85 % (3620325)Instructions burned: 496 (million)
% 8.43/1.85 % (3620347)Instruction limit reached!
% 8.43/1.85 % (3620347)------------------------------
% 8.43/1.85 % (3620347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.43/1.85 % (3620347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.43/1.85 % (3620347)CaDiCaL version: 2.1.3
% 8.43/1.85 % (3620347)Termination reason: Instruction limit
% 8.43/1.85 % (3620347)Termination phase: Saturation
% 8.43/1.85 % (3620347)Time elapsed: 0.091 s
% 8.43/1.85 % (3620347)Peak memory usage: 13 MB
% 8.43/1.85 % (3620347)Instructions burned: 116 (million)
% 8.43/1.85 % (3620356)lrs+1010_1_sil=128000:si=on:sos=all:uwa=off:nwc=1:random_seed=2920504521:i=421:rtra=on:ss=axioms_2987 on theBenchmark for (2987ds/421Mi)
% 8.43/1.85 % (3620357)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
% 8.43/1.85 % (3620356)Refutation not found, incomplete strategy
% 8.43/1.85 % (3620356)------------------------------
% 8.43/1.85 % (3620356)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.43/1.85 % (3620356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.43/1.85 % (3620356)CaDiCaL version: 2.1.3
% 8.43/1.85 % (3620356)Termination reason: Refutation not found, incomplete strategy
% 11.34/2.12 % (3620356)Time elapsed: 0.011 s
% 11.34/2.12 % (3620356)Peak memory usage: 12 MB
% 11.34/2.12 % (3620356)Instructions burned: 21 (million)
% 11.34/2.12 % (3620357)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=795715664:avsq=on:i=270:s2at=3:avsqr=1,16:rtra=on:ntd=on_2987 on theBenchmark for (2987ds/270Mi)
% 11.34/2.12 % (3620356)------------------------------
% 11.34/2.12 % (3620356)------------------------------
% 11.34/2.12 % (3620360)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=978042667:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2987 on theBenchmark for (2987ds/31Mi)
% 11.34/2.12 % (3620360)Instruction limit reached!
% 11.34/2.12 % (3620360)------------------------------
% 11.34/2.12 % (3620360)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.34/2.12 % (3620360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.34/2.12 % (3620360)CaDiCaL version: 2.1.3
% 11.34/2.12 % (3620360)Termination reason: Instruction limit
% 11.34/2.12 % (3620360)Termination phase: Saturation
% 11.34/2.12 % (3620360)Time elapsed: 0.014 s
% 11.34/2.12 % (3620360)Peak memory usage: 11 MB
% 11.34/2.12 % (3620360)Instructions burned: 32 (million)
% 11.34/2.12 % (3620362)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 11.34/2.12 % (3620362)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
% 11.34/2.12 % (3620362)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=1339695463:hsqr=1,8:i=1440:s2at=5:add=on:nm=2:rtra=on_2986 on theBenchmark for (2986ds/1440Mi)
% 11.34/2.12 % (3620345)Instruction limit reached!
% 11.34/2.12 % (3620345)------------------------------
% 11.34/2.12 % (3620345)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.34/2.12 % (3620345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.34/2.12 % (3620345)CaDiCaL version: 2.1.3
% 11.34/2.12 % (3620345)Termination reason: Instruction limit
% 11.34/2.12 % (3620345)Termination phase: Saturation
% 11.34/2.12 % (3620345)Time elapsed: 0.186 s
% 11.34/2.12 % (3620345)Peak memory usage: 13 MB
% 11.34/2.12 % (3620345)Instructions burned: 374 (million)
% 11.34/2.12 % (3620364)dis+10_2_sil=128000:si=on:random_seed=2649583293:s2a=on:i=339:av=off:rtra=on:fe=abstraction:ss=axioms:fsd=on:ntd=on_2986 on theBenchmark for (2986ds/339Mi)
% 11.34/2.12 % (3620338)Instruction limit reached!
% 11.34/2.12 % (3620338)------------------------------
% 11.34/2.12 % (3620338)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.34/2.12 % (3620338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.34/2.12 % (3620338)CaDiCaL version: 2.1.3
% 11.34/2.12 % (3620338)Termination reason: Instruction limit
% 11.34/2.12 % (3620338)Termination phase: Saturation
% 11.34/2.12 % (3620338)Time elapsed: 0.281 s
% 11.34/2.12 % (3620338)Peak memory usage: 14 MB
% 11.34/2.12 % (3620338)Instructions burned: 341 (million)
% 11.34/2.12 % (3620366)lrs+2_16:1_si=on:cbe=off:uwa=interpreted_only:random_seed=2616260432:i=111:add=on:fgj=on:rtra=on:fdi=1024_2986 on theBenchmark for (2986ds/111Mi)
% 11.34/2.12 % (3620357)Instruction limit reached!
% 11.34/2.12 % (3620357)------------------------------
% 11.34/2.12 % (3620357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.34/2.12 % (3620357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.34/2.12 % (3620357)CaDiCaL version: 2.1.3
% 11.34/2.12 % (3620357)Termination reason: Instruction limit
% 11.34/2.12 % (3620357)Termination phase: Saturation
% 11.34/2.12 % (3620357)Time elapsed: 0.134 s
% 11.34/2.12 % (3620357)Peak memory usage: 13 MB
% 11.34/2.12 % (3620357)Instructions burned: 271 (million)
% 11.34/2.12 % (3620369)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=1965653692:st=3:avsq=on:i=122:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2985 on theBenchmark for (2985ds/122Mi)
% 11.34/2.12 % (3620369)Refutation not found, incomplete strategy
% 11.34/2.12 % (3620369)------------------------------
% 11.34/2.12 % (3620369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.34/2.12 % (3620369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.91/2.33 % (3620369)CaDiCaL version: 2.1.3
% 12.91/2.33 % (3620369)Termination reason: Refutation not found, incomplete strategy
% 12.91/2.33 % (3620369)Time elapsed: 0.013 s
% 12.91/2.33 % (3620369)Peak memory usage: 12 MB
% 12.91/2.33 % (3620369)Instructions burned: 24 (million)
% 12.91/2.33 % (3620369)------------------------------
% 12.91/2.33 % (3620369)------------------------------
% 12.91/2.33 % (3620351)Instruction limit reached!
% 12.91/2.33 % (3620351)------------------------------
% 12.91/2.33 % (3620351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.91/2.33 % (3620351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.91/2.33 % (3620351)CaDiCaL version: 2.1.3
% 12.91/2.33 % (3620351)Termination reason: Instruction limit
% 12.91/2.33 % (3620351)Termination phase: Saturation
% 12.91/2.33 % (3620351)Time elapsed: 0.237 s
% 12.91/2.33 % (3620351)Peak memory usage: 13 MB
% 12.91/2.33 % (3620351)Instructions burned: 271 (million)
% 12.91/2.33 % (3620366)Instruction limit reached!
% 12.91/2.33 % (3620366)------------------------------
% 12.91/2.33 % (3620366)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.91/2.33 % (3620366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.91/2.33 % (3620366)CaDiCaL version: 2.1.3
% 12.91/2.33 % (3620366)Termination reason: Instruction limit
% 12.91/2.33 % (3620366)Termination phase: Saturation
% 12.91/2.33 % (3620366)Time elapsed: 0.058 s
% 12.91/2.33 % (3620366)Peak memory usage: 13 MB
% 12.91/2.33 % (3620366)Instructions burned: 111 (million)
% 12.91/2.33 % (3620374)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=820713010:i=1254:kws=precedence:bd=preordered:av=off:rtra=on_2985 on theBenchmark for (2985ds/1254Mi)
% 12.91/2.33 % (3620373)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=932308893:hsq=on:st=2:i=232:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2985 on theBenchmark for (2985ds/232Mi)
% 12.91/2.33 % (3620372)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=3502864348:uwa_fpi=on:avsq=on:i=136:avsqr=1,32:hud=15:nm=0:rtra=on:ntd=on_2985 on theBenchmark for (2985ds/136Mi)
% 12.91/2.33 % (3620374)Refutation not found, incomplete strategy
% 12.91/2.33 % (3620374)------------------------------
% 12.91/2.33 % (3620374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.91/2.33 % (3620374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.91/2.33 % (3620374)CaDiCaL version: 2.1.3
% 12.91/2.33 % (3620374)Termination reason: Refutation not found, incomplete strategy
% 12.91/2.33 % (3620374)Time elapsed: 0.017 s
% 12.91/2.33 % (3620374)Peak memory usage: 12 MB
% 12.91/2.33 % (3620374)Instructions burned: 37 (million)
% 12.91/2.33 % (3620374)------------------------------
% 12.91/2.33 % (3620374)------------------------------
% 12.91/2.33 % (3620372)Refutation not found, incomplete strategy
% 12.91/2.33 % (3620372)------------------------------
% 12.91/2.33 % (3620372)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.91/2.33 % (3620372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.91/2.33 % (3620372)CaDiCaL version: 2.1.3
% 12.91/2.33 % (3620372)Termination reason: Refutation not found, incomplete strategy
% 12.91/2.33 % (3620372)Time elapsed: 0.025 s
% 12.91/2.33 % (3620372)Peak memory usage: 12 MB
% 12.91/2.33 % (3620372)Instructions burned: 28 (million)
% 12.91/2.33 % (3620378)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 12.91/2.33 % (3620372)------------------------------
% 12.91/2.33 % (3620372)------------------------------
% 12.91/2.33 % (3620378)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=3740457362:s2a=on:i=281:add=on:rtra=on:fe=axiom:fdi=1024_2984 on theBenchmark for (2984ds/281Mi)
% 12.91/2.33 % (3620364)Instruction limit reached!
% 12.91/2.33 % (3620364)------------------------------
% 12.91/2.33 % (3620364)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.91/2.33 % (3620364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.91/2.33 % (3620364)CaDiCaL version: 2.1.3
% 12.91/2.33 % (3620364)Termination reason: Instruction limit
% 12.91/2.33 % (3620364)Termination phase: Saturation
% 12.91/2.33 % (3620364)Time elapsed: 0.168 s
% 12.91/2.33 % (3620364)Peak memory usage: 13 MB
% 10.96/2.40 % (3620364)Instructions burned: 339 (million)
% 10.96/2.40 % (3620381)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=3728809155:i=865:bs=unit_only:ins=25:rtra=on:ntd=on_2984 on theBenchmark for (2984ds/865Mi)
% 10.96/2.40 % (3620379)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=1602557173:i=619:add=on:rtra=on_2984 on theBenchmark for (2984ds/619Mi)
% 10.96/2.40 % (3620379)Refutation not found, incomplete strategy
% 10.96/2.40 % (3620379)------------------------------
% 10.96/2.40 % (3620379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.96/2.40 % (3620379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.40 % (3620379)CaDiCaL version: 2.1.3
% 10.96/2.40 % (3620379)Termination reason: Refutation not found, incomplete strategy
% 10.96/2.40 % (3620379)Time elapsed: 0.021 s
% 10.96/2.40 % (3620379)Peak memory usage: 12 MB
% 10.96/2.40 % (3620379)Instructions burned: 24 (million)
% 10.96/2.40 % (3620379)------------------------------
% 10.96/2.40 % (3620379)------------------------------
% 10.96/2.40 % (3620384)lrs+10_1_sil=128000:si=on:urr=on:random_seed=2881928207:i=212:sd=1:rtra=on:ss=axioms:sgt=64_2984 on theBenchmark for (2984ds/212Mi)
% 10.96/2.40 % (3620373)Instruction limit reached!
% 10.96/2.40 % (3620373)------------------------------
% 10.96/2.40 % (3620373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.96/2.40 % (3620373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.40 % (3620373)CaDiCaL version: 2.1.3
% 10.96/2.40 % (3620373)Termination reason: Instruction limit
% 10.96/2.40 % (3620373)Termination phase: Saturation
% 10.96/2.40 % (3620373)Time elapsed: 0.191 s
% 10.96/2.40 % (3620373)Peak memory usage: 12 MB
% 10.96/2.40 % (3620373)Instructions burned: 233 (million)
% 10.96/2.40 % (3620387)lrs+1010_64_sil=128000:si=on:avsql=on:uwa=off:random_seed=3585094357:hsq=on:st=3:avsq=on:i=130:avsqr=1,16:sd=1:rtra=on:ss=axioms_2983 on theBenchmark for (2983ds/130Mi)
% 10.96/2.40 % (3620378)Instruction limit reached!
% 10.96/2.40 % (3620378)------------------------------
% 10.96/2.40 % (3620378)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.96/2.40 % (3620378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.40 % (3620378)CaDiCaL version: 2.1.3
% 10.96/2.40 % (3620378)Termination reason: Instruction limit
% 10.96/2.40 % (3620378)Termination phase: Saturation
% 10.96/2.40 % (3620378)Time elapsed: 0.226 s
% 10.96/2.40 % (3620378)Peak memory usage: 14 MB
% 10.96/2.40 % (3620378)Instructions burned: 281 (million)
% 10.96/2.40 % (3620389)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=1132763532:st=1.5:i=346:rtra=on:ss=axioms_2982 on theBenchmark for (2982ds/346Mi)
% 10.96/2.40 % (3620387)Instruction limit reached!
% 10.96/2.40 % (3620387)------------------------------
% 10.96/2.40 % (3620387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.96/2.40 % (3620387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.40 % (3620387)CaDiCaL version: 2.1.3
% 10.96/2.40 % (3620387)Termination reason: Instruction limit
% 10.96/2.40 % (3620387)Termination phase: Saturation
% 10.96/2.40 % (3620387)Time elapsed: 0.073 s
% 10.96/2.40 % (3620387)Peak memory usage: 13 MB
% 10.96/2.40 % (3620387)Instructions burned: 130 (million)
% 10.96/2.40 % (3620384)Instruction limit reached!
% 10.96/2.40 % (3620384)------------------------------
% 10.96/2.40 % (3620384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.96/2.40 % (3620384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.40 % (3620384)CaDiCaL version: 2.1.3
% 10.96/2.40 % (3620384)Termination reason: Instruction limit
% 10.96/2.40 % (3620384)Termination phase: Saturation
% 10.96/2.40 % (3620384)Time elapsed: 0.181 s
% 10.96/2.40 % (3620384)Peak memory usage: 13 MB
% 10.96/2.40 % (3620384)Instructions burned: 212 (million)
% 10.96/2.40 % (3620391)lrs+1010_3_sil=128000:si=on:slsq=on:random_seed=165421023:avsq=on:i=152:avsqr=8,1:hud=5:ins=1:fsr=off:rtra=on_2982 on theBenchmark for (2982ds/152Mi)
% 10.96/2.40 % (3620389)Refutation not found, incomplete strategy
% 10.96/2.40 % (3620389)------------------------------
% 10.96/2.40 % (3620389)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.96/2.40 % (3620389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.40 % (3620389)CaDiCaL version: 2.1.3
% 10.96/2.40 % (3620389)Termination reason: Refutation not found, incomplete strategy
% 10.96/2.40 % (3620389)Time elapsed: 0.029 s
% 10.96/2.40 % (3620389)Peak memory usage: 13 MB
% 10.96/2.40 % (3620389)Instructions burned: 52 (million)
% 10.96/2.40 % (3620389)------------------------------
% 10.96/2.40 % (3620389)------------------------------
% 10.96/2.40 % (3620394)dis+10_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=one_side_interpreted:nwc=5:random_seed=1545317392:st=2.5:i=387:sd=2:rtra=on:ss=axioms_2981 on theBenchmark for (2981ds/387Mi)
% 10.96/2.40 % (3620392)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=1896314177:i=75:ep=R:rtra=on:ntd=on_2982 on theBenchmark for (2982ds/75Mi)
% 10.96/2.40 % (3620394)Refutation not found, incomplete strategy
% 10.96/2.40 % (3620394)------------------------------
% 10.96/2.40 % (3620394)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.96/2.40 % (3620394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.40 % (3620394)CaDiCaL version: 2.1.3
% 10.96/2.40 % (3620394)Termination reason: Refutation not found, incomplete strategy
% 10.96/2.40 % (3620394)Time elapsed: 0.033 s
% 10.96/2.40 % (3620394)Peak memory usage: 12 MB
% 10.96/2.40 % (3620394)Instructions burned: 58 (million)
% 10.96/2.40 % (3620394)------------------------------
% 10.96/2.40 % (3620394)------------------------------
% 10.96/2.40 % (3620391)Instruction limit reached!
% 10.96/2.40 % (3620391)------------------------------
% 10.96/2.40 % (3620391)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.96/2.40 % (3620391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.40 % (3620391)CaDiCaL version: 2.1.3
% 10.96/2.40 % (3620391)Termination reason: Instruction limit
% 10.96/2.40 % (3620391)Termination phase: Saturation
% 10.96/2.40 % (3620391)Time elapsed: 0.069 s
% 10.96/2.40 % (3620391)Peak memory usage: 12 MB
% 10.96/2.40 % (3620391)Instructions burned: 153 (million)
% 10.96/2.40 % (3620397)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=170147598:uwa_fpi=on:i=148:doe=on:bd=preordered:rtra=on:fsd=on_2981 on theBenchmark for (2981ds/148Mi)
% 10.96/2.40 % (3620398)dis+1010_3_si=on:uwa=one_side_interpreted:random_seed=1622563728:i=161:piset=and:rtra=on:ntd=on_2981 on theBenchmark for (2981ds/161Mi)
% 10.96/2.40 % (3620392)Instruction limit reached!
% 10.96/2.40 % (3620392)------------------------------
% 10.96/2.40 % (3620392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.96/2.40 % (3620392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.40 % (3620392)CaDiCaL version: 2.1.3
% 10.96/2.40 % (3620392)Termination reason: Instruction limit
% 10.96/2.40 % (3620392)Termination phase: Saturation
% 10.96/2.40 % (3620392)Time elapsed: 0.075 s
% 10.96/2.40 % (3620392)Peak memory usage: 13 MB
% 10.96/2.40 % (3620392)Instructions burned: 75 (million)
% 10.96/2.40 % (3620401)lrs+10_1_sil=128000:si=on:random_seed=1798393370:st=5:i=888:sd=3:bd=preordered:rtra=on:ss=axioms_2980 on theBenchmark for (2980ds/888Mi)
% 10.96/2.40 % (3620397)Instruction limit reached!
% 10.96/2.40 % (3620397)------------------------------
% 10.96/2.40 % (3620397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.96/2.40 % (3620397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.40 % (3620397)CaDiCaL version: 2.1.3
% 10.96/2.40 % (3620397)Termination reason: Instruction limit
% 10.96/2.40 % (3620397)Termination phase: Saturation
% 10.96/2.40 % (3620397)Time elapsed: 0.073 s
% 10.96/2.40 % (3620397)Peak memory usage: 13 MB
% 10.96/2.40 % (3620397)Instructions burned: 148 (million)
% 10.96/2.40 % (3620403)ott-1003_1_sil=128000:plsq=on:plsqc=1:si=on:sp=weighted_frequency:lma=off:plsqr=1,32:urr=on:cbe=off:random_seed=3794035270:i=136:add=on:ins=4:rtra=on:sup=off_2980 on theBenchmark for (2980ds/136Mi)
% 10.96/2.40 % (3620398)Instruction limit reached!
% 10.96/2.40 % (3620398)------------------------------
% 10.96/2.40 % (3620398)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.96/2.40 % (3620398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.40 % (3620398)CaDiCaL version: 2.1.3
% 10.96/2.40 % (3620398)Termination reason: Instruction limit
% 10.96/2.40 % (3620398)Termination phase: Saturation
% 10.96/2.40 % (3620398)Time elapsed: 0.094 s
% 10.96/2.40 % (3620398)Peak memory usage: 13 MB
% 10.96/2.40 % (3620398)Instructions burned: 162 (million)
% 10.96/2.40 % (3620405)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=1912523974:i=88:s2at=3:nm=2:rtra=on:rawr=on_2980 on theBenchmark for (2980ds/88Mi)
% 10.96/2.40 % (3620403)Instruction limit reached!
% 10.96/2.40 % (3620403)------------------------------
% 10.96/2.40 % (3620403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.96/2.40 % (3620403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.40 % (3620403)CaDiCaL version: 2.1.3
% 10.96/2.40 % (3620403)Termination reason: Instruction limit
% 10.96/2.40 % (3620403)Termination phase: Saturation
% 10.96/2.40 % (3620403)Time elapsed: 0.062 s
% 10.96/2.40 % (3620403)Peak memory usage: 12 MB
% 10.96/2.40 % (3620403)Instructions burned: 136 (million)
% 10.96/2.40 % (3620405)Instruction limit reached!
% 10.96/2.40 % (3620405)------------------------------
% 10.96/2.40 % (3620405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.96/2.40 % (3620405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.40 % (3620405)CaDiCaL version: 2.1.3
% 10.96/2.40 % (3620405)Termination reason: Instruction limit
% 10.96/2.40 % (3620405)Termination phase: Saturation
% 10.96/2.40 % (3620405)Time elapsed: 0.042 s
% 10.96/2.40 % (3620405)Peak memory usage: 13 MB
% 10.96/2.40 % (3620405)Instructions burned: 88 (million)
% 10.96/2.40 % (3620407)dis+1002_5:4_to=kbo:sil=128000:cnfonf=conj_eager:si=on:sp=reverse_arity:lma=off:hi=on:nwc=20:random_seed=2376810522:s2a=on:cond=on:i=93:add=on:bd=preordered:rtra=on:er=filter_2979 on theBenchmark for (2979ds/93Mi)
% 10.96/2.40 % (3620362) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3620182-3620362"...
% 10.96/2.40 % (3620408)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=680833077:i=2186:rtra=on:ixr=off_2979 on theBenchmark for (2979ds/2186Mi)
% 10.96/2.40 % (3620362)...printing done.
% 10.96/2.40 % (3620362)Refutation found. Thanks to Tanya!
% 10.96/2.40 % SZS status Theorem for theBenchmark
% 10.96/2.40 % SZS output start Proof for theBenchmark
% 10.96/2.40 thf(type_def_5, type, del: $tType).
% 10.96/2.40 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 10.96/2.40 thf(type_def_7, type, tp__ty_2Einteger_2Eint: $tType).
% 10.96/2.40 thf(type_def_8, type, tp__ty_2Enum_2Enum: $tType).
% 10.96/2.40 thf(func_def_0, type, bool: del).
% 10.96/2.40 thf(func_def_1, type, ind: del).
% 10.96/2.40 thf(func_def_2, type, arr: (del > del > del)).
% 10.96/2.40 thf(func_def_3, type, mem: ($i > del > $o)).
% 10.96/2.40 thf(func_def_4, type, ap: ($i > $i > $i)).
% 10.96/2.40 thf(func_def_5, type, lam: (del > ($i > $i) > $i)).
% 10.96/2.40 thf(func_def_6, type, p: ($i > $o)).
% 10.96/2.40 thf(func_def_7, type, inj__o: ($o > $i)).
% 10.96/2.40 thf(func_def_14, type, ty_2Einteger_2Eint: del).
% 10.96/2.40 thf(func_def_15, type, inj__ty_2Einteger_2Eint: (tp__ty_2Einteger_2Eint > $i)).
% 10.96/2.40 thf(func_def_16, type, surj__ty_2Einteger_2Eint: ($i > tp__ty_2Einteger_2Eint)).
% 10.96/2.40 thf(func_def_18, type, fo__c_2Einteger_2Eint__neg: (tp__ty_2Einteger_2Eint > tp__ty_2Einteger_2Eint)).
% 10.96/2.40 thf(func_def_19, type, ty_2Enum_2Enum: del).
% 10.96/2.40 thf(func_def_20, type, inj__ty_2Enum_2Enum: (tp__ty_2Enum_2Enum > $i)).
% 10.96/2.40 thf(func_def_21, type, surj__ty_2Enum_2Enum: ($i > tp__ty_2Enum_2Enum)).
% 10.96/2.40 thf(func_def_23, type, fo__c_2Einteger_2ENum: (tp__ty_2Einteger_2Eint > tp__ty_2Enum_2Enum)).
% 10.96/2.40 thf(func_def_25, type, fo__c_2Einteger_2Eint__of__num: (tp__ty_2Enum_2Enum > tp__ty_2Einteger_2Eint)).
% 10.96/2.40 thf(func_def_27, type, c_2Ebool_2ECOND: (del > $i)).
% 10.96/2.40 thf(func_def_28, type, ty_2Efcp_2Ecart: (del > del > del)).
% 10.96/2.40 thf(func_def_29, type, c_2Einteger__word_2Ei2w: (del > $i)).
% 10.96/2.40 thf(func_def_32, type, ty_2Ebool_2Eitself: (del > del)).
% 10.96/2.40 thf(func_def_33, type, c_2Ebool_2Ethe__value: (del > $i)).
% 10.96/2.40 thf(func_def_34, type, c_2Ewords_2Edimword: (del > $i)).
% 10.96/2.40 thf(func_def_36, type, fo__c_2Earithmetic_2EMOD: (tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum)).
% 10.96/2.40 thf(func_def_37, type, c_2Ebool_2E_21: (del > $i)).
% 10.96/2.40 thf(func_def_39, type, fo__c_2Enum_2E0: tp__ty_2Enum_2Enum).
% 10.96/2.40 thf(func_def_40, type, c_2Ewords_2En2w: (del > $i)).
% 10.96/2.40 thf(func_def_41, type, c_2Ewords_2Eword__2comp: (del > $i)).
% 10.96/2.40 thf(func_def_42, type, c_2Emin_2E_3D: (del > $i)).
% 10.96/2.40 thf(func_def_45, type, sP0: ($i > del > $o)).
% 10.96/2.40 thf(func_def_46, type, sP1: ($i > del > $o)).
% 10.96/2.40 thf(func_def_47, type, sP2: ($i > $i > $o)).
% 10.96/2.40 thf(func_def_48, type, sP3: ($i > $i > $o)).
% 10.96/2.40 thf(func_def_49, type, sP4: ($i > $i > $o)).
% 10.96/2.40 thf(func_def_50, type, sP5: ($i > $i > $o)).
% 10.96/2.40 thf(func_def_51, type, sP6: ($i > $i > $o)).
% 10.96/2.40 thf(func_def_52, type, sP7: ($i > $i > $o)).
% 10.96/2.40 thf(func_def_53, type, sP8: ($i > $i > $o)).
% 10.96/2.40 thf(func_def_54, type, sP9: ($i > $i > $i > $o)).
% 10.96/2.40 thf(func_def_55, type, sP10: ($i > $i > $i > $o)).
% 10.96/2.40 thf(func_def_56, type, sP11: ($i > $i > $i > $o)).
% 10.96/2.40 thf(func_def_57, type, sK12: ($i > del > $i > $i)).
% 10.96/2.40 thf(func_def_58, type, sK13: ($i > del > $i)).
% 10.96/2.40 thf(func_def_59, type, sK14: (del > del > ($i > $i) > $i)).
% 10.96/2.40 thf(func_def_60, type, sK15: del).
% 10.96/2.40 thf(f3,axiom,(
% 10.96/2.40 ! [X0 : $i] : ((mem @ X0 @ bool) => (X0 = ((inj__o @ (p @ X0)))))),
% 10.96/2.40 file('/export/starexec/sandbox2/benchmark/Axioms/ITP001/ITP001^2.ax',stp_iso_mem_o)).
% 10.96/2.40 thf(f4,axiom,(
% 10.96/2.40 ! [X2 : $i,X0 : del,X1 : del] : ((mem @ X2 @ (arr @ X0 @ X1)) => ! [X3 : $i] : ((mem @ X3 @ X0) => (mem @ (ap @ X2 @ X3) @ X1)))),
% 10.96/2.40 file('/export/starexec/sandbox2/benchmark/Axioms/ITP001/ITP001^2.ax',ap_tp)).
% 10.96/2.40 thf(f12,axiom,(
% 10.96/2.40 (mem @ c_2Ebool_2EF @ bool)),
% 10.96/2.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Ebool_2EF)).
% 10.96/2.40 thf(f13,axiom,(
% 10.96/2.40 ~(p @ c_2Ebool_2EF)),
% 10.96/2.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_false_p)).
% 10.96/2.40 thf(f18,axiom,(
% 10.96/2.40 ! [X0 : tp__ty_2Einteger_2Eint] : (((surj__ty_2Einteger_2Eint @ (inj__ty_2Einteger_2Eint @ X0))) = X0)),
% 10.96/2.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',stp_inj_surj_ty_2Einteger_2Eint)).
% 10.96/2.40 thf(f19,axiom,(
% 10.96/2.40 ! [X0 : tp__ty_2Einteger_2Eint] : (mem @ (inj__ty_2Einteger_2Eint @ X0) @ ty_2Einteger_2Eint)),
% 10.96/2.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',stp_inj_mem_ty_2Einteger_2Eint)).
% 10.96/2.40 thf(f22,axiom,(
% 10.96/2.40 ! [X0 : tp__ty_2Einteger_2Eint] : (((inj__ty_2Einteger_2Eint @ (fo__c_2Einteger_2Eint__neg @ X0))) = ((ap @ c_2Einteger_2Eint__neg @ (inj__ty_2Einteger_2Eint @ X0))))),
% 10.96/2.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',stp_eq_fo_c_2Einteger_2Eint__neg)).
% 10.96/2.40 thf(f23,axiom,(
% 10.96/2.40 ! [X0 : tp__ty_2Enum_2Enum] : (((surj__ty_2Enum_2Enum @ (inj__ty_2Enum_2Enum @ X0))) = X0)),
% 10.96/2.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',stp_inj_surj_ty_2Enum_2Enum)).
% 10.96/2.40 thf(f27,axiom,(
% 10.96/2.40 ! [X0 : tp__ty_2Einteger_2Eint] : (((inj__ty_2Enum_2Enum @ (fo__c_2Einteger_2ENum @ X0))) = ((ap @ c_2Einteger_2ENum @ (inj__ty_2Einteger_2Eint @ X0))))),
% 10.96/2.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',stp_eq_fo_c_2Einteger_2ENum)).
% 10.96/2.40 thf(f29,axiom,(
% 10.96/2.40 ! [X0 : tp__ty_2Enum_2Enum] : (((inj__ty_2Einteger_2Eint @ (fo__c_2Einteger_2Eint__of__num @ X0))) = ((ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X0))))),
% 10.96/2.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',stp_eq_fo_c_2Einteger_2Eint__of__num)).
% 10.96/2.40 thf(f30,axiom,(
% 10.96/2.40 (mem @ c_2Einteger_2Eint__lt @ (arr @ ty_2Einteger_2Eint @ (arr @ ty_2Einteger_2Eint @ bool)))),
% 10.96/2.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Einteger_2Eint__lt)).
% 10.96/2.40 thf(f42,axiom,(
% 10.96/2.40 (mem @ c_2Enum_2E0 @ ty_2Enum_2Enum)),
% 10.96/2.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Enum_2E0)).
% 10.96/2.40 thf(f43,axiom,(
% 10.96/2.40 (((inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)) = c_2Enum_2E0)),
% 10.96/2.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',stp_eq_fo_c_2Enum_2E0)).
% 10.96/2.40 thf(f44,axiom,(
% 10.96/2.40 ! [X0 : del] : (mem @ (c_2Ewords_2En2w @ X0) @ (arr @ ty_2Enum_2Enum @ (ty_2Efcp_2Ecart @ bool @ X0)))),
% 10.96/2.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Ewords_2En2w)).
% 10.96/2.40 thf(f55,axiom,(
% 10.96/2.40 ! [X0 : del] : (! [X1 : $i] : ((mem @ X1 @ X0) => ! [X2 : $i] : ((mem @ X2 @ X0) => (((ap @ (ap @ (ap @ (c_2Ebool_2ECOND @ X0) @ c_2Ebool_2ET) @ X1) @ X2)) = X1))) & ! [X3 : $i] : ((mem @ X3 @ X0) => ! [X4 : $i] : ((mem @ X4 @ X0) => (((ap @ (ap @ (ap @ (c_2Ebool_2ECOND @ X0) @ c_2Ebool_2EF) @ X3) @ X4)) = X4))))),
% 10.96/2.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Ebool_2Ebool__case__thm)).
% 10.96/2.40 thf(f56,axiom,(
% 10.96/2.40 (((surj__ty_2Einteger_2Eint @ (ap @ c_2Einteger_2Eint__neg @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) = ((surj__ty_2Einteger_2Eint @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))),
% 10.96/2.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Einteger_2EINT__NEG__0)).
% 10.96/2.40 thf(f57,axiom,(
% 10.96/2.40 ! [X1 : tp__ty_2Enum_2Enum,X0 : tp__ty_2Enum_2Enum] : (((p @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X0))) @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X1)))) <=> (p @ (ap @ (ap @ c_2Eprim__rec_2E_3C @ (inj__ty_2Enum_2Enum @ X0)) @ (inj__ty_2Enum_2Enum @ X1)))) & ((p @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X0))) @ (ap @ c_2Einteger_2Eint__neg @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X1))))) <=> $false) & (((X0 != fo__c_2Enum_2E0) | (X1 != fo__c_2Enum_2E0)) <=> (p @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (ap @ c_2Einteger_2Eint__neg @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X0)))) @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X1))))) & ((p @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (ap @ c_2Einteger_2Eint__neg @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X0)))) @ (ap @ c_2Einteger_2Eint__neg @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X1))))) <=> (p @ (ap @ (ap @ c_2Eprim__rec_2E_3C @ (inj__ty_2Enum_2Enum @ X1)) @ (inj__ty_2Enum_2Enum @ X0)))))),
% 10.96/2.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Einteger_2EINT__LT__CALCULATE)).
% 10.96/2.40 thf(f58,axiom,(
% 10.96/2.40 ! [X0 : tp__ty_2Enum_2Enum] : (((surj__ty_2Enum_2Enum @ (ap @ c_2Einteger_2ENum @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X0))))) = X0)),
% 10.96/2.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Einteger_2ENUM__OF__INT)).
% 10.96/2.40 thf(f59,axiom,(
% 10.96/2.40 ! [X1 : tp__ty_2Einteger_2Eint,X0 : del] : (((ap @ (c_2Einteger__word_2Ei2w @ X0) @ (inj__ty_2Einteger_2Eint @ X1))) = ((ap @ (ap @ (ap @ (c_2Ebool_2ECOND @ (ty_2Efcp_2Ecart @ bool @ X0)) @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (inj__ty_2Einteger_2Eint @ X1)) @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) @ (ap @ (c_2Ewords_2Eword__2comp @ X0) @ (ap @ (c_2Ewords_2En2w @ X0) @ (ap @ c_2Einteger_2ENum @ (ap @ c_2Einteger_2Eint__neg @ (inj__ty_2Einteger_2Eint @ X1)))))) @ (ap @ (c_2Ewords_2En2w @ X0) @ (ap @ c_2Einteger_2ENum @ (inj__ty_2Einteger_2Eint @ X1))))))),
% 10.96/2.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_thm_2Einteger__word_2Ei2w__def)).
% 10.96/2.40 thf(f62,axiom,(
% 10.96/2.40 ! [X0 : del] : (((ap @ (c_2Ewords_2Eword__2comp @ X0) @ (ap @ (c_2Ewords_2En2w @ X0) @ (inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) = ((ap @ (c_2Ewords_2En2w @ X0) @ (inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))),
% 10.96/2.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Ewords_2EWORD__NEG__0)).
% 10.96/2.40 thf(f63,conjecture,(
% 10.96/2.40 ! [X0 : del] : (((ap @ (c_2Einteger__word_2Ei2w @ X0) @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) = ((ap @ (c_2Ewords_2En2w @ X0) @ (inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))),
% 10.96/2.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Einteger__word_2Ei2w__0)).
% 10.96/2.40 thf(f64,negated_conjecture,(
% 10.96/2.40 ~ ! [X0 : del] : (((ap @ (c_2Einteger__word_2Ei2w @ X0) @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) = ((ap @ (c_2Ewords_2En2w @ X0) @ (inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))),
% 10.96/2.40 inference(negated_conjecture,[status(cth)],[f63])).
% 10.96/2.40 thf(f79,plain,(
% 10.96/2.40 ! [X0 : del] : (mem @ (c_2Ewords_2En2w @ X0) @ (arr @ ty_2Enum_2Enum @ (ty_2Efcp_2Ecart @ bool @ X0)))),
% 10.96/2.40 inference(rectify,[],[f44])).
% 10.96/2.40 thf(f80,plain,(
% 10.96/2.40 ! [X0 : del] : (((mem @ (c_2Ewords_2En2w @ X0) @ (arr @ ty_2Enum_2Enum @ (ty_2Efcp_2Ecart @ bool @ X0)))) = $true)),
% 10.96/2.40 inference(fool_elimination,[],[f79])).
% 10.96/2.40 thf(f83,plain,(
% 10.96/2.40 ! [X0 : $i] : ((mem @ X0 @ bool) => (X0 = ((inj__o @ (p @ X0)))))),
% 10.96/2.40 inference(rectify,[],[f3])).
% 10.96/2.40 thf(f84,plain,(
% 10.96/2.40 ! [X0 : $i] : ((((mem @ X0 @ bool)) = $true) => (((inj__o @ (p @ X0))) = X0))),
% 10.96/2.40 inference(fool_elimination,[],[f83])).
% 10.96/2.40 thf(f85,plain,(
% 10.96/2.40 ! [X0 : del] : (! [X1 : $i] : ((mem @ X1 @ X0) => ! [X2 : $i] : ((mem @ X2 @ X0) => (((ap @ (ap @ (ap @ (c_2Ebool_2ECOND @ X0) @ c_2Ebool_2ET) @ X1) @ X2)) = X1))) & ! [X3 : $i] : ((mem @ X3 @ X0) => ! [X4 : $i] : ((mem @ X4 @ X0) => (((ap @ (ap @ (ap @ (c_2Ebool_2ECOND @ X0) @ c_2Ebool_2EF) @ X3) @ X4)) = X4))))),
% 10.96/2.40 inference(rectify,[],[f55])).
% 10.96/2.40 thf(f86,plain,(
% 10.96/2.40 ! [X0 : del] : (! [X3 : $i] : ((((mem @ X3 @ X0)) = $true) => ! [X4 : $i] : ((((mem @ X4 @ X0)) = $true) => (((ap @ (ap @ (ap @ (c_2Ebool_2ECOND @ X0) @ c_2Ebool_2EF) @ X3) @ X4)) = X4))) & ! [X1 : $i] : ((((mem @ X1 @ X0)) = $true) => ! [X2 : $i] : ((((mem @ X2 @ X0)) = $true) => (((ap @ (ap @ (ap @ (c_2Ebool_2ECOND @ X0) @ c_2Ebool_2ET) @ X1) @ X2)) = X1))))),
% 10.96/2.40 inference(fool_elimination,[],[f85])).
% 10.96/2.40 thf(f103,plain,(
% 10.96/2.40 ! [X0 : tp__ty_2Einteger_2Eint] : (mem @ (inj__ty_2Einteger_2Eint @ X0) @ ty_2Einteger_2Eint)),
% 10.96/2.40 inference(rectify,[],[f19])).
% 10.96/2.40 thf(f104,plain,(
% 10.96/2.40 ! [X0 : tp__ty_2Einteger_2Eint] : (((mem @ (inj__ty_2Einteger_2Eint @ X0) @ ty_2Einteger_2Eint)) = $true)),
% 10.96/2.40 inference(fool_elimination,[],[f103])).
% 10.96/2.40 thf(f115,plain,(
% 10.96/2.40 ! [X0 : $i,X1 : del,X2 : del] : ((mem @ X0 @ (arr @ X1 @ X2)) => ! [X3 : $i] : ((mem @ X3 @ X1) => (mem @ (ap @ X0 @ X3) @ X2)))),
% 10.96/2.40 inference(rectify,[],[f4])).
% 10.96/2.40 thf(f116,plain,(
% 10.96/2.40 ! [X1 : del,X2 : del,X0 : $i] : ((((mem @ X0 @ (arr @ X1 @ X2))) = $true) => ! [X3 : $i] : (($true = ((mem @ X3 @ X1))) => ($true = ((mem @ (ap @ X0 @ X3) @ X2)))))),
% 10.96/2.40 inference(fool_elimination,[],[f115])).
% 10.96/2.40 thf(f119,plain,(
% 10.96/2.40 (mem @ c_2Ebool_2EF @ bool)),
% 10.96/2.40 inference(rectify,[],[f12])).
% 10.96/2.40 thf(f120,plain,(
% 10.96/2.40 (((mem @ c_2Ebool_2EF @ bool)) = $true)),
% 10.96/2.40 inference(fool_elimination,[],[f119])).
% 10.96/2.40 thf(f129,plain,(
% 10.96/2.40 ~(p @ c_2Ebool_2EF)),
% 10.96/2.40 inference(rectify,[],[f13])).
% 10.96/2.40 thf(f130,plain,(
% 10.96/2.40 ~ (((p @ c_2Ebool_2EF)) = $true)),
% 10.96/2.40 inference(fool_elimination,[],[f129])).
% 10.96/2.40 thf(f133,plain,(
% 10.96/2.40 (mem @ c_2Einteger_2Eint__lt @ (arr @ ty_2Einteger_2Eint @ (arr @ ty_2Einteger_2Eint @ bool)))),
% 10.96/2.40 inference(rectify,[],[f30])).
% 10.96/2.40 thf(f134,plain,(
% 10.96/2.40 (((mem @ c_2Einteger_2Eint__lt @ (arr @ ty_2Einteger_2Eint @ (arr @ ty_2Einteger_2Eint @ bool)))) = $true)),
% 10.96/2.40 inference(fool_elimination,[],[f133])).
% 10.96/2.40 thf(f145,plain,(
% 10.96/2.40 (mem @ c_2Enum_2E0 @ ty_2Enum_2Enum)),
% 10.96/2.40 inference(rectify,[],[f42])).
% 10.96/2.40 thf(f146,plain,(
% 10.96/2.40 (((mem @ c_2Enum_2E0 @ ty_2Enum_2Enum)) = $true)),
% 10.96/2.40 inference(fool_elimination,[],[f145])).
% 10.96/2.40 thf(f157,plain,(
% 10.96/2.40 ! [X0 : tp__ty_2Enum_2Enum,X1 : tp__ty_2Enum_2Enum] : (((p @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X1))) @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X0)))) <=> (p @ (ap @ (ap @ c_2Eprim__rec_2E_3C @ (inj__ty_2Enum_2Enum @ X1)) @ (inj__ty_2Enum_2Enum @ X0)))) & ((p @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X1))) @ (ap @ c_2Einteger_2Eint__neg @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X0))))) <=> $false) & (((fo__c_2Enum_2E0 != X1) | (fo__c_2Enum_2E0 != X0)) <=> (p @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (ap @ c_2Einteger_2Eint__neg @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X1)))) @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X0))))) & ((p @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (ap @ c_2Einteger_2Eint__neg @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X1)))) @ (ap @ c_2Einteger_2Eint__neg @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X0))))) <=> (p @ (ap @ (ap @ c_2Eprim__rec_2E_3C @ (inj__ty_2Enum_2Enum @ X0)) @ (inj__ty_2Enum_2Enum @ X1)))))),
% 10.96/2.40 inference(rectify,[],[f57])).
% 10.96/2.40 thf(f158,plain,(
% 10.96/2.40 ! [X0 : tp__ty_2Enum_2Enum,X1 : tp__ty_2Enum_2Enum] : ((((p @ (ap @ (ap @ c_2Eprim__rec_2E_3C @ (inj__ty_2Enum_2Enum @ X1)) @ (inj__ty_2Enum_2Enum @ X0)))) = ((p @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X1))) @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X0)))))) & ((((p @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X1))) @ (ap @ c_2Einteger_2Eint__neg @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X0)))))) = $true) <=> $false) & (((fo__c_2Enum_2E0 != X0) | (fo__c_2Enum_2E0 != X1)) <=> (((p @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (ap @ c_2Einteger_2Eint__neg @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X1)))) @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X0))))) = $true)) & (((p @ (ap @ (ap @ c_2Eprim__rec_2E_3C @ (inj__ty_2Enum_2Enum @ X0)) @ (inj__ty_2Enum_2Enum @ X1)))) = ((p @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (ap @ c_2Einteger_2Eint__neg @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X1)))) @ (ap @ c_2Einteger_2Eint__neg @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X0))))))))),
% 10.96/2.40 inference(fool_elimination,[],[f157])).
% 10.96/2.40 thf(f163,plain,(
% 10.96/2.40 ! [X0 : tp__ty_2Einteger_2Eint,X1 : del] : (((ap @ (ap @ (ap @ (c_2Ebool_2ECOND @ (ty_2Efcp_2Ecart @ bool @ X1)) @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (inj__ty_2Einteger_2Eint @ X0)) @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) @ (ap @ (c_2Ewords_2Eword__2comp @ X1) @ (ap @ (c_2Ewords_2En2w @ X1) @ (ap @ c_2Einteger_2ENum @ (ap @ c_2Einteger_2Eint__neg @ (inj__ty_2Einteger_2Eint @ X0)))))) @ (ap @ (c_2Ewords_2En2w @ X1) @ (ap @ c_2Einteger_2ENum @ (inj__ty_2Einteger_2Eint @ X0))))) = ((ap @ (c_2Einteger__word_2Ei2w @ X1) @ (inj__ty_2Einteger_2Eint @ X0))))),
% 10.96/2.40 inference(rectify,[],[f59])).
% 10.96/2.40 thf(f166,plain,(
% 10.96/2.40 (((p @ c_2Ebool_2EF)) != $true)),
% 10.96/2.40 inference(flattening,[],[f130])).
% 10.96/2.40 thf(f169,plain,(
% 10.96/2.40 ! [X0 : tp__ty_2Enum_2Enum,X1 : tp__ty_2Enum_2Enum] : ((((p @ (ap @ (ap @ c_2Eprim__rec_2E_3C @ (inj__ty_2Enum_2Enum @ X1)) @ (inj__ty_2Enum_2Enum @ X0)))) = ((p @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X1))) @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X0)))))) & ~ (((p @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X1))) @ (ap @ c_2Einteger_2Eint__neg @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X0)))))) = $true) & (((fo__c_2Enum_2E0 != X0) | (fo__c_2Enum_2E0 != X1)) <=> (((p @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (ap @ c_2Einteger_2Eint__neg @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X1)))) @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X0))))) = $true)) & (((p @ (ap @ (ap @ c_2Eprim__rec_2E_3C @ (inj__ty_2Enum_2Enum @ X0)) @ (inj__ty_2Enum_2Enum @ X1)))) = ((p @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (ap @ c_2Einteger_2Eint__neg @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X1)))) @ (ap @ c_2Einteger_2Eint__neg @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X0))))))))),
% 10.96/2.40 inference(true_and_false_elimination,[],[f158])).
% 10.96/2.40 thf(f170,plain,(
% 10.96/2.40 ! [X0 : tp__ty_2Enum_2Enum,X1 : tp__ty_2Enum_2Enum] : ((((p @ (ap @ (ap @ c_2Eprim__rec_2E_3C @ (inj__ty_2Enum_2Enum @ X0)) @ (inj__ty_2Enum_2Enum @ X1)))) = ((p @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (ap @ c_2Einteger_2Eint__neg @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X1)))) @ (ap @ c_2Einteger_2Eint__neg @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X0))))))) & (((p @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X1))) @ (ap @ c_2Einteger_2Eint__neg @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X0)))))) != $true) & (((fo__c_2Enum_2E0 != X0) | (fo__c_2Enum_2E0 != X1)) <=> (((p @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (ap @ c_2Einteger_2Eint__neg @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X1)))) @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X0))))) = $true)) & (((p @ (ap @ (ap @ c_2Eprim__rec_2E_3C @ (inj__ty_2Enum_2Enum @ X1)) @ (inj__ty_2Enum_2Enum @ X0)))) = ((p @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X1))) @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X0)))))))),
% 10.96/2.40 inference(flattening,[],[f169])).
% 10.96/2.40 thf(f178,plain,(
% 10.96/2.40 ! [X2 : del,X0 : $i,X1 : del] : (! [X3 : $i] : (($true != ((mem @ X3 @ X1))) | ($true = ((mem @ (ap @ X0 @ X3) @ X2)))) | (((mem @ X0 @ (arr @ X1 @ X2))) != $true))),
% 10.96/2.40 inference(ennf_transformation,[],[f116])).
% 10.96/2.40 thf(f186,plain,(
% 10.96/2.40 ! [X0 : del] : (! [X3 : $i] : ((((mem @ X3 @ X0)) != $true) | ! [X4 : $i] : ((((ap @ (ap @ (ap @ (c_2Ebool_2ECOND @ X0) @ c_2Ebool_2EF) @ X3) @ X4)) = X4) | (((mem @ X4 @ X0)) != $true))) & ! [X1 : $i] : ((((mem @ X1 @ X0)) != $true) | ! [X2 : $i] : ((((ap @ (ap @ (ap @ (c_2Ebool_2ECOND @ X0) @ c_2Ebool_2ET) @ X1) @ X2)) = X1) | (((mem @ X2 @ X0)) != $true))))),
% 10.96/2.40 inference(ennf_transformation,[],[f86])).
% 10.96/2.40 thf(f193,plain,(
% 10.96/2.40 ? [X0 : del] : (((ap @ (c_2Ewords_2En2w @ X0) @ (inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) != ((ap @ (c_2Einteger__word_2Ei2w @ X0) @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))),
% 10.96/2.40 inference(ennf_transformation,[],[f64])).
% 10.96/2.40 thf(f194,plain,(
% 10.96/2.40 ! [X0 : $i] : ((((mem @ X0 @ bool)) != $true) | (((inj__o @ (p @ X0))) = X0))),
% 10.96/2.40 inference(ennf_transformation,[],[f84])).
% 10.96/2.40 thf(f223,plain,(
% 10.96/2.40 ! [X0 : tp__ty_2Enum_2Enum,X1 : tp__ty_2Enum_2Enum] : ((((p @ (ap @ (ap @ c_2Eprim__rec_2E_3C @ (inj__ty_2Enum_2Enum @ X0)) @ (inj__ty_2Enum_2Enum @ X1)))) = ((p @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (ap @ c_2Einteger_2Eint__neg @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X1)))) @ (ap @ c_2Einteger_2Eint__neg @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X0))))))) & (((p @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X1))) @ (ap @ c_2Einteger_2Eint__neg @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X0)))))) != $true) & ((((fo__c_2Enum_2E0 != X0) | (fo__c_2Enum_2E0 != X1)) | (((p @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (ap @ c_2Einteger_2Eint__neg @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X1)))) @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X0))))) != $true)) & ((((p @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (ap @ c_2Einteger_2Eint__neg @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X1)))) @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X0))))) = $true) | ((fo__c_2Enum_2E0 = X0) & (fo__c_2Enum_2E0 = X1)))) & (((p @ (ap @ (ap @ c_2Eprim__rec_2E_3C @ (inj__ty_2Enum_2Enum @ X1)) @ (inj__ty_2Enum_2Enum @ X0)))) = ((p @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X1))) @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X0)))))))),
% 10.96/2.40 inference(nnf_transformation,[],[f170])).
% 10.96/2.40 thf(f224,plain,(
% 10.96/2.40 ! [X0 : tp__ty_2Enum_2Enum,X1 : tp__ty_2Enum_2Enum] : ((((p @ (ap @ (ap @ c_2Eprim__rec_2E_3C @ (inj__ty_2Enum_2Enum @ X0)) @ (inj__ty_2Enum_2Enum @ X1)))) = ((p @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (ap @ c_2Einteger_2Eint__neg @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X1)))) @ (ap @ c_2Einteger_2Eint__neg @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X0))))))) & (((p @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X1))) @ (ap @ c_2Einteger_2Eint__neg @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X0)))))) != $true) & ((fo__c_2Enum_2E0 != X0) | (fo__c_2Enum_2E0 != X1) | (((p @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (ap @ c_2Einteger_2Eint__neg @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X1)))) @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X0))))) != $true)) & ((((p @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (ap @ c_2Einteger_2Eint__neg @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X1)))) @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X0))))) = $true) | ((fo__c_2Enum_2E0 = X0) & (fo__c_2Enum_2E0 = X1))) & (((p @ (ap @ (ap @ c_2Eprim__rec_2E_3C @ (inj__ty_2Enum_2Enum @ X1)) @ (inj__ty_2Enum_2Enum @ X0)))) = ((p @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X1))) @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X0)))))))),
% 10.96/2.40 inference(flattening,[],[f223])).
% 10.96/2.40 thf(f225,plain,(
% 10.96/2.40 (((ap @ (c_2Einteger__word_2Ei2w @ sK15) @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) != ((ap @ (c_2Ewords_2En2w @ sK15) @ (inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))),
% 10.96/2.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK15]),skolemize(X0,sK15)],[f193])).
% 10.96/2.40 thf(f240,plain,(
% 10.96/2.40 ! [X0 : del] : (! [X1 : $i] : ((((mem @ X1 @ X0)) != $true) | ! [X2 : $i] : ((((ap @ (ap @ (ap @ (c_2Ebool_2ECOND @ X0) @ c_2Ebool_2EF) @ X1) @ X2)) = X2) | (((mem @ X2 @ X0)) != $true))) & ! [X3 : $i] : ((((mem @ X3 @ X0)) != $true) | ! [X4 : $i] : ((((ap @ (ap @ (ap @ (c_2Ebool_2ECOND @ X0) @ c_2Ebool_2ET) @ X3) @ X4)) = X3) | (((mem @ X4 @ X0)) != $true))))),
% 10.96/2.40 inference(rectify,[],[f186])).
% 10.96/2.40 thf(f248,plain,(
% 10.96/2.40 ! [X0 : del,X1 : $i,X2 : del] : (! [X3 : $i] : ((((mem @ X3 @ X2)) != $true) | ($true = ((mem @ (ap @ X1 @ X3) @ X0)))) | (((mem @ X1 @ (arr @ X2 @ X0))) != $true))),
% 10.96/2.40 inference(rectify,[],[f178])).
% 10.96/2.40 thf(f255,plain,(
% 10.96/2.40 ( ! [X0 : tp__ty_2Einteger_2Eint,X1 : del] : ((((ap @ (ap @ (ap @ (c_2Ebool_2ECOND @ (ty_2Efcp_2Ecart @ bool @ X1)) @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (inj__ty_2Einteger_2Eint @ X0)) @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) @ (ap @ (c_2Ewords_2Eword__2comp @ X1) @ (ap @ (c_2Ewords_2En2w @ X1) @ (ap @ c_2Einteger_2ENum @ (ap @ c_2Einteger_2Eint__neg @ (inj__ty_2Einteger_2Eint @ X0)))))) @ (ap @ (c_2Ewords_2En2w @ X1) @ (ap @ c_2Einteger_2ENum @ (inj__ty_2Einteger_2Eint @ X0))))) = ((ap @ (c_2Einteger__word_2Ei2w @ X1) @ (inj__ty_2Einteger_2Eint @ X0))))) )),
% 10.96/2.40 inference(cnf_transformation,[],[f163])).
% 10.96/2.40 thf(f265,plain,(
% 10.96/2.40 ( ! [X0 : del] : ((((ap @ (c_2Ewords_2En2w @ X0) @ (inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) = ((ap @ (c_2Ewords_2Eword__2comp @ X0) @ (ap @ (c_2Ewords_2En2w @ X0) @ (inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))) )),
% 10.96/2.40 inference(cnf_transformation,[],[f62])).
% 10.96/2.40 thf(f266,plain,(
% 10.96/2.40 ( ! [X0 : tp__ty_2Einteger_2Eint] : ((((inj__ty_2Einteger_2Eint @ (fo__c_2Einteger_2Eint__neg @ X0))) = ((ap @ c_2Einteger_2Eint__neg @ (inj__ty_2Einteger_2Eint @ X0))))) )),
% 10.96/2.40 inference(cnf_transformation,[],[f22])).
% 10.96/2.40 thf(f271,plain,(
% 10.96/2.40 (((mem @ c_2Ebool_2EF @ bool)) = $true)),
% 10.96/2.40 inference(cnf_transformation,[],[f120])).
% 10.96/2.40 thf(f272,plain,(
% 10.96/2.40 ( ! [X0 : $i] : ((((mem @ X0 @ bool)) != $true) | (((inj__o @ (p @ X0))) = X0)) )),
% 10.96/2.40 inference(cnf_transformation,[],[f194])).
% 10.96/2.40 thf(f283,plain,(
% 10.96/2.40 ( ! [X0 : tp__ty_2Enum_2Enum,X1 : tp__ty_2Enum_2Enum] : ((((p @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X1))) @ (ap @ c_2Einteger_2Eint__neg @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X0)))))) != $true)) )),
% 10.96/2.40 inference(cnf_transformation,[],[f224])).
% 10.96/2.40 thf(f285,plain,(
% 10.96/2.40 ( ! [X0 : tp__ty_2Einteger_2Eint] : ((((inj__ty_2Enum_2Enum @ (fo__c_2Einteger_2ENum @ X0))) = ((ap @ c_2Einteger_2ENum @ (inj__ty_2Einteger_2Eint @ X0))))) )),
% 10.96/2.40 inference(cnf_transformation,[],[f27])).
% 10.96/2.40 thf(f286,plain,(
% 10.96/2.40 (((ap @ (c_2Einteger__word_2Ei2w @ sK15) @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) != ((ap @ (c_2Ewords_2En2w @ sK15) @ (inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))),
% 10.96/2.40 inference(cnf_transformation,[],[f225])).
% 10.96/2.40 thf(f297,plain,(
% 10.96/2.40 ( ! [X0 : tp__ty_2Einteger_2Eint] : ((((mem @ (inj__ty_2Einteger_2Eint @ X0) @ ty_2Einteger_2Eint)) = $true)) )),
% 10.96/2.40 inference(cnf_transformation,[],[f104])).
% 10.96/2.40 thf(f298,plain,(
% 10.96/2.40 ( ! [X0 : tp__ty_2Enum_2Enum] : ((((surj__ty_2Enum_2Enum @ (ap @ c_2Einteger_2ENum @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X0))))) = X0)) )),
% 10.96/2.40 inference(cnf_transformation,[],[f58])).
% 10.96/2.40 thf(f318,plain,(
% 10.96/2.40 ( ! [X0 : tp__ty_2Enum_2Enum] : ((((surj__ty_2Enum_2Enum @ (inj__ty_2Enum_2Enum @ X0))) = X0)) )),
% 10.96/2.40 inference(cnf_transformation,[],[f23])).
% 10.96/2.40 thf(f319,plain,(
% 10.96/2.40 ( ! [X0 : del] : ((((mem @ (c_2Ewords_2En2w @ X0) @ (arr @ ty_2Enum_2Enum @ (ty_2Efcp_2Ecart @ bool @ X0)))) = $true)) )),
% 10.96/2.40 inference(cnf_transformation,[],[f80])).
% 10.96/2.40 thf(f321,plain,(
% 10.96/2.40 (((mem @ c_2Enum_2E0 @ ty_2Enum_2Enum)) = $true)),
% 10.96/2.40 inference(cnf_transformation,[],[f146])).
% 10.96/2.40 thf(f329,plain,(
% 10.96/2.40 ( ! [X2 : $i,X0 : del,X1 : $i] : ((((ap @ (ap @ (ap @ (c_2Ebool_2ECOND @ X0) @ c_2Ebool_2EF) @ X1) @ X2)) = X2) | (((mem @ X1 @ X0)) != $true) | (((mem @ X2 @ X0)) != $true)) )),
% 10.96/2.40 inference(cnf_transformation,[],[f240])).
% 10.96/2.40 thf(f340,plain,(
% 10.96/2.40 ( ! [X2 : del,X3 : $i,X0 : del,X1 : $i] : (($true = ((mem @ (ap @ X1 @ X3) @ X0))) | (((mem @ X1 @ (arr @ X2 @ X0))) != $true) | (((mem @ X3 @ X2)) != $true)) )),
% 10.96/2.40 inference(cnf_transformation,[],[f248])).
% 10.96/2.40 thf(f342,plain,(
% 10.96/2.40 ( ! [X0 : tp__ty_2Einteger_2Eint] : ((((surj__ty_2Einteger_2Eint @ (inj__ty_2Einteger_2Eint @ X0))) = X0)) )),
% 10.96/2.40 inference(cnf_transformation,[],[f18])).
% 10.96/2.40 thf(f343,plain,(
% 10.96/2.40 (c_2Enum_2E0 = ((inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))),
% 10.96/2.40 inference(cnf_transformation,[],[f43])).
% 10.96/2.40 thf(f347,plain,(
% 10.96/2.40 (((surj__ty_2Einteger_2Eint @ (ap @ c_2Einteger_2Eint__neg @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) = ((surj__ty_2Einteger_2Eint @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))),
% 10.96/2.40 inference(cnf_transformation,[],[f56])).
% 10.96/2.40 thf(f351,plain,(
% 10.96/2.40 (((mem @ c_2Einteger_2Eint__lt @ (arr @ ty_2Einteger_2Eint @ (arr @ ty_2Einteger_2Eint @ bool)))) = $true)),
% 10.96/2.40 inference(cnf_transformation,[],[f134])).
% 10.96/2.40 thf(f357,plain,(
% 10.96/2.40 ( ! [X0 : tp__ty_2Enum_2Enum] : ((((inj__ty_2Einteger_2Eint @ (fo__c_2Einteger_2Eint__of__num @ X0))) = ((ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X0))))) )),
% 10.96/2.40 inference(cnf_transformation,[],[f29])).
% 10.96/2.40 thf(f360,plain,(
% 10.96/2.40 (((p @ c_2Ebool_2EF)) != $true)),
% 10.96/2.40 inference(cnf_transformation,[],[f166])).
% 10.96/2.40 thf(f364,definition,(
% 10.96/2.40 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 10.96/2.40 introduced(theory,[fool_exhaustiveness_axiom])).
% 10.96/2.40 thf(f372,definition,(
% 10.96/2.40 (sF16 = ((c_2Einteger__word_2Ei2w @ sK15)))),
% 10.96/2.40 introduced(definition,[new_symbols(definition,[sF16])],[function_definition])).
% 10.96/2.40 thf(f373,plain,(
% 10.96/2.40 (((c_2Einteger__word_2Ei2w @ sK15)) = sF16)),
% 10.96/2.40 inference(reorient_equations,[],[f372])).
% 10.96/2.40 thf(f374,definition,(
% 10.96/2.40 (sF17 = ((inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))),
% 10.96/2.40 introduced(definition,[new_symbols(definition,[sF17])],[function_definition])).
% 10.96/2.40 thf(f375,plain,(
% 10.96/2.40 (((inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)) = sF17)),
% 10.96/2.40 inference(reorient_equations,[],[f374])).
% 10.96/2.40 thf(f376,definition,(
% 10.96/2.40 (sF18 = ((ap @ c_2Einteger_2Eint__of__num @ sF17)))),
% 10.96/2.40 introduced(definition,[new_symbols(definition,[sF18])],[function_definition])).
% 10.96/2.40 thf(f377,plain,(
% 10.96/2.40 (((ap @ c_2Einteger_2Eint__of__num @ sF17)) = sF18)),
% 10.96/2.40 inference(reorient_equations,[],[f376])).
% 10.96/2.40 thf(f378,definition,(
% 10.96/2.40 (sF19 = ((ap @ sF16 @ sF18)))),
% 10.96/2.40 introduced(definition,[new_symbols(definition,[sF19])],[function_definition])).
% 10.96/2.40 thf(f379,plain,(
% 10.96/2.40 (((ap @ sF16 @ sF18)) = sF19)),
% 10.96/2.40 inference(reorient_equations,[],[f378])).
% 10.96/2.40 thf(f380,definition,(
% 10.96/2.40 (sF20 = ((c_2Ewords_2En2w @ sK15)))),
% 10.96/2.40 introduced(definition,[new_symbols(definition,[sF20])],[function_definition])).
% 10.96/2.40 thf(f381,definition,(
% 10.96/2.40 (sF21 = ((ap @ sF20 @ sF17)))),
% 10.96/2.40 introduced(definition,[new_symbols(definition,[sF21])],[function_definition])).
% 10.96/2.40 thf(f382,plain,(
% 10.96/2.40 (sF21 != sF19)),
% 10.96/2.40 inference(definition_folding,[],[f286,f381,f375,f380,f379,f377,f375,f373])).
% 10.96/2.40 thf(f411,plain,(
% 10.96/2.40 (((p @ c_2Ebool_2EF)) = $false) | ($true != $true)),
% 10.96/2.40 inference(constrained_superposition,[],[f360,f364])).
% 10.96/2.40 thf(f412,plain,(
% 10.96/2.40 (((p @ c_2Ebool_2EF)) = $false)),
% 10.96/2.40 inference(trivial_inequality_removal,[],[f411])).
% 10.96/2.40 thf(f413,plain,(
% 10.96/2.40 (c_2Enum_2E0 = sF17)),
% 10.96/2.40 inference(forward_demodulation,[],[f375,f343])).
% 10.96/2.40 thf(f419,plain,(
% 10.96/2.40 (((mem @ sF17 @ ty_2Enum_2Enum)) = $true)),
% 10.96/2.40 inference(forward_demodulation,[],[f321,f413])).
% 10.96/2.40 thf(f461,plain,(
% 10.96/2.40 ($true != $true) | (c_2Ebool_2EF = ((inj__o @ (p @ c_2Ebool_2EF))))),
% 10.96/2.40 inference(constrained_superposition,[],[f272,f271])).
% 10.96/2.40 thf(f465,plain,(
% 10.96/2.40 (c_2Ebool_2EF = ((inj__o @ (p @ c_2Ebool_2EF))))),
% 10.96/2.40 inference(trivial_inequality_removal,[],[f461])).
% 10.96/2.40 thf(f469,plain,(
% 10.96/2.40 (c_2Ebool_2EF = ((inj__o @ $false)))),
% 10.96/2.40 inference(forward_demodulation,[],[f465,f412])).
% 10.96/2.40 thf(f610,plain,(
% 10.96/2.40 (((ap @ c_2Einteger_2Eint__of__num @ c_2Enum_2E0)) = ((inj__ty_2Einteger_2Eint @ (fo__c_2Einteger_2Eint__of__num @ fo__c_2Enum_2E0))))),
% 10.96/2.40 inference(constrained_superposition,[],[f357,f343])).
% 10.96/2.40 thf(f611,plain,(
% 10.96/2.40 (((ap @ c_2Einteger_2Eint__of__num @ sF17)) = ((inj__ty_2Einteger_2Eint @ (fo__c_2Einteger_2Eint__of__num @ fo__c_2Enum_2E0))))),
% 10.96/2.40 inference(forward_demodulation,[],[f610,f413])).
% 10.96/2.40 thf(f612,plain,(
% 10.96/2.40 (sF18 = ((inj__ty_2Einteger_2Eint @ (fo__c_2Einteger_2Eint__of__num @ fo__c_2Enum_2E0))))),
% 10.96/2.40 inference(forward_demodulation,[],[f611,f377])).
% 10.96/2.40 thf(f613,plain,(
% 10.96/2.40 (((inj__ty_2Enum_2Enum @ (fo__c_2Einteger_2ENum @ (fo__c_2Einteger_2Eint__of__num @ fo__c_2Enum_2E0)))) = ((ap @ c_2Einteger_2ENum @ sF18)))),
% 10.96/2.40 inference(constrained_superposition,[],[f285,f612])).
% 10.96/2.40 thf(f614,plain,(
% 10.96/2.40 (((ap @ c_2Einteger_2Eint__neg @ sF18)) = ((inj__ty_2Einteger_2Eint @ (fo__c_2Einteger_2Eint__neg @ (fo__c_2Einteger_2Eint__of__num @ fo__c_2Enum_2E0)))))),
% 10.96/2.40 inference(constrained_superposition,[],[f266,f612])).
% 10.96/2.40 thf(f615,plain,(
% 10.96/2.40 (((mem @ sF18 @ ty_2Einteger_2Eint)) = $true)),
% 10.96/2.40 inference(constrained_superposition,[],[f297,f612])).
% 10.96/2.40 thf(f616,plain,(
% 10.96/2.40 (((fo__c_2Einteger_2Eint__of__num @ fo__c_2Enum_2E0)) = ((surj__ty_2Einteger_2Eint @ sF18)))),
% 10.96/2.40 inference(constrained_superposition,[],[f342,f612])).
% 10.96/2.40 thf(f617,plain,(
% 10.96/2.40 (((inj__ty_2Einteger_2Eint @ (surj__ty_2Einteger_2Eint @ sF18))) = sF18)),
% 10.96/2.40 inference(constrained_superposition,[],[f612,f616])).
% 10.96/2.40 thf(f627,plain,(
% 10.96/2.40 (((inj__ty_2Enum_2Enum @ (fo__c_2Einteger_2ENum @ (surj__ty_2Einteger_2Eint @ sF18)))) = ((ap @ c_2Einteger_2ENum @ sF18)))),
% 10.96/2.40 inference(forward_demodulation,[],[f613,f616])).
% 10.96/2.40 thf(f628,plain,(
% 10.96/2.40 (((ap @ c_2Einteger_2Eint__neg @ sF18)) = ((inj__ty_2Einteger_2Eint @ (fo__c_2Einteger_2Eint__neg @ (surj__ty_2Einteger_2Eint @ sF18)))))),
% 10.96/2.40 inference(forward_demodulation,[],[f614,f616])).
% 10.96/2.40 thf(f686,plain,(
% 10.96/2.40 ( ! [X0 : tp__ty_2Enum_2Enum] : ((((surj__ty_2Enum_2Enum @ (ap @ c_2Einteger_2ENum @ (inj__ty_2Einteger_2Eint @ (fo__c_2Einteger_2Eint__of__num @ X0))))) = X0)) )),
% 10.96/2.40 inference(forward_demodulation,[],[f298,f357])).
% 10.96/2.40 thf(f687,plain,(
% 10.96/2.40 ( ! [X0 : tp__ty_2Enum_2Enum] : ((((surj__ty_2Enum_2Enum @ (inj__ty_2Enum_2Enum @ (fo__c_2Einteger_2ENum @ (fo__c_2Einteger_2Eint__of__num @ X0))))) = X0)) )),
% 10.96/2.40 inference(forward_demodulation,[],[f686,f285])).
% 10.96/2.40 thf(f688,plain,(
% 10.96/2.40 ( ! [X0 : tp__ty_2Enum_2Enum] : ((((fo__c_2Einteger_2ENum @ (fo__c_2Einteger_2Eint__of__num @ X0))) = X0)) )),
% 10.96/2.40 inference(forward_demodulation,[],[f687,f318])).
% 10.96/2.40 thf(f689,plain,(
% 10.96/2.40 (fo__c_2Enum_2E0 = ((fo__c_2Einteger_2ENum @ (surj__ty_2Einteger_2Eint @ sF18))))),
% 10.96/2.40 inference(constrained_superposition,[],[f688,f616])).
% 10.96/2.40 thf(f690,plain,(
% 10.96/2.40 (((inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)) = ((ap @ c_2Einteger_2ENum @ sF18)))),
% 10.96/2.40 inference(constrained_superposition,[],[f627,f689])).
% 10.96/2.40 thf(f691,plain,(
% 10.96/2.40 (c_2Enum_2E0 = ((ap @ c_2Einteger_2ENum @ sF18)))),
% 10.96/2.40 inference(forward_demodulation,[],[f690,f343])).
% 10.96/2.40 thf(f692,plain,(
% 10.96/2.40 (sF17 = ((ap @ c_2Einteger_2ENum @ sF18)))),
% 10.96/2.40 inference(forward_demodulation,[],[f691,f413])).
% 10.96/2.40 thf(f768,plain,(
% 10.96/2.40 (((mem @ sF20 @ (arr @ ty_2Enum_2Enum @ (ty_2Efcp_2Ecart @ bool @ sK15)))) = $true)),
% 10.96/2.40 inference(constrained_superposition,[],[f319,f380])).
% 10.96/2.40 thf(f1368,plain,(
% 10.96/2.40 (((surj__ty_2Einteger_2Eint @ (ap @ c_2Einteger_2Eint__neg @ (inj__ty_2Einteger_2Eint @ (fo__c_2Einteger_2Eint__of__num @ fo__c_2Enum_2E0))))) = ((surj__ty_2Einteger_2Eint @ (inj__ty_2Einteger_2Eint @ (fo__c_2Einteger_2Eint__of__num @ fo__c_2Enum_2E0)))))),
% 10.96/2.40 inference(forward_demodulation,[],[f347,f357])).
% 10.96/2.40 thf(f1369,plain,(
% 10.96/2.40 (((surj__ty_2Einteger_2Eint @ (ap @ c_2Einteger_2Eint__neg @ (inj__ty_2Einteger_2Eint @ (fo__c_2Einteger_2Eint__of__num @ fo__c_2Enum_2E0))))) = ((fo__c_2Einteger_2Eint__of__num @ fo__c_2Enum_2E0)))),
% 10.96/2.40 inference(forward_demodulation,[],[f1368,f342])).
% 10.96/2.40 thf(f1370,plain,(
% 10.96/2.40 (((surj__ty_2Einteger_2Eint @ (ap @ c_2Einteger_2Eint__neg @ (inj__ty_2Einteger_2Eint @ (surj__ty_2Einteger_2Eint @ sF18))))) = ((surj__ty_2Einteger_2Eint @ sF18)))),
% 10.96/2.40 inference(forward_demodulation,[],[f1369,f616])).
% 10.96/2.40 thf(f1371,plain,(
% 10.96/2.40 (((surj__ty_2Einteger_2Eint @ (inj__ty_2Einteger_2Eint @ (fo__c_2Einteger_2Eint__neg @ (surj__ty_2Einteger_2Eint @ sF18))))) = ((surj__ty_2Einteger_2Eint @ sF18)))),
% 10.96/2.40 inference(forward_demodulation,[],[f1370,f266])).
% 10.96/2.40 thf(f1372,plain,(
% 10.96/2.40 (((fo__c_2Einteger_2Eint__neg @ (surj__ty_2Einteger_2Eint @ sF18))) = ((surj__ty_2Einteger_2Eint @ sF18)))),
% 10.96/2.40 inference(forward_demodulation,[],[f1371,f342])).
% 10.96/2.40 thf(f1407,plain,(
% 10.96/2.40 (((inj__ty_2Einteger_2Eint @ (surj__ty_2Einteger_2Eint @ sF18))) = ((ap @ c_2Einteger_2Eint__neg @ sF18)))),
% 10.96/2.40 inference(constrained_superposition,[],[f628,f1372])).
% 10.96/2.40 thf(f1408,plain,(
% 10.96/2.40 (((ap @ c_2Einteger_2Eint__neg @ sF18)) = sF18)),
% 10.96/2.40 inference(forward_demodulation,[],[f1407,f617])).
% 10.96/2.40 thf(f1467,plain,(
% 10.96/2.40 ( ! [X0 : del] : ((((ap @ (c_2Ewords_2En2w @ X0) @ c_2Enum_2E0)) = ((ap @ (c_2Ewords_2Eword__2comp @ X0) @ (ap @ (c_2Ewords_2En2w @ X0) @ c_2Enum_2E0))))) )),
% 10.96/2.40 inference(forward_demodulation,[],[f265,f343])).
% 10.96/2.40 thf(f1468,plain,(
% 10.96/2.40 ( ! [X0 : del] : ((((ap @ (c_2Ewords_2En2w @ X0) @ sF17)) = ((ap @ (c_2Ewords_2Eword__2comp @ X0) @ (ap @ (c_2Ewords_2En2w @ X0) @ sF17))))) )),
% 10.96/2.40 inference(forward_demodulation,[],[f1467,f413])).
% 10.96/2.40 thf(f1510,plain,(
% 10.96/2.40 (((ap @ (c_2Ewords_2Eword__2comp @ sK15) @ (ap @ sF20 @ sF17))) = ((ap @ sF20 @ sF17)))),
% 10.96/2.40 inference(constrained_superposition,[],[f1468,f380])).
% 10.96/2.40 thf(f1512,plain,(
% 10.96/2.40 (sF21 = ((ap @ (c_2Ewords_2Eword__2comp @ sK15) @ sF21)))),
% 10.96/2.40 inference(forward_demodulation,[],[f1510,f381])).
% 10.96/2.40 thf(f1711,plain,(
% 10.96/2.40 ( ! [X0 : del,X1 : del] : ((((mem @ sF20 @ (arr @ X1 @ X0))) != $true) | (((mem @ sF21 @ X0)) = $true) | (((mem @ sF17 @ X1)) != $true)) )),
% 10.96/2.40 inference(constrained_superposition,[],[f340,f381])).
% 10.96/2.40 thf(f1723,plain,(
% 10.96/2.40 ( ! [X2 : del,X0 : $i,X1 : $i] : ((((mem @ X1 @ X2)) != $true) | (((inj__o @ (p @ (ap @ X0 @ X1)))) = ((ap @ X0 @ X1))) | (((mem @ X0 @ (arr @ X2 @ bool))) != $true) | ($true != $true)) )),
% 10.96/2.40 inference(constrained_superposition,[],[f272,f340])).
% 10.96/2.40 thf(f1732,plain,(
% 10.96/2.40 ( ! [X2 : del,X0 : $i,X1 : $i] : ((((inj__o @ (p @ (ap @ X0 @ X1)))) = ((ap @ X0 @ X1))) | (((mem @ X0 @ (arr @ X2 @ bool))) != $true) | (((mem @ X1 @ X2)) != $true)) )),
% 10.96/2.40 inference(trivial_inequality_removal,[],[f1723])).
% 10.96/2.40 thf(f1754,plain,(
% 10.96/2.40 ($true = ((mem @ sF21 @ (ty_2Efcp_2Ecart @ bool @ sK15)))) | ($true != $true) | (((mem @ sF17 @ ty_2Enum_2Enum)) != $true)),
% 10.96/2.40 inference(constrained_superposition,[],[f1711,f768])).
% 10.96/2.40 thf(f1758,plain,(
% 10.96/2.40 ($true = ((mem @ sF21 @ (ty_2Efcp_2Ecart @ bool @ sK15)))) | (((mem @ sF17 @ ty_2Enum_2Enum)) != $true)),
% 10.96/2.40 inference(trivial_inequality_removal,[],[f1754])).
% 10.96/2.40 thf(f1759,plain,(
% 10.96/2.40 ($true = ((mem @ sF21 @ (ty_2Efcp_2Ecart @ bool @ sK15))))),
% 10.96/2.40 inference(forward_subsumption_resolution,[],[f1758,f419])).
% 10.96/2.40 thf(f1947,plain,(
% 10.96/2.40 ( ! [X0 : tp__ty_2Enum_2Enum,X1 : tp__ty_2Enum_2Enum] : (($true != ((p @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (inj__ty_2Einteger_2Eint @ (fo__c_2Einteger_2Eint__of__num @ X1))) @ (ap @ c_2Einteger_2Eint__neg @ (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X0)))))))) )),
% 10.96/2.40 inference(forward_demodulation,[],[f283,f357])).
% 10.96/2.40 thf(f1948,plain,(
% 10.96/2.40 ( ! [X0 : tp__ty_2Enum_2Enum,X1 : tp__ty_2Enum_2Enum] : ((((p @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (inj__ty_2Einteger_2Eint @ (fo__c_2Einteger_2Eint__of__num @ X1))) @ (ap @ c_2Einteger_2Eint__neg @ (inj__ty_2Einteger_2Eint @ (fo__c_2Einteger_2Eint__of__num @ X0)))))) != $true)) )),
% 10.96/2.40 inference(forward_demodulation,[],[f1947,f357])).
% 10.96/2.40 thf(f1949,plain,(
% 10.96/2.40 ( ! [X0 : tp__ty_2Enum_2Enum,X1 : tp__ty_2Enum_2Enum] : ((((p @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (inj__ty_2Einteger_2Eint @ (fo__c_2Einteger_2Eint__of__num @ X1))) @ (inj__ty_2Einteger_2Eint @ (fo__c_2Einteger_2Eint__neg @ (fo__c_2Einteger_2Eint__of__num @ X0)))))) != $true)) )),
% 10.96/2.40 inference(forward_demodulation,[],[f1948,f266])).
% 10.96/2.40 thf(f1950,plain,(
% 10.96/2.40 ( ! [X0 : tp__ty_2Enum_2Enum] : ((((p @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (inj__ty_2Einteger_2Eint @ (fo__c_2Einteger_2Eint__of__num @ X0))) @ (inj__ty_2Einteger_2Eint @ (fo__c_2Einteger_2Eint__neg @ (surj__ty_2Einteger_2Eint @ sF18)))))) != $true)) )),
% 10.96/2.40 inference(constrained_superposition,[],[f1949,f616])).
% 10.96/2.40 thf(f1959,plain,(
% 10.96/2.40 ( ! [X0 : tp__ty_2Enum_2Enum] : (($true != ((p @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (inj__ty_2Einteger_2Eint @ (fo__c_2Einteger_2Eint__of__num @ X0))) @ (ap @ c_2Einteger_2Eint__neg @ sF18)))))) )),
% 10.96/2.40 inference(forward_demodulation,[],[f1950,f628])).
% 10.96/2.40 thf(f1960,plain,(
% 10.96/2.40 ( ! [X0 : tp__ty_2Enum_2Enum] : (($true != ((p @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (inj__ty_2Einteger_2Eint @ (fo__c_2Einteger_2Eint__of__num @ X0))) @ sF18))))) )),
% 10.96/2.40 inference(forward_demodulation,[],[f1959,f1408])).
% 10.96/2.40 thf(f1962,plain,(
% 10.96/2.40 (((p @ (ap @ (ap @ c_2Einteger_2Eint__lt @ sF18) @ sF18))) != $true)),
% 10.96/2.40 inference(constrained_superposition,[],[f1960,f612])).
% 10.96/2.40 thf(f1970,plain,(
% 10.96/2.40 (((p @ (ap @ (ap @ c_2Einteger_2Eint__lt @ sF18) @ sF18))) = $false) | ($true != $true)),
% 10.96/2.40 inference(constrained_superposition,[],[f1962,f364])).
% 10.96/2.40 thf(f1972,plain,(
% 10.96/2.40 (((p @ (ap @ (ap @ c_2Einteger_2Eint__lt @ sF18) @ sF18))) = $false)),
% 10.96/2.40 inference(trivial_inequality_removal,[],[f1970])).
% 10.96/2.40 thf(f2670,plain,(
% 10.96/2.40 ( ! [X0 : tp__ty_2Einteger_2Eint,X1 : del] : ((((ap @ (ap @ (ap @ (c_2Ebool_2ECOND @ (ty_2Efcp_2Ecart @ bool @ X1)) @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (inj__ty_2Einteger_2Eint @ X0)) @ (inj__ty_2Einteger_2Eint @ (fo__c_2Einteger_2Eint__of__num @ fo__c_2Enum_2E0)))) @ (ap @ (c_2Ewords_2Eword__2comp @ X1) @ (ap @ (c_2Ewords_2En2w @ X1) @ (ap @ c_2Einteger_2ENum @ (ap @ c_2Einteger_2Eint__neg @ (inj__ty_2Einteger_2Eint @ X0)))))) @ (ap @ (c_2Ewords_2En2w @ X1) @ (ap @ c_2Einteger_2ENum @ (inj__ty_2Einteger_2Eint @ X0))))) = ((ap @ (c_2Einteger__word_2Ei2w @ X1) @ (inj__ty_2Einteger_2Eint @ X0))))) )),
% 10.96/2.40 inference(forward_demodulation,[],[f255,f357])).
% 10.96/2.40 thf(f2671,plain,(
% 10.96/2.40 ( ! [X0 : tp__ty_2Einteger_2Eint,X1 : del] : ((((ap @ (c_2Einteger__word_2Ei2w @ X1) @ (inj__ty_2Einteger_2Eint @ X0))) = ((ap @ (ap @ (ap @ (c_2Ebool_2ECOND @ (ty_2Efcp_2Ecart @ bool @ X1)) @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (inj__ty_2Einteger_2Eint @ X0)) @ sF18)) @ (ap @ (c_2Ewords_2Eword__2comp @ X1) @ (ap @ (c_2Ewords_2En2w @ X1) @ (ap @ c_2Einteger_2ENum @ (ap @ c_2Einteger_2Eint__neg @ (inj__ty_2Einteger_2Eint @ X0)))))) @ (ap @ (c_2Ewords_2En2w @ X1) @ (ap @ c_2Einteger_2ENum @ (inj__ty_2Einteger_2Eint @ X0))))))) )),
% 10.96/2.40 inference(forward_demodulation,[],[f2670,f612])).
% 10.96/2.40 thf(f2672,plain,(
% 10.96/2.40 ( ! [X0 : tp__ty_2Einteger_2Eint,X1 : del] : ((((ap @ (ap @ (ap @ (c_2Ebool_2ECOND @ (ty_2Efcp_2Ecart @ bool @ X1)) @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (inj__ty_2Einteger_2Eint @ X0)) @ sF18)) @ (ap @ (c_2Ewords_2Eword__2comp @ X1) @ (ap @ (c_2Ewords_2En2w @ X1) @ (ap @ c_2Einteger_2ENum @ (inj__ty_2Einteger_2Eint @ (fo__c_2Einteger_2Eint__neg @ X0)))))) @ (ap @ (c_2Ewords_2En2w @ X1) @ (ap @ c_2Einteger_2ENum @ (inj__ty_2Einteger_2Eint @ X0))))) = ((ap @ (c_2Einteger__word_2Ei2w @ X1) @ (inj__ty_2Einteger_2Eint @ X0))))) )),
% 10.96/2.40 inference(forward_demodulation,[],[f2671,f266])).
% 10.96/2.40 thf(f2673,plain,(
% 10.96/2.40 ( ! [X0 : tp__ty_2Einteger_2Eint,X1 : del] : ((((ap @ (c_2Einteger__word_2Ei2w @ X1) @ (inj__ty_2Einteger_2Eint @ X0))) = ((ap @ (ap @ (ap @ (c_2Ebool_2ECOND @ (ty_2Efcp_2Ecart @ bool @ X1)) @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (inj__ty_2Einteger_2Eint @ X0)) @ sF18)) @ (ap @ (c_2Ewords_2Eword__2comp @ X1) @ (ap @ (c_2Ewords_2En2w @ X1) @ (inj__ty_2Enum_2Enum @ (fo__c_2Einteger_2ENum @ (fo__c_2Einteger_2Eint__neg @ X0)))))) @ (ap @ (c_2Ewords_2En2w @ X1) @ (ap @ c_2Einteger_2ENum @ (inj__ty_2Einteger_2Eint @ X0))))))) )),
% 10.96/2.40 inference(forward_demodulation,[],[f2672,f285])).
% 10.96/2.40 thf(f2674,plain,(
% 10.96/2.40 ( ! [X0 : tp__ty_2Einteger_2Eint,X1 : del] : ((((ap @ (ap @ (ap @ (c_2Ebool_2ECOND @ (ty_2Efcp_2Ecart @ bool @ X1)) @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (inj__ty_2Einteger_2Eint @ X0)) @ sF18)) @ (ap @ (c_2Ewords_2Eword__2comp @ X1) @ (ap @ (c_2Ewords_2En2w @ X1) @ (inj__ty_2Enum_2Enum @ (fo__c_2Einteger_2ENum @ (fo__c_2Einteger_2Eint__neg @ X0)))))) @ (ap @ (c_2Ewords_2En2w @ X1) @ (inj__ty_2Enum_2Enum @ (fo__c_2Einteger_2ENum @ X0))))) = ((ap @ (c_2Einteger__word_2Ei2w @ X1) @ (inj__ty_2Einteger_2Eint @ X0))))) )),
% 10.96/2.40 inference(forward_demodulation,[],[f2673,f285])).
% 10.96/2.40 thf(f2723,plain,(
% 10.96/2.40 ( ! [X0 : del] : ((((mem @ sF18 @ X0)) != $true) | ($true != ((mem @ (ap @ c_2Einteger_2Eint__lt @ sF18) @ (arr @ X0 @ bool)))) | (((ap @ (ap @ c_2Einteger_2Eint__lt @ sF18) @ sF18)) = ((inj__o @ $false)))) )),
% 10.96/2.40 inference(constrained_superposition,[],[f1732,f1972])).
% 10.96/2.40 thf(f2766,plain,(
% 10.96/2.40 ( ! [X0 : del] : ((((mem @ sF18 @ X0)) != $true) | ($true != ((mem @ (ap @ c_2Einteger_2Eint__lt @ sF18) @ (arr @ X0 @ bool)))) | (c_2Ebool_2EF = ((ap @ (ap @ c_2Einteger_2Eint__lt @ sF18) @ sF18)))) )),
% 10.96/2.40 inference(forward_demodulation,[],[f2723,f469])).
% 10.96/2.40 thf(f2810,definition,(
% 10.96/2.40 spl22_64 <=> (c_2Ebool_2EF = ((ap @ (ap @ c_2Einteger_2Eint__lt @ sF18) @ sF18)))),
% 10.96/2.40 introduced(definition,[new_symbols(definition,[spl22_64])],[avatar_definition])).
% 10.96/2.40 thf(f2812,plain,(
% 10.96/2.40 (c_2Ebool_2EF = ((ap @ (ap @ c_2Einteger_2Eint__lt @ sF18) @ sF18))) | ~spl22_64),
% 10.96/2.40 inference(avatar_component_clause,[],[f2810])).
% 10.96/2.40 thf(f2814,definition,(
% 10.96/2.40 spl22_65 <=> ! [X0 : del] : ((((mem @ sF18 @ X0)) != $true) | ($true != ((mem @ (ap @ c_2Einteger_2Eint__lt @ sF18) @ (arr @ X0 @ bool)))))),
% 10.96/2.40 introduced(definition,[new_symbols(definition,[spl22_65])],[avatar_definition])).
% 10.96/2.40 thf(f2815,plain,(
% 10.96/2.40 ( ! [X0 : del] : (($true != ((mem @ (ap @ c_2Einteger_2Eint__lt @ sF18) @ (arr @ X0 @ bool)))) | (((mem @ sF18 @ X0)) != $true)) ) | ~spl22_65),
% 10.96/2.40 inference(avatar_component_clause,[],[f2814])).
% 10.96/2.40 thf(f2816,plain,(
% 10.96/2.40 spl22_64 | spl22_65),
% 10.96/2.40 inference(avatar_split_clause,[],[f2766,f2814,f2810])).
% 10.96/2.40 thf(f2971,plain,(
% 10.96/2.40 ( ! [X0 : tp__ty_2Einteger_2Eint] : ((((ap @ (ap @ (ap @ (c_2Ebool_2ECOND @ (ty_2Efcp_2Ecart @ bool @ sK15)) @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (inj__ty_2Einteger_2Eint @ X0)) @ sF18)) @ (ap @ (c_2Ewords_2Eword__2comp @ sK15) @ (ap @ sF20 @ (inj__ty_2Enum_2Enum @ (fo__c_2Einteger_2ENum @ (fo__c_2Einteger_2Eint__neg @ X0)))))) @ (ap @ sF20 @ (inj__ty_2Enum_2Enum @ (fo__c_2Einteger_2ENum @ X0))))) = ((ap @ (c_2Einteger__word_2Ei2w @ sK15) @ (inj__ty_2Einteger_2Eint @ X0))))) )),
% 10.96/2.40 inference(constrained_superposition,[],[f2674,f380])).
% 10.96/2.40 thf(f2986,plain,(
% 10.96/2.40 ( ! [X0 : tp__ty_2Einteger_2Eint] : ((((ap @ (ap @ (ap @ (c_2Ebool_2ECOND @ (ty_2Efcp_2Ecart @ bool @ sK15)) @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (inj__ty_2Einteger_2Eint @ X0)) @ sF18)) @ (ap @ (c_2Ewords_2Eword__2comp @ sK15) @ (ap @ sF20 @ (inj__ty_2Enum_2Enum @ (fo__c_2Einteger_2ENum @ (fo__c_2Einteger_2Eint__neg @ X0)))))) @ (ap @ sF20 @ (inj__ty_2Enum_2Enum @ (fo__c_2Einteger_2ENum @ X0))))) = ((ap @ sF16 @ (inj__ty_2Einteger_2Eint @ X0))))) )),
% 10.96/2.40 inference(forward_demodulation,[],[f2971,f373])).
% 10.96/2.40 thf(f7072,plain,(
% 10.96/2.40 ( ! [X0 : del,X1 : del] : ((((mem @ sF18 @ X0)) != $true) | ($true != $true) | (((mem @ c_2Einteger_2Eint__lt @ (arr @ X1 @ (arr @ X0 @ bool)))) != $true) | (((mem @ sF18 @ X1)) != $true)) ) | ~spl22_65),
% 10.96/2.40 inference(constrained_superposition,[],[f2815,f340])).
% 10.96/2.40 thf(f7074,plain,(
% 10.96/2.40 ( ! [X0 : del,X1 : del] : ((((mem @ c_2Einteger_2Eint__lt @ (arr @ X1 @ (arr @ X0 @ bool)))) != $true) | (((mem @ sF18 @ X1)) != $true) | (((mem @ sF18 @ X0)) != $true)) ) | ~spl22_65),
% 10.96/2.40 inference(trivial_inequality_removal,[],[f7072])).
% 10.96/2.40 thf(f7227,plain,(
% 10.96/2.40 (((mem @ sF18 @ ty_2Einteger_2Eint)) != $true) | (((mem @ sF18 @ ty_2Einteger_2Eint)) != $true) | ($true != $true) | ~spl22_65),
% 10.96/2.40 inference(constrained_superposition,[],[f7074,f351])).
% 10.96/2.40 thf(f7229,plain,(
% 10.96/2.40 ($true != $true) | (((mem @ sF18 @ ty_2Einteger_2Eint)) != $true) | ~spl22_65),
% 10.96/2.40 inference(duplicate_literal_removal,[],[f7227])).
% 10.96/2.40 thf(f7230,plain,(
% 10.96/2.40 (((mem @ sF18 @ ty_2Einteger_2Eint)) != $true) | ~spl22_65),
% 10.96/2.40 inference(trivial_inequality_removal,[],[f7229])).
% 10.96/2.40 thf(f7232,plain,(
% 10.96/2.40 $false | ~spl22_65),
% 10.96/2.40 inference(forward_subsumption_resolution,[],[f7230,f615])).
% 10.96/2.40 thf(f7233,plain,(
% 10.96/2.40 ~spl22_65),
% 10.96/2.40 inference(avatar_contradiction_clause,[],[f7232])).
% 10.96/2.40 thf(f7948,plain,(
% 10.96/2.40 (((ap @ sF16 @ (inj__ty_2Einteger_2Eint @ (surj__ty_2Einteger_2Eint @ sF18)))) = ((ap @ (ap @ (ap @ (c_2Ebool_2ECOND @ (ty_2Efcp_2Ecart @ bool @ sK15)) @ (ap @ (ap @ c_2Einteger_2Eint__lt @ (inj__ty_2Einteger_2Eint @ (surj__ty_2Einteger_2Eint @ sF18))) @ sF18)) @ (ap @ (c_2Ewords_2Eword__2comp @ sK15) @ (ap @ sF20 @ (inj__ty_2Enum_2Enum @ (fo__c_2Einteger_2ENum @ (surj__ty_2Einteger_2Eint @ sF18)))))) @ (ap @ sF20 @ (inj__ty_2Enum_2Enum @ (fo__c_2Einteger_2ENum @ (surj__ty_2Einteger_2Eint @ sF18)))))))),
% 10.96/2.40 inference(constrained_superposition,[],[f2986,f1372])).
% 10.96/2.40 thf(f7971,plain,(
% 10.96/2.40 (((ap @ sF16 @ sF18)) = ((ap @ (ap @ (ap @ (c_2Ebool_2ECOND @ (ty_2Efcp_2Ecart @ bool @ sK15)) @ (ap @ (ap @ c_2Einteger_2Eint__lt @ sF18) @ sF18)) @ (ap @ (c_2Ewords_2Eword__2comp @ sK15) @ (ap @ sF20 @ (inj__ty_2Enum_2Enum @ (fo__c_2Einteger_2ENum @ (surj__ty_2Einteger_2Eint @ sF18)))))) @ (ap @ sF20 @ (inj__ty_2Enum_2Enum @ (fo__c_2Einteger_2ENum @ (surj__ty_2Einteger_2Eint @ sF18)))))))),
% 10.96/2.40 inference(forward_demodulation,[],[f7948,f617])).
% 10.96/2.40 thf(f7978,plain,(
% 10.96/2.40 (((ap @ (ap @ (ap @ (c_2Ebool_2ECOND @ (ty_2Efcp_2Ecart @ bool @ sK15)) @ c_2Ebool_2EF) @ (ap @ (c_2Ewords_2Eword__2comp @ sK15) @ (ap @ sF20 @ (inj__ty_2Enum_2Enum @ (fo__c_2Einteger_2ENum @ (surj__ty_2Einteger_2Eint @ sF18)))))) @ (ap @ sF20 @ (inj__ty_2Enum_2Enum @ (fo__c_2Einteger_2ENum @ (surj__ty_2Einteger_2Eint @ sF18)))))) = ((ap @ sF16 @ sF18))) | ~spl22_64),
% 10.96/2.40 inference(forward_demodulation,[],[f7971,f2812])).
% 10.96/2.40 thf(f7984,plain,(
% 10.96/2.40 (((ap @ (ap @ (ap @ (c_2Ebool_2ECOND @ (ty_2Efcp_2Ecart @ bool @ sK15)) @ c_2Ebool_2EF) @ (ap @ (c_2Ewords_2Eword__2comp @ sK15) @ (ap @ sF20 @ (inj__ty_2Enum_2Enum @ (fo__c_2Einteger_2ENum @ (surj__ty_2Einteger_2Eint @ sF18)))))) @ (ap @ sF20 @ (inj__ty_2Enum_2Enum @ (fo__c_2Einteger_2ENum @ (surj__ty_2Einteger_2Eint @ sF18)))))) = sF19) | ~spl22_64),
% 10.96/2.40 inference(forward_demodulation,[],[f7978,f379])).
% 10.96/2.40 thf(f7990,plain,(
% 10.96/2.40 (((ap @ (ap @ (ap @ (c_2Ebool_2ECOND @ (ty_2Efcp_2Ecart @ bool @ sK15)) @ c_2Ebool_2EF) @ (ap @ (c_2Ewords_2Eword__2comp @ sK15) @ (ap @ sF20 @ (ap @ c_2Einteger_2ENum @ sF18)))) @ (ap @ sF20 @ (ap @ c_2Einteger_2ENum @ sF18)))) = sF19) | ~spl22_64),
% 10.96/2.40 inference(forward_demodulation,[],[f7984,f627])).
% 10.96/2.40 thf(f7996,plain,(
% 10.96/2.40 (((ap @ (ap @ (ap @ (c_2Ebool_2ECOND @ (ty_2Efcp_2Ecart @ bool @ sK15)) @ c_2Ebool_2EF) @ (ap @ (c_2Ewords_2Eword__2comp @ sK15) @ (ap @ sF20 @ sF17))) @ (ap @ sF20 @ sF17))) = sF19) | ~spl22_64),
% 10.96/2.40 inference(forward_demodulation,[],[f7990,f692])).
% 10.96/2.40 thf(f8002,plain,(
% 10.96/2.40 (((ap @ (ap @ (ap @ (c_2Ebool_2ECOND @ (ty_2Efcp_2Ecart @ bool @ sK15)) @ c_2Ebool_2EF) @ (ap @ (c_2Ewords_2Eword__2comp @ sK15) @ sF21)) @ sF21)) = sF19) | ~spl22_64),
% 10.96/2.40 inference(forward_demodulation,[],[f7996,f381])).
% 10.96/2.40 thf(f8008,plain,(
% 10.96/2.40 (((ap @ (ap @ (ap @ (c_2Ebool_2ECOND @ (ty_2Efcp_2Ecart @ bool @ sK15)) @ c_2Ebool_2EF) @ sF21) @ sF21)) = sF19) | ~spl22_64),
% 10.96/2.40 inference(forward_demodulation,[],[f8002,f1512])).
% 10.96/2.40 thf(f8193,plain,(
% 10.96/2.40 ($true != ((mem @ sF21 @ (ty_2Efcp_2Ecart @ bool @ sK15)))) | (sF21 = sF19) | ($true != ((mem @ sF21 @ (ty_2Efcp_2Ecart @ bool @ sK15)))) | ~spl22_64),
% 10.96/2.40 inference(constrained_superposition,[],[f8008,f329])).
% 10.96/2.40 thf(f8201,plain,(
% 10.96/2.40 (sF21 = sF19) | ($true != ((mem @ sF21 @ (ty_2Efcp_2Ecart @ bool @ sK15)))) | ~spl22_64),
% 10.96/2.40 inference(duplicate_literal_removal,[],[f8193])).
% 10.96/2.40 thf(f8207,plain,(
% 10.96/2.40 ($true != ((mem @ sF21 @ (ty_2Efcp_2Ecart @ bool @ sK15)))) | ~spl22_64),
% 10.96/2.40 inference(forward_subsumption_resolution,[],[f8201,f382])).
% 10.96/2.40 thf(f8211,plain,(
% 10.96/2.40 $false | ~spl22_64),
% 10.96/2.40 inference(forward_subsumption_resolution,[],[f8207,f1759])).
% 10.96/2.40 thf(f8212,plain,(
% 10.96/2.40 ~spl22_64),
% 10.96/2.40 inference(avatar_contradiction_clause,[],[f8211])).
% 10.96/2.40 cnf(s53, plain, spl22_64 | spl22_65, inference(sat_conversion,[],[f2816])).
% 10.96/2.40 cnf(s424, plain, ~spl22_65, inference(sat_conversion,[],[f7233])).
% 10.96/2.40 cnf(s481, plain, ~spl22_64, inference(sat_conversion,[],[f8212])).
% 10.96/2.40 cnf(s485, plain, $false, inference(rat,[],[s53,s424,s481])).
% 10.96/2.40 thf(f8217,plain,(
% 10.96/2.40 $false),
% 10.96/2.40 inference(avatar_sat_refutation,[],[s485])).
% 10.96/2.40 % SZS output end Proof for theBenchmark
% 10.96/2.40 % (3620362)------------------------------
% 10.96/2.40 % (3620362)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.96/2.40 % (3620362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.40 % (3620362)CaDiCaL version: 2.1.3
% 10.96/2.40 % (3620362)Termination reason: Refutation
% 10.96/2.40 % (3620362)Time elapsed: 0.729 s
% 10.96/2.40 % (3620362)Peak memory usage: 16 MB
% 10.96/2.40 % (3620362)Instructions burned: 821 (million)
% 10.96/2.40 % (3620182)Success in time 2.084 s
% 10.96/2.40 % Vampire exiting
%------------------------------------------------------------------------------