%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW470^1 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:40:17 AM UTC 2026
% Result : Theorem 6.05s 1.21s
% Output : Refutation 6.05s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW470^1 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.21 % Computer : n016.cluster.edu
% 0.11/0.21 % Model : x86_64 x86_64
% 0.11/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.21 % Memory : 8046.5625MB
% 0.11/0.21 % OS : Linux 6.8.0-71-generic
% 0.11/0.22 % CPULimit : 300
% 0.11/0.22 % WCLimit : 300
% 0.11/0.22 % DateTime : Tue Sep 29 16:09:50 UTC 2026
% 0.11/0.22 % CPUTime :
% 0.11/0.22 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.26 Running higher-order theorem proving
% 0.25/0.30 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.32/0.49 % (534056)Detected a higher-order problem, will run a greedy HOL sequence.
% 1.32/0.49 % (534063)lrs+10_16_si=on:nwc=1.5:random_seed=4007938882:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 1.32/0.49 % (534068)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=3536945626:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 1.32/0.49 % (534069)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 1.32/0.49 % (534069)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 1.32/0.49 % (534063)Instruction limit reached!
% 1.32/0.49 % (534063)------------------------------
% 1.32/0.49 % (534063)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.32/0.49 % (534063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.32/0.49 % (534063)CaDiCaL version: 2.1.3
% 1.32/0.49 % (534063)Termination reason: Instruction limit
% 1.32/0.49 % (534063)Termination phase: Property scanning
% 1.32/0.49 % (534063)Time elapsed: 0.011 s
% 1.32/0.49 % (534063)Peak memory usage: 11 MB
% 1.32/0.49 % (534063)Instructions burned: 26 (million)
% 1.32/0.49 % (534062)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3087935636:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 1.32/0.49 % (534067)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=1172362708:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 1.32/0.49 % (534065)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=2558655677:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 1.32/0.49 % (534066)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=2088544075:hsq=on:hsqr=16,1:s2a=on:i=634:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2999 on theBenchmark for (2999ds/634Mi)
% 1.32/0.49 % (534069)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=3880955021:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 1.32/0.49 % (534065)Instruction limit reached!
% 1.32/0.49 % (534065)------------------------------
% 1.32/0.49 % (534065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.32/0.49 % (534065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.32/0.49 % (534065)CaDiCaL version: 2.1.3
% 1.32/0.49 % (534065)Termination reason: Instruction limit
% 1.32/0.49 % (534065)Termination phase: shuffling
% 1.32/0.49 % (534065)Time elapsed: 0.003 s
% 1.32/0.49 % (534065)Peak memory usage: 10 MB
% 1.32/0.49 % (534065)Instructions burned: 4 (million)
% 1.32/0.49 % (534073)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3058268866:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 1.32/0.49 % (534073)Instruction limit reached!
% 1.32/0.49 % (534073)------------------------------
% 1.32/0.49 % (534073)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.32/0.49 % (534073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.32/0.49 % (534073)CaDiCaL version: 2.1.3
% 1.32/0.49 % (534073)Termination reason: Instruction limit
% 1.32/0.49 % (534073)Termination phase: shuffling
% 1.32/0.49 % (534073)Time elapsed: 0.001 s
% 1.32/0.49 % (534073)Peak memory usage: 10 MB
% 1.32/0.49 % (534073)Instructions burned: 3 (million)
% 1.32/0.49 % (534067)Instruction limit reached!
% 1.32/0.49 % (534067)------------------------------
% 1.32/0.49 % (534067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.32/0.49 % (534067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.32/0.49 % (534067)CaDiCaL version: 2.1.3
% 1.32/0.49 % (534067)Termination reason: Instruction limit
% 1.32/0.49 % (534067)Termination phase: Property scanning
% 1.32/0.49 % (534067)Time elapsed: 0.020 s
% 1.32/0.49 % (534067)Peak memory usage: 11 MB
% 1.32/0.49 % (534067)Instructions burned: 24 (million)
% 1.32/0.49 % (534081)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.32/0.49 % (534081)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=41638887:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 1.32/0.55 % (534078)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=445662364:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 1.32/0.55 % (534081)Instruction limit reached!
% 1.32/0.55 % (534081)------------------------------
% 1.32/0.55 % (534081)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.32/0.55 % (534081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.32/0.55 % (534081)CaDiCaL version: 2.1.3
% 1.32/0.55 % (534081)Termination reason: Instruction limit
% 1.32/0.55 % (534081)Termination phase: shuffling
% 1.32/0.55 % (534081)Time elapsed: 0.004 s
% 1.32/0.55 % (534081)Peak memory usage: 10 MB
% 1.32/0.55 % (534081)Instructions burned: 9 (million)
% 1.32/0.55 % (534078)Instruction limit reached!
% 1.32/0.55 % (534078)------------------------------
% 1.32/0.55 % (534078)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.32/0.55 % (534078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.32/0.55 % (534078)CaDiCaL version: 2.1.3
% 1.32/0.55 % (534078)Termination reason: Instruction limit
% 1.32/0.55 % (534078)Termination phase: shuffling
% 1.32/0.55 % (534078)Time elapsed: 0.005 s
% 1.32/0.55 % (534078)Peak memory usage: 10 MB
% 1.32/0.55 % (534078)Instructions burned: 6 (million)
% 1.32/0.55 % (534068)Instruction limit reached!
% 1.32/0.55 % (534068)------------------------------
% 1.32/0.55 % (534068)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.32/0.55 % (534068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.32/0.55 % (534068)CaDiCaL version: 2.1.3
% 1.32/0.55 % (534068)Termination reason: Instruction limit
% 1.32/0.55 % (534068)Termination phase: Saturation
% 1.32/0.55 % (534068)Time elapsed: 0.065 s
% 1.32/0.55 % (534068)Peak memory usage: 13 MB
% 1.32/0.55 % (534068)Instructions burned: 75 (million)
% 1.32/0.55 % (534082)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=1875064067:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 1.32/0.55 % (534085)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 1.32/0.55 % (534085)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.32/0.55 % (534085)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=931418671:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 1.32/0.55 % (534087)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=274348219:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 1.32/0.55 % (534082)Instruction limit reached!
% 1.32/0.55 % (534082)------------------------------
% 1.32/0.55 % (534082)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.32/0.55 % (534082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.32/0.55 % (534082)CaDiCaL version: 2.1.3
% 1.32/0.55 % (534082)Termination reason: Instruction limit
% 1.32/0.55 % (534082)Termination phase: Property scanning
% 1.32/0.55 % (534082)Time elapsed: 0.010 s
% 1.32/0.55 % (534082)Peak memory usage: 10 MB
% 1.32/0.55 % (534082)Instructions burned: 12 (million)
% 1.32/0.55 % (534085)Instruction limit reached!
% 1.32/0.55 % (534085)------------------------------
% 1.32/0.55 % (534085)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.32/0.55 % (534085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.32/0.55 % (534085)CaDiCaL version: 2.1.3
% 1.32/0.55 % (534085)Termination reason: Instruction limit
% 1.32/0.55 % (534085)Termination phase: Property scanning
% 1.32/0.55 % (534085)Time elapsed: 0.011 s
% 1.32/0.55 % (534085)Peak memory usage: 10 MB
% 1.32/0.55 % (534085)Instructions burned: 28 (million)
% 1.32/0.55 % (534062)Instruction limit reached!
% 1.32/0.55 % (534062)------------------------------
% 1.32/0.55 % (534062)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.32/0.55 % (534062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.07/0.62 % (534062)CaDiCaL version: 2.1.3
% 2.07/0.62 % (534062)Termination reason: Instruction limit
% 2.07/0.62 % (534062)Termination phase: Saturation
% 2.07/0.62 % (534062)Time elapsed: 0.076 s
% 2.07/0.62 % (534062)Peak memory usage: 13 MB
% 2.07/0.62 % (534062)Instructions burned: 87 (million)
% 2.07/0.62 % (534093)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=359293285:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/38Mi)
% 2.07/0.62 % (534089)lrs+10_1_si=on:cs=on:random_seed=800772114:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 2.07/0.62 % (534092)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 2.07/0.62 % (534092)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=3203562022:i=2:add=on:rtra=on_2998 on theBenchmark for (2998ds/2Mi)
% 2.07/0.62 % (534089)Instruction limit reached!
% 2.07/0.62 % (534089)------------------------------
% 2.07/0.62 % (534089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.07/0.62 % (534089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.07/0.62 % (534089)CaDiCaL version: 2.1.3
% 2.07/0.62 % (534089)Termination reason: Instruction limit
% 2.07/0.62 % (534089)Termination phase: Property scanning
% 2.07/0.62 % (534089)Time elapsed: 0.009 s
% 2.07/0.62 % (534089)Peak memory usage: 10 MB
% 2.07/0.62 % (534089)Instructions burned: 11 (million)
% 2.07/0.62 % (534092)Instruction limit reached!
% 2.07/0.62 % (534092)------------------------------
% 2.07/0.62 % (534092)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.07/0.62 % (534092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.07/0.62 % (534092)CaDiCaL version: 2.1.3
% 2.07/0.62 % (534092)Termination reason: Instruction limit
% 2.07/0.62 % (534092)Termination phase: shuffling
% 2.07/0.62 % (534092)Time elapsed: 0.003 s
% 2.07/0.62 % (534092)Peak memory usage: 10 MB
% 2.07/0.62 % (534092)Instructions burned: 2 (million)
% 2.07/0.62 % (534094)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=2468066999:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 2.07/0.62 % (534093)Instruction limit reached!
% 2.07/0.62 % (534093)------------------------------
% 2.07/0.62 % (534093)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.07/0.62 % (534093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.07/0.62 % (534093)CaDiCaL version: 2.1.3
% 2.07/0.62 % (534093)Termination reason: Instruction limit
% 2.07/0.62 % (534093)Termination phase: Saturation
% 2.07/0.62 % (534093)Time elapsed: 0.017 s
% 2.07/0.62 % (534093)Peak memory usage: 12 MB
% 2.07/0.62 % (534093)Instructions burned: 38 (million)
% 2.07/0.62 % (534087)Instruction limit reached!
% 2.07/0.62 % (534087)------------------------------
% 2.07/0.62 % (534087)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.07/0.62 % (534087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.07/0.62 % (534087)CaDiCaL version: 2.1.3
% 2.07/0.62 % (534087)Termination reason: Instruction limit
% 2.07/0.62 % (534087)Termination phase: Saturation
% 2.07/0.62 % (534087)Time elapsed: 0.058 s
% 2.07/0.62 % (534087)Peak memory usage: 13 MB
% 2.07/0.62 % (534087)Instructions burned: 86 (million)
% 2.07/0.62 % (534102)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=2047188335:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 2.07/0.62 % (534099)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=478089778:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 2.07/0.62 % (534100)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=3055761981:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 2.07/0.62 % (534069)Instruction limit reached!
% 2.07/0.62 % (534069)------------------------------
% 2.07/0.62 % (534069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.07/0.62 % (534069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.07/0.62 % (534069)CaDiCaL version: 2.1.3
% 2.07/0.62 % (534069)Termination reason: Instruction limit
% 2.07/0.62 % (534069)Termination phase: Saturation
% 2.07/0.62 % (534069)Time elapsed: 0.140 s
% 2.46/0.69 % (534069)Peak memory usage: 13 MB
% 2.46/0.69 % (534069)Instructions burned: 157 (million)
% 2.46/0.69 % (534100)Instruction limit reached!
% 2.46/0.69 % (534100)------------------------------
% 2.46/0.69 % (534100)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.46/0.69 % (534100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.46/0.69 % (534100)CaDiCaL version: 2.1.3
% 2.46/0.69 % (534100)Termination reason: Instruction limit
% 2.46/0.69 % (534100)Termination phase: Preprocessing 3
% 2.46/0.69 % (534100)Time elapsed: 0.013 s
% 2.46/0.69 % (534100)Peak memory usage: 10 MB
% 2.46/0.69 % (534100)Instructions burned: 14 (million)
% 2.46/0.69 % (534099)Instruction limit reached!
% 2.46/0.69 % (534099)------------------------------
% 2.46/0.69 % (534099)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.46/0.69 % (534099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.46/0.69 % (534099)CaDiCaL version: 2.1.3
% 2.46/0.69 % (534099)Termination reason: Instruction limit
% 2.46/0.69 % (534099)Termination phase: Property scanning
% 2.46/0.69 % (534099)Time elapsed: 0.022 s
% 2.46/0.69 % (534099)Peak memory usage: 11 MB
% 2.46/0.69 % (534099)Instructions burned: 26 (million)
% 2.46/0.69 % (534103)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=799388394:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 2.46/0.69 % (534108)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=3740991508:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2998 on theBenchmark for (2998ds/2Mi)
% 2.46/0.69 % (534108)Instruction limit reached!
% 2.46/0.69 % (534108)------------------------------
% 2.46/0.69 % (534108)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.46/0.69 % (534108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.46/0.69 % (534108)CaDiCaL version: 2.1.3
% 2.46/0.69 % (534108)Termination reason: Instruction limit
% 2.46/0.69 % (534108)Termination phase: shuffling
% 2.46/0.69 % (534108)Time elapsed: 0.002 s
% 2.46/0.69 % (534108)Peak memory usage: 10 MB
% 2.46/0.69 % (534108)Instructions burned: 4 (million)
% 2.46/0.69 % (534103)Instruction limit reached!
% 2.46/0.69 % (534103)------------------------------
% 2.46/0.69 % (534103)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.46/0.69 % (534103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.46/0.69 % (534103)CaDiCaL version: 2.1.3
% 2.46/0.69 % (534103)Termination reason: Instruction limit
% 2.46/0.69 % (534103)Termination phase: Preprocessing 3
% 2.46/0.69 % (534103)Time elapsed: 0.012 s
% 2.46/0.69 % (534103)Peak memory usage: 10 MB
% 2.46/0.69 % (534103)Instructions burned: 14 (million)
% 2.46/0.69 % (534109)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3619567024:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 2.46/0.69 % (534113)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=1891297157:cond=on:i=60:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/60Mi)
% 2.46/0.69 % (534110)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=1141442164:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 2.46/0.69 % (534114)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.46/0.69 % (534114)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 2.46/0.69 % (534114)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=1327948137:i=14:add=off:nm=40:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 2.46/0.69 % (534110)Instruction limit reached!
% 2.46/0.69 % (534110)------------------------------
% 2.46/0.69 % (534110)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.46/0.69 % (534110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.46/0.69 % (534110)CaDiCaL version: 2.1.3
% 2.46/0.69 % (534110)Termination reason: Instruction limit
% 2.46/0.69 % (534110)Termination phase: Property scanning
% 2.46/0.69 % (534110)Time elapsed: 0.019 s
% 2.46/0.69 % (534110)Peak memory usage: 11 MB
% 2.63/0.77 % (534110)Instructions burned: 23 (million)
% 2.63/0.77 % (534109)Instruction limit reached!
% 2.63/0.77 % (534109)------------------------------
% 2.63/0.77 % (534109)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.63/0.77 % (534109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.63/0.77 % (534109)CaDiCaL version: 2.1.3
% 2.63/0.77 % (534109)Termination reason: Instruction limit
% 2.63/0.77 % (534109)Termination phase: Property scanning
% 2.63/0.77 % (534109)Time elapsed: 0.022 s
% 2.63/0.77 % (534109)Peak memory usage: 10 MB
% 2.63/0.77 % (534109)Instructions burned: 27 (million)
% 2.63/0.77 % (534114)Instruction limit reached!
% 2.63/0.77 % (534114)------------------------------
% 2.63/0.77 % (534114)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.63/0.77 % (534114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.63/0.77 % (534114)CaDiCaL version: 2.1.3
% 2.63/0.77 % (534114)Termination reason: Instruction limit
% 2.63/0.77 % (534114)Termination phase: Property scanning
% 2.63/0.77 % (534114)Time elapsed: 0.013 s
% 2.63/0.77 % (534114)Peak memory usage: 10 MB
% 2.63/0.77 % (534114)Instructions burned: 14 (million)
% 2.63/0.77 % (534119)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 2.63/0.77 % (534113)Instruction limit reached!
% 2.63/0.77 % (534113)------------------------------
% 2.63/0.77 % (534113)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.63/0.77 % (534113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.63/0.77 % (534113)CaDiCaL version: 2.1.3
% 2.63/0.77 % (534113)Termination reason: Instruction limit
% 2.63/0.77 % (534113)Termination phase: Saturation
% 2.63/0.77 % (534113)Time elapsed: 0.051 s
% 2.63/0.77 % (534113)Peak memory usage: 13 MB
% 2.63/0.77 % (534113)Instructions burned: 60 (million)
% 2.63/0.77 % (534119)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=434623974:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2997 on theBenchmark for (2997ds/8Mi)
% 2.63/0.77 % (534120)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=978603099:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2997 on theBenchmark for (2997ds/31Mi)
% 2.63/0.77 % (534121)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=2770737194:i=7:hud=5:bd=preordered:rtra=on:bet=on_2997 on theBenchmark for (2997ds/7Mi)
% 2.63/0.77 % (534119)Instruction limit reached!
% 2.63/0.77 % (534119)------------------------------
% 2.63/0.77 % (534119)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.63/0.77 % (534119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.63/0.77 % (534119)CaDiCaL version: 2.1.3
% 2.63/0.77 % (534119)Termination reason: Instruction limit
% 2.63/0.77 % (534119)Termination phase: shuffling
% 2.63/0.77 % (534119)Time elapsed: 0.007 s
% 2.63/0.77 % (534119)Peak memory usage: 10 MB
% 2.63/0.77 % (534119)Instructions burned: 8 (million)
% 2.63/0.77 % (534121)Instruction limit reached!
% 2.63/0.77 % (534121)------------------------------
% 2.63/0.77 % (534121)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.63/0.77 % (534121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.63/0.77 % (534121)CaDiCaL version: 2.1.3
% 2.63/0.77 % (534121)Termination reason: Instruction limit
% 2.63/0.77 % (534121)Termination phase: shuffling
% 2.63/0.77 % (534121)Time elapsed: 0.006 s
% 2.63/0.77 % (534121)Peak memory usage: 10 MB
% 2.63/0.77 % (534121)Instructions burned: 7 (million)
% 2.63/0.77 % (534102)Instruction limit reached!
% 2.63/0.77 % (534102)------------------------------
% 2.63/0.77 % (534102)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.63/0.77 % (534102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.63/0.77 % (534102)CaDiCaL version: 2.1.3
% 2.63/0.77 % (534102)Termination reason: Instruction limit
% 2.63/0.77 % (534102)Termination phase: Saturation
% 2.63/0.77 % (534102)Time elapsed: 0.133 s
% 2.63/0.77 % (534102)Peak memory usage: 13 MB
% 2.63/0.77 % (534102)Instructions burned: 339 (million)
% 2.63/0.77 % (534122)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=2022064291:i=23:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/23Mi)
% 2.63/0.77 % (534120)Instruction limit reached!
% 3.60/0.93 % (534120)------------------------------
% 3.60/0.93 % (534120)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.60/0.93 % (534120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.60/0.93 % (534120)CaDiCaL version: 2.1.3
% 3.60/0.93 % (534120)Termination reason: Instruction limit
% 3.60/0.93 % (534120)Termination phase: Property scanning
% 3.60/0.93 % (534120)Time elapsed: 0.026 s
% 3.60/0.93 % (534120)Peak memory usage: 10 MB
% 3.60/0.93 % (534120)Instructions burned: 31 (million)
% 3.60/0.93 % (534128)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=1242353246:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2997 on theBenchmark for (2997ds/143Mi)
% 3.60/0.93 % (534126)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=3638193822:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2997 on theBenchmark for (2997ds/20Mi)
% 3.60/0.93 % (534127)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=1010008591:i=1240:rtra=on:ixr=off_2997 on theBenchmark for (2997ds/1240Mi)
% 3.60/0.93 % (534094)Instruction limit reached!
% 3.60/0.93 % (534094)------------------------------
% 3.60/0.93 % (534094)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.60/0.93 % (534094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.60/0.93 % (534094)CaDiCaL version: 2.1.3
% 3.60/0.93 % (534094)Termination reason: Instruction limit
% 3.60/0.93 % (534094)Termination phase: Saturation
% 3.60/0.93 % (534094)Time elapsed: 0.178 s
% 3.60/0.93 % (534094)Peak memory usage: 13 MB
% 3.60/0.93 % (534094)Instructions burned: 250 (million)
% 3.60/0.93 % (534122)Instruction limit reached!
% 3.60/0.93 % (534122)------------------------------
% 3.60/0.93 % (534122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.60/0.93 % (534122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.60/0.93 % (534122)CaDiCaL version: 2.1.3
% 3.60/0.93 % (534122)Termination reason: Instruction limit
% 3.60/0.93 % (534122)Termination phase: Property scanning
% 3.60/0.93 % (534122)Time elapsed: 0.020 s
% 3.60/0.93 % (534122)Peak memory usage: 10 MB
% 3.60/0.93 % (534122)Instructions burned: 25 (million)
% 3.60/0.93 % (534126)Instruction limit reached!
% 3.60/0.93 % (534126)------------------------------
% 3.60/0.93 % (534126)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.60/0.93 % (534126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.60/0.93 % (534126)CaDiCaL version: 2.1.3
% 3.60/0.93 % (534126)Termination reason: Instruction limit
% 3.60/0.93 % (534126)Termination phase: Preprocessing 3
% 3.60/0.93 % (534126)Time elapsed: 0.018 s
% 3.60/0.93 % (534126)Peak memory usage: 11 MB
% 3.60/0.93 % (534126)Instructions burned: 21 (million)
% 3.60/0.93 % (534130)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=2597676041:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/193Mi)
% 3.60/0.93 % (534134)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3054823677:i=42:hud=10:rtra=on_2996 on theBenchmark for (2996ds/42Mi)
% 3.60/0.93 % (534135)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 3.60/0.93 % (534135)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1097771024:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2996 on theBenchmark for (2996ds/7Mi)
% 3.60/0.93 % (534137)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=3918384069:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/181Mi)
% 3.60/0.93 % (534135)Instruction limit reached!
% 3.60/0.93 % (534135)------------------------------
% 3.60/0.93 % (534135)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.60/0.93 % (534135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.60/0.93 % (534135)CaDiCaL version: 2.1.3
% 3.60/0.93 % (534135)Termination reason: Instruction limit
% 3.60/0.93 % (534135)Termination phase: shuffling
% 3.60/0.93 % (534135)Time elapsed: 0.006 s
% 3.60/0.93 % (534135)Peak memory usage: 9 MB
% 3.60/0.93 % (534135)Instructions burned: 7 (million)
% 3.60/0.93 % (534128)Instruction limit reached!
% 3.60/0.93 % (534128)------------------------------
% 3.60/0.93 % (534128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.60/0.93 % (534128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.60/1.04 % (534128)CaDiCaL version: 2.1.3
% 3.60/1.04 % (534128)Termination reason: Instruction limit
% 3.60/1.04 % (534128)Termination phase: Saturation
% 3.60/1.04 % (534128)Time elapsed: 0.067 s
% 3.60/1.04 % (534128)Peak memory usage: 13 MB
% 3.60/1.04 % (534128)Instructions burned: 144 (million)
% 3.60/1.04 % (534134)Instruction limit reached!
% 3.60/1.04 % (534134)------------------------------
% 3.60/1.04 % (534134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.60/1.04 % (534134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.60/1.04 % (534134)CaDiCaL version: 2.1.3
% 3.60/1.04 % (534134)Termination reason: Instruction limit
% 3.60/1.04 % (534134)Termination phase: Saturation
% 3.60/1.04 % (534134)Time elapsed: 0.035 s
% 3.60/1.04 % (534134)Peak memory usage: 12 MB
% 3.60/1.04 % (534134)Instructions burned: 42 (million)
% 3.60/1.04 % (534143)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=556905206: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)
% 3.60/1.04 % (534144)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 3.60/1.04 % (534144)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=2522479511:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2996 on theBenchmark for (2996ds/6Mi)
% 3.60/1.04 % (534144)Instruction limit reached!
% 3.60/1.04 % (534144)------------------------------
% 3.60/1.04 % (534144)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.60/1.04 % (534144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.60/1.04 % (534144)CaDiCaL version: 2.1.3
% 3.60/1.04 % (534144)Termination reason: Instruction limit
% 3.60/1.04 % (534144)Termination phase: shuffling
% 3.60/1.04 % (534144)Time elapsed: 0.005 s
% 3.60/1.04 % (534144)Peak memory usage: 10 MB
% 3.60/1.04 % (534144)Instructions burned: 6 (million)
% 3.60/1.04 % (534143)Refutation not found, incomplete strategy
% 3.60/1.04 % (534143)------------------------------
% 3.60/1.04 % (534143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.60/1.04 % (534143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.60/1.04 % (534143)CaDiCaL version: 2.1.3
% 3.60/1.04 % (534143)Termination reason: Refutation not found, incomplete strategy
% 3.60/1.04 % (534143)Time elapsed: 0.027 s
% 3.60/1.04 % (534143)Peak memory usage: 13 MB
% 3.60/1.04 % (534143)Instructions burned: 50 (million)
% 3.60/1.04 % (534143)------------------------------
% 3.60/1.04 % (534143)------------------------------
% 3.60/1.04 % (534145)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=271748763:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2996 on theBenchmark for (2996ds/22Mi)
% 3.60/1.04 % (534150)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=3646365681:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/316Mi)
% 3.60/1.04 % (534145)Instruction limit reached!
% 3.60/1.04 % (534145)------------------------------
% 3.60/1.04 % (534145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.60/1.04 % (534145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.60/1.04 % (534145)CaDiCaL version: 2.1.3
% 3.60/1.04 % (534145)Termination reason: Instruction limit
% 3.60/1.04 % (534145)Termination phase: Property scanning
% 3.60/1.04 % (534145)Time elapsed: 0.019 s
% 3.60/1.04 % (534145)Peak memory usage: 11 MB
% 3.60/1.04 % (534145)Instructions burned: 22 (million)
% 3.60/1.04 % (534149)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=3998184086:i=19:add=on:rtra=on_2995 on theBenchmark for (2995ds/19Mi)
% 3.60/1.04 % (534149)Instruction limit reached!
% 3.60/1.04 % (534149)------------------------------
% 3.60/1.04 % (534149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.60/1.04 % (534149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.60/1.04 % (534149)CaDiCaL version: 2.1.3
% 3.60/1.04 % (534149)Termination reason: Instruction limit
% 3.60/1.04 % (534149)Termination phase: Property scanning
% 3.60/1.04 % (534149)Time elapsed: 0.016 s
% 3.60/1.04 % (534149)Peak memory usage: 10 MB
% 6.05/1.21 % (534149)Instructions burned: 19 (million)
% 6.05/1.21 % (534153)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=756539144:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2995 on theBenchmark for (2995ds/853Mi)
% 6.05/1.21 % (534156)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=4230899170: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)
% 6.05/1.21 % (534130)Instruction limit reached!
% 6.05/1.21 % (534130)------------------------------
% 6.05/1.21 % (534130)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.05/1.21 % (534130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.21 % (534130)CaDiCaL version: 2.1.3
% 6.05/1.21 % (534130)Termination reason: Instruction limit
% 6.05/1.21 % (534130)Termination phase: Saturation
% 6.05/1.21 % (534130)Time elapsed: 0.167 s
% 6.05/1.21 % (534130)Peak memory usage: 13 MB
% 6.05/1.21 % (534130)Instructions burned: 193 (million)
% 6.05/1.21 % (534156)Instruction limit reached!
% 6.05/1.21 % (534156)------------------------------
% 6.05/1.21 % (534156)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.05/1.21 % (534156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.21 % (534156)CaDiCaL version: 2.1.3
% 6.05/1.21 % (534156)Termination reason: Instruction limit
% 6.05/1.21 % (534156)Termination phase: Saturation
% 6.05/1.21 % (534156)Time elapsed: 0.034 s
% 6.05/1.21 % (534156)Peak memory usage: 12 MB
% 6.05/1.21 % (534156)Instructions burned: 45 (million)
% 6.05/1.21 % (534137)Instruction limit reached!
% 6.05/1.21 % (534137)------------------------------
% 6.05/1.21 % (534137)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.05/1.21 % (534137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.21 % (534137)CaDiCaL version: 2.1.3
% 6.05/1.21 % (534137)Termination reason: Instruction limit
% 6.05/1.21 % (534137)Termination phase: Saturation
% 6.05/1.21 % (534137)Time elapsed: 0.161 s
% 6.05/1.21 % (534137)Peak memory usage: 14 MB
% 6.05/1.21 % (534137)Instructions burned: 182 (million)
% 6.05/1.21 % (534159)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=1102123466:i=480:rtra=on_2994 on theBenchmark for (2994ds/480Mi)
% 6.05/1.21 % (534162)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 6.05/1.21 % (534162)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=973737030:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/200Mi)
% 6.05/1.21 % (534161)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=977515086:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2994 on theBenchmark for (2994ds/21Mi)
% 6.05/1.21 % (534161)Instruction limit reached!
% 6.05/1.21 % (534161)------------------------------
% 6.05/1.21 % (534161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.05/1.21 % (534161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.21 % (534161)CaDiCaL version: 2.1.3
% 6.05/1.21 % (534161)Termination reason: Instruction limit
% 6.05/1.21 % (534161)Termination phase: Property scanning
% 6.05/1.21 % (534161)Time elapsed: 0.019 s
% 6.05/1.21 % (534161)Peak memory usage: 11 MB
% 6.05/1.21 % (534161)Instructions burned: 22 (million)
% 6.05/1.21 % (534066)Instruction limit reached!
% 6.05/1.21 % (534066)------------------------------
% 6.05/1.21 % (534066)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.05/1.21 % (534066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.21 % (534066)CaDiCaL version: 2.1.3
% 6.05/1.21 % (534066)Termination reason: Instruction limit
% 6.05/1.21 % (534066)Termination phase: Saturation
% 6.05/1.21 % (534066)Time elapsed: 0.549 s
% 6.05/1.21 % (534066)Peak memory usage: 15 MB
% 6.05/1.21 % (534066)Instructions burned: 634 (million)
% 6.05/1.21 % (534169)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=1627433028:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2994 on theBenchmark for (2994ds/13Mi)
% 6.05/1.21 % (534169)Instruction limit reached!
% 6.05/1.21 % (534169)------------------------------
% 6.05/1.21 % (534169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.05/1.21 % (534169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.21 % (534169)CaDiCaL version: 2.1.3
% 6.05/1.21 % (534169)Termination reason: Instruction limit
% 6.05/1.21 % (534169)Termination phase: SInE selection
% 6.05/1.21 % (534169)Time elapsed: 0.011 s
% 6.05/1.21 % (534169)Peak memory usage: 10 MB
% 6.05/1.21 % (534169)Instructions burned: 13 (million)
% 6.05/1.21 % (534170)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=1400256113:i=66:s2at=3:nm=2:rtra=on:rawr=on_2994 on theBenchmark for (2994ds/66Mi)
% 6.05/1.21 % (534173)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=3448560087:i=51:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/51Mi)
% 6.05/1.21 % (534162)Instruction limit reached!
% 6.05/1.21 % (534162)------------------------------
% 6.05/1.21 % (534162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.05/1.21 % (534162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.21 % (534162)CaDiCaL version: 2.1.3
% 6.05/1.21 % (534162)Termination reason: Instruction limit
% 6.05/1.21 % (534162)Termination phase: Saturation
% 6.05/1.21 % (534162)Time elapsed: 0.106 s
% 6.05/1.21 % (534162)Peak memory usage: 13 MB
% 6.05/1.21 % (534162)Instructions burned: 200 (million)
% 6.05/1.21 % (534170)Instruction limit reached!
% 6.05/1.21 % (534170)------------------------------
% 6.05/1.21 % (534170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.05/1.21 % (534170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.21 % (534170)CaDiCaL version: 2.1.3
% 6.05/1.21 % (534170)Termination reason: Instruction limit
% 6.05/1.21 % (534170)Termination phase: Saturation
% 6.05/1.21 % (534170)Time elapsed: 0.053 s
% 6.05/1.21 % (534170)Peak memory usage: 12 MB
% 6.05/1.21 % (534170)Instructions burned: 67 (million)
% 6.05/1.21 % (534175)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=3367282103:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/31Mi)
% 6.05/1.21 % (534176)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=3131985089:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2993 on theBenchmark for (2993ds/137Mi)
% 6.05/1.21 % (534173)Instruction limit reached!
% 6.05/1.21 % (534173)------------------------------
% 6.05/1.21 % (534173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.05/1.21 % (534173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.21 % (534173)CaDiCaL version: 2.1.3
% 6.05/1.21 % (534173)Termination reason: Instruction limit
% 6.05/1.21 % (534173)Termination phase: Saturation
% 6.05/1.21 % (534173)Time elapsed: 0.044 s
% 6.05/1.21 % (534173)Peak memory usage: 12 MB
% 6.05/1.21 % (534173)Instructions burned: 51 (million)
% 6.05/1.21 % (534175)Instruction limit reached!
% 6.05/1.21 % (534175)------------------------------
% 6.05/1.21 % (534175)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.05/1.21 % (534175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.21 % (534175)CaDiCaL version: 2.1.3
% 6.05/1.21 % (534175)Termination reason: Instruction limit
% 6.05/1.21 % (534175)Termination phase: Property scanning
% 6.05/1.21 % (534175)Time elapsed: 0.028 s
% 6.05/1.21 % (534175)Peak memory usage: 10 MB
% 6.05/1.21 % (534175)Instructions burned: 31 (million)
% 6.05/1.21 % (534150)Instruction limit reached!
% 6.05/1.21 % (534150)------------------------------
% 6.05/1.21 % (534150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.05/1.21 % (534150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.21 % (534150)CaDiCaL version: 2.1.3
% 6.05/1.21 % (534150)Termination reason: Instruction limit
% 6.05/1.21 % (534150)Termination phase: Saturation
% 6.05/1.21 % (534150)Time elapsed: 0.269 s
% 6.05/1.21 % (534150)Peak memory usage: 15 MB
% 6.05/1.21 % (534150)Instructions burned: 316 (million)
% 6.05/1.21 % (534179)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=4253221776:cond=on:i=34:hud=10:nm=10:rtra=on_2993 on theBenchmark for (2993ds/34Mi)
% 6.05/1.21 % (534179)Instruction limit reached!
% 6.05/1.21 % (534179)------------------------------
% 6.05/1.21 % (534179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.05/1.21 % (534179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.21 % (534179)CaDiCaL version: 2.1.3
% 6.05/1.21 % (534179)Termination reason: Instruction limit
% 6.05/1.21 % (534179)Termination phase: Function definition elimination
% 6.05/1.21 % (534179)Time elapsed: 0.016 s
% 6.05/1.21 % (534179)Peak memory usage: 10 MB
% 6.05/1.21 % (534179)Instructions burned: 34 (million)
% 6.05/1.21 % (534181)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 6.05/1.21 % (534180)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=2583812886:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2992 on theBenchmark for (2992ds/67Mi)
% 6.05/1.21 % (534181)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=1381345960:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2992 on theBenchmark for (2992ds/180Mi)
% 6.05/1.21 % (534183)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=853397090:st=2:i=246:sd=3:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/246Mi)
% 6.05/1.21 % (534180)Instruction limit reached!
% 6.05/1.21 % (534180)------------------------------
% 6.05/1.21 % (534180)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.05/1.21 % (534180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.21 % (534180)CaDiCaL version: 2.1.3
% 6.05/1.21 % (534180)Termination reason: Instruction limit
% 6.05/1.21 % (534180)Termination phase: Saturation
% 6.05/1.21 % (534180)Time elapsed: 0.040 s
% 6.05/1.21 % (534180)Peak memory usage: 13 MB
% 6.05/1.21 % (534180)Instructions burned: 69 (million)
% 6.05/1.21 % (534188)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=1556352826:cond=on:i=96:bd=all:rtra=on_2992 on theBenchmark for (2992ds/96Mi)
% 6.05/1.21 % (534176)Instruction limit reached!
% 6.05/1.21 % (534176)------------------------------
% 6.05/1.21 % (534176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.05/1.21 % (534176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.21 % (534176)CaDiCaL version: 2.1.3
% 6.05/1.21 % (534176)Termination reason: Instruction limit
% 6.05/1.21 % (534176)Termination phase: Saturation
% 6.05/1.21 % (534176)Time elapsed: 0.135 s
% 6.05/1.21 % (534176)Peak memory usage: 13 MB
% 6.05/1.21 % (534176)Instructions burned: 137 (million)
% 6.05/1.21 % (534191)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=1948888002:i=427:sd=1:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/427Mi)
% 6.05/1.21 % (534188)Instruction limit reached!
% 6.05/1.21 % (534188)------------------------------
% 6.05/1.21 % (534188)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.05/1.21 % (534188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.21 % (534188)CaDiCaL version: 2.1.3
% 6.05/1.21 % (534188)Termination reason: Instruction limit
% 6.05/1.21 % (534188)Termination phase: Saturation
% 6.05/1.21 % (534188)Time elapsed: 0.063 s
% 6.05/1.21 % (534188)Peak memory usage: 13 MB
% 6.05/1.21 % (534188)Instructions burned: 96 (million)
% 6.05/1.21 % (534159)Instruction limit reached!
% 6.05/1.21 % (534159)------------------------------
% 6.05/1.21 % (534159)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.05/1.21 % (534159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.21 % (534159)CaDiCaL version: 2.1.3
% 6.05/1.21 % (534159)Termination reason: Instruction limit
% 6.05/1.21 % (534159)Termination phase: Saturation
% 6.05/1.21 % (534159)Time elapsed: 0.331 s
% 6.05/1.21 % (534159)Peak memory usage: 13 MB
% 6.05/1.21 % (534159)Instructions burned: 480 (million)
% 6.05/1.21 % (534193)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=3454404924:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/874Mi)
% 6.05/1.21 % (534191) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-534056-534191"...
% 6.05/1.21 % (534191)...printing done.
% 6.05/1.21 % (534191)Refutation found. Thanks to Tanya!
% 6.05/1.21 % SZS status Theorem for theBenchmark
% 6.05/1.21 % SZS output start Proof for theBenchmark
% 6.05/1.21 thf(type_def_5, type, x_a: $tType).
% 6.05/1.21 thf(type_def_6, type, com: $tType).
% 6.05/1.21 thf(type_def_7, type, state: $tType).
% 6.05/1.21 thf(type_def_8, type, hoare_669141180iple_a: $tType).
% 6.05/1.21 thf(type_def_9, type, sTfun: ($tType * $tType) > $tType).
% 6.05/1.21 thf(func_def_0, type, skip: com).
% 6.05/1.21 thf(func_def_1, type, semi: (com > com > com)).
% 6.05/1.21 thf(func_def_2, type, ex: ((hoare_669141180iple_a > $o) > $o)).
% 6.05/1.21 thf(func_def_3, type, finite957651855iple_a: ((hoare_669141180iple_a > $o) > $o)).
% 6.05/1.21 thf(func_def_4, type, finite840267660iple_a: ((hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a) > (hoare_669141180iple_a > $o) > hoare_669141180iple_a > $o)).
% 6.05/1.21 thf(func_def_5, type, finite684844060iple_a: ((hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a) > (hoare_669141180iple_a > $o) > hoare_669141180iple_a)).
% 6.05/1.21 thf(func_def_6, type, finite590756294iple_a: ((hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a) > hoare_669141180iple_a > (hoare_669141180iple_a > $o) > hoare_669141180iple_a > $o)).
% 6.05/1.21 thf(func_def_7, type, finite972428089iple_a: ((hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a) > ((hoare_669141180iple_a > $o) > hoare_669141180iple_a) > $o)).
% 6.05/1.21 thf(func_def_8, type, finite252461622iple_a: ((hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a) > ((hoare_669141180iple_a > $o) > hoare_669141180iple_a) > $o)).
% 6.05/1.21 thf(func_def_9, type, the_Ho49089901iple_a: ((hoare_669141180iple_a > $o) > hoare_669141180iple_a)).
% 6.05/1.21 thf(func_def_10, type, hoare_2128652938rivs_a: ((hoare_669141180iple_a > $o) > (hoare_669141180iple_a > $o) > $o)).
% 6.05/1.21 thf(func_def_11, type, hoare_1295064928iple_a: ((x_a > state > $o) > com > (x_a > state > $o) > hoare_669141180iple_a)).
% 6.05/1.21 thf(func_def_12, type, bot_bo280939947le_a_o: (hoare_669141180iple_a > $o)).
% 6.05/1.21 thf(func_def_13, type, bot_bot_o: $o).
% 6.05/1.21 thf(func_def_14, type, collec1717965009iple_a: ((hoare_669141180iple_a > $o) > hoare_669141180iple_a > $o)).
% 6.05/1.21 thf(func_def_15, type, insert175534902iple_a: (hoare_669141180iple_a > (hoare_669141180iple_a > $o) > hoare_669141180iple_a > $o)).
% 6.05/1.21 thf(func_def_16, type, the_el738790235iple_a: ((hoare_669141180iple_a > $o) > hoare_669141180iple_a)).
% 6.05/1.21 thf(func_def_17, type, fequal182287803iple_a: (hoare_669141180iple_a > hoare_669141180iple_a > $o)).
% 6.05/1.21 thf(func_def_18, type, member1016246415iple_a: (hoare_669141180iple_a > (hoare_669141180iple_a > $o) > $o)).
% 6.05/1.21 thf(func_def_19, type, g: (hoare_669141180iple_a > $o)).
% 6.05/1.21 thf(func_def_20, type, p: (x_a > state > $o)).
% 6.05/1.21 thf(func_def_21, type, b: (state > $o)).
% 6.05/1.21 thf(func_def_22, type, c: com).
% 6.05/1.21 thf(func_def_24, type, vAND: ($o > $o > $o)).
% 6.05/1.21 thf(func_def_25, type, vIMP: ($o > $o > $o)).
% 6.05/1.21 thf(func_def_26, type, vNOT: ($o > $o)).
% 6.05/1.21 thf(func_def_27, type, vOR: ($o > $o > $o)).
% 6.05/1.21 thf(func_def_30, type, db1: !>[X0: $tType]:(X0)).
% 6.05/1.21 thf(func_def_31, type, db0: !>[X0: $tType]:(X0)).
% 6.05/1.21 thf(func_def_32, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 6.05/1.21 thf(func_def_33, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 6.05/1.21 thf(func_def_34, type, sK0: ((x_a > state > $o) > (x_a > state > $o) > (x_a > state > $o) > (x_a > state > $o) > state)).
% 6.05/1.21 thf(func_def_35, type, sK1: ((x_a > state > $o) > (x_a > state > $o) > (x_a > state > $o) > (x_a > state > $o) > x_a)).
% 6.05/1.21 thf(func_def_36, type, sK2: ((x_a > state > $o) > (x_a > state > $o) > (x_a > state > $o) > (x_a > state > $o) > state)).
% 6.05/1.21 thf(func_def_37, type, sK3: ((x_a > state > $o) > (x_a > state > $o) > x_a)).
% 6.05/1.21 thf(func_def_38, type, sK4: ((x_a > state > $o) > (x_a > state > $o) > state)).
% 6.05/1.21 thf(func_def_39, type, sK5: ((x_a > state > $o) > (x_a > state > $o) > state)).
% 6.05/1.21 thf(func_def_40, type, sK6: ((x_a > state > $o) > (x_a > state > $o) > x_a)).
% 6.05/1.21 thf(func_def_41, type, sK7: (hoare_669141180iple_a > x_a > state > $o)).
% 6.05/1.21 thf(func_def_42, type, sK8: (hoare_669141180iple_a > x_a > state > $o)).
% 6.05/1.21 thf(func_def_43, type, sK9: (hoare_669141180iple_a > com)).
% 6.05/1.21 thf(func_def_44, type, sK10: ((x_a > state > $o) > (x_a > state > $o) > com > (hoare_669141180iple_a > $o) > state)).
% 6.05/1.21 thf(func_def_45, type, sK11: ((x_a > state > $o) > (x_a > state > $o) > com > (hoare_669141180iple_a > $o) > x_a)).
% 6.05/1.21 thf(func_def_46, type, sK12: ((x_a > state > $o) > (x_a > state > $o) > (x_a > state > $o) > (x_a > state > $o) > com > (hoare_669141180iple_a > $o) > state)).
% 6.05/1.21 thf(func_def_47, type, db2: !>[X0: $tType]:(X0)).
% 6.05/1.21 thf(func_def_48, type, db3: !>[X0: $tType]:(X0)).
% 6.05/1.21 thf(f23,axiom,(
% 6.05/1.21 (bot_bo280939947le_a_o = ((collec1717965009iple_a @ (^[X0 : hoare_669141180iple_a] : ($false)))))),
% 6.05/1.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_22_empty__def)).
% 6.05/1.21 thf(f61,axiom,(
% 6.05/1.21 ! [X3 : (x_a > state > $o),X2 : com,X1 : (hoare_669141180iple_a > $o),X0 : (x_a > state > $o)] : (! [X5 : state,X4 : x_a] : ((X3 @ X4 @ X5) => ? [X6 : (x_a > state > $o),X7 : (x_a > state > $o)] : ((hoare_2128652938rivs_a @ X1 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X6 @ X2 @ X7) @ bot_bo280939947le_a_o)) & ! [X8 : state] : (! [X9 : x_a] : ((X6 @ X9 @ X5) => (X7 @ X9 @ X8)) => (X0 @ X4 @ X8)))) => (hoare_2128652938rivs_a @ X1 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X3 @ X2 @ X0) @ bot_bo280939947le_a_o)))),
% 6.05/1.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_60_conseq)).
% 6.05/1.21 thf(f98,conjecture,(
% 6.05/1.21 (hoare_2128652938rivs_a @ g @ (insert175534902iple_a @ (hoare_1295064928iple_a @ (^[X0 : x_a, X1 : state] : ($false)) @ c @ (^[X0 : x_a, X1 : state] : (((p @ X0 @ X1) & (~ (b @ X1)))))) @ bot_bo280939947le_a_o))),
% 6.05/1.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0)).
% 6.05/1.21 thf(f99,negated_conjecture,(
% 6.05/1.21 ~(hoare_2128652938rivs_a @ g @ (insert175534902iple_a @ (hoare_1295064928iple_a @ (^[X0 : x_a, X1 : state] : ($false)) @ c @ (^[X0 : x_a, X1 : state] : (((p @ X0 @ X1) & (~ (b @ X1)))))) @ bot_bo280939947le_a_o))),
% 6.05/1.21 inference(negated_conjecture,[status(cth)],[f98])).
% 6.05/1.21 thf(f140,plain,(
% 6.05/1.21 ~(hoare_2128652938rivs_a @ g @ (insert175534902iple_a @ (hoare_1295064928iple_a @ (^[X0 : x_a, X1 : state] : ($false)) @ c @ (^[X2 : x_a, X3 : state] : (((p @ X2 @ X3) & (~ (b @ X3)))))) @ bot_bo280939947le_a_o))),
% 6.05/1.21 inference(rectify,[],[f99])).
% 6.05/1.21 thf(f141,plain,(
% 6.05/1.21 ~ (((hoare_2128652938rivs_a @ g @ (insert175534902iple_a @ (hoare_1295064928iple_a @ (^[Y0 : x_a]: ((^[Y1 : state]: ($false)))) @ c @ (^[Y0 : x_a]: ((^[Y1 : state]: ((p @ Y0 @ Y1) & (~ (b @ Y1))))))) @ bot_bo280939947le_a_o))) = $true)),
% 6.05/1.21 inference(fool_elimination,[],[f140])).
% 6.05/1.21 thf(f142,plain,(
% 6.05/1.21 ! [X0 : (x_a > state > $o),X1 : com,X2 : (hoare_669141180iple_a > $o),X3 : (x_a > state > $o)] : (! [X4 : state,X5 : x_a] : ((X0 @ X5 @ X4) => ? [X6 : (x_a > state > $o),X7 : (x_a > state > $o)] : ((hoare_2128652938rivs_a @ X2 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X6 @ X1 @ X7) @ bot_bo280939947le_a_o)) & ! [X8 : state] : (! [X9 : x_a] : ((X6 @ X9 @ X4) => (X7 @ X9 @ X8)) => (X3 @ X5 @ X8)))) => (hoare_2128652938rivs_a @ X2 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X0 @ X1 @ X3) @ bot_bo280939947le_a_o)))),
% 6.05/1.21 inference(rectify,[],[f61])).
% 6.05/1.21 thf(f143,plain,(
% 6.05/1.21 ! [X2 : (hoare_669141180iple_a > $o),X0 : (x_a > state > $o),X1 : com,X3 : (x_a > state > $o)] : (! [X4 : state,X5 : x_a] : ((((X0 @ X5 @ X4)) = $true) => ? [X7 : (x_a > state > $o),X6 : (x_a > state > $o)] : ((((hoare_2128652938rivs_a @ X2 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X6 @ X1 @ X7) @ bot_bo280939947le_a_o))) = $true) & ! [X8 : state] : (! [X9 : x_a] : ((((X6 @ X9 @ X4)) = $true) => (((X7 @ X9 @ X8)) = $true)) => (((X3 @ X5 @ X8)) = $true)))) => (((hoare_2128652938rivs_a @ X2 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X0 @ X1 @ X3) @ bot_bo280939947le_a_o))) = $true))),
% 6.05/1.21 inference(fool_elimination,[],[f142])).
% 6.05/1.21 thf(f258,plain,(
% 6.05/1.21 (bot_bo280939947le_a_o = ((collec1717965009iple_a @ (^[X0 : hoare_669141180iple_a] : ($false)))))),
% 6.05/1.21 inference(rectify,[],[f23])).
% 6.05/1.21 thf(f259,plain,(
% 6.05/1.21 (bot_bo280939947le_a_o = ((collec1717965009iple_a @ (^[Y0 : hoare_669141180iple_a]: ($false)))))),
% 6.05/1.21 inference(fool_elimination,[],[f258])).
% 6.05/1.21 thf(f260,plain,(
% 6.05/1.21 (((hoare_2128652938rivs_a @ g @ (insert175534902iple_a @ (hoare_1295064928iple_a @ (^[Y0 : x_a]: ((^[Y1 : state]: ($false)))) @ c @ (^[Y0 : x_a]: ((^[Y1 : state]: ((p @ Y0 @ Y1) & (~ (b @ Y1))))))) @ bot_bo280939947le_a_o))) != $true)),
% 6.05/1.21 inference(flattening,[],[f141])).
% 6.05/1.21 thf(f268,plain,(
% 6.05/1.21 ! [X2 : (hoare_669141180iple_a > $o),X1 : com,X0 : (x_a > state > $o),X3 : (x_a > state > $o)] : ((((hoare_2128652938rivs_a @ X2 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X0 @ X1 @ X3) @ bot_bo280939947le_a_o))) = $true) | ? [X4 : state,X5 : x_a] : (! [X7 : (x_a > state > $o),X6 : (x_a > state > $o)] : ((((hoare_2128652938rivs_a @ X2 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X6 @ X1 @ X7) @ bot_bo280939947le_a_o))) != $true) | ? [X8 : state] : (! [X9 : x_a] : ((((X6 @ X9 @ X4)) != $true) | (((X7 @ X9 @ X8)) = $true)) & (((X3 @ X5 @ X8)) != $true))) & (((X0 @ X5 @ X4)) = $true)))),
% 6.05/1.21 inference(ennf_transformation,[],[f143])).
% 6.05/1.21 thf(f295,plain,(
% 6.05/1.21 ! [X0 : (hoare_669141180iple_a > $o),X1 : com,X2 : (x_a > state > $o),X3 : (x_a > state > $o)] : ((((hoare_2128652938rivs_a @ X0 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X2 @ X1 @ X3) @ bot_bo280939947le_a_o))) = $true) | ? [X4 : state,X5 : x_a] : (! [X6 : (x_a > state > $o),X7 : (x_a > state > $o)] : ((((hoare_2128652938rivs_a @ X0 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X7 @ X1 @ X6) @ bot_bo280939947le_a_o))) != $true) | ? [X8 : state] : (! [X9 : x_a] : ((((X7 @ X9 @ X4)) != $true) | (((X6 @ X9 @ X8)) = $true)) & (((X3 @ X5 @ X8)) != $true))) & ($true = ((X2 @ X5 @ X4)))))),
% 6.05/1.21 inference(rectify,[],[f268])).
% 6.05/1.21 thf(f296,plain,(
% 6.05/1.21 ! [X0 : (hoare_669141180iple_a > $o),X1 : com,X2 : (x_a > state > $o),X3 : (x_a > state > $o)] : ((((hoare_2128652938rivs_a @ X0 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X2 @ X1 @ X3) @ bot_bo280939947le_a_o))) = $true) | (! [X6 : (x_a > state > $o),X7 : (x_a > state > $o)] : ((((hoare_2128652938rivs_a @ X0 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X7 @ X1 @ X6) @ bot_bo280939947le_a_o))) != $true) | (! [X9 : x_a] : (($true != ((X7 @ X9 @ (sK10 @ X3 @ X2 @ X1 @ X0)))) | (((X6 @ X9 @ (sK12 @ X7 @ X6 @ X3 @ X2 @ X1 @ X0))) = $true)) & (((X3 @ (sK11 @ X3 @ X2 @ X1 @ X0) @ (sK12 @ X7 @ X6 @ X3 @ X2 @ X1 @ X0))) != $true))) & (((X2 @ (sK11 @ X3 @ X2 @ X1 @ X0) @ (sK10 @ X3 @ X2 @ X1 @ X0))) = $true)))),
% 6.05/1.21 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP,vAPP,vAPP]),skolemize(X8,sK2 @ X5 @ X4 @ X3 @ X1),skolemize(X8,sK2 @ X5 @ X4 @ X3 @ X1),skolemize(X8,sK2 @ X5 @ X4 @ X3 @ X1)],[f295])).
% 6.05/1.21 thf(f307,plain,(
% 6.05/1.21 (bot_bo280939947le_a_o = ((collec1717965009iple_a @ (^[Y0 : hoare_669141180iple_a]: ($false)))))),
% 6.05/1.21 inference(cnf_transformation,[],[f259])).
% 6.05/1.21 thf(f323,plain,(
% 6.05/1.21 ( ! [X2 : (x_a > state > $o),X3 : (x_a > state > $o),X0 : (hoare_669141180iple_a > $o),X1 : com] : ((((hoare_2128652938rivs_a @ X0 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X2 @ X1 @ X3) @ bot_bo280939947le_a_o))) = $true) | (((X2 @ (sK11 @ X3 @ X2 @ X1 @ X0) @ (sK10 @ X3 @ X2 @ X1 @ X0))) = $true)) )),
% 6.05/1.21 inference(cnf_transformation,[],[f296])).
% 6.05/1.21 thf(f343,plain,(
% 6.05/1.21 (((hoare_2128652938rivs_a @ g @ (insert175534902iple_a @ (hoare_1295064928iple_a @ (^[Y0 : x_a]: ((^[Y1 : state]: ($false)))) @ c @ (^[Y0 : x_a]: ((^[Y1 : state]: ((p @ Y0 @ Y1) & (~ (b @ Y1))))))) @ bot_bo280939947le_a_o))) != $true)),
% 6.05/1.21 inference(cnf_transformation,[],[f260])).
% 6.05/1.21 thf(f363,plain,(
% 6.05/1.21 ( ! [X2 : (x_a > state > $o),X3 : (x_a > state > $o),X0 : (hoare_669141180iple_a > $o),X1 : com] : ((((X2 @ (sK11 @ X3 @ X2 @ X1 @ X0) @ (sK10 @ X3 @ X2 @ X1 @ X0))) = $true) | (((hoare_2128652938rivs_a @ X0 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X2 @ X1 @ X3) @ (collec1717965009iple_a @ (^[Y0 : hoare_669141180iple_a]: ($false)))))) = $true)) )),
% 6.05/1.21 inference(definition_unfolding,[],[f323,f307])).
% 6.05/1.21 thf(f378,plain,(
% 6.05/1.21 ($true != ((hoare_2128652938rivs_a @ g @ (insert175534902iple_a @ (hoare_1295064928iple_a @ (^[Y0 : x_a]: ((^[Y1 : state]: ($false)))) @ c @ (^[Y0 : x_a]: ((^[Y1 : state]: ((p @ Y0 @ Y1) & (~ (b @ Y1))))))) @ (collec1717965009iple_a @ (^[Y0 : hoare_669141180iple_a]: ($false)))))))),
% 6.05/1.21 inference(definition_unfolding,[],[f343,f307])).
% 6.05/1.21 thf(f389,plain,(
% 6.05/1.21 ((((^[Y0 : x_a]: ((^[Y1 : state]: ($false)))) @ (sK11 @ (^[Y0 : x_a]: ((^[Y1 : state]: ((p @ Y0 @ Y1) & (~ (b @ Y1)))))) @ (^[Y0 : x_a]: ((^[Y1 : state]: ($false)))) @ c @ g) @ (sK10 @ (^[Y0 : x_a]: ((^[Y1 : state]: ((p @ Y0 @ Y1) & (~ (b @ Y1)))))) @ (^[Y0 : x_a]: ((^[Y1 : state]: ($false)))) @ c @ g))) = $true)),
% 6.05/1.21 inference(unit_resulting_resolution,[],[f363,f378])).
% 6.05/1.21 thf(f397,plain,(
% 6.05/1.21 ($true = $false)),
% 6.05/1.21 inference(beta-eta_normalization,[],[f389])).
% 6.05/1.21 thf(f398,plain,(
% 6.05/1.21 $false),
% 6.05/1.21 inference(trivial_inequality_removal,[],[f397])).
% 6.05/1.21 % SZS output end Proof for theBenchmark
% 6.05/1.21 % (534191)------------------------------
% 6.05/1.21 % (534191)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.05/1.21 % (534191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.21 % (534191)CaDiCaL version: 2.1.3
% 6.05/1.21 % (534191)Termination reason: Refutation
% 6.05/1.21 % (534191)Time elapsed: 0.033 s
% 6.05/1.21 % (534191)Peak memory usage: 13 MB
% 6.05/1.21 % (534191)Instructions burned: 37 (million)
% 6.05/1.21 % (534056)Success in time 0.905 s
% 6.05/1.21 % Vampire exiting
%------------------------------------------------------------------------------