%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP060^2 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:08:10 AM UTC 2026
% Result : Theorem 4.67s 1.06s
% Output : Refutation 4.67s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP060^2 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.25 % Computer : n010.cluster.edu
% 0.12/0.25 % Model : x86_64 x86_64
% 0.12/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.25 % Memory : 8046.5625MB
% 0.12/0.25 % OS : Linux 6.8.0-71-generic
% 0.12/0.25 % CPULimit : 300
% 0.12/0.25 % WCLimit : 300
% 0.12/0.25 % DateTime : Tue Sep 29 19:45:18 UTC 2026
% 0.12/0.25 % CPUTime :
% 0.12/0.25 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.25/0.31 Running higher-order theorem proving
% 0.25/0.36 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.78/0.58 % (3319011)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.78/0.58 % (3319018)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=3377201435:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.78/0.58 % (3319016)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=1836583640:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.78/0.58 % (3319018)Instruction limit reached!
% 0.78/0.58 % (3319018)------------------------------
% 0.78/0.58 % (3319018)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.58 % (3319018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.58 % (3319018)CaDiCaL version: 2.1.3
% 0.78/0.58 % (3319018)Termination reason: Instruction limit
% 0.78/0.58 % (3319018)Termination phase: shuffling
% 0.78/0.58 % (3319018)Time elapsed: 0.002 s
% 0.78/0.58 % (3319018)Peak memory usage: 10 MB
% 0.78/0.58 % (3319018)Instructions burned: 5 (million)
% 0.78/0.58 % (3319022)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.78/0.58 % (3319022)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.78/0.58 % (3319017)lrs+10_16_si=on:nwc=1.5:random_seed=4137642813:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.78/0.58 % (3319021)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=2061312573:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.78/0.58 % (3319022)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=1413696870:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.78/0.58 % (3319019)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=384489534: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.78/0.58 % (3319020)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=1704880029:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.78/0.58 % (3319025)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=972002845:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.78/0.58 % (3319025)Instruction limit reached!
% 0.78/0.58 % (3319025)------------------------------
% 0.78/0.58 % (3319025)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.58 % (3319025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.58 % (3319025)CaDiCaL version: 2.1.3
% 0.78/0.58 % (3319025)Termination reason: Instruction limit
% 0.78/0.58 % (3319025)Termination phase: shuffling
% 0.78/0.58 % (3319025)Time elapsed: 0.001 s
% 0.78/0.58 % (3319025)Peak memory usage: 10 MB
% 0.78/0.58 % (3319025)Instructions burned: 2 (million)
% 0.78/0.58 % (3319017)Instruction limit reached!
% 0.78/0.58 % (3319017)------------------------------
% 0.78/0.58 % (3319017)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.58 % (3319017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.58 % (3319017)CaDiCaL version: 2.1.3
% 0.78/0.58 % (3319017)Termination reason: Instruction limit
% 0.78/0.58 % (3319017)Termination phase: Property scanning
% 0.78/0.58 % (3319017)Time elapsed: 0.014 s
% 0.78/0.58 % (3319017)Peak memory usage: 10 MB
% 0.78/0.58 % (3319017)Instructions burned: 19 (million)
% 0.78/0.58 % (3319020)Instruction limit reached!
% 0.78/0.58 % (3319020)------------------------------
% 0.78/0.58 % (3319020)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.78/0.58 % (3319020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.78/0.58 % (3319020)CaDiCaL version: 2.1.3
% 0.78/0.58 % (3319020)Termination reason: Instruction limit
% 0.78/0.58 % (3319020)Termination phase: Property scanning
% 0.78/0.58 % (3319020)Time elapsed: 0.022 s
% 0.78/0.58 % (3319020)Peak memory usage: 10 MB
% 0.78/0.58 % (3319020)Instructions burned: 26 (million)
% 0.78/0.58 % (3319032)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=2722986222:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 1.51/0.64 % (3319032)Instruction limit reached!
% 1.51/0.64 % (3319032)------------------------------
% 1.51/0.64 % (3319032)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.51/0.64 % (3319032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.64 % (3319032)CaDiCaL version: 2.1.3
% 1.51/0.64 % (3319032)Termination reason: Instruction limit
% 1.51/0.64 % (3319032)Termination phase: shuffling
% 1.51/0.64 % (3319032)Time elapsed: 0.002 s
% 1.51/0.64 % (3319032)Peak memory usage: 10 MB
% 1.51/0.64 % (3319032)Instructions burned: 5 (million)
% 1.51/0.64 % (3319033)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.51/0.64 % (3319033)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2511591460:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 1.51/0.64 % (3319037)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.51/0.64 % (3319037)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.51/0.64 % (3319037)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=3200835743: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.51/0.64 % (3319033)Instruction limit reached!
% 1.51/0.64 % (3319033)------------------------------
% 1.51/0.64 % (3319033)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.51/0.64 % (3319033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.64 % (3319033)CaDiCaL version: 2.1.3
% 1.51/0.64 % (3319033)Termination reason: Instruction limit
% 1.51/0.64 % (3319033)Termination phase: shuffling
% 1.51/0.64 % (3319033)Time elapsed: 0.006 s
% 1.51/0.64 % (3319033)Peak memory usage: 10 MB
% 1.51/0.64 % (3319033)Instructions burned: 8 (million)
% 1.51/0.64 % (3319016)Instruction limit reached!
% 1.51/0.64 % (3319016)------------------------------
% 1.51/0.64 % (3319016)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.51/0.64 % (3319016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.64 % (3319016)CaDiCaL version: 2.1.3
% 1.51/0.64 % (3319016)Termination reason: Instruction limit
% 1.51/0.64 % (3319016)Termination phase: Saturation
% 1.51/0.64 % (3319016)Time elapsed: 0.067 s
% 1.51/0.64 % (3319016)Peak memory usage: 12 MB
% 1.51/0.64 % (3319016)Instructions burned: 87 (million)
% 1.51/0.64 % (3319034)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=660059028:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 1.51/0.64 % (3319037)Instruction limit reached!
% 1.51/0.64 % (3319037)------------------------------
% 1.51/0.64 % (3319037)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.51/0.64 % (3319037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.64 % (3319037)CaDiCaL version: 2.1.3
% 1.51/0.64 % (3319037)Termination reason: Instruction limit
% 1.51/0.64 % (3319037)Termination phase: Property scanning
% 1.51/0.64 % (3319037)Time elapsed: 0.012 s
% 1.51/0.64 % (3319037)Peak memory usage: 10 MB
% 1.51/0.64 % (3319037)Instructions burned: 29 (million)
% 1.51/0.64 % (3319021)Instruction limit reached!
% 1.51/0.64 % (3319021)------------------------------
% 1.51/0.64 % (3319021)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.51/0.64 % (3319021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.64 % (3319021)CaDiCaL version: 2.1.3
% 1.51/0.64 % (3319021)Termination reason: Instruction limit
% 1.51/0.64 % (3319021)Termination phase: Property scanning
% 1.51/0.64 % (3319021)Time elapsed: 0.062 s
% 1.51/0.64 % (3319021)Peak memory usage: 12 MB
% 1.51/0.64 % (3319021)Instructions burned: 75 (million)
% 1.51/0.64 % (3319034)Instruction limit reached!
% 1.51/0.64 % (3319034)------------------------------
% 1.51/0.64 % (3319034)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.51/0.64 % (3319034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.64 % (3319034)CaDiCaL version: 2.1.3
% 1.51/0.64 % (3319034)Termination reason: Instruction limit
% 1.82/0.70 % (3319034)Termination phase: shuffling
% 1.82/0.70 % (3319034)Time elapsed: 0.011 s
% 1.82/0.70 % (3319034)Peak memory usage: 10 MB
% 1.82/0.70 % (3319034)Instructions burned: 13 (million)
% 1.82/0.70 % (3319043)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.82/0.70 % (3319043)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=1571961808:i=2:add=on:rtra=on_2998 on theBenchmark for (2998ds/2Mi)
% 1.82/0.70 % (3319043)Instruction limit reached!
% 1.82/0.70 % (3319043)------------------------------
% 1.82/0.70 % (3319043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.82/0.70 % (3319043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.82/0.70 % (3319043)CaDiCaL version: 2.1.3
% 1.82/0.70 % (3319043)Termination reason: Instruction limit
% 1.82/0.70 % (3319043)Termination phase: shuffling
% 1.82/0.70 % (3319043)Time elapsed: 0.002 s
% 1.82/0.70 % (3319043)Peak memory usage: 10 MB
% 1.82/0.70 % (3319043)Instructions burned: 4 (million)
% 1.82/0.70 % (3319040)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=919805510:i=86:piset=equals:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/86Mi)
% 1.82/0.70 % (3319041)lrs+10_1_si=on:cs=on:random_seed=3428717650:i=8:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.82/0.70 % (3319045)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=275887780:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/38Mi)
% 1.82/0.70 % (3319041)Instruction limit reached!
% 1.82/0.70 % (3319041)------------------------------
% 1.82/0.70 % (3319041)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.82/0.70 % (3319041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.82/0.70 % (3319041)CaDiCaL version: 2.1.3
% 1.82/0.70 % (3319041)Termination reason: Instruction limit
% 1.82/0.70 % (3319041)Termination phase: shuffling
% 1.82/0.70 % (3319041)Time elapsed: 0.008 s
% 1.82/0.70 % (3319041)Peak memory usage: 10 MB
% 1.82/0.70 % (3319041)Instructions burned: 8 (million)
% 1.82/0.70 % (3319046)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=2600998712:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 1.82/0.70 % (3319048)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=3217110170:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 1.82/0.70 % (3319048)Instruction limit reached!
% 1.82/0.70 % (3319048)------------------------------
% 1.82/0.70 % (3319048)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.82/0.70 % (3319048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.82/0.70 % (3319048)CaDiCaL version: 2.1.3
% 1.82/0.70 % (3319048)Termination reason: Instruction limit
% 1.82/0.70 % (3319048)Termination phase: SInE selection
% 1.82/0.70 % (3319048)Time elapsed: 0.011 s
% 1.82/0.70 % (3319048)Peak memory usage: 10 MB
% 1.82/0.70 % (3319048)Instructions burned: 28 (million)
% 1.82/0.70 % (3319045)Instruction limit reached!
% 1.82/0.70 % (3319045)------------------------------
% 1.82/0.70 % (3319045)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.82/0.70 % (3319045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.82/0.70 % (3319045)CaDiCaL version: 2.1.3
% 1.82/0.70 % (3319045)Termination reason: Instruction limit
% 1.82/0.70 % (3319045)Termination phase: Preprocessing 3
% 1.82/0.70 % (3319045)Time elapsed: 0.032 s
% 1.82/0.70 % (3319045)Peak memory usage: 11 MB
% 1.82/0.70 % (3319045)Instructions burned: 39 (million)
% 1.82/0.70 % (3319053)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=1092004298:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.82/0.70 % (3319055)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=908078665:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 1.82/0.70 % (3319022)Instruction limit reached!
% 1.82/0.70 % (3319022)------------------------------
% 1.82/0.70 % (3319022)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.82/0.70 % (3319022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.05/0.78 % (3319022)CaDiCaL version: 2.1.3
% 2.05/0.78 % (3319022)Termination reason: Instruction limit
% 2.05/0.78 % (3319022)Termination phase: Saturation
% 2.05/0.78 % (3319022)Time elapsed: 0.138 s
% 2.05/0.78 % (3319022)Peak memory usage: 13 MB
% 2.05/0.78 % (3319022)Instructions burned: 157 (million)
% 2.05/0.78 % (3319053)Instruction limit reached!
% 2.05/0.78 % (3319053)------------------------------
% 2.05/0.78 % (3319053)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.05/0.78 % (3319053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.05/0.78 % (3319053)CaDiCaL version: 2.1.3
% 2.05/0.78 % (3319053)Termination reason: Instruction limit
% 2.05/0.78 % (3319053)Termination phase: shuffling
% 2.05/0.78 % (3319053)Time elapsed: 0.013 s
% 2.05/0.78 % (3319053)Peak memory usage: 10 MB
% 2.05/0.78 % (3319053)Instructions burned: 14 (million)
% 2.05/0.78 % (3319040)Instruction limit reached!
% 2.05/0.78 % (3319040)------------------------------
% 2.05/0.78 % (3319040)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.05/0.78 % (3319040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.05/0.78 % (3319040)CaDiCaL version: 2.1.3
% 2.05/0.78 % (3319040)Termination reason: Instruction limit
% 2.05/0.78 % (3319040)Termination phase: Saturation
% 2.05/0.78 % (3319040)Time elapsed: 0.067 s
% 2.05/0.78 % (3319040)Peak memory usage: 12 MB
% 2.05/0.78 % (3319040)Instructions burned: 86 (million)
% 2.05/0.78 % (3319057)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=2947357838:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 2.05/0.78 % (3319062)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=979909930:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2997 on theBenchmark for (2997ds/23Mi)
% 2.05/0.78 % (3319060)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=3135691443:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2997 on theBenchmark for (2997ds/2Mi)
% 2.05/0.78 % (3319057)Instruction limit reached!
% 2.05/0.78 % (3319057)------------------------------
% 2.05/0.78 % (3319057)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.05/0.78 % (3319057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.05/0.78 % (3319057)CaDiCaL version: 2.1.3
% 2.05/0.78 % (3319057)Termination reason: Instruction limit
% 2.05/0.78 % (3319057)Termination phase: shuffling
% 2.05/0.78 % (3319057)Time elapsed: 0.013 s
% 2.05/0.78 % (3319057)Peak memory usage: 10 MB
% 2.05/0.78 % (3319057)Instructions burned: 14 (million)
% 2.05/0.78 % (3319061)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=918129524:i=26:ep=R:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/26Mi)
% 2.05/0.78 % (3319060)Instruction limit reached!
% 2.05/0.78 % (3319060)------------------------------
% 2.05/0.78 % (3319060)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.05/0.78 % (3319060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.05/0.78 % (3319060)CaDiCaL version: 2.1.3
% 2.05/0.78 % (3319060)Termination reason: Instruction limit
% 2.05/0.78 % (3319060)Termination phase: shuffling
% 2.05/0.78 % (3319060)Time elapsed: 0.003 s
% 2.05/0.78 % (3319060)Peak memory usage: 10 MB
% 2.05/0.78 % (3319060)Instructions burned: 3 (million)
% 2.05/0.78 % (3319062)Instruction limit reached!
% 2.05/0.78 % (3319062)------------------------------
% 2.05/0.78 % (3319062)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.05/0.78 % (3319062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.05/0.78 % (3319062)CaDiCaL version: 2.1.3
% 2.05/0.78 % (3319062)Termination reason: Instruction limit
% 2.05/0.78 % (3319062)Termination phase: Property scanning
% 2.05/0.78 % (3319062)Time elapsed: 0.012 s
% 2.05/0.78 % (3319062)Peak memory usage: 10 MB
% 2.05/0.78 % (3319062)Instructions burned: 25 (million)
% 2.05/0.78 % (3319061)Instruction limit reached!
% 2.05/0.78 % (3319061)------------------------------
% 2.05/0.78 % (3319061)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.05/0.78 % (3319061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.05/0.78 % (3319061)CaDiCaL version: 2.1.3
% 2.05/0.78 % (3319061)Termination reason: Instruction limit
% 2.05/0.78 % (3319061)Termination phase: Property scanning
% 2.05/0.78 % (3319061)Time elapsed: 0.022 s
% 2.05/0.78 % (3319061)Peak memory usage: 10 MB
% 2.72/0.86 % (3319061)Instructions burned: 26 (million)
% 2.72/0.86 % (3319070)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 2.72/0.86 % (3319069)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.72/0.86 % (3319069)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 2.72/0.86 % (3319068)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=238978213:cond=on:i=60:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/60Mi)
% 2.72/0.86 % (3319070)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=187655680:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2997 on theBenchmark for (2997ds/8Mi)
% 2.72/0.86 % (3319069)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=3631113331:i=14:add=off:nm=40:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 2.72/0.86 % (3319070)Instruction limit reached!
% 2.72/0.86 % (3319070)------------------------------
% 2.72/0.86 % (3319070)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.72/0.86 % (3319070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.72/0.86 % (3319070)CaDiCaL version: 2.1.3
% 2.72/0.86 % (3319070)Termination reason: Instruction limit
% 2.72/0.86 % (3319070)Termination phase: shuffling
% 2.72/0.86 % (3319070)Time elapsed: 0.008 s
% 2.72/0.86 % (3319070)Peak memory usage: 10 MB
% 2.72/0.86 % (3319070)Instructions burned: 9 (million)
% 2.72/0.86 % (3319069)Instruction limit reached!
% 2.72/0.86 % (3319069)------------------------------
% 2.72/0.86 % (3319069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.72/0.86 % (3319069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.72/0.86 % (3319069)CaDiCaL version: 2.1.3
% 2.72/0.86 % (3319069)Termination reason: Instruction limit
% 2.72/0.86 % (3319069)Termination phase: shuffling
% 2.72/0.86 % (3319069)Time elapsed: 0.013 s
% 2.72/0.86 % (3319069)Peak memory usage: 10 MB
% 2.72/0.86 % (3319069)Instructions burned: 15 (million)
% 2.72/0.86 % (3319071)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=2027092129:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2997 on theBenchmark for (2997ds/31Mi)
% 2.72/0.86 % (3319075)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=2538278562:i=7:hud=5:bd=preordered:rtra=on:bet=on_2997 on theBenchmark for (2997ds/7Mi)
% 2.72/0.86 % (3319075)Instruction limit reached!
% 2.72/0.86 % (3319075)------------------------------
% 2.72/0.86 % (3319075)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.72/0.86 % (3319075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.72/0.86 % (3319075)CaDiCaL version: 2.1.3
% 2.72/0.86 % (3319075)Termination reason: Instruction limit
% 2.72/0.86 % (3319075)Termination phase: shuffling
% 2.72/0.86 % (3319075)Time elapsed: 0.004 s
% 2.72/0.86 % (3319075)Peak memory usage: 10 MB
% 2.72/0.86 % (3319075)Instructions burned: 7 (million)
% 2.72/0.86 % (3319076)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=1033284435:i=23:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/23Mi)
% 2.72/0.86 % (3319068)Instruction limit reached!
% 2.72/0.86 % (3319068)------------------------------
% 2.72/0.86 % (3319068)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.72/0.86 % (3319068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.72/0.86 % (3319068)CaDiCaL version: 2.1.3
% 2.72/0.86 % (3319068)Termination reason: Instruction limit
% 2.72/0.86 % (3319068)Termination phase: Equality resolution with deletion
% 2.72/0.86 % (3319068)Time elapsed: 0.051 s
% 2.72/0.86 % (3319068)Peak memory usage: 11 MB
% 2.72/0.86 % (3319068)Instructions burned: 60 (million)
% 2.72/0.86 % (3319071)Instruction limit reached!
% 2.72/0.86 % (3319071)------------------------------
% 2.72/0.86 % (3319071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.72/0.86 % (3319071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.19/1.01 % (3319071)CaDiCaL version: 2.1.3
% 3.19/1.01 % (3319071)Termination reason: Instruction limit
% 3.19/1.01 % (3319071)Termination phase: Property scanning
% 3.19/1.01 % (3319071)Time elapsed: 0.027 s
% 3.19/1.01 % (3319071)Peak memory usage: 10 MB
% 3.19/1.01 % (3319071)Instructions burned: 32 (million)
% 3.19/1.01 % (3319055)Instruction limit reached!
% 3.19/1.01 % (3319055)------------------------------
% 3.19/1.01 % (3319055)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.19/1.01 % (3319055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.19/1.01 % (3319055)CaDiCaL version: 2.1.3
% 3.19/1.01 % (3319055)Termination reason: Instruction limit
% 3.19/1.01 % (3319055)Termination phase: Saturation
% 3.19/1.01 % (3319055)Time elapsed: 0.127 s
% 3.19/1.01 % (3319055)Peak memory usage: 14 MB
% 3.19/1.01 % (3319055)Instructions burned: 327 (million)
% 3.19/1.01 % (3319076)Instruction limit reached!
% 3.19/1.01 % (3319076)------------------------------
% 3.19/1.01 % (3319076)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.19/1.01 % (3319076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.19/1.01 % (3319076)CaDiCaL version: 2.1.3
% 3.19/1.01 % (3319076)Termination reason: Instruction limit
% 3.19/1.01 % (3319076)Termination phase: shuffling
% 3.19/1.01 % (3319076)Time elapsed: 0.020 s
% 3.19/1.01 % (3319076)Peak memory usage: 10 MB
% 3.19/1.01 % (3319076)Instructions burned: 23 (million)
% 3.19/1.01 % (3319083)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=3842681699:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/193Mi)
% 3.19/1.01 % (3319079)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=4023814593:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2996 on theBenchmark for (2996ds/20Mi)
% 3.19/1.01 % (3319082)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=1850207723:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2996 on theBenchmark for (2996ds/143Mi)
% 3.19/1.01 % (3319081)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=800532230:i=1240:rtra=on:ixr=off_2996 on theBenchmark for (2996ds/1240Mi)
% 3.19/1.01 % (3319046)Instruction limit reached!
% 3.19/1.01 % (3319046)------------------------------
% 3.19/1.01 % (3319046)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.19/1.01 % (3319046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.19/1.01 % (3319046)CaDiCaL version: 2.1.3
% 3.19/1.01 % (3319046)Termination reason: Instruction limit
% 3.19/1.01 % (3319046)Termination phase: Saturation
% 3.19/1.01 % (3319046)Time elapsed: 0.210 s
% 3.19/1.01 % (3319046)Peak memory usage: 14 MB
% 3.19/1.01 % (3319046)Instructions burned: 250 (million)
% 3.19/1.01 % (3319079)Instruction limit reached!
% 3.19/1.01 % (3319079)------------------------------
% 3.19/1.01 % (3319079)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.19/1.01 % (3319079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.19/1.01 % (3319079)CaDiCaL version: 2.1.3
% 3.19/1.01 % (3319079)Termination reason: Instruction limit
% 3.19/1.01 % (3319079)Termination phase: Property scanning
% 3.19/1.01 % (3319079)Time elapsed: 0.019 s
% 3.19/1.01 % (3319079)Peak memory usage: 10 MB
% 3.19/1.01 % (3319079)Instructions burned: 20 (million)
% 3.19/1.01 % (3319085)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3606121107:i=42:hud=10:rtra=on_2996 on theBenchmark for (2996ds/42Mi)
% 3.19/1.01 % (3319090)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=797381069:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/181Mi)
% 3.19/1.01 % (3319089)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 3.19/1.01 % (3319089)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=4196077018:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2996 on theBenchmark for (2996ds/7Mi)
% 3.19/1.01 % (3319089)Instruction limit reached!
% 3.19/1.01 % (3319089)------------------------------
% 3.19/1.01 % (3319089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.19/1.01 % (3319089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.19/1.01 % (3319089)CaDiCaL version: 2.1.3
% 3.19/1.01 % (3319089)Termination reason: Instruction limit
% 3.19/1.01 % (3319089)Termination phase: shuffling
% 4.67/1.06 % (3319089)Time elapsed: 0.007 s
% 4.67/1.06 % (3319089)Peak memory usage: 10 MB
% 4.67/1.06 % (3319089)Instructions burned: 8 (million)
% 4.67/1.06 % (3319085)Instruction limit reached!
% 4.67/1.06 % (3319085)------------------------------
% 4.67/1.06 % (3319085)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.67/1.06 % (3319085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.67/1.06 % (3319085)CaDiCaL version: 2.1.3
% 4.67/1.06 % (3319085)Termination reason: Instruction limit
% 4.67/1.06 % (3319085)Termination phase: Preprocessing 3
% 4.67/1.06 % (3319085)Time elapsed: 0.036 s
% 4.67/1.06 % (3319085)Peak memory usage: 11 MB
% 4.67/1.06 % (3319085)Instructions burned: 42 (million)
% 4.67/1.06 % (3319083)Instruction limit reached!
% 4.67/1.06 % (3319083)------------------------------
% 4.67/1.06 % (3319083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.67/1.06 % (3319083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.67/1.06 % (3319083)CaDiCaL version: 2.1.3
% 4.67/1.06 % (3319083)Termination reason: Instruction limit
% 4.67/1.06 % (3319083)Termination phase: Saturation
% 4.67/1.06 % (3319083)Time elapsed: 0.085 s
% 4.67/1.06 % (3319083)Peak memory usage: 14 MB
% 4.67/1.06 % (3319083)Instructions burned: 195 (million)
% 4.67/1.06 % (3319095)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 4.67/1.06 % (3319094)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=1415171188:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2995 on theBenchmark for (2995ds/169Mi)
% 4.67/1.06 % (3319095)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=2040150588:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2995 on theBenchmark for (2995ds/6Mi)
% 4.67/1.06 % (3319096)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=3968846702:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2995 on theBenchmark for (2995ds/22Mi)
% 4.67/1.06 % (3319095)Instruction limit reached!
% 4.67/1.06 % (3319095)------------------------------
% 4.67/1.06 % (3319095)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.67/1.06 % (3319095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.67/1.06 % (3319095)CaDiCaL version: 2.1.3
% 4.67/1.06 % (3319095)Termination reason: Instruction limit
% 4.67/1.06 % (3319095)Termination phase: shuffling
% 4.67/1.06 % (3319095)Time elapsed: 0.006 s
% 4.67/1.06 % (3319095)Peak memory usage: 10 MB
% 4.67/1.06 % (3319095)Instructions burned: 7 (million)
% 4.67/1.06 % (3319096)Instruction limit reached!
% 4.67/1.06 % (3319096)------------------------------
% 4.67/1.06 % (3319096)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.67/1.06 % (3319096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.67/1.06 % (3319096)CaDiCaL version: 2.1.3
% 4.67/1.06 % (3319096)Termination reason: Instruction limit
% 4.67/1.06 % (3319096)Termination phase: Property scanning
% 4.67/1.06 % (3319096)Time elapsed: 0.012 s
% 4.67/1.06 % (3319096)Peak memory usage: 10 MB
% 4.67/1.06 % (3319096)Instructions burned: 24 (million)
% 4.67/1.06 % (3319100)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=3479584294:i=19:add=on:rtra=on_2995 on theBenchmark for (2995ds/19Mi)
% 4.67/1.06 % (3319082)Instruction limit reached!
% 4.67/1.06 % (3319082)------------------------------
% 4.67/1.06 % (3319082)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.67/1.06 % (3319082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.67/1.06 % (3319082)CaDiCaL version: 2.1.3
% 4.67/1.06 % (3319082)Termination reason: Instruction limit
% 4.67/1.06 % (3319082)Termination phase: Saturation
% 4.67/1.06 % (3319082)Time elapsed: 0.123 s
% 4.67/1.06 % (3319082)Peak memory usage: 14 MB
% 4.67/1.06 % (3319082)Instructions burned: 143 (million)
% 4.67/1.06 % (3319100)Instruction limit reached!
% 4.67/1.06 % (3319100)------------------------------
% 4.67/1.06 % (3319100)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.67/1.06 % (3319100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.67/1.06 % (3319100)CaDiCaL version: 2.1.3
% 4.67/1.06 % (3319100)Termination reason: Instruction limit
% 4.67/1.06 % (3319100)Termination phase: shuffling
% 4.67/1.06 % (3319100)Time elapsed: 0.009 s
% 4.67/1.06 % (3319100)Peak memory usage: 10 MB
% 4.67/1.06 % (3319100)Instructions burned: 21 (million)
% 4.67/1.06 % (3319101)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=2318089934:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/316Mi)
% 4.67/1.06 % (3319103)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=3448115882: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)
% 4.67/1.06 % (3319104)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=711711787: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)
% 4.67/1.06 % (3319094)Refutation not found, incomplete strategy
% 4.67/1.06 % (3319094)------------------------------
% 4.67/1.06 % (3319094)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.67/1.06 % (3319094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.67/1.06 % (3319094)CaDiCaL version: 2.1.3
% 4.67/1.06 % (3319094)Termination reason: Refutation not found, incomplete strategy
% 4.67/1.06 % (3319094)Time elapsed: 0.087 s
% 4.67/1.06 % (3319094)Peak memory usage: 14 MB
% 4.67/1.06 % (3319094)Instructions burned: 103 (million)
% 4.67/1.06 % (3319094)------------------------------
% 4.67/1.06 % (3319094)------------------------------
% 4.67/1.06 % (3319090)Instruction limit reached!
% 4.67/1.06 % (3319090)------------------------------
% 4.67/1.06 % (3319090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.67/1.06 % (3319090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.67/1.06 % (3319090)CaDiCaL version: 2.1.3
% 4.67/1.06 % (3319090)Termination reason: Instruction limit
% 4.67/1.06 % (3319090)Termination phase: Saturation
% 4.67/1.06 % (3319090)Time elapsed: 0.140 s
% 4.67/1.06 % (3319090)Peak memory usage: 14 MB
% 4.67/1.06 % (3319090)Instructions burned: 181 (million)
% 4.67/1.06 % (3319104)Instruction limit reached!
% 4.67/1.06 % (3319104)------------------------------
% 4.67/1.06 % (3319104)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.67/1.06 % (3319104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.67/1.06 % (3319104)CaDiCaL version: 2.1.3
% 4.67/1.06 % (3319104)Termination reason: Instruction limit
% 4.67/1.06 % (3319104)Termination phase: Unused predicate definition removal
% 4.67/1.06 % (3319104)Time elapsed: 0.040 s
% 4.67/1.06 % (3319104)Peak memory usage: 11 MB
% 4.67/1.06 % (3319104)Instructions burned: 46 (million)
% 4.67/1.06 % (3319108)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=1162318511:i=480:rtra=on_2994 on theBenchmark for (2994ds/480Mi)
% 4.67/1.06 % (3319109)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=3090732537: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)
% 4.67/1.06 % (3319109)Instruction limit reached!
% 4.67/1.06 % (3319109)------------------------------
% 4.67/1.06 % (3319109)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.67/1.06 % (3319109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.67/1.06 % (3319109)CaDiCaL version: 2.1.3
% 4.67/1.06 % (3319109)Termination reason: Instruction limit
% 4.67/1.06 % (3319109)Termination phase: Property scanning
% 4.67/1.06 % (3319109)Time elapsed: 0.018 s
% 4.67/1.06 % (3319109)Peak memory usage: 10 MB
% 4.67/1.06 % (3319109)Instructions burned: 21 (million)
% 4.67/1.06 % (3319110)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 4.67/1.06 % (3319110)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=4279611255:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/200Mi)
% 4.67/1.06 % (3319113)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=3116259427:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2994 on theBenchmark for (2994ds/13Mi)
% 4.67/1.06 % (3319113)Instruction limit reached!
% 4.67/1.06 % (3319113)------------------------------
% 4.67/1.06 % (3319113)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.67/1.06 % (3319113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.67/1.06 % (3319113)CaDiCaL version: 2.1.3
% 4.67/1.06 % (3319113)Termination reason: Instruction limit
% 4.67/1.06 % (3319113)Termination phase: shuffling
% 4.67/1.06 % (3319113)Time elapsed: 0.012 s
% 4.67/1.06 % (3319113)Peak memory usage: 10 MB
% 4.67/1.06 % (3319113)Instructions burned: 13 (million)
% 4.67/1.06 % (3319101)Instruction limit reached!
% 4.67/1.06 % (3319101)------------------------------
% 4.67/1.06 % (3319101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.67/1.06 % (3319101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.67/1.06 % (3319101)CaDiCaL version: 2.1.3
% 4.67/1.06 % (3319101)Termination reason: Instruction limit
% 4.67/1.06 % (3319101)Termination phase: Saturation
% 4.67/1.06 % (3319101)Time elapsed: 0.153 s
% 4.67/1.06 % (3319101)Peak memory usage: 15 MB
% 4.67/1.06 % (3319101)Instructions burned: 318 (million)
% 4.67/1.06 % (3319019)Instruction limit reached!
% 4.67/1.06 % (3319019)------------------------------
% 4.67/1.06 % (3319019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.67/1.06 % (3319019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.67/1.06 % (3319019)CaDiCaL version: 2.1.3
% 4.67/1.06 % (3319019)Termination reason: Instruction limit
% 4.67/1.06 % (3319019)Termination phase: Saturation
% 4.67/1.06 % (3319019)Time elapsed: 0.579 s
% 4.67/1.06 % (3319019)Peak memory usage: 16 MB
% 4.67/1.06 % (3319019)Instructions burned: 634 (million)
% 4.67/1.06 % (3319117)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=1986667258:i=51:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/51Mi)
% 4.67/1.06 % (3319108) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3319011-3319108"...
% 4.67/1.06 % (3319108)...printing done.
% 4.67/1.06 % (3319116)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=2562958747:i=66:s2at=3:nm=2:rtra=on:rawr=on_2993 on theBenchmark for (2993ds/66Mi)
% 4.67/1.06 % (3319108)Refutation found. Thanks to Tanya!
% 4.67/1.06 % SZS status Theorem for theBenchmark
% 4.67/1.06 % SZS output start Proof for theBenchmark
% 4.67/1.06 thf(type_def_5, type, configuration_ext: ($tType * $tType * $tType * $tType) > $tType).
% 4.67/1.06 thf(type_def_6, type, message: ($tType * $tType) > $tType).
% 4.67/1.06 thf(type_def_7, type, product_unit: $tType).
% 4.67/1.06 thf(type_def_8, type, list: $tType > $tType).
% 4.67/1.06 thf(type_def_9, type, nat: $tType).
% 4.67/1.06 thf(type_def_10, type, v: $tType).
% 4.67/1.06 thf(type_def_11, type, s: $tType).
% 4.67/1.06 thf(type_def_12, type, p: $tType).
% 4.67/1.06 thf(type_def_13, type, sTfun: ($tType * $tType) > $tType).
% 4.67/1.06 thf(func_def_0, type, type: !>[X0: $tType]:($o)).
% 4.67/1.06 thf(func_def_1, type, size: !>[X0: $tType]:($o)).
% 4.67/1.06 thf(func_def_2, type, one: !>[X0: $tType]:($o)).
% 4.67/1.06 thf(func_def_3, type, zero: !>[X0: $tType]:($o)).
% 4.67/1.06 thf(func_def_4, type, neg_numeral: !>[X0: $tType]:($o)).
% 4.67/1.06 thf(func_def_5, type, order: !>[X0: $tType]:($o)).
% 4.67/1.06 thf(func_def_6, type, group_add: !>[X0: $tType]:($o)).
% 4.67/1.06 thf(func_def_7, type, wellorder: !>[X0: $tType]:($o)).
% 4.67/1.06 thf(func_def_8, type, comm_monoid_diff: !>[X0: $tType]:($o)).
% 4.67/1.06 thf(func_def_9, type, ordered_ab_group_add: !>[X0: $tType]:($o)).
% 4.67/1.06 thf(func_def_10, type, cancel1352612707id_add: !>[X0: $tType]:($o)).
% 4.67/1.06 thf(func_def_11, type, cancel146912293up_add: !>[X0: $tType]:($o)).
% 4.67/1.06 thf(func_def_12, type, linord1659791738miring: !>[X0: $tType]:($o)).
% 4.67/1.06 thf(func_def_13, type, canoni770627133id_add: !>[X0: $tType]:($o)).
% 4.67/1.06 thf(func_def_14, type, enabled: !>[X0: $tType, X1: $tType, X2: $tType]:((configuration_ext @ X0 @ X1 @ X2 @ product_unit > message @ X0 @ X1 > $o))).
% 4.67/1.06 thf(func_def_15, type, firstOccurrence: !>[X0: $tType, X1: $tType, X2: $tType]:((list @ configuration_ext @ X0 @ X1 @ X2 @ product_unit > list @ message @ X0 @ X1 > message @ X0 @ X1 > nat > $o))).
% 4.67/1.06 thf(func_def_16, type, fLPThe137922386ionCfg: !>[X0: $tType, X1: $tType, X2: $tType]:((configuration_ext @ X0 @ X1 @ X2 @ product_unit > (list @ configuration_ext @ X0 @ X1 @ X2 @ product_unit > list @ message @ X0 @ X1 > list @ configuration_ext @ X0 @ X1 @ X2 @ product_unit) > (list @ configuration_ext @ X0 @ X1 @ X2 @ product_unit > list @ message @ X0 @ X1 > list @ message @ X0 @ X1) > nat > list @ configuration_ext @ X0 @ X1 @ X2 @ product_unit))).
% 4.67/1.06 thf(func_def_17, type, fLPThe221390223ionMsg: !>[X0: $tType, X1: $tType, X2: $tType]:((configuration_ext @ X0 @ X1 @ X2 @ product_unit > (list @ configuration_ext @ X0 @ X1 @ X2 @ product_unit > list @ message @ X0 @ X1 > list @ configuration_ext @ X0 @ X1 @ X2 @ product_unit) > (list @ configuration_ext @ X0 @ X1 @ X2 @ product_unit > list @ message @ X0 @ X1 > list @ message @ X0 @ X1) > nat > list @ message @ X0 @ X1))).
% 4.67/1.06 thf(func_def_18, type, minus_minus: !>[X0: $tType]:((X0 > X0 > X0))).
% 4.67/1.06 thf(func_def_19, type, one_one: !>[X0: $tType]:(X0)).
% 4.67/1.06 thf(func_def_20, type, zero_zero: !>[X0: $tType]:(X0)).
% 4.67/1.06 thf(func_def_21, type, prefixList: !>[X0: $tType]:((list @ X0 > list @ X0 > $o))).
% 4.67/1.06 thf(func_def_22, type, last: !>[X0: $tType]:((list @ X0 > X0))).
% 4.67/1.06 thf(func_def_23, type, nil: !>[X0: $tType]:(list @ X0)).
% 4.67/1.06 thf(func_def_24, type, nth: !>[X0: $tType]:((list @ X0 > nat > X0))).
% 4.67/1.06 thf(func_def_25, type, suc: (nat > nat)).
% 4.67/1.06 thf(func_def_26, type, size_size: !>[X0: $tType]:((X0 > nat))).
% 4.67/1.06 thf(func_def_27, type, ord_less: !>[X0: $tType]:((X0 > X0 > $o))).
% 4.67/1.06 thf(func_def_28, type, ord_less_eq: !>[X0: $tType]:((X0 > X0 > $o))).
% 4.67/1.06 thf(func_def_29, type, fe: (nat > list @ configuration_ext @ p @ v @ s @ product_unit)).
% 4.67/1.06 thf(func_def_30, type, ft: (nat > list @ message @ p @ v)).
% 4.67/1.06 thf(func_def_31, type, index: nat).
% 4.67/1.06 thf(func_def_32, type, msgInSet: message @ p @ v).
% 4.67/1.06 thf(func_def_33, type, msg: message @ p @ v).
% 4.67/1.06 thf(func_def_34, type, n0: nat).
% 4.67/1.06 thf(func_def_35, type, n1: nat).
% 4.67/1.06 thf(func_def_36, type, nMsg: nat).
% 4.67/1.06 thf(func_def_37, type, n: nat).
% 4.67/1.06 thf(func_def_41, type, db1: !>[X0: $tType]:(X0)).
% 4.67/1.06 thf(func_def_42, type, db0: !>[X0: $tType]:(X0)).
% 4.67/1.06 thf(func_def_43, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 4.67/1.06 thf(func_def_44, type, vOR: ($o > $o > $o)).
% 4.67/1.06 thf(func_def_45, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 4.67/1.06 thf(func_def_46, type, vAND: ($o > $o > $o)).
% 4.67/1.06 thf(func_def_47, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 4.67/1.06 thf(func_def_48, type, vIMP: ($o > $o > $o)).
% 4.67/1.06 thf(func_def_49, type, db2: !>[X0: $tType]:(X0)).
% 4.67/1.06 thf(func_def_50, type, vNOT: ($o > $o)).
% 4.67/1.06 thf(func_def_51, type, sP0: ((configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > (configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > $o)).
% 4.67/1.06 thf(func_def_52, type, sP1: ((configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > (configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > $o)).
% 4.67/1.06 thf(func_def_53, type, sK2: ((nat > $o) > nat > nat)).
% 4.67/1.06 thf(func_def_54, type, sK3: (nat > nat)).
% 4.67/1.06 thf(func_def_55, type, sK4: !>[X0: $tType]:(((nat > X0) > nat))).
% 4.67/1.06 thf(func_def_56, type, sK5: (nat > (nat > $o) > nat)).
% 4.67/1.06 thf(func_def_57, type, sK6: (nat > (nat > $o) > nat)).
% 4.67/1.06 thf(func_def_58, type, sK7: (nat > nat)).
% 4.67/1.06 thf(func_def_59, type, sK8: (nat > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > nat)).
% 4.67/1.06 thf(func_def_60, type, sK9: !>[X0: $tType]:(((X0 > nat) > (X0 > $o) > X0))).
% 4.67/1.06 thf(func_def_61, type, sK10: !>[X0: $tType]:(((X0 > nat) > (X0 > $o) > X0))).
% 4.67/1.06 thf(func_def_62, type, sK11: ((nat > nat > $o) > nat)).
% 4.67/1.06 thf(func_def_63, type, sK12: ((nat > nat > $o) > nat)).
% 4.67/1.06 thf(func_def_64, type, sK13: ((nat > nat > $o) > nat)).
% 4.67/1.06 thf(func_def_65, type, sK14: ((nat > nat > $o) > nat)).
% 4.67/1.06 thf(func_def_66, type, sK15: ((nat > nat > $o) > nat)).
% 4.67/1.06 thf(func_def_67, type, sK16: (nat > nat > nat)).
% 4.67/1.06 thf(func_def_68, type, sK17: (nat > nat > nat)).
% 4.67/1.06 thf(func_def_69, type, sK18: !>[X0: $tType]:((nat > (nat > X0 > $o) > X0))).
% 4.67/1.06 thf(func_def_70, type, sK19: !>[X0: $tType]:((list @ X0 > (nat > X0 > $o) > nat > nat))).
% 4.67/1.06 thf(func_def_71, type, sK20: !>[X0: $tType]:(((nat > X0 > $o) > nat > list @ X0))).
% 4.67/1.06 thf(func_def_72, type, sK21: !>[X0: $tType]:(((nat > X0 > $o) > nat > nat))).
% 4.67/1.06 thf(func_def_73, type, sK22: ((nat > $o) > nat > nat)).
% 4.67/1.06 thf(func_def_74, type, sK23: (nat > (nat > $o) > nat)).
% 4.67/1.06 thf(func_def_75, type, sK24: ((nat > $o) > nat)).
% 4.67/1.06 thf(func_def_76, type, sK25: (nat > nat > nat)).
% 4.67/1.06 thf(func_def_77, type, sK26: (nat > nat > nat)).
% 4.67/1.06 thf(func_def_78, type, sK27: ((configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > (configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > configuration_ext @ p @ v @ s @ product_unit)).
% 4.67/1.06 thf(func_def_79, type, sK28: ((configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > (configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > nat)).
% 4.67/1.06 thf(func_def_80, type, sK29: ((configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > (configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit)).
% 4.67/1.06 thf(func_def_81, type, sK30: ((configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > (configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v)).
% 4.67/1.06 thf(func_def_82, type, sK31: ((configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > (configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > configuration_ext @ p @ v @ s @ product_unit)).
% 4.67/1.06 thf(func_def_83, type, sK32: ((configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > (configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v)).
% 4.67/1.06 thf(func_def_84, type, sK33: ((configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > (configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit)).
% 4.67/1.06 thf(func_def_85, type, sK34: ((configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > (configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > nat)).
% 4.67/1.06 thf(func_def_86, type, sK35: ((configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit)).
% 4.67/1.06 thf(func_def_87, type, sK36: ((configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > configuration_ext @ p @ v @ s @ product_unit)).
% 4.67/1.06 thf(func_def_88, type, sK37: ((configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v)).
% 4.67/1.06 thf(func_def_89, type, sK38: ((configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v)).
% 4.67/1.06 thf(func_def_90, type, sK39: ((configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > configuration_ext @ p @ v @ s @ product_unit)).
% 4.67/1.06 thf(func_def_91, type, sK40: ((configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit)).
% 4.67/1.06 thf(func_def_92, type, sK41: ((configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > (configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > configuration_ext @ p @ v @ s @ product_unit)).
% 4.67/1.06 thf(func_def_93, type, sK42: ((configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > (configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v)).
% 4.67/1.06 thf(func_def_94, type, sK43: ((configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > (configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > nat)).
% 4.67/1.06 thf(func_def_95, type, sK44: ((configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > (configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit)).
% 4.67/1.06 thf(func_def_96, type, sK45: ((configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > (configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v)).
% 4.67/1.06 thf(func_def_97, type, sK46: ((configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > (configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit)).
% 4.67/1.06 thf(func_def_98, type, sK47: ((configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > (configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > configuration_ext @ p @ v @ s @ product_unit)).
% 4.67/1.06 thf(func_def_99, type, sK48: ((configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > (configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > nat)).
% 4.67/1.06 thf(func_def_100, type, sK49: ((configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > configuration_ext @ p @ v @ s @ product_unit)).
% 4.67/1.06 thf(func_def_101, type, sK50: ((configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v)).
% 4.67/1.06 thf(func_def_102, type, sK51: ((configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit)).
% 4.67/1.06 thf(func_def_103, type, sK52: ((configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > configuration_ext @ p @ v @ s @ product_unit)).
% 4.67/1.06 thf(func_def_104, type, sK53: ((configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit)).
% 4.67/1.06 thf(func_def_105, type, sK54: ((configuration_ext @ p @ v @ s @ product_unit > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ configuration_ext @ p @ v @ s @ product_unit) > (list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v) > nat > $o) > list @ configuration_ext @ p @ v @ s @ product_unit > list @ message @ p @ v > list @ message @ p @ v)).
% 4.67/1.06 thf(func_def_106, type, sK55: !>[X0: $tType]:((list @ X0 > list @ X0 > nat))).
% 4.67/1.06 thf(func_def_107, type, sK56: (nat > nat > (nat > $o) > nat)).
% 4.67/1.06 thf(func_def_108, type, sK57: (nat > nat)).
% 4.67/1.06 thf(func_def_109, type, sK58: ((nat > $o) > nat > nat)).
% 4.67/1.06 thf(func_def_110, type, sK59: ((nat > $o) > nat)).
% 4.67/1.06 thf(func_def_111, type, sK60: ((nat > $o) > (nat > $o) > nat > nat)).
% 4.67/1.06 thf(func_def_112, type, sK61: !>[X0: $tType, X1: $tType]:(((X1 > X0) > (X1 > $o) > X1))).
% 4.67/1.06 thf(func_def_113, type, sK62: !>[X0: $tType]:(((nat > X0) > nat))).
% 4.67/1.06 thf(func_def_114, type, sK63: !>[X0: $tType]:(((list @ X0 > $o) > list @ X0))).
% 4.67/1.06 thf(func_def_115, type, sK64: nat).
% 4.67/1.06 thf(func_def_116, type, sK65: nat).
% 4.67/1.06 thf(func_def_117, type, sK66: !>[X0: $tType]:(((nat > X0) > nat))).
% 4.67/1.06 thf(func_def_118, type, sK67: ((nat > nat) > nat)).
% 4.67/1.06 thf(func_def_119, type, sK68: ((nat > nat) > nat)).
% 4.67/1.06 thf(func_def_120, type, sK69: (nat > nat)).
% 4.67/1.06 thf(func_def_121, type, sK70: !>[X0: $tType]:(((nat > X0) > nat))).
% 4.67/1.06 thf(func_def_122, type, sK71: ((nat > nat > $o) > nat)).
% 4.67/1.06 thf(func_def_123, type, sK72: ((nat > nat > $o) > nat)).
% 4.67/1.06 thf(func_def_124, type, sK73: ((nat > nat > $o) > nat)).
% 4.67/1.06 thf(func_def_125, type, sK74: ((nat > nat > $o) > nat)).
% 4.67/1.06 thf(func_def_126, type, sK75: ((nat > $o) > nat)).
% 4.67/1.06 thf(func_def_127, type, sK76: ((nat > $o) > nat)).
% 4.67/1.06 thf(func_def_128, type, sK77: ((nat > $o) > nat > nat)).
% 4.67/1.06 thf(func_def_129, type, sK78: ((nat > $o) > nat)).
% 4.67/1.06 thf(func_def_130, type, sK79: (nat > nat > message @ p @ v > nat)).
% 4.67/1.06 thf(func_def_131, type, sK80: ((nat > $o) > nat)).
% 4.67/1.06 thf(func_def_132, type, sK81: ((nat > $o) > nat)).
% 4.67/1.06 thf(func_def_133, type, sK82: (nat > nat)).
% 4.67/1.06 thf(func_def_134, type, sK83: ((nat > $o) > nat)).
% 4.67/1.06 thf(func_def_135, type, sK84: !>[X0: $tType, X1: $tType]:(((X0 > $o) > (X0 > X1) > X0))).
% 4.67/1.06 thf(func_def_136, type, sK85: (nat > (nat > $o) > nat)).
% 4.67/1.06 thf(func_def_137, type, sK86: (nat > (nat > $o) > nat)).
% 4.67/1.06 thf(func_def_138, type, sK87: !>[X0: $tType]:(((X0 > nat) > (X0 > $o) > X0))).
% 4.67/1.06 thf(func_def_139, type, sK88: ((nat > $o) > nat > nat)).
% 4.67/1.06 thf(func_def_140, type, sK89: ((nat > $o) > nat > nat)).
% 4.67/1.06 thf(func_def_141, type, sK90: ((nat > $o) > nat > nat)).
% 4.67/1.06 thf(func_def_142, type, sK91: ((nat > $o) > nat > nat)).
% 4.67/1.06 thf(func_def_143, type, sK92: ((nat > $o) > nat)).
% 4.67/1.06 thf(func_def_144, type, sK93: ((nat > $o) > nat)).
% 4.67/1.06 thf(func_def_145, type, sK94: ((nat > nat > $o) > nat)).
% 4.67/1.06 thf(func_def_146, type, sK95: ((nat > nat > $o) > nat)).
% 4.67/1.06 thf(func_def_147, type, sK96: ((nat > nat > $o) > nat)).
% 4.67/1.06 thf(func_def_148, type, sK97: ((nat > nat > $o) > nat)).
% 4.67/1.06 thf(func_def_149, type, sK98: (nat > (nat > $o) > nat)).
% 4.67/1.06 thf(func_def_150, type, sK99: (nat > (nat > $o) > nat)).
% 4.67/1.06 thf(func_def_151, type, sK100: ((nat > $o) > nat)).
% 4.67/1.06 thf(func_def_152, type, sK101: !>[X0: $tType]:((nat > list @ X0))).
% 4.67/1.06 thf(func_def_153, type, sK102: ((nat > $o) > nat)).
% 4.67/1.06 thf(func_def_154, type, sK103: (nat > (nat > $o) > nat > nat)).
% 4.67/1.06 thf(f1,axiom,(
% 4.67/1.06 (ord_less @ nat @ n1 @ (size_size @ list @ configuration_ext @ p @ v @ s @ product_unit @ (fe @ index)))),
% 4.67/1.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_Occ3_H)).
% 4.67/1.06 thf(f2,axiom,(
% 4.67/1.06 ! [X0 : nat] : ((ord_less @ nat @ X0 @ (size_size @ list @ configuration_ext @ p @ v @ s @ product_unit @ (fe @ index))) => (((nth @ configuration_ext @ p @ v @ s @ product_unit @ (fe @ index) @ X0)) = ((nth @ configuration_ext @ p @ v @ s @ product_unit @ (fe @ (suc @ index)) @ X0))))),
% 4.67/1.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1_SameCfgOnLow)).
% 4.67/1.06 thf(f158,axiom,(
% 4.67/1.06 ! [X0 : nat,X2 : nat,X1 : nat] : ((ord_less @ nat @ X0 @ X1) => (ord_less @ nat @ (minus_minus @ nat @ X0 @ X2) @ X1))),
% 4.67/1.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_157_less__imp__diff__less)).
% 4.67/1.06 thf(f268,conjecture,(
% 4.67/1.06 (((nth @ configuration_ext @ p @ v @ s @ product_unit @ (fe @ (suc @ index)) @ (minus_minus @ nat @ n1 @ one_one @ nat))) = ((nth @ configuration_ext @ p @ v @ s @ product_unit @ (fe @ index) @ (minus_minus @ nat @ n1 @ one_one @ nat))))),
% 4.67/1.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0)).
% 4.67/1.06 thf(f269,negated_conjecture,(
% 4.67/1.06 ~ (((nth @ configuration_ext @ p @ v @ s @ product_unit @ (fe @ (suc @ index)) @ (minus_minus @ nat @ n1 @ one_one @ nat))) = ((nth @ configuration_ext @ p @ v @ s @ product_unit @ (fe @ index) @ (minus_minus @ nat @ n1 @ one_one @ nat))))),
% 4.67/1.06 inference(negated_conjecture,[status(cth)],[f268])).
% 4.67/1.06 thf(f288,plain,(
% 4.67/1.06 ! [X0 : nat] : ((ord_less @ nat @ X0 @ (size_size @ list @ configuration_ext @ p @ v @ s @ product_unit @ (fe @ index))) => (((nth @ configuration_ext @ p @ v @ s @ product_unit @ (fe @ index) @ X0)) = ((nth @ configuration_ext @ p @ v @ s @ product_unit @ (fe @ (suc @ index)) @ X0))))),
% 4.67/1.06 inference(rectify,[],[f2])).
% 4.67/1.06 thf(f289,plain,(
% 4.67/1.06 ! [X0 : nat] : ((((ord_less @ nat @ X0 @ (size_size @ list @ configuration_ext @ p @ v @ s @ product_unit @ (fe @ index)))) = $true) => (((nth @ configuration_ext @ p @ v @ s @ product_unit @ (fe @ index) @ X0)) = ((nth @ configuration_ext @ p @ v @ s @ product_unit @ (fe @ (suc @ index)) @ X0))))),
% 4.67/1.06 inference(fool_elimination,[],[f288])).
% 4.67/1.06 thf(f360,plain,(
% 4.67/1.06 (ord_less @ nat @ n1 @ (size_size @ list @ configuration_ext @ p @ v @ s @ product_unit @ (fe @ index)))),
% 4.67/1.06 inference(rectify,[],[f1])).
% 4.67/1.06 thf(f361,plain,(
% 4.67/1.06 (((ord_less @ nat @ n1 @ (size_size @ list @ configuration_ext @ p @ v @ s @ product_unit @ (fe @ index)))) = $true)),
% 4.67/1.06 inference(fool_elimination,[],[f360])).
% 4.67/1.06 thf(f456,plain,(
% 4.67/1.06 ! [X0 : nat,X1 : nat,X2 : nat] : ((ord_less @ nat @ X0 @ X2) => (ord_less @ nat @ (minus_minus @ nat @ X0 @ X1) @ X2))),
% 4.67/1.06 inference(rectify,[],[f158])).
% 4.67/1.06 thf(f457,plain,(
% 4.67/1.06 ! [X0 : nat,X2 : nat,X1 : nat] : ((((ord_less @ nat @ X0 @ X2)) = $true) => ($true = ((ord_less @ nat @ (minus_minus @ nat @ X0 @ X1) @ X2))))),
% 4.67/1.06 inference(fool_elimination,[],[f456])).
% 4.67/1.06 thf(f748,plain,(
% 4.67/1.06 (((nth @ configuration_ext @ p @ v @ s @ product_unit @ (fe @ index) @ (minus_minus @ nat @ n1 @ one_one @ nat))) != ((nth @ configuration_ext @ p @ v @ s @ product_unit @ (fe @ (suc @ index)) @ (minus_minus @ nat @ n1 @ one_one @ nat))))),
% 4.67/1.06 inference(flattening,[],[f269])).
% 4.67/1.06 thf(f924,plain,(
% 4.67/1.06 ! [X0 : nat] : ((((nth @ configuration_ext @ p @ v @ s @ product_unit @ (fe @ index) @ X0)) = ((nth @ configuration_ext @ p @ v @ s @ product_unit @ (fe @ (suc @ index)) @ X0))) | (((ord_less @ nat @ X0 @ (size_size @ list @ configuration_ext @ p @ v @ s @ product_unit @ (fe @ index)))) != $true))),
% 4.67/1.06 inference(ennf_transformation,[],[f289])).
% 4.67/1.06 thf(f938,plain,(
% 4.67/1.06 ! [X1 : nat,X0 : nat,X2 : nat] : ((((ord_less @ nat @ X0 @ X2)) != $true) | ($true = ((ord_less @ nat @ (minus_minus @ nat @ X0 @ X1) @ X2))))),
% 4.67/1.06 inference(ennf_transformation,[],[f457])).
% 4.67/1.06 thf(f1153,plain,(
% 4.67/1.06 ! [X0 : nat,X1 : nat,X2 : nat] : ((((ord_less @ nat @ X1 @ X2)) != $true) | (((ord_less @ nat @ (minus_minus @ nat @ X1 @ X0) @ X2)) = $true))),
% 4.67/1.06 inference(rectify,[],[f938])).
% 4.67/1.06 thf(f1265,plain,(
% 4.67/1.06 (((nth @ configuration_ext @ p @ v @ s @ product_unit @ (fe @ index) @ (minus_minus @ nat @ n1 @ one_one @ nat))) != ((nth @ configuration_ext @ p @ v @ s @ product_unit @ (fe @ (suc @ index)) @ (minus_minus @ nat @ n1 @ one_one @ nat))))),
% 4.67/1.06 inference(cnf_transformation,[],[f748])).
% 4.67/1.06 thf(f1321,plain,(
% 4.67/1.06 ( ! [X0 : nat] : ((((nth @ configuration_ext @ p @ v @ s @ product_unit @ (fe @ index) @ X0)) = ((nth @ configuration_ext @ p @ v @ s @ product_unit @ (fe @ (suc @ index)) @ X0))) | (((ord_less @ nat @ X0 @ (size_size @ list @ configuration_ext @ p @ v @ s @ product_unit @ (fe @ index)))) != $true)) )),
% 4.67/1.06 inference(cnf_transformation,[],[f924])).
% 4.67/1.06 thf(f1493,plain,(
% 4.67/1.06 (((ord_less @ nat @ n1 @ (size_size @ list @ configuration_ext @ p @ v @ s @ product_unit @ (fe @ index)))) = $true)),
% 4.67/1.06 inference(cnf_transformation,[],[f361])).
% 4.67/1.06 thf(f1555,plain,(
% 4.67/1.06 ( ! [X2 : nat,X0 : nat,X1 : nat] : ((((ord_less @ nat @ (minus_minus @ nat @ X1 @ X0) @ X2)) = $true) | (((ord_less @ nat @ X1 @ X2)) != $true)) )),
% 4.67/1.06 inference(cnf_transformation,[],[f1153])).
% 4.67/1.06 thf(f1611,plain,(
% 4.67/1.06 (((nth @ configuration_ext @ p @ v @ s @ product_unit @ (fe @ index) @ (minus_minus @ nat @ n1 @ one_one @ nat))) != ((nth @ configuration_ext @ p @ v @ s @ product_unit @ (fe @ index) @ (minus_minus @ nat @ n1 @ one_one @ nat)))) | (((ord_less @ nat @ (minus_minus @ nat @ n1 @ one_one @ nat) @ (size_size @ list @ configuration_ext @ p @ v @ s @ product_unit @ (fe @ index)))) != $true)),
% 4.67/1.06 inference(constrained_superposition,[],[f1265,f1321])).
% 4.67/1.06 thf(f1614,plain,(
% 4.67/1.06 (((ord_less @ nat @ (minus_minus @ nat @ n1 @ one_one @ nat) @ (size_size @ list @ configuration_ext @ p @ v @ s @ product_unit @ (fe @ index)))) != $true)),
% 4.67/1.06 inference(trivial_inequality_removal,[],[f1611])).
% 4.67/1.06 thf(f1635,plain,(
% 4.67/1.06 (((ord_less @ nat @ n1 @ (size_size @ list @ configuration_ext @ p @ v @ s @ product_unit @ (fe @ index)))) != $true) | ($true != $true)),
% 4.67/1.06 inference(constrained_superposition,[],[f1614,f1555])).
% 4.67/1.06 thf(f1645,plain,(
% 4.67/1.06 (((ord_less @ nat @ n1 @ (size_size @ list @ configuration_ext @ p @ v @ s @ product_unit @ (fe @ index)))) != $true)),
% 4.67/1.06 inference(trivial_inequality_removal,[],[f1635])).
% 4.67/1.06 thf(f1660,plain,(
% 4.67/1.06 $false),
% 4.67/1.06 inference(forward_subsumption_resolution,[],[f1645,f1493])).
% 4.67/1.06 % SZS output end Proof for theBenchmark
% 4.67/1.06 % (3319108)------------------------------
% 4.67/1.06 % (3319108)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.67/1.06 % (3319108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.67/1.06 % (3319108)CaDiCaL version: 2.1.3
% 4.67/1.06 % (3319108)Termination reason: Refutation
% 4.67/1.06 % (3319108)Time elapsed: 0.104 s
% 4.67/1.06 % (3319108)Peak memory usage: 14 MB
% 4.67/1.06 % (3319108)Instructions burned: 122 (million)
% 4.67/1.06 % (3319011)Success in time 0.678 s
% 4.67/1.06 % Vampire exiting
%------------------------------------------------------------------------------