%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP102^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 : n017.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:21 AM UTC 2026
% Result : Theorem 0.64s 0.43s
% Output : Refutation 0.64s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP102^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.10/0.17 % Computer : n017.cluster.edu
% 0.10/0.17 % Model : x86_64 x86_64
% 0.10/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.17 % Memory : 8046.5625MB
% 0.10/0.17 % OS : Linux 6.8.0-71-generic
% 0.10/0.17 % CPULimit : 300
% 0.10/0.17 % WCLimit : 300
% 0.10/0.17 % DateTime : Tue Sep 29 19:49:07 UTC 2026
% 0.10/0.17 % CPUTime :
% 0.10/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.21 Running higher-order theorem proving
% 0.10/0.25 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.64/0.40 % (811892)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.64/0.40 % (811902)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=3634350044:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.64/0.40 % (811903)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.64/0.40 % (811903)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.64/0.40 % (811897)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=463001616:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.64/0.40 % (811898)lrs+10_16_si=on:nwc=1.5:random_seed=896594669:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.64/0.40 % (811899)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=3752104499:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.64/0.40 % (811901)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=3788340877:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.64/0.40 % (811900)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=843720603: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.64/0.40 % (811903)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=1823007089:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.64/0.40 % (811899)Instruction limit reached!
% 0.64/0.40 % (811899)------------------------------
% 0.64/0.40 % (811899)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.64/0.40 % (811899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.64/0.40 % (811899)CaDiCaL version: 2.1.3
% 0.64/0.40 % (811899)Termination reason: Instruction limit
% 0.64/0.40 % (811899)Termination phase: shuffling
% 0.64/0.40 % (811899)Time elapsed: 0.003 s
% 0.64/0.40 % (811899)Peak memory usage: 10 MB
% 0.64/0.40 % (811899)Instructions burned: 6 (million)
% 0.64/0.40 % (811898)Instruction limit reached!
% 0.64/0.40 % (811898)------------------------------
% 0.64/0.40 % (811898)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.64/0.40 % (811898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.64/0.40 % (811898)CaDiCaL version: 2.1.3
% 0.64/0.40 % (811898)Termination reason: Instruction limit
% 0.64/0.40 % (811898)Termination phase: Property scanning
% 0.64/0.40 % (811898)Time elapsed: 0.009 s
% 0.64/0.40 % (811898)Peak memory usage: 10 MB
% 0.64/0.40 % (811898)Instructions burned: 18 (million)
% 0.64/0.40 % (811902)Instruction limit reached!
% 0.64/0.40 % (811902)------------------------------
% 0.64/0.40 % (811902)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.64/0.40 % (811902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.64/0.40 % (811902)CaDiCaL version: 2.1.3
% 0.64/0.40 % (811902)Termination reason: Instruction limit
% 0.64/0.40 % (811902)Termination phase: Property scanning
% 0.64/0.40 % (811902)Time elapsed: 0.019 s
% 0.64/0.40 % (811902)Peak memory usage: 12 MB
% 0.64/0.40 % (811902)Instructions burned: 77 (million)
% 0.64/0.40 % (811901)Instruction limit reached!
% 0.64/0.40 % (811901)------------------------------
% 0.64/0.40 % (811901)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.64/0.40 % (811901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.64/0.40 % (811901)CaDiCaL version: 2.1.3
% 0.64/0.40 % (811901)Termination reason: Instruction limit
% 0.64/0.40 % (811901)Termination phase: Property scanning
% 0.64/0.40 % (811901)Time elapsed: 0.012 s
% 0.64/0.40 % (811901)Peak memory usage: 10 MB
% 0.64/0.40 % (811901)Instructions burned: 25 (million)
% 0.64/0.40 % (811913)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.64/0.40 % (811913)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3669837290:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.64/0.43 % (811911)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=911794927:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.64/0.43 % (811913)Instruction limit reached!
% 0.64/0.43 % (811913)------------------------------
% 0.64/0.43 % (811913)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.64/0.43 % (811913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.64/0.43 % (811913)CaDiCaL version: 2.1.3
% 0.64/0.43 % (811913)Termination reason: Instruction limit
% 0.64/0.43 % (811913)Termination phase: shuffling
% 0.64/0.43 % (811913)Time elapsed: 0.003 s
% 0.64/0.43 % (811913)Peak memory usage: 10 MB
% 0.64/0.43 % (811913)Instructions burned: 11 (million)
% 0.64/0.43 % (811911)Instruction limit reached!
% 0.64/0.43 % (811911)------------------------------
% 0.64/0.43 % (811911)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.64/0.43 % (811911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.64/0.43 % (811911)CaDiCaL version: 2.1.3
% 0.64/0.43 % (811911)Termination reason: Instruction limit
% 0.64/0.43 % (811911)Termination phase: shuffling
% 0.64/0.43 % (811911)Time elapsed: 0.002 s
% 0.64/0.43 % (811911)Peak memory usage: 10 MB
% 0.64/0.43 % (811911)Instructions burned: 4 (million)
% 0.64/0.43 % (811917)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.64/0.43 % (811917)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.64/0.43 % (811914)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=428173934:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.64/0.43 % (811917)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=3416757706: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.64/0.43 % (811912)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=2363063470:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.64/0.43 % (811912)Instruction limit reached!
% 0.64/0.43 % (811912)------------------------------
% 0.64/0.43 % (811912)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.64/0.43 % (811912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.64/0.43 % (811912)CaDiCaL version: 2.1.3
% 0.64/0.43 % (811912)Termination reason: Instruction limit
% 0.64/0.43 % (811912)Termination phase: shuffling
% 0.64/0.43 % (811912)Time elapsed: 0.003 s
% 0.64/0.43 % (811912)Peak memory usage: 10 MB
% 0.64/0.43 % (811912)Instructions burned: 6 (million)
% 0.64/0.43 % (811897)Instruction limit reached!
% 0.64/0.43 % (811897)------------------------------
% 0.64/0.43 % (811897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.64/0.43 % (811897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.64/0.43 % (811897)CaDiCaL version: 2.1.3
% 0.64/0.43 % (811897)Termination reason: Instruction limit
% 0.64/0.43 % (811897)Termination phase: Property scanning
% 0.64/0.43 % (811897)Time elapsed: 0.040 s
% 0.64/0.43 % (811897)Peak memory usage: 12 MB
% 0.64/0.43 % (811897)Instructions burned: 88 (million)
% 0.64/0.43 % (811914)Instruction limit reached!
% 0.64/0.43 % (811914)------------------------------
% 0.64/0.43 % (811914)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.64/0.43 % (811914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.64/0.43 % (811914)CaDiCaL version: 2.1.3
% 0.64/0.43 % (811914)Termination reason: Instruction limit
% 0.64/0.43 % (811914)Termination phase: shuffling
% 0.64/0.43 % (811914)Time elapsed: 0.006 s
% 0.64/0.43 % (811914)Peak memory usage: 10 MB
% 0.64/0.43 % (811914)Instructions burned: 13 (million)
% 0.64/0.43 % (811917)Instruction limit reached!
% 0.64/0.43 % (811917)------------------------------
% 0.64/0.43 % (811917)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.64/0.43 % (811917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.64/0.43 % (811917)CaDiCaL version: 2.1.3
% 0.64/0.43 % (811917)Termination reason: Instruction limit
% 0.64/0.43 % (811917)Termination phase: Property scanning
% 0.64/0.43 % (811917)Time elapsed: 0.007 s
% 0.64/0.43 % (811917)Peak memory usage: 10 MB
% 0.64/0.43 % (811917)Instructions burned: 31 (million)
% 0.64/0.43 % (811923)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.64/0.43 % (811923)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=403958943:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.64/0.43 % (811923)Instruction limit reached!
% 0.64/0.43 % (811923)------------------------------
% 0.64/0.43 % (811923)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.64/0.43 % (811923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.64/0.43 % (811923)CaDiCaL version: 2.1.3
% 0.64/0.43 % (811923)Termination reason: Instruction limit
% 0.64/0.43 % (811923)Termination phase: shuffling
% 0.64/0.43 % (811923)Time elapsed: 0.002 s
% 0.64/0.43 % (811923)Peak memory usage: 10 MB
% 0.64/0.43 % (811923)Instructions burned: 7 (million)
% 0.64/0.43 % (811918)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=1234078822:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.64/0.43 % (811922)lrs+10_1_si=on:cs=on:random_seed=2192718286:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.64/0.43 % (811924)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=4036040838:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.64/0.43 % (811922)Instruction limit reached!
% 0.64/0.43 % (811922)------------------------------
% 0.64/0.43 % (811922)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.64/0.43 % (811922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.64/0.43 % (811922)CaDiCaL version: 2.1.3
% 0.64/0.43 % (811922)Termination reason: Instruction limit
% 0.64/0.43 % (811922)Termination phase: shuffling
% 0.64/0.43 % (811922)Time elapsed: 0.005 s
% 0.64/0.43 % (811922)Peak memory usage: 10 MB
% 0.64/0.43 % (811922)Instructions burned: 10 (million)
% 0.64/0.43 % (811927)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=1441778747:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 0.64/0.43 % (811925)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=489798795:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.64/0.43 % (811927)Instruction limit reached!
% 0.64/0.43 % (811927)------------------------------
% 0.64/0.43 % (811927)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.64/0.43 % (811927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.64/0.43 % (811927)CaDiCaL version: 2.1.3
% 0.64/0.43 % (811927)Termination reason: Instruction limit
% 0.64/0.43 % (811927)Termination phase: Property scanning
% 0.64/0.43 % (811927)Time elapsed: 0.006 s
% 0.64/0.43 % (811927)Peak memory usage: 10 MB
% 0.64/0.43 % (811927)Instructions burned: 27 (million)
% 0.64/0.43 % (811903)Instruction limit reached!
% 0.64/0.43 % (811903)------------------------------
% 0.64/0.43 % (811903)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.64/0.43 % (811903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.64/0.43 % (811903)CaDiCaL version: 2.1.3
% 0.64/0.43 % (811903)Termination reason: Instruction limit
% 0.64/0.43 % (811903)Termination phase: Saturation
% 0.64/0.43 % (811903)Time elapsed: 0.077 s
% 0.64/0.43 % (811903)Peak memory usage: 14 MB
% 0.64/0.43 % (811903)Instructions burned: 158 (million)
% 0.64/0.43 % (811924)Instruction limit reached!
% 0.64/0.43 % (811924)------------------------------
% 0.64/0.43 % (811924)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.64/0.43 % (811924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.64/0.43 % (811924)CaDiCaL version: 2.1.3
% 0.64/0.43 % (811924)Termination reason: Instruction limit
% 0.64/0.43 % (811924)Termination phase: Property scanning
% 0.64/0.43 % (811924)Time elapsed: 0.018 s
% 0.64/0.43 % (811924)Peak memory usage: 11 MB
% 0.64/0.43 % (811924)Instructions burned: 38 (million)
% 0.64/0.43 % (811931)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=2642776207:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 0.64/0.43 % (811934)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=1251252019:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 0.64/0.43 % (811931)Instruction limit reached!
% 0.64/0.43 % (811931)------------------------------
% 0.64/0.43 % (811931)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.64/0.43 % (811931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.64/0.43 % (811931)CaDiCaL version: 2.1.3
% 0.64/0.43 % (811931)Termination reason: Instruction limit
% 0.64/0.43 % (811931)Termination phase: shuffling
% 0.64/0.43 % (811931)Time elapsed: 0.007 s
% 0.64/0.43 % (811931)Peak memory usage: 10 MB
% 0.64/0.43 % (811931)Instructions burned: 15 (million)
% 0.64/0.43 % (811935)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=3144736110:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 0.64/0.43 % (811936)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=3782611654:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2998 on theBenchmark for (2998ds/2Mi)
% 0.64/0.43 % (811936)Instruction limit reached!
% 0.64/0.43 % (811936)------------------------------
% 0.64/0.43 % (811936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.64/0.43 % (811936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.64/0.43 % (811936)CaDiCaL version: 2.1.3
% 0.64/0.43 % (811936)Termination reason: Instruction limit
% 0.64/0.43 % (811936)Termination phase: shuffling
% 0.64/0.43 % (811936)Time elapsed: 0.003 s
% 0.64/0.43 % (811936)Peak memory usage: 10 MB
% 0.64/0.43 % (811936)Instructions burned: 6 (million)
% 0.64/0.43 % (811935)Instruction limit reached!
% 0.64/0.43 % (811935)------------------------------
% 0.64/0.43 % (811935)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.64/0.43 % (811935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.64/0.43 % (811935)CaDiCaL version: 2.1.3
% 0.64/0.43 % (811935)Termination reason: Instruction limit
% 0.64/0.43 % (811935)Termination phase: shuffling
% 0.64/0.43 % (811935)Time elapsed: 0.007 s
% 0.64/0.43 % (811935)Peak memory usage: 10 MB
% 0.64/0.43 % (811935)Instructions burned: 15 (million)
% 0.64/0.43 % (811925) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-811892-811925"...
% 0.64/0.43 % (811939)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=928209896:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 0.64/0.43 % (811925)...printing done.
% 0.64/0.43 % (811925)Refutation found. Thanks to Tanya!
% 0.64/0.43 % SZS status Theorem for theBenchmark
% 0.64/0.43 % SZS output start Proof for theBenchmark
% 0.64/0.43 thf(type_def_5, type, list: $tType > $tType).
% 0.64/0.43 thf(type_def_6, type, nat: $tType).
% 0.64/0.43 thf(type_def_7, type, a: $tType).
% 0.64/0.43 thf(type_def_8, type, sTfun: ($tType * $tType) > $tType).
% 0.64/0.43 thf(func_def_0, type, type: !>[X0: $tType]:($o)).
% 0.64/0.43 thf(func_def_1, type, size: !>[X0: $tType]:($o)).
% 0.64/0.43 thf(func_def_2, type, ord: !>[X0: $tType]:($o)).
% 0.64/0.43 thf(func_def_3, type, order: !>[X0: $tType]:($o)).
% 0.64/0.43 thf(func_def_4, type, no_bot: !>[X0: $tType]:($o)).
% 0.64/0.43 thf(func_def_5, type, no_top: !>[X0: $tType]:($o)).
% 0.64/0.43 thf(func_def_6, type, linorder: !>[X0: $tType]:($o)).
% 0.64/0.43 thf(func_def_7, type, preorder: !>[X0: $tType]:($o)).
% 0.64/0.43 thf(func_def_8, type, wellorder: !>[X0: $tType]:($o)).
% 0.64/0.43 thf(func_def_9, type, dense_order: !>[X0: $tType]:($o)).
% 0.64/0.43 thf(func_def_10, type, dense_linorder: !>[X0: $tType]:($o)).
% 0.64/0.43 thf(func_def_11, type, condit1656338222tinuum: !>[X0: $tType]:($o)).
% 0.64/0.43 thf(func_def_12, type, condit1037483654norder: !>[X0: $tType]:($o)).
% 0.64/0.43 thf(func_def_13, type, minus_minus: !>[X0: $tType]:((X0 > X0 > X0))).
% 0.64/0.43 thf(func_def_14, type, list_asc: !>[X0: $tType]:((list @ X0 > $o))).
% 0.64/0.43 thf(func_def_15, type, list_desc: !>[X0: $tType]:((list @ X0 > $o))).
% 0.64/0.43 thf(func_def_16, type, list_strict_asc: !>[X0: $tType]:((list @ X0 > $o))).
% 0.64/0.43 thf(func_def_17, type, list_strict_desc: !>[X0: $tType]:((list @ X0 > $o))).
% 0.64/0.43 thf(func_def_18, type, listIn521021761append: !>[X0: $tType]:((list @ X0 > (nat > X0) > nat > X0))).
% 0.64/0.43 thf(func_def_19, type, linorder_sorted: !>[X0: $tType]:((list @ X0 > $o))).
% 0.64/0.43 thf(func_def_20, type, list_ex: !>[X0: $tType]:(((X0 > $o) > list @ X0 > $o))).
% 0.64/0.43 thf(func_def_21, type, nth: !>[X0: $tType]:((list @ X0 > nat > X0))).
% 0.64/0.43 thf(func_def_22, type, rev: !>[X0: $tType]:((list @ X0 > list @ X0))).
% 0.64/0.43 thf(func_def_23, type, suc: (nat > nat)).
% 0.64/0.43 thf(func_def_24, type, size_size: !>[X0: $tType]:((X0 > nat))).
% 0.64/0.43 thf(func_def_25, type, ord_less: !>[X0: $tType]:((X0 > X0 > $o))).
% 0.64/0.43 thf(func_def_26, type, ord_less_eq: !>[X0: $tType]:((X0 > X0 > $o))).
% 0.64/0.43 thf(func_def_27, type, f: (nat > a)).
% 0.64/0.43 thf(func_def_28, type, g: (nat > a)).
% 0.64/0.43 thf(func_def_29, type, xs: list @ a).
% 0.64/0.43 thf(func_def_30, type, ys: list @ a).
% 0.64/0.43 thf(func_def_34, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 0.64/0.43 thf(func_def_35, type, vAND: ($o > $o > $o)).
% 0.64/0.43 thf(func_def_36, type, db1: !>[X0: $tType]:(X0)).
% 0.64/0.43 thf(func_def_37, type, db0: !>[X0: $tType]:(X0)).
% 0.64/0.43 thf(func_def_38, type, vNOT: ($o > $o)).
% 0.64/0.43 thf(func_def_39, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 0.64/0.43 thf(func_def_40, type, vOR: ($o > $o > $o)).
% 0.64/0.43 thf(func_def_41, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 0.64/0.43 thf(func_def_42, type, vIMP: ($o > $o > $o)).
% 0.64/0.43 thf(func_def_43, type, db2: !>[X0: $tType]:(X0)).
% 0.64/0.43 thf(func_def_44, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 0.64/0.43 thf(func_def_45, type, sK0: !>[X0: $tType]:((nat > list @ X0))).
% 0.64/0.43 thf(func_def_46, type, sK1: !>[X0: $tType]:(((X0 > nat) > (X0 > $o) > X0))).
% 0.64/0.43 thf(func_def_47, type, sK2: (nat > (nat > $o) > nat)).
% 0.64/0.43 thf(func_def_48, type, sK3: (nat > (nat > $o) > nat)).
% 0.64/0.43 thf(func_def_49, type, sK4: !>[X0: $tType, X1: $tType]:(((X0 > X1) > (X0 > X1) > X0))).
% 0.64/0.43 thf(func_def_50, type, sK5: ((nat > $o) > nat)).
% 0.64/0.43 thf(func_def_51, type, sK6: !>[X0: $tType]:((list @ X0 > list @ X0 > nat))).
% 0.64/0.43 thf(func_def_52, type, sK7: ((nat > $o) > nat)).
% 0.64/0.43 thf(func_def_53, type, sK8: ((nat > $o) > nat)).
% 0.64/0.43 thf(func_def_54, type, sK9: (nat > (nat > $o) > nat)).
% 0.64/0.43 thf(func_def_55, type, sK10: !>[X0: $tType]:(((X0 > nat) > (X0 > $o) > X0))).
% 0.64/0.43 thf(func_def_56, type, sK11: nat).
% 0.64/0.43 thf(func_def_57, type, sK12: ((nat > nat) > nat)).
% 0.64/0.43 thf(func_def_58, type, sK13: ((nat > nat) > nat)).
% 0.64/0.43 thf(func_def_59, type, sK14: !>[X0: $tType]:(((list @ X0 > $o) > list @ X0))).
% 0.64/0.43 thf(func_def_60, type, sK15: !>[X0: $tType]:(((X0 > $o) > (X0 > nat) > nat > X0))).
% 0.64/0.43 thf(func_def_61, type, sK16: !>[X0: $tType]:(((X0 > $o) > (X0 > nat) > X0))).
% 0.64/0.43 thf(f2,axiom,(
% 0.64/0.43 ! [X0 : $tType,X3 : (nat > X0),X2 : list @ X0,X1 : nat] : ((ord_less @ nat @ X1 @ (size_size @ list @ X0 @ X2)) => (((listIn521021761append @ X0 @ X2 @ X3 @ X1)) = ((nth @ X0 @ X2 @ X1))))),
% 0.64/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1_i__append__nth1)).
% 0.64/0.43 thf(f10,axiom,(
% 0.64/0.43 ! [X0 : nat,X1 : nat] : ((ord_less @ nat @ X0 @ X1) => (ord_less_eq @ nat @ X0 @ X1))),
% 0.64/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_9_less__imp__le__nat)).
% 0.64/0.43 thf(f13,axiom,(
% 0.64/0.43 ! [X1 : nat,X0 : nat] : ((ord_less_eq @ nat @ X0 @ X1) => ((X0 != X1) => (ord_less @ nat @ X0 @ X1)))),
% 0.64/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_12_le__neq__implies__less)).
% 0.64/0.43 thf(f89,axiom,(
% 0.64/0.43 ! [X1 : nat,X0 : nat] : ((ord_less_eq @ nat @ X0 @ X1) | (ord_less_eq @ nat @ X1 @ X0))),
% 0.64/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_88_nat__le__linear)).
% 0.64/0.43 thf(f90,axiom,(
% 0.64/0.43 ! [X1 : nat,X0 : nat] : ((ord_less_eq @ nat @ X0 @ X1) => ((ord_less_eq @ nat @ X1 @ X0) => (X0 = X1)))),
% 0.64/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_89_le__antisym)).
% 0.64/0.43 thf(f92,axiom,(
% 0.64/0.43 ! [X1 : nat,X0 : nat,X2 : nat] : ((ord_less_eq @ nat @ X0 @ X1) => ((ord_less_eq @ nat @ X1 @ X2) => (ord_less_eq @ nat @ X0 @ X2)))),
% 0.64/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_91_le__trans)).
% 0.64/0.43 thf(f272,axiom,(
% 0.64/0.43 ! [X0 : nat] : (((listIn521021761append @ a @ xs @ f @ X0)) = ((listIn521021761append @ a @ ys @ g @ X0)))),
% 0.64/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0)).
% 0.64/0.43 thf(f273,axiom,(
% 0.64/0.43 (ord_less_eq @ nat @ (size_size @ list @ a @ xs) @ (size_size @ list @ a @ ys))),
% 0.64/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_1)).
% 0.64/0.43 thf(f274,conjecture,(
% 0.64/0.43 ! [X0 : nat] : (~(ord_less @ nat @ X0 @ (size_size @ list @ a @ xs)) | (((nth @ a @ xs @ X0)) = ((nth @ a @ ys @ X0))))),
% 0.64/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_2)).
% 0.64/0.43 thf(f275,negated_conjecture,(
% 0.64/0.43 ~ ! [X0 : nat] : (~(ord_less @ nat @ X0 @ (size_size @ list @ a @ xs)) | (((nth @ a @ xs @ X0)) = ((nth @ a @ ys @ X0))))),
% 0.64/0.43 inference(negated_conjecture,[status(cth)],[f274])).
% 0.64/0.43 thf(f346,plain,(
% 0.64/0.43 ! [X0 : nat,X1 : nat] : ((ord_less_eq @ nat @ X1 @ X0) => ((ord_less_eq @ nat @ X0 @ X1) => (X0 = X1)))),
% 0.64/0.43 inference(rectify,[],[f90])).
% 0.64/0.43 thf(f347,plain,(
% 0.64/0.43 ! [X1 : nat,X0 : nat] : ((((ord_less_eq @ nat @ X1 @ X0)) = $true) => ((((ord_less_eq @ nat @ X0 @ X1)) = $true) => (X0 = X1)))),
% 0.64/0.43 inference(fool_elimination,[],[f346])).
% 0.64/0.43 thf(f354,plain,(
% 0.64/0.43 ! [X0 : nat,X1 : nat,X2 : nat] : ((ord_less_eq @ nat @ X1 @ X0) => ((ord_less_eq @ nat @ X0 @ X2) => (ord_less_eq @ nat @ X1 @ X2)))),
% 0.64/0.43 inference(rectify,[],[f92])).
% 0.64/0.43 thf(f355,plain,(
% 0.64/0.43 ! [X2 : nat,X0 : nat,X1 : nat] : ((((ord_less_eq @ nat @ X1 @ X0)) = $true) => ((((ord_less_eq @ nat @ X0 @ X2)) = $true) => (((ord_less_eq @ nat @ X1 @ X2)) = $true)))),
% 0.64/0.43 inference(fool_elimination,[],[f354])).
% 0.64/0.43 thf(f394,plain,(
% 0.64/0.43 (ord_less_eq @ nat @ (size_size @ list @ a @ xs) @ (size_size @ list @ a @ ys))),
% 0.64/0.43 inference(rectify,[],[f273])).
% 0.64/0.43 thf(f395,plain,(
% 0.64/0.43 (((ord_less_eq @ nat @ (size_size @ list @ a @ xs) @ (size_size @ list @ a @ ys))) = $true)),
% 0.64/0.43 inference(fool_elimination,[],[f394])).
% 0.64/0.43 thf(f519,plain,(
% 0.64/0.43 ! [X0 : nat,X1 : nat] : ((ord_less_eq @ nat @ X1 @ X0) | (ord_less_eq @ nat @ X0 @ X1))),
% 0.64/0.43 inference(rectify,[],[f89])).
% 0.64/0.43 thf(f520,plain,(
% 0.64/0.43 ! [X1 : nat,X0 : nat] : ((((ord_less_eq @ nat @ X0 @ X1)) = $true) | (((ord_less_eq @ nat @ X1 @ X0)) = $true))),
% 0.64/0.43 inference(fool_elimination,[],[f519])).
% 0.64/0.43 thf(f587,plain,(
% 0.64/0.43 ! [X0 : $tType,X1 : (nat > X0),X2 : list @ X0,X3 : nat] : ((ord_less @ nat @ X3 @ (size_size @ list @ X0 @ X2)) => (((nth @ X0 @ X2 @ X3)) = ((listIn521021761append @ X0 @ X2 @ X1 @ X3))))),
% 0.64/0.43 inference(rectify,[],[f2])).
% 0.64/0.43 thf(f588,plain,(
% 0.64/0.43 ! [X0 : $tType,X1 : (nat > X0),X2 : list @ X0,X3 : nat] : ((((ord_less @ nat @ X3 @ (size_size @ list @ X0 @ X2))) = $true) => (((nth @ X0 @ X2 @ X3)) = ((listIn521021761append @ X0 @ X2 @ X1 @ X3))))),
% 0.64/0.43 inference(fool_elimination,[],[f587])).
% 0.64/0.43 thf(f609,plain,(
% 0.64/0.43 ~ ! [X0 : nat] : (~(ord_less @ nat @ X0 @ (size_size @ list @ a @ xs)) | (((nth @ a @ xs @ X0)) = ((nth @ a @ ys @ X0))))),
% 0.64/0.43 inference(rectify,[],[f275])).
% 0.64/0.43 thf(f610,plain,(
% 0.64/0.43 ~ ! [X0 : nat] : (~ (((ord_less @ nat @ X0 @ (size_size @ list @ a @ xs))) = $true) | (((nth @ a @ xs @ X0)) = ((nth @ a @ ys @ X0))))),
% 0.64/0.43 inference(fool_elimination,[],[f609])).
% 0.64/0.43 thf(f737,plain,(
% 0.64/0.43 ! [X0 : nat,X1 : nat] : ((ord_less @ nat @ X0 @ X1) => (ord_less_eq @ nat @ X0 @ X1))),
% 0.64/0.43 inference(rectify,[],[f10])).
% 0.64/0.43 thf(f738,plain,(
% 0.64/0.43 ! [X0 : nat,X1 : nat] : ((((ord_less @ nat @ X0 @ X1)) = $true) => (((ord_less_eq @ nat @ X0 @ X1)) = $true))),
% 0.64/0.43 inference(fool_elimination,[],[f737])).
% 0.64/0.43 thf(f775,plain,(
% 0.64/0.43 ! [X0 : nat,X1 : nat] : ((ord_less_eq @ nat @ X1 @ X0) => ((X0 != X1) => (ord_less @ nat @ X1 @ X0)))),
% 0.64/0.43 inference(rectify,[],[f13])).
% 0.64/0.43 thf(f776,plain,(
% 0.64/0.43 ! [X0 : nat,X1 : nat] : ((((ord_less_eq @ nat @ X1 @ X0)) = $true) => ((X0 != X1) => (((ord_less @ nat @ X1 @ X0)) = $true)))),
% 0.64/0.43 inference(fool_elimination,[],[f775])).
% 0.64/0.43 thf(f791,plain,(
% 0.64/0.43 ~ ! [X0 : nat] : ((((nth @ a @ xs @ X0)) = ((nth @ a @ ys @ X0))) | (((ord_less @ nat @ X0 @ (size_size @ list @ a @ xs))) != $true))),
% 0.64/0.43 inference(flattening,[],[f610])).
% 0.64/0.43 thf(f801,plain,(
% 0.64/0.43 ! [X0 : nat,X1 : nat] : ((((ord_less @ nat @ X0 @ X1)) != $true) | (((ord_less_eq @ nat @ X0 @ X1)) = $true))),
% 0.64/0.43 inference(ennf_transformation,[],[f738])).
% 0.64/0.43 thf(f802,plain,(
% 0.64/0.43 ! [X1 : nat,X0 : nat] : (((X0 = X1) | (((ord_less_eq @ nat @ X0 @ X1)) != $true)) | (((ord_less_eq @ nat @ X1 @ X0)) != $true))),
% 0.64/0.43 inference(ennf_transformation,[],[f347])).
% 0.64/0.43 thf(f803,plain,(
% 0.64/0.43 ! [X1 : nat,X0 : nat] : ((X0 = X1) | (((ord_less_eq @ nat @ X0 @ X1)) != $true) | (((ord_less_eq @ nat @ X1 @ X0)) != $true))),
% 0.64/0.43 inference(flattening,[],[f802])).
% 0.64/0.43 thf(f809,plain,(
% 0.64/0.43 ? [X0 : nat] : ((((nth @ a @ xs @ X0)) != ((nth @ a @ ys @ X0))) & (((ord_less @ nat @ X0 @ (size_size @ list @ a @ xs))) = $true))),
% 0.64/0.43 inference(ennf_transformation,[],[f791])).
% 0.64/0.43 thf(f821,plain,(
% 0.64/0.43 ! [X2 : nat,X0 : nat,X1 : nat] : (((((ord_less_eq @ nat @ X1 @ X2)) = $true) | (((ord_less_eq @ nat @ X0 @ X2)) != $true)) | (((ord_less_eq @ nat @ X1 @ X0)) != $true))),
% 0.64/0.43 inference(ennf_transformation,[],[f355])).
% 0.64/0.43 thf(f822,plain,(
% 0.64/0.43 ! [X0 : nat,X2 : nat,X1 : nat] : ((((ord_less_eq @ nat @ X1 @ X2)) = $true) | (((ord_less_eq @ nat @ X1 @ X0)) != $true) | (((ord_less_eq @ nat @ X0 @ X2)) != $true))),
% 0.64/0.43 inference(flattening,[],[f821])).
% 0.64/0.43 thf(f824,plain,(
% 0.64/0.43 ! [X0 : $tType,X2 : list @ X0,X3 : nat,X1 : (nat > X0)] : ((((ord_less @ nat @ X3 @ (size_size @ list @ X0 @ X2))) != $true) | (((nth @ X0 @ X2 @ X3)) = ((listIn521021761append @ X0 @ X2 @ X1 @ X3))))),
% 0.64/0.43 inference(ennf_transformation,[],[f588])).
% 0.64/0.43 thf(f825,plain,(
% 0.64/0.43 ! [X0 : nat,X1 : nat] : (((((ord_less @ nat @ X1 @ X0)) = $true) | (X0 = X1)) | (((ord_less_eq @ nat @ X1 @ X0)) != $true))),
% 0.64/0.43 inference(ennf_transformation,[],[f776])).
% 0.64/0.43 thf(f826,plain,(
% 0.64/0.43 ! [X1 : nat,X0 : nat] : ((X0 = X1) | (((ord_less_eq @ nat @ X1 @ X0)) != $true) | (((ord_less @ nat @ X1 @ X0)) = $true))),
% 0.64/0.43 inference(flattening,[],[f825])).
% 0.64/0.43 thf(f847,plain,(
% 0.64/0.43 ! [X0 : nat,X1 : nat,X2 : nat] : ((((ord_less_eq @ nat @ X2 @ X1)) = $true) | (((ord_less_eq @ nat @ X2 @ X0)) != $true) | (((ord_less_eq @ nat @ X0 @ X1)) != $true))),
% 0.64/0.43 inference(rectify,[],[f822])).
% 0.64/0.43 thf(f850,plain,(
% 0.64/0.43 ! [X0 : $tType,X1 : list @ X0,X2 : nat,X3 : (nat > X0)] : ((((ord_less @ nat @ X2 @ (size_size @ list @ X0 @ X1))) != $true) | (((nth @ X0 @ X1 @ X2)) = ((listIn521021761append @ X0 @ X1 @ X3 @ X2))))),
% 0.64/0.43 inference(rectify,[],[f824])).
% 0.64/0.43 thf(f851,plain,(
% 0.64/0.43 ! [X0 : nat,X1 : nat] : ((X0 = X1) | (((ord_less_eq @ nat @ X1 @ X0)) != $true) | (((ord_less_eq @ nat @ X0 @ X1)) != $true))),
% 0.64/0.43 inference(rectify,[],[f803])).
% 0.64/0.43 thf(f852,plain,(
% 0.64/0.43 (((nth @ a @ xs @ sK11)) != ((nth @ a @ ys @ sK11))) & (((ord_less @ nat @ sK11 @ (size_size @ list @ a @ xs))) = $true)),
% 0.64/0.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(X0,sK11)],[f809])).
% 0.64/0.43 thf(f856,plain,(
% 0.64/0.43 ! [X0 : nat,X1 : nat] : ((X0 = X1) | (((ord_less_eq @ nat @ X0 @ X1)) != $true) | (((ord_less @ nat @ X0 @ X1)) = $true))),
% 0.64/0.43 inference(rectify,[],[f826])).
% 0.64/0.43 thf(f860,plain,(
% 0.64/0.43 ! [X0 : nat,X1 : nat] : ((((ord_less_eq @ nat @ X1 @ X0)) = $true) | (((ord_less_eq @ nat @ X0 @ X1)) = $true))),
% 0.64/0.43 inference(rectify,[],[f520])).
% 0.64/0.43 thf(f866,plain,(
% 0.64/0.43 (((ord_less_eq @ nat @ (size_size @ list @ a @ xs) @ (size_size @ list @ a @ ys))) = $true)),
% 0.64/0.43 inference(cnf_transformation,[],[f395])).
% 0.64/0.43 thf(f891,plain,(
% 0.64/0.43 ( ! [X2 : nat,X0 : nat,X1 : nat] : ((((ord_less_eq @ nat @ X2 @ X1)) = $true) | (((ord_less_eq @ nat @ X0 @ X1)) != $true) | (((ord_less_eq @ nat @ X2 @ X0)) != $true)) )),
% 0.64/0.43 inference(cnf_transformation,[],[f847])).
% 0.64/0.43 thf(f894,plain,(
% 0.64/0.43 ( ! [X0 : nat] : ((((listIn521021761append @ a @ xs @ f @ X0)) = ((listIn521021761append @ a @ ys @ g @ X0)))) )),
% 0.64/0.43 inference(cnf_transformation,[],[f272])).
% 0.64/0.43 thf(f895,plain,(
% 0.64/0.43 ( ! [X0 : $tType,X2 : nat,X3 : (nat > X0),X1 : list @ X0] : ((((nth @ X0 @ X1 @ X2)) = ((listIn521021761append @ X0 @ X1 @ X3 @ X2))) | (((ord_less @ nat @ X2 @ (size_size @ list @ X0 @ X1))) != $true)) )),
% 0.64/0.43 inference(cnf_transformation,[],[f850])).
% 0.64/0.43 thf(f896,plain,(
% 0.64/0.43 ( ! [X0 : nat,X1 : nat] : ((((ord_less_eq @ nat @ X1 @ X0)) != $true) | (X0 = X1) | (((ord_less_eq @ nat @ X0 @ X1)) != $true)) )),
% 0.64/0.43 inference(cnf_transformation,[],[f851])).
% 0.64/0.43 thf(f897,plain,(
% 0.64/0.43 (((ord_less @ nat @ sK11 @ (size_size @ list @ a @ xs))) = $true)),
% 0.64/0.43 inference(cnf_transformation,[],[f852])).
% 0.64/0.43 thf(f898,plain,(
% 0.64/0.43 (((nth @ a @ xs @ sK11)) != ((nth @ a @ ys @ sK11)))),
% 0.64/0.43 inference(cnf_transformation,[],[f852])).
% 0.64/0.43 thf(f902,plain,(
% 0.64/0.43 ( ! [X0 : nat,X1 : nat] : ((((ord_less @ nat @ X0 @ X1)) = $true) | (X0 = X1) | (((ord_less_eq @ nat @ X0 @ X1)) != $true)) )),
% 0.64/0.43 inference(cnf_transformation,[],[f856])).
% 0.64/0.43 thf(f906,plain,(
% 0.64/0.43 ( ! [X0 : nat,X1 : nat] : ((((ord_less_eq @ nat @ X0 @ X1)) = $true) | (((ord_less @ nat @ X0 @ X1)) != $true)) )),
% 0.64/0.43 inference(cnf_transformation,[],[f801])).
% 0.64/0.43 thf(f910,plain,(
% 0.64/0.43 ( ! [X0 : nat,X1 : nat] : ((((ord_less_eq @ nat @ X1 @ X0)) = $true) | (((ord_less_eq @ nat @ X0 @ X1)) = $true)) )),
% 0.64/0.43 inference(cnf_transformation,[],[f860])).
% 0.64/0.43 thf(f919,definition,(
% 0.64/0.43 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 0.64/0.43 introduced(theory,[fool_exhaustiveness_axiom])).
% 0.64/0.43 thf(f926,plain,(
% 0.64/0.43 (((size_size @ list @ a @ xs)) = ((size_size @ list @ a @ ys))) | ($true != $true) | (((ord_less_eq @ nat @ (size_size @ list @ a @ ys) @ (size_size @ list @ a @ xs))) != $true)),
% 0.64/0.43 inference(superposition,[],[f896,f866])).
% 0.64/0.43 thf(f927,plain,(
% 0.64/0.43 (((ord_less_eq @ nat @ (size_size @ list @ a @ ys) @ (size_size @ list @ a @ xs))) != $true) | (((size_size @ list @ a @ xs)) = ((size_size @ list @ a @ ys)))),
% 0.64/0.43 inference(trivial_inequality_removal,[],[f926])).
% 0.64/0.43 thf(f929,definition,(
% 0.64/0.43 spl17_1 <=> (((size_size @ list @ a @ xs)) = ((size_size @ list @ a @ ys)))),
% 0.64/0.43 introduced(definition,[new_symbols(definition,[spl17_1])],[avatar_definition])).
% 0.64/0.43 thf(f931,plain,(
% 0.64/0.43 (((size_size @ list @ a @ xs)) = ((size_size @ list @ a @ ys))) | ~spl17_1),
% 0.64/0.43 inference(avatar_component_clause,[],[f929])).
% 0.64/0.43 thf(f933,definition,(
% 0.64/0.43 spl17_2 <=> (((ord_less_eq @ nat @ (size_size @ list @ a @ ys) @ (size_size @ list @ a @ xs))) = $true)),
% 0.64/0.43 introduced(definition,[new_symbols(definition,[spl17_2])],[avatar_definition])).
% 0.64/0.43 thf(f935,plain,(
% 0.64/0.43 (((ord_less_eq @ nat @ (size_size @ list @ a @ ys) @ (size_size @ list @ a @ xs))) != $true) | spl17_2),
% 0.64/0.43 inference(avatar_component_clause,[],[f933])).
% 0.64/0.43 thf(f936,plain,(
% 0.64/0.43 spl17_1 | ~spl17_2),
% 0.64/0.43 inference(avatar_split_clause,[],[f927,f933,f929])).
% 0.64/0.43 thf(f940,plain,(
% 0.64/0.43 ( ! [X0 : nat] : ((((listIn521021761append @ a @ xs @ f @ X0)) = ((nth @ a @ ys @ X0))) | (((ord_less @ nat @ X0 @ (size_size @ list @ a @ ys))) != $true)) )),
% 0.64/0.43 inference(superposition,[],[f895,f894])).
% 0.64/0.43 thf(f941,plain,(
% 0.64/0.43 ($true != $true) | (((ord_less @ nat @ (size_size @ list @ a @ ys) @ (size_size @ list @ a @ xs))) != $true) | spl17_2),
% 0.64/0.43 inference(superposition,[],[f935,f906])).
% 0.64/0.43 thf(f943,plain,(
% 0.64/0.43 ( ! [X0 : nat] : ((((ord_less_eq @ nat @ X0 @ (size_size @ list @ a @ xs))) != $true) | ($true != $true) | (((ord_less_eq @ nat @ (size_size @ list @ a @ ys) @ X0)) != $true)) ) | spl17_2),
% 0.64/0.43 inference(superposition,[],[f935,f891])).
% 0.64/0.43 thf(f947,plain,(
% 0.64/0.43 (((ord_less @ nat @ (size_size @ list @ a @ ys) @ (size_size @ list @ a @ xs))) != $true) | spl17_2),
% 0.64/0.43 inference(trivial_inequality_removal,[],[f941])).
% 0.64/0.43 thf(f948,plain,(
% 0.64/0.43 ( ! [X0 : nat] : ((((ord_less_eq @ nat @ (size_size @ list @ a @ ys) @ X0)) != $true) | (((ord_less_eq @ nat @ X0 @ (size_size @ list @ a @ xs))) != $true)) ) | spl17_2),
% 0.64/0.43 inference(trivial_inequality_removal,[],[f943])).
% 0.64/0.43 thf(f953,plain,(
% 0.64/0.43 (((ord_less @ nat @ sK11 @ (size_size @ list @ a @ ys))) != $true) | (((nth @ a @ xs @ sK11)) != ((listIn521021761append @ a @ xs @ f @ sK11)))),
% 0.64/0.43 inference(superposition,[],[f898,f940])).
% 0.64/0.43 thf(f955,definition,(
% 0.64/0.43 spl17_3 <=> (((nth @ a @ xs @ sK11)) = ((listIn521021761append @ a @ xs @ f @ sK11)))),
% 0.64/0.43 introduced(definition,[new_symbols(definition,[spl17_3])],[avatar_definition])).
% 0.64/0.43 thf(f957,plain,(
% 0.64/0.43 (((nth @ a @ xs @ sK11)) != ((listIn521021761append @ a @ xs @ f @ sK11))) | spl17_3),
% 0.64/0.43 inference(avatar_component_clause,[],[f955])).
% 0.64/0.43 thf(f959,definition,(
% 0.64/0.43 spl17_4 <=> (((ord_less @ nat @ sK11 @ (size_size @ list @ a @ ys))) = $true)),
% 0.64/0.43 introduced(definition,[new_symbols(definition,[spl17_4])],[avatar_definition])).
% 0.64/0.43 thf(f961,plain,(
% 0.64/0.43 (((ord_less @ nat @ sK11 @ (size_size @ list @ a @ ys))) != $true) | spl17_4),
% 0.64/0.43 inference(avatar_component_clause,[],[f959])).
% 0.64/0.43 thf(f962,plain,(
% 0.64/0.43 ~spl17_3 | ~spl17_4),
% 0.64/0.43 inference(avatar_split_clause,[],[f953,f959,f955])).
% 0.64/0.43 thf(f965,plain,(
% 0.64/0.43 (((nth @ a @ xs @ sK11)) != ((nth @ a @ xs @ sK11))) | (((ord_less @ nat @ sK11 @ (size_size @ list @ a @ xs))) != $true) | spl17_3),
% 0.64/0.43 inference(superposition,[],[f957,f895])).
% 0.64/0.43 thf(f966,plain,(
% 0.64/0.43 (((ord_less @ nat @ sK11 @ (size_size @ list @ a @ xs))) != $true) | spl17_3),
% 0.64/0.43 inference(trivial_inequality_removal,[],[f965])).
% 0.64/0.43 thf(f976,plain,(
% 0.64/0.43 $false | spl17_3),
% 0.64/0.43 inference(forward_subsumption_resolution,[],[f966,f897])).
% 0.64/0.43 thf(f977,plain,(
% 0.64/0.43 spl17_3),
% 0.64/0.43 inference(avatar_contradiction_clause,[],[f976])).
% 0.64/0.43 thf(f984,plain,(
% 0.64/0.43 ($true != $true) | (((ord_less @ nat @ sK11 @ (size_size @ list @ a @ ys))) = $false) | spl17_4),
% 0.64/0.43 inference(superposition,[],[f961,f919])).
% 0.64/0.43 thf(f987,plain,(
% 0.64/0.43 (((ord_less @ nat @ sK11 @ (size_size @ list @ a @ ys))) = $false) | spl17_4),
% 0.64/0.43 inference(trivial_inequality_removal,[],[f984])).
% 0.64/0.43 thf(f993,definition,(
% 0.64/0.43 spl17_8 <=> (((size_size @ list @ a @ ys)) = sK11)),
% 0.64/0.43 introduced(definition,[new_symbols(definition,[spl17_8])],[avatar_definition])).
% 0.64/0.43 thf(f995,plain,(
% 0.64/0.43 (((size_size @ list @ a @ ys)) = sK11) | ~spl17_8),
% 0.64/0.43 inference(avatar_component_clause,[],[f993])).
% 0.64/0.43 thf(f998,definition,(
% 0.64/0.43 spl17_9 <=> (((ord_less_eq @ nat @ sK11 @ (size_size @ list @ a @ ys))) = $true)),
% 0.64/0.43 introduced(definition,[new_symbols(definition,[spl17_9])],[avatar_definition])).
% 0.64/0.43 thf(f1000,plain,(
% 0.64/0.43 (((ord_less_eq @ nat @ sK11 @ (size_size @ list @ a @ ys))) != $true) | spl17_9),
% 0.64/0.43 inference(avatar_component_clause,[],[f998])).
% 0.64/0.43 thf(f1007,definition,(
% 0.64/0.43 spl17_10 <=> (((ord_less_eq @ nat @ (size_size @ list @ a @ ys) @ sK11)) = $true)),
% 0.64/0.43 introduced(definition,[new_symbols(definition,[spl17_10])],[avatar_definition])).
% 0.64/0.43 thf(f1008,plain,(
% 0.64/0.43 (((ord_less_eq @ nat @ (size_size @ list @ a @ ys) @ sK11)) = $true) | ~spl17_10),
% 0.64/0.43 inference(avatar_component_clause,[],[f1007])).
% 0.64/0.43 thf(f1039,plain,(
% 0.64/0.43 (((size_size @ list @ a @ ys)) = sK11) | ($false = $true) | (((ord_less_eq @ nat @ sK11 @ (size_size @ list @ a @ ys))) != $true) | spl17_4),
% 0.64/0.43 inference(superposition,[],[f987,f902])).
% 0.64/0.43 thf(f1045,plain,(
% 0.64/0.43 (((ord_less_eq @ nat @ sK11 @ (size_size @ list @ a @ ys))) != $true) | (((size_size @ list @ a @ ys)) = sK11) | spl17_4),
% 0.64/0.43 inference(trivial_inequality_removal,[],[f1039])).
% 0.64/0.43 thf(f1054,plain,(
% 0.64/0.43 (((ord_less @ nat @ sK11 @ (size_size @ list @ a @ xs))) != $true) | (~spl17_1 | spl17_4)),
% 0.64/0.43 inference(superposition,[],[f961,f931])).
% 0.64/0.43 thf(f1061,plain,(
% 0.64/0.43 $false | (~spl17_1 | spl17_4)),
% 0.64/0.43 inference(forward_subsumption_resolution,[],[f1054,f897])).
% 0.64/0.43 thf(f1062,plain,(
% 0.64/0.43 ~spl17_1 | spl17_4),
% 0.64/0.43 inference(avatar_contradiction_clause,[],[f1061])).
% 0.64/0.43 thf(f1066,plain,(
% 0.64/0.43 (((ord_less_eq @ nat @ (size_size @ list @ a @ ys) @ sK11)) = $true) | ($true != $true) | spl17_9),
% 0.64/0.43 inference(superposition,[],[f1000,f910])).
% 0.64/0.43 thf(f1071,plain,(
% 0.64/0.43 (((ord_less_eq @ nat @ (size_size @ list @ a @ ys) @ sK11)) = $true) | spl17_9),
% 0.64/0.43 inference(trivial_inequality_removal,[],[f1066])).
% 0.64/0.43 thf(f1077,plain,(
% 0.64/0.43 spl17_8 | ~spl17_9 | spl17_4),
% 0.64/0.43 inference(avatar_split_clause,[],[f1045,f959,f998,f993])).
% 0.64/0.43 thf(f1099,plain,(
% 0.64/0.43 (((ord_less @ nat @ (size_size @ list @ a @ ys) @ (size_size @ list @ a @ xs))) = $true) | ~spl17_8),
% 0.64/0.43 inference(superposition,[],[f897,f995])).
% 0.64/0.43 thf(f1106,plain,(
% 0.64/0.43 $false | (spl17_2 | ~spl17_8)),
% 0.64/0.43 inference(forward_subsumption_resolution,[],[f1099,f947])).
% 0.64/0.43 thf(f1107,plain,(
% 0.64/0.43 spl17_2 | ~spl17_8),
% 0.64/0.43 inference(avatar_contradiction_clause,[],[f1106])).
% 0.64/0.43 thf(f1113,plain,(
% 0.64/0.43 spl17_10 | spl17_9),
% 0.64/0.43 inference(avatar_split_clause,[],[f1071,f998,f1007])).
% 0.64/0.43 thf(f1184,plain,(
% 0.64/0.43 (((ord_less_eq @ nat @ sK11 @ (size_size @ list @ a @ xs))) != $true) | ($true != $true) | (spl17_2 | ~spl17_10)),
% 0.64/0.43 inference(superposition,[],[f948,f1008])).
% 0.64/0.43 thf(f1186,plain,(
% 0.64/0.43 (((ord_less_eq @ nat @ sK11 @ (size_size @ list @ a @ xs))) != $true) | (spl17_2 | ~spl17_10)),
% 0.64/0.43 inference(trivial_inequality_removal,[],[f1184])).
% 0.64/0.43 thf(f1226,plain,(
% 0.64/0.43 (((ord_less @ nat @ sK11 @ (size_size @ list @ a @ xs))) != $true) | ($true != $true) | (spl17_2 | ~spl17_10)),
% 0.64/0.43 inference(superposition,[],[f1186,f906])).
% 0.64/0.43 thf(f1235,plain,(
% 0.64/0.43 (((ord_less @ nat @ sK11 @ (size_size @ list @ a @ xs))) != $true) | (spl17_2 | ~spl17_10)),
% 0.64/0.43 inference(trivial_inequality_removal,[],[f1226])).
% 0.64/0.43 thf(f1238,plain,(
% 0.64/0.43 $false | (spl17_2 | ~spl17_10)),
% 0.64/0.43 inference(forward_subsumption_resolution,[],[f1235,f897])).
% 0.64/0.43 thf(f1239,plain,(
% 0.64/0.43 spl17_2 | ~spl17_10),
% 0.64/0.43 inference(avatar_contradiction_clause,[],[f1238])).
% 0.64/0.43 cnf(s1, plain, spl17_1 | ~spl17_2, inference(sat_conversion,[],[f936])).
% 0.64/0.43 cnf(s2, plain, ~spl17_3 | ~spl17_4, inference(sat_conversion,[],[f962])).
% 0.64/0.43 cnf(s4, plain, spl17_3, inference(sat_conversion,[],[f977])).
% 0.64/0.43 cnf(s12, plain, ~spl17_1 | spl17_4, inference(sat_conversion,[],[f1062])).
% 0.64/0.43 cnf(s15, plain, spl17_4 | spl17_8 | ~spl17_9, inference(sat_conversion,[],[f1077])).
% 0.64/0.43 cnf(s16, plain, spl17_2 | ~spl17_8, inference(sat_conversion,[],[f1107])).
% 0.64/0.43 cnf(s19, plain, spl17_9 | spl17_10, inference(sat_conversion,[],[f1113])).
% 0.64/0.43 cnf(s26, plain, spl17_2 | ~spl17_10, inference(sat_conversion,[],[f1239])).
% 0.64/0.43 cnf(s27, plain, ~spl17_4, inference(rat,[],[s2,s4])).
% 0.64/0.43 cnf(s28, plain, ~spl17_1, inference(rat,[],[s12,s27])).
% 0.64/0.43 cnf(s29, plain, ~spl17_2, inference(rat,[],[s1,s28])).
% 0.64/0.43 cnf(s30, plain, ~spl17_10, inference(rat,[],[s26,s29])).
% 0.64/0.43 cnf(s31, plain, ~spl17_8, inference(rat,[],[s16,s29])).
% 0.64/0.43 cnf(s33, plain, spl17_9, inference(rat,[],[s19,s30])).
% 0.64/0.43 cnf(s34, plain, $false, inference(rat,[],[s15,s27,s33,s31])).
% 0.64/0.43 thf(f1240,plain,(
% 0.64/0.43 $false),
% 0.64/0.43 inference(avatar_sat_refutation,[],[s34])).
% 0.64/0.43 % SZS output end Proof for theBenchmark
% 0.64/0.43 % (811925)------------------------------
% 0.64/0.43 % (811925)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.64/0.43 % (811925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.64/0.43 % (811925)CaDiCaL version: 2.1.3
% 0.64/0.43 % (811925)Termination reason: Refutation
% 0.64/0.43 % (811925)Time elapsed: 0.040 s
% 0.64/0.43 % (811925)Peak memory usage: 14 MB
% 0.64/0.43 % (811925)Instructions burned: 74 (million)
% 0.64/0.43 % (811892)Success in time 0.166 s
% 0.64/0.43 % Vampire exiting
%------------------------------------------------------------------------------