%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV433^2 : TPTP v9.3.1. Released v3.6.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n009.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:39:58 AM UTC 2026
% Result : Theorem 7.10s 1.52s
% Output : Refutation 7.10s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV433^2 : TPTP v9.3.1. Released v3.6.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.21 % Computer : n009.cluster.edu
% 0.10/0.21 % Model : x86_64 x86_64
% 0.10/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.21 % Memory : 8046.5625MB
% 0.10/0.21 % OS : Linux 6.8.0-71-generic
% 0.10/0.21 % CPULimit : 300
% 0.10/0.21 % WCLimit : 300
% 0.10/0.21 % DateTime : Tue Sep 29 16:03:15 UTC 2026
% 0.10/0.22 % CPUTime :
% 0.10/0.22 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.27 Running higher-order theorem proving
% 0.10/0.28 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.95/0.44 % (4182602)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.95/0.44 % (4182613)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.95/0.44 % (4182613)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.95/0.44 % (4182613)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=3861164214:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.95/0.44 % (4182607)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=2384065875:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.95/0.44 % (4182612)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=581075418:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.95/0.44 % (4182611)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=216150759:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.95/0.44 % (4182608)lrs+10_16_si=on:nwc=1.5:random_seed=1909980696:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.95/0.44 % (4182609)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=2230723846:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.95/0.44 % (4182610)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=3900859929: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.95/0.44 % (4182609)Instruction limit reached!
% 0.95/0.44 % (4182609)------------------------------
% 0.95/0.44 % (4182609)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.95/0.44 % (4182609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.95/0.44 % (4182609)CaDiCaL version: 2.1.3
% 0.95/0.44 % (4182609)Termination reason: Instruction limit
% 0.95/0.44 % (4182609)Termination phase: Property scanning
% 0.95/0.44 % (4182609)Time elapsed: 0.003 s
% 0.95/0.44 % (4182609)Peak memory usage: 10 MB
% 0.95/0.44 % (4182609)Instructions burned: 3 (million)
% 0.95/0.44 % (4182608)Instruction limit reached!
% 0.95/0.44 % (4182608)------------------------------
% 0.95/0.44 % (4182608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.95/0.44 % (4182608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.95/0.44 % (4182608)CaDiCaL version: 2.1.3
% 0.95/0.44 % (4182608)Termination reason: Instruction limit
% 0.95/0.44 % (4182608)Termination phase: Saturation
% 0.95/0.44 % (4182608)Time elapsed: 0.017 s
% 0.95/0.44 % (4182608)Peak memory usage: 12 MB
% 0.95/0.44 % (4182608)Instructions burned: 18 (million)
% 0.95/0.44 % (4182611)Instruction limit reached!
% 0.95/0.44 % (4182611)------------------------------
% 0.95/0.44 % (4182611)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.95/0.44 % (4182611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.95/0.44 % (4182611)CaDiCaL version: 2.1.3
% 0.95/0.44 % (4182611)Termination reason: Instruction limit
% 0.95/0.44 % (4182611)Termination phase: Saturation
% 0.95/0.44 % (4182611)Time elapsed: 0.023 s
% 0.95/0.44 % (4182611)Peak memory usage: 11 MB
% 0.95/0.44 % (4182611)Instructions burned: 24 (million)
% 0.95/0.44 % (4182607)Instruction limit reached!
% 0.95/0.44 % (4182607)------------------------------
% 0.95/0.44 % (4182607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.95/0.44 % (4182607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.95/0.44 % (4182607)CaDiCaL version: 2.1.3
% 0.95/0.44 % (4182607)Termination reason: Instruction limit
% 0.95/0.44 % (4182607)Termination phase: Saturation
% 0.95/0.44 % (4182607)Time elapsed: 0.050 s
% 0.95/0.44 % (4182607)Peak memory usage: 13 MB
% 0.95/0.44 % (4182607)Instructions burned: 89 (million)
% 0.95/0.44 % (4182621)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2686516088:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.95/0.44 % (4182621)Instruction limit reached!
% 0.95/0.44 % (4182621)------------------------------
% 0.95/0.44 % (4182621)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.95/0.48 % (4182621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.95/0.48 % (4182621)CaDiCaL version: 2.1.3
% 0.95/0.48 % (4182621)Termination reason: Instruction limit
% 0.95/0.48 % (4182621)Termination phase: Naming
% 0.95/0.48 % (4182621)Time elapsed: 0.003 s
% 0.95/0.48 % (4182621)Peak memory usage: 10 MB
% 0.95/0.48 % (4182621)Instructions burned: 2 (million)
% 0.95/0.48 % (4182622)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=1361056867:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.95/0.48 % (4182623)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.95/0.48 % (4182622)Instruction limit reached!
% 0.95/0.48 % (4182622)------------------------------
% 0.95/0.48 % (4182622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.95/0.48 % (4182622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.95/0.48 % (4182622)CaDiCaL version: 2.1.3
% 0.95/0.48 % (4182622)Termination reason: Instruction limit
% 0.95/0.48 % (4182622)Termination phase: Property scanning
% 0.95/0.48 % (4182622)Time elapsed: 0.005 s
% 0.95/0.48 % (4182622)Peak memory usage: 11 MB
% 0.95/0.48 % (4182622)Instructions burned: 5 (million)
% 0.95/0.48 % (4182623)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=721750234:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.95/0.48 % (4182613)Instruction limit reached!
% 0.95/0.48 % (4182613)------------------------------
% 0.95/0.48 % (4182613)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.95/0.48 % (4182613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.95/0.48 % (4182613)CaDiCaL version: 2.1.3
% 0.95/0.48 % (4182613)Termination reason: Instruction limit
% 0.95/0.48 % (4182613)Termination phase: Saturation
% 0.95/0.48 % (4182613)Time elapsed: 0.071 s
% 0.95/0.48 % (4182613)Peak memory usage: 12 MB
% 0.95/0.48 % (4182613)Instructions burned: 157 (million)
% 0.95/0.48 % (4182624)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=1155936887:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.95/0.48 % (4182623)Instruction limit reached!
% 0.95/0.48 % (4182623)------------------------------
% 0.95/0.48 % (4182623)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.95/0.48 % (4182623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.95/0.48 % (4182623)CaDiCaL version: 2.1.3
% 0.95/0.48 % (4182623)Termination reason: Instruction limit
% 0.95/0.48 % (4182623)Termination phase: Saturation
% 0.95/0.48 % (4182623)Time elapsed: 0.006 s
% 0.95/0.48 % (4182623)Peak memory usage: 11 MB
% 0.95/0.48 % (4182623)Instructions burned: 7 (million)
% 0.95/0.48 % (4182612)Instruction limit reached!
% 0.95/0.48 % (4182612)------------------------------
% 0.95/0.48 % (4182612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.95/0.48 % (4182612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.95/0.48 % (4182612)CaDiCaL version: 2.1.3
% 0.95/0.48 % (4182612)Termination reason: Instruction limit
% 0.95/0.48 % (4182612)Termination phase: Saturation
% 0.95/0.48 % (4182612)Time elapsed: 0.066 s
% 0.95/0.48 % (4182612)Peak memory usage: 12 MB
% 0.95/0.48 % (4182612)Instructions burned: 75 (million)
% 0.95/0.48 % (4182624)Instruction limit reached!
% 0.95/0.48 % (4182624)------------------------------
% 0.95/0.48 % (4182624)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.95/0.48 % (4182624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.95/0.48 % (4182624)CaDiCaL version: 2.1.3
% 0.95/0.48 % (4182624)Termination reason: Instruction limit
% 0.95/0.48 % (4182624)Termination phase: Saturation
% 0.95/0.48 % (4182624)Time elapsed: 0.010 s
% 0.95/0.48 % (4182624)Peak memory usage: 11 MB
% 0.95/0.48 % (4182624)Instructions burned: 12 (million)
% 0.95/0.48 % (4182630)lrs+10_1_si=on:cs=on:random_seed=1993554199:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.95/0.48 % (4182630)Instruction limit reached!
% 0.95/0.48 % (4182630)------------------------------
% 0.95/0.48 % (4182630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.95/0.48 % (4182630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.95/0.48 % (4182630)CaDiCaL version: 2.1.3
% 0.95/0.52 % (4182630)Termination reason: Instruction limit
% 0.95/0.52 % (4182630)Termination phase: Saturation
% 0.95/0.52 % (4182630)Time elapsed: 0.004 s
% 0.95/0.52 % (4182630)Peak memory usage: 11 MB
% 0.95/0.52 % (4182630)Instructions burned: 8 (million)
% 0.95/0.52 % (4182626)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.95/0.52 % (4182626)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.95/0.52 % (4182628)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=1079745594:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.95/0.52 % (4182633)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=4091896722:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/38Mi)
% 0.95/0.52 % (4182626)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=3867494306: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.95/0.52 % (4182633)Refutation not found, incomplete strategy
% 0.95/0.52 % (4182633)------------------------------
% 0.95/0.52 % (4182633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.95/0.52 % (4182633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.95/0.52 % (4182633)CaDiCaL version: 2.1.3
% 0.95/0.52 % (4182633)Termination reason: Refutation not found, incomplete strategy
% 0.95/0.52 % (4182633)Time elapsed: 0.002 s
% 0.95/0.52 % (4182633)Peak memory usage: 12 MB
% 0.95/0.52 % (4182633)Instructions burned: 3 (million)
% 0.95/0.52 % (4182632)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.95/0.52 % (4182633)------------------------------
% 0.95/0.52 % (4182633)------------------------------
% 0.95/0.52 % (4182632)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=2465574362:i=2:add=on:rtra=on_2998 on theBenchmark for (2998ds/2Mi)
% 0.95/0.52 % (4182632)Instruction limit reached!
% 0.95/0.52 % (4182632)------------------------------
% 0.95/0.52 % (4182632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.95/0.52 % (4182632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.95/0.52 % (4182632)CaDiCaL version: 2.1.3
% 0.95/0.52 % (4182632)Termination reason: Instruction limit
% 0.95/0.52 % (4182632)Termination phase: Preprocessing 2
% 0.95/0.52 % (4182632)Time elapsed: 0.002 s
% 0.95/0.52 % (4182632)Peak memory usage: 10 MB
% 0.95/0.52 % (4182632)Instructions burned: 2 (million)
% 0.95/0.52 % (4182637)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=2507702283:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 0.95/0.52 % (4182634)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=1334335518:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 0.95/0.52 % (4182634)Refutation not found, incomplete strategy
% 0.95/0.52 % (4182634)------------------------------
% 0.95/0.52 % (4182634)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.95/0.52 % (4182634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.95/0.52 % (4182634)CaDiCaL version: 2.1.3
% 0.95/0.52 % (4182634)Termination reason: Refutation not found, incomplete strategy
% 0.95/0.52 % (4182634)Time elapsed: 0.005 s
% 0.95/0.52 % (4182634)Peak memory usage: 12 MB
% 0.95/0.52 % (4182634)Instructions burned: 5 (million)
% 0.95/0.52 % (4182640)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=3610725912:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 0.95/0.52 % (4182634)------------------------------
% 0.95/0.52 % (4182634)------------------------------
% 0.95/0.52 % (4182626)Instruction limit reached!
% 0.95/0.52 % (4182626)------------------------------
% 0.95/0.52 % (4182626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.95/0.52 % (4182626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.74/0.57 % (4182626)CaDiCaL version: 2.1.3
% 1.74/0.57 % (4182626)Termination reason: Instruction limit
% 1.74/0.57 % (4182626)Termination phase: Saturation
% 1.74/0.57 % (4182626)Time elapsed: 0.025 s
% 1.74/0.57 % (4182626)Peak memory usage: 11 MB
% 1.74/0.57 % (4182626)Instructions burned: 28 (million)
% 1.74/0.57 % (4182637)Instruction limit reached!
% 1.74/0.57 % (4182637)------------------------------
% 1.74/0.57 % (4182637)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.74/0.57 % (4182637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.74/0.57 % (4182637)CaDiCaL version: 2.1.3
% 1.74/0.57 % (4182637)Termination reason: Instruction limit
% 1.74/0.57 % (4182637)Termination phase: Saturation
% 1.74/0.57 % (4182637)Time elapsed: 0.014 s
% 1.74/0.57 % (4182637)Peak memory usage: 12 MB
% 1.74/0.57 % (4182637)Instructions burned: 26 (million)
% 1.74/0.57 % (4182640)Instruction limit reached!
% 1.74/0.57 % (4182640)------------------------------
% 1.74/0.57 % (4182640)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.74/0.57 % (4182640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.74/0.57 % (4182640)CaDiCaL version: 2.1.3
% 1.74/0.57 % (4182640)Termination reason: Instruction limit
% 1.74/0.57 % (4182640)Termination phase: Saturation
% 1.74/0.57 % (4182640)Time elapsed: 0.012 s
% 1.74/0.57 % (4182640)Peak memory usage: 11 MB
% 1.74/0.57 % (4182640)Instructions burned: 14 (million)
% 1.74/0.57 % (4182642)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=3793496116:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 1.74/0.57 % (4182646)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=2352755913:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.74/0.57 % (4182648)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=722536822:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.74/0.57 % (4182646)Instruction limit reached!
% 1.74/0.57 % (4182646)------------------------------
% 1.74/0.57 % (4182646)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.74/0.57 % (4182646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.74/0.57 % (4182646)CaDiCaL version: 2.1.3
% 1.74/0.57 % (4182646)Termination reason: Instruction limit
% 1.74/0.57 % (4182646)Termination phase: Saturation
% 1.74/0.57 % (4182646)Time elapsed: 0.007 s
% 1.74/0.57 % (4182646)Peak memory usage: 11 MB
% 1.74/0.57 % (4182646)Instructions burned: 15 (million)
% 1.74/0.57 % (4182642)Refutation not found, incomplete strategy
% 1.74/0.57 % (4182642)------------------------------
% 1.74/0.57 % (4182642)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.74/0.57 % (4182642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.74/0.57 % (4182642)CaDiCaL version: 2.1.3
% 1.74/0.57 % (4182642)Termination reason: Refutation not found, incomplete strategy
% 1.74/0.57 % (4182642)Time elapsed: 0.009 s
% 1.74/0.57 % (4182642)Peak memory usage: 12 MB
% 1.74/0.57 % (4182642)Instructions burned: 10 (million)
% 1.74/0.57 % (4182642)------------------------------
% 1.74/0.57 % (4182642)------------------------------
% 1.74/0.57 % (4182647)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=2131847654: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.74/0.57 % (4182647)Instruction limit reached!
% 1.74/0.57 % (4182647)------------------------------
% 1.74/0.57 % (4182647)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.74/0.57 % (4182647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.74/0.57 % (4182647)CaDiCaL version: 2.1.3
% 1.74/0.57 % (4182647)Termination reason: Instruction limit
% 1.74/0.57 % (4182647)Termination phase: Property scanning
% 1.74/0.57 % (4182647)Time elapsed: 0.002 s
% 1.74/0.57 % (4182647)Peak memory usage: 10 MB
% 1.74/0.57 % (4182647)Instructions burned: 2 (million)
% 1.74/0.57 % (4182648)Instruction limit reached!
% 1.74/0.57 % (4182648)------------------------------
% 1.74/0.57 % (4182648)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.74/0.57 % (4182648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.74/0.57 % (4182648)CaDiCaL version: 2.1.3
% 1.74/0.57 % (4182648)Termination reason: Instruction limit
% 1.74/0.57 % (4182648)Termination phase: Saturation
% 1.74/0.57 % (4182648)Time elapsed: 0.015 s
% 2.38/0.62 % (4182648)Peak memory usage: 12 MB
% 2.38/0.62 % (4182648)Instructions burned: 27 (million)
% 2.38/0.62 % (4182628)Instruction limit reached!
% 2.38/0.62 % (4182628)------------------------------
% 2.38/0.62 % (4182628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.38/0.62 % (4182628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.38/0.62 % (4182628)CaDiCaL version: 2.1.3
% 2.38/0.62 % (4182628)Termination reason: Instruction limit
% 2.38/0.62 % (4182628)Termination phase: Saturation
% 2.38/0.62 % (4182628)Time elapsed: 0.073 s
% 2.38/0.62 % (4182628)Peak memory usage: 12 MB
% 2.38/0.62 % (4182628)Instructions burned: 87 (million)
% 2.38/0.62 % (4182649)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=571300408:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 2.38/0.62 % (4182653)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=642295041:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 2.38/0.62 % (4182654)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.38/0.62 % (4182654)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 2.38/0.62 % (4182657)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=646948230:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 2.38/0.62 % (4182656)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 2.38/0.62 % (4182654)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=1382357772:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 2.38/0.62 % (4182659)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=2706033242:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 2.38/0.62 % (4182649)Instruction limit reached!
% 2.38/0.62 % (4182649)------------------------------
% 2.38/0.62 % (4182649)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.38/0.62 % (4182649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.38/0.62 % (4182649)CaDiCaL version: 2.1.3
% 2.38/0.62 % (4182649)Termination reason: Instruction limit
% 2.38/0.62 % (4182649)Termination phase: Saturation
% 2.38/0.62 % (4182649)Time elapsed: 0.021 s
% 2.38/0.62 % (4182649)Peak memory usage: 11 MB
% 2.38/0.62 % (4182649)Instructions burned: 23 (million)
% 2.38/0.62 % (4182656)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=1588562675:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 2.38/0.62 % (4182659)Instruction limit reached!
% 2.38/0.62 % (4182659)------------------------------
% 2.38/0.62 % (4182659)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.38/0.62 % (4182659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.38/0.62 % (4182659)CaDiCaL version: 2.1.3
% 2.38/0.62 % (4182659)Termination reason: Instruction limit
% 2.38/0.62 % (4182659)Termination phase: Property scanning
% 2.38/0.62 % (4182659)Time elapsed: 0.005 s
% 2.38/0.62 % (4182659)Peak memory usage: 10 MB
% 2.38/0.62 % (4182659)Instructions burned: 7 (million)
% 2.38/0.62 % (4182656)Instruction limit reached!
% 2.38/0.62 % (4182656)------------------------------
% 2.38/0.62 % (4182656)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.38/0.62 % (4182656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.38/0.62 % (4182656)CaDiCaL version: 2.1.3
% 2.38/0.62 % (4182656)Termination reason: Instruction limit
% 2.38/0.62 % (4182656)Termination phase: Saturation
% 2.38/0.62 % (4182656)Time elapsed: 0.007 s
% 2.38/0.62 % (4182656)Peak memory usage: 11 MB
% 2.38/0.62 % (4182656)Instructions burned: 8 (million)
% 2.38/0.62 % (4182654)Instruction limit reached!
% 2.38/0.62 % (4182654)------------------------------
% 2.38/0.62 % (4182654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.38/0.62 % (4182654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.56/0.69 % (4182654)CaDiCaL version: 2.1.3
% 2.56/0.69 % (4182654)Termination reason: Instruction limit
% 2.56/0.69 % (4182654)Termination phase: Saturation
% 2.56/0.69 % (4182654)Time elapsed: 0.013 s
% 2.56/0.69 % (4182654)Peak memory usage: 12 MB
% 2.56/0.69 % (4182654)Instructions burned: 14 (million)
% 2.56/0.69 % (4182657)Instruction limit reached!
% 2.56/0.69 % (4182657)------------------------------
% 2.56/0.69 % (4182657)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.56/0.69 % (4182657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.56/0.69 % (4182657)CaDiCaL version: 2.1.3
% 2.56/0.69 % (4182657)Termination reason: Instruction limit
% 2.56/0.69 % (4182657)Termination phase: Saturation
% 2.56/0.69 % (4182657)Time elapsed: 0.017 s
% 2.56/0.69 % (4182657)Peak memory usage: 12 MB
% 2.56/0.69 % (4182657)Instructions burned: 33 (million)
% 2.56/0.69 % (4182669)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=2123536820:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/193Mi)
% 2.56/0.69 % (4182664)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=2357200867:i=23:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/23Mi)
% 2.56/0.69 % (4182667)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=475400929:i=1240:rtra=on:ixr=off_2997 on theBenchmark for (2997ds/1240Mi)
% 2.56/0.69 % (4182669)Refutation not found, incomplete strategy
% 2.56/0.69 % (4182669)------------------------------
% 2.56/0.69 % (4182669)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.56/0.69 % (4182669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.56/0.69 % (4182669)CaDiCaL version: 2.1.3
% 2.56/0.69 % (4182669)Termination reason: Refutation not found, incomplete strategy
% 2.56/0.69 % (4182669)Time elapsed: 0.004 s
% 2.56/0.69 % (4182669)Peak memory usage: 12 MB
% 2.56/0.69 % (4182669)Instructions burned: 8 (million)
% 2.56/0.69 % (4182669)------------------------------
% 2.56/0.69 % (4182669)------------------------------
% 2.56/0.69 % (4182666)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=288894607:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2997 on theBenchmark for (2997ds/20Mi)
% 2.56/0.69 % (4182653)Instruction limit reached!
% 2.56/0.69 % (4182653)------------------------------
% 2.56/0.69 % (4182653)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.56/0.69 % (4182653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.56/0.69 % (4182653)CaDiCaL version: 2.1.3
% 2.56/0.69 % (4182653)Termination reason: Instruction limit
% 2.56/0.69 % (4182653)Termination phase: Saturation
% 2.56/0.69 % (4182653)Time elapsed: 0.055 s
% 2.56/0.69 % (4182653)Peak memory usage: 12 MB
% 2.56/0.69 % (4182653)Instructions burned: 60 (million)
% 2.56/0.69 % (4182668)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=3803453471:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2997 on theBenchmark for (2997ds/143Mi)
% 2.56/0.69 % (4182664)Instruction limit reached!
% 2.56/0.69 % (4182664)------------------------------
% 2.56/0.69 % (4182664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.56/0.69 % (4182664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.56/0.69 % (4182664)CaDiCaL version: 2.1.3
% 2.56/0.69 % (4182664)Termination reason: Instruction limit
% 2.56/0.69 % (4182664)Termination phase: Saturation
% 2.56/0.69 % (4182664)Time elapsed: 0.019 s
% 2.56/0.69 % (4182664)Peak memory usage: 11 MB
% 2.56/0.69 % (4182664)Instructions burned: 23 (million)
% 2.56/0.69 % (4182675)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 2.56/0.69 % (4182675)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1416270494:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2997 on theBenchmark for (2997ds/7Mi)
% 2.56/0.69 % (4182666)Instruction limit reached!
% 2.56/0.69 % (4182666)------------------------------
% 2.56/0.69 % (4182666)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.56/0.69 % (4182666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.56/0.69 % (4182666)CaDiCaL version: 2.1.3
% 2.56/0.69 % (4182666)Termination reason: Instruction limit
% 2.56/0.69 % (4182666)Termination phase: Saturation
% 2.56/0.69 % (4182666)Time elapsed: 0.020 s
% 3.21/0.86 % (4182666)Peak memory usage: 12 MB
% 3.21/0.86 % (4182666)Instructions burned: 20 (million)
% 3.21/0.86 % (4182675)Instruction limit reached!
% 3.21/0.86 % (4182675)------------------------------
% 3.21/0.86 % (4182675)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.21/0.86 % (4182675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.21/0.86 % (4182675)CaDiCaL version: 2.1.3
% 3.21/0.86 % (4182675)Termination reason: Instruction limit
% 3.21/0.86 % (4182675)Termination phase: Saturation
% 3.21/0.86 % (4182675)Time elapsed: 0.003 s
% 3.21/0.86 % (4182675)Peak memory usage: 11 MB
% 3.21/0.86 % (4182675)Instructions burned: 7 (million)
% 3.21/0.86 % (4182673)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3961318097:i=42:hud=10:rtra=on_2997 on theBenchmark for (2997ds/42Mi)
% 3.21/0.86 % (4182677)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=3864869284:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/181Mi)
% 3.21/0.86 % (4182677)Refutation not found, incomplete strategy
% 3.21/0.86 % (4182677)------------------------------
% 3.21/0.86 % (4182677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.21/0.86 % (4182677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.21/0.86 % (4182677)CaDiCaL version: 2.1.3
% 3.21/0.86 % (4182677)Termination reason: Refutation not found, incomplete strategy
% 3.21/0.86 % (4182677)Time elapsed: 0.003 s
% 3.21/0.86 % (4182677)Peak memory usage: 12 MB
% 3.21/0.86 % (4182677)Instructions burned: 4 (million)
% 3.21/0.86 % (4182677)------------------------------
% 3.21/0.86 % (4182677)------------------------------
% 3.21/0.86 % (4182680)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 3.21/0.86 % (4182680)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=1360911269:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2997 on theBenchmark for (2997ds/6Mi)
% 3.21/0.86 % (4182680)Instruction limit reached!
% 3.21/0.86 % (4182680)------------------------------
% 3.21/0.86 % (4182680)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.21/0.86 % (4182680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.21/0.86 % (4182680)CaDiCaL version: 2.1.3
% 3.21/0.86 % (4182680)Termination reason: Instruction limit
% 3.21/0.86 % (4182680)Termination phase: Property scanning
% 3.21/0.86 % (4182680)Time elapsed: 0.003 s
% 3.21/0.86 % (4182680)Peak memory usage: 10 MB
% 3.21/0.86 % (4182680)Instructions burned: 7 (million)
% 3.21/0.86 % (4182679)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=3027278538: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)
% 3.21/0.86 % (4182683)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=2963584481:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2997 on theBenchmark for (2997ds/22Mi)
% 3.21/0.86 % (4182679)Refutation not found, incomplete strategy
% 3.21/0.86 % (4182679)------------------------------
% 3.21/0.86 % (4182679)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.21/0.86 % (4182679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.21/0.86 % (4182679)CaDiCaL version: 2.1.3
% 3.21/0.86 % (4182679)Termination reason: Refutation not found, incomplete strategy
% 3.21/0.86 % (4182679)Time elapsed: 0.008 s
% 3.21/0.86 % (4182679)Peak memory usage: 12 MB
% 3.21/0.86 % (4182679)Instructions burned: 8 (million)
% 3.21/0.86 % (4182679)------------------------------
% 3.21/0.86 % (4182679)------------------------------
% 3.21/0.86 % (4182685)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=1167473052:i=19:add=on:rtra=on_2996 on theBenchmark for (2996ds/19Mi)
% 3.21/0.86 % (4182685)Refutation not found, incomplete strategy
% 3.21/0.86 % (4182685)------------------------------
% 3.21/0.86 % (4182685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.21/0.86 % (4182685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.21/0.86 % (4182685)CaDiCaL version: 2.1.3
% 3.21/0.86 % (4182685)Termination reason: Refutation not found, incomplete strategy
% 3.21/0.86 % (4182685)Time elapsed: 0.006 s
% 3.21/0.86 % (4182685)Peak memory usage: 12 MB
% 3.19/0.92 % (4182685)Instructions burned: 12 (million)
% 3.19/0.92 % (4182683)Instruction limit reached!
% 3.19/0.92 % (4182683)------------------------------
% 3.19/0.92 % (4182683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.19/0.92 % (4182683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.19/0.92 % (4182683)CaDiCaL version: 2.1.3
% 3.19/0.92 % (4182683)Termination reason: Instruction limit
% 3.19/0.92 % (4182683)Termination phase: Saturation
% 3.19/0.92 % (4182683)Time elapsed: 0.013 s
% 3.19/0.92 % (4182683)Peak memory usage: 12 MB
% 3.19/0.92 % (4182683)Instructions burned: 22 (million)
% 3.19/0.92 % (4182685)------------------------------
% 3.19/0.92 % (4182685)------------------------------
% 3.19/0.92 % (4182673)Instruction limit reached!
% 3.19/0.92 % (4182673)------------------------------
% 3.19/0.92 % (4182673)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.19/0.92 % (4182673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.19/0.92 % (4182673)CaDiCaL version: 2.1.3
% 3.19/0.92 % (4182673)Termination reason: Instruction limit
% 3.19/0.92 % (4182673)Termination phase: Saturation
% 3.19/0.92 % (4182673)Time elapsed: 0.044 s
% 3.19/0.92 % (4182673)Peak memory usage: 12 MB
% 3.19/0.92 % (4182673)Instructions burned: 42 (million)
% 3.19/0.92 % (4182691)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=3896011572: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.19/0.92 % (4182690)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=957382757: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.19/0.92 % (4182689)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=2579921946:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/316Mi)
% 3.19/0.92 % (4182692)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=2453558753:i=480:rtra=on_2996 on theBenchmark for (2996ds/480Mi)
% 3.19/0.92 % (4182691)Instruction limit reached!
% 3.19/0.92 % (4182691)------------------------------
% 3.19/0.92 % (4182691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.19/0.92 % (4182691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.19/0.92 % (4182691)CaDiCaL version: 2.1.3
% 3.19/0.92 % (4182691)Termination reason: Instruction limit
% 3.19/0.92 % (4182691)Termination phase: Saturation
% 3.19/0.92 % (4182691)Time elapsed: 0.022 s
% 3.19/0.92 % (4182691)Peak memory usage: 12 MB
% 3.19/0.92 % (4182691)Instructions burned: 46 (million)
% 3.19/0.92 % (4182692)Refutation not found, incomplete strategy
% 3.19/0.92 % (4182692)------------------------------
% 3.19/0.92 % (4182692)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.19/0.92 % (4182692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.19/0.92 % (4182692)CaDiCaL version: 2.1.3
% 3.19/0.92 % (4182692)Termination reason: Refutation not found, incomplete strategy
% 3.19/0.92 % (4182692)Time elapsed: 0.007 s
% 3.19/0.92 % (4182692)Peak memory usage: 12 MB
% 3.19/0.92 % (4182692)Instructions burned: 6 (million)
% 3.19/0.92 % (4182692)------------------------------
% 3.19/0.92 % (4182692)------------------------------
% 3.19/0.92 % (4182668)Instruction limit reached!
% 3.19/0.92 % (4182668)------------------------------
% 3.19/0.92 % (4182668)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.19/0.92 % (4182668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.19/0.92 % (4182668)CaDiCaL version: 2.1.3
% 3.19/0.92 % (4182668)Termination reason: Instruction limit
% 3.19/0.92 % (4182668)Termination phase: Saturation
% 3.19/0.92 % (4182668)Time elapsed: 0.129 s
% 3.19/0.92 % (4182668)Peak memory usage: 13 MB
% 3.19/0.92 % (4182668)Instructions burned: 143 (million)
% 3.19/0.92 % (4182697)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=2901683989: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.19/0.92 % (4182698)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 3.19/0.99 % (4182698)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=2776826841:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/200Mi)
% 3.19/0.99 % (4182699)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=1965072575:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2996 on theBenchmark for (2996ds/13Mi)
% 3.19/0.99 % (4182697)Instruction limit reached!
% 3.19/0.99 % (4182697)------------------------------
% 3.19/0.99 % (4182697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.19/0.99 % (4182697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.19/0.99 % (4182697)CaDiCaL version: 2.1.3
% 3.19/0.99 % (4182697)Termination reason: Instruction limit
% 3.19/0.99 % (4182697)Termination phase: Saturation
% 3.19/0.99 % (4182697)Time elapsed: 0.021 s
% 3.19/0.99 % (4182697)Peak memory usage: 12 MB
% 3.19/0.99 % (4182697)Instructions burned: 21 (million)
% 3.19/0.99 % (4182699)Instruction limit reached!
% 3.19/0.99 % (4182699)------------------------------
% 3.19/0.99 % (4182699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.19/0.99 % (4182699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.19/0.99 % (4182699)CaDiCaL version: 2.1.3
% 3.19/0.99 % (4182699)Termination reason: Instruction limit
% 3.19/0.99 % (4182699)Termination phase: Saturation
% 3.19/0.99 % (4182699)Time elapsed: 0.008 s
% 3.19/0.99 % (4182699)Peak memory usage: 12 MB
% 3.19/0.99 % (4182699)Instructions burned: 13 (million)
% 3.19/0.99 % (4182704)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=2019965817:i=51:fsr=off:rtra=on_2995 on theBenchmark for (2995ds/51Mi)
% 3.19/0.99 % (4182703)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=3116919239:i=66:s2at=3:nm=2:rtra=on:rawr=on_2995 on theBenchmark for (2995ds/66Mi)
% 3.19/0.99 % (4182704)Refutation not found, incomplete strategy
% 3.19/0.99 % (4182704)------------------------------
% 3.19/0.99 % (4182704)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.19/0.99 % (4182704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.19/0.99 % (4182704)CaDiCaL version: 2.1.3
% 3.19/0.99 % (4182704)Termination reason: Refutation not found, incomplete strategy
% 3.19/0.99 % (4182704)Time elapsed: 0.007 s
% 3.19/0.99 % (4182704)Peak memory usage: 12 MB
% 3.19/0.99 % (4182704)Instructions burned: 12 (million)
% 3.19/0.99 % (4182704)------------------------------
% 3.19/0.99 % (4182704)------------------------------
% 3.19/0.99 % (4182707)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=121139022:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/31Mi)
% 3.19/0.99 % (4182707)Instruction limit reached!
% 3.19/0.99 % (4182707)------------------------------
% 3.19/0.99 % (4182707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.19/0.99 % (4182707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.19/0.99 % (4182707)CaDiCaL version: 2.1.3
% 3.19/0.99 % (4182707)Termination reason: Instruction limit
% 3.19/0.99 % (4182707)Termination phase: Saturation
% 3.19/0.99 % (4182707)Time elapsed: 0.015 s
% 3.19/0.99 % (4182707)Peak memory usage: 12 MB
% 3.19/0.99 % (4182707)Instructions burned: 31 (million)
% 3.19/0.99 % (4182709)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=3836528743:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2995 on theBenchmark for (2995ds/137Mi)
% 3.19/0.99 % (4182703)Instruction limit reached!
% 3.19/0.99 % (4182703)------------------------------
% 3.19/0.99 % (4182703)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.19/0.99 % (4182703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.19/0.99 % (4182703)CaDiCaL version: 2.1.3
% 3.19/0.99 % (4182703)Termination reason: Instruction limit
% 3.19/0.99 % (4182703)Termination phase: Saturation
% 3.19/0.99 % (4182703)Time elapsed: 0.059 s
% 3.19/0.99 % (4182703)Peak memory usage: 13 MB
% 3.19/0.99 % (4182703)Instructions burned: 66 (million)
% 3.19/0.99 % (4182711)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=1714993048:cond=on:i=34:hud=10:nm=10:rtra=on_2994 on theBenchmark for (2994ds/34Mi)
% 3.19/0.99 % (4182709)Instruction limit reached!
% 5.37/1.10 % (4182709)------------------------------
% 5.37/1.10 % (4182709)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.37/1.10 % (4182709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.37/1.10 % (4182709)CaDiCaL version: 2.1.3
% 5.37/1.10 % (4182709)Termination reason: Instruction limit
% 5.37/1.10 % (4182709)Termination phase: Saturation
% 5.37/1.10 % (4182709)Time elapsed: 0.066 s
% 5.37/1.10 % (4182709)Peak memory usage: 13 MB
% 5.37/1.10 % (4182709)Instructions burned: 138 (million)
% 5.37/1.10 % (4182711)Instruction limit reached!
% 5.37/1.10 % (4182711)------------------------------
% 5.37/1.10 % (4182711)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.37/1.10 % (4182711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.37/1.10 % (4182711)CaDiCaL version: 2.1.3
% 5.37/1.10 % (4182711)Termination reason: Instruction limit
% 5.37/1.10 % (4182711)Termination phase: Saturation
% 5.37/1.10 % (4182711)Time elapsed: 0.041 s
% 5.37/1.10 % (4182711)Peak memory usage: 12 MB
% 5.37/1.10 % (4182711)Instructions burned: 34 (million)
% 5.37/1.10 % (4182698)Instruction limit reached!
% 5.37/1.10 % (4182698)------------------------------
% 5.37/1.10 % (4182698)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.37/1.10 % (4182698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.37/1.10 % (4182698)CaDiCaL version: 2.1.3
% 5.37/1.10 % (4182698)Termination reason: Instruction limit
% 5.37/1.10 % (4182698)Termination phase: Saturation
% 5.37/1.10 % (4182698)Time elapsed: 0.175 s
% 5.37/1.10 % (4182698)Peak memory usage: 12 MB
% 5.37/1.10 % (4182698)Instructions burned: 201 (million)
% 5.37/1.10 % (4182713)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=2284831277:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2994 on theBenchmark for (2994ds/67Mi)
% 5.37/1.10 % (4182713)Refutation not found, incomplete strategy
% 5.37/1.10 % (4182713)------------------------------
% 5.37/1.10 % (4182713)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.37/1.10 % (4182713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.37/1.10 % (4182713)CaDiCaL version: 2.1.3
% 5.37/1.10 % (4182713)Termination reason: Refutation not found, incomplete strategy
% 5.37/1.10 % (4182713)Time elapsed: 0.006 s
% 5.37/1.10 % (4182713)Peak memory usage: 12 MB
% 5.37/1.10 % (4182713)Instructions burned: 12 (million)
% 5.37/1.10 % (4182713)------------------------------
% 5.37/1.10 % (4182713)------------------------------
% 5.37/1.10 % (4182714)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 5.37/1.10 % (4182714)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=2903809124:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2994 on theBenchmark for (2994ds/180Mi)
% 5.37/1.10 % (4182610)Instruction limit reached!
% 5.37/1.10 % (4182610)------------------------------
% 5.37/1.10 % (4182610)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.37/1.10 % (4182610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.37/1.10 % (4182610)CaDiCaL version: 2.1.3
% 5.37/1.10 % (4182610)Termination reason: Instruction limit
% 5.37/1.10 % (4182610)Termination phase: Saturation
% 5.37/1.10 % (4182610)Time elapsed: 0.569 s
% 5.37/1.10 % (4182610)Peak memory usage: 15 MB
% 5.37/1.10 % (4182610)Instructions burned: 634 (million)
% 5.37/1.10 % (4182717)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=778490378:cond=on:i=96:bd=all:rtra=on_2994 on theBenchmark for (2994ds/96Mi)
% 5.37/1.10 % (4182715)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=831377334:st=2:i=246:sd=3:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/246Mi)
% 5.37/1.10 % (4182715)Refutation not found, incomplete strategy
% 5.37/1.10 % (4182715)------------------------------
% 5.37/1.10 % (4182715)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.37/1.10 % (4182715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.37/1.10 % (4182715)CaDiCaL version: 2.1.3
% 5.37/1.10 % (4182715)Termination reason: Refutation not found, incomplete strategy
% 5.37/1.10 % (4182715)Time elapsed: 0.009 s
% 5.37/1.10 % (4182715)Peak memory usage: 12 MB
% 5.37/1.10 % (4182715)Instructions burned: 9 (million)
% 5.37/1.10 % (4182715)------------------------------
% 5.37/1.10 % (4182715)------------------------------
% 5.37/1.10 % (4182720)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=902741183:i=427:sd=1:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/427Mi)
% 6.25/1.22 % (4182720)Refutation not found, incomplete strategy
% 6.25/1.22 % (4182720)------------------------------
% 6.25/1.22 % (4182720)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.25/1.22 % (4182720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.25/1.22 % (4182720)CaDiCaL version: 2.1.3
% 6.25/1.22 % (4182720)Termination reason: Refutation not found, incomplete strategy
% 6.25/1.22 % (4182720)Time elapsed: 0.003 s
% 6.25/1.22 % (4182720)Peak memory usage: 12 MB
% 6.25/1.22 % (4182720)Instructions burned: 3 (million)
% 6.25/1.22 % (4182720)------------------------------
% 6.25/1.22 % (4182720)------------------------------
% 6.25/1.22 % (4182689)Instruction limit reached!
% 6.25/1.22 % (4182689)------------------------------
% 6.25/1.22 % (4182689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.25/1.22 % (4182689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.25/1.22 % (4182689)CaDiCaL version: 2.1.3
% 6.25/1.22 % (4182689)Termination reason: Instruction limit
% 6.25/1.22 % (4182689)Termination phase: Saturation
% 6.25/1.22 % (4182689)Time elapsed: 0.299 s
% 6.25/1.22 % (4182689)Peak memory usage: 16 MB
% 6.25/1.22 % (4182689)Instructions burned: 316 (million)
% 6.25/1.22 % (4182717)Instruction limit reached!
% 6.25/1.22 % (4182717)------------------------------
% 6.25/1.22 % (4182717)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.25/1.22 % (4182717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.25/1.22 % (4182717)CaDiCaL version: 2.1.3
% 6.25/1.22 % (4182717)Termination reason: Instruction limit
% 6.25/1.22 % (4182717)Termination phase: Saturation
% 6.25/1.22 % (4182717)Time elapsed: 0.044 s
% 6.25/1.22 % (4182717)Peak memory usage: 12 MB
% 6.25/1.22 % (4182717)Instructions burned: 98 (million)
% 6.25/1.22 % (4182724)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=1602205300:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/515Mi)
% 6.25/1.22 % (4182722)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=1013803238:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/874Mi)
% 6.25/1.22 % (4182724)Refutation not found, incomplete strategy
% 6.25/1.22 % (4182724)------------------------------
% 6.25/1.22 % (4182724)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.25/1.22 % (4182724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.25/1.22 % (4182724)CaDiCaL version: 2.1.3
% 6.25/1.22 % (4182724)Termination reason: Refutation not found, incomplete strategy
% 6.25/1.22 % (4182724)Time elapsed: 0.006 s
% 6.25/1.22 % (4182724)Peak memory usage: 13 MB
% 6.25/1.22 % (4182724)Instructions burned: 10 (million)
% 6.25/1.22 % (4182724)------------------------------
% 6.25/1.22 % (4182724)------------------------------
% 6.25/1.22 % (4182722)Refutation not found, incomplete strategy
% 6.25/1.22 % (4182722)------------------------------
% 6.25/1.22 % (4182722)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.25/1.22 % (4182722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.25/1.22 % (4182722)CaDiCaL version: 2.1.3
% 6.25/1.22 % (4182722)Termination reason: Refutation not found, incomplete strategy
% 6.25/1.22 % (4182722)Time elapsed: 0.009 s
% 6.25/1.22 % (4182722)Peak memory usage: 12 MB
% 6.25/1.22 % (4182722)Instructions burned: 10 (million)
% 6.25/1.22 % (4182722)------------------------------
% 6.25/1.22 % (4182722)------------------------------
% 6.25/1.22 % (4182726)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=2185212364:i=44:ep=R:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/44Mi)
% 6.25/1.22 % (4182730)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=2986811809:i=450:rtra=on:ixr=off:ntd=on_2993 on theBenchmark for (2993ds/450Mi)
% 6.25/1.22 % (4182725)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=2023228337:st=1.5:i=130:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/130Mi)
% 6.25/1.22 % (4182729)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=4092369671:s2a=on:i=571:nm=16:rtra=on_2993 on theBenchmark for (2993ds/571Mi)
% 6.25/1.22 % (4182725)Refutation not found, incomplete strategy
% 6.25/1.22 % (4182725)------------------------------
% 6.25/1.22 % (4182725)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.61/1.39 % (4182725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.61/1.39 % (4182725)CaDiCaL version: 2.1.3
% 6.61/1.39 % (4182725)Termination reason: Refutation not found, incomplete strategy
% 6.61/1.39 % (4182725)Time elapsed: 0.006 s
% 6.61/1.39 % (4182725)Peak memory usage: 12 MB
% 6.61/1.39 % (4182725)Instructions burned: 6 (million)
% 6.61/1.39 % (4182729)Refutation not found, incomplete strategy
% 6.61/1.39 % (4182729)------------------------------
% 6.61/1.39 % (4182729)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.61/1.39 % (4182729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.61/1.39 % (4182729)CaDiCaL version: 2.1.3
% 6.61/1.39 % (4182729)Termination reason: Refutation not found, incomplete strategy
% 6.61/1.39 % (4182729)Time elapsed: 0.004 s
% 6.61/1.39 % (4182729)Peak memory usage: 12 MB
% 6.61/1.39 % (4182729)Instructions burned: 6 (million)
% 6.61/1.39 % (4182725)------------------------------
% 6.61/1.39 % (4182725)------------------------------
% 6.61/1.39 % (4182729)------------------------------
% 6.61/1.39 % (4182729)------------------------------
% 6.61/1.39 % (4182735)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=4198578328:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/95Mi)
% 6.61/1.39 % (4182726)Instruction limit reached!
% 6.61/1.39 % (4182726)------------------------------
% 6.61/1.39 % (4182726)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.61/1.39 % (4182726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.61/1.39 % (4182726)CaDiCaL version: 2.1.3
% 6.61/1.39 % (4182726)Termination reason: Instruction limit
% 6.61/1.39 % (4182726)Termination phase: Saturation
% 6.61/1.39 % (4182726)Time elapsed: 0.041 s
% 6.61/1.39 % (4182726)Peak memory usage: 12 MB
% 6.61/1.39 % (4182726)Instructions burned: 44 (million)
% 6.61/1.39 % (4182736)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=1103491872:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2993 on theBenchmark for (2993ds/65Mi)
% 6.61/1.39 % (4182714)Instruction limit reached!
% 6.61/1.39 % (4182714)------------------------------
% 6.61/1.39 % (4182714)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.61/1.39 % (4182714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.61/1.39 % (4182714)CaDiCaL version: 2.1.3
% 6.61/1.39 % (4182714)Termination reason: Instruction limit
% 6.61/1.39 % (4182714)Termination phase: Saturation
% 6.61/1.39 % (4182714)Time elapsed: 0.152 s
% 6.61/1.39 % (4182714)Peak memory usage: 13 MB
% 6.61/1.39 % (4182714)Instructions burned: 180 (million)
% 6.61/1.39 % (4182739)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=2390750798: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_2992 on theBenchmark for (2992ds/105Mi)
% 6.61/1.39 % (4182740)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=516474445:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2992 on theBenchmark for (2992ds/5755Mi)
% 6.61/1.39 % (4182736)Instruction limit reached!
% 6.61/1.39 % (4182736)------------------------------
% 6.61/1.39 % (4182736)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.61/1.39 % (4182736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.61/1.39 % (4182736)CaDiCaL version: 2.1.3
% 6.61/1.39 % (4182736)Termination reason: Instruction limit
% 6.61/1.39 % (4182736)Termination phase: Saturation
% 6.61/1.39 % (4182736)Time elapsed: 0.060 s
% 6.61/1.39 % (4182736)Peak memory usage: 12 MB
% 6.61/1.39 % (4182736)Instructions burned: 66 (million)
% 6.61/1.39 % (4182735)Instruction limit reached!
% 6.61/1.39 % (4182735)------------------------------
% 6.61/1.39 % (4182735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.61/1.39 % (4182735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.61/1.39 % (4182735)CaDiCaL version: 2.1.3
% 6.61/1.39 % (4182735)Termination reason: Instruction limit
% 6.61/1.39 % (4182735)Termination phase: Saturation
% 6.61/1.39 % (4182735)Time elapsed: 0.085 s
% 6.61/1.39 % (4182735)Peak memory usage: 12 MB
% 7.10/1.52 % (4182735)Instructions burned: 95 (million)
% 7.10/1.52 % (4182743)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=2040121939:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/375Mi)
% 7.10/1.52 % (4182743)Refutation not found, incomplete strategy
% 7.10/1.52 % (4182743)------------------------------
% 7.10/1.52 % (4182743)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.10/1.52 % (4182743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.10/1.52 % (4182743)CaDiCaL version: 2.1.3
% 7.10/1.52 % (4182743)Termination reason: Refutation not found, incomplete strategy
% 7.10/1.52 % (4182743)Time elapsed: 0.008 s
% 7.10/1.52 % (4182743)Peak memory usage: 12 MB
% 7.10/1.52 % (4182743)Instructions burned: 8 (million)
% 7.10/1.52 % (4182743)------------------------------
% 7.10/1.52 % (4182743)------------------------------
% 7.10/1.52 % (4182744)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=602216053:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2991 on theBenchmark for (2991ds/495Mi)
% 7.10/1.52 % (4182739)Instruction limit reached!
% 7.10/1.52 % (4182739)------------------------------
% 7.10/1.52 % (4182739)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.10/1.52 % (4182739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.10/1.52 % (4182739)CaDiCaL version: 2.1.3
% 7.10/1.52 % (4182739)Termination reason: Instruction limit
% 7.10/1.52 % (4182739)Termination phase: Saturation
% 7.10/1.52 % (4182739)Time elapsed: 0.095 s
% 7.10/1.52 % (4182739)Peak memory usage: 13 MB
% 7.10/1.52 % (4182739)Instructions burned: 106 (million)
% 7.10/1.52 % (4182746)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=2400548229:cond=on:i=34:hud=10:nm=10:rtra=on_2991 on theBenchmark for (2991ds/34Mi)
% 7.10/1.52 % (4182748)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=1917753015:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2991 on theBenchmark for (2991ds/91Mi)
% 7.10/1.52 % (4182730)Instruction limit reached!
% 7.10/1.52 % (4182730)------------------------------
% 7.10/1.52 % (4182730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.10/1.52 % (4182730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.10/1.52 % (4182730)CaDiCaL version: 2.1.3
% 7.10/1.52 % (4182730)Termination reason: Instruction limit
% 7.10/1.52 % (4182730)Termination phase: Saturation
% 7.10/1.52 % (4182730)Time elapsed: 0.200 s
% 7.10/1.52 % (4182730)Peak memory usage: 13 MB
% 7.10/1.52 % (4182730)Instructions burned: 451 (million)
% 7.10/1.52 % (4182746)Instruction limit reached!
% 7.10/1.52 % (4182746)------------------------------
% 7.10/1.52 % (4182746)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.10/1.52 % (4182746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.10/1.52 % (4182746)CaDiCaL version: 2.1.3
% 7.10/1.52 % (4182746)Termination reason: Instruction limit
% 7.10/1.52 % (4182746)Termination phase: Saturation
% 7.10/1.52 % (4182746)Time elapsed: 0.031 s
% 7.10/1.52 % (4182746)Peak memory usage: 12 MB
% 7.10/1.52 % (4182746)Instructions burned: 34 (million)
% 7.10/1.52 % (4182751)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=2109932245:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2991 on theBenchmark for (2991ds/66Mi)
% 7.10/1.52 % (4182751)Refutation not found, incomplete strategy
% 7.10/1.52 % (4182751)------------------------------
% 7.10/1.52 % (4182751)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.10/1.52 % (4182751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.10/1.52 % (4182751)CaDiCaL version: 2.1.3
% 7.10/1.52 % (4182751)Termination reason: Refutation not found, incomplete strategy
% 7.10/1.52 % (4182751)Time elapsed: 0.002 s
% 7.10/1.52 % (4182751)Peak memory usage: 12 MB
% 7.10/1.52 % (4182751)Instructions burned: 3 (million)
% 7.10/1.52 % (4182751)------------------------------
% 7.10/1.52 % (4182751)------------------------------
% 7.10/1.52 % (4182752)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=1590619567:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2991 on theBenchmark for (2991ds/22Mi)
% 7.10/1.52 % (4182752)Instruction limit reached!
% 7.10/1.52 % (4182752)------------------------------
% 7.10/1.52 % (4182752)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.10/1.52 % (4182752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.10/1.52 % (4182752)CaDiCaL version: 2.1.3
% 7.10/1.52 % (4182752)Termination reason: Instruction limit
% 7.10/1.52 % (4182752)Termination phase: Saturation
% 7.10/1.52 % (4182752)Time elapsed: 0.011 s
% 7.10/1.52 % (4182752)Peak memory usage: 12 MB
% 7.10/1.52 % (4182752)Instructions burned: 23 (million)
% 7.10/1.52 % (4182754)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=1491227577:i=338:bd=all:ins=4:rtra=on_2990 on theBenchmark for (2990ds/338Mi)
% 7.10/1.52 % (4182756)lrs+10_1_sil=128000:si=on:urr=on:random_seed=563007878:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2990 on theBenchmark for (2990ds/28Mi)
% 7.10/1.52 % (4182748)Instruction limit reached!
% 7.10/1.52 % (4182748)------------------------------
% 7.10/1.52 % (4182748)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.10/1.52 % (4182748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.10/1.52 % (4182748)CaDiCaL version: 2.1.3
% 7.10/1.52 % (4182748)Termination reason: Instruction limit
% 7.10/1.52 % (4182748)Termination phase: Saturation
% 7.10/1.52 % (4182748)Time elapsed: 0.073 s
% 7.10/1.52 % (4182748)Peak memory usage: 13 MB
% 7.10/1.52 % (4182748)Instructions burned: 91 (million)
% 7.10/1.52 % (4182756)Instruction limit reached!
% 7.10/1.52 % (4182756)------------------------------
% 7.10/1.52 % (4182756)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.10/1.52 % (4182756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.10/1.52 % (4182756)CaDiCaL version: 2.1.3
% 7.10/1.52 % (4182756)Termination reason: Instruction limit
% 7.10/1.52 % (4182756)Termination phase: Saturation
% 7.10/1.52 % (4182756)Time elapsed: 0.016 s
% 7.10/1.52 % (4182756)Peak memory usage: 12 MB
% 7.10/1.52 % (4182756)Instructions burned: 28 (million)
% 7.10/1.52 % (4182759)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 7.10/1.52 % (4182759)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=3452029996:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2990 on theBenchmark for (2990ds/137Mi)
% 7.10/1.52 % (4182760)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=752898650:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2990 on theBenchmark for (2990ds/340Mi)
% 7.10/1.52 % (4182759)Instruction limit reached!
% 7.10/1.52 % (4182759)------------------------------
% 7.10/1.52 % (4182759)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.10/1.52 % (4182759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.10/1.52 % (4182759)CaDiCaL version: 2.1.3
% 7.10/1.52 % (4182759)Termination reason: Instruction limit
% 7.10/1.52 % (4182759)Termination phase: Saturation
% 7.10/1.52 % (4182759)Time elapsed: 0.064 s
% 7.10/1.52 % (4182759)Peak memory usage: 13 MB
% 7.10/1.52 % (4182759)Instructions burned: 137 (million)
% 7.10/1.52 % (4182763)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=1389611232:i=227:sd=1:bd=all:rtra=on:ss=axioms_2989 on theBenchmark for (2989ds/227Mi)
% 7.10/1.52 % (4182763)Refutation not found, incomplete strategy
% 7.10/1.52 % (4182763)------------------------------
% 7.10/1.52 % (4182763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.10/1.52 % (4182763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.10/1.52 % (4182763)CaDiCaL version: 2.1.3
% 7.10/1.52 % (4182763)Termination reason: Refutation not found, incomplete strategy
% 7.10/1.52 % (4182763)Time elapsed: 0.002 s
% 7.10/1.52 % (4182763)Peak memory usage: 12 MB
% 7.10/1.52 % (4182763)Instructions burned: 3 (million)
% 7.10/1.52 % (4182763)------------------------------
% 7.10/1.52 % (4182763)------------------------------
% 7.10/1.52 % (4182765)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 7.10/1.52 % (4182765)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=3321268638:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2989 on theBenchmark for (2989ds/373Mi)
% 7.10/1.52 % (4182690)Instruction limit reached!
% 7.10/1.52 % (4182690)------------------------------
% 7.10/1.52 % (4182690)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.10/1.52 % (4182690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.10/1.52 % (4182690)CaDiCaL version: 2.1.3
% 7.10/1.52 % (4182690)Termination reason: Instruction limit
% 7.10/1.52 % (4182690)Termination phase: Saturation
% 7.10/1.52 % (4182690)Time elapsed: 0.743 s
% 7.10/1.52 % (4182690)Peak memory usage: 17 MB
% 7.10/1.52 % (4182690)Instructions burned: 853 (million)
% 7.10/1.52 % (4182767)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=3459858458:i=116:ep=RSTC:rtra=on:ntd=on_2989 on theBenchmark for (2989ds/116Mi)
% 7.10/1.52 % (4182767)Instruction limit reached!
% 7.10/1.52 % (4182767)------------------------------
% 7.10/1.52 % (4182767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.10/1.52 % (4182767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.10/1.52 % (4182767)CaDiCaL version: 2.1.3
% 7.10/1.52 % (4182767)Termination reason: Instruction limit
% 7.10/1.52 % (4182767)Termination phase: Saturation
% 7.10/1.52 % (4182767)Time elapsed: 0.074 s
% 7.10/1.52 % (4182767)Peak memory usage: 12 MB
% 7.10/1.52 % (4182767)Instructions burned: 117 (million)
% 7.10/1.52 % (4182760) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-4182602-4182760"...
% 7.10/1.52 % (4182769)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=533075898:i=575:rtra=on_2988 on theBenchmark for (2988ds/575Mi)
% 7.10/1.52 % (4182667)Instruction limit reached!
% 7.10/1.52 % (4182667)------------------------------
% 7.10/1.52 % (4182667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.10/1.52 % (4182667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.10/1.52 % (4182667)CaDiCaL version: 2.1.3
% 7.10/1.52 % (4182667)Termination reason: Instruction limit
% 7.10/1.52 % (4182667)Termination phase: Saturation
% 7.10/1.52 % (4182667)Time elapsed: 0.972 s
% 7.10/1.52 % (4182667)Peak memory usage: 14 MB
% 7.10/1.52 % (4182667)Instructions burned: 1240 (million)
% 7.10/1.52 % (4182760)...printing done.
% 7.10/1.52 % (4182760)Refutation found. Thanks to Tanya!
% 7.10/1.52 % SZS status Theorem for theBenchmark
% 7.10/1.52 % SZS output start Proof for theBenchmark
% 7.10/1.52 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 7.10/1.52 thf(type_def_6, type, individuals: $tType).
% 7.10/1.52 thf(func_def_1, type, prop_a: ($i > $o)).
% 7.10/1.52 thf(func_def_2, type, prop_b: ($i > $o)).
% 7.10/1.52 thf(func_def_3, type, prop_c: ($i > $o)).
% 7.10/1.52 thf(func_def_4, type, mfalse: ($i > $o)).
% 7.10/1.52 thf(func_def_5, type, mtrue: ($i > $o)).
% 7.10/1.52 thf(func_def_6, type, mnot: (($i > $o) > $i > $o)).
% 7.10/1.52 thf(func_def_8, type, mor: (($i > $o) > ($i > $o) > $i > $o)).
% 7.10/1.52 thf(func_def_9, type, mand: (($i > $o) > ($i > $o) > $i > $o)).
% 7.10/1.52 thf(func_def_10, type, mimpl: (($i > $o) > ($i > $o) > $i > $o)).
% 7.10/1.52 thf(func_def_11, type, miff: (($i > $o) > ($i > $o) > $i > $o)).
% 7.10/1.52 thf(func_def_12, type, mbox: (($i > $i > $o) > ($i > $o) > $i > $o)).
% 7.10/1.52 thf(func_def_13, type, mdia: (($i > $i > $o) > ($i > $o) > $i > $o)).
% 7.10/1.52 thf(func_def_14, type, mall: ((individuals > $i > $o) > $i > $o)).
% 7.10/1.52 thf(func_def_15, type, mexists: ((individuals > $i > $o) > $i > $o)).
% 7.10/1.52 thf(func_def_16, type, mvalid: (($i > $o) > $o)).
% 7.10/1.52 thf(func_def_17, type, msatisfiable: (($i > $o) > $o)).
% 7.10/1.52 thf(func_def_18, type, mcountersatisfiable: (($i > $o) > $o)).
% 7.10/1.52 thf(func_def_19, type, minvalid: (($i > $o) > $o)).
% 7.10/1.52 thf(func_def_20, type, rel: ($i > $i > $o)).
% 7.10/1.52 thf(func_def_21, type, icl_atom: (($i > $o) > $i > $o)).
% 7.10/1.52 thf(func_def_22, type, icl_princ: (($i > $o) > $i > $o)).
% 7.10/1.52 thf(func_def_23, type, icl_and: (($i > $o) > ($i > $o) > $i > $o)).
% 7.10/1.52 thf(func_def_24, type, icl_or: (($i > $o) > ($i > $o) > $i > $o)).
% 7.10/1.52 thf(func_def_25, type, icl_impl: (($i > $o) > ($i > $o) > $i > $o)).
% 7.10/1.52 thf(func_def_26, type, icl_true: ($i > $o)).
% 7.10/1.52 thf(func_def_27, type, icl_false: ($i > $o)).
% 7.10/1.52 thf(func_def_28, type, icl_says: (($i > $o) > ($i > $o) > $i > $o)).
% 7.10/1.52 thf(func_def_29, type, iclval: (($i > $o) > $o)).
% 7.10/1.52 thf(func_def_30, type, icl_impl_princ: (($i > $o) > ($i > $o) > $i > $o)).
% 7.10/1.52 thf(func_def_31, type, admin: ($i > $o)).
% 7.10/1.52 thf(func_def_32, type, bob: ($i > $o)).
% 7.10/1.52 thf(func_def_33, type, alice: ($i > $o)).
% 7.10/1.52 thf(func_def_34, type, deletefile1: ($i > $o)).
% 7.10/1.52 thf(func_def_35, type, db1: !>[X0: $tType]:(X0)).
% 7.10/1.52 thf(func_def_36, type, db0: !>[X0: $tType]:(X0)).
% 7.10/1.52 thf(func_def_37, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 7.10/1.52 thf(func_def_38, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 7.10/1.52 thf(func_def_39, type, db2: !>[X0: $tType]:(X0)).
% 7.10/1.52 thf(func_def_42, type, vNOT: ($o > $o)).
% 7.10/1.52 thf(func_def_43, type, vIMP: ($o > $o > $o)).
% 7.10/1.52 thf(func_def_44, type, db3: !>[X0: $tType]:(X0)).
% 7.10/1.52 thf(func_def_45, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 7.10/1.52 thf(func_def_46, type, vAND: ($o > $o > $o)).
% 7.10/1.52 thf(func_def_47, type, vOR: ($o > $o > $o)).
% 7.10/1.52 thf(func_def_48, type, sF0: $o).
% 7.10/1.52 thf(func_def_49, type, sF1: $o).
% 7.10/1.52 thf(func_def_50, type, db4: !>[X0: $tType]:(X0)).
% 7.10/1.52 thf(func_def_54, type, sK5: (($i > $o) > $i > $i)).
% 7.10/1.52 thf(func_def_61, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 7.10/1.52 thf(f3,axiom,(
% 7.10/1.52 (mnot = (^[X0 : ($i > $o), X1 : $i] : (~(X0 @ X1))))),
% 7.10/1.52 file('/export/starexec/sandbox2/benchmark/Axioms/LCL008^0.ax',mnot)).
% 7.10/1.52 thf(f4,axiom,(
% 7.10/1.52 (mor = (^[X0 : ($i > $o), X1 : ($i > $o), X2 : $i] : ((X1 @ X2) | (X0 @ X2))))),
% 7.10/1.52 file('/export/starexec/sandbox2/benchmark/Axioms/LCL008^0.ax',mor)).
% 7.10/1.52 thf(f6,axiom,(
% 7.10/1.52 (mimpl = (^[X0 : ($i > $o), X1 : ($i > $o)] : ((mor @ (mnot @ X0) @ X1))))),
% 7.10/1.52 file('/export/starexec/sandbox2/benchmark/Axioms/LCL008^0.ax',mimpl)).
% 7.10/1.52 thf(f8,axiom,(
% 7.10/1.52 (mbox = (^[X0 : ($i > $i > $o), X1 : ($i > $o), X2 : $i] : (! [X3 : $i] : ((X0 @ X2 @ X3) => (X1 @ X3)))))),
% 7.10/1.52 file('/export/starexec/sandbox2/benchmark/Axioms/LCL008^0.ax',mbox)).
% 7.10/1.52 thf(f12,axiom,(
% 7.10/1.52 (mvalid = (^[X0 : ($i > $o)] : (! [X1 : $i] : (X0 @ X1))))),
% 7.10/1.52 file('/export/starexec/sandbox2/benchmark/Axioms/LCL008^0.ax',mvalid)).
% 7.10/1.52 thf(f16,axiom,(
% 7.10/1.52 (icl_atom = (^[X0 : ($i > $o)] : ((mbox @ rel @ X0))))),
% 7.10/1.52 file('/export/starexec/sandbox2/benchmark/Axioms/SWV008^0.ax',icl_atom)).
% 7.10/1.52 thf(f17,axiom,(
% 7.10/1.52 (icl_princ = (^[X0 : ($i > $o)] : (X0)))),
% 7.10/1.52 file('/export/starexec/sandbox2/benchmark/Axioms/SWV008^0.ax',icl_princ)).
% 7.10/1.52 thf(f20,axiom,(
% 7.10/1.52 (icl_impl = (^[X0 : ($i > $o), X1 : ($i > $o)] : ((mbox @ rel @ (mimpl @ X0 @ X1)))))),
% 7.10/1.52 file('/export/starexec/sandbox2/benchmark/Axioms/SWV008^0.ax',icl_impl)).
% 7.10/1.52 thf(f23,axiom,(
% 7.10/1.52 ((^[X0 : ($i > $o), X1 : ($i > $o)] : ((mbox @ rel @ (mor @ X0 @ X1)))) = icl_says)),
% 7.10/1.52 file('/export/starexec/sandbox2/benchmark/Axioms/SWV008^0.ax',icl_says)).
% 7.10/1.52 thf(f24,axiom,(
% 7.10/1.52 (iclval = (^[X0 : ($i > $o)] : ((mvalid @ X0))))),
% 7.10/1.52 file('/export/starexec/sandbox2/benchmark/Axioms/SWV008^0.ax',icl_s4_valid)).
% 7.10/1.52 thf(f25,axiom,(
% 7.10/1.52 ! [X0 : ($i > $o)] : (mvalid @ (mimpl @ (mbox @ rel @ X0) @ X0))),
% 7.10/1.52 file('/export/starexec/sandbox2/benchmark/Axioms/SWV008^1.ax',refl_axiom)).
% 7.10/1.52 thf(f27,axiom,(
% 7.10/1.52 (icl_impl_princ = (^[X0 : ($i > $o), X1 : ($i > $o)] : ((mbox @ rel @ (mimpl @ X0 @ X1)))))),
% 7.10/1.52 file('/export/starexec/sandbox2/benchmark/Axioms/SWV008^2.ax',icl_impl_princ)).
% 7.10/1.52 thf(f28,axiom,(
% 7.10/1.52 (iclval @ (icl_impl @ (icl_says @ (icl_princ @ admin) @ (icl_atom @ deletefile1)) @ (icl_atom @ deletefile1)))),
% 7.10/1.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1)).
% 7.10/1.52 thf(f29,axiom,(
% 7.10/1.52 (iclval @ (icl_says @ (icl_princ @ admin) @ (icl_impl @ (icl_says @ (icl_princ @ bob) @ (icl_atom @ deletefile1)) @ (icl_atom @ deletefile1))))),
% 7.10/1.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2)).
% 7.10/1.52 thf(f30,axiom,(
% 7.10/1.52 (iclval @ (icl_says @ (icl_princ @ bob) @ (icl_impl_princ @ (icl_princ @ alice) @ (icl_princ @ bob))))),
% 7.10/1.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3)).
% 7.10/1.52 thf(f31,axiom,(
% 7.10/1.52 (iclval @ (icl_says @ (icl_princ @ alice) @ (icl_atom @ deletefile1)))),
% 7.10/1.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4)).
% 7.10/1.52 thf(f32,conjecture,(
% 7.10/1.52 (iclval @ (icl_atom @ deletefile1))),
% 7.10/1.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj)).
% 7.10/1.52 thf(f33,negated_conjecture,(
% 7.10/1.52 ~(iclval @ (icl_atom @ deletefile1))),
% 7.10/1.52 inference(negated_conjecture,[status(cth)],[f32])).
% 7.10/1.52 thf(f34,plain,(
% 7.10/1.52 (icl_says = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mbox @ rel @ (mor @ Y0 @ Y1))))))),
% 7.10/1.52 inference(fool_elimination,[],[f23])).
% 7.10/1.52 thf(f37,plain,(
% 7.10/1.52 (iclval @ (icl_impl @ (icl_says @ (icl_princ @ admin) @ (icl_atom @ deletefile1)) @ (icl_atom @ deletefile1)))),
% 7.10/1.52 inference(rectify,[],[f28])).
% 7.10/1.52 thf(f38,plain,(
% 7.10/1.52 (((iclval @ (icl_impl @ (icl_says @ (icl_princ @ admin) @ (icl_atom @ deletefile1)) @ (icl_atom @ deletefile1)))) = $true)),
% 7.10/1.52 inference(fool_elimination,[],[f37])).
% 7.10/1.52 thf(f42,plain,(
% 7.10/1.52 (mnot = (^[X0 : ($i > $o), X1 : $i] : (~(X0 @ X1))))),
% 7.10/1.52 inference(rectify,[],[f3])).
% 7.10/1.52 thf(f43,plain,(
% 7.10/1.52 (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1))))))),
% 7.10/1.52 inference(fool_elimination,[],[f42])).
% 7.10/1.52 thf(f45,plain,(
% 7.10/1.52 (iclval @ (icl_says @ (icl_princ @ bob) @ (icl_impl_princ @ (icl_princ @ alice) @ (icl_princ @ bob))))),
% 7.10/1.52 inference(rectify,[],[f30])).
% 7.10/1.52 thf(f46,plain,(
% 7.10/1.52 (((iclval @ (icl_says @ (icl_princ @ bob) @ (icl_impl_princ @ (icl_princ @ alice) @ (icl_princ @ bob))))) = $true)),
% 7.10/1.52 inference(fool_elimination,[],[f45])).
% 7.10/1.52 thf(f47,plain,(
% 7.10/1.52 (mbox = (^[X0 : ($i > $i > $o), X1 : ($i > $o), X2 : $i] : (! [X3 : $i] : ((X0 @ X2 @ X3) => (X1 @ X3)))))),
% 7.10/1.52 inference(rectify,[],[f8])).
% 7.10/1.52 thf(f48,plain,(
% 7.10/1.52 (mbox = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y2 @ Y3) => (Y1 @ Y3))))))))))),
% 7.10/1.52 inference(fool_elimination,[],[f47])).
% 7.10/1.52 thf(f51,plain,(
% 7.10/1.52 (icl_atom = (^[Y0 : $i > $o]: (mbox @ rel @ Y0)))),
% 7.10/1.52 inference(fool_elimination,[],[f16])).
% 7.10/1.52 thf(f52,plain,(
% 7.10/1.52 (icl_princ = (^[Y0 : $i > $o]: (Y0)))),
% 7.10/1.52 inference(fool_elimination,[],[f17])).
% 7.10/1.52 thf(f54,plain,(
% 7.10/1.52 (iclval = (^[Y0 : $i > $o]: (mvalid @ Y0)))),
% 7.10/1.52 inference(fool_elimination,[],[f24])).
% 7.10/1.52 thf(f55,plain,(
% 7.10/1.52 ! [X0 : ($i > $o)] : (mvalid @ (mimpl @ (mbox @ rel @ X0) @ X0))),
% 7.10/1.52 inference(rectify,[],[f25])).
% 7.10/1.52 thf(f56,plain,(
% 7.10/1.52 ($true = ((!! @ ($i > $o) @ (^[Y0 : $i > $o]: (mvalid @ (mimpl @ (mbox @ rel @ Y0) @ Y0))))))),
% 7.10/1.52 inference(fool_elimination,[],[f55])).
% 7.10/1.52 thf(f57,plain,(
% 7.10/1.52 (icl_impl_princ = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mbox @ rel @ (mimpl @ Y0 @ Y1))))))),
% 7.10/1.52 inference(fool_elimination,[],[f27])).
% 7.10/1.52 thf(f58,plain,(
% 7.10/1.52 (mimpl = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mor @ (mnot @ Y0) @ Y1)))))),
% 7.10/1.52 inference(fool_elimination,[],[f6])).
% 7.10/1.52 thf(f60,plain,(
% 7.10/1.52 (iclval @ (icl_says @ (icl_princ @ alice) @ (icl_atom @ deletefile1)))),
% 7.10/1.52 inference(rectify,[],[f31])).
% 7.10/1.52 thf(f61,plain,(
% 7.10/1.52 (((iclval @ (icl_says @ (icl_princ @ alice) @ (icl_atom @ deletefile1)))) = $true)),
% 7.10/1.52 inference(fool_elimination,[],[f60])).
% 7.10/1.52 thf(f68,plain,(
% 7.10/1.52 (mvalid = (^[X0 : ($i > $o)] : (! [X1 : $i] : (X0 @ X1))))),
% 7.10/1.52 inference(rectify,[],[f12])).
% 7.10/1.52 thf(f69,plain,(
% 7.10/1.52 (mvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))),
% 7.10/1.52 inference(fool_elimination,[],[f68])).
% 7.10/1.52 thf(f74,plain,(
% 7.10/1.52 ~(iclval @ (icl_atom @ deletefile1))),
% 7.10/1.52 inference(rectify,[],[f33])).
% 7.10/1.52 thf(f75,plain,(
% 7.10/1.52 (((~ (iclval @ (icl_atom @ deletefile1)))) = $true)),
% 7.10/1.52 inference(fool_elimination,[],[f74])).
% 7.10/1.52 thf(f78,plain,(
% 7.10/1.52 (mor = (^[X0 : ($i > $o), X1 : ($i > $o), X2 : $i] : ((X1 @ X2) | (X0 @ X2))))),
% 7.10/1.52 inference(rectify,[],[f4])).
% 7.10/1.52 thf(f79,plain,(
% 7.10/1.52 (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2))))))))),
% 7.10/1.52 inference(fool_elimination,[],[f78])).
% 7.10/1.52 thf(f80,plain,(
% 7.10/1.52 (iclval @ (icl_says @ (icl_princ @ admin) @ (icl_impl @ (icl_says @ (icl_princ @ bob) @ (icl_atom @ deletefile1)) @ (icl_atom @ deletefile1))))),
% 7.10/1.52 inference(rectify,[],[f29])).
% 7.10/1.52 thf(f81,plain,(
% 7.10/1.52 (((iclval @ (icl_says @ (icl_princ @ admin) @ (icl_impl @ (icl_says @ (icl_princ @ bob) @ (icl_atom @ deletefile1)) @ (icl_atom @ deletefile1))))) = $true)),
% 7.10/1.52 inference(fool_elimination,[],[f80])).
% 7.10/1.52 thf(f83,plain,(
% 7.10/1.52 (icl_impl = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mbox @ rel @ (mimpl @ Y0 @ Y1))))))),
% 7.10/1.52 inference(fool_elimination,[],[f20])).
% 7.10/1.52 thf(f87,plain,(
% 7.10/1.52 (((iclval @ (icl_says @ (icl_princ @ alice) @ (icl_atom @ deletefile1)))) = $true)),
% 7.10/1.52 inference(cnf_transformation,[],[f61])).
% 7.10/1.52 thf(f88,plain,(
% 7.10/1.52 (iclval = (^[Y0 : $i > $o]: (mvalid @ Y0)))),
% 7.10/1.52 inference(cnf_transformation,[],[f54])).
% 7.10/1.52 thf(f89,plain,(
% 7.10/1.52 (icl_atom = (^[Y0 : $i > $o]: (mbox @ rel @ Y0)))),
% 7.10/1.52 inference(cnf_transformation,[],[f51])).
% 7.10/1.52 thf(f92,plain,(
% 7.10/1.52 (mvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))),
% 7.10/1.52 inference(cnf_transformation,[],[f69])).
% 7.10/1.52 thf(f93,plain,(
% 7.10/1.52 (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1))))))),
% 7.10/1.52 inference(cnf_transformation,[],[f43])).
% 7.10/1.52 thf(f94,plain,(
% 7.10/1.52 (((iclval @ (icl_says @ (icl_princ @ admin) @ (icl_impl @ (icl_says @ (icl_princ @ bob) @ (icl_atom @ deletefile1)) @ (icl_atom @ deletefile1))))) = $true)),
% 7.10/1.52 inference(cnf_transformation,[],[f81])).
% 7.10/1.52 thf(f95,plain,(
% 7.10/1.52 (icl_princ = (^[Y0 : $i > $o]: (Y0)))),
% 7.10/1.52 inference(cnf_transformation,[],[f52])).
% 7.10/1.52 thf(f97,plain,(
% 7.10/1.52 ($true = ((!! @ ($i > $o) @ (^[Y0 : $i > $o]: (mvalid @ (mimpl @ (mbox @ rel @ Y0) @ Y0))))))),
% 7.10/1.52 inference(cnf_transformation,[],[f56])).
% 7.10/1.52 thf(f100,plain,(
% 7.10/1.52 (((iclval @ (icl_impl @ (icl_says @ (icl_princ @ admin) @ (icl_atom @ deletefile1)) @ (icl_atom @ deletefile1)))) = $true)),
% 7.10/1.52 inference(cnf_transformation,[],[f38])).
% 7.10/1.52 thf(f101,plain,(
% 7.10/1.52 (icl_impl = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mbox @ rel @ (mimpl @ Y0 @ Y1))))))),
% 7.10/1.52 inference(cnf_transformation,[],[f83])).
% 7.10/1.52 thf(f102,plain,(
% 7.10/1.52 (((iclval @ (icl_says @ (icl_princ @ bob) @ (icl_impl_princ @ (icl_princ @ alice) @ (icl_princ @ bob))))) = $true)),
% 7.10/1.52 inference(cnf_transformation,[],[f46])).
% 7.10/1.52 thf(f103,plain,(
% 7.10/1.52 (icl_says = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mbox @ rel @ (mor @ Y0 @ Y1))))))),
% 7.10/1.52 inference(cnf_transformation,[],[f34])).
% 7.10/1.52 thf(f104,plain,(
% 7.10/1.52 (icl_impl_princ = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mbox @ rel @ (mimpl @ Y0 @ Y1))))))),
% 7.10/1.52 inference(cnf_transformation,[],[f57])).
% 7.10/1.52 thf(f110,plain,(
% 7.10/1.52 (((~ (iclval @ (icl_atom @ deletefile1)))) = $true)),
% 7.10/1.52 inference(cnf_transformation,[],[f75])).
% 7.10/1.52 thf(f112,plain,(
% 7.10/1.52 (mbox = (^[Y0 : $i > $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y2 @ Y3) => (Y1 @ Y3))))))))))),
% 7.10/1.52 inference(cnf_transformation,[],[f48])).
% 7.10/1.52 thf(f113,plain,(
% 7.10/1.52 (mimpl = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mor @ (mnot @ Y0) @ Y1)))))),
% 7.10/1.52 inference(cnf_transformation,[],[f58])).
% 7.10/1.52 thf(f115,plain,(
% 7.10/1.52 (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2))))))))),
% 7.10/1.52 inference(cnf_transformation,[],[f79])).
% 7.10/1.52 thf(f117,definition,(
% 7.10/1.52 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 7.10/1.52 introduced(theory,[fool_exhaustiveness_axiom])).
% 7.10/1.52 thf(f118,plain,(
% 7.10/1.52 (mimpl = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) | (Y3 @ Y4))))))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (~ (Y2 @ Y3))))) @ Y0) @ Y1)))))),
% 7.10/1.52 inference(definition_unfolding,[],[f113,f115,f93])).
% 7.10/1.52 thf(f120,plain,(
% 7.10/1.52 (icl_atom = (^[Y0 : $i > $o]: ((^[Y1 : $i > $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((Y1 @ Y3 @ Y4) => (Y2 @ Y4))))))))) @ rel @ Y0)))),
% 7.10/1.52 inference(definition_unfolding,[],[f89,f112])).
% 7.10/1.52 thf(f123,plain,(
% 7.10/1.52 (icl_impl = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((Y2 @ Y4 @ Y5) => (Y3 @ Y5))))))))) @ rel @ ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i > $o]: ((^[Y5 : $i > $o]: ((^[Y6 : $i]: ((Y4 @ Y6) | (Y5 @ Y6))))))) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (~ (Y4 @ Y5))))) @ Y2) @ Y3)))) @ Y0 @ Y1))))))),
% 7.10/1.52 inference(definition_unfolding,[],[f101,f112,f118])).
% 7.10/1.52 thf(f126,plain,(
% 7.10/1.52 (icl_says = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((Y2 @ Y4 @ Y5) => (Y3 @ Y5))))))))) @ rel @ ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) | (Y3 @ Y4))))))) @ Y0 @ Y1))))))),
% 7.10/1.52 inference(definition_unfolding,[],[f103,f112,f115])).
% 7.10/1.52 thf(f127,plain,(
% 7.10/1.52 (iclval = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: (Y1 @ Y2)))) @ Y0)))),
% 7.10/1.52 inference(definition_unfolding,[],[f88,f92])).
% 7.10/1.52 thf(f128,plain,(
% 7.10/1.52 (icl_impl_princ = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((Y2 @ Y4 @ Y5) => (Y3 @ Y5))))))))) @ rel @ ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i > $o]: ((^[Y5 : $i > $o]: ((^[Y6 : $i]: ((Y4 @ Y6) | (Y5 @ Y6))))))) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (~ (Y4 @ Y5))))) @ Y2) @ Y3)))) @ Y0 @ Y1))))))),
% 7.10/1.52 inference(definition_unfolding,[],[f104,f112,f118])).
% 7.10/1.52 thf(f129,plain,(
% 7.10/1.52 ($true = (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: (Y1 @ Y2)))) @ Y0)) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((Y2 @ Y4 @ Y5) => (Y3 @ Y5))))))))) @ rel @ ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) | (Y3 @ Y4))))))) @ Y0 @ Y1))))) @ ((^[Y0 : $i > $o]: (Y0)) @ alice) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((Y1 @ Y3 @ Y4) => (Y2 @ Y4))))))))) @ rel @ Y0)) @ deletefile1)))))),
% 7.10/1.52 inference(definition_unfolding,[],[f87,f127,f126,f95,f120])).
% 7.10/1.52 thf(f130,plain,(
% 7.10/1.52 ((((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: (Y1 @ Y2)))) @ Y0)) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((Y2 @ Y4 @ Y5) => (Y3 @ Y5))))))))) @ rel @ ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) | (Y3 @ Y4))))))) @ Y0 @ Y1))))) @ ((^[Y0 : $i > $o]: (Y0)) @ admin) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((Y2 @ Y4 @ Y5) => (Y3 @ Y5))))))))) @ rel @ ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i > $o]: ((^[Y5 : $i > $o]: ((^[Y6 : $i]: ((Y4 @ Y6) | (Y5 @ Y6))))))) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (~ (Y4 @ Y5))))) @ Y2) @ Y3)))) @ Y0 @ Y1))))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((Y2 @ Y4 @ Y5) => (Y3 @ Y5))))))))) @ rel @ ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) | (Y3 @ Y4))))))) @ Y0 @ Y1))))) @ ((^[Y0 : $i > $o]: (Y0)) @ bob) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((Y1 @ Y3 @ Y4) => (Y2 @ Y4))))))))) @ rel @ Y0)) @ deletefile1)) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((Y1 @ Y3 @ Y4) => (Y2 @ Y4))))))))) @ rel @ Y0)) @ deletefile1))))) = $true)),
% 7.10/1.52 inference(definition_unfolding,[],[f94,f127,f126,f95,f123,f126,f95,f120,f120])).
% 7.10/1.52 thf(f131,plain,(
% 7.10/1.52 ($true = ((!! @ ($i > $o) @ (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: (Y1 @ Y2)))) @ ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i > $o]: ((^[Y5 : $i]: ((Y3 @ Y5) | (Y4 @ Y5))))))) @ ((^[Y3 : $i > $o]: ((^[Y4 : $i]: (~ (Y3 @ Y4))))) @ Y1) @ Y2)))) @ ((^[Y1 : $i > $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((Y1 @ Y3 @ Y4) => (Y2 @ Y4))))))))) @ rel @ Y0) @ Y0))))))),
% 7.10/1.52 inference(definition_unfolding,[],[f97,f92,f118,f112])).
% 7.10/1.52 thf(f133,plain,(
% 7.10/1.52 ($true = (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: (Y1 @ Y2)))) @ Y0)) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((Y2 @ Y4 @ Y5) => (Y3 @ Y5))))))))) @ rel @ ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i > $o]: ((^[Y5 : $i > $o]: ((^[Y6 : $i]: ((Y4 @ Y6) | (Y5 @ Y6))))))) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (~ (Y4 @ Y5))))) @ Y2) @ Y3)))) @ Y0 @ Y1))))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((Y2 @ Y4 @ Y5) => (Y3 @ Y5))))))))) @ rel @ ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) | (Y3 @ Y4))))))) @ Y0 @ Y1))))) @ ((^[Y0 : $i > $o]: (Y0)) @ admin) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((Y1 @ Y3 @ Y4) => (Y2 @ Y4))))))))) @ rel @ Y0)) @ deletefile1)) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((Y1 @ Y3 @ Y4) => (Y2 @ Y4))))))))) @ rel @ Y0)) @ deletefile1)))))),
% 7.10/1.52 inference(definition_unfolding,[],[f100,f127,f123,f126,f95,f120,f120])).
% 7.10/1.52 thf(f134,plain,(
% 7.10/1.52 ($true = (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: (Y1 @ Y2)))) @ Y0)) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((Y2 @ Y4 @ Y5) => (Y3 @ Y5))))))))) @ rel @ ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) | (Y3 @ Y4))))))) @ Y0 @ Y1))))) @ ((^[Y0 : $i > $o]: (Y0)) @ bob) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: ((Y2 @ Y4 @ Y5) => (Y3 @ Y5))))))))) @ rel @ ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i > $o]: ((^[Y5 : $i > $o]: ((^[Y6 : $i]: ((Y4 @ Y6) | (Y5 @ Y6))))))) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (~ (Y4 @ Y5))))) @ Y2) @ Y3)))) @ Y0 @ Y1))))) @ ((^[Y0 : $i > $o]: (Y0)) @ alice) @ ((^[Y0 : $i > $o]: (Y0)) @ bob))))))),
% 7.10/1.52 inference(definition_unfolding,[],[f102,f127,f126,f95,f128,f95,f95])).
% 7.10/1.52 thf(f135,plain,(
% 7.10/1.52 (((~ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: (Y1 @ Y2)))) @ Y0)) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((Y1 @ Y3 @ Y4) => (Y2 @ Y4))))))))) @ rel @ Y0)) @ deletefile1)))) = $true)),
% 7.10/1.52 inference(definition_unfolding,[],[f110,f127,f120])).
% 7.10/1.52 thf(f136,definition,(
% 7.10/1.52 (sF0 = (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: (Y1 @ Y2)))) @ Y0)) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((Y1 @ Y3 @ Y4) => (Y2 @ Y4))))))))) @ rel @ Y0)) @ deletefile1))))),
% 7.10/1.52 introduced(definition,[new_symbols(definition,[sF0])],[function_definition])).
% 7.10/1.52 thf(f137,plain,(
% 7.10/1.52 ((((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: (Y1 @ Y2)))) @ Y0)) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((Y1 @ Y3 @ Y4) => (Y2 @ Y4))))))))) @ rel @ Y0)) @ deletefile1))) = sF0)),
% 7.10/1.52 inference(reorient_equations,[],[f136])).
% 7.10/1.52 thf(f138,definition,(
% 7.10/1.52 (sF1 = ((~ sF0)))),
% 7.10/1.52 introduced(definition,[new_symbols(definition,[sF1])],[function_definition])).
% 7.10/1.52 thf(f139,plain,(
% 7.10/1.52 ($true = sF1)),
% 7.10/1.52 inference(definition_folding,[],[f135,f138,f137])).
% 7.10/1.52 thf(f140,plain,(
% 7.10/1.52 ($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => ((~ (!! @ $i @ (^[Y2 : $i]: ((rel @ Y1 @ Y2) => ((admin @ Y2) | (!! @ $i @ (^[Y3 : $i]: ((rel @ Y2 @ Y3) => (deletefile1 @ Y3))))))))) | (!! @ $i @ (^[Y2 : $i]: ((rel @ Y1 @ Y2) => (deletefile1 @ Y2))))))))))))),
% 7.10/1.52 inference(beta-eta_normalization,[],[f133])).
% 7.10/1.52 thf(f142,plain,(
% 7.10/1.52 (((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => ((admin @ Y1) | (!! @ $i @ (^[Y2 : $i]: ((rel @ Y1 @ Y2) => ((~ (!! @ $i @ (^[Y3 : $i]: ((rel @ Y2 @ Y3) => ((bob @ Y3) | (!! @ $i @ (^[Y4 : $i]: ((rel @ Y3 @ Y4) => (deletefile1 @ Y4))))))))) | (!! @ $i @ (^[Y3 : $i]: ((rel @ Y2 @ Y3) => (deletefile1 @ Y3))))))))))))))) = $true)),
% 7.10/1.52 inference(beta-eta_normalization,[],[f130])).
% 7.10/1.52 thf(f143,plain,(
% 7.10/1.52 ($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => ((bob @ Y1) | (!! @ $i @ (^[Y2 : $i]: ((rel @ Y1 @ Y2) => ((~ (alice @ Y2)) | (bob @ Y2)))))))))))))),
% 7.10/1.52 inference(beta-eta_normalization,[],[f134])).
% 7.10/1.52 thf(f144,plain,(
% 7.10/1.52 ($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => ((alice @ Y1) | (!! @ $i @ (^[Y2 : $i]: ((rel @ Y1 @ Y2) => (deletefile1 @ Y2))))))))))))),
% 7.10/1.52 inference(beta-eta_normalization,[],[f129])).
% 7.10/1.52 thf(f145,plain,(
% 7.10/1.52 ($true = ((!! @ ($i > $o) @ (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: ((~ (!! @ $i @ (^[Y2 : $i]: ((rel @ Y1 @ Y2) => (Y0 @ Y2))))) | (Y0 @ Y1))))))))),
% 7.10/1.52 inference(beta-eta_normalization,[],[f131])).
% 7.10/1.52 thf(f146,plain,(
% 7.10/1.52 (sF0 = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => (deletefile1 @ Y1))))))))),
% 7.10/1.52 inference(beta-eta_normalization,[],[f137])).
% 7.10/1.52 thf(f155,plain,(
% 7.10/1.52 ( ! [X1 : ($i > $o)] : (($true = (((^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: ((~ (!! @ $i @ (^[Y2 : $i]: ((rel @ Y1 @ Y2) => (Y0 @ Y2))))) | (Y0 @ Y1))))) @ X1)))) )),
% 7.10/1.52 inference(pi_proxy_clausification,[],[f145])).
% 7.10/1.52 thf(f156,plain,(
% 7.10/1.52 ( ! [X1 : ($i > $o)] : ((((!! @ $i @ (^[Y0 : $i]: ((~ (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => (X1 @ Y1))))) | (X1 @ Y0))))) = $true)) )),
% 7.10/1.52 inference(beta-eta_normalization,[],[f155])).
% 7.10/1.52 thf(f157,plain,(
% 7.10/1.52 ( ! [X2 : $i,X1 : ($i > $o)] : (($true = (((^[Y0 : $i]: ((~ (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => (X1 @ Y1))))) | (X1 @ Y0))) @ X2)))) )),
% 7.10/1.52 inference(pi_proxy_clausification,[],[f156])).
% 7.10/1.52 thf(f158,plain,(
% 7.10/1.52 ( ! [X2 : $i,X1 : ($i > $o)] : (($true = (((~ (!! @ $i @ (^[Y0 : $i]: ((rel @ X2 @ Y0) => (X1 @ Y0))))) | (X1 @ X2))))) )),
% 7.10/1.52 inference(beta-eta_normalization,[],[f157])).
% 7.10/1.52 thf(f161,plain,(
% 7.10/1.52 ( ! [X0 : $i,X1 : ($i > $o)] : (($false = ((!! @ $i @ (^[Y0 : $i]: ((rel @ X0 @ Y0) => (X1 @ Y0)))))) | ($true = (((~ $true) | (X1 @ X0))))) )),
% 7.10/1.52 inference(constrained_superposition,[],[f158,f117])).
% 7.10/1.52 thf(f165,plain,(
% 7.10/1.52 ( ! [X0 : $i,X1 : ($i > $o)] : (((($false | (X1 @ X0))) = $true) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((rel @ X0 @ Y0) => (X1 @ Y0))))))) )),
% 7.10/1.52 inference(boolean_simplification,[],[f161])).
% 7.10/1.52 thf(f166,plain,(
% 7.10/1.52 ( ! [X0 : $i,X1 : ($i > $o)] : (($false = ((!! @ $i @ (^[Y0 : $i]: ((rel @ X0 @ Y0) => (X1 @ Y0)))))) | ($true = ((X1 @ X0)))) )),
% 7.10/1.52 inference(boolean_simplification,[],[f165])).
% 7.10/1.52 thf(f167,plain,(
% 7.10/1.52 ( ! [X1 : $i] : (((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => ((alice @ Y1) | (!! @ $i @ (^[Y2 : $i]: ((rel @ Y1 @ Y2) => (deletefile1 @ Y2))))))))) @ X1)) = $true)) )),
% 7.10/1.52 inference(pi_proxy_clausification,[],[f144])).
% 7.10/1.53 thf(f168,plain,(
% 7.10/1.53 ( ! [X1 : $i] : ((((!! @ $i @ (^[Y0 : $i]: ((rel @ X1 @ Y0) => ((alice @ Y0) | (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => (deletefile1 @ Y1))))))))) = $true)) )),
% 7.10/1.53 inference(beta-eta_normalization,[],[f167])).
% 7.10/1.53 thf(f169,plain,(
% 7.10/1.53 ( ! [X2 : $i,X1 : $i] : (((((^[Y0 : $i]: ((rel @ X1 @ Y0) => ((alice @ Y0) | (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => (deletefile1 @ Y1))))))) @ X2)) = $true)) )),
% 7.10/1.53 inference(pi_proxy_clausification,[],[f168])).
% 7.10/1.53 thf(f170,plain,(
% 7.10/1.53 ( ! [X2 : $i,X1 : $i] : (($true = (((rel @ X1 @ X2) => ((alice @ X2) | (!! @ $i @ (^[Y0 : $i]: ((rel @ X2 @ Y0) => (deletefile1 @ Y0))))))))) )),
% 7.10/1.53 inference(beta-eta_normalization,[],[f169])).
% 7.10/1.53 thf(f182,plain,(
% 7.10/1.53 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => ((bob @ Y1) | (!! @ $i @ (^[Y2 : $i]: ((rel @ Y1 @ Y2) => ((~ (alice @ Y2)) | (bob @ Y2)))))))))) @ X1)))) )),
% 7.10/1.53 inference(pi_proxy_clausification,[],[f143])).
% 7.10/1.53 thf(f183,plain,(
% 7.10/1.53 ( ! [X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: ((rel @ X1 @ Y0) => ((bob @ Y0) | (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => ((~ (alice @ Y1)) | (bob @ Y1)))))))))))) )),
% 7.10/1.53 inference(beta-eta_normalization,[],[f182])).
% 7.10/1.53 thf(f185,plain,(
% 7.10/1.53 ( ! [X2 : $i,X1 : $i] : (((((^[Y0 : $i]: ((rel @ X1 @ Y0) => ((bob @ Y0) | (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => ((~ (alice @ Y1)) | (bob @ Y1)))))))) @ X2)) = $true)) )),
% 7.10/1.53 inference(pi_proxy_clausification,[],[f183])).
% 7.10/1.53 thf(f186,plain,(
% 7.10/1.53 ( ! [X2 : $i,X1 : $i] : (((((rel @ X1 @ X2) => ((bob @ X2) | (!! @ $i @ (^[Y0 : $i]: ((rel @ X2 @ Y0) => ((~ (alice @ Y0)) | (bob @ Y0)))))))) = $true)) )),
% 7.10/1.53 inference(beta-eta_normalization,[],[f185])).
% 7.10/1.53 thf(f210,plain,(
% 7.10/1.53 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => ((~ (!! @ $i @ (^[Y2 : $i]: ((rel @ Y1 @ Y2) => ((admin @ Y2) | (!! @ $i @ (^[Y3 : $i]: ((rel @ Y2 @ Y3) => (deletefile1 @ Y3))))))))) | (!! @ $i @ (^[Y2 : $i]: ((rel @ Y1 @ Y2) => (deletefile1 @ Y2))))))))) @ X1)))) )),
% 7.10/1.53 inference(pi_proxy_clausification,[],[f140])).
% 7.10/1.53 thf(f211,plain,(
% 7.10/1.53 ( ! [X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: ((rel @ X1 @ Y0) => ((~ (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => ((admin @ Y1) | (!! @ $i @ (^[Y2 : $i]: ((rel @ Y1 @ Y2) => (deletefile1 @ Y2))))))))) | (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => (deletefile1 @ Y1))))))))))) )),
% 7.10/1.53 inference(beta-eta_normalization,[],[f210])).
% 7.10/1.53 thf(f212,plain,(
% 7.10/1.53 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((rel @ X1 @ Y0) => ((~ (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => ((admin @ Y1) | (!! @ $i @ (^[Y2 : $i]: ((rel @ Y1 @ Y2) => (deletefile1 @ Y2))))))))) | (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => (deletefile1 @ Y1))))))) @ X2)))) )),
% 7.10/1.53 inference(pi_proxy_clausification,[],[f211])).
% 7.10/1.53 thf(f213,plain,(
% 7.10/1.53 ( ! [X2 : $i,X1 : $i] : (($true = (((rel @ X1 @ X2) => ((~ (!! @ $i @ (^[Y0 : $i]: ((rel @ X2 @ Y0) => ((admin @ Y0) | (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => (deletefile1 @ Y1))))))))) | (!! @ $i @ (^[Y0 : $i]: ((rel @ X2 @ Y0) => (deletefile1 @ Y0))))))))) )),
% 7.10/1.53 inference(beta-eta_normalization,[],[f212])).
% 7.10/1.53 thf(f228,plain,(
% 7.10/1.53 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => ((admin @ Y1) | (!! @ $i @ (^[Y2 : $i]: ((rel @ Y1 @ Y2) => ((~ (!! @ $i @ (^[Y3 : $i]: ((rel @ Y2 @ Y3) => ((bob @ Y3) | (!! @ $i @ (^[Y4 : $i]: ((rel @ Y3 @ Y4) => (deletefile1 @ Y4))))))))) | (!! @ $i @ (^[Y3 : $i]: ((rel @ Y2 @ Y3) => (deletefile1 @ Y3))))))))))))) @ X1)))) )),
% 7.10/1.53 inference(pi_proxy_clausification,[],[f142])).
% 7.10/1.53 thf(f229,plain,(
% 7.10/1.53 ( ! [X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: ((rel @ X1 @ Y0) => ((admin @ Y0) | (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => ((~ (!! @ $i @ (^[Y2 : $i]: ((rel @ Y1 @ Y2) => ((bob @ Y2) | (!! @ $i @ (^[Y3 : $i]: ((rel @ Y2 @ Y3) => (deletefile1 @ Y3))))))))) | (!! @ $i @ (^[Y2 : $i]: ((rel @ Y1 @ Y2) => (deletefile1 @ Y2))))))))))))))) )),
% 7.10/1.53 inference(beta-eta_normalization,[],[f228])).
% 7.10/1.53 thf(f230,plain,(
% 7.10/1.53 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((rel @ X1 @ Y0) => ((admin @ Y0) | (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => ((~ (!! @ $i @ (^[Y2 : $i]: ((rel @ Y1 @ Y2) => ((bob @ Y2) | (!! @ $i @ (^[Y3 : $i]: ((rel @ Y2 @ Y3) => (deletefile1 @ Y3))))))))) | (!! @ $i @ (^[Y2 : $i]: ((rel @ Y1 @ Y2) => (deletefile1 @ Y2))))))))))) @ X2)))) )),
% 7.10/1.53 inference(pi_proxy_clausification,[],[f229])).
% 7.10/1.53 thf(f231,plain,(
% 7.10/1.53 ( ! [X2 : $i,X1 : $i] : (($true = (((rel @ X1 @ X2) => ((admin @ X2) | (!! @ $i @ (^[Y0 : $i]: ((rel @ X2 @ Y0) => ((~ (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => ((bob @ Y1) | (!! @ $i @ (^[Y2 : $i]: ((rel @ Y1 @ Y2) => (deletefile1 @ Y2))))))))) | (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => (deletefile1 @ Y1))))))))))))) )),
% 7.10/1.53 inference(beta-eta_normalization,[],[f230])).
% 7.10/1.53 thf(f243,plain,(
% 7.10/1.53 ($true = ((~ sF0)))),
% 7.10/1.53 inference(forward_demodulation,[],[f138,f139])).
% 7.10/1.53 thf(f244,plain,(
% 7.10/1.53 ($false = sF0)),
% 7.10/1.53 inference(not_proxy_clausification,[],[f243])).
% 7.10/1.53 thf(f249,plain,(
% 7.10/1.53 ($false = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => (deletefile1 @ Y1))))))))),
% 7.10/1.53 inference(backward_demodulation,[],[f146,f244])).
% 7.10/1.53 thf(f253,plain,(
% 7.10/1.53 ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => (deletefile1 @ Y1))))) @ sK2)))),
% 7.10/1.53 inference(sigma_proxy_clausification,[],[f249])).
% 7.10/1.53 thf(f256,plain,(
% 7.10/1.53 (((!! @ $i @ (^[Y0 : $i]: ((rel @ sK2 @ Y0) => (deletefile1 @ Y0))))) = $false)),
% 7.10/1.53 inference(beta-eta_normalization,[],[f253])).
% 7.10/1.53 thf(f257,plain,(
% 7.10/1.53 ((((^[Y0 : $i]: ((rel @ sK2 @ Y0) => (deletefile1 @ Y0))) @ sK3)) = $false)),
% 7.10/1.53 inference(sigma_proxy_clausification,[],[f256])).
% 7.10/1.53 thf(f259,plain,(
% 7.10/1.53 ($false = (((rel @ sK2 @ sK3) => (deletefile1 @ sK3))))),
% 7.10/1.53 inference(beta-eta_normalization,[],[f257])).
% 7.10/1.53 thf(f261,plain,(
% 7.10/1.53 ($false = ((deletefile1 @ sK3)))),
% 7.10/1.53 inference(imp_proxy_clausification,[],[f259])).
% 7.10/1.53 thf(f262,plain,(
% 7.10/1.53 ($true = ((rel @ sK2 @ sK3)))),
% 7.10/1.53 inference(imp_proxy_clausification,[],[f259])).
% 7.10/1.53 thf(f272,plain,(
% 7.10/1.53 ((((~ (!! @ $i @ (^[Y0 : $i]: ((rel @ sK3 @ Y0) => (deletefile1 @ Y0))))) | $false)) = $true)),
% 7.10/1.53 inference(constrained_superposition,[],[f158,f261])).
% 7.10/1.53 thf(f273,plain,(
% 7.10/1.53 (((~ (!! @ $i @ (^[Y0 : $i]: ((rel @ sK3 @ Y0) => (deletefile1 @ Y0)))))) = $true)),
% 7.10/1.53 inference(boolean_simplification,[],[f272])).
% 7.10/1.53 thf(f276,plain,(
% 7.10/1.53 ($false = ((!! @ $i @ (^[Y0 : $i]: ((rel @ sK3 @ Y0) => (deletefile1 @ Y0))))))),
% 7.10/1.53 inference(not_proxy_clausification,[],[f273])).
% 7.10/1.53 thf(f286,plain,(
% 7.10/1.53 ( ! [X0 : $i,X1 : ($i > $o)] : (($true = ((X1 @ X0))) | ($false = (((^[Y0 : $i]: ((rel @ X0 @ Y0) => (X1 @ Y0))) @ (sK5 @ X1 @ X0))))) )),
% 7.10/1.53 inference(sigma_proxy_clausification,[],[f166])).
% 7.10/1.53 thf(f289,plain,(
% 7.10/1.53 ( ! [X0 : $i,X1 : ($i > $o)] : (((((rel @ X0 @ (sK5 @ X1 @ X0)) => (X1 @ (sK5 @ X1 @ X0)))) = $false) | ($true = ((X1 @ X0)))) )),
% 7.10/1.53 inference(beta-eta_normalization,[],[f286])).
% 7.10/1.53 thf(f292,plain,(
% 7.10/1.53 ($true = (($true => ((~ (!! @ $i @ (^[Y0 : $i]: ((rel @ sK3 @ Y0) => ((admin @ Y0) | (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => (deletefile1 @ Y1))))))))) | (!! @ $i @ (^[Y0 : $i]: ((rel @ sK3 @ Y0) => (deletefile1 @ Y0))))))))),
% 7.10/1.53 inference(constrained_superposition,[],[f213,f262])).
% 7.10/1.53 thf(f297,plain,(
% 7.10/1.53 ((((~ (!! @ $i @ (^[Y0 : $i]: ((rel @ sK3 @ Y0) => ((admin @ Y0) | (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => (deletefile1 @ Y1))))))))) | (!! @ $i @ (^[Y0 : $i]: ((rel @ sK3 @ Y0) => (deletefile1 @ Y0)))))) = $true)),
% 7.10/1.53 inference(boolean_simplification,[],[f292])).
% 7.10/1.53 thf(f300,plain,(
% 7.10/1.53 ($true = (((~ (!! @ $i @ (^[Y0 : $i]: ((rel @ sK3 @ Y0) => ((admin @ Y0) | (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => (deletefile1 @ Y1))))))))) | $false)))),
% 7.10/1.53 inference(forward_demodulation,[],[f297,f276])).
% 7.10/1.53 thf(f301,plain,(
% 7.10/1.53 (((~ (!! @ $i @ (^[Y0 : $i]: ((rel @ sK3 @ Y0) => ((admin @ Y0) | (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => (deletefile1 @ Y1)))))))))) = $true)),
% 7.10/1.53 inference(boolean_simplification,[],[f300])).
% 7.10/1.53 thf(f314,plain,(
% 7.10/1.53 ($false = ((!! @ $i @ (^[Y0 : $i]: ((rel @ sK3 @ Y0) => ((admin @ Y0) | (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => (deletefile1 @ Y1))))))))))),
% 7.10/1.53 inference(not_proxy_clausification,[],[f301])).
% 7.10/1.53 thf(f319,plain,(
% 7.10/1.53 ($false = (((^[Y0 : $i]: ((rel @ sK3 @ Y0) => ((admin @ Y0) | (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => (deletefile1 @ Y1))))))) @ sK6)))),
% 7.10/1.53 inference(sigma_proxy_clausification,[],[f314])).
% 7.10/1.53 thf(f323,plain,(
% 7.10/1.53 ($false = (((rel @ sK3 @ sK6) => ((admin @ sK6) | (!! @ $i @ (^[Y0 : $i]: ((rel @ sK6 @ Y0) => (deletefile1 @ Y0))))))))),
% 7.10/1.53 inference(beta-eta_normalization,[],[f319])).
% 7.10/1.53 thf(f325,plain,(
% 7.10/1.53 ($true = ((rel @ sK3 @ sK6)))),
% 7.10/1.53 inference(imp_proxy_clausification,[],[f323])).
% 7.10/1.53 thf(f326,plain,(
% 7.10/1.53 ($false = ((!! @ $i @ (^[Y0 : $i]: ((rel @ sK6 @ Y0) => (deletefile1 @ Y0)))))) | ($false = (((rel @ sK3 @ sK6) => ((admin @ sK6) | $true))))),
% 7.10/1.53 inference(constrained_superposition,[],[f323,f117])).
% 7.10/1.53 thf(f327,plain,(
% 7.10/1.53 ($false = (((rel @ sK3 @ sK6) => ($true | (!! @ $i @ (^[Y0 : $i]: ((rel @ sK6 @ Y0) => (deletefile1 @ Y0)))))))) | ($false = ((admin @ sK6)))),
% 7.10/1.53 inference(constrained_superposition,[],[f323,f117])).
% 7.10/1.53 thf(f331,plain,(
% 7.10/1.53 ((((rel @ sK3 @ sK6) => $true)) = $false) | ($false = ((admin @ sK6)))),
% 7.10/1.53 inference(boolean_simplification,[],[f327])).
% 7.10/1.53 thf(f332,plain,(
% 7.10/1.53 ($false = $true) | ($false = ((admin @ sK6)))),
% 7.10/1.53 inference(boolean_simplification,[],[f331])).
% 7.10/1.53 thf(f333,plain,(
% 7.10/1.53 ($false = ((admin @ sK6)))),
% 7.10/1.53 inference(trivial_inequality_removal,[],[f332])).
% 7.10/1.53 thf(f334,plain,(
% 7.10/1.53 ($false = ((!! @ $i @ (^[Y0 : $i]: ((rel @ sK6 @ Y0) => (deletefile1 @ Y0)))))) | ((((rel @ sK3 @ sK6) => $true)) = $false)),
% 7.10/1.53 inference(boolean_simplification,[],[f326])).
% 7.10/1.53 thf(f335,plain,(
% 7.10/1.53 ($false = ((!! @ $i @ (^[Y0 : $i]: ((rel @ sK6 @ Y0) => (deletefile1 @ Y0)))))) | ($false = $true)),
% 7.10/1.53 inference(boolean_simplification,[],[f334])).
% 7.10/1.53 thf(f336,plain,(
% 7.10/1.53 ($false = ((!! @ $i @ (^[Y0 : $i]: ((rel @ sK6 @ Y0) => (deletefile1 @ Y0))))))),
% 7.10/1.53 inference(trivial_inequality_removal,[],[f335])).
% 7.10/1.53 thf(f378,plain,(
% 7.10/1.53 ($true = (($true => ((admin @ sK6) | (!! @ $i @ (^[Y0 : $i]: ((rel @ sK6 @ Y0) => ((~ (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => ((bob @ Y1) | (!! @ $i @ (^[Y2 : $i]: ((rel @ Y1 @ Y2) => (deletefile1 @ Y2))))))))) | (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => (deletefile1 @ Y1))))))))))))),
% 7.10/1.53 inference(constrained_superposition,[],[f231,f325])).
% 7.10/1.53 thf(f388,plain,(
% 7.10/1.53 ($true = (((admin @ sK6) | (!! @ $i @ (^[Y0 : $i]: ((rel @ sK6 @ Y0) => ((~ (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => ((bob @ Y1) | (!! @ $i @ (^[Y2 : $i]: ((rel @ Y1 @ Y2) => (deletefile1 @ Y2))))))))) | (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => (deletefile1 @ Y1)))))))))))),
% 7.10/1.53 inference(boolean_simplification,[],[f378])).
% 7.10/1.53 thf(f393,plain,(
% 7.10/1.53 ((($false | (!! @ $i @ (^[Y0 : $i]: ((rel @ sK6 @ Y0) => ((~ (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => ((bob @ Y1) | (!! @ $i @ (^[Y2 : $i]: ((rel @ Y1 @ Y2) => (deletefile1 @ Y2))))))))) | (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => (deletefile1 @ Y1)))))))))) = $true)),
% 7.10/1.53 inference(forward_demodulation,[],[f388,f333])).
% 7.10/1.53 thf(f394,plain,(
% 7.10/1.53 ($true = ((!! @ $i @ (^[Y0 : $i]: ((rel @ sK6 @ Y0) => ((~ (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => ((bob @ Y1) | (!! @ $i @ (^[Y2 : $i]: ((rel @ Y1 @ Y2) => (deletefile1 @ Y2))))))))) | (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => (deletefile1 @ Y1))))))))))),
% 7.10/1.53 inference(boolean_simplification,[],[f393])).
% 7.10/1.53 thf(f443,plain,(
% 7.10/1.53 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: ((rel @ sK6 @ Y0) => ((~ (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => ((bob @ Y1) | (!! @ $i @ (^[Y2 : $i]: ((rel @ Y1 @ Y2) => (deletefile1 @ Y2))))))))) | (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => (deletefile1 @ Y1))))))) @ X1)))) )),
% 7.10/1.53 inference(pi_proxy_clausification,[],[f394])).
% 7.10/1.53 thf(f445,plain,(
% 7.10/1.53 ( ! [X1 : $i] : (($true = (((rel @ sK6 @ X1) => ((~ (!! @ $i @ (^[Y0 : $i]: ((rel @ X1 @ Y0) => ((bob @ Y0) | (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => (deletefile1 @ Y1))))))))) | (!! @ $i @ (^[Y0 : $i]: ((rel @ X1 @ Y0) => (deletefile1 @ Y0))))))))) )),
% 7.10/1.53 inference(beta-eta_normalization,[],[f443])).
% 7.10/1.53 thf(f630,plain,(
% 7.10/1.53 ( ! [X0 : $i,X1 : ($i > $o)] : ((((X1 @ (sK5 @ X1 @ X0))) = $false) | ($true = ((X1 @ X0)))) )),
% 7.10/1.53 inference(imp_proxy_clausification,[],[f289])).
% 7.10/1.53 thf(f794,plain,(
% 7.10/1.53 ( ! [X0 : $i] : (($true = ((rel @ X0 @ X0))) | ($true = ((rel @ X0 @ X0))) | ($false = (($false => $false)))) )),
% 7.10/1.53 inference(constrained_superposition,[],[f289,f630])).
% 7.10/1.53 thf(f800,plain,(
% 7.10/1.53 ( ! [X0 : $i] : (($false = (($false => $false))) | ($true = ((rel @ X0 @ X0)))) )),
% 7.10/1.53 inference(duplicate_literal_removal,[],[f794])).
% 7.10/1.53 thf(f801,plain,(
% 7.10/1.53 ( ! [X0 : $i] : (($false = $true) | ($true = ((rel @ X0 @ X0)))) )),
% 7.10/1.53 inference(boolean_simplification,[],[f800])).
% 7.10/1.53 thf(f802,plain,(
% 7.10/1.53 ( ! [X0 : $i] : (($true = ((rel @ X0 @ X0)))) )),
% 7.10/1.53 inference(trivial_inequality_removal,[],[f801])).
% 7.10/1.53 thf(f863,plain,(
% 7.10/1.53 ($true = (($true => ((~ (!! @ $i @ (^[Y0 : $i]: ((rel @ sK6 @ Y0) => ((bob @ Y0) | (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => (deletefile1 @ Y1))))))))) | (!! @ $i @ (^[Y0 : $i]: ((rel @ sK6 @ Y0) => (deletefile1 @ Y0))))))))),
% 7.10/1.53 inference(constrained_superposition,[],[f445,f802])).
% 7.10/1.53 thf(f867,plain,(
% 7.10/1.53 ( ! [X0 : $i] : (((($true => ((bob @ X0) | (!! @ $i @ (^[Y0 : $i]: ((rel @ X0 @ Y0) => ((~ (alice @ Y0)) | (bob @ Y0)))))))) = $true)) )),
% 7.10/1.53 inference(constrained_superposition,[],[f186,f802])).
% 7.10/1.53 thf(f868,plain,(
% 7.10/1.53 ( ! [X0 : $i] : (($true = (($true => ((alice @ X0) | (!! @ $i @ (^[Y0 : $i]: ((rel @ X0 @ Y0) => (deletefile1 @ Y0))))))))) )),
% 7.10/1.53 inference(constrained_superposition,[],[f170,f802])).
% 7.10/1.53 thf(f872,plain,(
% 7.10/1.53 ( ! [X0 : $i] : (((((alice @ X0) | (!! @ $i @ (^[Y0 : $i]: ((rel @ X0 @ Y0) => (deletefile1 @ Y0)))))) = $true)) )),
% 7.10/1.53 inference(boolean_simplification,[],[f868])).
% 7.10/1.53 thf(f875,plain,(
% 7.10/1.53 ( ! [X0 : $i] : (((((bob @ X0) | (!! @ $i @ (^[Y0 : $i]: ((rel @ X0 @ Y0) => ((~ (alice @ Y0)) | (bob @ Y0))))))) = $true)) )),
% 7.10/1.53 inference(boolean_simplification,[],[f867])).
% 7.10/1.53 thf(f880,plain,(
% 7.10/1.53 ($true = (((~ (!! @ $i @ (^[Y0 : $i]: ((rel @ sK6 @ Y0) => ((bob @ Y0) | (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => (deletefile1 @ Y1))))))))) | (!! @ $i @ (^[Y0 : $i]: ((rel @ sK6 @ Y0) => (deletefile1 @ Y0)))))))),
% 7.10/1.53 inference(boolean_simplification,[],[f863])).
% 7.10/1.53 thf(f885,plain,(
% 7.10/1.53 ($true = (((~ (!! @ $i @ (^[Y0 : $i]: ((rel @ sK6 @ Y0) => ((bob @ Y0) | (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => (deletefile1 @ Y1))))))))) | $false)))),
% 7.10/1.53 inference(forward_demodulation,[],[f880,f336])).
% 7.10/1.53 thf(f886,plain,(
% 7.10/1.53 ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((rel @ sK6 @ Y0) => ((bob @ Y0) | (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => (deletefile1 @ Y1)))))))))))),
% 7.10/1.53 inference(boolean_simplification,[],[f885])).
% 7.10/1.53 thf(f939,plain,(
% 7.10/1.53 ($false = ((!! @ $i @ (^[Y0 : $i]: ((rel @ sK6 @ Y0) => ((bob @ Y0) | (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => (deletefile1 @ Y1))))))))))),
% 7.10/1.53 inference(not_proxy_clausification,[],[f886])).
% 7.10/1.53 thf(f944,plain,(
% 7.10/1.53 ($false = (((^[Y0 : $i]: ((rel @ sK6 @ Y0) => ((bob @ Y0) | (!! @ $i @ (^[Y1 : $i]: ((rel @ Y0 @ Y1) => (deletefile1 @ Y1))))))) @ sK12)))),
% 7.10/1.53 inference(sigma_proxy_clausification,[],[f939])).
% 7.10/1.53 thf(f946,plain,(
% 7.10/1.53 ($false = (((rel @ sK6 @ sK12) => ((bob @ sK12) | (!! @ $i @ (^[Y0 : $i]: ((rel @ sK12 @ Y0) => (deletefile1 @ Y0))))))))),
% 7.10/1.53 inference(beta-eta_normalization,[],[f944])).
% 7.10/1.53 thf(f951,plain,(
% 7.10/1.53 ($false = ((!! @ $i @ (^[Y0 : $i]: ((rel @ sK12 @ Y0) => (deletefile1 @ Y0)))))) | ($false = (((rel @ sK6 @ sK12) => ((bob @ sK12) | $true))))),
% 7.10/1.53 inference(constrained_superposition,[],[f946,f117])).
% 7.10/1.53 thf(f952,plain,(
% 7.10/1.53 ($false = ((bob @ sK12))) | ($false = (((rel @ sK6 @ sK12) => ($true | (!! @ $i @ (^[Y0 : $i]: ((rel @ sK12 @ Y0) => (deletefile1 @ Y0))))))))),
% 7.10/1.53 inference(constrained_superposition,[],[f946,f117])).
% 7.10/1.53 thf(f960,plain,(
% 7.10/1.53 ($false = ((bob @ sK12))) | ($false = (((rel @ sK6 @ sK12) => $true)))),
% 7.10/1.53 inference(boolean_simplification,[],[f952])).
% 7.10/1.53 thf(f961,plain,(
% 7.10/1.53 ($false = $true) | ($false = ((bob @ sK12)))),
% 7.10/1.53 inference(boolean_simplification,[],[f960])).
% 7.10/1.53 thf(f962,plain,(
% 7.10/1.53 ($false = ((bob @ sK12)))),
% 7.10/1.53 inference(trivial_inequality_removal,[],[f961])).
% 7.10/1.53 thf(f963,plain,(
% 7.10/1.53 ($false = ((!! @ $i @ (^[Y0 : $i]: ((rel @ sK12 @ Y0) => (deletefile1 @ Y0)))))) | ($false = (((rel @ sK6 @ sK12) => $true)))),
% 7.10/1.53 inference(boolean_simplification,[],[f951])).
% 7.10/1.53 thf(f964,plain,(
% 7.10/1.53 ($false = ((!! @ $i @ (^[Y0 : $i]: ((rel @ sK12 @ Y0) => (deletefile1 @ Y0)))))) | ($false = $true)),
% 7.10/1.53 inference(boolean_simplification,[],[f963])).
% 7.10/1.53 thf(f965,plain,(
% 7.10/1.53 ($false = ((!! @ $i @ (^[Y0 : $i]: ((rel @ sK12 @ Y0) => (deletefile1 @ Y0))))))),
% 7.10/1.53 inference(trivial_inequality_removal,[],[f964])).
% 7.10/1.53 thf(f978,plain,(
% 7.10/1.53 ((($false | (!! @ $i @ (^[Y0 : $i]: ((rel @ sK12 @ Y0) => ((~ (alice @ Y0)) | (bob @ Y0))))))) = $true)),
% 7.10/1.53 inference(constrained_superposition,[],[f875,f962])).
% 7.10/1.53 thf(f980,plain,(
% 7.10/1.53 ($true = ((!! @ $i @ (^[Y0 : $i]: ((rel @ sK12 @ Y0) => ((~ (alice @ Y0)) | (bob @ Y0)))))))),
% 7.10/1.53 inference(boolean_simplification,[],[f978])).
% 7.10/1.53 thf(f992,plain,(
% 7.10/1.53 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: ((rel @ sK12 @ Y0) => ((~ (alice @ Y0)) | (bob @ Y0)))) @ X1)))) )),
% 7.10/1.53 inference(pi_proxy_clausification,[],[f980])).
% 7.10/1.53 thf(f993,plain,(
% 7.10/1.53 ( ! [X1 : $i] : (($true = (((rel @ sK12 @ X1) => ((~ (alice @ X1)) | (bob @ X1)))))) )),
% 7.10/1.53 inference(beta-eta_normalization,[],[f992])).
% 7.10/1.53 thf(f2875,plain,(
% 7.10/1.53 ($true = (($true => ((~ (alice @ sK12)) | (bob @ sK12)))))),
% 7.10/1.53 inference(constrained_superposition,[],[f993,f802])).
% 7.10/1.53 thf(f2888,plain,(
% 7.10/1.53 ((((~ (alice @ sK12)) | (bob @ sK12))) = $true)),
% 7.10/1.53 inference(boolean_simplification,[],[f2875])).
% 7.10/1.53 thf(f2934,plain,(
% 7.10/1.53 ((((~ (alice @ sK12)) | $false)) = $true)),
% 7.10/1.53 inference(forward_demodulation,[],[f2888,f962])).
% 7.10/1.53 thf(f2935,plain,(
% 7.10/1.53 (((~ (alice @ sK12))) = $true)),
% 7.10/1.53 inference(boolean_simplification,[],[f2934])).
% 7.10/1.53 thf(f2949,plain,(
% 7.10/1.53 ($false = ((alice @ sK12)))),
% 7.10/1.53 inference(not_proxy_clausification,[],[f2935])).
% 7.10/1.53 thf(f3007,plain,(
% 7.10/1.53 ($true = (($false | (!! @ $i @ (^[Y0 : $i]: ((rel @ sK12 @ Y0) => (deletefile1 @ Y0)))))))),
% 7.10/1.53 inference(constrained_superposition,[],[f872,f2949])).
% 7.10/1.53 thf(f3016,plain,(
% 7.10/1.53 ($true = ((!! @ $i @ (^[Y0 : $i]: ((rel @ sK12 @ Y0) => (deletefile1 @ Y0))))))),
% 7.10/1.53 inference(boolean_simplification,[],[f3007])).
% 7.10/1.53 thf(f3017,plain,(
% 7.10/1.53 ($false = $true)),
% 7.10/1.53 inference(forward_demodulation,[],[f3016,f965])).
% 7.10/1.53 thf(f3018,plain,(
% 7.10/1.53 $false),
% 7.10/1.53 inference(trivial_inequality_removal,[],[f3017])).
% 7.10/1.53 % SZS output end Proof for theBenchmark
% 7.10/1.53 % (4182760)------------------------------
% 7.10/1.53 % (4182760)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.10/1.53 % (4182760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.10/1.53 % (4182760)CaDiCaL version: 2.1.3
% 7.10/1.53 % (4182760)Termination reason: Refutation
% 7.10/1.53 % (4182760)Time elapsed: 0.223 s
% 7.10/1.53 % (4182760)Peak memory usage: 13 MB
% 7.10/1.53 % (4182760)Instructions burned: 251 (million)
% 7.10/1.53 % (4182602)Success in time 1.228 s
% 7.10/1.53 % Vampire exiting
%------------------------------------------------------------------------------