%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYO868^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n026.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:48:30 AM UTC 2026
% Result : Theorem 1.16s 0.50s
% Output : Refutation 1.16s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO868^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.20 % Computer : n026.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Tue Sep 29 17:24:27 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.24 Running higher-order theorem proving
% 0.21/0.27 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.53/0.47 % (903857)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.53/0.47 % (903863)lrs+10_16_si=on:nwc=1.5:random_seed=2175188504:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.53/0.47 % (903862)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=2626205306:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.53/0.47 % (903864)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=1637586914:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.53/0.47 % (903864)Instruction limit reached!
% 0.53/0.47 % (903864)------------------------------
% 0.53/0.47 % (903864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.53/0.47 % (903864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.53/0.47 % (903864)CaDiCaL version: 2.1.3
% 0.53/0.47 % (903864)Termination reason: Instruction limit
% 0.53/0.47 % (903864)Termination phase: shuffling
% 0.53/0.47 % (903864)Time elapsed: 0.002 s
% 0.53/0.47 % (903864)Peak memory usage: 10 MB
% 0.53/0.47 % (903864)Instructions burned: 4 (million)
% 0.53/0.47 % (903863)Instruction limit reached!
% 0.53/0.47 % (903863)------------------------------
% 0.53/0.47 % (903863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.53/0.47 % (903863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.53/0.47 % (903863)CaDiCaL version: 2.1.3
% 0.53/0.47 % (903863)Termination reason: Instruction limit
% 0.53/0.47 % (903863)Termination phase: Property scanning
% 0.53/0.47 % (903863)Time elapsed: 0.009 s
% 0.53/0.47 % (903863)Peak memory usage: 10 MB
% 0.53/0.47 % (903863)Instructions burned: 19 (million)
% 0.53/0.47 % (903866)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=717195640:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.53/0.47 % (903872)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=328632326:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.53/0.47 % (903872)Instruction limit reached!
% 0.53/0.47 % (903872)------------------------------
% 0.53/0.47 % (903872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.53/0.47 % (903872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.53/0.47 % (903872)CaDiCaL version: 2.1.3
% 0.53/0.47 % (903872)Termination reason: Instruction limit
% 0.53/0.47 % (903872)Termination phase: shuffling
% 0.53/0.47 % (903872)Time elapsed: 0.002 s
% 0.53/0.47 % (903872)Peak memory usage: 10 MB
% 0.53/0.47 % (903872)Instructions burned: 3 (million)
% 0.53/0.47 % (903868)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.53/0.47 % (903868)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.53/0.47 % (903873)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=3913915866:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.53/0.47 % (903868)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=1682731461:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.53/0.47 % (903865)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=3338375851: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.53/0.47 % (903867)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=3658495178:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.53/0.47 % (903873)Instruction limit reached!
% 0.53/0.47 % (903873)------------------------------
% 0.53/0.47 % (903873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.53/0.47 % (903873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.53/0.47 % (903873)CaDiCaL version: 2.1.3
% 0.53/0.47 % (903873)Termination reason: Instruction limit
% 0.53/0.47 % (903873)Termination phase: shuffling
% 0.53/0.47 % (903873)Time elapsed: 0.003 s
% 0.53/0.47 % (903873)Peak memory usage: 10 MB
% 0.53/0.47 % (903873)Instructions burned: 8 (million)
% 0.53/0.47 % (903866)Instruction limit reached!
% 1.16/0.50 % (903866)------------------------------
% 1.16/0.50 % (903866)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.50 % (903866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.50 % (903866)CaDiCaL version: 2.1.3
% 1.16/0.50 % (903866)Termination reason: Instruction limit
% 1.16/0.50 % (903866)Termination phase: Naming
% 1.16/0.50 % (903866)Time elapsed: 0.020 s
% 1.16/0.50 % (903866)Peak memory usage: 10 MB
% 1.16/0.50 % (903866)Instructions burned: 25 (million)
% 1.16/0.50 % (903876)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.16/0.50 % (903862)Instruction limit reached!
% 1.16/0.50 % (903862)------------------------------
% 1.16/0.50 % (903862)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.50 % (903862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.50 % (903862)CaDiCaL version: 2.1.3
% 1.16/0.50 % (903862)Termination reason: Instruction limit
% 1.16/0.50 % (903862)Termination phase: Property scanning
% 1.16/0.50 % (903862)Time elapsed: 0.053 s
% 1.16/0.50 % (903862)Peak memory usage: 11 MB
% 1.16/0.50 % (903862)Instructions burned: 88 (million)
% 1.16/0.50 % (903876)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=981528482:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 1.16/0.50 % (903882)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 1.16/0.50 % (903882)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.16/0.50 % (903881)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=1518043473:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 1.16/0.50 % (903876)Instruction limit reached!
% 1.16/0.50 % (903876)------------------------------
% 1.16/0.50 % (903876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.50 % (903876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.50 % (903876)CaDiCaL version: 2.1.3
% 1.16/0.50 % (903876)Termination reason: Instruction limit
% 1.16/0.50 % (903876)Termination phase: shuffling
% 1.16/0.50 % (903876)Time elapsed: 0.007 s
% 1.16/0.50 % (903876)Peak memory usage: 10 MB
% 1.16/0.50 % (903876)Instructions burned: 7 (million)
% 1.16/0.50 % (903882)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=679359004:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 1.16/0.50 % (903881)Instruction limit reached!
% 1.16/0.50 % (903881)------------------------------
% 1.16/0.50 % (903881)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.50 % (903881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.50 % (903881)CaDiCaL version: 2.1.3
% 1.16/0.50 % (903881)Termination reason: Instruction limit
% 1.16/0.50 % (903881)Termination phase: shuffling
% 1.16/0.50 % (903881)Time elapsed: 0.006 s
% 1.16/0.50 % (903881)Peak memory usage: 10 MB
% 1.16/0.50 % (903881)Instructions burned: 12 (million)
% 1.16/0.50 % (903882)Instruction limit reached!
% 1.16/0.50 % (903882)------------------------------
% 1.16/0.50 % (903882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.50 % (903882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.50 % (903882)CaDiCaL version: 2.1.3
% 1.16/0.50 % (903882)Termination reason: Instruction limit
% 1.16/0.50 % (903882)Termination phase: Property scanning
% 1.16/0.50 % (903882)Time elapsed: 0.012 s
% 1.16/0.50 % (903882)Peak memory usage: 10 MB
% 1.16/0.50 % (903882)Instructions burned: 28 (million)
% 1.16/0.50 % (903867)Instruction limit reached!
% 1.16/0.50 % (903867)------------------------------
% 1.16/0.50 % (903867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.50 % (903867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.50 % (903867)CaDiCaL version: 2.1.3
% 1.16/0.50 % (903867)Termination reason: Instruction limit
% 1.16/0.50 % (903867)Termination phase: Function definition elimination
% 1.16/0.50 % (903867)Time elapsed: 0.054 s
% 1.16/0.50 % (903867)Peak memory usage: 11 MB
% 1.16/0.50 % (903867)Instructions burned: 76 (million)
% 1.16/0.50 % (903884)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=904374692:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 1.16/0.50 % (903888)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 1.16/0.50 % (903888)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=3351849898:i=2:add=on:rtra=on_2998 on theBenchmark for (2998ds/2Mi)
% 1.16/0.50 % (903889)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=1713732703:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/38Mi)
% 1.16/0.50 % (903888)Instruction limit reached!
% 1.16/0.50 % (903888)------------------------------
% 1.16/0.50 % (903888)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.50 % (903888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.50 % (903888)CaDiCaL version: 2.1.3
% 1.16/0.50 % (903888)Termination reason: Instruction limit
% 1.16/0.50 % (903888)Termination phase: shuffling
% 1.16/0.50 % (903888)Time elapsed: 0.003 s
% 1.16/0.50 % (903888)Peak memory usage: 9 MB
% 1.16/0.50 % (903888)Instructions burned: 3 (million)
% 1.16/0.50 % (903886)lrs+10_1_si=on:cs=on:random_seed=3402538941:i=8:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.16/0.50 % (903868)Instruction limit reached!
% 1.16/0.50 % (903868)------------------------------
% 1.16/0.50 % (903868)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.50 % (903868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.50 % (903868)CaDiCaL version: 2.1.3
% 1.16/0.50 % (903868)Termination reason: Instruction limit
% 1.16/0.50 % (903868)Termination phase: Saturation
% 1.16/0.50 % (903868)Time elapsed: 0.073 s
% 1.16/0.50 % (903868)Peak memory usage: 12 MB
% 1.16/0.50 % (903868)Instructions burned: 157 (million)
% 1.16/0.50 % (903886)Instruction limit reached!
% 1.16/0.50 % (903886)------------------------------
% 1.16/0.50 % (903886)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.50 % (903886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.50 % (903886)CaDiCaL version: 2.1.3
% 1.16/0.50 % (903886)Termination reason: Instruction limit
% 1.16/0.50 % (903886)Termination phase: shuffling
% 1.16/0.50 % (903886)Time elapsed: 0.008 s
% 1.16/0.50 % (903886)Peak memory usage: 10 MB
% 1.16/0.50 % (903886)Instructions burned: 8 (million)
% 1.16/0.50 % (903890)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=3943270161:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 1.16/0.50 % (903895)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=2507638810:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 1.16/0.50 % (903895)Instruction limit reached!
% 1.16/0.50 % (903895)------------------------------
% 1.16/0.50 % (903895)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.50 % (903895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.50 % (903895)CaDiCaL version: 2.1.3
% 1.16/0.50 % (903895)Termination reason: Instruction limit
% 1.16/0.50 % (903895)Termination phase: SInE selection
% 1.16/0.50 % (903895)Time elapsed: 0.012 s
% 1.16/0.50 % (903895)Peak memory usage: 10 MB
% 1.16/0.50 % (903895)Instructions burned: 27 (million)
% 1.16/0.50 % (903889)Instruction limit reached!
% 1.16/0.50 % (903889)------------------------------
% 1.16/0.50 % (903889)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.50 % (903889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.50 % (903889)CaDiCaL version: 2.1.3
% 1.16/0.50 % (903889)Termination reason: Instruction limit
% 1.16/0.50 % (903889)Termination phase: Property scanning
% 1.16/0.50 % (903889)Time elapsed: 0.044 s
% 1.16/0.50 % (903889)Peak memory usage: 11 MB
% 1.16/0.50 % (903889)Instructions burned: 39 (million)
% 1.16/0.50 % (903884)Instruction limit reached!
% 1.16/0.50 % (903884)------------------------------
% 1.16/0.50 % (903884)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.50 % (903884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.50 % (903884)CaDiCaL version: 2.1.3
% 1.16/0.50 % (903884)Termination reason: Instruction limit
% 1.16/0.50 % (903884)Termination phase: Property scanning
% 1.16/0.50 % (903884)Time elapsed: 0.053 s
% 1.16/0.50 % (903884)Peak memory usage: 10 MB
% 1.16/0.50 % (903884)Instructions burned: 87 (million)
% 1.16/0.50 % (903897)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=1842215079:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 1.16/0.50 % (903896)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=415249299:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.16/0.50 % (903896)Instruction limit reached!
% 1.16/0.50 % (903896)------------------------------
% 1.16/0.50 % (903896)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.50 % (903896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.50 % (903896)CaDiCaL version: 2.1.3
% 1.16/0.50 % (903896)Termination reason: Instruction limit
% 1.16/0.50 % (903896)Termination phase: Property scanning
% 1.16/0.50 % (903896)Time elapsed: 0.015 s
% 1.16/0.50 % (903896)Peak memory usage: 10 MB
% 1.16/0.50 % (903896)Instructions burned: 15 (million)
% 1.16/0.50 % (903900)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=4232612670:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.16/0.50 % (903865) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-903857-903865"...
% 1.16/0.50 % (903901)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=3264136672: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.16/0.50 % (903865)...printing done.
% 1.16/0.50 % (903900)Instruction limit reached!
% 1.16/0.50 % (903900)------------------------------
% 1.16/0.50 % (903900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.50 % (903900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.50 % (903900)CaDiCaL version: 2.1.3
% 1.16/0.50 % (903900)Termination reason: Instruction limit
% 1.16/0.50 % (903900)Termination phase: Property scanning
% 1.16/0.50 % (903900)Time elapsed: 0.006 s
% 1.16/0.50 % (903900)Peak memory usage: 10 MB
% 1.16/0.50 % (903900)Instructions burned: 15 (million)
% 1.16/0.50 % (903865)Refutation found. Thanks to Tanya!
% 1.16/0.50 % SZS status Theorem for theBenchmark
% 1.16/0.50 % SZS output start Proof for theBenchmark
% 1.16/0.50 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 1.16/0.50 thf(func_def_0, type, c_Eps_i: (($i > $o) > $i)).
% 1.16/0.50 thf(func_def_1, type, c_False: $o).
% 1.16/0.50 thf(func_def_2, type, c_True: $o).
% 1.16/0.50 thf(func_def_3, type, c_not: ($o > $o)).
% 1.16/0.50 thf(func_def_4, type, c_and: ($o > $o > $o)).
% 1.16/0.50 thf(func_def_5, type, c_or: ($o > $o > $o)).
% 1.16/0.50 thf(func_def_6, type, c_iff: ($o > $o > $o)).
% 1.16/0.50 thf(func_def_7, type, c_In: ($i > $i > $o)).
% 1.16/0.50 thf(func_def_8, type, c_Subq: ($i > $i > $o)).
% 1.16/0.50 thf(func_def_10, type, c_Union: ($i > $i)).
% 1.16/0.50 thf(func_def_11, type, c_Power: ($i > $i)).
% 1.16/0.50 thf(func_def_12, type, c_Repl: ($i > ($i > $i) > $i)).
% 1.16/0.50 thf(func_def_13, type, c_TransSet: ($i > $o)).
% 1.16/0.50 thf(func_def_14, type, c_atleast2: ($i > $o)).
% 1.16/0.50 thf(func_def_15, type, c_atleast3: ($i > $o)).
% 1.16/0.50 thf(func_def_16, type, c_atleast4: ($i > $o)).
% 1.16/0.50 thf(func_def_17, type, c_atleast5: ($i > $o)).
% 1.16/0.50 thf(func_def_18, type, c_atleast6: ($i > $o)).
% 1.16/0.50 thf(func_def_19, type, c_exactly2: ($i > $o)).
% 1.16/0.50 thf(func_def_20, type, c_exactly3: ($i > $o)).
% 1.16/0.50 thf(func_def_21, type, c_exactly4: ($i > $o)).
% 1.16/0.50 thf(func_def_22, type, c_exactly5: ($i > $o)).
% 1.16/0.50 thf(func_def_23, type, c_exu_i: (($i > $o) > $o)).
% 1.16/0.50 thf(func_def_24, type, c_reflexive_i: (($i > $i > $o) > $o)).
% 1.16/0.50 thf(func_def_25, type, c_irreflexive_i: (($i > $i > $o) > $o)).
% 1.16/0.50 thf(func_def_26, type, c_symmetric_i: (($i > $i > $o) > $o)).
% 1.16/0.50 thf(func_def_27, type, c_antisymmetric_i: (($i > $i > $o) > $o)).
% 1.16/0.50 thf(func_def_28, type, c_transitive_i: (($i > $i > $o) > $o)).
% 1.16/0.50 thf(func_def_29, type, c_eqreln_i: (($i > $i > $o) > $o)).
% 1.16/0.50 thf(func_def_30, type, c_per_i: (($i > $i > $o) > $o)).
% 1.16/0.50 thf(func_def_31, type, c_linear_i: (($i > $i > $o) > $o)).
% 1.16/0.50 thf(func_def_32, type, c_trichotomous_or_i: (($i > $i > $o) > $o)).
% 1.16/0.50 thf(func_def_33, type, c_partialorder_i: (($i > $i > $o) > $o)).
% 1.16/0.50 thf(func_def_34, type, c_totalorder_i: (($i > $i > $o) > $o)).
% 1.16/0.50 thf(func_def_35, type, c_strictpartialorder_i: (($i > $i > $o) > $o)).
% 1.16/0.50 thf(func_def_36, type, c_stricttotalorder_i: (($i > $i > $o) > $o)).
% 1.16/0.50 thf(func_def_37, type, c_If_i: ($o > $i > $i > $i)).
% 1.16/0.50 thf(func_def_38, type, c_exactly1of2: ($o > $o > $o)).
% 1.16/0.50 thf(func_def_39, type, c_exactly1of3: ($o > $o > $o > $o)).
% 1.16/0.50 thf(func_def_40, type, c_nIn: ($i > $i > $o)).
% 1.16/0.50 thf(func_def_41, type, c_nSubq: ($i > $i > $o)).
% 1.16/0.50 thf(func_def_42, type, c_UPair: ($i > $i > $i)).
% 1.16/0.50 thf(func_def_43, type, c_Sing: ($i > $i)).
% 1.16/0.50 thf(func_def_44, type, c_binunion: ($i > $i > $i)).
% 1.16/0.50 thf(func_def_45, type, c_SetAdjoin: ($i > $i > $i)).
% 1.16/0.50 thf(func_def_46, type, c_famunion: ($i > ($i > $i) > $i)).
% 1.16/0.50 thf(func_def_47, type, c_Sep: ($i > ($i > $o) > $i)).
% 1.16/0.50 thf(func_def_48, type, c_ReplSep: ($i > ($i > $o) > ($i > $i) > $i)).
% 1.16/0.50 thf(func_def_49, type, c_binintersect: ($i > $i > $i)).
% 1.16/0.50 thf(func_def_50, type, c_setminus: ($i > $i > $i)).
% 1.16/0.50 thf(func_def_51, type, c_inj: ($i > $i > ($i > $i) > $o)).
% 1.16/0.50 thf(func_def_52, type, c_bij: ($i > $i > ($i > $i) > $o)).
% 1.16/0.50 thf(func_def_53, type, c_atleastp: ($i > $i > $o)).
% 1.16/0.50 thf(func_def_54, type, c_equip: ($i > $i > $o)).
% 1.16/0.50 thf(func_def_55, type, c_In_rec_poly_G_i: (($i > ($i > $i) > $i) > $i > $i > $o)).
% 1.16/0.50 thf(func_def_56, type, c_In_rec_poly_i: (($i > ($i > $i) > $i) > $i > $i)).
% 1.16/0.50 thf(func_def_57, type, c_ordsucc: ($i > $i)).
% 1.16/0.50 thf(func_def_58, type, c_nat_p: ($i > $o)).
% 1.16/0.50 thf(func_def_59, type, c_nat_primrec: ($i > ($i > $i > $i) > $i > $i)).
% 1.16/0.50 thf(func_def_60, type, c_add_nat: ($i > $i > $i)).
% 1.16/0.50 thf(func_def_61, type, c_mul_nat: ($i > $i > $i)).
% 1.16/0.50 thf(func_def_62, type, c_ordinal: ($i > $o)).
% 1.16/0.50 thf(func_def_63, type, c_V_: ($i > $i)).
% 1.16/0.50 thf(func_def_64, type, c_Inj1: ($i > $i)).
% 1.16/0.50 thf(func_def_65, type, c_Inj0: ($i > $i)).
% 1.16/0.50 thf(func_def_66, type, c_Unj: ($i > $i)).
% 1.16/0.50 thf(func_def_67, type, c_combine_funcs: ($i > $i > ($i > $i) > ($i > $i) > $i > $i)).
% 1.16/0.50 thf(func_def_68, type, c_setsum: ($i > $i > $i)).
% 1.16/0.50 thf(func_def_69, type, c_proj0: ($i > $i)).
% 1.16/0.50 thf(func_def_70, type, c_proj1: ($i > $i)).
% 1.16/0.50 thf(func_def_71, type, c_binrep: ($i > $i > $i)).
% 1.16/0.50 thf(func_def_72, type, c_lam: ($i > ($i > $i) > $i)).
% 1.16/0.50 thf(func_def_73, type, c_setprod: ($i > $i > $i)).
% 1.16/0.50 thf(func_def_74, type, c_ap: ($i > $i > $i)).
% 1.16/0.50 thf(func_def_75, type, c_setsum_p: ($i > $o)).
% 1.16/0.50 thf(func_def_76, type, c_tuple_p: ($i > $i > $o)).
% 1.16/0.50 thf(func_def_77, type, c_Pi: ($i > ($i > $i) > $i)).
% 1.16/0.50 thf(func_def_78, type, c_setexp: ($i > $i > $i)).
% 1.16/0.50 thf(func_def_79, type, c_Sep2: ($i > ($i > $i) > ($i > $i > $o) > $i)).
% 1.16/0.50 thf(func_def_80, type, c_set_of_pairs: ($i > $o)).
% 1.16/0.50 thf(func_def_81, type, c_lam2: ($i > ($i > $i) > ($i > $i > $i) > $i)).
% 1.16/0.50 thf(func_def_82, type, c_PNoEq_: ($i > ($i > $o) > ($i > $o) > $o)).
% 1.16/0.50 thf(func_def_83, type, c_PNoLt_: ($i > ($i > $o) > ($i > $o) > $o)).
% 1.16/0.50 thf(func_def_84, type, c_PNoLt: ($i > ($i > $o) > $i > ($i > $o) > $o)).
% 1.16/0.50 thf(func_def_85, type, c_PNoLe: ($i > ($i > $o) > $i > ($i > $o) > $o)).
% 1.16/0.50 thf(func_def_86, type, c_PNo_downc: (($i > ($i > $o) > $o) > $i > ($i > $o) > $o)).
% 1.16/0.50 thf(func_def_87, type, c_PNo_upc: (($i > ($i > $o) > $o) > $i > ($i > $o) > $o)).
% 1.16/0.50 thf(func_def_88, type, c_SNoElts_: ($i > $i)).
% 1.16/0.50 thf(func_def_89, type, c_SNo_: ($i > $i > $o)).
% 1.16/0.50 thf(func_def_90, type, c_PSNo: ($i > ($i > $o) > $i)).
% 1.16/0.50 thf(func_def_91, type, c_SNo: ($i > $o)).
% 1.16/0.50 thf(func_def_92, type, c_SNoLev: ($i > $i)).
% 1.16/0.50 thf(func_def_93, type, c_SNoEq_: ($i > $i > $i > $o)).
% 1.16/0.50 thf(func_def_94, type, c_SNoLt: ($i > $i > $o)).
% 1.16/0.50 thf(func_def_95, type, c_SNoLe: ($i > $i > $o)).
% 1.16/0.50 thf(func_def_96, type, c_binop_on: ($i > ($i > $i > $i) > $o)).
% 1.16/0.50 thf(func_def_97, type, c_Loop: ($i > ($i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > $i > $o)).
% 1.16/0.50 thf(func_def_98, type, c_Loop_with_defs: ($i > ($i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > $i > ($i > $i > $i) > ($i > $i > $i > $i) > ($i > $i > $i) > ($i > $i > $i > $i) > ($i > $i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > $o)).
% 1.16/0.50 thf(func_def_99, type, c_Loop_with_defs_cex1: ($i > ($i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > $i > ($i > $i > $i) > ($i > $i > $i > $i) > ($i > $i > $i) > ($i > $i > $i > $i) > ($i > $i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > $o)).
% 1.16/0.50 thf(func_def_100, type, c_Loop_with_defs_cex2: ($i > ($i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > $i > ($i > $i > $i) > ($i > $i > $i > $i) > ($i > $i > $i) > ($i > $i > $i > $i) > ($i > $i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > $o)).
% 1.16/0.50 thf(func_def_101, type, c_combinator: ($i > $o)).
% 1.16/0.50 thf(func_def_102, type, c_combinator_equiv: ($i > $i > $o)).
% 1.16/0.50 thf(func_def_103, type, c_equip_mod: ($i > $i > $i > $o)).
% 1.16/0.50 thf(func_def_105, type, db0: !>[X0: $tType]:(X0)).
% 1.16/0.50 thf(func_def_106, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 1.16/0.50 thf(func_def_107, type, db2: !>[X0: $tType]:(X0)).
% 1.16/0.50 thf(func_def_108, type, db1: !>[X0: $tType]:(X0)).
% 1.16/0.50 thf(func_def_109, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 1.16/0.50 thf(func_def_110, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 1.16/0.50 thf(func_def_111, type, vIMP: ($o > $o > $o)).
% 1.16/0.50 thf(func_def_112, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 1.16/0.50 thf(func_def_113, type, db3: !>[X0: $tType]:(X0)).
% 1.16/0.50 thf(func_def_114, type, db4: !>[X0: $tType]:(X0)).
% 1.16/0.50 thf(func_def_117, type, db13: !>[X0: $tType]:(X0)).
% 1.16/0.50 thf(func_def_118, type, db12: !>[X0: $tType]:(X0)).
% 1.16/0.50 thf(func_def_119, type, db11: !>[X0: $tType]:(X0)).
% 1.16/0.50 thf(func_def_120, type, db10: !>[X0: $tType]:(X0)).
% 1.16/0.50 thf(func_def_121, type, db9: !>[X0: $tType]:(X0)).
% 1.16/0.50 thf(func_def_122, type, db8: !>[X0: $tType]:(X0)).
% 1.16/0.50 thf(func_def_123, type, db7: !>[X0: $tType]:(X0)).
% 1.16/0.50 thf(func_def_124, type, db6: !>[X0: $tType]:(X0)).
% 1.16/0.50 thf(func_def_125, type, db5: !>[X0: $tType]:(X0)).
% 1.16/0.50 thf(func_def_126, type, db14: !>[X0: $tType]:(X0)).
% 1.16/0.50 thf(func_def_127, type, db15: !>[X0: $tType]:(X0)).
% 1.16/0.50 thf(func_def_128, type, db16: !>[X0: $tType]:(X0)).
% 1.16/0.50 thf(func_def_129, type, db17: !>[X0: $tType]:(X0)).
% 1.16/0.50 thf(func_def_130, type, db18: !>[X0: $tType]:(X0)).
% 1.16/0.50 thf(func_def_131, type, sP0: (($i > $o) > $o)).
% 1.16/0.50 thf(func_def_132, type, sK1: $o).
% 1.16/0.50 thf(func_def_136, type, sK5: ($i > $i)).
% 1.16/0.50 thf(func_def_137, type, sK6: (($i > $o) > $i)).
% 1.16/0.50 thf(func_def_138, type, sK7: $o).
% 1.16/0.50 thf(func_def_139, type, sK8: (($i > $o) > $i)).
% 1.16/0.50 thf(func_def_140, type, sK9: (($i > $o) > $i)).
% 1.16/0.50 thf(func_def_141, type, sK10: (($i > $o) > $i)).
% 1.16/0.50 thf(func_def_142, type, sK11: (($i > $o) > $i > $i)).
% 1.16/0.50 thf(func_def_143, type, sK12: (($i > $o) > $i)).
% 1.16/0.50 thf(func_def_144, type, sK13: (($i > $o) > $i)).
% 1.16/0.50 thf(func_def_145, type, vNOT: ($o > $o)).
% 1.16/0.50 thf(f5,axiom,(
% 1.16/0.50 (c_not @ ? [X0 : $i] : (c_In @ X0 @ c_Empty))),
% 1.16/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5)).
% 1.16/0.50 thf(f11,axiom,(
% 1.16/0.50 (c_False = ! [X0 : $o] : X0)),
% 1.16/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax11)).
% 1.16/0.50 thf(f13,axiom,(
% 1.16/0.50 (c_not = (^[X0 : $o] : (X0 => c_False)))),
% 1.16/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax13)).
% 1.16/0.50 thf(f109,conjecture,(
% 1.16/0.50 ! [X0 : $i] : ((c_In @ X0 @ c_Empty) => ! [X1 : $i] : ((c_In @ X1 @ X0) => ! [X2 : $i] : ((c_In @ X2 @ X1) => ? [X3 : $i] : ! [X4 : $i] : (((c_ordinal @ X3) => (c_and @ (c_exactly2 @ X3) @ (c_not @ (c_exactly5 @ X4)))) => ((((c_ordinal @ X3) => (c_exactly2 @ X3)) => ((c_atleast2 @ X3) => ((((c_not @ (c_atleast2 @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)))) => (X3 = X4)) => (c_atleast3 @ X3)) => (c_and @ (c_atleast5 @ X2) @ (c_not @ (c_exactly1of2 @ (c_SNoLt @ X2 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ (c_Power @ c_Empty)))) @ c_Empty)) @ (c_TransSet @ X4))))))) => (c_nat_p @ X3))))))),
% 1.16/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj)).
% 1.16/0.50 thf(f110,negated_conjecture,(
% 1.16/0.50 ~ ! [X0 : $i] : ((c_In @ X0 @ c_Empty) => ! [X1 : $i] : ((c_In @ X1 @ X0) => ! [X2 : $i] : ((c_In @ X2 @ X1) => ? [X3 : $i] : ! [X4 : $i] : (((c_ordinal @ X3) => (c_and @ (c_exactly2 @ X3) @ (c_not @ (c_exactly5 @ X4)))) => ((((c_ordinal @ X3) => (c_exactly2 @ X3)) => ((c_atleast2 @ X3) => ((((c_not @ (c_atleast2 @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)))) => (X3 = X4)) => (c_atleast3 @ X3)) => (c_and @ (c_atleast5 @ X2) @ (c_not @ (c_exactly1of2 @ (c_SNoLt @ X2 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ (c_Power @ c_Empty)))) @ c_Empty)) @ (c_TransSet @ X4))))))) => (c_nat_p @ X3))))))),
% 1.16/0.50 inference(negated_conjecture,[status(cth)],[f109])).
% 1.16/0.50 thf(f156,plain,(
% 1.16/0.50 ~ ! [X0 : $i] : ((c_In @ X0 @ c_Empty) => ! [X1 : $i] : ((c_In @ X1 @ X0) => ! [X2 : $i] : ((c_In @ X2 @ X1) => ? [X3 : $i] : ! [X4 : $i] : (((c_ordinal @ X3) => (c_and @ (c_exactly2 @ X3) @ (c_not @ (c_exactly5 @ X4)))) => ((((c_ordinal @ X3) => (c_exactly2 @ X3)) => ((c_atleast2 @ X3) => ((((c_not @ (c_atleast2 @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)))) => (X3 = X4)) => (c_atleast3 @ X3)) => (c_and @ (c_atleast5 @ X2) @ (c_not @ (c_exactly1of2 @ (c_SNoLt @ X2 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ (c_Power @ c_Empty)))) @ c_Empty)) @ (c_TransSet @ X4))))))) => (c_nat_p @ X3))))))),
% 1.16/0.50 inference(rectify,[],[f110])).
% 1.16/0.50 thf(f157,plain,(
% 1.16/0.50 ~ ! [X0 : $i] : ((((c_In @ X0 @ c_Empty)) = $true) => ! [X1 : $i] : ((((c_In @ X1 @ X0)) = $true) => ! [X2 : $i] : ((((c_In @ X2 @ X1)) = $true) => ? [X3 : $i] : ! [X4 : $i] : (((((c_ordinal @ X3)) = $true) => (((c_and @ (c_exactly2 @ X3) @ (c_not @ (c_exactly5 @ X4)))) = $true)) => ((((((c_ordinal @ X3)) = $true) => (((c_exactly2 @ X3)) = $true)) => ((((c_atleast2 @ X3)) = $true) => ((((((c_not @ (c_atleast2 @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty))))) = $true) => (X3 = X4)) => (((c_atleast3 @ X3)) = $true)) => (((c_and @ (c_atleast5 @ X2) @ (c_not @ (c_exactly1of2 @ (c_SNoLt @ X2 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ (c_Power @ c_Empty)))) @ c_Empty)) @ (c_TransSet @ X4))))) = $true)))) => (((c_nat_p @ X3)) = $true))))))),
% 1.16/0.50 inference(fool_elimination,[],[f156])).
% 1.16/0.50 thf(f163,plain,(
% 1.16/0.50 (c_not = (^[X0 : $o] : (X0 => c_False)))),
% 1.16/0.50 inference(rectify,[],[f13])).
% 1.16/0.50 thf(f164,plain,(
% 1.16/0.50 (c_not = (^[Y0 : $o]: (Y0 => c_False)))),
% 1.16/0.50 inference(fool_elimination,[],[f163])).
% 1.16/0.50 thf(f215,plain,(
% 1.16/0.50 (c_not @ ? [X0 : $i] : (c_In @ X0 @ c_Empty))),
% 1.16/0.50 inference(rectify,[],[f5])).
% 1.16/0.50 thf(f216,plain,(
% 1.16/0.50 ($true = ((c_not @ (?? @ $i @ (^[Y0 : $i]: (c_In @ Y0 @ c_Empty))))))),
% 1.16/0.50 inference(fool_elimination,[],[f215])).
% 1.16/0.50 thf(f302,plain,(
% 1.16/0.50 (c_False = ! [X0 : $o] : X0)),
% 1.16/0.50 inference(rectify,[],[f11])).
% 1.16/0.50 thf(f303,plain,(
% 1.16/0.50 ! [X0 : $o] : ($true = X0) <=> (c_False = $true)),
% 1.16/0.50 inference(fool_elimination,[],[f302])).
% 1.16/0.50 thf(f309,plain,(
% 1.16/0.50 ? [X0 : $i] : (? [X1 : $i] : (? [X2 : $i] : (! [X3 : $i] : ? [X4 : $i] : (((((c_nat_p @ X3)) != $true) & ((((((c_and @ (c_atleast5 @ X2) @ (c_not @ (c_exactly1of2 @ (c_SNoLt @ X2 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ (c_Power @ c_Empty)))) @ c_Empty)) @ (c_TransSet @ X4))))) = $true) | ((((c_atleast3 @ X3)) != $true) & ((((c_not @ (c_atleast2 @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty))))) != $true) | (X3 = X4)))) | (((c_atleast2 @ X3)) != $true)) | ((((c_ordinal @ X3)) = $true) & (((c_exactly2 @ X3)) != $true)))) & ((((c_and @ (c_exactly2 @ X3) @ (c_not @ (c_exactly5 @ X4)))) = $true) | (((c_ordinal @ X3)) != $true))) & (((c_In @ X2 @ X1)) = $true)) & (((c_In @ X1 @ X0)) = $true)) & (((c_In @ X0 @ c_Empty)) = $true))),
% 1.16/0.50 inference(ennf_transformation,[],[f157])).
% 1.16/0.50 thf(f310,plain,(
% 1.16/0.50 ? [X0 : $i] : (? [X1 : $i] : (? [X2 : $i] : (! [X3 : $i] : ? [X4 : $i] : ((((c_nat_p @ X3)) != $true) & (((((c_ordinal @ X3)) = $true) & (((c_exactly2 @ X3)) != $true)) | (((c_atleast2 @ X3)) != $true) | (((c_and @ (c_atleast5 @ X2) @ (c_not @ (c_exactly1of2 @ (c_SNoLt @ X2 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ (c_Power @ c_Empty)))) @ c_Empty)) @ (c_TransSet @ X4))))) = $true) | ((((c_atleast3 @ X3)) != $true) & ((((c_not @ (c_atleast2 @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty))))) != $true) | (X3 = X4)))) & ((((c_and @ (c_exactly2 @ X3) @ (c_not @ (c_exactly5 @ X4)))) = $true) | (((c_ordinal @ X3)) != $true))) & (((c_In @ X2 @ X1)) = $true)) & (((c_In @ X1 @ X0)) = $true)) & (((c_In @ X0 @ c_Empty)) = $true))),
% 1.16/0.50 inference(flattening,[],[f309])).
% 1.16/0.50 thf(f320,definition,(
% 1.16/0.50 ! [X0 : ($i > $o)] : (? [X1 : $i] : (? [X2 : $i] : ((((X0 @ X2)) != $true) & (((c_In @ X2 @ X1)) = $true)) & (((X0 @ X1)) = $true)) | ~ (((sP0 @ X0)) = $true))),
% 1.16/0.50 introduced(definition,[new_symbols(definition,[=])],[predicate_definition_introduction])).
% 1.16/0.50 thf(f326,plain,(
% 1.16/0.50 ((! [X3 : $i] : ((((c_nat_p @ X3)) != $true) & (((((c_ordinal @ X3)) = $true) & (((c_exactly2 @ X3)) != $true)) | (((c_atleast2 @ X3)) != $true) | ($true = ((c_and @ (c_atleast5 @ sK4) @ (c_not @ (c_exactly1of2 @ (c_SNoLt @ sK4 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ (c_Power @ c_Empty)))) @ c_Empty)) @ (c_TransSet @ (sK5 @ X3))))))) | ((((c_atleast3 @ X3)) != $true) & ((((c_not @ (c_atleast2 @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty))))) != $true) | (((sK5 @ X3)) = X3)))) & (($true = ((c_and @ (c_exactly2 @ X3) @ (c_not @ (c_exactly5 @ (sK5 @ X3)))))) | (((c_ordinal @ X3)) != $true))) & ($true = ((c_In @ sK4 @ sK3)))) & ($true = ((c_In @ sK3 @ sK2)))) & (((c_In @ sK2 @ c_Empty)) = $true)),
% 1.16/0.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4,vAPP]),skolemize(X0,sK2),skolemize(X1,sK3),skolemize(X2,sK4),skolemize(X4,sK5 @ X3)],[f310])).
% 1.16/0.50 thf(f330,plain,(
% 1.16/0.50 (! [X0 : $o] : ($true = X0) | (c_False != $true)) & ((c_False = $true) | ? [X0 : $o] : ($true != X0))),
% 1.16/0.50 inference(nnf_transformation,[],[f303])).
% 1.16/0.50 thf(f331,plain,(
% 1.16/0.50 (! [X0 : $o] : ($true = X0) | (c_False != $true)) & ((c_False = $true) | ? [X1 : $o] : ($true != X1))),
% 1.16/0.50 inference(rectify,[],[f330])).
% 1.16/0.50 thf(f332,plain,(
% 1.16/0.50 (! [X0 : $o] : ($true = X0) | (c_False != $true)) & ((c_False = $true) | ($true != sK7))),
% 1.16/0.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X1,sK7)],[f331])).
% 1.16/0.50 thf(f333,plain,(
% 1.16/0.50 ! [X0 : ($i > $o)] : (? [X1 : $i] : (? [X2 : $i] : ((((X0 @ X2)) != $true) & (((c_In @ X2 @ X1)) = $true)) & (((X0 @ X1)) = $true)) | (((sP0 @ X0)) != $true))),
% 1.16/0.50 inference(nnf_transformation,[],[f320])).
% 1.16/0.50 thf(f334,plain,(
% 1.16/0.50 ! [X0 : ($i > $o)] : (((($true != ((X0 @ (sK9 @ X0)))) & ($true = ((c_In @ (sK9 @ X0) @ (sK8 @ X0))))) & ($true = ((X0 @ (sK8 @ X0))))) | (((sP0 @ X0)) != $true))),
% 1.16/0.50 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP,vAPP]),skolemize(X4,sK5 @ X3),skolemize(X4,sK5 @ X3)],[f333])).
% 1.16/0.50 thf(f358,plain,(
% 1.16/0.50 (((c_In @ sK2 @ c_Empty)) = $true)),
% 1.16/0.50 inference(cnf_transformation,[],[f326])).
% 1.16/0.50 thf(f390,plain,(
% 1.16/0.50 ($true = ((c_not @ (?? @ $i @ (^[Y0 : $i]: (c_In @ Y0 @ c_Empty))))))),
% 1.16/0.50 inference(cnf_transformation,[],[f216])).
% 1.16/0.50 thf(f408,plain,(
% 1.16/0.50 (c_not = (^[Y0 : $o]: (Y0 => c_False)))),
% 1.16/0.50 inference(cnf_transformation,[],[f164])).
% 1.16/0.50 thf(f425,plain,(
% 1.16/0.50 ( ! [X0 : $o] : (($true = X0) | (c_False != $true)) )),
% 1.16/0.50 inference(cnf_transformation,[],[f332])).
% 1.16/0.50 thf(f451,plain,(
% 1.16/0.50 ( ! [X0 : ($i > $o)] : (($true != ((X0 @ (sK9 @ X0)))) | (((sP0 @ X0)) != $true)) )),
% 1.16/0.50 inference(cnf_transformation,[],[f334])).
% 1.16/0.50 thf(f604,definition,(
% 1.16/0.50 spl14_21 <=> (c_not = (^[Y0 : $o]: (Y0 => c_False)))),
% 1.16/0.50 introduced(definition,[new_symbols(definition,[spl14_21])],[avatar_definition])).
% 1.16/0.50 thf(f606,plain,(
% 1.16/0.50 (c_not = (^[Y0 : $o]: (Y0 => c_False))) | ~spl14_21),
% 1.16/0.50 inference(avatar_component_clause,[],[f604])).
% 1.16/0.50 thf(f607,plain,(
% 1.16/0.50 spl14_21),
% 1.16/0.50 inference(avatar_split_clause,[],[f408,f604])).
% 1.16/0.50 thf(f788,definition,(
% 1.16/0.50 spl14_58 <=> (((c_In @ sK2 @ c_Empty)) = $true)),
% 1.16/0.50 introduced(definition,[new_symbols(definition,[spl14_58])],[avatar_definition])).
% 1.16/0.50 thf(f790,plain,(
% 1.16/0.50 (((c_In @ sK2 @ c_Empty)) = $true) | ~spl14_58),
% 1.16/0.50 inference(avatar_component_clause,[],[f788])).
% 1.16/0.50 thf(f791,plain,(
% 1.16/0.50 spl14_58),
% 1.16/0.50 inference(avatar_split_clause,[],[f358,f788])).
% 1.16/0.50 thf(f823,definition,(
% 1.16/0.50 spl14_65 <=> ! [X0 : $o] : ($true = X0)),
% 1.16/0.50 introduced(definition,[new_symbols(definition,[spl14_65])],[avatar_definition])).
% 1.16/0.50 thf(f824,plain,(
% 1.16/0.50 ( ! [X0 : $o] : (($true = X0)) ) | ~spl14_65),
% 1.16/0.50 inference(avatar_component_clause,[],[f823])).
% 1.16/0.50 thf(f826,definition,(
% 1.16/0.50 spl14_66 <=> (c_False = $true)),
% 1.16/0.50 introduced(definition,[new_symbols(definition,[spl14_66])],[avatar_definition])).
% 1.16/0.50 thf(f828,plain,(
% 1.16/0.50 (c_False != $true) | spl14_66),
% 1.16/0.50 inference(avatar_component_clause,[],[f826])).
% 1.16/0.50 thf(f829,plain,(
% 1.16/0.50 spl14_65 | ~spl14_66),
% 1.16/0.50 inference(avatar_split_clause,[],[f425,f826,f823])).
% 1.16/0.50 thf(f965,definition,(
% 1.16/0.50 spl14_94 <=> ($true = ((c_not @ (?? @ $i @ (^[Y0 : $i]: (c_In @ Y0 @ c_Empty))))))),
% 1.16/0.50 introduced(definition,[new_symbols(definition,[spl14_94])],[avatar_definition])).
% 1.16/0.50 thf(f967,plain,(
% 1.16/0.50 ($true = ((c_not @ (?? @ $i @ (^[Y0 : $i]: (c_In @ Y0 @ c_Empty)))))) | ~spl14_94),
% 1.16/0.50 inference(avatar_component_clause,[],[f965])).
% 1.16/0.50 thf(f968,plain,(
% 1.16/0.50 spl14_94),
% 1.16/0.50 inference(avatar_split_clause,[],[f390,f965])).
% 1.16/0.50 thf(f1150,definition,(
% 1.16/0.50 spl14_129 <=> ($true = ((c_not @ $true)))),
% 1.16/0.50 introduced(definition,[new_symbols(definition,[spl14_129])],[avatar_definition])).
% 1.16/0.50 thf(f1151,plain,(
% 1.16/0.50 ($true = ((c_not @ $true))) | ~spl14_129),
% 1.16/0.50 inference(avatar_component_clause,[],[f1150])).
% 1.16/0.50 thf(f1152,plain,(
% 1.16/0.50 ($true != ((c_not @ $true))) | spl14_129),
% 1.16/0.50 inference(avatar_component_clause,[],[f1150])).
% 1.16/0.50 thf(f1239,plain,(
% 1.16/0.50 ((((^[Y0 : $i]: ($true)) @ (sK9 @ (^[Y0 : $i]: ($true))))) != $true) | ($true != ((sP0 @ (^[Y0 : $i]: ($true)))))),
% 1.16/0.50 inference(primitive_instantiation,[],[f451])).
% 1.16/0.50 thf(f1243,plain,(
% 1.16/0.50 ($true != $true) | ($true != ((sP0 @ (^[Y0 : $i]: ($true)))))),
% 1.16/0.50 inference(beta-eta_normalization,[],[f1239])).
% 1.16/0.50 thf(f1244,plain,(
% 1.16/0.50 ($true != ((sP0 @ (^[Y0 : $i]: ($true)))))),
% 1.16/0.50 inference(trivial_inequality_removal,[],[f1243])).
% 1.16/0.50 thf(f1251,definition,(
% 1.16/0.50 spl14_142 <=> ($true = ((sP0 @ (^[Y0 : $i]: ($true)))))),
% 1.16/0.50 introduced(definition,[new_symbols(definition,[spl14_142])],[avatar_definition])).
% 1.16/0.50 thf(f1253,plain,(
% 1.16/0.50 ($true != ((sP0 @ (^[Y0 : $i]: ($true))))) | spl14_142),
% 1.16/0.50 inference(avatar_component_clause,[],[f1251])).
% 1.16/0.50 thf(f1254,plain,(
% 1.16/0.50 ~spl14_142),
% 1.16/0.50 inference(avatar_split_clause,[],[f1244,f1251])).
% 1.16/0.50 thf(f1292,plain,(
% 1.16/0.50 $false | (~spl14_65 | spl14_142)),
% 1.16/0.50 inference(forward_subsumption_resolution,[],[f1253,f824])).
% 1.16/0.50 thf(f1293,plain,(
% 1.16/0.50 ~spl14_65 | spl14_142),
% 1.16/0.50 inference(avatar_contradiction_clause,[],[f1292])).
% 1.16/0.50 thf(f1618,plain,(
% 1.16/0.50 ( ! [X1 : $o] : ((((c_not @ X1)) = (((^[Y0 : $o]: (Y0 => c_False)) @ X1)))) ) | ~spl14_21),
% 1.16/0.50 inference(argument_congruence,[],[f606])).
% 1.16/0.50 thf(f1620,plain,(
% 1.16/0.50 ( ! [X1 : $o] : (($true = (((^[Y0 : $o]: (Y0 => c_False)) @ X1))) | (((c_not @ X1)) = $false)) ) | ~spl14_21),
% 1.16/0.50 inference(iff_proxy_clausification,[],[f1618])).
% 1.16/0.50 thf(f1621,plain,(
% 1.16/0.50 ( ! [X1 : $o] : ((((c_not @ X1)) = $false) | ($true = ((X1 => c_False)))) ) | ~spl14_21),
% 1.16/0.50 inference(beta-eta_normalization,[],[f1620])).
% 1.16/0.50 thf(f1622,plain,(
% 1.16/0.50 ( ! [X1 : $o] : ((((c_not @ X1)) = $false) | (c_False = $true) | ($false = X1)) ) | ~spl14_21),
% 1.16/0.50 inference(imp_proxy_clausification,[],[f1621])).
% 1.16/0.50 thf(f1627,plain,(
% 1.16/0.50 ( ! [X1 : $o] : ((((c_not @ X1)) = $false) | ($false = X1)) ) | (~spl14_21 | spl14_66)),
% 1.16/0.50 inference(forward_subsumption_resolution,[],[f1622,f828])).
% 1.16/0.50 thf(f1628,plain,(
% 1.16/0.50 ($true = ((c_not @ $true))) | ($false = ((?? @ $i @ (^[Y0 : $i]: (c_In @ Y0 @ c_Empty))))) | ~spl14_94),
% 1.16/0.50 inference(fool_paramodulation,[],[f967])).
% 1.16/0.50 thf(f1632,plain,(
% 1.16/0.50 ( ! [X1 : $i] : (($true = ((c_not @ $true))) | ($false = (((^[Y0 : $i]: (c_In @ Y0 @ c_Empty)) @ X1)))) ) | ~spl14_94),
% 1.16/0.50 inference(pi_proxy_clausification,[],[f1628])).
% 1.16/0.50 thf(f1633,plain,(
% 1.16/0.50 ( ! [X1 : $i] : (($true = ((c_not @ $true))) | ($false = ((c_In @ X1 @ c_Empty)))) ) | ~spl14_94),
% 1.16/0.50 inference(beta-eta_normalization,[],[f1632])).
% 1.16/0.50 thf(f1634,plain,(
% 1.16/0.50 ( ! [X1 : $i] : (($false = ((c_In @ X1 @ c_Empty)))) ) | (~spl14_94 | spl14_129)),
% 1.16/0.50 inference(forward_subsumption_resolution,[],[f1633,f1152])).
% 1.16/0.50 thf(f1635,plain,(
% 1.16/0.50 ($false = $true) | (~spl14_58 | ~spl14_94 | spl14_129)),
% 1.16/0.50 inference(superposition,[],[f1634,f790])).
% 1.16/0.50 thf(f1639,plain,(
% 1.16/0.50 $false | (~spl14_58 | ~spl14_94 | spl14_129)),
% 1.16/0.50 inference(trivial_inequality_removal,[],[f1635])).
% 1.16/0.50 thf(f1640,plain,(
% 1.16/0.50 ~spl14_58 | ~spl14_94 | spl14_129),
% 1.16/0.50 inference(avatar_contradiction_clause,[],[f1639])).
% 1.16/0.50 thf(f1776,plain,(
% 1.16/0.50 ($false = $true) | ($false = $true) | (~spl14_21 | spl14_66 | ~spl14_129)),
% 1.16/0.50 inference(superposition,[],[f1627,f1151])).
% 1.16/0.50 thf(f1798,plain,(
% 1.16/0.50 ($false = $true) | (~spl14_21 | spl14_66 | ~spl14_129)),
% 1.16/0.50 inference(duplicate_literal_removal,[],[f1776])).
% 1.16/0.50 thf(f1799,plain,(
% 1.16/0.50 $false | (~spl14_21 | spl14_66 | ~spl14_129)),
% 1.16/0.50 inference(trivial_inequality_removal,[],[f1798])).
% 1.16/0.50 thf(f1800,plain,(
% 1.16/0.50 ~spl14_21 | spl14_66 | ~spl14_129),
% 1.16/0.50 inference(avatar_contradiction_clause,[],[f1799])).
% 1.16/0.50 cnf(s20, plain, spl14_21, inference(sat_conversion,[],[f607])).
% 1.16/0.50 cnf(s56, plain, spl14_58, inference(sat_conversion,[],[f791])).
% 1.16/0.50 cnf(s63, plain, spl14_65 | ~spl14_66, inference(sat_conversion,[],[f829])).
% 1.16/0.50 cnf(s91, plain, spl14_94, inference(sat_conversion,[],[f968])).
% 1.16/0.50 cnf(s137, plain, ~spl14_142, inference(sat_conversion,[],[f1254])).
% 1.16/0.50 cnf(s139, plain, ~spl14_65 | spl14_142, inference(sat_conversion,[],[f1293])).
% 1.16/0.50 cnf(s181, plain, ~spl14_58 | ~spl14_94 | spl14_129, inference(sat_conversion,[],[f1640])).
% 1.16/0.50 cnf(s213, plain, ~spl14_21 | spl14_66 | ~spl14_129, inference(sat_conversion,[],[f1800])).
% 1.16/0.50 cnf(s217, plain, ~spl14_65, inference(rat,[],[s139,s137])).
% 1.16/0.50 cnf(s218, plain, ~spl14_66, inference(rat,[],[s63,s217])).
% 1.16/0.50 cnf(s222, plain, spl14_129, inference(rat,[],[s181,s91,s56])).
% 1.16/0.50 cnf(s227, plain, ~spl14_21, inference(rat,[],[s213,s218,s222])).
% 1.16/0.50 cnf(s232, plain, $false, inference(rat,[],[s20,s227])).
% 1.16/0.50 thf(f1806,plain,(
% 1.16/0.50 $false),
% 1.16/0.50 inference(avatar_sat_refutation,[],[s232])).
% 1.16/0.50 % SZS output end Proof for theBenchmark
% 1.16/0.50 % (903865)------------------------------
% 1.16/0.50 % (903865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.50 % (903865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.50 % (903865)CaDiCaL version: 2.1.3
% 1.16/0.50 % (903865)Termination reason: Refutation
% 1.16/0.50 % (903865)Time elapsed: 0.137 s
% 1.16/0.50 % (903865)Peak memory usage: 15 MB
% 1.16/0.50 % (903865)Instructions burned: 154 (million)
% 1.16/0.50 % (903857)Success in time 0.218 s
% 1.16/0.50 % Vampire exiting
%------------------------------------------------------------------------------