%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR132^1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 07:47:06 AM UTC 2026
% Result : Theorem 3.54s 0.92s
% Output : Refutation 3.54s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : CSR132^1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.24/0.27 % Computer : n017.cluster.edu
% 0.24/0.27 % Model : x86_64 x86_64
% 0.24/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.24/0.27 % Memory : 8046.5625MB
% 0.24/0.27 % OS : Linux 6.8.0-71-generic
% 0.24/0.28 % CPULimit : 300
% 0.24/0.28 % WCLimit : 300
% 0.24/0.28 % DateTime : Tue Sep 29 17:51:08 UTC 2026
% 0.24/0.28 % CPUTime :
% 0.24/0.28 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.24/0.31 Running higher-order theorem proving
% 0.24/0.33 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
% 1.02/0.48 % (675751)Detected a higher-order problem, will run a greedy HOL sequence.
% 1.02/0.48 % (675762)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 1.02/0.48 % (675762)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 1.02/0.48 % (675762)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=378859420:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 1.02/0.48 % (675756)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=701524379:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 1.02/0.48 % (675757)lrs+10_16_si=on:nwc=1.5:random_seed=2145384960:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 1.02/0.48 % (675758)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=583929617:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 1.02/0.48 % (675760)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=2164974734:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 1.02/0.48 % (675759)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=1373395773: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)
% 1.02/0.48 % (675761)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=1023006539:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 1.02/0.48 % (675758)Instruction limit reached!
% 1.02/0.48 % (675758)------------------------------
% 1.02/0.48 % (675758)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.02/0.48 % (675758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.02/0.48 % (675758)CaDiCaL version: 2.1.3
% 1.02/0.48 % (675758)Termination reason: Instruction limit
% 1.02/0.48 % (675758)Termination phase: Saturation
% 1.02/0.48 % (675758)Time elapsed: 0.004 s
% 1.02/0.48 % (675758)Peak memory usage: 12 MB
% 1.02/0.48 % (675758)Instructions burned: 3 (million)
% 1.02/0.48 % (675756)Refutation not found, incomplete strategy
% 1.02/0.48 % (675756)------------------------------
% 1.02/0.48 % (675756)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.02/0.48 % (675756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.02/0.48 % (675756)CaDiCaL version: 2.1.3
% 1.02/0.48 % (675756)Termination reason: Refutation not found, incomplete strategy
% 1.02/0.48 % (675756)Time elapsed: 0.005 s
% 1.02/0.48 % (675756)Peak memory usage: 12 MB
% 1.02/0.48 % (675756)Instructions burned: 4 (million)
% 1.02/0.48 % (675760)Refutation not found, incomplete strategy
% 1.02/0.48 % (675760)------------------------------
% 1.02/0.48 % (675760)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.02/0.48 % (675760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.02/0.48 % (675760)CaDiCaL version: 2.1.3
% 1.02/0.48 % (675760)Termination reason: Refutation not found, incomplete strategy
% 1.02/0.48 % (675760)Time elapsed: 0.004 s
% 1.02/0.48 % (675760)Peak memory usage: 11 MB
% 1.02/0.48 % (675760)Instructions burned: 4 (million)
% 1.02/0.48 % (675756)------------------------------
% 1.02/0.48 % (675756)------------------------------
% 1.02/0.48 % (675760)------------------------------
% 1.02/0.48 % (675760)------------------------------
% 1.02/0.48 % (675757)Instruction limit reached!
% 1.02/0.48 % (675757)------------------------------
% 1.02/0.48 % (675757)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.02/0.48 % (675757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.02/0.48 % (675757)CaDiCaL version: 2.1.3
% 1.02/0.48 % (675757)Termination reason: Instruction limit
% 1.02/0.48 % (675757)Termination phase: Saturation
% 1.02/0.48 % (675757)Time elapsed: 0.016 s
% 1.02/0.48 % (675757)Peak memory usage: 12 MB
% 1.02/0.48 % (675757)Instructions burned: 18 (million)
% 1.02/0.48 % (675772)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.02/0.48 % (675771)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=2095505690:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 1.02/0.54 % (675773)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=997176050:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 1.02/0.54 % (675770)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2751824985:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 1.02/0.54 % (675770)Instruction limit reached!
% 1.02/0.54 % (675770)------------------------------
% 1.02/0.54 % (675770)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.02/0.54 % (675770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.02/0.54 % (675770)CaDiCaL version: 2.1.3
% 1.02/0.54 % (675770)Termination reason: Instruction limit
% 1.02/0.54 % (675770)Termination phase: Saturation
% 1.02/0.54 % (675770)Time elapsed: 0.003 s
% 1.02/0.54 % (675770)Peak memory usage: 12 MB
% 1.02/0.54 % (675770)Instructions burned: 2 (million)
% 1.02/0.54 % (675772)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3027393564:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 1.02/0.54 % (675771)Instruction limit reached!
% 1.02/0.54 % (675771)------------------------------
% 1.02/0.54 % (675771)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.02/0.54 % (675771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.02/0.54 % (675771)CaDiCaL version: 2.1.3
% 1.02/0.54 % (675771)Termination reason: Instruction limit
% 1.02/0.54 % (675771)Termination phase: Saturation
% 1.02/0.54 % (675771)Time elapsed: 0.006 s
% 1.02/0.54 % (675771)Peak memory usage: 11 MB
% 1.02/0.54 % (675771)Instructions burned: 6 (million)
% 1.02/0.54 % (675773)Instruction limit reached!
% 1.02/0.54 % (675773)------------------------------
% 1.02/0.54 % (675773)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.02/0.54 % (675773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.02/0.54 % (675773)CaDiCaL version: 2.1.3
% 1.02/0.54 % (675773)Termination reason: Instruction limit
% 1.02/0.54 % (675773)Termination phase: Saturation
% 1.02/0.54 % (675773)Time elapsed: 0.008 s
% 1.02/0.54 % (675773)Peak memory usage: 12 MB
% 1.02/0.54 % (675773)Instructions burned: 12 (million)
% 1.02/0.54 % (675772)Instruction limit reached!
% 1.02/0.54 % (675772)------------------------------
% 1.02/0.54 % (675772)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.02/0.54 % (675772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.02/0.54 % (675772)CaDiCaL version: 2.1.3
% 1.02/0.54 % (675772)Termination reason: Instruction limit
% 1.02/0.54 % (675772)Termination phase: Saturation
% 1.02/0.54 % (675772)Time elapsed: 0.008 s
% 1.02/0.54 % (675772)Peak memory usage: 12 MB
% 1.02/0.54 % (675772)Instructions burned: 8 (million)
% 1.02/0.54 % (675762)Instruction limit reached!
% 1.02/0.54 % (675762)------------------------------
% 1.02/0.54 % (675762)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.02/0.54 % (675762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.02/0.54 % (675762)CaDiCaL version: 2.1.3
% 1.02/0.54 % (675762)Termination reason: Instruction limit
% 1.02/0.54 % (675762)Termination phase: Saturation
% 1.02/0.54 % (675762)Time elapsed: 0.079 s
% 1.02/0.54 % (675762)Peak memory usage: 12 MB
% 1.02/0.54 % (675762)Instructions burned: 158 (million)
% 1.02/0.54 % (675781)lrs+10_1_si=on:cs=on:random_seed=61341019:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 1.02/0.54 % (675761)Instruction limit reached!
% 1.02/0.54 % (675761)------------------------------
% 1.02/0.54 % (675761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.02/0.54 % (675761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.02/0.54 % (675761)CaDiCaL version: 2.1.3
% 1.02/0.54 % (675761)Termination reason: Instruction limit
% 1.02/0.54 % (675761)Termination phase: Saturation
% 1.02/0.54 % (675761)Time elapsed: 0.066 s
% 1.02/0.54 % (675761)Peak memory usage: 12 MB
% 1.02/0.54 % (675761)Instructions burned: 75 (million)
% 1.02/0.54 % (675779)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 1.02/0.54 % (675779)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.84/0.58 % (675780)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=1253659302:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 1.84/0.58 % (675779)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=995127187:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 1.84/0.58 % (675781)Instruction limit reached!
% 1.84/0.58 % (675781)------------------------------
% 1.84/0.58 % (675781)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.84/0.58 % (675781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.84/0.58 % (675781)CaDiCaL version: 2.1.3
% 1.84/0.58 % (675781)Termination reason: Instruction limit
% 1.84/0.58 % (675781)Termination phase: Saturation
% 1.84/0.58 % (675781)Time elapsed: 0.008 s
% 1.84/0.58 % (675781)Peak memory usage: 11 MB
% 1.84/0.58 % (675781)Instructions burned: 9 (million)
% 1.84/0.58 % (675780)Refutation not found, incomplete strategy
% 1.84/0.58 % (675780)------------------------------
% 1.84/0.58 % (675780)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.84/0.58 % (675780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.84/0.58 % (675780)CaDiCaL version: 2.1.3
% 1.84/0.58 % (675780)Termination reason: Refutation not found, incomplete strategy
% 1.84/0.58 % (675780)Time elapsed: 0.007 s
% 1.84/0.58 % (675780)Peak memory usage: 12 MB
% 1.84/0.58 % (675780)Instructions burned: 6 (million)
% 1.84/0.58 % (675780)------------------------------
% 1.84/0.58 % (675780)------------------------------
% 1.84/0.58 % (675782)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 1.84/0.58 % (675782)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=755328520:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 1.84/0.58 % (675787)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=1699935199:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 1.84/0.58 % (675782)Instruction limit reached!
% 1.84/0.58 % (675782)------------------------------
% 1.84/0.58 % (675782)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.84/0.58 % (675782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.84/0.58 % (675782)CaDiCaL version: 2.1.3
% 1.84/0.58 % (675782)Termination reason: Instruction limit
% 1.84/0.58 % (675782)Termination phase: Saturation
% 1.84/0.58 % (675782)Time elapsed: 0.003 s
% 1.84/0.58 % (675782)Peak memory usage: 12 MB
% 1.84/0.58 % (675782)Instructions burned: 2 (million)
% 1.84/0.58 % (675779)Instruction limit reached!
% 1.84/0.58 % (675779)------------------------------
% 1.84/0.58 % (675779)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.84/0.58 % (675779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.84/0.58 % (675779)CaDiCaL version: 2.1.3
% 1.84/0.58 % (675779)Termination reason: Instruction limit
% 1.84/0.58 % (675779)Termination phase: Saturation
% 1.84/0.58 % (675779)Time elapsed: 0.025 s
% 1.84/0.58 % (675779)Peak memory usage: 12 MB
% 1.84/0.58 % (675779)Instructions burned: 28 (million)
% 1.84/0.58 % (675786)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=1593729552:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/38Mi)
% 1.84/0.58 % (675790)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=426571567:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 1.84/0.58 % (675786)Refutation not found, incomplete strategy
% 1.84/0.58 % (675786)------------------------------
% 1.84/0.58 % (675786)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.84/0.58 % (675786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.84/0.58 % (675786)CaDiCaL version: 2.1.3
% 1.84/0.58 % (675786)Termination reason: Refutation not found, incomplete strategy
% 1.84/0.58 % (675786)Time elapsed: 0.004 s
% 1.84/0.58 % (675786)Peak memory usage: 12 MB
% 1.84/0.58 % (675786)Instructions burned: 3 (million)
% 1.84/0.58 % (675786)------------------------------
% 1.84/0.58 % (675786)------------------------------
% 2.15/0.67 % (675790)Refutation not found, incomplete strategy
% 2.15/0.67 % (675790)------------------------------
% 2.15/0.67 % (675790)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.15/0.67 % (675790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.15/0.67 % (675790)CaDiCaL version: 2.1.3
% 2.15/0.67 % (675790)Termination reason: Refutation not found, incomplete strategy
% 2.15/0.67 % (675790)Time elapsed: 0.004 s
% 2.15/0.67 % (675790)Peak memory usage: 12 MB
% 2.15/0.67 % (675790)Instructions burned: 4 (million)
% 2.15/0.67 % (675790)------------------------------
% 2.15/0.67 % (675790)------------------------------
% 2.15/0.67 % (675791)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=800848548:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 2.15/0.67 % (675791)Refutation not found, incomplete strategy
% 2.15/0.67 % (675791)------------------------------
% 2.15/0.67 % (675791)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.15/0.67 % (675791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.15/0.67 % (675791)CaDiCaL version: 2.1.3
% 2.15/0.67 % (675791)Termination reason: Refutation not found, incomplete strategy
% 2.15/0.67 % (675791)Time elapsed: 0.005 s
% 2.15/0.67 % (675791)Peak memory usage: 12 MB
% 2.15/0.67 % (675791)Instructions burned: 4 (million)
% 2.15/0.67 % (675791)------------------------------
% 2.15/0.67 % (675791)------------------------------
% 2.15/0.67 % (675794)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=2891464870:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 2.15/0.67 % (675801)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=1680799818:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 2.15/0.67 % (675801)Refutation not found, incomplete strategy
% 2.15/0.67 % (675801)------------------------------
% 2.15/0.67 % (675801)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.15/0.67 % (675801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.15/0.67 % (675801)CaDiCaL version: 2.1.3
% 2.15/0.67 % (675801)Termination reason: Refutation not found, incomplete strategy
% 2.15/0.67 % (675801)Time elapsed: 0.004 s
% 2.15/0.67 % (675801)Peak memory usage: 12 MB
% 2.15/0.67 % (675801)Instructions burned: 5 (million)
% 2.15/0.67 % (675800)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=3751008896: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)
% 2.15/0.67 % (675798)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=3281920952:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 2.15/0.67 % (675801)------------------------------
% 2.15/0.67 % (675801)------------------------------
% 2.15/0.67 % (675800)Instruction limit reached!
% 2.15/0.67 % (675800)------------------------------
% 2.15/0.67 % (675800)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.15/0.67 % (675800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.15/0.67 % (675800)CaDiCaL version: 2.1.3
% 2.15/0.67 % (675800)Termination reason: Instruction limit
% 2.15/0.68 % (675800)Termination phase: Saturation
% 2.15/0.68 % (675800)Time elapsed: 0.003 s
% 2.15/0.68 % (675800)Peak memory usage: 11 MB
% 2.15/0.68 % (675800)Instructions burned: 2 (million)
% 2.15/0.68 % (675798)Instruction limit reached!
% 2.15/0.68 % (675798)------------------------------
% 2.15/0.68 % (675798)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.15/0.68 % (675798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.15/0.68 % (675798)CaDiCaL version: 2.1.3
% 2.15/0.68 % (675798)Termination reason: Instruction limit
% 2.15/0.68 % (675798)Termination phase: Saturation
% 2.15/0.68 % (675798)Time elapsed: 0.014 s
% 2.15/0.68 % (675798)Peak memory usage: 12 MB
% 2.15/0.68 % (675798)Instructions burned: 14 (million)
% 2.15/0.68 % (675803)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=287320792:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 2.15/0.68 % (675809)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=2970563039:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 2.15/0.68 % (675809)Refutation not found, incomplete strategy
% 2.86/0.81 % (675809)------------------------------
% 2.86/0.81 % (675809)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.81 % (675809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.81 % (675809)CaDiCaL version: 2.1.3
% 2.86/0.81 % (675809)Termination reason: Refutation not found, incomplete strategy
% 2.86/0.81 % (675809)Time elapsed: 0.004 s
% 2.86/0.81 % (675809)Peak memory usage: 12 MB
% 2.86/0.81 % (675809)Instructions burned: 6 (million)
% 2.86/0.81 % (675809)------------------------------
% 2.86/0.81 % (675809)------------------------------
% 2.86/0.81 % (675810)WARNING Broken Constraint: if sine_to_age_generality_threshold(10) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 2.86/0.81 % (675810)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 2.86/0.81 % (675810)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=2779960186:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 2.86/0.81 % (675803)Instruction limit reached!
% 2.86/0.81 % (675803)------------------------------
% 2.86/0.81 % (675803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.81 % (675803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.81 % (675803)CaDiCaL version: 2.1.3
% 2.86/0.81 % (675803)Termination reason: Instruction limit
% 2.86/0.81 % (675803)Termination phase: Saturation
% 2.86/0.81 % (675803)Time elapsed: 0.022 s
% 2.86/0.81 % (675803)Peak memory usage: 12 MB
% 2.86/0.81 % (675803)Instructions burned: 23 (million)
% 2.86/0.81 % (675812)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 2.86/0.81 % (675810)Refutation not found, incomplete strategy
% 2.86/0.81 % (675810)------------------------------
% 2.86/0.81 % (675810)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.81 % (675810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.81 % (675810)CaDiCaL version: 2.1.3
% 2.86/0.81 % (675810)Termination reason: Refutation not found, incomplete strategy
% 2.86/0.81 % (675810)Time elapsed: 0.007 s
% 2.86/0.81 % (675810)Peak memory usage: 12 MB
% 2.86/0.81 % (675810)Instructions burned: 6 (million)
% 2.86/0.81 % (675810)------------------------------
% 2.86/0.81 % (675810)------------------------------
% 2.86/0.81 % (675812)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=497265250:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 2.86/0.81 % (675812)Instruction limit reached!
% 2.86/0.81 % (675812)------------------------------
% 2.86/0.81 % (675812)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.81 % (675812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.81 % (675812)CaDiCaL version: 2.1.3
% 2.86/0.81 % (675812)Termination reason: Instruction limit
% 2.86/0.81 % (675812)Termination phase: Saturation
% 2.86/0.81 % (675812)Time elapsed: 0.009 s
% 2.86/0.81 % (675812)Peak memory usage: 12 MB
% 2.86/0.81 % (675812)Instructions burned: 8 (million)
% 2.86/0.81 % (675787)Instruction limit reached!
% 2.86/0.81 % (675787)------------------------------
% 2.86/0.81 % (675787)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.81 % (675787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.81 % (675787)CaDiCaL version: 2.1.3
% 2.86/0.81 % (675787)Termination reason: Instruction limit
% 2.86/0.81 % (675787)Termination phase: Saturation
% 2.86/0.81 % (675787)Time elapsed: 0.113 s
% 2.86/0.81 % (675787)Peak memory usage: 13 MB
% 2.86/0.81 % (675787)Instructions burned: 249 (million)
% 2.86/0.81 % (675815)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=1066092467:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 2.86/0.81 % (675818)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=970672646:i=7:hud=5:bd=preordered:rtra=on:bet=on_2997 on theBenchmark for (2997ds/7Mi)
% 2.86/0.81 % (675819)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=3472203031:i=23:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/23Mi)
% 2.86/0.85 % (675818)Instruction limit reached!
% 2.86/0.85 % (675818)------------------------------
% 2.86/0.85 % (675818)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.85 % (675818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.85 % (675818)CaDiCaL version: 2.1.3
% 2.86/0.85 % (675818)Termination reason: Instruction limit
% 2.86/0.85 % (675818)Termination phase: Saturation
% 2.86/0.85 % (675818)Time elapsed: 0.007 s
% 2.86/0.85 % (675818)Peak memory usage: 12 MB
% 2.86/0.85 % (675818)Instructions burned: 7 (million)
% 2.86/0.85 % (675822)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=3490024098:i=1240:rtra=on:ixr=off_2997 on theBenchmark for (2997ds/1240Mi)
% 2.86/0.85 % (675821)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=3981197126:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2997 on theBenchmark for (2997ds/20Mi)
% 2.86/0.85 % (675815)Instruction limit reached!
% 2.86/0.85 % (675815)------------------------------
% 2.86/0.85 % (675815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.85 % (675815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.85 % (675815)CaDiCaL version: 2.1.3
% 2.86/0.85 % (675815)Termination reason: Instruction limit
% 2.86/0.85 % (675815)Termination phase: Saturation
% 2.86/0.85 % (675815)Time elapsed: 0.029 s
% 2.86/0.85 % (675815)Peak memory usage: 12 MB
% 2.86/0.85 % (675815)Instructions burned: 31 (million)
% 2.86/0.85 % (675819)Instruction limit reached!
% 2.86/0.85 % (675819)------------------------------
% 2.86/0.85 % (675819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.85 % (675819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.85 % (675819)CaDiCaL version: 2.1.3
% 2.86/0.85 % (675819)Termination reason: Instruction limit
% 2.86/0.85 % (675819)Termination phase: Saturation
% 2.86/0.85 % (675819)Time elapsed: 0.019 s
% 2.86/0.85 % (675819)Peak memory usage: 11 MB
% 2.86/0.85 % (675819)Instructions burned: 23 (million)
% 2.86/0.85 % (675827)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=2449832818:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2997 on theBenchmark for (2997ds/143Mi)
% 2.86/0.85 % (675821)Instruction limit reached!
% 2.86/0.85 % (675821)------------------------------
% 2.86/0.85 % (675821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.85 % (675821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.85 % (675821)CaDiCaL version: 2.1.3
% 2.86/0.85 % (675821)Termination reason: Instruction limit
% 2.86/0.85 % (675821)Termination phase: Saturation
% 2.86/0.85 % (675821)Time elapsed: 0.018 s
% 2.86/0.85 % (675821)Peak memory usage: 12 MB
% 2.86/0.85 % (675821)Instructions burned: 20 (million)
% 2.86/0.85 % (675830)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3910908616:i=42:hud=10:rtra=on_2997 on theBenchmark for (2997ds/42Mi)
% 2.86/0.85 % (675829)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=874153770:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/193Mi)
% 2.86/0.85 % (675832)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 2.86/0.85 % (675832)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=536437879:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2997 on theBenchmark for (2997ds/7Mi)
% 2.86/0.85 % (675832)Instruction limit reached!
% 2.86/0.85 % (675832)------------------------------
% 2.86/0.85 % (675832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.85 % (675832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.85 % (675832)CaDiCaL version: 2.1.3
% 2.86/0.85 % (675832)Termination reason: Instruction limit
% 2.86/0.85 % (675832)Termination phase: Saturation
% 2.86/0.85 % (675832)Time elapsed: 0.007 s
% 2.86/0.85 % (675832)Peak memory usage: 12 MB
% 2.86/0.85 % (675832)Instructions burned: 7 (million)
% 2.86/0.85 % (675830)Instruction limit reached!
% 2.86/0.85 % (675830)------------------------------
% 2.86/0.85 % (675830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.85 % (675830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.54/0.91 % (675830)CaDiCaL version: 2.1.3
% 3.54/0.91 % (675830)Termination reason: Instruction limit
% 3.54/0.91 % (675830)Termination phase: Saturation
% 3.54/0.91 % (675830)Time elapsed: 0.038 s
% 3.54/0.91 % (675830)Peak memory usage: 12 MB
% 3.54/0.91 % (675830)Instructions burned: 43 (million)
% 3.54/0.91 % (675836)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=4017757108:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/181Mi)
% 3.54/0.91 % (675837)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=995091613:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2996 on theBenchmark for (2996ds/169Mi)
% 3.54/0.91 % (675837)Refutation not found, incomplete strategy
% 3.54/0.91 % (675837)------------------------------
% 3.54/0.91 % (675837)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.54/0.91 % (675837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.54/0.91 % (675837)CaDiCaL version: 2.1.3
% 3.54/0.91 % (675837)Termination reason: Refutation not found, incomplete strategy
% 3.54/0.91 % (675837)Time elapsed: 0.004 s
% 3.54/0.91 % (675837)Peak memory usage: 12 MB
% 3.54/0.91 % (675837)Instructions burned: 3 (million)
% 3.54/0.91 % (675837)------------------------------
% 3.54/0.91 % (675837)------------------------------
% 3.54/0.91 % (675827)Instruction limit reached!
% 3.54/0.91 % (675827)------------------------------
% 3.54/0.91 % (675827)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.54/0.91 % (675827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.54/0.91 % (675827)CaDiCaL version: 2.1.3
% 3.54/0.91 % (675827)Termination reason: Instruction limit
% 3.54/0.91 % (675827)Termination phase: Saturation
% 3.54/0.91 % (675827)Time elapsed: 0.110 s
% 3.54/0.91 % (675827)Peak memory usage: 13 MB
% 3.54/0.91 % (675827)Instructions burned: 144 (million)
% 3.54/0.91 % (675843)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 3.54/0.91 % (675843)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=83577785:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2996 on theBenchmark for (2996ds/6Mi)
% 3.54/0.92 % (675843)Instruction limit reached!
% 3.54/0.92 % (675843)------------------------------
% 3.54/0.92 % (675843)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.54/0.92 % (675843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.54/0.92 % (675843)CaDiCaL version: 2.1.3
% 3.54/0.92 % (675843)Termination reason: Instruction limit
% 3.54/0.92 % (675843)Termination phase: Saturation
% 3.54/0.92 % (675843)Time elapsed: 0.006 s
% 3.54/0.92 % (675843)Peak memory usage: 12 MB
% 3.54/0.92 % (675843)Instructions burned: 6 (million)
% 3.54/0.92 % (675844)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=1359906651:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2996 on theBenchmark for (2996ds/22Mi)
% 3.54/0.92 % (675844)Instruction limit reached!
% 3.54/0.92 % (675844)------------------------------
% 3.54/0.92 % (675844)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.54/0.92 % (675844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.54/0.92 % (675844)CaDiCaL version: 2.1.3
% 3.54/0.92 % (675844)Termination reason: Instruction limit
% 3.54/0.92 % (675844)Termination phase: Saturation
% 3.54/0.92 % (675844)Time elapsed: 0.020 s
% 3.54/0.92 % (675844)Peak memory usage: 12 MB
% 3.54/0.92 % (675844)Instructions burned: 22 (million)
% 3.54/0.92 % (675847)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=1602823675:i=19:add=on:rtra=on_2995 on theBenchmark for (2995ds/19Mi)
% 3.54/0.92 % (675794)Instruction limit reached!
% 3.54/0.92 % (675794)------------------------------
% 3.54/0.92 % (675794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.54/0.92 % (675794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.54/0.92 % (675794)CaDiCaL version: 2.1.3
% 3.54/0.92 % (675794)Termination reason: Instruction limit
% 3.54/0.92 % (675794)Termination phase: Saturation
% 3.54/0.92 % (675794)Time elapsed: 0.292 s
% 3.54/0.92 % (675794)Peak memory usage: 14 MB
% 3.54/0.92 % (675794)Instructions burned: 327 (million)
% 3.54/0.92 % (675849)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=2038838126:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/316Mi)
% 3.54/0.92 % (675847)Instruction limit reached!
% 3.54/0.92 % (675847)------------------------------
% 3.54/0.92 % (675847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.54/0.92 % (675847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.54/0.92 % (675847)CaDiCaL version: 2.1.3
% 3.54/0.92 % (675847)Termination reason: Instruction limit
% 3.54/0.92 % (675847)Termination phase: Saturation
% 3.54/0.92 % (675847)Time elapsed: 0.018 s
% 3.54/0.92 % (675847)Peak memory usage: 12 MB
% 3.54/0.92 % (675847)Instructions burned: 19 (million)
% 3.54/0.92 % (675829)Instruction limit reached!
% 3.54/0.92 % (675829)------------------------------
% 3.54/0.92 % (675829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.54/0.92 % (675829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.54/0.92 % (675829)CaDiCaL version: 2.1.3
% 3.54/0.92 % (675829)Termination reason: Instruction limit
% 3.54/0.92 % (675829)Termination phase: Saturation
% 3.54/0.92 % (675829)Time elapsed: 0.173 s
% 3.54/0.92 % (675829)Peak memory usage: 13 MB
% 3.54/0.92 % (675829)Instructions burned: 193 (million)
% 3.54/0.92 % (675849)Refutation not found, incomplete strategy
% 3.54/0.92 % (675849)------------------------------
% 3.54/0.92 % (675849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.54/0.92 % (675849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.54/0.92 % (675849)CaDiCaL version: 2.1.3
% 3.54/0.92 % (675849)Termination reason: Refutation not found, incomplete strategy
% 3.54/0.92 % (675849)Time elapsed: 0.008 s
% 3.54/0.92 % (675849)Peak memory usage: 12 MB
% 3.54/0.92 % (675849)Instructions burned: 6 (million)
% 3.54/0.92 % (675849)------------------------------
% 3.54/0.92 % (675849)------------------------------
% 3.54/0.92 % (675851)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=1455034262:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2995 on theBenchmark for (2995ds/853Mi)
% 3.54/0.92 % (675855)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=1610512664:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2995 on theBenchmark for (2995ds/21Mi)
% 3.54/0.92 % (675853)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=3403605063:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2995 on theBenchmark for (2995ds/45Mi)
% 3.54/0.92 % (675759)Instruction limit reached!
% 3.54/0.92 % (675759)------------------------------
% 3.54/0.92 % (675759)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.54/0.92 % (675759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.54/0.92 % (675759)CaDiCaL version: 2.1.3
% 3.54/0.92 % (675759)Termination reason: Instruction limit
% 3.54/0.92 % (675759)Termination phase: Saturation
% 3.54/0.92 % (675759)Time elapsed: 0.473 s
% 3.54/0.92 % (675759)Peak memory usage: 13 MB
% 3.54/0.92 % (675759)Instructions burned: 634 (million)
% 3.54/0.92 % (675836)Instruction limit reached!
% 3.54/0.92 % (675836)------------------------------
% 3.54/0.92 % (675836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.54/0.92 % (675836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.54/0.92 % (675836)CaDiCaL version: 2.1.3
% 3.54/0.92 % (675836)Termination reason: Instruction limit
% 3.54/0.92 % (675836)Termination phase: Saturation
% 3.54/0.92 % (675836)Time elapsed: 0.156 s
% 3.54/0.92 % (675836)Peak memory usage: 12 MB
% 3.54/0.92 % (675836)Instructions burned: 181 (million)
% 3.54/0.92 % (675854)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=3075261666:i=480:rtra=on_2995 on theBenchmark for (2995ds/480Mi)
% 3.54/0.92 % (675853)Refutation not found, incomplete strategy
% 3.54/0.92 % (675853)------------------------------
% 3.54/0.92 % (675853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.54/0.92 % (675853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.54/0.92 % (675853)CaDiCaL version: 2.1.3
% 3.54/0.92 % (675853)Termination reason: Refutation not found, incomplete strategy
% 3.54/0.92 % (675853)Time elapsed: 0.006 s
% 3.54/0.92 % (675853)Peak memory usage: 12 MB
% 3.54/0.92 % (675853)Instructions burned: 5 (million)
% 3.54/0.92 % (675855)Instruction limit reached!
% 3.54/0.92 % (675855)------------------------------
% 3.54/0.92 % (675855)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.54/0.92 % (675855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.54/0.92 % (675855)CaDiCaL version: 2.1.3
% 3.54/0.92 % (675855)Termination reason: Instruction limit
% 3.54/0.92 % (675855)Termination phase: Saturation
% 3.54/0.92 % (675855)Time elapsed: 0.013 s
% 3.54/0.92 % (675855)Peak memory usage: 12 MB
% 3.54/0.92 % (675855)Instructions burned: 22 (million)
% 3.54/0.92 % (675853)------------------------------
% 3.54/0.92 % (675853)------------------------------
% 3.54/0.92 % (675859)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 3.54/0.92 % (675859)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=3410198412:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/200Mi)
% 3.54/0.92 % (675861)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=3802755583:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2994 on theBenchmark for (2994ds/13Mi)
% 3.54/0.92 % (675863)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=1180228263:i=51:fsr=off:rtra=on_2994 on theBenchmark for (2994ds/51Mi)
% 3.54/0.92 % (675862)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=3915948354:i=66:s2at=3:nm=2:rtra=on:rawr=on_2994 on theBenchmark for (2994ds/66Mi)
% 3.54/0.92 % (675861)Instruction limit reached!
% 3.54/0.92 % (675861)------------------------------
% 3.54/0.92 % (675861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.54/0.92 % (675861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.54/0.92 % (675861)CaDiCaL version: 2.1.3
% 3.54/0.92 % (675861)Termination reason: Instruction limit
% 3.54/0.92 % (675861)Termination phase: Saturation
% 3.54/0.92 % (675861)Time elapsed: 0.013 s
% 3.54/0.92 % (675861)Peak memory usage: 12 MB
% 3.54/0.92 % (675861)Instructions burned: 13 (million)
% 3.54/0.92 % (675863) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-675751-675863"...
% 3.54/0.92 % (675863)...printing done.
% 3.54/0.92 % (675863)Refutation found. Thanks to Tanya!
% 3.54/0.92 % SZS status Theorem for theBenchmark
% 3.54/0.92 % SZS output start Proof for theBenchmark
% 3.54/0.92 thf(type_def_5, type, num: $tType).
% 3.54/0.92 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 3.54/0.92 thf(func_def_0, type, holdsDuring_THFTYPE_IiooI: ($i > $o > $o)).
% 3.54/0.92 thf(func_def_7, type, lYearFn_THFTYPE_IiiI: ($i > $i)).
% 3.54/0.92 thf(func_def_8, type, likes_THFTYPE_IiioI: ($i > $i > $o)).
% 3.54/0.92 thf(func_def_10, type, parent_THFTYPE_IiioI: ($i > $i > $o)).
% 3.54/0.92 thf(func_def_12, type, vNOT: ($o > $o)).
% 3.54/0.92 thf(func_def_15, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 3.54/0.92 thf(func_def_16, type, db1: !>[X0: $tType]:(X0)).
% 3.54/0.92 thf(func_def_17, type, db0: !>[X0: $tType]:(X0)).
% 3.54/0.92 thf(func_def_18, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 3.54/0.92 thf(func_def_19, type, vAND: ($o > $o > $o)).
% 3.54/0.92 thf(func_def_20, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 3.54/0.92 thf(f1,axiom,(
% 3.54/0.92 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lAnna_THFTYPE_i))),
% 3.54/0.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax)).
% 3.54/0.92 thf(f2,axiom,(
% 3.54/0.92 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ? [X1 : $i,X0 : $i] : (~ (parent_THFTYPE_IiioI @ X0 @ X1)))),
% 3.54/0.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_001)).
% 3.54/0.92 thf(f6,axiom,(
% 3.54/0.92 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ? [X1 : $i,X0 : $i] : (~ (likes_THFTYPE_IiioI @ X0 @ X1)))),
% 3.54/0.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_005)).
% 3.54/0.92 thf(f7,axiom,(
% 3.54/0.92 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i))),
% 3.54/0.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_006)).
% 3.54/0.92 thf(f10,conjecture,(
% 3.54/0.92 ? [X2 : $i,X1 : ($i > $i > $o),X0 : ($i > $i > $o)] : (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (X1 @ X2 @ lBill_THFTYPE_i) & (~ ((^[X3 : $i, X4 : $i] : ($true)) = X1)) & (X0 @ X2 @ lAnna_THFTYPE_i) & (~ (X0 = (^[X3 : $i, X4 : $i] : ($true)))))),
% 3.54/0.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',con)).
% 3.54/0.92 thf(f11,negated_conjecture,(
% 3.54/0.92 ~ ? [X2 : $i,X1 : ($i > $i > $o),X0 : ($i > $i > $o)] : (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (X1 @ X2 @ lBill_THFTYPE_i) & (~ ((^[X3 : $i, X4 : $i] : ($true)) = X1)) & (X0 @ X2 @ lAnna_THFTYPE_i) & (~ (X0 = (^[X3 : $i, X4 : $i] : ($true)))))),
% 3.54/0.92 inference(negated_conjecture,[status(cth)],[f10])).
% 3.54/0.92 thf(f14,plain,(
% 3.54/0.92 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i))),
% 3.54/0.92 inference(rectify,[],[f7])).
% 3.54/0.92 thf(f15,plain,(
% 3.54/0.92 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i))) = $true)),
% 3.54/0.92 inference(fool_elimination,[],[f14])).
% 3.54/0.92 thf(f16,plain,(
% 3.54/0.92 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lAnna_THFTYPE_i))),
% 3.54/0.92 inference(rectify,[],[f1])).
% 3.54/0.92 thf(f17,plain,(
% 3.54/0.92 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lAnna_THFTYPE_i))) = $true)),
% 3.54/0.92 inference(fool_elimination,[],[f16])).
% 3.54/0.92 thf(f20,plain,(
% 3.54/0.92 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ? [X0 : $i,X1 : $i] : (~ (likes_THFTYPE_IiioI @ X1 @ X0)))),
% 3.54/0.92 inference(rectify,[],[f6])).
% 3.54/0.92 thf(f21,plain,(
% 3.54/0.92 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (?? @ $i @ (^[Y0 : $i]: (?? @ $i @ (^[Y1 : $i]: (~ (likes_THFTYPE_IiioI @ Y0 @ Y1)))))))) = $true)),
% 3.54/0.92 inference(fool_elimination,[],[f20])).
% 3.54/0.92 thf(f22,plain,(
% 3.54/0.92 ~ ? [X0 : $i,X1 : ($i > $i > $o),X2 : ($i > $i > $o)] : (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (X1 @ X0 @ lBill_THFTYPE_i) & (~ ((^[X3 : $i, X4 : $i] : ($true)) = X1)) & (X2 @ X0 @ lAnna_THFTYPE_i) & (~ (X2 = (^[X5 : $i, X6 : $i] : ($true)))))),
% 3.54/0.92 inference(rectify,[],[f11])).
% 3.54/0.92 thf(f23,plain,(
% 3.54/0.92 ~ ? [X0 : $i,X2 : ($i > $i > $o),X1 : ($i > $i > $o)] : (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ((((~ (X2 = (^[Y0 : $i]: ((^[Y1 : $i]: ($true)))))) & (X2 @ X0 @ lAnna_THFTYPE_i)) & (~ ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X1))) & (X1 @ X0 @ lBill_THFTYPE_i)))) = $true)),
% 3.54/0.92 inference(fool_elimination,[],[f22])).
% 3.54/0.92 thf(f28,plain,(
% 3.54/0.92 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ? [X0 : $i,X1 : $i] : (~ (parent_THFTYPE_IiioI @ X1 @ X0)))),
% 3.54/0.92 inference(rectify,[],[f2])).
% 3.54/0.92 thf(f29,plain,(
% 3.54/0.92 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (?? @ $i @ (^[Y0 : $i]: (?? @ $i @ (^[Y1 : $i]: (~ (parent_THFTYPE_IiioI @ Y0 @ Y1)))))))) = $true)),
% 3.54/0.92 inference(fool_elimination,[],[f28])).
% 3.54/0.92 thf(f32,plain,(
% 3.54/0.92 ! [X2 : ($i > $i > $o),X0 : $i,X1 : ($i > $i > $o)] : (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ((((~ (X2 = (^[Y0 : $i]: ((^[Y1 : $i]: ($true)))))) & (X2 @ X0 @ lAnna_THFTYPE_i)) & (~ ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X1))) & (X1 @ X0 @ lBill_THFTYPE_i)))) != $true)),
% 3.54/0.92 inference(ennf_transformation,[],[f23])).
% 3.54/0.92 thf(f33,plain,(
% 3.54/0.92 ! [X0 : ($i > $i > $o),X1 : $i,X2 : ($i > $i > $o)] : ($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ((((~ (X0 = (^[Y0 : $i]: ((^[Y1 : $i]: ($true)))))) & (X0 @ X1 @ lAnna_THFTYPE_i)) & (~ ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X2))) & (X2 @ X1 @ lBill_THFTYPE_i)))))),
% 3.54/0.92 inference(rectify,[],[f32])).
% 3.54/0.92 thf(f35,plain,(
% 3.54/0.92 ( ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o),X1 : $i] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ((((~ (X0 = (^[Y0 : $i]: ((^[Y1 : $i]: ($true)))))) & (X0 @ X1 @ lAnna_THFTYPE_i)) & (~ ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X2))) & (X2 @ X1 @ lBill_THFTYPE_i)))))) )),
% 3.54/0.92 inference(cnf_transformation,[],[f33])).
% 3.54/0.92 thf(f36,plain,(
% 3.54/0.92 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (?? @ $i @ (^[Y0 : $i]: (?? @ $i @ (^[Y1 : $i]: (~ (likes_THFTYPE_IiioI @ Y0 @ Y1)))))))) = $true)),
% 3.54/0.92 inference(cnf_transformation,[],[f21])).
% 3.54/0.92 thf(f37,plain,(
% 3.54/0.92 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lAnna_THFTYPE_i))) = $true)),
% 3.54/0.92 inference(cnf_transformation,[],[f17])).
% 3.54/0.92 thf(f39,plain,(
% 3.54/0.92 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (?? @ $i @ (^[Y0 : $i]: (?? @ $i @ (^[Y1 : $i]: (~ (parent_THFTYPE_IiioI @ Y0 @ Y1)))))))) = $true)),
% 3.54/0.92 inference(cnf_transformation,[],[f29])).
% 3.54/0.92 thf(f41,plain,(
% 3.54/0.92 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i))) = $true)),
% 3.54/0.92 inference(cnf_transformation,[],[f15])).
% 3.54/0.92 thf(f45,definition,(
% 3.54/0.92 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 3.54/0.92 introduced(theory,[fool_exhaustiveness_axiom])).
% 3.54/0.92 thf(f62,plain,(
% 3.54/0.92 ( ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o),X1 : $i] : (((((((~ (X0 = (^[Y0 : $i]: ((^[Y1 : $i]: ($true)))))) & (X0 @ X1 @ lAnna_THFTYPE_i)) & (~ ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X2))) & (X2 @ X1 @ lBill_THFTYPE_i))) = $true) | ($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false)))) )),
% 3.54/0.92 inference(superposition,[],[f35,f45])).
% 3.54/0.92 thf(f63,plain,(
% 3.54/0.92 ( ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o),X1 : $i] : (((((((~ (X0 = (^[Y0 : $i]: ((^[Y1 : $i]: ($true)))))) & (X0 @ X1 @ lAnna_THFTYPE_i)) & (~ ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X2))) & (X2 @ X1 @ lBill_THFTYPE_i))) = $false) | (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true)) != $true)) )),
% 3.54/0.92 inference(superposition,[],[f35,f45])).
% 3.54/0.92 thf(f89,plain,(
% 3.54/0.92 ( ! [X2 : ($i > $i > $o),X1 : $i] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false))) | (((X2 @ X1 @ lBill_THFTYPE_i)) = $true)) )),
% 3.54/0.92 inference(and_proxy_clausification,[],[f62])).
% 3.54/0.92 thf(f129,plain,(
% 3.54/0.92 ( ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o),X1 : $i] : (($false = ((((~ (X0 = (^[Y0 : $i]: ((^[Y1 : $i]: ($true)))))) & (X0 @ X1 @ lAnna_THFTYPE_i)) & (~ ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X2))))) | (((X2 @ X1 @ lBill_THFTYPE_i)) = $false) | (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true)) != $true)) )),
% 3.54/0.92 inference(and_proxy_clausification,[],[f63])).
% 3.54/0.92 thf(f130,plain,(
% 3.54/0.92 ( ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o),X1 : $i] : ((((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true)) != $true) | ($false = ((~ ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X2)))) | ((((~ (X0 = (^[Y0 : $i]: ((^[Y1 : $i]: ($true)))))) & (X0 @ X1 @ lAnna_THFTYPE_i))) = $false) | (((X2 @ X1 @ lBill_THFTYPE_i)) = $false)) )),
% 3.54/0.92 inference(and_proxy_clausification,[],[f129])).
% 3.54/0.92 thf(f131,plain,(
% 3.54/0.92 ( ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o),X1 : $i] : (((((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X2)) = $true) | (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true)) != $true) | (((X2 @ X1 @ lBill_THFTYPE_i)) = $false) | ((((~ (X0 = (^[Y0 : $i]: ((^[Y1 : $i]: ($true)))))) & (X0 @ X1 @ lAnna_THFTYPE_i))) = $false)) )),
% 3.54/0.92 inference(not_proxy_clausification,[],[f130])).
% 3.54/0.92 thf(f132,plain,(
% 3.54/0.92 ( ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o),X1 : $i] : (((((~ (X0 = (^[Y0 : $i]: ((^[Y1 : $i]: ($true)))))) & (X0 @ X1 @ lAnna_THFTYPE_i))) = $false) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X2) | (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true)) != $true) | (((X2 @ X1 @ lBill_THFTYPE_i)) = $false)) )),
% 3.54/0.92 inference(equality_proxy_clausification,[],[f131])).
% 3.54/0.92 thf(f133,plain,(
% 3.54/0.92 ( ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o),X1 : $i] : ((((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true)) != $true) | (((X2 @ X1 @ lBill_THFTYPE_i)) = $false) | (((~ (X0 = (^[Y0 : $i]: ((^[Y1 : $i]: ($true))))))) = $false) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X2) | (((X0 @ X1 @ lAnna_THFTYPE_i)) = $false)) )),
% 3.54/0.92 inference(and_proxy_clausification,[],[f132])).
% 3.54/0.92 thf(f134,plain,(
% 3.54/0.92 ( ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o),X1 : $i] : ((((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true)) != $true) | (((X0 @ X1 @ lAnna_THFTYPE_i)) = $false) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X2) | (((X0 = (^[Y0 : $i]: ((^[Y1 : $i]: ($true)))))) = $true) | (((X2 @ X1 @ lBill_THFTYPE_i)) = $false)) )),
% 3.54/0.92 inference(not_proxy_clausification,[],[f133])).
% 3.54/0.92 thf(f135,plain,(
% 3.54/0.92 ( ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o),X1 : $i] : (((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X2) | (((X0 @ X1 @ lAnna_THFTYPE_i)) = $false) | (((X2 @ X1 @ lBill_THFTYPE_i)) = $false) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X0) | (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true)) != $true)) )),
% 3.54/0.92 inference(equality_proxy_clausification,[],[f134])).
% 3.54/0.92 thf(f154,definition,(
% 3.54/0.92 spl0_2 <=> ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false)))),
% 3.54/0.92 introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition])).
% 3.54/0.92 thf(f156,plain,(
% 3.54/0.92 ($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false))) | spl0_2),
% 3.54/0.92 inference(avatar_component_clause,[],[f154])).
% 3.54/0.92 thf(f159,definition,(
% 3.54/0.92 spl0_3 <=> ! [X2 : ($i > $i > $o),X1 : $i] : (((X2 @ X1 @ lBill_THFTYPE_i)) = $true)),
% 3.54/0.92 introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition])).
% 3.54/0.92 thf(f160,plain,(
% 3.54/0.92 ( ! [X2 : ($i > $i > $o),X1 : $i] : ((((X2 @ X1 @ lBill_THFTYPE_i)) = $true)) ) | ~spl0_3),
% 3.54/0.92 inference(avatar_component_clause,[],[f159])).
% 3.54/0.92 thf(f170,plain,(
% 3.54/0.92 ~spl0_2 | spl0_3),
% 3.54/0.92 inference(avatar_split_clause,[],[f89,f159,f154])).
% 3.54/0.92 thf(f178,definition,(
% 3.54/0.92 spl0_5 <=> (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true)) = $true)),
% 3.54/0.92 introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition])).
% 3.54/0.92 thf(f182,definition,(
% 3.54/0.92 spl0_6 <=> ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o),X1 : $i] : (((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X2) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X0) | (((X2 @ X1 @ lBill_THFTYPE_i)) = $false) | (((X0 @ X1 @ lAnna_THFTYPE_i)) = $false))),
% 3.54/0.92 introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition])).
% 3.54/0.92 thf(f183,plain,(
% 3.54/0.92 ( ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o),X1 : $i] : ((((X2 @ X1 @ lBill_THFTYPE_i)) = $false) | (((X0 @ X1 @ lAnna_THFTYPE_i)) = $false) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X2) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X0)) ) | ~spl0_6),
% 3.54/0.92 inference(avatar_component_clause,[],[f182])).
% 3.54/0.92 thf(f184,plain,(
% 3.54/0.92 ~spl0_5 | spl0_6),
% 3.54/0.92 inference(avatar_split_clause,[],[f135,f182,f178])).
% 3.54/0.92 thf(f186,plain,(
% 3.54/0.92 ( ! [X0 : $o] : ((((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ X0)) != $true) | ($true = X0)) ) | spl0_2),
% 3.54/0.92 inference(superposition,[],[f156,f45])).
% 3.54/0.92 thf(f188,plain,(
% 3.54/0.92 ($false = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false))) | ($true != $true) | spl0_2),
% 3.54/0.92 inference(superposition,[],[f156,f45])).
% 3.54/0.92 thf(f189,plain,(
% 3.54/0.92 ($false = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false))) | spl0_2),
% 3.54/0.92 inference(trivial_inequality_removal,[],[f188])).
% 3.54/0.92 thf(f197,plain,(
% 3.54/0.92 ( ! [X0 : $o] : (($true = X0) | (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ X0)) = X0)) ) | spl0_2),
% 3.54/0.92 inference(superposition,[],[f189,f45])).
% 3.54/0.92 thf(f202,plain,(
% 3.54/0.92 ( ! [X0 : $o] : (($true = X0) | ($true = X0) | (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ X0)) = $false)) ) | spl0_2),
% 3.54/0.92 inference(iff_proxy_clausification,[],[f197])).
% 3.54/0.92 thf(f203,plain,(
% 3.54/0.92 ( ! [X0 : $o] : ((((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ X0)) = $false) | ($true = X0)) ) | spl0_2),
% 3.54/0.92 inference(duplicate_literal_removal,[],[f202])).
% 3.54/0.92 thf(f211,plain,(
% 3.54/0.92 ($true != $true) | (((parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lAnna_THFTYPE_i)) = $true) | spl0_2),
% 3.54/0.92 inference(superposition,[],[f186,f37])).
% 3.54/0.92 thf(f220,plain,(
% 3.54/0.92 (((parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lAnna_THFTYPE_i)) = $true) | spl0_2),
% 3.54/0.92 inference(trivial_inequality_removal,[],[f211])).
% 3.54/0.92 thf(f241,plain,(
% 3.54/0.92 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true)) = $true) | spl0_2),
% 3.54/0.92 inference(superposition,[],[f37,f220])).
% 3.54/0.92 thf(f248,plain,(
% 3.54/0.92 spl0_5 | spl0_2),
% 3.54/0.92 inference(avatar_split_clause,[],[f241,f154,f178])).
% 3.54/0.92 thf(f306,plain,(
% 3.54/0.92 (((?? @ $i @ (^[Y0 : $i]: (?? @ $i @ (^[Y1 : $i]: (~ (parent_THFTYPE_IiioI @ Y0 @ Y1))))))) = $true) | ($true = $false) | spl0_2),
% 3.54/0.92 inference(superposition,[],[f203,f39])).
% 3.54/0.92 thf(f319,plain,(
% 3.54/0.92 ($true = ((?? @ $i @ (^[Y0 : $i]: (?? @ $i @ (^[Y1 : $i]: (~ (likes_THFTYPE_IiioI @ Y0 @ Y1)))))))) | ($true = $false) | spl0_2),
% 3.54/0.92 inference(superposition,[],[f36,f203])).
% 3.54/0.92 thf(f324,plain,(
% 3.54/0.92 ($true = (((^[Y0 : $i]: (?? @ $i @ (^[Y1 : $i]: (~ (likes_THFTYPE_IiioI @ Y0 @ Y1))))) @ sK5))) | ($true = $false) | spl0_2),
% 3.54/0.92 inference(sigma_proxy_clausification,[],[f319])).
% 3.54/0.92 thf(f325,plain,(
% 3.54/0.92 ($true = (((^[Y0 : $i]: (?? @ $i @ (^[Y1 : $i]: (~ (likes_THFTYPE_IiioI @ Y0 @ Y1))))) @ sK5))) | spl0_2),
% 3.54/0.92 inference(trivial_inequality_removal,[],[f324])).
% 3.54/0.92 thf(f326,plain,(
% 3.54/0.92 ($true = ((?? @ $i @ (^[Y0 : $i]: (~ (likes_THFTYPE_IiioI @ sK5 @ Y0)))))) | spl0_2),
% 3.54/0.92 inference(beta-eta_normalization,[],[f325])).
% 3.54/0.92 thf(f327,plain,(
% 3.54/0.92 ((((^[Y0 : $i]: (~ (likes_THFTYPE_IiioI @ sK5 @ Y0))) @ sK6)) = $true) | spl0_2),
% 3.54/0.92 inference(sigma_proxy_clausification,[],[f326])).
% 3.54/0.92 thf(f328,plain,(
% 3.54/0.92 (((~ (likes_THFTYPE_IiioI @ sK5 @ sK6))) = $true) | spl0_2),
% 3.54/0.92 inference(beta-eta_normalization,[],[f327])).
% 3.54/0.92 thf(f329,plain,(
% 3.54/0.92 (((likes_THFTYPE_IiioI @ sK5 @ sK6)) = $false) | spl0_2),
% 3.54/0.92 inference(not_proxy_clausification,[],[f328])).
% 3.54/0.92 thf(f341,plain,(
% 3.54/0.92 ($true = $false) | ((((^[Y0 : $i]: (?? @ $i @ (^[Y1 : $i]: (~ (parent_THFTYPE_IiioI @ Y0 @ Y1))))) @ sK9)) = $true) | spl0_2),
% 3.54/0.92 inference(sigma_proxy_clausification,[],[f306])).
% 3.54/0.92 thf(f342,plain,(
% 3.54/0.92 ((((^[Y0 : $i]: (?? @ $i @ (^[Y1 : $i]: (~ (parent_THFTYPE_IiioI @ Y0 @ Y1))))) @ sK9)) = $true) | spl0_2),
% 3.54/0.92 inference(trivial_inequality_removal,[],[f341])).
% 3.54/0.92 thf(f343,plain,(
% 3.54/0.92 ($true = ((?? @ $i @ (^[Y0 : $i]: (~ (parent_THFTYPE_IiioI @ sK9 @ Y0)))))) | spl0_2),
% 3.54/0.92 inference(beta-eta_normalization,[],[f342])).
% 3.54/0.92 thf(f344,plain,(
% 3.54/0.92 ($true = (((^[Y0 : $i]: (~ (parent_THFTYPE_IiioI @ sK9 @ Y0))) @ sK10))) | spl0_2),
% 3.54/0.92 inference(sigma_proxy_clausification,[],[f343])).
% 3.54/0.92 thf(f345,plain,(
% 3.54/0.92 (((~ (parent_THFTYPE_IiioI @ sK9 @ sK10))) = $true) | spl0_2),
% 3.54/0.92 inference(beta-eta_normalization,[],[f344])).
% 3.54/0.92 thf(f346,plain,(
% 3.54/0.92 (((parent_THFTYPE_IiioI @ sK9 @ sK10)) = $false) | spl0_2),
% 3.54/0.92 inference(not_proxy_clausification,[],[f345])).
% 3.54/0.92 thf(f395,plain,(
% 3.54/0.92 ( ! [X0 : ($i > $i > $o)] : (((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X0) | ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false))) | (((X0 @ lMary_THFTYPE_i @ lAnna_THFTYPE_i)) = $false) | (likes_THFTYPE_IiioI = (^[Y0 : $i]: ((^[Y1 : $i]: ($true)))))) ) | ~spl0_6),
% 3.54/0.92 inference(superposition,[],[f41,f183])).
% 3.54/0.92 thf(f425,definition,(
% 3.54/0.92 spl0_9 <=> ! [X0 : ($i > $i > $o)] : ((((X0 @ lMary_THFTYPE_i @ lAnna_THFTYPE_i)) = $false) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X0))),
% 3.54/0.92 introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition])).
% 3.54/0.92 thf(f426,plain,(
% 3.54/0.92 ( ! [X0 : ($i > $i > $o)] : ((((X0 @ lMary_THFTYPE_i @ lAnna_THFTYPE_i)) = $false) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X0)) ) | ~spl0_9),
% 3.54/0.92 inference(avatar_component_clause,[],[f425])).
% 3.54/0.92 thf(f428,definition,(
% 3.54/0.92 spl0_10 <=> (likes_THFTYPE_IiioI = (^[Y0 : $i]: ((^[Y1 : $i]: ($true)))))),
% 3.54/0.92 introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition])).
% 3.54/0.92 thf(f430,plain,(
% 3.54/0.92 (likes_THFTYPE_IiioI = (^[Y0 : $i]: ((^[Y1 : $i]: ($true))))) | ~spl0_10),
% 3.54/0.92 inference(avatar_component_clause,[],[f428])).
% 3.54/0.92 thf(f451,plain,(
% 3.54/0.92 ( ! [X0 : ($i > $i > $o)] : (($true = $false) | (likes_THFTYPE_IiioI = (^[Y0 : $i]: ((^[Y1 : $i]: ($true))))) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X0) | (((X0 @ lMary_THFTYPE_i @ lAnna_THFTYPE_i)) = $false)) ) | (spl0_2 | ~spl0_6)),
% 3.54/0.92 inference(forward_demodulation,[],[f395,f189])).
% 3.54/0.92 thf(f452,plain,(
% 3.54/0.92 ( ! [X0 : ($i > $i > $o)] : (((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X0) | (likes_THFTYPE_IiioI = (^[Y0 : $i]: ((^[Y1 : $i]: ($true))))) | (((X0 @ lMary_THFTYPE_i @ lAnna_THFTYPE_i)) = $false)) ) | (spl0_2 | ~spl0_6)),
% 3.54/0.92 inference(trivial_inequality_removal,[],[f451])).
% 3.54/0.92 thf(f457,plain,(
% 3.54/0.92 spl0_10 | spl0_9 | spl0_2 | ~spl0_6),
% 3.54/0.92 inference(avatar_split_clause,[],[f452,f182,f154,f425,f428])).
% 3.54/0.92 thf(f460,plain,(
% 3.54/0.92 ( ! [X1 : $i] : (((((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) @ X1)) = ((likes_THFTYPE_IiioI @ X1)))) ) | ~spl0_10),
% 3.54/0.92 inference(argument_congruence,[],[f430])).
% 3.54/0.92 thf(f461,plain,(
% 3.54/0.92 ( ! [X1 : $i] : (((^[Y0 : $i]: ($true)) = ((likes_THFTYPE_IiioI @ X1)))) ) | ~spl0_10),
% 3.54/0.92 inference(beta-eta_normalization,[],[f460])).
% 3.54/0.92 thf(f462,plain,(
% 3.54/0.92 ( ! [X2 : $i,X1 : $i] : ((((likes_THFTYPE_IiioI @ X1 @ X2)) = (((^[Y0 : $i]: ($true)) @ X2)))) ) | ~spl0_10),
% 3.54/0.92 inference(argument_congruence,[],[f461])).
% 3.54/0.92 thf(f463,plain,(
% 3.54/0.92 ( ! [X2 : $i,X1 : $i] : ((((likes_THFTYPE_IiioI @ X1 @ X2)) = $true) | ($false = (((^[Y0 : $i]: ($true)) @ X2)))) ) | ~spl0_10),
% 3.54/0.92 inference(iff_proxy_clausification,[],[f462])).
% 3.54/0.92 thf(f466,plain,(
% 3.54/0.92 ( ! [X2 : $i,X1 : $i] : (($true = $false) | (((likes_THFTYPE_IiioI @ X1 @ X2)) = $true)) ) | ~spl0_10),
% 3.54/0.92 inference(beta-eta_normalization,[],[f463])).
% 3.54/0.92 thf(f467,plain,(
% 3.54/0.92 ( ! [X2 : $i,X1 : $i] : ((((likes_THFTYPE_IiioI @ X1 @ X2)) = $true)) ) | ~spl0_10),
% 3.54/0.92 inference(trivial_inequality_removal,[],[f466])).
% 3.54/0.92 thf(f469,plain,(
% 3.54/0.92 ($true = $false) | (spl0_2 | ~spl0_10)),
% 3.54/0.92 inference(superposition,[],[f467,f329])).
% 3.54/0.92 thf(f496,plain,(
% 3.54/0.92 $false | (spl0_2 | ~spl0_10)),
% 3.54/0.92 inference(trivial_inequality_removal,[],[f469])).
% 3.54/0.92 thf(f497,plain,(
% 3.54/0.92 spl0_2 | ~spl0_10),
% 3.54/0.92 inference(avatar_contradiction_clause,[],[f496])).
% 3.54/0.92 thf(f523,plain,(
% 3.54/0.92 (parent_THFTYPE_IiioI = (^[Y0 : $i]: ((^[Y1 : $i]: ($true))))) | ($true = $false) | (spl0_2 | ~spl0_9)),
% 3.54/0.92 inference(superposition,[],[f426,f220])).
% 3.54/0.92 thf(f531,plain,(
% 3.54/0.92 (parent_THFTYPE_IiioI = (^[Y0 : $i]: ((^[Y1 : $i]: ($true))))) | (spl0_2 | ~spl0_9)),
% 3.54/0.92 inference(trivial_inequality_removal,[],[f523])).
% 3.54/0.92 thf(f548,plain,(
% 3.54/0.92 ( ! [X1 : $i] : (((((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) @ X1)) = ((parent_THFTYPE_IiioI @ X1)))) ) | (spl0_2 | ~spl0_9)),
% 3.54/0.92 inference(argument_congruence,[],[f531])).
% 3.54/0.92 thf(f549,plain,(
% 3.54/0.92 ( ! [X1 : $i] : ((((parent_THFTYPE_IiioI @ X1)) = (^[Y0 : $i]: ($true)))) ) | (spl0_2 | ~spl0_9)),
% 3.54/0.92 inference(beta-eta_normalization,[],[f548])).
% 3.54/0.92 thf(f550,plain,(
% 3.54/0.92 ( ! [X2 : $i,X1 : $i] : ((((parent_THFTYPE_IiioI @ X1 @ X2)) = (((^[Y0 : $i]: ($true)) @ X2)))) ) | (spl0_2 | ~spl0_9)),
% 3.54/0.92 inference(argument_congruence,[],[f549])).
% 3.54/0.92 thf(f551,plain,(
% 3.54/0.92 ( ! [X2 : $i,X1 : $i] : ((((parent_THFTYPE_IiioI @ X1 @ X2)) = $true) | ($false = (((^[Y0 : $i]: ($true)) @ X2)))) ) | (spl0_2 | ~spl0_9)),
% 3.54/0.92 inference(iff_proxy_clausification,[],[f550])).
% 3.54/0.92 thf(f554,plain,(
% 3.54/0.92 ( ! [X2 : $i,X1 : $i] : ((((parent_THFTYPE_IiioI @ X1 @ X2)) = $true) | ($true = $false)) ) | (spl0_2 | ~spl0_9)),
% 3.54/0.92 inference(beta-eta_normalization,[],[f551])).
% 3.54/0.92 thf(f555,plain,(
% 3.54/0.92 ( ! [X2 : $i,X1 : $i] : ((((parent_THFTYPE_IiioI @ X1 @ X2)) = $true)) ) | (spl0_2 | ~spl0_9)),
% 3.54/0.92 inference(trivial_inequality_removal,[],[f554])).
% 3.54/0.92 thf(f571,plain,(
% 3.54/0.92 ($true = $false) | (spl0_2 | ~spl0_9)),
% 3.54/0.92 inference(superposition,[],[f346,f555])).
% 3.54/0.92 thf(f588,plain,(
% 3.54/0.92 $false | (spl0_2 | ~spl0_9)),
% 3.54/0.92 inference(trivial_inequality_removal,[],[f571])).
% 3.54/0.92 thf(f589,plain,(
% 3.54/0.92 spl0_2 | ~spl0_9),
% 3.54/0.92 inference(avatar_contradiction_clause,[],[f588])).
% 3.54/0.92 thf(f614,plain,(
% 3.54/0.92 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: ((^[Y1 : $i]: ($false)))) @ X1 @ lBill_THFTYPE_i)))) ) | ~spl0_3),
% 3.54/0.92 inference(primitive_instantiation,[],[f160])).
% 3.54/0.92 thf(f626,plain,(
% 3.54/0.92 ($true = $false) | ~spl0_3),
% 3.54/0.92 inference(beta-eta_normalization,[],[f614])).
% 3.54/0.92 thf(f627,plain,(
% 3.54/0.92 $false | ~spl0_3),
% 3.54/0.92 inference(trivial_inequality_removal,[],[f626])).
% 3.54/0.92 thf(f628,plain,(
% 3.54/0.92 ~spl0_3),
% 3.54/0.92 inference(avatar_contradiction_clause,[],[f627])).
% 3.54/0.92 cnf(s8, plain, ~spl0_2 | spl0_3, inference(sat_conversion,[],[f170])).
% 3.54/0.92 cnf(s15, plain, ~spl0_5 | spl0_6, inference(sat_conversion,[],[f184])).
% 3.54/0.92 cnf(s18, plain, spl0_2 | spl0_5, inference(sat_conversion,[],[f248])).
% 3.54/0.92 cnf(s29, plain, spl0_2 | ~spl0_6 | spl0_9 | spl0_10, inference(sat_conversion,[],[f457])).
% 3.54/0.92 cnf(s35, plain, spl0_2 | ~spl0_10, inference(sat_conversion,[],[f497])).
% 3.54/0.92 cnf(s42, plain, spl0_2 | ~spl0_9, inference(sat_conversion,[],[f589])).
% 3.54/0.92 cnf(s45, plain, ~spl0_3, inference(sat_conversion,[],[f628])).
% 3.54/0.92 cnf(s46, plain, ~spl0_2, inference(rat,[],[s8,s45])).
% 3.54/0.92 cnf(s47, plain, ~spl0_9, inference(rat,[],[s42,s46])).
% 3.54/0.92 cnf(s48, plain, ~spl0_10, inference(rat,[],[s35,s46])).
% 3.54/0.92 cnf(s49, plain, ~spl0_6, inference(rat,[],[s29,s48,s47,s46])).
% 3.54/0.92 cnf(s50, plain, spl0_5, inference(rat,[],[s18,s46])).
% 3.54/0.92 cnf(s51, plain, $false, inference(rat,[],[s15,s49,s50])).
% 3.54/0.92 thf(f641,plain,(
% 3.54/0.92 $false),
% 3.54/0.92 inference(avatar_sat_refutation,[],[s51])).
% 3.54/0.92 % SZS output end Proof for theBenchmark
% 3.54/0.92 % (675863)------------------------------
% 3.54/0.92 % (675863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.54/0.92 % (675863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.54/0.92 % (675863)CaDiCaL version: 2.1.3
% 3.54/0.92 % (675863)Termination reason: Refutation
% 3.54/0.92 % (675863)Time elapsed: 0.030 s
% 3.54/0.92 % (675863)Peak memory usage: 13 MB
% 3.54/0.92 % (675863)Instructions burned: 30 (million)
% 3.54/0.92 % (675751)Success in time 0.578 s
% 3.54/0.92 % Vampire exiting
%------------------------------------------------------------------------------