%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU621^1 : TPTP v9.3.1. Released v3.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n001.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:30:22 AM UTC 2026
% Result : Theorem 8.00s 1.65s
% Output : Refutation 8.00s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU621^1 : TPTP v9.3.1. Released v3.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.17 % Computer : n001.cluster.edu
% 0.07/0.17 % Model : x86_64 x86_64
% 0.07/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.17 % Memory : 8046.5625MB
% 0.07/0.17 % OS : Linux 6.8.0-71-generic
% 0.07/0.17 % CPULimit : 300
% 0.07/0.17 % WCLimit : 300
% 0.07/0.17 % DateTime : Tue Sep 29 14:04:36 UTC 2026
% 0.07/0.17 % CPUTime :
% 0.07/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.20 Running higher-order theorem proving
% 0.07/0.24 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.80/0.38 % (1287825)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.80/0.38 % (1287831)lrs+10_16_si=on:nwc=1.5:random_seed=3805374539:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.80/0.38 % (1287831)Instruction limit reached!
% 0.80/0.38 % (1287831)------------------------------
% 0.80/0.38 % (1287831)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.80/0.38 % (1287831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.80/0.38 % (1287831)CaDiCaL version: 2.1.3
% 0.80/0.38 % (1287831)Termination reason: Instruction limit
% 0.80/0.38 % (1287831)Termination phase: Property scanning
% 0.80/0.38 % (1287831)Time elapsed: 0.004 s
% 0.80/0.38 % (1287831)Peak memory usage: 10 MB
% 0.80/0.38 % (1287831)Instructions burned: 19 (million)
% 0.80/0.38 % (1287830)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=1477017128:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.80/0.38 % (1287832)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=1051460110:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.80/0.38 % (1287834)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=3493657085:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.80/0.38 % (1287833)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=1197767704: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.80/0.38 % (1287832)Instruction limit reached!
% 0.80/0.38 % (1287832)------------------------------
% 0.80/0.38 % (1287832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.80/0.38 % (1287832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.80/0.38 % (1287832)CaDiCaL version: 2.1.3
% 0.80/0.38 % (1287832)Termination reason: Instruction limit
% 0.80/0.38 % (1287832)Termination phase: shuffling
% 0.80/0.38 % (1287832)Time elapsed: 0.002 s
% 0.80/0.38 % (1287832)Peak memory usage: 10 MB
% 0.80/0.38 % (1287832)Instructions burned: 4 (million)
% 0.80/0.38 % (1287838)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=154733613:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.80/0.38 % (1287838)Instruction limit reached!
% 0.80/0.38 % (1287838)------------------------------
% 0.80/0.38 % (1287838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.80/0.38 % (1287838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.80/0.38 % (1287838)CaDiCaL version: 2.1.3
% 0.80/0.38 % (1287838)Termination reason: Instruction limit
% 0.80/0.38 % (1287838)Termination phase: shuffling
% 0.80/0.38 % (1287838)Time elapsed: 0.001 s
% 0.80/0.38 % (1287838)Peak memory usage: 10 MB
% 0.80/0.38 % (1287838)Instructions burned: 3 (million)
% 0.80/0.38 % (1287834)Instruction limit reached!
% 0.80/0.38 % (1287834)------------------------------
% 0.80/0.38 % (1287834)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.80/0.38 % (1287836)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.80/0.38 % (1287834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.80/0.38 % (1287834)CaDiCaL version: 2.1.3
% 0.80/0.38 % (1287836)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.80/0.38 % (1287834)Termination reason: Instruction limit
% 0.80/0.38 % (1287834)Termination phase: Preprocessing 3
% 0.80/0.38 % (1287834)Time elapsed: 0.012 s
% 0.80/0.38 % (1287834)Peak memory usage: 11 MB
% 0.80/0.38 % (1287834)Instructions burned: 24 (million)
% 0.80/0.38 % (1287835)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=835527251:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.80/0.38 % (1287845)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.80/0.38 % (1287845)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=708965744:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.80/0.42 % (1287836)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=858810580:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.80/0.42 % (1287843)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=1129246822:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.80/0.42 % (1287845)Instruction limit reached!
% 0.80/0.42 % (1287845)------------------------------
% 0.80/0.42 % (1287845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.80/0.42 % (1287845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.80/0.42 % (1287845)CaDiCaL version: 2.1.3
% 0.80/0.42 % (1287845)Termination reason: Instruction limit
% 0.80/0.42 % (1287845)Termination phase: shuffling
% 0.80/0.42 % (1287845)Time elapsed: 0.003 s
% 0.80/0.42 % (1287845)Peak memory usage: 10 MB
% 0.80/0.42 % (1287845)Instructions burned: 14 (million)
% 0.80/0.42 % (1287843)Instruction limit reached!
% 0.80/0.42 % (1287843)------------------------------
% 0.80/0.42 % (1287843)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.80/0.42 % (1287843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.80/0.42 % (1287843)CaDiCaL version: 2.1.3
% 0.80/0.42 % (1287843)Termination reason: Instruction limit
% 0.80/0.42 % (1287843)Termination phase: shuffling
% 0.80/0.42 % (1287843)Time elapsed: 0.003 s
% 0.80/0.42 % (1287843)Peak memory usage: 10 MB
% 0.80/0.42 % (1287843)Instructions burned: 7 (million)
% 0.80/0.42 % (1287851)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.80/0.42 % (1287851)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.80/0.42 % (1287846)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=3356150490:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.80/0.42 % (1287851)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=1093386364: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.80/0.42 % (1287846)Instruction limit reached!
% 0.80/0.42 % (1287846)------------------------------
% 0.80/0.42 % (1287846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.80/0.42 % (1287846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.80/0.42 % (1287846)CaDiCaL version: 2.1.3
% 0.80/0.42 % (1287846)Termination reason: Instruction limit
% 0.80/0.42 % (1287846)Termination phase: shuffling
% 0.80/0.42 % (1287846)Time elapsed: 0.006 s
% 0.80/0.42 % (1287846)Peak memory usage: 10 MB
% 0.80/0.42 % (1287846)Instructions burned: 14 (million)
% 0.80/0.42 % (1287851)Instruction limit reached!
% 0.80/0.42 % (1287851)------------------------------
% 0.80/0.42 % (1287851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.80/0.42 % (1287851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.80/0.42 % (1287851)CaDiCaL version: 2.1.3
% 0.80/0.42 % (1287851)Termination reason: Instruction limit
% 0.80/0.42 % (1287851)Termination phase: Property scanning
% 0.80/0.42 % (1287851)Time elapsed: 0.007 s
% 0.80/0.42 % (1287851)Peak memory usage: 10 MB
% 0.80/0.42 % (1287851)Instructions burned: 31 (million)
% 0.80/0.42 % (1287856)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.80/0.42 % (1287852)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=1330997368:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.80/0.42 % (1287856)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=2159456172:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.80/0.42 % (1287835)Instruction limit reached!
% 0.80/0.42 % (1287835)------------------------------
% 0.80/0.42 % (1287835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.80/0.42 % (1287835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.80/0.42 % (1287835)CaDiCaL version: 2.1.3
% 0.80/0.46 % (1287835)Termination reason: Instruction limit
% 0.80/0.46 % (1287835)Termination phase: Property scanning
% 0.80/0.46 % (1287835)Time elapsed: 0.034 s
% 0.80/0.46 % (1287835)Peak memory usage: 12 MB
% 0.80/0.46 % (1287835)Instructions burned: 76 (million)
% 0.80/0.46 % (1287856)Instruction limit reached!
% 0.80/0.46 % (1287856)------------------------------
% 0.80/0.46 % (1287856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.80/0.46 % (1287856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.80/0.46 % (1287856)CaDiCaL version: 2.1.3
% 0.80/0.46 % (1287856)Termination reason: Instruction limit
% 0.80/0.46 % (1287856)Termination phase: shuffling
% 0.80/0.46 % (1287856)Time elapsed: 0.001 s
% 0.80/0.46 % (1287856)Peak memory usage: 10 MB
% 0.80/0.46 % (1287856)Instructions burned: 5 (million)
% 0.80/0.46 % (1287855)lrs+10_1_si=on:cs=on:random_seed=3662032892:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.80/0.46 % (1287860)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=3874592557:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.80/0.46 % (1287855)Instruction limit reached!
% 0.80/0.46 % (1287855)------------------------------
% 0.80/0.46 % (1287855)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.80/0.46 % (1287855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.80/0.46 % (1287855)CaDiCaL version: 2.1.3
% 0.80/0.46 % (1287855)Termination reason: Instruction limit
% 0.80/0.46 % (1287855)Termination phase: shuffling
% 0.80/0.46 % (1287855)Time elapsed: 0.004 s
% 0.80/0.46 % (1287855)Peak memory usage: 10 MB
% 0.80/0.46 % (1287855)Instructions burned: 9 (million)
% 0.80/0.46 % (1287830)Instruction limit reached!
% 0.80/0.46 % (1287830)------------------------------
% 0.80/0.46 % (1287830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.80/0.46 % (1287830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.80/0.46 % (1287830)CaDiCaL version: 2.1.3
% 0.80/0.46 % (1287830)Termination reason: Instruction limit
% 0.80/0.46 % (1287830)Termination phase: Saturation
% 0.80/0.46 % (1287830)Time elapsed: 0.064 s
% 0.80/0.46 % (1287830)Peak memory usage: 13 MB
% 0.80/0.46 % (1287830)Instructions burned: 87 (million)
% 0.80/0.46 % (1287859)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=4049862209:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.80/0.46 % (1287863)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=389496935:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/25Mi)
% 0.80/0.46 % (1287864)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=2202091704:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 0.80/0.46 % (1287859)Instruction limit reached!
% 0.80/0.46 % (1287859)------------------------------
% 0.80/0.46 % (1287859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.80/0.46 % (1287859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.80/0.46 % (1287859)CaDiCaL version: 2.1.3
% 0.80/0.46 % (1287859)Termination reason: Instruction limit
% 0.80/0.46 % (1287859)Termination phase: Preprocessing 3
% 0.80/0.46 % (1287859)Time elapsed: 0.018 s
% 0.80/0.46 % (1287859)Peak memory usage: 12 MB
% 0.80/0.46 % (1287859)Instructions burned: 38 (million)
% 0.80/0.46 % (1287863)Instruction limit reached!
% 0.80/0.46 % (1287863)------------------------------
% 0.80/0.46 % (1287863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.80/0.46 % (1287863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.80/0.46 % (1287863)CaDiCaL version: 2.1.3
% 0.80/0.46 % (1287863)Termination reason: Instruction limit
% 0.80/0.46 % (1287863)Termination phase: Preprocessing 3
% 0.80/0.46 % (1287863)Time elapsed: 0.012 s
% 0.80/0.46 % (1287863)Peak memory usage: 11 MB
% 0.80/0.46 % (1287863)Instructions burned: 26 (million)
% 0.80/0.46 % (1287864)Instruction limit reached!
% 0.80/0.46 % (1287864)------------------------------
% 0.80/0.46 % (1287864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.80/0.46 % (1287864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.80/0.46 % (1287864)CaDiCaL version: 2.1.3
% 0.80/0.46 % (1287864)Termination reason: Instruction limit
% 0.80/0.46 % (1287864)Termination phase: shuffling
% 1.59/0.54 % (1287864)Time elapsed: 0.011 s
% 1.59/0.54 % (1287864)Peak memory usage: 10 MB
% 1.59/0.54 % (1287864)Instructions burned: 14 (million)
% 1.59/0.54 % (1287868)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=1109767812:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 1.59/0.54 % (1287869)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=509493903:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.59/0.54 % (1287870)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=3528761641: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.59/0.54 % (1287870)Instruction limit reached!
% 1.59/0.54 % (1287870)------------------------------
% 1.59/0.54 % (1287870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.59/0.54 % (1287870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.59/0.54 % (1287870)CaDiCaL version: 2.1.3
% 1.59/0.54 % (1287870)Termination reason: Instruction limit
% 1.59/0.54 % (1287870)Termination phase: shuffling
% 1.59/0.54 % (1287870)Time elapsed: 0.002 s
% 1.59/0.54 % (1287870)Peak memory usage: 10 MB
% 1.59/0.54 % (1287870)Instructions burned: 4 (million)
% 1.59/0.54 % (1287852)Instruction limit reached!
% 1.59/0.54 % (1287852)------------------------------
% 1.59/0.54 % (1287852)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.59/0.54 % (1287852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.59/0.54 % (1287852)CaDiCaL version: 2.1.3
% 1.59/0.54 % (1287852)Termination reason: Instruction limit
% 1.59/0.54 % (1287852)Termination phase: Saturation
% 1.59/0.54 % (1287852)Time elapsed: 0.070 s
% 1.59/0.54 % (1287852)Peak memory usage: 13 MB
% 1.59/0.54 % (1287852)Instructions burned: 87 (million)
% 1.59/0.54 % (1287869)Instruction limit reached!
% 1.59/0.54 % (1287869)------------------------------
% 1.59/0.54 % (1287869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.59/0.54 % (1287869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.59/0.54 % (1287869)CaDiCaL version: 2.1.3
% 1.59/0.54 % (1287869)Termination reason: Instruction limit
% 1.59/0.54 % (1287869)Termination phase: shuffling
% 1.59/0.54 % (1287869)Time elapsed: 0.006 s
% 1.59/0.54 % (1287869)Peak memory usage: 10 MB
% 1.59/0.54 % (1287869)Instructions burned: 14 (million)
% 1.59/0.54 % (1287860)Instruction limit reached!
% 1.59/0.54 % (1287860)------------------------------
% 1.59/0.54 % (1287860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.59/0.54 % (1287860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.59/0.54 % (1287860)CaDiCaL version: 2.1.3
% 1.59/0.54 % (1287860)Termination reason: Instruction limit
% 1.59/0.54 % (1287860)Termination phase: Saturation
% 1.59/0.54 % (1287860)Time elapsed: 0.068 s
% 1.59/0.54 % (1287860)Peak memory usage: 14 MB
% 1.59/0.54 % (1287860)Instructions burned: 252 (million)
% 1.59/0.54 % (1287836)Instruction limit reached!
% 1.59/0.54 % (1287836)------------------------------
% 1.59/0.54 % (1287836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.59/0.54 % (1287836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.59/0.54 % (1287836)CaDiCaL version: 2.1.3
% 1.59/0.54 % (1287836)Termination reason: Instruction limit
% 1.59/0.54 % (1287836)Termination phase: Saturation
% 1.59/0.54 % (1287836)Time elapsed: 0.111 s
% 1.59/0.54 % (1287836)Peak memory usage: 14 MB
% 1.59/0.54 % (1287836)Instructions burned: 158 (million)
% 1.59/0.54 % (1287874)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3387212522:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.59/0.54 % (1287877)WARNING Broken Constraint: if sine_to_age_generality_threshold(10) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 1.59/0.54 % (1287877)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 1.59/0.54 % (1287876)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=2913788942:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 1.59/0.54 % (1287877)ott+21_1_to=kbo:sil=128000:cnfonf=lazy_gen:bsd=on:si=on:sp=const_frequency:lma=off:uwa=off:foolp=on:s2agt=10:lwlo=on:random_seed=1717243341:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 2.26/0.63 % (1287875)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=1000642718:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 2.26/0.63 % (1287877)Instruction limit reached!
% 2.26/0.63 % (1287877)------------------------------
% 2.26/0.63 % (1287877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.26/0.63 % (1287877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.26/0.63 % (1287877)CaDiCaL version: 2.1.3
% 2.26/0.63 % (1287877)Termination reason: Instruction limit
% 2.26/0.63 % (1287877)Termination phase: Property scanning
% 2.26/0.63 % (1287877)Time elapsed: 0.004 s
% 2.26/0.63 % (1287877)Peak memory usage: 10 MB
% 2.26/0.63 % (1287877)Instructions burned: 17 (million)
% 2.26/0.63 % (1287874)Instruction limit reached!
% 2.26/0.63 % (1287874)------------------------------
% 2.26/0.63 % (1287874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.26/0.63 % (1287874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.26/0.63 % (1287874)CaDiCaL version: 2.1.3
% 2.26/0.63 % (1287874)Termination reason: Instruction limit
% 2.26/0.63 % (1287874)Termination phase: Property scanning
% 2.26/0.63 % (1287874)Time elapsed: 0.012 s
% 2.26/0.63 % (1287874)Peak memory usage: 10 MB
% 2.26/0.63 % (1287874)Instructions burned: 27 (million)
% 2.26/0.63 % (1287878)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 2.26/0.63 % (1287878)lrs+1010_4:1_slsqr=8,1:to=kbo:cha=on:drc=off:si=on:sp=arity:lcm=predicate:uwa=off:fd=preordered:gs=on:nwc=5:s2agt=32:slsqc=1:kmz=on:updr=off:chr=on:pe=on:slsq=on:random_seed=44178009:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 2.26/0.63 % (1287883)dis+1004_50_to=lpo:drc=off:fde=unused:cnfonf=lazy_not_gen_be_off:si=on:sp=reverse_arity:spb=units:cbe=off:foolp=on:random_seed=3610831313:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 2.26/0.63 % (1287878)Instruction limit reached!
% 2.26/0.63 % (1287878)------------------------------
% 2.26/0.63 % (1287878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.26/0.63 % (1287878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.26/0.63 % (1287878)CaDiCaL version: 2.1.3
% 2.26/0.63 % (1287878)Termination reason: Instruction limit
% 2.26/0.63 % (1287878)Termination phase: shuffling
% 2.26/0.63 % (1287878)Time elapsed: 0.004 s
% 2.26/0.63 % (1287878)Peak memory usage: 10 MB
% 2.26/0.63 % (1287878)Instructions burned: 8 (million)
% 2.26/0.63 % (1287875)Instruction limit reached!
% 2.26/0.63 % (1287875)------------------------------
% 2.26/0.63 % (1287875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.26/0.63 % (1287875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.26/0.63 % (1287875)CaDiCaL version: 2.1.3
% 2.26/0.63 % (1287875)Termination reason: Instruction limit
% 2.26/0.63 % (1287875)Termination phase: Property scanning
% 2.26/0.63 % (1287875)Time elapsed: 0.020 s
% 2.26/0.63 % (1287875)Peak memory usage: 10 MB
% 2.26/0.63 % (1287875)Instructions burned: 23 (million)
% 2.26/0.63 % (1287883)Instruction limit reached!
% 2.26/0.63 % (1287883)------------------------------
% 2.26/0.63 % (1287883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.26/0.63 % (1287883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.26/0.63 % (1287883)CaDiCaL version: 2.1.3
% 2.26/0.63 % (1287883)Termination reason: Instruction limit
% 2.26/0.63 % (1287883)Termination phase: Property scanning
% 2.26/0.63 % (1287883)Time elapsed: 0.007 s
% 2.26/0.63 % (1287883)Peak memory usage: 10 MB
% 2.26/0.63 % (1287883)Instructions burned: 34 (million)
% 2.26/0.63 % (1287876)Instruction limit reached!
% 2.26/0.63 % (1287876)------------------------------
% 2.26/0.63 % (1287876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.26/0.63 % (1287876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.26/0.63 % (1287876)CaDiCaL version: 2.1.3
% 2.26/0.63 % (1287876)Termination reason: Instruction limit
% 2.26/0.63 % (1287876)Termination phase: Property scanning
% 2.26/0.63 % (1287876)Time elapsed: 0.028 s
% 2.26/0.63 % (1287876)Peak memory usage: 12 MB
% 2.26/0.63 % (1287876)Instructions burned: 61 (million)
% 2.26/0.63 % (1287889)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=2002775088:i=1240:rtra=on:ixr=off_2997 on theBenchmark for (2997ds/1240Mi)
% 2.76/0.70 % (1287887)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=261038759:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 2.76/0.70 % (1287884)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=1233802443:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 2.76/0.70 % (1287884)Instruction limit reached!
% 2.76/0.70 % (1287884)------------------------------
% 2.76/0.70 % (1287884)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.76/0.70 % (1287884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.76/0.70 % (1287884)CaDiCaL version: 2.1.3
% 2.76/0.70 % (1287884)Termination reason: Instruction limit
% 2.76/0.70 % (1287884)Termination phase: shuffling
% 2.76/0.70 % (1287884)Time elapsed: 0.009 s
% 2.76/0.70 % (1287884)Peak memory usage: 10 MB
% 2.76/0.70 % (1287884)Instructions burned: 13 (million)
% 2.76/0.70 % (1287890)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=379327049:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2997 on theBenchmark for (2997ds/143Mi)
% 2.76/0.70 % (1287888)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=2851359359:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 2.76/0.70 % (1287887)Instruction limit reached!
% 2.76/0.70 % (1287887)------------------------------
% 2.76/0.70 % (1287887)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.76/0.70 % (1287887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.76/0.70 % (1287887)CaDiCaL version: 2.1.3
% 2.76/0.70 % (1287887)Termination reason: Instruction limit
% 2.76/0.70 % (1287887)Termination phase: Property scanning
% 2.76/0.70 % (1287887)Time elapsed: 0.017 s
% 2.76/0.70 % (1287887)Peak memory usage: 10 MB
% 2.76/0.70 % (1287887)Instructions burned: 24 (million)
% 2.76/0.70 % (1287894)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=1889007169:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/193Mi)
% 2.76/0.70 % (1287888)Instruction limit reached!
% 2.76/0.70 % (1287888)------------------------------
% 2.76/0.70 % (1287888)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.76/0.70 % (1287888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.76/0.70 % (1287888)CaDiCaL version: 2.1.3
% 2.76/0.70 % (1287888)Termination reason: Instruction limit
% 2.76/0.70 % (1287888)Termination phase: Property scanning
% 2.76/0.70 % (1287888)Time elapsed: 0.017 s
% 2.76/0.70 % (1287888)Peak memory usage: 10 MB
% 2.76/0.70 % (1287888)Instructions burned: 21 (million)
% 2.76/0.70 % (1287899)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 2.76/0.70 % (1287899)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=880165392:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2997 on theBenchmark for (2997ds/7Mi)
% 2.76/0.70 % (1287899)Instruction limit reached!
% 2.76/0.70 % (1287899)------------------------------
% 2.76/0.70 % (1287899)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.76/0.70 % (1287899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.76/0.70 % (1287899)CaDiCaL version: 2.1.3
% 2.76/0.70 % (1287899)Termination reason: Instruction limit
% 2.76/0.70 % (1287899)Termination phase: shuffling
% 2.76/0.70 % (1287899)Time elapsed: 0.004 s
% 2.76/0.70 % (1287899)Peak memory usage: 10 MB
% 2.76/0.70 % (1287899)Instructions burned: 8 (million)
% 2.76/0.70 % (1287897)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=742135508:i=42:hud=10:rtra=on_2997 on theBenchmark for (2997ds/42Mi)
% 2.76/0.70 % (1287897)Instruction limit reached!
% 2.76/0.70 % (1287897)------------------------------
% 2.76/0.70 % (1287897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.76/0.70 % (1287897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.76/0.70 % (1287897)CaDiCaL version: 2.1.3
% 2.76/0.70 % (1287897)Termination reason: Instruction limit
% 2.76/0.70 % (1287897)Termination phase: Function definition elimination
% 2.76/0.70 % (1287897)Time elapsed: 0.018 s
% 2.76/0.70 % (1287897)Peak memory usage: 11 MB
% 2.76/0.70 % (1287897)Instructions burned: 43 (million)
% 2.76/0.70 % (1287901)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=1533141576:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/181Mi)
% 2.76/0.78 % (1287868)Instruction limit reached!
% 2.76/0.78 % (1287868)------------------------------
% 2.76/0.78 % (1287868)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.76/0.78 % (1287868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.76/0.78 % (1287868)CaDiCaL version: 2.1.3
% 2.76/0.78 % (1287868)Termination reason: Instruction limit
% 2.76/0.78 % (1287868)Termination phase: Saturation
% 2.76/0.78 % (1287868)Time elapsed: 0.160 s
% 2.76/0.78 % (1287868)Peak memory usage: 14 MB
% 2.76/0.78 % (1287868)Instructions burned: 328 (million)
% 2.76/0.78 % (1287903)dis+10_8_sil=128000:plsq=on:plsqc=1:si=on:sp=unary_first:sos=on:lma=off:plsqr=64,1:uwa=interpreted_only:foolp=on:random_seed=2334708866:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2997 on theBenchmark for (2997ds/169Mi)
% 2.76/0.78 % (1287905)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 2.76/0.78 % (1287905)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=1676690758:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2996 on theBenchmark for (2996ds/6Mi)
% 2.76/0.78 % (1287905)Instruction limit reached!
% 2.76/0.78 % (1287905)------------------------------
% 2.76/0.78 % (1287905)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.76/0.78 % (1287905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.76/0.78 % (1287905)CaDiCaL version: 2.1.3
% 2.76/0.78 % (1287905)Termination reason: Instruction limit
% 2.76/0.78 % (1287905)Termination phase: shuffling
% 2.76/0.78 % (1287905)Time elapsed: 0.003 s
% 2.76/0.78 % (1287905)Peak memory usage: 10 MB
% 2.76/0.78 % (1287905)Instructions burned: 6 (million)
% 2.76/0.78 % (1287890)Instruction limit reached!
% 2.76/0.78 % (1287890)------------------------------
% 2.76/0.78 % (1287890)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.76/0.78 % (1287890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.76/0.78 % (1287890)CaDiCaL version: 2.1.3
% 2.76/0.78 % (1287890)Termination reason: Instruction limit
% 2.76/0.78 % (1287890)Termination phase: Saturation
% 2.76/0.78 % (1287890)Time elapsed: 0.108 s
% 2.76/0.78 % (1287890)Peak memory usage: 13 MB
% 2.76/0.78 % (1287890)Instructions burned: 144 (million)
% 2.76/0.78 % (1287894)Instruction limit reached!
% 2.76/0.78 % (1287894)------------------------------
% 2.76/0.78 % (1287894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.76/0.78 % (1287894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.76/0.78 % (1287894)CaDiCaL version: 2.1.3
% 2.76/0.78 % (1287894)Termination reason: Instruction limit
% 2.76/0.78 % (1287894)Termination phase: Saturation
% 2.76/0.78 % (1287894)Time elapsed: 0.096 s
% 2.76/0.78 % (1287894)Peak memory usage: 14 MB
% 2.76/0.78 % (1287894)Instructions burned: 194 (million)
% 2.76/0.78 % (1287910)ott+10_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:lma=off:plsqr=128,1:urr=ec_only:uwa=off:rp=on:nwc=20:br=off:random_seed=3482217960:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/316Mi)
% 2.76/0.78 % (1287909)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=235368526:i=19:add=on:rtra=on_2996 on theBenchmark for (2996ds/19Mi)
% 2.76/0.78 % (1287908)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=2523313086:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2996 on theBenchmark for (2996ds/22Mi)
% 2.76/0.78 % (1287833)Instruction limit reached!
% 2.76/0.78 % (1287833)------------------------------
% 2.76/0.78 % (1287833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.76/0.78 % (1287833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.76/0.78 % (1287833)CaDiCaL version: 2.1.3
% 2.76/0.78 % (1287833)Termination reason: Instruction limit
% 2.76/0.78 % (1287833)Termination phase: Saturation
% 2.76/0.78 % (1287833)Time elapsed: 0.348 s
% 2.76/0.78 % (1287833)Peak memory usage: 19 MB
% 2.76/0.78 % (1287833)Instructions burned: 635 (million)
% 2.76/0.78 % (1287908)Instruction limit reached!
% 2.76/0.78 % (1287908)------------------------------
% 2.76/0.78 % (1287908)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.32/0.86 % (1287908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.32/0.86 % (1287908)CaDiCaL version: 2.1.3
% 3.32/0.86 % (1287908)Termination reason: Instruction limit
% 3.32/0.86 % (1287908)Termination phase: Property scanning
% 3.32/0.86 % (1287908)Time elapsed: 0.015 s
% 3.32/0.86 % (1287908)Peak memory usage: 10 MB
% 3.32/0.86 % (1287908)Instructions burned: 22 (million)
% 3.32/0.86 % (1287909)Instruction limit reached!
% 3.32/0.86 % (1287909)------------------------------
% 3.32/0.86 % (1287909)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.32/0.86 % (1287909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.32/0.86 % (1287909)CaDiCaL version: 2.1.3
% 3.32/0.86 % (1287909)Termination reason: Instruction limit
% 3.32/0.86 % (1287909)Termination phase: Property scanning
% 3.32/0.86 % (1287909)Time elapsed: 0.016 s
% 3.32/0.86 % (1287909)Peak memory usage: 10 MB
% 3.32/0.86 % (1287909)Instructions burned: 21 (million)
% 3.32/0.86 % (1287903)Instruction limit reached!
% 3.32/0.86 % (1287903)------------------------------
% 3.32/0.86 % (1287903)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.32/0.86 % (1287903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.32/0.86 % (1287903)CaDiCaL version: 2.1.3
% 3.32/0.86 % (1287903)Termination reason: Instruction limit
% 3.32/0.86 % (1287903)Termination phase: Saturation
% 3.32/0.86 % (1287903)Time elapsed: 0.076 s
% 3.32/0.86 % (1287903)Peak memory usage: 13 MB
% 3.32/0.86 % (1287903)Instructions burned: 171 (million)
% 3.32/0.86 % (1287914)dis+1004_4:1_slsqr=1,2:to=lpo:plsq=on:fde=unused:e2e=on:si=on:spb=goal_then_units:acc=on:urr=on:uwa=off:fd=preordered:s2agt=16:slsqc=1:slsq=on:random_seed=3647570159:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2996 on theBenchmark for (2996ds/853Mi)
% 3.32/0.86 % (1287915)dis+1003_3:4_to=kbo:plsq=on:prc=on:sims=off:e2e=on:si=on:spb=intro:acc=on:urr=on:uwa=off:foolp=on:s2agt=32:slsqc=3:slsq=on:random_seed=4153372957:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2996 on theBenchmark for (2996ds/45Mi)
% 3.32/0.86 % (1287916)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=502212055:i=480:rtra=on_2996 on theBenchmark for (2996ds/480Mi)
% 3.32/0.86 % (1287917)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=1888345334:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2996 on theBenchmark for (2996ds/21Mi)
% 3.32/0.86 % (1287917)Instruction limit reached!
% 3.32/0.86 % (1287917)------------------------------
% 3.32/0.86 % (1287917)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.32/0.86 % (1287917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.32/0.86 % (1287917)CaDiCaL version: 2.1.3
% 3.32/0.86 % (1287917)Termination reason: Instruction limit
% 3.32/0.86 % (1287917)Termination phase: Property scanning
% 3.32/0.86 % (1287917)Time elapsed: 0.009 s
% 3.32/0.86 % (1287917)Peak memory usage: 10 MB
% 3.32/0.86 % (1287917)Instructions burned: 21 (million)
% 3.32/0.86 % (1287915)Instruction limit reached!
% 3.32/0.86 % (1287915)------------------------------
% 3.32/0.86 % (1287915)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.32/0.86 % (1287915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.32/0.86 % (1287915)CaDiCaL version: 2.1.3
% 3.32/0.86 % (1287915)Termination reason: Instruction limit
% 3.32/0.86 % (1287915)Termination phase: Preprocessing 3
% 3.32/0.86 % (1287915)Time elapsed: 0.021 s
% 3.32/0.86 % (1287915)Peak memory usage: 12 MB
% 3.32/0.86 % (1287915)Instructions burned: 45 (million)
% 3.32/0.86 % (1287922)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 3.32/0.86 % (1287922)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=3145709103:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/200Mi)
% 3.32/0.86 % (1287923)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=32286434:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2995 on theBenchmark for (2995ds/13Mi)
% 3.32/0.86 % (1287923)Instruction limit reached!
% 3.32/0.86 % (1287923)------------------------------
% 3.32/0.86 % (1287923)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.87/1.02 % (1287923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.87/1.02 % (1287923)CaDiCaL version: 2.1.3
% 3.87/1.02 % (1287923)Termination reason: Instruction limit
% 3.87/1.02 % (1287923)Termination phase: shuffling
% 3.87/1.02 % (1287923)Time elapsed: 0.006 s
% 3.87/1.02 % (1287923)Peak memory usage: 10 MB
% 3.87/1.02 % (1287923)Instructions burned: 13 (million)
% 3.87/1.02 % (1287901)Instruction limit reached!
% 3.87/1.02 % (1287901)------------------------------
% 3.87/1.02 % (1287901)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.87/1.02 % (1287901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.87/1.02 % (1287901)CaDiCaL version: 2.1.3
% 3.87/1.02 % (1287901)Termination reason: Instruction limit
% 3.87/1.02 % (1287901)Termination phase: Saturation
% 3.87/1.02 % (1287901)Time elapsed: 0.158 s
% 3.87/1.02 % (1287901)Peak memory usage: 14 MB
% 3.87/1.02 % (1287901)Instructions burned: 181 (million)
% 3.87/1.02 % (1287926)lrs+1010_1_anc=none:slsqr=1,2:sil=128000:cnfonf=conj_eager:sas=cadical:si=on:hi=on:uwa=one_side_interpreted:rp=on:nwc=2:slsqc=3:slsq=on:random_seed=4109468995:i=66:s2at=3:nm=2:rtra=on:rawr=on_2995 on theBenchmark for (2995ds/66Mi)
% 3.87/1.02 % (1287927)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=1533733308:i=51:fsr=off:rtra=on_2995 on theBenchmark for (2995ds/51Mi)
% 3.87/1.02 % (1287910)Instruction limit reached!
% 3.87/1.02 % (1287910)------------------------------
% 3.87/1.02 % (1287910)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.87/1.02 % (1287910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.87/1.02 % (1287910)CaDiCaL version: 2.1.3
% 3.87/1.02 % (1287910)Termination reason: Instruction limit
% 3.87/1.02 % (1287910)Termination phase: Saturation
% 3.87/1.02 % (1287910)Time elapsed: 0.139 s
% 3.87/1.02 % (1287910)Peak memory usage: 16 MB
% 3.87/1.02 % (1287910)Instructions burned: 316 (million)
% 3.87/1.02 % (1287927)Instruction limit reached!
% 3.87/1.02 % (1287927)------------------------------
% 3.87/1.02 % (1287927)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.87/1.02 % (1287927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.87/1.02 % (1287927)CaDiCaL version: 2.1.3
% 3.87/1.02 % (1287927)Termination reason: Instruction limit
% 3.87/1.02 % (1287927)Termination phase: Property scanning
% 3.87/1.02 % (1287927)Time elapsed: 0.022 s
% 3.87/1.02 % (1287927)Peak memory usage: 11 MB
% 3.87/1.02 % (1287927)Instructions burned: 52 (million)
% 3.87/1.02 % (1287930)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=1273004197:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/31Mi)
% 3.87/1.02 % (1287922)Instruction limit reached!
% 3.87/1.02 % (1287922)------------------------------
% 3.87/1.02 % (1287922)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.87/1.02 % (1287922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.87/1.02 % (1287922)CaDiCaL version: 2.1.3
% 3.87/1.02 % (1287922)Termination reason: Instruction limit
% 3.87/1.02 % (1287922)Termination phase: Saturation
% 3.87/1.02 % (1287922)Time elapsed: 0.089 s
% 3.87/1.02 % (1287922)Peak memory usage: 13 MB
% 3.87/1.02 % (1287922)Instructions burned: 200 (million)
% 3.87/1.02 % (1287930)Instruction limit reached!
% 3.87/1.02 % (1287930)------------------------------
% 3.87/1.02 % (1287930)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.87/1.02 % (1287930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.87/1.02 % (1287930)CaDiCaL version: 2.1.3
% 3.87/1.02 % (1287930)Termination reason: Instruction limit
% 3.87/1.02 % (1287930)Termination phase: Property scanning
% 3.87/1.02 % (1287930)Time elapsed: 0.013 s
% 3.87/1.02 % (1287930)Peak memory usage: 10 MB
% 3.87/1.02 % (1287930)Instructions burned: 32 (million)
% 3.87/1.02 % (1287889)Instruction limit reached!
% 3.87/1.02 % (1287889)------------------------------
% 3.87/1.02 % (1287889)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.87/1.02 % (1287889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.87/1.02 % (1287889)CaDiCaL version: 2.1.3
% 3.87/1.02 % (1287889)Termination reason: Instruction limit
% 3.87/1.02 % (1287889)Termination phase: Saturation
% 3.87/1.02 % (1287889)Time elapsed: 0.321 s
% 3.87/1.02 % (1287889)Peak memory usage: 18 MB
% 3.87/1.02 % (1287889)Instructions burned: 1240 (million)
% 3.87/1.02 % (1287931)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=2670979989:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2994 on theBenchmark for (2994ds/137Mi)
% 5.45/1.17 % (1287935)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 5.45/1.17 % (1287935)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=14239902:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2994 on theBenchmark for (2994ds/180Mi)
% 5.45/1.17 % (1287926)Instruction limit reached!
% 5.45/1.17 % (1287926)------------------------------
% 5.45/1.17 % (1287926)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.45/1.17 % (1287926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.45/1.17 % (1287926)CaDiCaL version: 2.1.3
% 5.45/1.17 % (1287926)Termination reason: Instruction limit
% 5.45/1.17 % (1287926)Termination phase: Property scanning
% 5.45/1.17 % (1287926)Time elapsed: 0.054 s
% 5.45/1.17 % (1287926)Peak memory usage: 11 MB
% 5.45/1.17 % (1287926)Instructions burned: 66 (million)
% 5.45/1.17 % (1287934)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=530971197:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2994 on theBenchmark for (2994ds/67Mi)
% 5.45/1.17 % (1287933)dis+10_2_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_pi_sigma_gen:si=on:sp=occurrence:plsqr=5,1:bsr=on:plsql=on:random_seed=1999261217:cond=on:i=34:hud=10:nm=10:rtra=on_2994 on theBenchmark for (2994ds/34Mi)
% 5.45/1.17 % (1287933)Instruction limit reached!
% 5.45/1.17 % (1287933)------------------------------
% 5.45/1.17 % (1287933)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.45/1.17 % (1287933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.45/1.17 % (1287933)CaDiCaL version: 2.1.3
% 5.45/1.17 % (1287933)Termination reason: Instruction limit
% 5.45/1.17 % (1287933)Termination phase: Property scanning
% 5.45/1.17 % (1287933)Time elapsed: 0.025 s
% 5.45/1.17 % (1287933)Peak memory usage: 10 MB
% 5.45/1.17 % (1287933)Instructions burned: 34 (million)
% 5.45/1.17 % (1287934)Instruction limit reached!
% 5.45/1.17 % (1287934)------------------------------
% 5.45/1.17 % (1287934)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.45/1.17 % (1287934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.45/1.17 % (1287934)CaDiCaL version: 2.1.3
% 5.45/1.17 % (1287934)Termination reason: Instruction limit
% 5.45/1.17 % (1287934)Termination phase: Saturation
% 5.45/1.17 % (1287934)Time elapsed: 0.028 s
% 5.45/1.17 % (1287934)Peak memory usage: 12 MB
% 5.45/1.17 % (1287934)Instructions burned: 67 (million)
% 5.45/1.17 % (1287938)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=1701231382:st=2:i=246:sd=3:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/246Mi)
% 5.45/1.17 % (1287935)Instruction limit reached!
% 5.45/1.17 % (1287935)------------------------------
% 5.45/1.17 % (1287935)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.45/1.17 % (1287935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.45/1.17 % (1287935)CaDiCaL version: 2.1.3
% 5.45/1.17 % (1287935)Termination reason: Instruction limit
% 5.45/1.17 % (1287935)Termination phase: Saturation
% 5.45/1.17 % (1287935)Time elapsed: 0.043 s
% 5.45/1.17 % (1287935)Peak memory usage: 13 MB
% 5.45/1.17 % (1287935)Instructions burned: 184 (million)
% 5.45/1.17 % (1287931)Instruction limit reached!
% 5.45/1.17 % (1287931)------------------------------
% 5.45/1.17 % (1287931)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.45/1.17 % (1287931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.45/1.17 % (1287931)CaDiCaL version: 2.1.3
% 5.45/1.17 % (1287931)Termination reason: Instruction limit
% 5.45/1.17 % (1287931)Termination phase: Saturation
% 5.45/1.17 % (1287931)Time elapsed: 0.058 s
% 5.45/1.17 % (1287931)Peak memory usage: 13 MB
% 5.45/1.17 % (1287931)Instructions burned: 138 (million)
% 5.45/1.17 % (1287944)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=1453667260:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/874Mi)
% 5.45/1.17 % (1287941)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=815508369:cond=on:i=96:bd=all:rtra=on_2994 on theBenchmark for (2994ds/96Mi)
% 5.45/1.17 % (1287943)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=1874210987:i=427:sd=1:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/427Mi)
% 5.45/1.17 % (1287945)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=3826314380:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/515Mi)
% 6.20/1.28 % (1287941)Instruction limit reached!
% 6.20/1.28 % (1287941)------------------------------
% 6.20/1.28 % (1287941)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.20/1.28 % (1287941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.20/1.28 % (1287941)CaDiCaL version: 2.1.3
% 6.20/1.28 % (1287941)Termination reason: Instruction limit
% 6.20/1.28 % (1287941)Termination phase: Saturation
% 6.20/1.28 % (1287941)Time elapsed: 0.042 s
% 6.20/1.28 % (1287941)Peak memory usage: 13 MB
% 6.20/1.28 % (1287941)Instructions burned: 96 (million)
% 6.20/1.28 % (1287916)Instruction limit reached!
% 6.20/1.28 % (1287916)------------------------------
% 6.20/1.28 % (1287916)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.20/1.28 % (1287916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.20/1.28 % (1287916)CaDiCaL version: 2.1.3
% 6.20/1.28 % (1287916)Termination reason: Instruction limit
% 6.20/1.28 % (1287916)Termination phase: Saturation
% 6.20/1.28 % (1287916)Time elapsed: 0.237 s
% 6.20/1.28 % (1287916)Peak memory usage: 16 MB
% 6.20/1.28 % (1287916)Instructions burned: 482 (million)
% 6.20/1.28 % (1287950)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=1977707236:st=1.5:i=130:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/130Mi)
% 6.20/1.28 % (1287951)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=2106183966:i=44:ep=R:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/44Mi)
% 6.20/1.28 % (1287951)Instruction limit reached!
% 6.20/1.28 % (1287951)------------------------------
% 6.20/1.28 % (1287951)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.20/1.28 % (1287951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.20/1.28 % (1287951)CaDiCaL version: 2.1.3
% 6.20/1.28 % (1287951)Termination reason: Instruction limit
% 6.20/1.28 % (1287951)Termination phase: Function definition elimination
% 6.20/1.28 % (1287951)Time elapsed: 0.018 s
% 6.20/1.28 % (1287951)Peak memory usage: 10 MB
% 6.20/1.28 % (1287951)Instructions burned: 44 (million)
% 6.20/1.28 % (1287938)Instruction limit reached!
% 6.20/1.28 % (1287938)------------------------------
% 6.20/1.28 % (1287938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.20/1.28 % (1287938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.20/1.28 % (1287938)CaDiCaL version: 2.1.3
% 6.20/1.28 % (1287938)Termination reason: Instruction limit
% 6.20/1.28 % (1287938)Termination phase: Saturation
% 6.20/1.28 % (1287938)Time elapsed: 0.117 s
% 6.20/1.28 % (1287938)Peak memory usage: 14 MB
% 6.20/1.28 % (1287938)Instructions burned: 246 (million)
% 6.20/1.28 % (1287954)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=3394232970:s2a=on:i=571:nm=16:rtra=on_2993 on theBenchmark for (2993ds/571Mi)
% 6.20/1.28 % (1287950)Instruction limit reached!
% 6.20/1.28 % (1287950)------------------------------
% 6.20/1.28 % (1287950)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.20/1.28 % (1287950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.20/1.28 % (1287950)CaDiCaL version: 2.1.3
% 6.20/1.28 % (1287950)Termination reason: Instruction limit
% 6.20/1.28 % (1287950)Termination phase: Saturation
% 6.20/1.28 % (1287950)Time elapsed: 0.056 s
% 6.20/1.28 % (1287950)Peak memory usage: 13 MB
% 6.20/1.28 % (1287950)Instructions burned: 130 (million)
% 6.20/1.28 % (1287955)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=1556944587:i=450:rtra=on:ixr=off:ntd=on_2993 on theBenchmark for (2993ds/450Mi)
% 6.20/1.28 % (1287957)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=1475613979:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2992 on theBenchmark for (2992ds/95Mi)
% 6.20/1.28 % (1287957)Instruction limit reached!
% 6.20/1.28 % (1287957)------------------------------
% 6.20/1.28 % (1287957)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.20/1.28 % (1287957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.20/1.28 % (1287957)CaDiCaL version: 2.1.3
% 6.20/1.28 % (1287957)Termination reason: Instruction limit
% 6.20/1.28 % (1287957)Termination phase: Saturation
% 6.20/1.28 % (1287957)Time elapsed: 0.042 s
% 6.48/1.39 % (1287957)Peak memory usage: 13 MB
% 6.48/1.39 % (1287957)Instructions burned: 96 (million)
% 6.48/1.39 % (1287960)lrs+1003_1_sil=128000:drc=off:cnfonf=lazy_pi_sigma_gen:si=on:uwa=one_side_interpreted:fd=off:rp=on:sac=on:random_seed=3844647370:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2992 on theBenchmark for (2992ds/65Mi)
% 6.48/1.39 % (1287944)Instruction limit reached!
% 6.48/1.39 % (1287944)------------------------------
% 6.48/1.39 % (1287944)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.48/1.39 % (1287944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.48/1.39 % (1287944)CaDiCaL version: 2.1.3
% 6.48/1.39 % (1287944)Termination reason: Instruction limit
% 6.48/1.39 % (1287944)Termination phase: Saturation
% 6.48/1.39 % (1287944)Time elapsed: 0.222 s
% 6.48/1.39 % (1287944)Peak memory usage: 15 MB
% 6.48/1.39 % (1287944)Instructions burned: 894 (million)
% 6.48/1.39 % (1287960)Instruction limit reached!
% 6.48/1.39 % (1287960)------------------------------
% 6.48/1.39 % (1287960)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.48/1.39 % (1287960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.48/1.39 % (1287960)CaDiCaL version: 2.1.3
% 6.48/1.39 % (1287960)Termination reason: Instruction limit
% 6.48/1.39 % (1287960)Termination phase: Property scanning
% 6.48/1.39 % (1287960)Time elapsed: 0.027 s
% 6.48/1.39 % (1287960)Peak memory usage: 11 MB
% 6.48/1.39 % (1287960)Instructions burned: 66 (million)
% 6.48/1.39 % (1287962)dis+1010_2:1_slsqr=2,1:to=lpo:plsq=on:cnfonf=lazy_pi_sigma_gen:si=on:sp=reverse_arity:acc=on:uwa=hol:fd=preordered:s2agt=16:flr=on:pe=on:slsq=on:random_seed=3246652022:uwa_fpi=on:avsq=on:s2a=on:cond=fast:i=105:s2at=1.5:aac=none:fgj=on:piset=and:hud=3:fsr=off:rtra=on:er=filter:rawr=on_2991 on theBenchmark for (2991ds/105Mi)
% 6.48/1.39 % (1287963)dis+10_4:1_sfv=off:to=kbo:fde=unused:cnfonf=off:sas=cadical:e2e=on:si=on:sp=occurrence:acc=on:uwa=off:fd=preordered:foolp=on:random_seed=1483381609:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2991 on theBenchmark for (2991ds/5755Mi)
% 6.48/1.39 % (1287945)Instruction limit reached!
% 6.48/1.39 % (1287945)------------------------------
% 6.48/1.39 % (1287945)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.48/1.39 % (1287945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.48/1.39 % (1287945)CaDiCaL version: 2.1.3
% 6.48/1.39 % (1287945)Termination reason: Instruction limit
% 6.48/1.39 % (1287945)Termination phase: Saturation
% 6.48/1.39 % (1287945)Time elapsed: 0.233 s
% 6.48/1.39 % (1287945)Peak memory usage: 14 MB
% 6.48/1.39 % (1287945)Instructions burned: 515 (million)
% 6.48/1.39 % (1287966)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=4248448062:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/375Mi)
% 6.48/1.39 % (1287962)Instruction limit reached!
% 6.48/1.39 % (1287962)------------------------------
% 6.48/1.39 % (1287962)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.48/1.39 % (1287962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.48/1.39 % (1287962)CaDiCaL version: 2.1.3
% 6.48/1.39 % (1287962)Termination reason: Instruction limit
% 6.48/1.39 % (1287962)Termination phase: Saturation
% 6.48/1.39 % (1287962)Time elapsed: 0.044 s
% 6.48/1.39 % (1287962)Peak memory usage: 12 MB
% 6.48/1.39 % (1287962)Instructions burned: 106 (million)
% 6.48/1.39 % (1287914)Instruction limit reached!
% 6.48/1.39 % (1287914)------------------------------
% 6.48/1.39 % (1287914)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.48/1.39 % (1287914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.48/1.39 % (1287914)CaDiCaL version: 2.1.3
% 6.48/1.39 % (1287914)Termination reason: Instruction limit
% 6.48/1.39 % (1287914)Termination phase: Saturation
% 6.48/1.39 % (1287914)Time elapsed: 0.492 s
% 6.48/1.39 % (1287914)Peak memory usage: 20 MB
% 6.48/1.39 % (1287914)Instructions burned: 855 (million)
% 6.48/1.39 % (1287968)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=687743359:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2991 on theBenchmark for (2991ds/495Mi)
% 6.48/1.39 % (1287969)dis+10_2_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_pi_sigma_gen:si=on:sp=occurrence:plsqr=5,1:bsr=on:plsql=on:random_seed=572129473:cond=on:i=34:hud=10:nm=10:rtra=on_2990 on theBenchmark for (2990ds/34Mi)
% 7.16/1.48 % (1287969)Instruction limit reached!
% 7.16/1.48 % (1287969)------------------------------
% 7.16/1.48 % (1287969)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.16/1.48 % (1287969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.16/1.48 % (1287969)CaDiCaL version: 2.1.3
% 7.16/1.48 % (1287969)Termination reason: Instruction limit
% 7.16/1.48 % (1287969)Termination phase: Property scanning
% 7.16/1.48 % (1287969)Time elapsed: 0.014 s
% 7.16/1.48 % (1287969)Peak memory usage: 10 MB
% 7.16/1.48 % (1287969)Instructions burned: 34 (million)
% 7.16/1.48 % (1287972)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=3819709370:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2990 on theBenchmark for (2990ds/91Mi)
% 7.16/1.48 % (1287943)Instruction limit reached!
% 7.16/1.48 % (1287943)------------------------------
% 7.16/1.48 % (1287943)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.16/1.48 % (1287943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.16/1.48 % (1287943)CaDiCaL version: 2.1.3
% 7.16/1.48 % (1287943)Termination reason: Instruction limit
% 7.16/1.48 % (1287943)Termination phase: Saturation
% 7.16/1.48 % (1287943)Time elapsed: 0.364 s
% 7.16/1.48 % (1287943)Peak memory usage: 15 MB
% 7.16/1.48 % (1287943)Instructions burned: 428 (million)
% 7.16/1.48 % (1287954)Instruction limit reached!
% 7.16/1.48 % (1287954)------------------------------
% 7.16/1.48 % (1287954)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.16/1.48 % (1287954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.16/1.48 % (1287954)CaDiCaL version: 2.1.3
% 7.16/1.48 % (1287954)Termination reason: Instruction limit
% 7.16/1.48 % (1287954)Termination phase: Saturation
% 7.16/1.48 % (1287954)Time elapsed: 0.275 s
% 7.16/1.48 % (1287954)Peak memory usage: 17 MB
% 7.16/1.48 % (1287954)Instructions burned: 572 (million)
% 7.16/1.48 % (1287972)Instruction limit reached!
% 7.16/1.48 % (1287972)------------------------------
% 7.16/1.48 % (1287972)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.16/1.48 % (1287972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.16/1.48 % (1287972)CaDiCaL version: 2.1.3
% 7.16/1.48 % (1287972)Termination reason: Instruction limit
% 7.16/1.48 % (1287972)Termination phase: Saturation
% 7.16/1.48 % (1287972)Time elapsed: 0.040 s
% 7.16/1.48 % (1287972)Peak memory usage: 13 MB
% 7.16/1.48 % (1287972)Instructions burned: 92 (million)
% 7.16/1.48 % (1287974)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=408462075:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2990 on theBenchmark for (2990ds/66Mi)
% 7.16/1.48 % (1287975)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=2303173394:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2990 on theBenchmark for (2990ds/22Mi)
% 7.16/1.48 % (1287955)Instruction limit reached!
% 7.16/1.48 % (1287955)------------------------------
% 7.16/1.48 % (1287955)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.16/1.48 % (1287955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.16/1.48 % (1287955)CaDiCaL version: 2.1.3
% 7.16/1.48 % (1287955)Termination reason: Instruction limit
% 7.16/1.48 % (1287955)Termination phase: Saturation
% 7.16/1.48 % (1287955)Time elapsed: 0.290 s
% 7.16/1.48 % (1287955)Peak memory usage: 19 MB
% 7.16/1.48 % (1287955)Instructions burned: 450 (million)
% 7.16/1.48 % (1287975)Instruction limit reached!
% 7.16/1.48 % (1287975)------------------------------
% 7.16/1.48 % (1287975)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.16/1.48 % (1287975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.16/1.48 % (1287975)CaDiCaL version: 2.1.3
% 7.16/1.48 % (1287975)Termination reason: Instruction limit
% 7.16/1.48 % (1287975)Termination phase: Property scanning
% 7.16/1.48 % (1287975)Time elapsed: 0.010 s
% 7.16/1.48 % (1287975)Peak memory usage: 10 MB
% 7.16/1.48 % (1287975)Instructions burned: 23 (million)
% 7.16/1.48 % (1287976)lrs+21_16_anc=none:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:sas=cadical:si=on:plsqr=32,1:uwa=interpreted_only:foolp=on:nwc=3:random_seed=4122407196:i=338:bd=all:ins=4:rtra=on_2990 on theBenchmark for (2990ds/338Mi)
% 7.16/1.48 % (1287980)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 7.16/1.48 % (1287980)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=485058837:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2989 on theBenchmark for (2989ds/137Mi)
% 8.00/1.65 % (1287974)Instruction limit reached!
% 8.00/1.65 % (1287974)------------------------------
% 8.00/1.65 % (1287974)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.00/1.65 % (1287974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.00/1.65 % (1287974)CaDiCaL version: 2.1.3
% 8.00/1.65 % (1287974)Termination reason: Instruction limit
% 8.00/1.65 % (1287974)Termination phase: Twee Goal Transformation
% 8.00/1.65 % (1287974)Time elapsed: 0.036 s
% 8.00/1.65 % (1287974)Peak memory usage: 13 MB
% 8.00/1.65 % (1287974)Instructions burned: 68 (million)
% 8.00/1.65 % (1287979)lrs+10_1_sil=128000:si=on:urr=on:random_seed=376940339:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2989 on theBenchmark for (2989ds/28Mi)
% 8.00/1.65 % (1287966)Instruction limit reached!
% 8.00/1.65 % (1287966)------------------------------
% 8.00/1.65 % (1287966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.00/1.65 % (1287966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.00/1.65 % (1287966)CaDiCaL version: 2.1.3
% 8.00/1.65 % (1287966)Termination reason: Instruction limit
% 8.00/1.65 % (1287966)Termination phase: Saturation
% 8.00/1.65 % (1287966)Time elapsed: 0.187 s
% 8.00/1.65 % (1287966)Peak memory usage: 15 MB
% 8.00/1.65 % (1287966)Instructions burned: 376 (million)
% 8.00/1.65 % (1287983)dis+10_32_sil=128000:tgt=ground:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=32,1:uwa=one_side_interpreted:nwc=1:random_seed=2403408568:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2989 on theBenchmark for (2989ds/340Mi)
% 8.00/1.65 % (1287968)Instruction limit reached!
% 8.00/1.65 % (1287968)------------------------------
% 8.00/1.65 % (1287968)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.00/1.65 % (1287968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.00/1.65 % (1287968)CaDiCaL version: 2.1.3
% 8.00/1.65 % (1287968)Termination reason: Instruction limit
% 8.00/1.65 % (1287968)Termination phase: Saturation
% 8.00/1.65 % (1287968)Time elapsed: 0.160 s
% 8.00/1.65 % (1287968)Peak memory usage: 17 MB
% 8.00/1.65 % (1287968)Instructions burned: 498 (million)
% 8.00/1.65 % (1287979)Instruction limit reached!
% 8.00/1.65 % (1287979)------------------------------
% 8.00/1.65 % (1287979)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.00/1.65 % (1287979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.00/1.65 % (1287979)CaDiCaL version: 2.1.3
% 8.00/1.65 % (1287979)Termination reason: Instruction limit
% 8.00/1.65 % (1287979)Termination phase: SInE selection
% 8.00/1.65 % (1287979)Time elapsed: 0.023 s
% 8.00/1.65 % (1287979)Peak memory usage: 10 MB
% 8.00/1.65 % (1287979)Instructions burned: 28 (million)
% 8.00/1.65 % (1287987)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 8.00/1.65 % (1287986)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=2303147758:i=227:sd=1:bd=all:rtra=on:ss=axioms_2989 on theBenchmark for (2989ds/227Mi)
% 8.00/1.65 % (1287987)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=2790424821:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2989 on theBenchmark for (2989ds/373Mi)
% 8.00/1.65 % (1287980)Instruction limit reached!
% 8.00/1.65 % (1287980)------------------------------
% 8.00/1.65 % (1287980)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.00/1.65 % (1287980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.00/1.65 % (1287980)CaDiCaL version: 2.1.3
% 8.00/1.65 % (1287980)Termination reason: Instruction limit
% 8.00/1.65 % (1287980)Termination phase: Saturation
% 8.00/1.65 % (1287980)Time elapsed: 0.057 s
% 8.00/1.65 % (1287980)Peak memory usage: 13 MB
% 8.00/1.65 % (1287980)Instructions burned: 137 (million)
% 8.00/1.65 % (1287988)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=416873649:i=116:ep=RSTC:rtra=on:ntd=on_2989 on theBenchmark for (2989ds/116Mi)
% 8.00/1.65 % (1287991)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=2087836599:i=575:rtra=on_2989 on theBenchmark for (2989ds/575Mi)
% 8.00/1.65 % (1287976)Instruction limit reached!
% 8.00/1.65 % (1287976)------------------------------
% 8.00/1.65 % (1287976)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.00/1.65 % (1287976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.00/1.65 % (1287976)CaDiCaL version: 2.1.3
% 8.00/1.65 % (1287976)Termination reason: Instruction limit
% 8.00/1.65 % (1287976)Termination phase: Saturation
% 8.00/1.65 % (1287976)Time elapsed: 0.134 s
% 8.00/1.65 % (1287976)Peak memory usage: 15 MB
% 8.00/1.65 % (1287976)Instructions burned: 339 (million)
% 8.00/1.65 % (1287987)Instruction limit reached!
% 8.00/1.65 % (1287987)------------------------------
% 8.00/1.65 % (1287987)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.00/1.65 % (1287987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.00/1.65 % (1287987)CaDiCaL version: 2.1.3
% 8.00/1.65 % (1287987)Termination reason: Instruction limit
% 8.00/1.65 % (1287987)Termination phase: Saturation
% 8.00/1.65 % (1287987)Time elapsed: 0.089 s
% 8.00/1.65 % (1287987)Peak memory usage: 12 MB
% 8.00/1.65 % (1287987)Instructions burned: 376 (million)
% 8.00/1.65 % (1287994)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=980785139:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2988 on theBenchmark for (2988ds/270Mi)
% 8.00/1.65 % (1287995)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=2057769421:hsq=on:hsqr=16,1:s2a=on:i=9840:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2988 on theBenchmark for (2988ds/9840Mi)
% 8.00/1.65 % (1287986)Instruction limit reached!
% 8.00/1.65 % (1287986)------------------------------
% 8.00/1.65 % (1287986)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.00/1.65 % (1287986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.00/1.65 % (1287986)CaDiCaL version: 2.1.3
% 8.00/1.65 % (1287986)Termination reason: Instruction limit
% 8.00/1.65 % (1287986)Termination phase: Saturation
% 8.00/1.65 % (1287986)Time elapsed: 0.112 s
% 8.00/1.65 % (1287986)Peak memory usage: 14 MB
% 8.00/1.65 % (1287986)Instructions burned: 229 (million)
% 8.00/1.65 % (1287988)Instruction limit reached!
% 8.00/1.65 % (1287988)------------------------------
% 8.00/1.65 % (1287988)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.00/1.65 % (1287988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.00/1.65 % (1287988)CaDiCaL version: 2.1.3
% 8.00/1.65 % (1287988)Termination reason: Instruction limit
% 8.00/1.65 % (1287988)Termination phase: Saturation
% 8.00/1.65 % (1287988)Time elapsed: 0.098 s
% 8.00/1.65 % (1287988)Peak memory usage: 14 MB
% 8.00/1.65 % (1287988)Instructions burned: 116 (million)
% 8.00/1.65 % (1287983)Instruction limit reached!
% 8.00/1.65 % (1287983)------------------------------
% 8.00/1.65 % (1287983)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.00/1.65 % (1287983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.00/1.65 % (1287983)CaDiCaL version: 2.1.3
% 8.00/1.65 % (1287983)Termination reason: Instruction limit
% 8.00/1.65 % (1287983)Termination phase: Saturation
% 8.00/1.65 % (1287983)Time elapsed: 0.146 s
% 8.00/1.65 % (1287983)Peak memory usage: 13 MB
% 8.00/1.65 % (1287983)Instructions burned: 342 (million)
% 8.00/1.65 % (1287998)lrs+1010_1_sil=128000:si=on:sos=all:uwa=off:nwc=1:random_seed=84567948:i=421:rtra=on:ss=axioms_2988 on theBenchmark for (2988ds/421Mi)
% 8.00/1.65 % (1288000)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=2708265987:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2987 on theBenchmark for (2987ds/31Mi)
% 8.00/1.65 % (1287999)WARNING Broken Constraint: if sine_to_age_tolerance(3) 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
% 8.00/1.65 % (1287999)lrs+10_40_sil=128000:tgt=full:cnfonf=off:si=on:sp=reverse_frequency:spb=goal_then_units:uwa=off:fd=preordered:nwc=1:random_seed=1089748531:avsq=on:i=270:s2at=3:avsqr=1,16:rtra=on:ntd=on_2988 on theBenchmark for (2988ds/270Mi)
% 8.00/1.65 % (1288000)Instruction limit reached!
% 8.00/1.65 % (1288000)------------------------------
% 8.00/1.65 % (1288000)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.00/1.65 % (1288000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.00/1.65 % (1288000)CaDiCaL version: 2.1.3
% 8.00/1.65 % (1288000)Termination reason: Instruction limit
% 8.00/1.65 % (1288000)Termination phase: Property scanning
% 8.00/1.65 % (1288000)Time elapsed: 0.013 s
% 8.00/1.65 % (1288000)Peak memory usage: 10 MB
% 8.00/1.65 % (1288000)Instructions burned: 32 (million)
% 8.00/1.65 % (1288004)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 8.00/1.65 % (1288004)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
% 8.00/1.65 % (1288004)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=1247705890:hsqr=1,8:i=1440:s2at=5:add=on:nm=2:rtra=on_2987 on theBenchmark for (2987ds/1440Mi)
% 8.00/1.65 % (1287994)Instruction limit reached!
% 8.00/1.65 % (1287994)------------------------------
% 8.00/1.65 % (1287994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.00/1.65 % (1287994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.00/1.65 % (1287994)CaDiCaL version: 2.1.3
% 8.00/1.65 % (1287994)Termination reason: Instruction limit
% 8.00/1.65 % (1287994)Termination phase: Saturation
% 8.00/1.65 % (1287994)Time elapsed: 0.117 s
% 8.00/1.65 % (1287994)Peak memory usage: 14 MB
% 8.00/1.65 % (1287994)Instructions burned: 270 (million)
% 8.00/1.65 % (1288006)dis+10_2_sil=128000:si=on:random_seed=3849837778:s2a=on:i=339:av=off:rtra=on:fe=abstraction:ss=axioms:fsd=on:ntd=on_2987 on theBenchmark for (2987ds/339Mi)
% 8.00/1.65 % (1287999)Refutation not found, incomplete strategy
% 8.00/1.65 % (1287999)------------------------------
% 8.00/1.65 % (1287999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.00/1.65 % (1287999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.00/1.65 % (1287999)CaDiCaL version: 2.1.3
% 8.00/1.65 % (1287999)Termination reason: Refutation not found, incomplete strategy
% 8.00/1.65 % (1287999)Time elapsed: 0.096 s
% 8.00/1.65 % (1287999)Peak memory usage: 13 MB
% 8.00/1.65 % (1287999)Instructions burned: 117 (million)
% 8.00/1.65 % (1287999)------------------------------
% 8.00/1.65 % (1287999)------------------------------
% 8.00/1.65 % (1287991)Instruction limit reached!
% 8.00/1.65 % (1287991)------------------------------
% 8.00/1.65 % (1287991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.00/1.65 % (1287991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.00/1.65 % (1287991)CaDiCaL version: 2.1.3
% 8.00/1.65 % (1287991)Termination reason: Instruction limit
% 8.00/1.65 % (1287991)Termination phase: Saturation
% 8.00/1.65 % (1287991)Time elapsed: 0.253 s
% 8.00/1.65 % (1287991)Peak memory usage: 15 MB
% 8.00/1.65 % (1287991)Instructions burned: 576 (million)
% 8.00/1.65 % (1288008)lrs+2_16:1_si=on:cbe=off:uwa=interpreted_only:random_seed=3665230235:i=111:add=on:fgj=on:rtra=on:fdi=1024_2986 on theBenchmark for (2986ds/111Mi)
% 8.00/1.65 % (1288009)dis+10_8_sil=128000:plsq=on:plsqc=1:si=on:sp=unary_first:sos=on:lma=off:plsqr=64,1:uwa=interpreted_only:foolp=on:random_seed=4114229329:st=3:avsq=on:i=122:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2986 on theBenchmark for (2986ds/122Mi)
% 8.00/1.65 % (1287995) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1287825-1287995"...
% 8.00/1.65 % (1287995)...printing done.
% 8.00/1.65 % (1287995)Refutation found. Thanks to Tanya!
% 8.00/1.65 % SZS status Theorem for theBenchmark
% 8.00/1.65 % SZS output start Proof for theBenchmark
% 8.00/1.65 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 8.00/1.65 thf(func_def_0, type, in: ($i > $i > $o)).
% 8.00/1.65 thf(func_def_1, type, exu: (($i > $o) > $o)).
% 8.00/1.65 thf(func_def_3, type, setextAx: $o).
% 8.00/1.65 thf(func_def_5, type, emptysetAx: $o).
% 8.00/1.65 thf(func_def_6, type, setadjoin: ($i > $i > $i)).
% 8.00/1.65 thf(func_def_7, type, setadjoinAx: $o).
% 8.00/1.65 thf(func_def_8, type, powerset: ($i > $i)).
% 8.00/1.65 thf(func_def_9, type, powersetAx: $o).
% 8.00/1.65 thf(func_def_10, type, setunion: ($i > $i)).
% 8.00/1.65 thf(func_def_11, type, setunionAx: $o).
% 8.00/1.65 thf(func_def_13, type, omega0Ax: $o).
% 8.00/1.65 thf(func_def_14, type, omegaSAx: $o).
% 8.00/1.65 thf(func_def_15, type, omegaIndAx: $o).
% 8.00/1.65 thf(func_def_16, type, replAx: $o).
% 8.00/1.65 thf(func_def_17, type, foundationAx: $o).
% 8.00/1.65 thf(func_def_18, type, wellorderingAx: $o).
% 8.00/1.65 thf(func_def_19, type, descr: (($i > $o) > $i)).
% 8.00/1.65 thf(func_def_20, type, descrp: $o).
% 8.00/1.65 thf(func_def_21, type, dsetconstr: ($i > ($i > $o) > $i)).
% 8.00/1.65 thf(func_def_22, type, dsetconstrI: $o).
% 8.00/1.65 thf(func_def_23, type, dsetconstrEL: $o).
% 8.00/1.65 thf(func_def_24, type, dsetconstrER: $o).
% 8.00/1.65 thf(func_def_25, type, exuE1: $o).
% 8.00/1.65 thf(func_def_26, type, prop2set: ($o > $i)).
% 8.00/1.65 thf(func_def_27, type, prop2setE: $o).
% 8.00/1.65 thf(func_def_28, type, emptysetE: $o).
% 8.00/1.65 thf(func_def_29, type, emptysetimpfalse: $o).
% 8.00/1.65 thf(func_def_30, type, notinemptyset: $o).
% 8.00/1.65 thf(func_def_31, type, exuE3e: $o).
% 8.00/1.65 thf(func_def_32, type, setext: $o).
% 8.00/1.65 thf(func_def_33, type, emptyI: $o).
% 8.00/1.65 thf(func_def_34, type, noeltsimpempty: $o).
% 8.00/1.65 thf(func_def_35, type, setbeta: $o).
% 8.00/1.65 thf(func_def_36, type, nonempty: ($i > $o)).
% 8.00/1.65 thf(func_def_37, type, nonemptyE1: $o).
% 8.00/1.65 thf(func_def_38, type, nonemptyI: $o).
% 8.00/1.65 thf(func_def_39, type, nonemptyI1: $o).
% 8.00/1.65 thf(func_def_40, type, setadjoinIL: $o).
% 8.00/1.65 thf(func_def_41, type, emptyinunitempty: $o).
% 8.00/1.65 thf(func_def_42, type, setadjoinIR: $o).
% 8.00/1.65 thf(func_def_43, type, setadjoinE: $o).
% 8.00/1.65 thf(func_def_44, type, setadjoinOr: $o).
% 8.00/1.65 thf(func_def_45, type, setoftrueEq: $o).
% 8.00/1.65 thf(func_def_46, type, powersetI: $o).
% 8.00/1.65 thf(func_def_47, type, emptyinPowerset: $o).
% 8.00/1.65 thf(func_def_48, type, emptyInPowerset: $o).
% 8.00/1.65 thf(func_def_49, type, powersetE: $o).
% 8.00/1.65 thf(func_def_50, type, setunionI: $o).
% 8.00/1.65 thf(func_def_51, type, setunionE: $o).
% 8.00/1.65 thf(func_def_52, type, subPowSU: $o).
% 8.00/1.65 thf(func_def_53, type, exuE2: $o).
% 8.00/1.65 thf(func_def_54, type, nonemptyImpWitness: $o).
% 8.00/1.65 thf(func_def_55, type, uniqinunit: $o).
% 8.00/1.65 thf(func_def_56, type, notinsingleton: $o).
% 8.00/1.65 thf(func_def_57, type, eqinunit: $o).
% 8.00/1.65 thf(func_def_58, type, singletonsswitch: $o).
% 8.00/1.65 thf(func_def_59, type, upairsetE: $o).
% 8.00/1.65 thf(func_def_60, type, upairsetIL: $o).
% 8.00/1.65 thf(func_def_61, type, upairsetIR: $o).
% 8.00/1.65 thf(func_def_62, type, emptyE1: $o).
% 8.00/1.65 thf(func_def_63, type, vacuousDall: $o).
% 8.00/1.65 thf(func_def_64, type, quantDeMorgan1: $o).
% 8.00/1.65 thf(func_def_65, type, quantDeMorgan2: $o).
% 8.00/1.65 thf(func_def_66, type, quantDeMorgan3: $o).
% 8.00/1.65 thf(func_def_67, type, quantDeMorgan4: $o).
% 8.00/1.65 thf(func_def_68, type, prop2setI: $o).
% 8.00/1.65 thf(func_def_69, type, set2prop: ($i > $o)).
% 8.00/1.65 thf(func_def_70, type, prop2set2propI: $o).
% 8.00/1.65 thf(func_def_71, type, notdexE: $o).
% 8.00/1.65 thf(func_def_72, type, notdallE: $o).
% 8.00/1.65 thf(func_def_73, type, exuI1: $o).
% 8.00/1.65 thf(func_def_74, type, exuI3: $o).
% 8.00/1.65 thf(func_def_75, type, exuI2: $o).
% 8.00/1.65 thf(func_def_76, type, inCongP: $o).
% 8.00/1.65 thf(func_def_77, type, in__Cong: $o).
% 8.00/1.65 thf(func_def_78, type, exuE3u: $o).
% 8.00/1.65 thf(func_def_79, type, exu__Cong: $o).
% 8.00/1.65 thf(func_def_80, type, emptyset__Cong: $o).
% 8.00/1.65 thf(func_def_81, type, setadjoin__Cong: $o).
% 8.00/1.65 thf(func_def_82, type, powerset__Cong: $o).
% 8.00/1.65 thf(func_def_83, type, setunion__Cong: $o).
% 8.00/1.65 thf(func_def_84, type, omega__Cong: $o).
% 8.00/1.65 thf(func_def_85, type, exuEu: $o).
% 8.00/1.65 thf(func_def_86, type, descr__Cong: $o).
% 8.00/1.65 thf(func_def_87, type, dsetconstr__Cong: $o).
% 8.00/1.65 thf(func_def_88, type, subset: ($i > $i > $o)).
% 8.00/1.65 thf(func_def_89, type, disjoint: ($i > $i > $o)).
% 8.00/1.65 thf(func_def_90, type, setsmeet: ($i > $i > $o)).
% 8.00/1.65 thf(func_def_91, type, subsetI1: $o).
% 8.00/1.65 thf(func_def_92, type, eqimpsubset2: $o).
% 8.00/1.65 thf(func_def_93, type, eqimpsubset1: $o).
% 8.00/1.65 thf(func_def_94, type, subsetI2: $o).
% 8.00/1.65 thf(func_def_95, type, emptysetsubset: $o).
% 8.00/1.65 thf(func_def_96, type, subsetE: $o).
% 8.00/1.65 thf(func_def_97, type, subsetE2: $o).
% 8.00/1.65 thf(func_def_98, type, notsubsetI: $o).
% 8.00/1.65 thf(func_def_99, type, notequalI1: $o).
% 8.00/1.65 thf(func_def_100, type, notequalI2: $o).
% 8.00/1.65 thf(func_def_101, type, subsetRefl: $o).
% 8.00/1.65 thf(func_def_102, type, subsetTrans: $o).
% 8.00/1.65 thf(func_def_103, type, setadjoinSub: $o).
% 8.00/1.65 thf(func_def_104, type, setadjoinSub2: $o).
% 8.00/1.65 thf(func_def_105, type, subset2powerset: $o).
% 8.00/1.65 thf(func_def_106, type, setextsub: $o).
% 8.00/1.65 thf(func_def_107, type, subsetemptysetimpeq: $o).
% 8.00/1.65 thf(func_def_108, type, powersetI1: $o).
% 8.00/1.65 thf(func_def_109, type, powersetE1: $o).
% 8.00/1.65 thf(func_def_110, type, inPowerset: $o).
% 8.00/1.65 thf(func_def_111, type, powersetsubset: $o).
% 8.00/1.65 thf(func_def_112, type, sepInPowerset: $o).
% 8.00/1.65 thf(func_def_113, type, sepSubset: $o).
% 8.00/1.65 thf(func_def_114, type, binunion: ($i > $i > $i)).
% 8.00/1.65 thf(func_def_115, type, binunionIL: $o).
% 8.00/1.65 thf(func_def_116, type, upairset2IR: $o).
% 8.00/1.65 thf(func_def_117, type, binunionIR: $o).
% 8.00/1.65 thf(func_def_118, type, binunionEcases: $o).
% 8.00/1.65 thf(func_def_119, type, binunionE: $o).
% 8.00/1.65 thf(func_def_120, type, binunionLsub: $o).
% 8.00/1.65 thf(func_def_121, type, binunionRsub: $o).
% 8.00/1.65 thf(func_def_122, type, binintersect: ($i > $i > $i)).
% 8.00/1.65 thf(func_def_123, type, binintersectI: $o).
% 8.00/1.65 thf(func_def_124, type, binintersectSubset5: $o).
% 8.00/1.65 thf(func_def_125, type, binintersectEL: $o).
% 8.00/1.65 thf(func_def_126, type, binintersectLsub: $o).
% 8.00/1.65 thf(func_def_127, type, binintersectSubset2: $o).
% 8.00/1.65 thf(func_def_128, type, binintersectSubset3: $o).
% 8.00/1.65 thf(func_def_129, type, binintersectER: $o).
% 8.00/1.65 thf(func_def_130, type, disjointsetsI1: $o).
% 8.00/1.65 thf(func_def_131, type, binintersectRsub: $o).
% 8.00/1.65 thf(func_def_132, type, binintersectSubset4: $o).
% 8.00/1.65 thf(func_def_133, type, binintersectSubset1: $o).
% 8.00/1.65 thf(func_def_134, type, bs114d: $o).
% 8.00/1.65 thf(func_def_135, type, regular: ($i > $o)).
% 8.00/1.65 thf(func_def_136, type, setminus: ($i > $i > $i)).
% 8.00/1.65 thf(func_def_137, type, setminusI: $o).
% 8.00/1.65 thf(func_def_138, type, setminusEL: $o).
% 8.00/1.65 thf(func_def_139, type, setminusER: $o).
% 8.00/1.65 thf(func_def_140, type, setminusSubset2: $o).
% 8.00/1.65 thf(func_def_141, type, setminusERneg: $o).
% 8.00/1.65 thf(func_def_142, type, setminusELneg: $o).
% 8.00/1.65 thf(func_def_143, type, setminusILneg: $o).
% 8.00/1.65 thf(func_def_144, type, setminusIRneg: $o).
% 8.00/1.65 thf(func_def_145, type, setminusLsub: $o).
% 8.00/1.65 thf(func_def_146, type, setminusSubset1: $o).
% 8.00/1.65 thf(func_def_147, type, symdiff: ($i > $i > $i)).
% 8.00/1.65 thf(func_def_148, type, symdiffE: $o).
% 8.00/1.65 thf(func_def_149, type, symdiffI1: $o).
% 8.00/1.65 thf(func_def_150, type, symdiffI2: $o).
% 8.00/1.65 thf(func_def_151, type, symdiffIneg1: $o).
% 8.00/1.65 thf(func_def_152, type, symdiffIneg2: $o).
% 8.00/1.65 thf(func_def_153, type, iskpair: ($i > $o)).
% 8.00/1.65 thf(func_def_154, type, secondinupair: $o).
% 8.00/1.65 thf(func_def_155, type, setukpairIL: $o).
% 8.00/1.65 thf(func_def_156, type, setukpairIR: $o).
% 8.00/1.65 thf(func_def_157, type, kpairiskpair: $o).
% 8.00/1.65 thf(func_def_158, type, kpair: ($i > $i > $i)).
% 8.00/1.65 thf(func_def_159, type, kpairp: $o).
% 8.00/1.65 thf(func_def_160, type, cartprod: ($i > $i > $i)).
% 8.00/1.65 thf(func_def_163, type, db0: !>[X0: $tType]:(X0)).
% 8.00/1.65 thf(func_def_164, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 8.00/1.65 thf(func_def_165, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 8.00/1.65 thf(func_def_166, type, vAND: ($o > $o > $o)).
% 8.00/1.65 thf(func_def_167, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 8.00/1.65 thf(func_def_168, type, vIMP: ($o > $o > $o)).
% 8.00/1.65 thf(func_def_169, type, db2: !>[X0: $tType]:(X0)).
% 8.00/1.65 thf(func_def_170, type, db1: !>[X0: $tType]:(X0)).
% 8.00/1.65 thf(func_def_171, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 8.00/1.65 thf(func_def_172, type, vNOT: ($o > $o)).
% 8.00/1.65 thf(func_def_173, type, db3: !>[X0: $tType]:(X0)).
% 8.00/1.65 thf(func_def_174, type, sP0: ($i > $i > $o)).
% 8.00/1.65 thf(func_def_175, type, sP1: ($i > $o)).
% 8.00/1.65 thf(func_def_176, type, sP2: $o).
% 8.00/1.65 thf(func_def_189, type, sK15: ($i > $o)).
% 8.00/1.65 thf(func_def_191, type, sK17: (($i > $o) > $i > $i)).
% 8.00/1.65 thf(func_def_192, type, sK18: ($i > $i > $i)).
% 8.00/1.65 thf(func_def_209, type, sK35: ($i > $o)).
% 8.00/1.65 thf(func_def_219, type, sK45: ($i > $o)).
% 8.00/1.65 thf(func_def_224, type, sK50: ($i > $i)).
% 8.00/1.65 thf(func_def_225, type, sK51: ($i > $i)).
% 8.00/1.65 thf(func_def_226, type, sK52: ($i > $o)).
% 8.00/1.65 thf(func_def_229, type, sK55: ($i > $i)).
% 8.00/1.65 thf(func_def_234, type, sK60: ($i > $i)).
% 8.00/1.65 thf(func_def_236, type, sK62: ($i > $i > $i)).
% 8.00/1.65 thf(func_def_243, type, sK69: $o).
% 8.00/1.65 thf(func_def_249, type, sK75: ($i > $i > $i)).
% 8.00/1.65 thf(func_def_254, type, sK80: ($i > $o)).
% 8.00/1.65 thf(func_def_256, type, sK82: ($i > ($i > $o) > $i)).
% 8.00/1.65 thf(func_def_258, type, sK84: $o).
% 8.00/1.65 thf(func_def_262, type, sK88: ($i > $o)).
% 8.00/1.65 thf(func_def_264, type, sK90: ($i > $i > $i)).
% 8.00/1.65 thf(func_def_269, type, sK95: ($i > $o)).
% 8.00/1.65 thf(func_def_271, type, sK97: (($i > $o) > $i)).
% 8.00/1.65 thf(func_def_272, type, sK98: (($i > $o) > $i)).
% 8.00/1.65 thf(func_def_282, type, sK108: ($i > $o)).
% 8.00/1.65 thf(func_def_283, type, sK109: ($i > $o)).
% 8.00/1.65 thf(func_def_284, type, sK110: (($i > $o) > ($i > $o) > $i)).
% 8.00/1.65 thf(func_def_285, type, sK111: (($i > $o) > ($i > $o) > $i)).
% 8.00/1.65 thf(func_def_304, type, sK130: ($i > $i > $i)).
% 8.00/1.65 thf(func_def_310, type, sK136: $o).
% 8.00/1.65 thf(func_def_314, type, sK140: ($i > $o)).
% 8.00/1.65 thf(func_def_327, type, sK153: ($i > ($i > $o) > $i)).
% 8.00/1.65 thf(func_def_328, type, sK154: ($i > $o)).
% 8.00/1.65 thf(func_def_336, type, sK162: $o).
% 8.00/1.65 thf(func_def_338, type, sK164: ($i > $o)).
% 8.00/1.65 thf(func_def_343, type, sK169: ($i > $o)).
% 8.00/1.65 thf(func_def_344, type, sK170: ($i > $i)).
% 8.00/1.65 thf(func_def_345, type, sK171: (($i > $o) > $i)).
% 8.00/1.65 thf(func_def_349, type, sK175: $o).
% 8.00/1.65 thf(func_def_352, type, sK178: ($i > $i)).
% 8.00/1.65 thf(func_def_353, type, sK179: ($i > $i)).
% 8.00/1.65 thf(func_def_354, type, sK180: ($i > $i)).
% 8.00/1.65 thf(func_def_355, type, sK181: ($i > $i)).
% 8.00/1.65 thf(func_def_356, type, sK182: ($i > $i)).
% 8.00/1.65 thf(func_def_357, type, sK183: ($i > $i > $i > $i)).
% 8.00/1.65 thf(func_def_358, type, sK184: ($i > $i)).
% 8.00/1.65 thf(func_def_359, type, sK185: ($i > $i)).
% 8.00/1.65 thf(func_def_360, type, sK186: ($i > $i)).
% 8.00/1.65 thf(func_def_361, type, sK187: ($i > $i)).
% 8.00/1.65 thf(func_def_362, type, sK188: ($i > $i > $i)).
% 8.00/1.65 thf(func_def_363, type, sK189: ($i > $i > $i)).
% 8.00/1.65 thf(func_def_364, type, sK190: ($i > $i > $i > $i)).
% 8.00/1.65 thf(func_def_365, type, sK191: ($i > $i > $i > $i)).
% 8.00/1.65 thf(func_def_366, type, sK192: ($i > $i > $i > $i)).
% 8.00/1.65 thf(func_def_367, type, sK193: ($i > $i > $i)).
% 8.00/1.65 thf(func_def_368, type, sK194: ($i > $i > $i)).
% 8.00/1.65 thf(func_def_369, type, sK195: ($i > $i > $i)).
% 8.00/1.65 thf(func_def_370, type, sK196: ($i > $o)).
% 8.00/1.65 thf(func_def_373, type, sK199: ($i > ($i > $o) > $i)).
% 8.00/1.65 thf(func_def_374, type, sK200: ($i > $o)).
% 8.00/1.65 thf(func_def_382, type, sK208: ($i > $i > $i)).
% 8.00/1.65 thf(func_def_385, type, sK211: ($o > $i > $i > $i)).
% 8.00/1.65 thf(func_def_388, type, sK214: $o).
% 8.00/1.65 thf(func_def_389, type, sK215: ($i > $o)).
% 8.00/1.65 thf(func_def_391, type, sK217: ($i > ($i > $o) > $i)).
% 8.00/1.65 thf(func_def_397, type, sK223: ($i > ($i > $o) > $i)).
% 8.00/1.65 thf(func_def_398, type, sK224: ($i > $o)).
% 8.00/1.65 thf(func_def_408, type, sK234: ($i > $o)).
% 8.00/1.65 thf(func_def_411, type, sK237: ($i > $o)).
% 8.00/1.65 thf(func_def_428, type, sK254: ($i > $o)).
% 8.00/1.65 thf(func_def_429, type, sK255: ($i > $o)).
% 8.00/1.65 thf(func_def_430, type, sK256: (($i > $o) > ($i > $o) > $i > $i > $i)).
% 8.00/1.65 thf(func_def_431, type, sK257: (($i > $o) > ($i > $o) > $i > $i > $i)).
% 8.00/1.65 thf(func_def_445, type, sK271: ($i > $i)).
% 8.00/1.65 thf(func_def_450, type, sK276: $o).
% 8.00/1.65 thf(func_def_457, type, sK283: ($i > $i > $o)).
% 8.00/1.65 thf(func_def_459, type, sK285: ($i > $i)).
% 8.00/1.65 thf(func_def_460, type, sK286: ($i > $i)).
% 8.00/1.65 thf(func_def_461, type, sK287: ($i > ($i > $i > $o) > $i)).
% 8.00/1.65 thf(func_def_462, type, sK288: ($i > $i > ($i > $i > $o) > $i)).
% 8.00/1.65 thf(func_def_463, type, sK289: ($i > ($i > $i > $o) > $i)).
% 8.00/1.65 thf(func_def_470, type, sK296: ($i > $o)).
% 8.00/1.65 thf(func_def_485, type, sK311: ($i > $i)).
% 8.00/1.65 thf(func_def_491, type, sK317: $o).
% 8.00/1.65 thf(func_def_492, type, sK318: (($i > $o) > $i > $i)).
% 8.00/1.65 thf(func_def_494, type, sK320: ($i > $o)).
% 8.00/1.65 thf(func_def_501, type, sK327: ($i > $i > $i)).
% 8.00/1.65 thf(func_def_504, type, sK330: ($i > $o)).
% 8.00/1.65 thf(func_def_505, type, sK331: (($i > $o) > $i)).
% 8.00/1.65 thf(func_def_511, type, sK337: ($i > $i)).
% 8.00/1.65 thf(func_def_513, type, sK339: ($i > $i > $i)).
% 8.00/1.65 thf(func_def_514, type, sK340: ($i > $i > $i)).
% 8.00/1.65 thf(func_def_517, type, sK343: (($i > $o) > $i)).
% 8.00/1.65 thf(func_def_518, type, sK344: ($i > $o)).
% 8.00/1.65 thf(func_def_519, type, sK345: ($i > $i)).
% 8.00/1.65 thf(func_def_521, type, sK347: ($i > $o)).
% 8.00/1.65 thf(func_def_537, type, sK363: ($i > $o)).
% 8.00/1.65 thf(func_def_538, type, sK364: ($i > ($i > $o) > $i)).
% 8.00/1.65 thf(func_def_539, type, sK365: ($i > $o)).
% 8.00/1.65 thf(func_def_542, type, sK368: ($i > $o)).
% 8.00/1.65 thf(func_def_543, type, sK369: ($i > $o)).
% 8.00/1.65 thf(func_def_544, type, sK370: (($i > $o) > ($i > $o) > $i)).
% 8.00/1.65 thf(func_def_545, type, sK371: (($i > $o) > ($i > $o) > $i)).
% 8.00/1.65 thf(f46,axiom,(
% 8.00/1.65 (! [X1 : $i,X0 : $i] : ((in @ X0 @ (setadjoin @ X1 @ emptyset)) => (X0 = X1)) = uniqinunit)),
% 8.00/1.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',uniqinunit)).
% 8.00/1.65 thf(f78,axiom,(
% 8.00/1.65 (! [X1 : $i,X0 : $i] : (! [X2 : $i] : ((in @ X2 @ X0) => (in @ X2 @ X1)) => (subset @ X0 @ X1)) = subsetI1)),
% 8.00/1.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subsetI1)).
% 8.00/1.65 thf(f143,conjecture,(
% 8.00/1.65 setextAx => (emptysetAx => (setadjoinAx => (powersetAx => (setunionAx => (omega0Ax => (omegaSAx => (omegaIndAx => (replAx => (foundationAx => (wellorderingAx => (descrp => (dsetconstrI => (dsetconstrEL => (dsetconstrER => (exuE1 => (prop2setE => (emptysetE => (emptysetimpfalse => (notinemptyset => (exuE3e => (setext => (emptyI => (noeltsimpempty => (setbeta => (nonemptyE1 => (nonemptyI => (nonemptyI1 => (setadjoinIL => (emptyinunitempty => (setadjoinIR => (setadjoinE => (setadjoinOr => (setoftrueEq => (powersetI => (emptyinPowerset => (emptyInPowerset => (powersetE => (setunionI => (setunionE => (subPowSU => (exuE2 => (nonemptyImpWitness => (uniqinunit => (notinsingleton => (eqinunit => (singletonsswitch => (upairsetE => (upairsetIL => (upairsetIR => (emptyE1 => (vacuousDall => (quantDeMorgan1 => (quantDeMorgan2 => (quantDeMorgan3 => (quantDeMorgan4 => (prop2setI => (prop2set2propI => (notdexE => (notdallE => (exuI1 => (exuI3 => (exuI2 => (inCongP => (in__Cong => (exuE3u => (exu__Cong => (emptyset__Cong => (setadjoin__Cong => (powerset__Cong => (setunion__Cong => (omega__Cong => (exuEu => (descr__Cong => (dsetconstr__Cong => (subsetI1 => (eqimpsubset2 => (eqimpsubset1 => (subsetI2 => (emptysetsubset => (subsetE => (subsetE2 => (notsubsetI => (notequalI1 => (notequalI2 => (subsetRefl => (subsetTrans => (setadjoinSub => (setadjoinSub2 => (subset2powerset => (setextsub => (subsetemptysetimpeq => (powersetI1 => (powersetE1 => (inPowerset => (powersetsubset => (sepInPowerset => (sepSubset => (binunionIL => (upairset2IR => (binunionIR => (binunionEcases => (binunionE => (binunionLsub => (binunionRsub => (binintersectI => (binintersectSubset5 => (binintersectEL => (binintersectLsub => (binintersectSubset2 => (binintersectSubset3 => (binintersectER => (disjointsetsI1 => (binintersectRsub => (binintersectSubset4 => (binintersectSubset1 => (bs114d => (setminusI => (setminusEL => (setminusER => (setminusSubset2 => (setminusERneg => (setminusELneg => (setminusILneg => (setminusIRneg => (setminusLsub => (setminusSubset1 => (symdiffE => (symdiffI1 => (symdiffI2 => (symdiffIneg1 => (symdiffIneg2 => (secondinupair => (setukpairIL => (setukpairIR => (kpairiskpair => (kpairp => ! [X0 : $i,X1 : $i] : ((in @ X1 @ X0) => (subset @ (setadjoin @ X1 @ emptyset) @ X0))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),
% 8.00/1.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',singletonsubset)).
% 8.00/1.65 thf(f144,negated_conjecture,(
% 8.00/1.65 ~(setextAx => (emptysetAx => (setadjoinAx => (powersetAx => (setunionAx => (omega0Ax => (omegaSAx => (omegaIndAx => (replAx => (foundationAx => (wellorderingAx => (descrp => (dsetconstrI => (dsetconstrEL => (dsetconstrER => (exuE1 => (prop2setE => (emptysetE => (emptysetimpfalse => (notinemptyset => (exuE3e => (setext => (emptyI => (noeltsimpempty => (setbeta => (nonemptyE1 => (nonemptyI => (nonemptyI1 => (setadjoinIL => (emptyinunitempty => (setadjoinIR => (setadjoinE => (setadjoinOr => (setoftrueEq => (powersetI => (emptyinPowerset => (emptyInPowerset => (powersetE => (setunionI => (setunionE => (subPowSU => (exuE2 => (nonemptyImpWitness => (uniqinunit => (notinsingleton => (eqinunit => (singletonsswitch => (upairsetE => (upairsetIL => (upairsetIR => (emptyE1 => (vacuousDall => (quantDeMorgan1 => (quantDeMorgan2 => (quantDeMorgan3 => (quantDeMorgan4 => (prop2setI => (prop2set2propI => (notdexE => (notdallE => (exuI1 => (exuI3 => (exuI2 => (inCongP => (in__Cong => (exuE3u => (exu__Cong => (emptyset__Cong => (setadjoin__Cong => (powerset__Cong => (setunion__Cong => (omega__Cong => (exuEu => (descr__Cong => (dsetconstr__Cong => (subsetI1 => (eqimpsubset2 => (eqimpsubset1 => (subsetI2 => (emptysetsubset => (subsetE => (subsetE2 => (notsubsetI => (notequalI1 => (notequalI2 => (subsetRefl => (subsetTrans => (setadjoinSub => (setadjoinSub2 => (subset2powerset => (setextsub => (subsetemptysetimpeq => (powersetI1 => (powersetE1 => (inPowerset => (powersetsubset => (sepInPowerset => (sepSubset => (binunionIL => (upairset2IR => (binunionIR => (binunionEcases => (binunionE => (binunionLsub => (binunionRsub => (binintersectI => (binintersectSubset5 => (binintersectEL => (binintersectLsub => (binintersectSubset2 => (binintersectSubset3 => (binintersectER => (disjointsetsI1 => (binintersectRsub => (binintersectSubset4 => (binintersectSubset1 => (bs114d => (setminusI => (setminusEL => (setminusER => (setminusSubset2 => (setminusERneg => (setminusELneg => (setminusILneg => (setminusIRneg => (setminusLsub => (setminusSubset1 => (symdiffE => (symdiffI1 => (symdiffI2 => (symdiffIneg1 => (symdiffIneg2 => (secondinupair => (setukpairIL => (setukpairIR => (kpairiskpair => (kpairp => ! [X0 : $i,X1 : $i] : ((in @ X1 @ X0) => (subset @ (setadjoin @ X1 @ emptyset) @ X0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),
% 8.00/1.65 inference(negated_conjecture,[status(cth)],[f143])).
% 8.00/1.65 thf(f242,plain,(
% 8.00/1.65 (! [X0 : $i,X1 : $i] : ((in @ X1 @ (setadjoin @ X0 @ emptyset)) => (X0 = X1)) = uniqinunit)),
% 8.00/1.65 inference(rectify,[],[f46])).
% 8.00/1.65 thf(f243,plain,(
% 8.00/1.65 ! [X0 : $i,X1 : $i] : ((((in @ X1 @ (setadjoin @ X0 @ emptyset))) = $true) => (X0 = X1)) <=> (uniqinunit = $true)),
% 8.00/1.65 inference(fool_elimination,[],[f242])).
% 8.00/1.65 thf(f367,plain,(
% 8.00/1.65 (! [X0 : $i,X1 : $i] : (! [X2 : $i] : ((in @ X2 @ X1) => (in @ X2 @ X0)) => (subset @ X1 @ X0)) = subsetI1)),
% 8.00/1.65 inference(rectify,[],[f78])).
% 8.00/1.65 thf(f368,plain,(
% 8.00/1.65 ! [X1 : $i,X0 : $i] : (! [X2 : $i] : ((((in @ X2 @ X1)) = $true) => (((in @ X2 @ X0)) = $true)) => (((subset @ X1 @ X0)) = $true)) <=> (subsetI1 = $true)),
% 8.00/1.65 inference(fool_elimination,[],[f367])).
% 8.00/1.65 thf(f397,plain,(
% 8.00/1.65 ~(setextAx => (emptysetAx => (setadjoinAx => (powersetAx => (setunionAx => (omega0Ax => (omegaSAx => (omegaIndAx => (replAx => (foundationAx => (wellorderingAx => (descrp => (dsetconstrI => (dsetconstrEL => (dsetconstrER => (exuE1 => (prop2setE => (emptysetE => (emptysetimpfalse => (notinemptyset => (exuE3e => (setext => (emptyI => (noeltsimpempty => (setbeta => (nonemptyE1 => (nonemptyI => (nonemptyI1 => (setadjoinIL => (emptyinunitempty => (setadjoinIR => (setadjoinE => (setadjoinOr => (setoftrueEq => (powersetI => (emptyinPowerset => (emptyInPowerset => (powersetE => (setunionI => (setunionE => (subPowSU => (exuE2 => (nonemptyImpWitness => (uniqinunit => (notinsingleton => (eqinunit => (singletonsswitch => (upairsetE => (upairsetIL => (upairsetIR => (emptyE1 => (vacuousDall => (quantDeMorgan1 => (quantDeMorgan2 => (quantDeMorgan3 => (quantDeMorgan4 => (prop2setI => (prop2set2propI => (notdexE => (notdallE => (exuI1 => (exuI3 => (exuI2 => (inCongP => (in__Cong => (exuE3u => (exu__Cong => (emptyset__Cong => (setadjoin__Cong => (powerset__Cong => (setunion__Cong => (omega__Cong => (exuEu => (descr__Cong => (dsetconstr__Cong => (subsetI1 => (eqimpsubset2 => (eqimpsubset1 => (subsetI2 => (emptysetsubset => (subsetE => (subsetE2 => (notsubsetI => (notequalI1 => (notequalI2 => (subsetRefl => (subsetTrans => (setadjoinSub => (setadjoinSub2 => (subset2powerset => (setextsub => (subsetemptysetimpeq => (powersetI1 => (powersetE1 => (inPowerset => (powersetsubset => (sepInPowerset => (sepSubset => (binunionIL => (upairset2IR => (binunionIR => (binunionEcases => (binunionE => (binunionLsub => (binunionRsub => (binintersectI => (binintersectSubset5 => (binintersectEL => (binintersectLsub => (binintersectSubset2 => (binintersectSubset3 => (binintersectER => (disjointsetsI1 => (binintersectRsub => (binintersectSubset4 => (binintersectSubset1 => (bs114d => (setminusI => (setminusEL => (setminusER => (setminusSubset2 => (setminusERneg => (setminusELneg => (setminusILneg => (setminusIRneg => (setminusLsub => (setminusSubset1 => (symdiffE => (symdiffI1 => (symdiffI2 => (symdiffIneg1 => (symdiffIneg2 => (secondinupair => (setukpairIL => (setukpairIR => (kpairiskpair => (kpairp => ! [X0 : $i,X1 : $i] : ((in @ X1 @ X0) => (subset @ (setadjoin @ X1 @ emptyset) @ X0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),
% 8.00/1.65 inference(rectify,[],[f144])).
% 8.00/1.65 thf(f398,plain,(
% 8.00/1.65 ~((setextAx = $true) => ((emptysetAx = $true) => ((setadjoinAx = $true) => ((powersetAx = $true) => ((setunionAx = $true) => ((omega0Ax = $true) => ((omegaSAx = $true) => ((omegaIndAx = $true) => ((replAx = $true) => ((foundationAx = $true) => ((wellorderingAx = $true) => ((descrp = $true) => ((dsetconstrI = $true) => ((dsetconstrEL = $true) => ((dsetconstrER = $true) => ((exuE1 = $true) => ((prop2setE = $true) => ((emptysetE = $true) => ((emptysetimpfalse = $true) => ((notinemptyset = $true) => ((exuE3e = $true) => ((setext = $true) => ((emptyI = $true) => ((noeltsimpempty = $true) => ((setbeta = $true) => ((nonemptyE1 = $true) => ((nonemptyI = $true) => ((nonemptyI1 = $true) => ((setadjoinIL = $true) => ((emptyinunitempty = $true) => ((setadjoinIR = $true) => ((setadjoinE = $true) => ((setadjoinOr = $true) => ((setoftrueEq = $true) => ((powersetI = $true) => ((emptyinPowerset = $true) => ((emptyInPowerset = $true) => ((powersetE = $true) => ((setunionI = $true) => ((setunionE = $true) => ((subPowSU = $true) => ((exuE2 = $true) => ((nonemptyImpWitness = $true) => ((uniqinunit = $true) => ((notinsingleton = $true) => ((eqinunit = $true) => ((singletonsswitch = $true) => ((upairsetE = $true) => ((upairsetIL = $true) => ((upairsetIR = $true) => ((emptyE1 = $true) => ((vacuousDall = $true) => ((quantDeMorgan1 = $true) => ((quantDeMorgan2 = $true) => ((quantDeMorgan3 = $true) => ((quantDeMorgan4 = $true) => ((prop2setI = $true) => ((prop2set2propI = $true) => ((notdexE = $true) => ((notdallE = $true) => ((exuI1 = $true) => ((exuI3 = $true) => ((exuI2 = $true) => ((inCongP = $true) => ((in__Cong = $true) => ((exuE3u = $true) => ((exu__Cong = $true) => ((emptyset__Cong = $true) => ((setadjoin__Cong = $true) => ((powerset__Cong = $true) => ((setunion__Cong = $true) => ((omega__Cong = $true) => ((exuEu = $true) => ((descr__Cong = $true) => ((dsetconstr__Cong = $true) => ((subsetI1 = $true) => ((eqimpsubset2 = $true) => ((eqimpsubset1 = $true) => ((subsetI2 = $true) => ((emptysetsubset = $true) => ((subsetE = $true) => ((subsetE2 = $true) => ((notsubsetI = $true) => ((notequalI1 = $true) => ((notequalI2 = $true) => ((subsetRefl = $true) => ((subsetTrans = $true) => ((setadjoinSub = $true) => ((setadjoinSub2 = $true) => ((subset2powerset = $true) => ((setextsub = $true) => ((subsetemptysetimpeq = $true) => ((powersetI1 = $true) => ((powersetE1 = $true) => ((inPowerset = $true) => ((powersetsubset = $true) => ((sepInPowerset = $true) => ((sepSubset = $true) => ((binunionIL = $true) => ((upairset2IR = $true) => ((binunionIR = $true) => ((binunionEcases = $true) => ((binunionE = $true) => ((binunionLsub = $true) => ((binunionRsub = $true) => ((binintersectI = $true) => ((binintersectSubset5 = $true) => ((binintersectEL = $true) => ((binintersectLsub = $true) => ((binintersectSubset2 = $true) => ((binintersectSubset3 = $true) => ((binintersectER = $true) => ((disjointsetsI1 = $true) => ((binintersectRsub = $true) => ((binintersectSubset4 = $true) => ((binintersectSubset1 = $true) => ((bs114d = $true) => ((setminusI = $true) => ((setminusEL = $true) => ((setminusER = $true) => ((setminusSubset2 = $true) => ((setminusERneg = $true) => ((setminusELneg = $true) => ((setminusILneg = $true) => ((setminusIRneg = $true) => ((setminusLsub = $true) => ((setminusSubset1 = $true) => ((symdiffE = $true) => ((symdiffI1 = $true) => ((symdiffI2 = $true) => ((symdiffIneg1 = $true) => ((symdiffIneg2 = $true) => ((secondinupair = $true) => ((setukpairIL = $true) => ((setukpairIR = $true) => ((kpairiskpair = $true) => ((kpairp = $true) => ! [X1 : $i,X0 : $i] : ((((in @ X1 @ X0)) = $true) => (((subset @ (setadjoin @ X1 @ emptyset) @ X0)) = $true)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),
% 8.00/1.65 inference(fool_elimination,[],[f397])).
% 8.00/1.65 thf(f517,plain,(
% 8.00/1.65 (uniqinunit = $true) <=> ! [X1 : $i,X0 : $i] : ((X0 = X1) | (((in @ X1 @ (setadjoin @ X0 @ emptyset))) != $true))),
% 8.00/1.65 inference(ennf_transformation,[],[f243])).
% 8.00/1.65 thf(f563,plain,(
% 8.00/1.65 ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((? [X1 : $i,X0 : $i] : ((((subset @ (setadjoin @ X1 @ emptyset) @ X0)) != $true) & (((in @ X1 @ X0)) = $true)) & (kpairp = $true)) & (kpairiskpair = $true)) & (setukpairIR = $true)) & (setukpairIL = $true)) & (secondinupair = $true)) & (symdiffIneg2 = $true)) & (symdiffIneg1 = $true)) & (symdiffI2 = $true)) & (symdiffI1 = $true)) & (symdiffE = $true)) & (setminusSubset1 = $true)) & (setminusLsub = $true)) & (setminusIRneg = $true)) & (setminusILneg = $true)) & (setminusELneg = $true)) & (setminusERneg = $true)) & (setminusSubset2 = $true)) & (setminusER = $true)) & (setminusEL = $true)) & (setminusI = $true)) & (bs114d = $true)) & (binintersectSubset1 = $true)) & (binintersectSubset4 = $true)) & (binintersectRsub = $true)) & (disjointsetsI1 = $true)) & (binintersectER = $true)) & (binintersectSubset3 = $true)) & (binintersectSubset2 = $true)) & (binintersectLsub = $true)) & (binintersectEL = $true)) & (binintersectSubset5 = $true)) & (binintersectI = $true)) & (binunionRsub = $true)) & (binunionLsub = $true)) & (binunionE = $true)) & (binunionEcases = $true)) & (binunionIR = $true)) & (upairset2IR = $true)) & (binunionIL = $true)) & (sepSubset = $true)) & (sepInPowerset = $true)) & (powersetsubset = $true)) & (inPowerset = $true)) & (powersetE1 = $true)) & (powersetI1 = $true)) & (subsetemptysetimpeq = $true)) & (setextsub = $true)) & (subset2powerset = $true)) & (setadjoinSub2 = $true)) & (setadjoinSub = $true)) & (subsetTrans = $true)) & (subsetRefl = $true)) & (notequalI2 = $true)) & (notequalI1 = $true)) & (notsubsetI = $true)) & (subsetE2 = $true)) & (subsetE = $true)) & (emptysetsubset = $true)) & (subsetI2 = $true)) & (eqimpsubset1 = $true)) & (eqimpsubset2 = $true)) & (subsetI1 = $true)) & (dsetconstr__Cong = $true)) & (descr__Cong = $true)) & (exuEu = $true)) & (omega__Cong = $true)) & (setunion__Cong = $true)) & (powerset__Cong = $true)) & (setadjoin__Cong = $true)) & (emptyset__Cong = $true)) & (exu__Cong = $true)) & (exuE3u = $true)) & (in__Cong = $true)) & (inCongP = $true)) & (exuI2 = $true)) & (exuI3 = $true)) & (exuI1 = $true)) & (notdallE = $true)) & (notdexE = $true)) & (prop2set2propI = $true)) & (prop2setI = $true)) & (quantDeMorgan4 = $true)) & (quantDeMorgan3 = $true)) & (quantDeMorgan2 = $true)) & (quantDeMorgan1 = $true)) & (vacuousDall = $true)) & (emptyE1 = $true)) & (upairsetIR = $true)) & (upairsetIL = $true)) & (upairsetE = $true)) & (singletonsswitch = $true)) & (eqinunit = $true)) & (notinsingleton = $true)) & (uniqinunit = $true)) & (nonemptyImpWitness = $true)) & (exuE2 = $true)) & (subPowSU = $true)) & (setunionE = $true)) & (setunionI = $true)) & (powersetE = $true)) & (emptyInPowerset = $true)) & (emptyinPowerset = $true)) & (powersetI = $true)) & (setoftrueEq = $true)) & (setadjoinOr = $true)) & (setadjoinE = $true)) & (setadjoinIR = $true)) & (emptyinunitempty = $true)) & (setadjoinIL = $true)) & (nonemptyI1 = $true)) & (nonemptyI = $true)) & (nonemptyE1 = $true)) & (setbeta = $true)) & (noeltsimpempty = $true)) & (emptyI = $true)) & (setext = $true)) & (exuE3e = $true)) & (notinemptyset = $true)) & (emptysetimpfalse = $true)) & (emptysetE = $true)) & (prop2setE = $true)) & (exuE1 = $true)) & (dsetconstrER = $true)) & (dsetconstrEL = $true)) & (dsetconstrI = $true)) & (descrp = $true)) & (wellorderingAx = $true)) & (foundationAx = $true)) & (replAx = $true)) & (omegaIndAx = $true)) & (omegaSAx = $true)) & (omega0Ax = $true)) & (setunionAx = $true)) & (powersetAx = $true)) & (setadjoinAx = $true)) & (emptysetAx = $true)) & (setextAx = $true)),
% 8.00/1.65 inference(ennf_transformation,[],[f398])).
% 8.00/1.65 thf(f564,plain,(
% 8.00/1.65 (setminusSubset1 = $true) & (subsetI2 = $true) & (bs114d = $true) & (prop2set2propI = $true) & (setminusERneg = $true) & (powersetE = $true) & (setadjoin__Cong = $true) & (binunionLsub = $true) & (omega__Cong = $true) & (exuE1 = $true) & (emptysetsubset = $true) & (binintersectI = $true) & (symdiffI2 = $true) & (nonemptyImpWitness = $true) & (dsetconstrER = $true) & (powersetAx = $true) & (kpairiskpair = $true) & (exuE3e = $true) & (emptyset__Cong = $true) & (exuEu = $true) & (nonemptyI1 = $true) & (setunionE = $true) & (setext = $true) & (noeltsimpempty = $true) & (setminusILneg = $true) & (setminusER = $true) & (notequalI2 = $true) & (dsetconstr__Cong = $true) & (omega0Ax = $true) & (exuE2 = $true) & (vacuousDall = $true) & (setadjoinE = $true) & (powerset__Cong = $true) & (eqinunit = $true) & (exu__Cong = $true) & (quantDeMorgan3 = $true) & (powersetI = $true) & (upairsetIL = $true) & (sepInPowerset = $true) & (setadjoinAx = $true) & (wellorderingAx = $true) & (in__Cong = $true) & (powersetI1 = $true) & (symdiffIneg2 = $true) & (exuE3u = $true) & (eqimpsubset1 = $true) & (symdiffE = $true) & (binintersectLsub = $true) & (symdiffIneg1 = $true) & (binintersectRsub = $true) & (emptysetE = $true) & (inCongP = $true) & (setminusLsub = $true) & (setminusELneg = $true) & (setunionI = $true) & (setadjoinIL = $true) & (setadjoinIR = $true) & (upairsetIR = $true) & (setadjoinOr = $true) & (setminusEL = $true) & ? [X1 : $i,X0 : $i] : ((((subset @ (setadjoin @ X1 @ emptyset) @ X0)) != $true) & (((in @ X1 @ X0)) = $true)) & (inPowerset = $true) & (dsetconstrI = $true) & (quantDeMorgan2 = $true) & (binintersectSubset3 = $true) & (notinsingleton = $true) & (uniqinunit = $true) & (emptyinPowerset = $true) & (quantDeMorgan1 = $true) & (setadjoinSub2 = $true) & (subPowSU = $true) & (quantDeMorgan4 = $true) & (emptyI = $true) & (binintersectER = $true) & (setextAx = $true) & (setunionAx = $true) & (exuI1 = $true) & (powersetsubset = $true) & (nonemptyE1 = $true) & (binintersectEL = $true) & (binunionE = $true) & (subset2powerset = $true) & (binunionEcases = $true) & (subsetE = $true) & (subsetRefl = $true) & (setextsub = $true) & (notequalI1 = $true) & (dsetconstrEL = $true) & (singletonsswitch = $true) & (emptysetimpfalse = $true) & (upairsetE = $true) & (emptyInPowerset = $true) & (setminusIRneg = $true) & (omegaSAx = $true) & (binintersectSubset2 = $true) & (subsetemptysetimpeq = $true) & (omegaIndAx = $true) & (binintersectSubset5 = $true) & (replAx = $true) & (disjointsetsI1 = $true) & (notsubsetI = $true) & (binunionRsub = $true) & (eqimpsubset2 = $true) & (setminusI = $true) & (binintersectSubset1 = $true) & (emptyE1 = $true) & (binunionIR = $true) & (secondinupair = $true) & (setukpairIL = $true) & (setoftrueEq = $true) & (notdexE = $true) & (setbeta = $true) & (descrp = $true) & (exuI2 = $true) & (prop2setI = $true) & (emptysetAx = $true) & (sepSubset = $true) & (nonemptyI = $true) & (binunionIL = $true) & (descr__Cong = $true) & (binintersectSubset4 = $true) & (notinemptyset = $true) & (setadjoinSub = $true) & (subsetI1 = $true) & (powersetE1 = $true) & (exuI3 = $true) & (symdiffI1 = $true) & (subsetE2 = $true) & (foundationAx = $true) & (upairset2IR = $true) & (prop2setE = $true) & (setunion__Cong = $true) & (notdallE = $true) & (subsetTrans = $true) & (kpairp = $true) & (setminusSubset2 = $true) & (emptyinunitempty = $true) & (setukpairIR = $true)),
% 8.00/1.65 inference(flattening,[],[f563])).
% 8.00/1.65 thf(f593,plain,(
% 8.00/1.65 ! [X0 : $i,X1 : $i] : ((((subset @ X1 @ X0)) = $true) | ? [X2 : $i] : ((((in @ X2 @ X1)) = $true) & (((in @ X2 @ X0)) != $true))) <=> (subsetI1 = $true)),
% 8.00/1.65 inference(ennf_transformation,[],[f368])).
% 8.00/1.65 thf(f823,plain,(
% 8.00/1.65 (setminusSubset1 = $true) & (subsetI2 = $true) & (bs114d = $true) & (prop2set2propI = $true) & (setminusERneg = $true) & (powersetE = $true) & (setadjoin__Cong = $true) & (binunionLsub = $true) & (omega__Cong = $true) & (exuE1 = $true) & (emptysetsubset = $true) & (binintersectI = $true) & (symdiffI2 = $true) & (nonemptyImpWitness = $true) & (dsetconstrER = $true) & (powersetAx = $true) & (kpairiskpair = $true) & (exuE3e = $true) & (emptyset__Cong = $true) & (exuEu = $true) & (nonemptyI1 = $true) & (setunionE = $true) & (setext = $true) & (noeltsimpempty = $true) & (setminusILneg = $true) & (setminusER = $true) & (notequalI2 = $true) & (dsetconstr__Cong = $true) & (omega0Ax = $true) & (exuE2 = $true) & (vacuousDall = $true) & (setadjoinE = $true) & (powerset__Cong = $true) & (eqinunit = $true) & (exu__Cong = $true) & (quantDeMorgan3 = $true) & (powersetI = $true) & (upairsetIL = $true) & (sepInPowerset = $true) & (setadjoinAx = $true) & (wellorderingAx = $true) & (in__Cong = $true) & (powersetI1 = $true) & (symdiffIneg2 = $true) & (exuE3u = $true) & (eqimpsubset1 = $true) & (symdiffE = $true) & (binintersectLsub = $true) & (symdiffIneg1 = $true) & (binintersectRsub = $true) & (emptysetE = $true) & (inCongP = $true) & (setminusLsub = $true) & (setminusELneg = $true) & (setunionI = $true) & (setadjoinIL = $true) & (setadjoinIR = $true) & (upairsetIR = $true) & (setadjoinOr = $true) & (setminusEL = $true) & ? [X0 : $i,X1 : $i] : (($true != ((subset @ (setadjoin @ X0 @ emptyset) @ X1))) & ($true = ((in @ X0 @ X1)))) & (inPowerset = $true) & (dsetconstrI = $true) & (quantDeMorgan2 = $true) & (binintersectSubset3 = $true) & (notinsingleton = $true) & (uniqinunit = $true) & (emptyinPowerset = $true) & (quantDeMorgan1 = $true) & (setadjoinSub2 = $true) & (subPowSU = $true) & (quantDeMorgan4 = $true) & (emptyI = $true) & (binintersectER = $true) & (setextAx = $true) & (setunionAx = $true) & (exuI1 = $true) & (powersetsubset = $true) & (nonemptyE1 = $true) & (binintersectEL = $true) & (binunionE = $true) & (subset2powerset = $true) & (binunionEcases = $true) & (subsetE = $true) & (subsetRefl = $true) & (setextsub = $true) & (notequalI1 = $true) & (dsetconstrEL = $true) & (singletonsswitch = $true) & (emptysetimpfalse = $true) & (upairsetE = $true) & (emptyInPowerset = $true) & (setminusIRneg = $true) & (omegaSAx = $true) & (binintersectSubset2 = $true) & (subsetemptysetimpeq = $true) & (omegaIndAx = $true) & (binintersectSubset5 = $true) & (replAx = $true) & (disjointsetsI1 = $true) & (notsubsetI = $true) & (binunionRsub = $true) & (eqimpsubset2 = $true) & (setminusI = $true) & (binintersectSubset1 = $true) & (emptyE1 = $true) & (binunionIR = $true) & (secondinupair = $true) & (setukpairIL = $true) & (setoftrueEq = $true) & (notdexE = $true) & (setbeta = $true) & (descrp = $true) & (exuI2 = $true) & (prop2setI = $true) & (emptysetAx = $true) & (sepSubset = $true) & (nonemptyI = $true) & (binunionIL = $true) & (descr__Cong = $true) & (binintersectSubset4 = $true) & (notinemptyset = $true) & (setadjoinSub = $true) & (subsetI1 = $true) & (powersetE1 = $true) & (exuI3 = $true) & (symdiffI1 = $true) & (subsetE2 = $true) & (foundationAx = $true) & (upairset2IR = $true) & (prop2setE = $true) & (setunion__Cong = $true) & (notdallE = $true) & (subsetTrans = $true) & (kpairp = $true) & (setminusSubset2 = $true) & (emptyinunitempty = $true) & (setukpairIR = $true)),
% 8.00/1.65 inference(rectify,[],[f564])).
% 8.00/1.65 thf(f824,plain,(
% 8.00/1.65 (setminusSubset1 = $true) & (subsetI2 = $true) & (bs114d = $true) & (prop2set2propI = $true) & (setminusERneg = $true) & (powersetE = $true) & (setadjoin__Cong = $true) & (binunionLsub = $true) & (omega__Cong = $true) & (exuE1 = $true) & (emptysetsubset = $true) & (binintersectI = $true) & (symdiffI2 = $true) & (nonemptyImpWitness = $true) & (dsetconstrER = $true) & (powersetAx = $true) & (kpairiskpair = $true) & (exuE3e = $true) & (emptyset__Cong = $true) & (exuEu = $true) & (nonemptyI1 = $true) & (setunionE = $true) & (setext = $true) & (noeltsimpempty = $true) & (setminusILneg = $true) & (setminusER = $true) & (notequalI2 = $true) & (dsetconstr__Cong = $true) & (omega0Ax = $true) & (exuE2 = $true) & (vacuousDall = $true) & (setadjoinE = $true) & (powerset__Cong = $true) & (eqinunit = $true) & (exu__Cong = $true) & (quantDeMorgan3 = $true) & (powersetI = $true) & (upairsetIL = $true) & (sepInPowerset = $true) & (setadjoinAx = $true) & (wellorderingAx = $true) & (in__Cong = $true) & (powersetI1 = $true) & (symdiffIneg2 = $true) & (exuE3u = $true) & (eqimpsubset1 = $true) & (symdiffE = $true) & (binintersectLsub = $true) & (symdiffIneg1 = $true) & (binintersectRsub = $true) & (emptysetE = $true) & (inCongP = $true) & (setminusLsub = $true) & (setminusELneg = $true) & (setunionI = $true) & (setadjoinIL = $true) & (setadjoinIR = $true) & (upairsetIR = $true) & (setadjoinOr = $true) & (setminusEL = $true) & (($true != ((subset @ (setadjoin @ sK197 @ emptyset) @ sK198))) & ($true = ((in @ sK197 @ sK198)))) & (inPowerset = $true) & (dsetconstrI = $true) & (quantDeMorgan2 = $true) & (binintersectSubset3 = $true) & (notinsingleton = $true) & (uniqinunit = $true) & (emptyinPowerset = $true) & (quantDeMorgan1 = $true) & (setadjoinSub2 = $true) & (subPowSU = $true) & (quantDeMorgan4 = $true) & (emptyI = $true) & (binintersectER = $true) & (setextAx = $true) & (setunionAx = $true) & (exuI1 = $true) & (powersetsubset = $true) & (nonemptyE1 = $true) & (binintersectEL = $true) & (binunionE = $true) & (subset2powerset = $true) & (binunionEcases = $true) & (subsetE = $true) & (subsetRefl = $true) & (setextsub = $true) & (notequalI1 = $true) & (dsetconstrEL = $true) & (singletonsswitch = $true) & (emptysetimpfalse = $true) & (upairsetE = $true) & (emptyInPowerset = $true) & (setminusIRneg = $true) & (omegaSAx = $true) & (binintersectSubset2 = $true) & (subsetemptysetimpeq = $true) & (omegaIndAx = $true) & (binintersectSubset5 = $true) & (replAx = $true) & (disjointsetsI1 = $true) & (notsubsetI = $true) & (binunionRsub = $true) & (eqimpsubset2 = $true) & (setminusI = $true) & (binintersectSubset1 = $true) & (emptyE1 = $true) & (binunionIR = $true) & (secondinupair = $true) & (setukpairIL = $true) & (setoftrueEq = $true) & (notdexE = $true) & (setbeta = $true) & (descrp = $true) & (exuI2 = $true) & (prop2setI = $true) & (emptysetAx = $true) & (sepSubset = $true) & (nonemptyI = $true) & (binunionIL = $true) & (descr__Cong = $true) & (binintersectSubset4 = $true) & (notinemptyset = $true) & (setadjoinSub = $true) & (subsetI1 = $true) & (powersetE1 = $true) & (exuI3 = $true) & (symdiffI1 = $true) & (subsetE2 = $true) & (foundationAx = $true) & (upairset2IR = $true) & (prop2setE = $true) & (setunion__Cong = $true) & (notdallE = $true) & (subsetTrans = $true) & (kpairp = $true) & (setminusSubset2 = $true) & (emptyinunitempty = $true) & (setukpairIR = $true)),
% 8.00/1.65 inference(skolemize,[status(esa),new_symbols(skolem,[sK197,sK198]),skolemize(X0,sK197),skolemize(X1,sK198)],[f823])).
% 8.00/1.65 thf(f834,plain,(
% 8.00/1.65 (! [X0 : $i,X1 : $i] : ((((subset @ X1 @ X0)) = $true) | ? [X2 : $i] : ((((in @ X2 @ X1)) = $true) & (((in @ X2 @ X0)) != $true))) | (subsetI1 != $true)) & ((subsetI1 = $true) | ? [X0 : $i,X1 : $i] : ((((subset @ X1 @ X0)) != $true) & ! [X2 : $i] : ((((in @ X2 @ X1)) != $true) | (((in @ X2 @ X0)) = $true))))),
% 8.00/1.65 inference(nnf_transformation,[],[f593])).
% 8.00/1.65 thf(f835,plain,(
% 8.00/1.65 (! [X0 : $i,X1 : $i] : ((((subset @ X1 @ X0)) = $true) | ? [X2 : $i] : ((((in @ X2 @ X1)) = $true) & (((in @ X2 @ X0)) != $true))) | (subsetI1 != $true)) & ((subsetI1 = $true) | ? [X3 : $i,X4 : $i] : ((((subset @ X4 @ X3)) != $true) & ! [X5 : $i] : ((((in @ X5 @ X4)) != $true) | (((in @ X5 @ X3)) = $true))))),
% 8.00/1.65 inference(rectify,[],[f834])).
% 8.00/1.65 thf(f836,plain,(
% 8.00/1.65 (! [X0 : $i,X1 : $i] : ((((subset @ X1 @ X0)) = $true) | (($true = ((in @ (sK208 @ X1 @ X0) @ X1))) & ($true != ((in @ (sK208 @ X1 @ X0) @ X0))))) | (subsetI1 != $true)) & ((subsetI1 = $true) | (($true != ((subset @ sK210 @ sK209))) & ! [X5 : $i] : ((((in @ X5 @ sK210)) != $true) | ($true = ((in @ X5 @ sK209))))))),
% 8.00/1.65 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP,sK209,sK210]),skolemize(X6,sK17 @ X5 @ X4),skolemize(X3,sK209),skolemize(X4,sK210)],[f835])).
% 8.00/1.65 thf(f925,plain,(
% 8.00/1.65 ((uniqinunit = $true) | ? [X1 : $i,X0 : $i] : ((X0 != X1) & (((in @ X1 @ (setadjoin @ X0 @ emptyset))) = $true))) & (! [X1 : $i,X0 : $i] : ((X0 = X1) | (((in @ X1 @ (setadjoin @ X0 @ emptyset))) != $true)) | (uniqinunit != $true))),
% 8.00/1.65 inference(nnf_transformation,[],[f517])).
% 8.00/1.65 thf(f926,plain,(
% 8.00/1.65 ((uniqinunit = $true) | ? [X0 : $i,X1 : $i] : ((X0 != X1) & (((in @ X0 @ (setadjoin @ X1 @ emptyset))) = $true))) & (! [X2 : $i,X3 : $i] : ((X2 = X3) | ($true != ((in @ X2 @ (setadjoin @ X3 @ emptyset))))) | (uniqinunit != $true))),
% 8.00/1.65 inference(rectify,[],[f925])).
% 8.00/1.65 thf(f927,plain,(
% 8.00/1.65 ((uniqinunit = $true) | ((sK291 != sK290) & ($true = ((in @ sK290 @ (setadjoin @ sK291 @ emptyset)))))) & (! [X2 : $i,X3 : $i] : ((X2 = X3) | ($true != ((in @ X2 @ (setadjoin @ X3 @ emptyset))))) | (uniqinunit != $true))),
% 8.00/1.65 inference(skolemize,[status(esa),new_symbols(skolem,[sK290,sK291]),skolemize(X0,sK290),skolemize(X1,sK291)],[f926])).
% 8.00/1.65 thf(f1328,plain,(
% 8.00/1.65 (subsetI1 = $true)),
% 8.00/1.65 inference(cnf_transformation,[],[f824])).
% 8.00/1.65 thf(f1385,plain,(
% 8.00/1.65 (uniqinunit = $true)),
% 8.00/1.65 inference(cnf_transformation,[],[f824])).
% 8.00/1.65 thf(f1391,plain,(
% 8.00/1.65 ($true = ((in @ sK197 @ sK198)))),
% 8.00/1.65 inference(cnf_transformation,[],[f824])).
% 8.00/1.65 thf(f1392,plain,(
% 8.00/1.65 ($true != ((subset @ (setadjoin @ sK197 @ emptyset) @ sK198)))),
% 8.00/1.65 inference(cnf_transformation,[],[f824])).
% 8.00/1.65 thf(f1467,plain,(
% 8.00/1.65 ( ! [X0 : $i,X1 : $i] : (($true != ((in @ (sK208 @ X1 @ X0) @ X0))) | (subsetI1 != $true) | (((subset @ X1 @ X0)) = $true)) )),
% 8.00/1.65 inference(cnf_transformation,[],[f836])).
% 8.00/1.65 thf(f1468,plain,(
% 8.00/1.65 ( ! [X0 : $i,X1 : $i] : ((subsetI1 != $true) | ($true = ((in @ (sK208 @ X1 @ X0) @ X1))) | (((subset @ X1 @ X0)) = $true)) )),
% 8.00/1.65 inference(cnf_transformation,[],[f836])).
% 8.00/1.65 thf(f1581,plain,(
% 8.00/1.65 ( ! [X2 : $i,X3 : $i] : ((X2 = X3) | (uniqinunit != $true) | ($true != ((in @ X2 @ (setadjoin @ X3 @ emptyset))))) )),
% 8.00/1.65 inference(cnf_transformation,[],[f927])).
% 8.00/1.65 thf(f2127,definition,(
% 8.00/1.65 spl372_65 <=> (subsetI1 = $true)),
% 8.00/1.65 introduced(definition,[new_symbols(definition,[spl372_65])],[avatar_definition])).
% 8.00/1.65 thf(f2130,plain,(
% 8.00/1.65 spl372_65),
% 8.00/1.65 inference(avatar_split_clause,[],[f1328,f2127])).
% 8.00/1.65 thf(f2619,definition,(
% 8.00/1.65 spl372_174 <=> ! [X0 : $i,X1 : $i] : (($true = ((in @ (sK208 @ X1 @ X0) @ X1))) | (((subset @ X1 @ X0)) = $true))),
% 8.00/1.65 introduced(definition,[new_symbols(definition,[spl372_174])],[avatar_definition])).
% 8.00/1.65 thf(f2620,plain,(
% 8.00/1.65 ( ! [X0 : $i,X1 : $i] : (($true = ((in @ (sK208 @ X1 @ X0) @ X1))) | (((subset @ X1 @ X0)) = $true)) ) | ~spl372_174),
% 8.00/1.65 inference(avatar_component_clause,[],[f2619])).
% 8.00/1.65 thf(f2621,plain,(
% 8.00/1.65 ~spl372_65 | spl372_174),
% 8.00/1.65 inference(avatar_split_clause,[],[f1468,f2619,f2127])).
% 8.00/1.65 thf(f2690,definition,(
% 8.00/1.65 spl372_190 <=> ($true = ((in @ sK197 @ sK198)))),
% 8.00/1.65 introduced(definition,[new_symbols(definition,[spl372_190])],[avatar_definition])).
% 8.00/1.65 thf(f2692,plain,(
% 8.00/1.65 ($true = ((in @ sK197 @ sK198))) | ~spl372_190),
% 8.00/1.65 inference(avatar_component_clause,[],[f2690])).
% 8.00/1.65 thf(f2693,plain,(
% 8.00/1.65 spl372_190),
% 8.00/1.65 inference(avatar_split_clause,[],[f1391,f2690])).
% 8.00/1.65 thf(f2695,definition,(
% 8.00/1.65 spl372_191 <=> (uniqinunit = $true)),
% 8.00/1.65 introduced(definition,[new_symbols(definition,[spl372_191])],[avatar_definition])).
% 8.00/1.65 thf(f3063,definition,(
% 8.00/1.65 spl372_272 <=> ! [X2 : $i,X3 : $i] : ((X2 = X3) | ($true != ((in @ X2 @ (setadjoin @ X3 @ emptyset)))))),
% 8.00/1.66 introduced(definition,[new_symbols(definition,[spl372_272])],[avatar_definition])).
% 8.00/1.66 thf(f3064,plain,(
% 8.00/1.66 ( ! [X2 : $i,X3 : $i] : (($true != ((in @ X2 @ (setadjoin @ X3 @ emptyset)))) | (X2 = X3)) ) | ~spl372_272),
% 8.00/1.66 inference(avatar_component_clause,[],[f3063])).
% 8.00/1.66 thf(f3065,plain,(
% 8.00/1.66 spl372_272 | ~spl372_191),
% 8.00/1.66 inference(avatar_split_clause,[],[f1581,f2695,f3063])).
% 8.00/1.66 thf(f3090,definition,(
% 8.00/1.66 spl372_278 <=> ! [X0 : $i,X1 : $i] : (($true != ((in @ (sK208 @ X1 @ X0) @ X0))) | (((subset @ X1 @ X0)) = $true))),
% 8.00/1.66 introduced(definition,[new_symbols(definition,[spl372_278])],[avatar_definition])).
% 8.00/1.66 thf(f3091,plain,(
% 8.00/1.66 ( ! [X0 : $i,X1 : $i] : (($true != ((in @ (sK208 @ X1 @ X0) @ X0))) | (((subset @ X1 @ X0)) = $true)) ) | ~spl372_278),
% 8.00/1.66 inference(avatar_component_clause,[],[f3090])).
% 8.00/1.66 thf(f3092,plain,(
% 8.00/1.66 ~spl372_65 | spl372_278),
% 8.00/1.66 inference(avatar_split_clause,[],[f1467,f3090,f2127])).
% 8.00/1.66 thf(f3178,plain,(
% 8.00/1.66 spl372_191),
% 8.00/1.66 inference(avatar_split_clause,[],[f1385,f2695])).
% 8.00/1.66 thf(f4108,definition,(
% 8.00/1.66 spl372_488 <=> ($true = ((subset @ (setadjoin @ sK197 @ emptyset) @ sK198)))),
% 8.00/1.66 introduced(definition,[new_symbols(definition,[spl372_488])],[avatar_definition])).
% 8.00/1.66 thf(f4110,plain,(
% 8.00/1.66 ($true != ((subset @ (setadjoin @ sK197 @ emptyset) @ sK198))) | spl372_488),
% 8.00/1.66 inference(avatar_component_clause,[],[f4108])).
% 8.00/1.66 thf(f4111,plain,(
% 8.00/1.66 ~spl372_488),
% 8.00/1.66 inference(avatar_split_clause,[],[f1392,f4108])).
% 8.00/1.66 thf(f5260,plain,(
% 8.00/1.66 ( ! [X0 : $i,X1 : $i] : (($true != $true) | (((sK208 @ (setadjoin @ X0 @ emptyset) @ X1)) = X0) | ($true = ((subset @ (setadjoin @ X0 @ emptyset) @ X1)))) ) | (~spl372_174 | ~spl372_272)),
% 8.00/1.66 inference(superposition,[],[f3064,f2620])).
% 8.00/1.66 thf(f5272,plain,(
% 8.00/1.66 ( ! [X0 : $i,X1 : $i] : (($true = ((subset @ (setadjoin @ X0 @ emptyset) @ X1))) | (((sK208 @ (setadjoin @ X0 @ emptyset) @ X1)) = X0)) ) | (~spl372_174 | ~spl372_272)),
% 8.00/1.66 inference(trivial_inequality_removal,[],[f5260])).
% 8.00/1.66 thf(f11645,plain,(
% 8.00/1.66 (((sK208 @ (setadjoin @ sK197 @ emptyset) @ sK198)) = sK197) | ($true != $true) | (~spl372_174 | ~spl372_272 | spl372_488)),
% 8.00/1.66 inference(superposition,[],[f4110,f5272])).
% 8.00/1.66 thf(f11690,plain,(
% 8.00/1.66 (((sK208 @ (setadjoin @ sK197 @ emptyset) @ sK198)) = sK197) | (~spl372_174 | ~spl372_272 | spl372_488)),
% 8.00/1.66 inference(trivial_inequality_removal,[],[f11645])).
% 8.00/1.66 thf(f11706,definition,(
% 8.00/1.66 spl372_806 <=> (((sK208 @ (setadjoin @ sK197 @ emptyset) @ sK198)) = sK197)),
% 8.00/1.66 introduced(definition,[new_symbols(definition,[spl372_806])],[avatar_definition])).
% 8.00/1.66 thf(f11708,plain,(
% 8.00/1.66 (((sK208 @ (setadjoin @ sK197 @ emptyset) @ sK198)) = sK197) | ~spl372_806),
% 8.00/1.66 inference(avatar_component_clause,[],[f11706])).
% 8.00/1.66 thf(f11709,plain,(
% 8.00/1.66 spl372_806 | ~spl372_174 | ~spl372_272 | spl372_488),
% 8.00/1.66 inference(avatar_split_clause,[],[f11690,f4108,f3063,f2619,f11706])).
% 8.00/1.66 thf(f11710,plain,(
% 8.00/1.66 ($true != ((in @ sK197 @ sK198))) | ($true = ((subset @ (setadjoin @ sK197 @ emptyset) @ sK198))) | (~spl372_278 | ~spl372_806)),
% 8.00/1.66 inference(superposition,[],[f3091,f11708])).
% 8.00/1.66 thf(f11712,plain,(
% 8.00/1.66 ($true = ((subset @ (setadjoin @ sK197 @ emptyset) @ sK198))) | (~spl372_190 | ~spl372_278 | ~spl372_806)),
% 8.00/1.66 inference(forward_subsumption_resolution,[],[f11710,f2692])).
% 8.00/1.66 thf(f11713,plain,(
% 8.00/1.66 $false | (~spl372_190 | ~spl372_278 | spl372_488 | ~spl372_806)),
% 8.00/1.66 inference(forward_subsumption_resolution,[],[f11712,f4110])).
% 8.00/1.66 thf(f11714,plain,(
% 8.00/1.66 ~spl372_190 | ~spl372_278 | spl372_488 | ~spl372_806),
% 8.00/1.66 inference(avatar_contradiction_clause,[],[f11713])).
% 8.00/1.66 cnf(s42, plain, spl372_65, inference(sat_conversion,[],[f2130])).
% 8.00/1.66 cnf(s125, plain, ~spl372_65 | spl372_174, inference(sat_conversion,[],[f2621])).
% 8.00/1.66 cnf(s137, plain, spl372_190, inference(sat_conversion,[],[f2693])).
% 8.00/1.66 cnf(s206, plain, ~spl372_191 | spl372_272, inference(sat_conversion,[],[f3065])).
% 8.00/1.66 cnf(s212, plain, ~spl372_65 | spl372_278, inference(sat_conversion,[],[f3092])).
% 8.00/1.66 cnf(s233, plain, spl372_191, inference(sat_conversion,[],[f3178])).
% 8.00/1.66 cnf(s471, plain, ~spl372_488, inference(sat_conversion,[],[f4111])).
% 8.00/1.66 cnf(s900, plain, ~spl372_174 | ~spl372_272 | spl372_488 | spl372_806, inference(sat_conversion,[],[f11709])).
% 8.00/1.66 cnf(s901, plain, ~spl372_190 | ~spl372_278 | spl372_488 | ~spl372_806, inference(sat_conversion,[],[f11714])).
% 8.00/1.66 cnf(s978, plain, spl372_272, inference(rat,[],[s206,s233])).
% 8.00/1.66 cnf(s1067, plain, spl372_278, inference(rat,[],[s212,s42])).
% 8.00/1.66 cnf(s1068, plain, spl372_174, inference(rat,[],[s125,s42])).
% 8.00/1.66 cnf(s1069, plain, ~spl372_806, inference(rat,[],[s901,s137,s471,s1067])).
% 8.00/1.66 cnf(s1070, plain, $false, inference(rat,[],[s900,s978,s471,s1069,s1068])).
% 8.00/1.66 thf(f11715,plain,(
% 8.00/1.66 $false),
% 8.00/1.66 inference(avatar_sat_refutation,[],[s1070])).
% 8.00/1.66 % SZS output end Proof for theBenchmark
% 8.00/1.66 % (1287995)------------------------------
% 8.00/1.66 % (1287995)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.00/1.66 % (1287995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.00/1.66 % (1287995)CaDiCaL version: 2.1.3
% 8.00/1.66 % (1287995)Termination reason: Refutation
% 8.00/1.66 % (1287995)Time elapsed: 0.226 s
% 8.00/1.66 % (1287995)Peak memory usage: 20 MB
% 8.00/1.66 % (1287995)Instructions burned: 758 (million)
% 8.00/1.66 % (1287825)Success in time 1.405 s
% 8.00/1.66 % Vampire exiting
%------------------------------------------------------------------------------