%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP059^1 : 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 : 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:08:09 AM UTC 2026
% Result : Theorem 1.93s 0.58s
% Output : Refutation 1.93s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP059^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n016.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Tue Sep 29 19:49:35 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running higher-order theorem proving
% 0.21/0.27 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.52/0.42 % (820602)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.52/0.42 % (820611)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=121367662:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.52/0.42 % (820613)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.52/0.42 % (820613)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.52/0.42 % (820607)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=4089005187:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.52/0.42 % (820611)Instruction limit reached!
% 0.52/0.42 % (820611)------------------------------
% 0.52/0.42 % (820611)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.52/0.42 % (820611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.52/0.42 % (820611)CaDiCaL version: 2.1.3
% 0.52/0.42 % (820611)Termination reason: Instruction limit
% 0.52/0.42 % (820611)Termination phase: Preprocessing 2
% 0.52/0.42 % (820611)Time elapsed: 0.006 s
% 0.52/0.42 % (820611)Peak memory usage: 10 MB
% 0.52/0.42 % (820611)Instructions burned: 24 (million)
% 0.52/0.42 % (820608)lrs+10_16_si=on:nwc=1.5:random_seed=2336544616:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.52/0.42 % (820609)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=1066335820:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.52/0.42 % (820610)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=4198451900: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.52/0.42 % (820612)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=565878899:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.52/0.42 % (820613)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=51937203:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.52/0.42 % (820609)Instruction limit reached!
% 0.52/0.42 % (820609)------------------------------
% 0.52/0.42 % (820609)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.52/0.42 % (820609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.52/0.42 % (820609)CaDiCaL version: 2.1.3
% 0.52/0.42 % (820609)Termination reason: Instruction limit
% 0.52/0.42 % (820609)Termination phase: shuffling
% 0.52/0.42 % (820609)Time elapsed: 0.002 s
% 0.52/0.42 % (820609)Peak memory usage: 10 MB
% 0.52/0.42 % (820609)Instructions burned: 4 (million)
% 0.52/0.42 % (820608)Instruction limit reached!
% 0.52/0.42 % (820608)------------------------------
% 0.52/0.42 % (820608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.52/0.42 % (820608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.52/0.42 % (820608)CaDiCaL version: 2.1.3
% 0.52/0.42 % (820608)Termination reason: Instruction limit
% 0.52/0.42 % (820608)Termination phase: Property scanning
% 0.52/0.42 % (820608)Time elapsed: 0.009 s
% 0.52/0.42 % (820608)Peak memory usage: 10 MB
% 0.52/0.42 % (820608)Instructions burned: 20 (million)
% 0.52/0.42 % (820618)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=60806450:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.52/0.42 % (820618)Instruction limit reached!
% 0.52/0.42 % (820618)------------------------------
% 0.52/0.42 % (820618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.52/0.42 % (820618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.52/0.42 % (820618)CaDiCaL version: 2.1.3
% 0.52/0.42 % (820618)Termination reason: Instruction limit
% 0.52/0.42 % (820618)Termination phase: shuffling
% 0.52/0.42 % (820618)Time elapsed: 0.002 s
% 0.52/0.42 % (820618)Peak memory usage: 10 MB
% 0.52/0.42 % (820618)Instructions burned: 9 (million)
% 0.52/0.42 % (820622)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=2120634288:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.52/0.42 % (820625)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=1886159934:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.52/0.45 % (820623)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.52/0.45 % (820622)Instruction limit reached!
% 0.52/0.45 % (820622)------------------------------
% 0.52/0.45 % (820622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.52/0.45 % (820622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.52/0.45 % (820622)CaDiCaL version: 2.1.3
% 0.52/0.45 % (820622)Termination reason: Instruction limit
% 0.52/0.45 % (820622)Termination phase: shuffling
% 0.52/0.45 % (820622)Time elapsed: 0.003 s
% 0.52/0.45 % (820622)Peak memory usage: 10 MB
% 0.52/0.45 % (820622)Instructions burned: 5 (million)
% 0.52/0.45 % (820625)Instruction limit reached!
% 0.52/0.45 % (820625)------------------------------
% 0.52/0.45 % (820625)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.52/0.45 % (820625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.52/0.45 % (820625)CaDiCaL version: 2.1.3
% 0.52/0.45 % (820625)Termination reason: Instruction limit
% 0.52/0.45 % (820625)Termination phase: Property scanning
% 0.52/0.45 % (820625)Time elapsed: 0.003 s
% 0.52/0.45 % (820625)Peak memory usage: 10 MB
% 0.52/0.45 % (820625)Instructions burned: 15 (million)
% 0.52/0.45 % (820623)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2885530941:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.52/0.45 % (820623)Instruction limit reached!
% 0.52/0.45 % (820623)------------------------------
% 0.52/0.45 % (820623)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.52/0.45 % (820623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.52/0.45 % (820623)CaDiCaL version: 2.1.3
% 0.52/0.45 % (820623)Termination reason: Instruction limit
% 0.52/0.45 % (820623)Termination phase: shuffling
% 0.52/0.45 % (820623)Time elapsed: 0.004 s
% 0.52/0.45 % (820623)Peak memory usage: 10 MB
% 0.52/0.45 % (820623)Instructions burned: 9 (million)
% 0.52/0.45 % (820612)Instruction limit reached!
% 0.52/0.45 % (820612)------------------------------
% 0.52/0.45 % (820612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.52/0.45 % (820612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.52/0.45 % (820612)CaDiCaL version: 2.1.3
% 0.52/0.45 % (820612)Termination reason: Instruction limit
% 0.52/0.45 % (820612)Termination phase: Property scanning
% 0.52/0.45 % (820612)Time elapsed: 0.035 s
% 0.52/0.45 % (820612)Peak memory usage: 11 MB
% 0.52/0.45 % (820612)Instructions burned: 77 (million)
% 0.52/0.45 % (820630)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=320437605:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.52/0.45 % (820628)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.52/0.45 % (820628)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.52/0.45 % (820628)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=603704279:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 0.52/0.45 % (820632)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 0.52/0.45 % (820631)lrs+10_1_si=on:cs=on:random_seed=2355652653:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.52/0.45 % (820632)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=726034179:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.52/0.45 % (820632)Instruction limit reached!
% 0.52/0.45 % (820632)------------------------------
% 0.52/0.45 % (820632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.52/0.45 % (820632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.23/0.48 % (820632)CaDiCaL version: 2.1.3
% 1.23/0.48 % (820632)Termination reason: Instruction limit
% 1.23/0.48 % (820632)Termination phase: shuffling
% 1.23/0.48 % (820632)Time elapsed: 0.002 s
% 1.23/0.48 % (820632)Peak memory usage: 10 MB
% 1.23/0.48 % (820632)Instructions burned: 4 (million)
% 1.23/0.48 % (820631)Instruction limit reached!
% 1.23/0.48 % (820631)------------------------------
% 1.23/0.48 % (820631)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.23/0.48 % (820631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.23/0.48 % (820631)CaDiCaL version: 2.1.3
% 1.23/0.48 % (820631)Termination reason: Instruction limit
% 1.23/0.48 % (820631)Termination phase: shuffling
% 1.23/0.48 % (820631)Time elapsed: 0.004 s
% 1.23/0.48 % (820631)Peak memory usage: 10 MB
% 1.23/0.48 % (820631)Instructions burned: 8 (million)
% 1.23/0.48 % (820628)Instruction limit reached!
% 1.23/0.48 % (820628)------------------------------
% 1.23/0.48 % (820628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.23/0.48 % (820628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.23/0.48 % (820628)CaDiCaL version: 2.1.3
% 1.23/0.48 % (820628)Termination reason: Instruction limit
% 1.23/0.48 % (820628)Termination phase: Property scanning
% 1.23/0.48 % (820628)Time elapsed: 0.013 s
% 1.23/0.48 % (820628)Peak memory usage: 10 MB
% 1.23/0.48 % (820628)Instructions burned: 29 (million)
% 1.23/0.48 % (820630)Instruction limit reached!
% 1.23/0.48 % (820630)------------------------------
% 1.23/0.48 % (820630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.23/0.48 % (820630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.23/0.48 % (820630)CaDiCaL version: 2.1.3
% 1.23/0.48 % (820630)Termination reason: Instruction limit
% 1.23/0.48 % (820630)Termination phase: Property scanning
% 1.23/0.48 % (820630)Time elapsed: 0.019 s
% 1.23/0.48 % (820630)Peak memory usage: 11 MB
% 1.23/0.48 % (820630)Instructions burned: 89 (million)
% 1.23/0.48 % (820607)Instruction limit reached!
% 1.23/0.48 % (820607)------------------------------
% 1.23/0.48 % (820607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.23/0.48 % (820607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.23/0.48 % (820607)CaDiCaL version: 2.1.3
% 1.23/0.48 % (820607)Termination reason: Instruction limit
% 1.23/0.48 % (820607)Termination phase: Saturation
% 1.23/0.48 % (820607)Time elapsed: 0.071 s
% 1.23/0.48 % (820607)Peak memory usage: 12 MB
% 1.23/0.48 % (820607)Instructions burned: 87 (million)
% 1.23/0.48 % (820640)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=2249580165:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.23/0.48 % (820640)Instruction limit reached!
% 1.23/0.48 % (820640)------------------------------
% 1.23/0.48 % (820640)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.23/0.48 % (820640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.23/0.48 % (820640)CaDiCaL version: 2.1.3
% 1.23/0.48 % (820640)Termination reason: Instruction limit
% 1.23/0.48 % (820640)Termination phase: Property scanning
% 1.23/0.48 % (820640)Time elapsed: 0.003 s
% 1.23/0.48 % (820640)Peak memory usage: 10 MB
% 1.23/0.48 % (820640)Instructions burned: 15 (million)
% 1.23/0.48 % (820637)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=4246647758:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/38Mi)
% 1.23/0.48 % (820613)Instruction limit reached!
% 1.23/0.48 % (820613)------------------------------
% 1.23/0.48 % (820613)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.23/0.48 % (820613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.23/0.48 % (820613)CaDiCaL version: 2.1.3
% 1.23/0.48 % (820613)Termination reason: Instruction limit
% 1.23/0.48 % (820613)Termination phase: Saturation
% 1.23/0.48 % (820613)Time elapsed: 0.076 s
% 1.23/0.48 % (820613)Peak memory usage: 14 MB
% 1.23/0.48 % (820613)Instructions burned: 157 (million)
% 1.23/0.48 % (820638)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=2728111242:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 1.23/0.48 % (820639)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=3447674696:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 1.23/0.48 % (820643)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=4106217613:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.23/0.56 % (820643)Instruction limit reached!
% 1.23/0.56 % (820643)------------------------------
% 1.23/0.56 % (820643)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.23/0.56 % (820643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.23/0.56 % (820643)CaDiCaL version: 2.1.3
% 1.23/0.56 % (820643)Termination reason: Instruction limit
% 1.23/0.56 % (820643)Termination phase: Property scanning
% 1.23/0.56 % (820643)Time elapsed: 0.004 s
% 1.23/0.56 % (820643)Peak memory usage: 10 MB
% 1.23/0.56 % (820643)Instructions burned: 15 (million)
% 1.23/0.56 % (820641)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=753762485:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 1.23/0.56 % (820639)Instruction limit reached!
% 1.23/0.56 % (820639)------------------------------
% 1.23/0.56 % (820639)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.23/0.56 % (820639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.23/0.56 % (820639)CaDiCaL version: 2.1.3
% 1.23/0.56 % (820639)Termination reason: Instruction limit
% 1.23/0.56 % (820639)Termination phase: SInE selection
% 1.23/0.56 % (820639)Time elapsed: 0.012 s
% 1.23/0.56 % (820639)Peak memory usage: 11 MB
% 1.23/0.56 % (820639)Instructions burned: 27 (million)
% 1.23/0.56 % (820637)Instruction limit reached!
% 1.23/0.56 % (820637)------------------------------
% 1.23/0.56 % (820637)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.23/0.56 % (820637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.23/0.56 % (820637)CaDiCaL version: 2.1.3
% 1.23/0.56 % (820637)Termination reason: Instruction limit
% 1.23/0.56 % (820637)Termination phase: Property scanning
% 1.23/0.56 % (820637)Time elapsed: 0.018 s
% 1.23/0.56 % (820637)Peak memory usage: 11 MB
% 1.23/0.56 % (820637)Instructions burned: 39 (million)
% 1.23/0.56 % (820645)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=2893944971:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2998 on theBenchmark for (2998ds/2Mi)
% 1.23/0.56 % (820645)Instruction limit reached!
% 1.23/0.56 % (820645)------------------------------
% 1.23/0.56 % (820645)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.23/0.56 % (820645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.23/0.56 % (820645)CaDiCaL version: 2.1.3
% 1.23/0.56 % (820645)Termination reason: Instruction limit
% 1.23/0.56 % (820645)Termination phase: shuffling
% 1.23/0.56 % (820645)Time elapsed: 0.002 s
% 1.23/0.56 % (820645)Peak memory usage: 10 MB
% 1.23/0.56 % (820645)Instructions burned: 3 (million)
% 1.23/0.56 % (820650)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3809895434:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.23/0.56 % (820650)Instruction limit reached!
% 1.23/0.56 % (820650)------------------------------
% 1.23/0.56 % (820650)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.23/0.56 % (820650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.23/0.56 % (820650)CaDiCaL version: 2.1.3
% 1.23/0.56 % (820650)Termination reason: Instruction limit
% 1.23/0.56 % (820650)Termination phase: Property scanning
% 1.23/0.56 % (820650)Time elapsed: 0.006 s
% 1.23/0.56 % (820650)Peak memory usage: 10 MB
% 1.23/0.56 % (820650)Instructions burned: 26 (million)
% 1.23/0.56 % (820652)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=1944559750:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 1.23/0.56 % (820654)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
% 1.23/0.56 % (820654)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 1.23/0.56 % (820656)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 1.23/0.56 % (820651)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=2878724988:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.23/0.56 % (820654)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=3610397098:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.93/0.58 % (820656)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=2924640292:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.93/0.58 % (820656)Instruction limit reached!
% 1.93/0.58 % (820656)------------------------------
% 1.93/0.58 % (820656)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.93/0.58 % (820656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.93/0.58 % (820656)CaDiCaL version: 2.1.3
% 1.93/0.58 % (820656)Termination reason: Instruction limit
% 1.93/0.58 % (820656)Termination phase: shuffling
% 1.93/0.58 % (820656)Time elapsed: 0.003 s
% 1.93/0.58 % (820656)Peak memory usage: 10 MB
% 1.93/0.58 % (820656)Instructions burned: 12 (million)
% 1.93/0.58 % (820654)Instruction limit reached!
% 1.93/0.58 % (820654)------------------------------
% 1.93/0.58 % (820654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.93/0.58 % (820654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.93/0.58 % (820654)CaDiCaL version: 2.1.3
% 1.93/0.58 % (820654)Termination reason: Instruction limit
% 1.93/0.58 % (820654)Termination phase: shuffling
% 1.93/0.58 % (820654)Time elapsed: 0.007 s
% 1.93/0.58 % (820654)Peak memory usage: 10 MB
% 1.93/0.58 % (820654)Instructions burned: 14 (million)
% 1.93/0.58 % (820661)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=4233696850:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 1.93/0.58 % (820651)Instruction limit reached!
% 1.93/0.58 % (820651)------------------------------
% 1.93/0.58 % (820651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.93/0.58 % (820651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.93/0.58 % (820651)CaDiCaL version: 2.1.3
% 1.93/0.58 % (820651)Termination reason: Instruction limit
% 1.93/0.58 % (820651)Termination phase: Preprocessing 1
% 1.93/0.58 % (820651)Time elapsed: 0.020 s
% 1.93/0.58 % (820651)Peak memory usage: 10 MB
% 1.93/0.58 % (820651)Instructions burned: 24 (million)
% 1.93/0.58 % (820652)Instruction limit reached!
% 1.93/0.58 % (820652)------------------------------
% 1.93/0.58 % (820652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.93/0.58 % (820652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.93/0.58 % (820652)CaDiCaL version: 2.1.3
% 1.93/0.58 % (820652)Termination reason: Instruction limit
% 1.93/0.58 % (820652)Termination phase: Property scanning
% 1.93/0.58 % (820652)Time elapsed: 0.026 s
% 1.93/0.58 % (820652)Peak memory usage: 11 MB
% 1.93/0.58 % (820652)Instructions burned: 60 (million)
% 1.93/0.58 % (820661)Instruction limit reached!
% 1.93/0.58 % (820661)------------------------------
% 1.93/0.58 % (820661)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.93/0.58 % (820661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.93/0.58 % (820661)CaDiCaL version: 2.1.3
% 1.93/0.58 % (820661)Termination reason: Instruction limit
% 1.93/0.58 % (820661)Termination phase: Property scanning
% 1.93/0.58 % (820661)Time elapsed: 0.008 s
% 1.93/0.58 % (820661)Peak memory usage: 10 MB
% 1.93/0.58 % (820661)Instructions burned: 33 (million)
% 1.93/0.58 % (820662)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=1303283959:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 1.93/0.58 % (820664)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=241620326:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.93/0.58 % (820662)Instruction limit reached!
% 1.93/0.58 % (820662)------------------------------
% 1.93/0.58 % (820662)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.93/0.58 % (820662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.93/0.58 % (820662)CaDiCaL version: 2.1.3
% 1.93/0.58 % (820662)Termination reason: Instruction limit
% 1.93/0.58 % (820662)Termination phase: shuffling
% 1.93/0.58 % (820662)Time elapsed: 0.004 s
% 1.93/0.58 % (820662)Peak memory usage: 10 MB
% 1.93/0.58 % (820662)Instructions burned: 8 (million)
% 1.93/0.58 % (820664)Instruction limit reached!
% 1.93/0.58 % (820664)------------------------------
% 1.93/0.58 % (820664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.93/0.58 % (820664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.93/0.58 % (820664)CaDiCaL version: 2.1.3
% 1.93/0.58 % (820664)Termination reason: Instruction limit
% 1.93/0.58 % (820664)Termination phase: Property scanning
% 1.93/0.58 % (820664)Time elapsed: 0.005 s
% 1.93/0.58 % (820664)Peak memory usage: 10 MB
% 1.93/0.58 % (820664)Instructions burned: 23 (million)
% 1.93/0.58 % (820665)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=1017880695:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 1.93/0.58 % (820666)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=1503702413:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 1.93/0.58 % (820670)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=2552858917:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/193Mi)
% 1.93/0.58 % (820665)Instruction limit reached!
% 1.93/0.58 % (820665)------------------------------
% 1.93/0.58 % (820665)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.93/0.58 % (820665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.93/0.58 % (820665)CaDiCaL version: 2.1.3
% 1.93/0.58 % (820665)Termination reason: Instruction limit
% 1.93/0.58 % (820665)Termination phase: Property scanning
% 1.93/0.58 % (820665)Time elapsed: 0.009 s
% 1.93/0.58 % (820665)Peak memory usage: 10 MB
% 1.93/0.58 % (820665)Instructions burned: 22 (million)
% 1.93/0.58 % (820669)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=918282448:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2997 on theBenchmark for (2997ds/143Mi)
% 1.93/0.58 % (820674)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=4131164394:i=42:hud=10:rtra=on_2997 on theBenchmark for (2997ds/42Mi)
% 1.93/0.58 % (820638)Instruction limit reached!
% 1.93/0.58 % (820638)------------------------------
% 1.93/0.58 % (820638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.93/0.58 % (820638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.93/0.58 % (820638)CaDiCaL version: 2.1.3
% 1.93/0.58 % (820638)Termination reason: Instruction limit
% 1.93/0.58 % (820638)Termination phase: Saturation
% 1.93/0.58 % (820638)Time elapsed: 0.126 s
% 1.93/0.58 % (820638)Peak memory usage: 14 MB
% 1.93/0.58 % (820638)Instructions burned: 251 (million)
% 1.93/0.58 % (820674)Instruction limit reached!
% 1.93/0.58 % (820674)------------------------------
% 1.93/0.58 % (820674)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.93/0.58 % (820674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.93/0.58 % (820674)CaDiCaL version: 2.1.3
% 1.93/0.58 % (820674)Termination reason: Instruction limit
% 1.93/0.58 % (820674)Termination phase: Property scanning
% 1.93/0.58 % (820674)Time elapsed: 0.019 s
% 1.93/0.58 % (820674)Peak memory usage: 11 MB
% 1.93/0.58 % (820674)Instructions burned: 42 (million)
% 1.93/0.58 % (820670)Instruction limit reached!
% 1.93/0.58 % (820670)------------------------------
% 1.93/0.58 % (820670)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.93/0.58 % (820670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.93/0.58 % (820670)CaDiCaL version: 2.1.3
% 1.93/0.58 % (820670)Termination reason: Instruction limit
% 1.93/0.58 % (820670)Termination phase: Saturation
% 1.93/0.58 % (820670)Time elapsed: 0.054 s
% 1.93/0.58 % (820670)Peak memory usage: 14 MB
% 1.93/0.58 % (820670)Instructions burned: 195 (million)
% 1.93/0.58 % (820677)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.93/0.58 % (820678)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=1796107163:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/181Mi)
% 1.93/0.58 % (820677)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=4286830551:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2997 on theBenchmark for (2997ds/7Mi)
% 1.93/0.58 % (820677)Instruction limit reached!
% 1.93/0.58 % (820677)------------------------------
% 1.93/0.58 % (820677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.93/0.58 % (820677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.93/0.58 % (820677)CaDiCaL version: 2.1.3
% 1.93/0.58 % (820677)Termination reason: Instruction limit
% 1.93/0.58 % (820677)Termination phase: shuffling
% 1.93/0.58 % (820677)Time elapsed: 0.004 s
% 1.93/0.58 % (820677)Peak memory usage: 10 MB
% 1.93/0.58 % (820677)Instructions burned: 8 (million)
% 1.93/0.58 % (820679)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=1754024921:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2997 on theBenchmark for (2997ds/169Mi)
% 1.93/0.58 % (820669)Instruction limit reached!
% 1.93/0.58 % (820669)------------------------------
% 1.93/0.58 % (820669)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.93/0.58 % (820669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.93/0.58 % (820669)CaDiCaL version: 2.1.3
% 1.93/0.58 % (820669)Termination reason: Instruction limit
% 1.93/0.58 % (820669)Termination phase: Saturation
% 1.93/0.58 % (820669)Time elapsed: 0.069 s
% 1.93/0.58 % (820669)Peak memory usage: 14 MB
% 1.93/0.58 % (820669)Instructions burned: 143 (million)
% 1.93/0.58 % (820610) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-820602-820610"...
% 1.93/0.58 % (820683)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 1.93/0.58 % (820683)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=3266165037:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2997 on theBenchmark for (2997ds/6Mi)
% 1.93/0.58 % (820610)...printing done.
% 1.93/0.58 % (820610)Refutation found. Thanks to Tanya!
% 1.93/0.58 % SZS status Theorem for theBenchmark
% 1.93/0.58 % SZS output start Proof for theBenchmark
% 1.93/0.58 thf(type_def_5, type, list_c1059388851t_unit: $tType).
% 1.93/0.58 thf(type_def_6, type, config256849571t_unit: $tType).
% 1.93/0.58 thf(type_def_7, type, list_message_p_v: $tType).
% 1.93/0.58 thf(type_def_8, type, set_message_p_v: $tType).
% 1.93/0.58 thf(type_def_9, type, message_p_v: $tType).
% 1.93/0.58 thf(type_def_10, type, nat: $tType).
% 1.93/0.58 thf(type_def_11, type, p: $tType).
% 1.93/0.58 thf(type_def_12, type, sTfun: ($tType * $tType) > $tType).
% 1.93/0.58 thf(func_def_0, type, msgs_p1029620568t_unit: (config256849571t_unit > message_p_v > nat)).
% 1.93/0.58 thf(func_def_1, type, enabled_p_v_s: (config256849571t_unit > message_p_v > $o)).
% 1.93/0.58 thf(func_def_2, type, isReceiverOf_p_v: (p > message_p_v > $o)).
% 1.93/0.58 thf(func_def_3, type, firstO1414030372_p_v_s: (list_c1059388851t_unit > list_message_p_v > message_p_v > nat > $o)).
% 1.93/0.58 thf(func_def_4, type, minus_minus_nat: (nat > nat > nat)).
% 1.93/0.58 thf(func_def_5, type, one_one_nat: nat).
% 1.93/0.58 thf(func_def_6, type, zero_zero_nat: nat).
% 1.93/0.58 thf(func_def_7, type, prefix1615116500t_unit: (list_c1059388851t_unit > list_c1059388851t_unit > $o)).
% 1.93/0.58 thf(func_def_8, type, prefix47729710ge_p_v: (list_message_p_v > list_message_p_v > $o)).
% 1.93/0.58 thf(func_def_9, type, last_c571238084t_unit: (list_c1059388851t_unit > config256849571t_unit)).
% 1.93/0.58 thf(func_def_10, type, last_message_p_v: (list_message_p_v > message_p_v)).
% 1.93/0.58 thf(func_def_11, type, nil_co1338500125t_unit: list_c1059388851t_unit).
% 1.93/0.58 thf(func_def_12, type, nil_message_p_v: list_message_p_v).
% 1.93/0.58 thf(func_def_13, type, nth_co1649820636t_unit: (list_c1059388851t_unit > nat > config256849571t_unit)).
% 1.93/0.58 thf(func_def_14, type, nth_message_p_v: (list_message_p_v > nat > message_p_v)).
% 1.93/0.58 thf(func_def_15, type, suc: (nat > nat)).
% 1.93/0.58 thf(func_def_16, type, size_s1406904903t_unit: (list_c1059388851t_unit > nat)).
% 1.93/0.58 thf(func_def_17, type, size_s1168481041ge_p_v: (list_message_p_v > nat)).
% 1.93/0.58 thf(func_def_18, type, ord_less_nat: (nat > nat > $o)).
% 1.93/0.58 thf(func_def_19, type, ord_less_eq_nat: (nat > nat > $o)).
% 1.93/0.58 thf(func_def_20, type, member_message_p_v: (message_p_v > set_message_p_v > $o)).
% 1.93/0.58 thf(func_def_21, type, fe: (nat > list_c1059388851t_unit)).
% 1.93/0.58 thf(func_def_22, type, firstOccSet: (nat > set_message_p_v)).
% 1.93/0.58 thf(func_def_23, type, ft: (nat > list_message_p_v)).
% 1.93/0.58 thf(func_def_24, type, index: nat).
% 1.93/0.58 thf(func_def_25, type, msgInSet: message_p_v).
% 1.93/0.58 thf(func_def_26, type, msg: message_p_v).
% 1.93/0.58 thf(func_def_27, type, n0: nat).
% 1.93/0.58 thf(func_def_28, type, n1: nat).
% 1.93/0.58 thf(func_def_29, type, nMsg: nat).
% 1.93/0.58 thf(func_def_30, type, n: nat).
% 1.93/0.58 thf(func_def_31, type, p2: p).
% 1.93/0.58 thf(func_def_35, type, db1: !>[X0: $tType]:(X0)).
% 1.93/0.58 thf(func_def_36, type, db0: !>[X0: $tType]:(X0)).
% 1.93/0.58 thf(func_def_37, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 1.93/0.58 thf(func_def_38, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 1.93/0.58 thf(func_def_39, type, vAND: ($o > $o > $o)).
% 1.93/0.58 thf(func_def_40, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 1.93/0.58 thf(func_def_41, type, vIMP: ($o > $o > $o)).
% 1.93/0.58 thf(func_def_42, type, db2: !>[X0: $tType]:(X0)).
% 1.93/0.58 thf(func_def_43, type, vOR: ($o > $o > $o)).
% 1.93/0.58 thf(func_def_44, type, vNOT: ($o > $o)).
% 1.93/0.58 thf(func_def_45, type, sK0: (nat > (nat > $o) > nat)).
% 1.93/0.58 thf(func_def_46, type, sK1: ((nat > $o) > nat > nat)).
% 1.93/0.58 thf(func_def_47, type, sK2: (list_message_p_v > list_message_p_v > nat)).
% 1.93/0.58 thf(func_def_48, type, sK3: ((nat > nat) > nat)).
% 1.93/0.58 thf(func_def_49, type, sK4: (nat > (nat > $o) > nat)).
% 1.93/0.58 thf(func_def_50, type, sK5: (nat > (nat > $o) > nat)).
% 1.93/0.58 thf(func_def_51, type, sK6: nat).
% 1.93/0.58 thf(func_def_52, type, sK7: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > config256849571t_unit)).
% 1.93/0.58 thf(func_def_53, type, sK8: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit)).
% 1.93/0.58 thf(func_def_54, type, sK9: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > list_c1059388851t_unit > list_message_p_v > list_message_p_v)).
% 1.93/0.58 thf(func_def_55, type, sK10: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > (config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > nat)).
% 1.93/0.58 thf(func_def_56, type, sK11: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > (config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > list_c1059388851t_unit > list_message_p_v > list_message_p_v)).
% 1.93/0.58 thf(func_def_57, type, sK12: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > (config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > config256849571t_unit)).
% 1.93/0.58 thf(func_def_58, type, sK13: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > (config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit)).
% 1.93/0.58 thf(func_def_59, type, sK14: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > config256849571t_unit)).
% 1.93/0.58 thf(func_def_60, type, sK15: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > list_c1059388851t_unit > list_message_p_v > list_message_p_v)).
% 1.93/0.58 thf(func_def_61, type, sK16: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit)).
% 1.93/0.58 thf(func_def_62, type, sK17: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > (config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > list_c1059388851t_unit > list_message_p_v > list_message_p_v)).
% 1.93/0.58 thf(func_def_63, type, sK18: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > (config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit)).
% 1.93/0.58 thf(func_def_64, type, sK19: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > (config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > nat)).
% 1.93/0.58 thf(func_def_65, type, sK20: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > (config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > config256849571t_unit)).
% 1.93/0.58 thf(func_def_66, type, sK21: (nat > nat > nat)).
% 1.93/0.58 thf(func_def_67, type, sK22: (list_c1059388851t_unit > list_c1059388851t_unit > nat)).
% 1.93/0.58 thf(func_def_68, type, sK23: (nat > nat > (nat > $o) > nat)).
% 1.93/0.58 thf(func_def_69, type, sK24: ((nat > $o) > nat)).
% 1.93/0.58 thf(func_def_70, type, sK25: (nat > (nat > $o) > nat)).
% 1.93/0.58 thf(func_def_71, type, sK26: ((nat > $o) > nat)).
% 1.93/0.59 thf(func_def_72, type, sK27: ((nat > $o) > nat)).
% 1.93/0.59 thf(func_def_73, type, sK28: ((nat > nat) > nat)).
% 1.93/0.59 thf(func_def_74, type, sK29: (nat > (nat > config256849571t_unit > $o) > config256849571t_unit)).
% 1.93/0.59 thf(func_def_75, type, sK30: (list_c1059388851t_unit > nat > (nat > config256849571t_unit > $o) > nat)).
% 1.93/0.59 thf(func_def_76, type, sK31: (nat > (nat > config256849571t_unit > $o) > list_c1059388851t_unit)).
% 1.93/0.59 thf(func_def_77, type, sK32: (nat > (nat > config256849571t_unit > $o) > nat)).
% 1.93/0.59 thf(func_def_78, type, sK33: ((nat > nat) > nat)).
% 1.93/0.59 thf(func_def_79, type, sK34: (nat > nat > (nat > $o) > nat)).
% 1.93/0.59 thf(func_def_80, type, sK35: ((nat > $o) > nat > nat)).
% 1.93/0.59 thf(func_def_81, type, sK36: ((nat > $o) > nat)).
% 1.93/0.59 thf(func_def_82, type, sK37: (nat > nat)).
% 1.93/0.59 thf(func_def_83, type, sK38: (nat > (nat > message_p_v > $o) > message_p_v)).
% 1.93/0.59 thf(func_def_84, type, sK39: (list_message_p_v > (nat > message_p_v > $o) > nat > nat)).
% 1.93/0.59 thf(func_def_85, type, sK40: ((nat > message_p_v > $o) > nat > list_message_p_v)).
% 1.93/0.59 thf(func_def_86, type, sK41: ((nat > message_p_v > $o) > nat > nat)).
% 1.93/0.59 thf(func_def_87, type, sK42: ((nat > nat > $o) > nat)).
% 1.93/0.59 thf(func_def_88, type, sK43: ((nat > nat > $o) > nat)).
% 1.93/0.59 thf(func_def_89, type, sK44: ((nat > nat > $o) > nat)).
% 1.93/0.59 thf(func_def_90, type, sK45: ((nat > nat > $o) > nat)).
% 1.93/0.59 thf(func_def_91, type, sK46: p).
% 1.93/0.59 thf(func_def_92, type, sK47: ((nat > $o) > nat)).
% 1.93/0.59 thf(func_def_93, type, sK48: ((nat > $o) > nat)).
% 1.93/0.59 thf(func_def_94, type, sK49: (nat > (nat > $o) > nat)).
% 1.93/0.59 thf(func_def_95, type, sK50: (nat > nat)).
% 1.93/0.59 thf(func_def_96, type, sK51: ((list_c1059388851t_unit > $o) > list_c1059388851t_unit)).
% 1.93/0.59 thf(func_def_97, type, sK52: ((nat > $o) > nat)).
% 1.93/0.59 thf(func_def_98, type, sK53: (nat > (nat > $o) > nat)).
% 1.93/0.59 thf(func_def_99, type, sK54: (nat > (nat > $o) > nat)).
% 1.93/0.59 thf(func_def_100, type, sK55: (nat > list_c1059388851t_unit)).
% 1.93/0.59 thf(func_def_101, type, sK56: (nat > nat)).
% 1.93/0.59 thf(func_def_102, type, sK57: ((nat > nat > $o) > nat)).
% 1.93/0.59 thf(func_def_103, type, sK58: ((nat > nat > $o) > nat)).
% 1.93/0.59 thf(func_def_104, type, sK59: ((nat > nat > $o) > nat)).
% 1.93/0.59 thf(func_def_105, type, sK60: ((nat > nat > $o) > nat)).
% 1.93/0.59 thf(func_def_106, type, sK61: (nat > nat > nat)).
% 1.93/0.59 thf(func_def_107, type, sK62: ((nat > nat) > nat)).
% 1.93/0.59 thf(func_def_108, type, sK63: ((nat > nat) > nat)).
% 1.93/0.59 thf(func_def_109, type, sK64: p).
% 1.93/0.59 thf(func_def_110, type, sK65: (nat > nat)).
% 1.93/0.59 thf(func_def_111, type, sK66: (nat > nat)).
% 1.93/0.59 thf(func_def_112, type, sK67: nat).
% 1.93/0.59 thf(func_def_113, type, sK68: nat).
% 1.93/0.59 thf(func_def_114, type, sK69: ((nat > $o) > nat)).
% 1.93/0.59 thf(func_def_115, type, sK70: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > (config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > config256849571t_unit)).
% 1.93/0.59 thf(func_def_116, type, sK71: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > (config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit)).
% 1.93/0.59 thf(func_def_117, type, sK72: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > (config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > nat)).
% 1.93/0.59 thf(func_def_118, type, sK73: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > (config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > list_c1059388851t_unit > list_message_p_v > list_message_p_v)).
% 1.93/0.59 thf(func_def_119, type, sK74: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > config256849571t_unit)).
% 1.93/0.59 thf(func_def_120, type, sK75: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit)).
% 1.93/0.59 thf(func_def_121, type, sK76: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > list_c1059388851t_unit > list_message_p_v > list_message_p_v)).
% 1.93/0.59 thf(func_def_122, type, sK77: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > list_c1059388851t_unit > list_message_p_v > list_message_p_v)).
% 1.93/0.59 thf(func_def_123, type, sK78: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit)).
% 1.93/0.59 thf(func_def_124, type, sK79: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > config256849571t_unit)).
% 1.93/0.59 thf(func_def_125, type, sK80: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > (config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > list_c1059388851t_unit > list_message_p_v > list_message_p_v)).
% 1.93/0.59 thf(func_def_126, type, sK81: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > (config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit)).
% 1.93/0.59 thf(func_def_127, type, sK82: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > (config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > nat)).
% 1.93/0.59 thf(func_def_128, type, sK83: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > (config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > config256849571t_unit)).
% 1.93/0.59 thf(func_def_129, type, sK84: (nat > nat > nat)).
% 1.93/0.59 thf(func_def_130, type, sK85: ((list_message_p_v > $o) > list_message_p_v)).
% 1.93/0.59 thf(func_def_131, type, sK86: ((nat > $o) > nat)).
% 1.93/0.59 thf(func_def_132, type, sK87: ((nat > $o) > nat)).
% 1.93/0.59 thf(func_def_133, type, sK88: (nat > (nat > $o) > nat)).
% 1.93/0.59 thf(func_def_134, type, sK89: (nat > (nat > $o) > nat)).
% 1.93/0.59 thf(func_def_135, type, sK90: ((nat > nat) > nat)).
% 1.93/0.59 thf(func_def_136, type, sK91: (nat > (nat > $o) > (nat > $o) > nat)).
% 1.93/0.59 thf(func_def_137, type, sK92: ((nat > $o) > nat > nat)).
% 1.93/0.59 thf(func_def_138, type, sK93: ((nat > $o) > nat > nat)).
% 1.93/0.59 thf(func_def_139, type, sK94: ((nat > $o) > nat)).
% 1.93/0.59 thf(func_def_140, type, sK95: ((nat > $o) > nat)).
% 1.93/0.59 thf(func_def_141, type, sK96: ((nat > $o) > nat > nat)).
% 1.93/0.59 thf(func_def_142, type, sK97: ((nat > $o) > nat > nat)).
% 1.93/0.59 thf(func_def_143, type, sK98: (nat > list_message_p_v)).
% 1.93/0.59 thf(func_def_144, type, sK99: ((nat > nat > $o) > nat)).
% 1.93/0.59 thf(func_def_145, type, sK100: ((nat > nat > $o) > nat)).
% 1.93/0.59 thf(func_def_146, type, sK101: ((nat > nat > $o) > nat)).
% 1.93/0.59 thf(func_def_147, type, sK102: ((nat > nat > $o) > nat)).
% 1.93/0.59 thf(func_def_148, type, sK103: ((nat > nat > $o) > nat)).
% 1.93/0.59 thf(func_def_149, type, sK104: nat).
% 1.93/0.59 thf(func_def_150, type, sK105: (nat > nat > nat)).
% 1.93/0.59 thf(func_def_151, type, sK106: (nat > message_p_v > nat > nat)).
% 1.93/0.59 thf(func_def_153, type, inv_suc_108: (nat > nat)).
% 1.93/0.59 thf(f1,axiom,(
% 1.93/0.59 (ord_less_nat @ zero_zero_nat @ nMsg)),
% 1.93/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_AssumpOcc6_I1_J)).
% 1.93/0.59 thf(f4,axiom,(
% 1.93/0.59 (firstO1414030372_p_v_s @ (fe @ (suc @ index)) @ (ft @ (suc @ index)) @ msg @ nMsg)),
% 1.93/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3_AssumptionSubset_I3_J)).
% 1.93/0.59 thf(f5,axiom,(
% 1.93/0.59 ! [X0 : nat] : ((firstO1414030372_p_v_s @ (fe @ (suc @ index)) @ (ft @ (suc @ index)) @ msg @ X0) => (ord_less_nat @ X0 @ (size_s1406904903t_unit @ (fe @ index))))),
% 1.93/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4_SmallIndex)).
% 1.93/0.59 thf(f8,axiom,(
% 1.93/0.59 ! [X0 : nat] : ((ord_less_nat @ zero_zero_nat @ X0) => (((suc @ (minus_minus_nat @ X0 @ (suc @ zero_zero_nat)))) = X0))),
% 1.93/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7_Suc__pred)).
% 1.93/0.59 thf(f17,axiom,(
% 1.93/0.59 ! [X0 : nat] : ~(ord_less_nat @ X0 @ zero_zero_nat)),
% 1.93/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_16_less__nat__zero__code)).
% 1.93/0.59 thf(f34,axiom,(
% 1.93/0.59 ! [X1 : nat,X0 : nat] : ((X0 != X1) => (~(ord_less_nat @ X0 @ X1) => (ord_less_nat @ X1 @ X0)))),
% 1.93/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_33_linorder__neqE__nat)).
% 1.93/0.59 thf(f126,axiom,(
% 1.93/0.59 ! [X1 : nat,X0 : nat] : ((ord_less_eq_nat @ X0 @ X1) => (((minus_minus_nat @ X0 @ X1)) = zero_zero_nat))),
% 1.93/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_125_diff__is__0__eq_H)).
% 1.93/0.59 thf(f139,axiom,(
% 1.93/0.59 ! [X1 : nat,X0 : nat] : ((ord_less_eq_nat @ X0 @ X1) | (ord_less_eq_nat @ X1 @ X0))),
% 1.93/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_138_nat__le__linear)).
% 1.93/0.59 thf(f193,axiom,(
% 1.93/0.59 ! [X0 : nat,X2 : nat,X1 : nat] : ((ord_less_nat @ X0 @ X1) => ((ord_less_eq_nat @ X2 @ X0) => (ord_less_nat @ (minus_minus_nat @ X0 @ X2) @ (minus_minus_nat @ X1 @ X2))))),
% 1.93/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_192_diff__less__mono)).
% 1.93/0.59 thf(f194,axiom,(
% 1.93/0.59 (one_one_nat = ((suc @ zero_zero_nat)))),
% 1.93/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_193_One__nat__def)).
% 1.93/0.59 thf(f241,axiom,(
% 1.93/0.59 (ord_less_eq_nat @ one_one_nat @ one_one_nat)),
% 1.93/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_240_le__numeral__extra_I4_J)).
% 1.93/0.59 thf(f245,conjecture,(
% 1.93/0.59 (ord_less_nat @ (minus_minus_nat @ nMsg @ (suc @ zero_zero_nat)) @ (minus_minus_nat @ (size_s1406904903t_unit @ (fe @ index)) @ (suc @ zero_zero_nat)))),
% 1.93/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0)).
% 1.93/0.59 thf(f246,negated_conjecture,(
% 1.93/0.59 ~(ord_less_nat @ (minus_minus_nat @ nMsg @ (suc @ zero_zero_nat)) @ (minus_minus_nat @ (size_s1406904903t_unit @ (fe @ index)) @ (suc @ zero_zero_nat)))),
% 1.93/0.59 inference(negated_conjecture,[status(cth)],[f245])).
% 1.93/0.59 thf(f267,plain,(
% 1.93/0.59 ~(ord_less_nat @ (minus_minus_nat @ nMsg @ (suc @ zero_zero_nat)) @ (minus_minus_nat @ (size_s1406904903t_unit @ (fe @ index)) @ (suc @ zero_zero_nat)))),
% 1.93/0.59 inference(rectify,[],[f246])).
% 1.93/0.59 thf(f268,plain,(
% 1.93/0.59 ~ (((ord_less_nat @ (minus_minus_nat @ nMsg @ (suc @ zero_zero_nat)) @ (minus_minus_nat @ (size_s1406904903t_unit @ (fe @ index)) @ (suc @ zero_zero_nat)))) = $true)),
% 1.93/0.59 inference(fool_elimination,[],[f267])).
% 1.93/0.59 thf(f296,plain,(
% 1.93/0.59 ! [X0 : nat] : ~(ord_less_nat @ X0 @ zero_zero_nat)),
% 1.93/0.59 inference(rectify,[],[f17])).
% 1.93/0.59 thf(f297,plain,(
% 1.93/0.59 ! [X0 : nat] : ~ (((ord_less_nat @ X0 @ zero_zero_nat)) = $true)),
% 1.93/0.59 inference(fool_elimination,[],[f296])).
% 1.93/0.59 thf(f326,plain,(
% 1.93/0.59 (firstO1414030372_p_v_s @ (fe @ (suc @ index)) @ (ft @ (suc @ index)) @ msg @ nMsg)),
% 1.93/0.59 inference(rectify,[],[f4])).
% 1.93/0.59 thf(f327,plain,(
% 1.93/0.59 (((firstO1414030372_p_v_s @ (fe @ (suc @ index)) @ (ft @ (suc @ index)) @ msg @ nMsg)) = $true)),
% 1.93/0.59 inference(fool_elimination,[],[f326])).
% 1.93/0.59 thf(f334,plain,(
% 1.93/0.59 ! [X0 : nat] : ((ord_less_nat @ zero_zero_nat @ X0) => (((suc @ (minus_minus_nat @ X0 @ (suc @ zero_zero_nat)))) = X0))),
% 1.93/0.59 inference(rectify,[],[f8])).
% 1.93/0.59 thf(f335,plain,(
% 1.93/0.59 ! [X0 : nat] : ((((ord_less_nat @ zero_zero_nat @ X0)) = $true) => (((suc @ (minus_minus_nat @ X0 @ (suc @ zero_zero_nat)))) = X0))),
% 1.93/0.59 inference(fool_elimination,[],[f334])).
% 1.93/0.59 thf(f338,plain,(
% 1.93/0.59 (ord_less_eq_nat @ one_one_nat @ one_one_nat)),
% 1.93/0.59 inference(rectify,[],[f241])).
% 1.93/0.59 thf(f339,plain,(
% 1.93/0.59 (((ord_less_eq_nat @ one_one_nat @ one_one_nat)) = $true)),
% 1.93/0.59 inference(fool_elimination,[],[f338])).
% 1.93/0.59 thf(f367,plain,(
% 1.93/0.59 ! [X0 : nat] : ((firstO1414030372_p_v_s @ (fe @ (suc @ index)) @ (ft @ (suc @ index)) @ msg @ X0) => (ord_less_nat @ X0 @ (size_s1406904903t_unit @ (fe @ index))))),
% 1.93/0.59 inference(rectify,[],[f5])).
% 1.93/0.59 thf(f368,plain,(
% 1.93/0.59 ! [X0 : nat] : ((((firstO1414030372_p_v_s @ (fe @ (suc @ index)) @ (ft @ (suc @ index)) @ msg @ X0)) = $true) => (((ord_less_nat @ X0 @ (size_s1406904903t_unit @ (fe @ index)))) = $true))),
% 1.93/0.59 inference(fool_elimination,[],[f367])).
% 1.93/0.59 thf(f373,plain,(
% 1.93/0.59 ! [X0 : nat,X1 : nat] : ((X0 != X1) => (~(ord_less_nat @ X1 @ X0) => (ord_less_nat @ X0 @ X1)))),
% 1.93/0.59 inference(rectify,[],[f34])).
% 1.93/0.59 thf(f374,plain,(
% 1.93/0.59 ! [X0 : nat,X1 : nat] : ((X0 != X1) => (~ (((ord_less_nat @ X1 @ X0)) = $true) => (((ord_less_nat @ X0 @ X1)) = $true)))),
% 1.93/0.59 inference(fool_elimination,[],[f373])).
% 1.93/0.59 thf(f496,plain,(
% 1.93/0.59 ! [X0 : nat,X1 : nat] : ((ord_less_eq_nat @ X1 @ X0) | (ord_less_eq_nat @ X0 @ X1))),
% 1.93/0.59 inference(rectify,[],[f139])).
% 1.93/0.59 thf(f497,plain,(
% 1.93/0.59 ! [X1 : nat,X0 : nat] : ((((ord_less_eq_nat @ X0 @ X1)) = $true) | (((ord_less_eq_nat @ X1 @ X0)) = $true))),
% 1.93/0.59 inference(fool_elimination,[],[f496])).
% 1.93/0.59 thf(f562,plain,(
% 1.93/0.59 (ord_less_nat @ zero_zero_nat @ nMsg)),
% 1.93/0.59 inference(rectify,[],[f1])).
% 1.93/0.59 thf(f563,plain,(
% 1.93/0.59 (((ord_less_nat @ zero_zero_nat @ nMsg)) = $true)),
% 1.93/0.59 inference(fool_elimination,[],[f562])).
% 1.93/0.59 thf(f605,plain,(
% 1.93/0.59 ! [X0 : nat,X1 : nat] : ((ord_less_eq_nat @ X1 @ X0) => (zero_zero_nat = ((minus_minus_nat @ X1 @ X0))))),
% 1.93/0.59 inference(rectify,[],[f126])).
% 1.93/0.59 thf(f606,plain,(
% 1.93/0.59 ! [X1 : nat,X0 : nat] : ((((ord_less_eq_nat @ X1 @ X0)) = $true) => (zero_zero_nat = ((minus_minus_nat @ X1 @ X0))))),
% 1.93/0.59 inference(fool_elimination,[],[f605])).
% 1.93/0.59 thf(f619,plain,(
% 1.93/0.59 ! [X0 : nat,X1 : nat,X2 : nat] : ((ord_less_nat @ X0 @ X2) => ((ord_less_eq_nat @ X1 @ X0) => (ord_less_nat @ (minus_minus_nat @ X0 @ X1) @ (minus_minus_nat @ X2 @ X1))))),
% 1.93/0.59 inference(rectify,[],[f193])).
% 1.93/0.59 thf(f620,plain,(
% 1.93/0.59 ! [X2 : nat,X0 : nat,X1 : nat] : ((((ord_less_nat @ X0 @ X2)) = $true) => ((((ord_less_eq_nat @ X1 @ X0)) = $true) => (((ord_less_nat @ (minus_minus_nat @ X0 @ X1) @ (minus_minus_nat @ X2 @ X1))) = $true)))),
% 1.93/0.59 inference(fool_elimination,[],[f619])).
% 1.93/0.59 thf(f633,plain,(
% 1.93/0.59 (((ord_less_nat @ (minus_minus_nat @ nMsg @ (suc @ zero_zero_nat)) @ (minus_minus_nat @ (size_s1406904903t_unit @ (fe @ index)) @ (suc @ zero_zero_nat)))) != $true)),
% 1.93/0.59 inference(flattening,[],[f268])).
% 1.93/0.59 thf(f635,plain,(
% 1.93/0.59 ! [X0 : nat] : (((ord_less_nat @ X0 @ zero_zero_nat)) != $true)),
% 1.93/0.59 inference(flattening,[],[f297])).
% 1.93/0.59 thf(f643,plain,(
% 1.93/0.59 ! [X0 : nat,X1 : nat] : ((X0 != X1) => ((((ord_less_nat @ X1 @ X0)) != $true) => (((ord_less_nat @ X0 @ X1)) = $true)))),
% 1.93/0.59 inference(flattening,[],[f374])).
% 1.93/0.59 thf(f671,plain,(
% 1.93/0.59 ! [X0 : nat] : ((((firstO1414030372_p_v_s @ (fe @ (suc @ index)) @ (ft @ (suc @ index)) @ msg @ X0)) != $true) | (((ord_less_nat @ X0 @ (size_s1406904903t_unit @ (fe @ index)))) = $true))),
% 1.93/0.59 inference(ennf_transformation,[],[f368])).
% 1.93/0.59 thf(f751,plain,(
% 1.93/0.59 ! [X0 : nat,X1 : nat] : ((((ord_less_eq_nat @ X1 @ X0)) != $true) | (zero_zero_nat = ((minus_minus_nat @ X1 @ X0))))),
% 1.93/0.59 inference(ennf_transformation,[],[f606])).
% 1.93/0.59 thf(f797,plain,(
% 1.93/0.59 ! [X2 : nat,X0 : nat,X1 : nat] : (((((ord_less_nat @ (minus_minus_nat @ X0 @ X1) @ (minus_minus_nat @ X2 @ X1))) = $true) | (((ord_less_eq_nat @ X1 @ X0)) != $true)) | (((ord_less_nat @ X0 @ X2)) != $true))),
% 1.93/0.59 inference(ennf_transformation,[],[f620])).
% 1.93/0.59 thf(f798,plain,(
% 1.93/0.59 ! [X1 : nat,X2 : nat,X0 : nat] : ((((ord_less_nat @ (minus_minus_nat @ X0 @ X1) @ (minus_minus_nat @ X2 @ X1))) = $true) | (((ord_less_nat @ X0 @ X2)) != $true) | (((ord_less_eq_nat @ X1 @ X0)) != $true))),
% 1.93/0.59 inference(flattening,[],[f797])).
% 1.93/0.59 thf(f818,plain,(
% 1.93/0.59 ! [X0 : nat] : ((((ord_less_nat @ zero_zero_nat @ X0)) != $true) | (((suc @ (minus_minus_nat @ X0 @ (suc @ zero_zero_nat)))) = X0))),
% 1.93/0.59 inference(ennf_transformation,[],[f335])).
% 1.93/0.59 thf(f846,plain,(
% 1.93/0.59 ! [X0 : nat,X1 : nat] : (((((ord_less_nat @ X0 @ X1)) = $true) | (((ord_less_nat @ X1 @ X0)) = $true)) | (X0 = X1))),
% 1.93/0.59 inference(ennf_transformation,[],[f643])).
% 1.93/0.59 thf(f847,plain,(
% 1.93/0.59 ! [X1 : nat,X0 : nat] : ((((ord_less_nat @ X1 @ X0)) = $true) | (X0 = X1) | (((ord_less_nat @ X0 @ X1)) = $true))),
% 1.93/0.59 inference(flattening,[],[f846])).
% 1.93/0.59 thf(f855,plain,(
% 1.93/0.59 ! [X0 : nat,X1 : nat,X2 : nat] : (($true = ((ord_less_nat @ (minus_minus_nat @ X2 @ X0) @ (minus_minus_nat @ X1 @ X0)))) | (((ord_less_nat @ X2 @ X1)) != $true) | (((ord_less_eq_nat @ X0 @ X2)) != $true))),
% 1.93/0.59 inference(rectify,[],[f798])).
% 1.93/0.59 thf(f926,plain,(
% 1.93/0.59 ! [X0 : nat,X1 : nat] : ((((ord_less_eq_nat @ X1 @ X0)) = $true) | (((ord_less_eq_nat @ X0 @ X1)) = $true))),
% 1.93/0.59 inference(rectify,[],[f497])).
% 1.93/0.59 thf(f952,plain,(
% 1.93/0.59 ! [X0 : nat,X1 : nat] : ((((ord_less_nat @ X0 @ X1)) = $true) | (X0 = X1) | (((ord_less_nat @ X1 @ X0)) = $true))),
% 1.93/0.59 inference(rectify,[],[f847])).
% 1.93/0.59 thf(f1052,plain,(
% 1.93/0.59 ( ! [X0 : nat] : ((((ord_less_nat @ X0 @ zero_zero_nat)) != $true)) )),
% 1.93/0.59 inference(cnf_transformation,[],[f635])).
% 1.93/0.59 thf(f1053,plain,(
% 1.93/0.59 ( ! [X2 : nat,X0 : nat,X1 : nat] : (($true = ((ord_less_nat @ (minus_minus_nat @ X2 @ X0) @ (minus_minus_nat @ X1 @ X0)))) | (((ord_less_eq_nat @ X0 @ X2)) != $true) | (((ord_less_nat @ X2 @ X1)) != $true)) )),
% 1.93/0.59 inference(cnf_transformation,[],[f855])).
% 1.93/0.59 thf(f1085,plain,(
% 1.93/0.59 (((ord_less_eq_nat @ one_one_nat @ one_one_nat)) = $true)),
% 1.93/0.59 inference(cnf_transformation,[],[f339])).
% 1.93/0.59 thf(f1096,plain,(
% 1.93/0.59 ( ! [X0 : nat,X1 : nat] : ((zero_zero_nat = ((minus_minus_nat @ X1 @ X0))) | (((ord_less_eq_nat @ X1 @ X0)) != $true)) )),
% 1.93/0.59 inference(cnf_transformation,[],[f751])).
% 1.93/0.59 thf(f1140,plain,(
% 1.93/0.59 (((suc @ zero_zero_nat)) = one_one_nat)),
% 1.93/0.59 inference(cnf_transformation,[],[f194])).
% 1.93/0.59 thf(f1197,plain,(
% 1.93/0.59 ( ! [X0 : nat,X1 : nat] : ((((ord_less_eq_nat @ X1 @ X0)) = $true) | (((ord_less_eq_nat @ X0 @ X1)) = $true)) )),
% 1.93/0.59 inference(cnf_transformation,[],[f926])).
% 1.93/0.59 thf(f1217,plain,(
% 1.93/0.59 (((ord_less_nat @ zero_zero_nat @ nMsg)) = $true)),
% 1.93/0.59 inference(cnf_transformation,[],[f563])).
% 1.93/0.59 thf(f1225,plain,(
% 1.93/0.59 (((ord_less_nat @ (minus_minus_nat @ nMsg @ (suc @ zero_zero_nat)) @ (minus_minus_nat @ (size_s1406904903t_unit @ (fe @ index)) @ (suc @ zero_zero_nat)))) != $true)),
% 1.93/0.59 inference(cnf_transformation,[],[f633])).
% 1.93/0.59 thf(f1237,plain,(
% 1.93/0.59 ( ! [X0 : nat] : ((((firstO1414030372_p_v_s @ (fe @ (suc @ index)) @ (ft @ (suc @ index)) @ msg @ X0)) != $true) | (((ord_less_nat @ X0 @ (size_s1406904903t_unit @ (fe @ index)))) = $true)) )),
% 1.93/0.59 inference(cnf_transformation,[],[f671])).
% 1.93/0.59 thf(f1254,plain,(
% 1.93/0.59 ( ! [X0 : nat,X1 : nat] : ((((ord_less_nat @ X1 @ X0)) = $true) | (X0 = X1) | (((ord_less_nat @ X0 @ X1)) = $true)) )),
% 1.93/0.59 inference(cnf_transformation,[],[f952])).
% 1.93/0.59 thf(f1264,plain,(
% 1.93/0.59 ( ! [X0 : nat] : ((((suc @ (minus_minus_nat @ X0 @ (suc @ zero_zero_nat)))) = X0) | (((ord_less_nat @ zero_zero_nat @ X0)) != $true)) )),
% 1.93/0.59 inference(cnf_transformation,[],[f818])).
% 1.93/0.59 thf(f1406,plain,(
% 1.93/0.59 (((firstO1414030372_p_v_s @ (fe @ (suc @ index)) @ (ft @ (suc @ index)) @ msg @ nMsg)) = $true)),
% 1.93/0.59 inference(cnf_transformation,[],[f327])).
% 1.93/0.59 thf(f1507,definition,(
% 1.93/0.59 spl107_4 <=> (((suc @ zero_zero_nat)) = one_one_nat)),
% 1.93/0.59 introduced(definition,[new_symbols(definition,[spl107_4])],[avatar_definition])).
% 1.93/0.59 thf(f1510,plain,(
% 1.93/0.59 spl107_4),
% 1.93/0.59 inference(avatar_split_clause,[],[f1140,f1507])).
% 1.93/0.59 thf(f1520,definition,(
% 1.93/0.59 spl107_7 <=> (((ord_less_nat @ (minus_minus_nat @ nMsg @ (suc @ zero_zero_nat)) @ (minus_minus_nat @ (size_s1406904903t_unit @ (fe @ index)) @ (suc @ zero_zero_nat)))) = $true)),
% 1.93/0.59 introduced(definition,[new_symbols(definition,[spl107_7])],[avatar_definition])).
% 1.93/0.59 thf(f1522,plain,(
% 1.93/0.59 (((ord_less_nat @ (minus_minus_nat @ nMsg @ (suc @ zero_zero_nat)) @ (minus_minus_nat @ (size_s1406904903t_unit @ (fe @ index)) @ (suc @ zero_zero_nat)))) != $true) | spl107_7),
% 1.93/0.59 inference(avatar_component_clause,[],[f1520])).
% 1.93/0.59 thf(f1523,plain,(
% 1.93/0.59 ~spl107_7),
% 1.93/0.59 inference(avatar_split_clause,[],[f1225,f1520])).
% 1.93/0.59 thf(f1540,definition,(
% 1.93/0.59 spl107_11 <=> (((firstO1414030372_p_v_s @ (fe @ (suc @ index)) @ (ft @ (suc @ index)) @ msg @ nMsg)) = $true)),
% 1.93/0.59 introduced(definition,[new_symbols(definition,[spl107_11])],[avatar_definition])).
% 1.93/0.59 thf(f1542,plain,(
% 1.93/0.59 (((firstO1414030372_p_v_s @ (fe @ (suc @ index)) @ (ft @ (suc @ index)) @ msg @ nMsg)) = $true) | ~spl107_11),
% 1.93/0.59 inference(avatar_component_clause,[],[f1540])).
% 1.93/0.59 thf(f1543,plain,(
% 1.93/0.59 spl107_11),
% 1.93/0.59 inference(avatar_split_clause,[],[f1406,f1540])).
% 1.93/0.59 thf(f1588,definition,(
% 1.93/0.59 spl107_21 <=> (((ord_less_nat @ zero_zero_nat @ nMsg)) = $true)),
% 1.93/0.59 introduced(definition,[new_symbols(definition,[spl107_21])],[avatar_definition])).
% 1.93/0.59 thf(f1590,plain,(
% 1.93/0.59 (((ord_less_nat @ zero_zero_nat @ nMsg)) = $true) | ~spl107_21),
% 1.93/0.59 inference(avatar_component_clause,[],[f1588])).
% 1.93/0.59 thf(f1591,plain,(
% 1.93/0.59 spl107_21),
% 1.93/0.59 inference(avatar_split_clause,[],[f1217,f1588])).
% 1.93/0.59 thf(f1598,definition,(
% 1.93/0.59 spl107_23 <=> (((ord_less_eq_nat @ one_one_nat @ one_one_nat)) = $true)),
% 1.93/0.59 introduced(definition,[new_symbols(definition,[spl107_23])],[avatar_definition])).
% 1.93/0.59 thf(f1601,plain,(
% 1.93/0.59 spl107_23),
% 1.93/0.59 inference(avatar_split_clause,[],[f1085,f1598])).
% 1.93/0.59 thf(f1884,definition,(
% 1.93/0.59 spl107_67 <=> ($true = ((ord_less_eq_nat @ nMsg @ (suc @ zero_zero_nat))))),
% 1.93/0.59 introduced(definition,[new_symbols(definition,[spl107_67])],[avatar_definition])).
% 1.93/0.59 thf(f1912,definition,(
% 1.93/0.59 spl107_69 <=> ($true = ((ord_less_nat @ (minus_minus_nat @ (size_s1406904903t_unit @ (fe @ index)) @ (suc @ zero_zero_nat)) @ (minus_minus_nat @ nMsg @ (suc @ zero_zero_nat)))))),
% 1.93/0.59 introduced(definition,[new_symbols(definition,[spl107_69])],[avatar_definition])).
% 1.93/0.59 thf(f1913,plain,(
% 1.93/0.59 ($true != ((ord_less_nat @ (minus_minus_nat @ (size_s1406904903t_unit @ (fe @ index)) @ (suc @ zero_zero_nat)) @ (minus_minus_nat @ nMsg @ (suc @ zero_zero_nat))))) | spl107_69),
% 1.93/0.59 inference(avatar_component_clause,[],[f1912])).
% 1.93/0.59 thf(f1914,plain,(
% 1.93/0.59 ($true = ((ord_less_nat @ (minus_minus_nat @ (size_s1406904903t_unit @ (fe @ index)) @ (suc @ zero_zero_nat)) @ (minus_minus_nat @ nMsg @ (suc @ zero_zero_nat))))) | ~spl107_69),
% 1.93/0.59 inference(avatar_component_clause,[],[f1912])).
% 1.93/0.59 thf(f1916,definition,(
% 1.93/0.59 spl107_70 <=> (((minus_minus_nat @ (size_s1406904903t_unit @ (fe @ index)) @ (suc @ zero_zero_nat))) = ((minus_minus_nat @ nMsg @ (suc @ zero_zero_nat))))),
% 1.93/0.59 introduced(definition,[new_symbols(definition,[spl107_70])],[avatar_definition])).
% 1.93/0.59 thf(f1918,plain,(
% 1.93/0.59 (((minus_minus_nat @ (size_s1406904903t_unit @ (fe @ index)) @ (suc @ zero_zero_nat))) = ((minus_minus_nat @ nMsg @ (suc @ zero_zero_nat)))) | ~spl107_70),
% 1.93/0.59 inference(avatar_component_clause,[],[f1916])).
% 1.93/0.59 thf(f1946,plain,(
% 1.93/0.59 ($true != ((ord_less_eq_nat @ nMsg @ (suc @ zero_zero_nat)))) | ($true = ((ord_less_nat @ (minus_minus_nat @ (size_s1406904903t_unit @ (fe @ index)) @ (suc @ zero_zero_nat)) @ zero_zero_nat))) | ~spl107_69),
% 1.93/0.59 inference(superposition,[],[f1914,f1096])).
% 1.93/0.59 thf(f1948,plain,(
% 1.93/0.59 ($true != ((ord_less_eq_nat @ nMsg @ (suc @ zero_zero_nat)))) | ~spl107_69),
% 1.93/0.59 inference(forward_subsumption_resolution,[],[f1946,f1052])).
% 1.93/0.59 thf(f1958,plain,(
% 1.93/0.59 ~spl107_67 | ~spl107_69),
% 1.93/0.59 inference(avatar_split_clause,[],[f1948,f1912,f1884])).
% 1.93/0.59 thf(f2163,definition,(
% 1.93/0.59 spl107_79 <=> (zero_zero_nat = ((minus_minus_nat @ nMsg @ (suc @ zero_zero_nat))))),
% 1.93/0.59 introduced(definition,[new_symbols(definition,[spl107_79])],[avatar_definition])).
% 1.93/0.59 thf(f2165,plain,(
% 1.93/0.59 (zero_zero_nat != ((minus_minus_nat @ nMsg @ (suc @ zero_zero_nat)))) | spl107_79),
% 1.93/0.59 inference(avatar_component_clause,[],[f2163])).
% 1.93/0.59 thf(f2224,plain,(
% 1.93/0.59 ($true != ((ord_less_eq_nat @ nMsg @ (suc @ zero_zero_nat)))) | (zero_zero_nat != zero_zero_nat) | spl107_79),
% 1.93/0.59 inference(superposition,[],[f2165,f1096])).
% 1.93/0.59 thf(f2225,plain,(
% 1.93/0.59 ($true != ((ord_less_eq_nat @ nMsg @ (suc @ zero_zero_nat)))) | spl107_79),
% 1.93/0.59 inference(trivial_inequality_removal,[],[f2224])).
% 1.93/0.59 thf(f3033,definition,(
% 1.93/0.59 spl107_121 <=> ($true = ((ord_less_nat @ nMsg @ (size_s1406904903t_unit @ (fe @ index)))))),
% 1.93/0.59 introduced(definition,[new_symbols(definition,[spl107_121])],[avatar_definition])).
% 1.93/0.59 thf(f3283,plain,(
% 1.93/0.59 (((ord_less_eq_nat @ (suc @ zero_zero_nat) @ nMsg)) != $true) | ($true != ((ord_less_nat @ nMsg @ (size_s1406904903t_unit @ (fe @ index))))) | ($true != $true) | spl107_7),
% 1.93/0.59 inference(superposition,[],[f1522,f1053])).
% 1.93/0.59 thf(f3286,plain,(
% 1.93/0.59 (((ord_less_eq_nat @ (suc @ zero_zero_nat) @ nMsg)) != $true) | ($true != ((ord_less_nat @ nMsg @ (size_s1406904903t_unit @ (fe @ index))))) | spl107_7),
% 1.93/0.59 inference(trivial_inequality_removal,[],[f3283])).
% 1.93/0.59 thf(f3293,definition,(
% 1.93/0.59 spl107_149 <=> (((ord_less_eq_nat @ (suc @ zero_zero_nat) @ nMsg)) = $true)),
% 1.93/0.59 introduced(definition,[new_symbols(definition,[spl107_149])],[avatar_definition])).
% 1.93/0.59 thf(f3295,plain,(
% 1.93/0.59 (((ord_less_eq_nat @ (suc @ zero_zero_nat) @ nMsg)) != $true) | spl107_149),
% 1.93/0.59 inference(avatar_component_clause,[],[f3293])).
% 1.93/0.59 thf(f3296,plain,(
% 1.93/0.59 ~spl107_121 | ~spl107_149 | spl107_7),
% 1.93/0.59 inference(avatar_split_clause,[],[f3286,f1520,f3293,f3033])).
% 1.93/0.59 thf(f3331,plain,(
% 1.93/0.59 ($true != $true) | ($true = ((ord_less_nat @ nMsg @ (size_s1406904903t_unit @ (fe @ index))))) | ~spl107_11),
% 1.93/0.59 inference(superposition,[],[f1237,f1542])).
% 1.93/0.59 thf(f3332,plain,(
% 1.93/0.59 ($true = ((ord_less_nat @ nMsg @ (size_s1406904903t_unit @ (fe @ index))))) | ~spl107_11),
% 1.93/0.59 inference(trivial_inequality_removal,[],[f3331])).
% 1.93/0.59 thf(f3333,plain,(
% 1.93/0.59 spl107_121 | ~spl107_11),
% 1.93/0.59 inference(avatar_split_clause,[],[f3332,f1540,f3033])).
% 1.93/0.59 thf(f5414,plain,(
% 1.93/0.59 ($true = ((ord_less_eq_nat @ nMsg @ (suc @ zero_zero_nat)))) | ($true != $true) | spl107_149),
% 1.93/0.59 inference(superposition,[],[f3295,f1197])).
% 1.93/0.59 thf(f5427,plain,(
% 1.93/0.59 ($true = ((ord_less_eq_nat @ nMsg @ (suc @ zero_zero_nat)))) | spl107_149),
% 1.93/0.59 inference(trivial_inequality_removal,[],[f5414])).
% 1.93/0.59 thf(f5467,plain,(
% 1.93/0.59 ~spl107_67 | spl107_79),
% 1.93/0.59 inference(avatar_split_clause,[],[f2225,f2163,f1884])).
% 1.93/0.59 thf(f5483,plain,(
% 1.93/0.59 spl107_67 | spl107_149),
% 1.93/0.59 inference(avatar_split_clause,[],[f5427,f3293,f1884])).
% 1.93/0.59 thf(f5586,plain,(
% 1.93/0.59 (((minus_minus_nat @ (size_s1406904903t_unit @ (fe @ index)) @ (suc @ zero_zero_nat))) = ((minus_minus_nat @ nMsg @ (suc @ zero_zero_nat)))) | (((ord_less_nat @ (minus_minus_nat @ nMsg @ (suc @ zero_zero_nat)) @ (minus_minus_nat @ (size_s1406904903t_unit @ (fe @ index)) @ (suc @ zero_zero_nat)))) = $true) | ($true != $true) | spl107_69),
% 1.93/0.59 inference(superposition,[],[f1913,f1254])).
% 1.93/0.59 thf(f5588,plain,(
% 1.93/0.59 (((minus_minus_nat @ (size_s1406904903t_unit @ (fe @ index)) @ (suc @ zero_zero_nat))) = ((minus_minus_nat @ nMsg @ (suc @ zero_zero_nat)))) | (((ord_less_nat @ (minus_minus_nat @ nMsg @ (suc @ zero_zero_nat)) @ (minus_minus_nat @ (size_s1406904903t_unit @ (fe @ index)) @ (suc @ zero_zero_nat)))) = $true) | spl107_69),
% 1.93/0.59 inference(trivial_inequality_removal,[],[f5586])).
% 1.93/0.59 thf(f5591,plain,(
% 1.93/0.59 (((minus_minus_nat @ (size_s1406904903t_unit @ (fe @ index)) @ (suc @ zero_zero_nat))) = ((minus_minus_nat @ nMsg @ (suc @ zero_zero_nat)))) | (spl107_7 | spl107_69)),
% 1.93/0.59 inference(forward_subsumption_resolution,[],[f5588,f1522])).
% 1.93/0.59 thf(f5599,plain,(
% 1.93/0.59 spl107_70 | spl107_7 | spl107_69),
% 1.93/0.59 inference(avatar_split_clause,[],[f5591,f1912,f1520,f1916])).
% 1.93/0.59 thf(f5618,plain,(
% 1.93/0.59 (((ord_less_nat @ zero_zero_nat @ nMsg)) != $true) | (nMsg = ((suc @ (minus_minus_nat @ (size_s1406904903t_unit @ (fe @ index)) @ (suc @ zero_zero_nat))))) | ~spl107_70),
% 1.93/0.59 inference(superposition,[],[f1264,f1918])).
% 1.93/0.59 thf(f5671,plain,(
% 1.93/0.59 (nMsg = ((suc @ (minus_minus_nat @ (size_s1406904903t_unit @ (fe @ index)) @ (suc @ zero_zero_nat))))) | (~spl107_21 | ~spl107_70)),
% 1.93/0.59 inference(forward_subsumption_resolution,[],[f5618,f1590])).
% 1.93/0.59 thf(f5680,definition,(
% 1.93/0.59 spl107_269 <=> (nMsg = ((suc @ (minus_minus_nat @ (size_s1406904903t_unit @ (fe @ index)) @ (suc @ zero_zero_nat)))))),
% 1.93/0.59 introduced(definition,[new_symbols(definition,[spl107_269])],[avatar_definition])).
% 1.93/0.59 thf(f5683,plain,(
% 1.93/0.59 spl107_269 | ~spl107_21 | ~spl107_70),
% 1.93/0.59 inference(avatar_split_clause,[],[f5671,f1916,f1588,f5680])).
% 1.93/0.59 thf(f5684,definition,(
% 1.93/0.59 (((minus_minus_nat @ (size_s1406904903t_unit @ (fe @ index)) @ (suc @ zero_zero_nat))) != ((minus_minus_nat @ nMsg @ (suc @ zero_zero_nat)))) | (zero_zero_nat != ((minus_minus_nat @ nMsg @ (suc @ zero_zero_nat)))) | (nMsg != ((suc @ (minus_minus_nat @ (size_s1406904903t_unit @ (fe @ index)) @ (suc @ zero_zero_nat))))) | (((suc @ zero_zero_nat)) != one_one_nat) | (((ord_less_eq_nat @ one_one_nat @ one_one_nat)) != $true) | (((ord_less_eq_nat @ (suc @ zero_zero_nat) @ nMsg)) = $true)),
% 1.93/0.59 introduced(theory,[theory_tautology_sat_conflict])).
% 1.93/0.59 cnf(s4, plain, spl107_4, inference(sat_conversion,[],[f1510])).
% 1.93/0.59 cnf(s6, plain, ~spl107_7, inference(sat_conversion,[],[f1523])).
% 1.93/0.59 cnf(s10, plain, spl107_11, inference(sat_conversion,[],[f1543])).
% 1.93/0.59 cnf(s18, plain, spl107_21, inference(sat_conversion,[],[f1591])).
% 1.93/0.59 cnf(s22, plain, spl107_23, inference(sat_conversion,[],[f1601])).
% 1.93/0.59 cnf(s76, plain, ~spl107_67 | ~spl107_69, inference(sat_conversion,[],[f1958])).
% 1.93/0.59 cnf(s153, plain, spl107_7 | ~spl107_121 | ~spl107_149, inference(sat_conversion,[],[f3296])).
% 1.93/0.59 cnf(s155, plain, ~spl107_11 | spl107_121, inference(sat_conversion,[],[f3333])).
% 1.93/0.59 cnf(s298, plain, ~spl107_67 | spl107_79, inference(sat_conversion,[],[f5467])).
% 1.93/0.59 cnf(s303, plain, spl107_67 | spl107_149, inference(sat_conversion,[],[f5483])).
% 1.93/0.59 cnf(s350, plain, spl107_7 | spl107_69 | spl107_70, inference(sat_conversion,[],[f5599])).
% 1.93/0.59 cnf(s361, plain, ~spl107_21 | ~spl107_70 | spl107_269, inference(sat_conversion,[],[f5683])).
% 1.93/0.59 cnf(s363, plain, ~spl107_4 | ~spl107_23 | ~spl107_70 | ~spl107_79 | spl107_149 | ~spl107_269, inference(sat_conversion,[],[f5684])).
% 1.93/0.59 cnf(s402, plain, spl107_121, inference(rat,[],[s155,s10])).
% 1.93/0.59 cnf(s410, plain, ~spl107_149, inference(rat,[],[s153,s402,s6])).
% 1.93/0.59 cnf(s412, plain, spl107_67, inference(rat,[],[s303,s410])).
% 1.93/0.59 cnf(s417, plain, spl107_79, inference(rat,[],[s298,s412])).
% 1.93/0.59 cnf(s418, plain, ~spl107_69, inference(rat,[],[s76,s412])).
% 1.93/0.59 cnf(s421, plain, spl107_70, inference(rat,[],[s350,s6,s418])).
% 1.93/0.59 cnf(s428, plain, spl107_269, inference(rat,[],[s361,s18,s421])).
% 1.93/0.59 cnf(s433, plain, ~spl107_4, inference(rat,[],[s363,s428,s410,s417,s22,s421])).
% 1.93/0.59 cnf(s445, plain, $false, inference(rat,[],[s4,s433])).
% 1.93/0.59 thf(f5689,plain,(
% 1.93/0.59 $false),
% 1.93/0.59 inference(avatar_sat_refutation,[],[s445])).
% 1.93/0.59 % SZS output end Proof for theBenchmark
% 1.93/0.59 % (820610)------------------------------
% 1.93/0.59 % (820610)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.93/0.59 % (820610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.93/0.59 % (820610)CaDiCaL version: 2.1.3
% 1.93/0.59 % (820610)Termination reason: Refutation
% 1.93/0.59 % (820610)Time elapsed: 0.249 s
% 1.93/0.59 % (820610)Peak memory usage: 16 MB
% 1.93/0.59 % (820610)Instructions burned: 452 (million)
% 1.93/0.59 % (820602)Success in time 0.306 s
% 1.93/0.59 % Vampire exiting
%------------------------------------------------------------------------------