%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP109^2 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:08:23 AM UTC 2026
% Result : Theorem 11.72s 2.04s
% Output : Refutation 11.72s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP109^2 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n020.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Tue Sep 29 19:55:35 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running higher-order theorem proving
% 0.20/0.29 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.07/0.50 % (1514090)Detected a higher-order problem, will run a greedy HOL sequence.
% 1.07/0.50 % (1514097)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=1790713715:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 1.07/0.50 % (1514097)Instruction limit reached!
% 1.07/0.50 % (1514097)------------------------------
% 1.07/0.50 % (1514097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.07/0.50 % (1514097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.07/0.50 % (1514097)CaDiCaL version: 2.1.3
% 1.07/0.50 % (1514097)Termination reason: Instruction limit
% 1.07/0.50 % (1514097)Termination phase: shuffling
% 1.07/0.50 % (1514097)Time elapsed: 0.001 s
% 1.07/0.50 % (1514097)Peak memory usage: 10 MB
% 1.07/0.50 % (1514097)Instructions burned: 3 (million)
% 1.07/0.50 % (1514095)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3448378451:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 1.07/0.50 % (1514096)lrs+10_16_si=on:nwc=1.5:random_seed=3818190885:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 1.07/0.50 % (1514104)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3471827035:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 1.07/0.50 % (1514104)Instruction limit reached!
% 1.07/0.50 % (1514104)------------------------------
% 1.07/0.50 % (1514104)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.07/0.50 % (1514104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.07/0.50 % (1514104)CaDiCaL version: 2.1.3
% 1.07/0.50 % (1514104)Termination reason: Instruction limit
% 1.07/0.50 % (1514104)Termination phase: shuffling
% 1.07/0.50 % (1514104)Time elapsed: 0.001 s
% 1.07/0.50 % (1514104)Peak memory usage: 10 MB
% 1.07/0.50 % (1514104)Instructions burned: 3 (million)
% 1.07/0.50 % (1514096)Instruction limit reached!
% 1.07/0.50 % (1514096)------------------------------
% 1.07/0.50 % (1514096)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.07/0.50 % (1514096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.07/0.50 % (1514096)CaDiCaL version: 2.1.3
% 1.07/0.50 % (1514096)Termination reason: Instruction limit
% 1.07/0.50 % (1514096)Termination phase: shuffling
% 1.07/0.50 % (1514096)Time elapsed: 0.009 s
% 1.07/0.50 % (1514096)Peak memory usage: 10 MB
% 1.07/0.50 % (1514096)Instructions burned: 18 (million)
% 1.07/0.50 % (1514098)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=782633991:hsq=on:hsqr=16,1:s2a=on:i=634:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2999 on theBenchmark for (2999ds/634Mi)
% 1.07/0.50 % (1514108)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=1918918004:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 1.07/0.50 % (1514108)Instruction limit reached!
% 1.07/0.50 % (1514108)------------------------------
% 1.07/0.50 % (1514108)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.07/0.50 % (1514108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.07/0.50 % (1514108)CaDiCaL version: 2.1.3
% 1.07/0.50 % (1514108)Termination reason: Instruction limit
% 1.07/0.50 % (1514108)Termination phase: shuffling
% 1.07/0.50 % (1514108)Time elapsed: 0.003 s
% 1.07/0.50 % (1514108)Peak memory usage: 10 MB
% 1.07/0.50 % (1514108)Instructions burned: 6 (million)
% 1.07/0.50 % (1514109)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.07/0.50 % (1514109)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3881955230:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 1.07/0.50 % (1514109)Instruction limit reached!
% 1.07/0.50 % (1514109)------------------------------
% 1.07/0.50 % (1514109)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.07/0.50 % (1514109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.07/0.50 % (1514109)CaDiCaL version: 2.1.3
% 1.07/0.50 % (1514109)Termination reason: Instruction limit
% 1.07/0.50 % (1514109)Termination phase: shuffling
% 1.07/0.50 % (1514109)Time elapsed: 0.005 s
% 1.07/0.50 % (1514109)Peak memory usage: 10 MB
% 1.07/0.50 % (1514109)Instructions burned: 9 (million)
% 1.07/0.54 % (1514102)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 1.07/0.54 % (1514102)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 1.07/0.54 % (1514100)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=550827444:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 1.07/0.54 % (1514101)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=3747772956:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 1.07/0.54 % (1514113)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=2477956670:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 1.07/0.54 % (1514102)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=491116234:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 1.07/0.54 % (1514115)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 1.07/0.54 % (1514115)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.07/0.54 % (1514113)Instruction limit reached!
% 1.07/0.54 % (1514113)------------------------------
% 1.07/0.54 % (1514113)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.07/0.54 % (1514113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.07/0.54 % (1514113)CaDiCaL version: 2.1.3
% 1.07/0.54 % (1514113)Termination reason: Instruction limit
% 1.07/0.54 % (1514113)Termination phase: shuffling
% 1.07/0.54 % (1514113)Time elapsed: 0.006 s
% 1.07/0.54 % (1514113)Peak memory usage: 10 MB
% 1.07/0.54 % (1514113)Instructions burned: 14 (million)
% 1.07/0.54 % (1514115)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=1758514050:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 1.07/0.54 % (1514095)Instruction limit reached!
% 1.07/0.54 % (1514095)------------------------------
% 1.07/0.54 % (1514095)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.07/0.54 % (1514095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.07/0.54 % (1514095)CaDiCaL version: 2.1.3
% 1.07/0.54 % (1514095)Termination reason: Instruction limit
% 1.07/0.54 % (1514095)Termination phase: Property scanning
% 1.07/0.54 % (1514095)Time elapsed: 0.062 s
% 1.07/0.54 % (1514095)Peak memory usage: 12 MB
% 1.07/0.54 % (1514095)Instructions burned: 88 (million)
% 1.07/0.54 % (1514115)Instruction limit reached!
% 1.07/0.54 % (1514115)------------------------------
% 1.07/0.54 % (1514115)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.07/0.54 % (1514115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.07/0.54 % (1514115)CaDiCaL version: 2.1.3
% 1.07/0.54 % (1514115)Termination reason: Instruction limit
% 1.07/0.54 % (1514115)Termination phase: shuffling
% 1.07/0.54 % (1514115)Time elapsed: 0.014 s
% 1.07/0.54 % (1514115)Peak memory usage: 10 MB
% 1.07/0.54 % (1514115)Instructions burned: 28 (million)
% 1.07/0.54 % (1514120)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=1060196790:i=86:piset=equals:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/86Mi)
% 1.07/0.54 % (1514122)lrs+10_1_si=on:cs=on:random_seed=2602208154:i=8:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.07/0.54 % (1514100)Instruction limit reached!
% 1.07/0.54 % (1514100)------------------------------
% 1.07/0.54 % (1514100)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.07/0.54 % (1514100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.07/0.54 % (1514100)CaDiCaL version: 2.1.3
% 1.07/0.54 % (1514100)Termination reason: Instruction limit
% 1.07/0.54 % (1514100)Termination phase: Property scanning
% 1.07/0.54 % (1514100)Time elapsed: 0.040 s
% 1.07/0.54 % (1514100)Peak memory usage: 11 MB
% 1.07/0.54 % (1514100)Instructions burned: 24 (million)
% 1.07/0.54 % (1514122)Instruction limit reached!
% 1.59/0.59 % (1514122)------------------------------
% 1.59/0.59 % (1514122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.59/0.59 % (1514122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.59/0.59 % (1514122)CaDiCaL version: 2.1.3
% 1.59/0.59 % (1514122)Termination reason: Instruction limit
% 1.59/0.59 % (1514122)Termination phase: shuffling
% 1.59/0.59 % (1514122)Time elapsed: 0.004 s
% 1.59/0.59 % (1514122)Peak memory usage: 10 MB
% 1.59/0.59 % (1514122)Instructions burned: 9 (million)
% 1.59/0.59 % (1514123)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 1.59/0.59 % (1514123)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=3374996162:i=2:add=on:rtra=on_2998 on theBenchmark for (2998ds/2Mi)
% 1.59/0.59 % (1514123)Instruction limit reached!
% 1.59/0.59 % (1514123)------------------------------
% 1.59/0.59 % (1514123)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.59/0.59 % (1514123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.59/0.59 % (1514123)CaDiCaL version: 2.1.3
% 1.59/0.59 % (1514123)Termination reason: Instruction limit
% 1.59/0.59 % (1514123)Termination phase: shuffling
% 1.59/0.59 % (1514123)Time elapsed: 0.001 s
% 1.59/0.59 % (1514123)Peak memory usage: 10 MB
% 1.59/0.59 % (1514123)Instructions burned: 2 (million)
% 1.59/0.59 % (1514129)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=4282646214:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 1.59/0.59 % (1514126)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=1252035830:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/38Mi)
% 1.59/0.59 % (1514120)Instruction limit reached!
% 1.59/0.59 % (1514120)------------------------------
% 1.59/0.59 % (1514120)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.59/0.59 % (1514120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.59/0.59 % (1514120)CaDiCaL version: 2.1.3
% 1.59/0.59 % (1514120)Termination reason: Instruction limit
% 1.59/0.59 % (1514120)Termination phase: Preprocessing 3
% 1.59/0.59 % (1514120)Time elapsed: 0.045 s
% 1.59/0.59 % (1514120)Peak memory usage: 11 MB
% 1.59/0.59 % (1514120)Instructions burned: 87 (million)
% 1.59/0.59 % (1514128)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=4029676250:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 1.59/0.59 % (1514129)Instruction limit reached!
% 1.59/0.59 % (1514129)------------------------------
% 1.59/0.59 % (1514129)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.59/0.59 % (1514129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.59/0.59 % (1514129)CaDiCaL version: 2.1.3
% 1.59/0.59 % (1514129)Termination reason: Instruction limit
% 1.59/0.59 % (1514129)Termination phase: Property scanning
% 1.59/0.59 % (1514129)Time elapsed: 0.013 s
% 1.59/0.59 % (1514129)Peak memory usage: 10 MB
% 1.59/0.59 % (1514129)Instructions burned: 27 (million)
% 1.59/0.59 % (1514101)Instruction limit reached!
% 1.59/0.59 % (1514101)------------------------------
% 1.59/0.59 % (1514101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.59/0.59 % (1514101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.59/0.59 % (1514101)CaDiCaL version: 2.1.3
% 1.59/0.59 % (1514101)Termination reason: Instruction limit
% 1.59/0.59 % (1514101)Termination phase: Property scanning
% 1.59/0.59 % (1514101)Time elapsed: 0.092 s
% 1.59/0.59 % (1514101)Peak memory usage: 12 MB
% 1.59/0.59 % (1514101)Instructions burned: 76 (million)
% 1.59/0.59 % (1514134)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=2417741524:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 1.59/0.59 % (1514126)Instruction limit reached!
% 1.59/0.59 % (1514126)------------------------------
% 1.59/0.59 % (1514126)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.59/0.59 % (1514126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.59/0.59 % (1514126)CaDiCaL version: 2.1.3
% 1.59/0.59 % (1514126)Termination reason: Instruction limit
% 1.59/0.59 % (1514126)Termination phase: SInE selection
% 1.59/0.59 % (1514126)Time elapsed: 0.034 s
% 1.88/0.66 % (1514126)Peak memory usage: 11 MB
% 1.88/0.66 % (1514126)Instructions burned: 39 (million)
% 1.88/0.66 % (1514133)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=1920278054:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.88/0.66 % (1514135)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=3549676788:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.88/0.66 % (1514135)Instruction limit reached!
% 1.88/0.66 % (1514135)------------------------------
% 1.88/0.66 % (1514135)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.88/0.66 % (1514135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.88/0.66 % (1514135)CaDiCaL version: 2.1.3
% 1.88/0.66 % (1514135)Termination reason: Instruction limit
% 1.88/0.66 % (1514135)Termination phase: shuffling
% 1.88/0.66 % (1514135)Time elapsed: 0.004 s
% 1.88/0.66 % (1514135)Peak memory usage: 10 MB
% 1.88/0.66 % (1514135)Instructions burned: 15 (million)
% 1.88/0.66 % (1514133)Instruction limit reached!
% 1.88/0.66 % (1514133)------------------------------
% 1.88/0.66 % (1514133)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.88/0.66 % (1514133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.88/0.66 % (1514133)CaDiCaL version: 2.1.3
% 1.88/0.66 % (1514133)Termination reason: Instruction limit
% 1.88/0.66 % (1514133)Termination phase: shuffling
% 1.88/0.66 % (1514133)Time elapsed: 0.013 s
% 1.88/0.66 % (1514133)Peak memory usage: 10 MB
% 1.88/0.66 % (1514133)Instructions burned: 14 (million)
% 1.88/0.66 % (1514137)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=1554604291:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2997 on theBenchmark for (2997ds/2Mi)
% 1.88/0.66 % (1514140)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=2040874775:i=26:ep=R:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/26Mi)
% 1.88/0.66 % (1514137)Instruction limit reached!
% 1.88/0.66 % (1514137)------------------------------
% 1.88/0.66 % (1514137)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.88/0.66 % (1514137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.88/0.66 % (1514137)CaDiCaL version: 2.1.3
% 1.88/0.66 % (1514137)Termination reason: Instruction limit
% 1.88/0.66 % (1514137)Termination phase: shuffling
% 1.88/0.66 % (1514137)Time elapsed: 0.005 s
% 1.88/0.66 % (1514137)Peak memory usage: 10 MB
% 1.88/0.66 % (1514137)Instructions burned: 3 (million)
% 1.88/0.66 % (1514102)Instruction limit reached!
% 1.88/0.66 % (1514102)------------------------------
% 1.88/0.66 % (1514102)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.88/0.66 % (1514140)Instruction limit reached!
% 1.88/0.66 % (1514140)------------------------------
% 1.88/0.66 % (1514140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.88/0.66 % (1514102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.88/0.66 % (1514140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.88/0.66 % (1514102)CaDiCaL version: 2.1.3
% 1.88/0.66 % (1514102)Termination reason: Instruction limit
% 1.88/0.66 % (1514102)Termination phase: Saturation
% 1.88/0.66 % (1514102)Time elapsed: 0.132 s
% 1.88/0.66 % (1514140)CaDiCaL version: 2.1.3
% 1.88/0.66 % (1514102)Peak memory usage: 14 MB
% 1.88/0.66 % (1514140)Termination reason: Instruction limit
% 1.88/0.66 % (1514140)Termination phase: shuffling
% 1.88/0.66 % (1514102)Instructions burned: 157 (million)
% 1.88/0.66 % (1514140)Time elapsed: 0.007 s
% 1.88/0.66 % (1514140)Peak memory usage: 10 MB
% 1.88/0.66 % (1514140)Instructions burned: 27 (million)
% 1.88/0.66 % (1514145)WARNING Broken Constraint: if sine_to_age_generality_threshold(10) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 1.88/0.66 % (1514145)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 1.88/0.66 % (1514145)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=1166841749:i=14:add=off:nm=40:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 1.88/0.66 % (1514141)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=302756582:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2997 on theBenchmark for (2997ds/23Mi)
% 2.16/0.77 % (1514145)Instruction limit reached!
% 2.16/0.77 % (1514145)------------------------------
% 2.16/0.77 % (1514145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.16/0.77 % (1514145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.16/0.77 % (1514145)CaDiCaL version: 2.1.3
% 2.16/0.77 % (1514145)Termination reason: Instruction limit
% 2.16/0.77 % (1514145)Termination phase: shuffling
% 2.16/0.77 % (1514145)Time elapsed: 0.004 s
% 2.16/0.77 % (1514145)Peak memory usage: 10 MB
% 2.16/0.77 % (1514145)Instructions burned: 15 (million)
% 2.16/0.77 % (1514149)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=2281722188:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2997 on theBenchmark for (2997ds/31Mi)
% 2.16/0.77 % (1514146)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 2.16/0.77 % (1514149)Instruction limit reached!
% 2.16/0.77 % (1514149)------------------------------
% 2.16/0.77 % (1514149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.16/0.77 % (1514149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.16/0.77 % (1514149)CaDiCaL version: 2.1.3
% 2.16/0.77 % (1514149)Termination reason: Instruction limit
% 2.16/0.77 % (1514149)Termination phase: shuffling
% 2.16/0.77 % (1514149)Time elapsed: 0.009 s
% 2.16/0.77 % (1514149)Peak memory usage: 10 MB
% 2.16/0.77 % (1514149)Instructions burned: 32 (million)
% 2.16/0.77 % (1514141)Instruction limit reached!
% 2.16/0.77 % (1514141)------------------------------
% 2.16/0.77 % (1514141)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.16/0.77 % (1514141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.16/0.77 % (1514141)CaDiCaL version: 2.1.3
% 2.16/0.77 % (1514141)Termination reason: Instruction limit
% 2.16/0.77 % (1514141)Termination phase: Property scanning
% 2.16/0.77 % (1514141)Time elapsed: 0.023 s
% 2.16/0.77 % (1514141)Peak memory usage: 10 MB
% 2.16/0.77 % (1514141)Instructions burned: 24 (million)
% 2.16/0.77 % (1514144)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=1285412957:cond=on:i=60:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/60Mi)
% 2.16/0.77 % (1514146)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=2558879822:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2997 on theBenchmark for (2997ds/8Mi)
% 2.16/0.77 % (1514146)Instruction limit reached!
% 2.16/0.77 % (1514146)------------------------------
% 2.16/0.77 % (1514146)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.16/0.77 % (1514146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.16/0.77 % (1514146)CaDiCaL version: 2.1.3
% 2.16/0.77 % (1514146)Termination reason: Instruction limit
% 2.16/0.77 % (1514146)Termination phase: shuffling
% 2.16/0.77 % (1514146)Time elapsed: 0.006 s
% 2.16/0.77 % (1514146)Peak memory usage: 10 MB
% 2.16/0.77 % (1514146)Instructions burned: 10 (million)
% 2.16/0.77 % (1514151)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=2547473025:i=7:hud=5:bd=preordered:rtra=on:bet=on_2997 on theBenchmark for (2997ds/7Mi)
% 2.16/0.77 % (1514151)Instruction limit reached!
% 2.16/0.77 % (1514151)------------------------------
% 2.16/0.77 % (1514151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.16/0.77 % (1514151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.16/0.77 % (1514151)CaDiCaL version: 2.1.3
% 2.16/0.77 % (1514151)Termination reason: Instruction limit
% 2.16/0.77 % (1514151)Termination phase: shuffling
% 2.16/0.77 % (1514151)Time elapsed: 0.003 s
% 2.16/0.77 % (1514151)Peak memory usage: 10 MB
% 2.16/0.77 % (1514151)Instructions burned: 8 (million)
% 2.16/0.77 % (1514128)Refutation not found, incomplete strategy
% 2.16/0.77 % (1514128)------------------------------
% 2.16/0.77 % (1514128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.16/0.77 % (1514128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.16/0.77 % (1514128)CaDiCaL version: 2.1.3
% 2.16/0.77 % (1514128)Termination reason: Refutation not found, incomplete strategy
% 2.16/0.77 % (1514128)Time elapsed: 0.116 s
% 2.16/0.77 % (1514128)Peak memory usage: 14 MB
% 2.99/0.91 % (1514128)Instructions burned: 136 (million)
% 2.99/0.91 % (1514128)------------------------------
% 2.99/0.91 % (1514128)------------------------------
% 2.99/0.91 % (1514157)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=995186063:i=1240:rtra=on:ixr=off_2997 on theBenchmark for (2997ds/1240Mi)
% 2.99/0.91 % (1514153)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=3659589666:i=23:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/23Mi)
% 2.99/0.91 % (1514156)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=3966272825:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2997 on theBenchmark for (2997ds/20Mi)
% 2.99/0.91 % (1514156)Instruction limit reached!
% 2.99/0.91 % (1514156)------------------------------
% 2.99/0.91 % (1514156)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.99/0.91 % (1514156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.99/0.91 % (1514156)CaDiCaL version: 2.1.3
% 2.99/0.91 % (1514156)Termination reason: Instruction limit
% 2.99/0.91 % (1514156)Termination phase: shuffling
% 2.99/0.91 % (1514156)Time elapsed: 0.011 s
% 2.99/0.91 % (1514156)Peak memory usage: 10 MB
% 2.99/0.91 % (1514156)Instructions burned: 22 (million)
% 2.99/0.91 % (1514144)Instruction limit reached!
% 2.99/0.91 % (1514144)------------------------------
% 2.99/0.91 % (1514144)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.99/0.91 % (1514144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.99/0.91 % (1514144)CaDiCaL version: 2.1.3
% 2.99/0.91 % (1514144)Termination reason: Instruction limit
% 2.99/0.91 % (1514144)Termination phase: Property scanning
% 2.99/0.91 % (1514144)Time elapsed: 0.047 s
% 2.99/0.91 % (1514144)Peak memory usage: 11 MB
% 2.99/0.91 % (1514144)Instructions burned: 60 (million)
% 2.99/0.91 % (1514153)Instruction limit reached!
% 2.99/0.91 % (1514153)------------------------------
% 2.99/0.91 % (1514153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.99/0.91 % (1514153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.99/0.91 % (1514153)CaDiCaL version: 2.1.3
% 2.99/0.91 % (1514153)Termination reason: Instruction limit
% 2.99/0.91 % (1514153)Termination phase: shuffling
% 2.99/0.91 % (1514153)Time elapsed: 0.020 s
% 2.99/0.91 % (1514153)Peak memory usage: 10 MB
% 2.99/0.91 % (1514153)Instructions burned: 23 (million)
% 2.99/0.91 % (1514158)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=2761891489:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2997 on theBenchmark for (2997ds/143Mi)
% 2.99/0.91 % (1514164)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 2.99/0.91 % (1514162)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=2036069207:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/193Mi)
% 2.99/0.91 % (1514164)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=924256232:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2996 on theBenchmark for (2996ds/7Mi)
% 2.99/0.91 % (1514134)Instruction limit reached!
% 2.99/0.91 % (1514134)------------------------------
% 2.99/0.91 % (1514134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.99/0.91 % (1514134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.99/0.91 % (1514134)CaDiCaL version: 2.1.3
% 2.99/0.91 % (1514134)Termination reason: Instruction limit
% 2.99/0.91 % (1514134)Termination phase: Saturation
% 2.99/0.91 % (1514134)Time elapsed: 0.164 s
% 2.99/0.91 % (1514134)Peak memory usage: 14 MB
% 2.99/0.91 % (1514134)Instructions burned: 328 (million)
% 2.99/0.91 % (1514163)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=829220646:i=42:hud=10:rtra=on_2996 on theBenchmark for (2996ds/42Mi)
% 2.99/0.91 % (1514164)Instruction limit reached!
% 2.99/0.91 % (1514164)------------------------------
% 2.99/0.91 % (1514164)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.99/0.91 % (1514164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.99/0.91 % (1514164)CaDiCaL version: 2.1.3
% 2.99/0.91 % (1514164)Termination reason: Instruction limit
% 2.99/0.91 % (1514164)Termination phase: shuffling
% 2.99/0.91 % (1514164)Time elapsed: 0.006 s
% 2.99/0.91 % (1514164)Peak memory usage: 10 MB
% 2.99/0.91 % (1514164)Instructions burned: 7 (million)
% 2.99/0.97 % (1514170)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=3156368460:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2996 on theBenchmark for (2996ds/169Mi)
% 2.99/0.97 % (1514169)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=2785864481:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/181Mi)
% 2.99/0.97 % (1514158)Instruction limit reached!
% 2.99/0.97 % (1514158)------------------------------
% 2.99/0.97 % (1514158)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.99/0.97 % (1514158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.99/0.97 % (1514158)CaDiCaL version: 2.1.3
% 2.99/0.97 % (1514158)Termination reason: Instruction limit
% 2.99/0.97 % (1514158)Termination phase: Saturation
% 2.99/0.97 % (1514158)Time elapsed: 0.068 s
% 2.99/0.97 % (1514158)Peak memory usage: 13 MB
% 2.99/0.97 % (1514158)Instructions burned: 143 (million)
% 2.99/0.97 % (1514163)Instruction limit reached!
% 2.99/0.97 % (1514163)------------------------------
% 2.99/0.97 % (1514163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.99/0.97 % (1514163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.99/0.97 % (1514163)CaDiCaL version: 2.1.3
% 2.99/0.97 % (1514163)Termination reason: Instruction limit
% 2.99/0.97 % (1514163)Termination phase: Preprocessing 3
% 2.99/0.97 % (1514163)Time elapsed: 0.039 s
% 2.99/0.97 % (1514163)Peak memory usage: 11 MB
% 2.99/0.97 % (1514163)Instructions burned: 44 (million)
% 2.99/0.97 % (1514173)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 2.99/0.97 % (1514173)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=2860738132:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2996 on theBenchmark for (2996ds/6Mi)
% 2.99/0.97 % (1514174)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=2808211634:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2995 on theBenchmark for (2995ds/22Mi)
% 2.99/0.97 % (1514173)Instruction limit reached!
% 2.99/0.97 % (1514173)------------------------------
% 2.99/0.97 % (1514173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.99/0.97 % (1514173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.99/0.97 % (1514173)CaDiCaL version: 2.1.3
% 2.99/0.97 % (1514173)Termination reason: Instruction limit
% 2.99/0.97 % (1514173)Termination phase: shuffling
% 2.99/0.97 % (1514173)Time elapsed: 0.003 s
% 2.99/0.97 % (1514173)Peak memory usage: 10 MB
% 2.99/0.97 % (1514173)Instructions burned: 7 (million)
% 2.99/0.97 % (1514174)Instruction limit reached!
% 2.99/0.97 % (1514174)------------------------------
% 2.99/0.97 % (1514174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.99/0.97 % (1514174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.99/0.97 % (1514174)CaDiCaL version: 2.1.3
% 2.99/0.97 % (1514174)Termination reason: Instruction limit
% 2.99/0.97 % (1514174)Termination phase: shuffling
% 2.99/0.97 % (1514174)Time elapsed: 0.011 s
% 2.99/0.97 % (1514174)Peak memory usage: 10 MB
% 2.99/0.97 % (1514174)Instructions burned: 22 (million)
% 2.99/0.97 % (1514177)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=1147882373:i=19:add=on:rtra=on_2995 on theBenchmark for (2995ds/19Mi)
% 2.99/0.97 % (1514178)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=2904249587:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/316Mi)
% 2.99/0.97 % (1514177)Instruction limit reached!
% 2.99/0.97 % (1514177)------------------------------
% 2.99/0.97 % (1514177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.99/0.97 % (1514177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.99/0.97 % (1514177)CaDiCaL version: 2.1.3
% 2.99/0.97 % (1514177)Termination reason: Instruction limit
% 2.99/0.97 % (1514177)Termination phase: shuffling
% 2.99/0.97 % (1514177)Time elapsed: 0.010 s
% 2.99/0.97 % (1514177)Peak memory usage: 10 MB
% 2.99/0.97 % (1514177)Instructions burned: 21 (million)
% 2.99/0.97 % (1514181)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=2484833041:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2995 on theBenchmark for (2995ds/853Mi)
% 2.99/1.03 % (1514162)Instruction limit reached!
% 2.99/1.03 % (1514162)------------------------------
% 2.99/1.03 % (1514162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.99/1.03 % (1514162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.99/1.03 % (1514162)CaDiCaL version: 2.1.3
% 2.99/1.03 % (1514162)Termination reason: Instruction limit
% 2.99/1.03 % (1514162)Termination phase: Saturation
% 2.99/1.03 % (1514162)Time elapsed: 0.124 s
% 2.99/1.03 % (1514162)Peak memory usage: 14 MB
% 2.99/1.03 % (1514162)Instructions burned: 193 (million)
% 2.99/1.03 % (1514183)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=1968408130:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2995 on theBenchmark for (2995ds/45Mi)
% 2.99/1.03 % (1514170)Instruction limit reached!
% 2.99/1.03 % (1514170)------------------------------
% 2.99/1.03 % (1514170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.99/1.03 % (1514170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.99/1.03 % (1514170)CaDiCaL version: 2.1.3
% 2.99/1.03 % (1514170)Termination reason: Instruction limit
% 2.99/1.03 % (1514170)Termination phase: Saturation
% 2.99/1.03 % (1514170)Time elapsed: 0.135 s
% 2.99/1.03 % (1514170)Peak memory usage: 14 MB
% 2.99/1.03 % (1514170)Instructions burned: 169 (million)
% 2.99/1.03 % (1514183)Instruction limit reached!
% 2.99/1.03 % (1514183)------------------------------
% 2.99/1.03 % (1514183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.99/1.03 % (1514183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.99/1.03 % (1514183)CaDiCaL version: 2.1.3
% 2.99/1.03 % (1514183)Termination reason: Instruction limit
% 2.99/1.03 % (1514183)Termination phase: Property scanning
% 2.99/1.03 % (1514183)Time elapsed: 0.021 s
% 2.99/1.03 % (1514183)Peak memory usage: 10 MB
% 2.99/1.03 % (1514183)Instructions burned: 47 (million)
% 2.99/1.03 % (1514169)Instruction limit reached!
% 2.99/1.03 % (1514169)------------------------------
% 2.99/1.03 % (1514169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.99/1.03 % (1514169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.99/1.03 % (1514169)CaDiCaL version: 2.1.3
% 2.99/1.03 % (1514169)Termination reason: Instruction limit
% 2.99/1.03 % (1514169)Termination phase: Saturation
% 2.99/1.03 % (1514169)Time elapsed: 0.146 s
% 2.99/1.03 % (1514169)Peak memory usage: 14 MB
% 2.99/1.03 % (1514169)Instructions burned: 181 (million)
% 2.99/1.03 % (1514185)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=1093632462:i=480:rtra=on_2994 on theBenchmark for (2994ds/480Mi)
% 2.99/1.03 % (1514187)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 2.99/1.03 % (1514186)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=617426883:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2994 on theBenchmark for (2994ds/21Mi)
% 2.99/1.03 % (1514187)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=2648945769:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/200Mi)
% 2.99/1.03 % (1514186)Instruction limit reached!
% 2.99/1.03 % (1514186)------------------------------
% 2.99/1.03 % (1514186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.99/1.03 % (1514186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.99/1.03 % (1514186)CaDiCaL version: 2.1.3
% 2.99/1.03 % (1514186)Termination reason: Instruction limit
% 2.99/1.03 % (1514186)Termination phase: shuffling
% 2.99/1.03 % (1514186)Time elapsed: 0.018 s
% 2.99/1.03 % (1514186)Peak memory usage: 10 MB
% 2.99/1.03 % (1514186)Instructions burned: 21 (million)
% 2.99/1.03 % (1514191)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=3348751288:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2994 on theBenchmark for (2994ds/13Mi)
% 2.99/1.03 % (1514191)Instruction limit reached!
% 2.99/1.03 % (1514191)------------------------------
% 2.99/1.03 % (1514191)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.25/1.21 % (1514191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.25/1.21 % (1514191)CaDiCaL version: 2.1.3
% 5.25/1.21 % (1514191)Termination reason: Instruction limit
% 5.25/1.21 % (1514191)Termination phase: shuffling
% 5.25/1.21 % (1514191)Time elapsed: 0.012 s
% 5.25/1.21 % (1514191)Peak memory usage: 10 MB
% 5.25/1.21 % (1514191)Instructions burned: 13 (million)
% 5.25/1.21 % (1514178)Instruction limit reached!
% 5.25/1.21 % (1514178)------------------------------
% 5.25/1.21 % (1514178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.25/1.21 % (1514178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.25/1.21 % (1514178)CaDiCaL version: 2.1.3
% 5.25/1.21 % (1514178)Termination reason: Instruction limit
% 5.25/1.21 % (1514178)Termination phase: Saturation
% 5.25/1.21 % (1514178)Time elapsed: 0.180 s
% 5.25/1.21 % (1514178)Peak memory usage: 17 MB
% 5.25/1.21 % (1514178)Instructions burned: 317 (million)
% 5.25/1.21 % (1514193)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=1194212927:i=66:s2at=3:nm=2:rtra=on:rawr=on_2993 on theBenchmark for (2993ds/66Mi)
% 5.25/1.21 % (1514185)Refutation not found, incomplete strategy
% 5.25/1.21 % (1514185)------------------------------
% 5.25/1.21 % (1514185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.25/1.21 % (1514185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.25/1.21 % (1514185)CaDiCaL version: 2.1.3
% 5.25/1.21 % (1514185)Termination reason: Refutation not found, incomplete strategy
% 5.25/1.21 % (1514185)Time elapsed: 0.093 s
% 5.25/1.21 % (1514185)Peak memory usage: 15 MB
% 5.25/1.21 % (1514185)Instructions burned: 185 (million)
% 5.25/1.21 % (1514185)------------------------------
% 5.25/1.21 % (1514185)------------------------------
% 5.25/1.21 % (1514098)Instruction limit reached!
% 5.25/1.21 % (1514098)------------------------------
% 5.25/1.21 % (1514098)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.25/1.21 % (1514098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.25/1.21 % (1514098)CaDiCaL version: 2.1.3
% 5.25/1.21 % (1514098)Termination reason: Instruction limit
% 5.25/1.21 % (1514098)Termination phase: Saturation
% 5.25/1.21 % (1514098)Time elapsed: 0.575 s
% 5.25/1.21 % (1514098)Peak memory usage: 16 MB
% 5.25/1.21 % (1514098)Instructions burned: 635 (million)
% 5.25/1.21 % (1514157)Instruction limit reached!
% 5.25/1.21 % (1514157)------------------------------
% 5.25/1.21 % (1514157)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.25/1.21 % (1514157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.25/1.21 % (1514157)CaDiCaL version: 2.1.3
% 5.25/1.21 % (1514157)Termination reason: Instruction limit
% 5.25/1.21 % (1514157)Termination phase: Saturation
% 5.25/1.21 % (1514157)Time elapsed: 0.350 s
% 5.25/1.21 % (1514157)Peak memory usage: 17 MB
% 5.25/1.21 % (1514157)Instructions burned: 1240 (million)
% 5.25/1.21 % (1514196)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=1746952940:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/31Mi)
% 5.25/1.21 % (1514198)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=360292894:cond=on:i=34:hud=10:nm=10:rtra=on_2993 on theBenchmark for (2993ds/34Mi)
% 5.25/1.21 % (1514197)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=3611267843:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2993 on theBenchmark for (2993ds/137Mi)
% 5.25/1.21 % (1514193)Instruction limit reached!
% 5.25/1.21 % (1514193)------------------------------
% 5.25/1.21 % (1514193)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.25/1.21 % (1514193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.25/1.21 % (1514193)CaDiCaL version: 2.1.3
% 5.25/1.21 % (1514193)Termination reason: Instruction limit
% 5.25/1.21 % (1514193)Termination phase: SInE selection
% 5.25/1.21 % (1514193)Time elapsed: 0.031 s
% 5.25/1.21 % (1514193)Peak memory usage: 11 MB
% 5.25/1.21 % (1514193)Instructions burned: 68 (million)
% 5.25/1.21 % (1514195)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=3167151531:i=51:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/51Mi)
% 5.25/1.21 % (1514198)Instruction limit reached!
% 5.25/1.21 % (1514198)------------------------------
% 5.66/1.33 % (1514198)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.66/1.33 % (1514198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.66/1.33 % (1514198)CaDiCaL version: 2.1.3
% 5.66/1.33 % (1514198)Termination reason: Instruction limit
% 5.66/1.33 % (1514198)Termination phase: Property scanning
% 5.66/1.33 % (1514198)Time elapsed: 0.010 s
% 5.66/1.33 % (1514198)Peak memory usage: 10 MB
% 5.66/1.33 % (1514198)Instructions burned: 35 (million)
% 5.66/1.33 % (1514196)Instruction limit reached!
% 5.66/1.33 % (1514196)------------------------------
% 5.66/1.33 % (1514196)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.66/1.33 % (1514196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.66/1.33 % (1514196)CaDiCaL version: 2.1.3
% 5.66/1.33 % (1514196)Termination reason: Instruction limit
% 5.66/1.33 % (1514196)Termination phase: shuffling
% 5.66/1.33 % (1514196)Time elapsed: 0.016 s
% 5.66/1.33 % (1514196)Peak memory usage: 10 MB
% 5.66/1.33 % (1514196)Instructions burned: 33 (million)
% 5.66/1.33 % (1514204)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 5.66/1.33 % (1514204)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=3636922649:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2993 on theBenchmark for (2993ds/180Mi)
% 5.66/1.33 % (1514202)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=2984118671:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2993 on theBenchmark for (2993ds/67Mi)
% 5.66/1.33 % (1514205)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=2630877966:st=2:i=246:sd=3:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/246Mi)
% 5.66/1.33 % (1514195)Instruction limit reached!
% 5.66/1.33 % (1514195)------------------------------
% 5.66/1.33 % (1514195)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.66/1.33 % (1514195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.66/1.33 % (1514195)CaDiCaL version: 2.1.3
% 5.66/1.33 % (1514195)Termination reason: Instruction limit
% 5.66/1.33 % (1514195)Termination phase: Preprocessing 3
% 5.66/1.33 % (1514195)Time elapsed: 0.044 s
% 5.66/1.33 % (1514195)Peak memory usage: 12 MB
% 5.66/1.33 % (1514195)Instructions burned: 52 (million)
% 5.66/1.33 % (1514187)Instruction limit reached!
% 5.66/1.33 % (1514187)------------------------------
% 5.66/1.33 % (1514187)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.66/1.33 % (1514187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.66/1.33 % (1514187)CaDiCaL version: 2.1.3
% 5.66/1.33 % (1514187)Termination reason: Instruction limit
% 5.66/1.33 % (1514187)Termination phase: Saturation
% 5.66/1.33 % (1514187)Time elapsed: 0.160 s
% 5.66/1.33 % (1514187)Peak memory usage: 13 MB
% 5.66/1.33 % (1514187)Instructions burned: 200 (million)
% 5.66/1.33 % (1514204)Instruction limit reached!
% 5.66/1.33 % (1514204)------------------------------
% 5.66/1.33 % (1514204)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.66/1.33 % (1514204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.66/1.33 % (1514204)CaDiCaL version: 2.1.3
% 5.66/1.33 % (1514204)Termination reason: Instruction limit
% 5.66/1.33 % (1514204)Termination phase: Saturation
% 5.66/1.33 % (1514204)Time elapsed: 0.043 s
% 5.66/1.33 % (1514204)Peak memory usage: 13 MB
% 5.66/1.33 % (1514204)Instructions burned: 182 (million)
% 5.66/1.33 % (1514197)Instruction limit reached!
% 5.66/1.33 % (1514197)------------------------------
% 5.66/1.33 % (1514197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.66/1.33 % (1514197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.66/1.33 % (1514197)CaDiCaL version: 2.1.3
% 5.66/1.33 % (1514197)Termination reason: Instruction limit
% 5.66/1.33 % (1514197)Termination phase: Saturation
% 5.66/1.33 % (1514197)Time elapsed: 0.066 s
% 5.66/1.33 % (1514197)Peak memory usage: 14 MB
% 5.66/1.33 % (1514197)Instructions burned: 138 (million)
% 5.66/1.33 % (1514202)Instruction limit reached!
% 5.66/1.33 % (1514202)------------------------------
% 5.66/1.33 % (1514202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.66/1.33 % (1514202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.66/1.33 % (1514202)CaDiCaL version: 2.1.3
% 5.66/1.33 % (1514202)Termination reason: Instruction limit
% 5.66/1.33 % (1514202)Termination phase: Property scanning
% 6.40/1.44 % (1514202)Time elapsed: 0.048 s
% 6.40/1.44 % (1514202)Peak memory usage: 11 MB
% 6.40/1.44 % (1514202)Instructions burned: 67 (million)
% 6.40/1.44 % (1514211)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=225684544:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/874Mi)
% 6.40/1.44 % (1514209)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=3666804193:cond=on:i=96:bd=all:rtra=on_2992 on theBenchmark for (2992ds/96Mi)
% 6.40/1.44 % (1514210)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=2674103522:i=427:sd=1:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/427Mi)
% 6.40/1.44 % (1514212)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=731695603:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/515Mi)
% 6.40/1.44 % (1514214)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=3963983008:st=1.5:i=130:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/130Mi)
% 6.40/1.44 % (1514209)Instruction limit reached!
% 6.40/1.44 % (1514209)------------------------------
% 6.40/1.44 % (1514209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.40/1.44 % (1514209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.40/1.44 % (1514209)CaDiCaL version: 2.1.3
% 6.40/1.44 % (1514209)Termination reason: Instruction limit
% 6.40/1.44 % (1514209)Termination phase: Property scanning
% 6.40/1.44 % (1514209)Time elapsed: 0.075 s
% 6.40/1.44 % (1514209)Peak memory usage: 12 MB
% 6.40/1.44 % (1514209)Instructions burned: 98 (million)
% 6.40/1.44 % (1514219)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=163684825:i=44:ep=R:rtra=on:ntd=on_2991 on theBenchmark for (2991ds/44Mi)
% 6.40/1.44 % (1514205)Instruction limit reached!
% 6.40/1.44 % (1514205)------------------------------
% 6.40/1.44 % (1514205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.40/1.44 % (1514205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.40/1.44 % (1514205)CaDiCaL version: 2.1.3
% 6.40/1.44 % (1514205)Termination reason: Instruction limit
% 6.40/1.44 % (1514205)Termination phase: Saturation
% 6.40/1.44 % (1514205)Time elapsed: 0.148 s
% 6.40/1.44 % (1514205)Peak memory usage: 14 MB
% 6.40/1.44 % (1514205)Instructions burned: 247 (million)
% 6.40/1.44 % (1514219)Instruction limit reached!
% 6.40/1.44 % (1514219)------------------------------
% 6.40/1.44 % (1514219)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.40/1.44 % (1514219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.40/1.44 % (1514219)CaDiCaL version: 2.1.3
% 6.40/1.44 % (1514219)Termination reason: Instruction limit
% 6.40/1.44 % (1514219)Termination phase: Property scanning
% 6.40/1.44 % (1514219)Time elapsed: 0.021 s
% 6.40/1.44 % (1514219)Peak memory usage: 10 MB
% 6.40/1.44 % (1514219)Instructions burned: 46 (million)
% 6.40/1.44 % (1514221)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=2161891345:s2a=on:i=571:nm=16:rtra=on_2991 on theBenchmark for (2991ds/571Mi)
% 6.40/1.44 % (1514222)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=3181169357:i=450:rtra=on:ixr=off:ntd=on_2991 on theBenchmark for (2991ds/450Mi)
% 6.40/1.44 % (1514214)Instruction limit reached!
% 6.40/1.44 % (1514214)------------------------------
% 6.40/1.44 % (1514214)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.40/1.44 % (1514214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.40/1.44 % (1514214)CaDiCaL version: 2.1.3
% 6.40/1.44 % (1514214)Termination reason: Instruction limit
% 6.40/1.44 % (1514214)Termination phase: Saturation
% 6.40/1.44 % (1514214)Time elapsed: 0.106 s
% 6.40/1.44 % (1514214)Peak memory usage: 13 MB
% 6.40/1.44 % (1514214)Instructions burned: 131 (million)
% 6.40/1.44 % (1514225)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=1920831706:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2991 on theBenchmark for (2991ds/95Mi)
% 6.40/1.44 % (1514181)Instruction limit reached!
% 6.40/1.44 % (1514181)------------------------------
% 6.40/1.44 % (1514181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.40/1.44 % (1514181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.40/1.44 % (1514181)CaDiCaL version: 2.1.3
% 6.40/1.44 % (1514181)Termination reason: Instruction limit
% 7.58/1.61 % (1514181)Termination phase: Saturation
% 7.58/1.61 % (1514181)Time elapsed: 0.444 s
% 7.58/1.61 % (1514181)Peak memory usage: 18 MB
% 7.58/1.61 % (1514181)Instructions burned: 853 (million)
% 7.58/1.61 % (1514227)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=2933257781:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2990 on theBenchmark for (2990ds/65Mi)
% 7.58/1.61 % (1514225)Instruction limit reached!
% 7.58/1.61 % (1514225)------------------------------
% 7.58/1.61 % (1514225)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.58/1.61 % (1514225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.58/1.61 % (1514225)CaDiCaL version: 2.1.3
% 7.58/1.61 % (1514225)Termination reason: Instruction limit
% 7.58/1.61 % (1514225)Termination phase: Property scanning
% 7.58/1.61 % (1514225)Time elapsed: 0.052 s
% 7.58/1.61 % (1514225)Peak memory usage: 12 MB
% 7.58/1.61 % (1514225)Instructions burned: 96 (million)
% 7.58/1.61 % (1514227)Instruction limit reached!
% 7.58/1.61 % (1514227)------------------------------
% 7.58/1.61 % (1514227)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.58/1.61 % (1514227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.58/1.61 % (1514227)CaDiCaL version: 2.1.3
% 7.58/1.61 % (1514227)Termination reason: Instruction limit
% 7.58/1.61 % (1514227)Termination phase: SInE selection
% 7.58/1.61 % (1514227)Time elapsed: 0.030 s
% 7.58/1.61 % (1514227)Peak memory usage: 11 MB
% 7.58/1.61 % (1514227)Instructions burned: 67 (million)
% 7.58/1.61 % (1514210)Instruction limit reached!
% 7.58/1.61 % (1514210)------------------------------
% 7.58/1.61 % (1514210)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.58/1.61 % (1514210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.58/1.61 % (1514210)CaDiCaL version: 2.1.3
% 7.58/1.61 % (1514210)Termination reason: Instruction limit
% 7.58/1.61 % (1514210)Termination phase: Saturation
% 7.58/1.61 % (1514210)Time elapsed: 0.230 s
% 7.58/1.61 % (1514210)Peak memory usage: 16 MB
% 7.58/1.61 % (1514210)Instructions burned: 428 (million)
% 7.58/1.61 % (1514229)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=1683880391: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_2990 on theBenchmark for (2990ds/105Mi)
% 7.58/1.61 % (1514230)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=262971171:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2990 on theBenchmark for (2990ds/5755Mi)
% 7.58/1.61 % (1514231)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=1762573903:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2990 on theBenchmark for (2990ds/375Mi)
% 7.58/1.61 % (1514211)Instruction limit reached!
% 7.58/1.61 % (1514211)------------------------------
% 7.58/1.61 % (1514211)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.58/1.61 % (1514211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.58/1.61 % (1514211)CaDiCaL version: 2.1.3
% 7.58/1.61 % (1514211)Termination reason: Instruction limit
% 7.58/1.61 % (1514211)Termination phase: Saturation
% 7.58/1.61 % (1514211)Time elapsed: 0.275 s
% 7.58/1.61 % (1514211)Peak memory usage: 17 MB
% 7.58/1.61 % (1514211)Instructions burned: 874 (million)
% 7.58/1.61 % (1514212)Instruction limit reached!
% 7.58/1.61 % (1514212)------------------------------
% 7.58/1.61 % (1514212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.58/1.61 % (1514212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.58/1.61 % (1514212)CaDiCaL version: 2.1.3
% 7.58/1.61 % (1514212)Termination reason: Instruction limit
% 7.58/1.61 % (1514212)Termination phase: Saturation
% 7.58/1.61 % (1514212)Time elapsed: 0.264 s
% 7.58/1.61 % (1514212)Peak memory usage: 17 MB
% 7.58/1.61 % (1514212)Instructions burned: 516 (million)
% 7.58/1.61 % (1514236)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=3631393288:cond=on:i=34:hud=10:nm=10:rtra=on_2989 on theBenchmark for (2989ds/34Mi)
% 7.58/1.61 % (1514229)Instruction limit reached!
% 7.58/1.61 % (1514229)------------------------------
% 8.57/1.81 % (1514229)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.57/1.81 % (1514229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/1.81 % (1514229)CaDiCaL version: 2.1.3
% 8.57/1.81 % (1514229)Termination reason: Instruction limit
% 8.57/1.81 % (1514229)Termination phase: Property scanning
% 8.57/1.81 % (1514229)Time elapsed: 0.057 s
% 8.57/1.81 % (1514229)Peak memory usage: 12 MB
% 8.57/1.81 % (1514229)Instructions burned: 107 (million)
% 8.57/1.81 % (1514235)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=2389719703:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2989 on theBenchmark for (2989ds/495Mi)
% 8.57/1.81 % (1514236)Instruction limit reached!
% 8.57/1.81 % (1514236)------------------------------
% 8.57/1.81 % (1514236)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.57/1.81 % (1514236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/1.81 % (1514236)CaDiCaL version: 2.1.3
% 8.57/1.81 % (1514236)Termination reason: Instruction limit
% 8.57/1.81 % (1514236)Termination phase: shuffling
% 8.57/1.81 % (1514236)Time elapsed: 0.016 s
% 8.57/1.81 % (1514236)Peak memory usage: 10 MB
% 8.57/1.81 % (1514236)Instructions burned: 35 (million)
% 8.57/1.81 % (1514238)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=2671210332:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2989 on theBenchmark for (2989ds/91Mi)
% 8.57/1.81 % (1514240)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=3278830556:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2989 on theBenchmark for (2989ds/66Mi)
% 8.57/1.81 % (1514240)Instruction limit reached!
% 8.57/1.81 % (1514240)------------------------------
% 8.57/1.81 % (1514240)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.57/1.81 % (1514240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/1.81 % (1514240)CaDiCaL version: 2.1.3
% 8.57/1.81 % (1514240)Termination reason: Instruction limit
% 8.57/1.81 % (1514240)Termination phase: Property scanning
% 8.57/1.81 % (1514240)Time elapsed: 0.031 s
% 8.57/1.81 % (1514240)Peak memory usage: 11 MB
% 8.57/1.81 % (1514240)Instructions burned: 67 (million)
% 8.57/1.81 % (1514222)Instruction limit reached!
% 8.57/1.81 % (1514222)------------------------------
% 8.57/1.81 % (1514222)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.57/1.81 % (1514222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/1.81 % (1514222)CaDiCaL version: 2.1.3
% 8.57/1.81 % (1514222)Termination reason: Instruction limit
% 8.57/1.81 % (1514222)Termination phase: Saturation
% 8.57/1.81 % (1514222)Time elapsed: 0.228 s
% 8.57/1.81 % (1514222)Peak memory usage: 17 MB
% 8.57/1.81 % (1514222)Instructions burned: 450 (million)
% 8.57/1.81 % (1514243)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=3402520068:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2988 on theBenchmark for (2988ds/22Mi)
% 8.57/1.81 % (1514244)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=1157461869:i=338:bd=all:ins=4:rtra=on_2988 on theBenchmark for (2988ds/338Mi)
% 8.57/1.81 % (1514243)Instruction limit reached!
% 8.57/1.81 % (1514243)------------------------------
% 8.57/1.81 % (1514243)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.57/1.81 % (1514243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/1.81 % (1514243)CaDiCaL version: 2.1.3
% 8.57/1.81 % (1514243)Termination reason: Instruction limit
% 8.57/1.81 % (1514243)Termination phase: Property scanning
% 8.57/1.81 % (1514243)Time elapsed: 0.011 s
% 8.57/1.81 % (1514243)Peak memory usage: 10 MB
% 8.57/1.81 % (1514243)Instructions burned: 24 (million)
% 8.57/1.81 % (1514238)Instruction limit reached!
% 8.57/1.81 % (1514238)------------------------------
% 8.57/1.81 % (1514238)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.57/1.81 % (1514238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/1.81 % (1514238)CaDiCaL version: 2.1.3
% 8.57/1.81 % (1514238)Termination reason: Instruction limit
% 8.57/1.81 % (1514238)Termination phase: Property scanning
% 8.57/1.81 % (1514238)Time elapsed: 0.070 s
% 8.57/1.81 % (1514238)Peak memory usage: 12 MB
% 8.57/1.81 % (1514238)Instructions burned: 94 (million)
% 8.57/1.81 % (1514247)lrs+10_1_sil=128000:si=on:urr=on:random_seed=2116907833:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2988 on theBenchmark for (2988ds/28Mi)
% 9.47/1.92 % (1514248)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 9.47/1.92 % (1514248)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=4022679091:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2988 on theBenchmark for (2988ds/137Mi)
% 9.47/1.92 % (1514247)Instruction limit reached!
% 9.47/1.92 % (1514247)------------------------------
% 9.47/1.92 % (1514247)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.47/1.92 % (1514247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.47/1.92 % (1514247)CaDiCaL version: 2.1.3
% 9.47/1.92 % (1514247)Termination reason: Instruction limit
% 9.47/1.92 % (1514247)Termination phase: Property scanning
% 9.47/1.92 % (1514247)Time elapsed: 0.009 s
% 9.47/1.92 % (1514247)Peak memory usage: 11 MB
% 9.47/1.92 % (1514247)Instructions burned: 29 (million)
% 9.47/1.92 % (1514251)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=1266702129:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2988 on theBenchmark for (2988ds/340Mi)
% 9.47/1.92 % (1514231)Instruction limit reached!
% 9.47/1.92 % (1514231)------------------------------
% 9.47/1.92 % (1514231)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.47/1.92 % (1514231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.47/1.92 % (1514231)CaDiCaL version: 2.1.3
% 9.47/1.92 % (1514231)Termination reason: Instruction limit
% 9.47/1.92 % (1514231)Termination phase: Saturation
% 9.47/1.92 % (1514231)Time elapsed: 0.212 s
% 9.47/1.92 % (1514231)Peak memory usage: 16 MB
% 9.47/1.92 % (1514231)Instructions burned: 377 (million)
% 9.47/1.92 % (1514248)Instruction limit reached!
% 9.47/1.92 % (1514248)------------------------------
% 9.47/1.92 % (1514248)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.47/1.92 % (1514248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.47/1.92 % (1514248)CaDiCaL version: 2.1.3
% 9.47/1.92 % (1514248)Termination reason: Instruction limit
% 9.47/1.92 % (1514248)Termination phase: Saturation
% 9.47/1.92 % (1514248)Time elapsed: 0.060 s
% 9.47/1.92 % (1514248)Peak memory usage: 13 MB
% 9.47/1.92 % (1514248)Instructions burned: 137 (million)
% 9.47/1.92 % (1514221)Instruction limit reached!
% 9.47/1.92 % (1514221)------------------------------
% 9.47/1.92 % (1514221)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.47/1.92 % (1514221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.47/1.92 % (1514221)CaDiCaL version: 2.1.3
% 9.47/1.92 % (1514221)Termination reason: Instruction limit
% 9.47/1.92 % (1514221)Termination phase: Saturation
% 9.47/1.92 % (1514221)Time elapsed: 0.345 s
% 9.47/1.92 % (1514221)Peak memory usage: 15 MB
% 9.47/1.92 % (1514221)Instructions burned: 571 (million)
% 9.47/1.92 % (1514254)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 9.47/1.92 % (1514254)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=2145599885:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2987 on theBenchmark for (2987ds/373Mi)
% 9.47/1.92 % (1514253)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=2638724627:i=227:sd=1:bd=all:rtra=on:ss=axioms_2987 on theBenchmark for (2987ds/227Mi)
% 9.47/1.92 % (1514255)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=3311866086:i=116:ep=RSTC:rtra=on:ntd=on_2987 on theBenchmark for (2987ds/116Mi)
% 9.47/1.92 % (1514255)Instruction limit reached!
% 9.47/1.92 % (1514255)------------------------------
% 9.47/1.92 % (1514255)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.47/1.92 % (1514255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.47/1.92 % (1514255)CaDiCaL version: 2.1.3
% 9.47/1.92 % (1514255)Termination reason: Instruction limit
% 9.47/1.92 % (1514255)Termination phase: Saturation
% 9.47/1.92 % (1514255)Time elapsed: 0.053 s
% 9.47/1.92 % (1514255)Peak memory usage: 13 MB
% 9.47/1.92 % (1514255)Instructions burned: 117 (million)
% 9.47/1.92 % (1514253)Instruction limit reached!
% 9.47/1.92 % (1514253)------------------------------
% 9.47/1.92 % (1514253)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.72/2.04 % (1514253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.04 % (1514253)CaDiCaL version: 2.1.3
% 11.72/2.04 % (1514253)Termination reason: Instruction limit
% 11.72/2.04 % (1514253)Termination phase: Saturation
% 11.72/2.04 % (1514253)Time elapsed: 0.079 s
% 11.72/2.04 % (1514253)Peak memory usage: 14 MB
% 11.72/2.04 % (1514253)Instructions burned: 228 (million)
% 11.72/2.04 % (1514260)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=1719719864:i=575:rtra=on_2986 on theBenchmark for (2986ds/575Mi)
% 11.72/2.04 % (1514261)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=1783546240:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2986 on theBenchmark for (2986ds/270Mi)
% 11.72/2.04 % (1514251)Instruction limit reached!
% 11.72/2.04 % (1514251)------------------------------
% 11.72/2.04 % (1514251)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.72/2.04 % (1514251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.04 % (1514251)CaDiCaL version: 2.1.3
% 11.72/2.04 % (1514251)Termination reason: Instruction limit
% 11.72/2.04 % (1514251)Termination phase: Saturation
% 11.72/2.04 % (1514251)Time elapsed: 0.171 s
% 11.72/2.04 % (1514251)Peak memory usage: 15 MB
% 11.72/2.04 % (1514251)Instructions burned: 341 (million)
% 11.72/2.04 % (1514264)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=1519545876:hsq=on:hsqr=16,1:s2a=on:i=9840:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2986 on theBenchmark for (2986ds/9840Mi)
% 11.72/2.04 % (1514261)Instruction limit reached!
% 11.72/2.04 % (1514261)------------------------------
% 11.72/2.04 % (1514261)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.72/2.04 % (1514261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.04 % (1514261)CaDiCaL version: 2.1.3
% 11.72/2.04 % (1514261)Termination reason: Instruction limit
% 11.72/2.04 % (1514261)Termination phase: Saturation
% 11.72/2.04 % (1514261)Time elapsed: 0.074 s
% 11.72/2.04 % (1514261)Peak memory usage: 14 MB
% 11.72/2.04 % (1514261)Instructions burned: 270 (million)
% 11.72/2.04 % (1514266)lrs+1010_1_sil=128000:si=on:sos=all:uwa=off:nwc=1:random_seed=3984867630:i=421:rtra=on:ss=axioms_2985 on theBenchmark for (2985ds/421Mi)
% 11.72/2.04 % (1514244)Instruction limit reached!
% 11.72/2.04 % (1514244)------------------------------
% 11.72/2.04 % (1514244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.72/2.04 % (1514244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.04 % (1514244)CaDiCaL version: 2.1.3
% 11.72/2.04 % (1514244)Termination reason: Instruction limit
% 11.72/2.04 % (1514244)Termination phase: Saturation
% 11.72/2.04 % (1514244)Time elapsed: 0.292 s
% 11.72/2.04 % (1514244)Peak memory usage: 17 MB
% 11.72/2.04 % (1514244)Instructions burned: 338 (million)
% 11.72/2.04 % (1514268)WARNING Broken Constraint: if sine_to_age_tolerance(3) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 11.72/2.04 % (1514268)lrs+10_40_sil=128000:tgt=full:cnfonf=off:si=on:sp=reverse_frequency:spb=goal_then_units:uwa=off:fd=preordered:nwc=1:random_seed=2371258980:avsq=on:i=270:s2at=3:avsqr=1,16:rtra=on:ntd=on_2985 on theBenchmark for (2985ds/270Mi)
% 11.72/2.04 % (1514254)Instruction limit reached!
% 11.72/2.04 % (1514254)------------------------------
% 11.72/2.04 % (1514254)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.72/2.04 % (1514254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.04 % (1514254)CaDiCaL version: 2.1.3
% 11.72/2.04 % (1514254)Termination reason: Instruction limit
% 11.72/2.04 % (1514254)Termination phase: Saturation
% 11.72/2.04 % (1514254)Time elapsed: 0.260 s
% 11.72/2.04 % (1514254)Peak memory usage: 14 MB
% 11.72/2.04 % (1514254)Instructions burned: 374 (million)
% 11.72/2.04 % (1514235)Instruction limit reached!
% 11.72/2.04 % (1514235)------------------------------
% 11.72/2.04 % (1514235)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.72/2.04 % (1514235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.04 % (1514235)CaDiCaL version: 2.1.3
% 11.72/2.04 % (1514235)Termination reason: Instruction limit
% 11.72/2.04 % (1514235)Termination phase: Saturation
% 11.72/2.04 % (1514235)Time elapsed: 0.464 s
% 11.72/2.04 % (1514235)Peak memory usage: 17 MB
% 11.72/2.04 % (1514235)Instructions burned: 495 (million)
% 11.72/2.04 % (1514270)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=2643715943:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2985 on theBenchmark for (2985ds/31Mi)
% 11.72/2.04 % (1514271)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 11.72/2.04 % (1514271)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
% 11.72/2.04 % (1514271)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=2592670279:hsqr=1,8:i=1440:s2at=5:add=on:nm=2:rtra=on_2984 on theBenchmark for (2984ds/1440Mi)
% 11.72/2.04 % (1514270)Instruction limit reached!
% 11.72/2.04 % (1514270)------------------------------
% 11.72/2.04 % (1514270)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.72/2.04 % (1514270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.04 % (1514270)CaDiCaL version: 2.1.3
% 11.72/2.04 % (1514270)Termination reason: Instruction limit
% 11.72/2.04 % (1514270)Termination phase: shuffling
% 11.72/2.04 % (1514270)Time elapsed: 0.015 s
% 11.72/2.04 % (1514270)Peak memory usage: 10 MB
% 11.72/2.04 % (1514270)Instructions burned: 32 (million)
% 11.72/2.04 % (1514266)Instruction limit reached!
% 11.72/2.04 % (1514266)------------------------------
% 11.72/2.04 % (1514266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.72/2.04 % (1514266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.04 % (1514266)CaDiCaL version: 2.1.3
% 11.72/2.04 % (1514266)Termination reason: Instruction limit
% 11.72/2.04 % (1514266)Termination phase: Saturation
% 11.72/2.04 % (1514266)Time elapsed: 0.121 s
% 11.72/2.04 % (1514266)Peak memory usage: 16 MB
% 11.72/2.04 % (1514266)Instructions burned: 421 (million)
% 11.72/2.04 % (1514275)lrs+2_16:1_si=on:cbe=off:uwa=interpreted_only:random_seed=458275542:i=111:add=on:fgj=on:rtra=on:fdi=1024_2984 on theBenchmark for (2984ds/111Mi)
% 11.72/2.04 % (1514274)dis+10_2_sil=128000:si=on:random_seed=499527373:s2a=on:i=339:av=off:rtra=on:fe=abstraction:ss=axioms:fsd=on:ntd=on_2984 on theBenchmark for (2984ds/339Mi)
% 11.72/2.04 % (1514275)Instruction limit reached!
% 11.72/2.04 % (1514275)------------------------------
% 11.72/2.04 % (1514275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.72/2.04 % (1514275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.04 % (1514275)CaDiCaL version: 2.1.3
% 11.72/2.04 % (1514275)Termination reason: Instruction limit
% 11.72/2.04 % (1514275)Termination phase: Saturation
% 11.72/2.04 % (1514275)Time elapsed: 0.032 s
% 11.72/2.04 % (1514275)Peak memory usage: 13 MB
% 11.72/2.04 % (1514275)Instructions burned: 115 (million)
% 11.72/2.04 % (1514268)Instruction limit reached!
% 11.72/2.04 % (1514268)------------------------------
% 11.72/2.04 % (1514268)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.72/2.04 % (1514268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.04 % (1514268)CaDiCaL version: 2.1.3
% 11.72/2.04 % (1514268)Termination reason: Instruction limit
% 11.72/2.04 % (1514268)Termination phase: Saturation
% 11.72/2.04 % (1514268)Time elapsed: 0.149 s
% 11.72/2.04 % (1514268)Peak memory usage: 15 MB
% 11.72/2.04 % (1514268)Instructions burned: 270 (million)
% 11.72/2.04 % (1514278)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=798479883:st=3:avsq=on:i=122:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2984 on theBenchmark for (2984ds/122Mi)
% 11.72/2.04 % (1514279)dis+1010_3:2_anc=all_dependent:sil=128000:si=on:sos=on:lma=off:spb=goal_then_units:bce=on:fd=off:random_seed=402499985:uwa_fpi=on:avsq=on:i=136:avsqr=1,32:hud=15:nm=0:rtra=on:ntd=on_2984 on theBenchmark for (2984ds/136Mi)
% 11.72/2.04 % (1514260)Instruction limit reached!
% 11.72/2.04 % (1514260)------------------------------
% 11.72/2.04 % (1514260)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.72/2.04 % (1514260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.04 % (1514260)CaDiCaL version: 2.1.3
% 11.72/2.04 % (1514260)Termination reason: Instruction limit
% 11.72/2.04 % (1514260)Termination phase: Saturation
% 11.72/2.04 % (1514260)Time elapsed: 0.306 s
% 11.72/2.04 % (1514260)Peak memory usage: 17 MB
% 11.72/2.04 % (1514260)Instructions burned: 576 (million)
% 11.72/2.04 % (1514282)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=1817510333:hsq=on:st=2:i=232:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2983 on theBenchmark for (2983ds/232Mi)
% 11.72/2.04 % (1514278)Instruction limit reached!
% 11.72/2.04 % (1514278)------------------------------
% 11.72/2.04 % (1514278)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.72/2.04 % (1514278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.04 % (1514278)CaDiCaL version: 2.1.3
% 11.72/2.04 % (1514278)Termination reason: Instruction limit
% 11.72/2.04 % (1514278)Termination phase: Saturation
% 11.72/2.04 % (1514278)Time elapsed: 0.052 s
% 11.72/2.04 % (1514278)Peak memory usage: 14 MB
% 11.72/2.04 % (1514278)Instructions burned: 124 (million)
% 11.72/2.04 % (1514284)lrs+1010_8:1_sil=128000:tgt=ground:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:sos=on:plsqr=256,1:uwa=off:random_seed=1720680622:i=1254:kws=precedence:bd=preordered:av=off:rtra=on_2983 on theBenchmark for (2983ds/1254Mi)
% 11.72/2.04 % (1514279)Instruction limit reached!
% 11.72/2.04 % (1514279)------------------------------
% 11.72/2.04 % (1514279)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.72/2.04 % (1514279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.04 % (1514279)CaDiCaL version: 2.1.3
% 11.72/2.04 % (1514279)Termination reason: Instruction limit
% 11.72/2.04 % (1514279)Termination phase: Saturation
% 11.72/2.04 % (1514279)Time elapsed: 0.101 s
% 11.72/2.04 % (1514279)Peak memory usage: 13 MB
% 11.72/2.04 % (1514279)Instructions burned: 136 (million)
% 11.72/2.04 % (1514274) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1514090-1514274"...
% 11.72/2.04 % (1514274)...printing done.
% 11.72/2.04 % (1514274)Refutation found. Thanks to Tanya!
% 11.72/2.04 % SZS status Theorem for theBenchmark
% 11.72/2.04 % SZS output start Proof for theBenchmark
% 11.72/2.04 thf(type_def_5, type, extended_ereal: $tType).
% 11.72/2.04 thf(type_def_6, type, real: $tType).
% 11.72/2.04 thf(type_def_7, type, set: $tType > $tType).
% 11.72/2.04 thf(type_def_8, type, nat: $tType).
% 11.72/2.04 thf(type_def_9, type, b: $tType).
% 11.72/2.04 thf(type_def_10, type, a: $tType).
% 11.72/2.04 thf(type_def_11, type, sTfun: ($tType * $tType) > $tType).
% 11.72/2.04 thf(func_def_0, type, type: !>[X0: $tType]:($o)).
% 11.72/2.04 thf(func_def_1, type, one: !>[X0: $tType]:($o)).
% 11.72/2.04 thf(func_def_2, type, ring: !>[X0: $tType]:($o)).
% 11.72/2.04 thf(func_def_3, type, plus: !>[X0: $tType]:($o)).
% 11.72/2.04 thf(func_def_4, type, field: !>[X0: $tType]:($o)).
% 11.72/2.04 thf(func_def_5, type, minus: !>[X0: $tType]:($o)).
% 11.72/2.04 thf(func_def_6, type, times: !>[X0: $tType]:($o)).
% 11.72/2.04 thf(func_def_7, type, ring_1: !>[X0: $tType]:($o)).
% 11.72/2.04 thf(func_def_8, type, semiring: !>[X0: $tType]:($o)).
% 11.72/2.04 thf(func_def_9, type, comm_ring: !>[X0: $tType]:($o)).
% 11.72/2.04 thf(func_def_10, type, group_add: !>[X0: $tType]:($o)).
% 11.72/2.04 thf(func_def_11, type, semiring_0: !>[X0: $tType]:($o)).
% 11.72/2.04 thf(func_def_12, type, finite_finite: !>[X0: $tType]:($o)).
% 11.72/2.04 thf(func_def_13, type, monoid_mult: !>[X0: $tType]:($o)).
% 11.72/2.04 thf(func_def_14, type, ab_group_add: !>[X0: $tType]:($o)).
% 11.72/2.04 thf(func_def_15, type, comm_semiring: !>[X0: $tType]:($o)).
% 11.72/2.04 thf(func_def_16, type, division_ring: !>[X0: $tType]:($o)).
% 11.72/2.04 thf(func_def_17, type, semigroup_add: !>[X0: $tType]:($o)).
% 11.72/2.04 thf(func_def_18, type, semiring_bits: !>[X0: $tType]:($o)).
% 11.72/2.04 thf(func_def_19, type, semidom_divide: !>[X0: $tType]:($o)).
% 11.72/2.04 thf(func_def_20, type, semigroup_mult: !>[X0: $tType]:($o)).
% 11.72/2.04 thf(func_def_21, type, comm_monoid_add: !>[X0: $tType]:($o)).
% 11.72/2.04 thf(func_def_22, type, ab_semigroup_add: !>[X0: $tType]:($o)).
% 11.72/2.04 thf(func_def_23, type, comm_monoid_mult: !>[X0: $tType]:($o)).
% 11.72/2.04 thf(func_def_24, type, ab_semigroup_mult: !>[X0: $tType]:($o)).
% 11.72/2.04 thf(func_def_25, type, real_Vector_scaleR: !>[X0: $tType]:($o)).
% 11.72/2.04 thf(func_def_26, type, cancel_semigroup_add: !>[X0: $tType]:($o)).
% 11.72/2.04 thf(func_def_27, type, comm_s1003936772cancel: !>[X0: $tType]:($o)).
% 11.72/2.04 thf(func_def_28, type, cancel1352612707id_add: !>[X0: $tType]:($o)).
% 11.72/2.04 thf(func_def_29, type, cancel146912293up_add: !>[X0: $tType]:($o)).
% 11.72/2.04 thf(func_def_30, type, real_V1076094709vector: !>[X0: $tType]:($o)).
% 11.72/2.04 thf(func_def_31, type, ordere779506340up_add: !>[X0: $tType]:($o)).
% 11.72/2.04 thf(func_def_32, type, real_V148923926lgebra: !>[X0: $tType]:($o)).
% 11.72/2.04 thf(func_def_33, type, real_V1015715145lgebra: !>[X0: $tType]:($o)).
% 11.72/2.04 thf(func_def_34, type, convex: !>[X0: $tType]:((set @ X0 > $o))).
% 11.72/2.04 thf(func_def_35, type, inverse_inverse: !>[X0: $tType]:((X0 > X0))).
% 11.72/2.04 thf(func_def_36, type, finite_finite2: !>[X0: $tType]:((set @ X0 > $o))).
% 11.72/2.04 thf(func_def_37, type, minus_minus: !>[X0: $tType]:((X0 > X0 > X0))).
% 11.72/2.04 thf(func_def_38, type, one_one: !>[X0: $tType]:(X0)).
% 11.72/2.04 thf(func_def_39, type, plus_plus: !>[X0: $tType]:((X0 > X0 > X0))).
% 11.72/2.04 thf(func_def_40, type, times_times: !>[X0: $tType]:((X0 > X0 > X0))).
% 11.72/2.04 thf(func_def_41, type, groups1340683514dd_sum: !>[X0: $tType, X1: $tType]:(((X0 > X1) > set @ X0 > X1))).
% 11.72/2.04 thf(func_def_42, type, if: !>[X0: $tType]:(($o > X0 > X0 > X0))).
% 11.72/2.04 thf(func_def_43, type, lower_673667120vex_on: !>[X0: $tType]:((set @ X0 > (X0 > extended_ereal) > $o))).
% 11.72/2.04 thf(func_def_44, type, bot_bot: !>[X0: $tType]:(X0)).
% 11.72/2.04 thf(func_def_45, type, ord_less_eq: !>[X0: $tType]:((X0 > X0 > $o))).
% 11.72/2.04 thf(func_def_46, type, real_V1908273582scaleR: !>[X0: $tType]:((real > X0 > X0))).
% 11.72/2.04 thf(func_def_47, type, divide_divide: !>[X0: $tType]:((X0 > X0 > X0))).
% 11.72/2.04 thf(func_def_48, type, collect: !>[X0: $tType]:(((X0 > $o) > set @ X0))).
% 11.72/2.04 thf(func_def_49, type, insert: !>[X0: $tType]:((X0 > set @ X0 > set @ X0))).
% 11.72/2.04 thf(func_def_50, type, member: !>[X0: $tType]:((X0 > set @ X0 > $o))).
% 11.72/2.04 thf(func_def_51, type, c: set @ b).
% 11.72/2.04 thf(func_def_52, type, a2: (a > real)).
% 11.72/2.04 thf(func_def_53, type, aa: (a > real)).
% 11.72/2.04 thf(func_def_54, type, f: (b > extended_ereal)).
% 11.72/2.04 thf(func_def_55, type, i: a).
% 11.72/2.04 thf(func_def_56, type, s: set @ a).
% 11.72/2.04 thf(func_def_57, type, sa: set @ a).
% 11.72/2.04 thf(func_def_58, type, y: (a > b)).
% 11.72/2.04 thf(func_def_62, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 11.72/2.04 thf(func_def_63, type, vNOT: ($o > $o)).
% 11.72/2.04 thf(func_def_64, type, db0: !>[X0: $tType]:(X0)).
% 11.72/2.04 thf(func_def_65, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 11.72/2.04 thf(func_def_66, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 11.72/2.04 thf(func_def_67, type, vIMP: ($o > $o > $o)).
% 11.72/2.04 thf(func_def_68, type, vAND: ($o > $o > $o)).
% 11.72/2.04 thf(func_def_69, type, db1: !>[X0: $tType]:(X0)).
% 11.72/2.04 thf(func_def_70, type, vOR: ($o > $o > $o)).
% 11.72/2.04 thf(func_def_71, type, db2: !>[X0: $tType]:(X0)).
% 11.72/2.04 thf(func_def_72, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 11.72/2.04 thf(func_def_73, type, sP0: !>[X0: $tType, X1: $tType]:(((X1 > X0) > (X0 > X1) > set @ X0 > $o))).
% 11.72/2.04 thf(func_def_74, type, sP1: !>[X0: $tType, X1: $tType]:((set @ X1 > (X0 > X1) > (X1 > X0) > $o))).
% 11.72/2.04 thf(func_def_75, type, sK2: !>[X0: $tType]:(((set @ X0 > $o) > set @ X0))).
% 11.72/2.04 thf(func_def_76, type, sK3: !>[X0: $tType]:((X0 > set @ X0 > set @ X0))).
% 11.72/2.04 thf(func_def_77, type, sK4: !>[X0: $tType, X1: $tType]:(((X1 > X0 > $o) > set @ X1 > X1))).
% 11.72/2.04 thf(func_def_78, type, sK5: !>[X0: $tType, X1: $tType]:(((X1 > X0 > $o) > set @ X1 > X1 > X0))).
% 11.72/2.04 thf(func_def_79, type, sK6: !>[X0: $tType, X1: $tType]:(((X0 > X1) > set @ X0 > (X0 > X1) > X0))).
% 11.72/2.04 thf(func_def_80, type, sK7: !>[X0: $tType]:(((set @ X0 > $o) > X0))).
% 11.72/2.04 thf(func_def_81, type, sK8: !>[X0: $tType]:(((set @ X0 > $o) > set @ X0))).
% 11.72/2.04 thf(func_def_82, type, sK9: !>[X0: $tType, X1: $tType]:(((X1 > set @ X0) > set @ X1 > X1))).
% 11.72/2.04 thf(func_def_83, type, sK10: !>[X0: $tType]:(((set @ X0 > $o) > X0))).
% 11.72/2.04 thf(func_def_84, type, sK11: !>[X0: $tType]:(((set @ X0 > $o) > set @ X0))).
% 11.72/2.04 thf(func_def_85, type, sK12: !>[X0: $tType]:((set @ X0 > X0))).
% 11.72/2.04 thf(func_def_86, type, sK13: !>[X0: $tType]:(((set @ X0 > $o) > set @ X0))).
% 11.72/2.04 thf(func_def_87, type, sK14: !>[X0: $tType]:(((set @ X0 > $o) > set @ X0))).
% 11.72/2.04 thf(func_def_88, type, sK15: !>[X0: $tType]:(((set @ X0 > $o) > X0))).
% 11.72/2.04 thf(func_def_89, type, sK16: !>[X0: $tType]:((set @ X0 > set @ X0))).
% 11.72/2.04 thf(func_def_90, type, sK17: !>[X0: $tType]:((set @ X0 > X0))).
% 11.72/2.04 thf(func_def_91, type, sK18: !>[X0: $tType]:(((set @ X0 > $o) > X0))).
% 11.72/2.04 thf(func_def_92, type, sK19: !>[X0: $tType]:(((set @ X0 > $o) > X0))).
% 11.72/2.04 thf(func_def_93, type, sK20: !>[X0: $tType]:(((set @ X0 > $o) > set @ X0))).
% 11.72/2.04 thf(func_def_94, type, sK21: !>[X0: $tType, X1: $tType]:((set @ X1 > (X0 > X1) > (X1 > X0) > X1))).
% 11.72/2.04 thf(func_def_95, type, sK22: !>[X0: $tType, X1: $tType]:(((X1 > X0) > (X0 > X1) > set @ X0 > X0))).
% 11.72/2.04 thf(func_def_96, type, sK23: !>[X0: $tType, X1: $tType]:((set @ X1 > (X0 > X1) > set @ X0 > X0))).
% 11.72/2.04 thf(func_def_97, type, sK24: !>[X0: $tType, X1: $tType, X2: $tType]:(((X0 > X1) > set @ X0 > (X1 > X2) > (X0 > X2) > X0))).
% 11.72/2.04 thf(func_def_98, type, sK25: !>[X0: $tType, X1: $tType]:(((X1 > X0) > set @ X1 > set @ X0 > X1))).
% 11.72/2.04 thf(func_def_99, type, sK26: !>[X0: $tType]:((X0 > set @ X0 > set @ X0))).
% 11.72/2.04 thf(func_def_100, type, sK27: !>[X0: $tType, X1: $tType]:(((X0 > X1) > (X0 > X1) > X0))).
% 11.72/2.04 thf(func_def_101, type, sK28: !>[X0: $tType]:(((set @ X0 > $o) > set @ X0))).
% 11.72/2.04 thf(func_def_102, type, sK29: !>[X0: $tType]:(((set @ X0 > $o) > X0))).
% 11.72/2.04 thf(func_def_103, type, sK30: !>[X0: $tType, X1: $tType, X2: $tType]:((set @ X1 > set @ X2 > (X2 > X1) > (X2 > X0) > (X1 > X0) > (X1 > X2) > X2))).
% 11.72/2.04 thf(func_def_104, type, sK31: !>[X0: $tType, X1: $tType]:((set @ X0 > set @ X1 > (X1 > X0) > (X0 > X1) > X0))).
% 11.72/2.04 thf(func_def_105, type, sK32: !>[X0: $tType, X1: $tType, X2: $tType]:(((X0 > X2) > (X2 > X1) > (X0 > X1) > set @ X2 > set @ X0 > X0))).
% 11.72/2.04 thf(func_def_106, type, sK33: !>[X0: $tType, X1: $tType]:(((X0 > X1) > set @ X1 > set @ X0 > X1))).
% 11.72/2.04 thf(func_def_107, type, sK34: !>[X0: $tType, X1: $tType]:((X0 > (X0 > X1) > set @ X1 > set @ X0 > X0))).
% 11.72/2.04 thf(func_def_108, type, sK35: set @ a).
% 11.72/2.04 thf(func_def_109, type, sK36: a).
% 11.72/2.04 thf(f3,axiom,(
% 11.72/2.04 (((groups1340683514dd_sum @ a @ b @ (^[X0 : a] : ((real_V1908273582scaleR @ b @ (inverse_inverse @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i))) @ (real_V1908273582scaleR @ b @ (aa @ X0) @ (y @ X0))))) @ sa)) = ((real_V1908273582scaleR @ b @ (inverse_inverse @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i))) @ (groups1340683514dd_sum @ a @ b @ (^[X1 : a] : ((real_V1908273582scaleR @ b @ (aa @ X1) @ (y @ X1)))) @ sa))))),
% 11.72/2.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2__092_060open_062_I_092_060Sum_062x_092_060in_062s_O_Aa_Ax_A_K_092_060_094sub_062R_Ay_Ax_A_P_092_060_094sub_062R_A_I1_A_N_Aa_Ai_J_J_A_061_A_I_092_060Sum_062j_092_060in_062s_O_Aa_Aj_A_K_092_060_094sub_062R_Ay_Aj_J_A_P_092_060_094sub_062R_A_I1_A_N_Aa_Ai_J_092_060close_062)).
% 11.72/2.04 thf(f12,axiom,(
% 11.72/2.04 ! [X0 : $tType] : (real_V1076094709vector @ X0 => ! [X3 : X0,X2 : real,X1 : real] : (((real_V1908273582scaleR @ X0 @ X1 @ (real_V1908273582scaleR @ X0 @ X2 @ X3))) = ((real_V1908273582scaleR @ X0 @ (times_times @ real @ X1 @ X2) @ X3))))),
% 11.72/2.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_11_scaleR__scaleR)).
% 11.72/2.04 thf(f31,axiom,(
% 11.72/2.04 (real_V1908273582scaleR @ real = times_times @ real)),
% 11.72/2.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_30_real__scaleR__def)).
% 11.72/2.04 thf(f32,axiom,(
% 11.72/2.04 ! [X0 : $tType] : (real_V1076094709vector @ X0 => ! [X1 : real,X2 : real,X3 : X0] : (((real_V1908273582scaleR @ X0 @ X1 @ (real_V1908273582scaleR @ X0 @ X2 @ X3))) = ((real_V1908273582scaleR @ X0 @ X2 @ (real_V1908273582scaleR @ X0 @ X1 @ X3)))))),
% 11.72/2.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_31_scale__left__commute)).
% 11.72/2.04 thf(f351,axiom,(
% 11.72/2.04 real_V1076094709vector @ b),
% 11.72/2.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tfree_0)).
% 11.72/2.04 thf(f352,conjecture,(
% 11.72/2.04 (((f @ (plus_plus @ b @ (real_V1908273582scaleR @ b @ (times_times @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i)) @ (inverse_inverse @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i)))) @ (groups1340683514dd_sum @ a @ b @ (^[X0 : a] : ((real_V1908273582scaleR @ b @ (aa @ X0) @ (y @ X0)))) @ sa)) @ (real_V1908273582scaleR @ b @ (aa @ i) @ (y @ i))))) = ((f @ (plus_plus @ b @ (real_V1908273582scaleR @ b @ (minus_minus @ real @ one_one @ real @ (aa @ i)) @ (groups1340683514dd_sum @ a @ b @ (^[X0 : a] : ((real_V1908273582scaleR @ b @ (times_times @ real @ (aa @ X0) @ (inverse_inverse @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i)))) @ (y @ X0)))) @ sa)) @ (real_V1908273582scaleR @ b @ (aa @ i) @ (y @ i))))))),
% 11.72/2.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0)).
% 11.72/2.04 thf(f353,negated_conjecture,(
% 11.72/2.04 ~ (((f @ (plus_plus @ b @ (real_V1908273582scaleR @ b @ (times_times @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i)) @ (inverse_inverse @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i)))) @ (groups1340683514dd_sum @ a @ b @ (^[X0 : a] : ((real_V1908273582scaleR @ b @ (aa @ X0) @ (y @ X0)))) @ sa)) @ (real_V1908273582scaleR @ b @ (aa @ i) @ (y @ i))))) = ((f @ (plus_plus @ b @ (real_V1908273582scaleR @ b @ (minus_minus @ real @ one_one @ real @ (aa @ i)) @ (groups1340683514dd_sum @ a @ b @ (^[X0 : a] : ((real_V1908273582scaleR @ b @ (times_times @ real @ (aa @ X0) @ (inverse_inverse @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i)))) @ (y @ X0)))) @ sa)) @ (real_V1908273582scaleR @ b @ (aa @ i) @ (y @ i))))))),
% 11.72/2.04 inference(negated_conjecture,[status(cth)],[f352])).
% 11.72/2.04 thf(f478,plain,(
% 11.72/2.04 ! [X0 : $tType] : (real_V1076094709vector @ X0 => ! [X1 : real,X2 : real,X3 : X0] : (((real_V1908273582scaleR @ X0 @ X1 @ (real_V1908273582scaleR @ X0 @ X2 @ X3))) = ((real_V1908273582scaleR @ X0 @ X2 @ (real_V1908273582scaleR @ X0 @ X1 @ X3)))))),
% 11.72/2.04 inference(rectify,[],[f32])).
% 11.72/2.04 thf(f479,plain,(
% 11.72/2.04 ! [X0 : $tType] : ((real_V1076094709vector @ X0 = $true) => ! [X3 : X0,X1 : real,X2 : real] : (((real_V1908273582scaleR @ X0 @ X1 @ (real_V1908273582scaleR @ X0 @ X2 @ X3))) = ((real_V1908273582scaleR @ X0 @ X2 @ (real_V1908273582scaleR @ X0 @ X1 @ X3)))))),
% 11.72/2.04 inference(fool_elimination,[],[f478])).
% 11.72/2.04 thf(f522,plain,(
% 11.72/2.04 (((groups1340683514dd_sum @ a @ b @ (^[X0 : a] : ((real_V1908273582scaleR @ b @ (inverse_inverse @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i))) @ (real_V1908273582scaleR @ b @ (aa @ X0) @ (y @ X0))))) @ sa)) = ((real_V1908273582scaleR @ b @ (inverse_inverse @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i))) @ (groups1340683514dd_sum @ a @ b @ (^[X1 : a] : ((real_V1908273582scaleR @ b @ (aa @ X1) @ (y @ X1)))) @ sa))))),
% 11.72/2.04 inference(rectify,[],[f3])).
% 11.72/2.04 thf(f523,plain,(
% 11.72/2.04 (((real_V1908273582scaleR @ b @ (inverse_inverse @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i))) @ (groups1340683514dd_sum @ a @ b @ (^[Y0 : a]: (real_V1908273582scaleR @ b @ (aa @ Y0) @ (y @ Y0))) @ sa))) = ((groups1340683514dd_sum @ a @ b @ (^[Y0 : a]: (real_V1908273582scaleR @ b @ (inverse_inverse @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i))) @ (real_V1908273582scaleR @ b @ (aa @ Y0) @ (y @ Y0)))) @ sa)))),
% 11.72/2.04 inference(fool_elimination,[],[f522])).
% 11.72/2.04 thf(f650,plain,(
% 11.72/2.04 real_V1076094709vector @ b),
% 11.72/2.04 inference(rectify,[],[f351])).
% 11.72/2.04 thf(f651,plain,(
% 11.72/2.04 (real_V1076094709vector @ b = $true)),
% 11.72/2.04 inference(fool_elimination,[],[f650])).
% 11.72/2.04 thf(f660,plain,(
% 11.72/2.04 ~ (((f @ (plus_plus @ b @ (real_V1908273582scaleR @ b @ (times_times @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i)) @ (inverse_inverse @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i)))) @ (groups1340683514dd_sum @ a @ b @ (^[X0 : a] : ((real_V1908273582scaleR @ b @ (aa @ X0) @ (y @ X0)))) @ sa)) @ (real_V1908273582scaleR @ b @ (aa @ i) @ (y @ i))))) = ((f @ (plus_plus @ b @ (real_V1908273582scaleR @ b @ (minus_minus @ real @ one_one @ real @ (aa @ i)) @ (groups1340683514dd_sum @ a @ b @ (^[X1 : a] : ((real_V1908273582scaleR @ b @ (times_times @ real @ (aa @ X1) @ (inverse_inverse @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i)))) @ (y @ X1)))) @ sa)) @ (real_V1908273582scaleR @ b @ (aa @ i) @ (y @ i))))))),
% 11.72/2.05 inference(rectify,[],[f353])).
% 11.72/2.05 thf(f661,plain,(
% 11.72/2.05 ~ (((f @ (plus_plus @ b @ (real_V1908273582scaleR @ b @ (minus_minus @ real @ one_one @ real @ (aa @ i)) @ (groups1340683514dd_sum @ a @ b @ (^[Y0 : a]: (real_V1908273582scaleR @ b @ (times_times @ real @ (aa @ Y0) @ (inverse_inverse @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i)))) @ (y @ Y0))) @ sa)) @ (real_V1908273582scaleR @ b @ (aa @ i) @ (y @ i))))) = ((f @ (plus_plus @ b @ (real_V1908273582scaleR @ b @ (times_times @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i)) @ (inverse_inverse @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i)))) @ (groups1340683514dd_sum @ a @ b @ (^[Y0 : a]: (real_V1908273582scaleR @ b @ (aa @ Y0) @ (y @ Y0))) @ sa)) @ (real_V1908273582scaleR @ b @ (aa @ i) @ (y @ i))))))),
% 11.72/2.05 inference(fool_elimination,[],[f660])).
% 11.72/2.05 thf(f824,plain,(
% 11.72/2.05 ! [X0 : $tType] : (real_V1076094709vector @ X0 => ! [X1 : X0,X2 : real,X3 : real] : (((real_V1908273582scaleR @ X0 @ (times_times @ real @ X3 @ X2) @ X1)) = ((real_V1908273582scaleR @ X0 @ X3 @ (real_V1908273582scaleR @ X0 @ X2 @ X1)))))),
% 11.72/2.05 inference(rectify,[],[f12])).
% 11.72/2.05 thf(f825,plain,(
% 11.72/2.05 ! [X0 : $tType] : ((real_V1076094709vector @ X0 = $true) => ! [X3 : real,X1 : X0,X2 : real] : (((real_V1908273582scaleR @ X0 @ (times_times @ real @ X3 @ X2) @ X1)) = ((real_V1908273582scaleR @ X0 @ X3 @ (real_V1908273582scaleR @ X0 @ X2 @ X1)))))),
% 11.72/2.05 inference(fool_elimination,[],[f824])).
% 11.72/2.05 thf(f1006,plain,(
% 11.72/2.05 (((f @ (plus_plus @ b @ (real_V1908273582scaleR @ b @ (minus_minus @ real @ one_one @ real @ (aa @ i)) @ (groups1340683514dd_sum @ a @ b @ (^[Y0 : a]: (real_V1908273582scaleR @ b @ (times_times @ real @ (aa @ Y0) @ (inverse_inverse @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i)))) @ (y @ Y0))) @ sa)) @ (real_V1908273582scaleR @ b @ (aa @ i) @ (y @ i))))) != ((f @ (plus_plus @ b @ (real_V1908273582scaleR @ b @ (times_times @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i)) @ (inverse_inverse @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i)))) @ (groups1340683514dd_sum @ a @ b @ (^[Y0 : a]: (real_V1908273582scaleR @ b @ (aa @ Y0) @ (y @ Y0))) @ sa)) @ (real_V1908273582scaleR @ b @ (aa @ i) @ (y @ i))))))),
% 11.72/2.05 inference(flattening,[],[f661])).
% 11.72/2.05 thf(f1063,plain,(
% 11.72/2.05 ! [X0 : $tType] : (! [X3 : X0,X1 : real,X2 : real] : (((real_V1908273582scaleR @ X0 @ X1 @ (real_V1908273582scaleR @ X0 @ X2 @ X3))) = ((real_V1908273582scaleR @ X0 @ X2 @ (real_V1908273582scaleR @ X0 @ X1 @ X3)))) | (real_V1076094709vector @ X0 != $true))),
% 11.72/2.05 inference(ennf_transformation,[],[f479])).
% 11.72/2.05 thf(f1097,plain,(
% 11.72/2.05 ! [X0 : $tType] : ((real_V1076094709vector @ X0 != $true) | ! [X3 : real,X1 : X0,X2 : real] : (((real_V1908273582scaleR @ X0 @ (times_times @ real @ X3 @ X2) @ X1)) = ((real_V1908273582scaleR @ X0 @ X3 @ (real_V1908273582scaleR @ X0 @ X2 @ X1)))))),
% 11.72/2.05 inference(ennf_transformation,[],[f825])).
% 11.72/2.05 thf(f1158,plain,(
% 11.72/2.05 ! [X0 : $tType] : (! [X1 : X0,X2 : real,X3 : real] : (((real_V1908273582scaleR @ X0 @ X2 @ (real_V1908273582scaleR @ X0 @ X3 @ X1))) = ((real_V1908273582scaleR @ X0 @ X3 @ (real_V1908273582scaleR @ X0 @ X2 @ X1)))) | (real_V1076094709vector @ X0 != $true))),
% 11.72/2.05 inference(rectify,[],[f1063])).
% 11.72/2.05 thf(f1196,plain,(
% 11.72/2.05 ! [X0 : $tType] : ((real_V1076094709vector @ X0 != $true) | ! [X1 : real,X2 : X0,X3 : real] : (((real_V1908273582scaleR @ X0 @ X1 @ (real_V1908273582scaleR @ X0 @ X3 @ X2))) = ((real_V1908273582scaleR @ X0 @ (times_times @ real @ X1 @ X3) @ X2))))),
% 11.72/2.05 inference(rectify,[],[f1097])).
% 11.72/2.05 thf(f1259,plain,(
% 11.72/2.05 ( ! [X0 : $tType,X2 : real,X3 : real,X1 : X0] : ((real_V1076094709vector @ X0 != $true) | (((real_V1908273582scaleR @ X0 @ X2 @ (real_V1908273582scaleR @ X0 @ X3 @ X1))) = ((real_V1908273582scaleR @ X0 @ X3 @ (real_V1908273582scaleR @ X0 @ X2 @ X1))))) )),
% 11.72/2.05 inference(cnf_transformation,[],[f1158])).
% 11.72/2.05 thf(f1266,plain,(
% 11.72/2.05 (times_times @ real = real_V1908273582scaleR @ real)),
% 11.72/2.05 inference(cnf_transformation,[],[f31])).
% 11.72/2.05 thf(f1328,plain,(
% 11.72/2.05 ( ! [X0 : $tType,X2 : X0,X3 : real,X1 : real] : ((real_V1076094709vector @ X0 != $true) | (((real_V1908273582scaleR @ X0 @ X1 @ (real_V1908273582scaleR @ X0 @ X3 @ X2))) = ((real_V1908273582scaleR @ X0 @ (times_times @ real @ X1 @ X3) @ X2)))) )),
% 11.72/2.05 inference(cnf_transformation,[],[f1196])).
% 11.72/2.05 thf(f1343,plain,(
% 11.72/2.05 (((f @ (plus_plus @ b @ (real_V1908273582scaleR @ b @ (minus_minus @ real @ one_one @ real @ (aa @ i)) @ (groups1340683514dd_sum @ a @ b @ (^[Y0 : a]: (real_V1908273582scaleR @ b @ (times_times @ real @ (aa @ Y0) @ (inverse_inverse @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i)))) @ (y @ Y0))) @ sa)) @ (real_V1908273582scaleR @ b @ (aa @ i) @ (y @ i))))) != ((f @ (plus_plus @ b @ (real_V1908273582scaleR @ b @ (times_times @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i)) @ (inverse_inverse @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i)))) @ (groups1340683514dd_sum @ a @ b @ (^[Y0 : a]: (real_V1908273582scaleR @ b @ (aa @ Y0) @ (y @ Y0))) @ sa)) @ (real_V1908273582scaleR @ b @ (aa @ i) @ (y @ i))))))),
% 11.72/2.05 inference(cnf_transformation,[],[f1006])).
% 11.72/2.05 thf(f1401,plain,(
% 11.72/2.05 (real_V1076094709vector @ b = $true)),
% 11.72/2.05 inference(cnf_transformation,[],[f651])).
% 11.72/2.05 thf(f1402,plain,(
% 11.72/2.05 (((real_V1908273582scaleR @ b @ (inverse_inverse @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i))) @ (groups1340683514dd_sum @ a @ b @ (^[Y0 : a]: (real_V1908273582scaleR @ b @ (aa @ Y0) @ (y @ Y0))) @ sa))) = ((groups1340683514dd_sum @ a @ b @ (^[Y0 : a]: (real_V1908273582scaleR @ b @ (inverse_inverse @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i))) @ (real_V1908273582scaleR @ b @ (aa @ Y0) @ (y @ Y0)))) @ sa)))),
% 11.72/2.05 inference(cnf_transformation,[],[f523])).
% 11.72/2.05 thf(f1450,plain,(
% 11.72/2.05 ( ! [X1 : real] : ((((times_times @ real @ X1)) = ((real_V1908273582scaleR @ real @ X1)))) )),
% 11.72/2.05 inference(argument_congruence,[],[f1266])).
% 11.72/2.05 thf(f1502,plain,(
% 11.72/2.05 ( ! [X2 : b,X0 : real,X1 : real] : (($true != $true) | (((real_V1908273582scaleR @ b @ X1 @ (real_V1908273582scaleR @ b @ X0 @ X2))) = ((real_V1908273582scaleR @ b @ X0 @ (real_V1908273582scaleR @ b @ X1 @ X2))))) )),
% 11.72/2.05 inference(constrained_superposition,[],[f1259,f1401])).
% 11.72/2.05 thf(f1504,plain,(
% 11.72/2.05 ( ! [X2 : b,X0 : real,X1 : real] : ((((real_V1908273582scaleR @ b @ X1 @ (real_V1908273582scaleR @ b @ X0 @ X2))) = ((real_V1908273582scaleR @ b @ X0 @ (real_V1908273582scaleR @ b @ X1 @ X2))))) )),
% 11.72/2.05 inference(trivial_inequality_removal,[],[f1502])).
% 11.72/2.05 thf(f1506,plain,(
% 11.72/2.05 ( ! [X2 : b,X0 : real,X1 : real] : ((((real_V1908273582scaleR @ b @ (times_times @ real @ X0 @ X1) @ X2)) = ((real_V1908273582scaleR @ b @ X0 @ (real_V1908273582scaleR @ b @ X1 @ X2)))) | ($true != $true)) )),
% 11.72/2.05 inference(constrained_superposition,[],[f1328,f1401])).
% 11.72/2.05 thf(f1509,plain,(
% 11.72/2.05 ( ! [X2 : b,X0 : real,X1 : real] : ((((real_V1908273582scaleR @ b @ (times_times @ real @ X0 @ X1) @ X2)) = ((real_V1908273582scaleR @ b @ X0 @ (real_V1908273582scaleR @ b @ X1 @ X2))))) )),
% 11.72/2.05 inference(trivial_inequality_removal,[],[f1506])).
% 11.72/2.05 thf(f1620,plain,(
% 11.72/2.05 ( ! [X2 : real,X1 : real] : ((((times_times @ real @ X1 @ X2)) = ((real_V1908273582scaleR @ real @ X1 @ X2)))) )),
% 11.72/2.05 inference(argument_congruence,[],[f1450])).
% 11.72/2.05 thf(f1693,plain,(
% 11.72/2.05 (((f @ (plus_plus @ b @ (real_V1908273582scaleR @ b @ (minus_minus @ real @ one_one @ real @ (aa @ i)) @ (groups1340683514dd_sum @ a @ b @ (^[Y0 : a]: (real_V1908273582scaleR @ b @ (times_times @ real @ (aa @ Y0) @ (inverse_inverse @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i)))) @ (y @ Y0))) @ sa)) @ (real_V1908273582scaleR @ b @ (aa @ i) @ (y @ i))))) != ((f @ (plus_plus @ b @ (real_V1908273582scaleR @ b @ (real_V1908273582scaleR @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i)) @ (inverse_inverse @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i)))) @ (groups1340683514dd_sum @ a @ b @ (^[Y0 : a]: (real_V1908273582scaleR @ b @ (aa @ Y0) @ (y @ Y0))) @ sa)) @ (real_V1908273582scaleR @ b @ (aa @ i) @ (y @ i))))))),
% 11.72/2.05 inference(constrained_superposition,[],[f1343,f1620])).
% 11.72/2.05 thf(f3744,plain,(
% 11.72/2.05 ( ! [X2 : b,X0 : real,X1 : real] : ((((real_V1908273582scaleR @ b @ (real_V1908273582scaleR @ real @ X0 @ X1) @ X2)) = ((real_V1908273582scaleR @ b @ X0 @ (real_V1908273582scaleR @ b @ X1 @ X2))))) )),
% 11.72/2.05 inference(forward_demodulation,[],[f1509,f1620])).
% 11.72/2.05 thf(f3764,plain,(
% 11.72/2.05 (((f @ (plus_plus @ b @ (real_V1908273582scaleR @ b @ (minus_minus @ real @ one_one @ real @ (aa @ i)) @ (groups1340683514dd_sum @ a @ b @ (^[Y0 : a]: (real_V1908273582scaleR @ b @ (times_times @ real @ (aa @ Y0) @ (inverse_inverse @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i)))) @ (y @ Y0))) @ sa)) @ (real_V1908273582scaleR @ b @ (aa @ i) @ (y @ i))))) != ((f @ (plus_plus @ b @ (real_V1908273582scaleR @ b @ (minus_minus @ real @ one_one @ real @ (aa @ i)) @ (real_V1908273582scaleR @ b @ (inverse_inverse @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i))) @ (groups1340683514dd_sum @ a @ b @ (^[Y0 : a]: (real_V1908273582scaleR @ b @ (aa @ Y0) @ (y @ Y0))) @ sa))) @ (real_V1908273582scaleR @ b @ (aa @ i) @ (y @ i))))))),
% 11.72/2.05 inference(constrained_superposition,[],[f1693,f3744])).
% 11.72/2.05 thf(f3788,plain,(
% 11.72/2.05 (((f @ (plus_plus @ b @ (real_V1908273582scaleR @ b @ (minus_minus @ real @ one_one @ real @ (aa @ i)) @ (real_V1908273582scaleR @ b @ (inverse_inverse @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i))) @ (groups1340683514dd_sum @ a @ b @ (^[Y0 : a]: (real_V1908273582scaleR @ b @ (aa @ Y0) @ (y @ Y0))) @ sa))) @ (real_V1908273582scaleR @ b @ (aa @ i) @ (y @ i))))) != ((f @ (plus_plus @ b @ (real_V1908273582scaleR @ b @ (minus_minus @ real @ one_one @ real @ (aa @ i)) @ (real_V1908273582scaleR @ b @ (inverse_inverse @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i))) @ (groups1340683514dd_sum @ a @ b @ (^[Y0 : a]: (real_V1908273582scaleR @ b @ (aa @ Y0) @ (y @ Y0))) @ sa))) @ (real_V1908273582scaleR @ b @ (aa @ i) @ (y @ i)))))) | ((^[Y0 : a]: (real_V1908273582scaleR @ b @ (times_times @ real @ (aa @ Y0) @ (inverse_inverse @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i)))) @ (y @ Y0))) != (^[Y0 : a]: (real_V1908273582scaleR @ b @ (inverse_inverse @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i))) @ (real_V1908273582scaleR @ b @ (aa @ Y0) @ (y @ Y0)))))),
% 11.72/2.05 inference(constrained_superposition,[],[f3764,f1402])).
% 11.72/2.05 thf(f3789,plain,(
% 11.72/2.05 ((^[Y0 : a]: (real_V1908273582scaleR @ b @ (times_times @ real @ (aa @ Y0) @ (inverse_inverse @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i)))) @ (y @ Y0))) != (^[Y0 : a]: (real_V1908273582scaleR @ b @ (inverse_inverse @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i))) @ (real_V1908273582scaleR @ b @ (aa @ Y0) @ (y @ Y0)))))),
% 11.72/2.05 inference(trivial_inequality_removal,[],[f3788])).
% 11.72/2.05 thf(f3791,plain,(
% 11.72/2.05 ((((^[Y0 : a]: (real_V1908273582scaleR @ b @ (inverse_inverse @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i))) @ (real_V1908273582scaleR @ b @ (aa @ Y0) @ (y @ Y0)))) @ sK36)) != (((^[Y0 : a]: (real_V1908273582scaleR @ b @ (times_times @ real @ (aa @ Y0) @ (inverse_inverse @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i)))) @ (y @ Y0))) @ sK36)))),
% 11.72/2.05 inference(negative_extensionality,[],[f3789])).
% 11.72/2.05 thf(f3793,plain,(
% 11.72/2.05 (((real_V1908273582scaleR @ b @ (inverse_inverse @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i))) @ (real_V1908273582scaleR @ b @ (aa @ sK36) @ (y @ sK36)))) != ((real_V1908273582scaleR @ b @ (times_times @ real @ (aa @ sK36) @ (inverse_inverse @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i)))) @ (y @ sK36))))),
% 11.72/2.05 inference(beta-eta_normalization,[],[f3791])).
% 11.72/2.05 thf(f3794,plain,(
% 11.72/2.05 (((real_V1908273582scaleR @ b @ (real_V1908273582scaleR @ real @ (aa @ sK36) @ (inverse_inverse @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i)))) @ (y @ sK36))) != ((real_V1908273582scaleR @ b @ (inverse_inverse @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i))) @ (real_V1908273582scaleR @ b @ (aa @ sK36) @ (y @ sK36)))))),
% 11.72/2.05 inference(forward_demodulation,[],[f3793,f1620])).
% 11.72/2.05 thf(f3796,plain,(
% 11.72/2.05 (((real_V1908273582scaleR @ b @ (real_V1908273582scaleR @ real @ (aa @ sK36) @ (inverse_inverse @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i)))) @ (y @ sK36))) != ((real_V1908273582scaleR @ b @ (aa @ sK36) @ (real_V1908273582scaleR @ b @ (inverse_inverse @ real @ (minus_minus @ real @ one_one @ real @ (aa @ i))) @ (y @ sK36)))))),
% 11.72/2.05 inference(forward_demodulation,[],[f3794,f1504])).
% 11.72/2.05 thf(f3797,plain,(
% 11.72/2.05 $false),
% 11.72/2.05 inference(forward_subsumption_resolution,[],[f3796,f3744])).
% 11.72/2.05 % SZS output end Proof for theBenchmark
% 11.72/2.05 % (1514274)------------------------------
% 11.72/2.05 % (1514274)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.72/2.05 % (1514274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.05 % (1514274)CaDiCaL version: 2.1.3
% 11.72/2.05 % (1514274)Termination reason: Refutation
% 11.72/2.05 % (1514274)Time elapsed: 0.179 s
% 11.72/2.05 % (1514274)Peak memory usage: 14 MB
% 11.72/2.05 % (1514274)Instructions burned: 272 (million)
% 11.72/2.05 % (1514090)Success in time 1.749 s
% 11.72/2.05 % Vampire exiting
%------------------------------------------------------------------------------