%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP156^2 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n008.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:35 AM UTC 2026
% Result : Theorem 3.04s 0.93s
% Output : Refutation 3.04s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP156^2 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.25 % Computer : n008.cluster.edu
% 0.09/0.25 % Model : x86_64 x86_64
% 0.09/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.25 % Memory : 8046.5625MB
% 0.09/0.25 % OS : Linux 6.8.0-71-generic
% 0.09/0.25 % CPULimit : 300
% 0.09/0.25 % WCLimit : 300
% 0.09/0.25 % DateTime : Tue Sep 29 20:03:24 UTC 2026
% 0.09/0.25 % CPUTime :
% 0.09/0.25 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.23/0.31 Running higher-order theorem proving
% 0.23/0.37 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.74/0.58 % (3664585)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.74/0.58 % (3664591)lrs+10_16_si=on:nwc=1.5:random_seed=1681138274:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.74/0.58 % (3664590)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=2820685057:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.74/0.58 % (3664596)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.74/0.58 % (3664596)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.74/0.58 % (3664591)Instruction limit reached!
% 0.74/0.58 % (3664591)------------------------------
% 0.74/0.58 % (3664591)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.74/0.58 % (3664591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.74/0.58 % (3664591)CaDiCaL version: 2.1.3
% 0.74/0.58 % (3664591)Termination reason: Instruction limit
% 0.74/0.58 % (3664591)Termination phase: shuffling
% 0.74/0.58 % (3664591)Time elapsed: 0.008 s
% 0.74/0.58 % (3664591)Peak memory usage: 10 MB
% 0.74/0.58 % (3664591)Instructions burned: 18 (million)
% 0.74/0.58 % (3664592)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=868376387:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.74/0.58 % (3664593)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=3830443152:hsq=on:hsqr=16,1:s2a=on:i=634:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2999 on theBenchmark for (2999ds/634Mi)
% 0.74/0.58 % (3664595)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=2627519452:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.74/0.58 % (3664594)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=2471342564:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.74/0.58 % (3664596)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=2524299192:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.74/0.58 % (3664592)Instruction limit reached!
% 0.74/0.58 % (3664592)------------------------------
% 0.74/0.58 % (3664592)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.74/0.58 % (3664592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.74/0.58 % (3664592)CaDiCaL version: 2.1.3
% 0.74/0.58 % (3664592)Termination reason: Instruction limit
% 0.74/0.58 % (3664592)Termination phase: shuffling
% 0.74/0.58 % (3664592)Time elapsed: 0.005 s
% 0.74/0.58 % (3664592)Peak memory usage: 10 MB
% 0.74/0.58 % (3664592)Instructions burned: 5 (million)
% 0.74/0.58 % (3664599)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3865819489:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.74/0.58 % (3664599)Instruction limit reached!
% 0.74/0.58 % (3664599)------------------------------
% 0.74/0.58 % (3664599)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.74/0.58 % (3664599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.74/0.58 % (3664599)CaDiCaL version: 2.1.3
% 0.74/0.58 % (3664599)Termination reason: Instruction limit
% 0.74/0.58 % (3664599)Termination phase: shuffling
% 0.74/0.58 % (3664599)Time elapsed: 0.002 s
% 0.74/0.58 % (3664599)Peak memory usage: 10 MB
% 0.74/0.58 % (3664599)Instructions burned: 4 (million)
% 0.74/0.58 % (3664594)Instruction limit reached!
% 0.74/0.58 % (3664594)------------------------------
% 0.74/0.58 % (3664594)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.74/0.58 % (3664594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.74/0.58 % (3664594)CaDiCaL version: 2.1.3
% 0.74/0.58 % (3664594)Termination reason: Instruction limit
% 0.74/0.58 % (3664594)Termination phase: Property scanning
% 0.74/0.58 % (3664594)Time elapsed: 0.021 s
% 0.74/0.58 % (3664594)Peak memory usage: 10 MB
% 0.74/0.58 % (3664594)Instructions burned: 24 (million)
% 0.74/0.58 % (3664605)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=1606078620:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 1.69/0.64 % (3664608)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=1517597862:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 1.69/0.64 % (3664605)Instruction limit reached!
% 1.69/0.64 % (3664605)------------------------------
% 1.69/0.64 % (3664605)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.69/0.64 % (3664605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.69/0.64 % (3664605)CaDiCaL version: 2.1.3
% 1.69/0.64 % (3664605)Termination reason: Instruction limit
% 1.69/0.64 % (3664605)Termination phase: shuffling
% 1.69/0.64 % (3664605)Time elapsed: 0.006 s
% 1.69/0.64 % (3664605)Peak memory usage: 10 MB
% 1.69/0.64 % (3664605)Instructions burned: 6 (million)
% 1.69/0.64 % (3664608)Instruction limit reached!
% 1.69/0.64 % (3664608)------------------------------
% 1.69/0.64 % (3664608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.69/0.64 % (3664608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.69/0.64 % (3664608)CaDiCaL version: 2.1.3
% 1.69/0.64 % (3664608)Termination reason: Instruction limit
% 1.69/0.64 % (3664608)Termination phase: shuffling
% 1.69/0.64 % (3664608)Time elapsed: 0.006 s
% 1.69/0.64 % (3664608)Peak memory usage: 10 MB
% 1.69/0.64 % (3664608)Instructions burned: 14 (million)
% 1.69/0.64 % (3664607)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.69/0.64 % (3664607)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2179004872:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 1.69/0.64 % (3664607)Instruction limit reached!
% 1.69/0.64 % (3664607)------------------------------
% 1.69/0.64 % (3664607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.69/0.64 % (3664607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.69/0.64 % (3664607)CaDiCaL version: 2.1.3
% 1.69/0.64 % (3664607)Termination reason: Instruction limit
% 1.69/0.64 % (3664607)Termination phase: shuffling
% 1.69/0.64 % (3664607)Time elapsed: 0.007 s
% 1.69/0.64 % (3664607)Peak memory usage: 10 MB
% 1.69/0.64 % (3664607)Instructions burned: 7 (million)
% 1.69/0.64 % (3664590)Instruction limit reached!
% 1.69/0.64 % (3664590)------------------------------
% 1.69/0.64 % (3664590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.69/0.64 % (3664590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.69/0.64 % (3664590)CaDiCaL version: 2.1.3
% 1.69/0.64 % (3664590)Termination reason: Instruction limit
% 1.69/0.64 % (3664590)Termination phase: Property scanning
% 1.69/0.64 % (3664590)Time elapsed: 0.074 s
% 1.69/0.64 % (3664590)Peak memory usage: 12 MB
% 1.69/0.64 % (3664590)Instructions burned: 87 (million)
% 1.69/0.64 % (3664611)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.69/0.64 % (3664611)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.69/0.64 % (3664595)Instruction limit reached!
% 1.69/0.64 % (3664595)------------------------------
% 1.69/0.64 % (3664595)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.69/0.64 % (3664595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.69/0.64 % (3664595)CaDiCaL version: 2.1.3
% 1.69/0.64 % (3664595)Termination reason: Instruction limit
% 1.69/0.64 % (3664595)Termination phase: Equality resolution with deletion
% 1.69/0.64 % (3664595)Time elapsed: 0.064 s
% 1.69/0.64 % (3664595)Peak memory usage: 12 MB
% 1.69/0.64 % (3664595)Instructions burned: 76 (million)
% 1.69/0.64 % (3664612)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=1621326774:i=86:piset=equals:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/86Mi)
% 1.69/0.64 % (3664611)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=1385761982:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2998 on theBenchmark for (2998ds/28Mi)
% 1.69/0.64 % (3664611)Instruction limit reached!
% 1.69/0.64 % (3664611)------------------------------
% 1.69/0.64 % (3664611)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.69/0.68 % (3664611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.69/0.68 % (3664611)CaDiCaL version: 2.1.3
% 1.69/0.68 % (3664611)Termination reason: Instruction limit
% 1.69/0.68 % (3664611)Termination phase: shuffling
% 1.69/0.68 % (3664611)Time elapsed: 0.014 s
% 1.69/0.68 % (3664611)Peak memory usage: 10 MB
% 1.69/0.68 % (3664611)Instructions burned: 29 (million)
% 1.69/0.68 % (3664615)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.69/0.68 % (3664614)lrs+10_1_si=on:cs=on:random_seed=1958962650:i=8:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.69/0.68 % (3664615)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=2875590918:i=2:add=on:rtra=on_2998 on theBenchmark for (2998ds/2Mi)
% 1.69/0.68 % (3664615)Instruction limit reached!
% 1.69/0.68 % (3664615)------------------------------
% 1.69/0.68 % (3664615)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.69/0.68 % (3664618)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=1284197556:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/38Mi)
% 1.69/0.68 % (3664615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.69/0.68 % (3664615)CaDiCaL version: 2.1.3
% 1.69/0.68 % (3664615)Termination reason: Instruction limit
% 1.69/0.68 % (3664615)Termination phase: shuffling
% 1.69/0.68 % (3664615)Time elapsed: 0.003 s
% 1.69/0.68 % (3664615)Peak memory usage: 10 MB
% 1.69/0.68 % (3664615)Instructions burned: 3 (million)
% 1.69/0.68 % (3664612)Instruction limit reached!
% 1.69/0.68 % (3664612)------------------------------
% 1.69/0.68 % (3664612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.69/0.68 % (3664612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.69/0.68 % (3664612)CaDiCaL version: 2.1.3
% 1.69/0.68 % (3664612)Termination reason: Instruction limit
% 1.69/0.68 % (3664612)Termination phase: Preprocessing 3
% 1.69/0.68 % (3664612)Time elapsed: 0.036 s
% 1.69/0.68 % (3664612)Peak memory usage: 11 MB
% 1.69/0.68 % (3664612)Instructions burned: 88 (million)
% 1.69/0.68 % (3664619)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=474266339:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 1.69/0.68 % (3664614)Instruction limit reached!
% 1.69/0.68 % (3664614)------------------------------
% 1.69/0.68 % (3664614)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.69/0.68 % (3664614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.69/0.68 % (3664614)CaDiCaL version: 2.1.3
% 1.69/0.68 % (3664614)Termination reason: Instruction limit
% 1.69/0.68 % (3664614)Termination phase: shuffling
% 1.69/0.68 % (3664614)Time elapsed: 0.010 s
% 1.69/0.68 % (3664614)Peak memory usage: 10 MB
% 1.69/0.68 % (3664614)Instructions burned: 11 (million)
% 1.69/0.68 % (3664624)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=403779051:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.69/0.68 % (3664624)Instruction limit reached!
% 1.69/0.68 % (3664624)------------------------------
% 1.69/0.68 % (3664624)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.69/0.68 % (3664624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.69/0.68 % (3664624)CaDiCaL version: 2.1.3
% 1.69/0.68 % (3664624)Termination reason: Instruction limit
% 1.69/0.68 % (3664624)Termination phase: shuffling
% 1.69/0.68 % (3664624)Time elapsed: 0.007 s
% 1.69/0.68 % (3664624)Peak memory usage: 11 MB
% 1.69/0.68 % (3664624)Instructions burned: 15 (million)
% 1.69/0.68 % (3664623)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=3959464637:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 1.69/0.68 % (3664618)Instruction limit reached!
% 1.69/0.68 % (3664618)------------------------------
% 1.69/0.68 % (3664618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.69/0.68 % (3664618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.69/0.68 % (3664618)CaDiCaL version: 2.1.3
% 1.69/0.68 % (3664618)Termination reason: Instruction limit
% 1.69/0.68 % (3664618)Termination phase: Naming
% 2.44/0.80 % (3664618)Time elapsed: 0.033 s
% 2.44/0.80 % (3664618)Peak memory usage: 11 MB
% 2.44/0.80 % (3664618)Instructions burned: 38 (million)
% 2.44/0.80 % (3664596)Instruction limit reached!
% 2.44/0.80 % (3664596)------------------------------
% 2.44/0.80 % (3664596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.44/0.80 % (3664596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.44/0.80 % (3664596)CaDiCaL version: 2.1.3
% 2.44/0.80 % (3664596)Termination reason: Instruction limit
% 2.44/0.80 % (3664596)Termination phase: Saturation
% 2.44/0.80 % (3664596)Time elapsed: 0.138 s
% 2.44/0.80 % (3664596)Peak memory usage: 14 MB
% 2.44/0.80 % (3664596)Instructions burned: 157 (million)
% 2.44/0.80 % (3664626)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=2129550454:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 2.44/0.80 % (3664628)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=1309094872:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 2.44/0.80 % (3664628)Instruction limit reached!
% 2.44/0.80 % (3664628)------------------------------
% 2.44/0.80 % (3664628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.44/0.80 % (3664628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.44/0.80 % (3664628)CaDiCaL version: 2.1.3
% 2.44/0.80 % (3664628)Termination reason: Instruction limit
% 2.44/0.80 % (3664628)Termination phase: shuffling
% 2.44/0.80 % (3664628)Time elapsed: 0.007 s
% 2.44/0.80 % (3664628)Peak memory usage: 11 MB
% 2.44/0.80 % (3664628)Instructions burned: 16 (million)
% 2.44/0.80 % (3664623)Instruction limit reached!
% 2.44/0.80 % (3664623)------------------------------
% 2.44/0.80 % (3664623)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.44/0.80 % (3664623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.44/0.80 % (3664623)CaDiCaL version: 2.1.3
% 2.44/0.80 % (3664623)Termination reason: Instruction limit
% 2.44/0.80 % (3664623)Termination phase: Property scanning
% 2.44/0.80 % (3664623)Time elapsed: 0.022 s
% 2.44/0.80 % (3664623)Peak memory usage: 10 MB
% 2.44/0.80 % (3664623)Instructions burned: 25 (million)
% 2.44/0.80 % (3664630)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=3120043472:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2998 on theBenchmark for (2998ds/2Mi)
% 2.44/0.80 % (3664630)Instruction limit reached!
% 2.44/0.80 % (3664630)------------------------------
% 2.44/0.80 % (3664630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.44/0.80 % (3664630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.44/0.80 % (3664630)CaDiCaL version: 2.1.3
% 2.44/0.80 % (3664630)Termination reason: Instruction limit
% 2.44/0.80 % (3664630)Termination phase: shuffling
% 2.44/0.80 % (3664630)Time elapsed: 0.003 s
% 2.44/0.80 % (3664630)Peak memory usage: 10 MB
% 2.44/0.80 % (3664630)Instructions burned: 2 (million)
% 2.44/0.80 % (3664634)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=237682863:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2997 on theBenchmark for (2997ds/23Mi)
% 2.44/0.80 % (3664631)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3029347700:i=26:ep=R:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/26Mi)
% 2.44/0.80 % (3664635)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=4131517820:cond=on:i=60:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/60Mi)
% 2.44/0.80 % (3664634)Instruction limit reached!
% 2.44/0.80 % (3664634)------------------------------
% 2.44/0.80 % (3664634)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.44/0.80 % (3664634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.44/0.80 % (3664634)CaDiCaL version: 2.1.3
% 2.44/0.80 % (3664634)Termination reason: Instruction limit
% 2.44/0.80 % (3664634)Termination phase: Property scanning
% 2.44/0.80 % (3664634)Time elapsed: 0.011 s
% 2.44/0.80 % (3664634)Peak memory usage: 10 MB
% 2.44/0.80 % (3664634)Instructions burned: 24 (million)
% 2.44/0.80 % (3664631)Instruction limit reached!
% 2.44/0.80 % (3664631)------------------------------
% 2.44/0.80 % (3664631)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.44/0.80 % (3664631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.44/0.80 % (3664631)CaDiCaL version: 2.1.3
% 3.04/0.92 % (3664631)Termination reason: Instruction limit
% 3.04/0.92 % (3664631)Termination phase: shuffling
% 3.04/0.92 % (3664631)Time elapsed: 0.023 s
% 3.04/0.92 % (3664631)Peak memory usage: 10 MB
% 3.04/0.92 % (3664631)Instructions burned: 27 (million)
% 3.04/0.92 % (3664637)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
% 3.04/0.92 % (3664637)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 3.04/0.92 % (3664637)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=3442956350:i=14:add=off:nm=40:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 3.04/0.92 % (3664635)Instruction limit reached!
% 3.04/0.92 % (3664635)------------------------------
% 3.04/0.92 % (3664635)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.92 % (3664635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.92 % (3664635)CaDiCaL version: 2.1.3
% 3.04/0.92 % (3664635)Termination reason: Instruction limit
% 3.04/0.92 % (3664635)Termination phase: Property scanning
% 3.04/0.92 % (3664635)Time elapsed: 0.031 s
% 3.04/0.92 % (3664635)Peak memory usage: 12 MB
% 3.04/0.92 % (3664635)Instructions burned: 62 (million)
% 3.04/0.92 % (3664641)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 3.04/0.92 % (3664637)Instruction limit reached!
% 3.04/0.92 % (3664637)------------------------------
% 3.04/0.92 % (3664637)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.92 % (3664637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.92 % (3664637)CaDiCaL version: 2.1.3
% 3.04/0.92 % (3664637)Termination reason: Instruction limit
% 3.04/0.92 % (3664637)Termination phase: shuffling
% 3.04/0.92 % (3664637)Time elapsed: 0.013 s
% 3.04/0.92 % (3664637)Peak memory usage: 10 MB
% 3.04/0.92 % (3664637)Instructions burned: 14 (million)
% 3.04/0.92 % (3664641)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=511248368:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2997 on theBenchmark for (2997ds/8Mi)
% 3.04/0.92 % (3664642)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=3337357430:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2997 on theBenchmark for (2997ds/31Mi)
% 3.04/0.92 % (3664644)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=4080160916:i=7:hud=5:bd=preordered:rtra=on:bet=on_2997 on theBenchmark for (2997ds/7Mi)
% 3.04/0.92 % (3664641)Instruction limit reached!
% 3.04/0.92 % (3664641)------------------------------
% 3.04/0.92 % (3664641)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.92 % (3664641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.92 % (3664641)CaDiCaL version: 2.1.3
% 3.04/0.92 % (3664641)Termination reason: Instruction limit
% 3.04/0.92 % (3664641)Termination phase: shuffling
% 3.04/0.92 % (3664641)Time elapsed: 0.007 s
% 3.04/0.92 % (3664641)Peak memory usage: 10 MB
% 3.04/0.92 % (3664641)Instructions burned: 8 (million)
% 3.04/0.92 % (3664644)Instruction limit reached!
% 3.04/0.92 % (3664644)------------------------------
% 3.04/0.92 % (3664644)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.92 % (3664644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.92 % (3664644)CaDiCaL version: 2.1.3
% 3.04/0.92 % (3664644)Termination reason: Instruction limit
% 3.04/0.92 % (3664644)Termination phase: shuffling
% 3.04/0.92 % (3664644)Time elapsed: 0.004 s
% 3.04/0.92 % (3664644)Peak memory usage: 10 MB
% 3.04/0.92 % (3664644)Instructions burned: 9 (million)
% 3.04/0.92 % (3664642)Instruction limit reached!
% 3.04/0.92 % (3664642)------------------------------
% 3.04/0.92 % (3664642)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.92 % (3664642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.92 % (3664642)CaDiCaL version: 2.1.3
% 3.04/0.92 % (3664642)Termination reason: Instruction limit
% 3.04/0.92 % (3664642)Termination phase: shuffling
% 3.04/0.92 % (3664642)Time elapsed: 0.016 s
% 3.04/0.92 % (3664642)Peak memory usage: 10 MB
% 3.04/0.93 % (3664642)Instructions burned: 31 (million)
% 3.04/0.93 % (3664650)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=233482921:i=1240:rtra=on:ixr=off_2997 on theBenchmark for (2997ds/1240Mi)
% 3.04/0.93 % (3664645)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=2925241:i=23:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/23Mi)
% 3.04/0.93 % (3664651)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=231080033:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2997 on theBenchmark for (2997ds/143Mi)
% 3.04/0.93 % (3664649)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=1125680970:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2997 on theBenchmark for (2997ds/20Mi)
% 3.04/0.93 % (3664645)Instruction limit reached!
% 3.04/0.93 % (3664645)------------------------------
% 3.04/0.93 % (3664645)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.93 % (3664645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.93 % (3664645)CaDiCaL version: 2.1.3
% 3.04/0.93 % (3664645)Termination reason: Instruction limit
% 3.04/0.93 % (3664645)Termination phase: shuffling
% 3.04/0.93 % (3664645)Time elapsed: 0.020 s
% 3.04/0.93 % (3664645)Peak memory usage: 11 MB
% 3.04/0.93 % (3664645)Instructions burned: 23 (million)
% 3.04/0.93 % (3664649)Instruction limit reached!
% 3.04/0.93 % (3664649)------------------------------
% 3.04/0.93 % (3664649)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.93 % (3664649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.93 % (3664649)CaDiCaL version: 2.1.3
% 3.04/0.93 % (3664649)Termination reason: Instruction limit
% 3.04/0.93 % (3664649)Termination phase: shuffling
% 3.04/0.93 % (3664649)Time elapsed: 0.018 s
% 3.04/0.93 % (3664649)Peak memory usage: 11 MB
% 3.04/0.93 % (3664649)Instructions burned: 20 (million)
% 3.04/0.93 % (3664656)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=3879885834:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/193Mi)
% 3.04/0.93 % (3664657)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=1385799803:i=42:hud=10:rtra=on_2996 on theBenchmark for (2996ds/42Mi)
% 3.04/0.93 % (3664619)Instruction limit reached!
% 3.04/0.93 % (3664619)------------------------------
% 3.04/0.93 % (3664619)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.93 % (3664619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.93 % (3664619)CaDiCaL version: 2.1.3
% 3.04/0.93 % (3664619)Termination reason: Instruction limit
% 3.04/0.93 % (3664619)Termination phase: Saturation
% 3.04/0.93 % (3664619)Time elapsed: 0.202 s
% 3.04/0.93 % (3664619)Peak memory usage: 14 MB
% 3.04/0.93 % (3664619)Instructions burned: 249 (million)
% 3.04/0.93 % (3664660)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 3.04/0.93 % (3664660)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1463404295:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2996 on theBenchmark for (2996ds/7Mi)
% 3.04/0.93 % (3664660)Instruction limit reached!
% 3.04/0.93 % (3664660)------------------------------
% 3.04/0.93 % (3664660)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.93 % (3664660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.93 % (3664660)CaDiCaL version: 2.1.3
% 3.04/0.93 % (3664660)Termination reason: Instruction limit
% 3.04/0.93 % (3664660)Termination phase: shuffling
% 3.04/0.93 % (3664660)Time elapsed: 0.005 s
% 3.04/0.93 % (3664660)Peak memory usage: 10 MB
% 3.04/0.93 % (3664660)Instructions burned: 9 (million)
% 3.04/0.93 % (3664657)Instruction limit reached!
% 3.04/0.93 % (3664657)------------------------------
% 3.04/0.93 % (3664657)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.93 % (3664657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.93 % (3664657)CaDiCaL version: 2.1.3
% 3.04/0.93 % (3664657)Termination reason: Instruction limit
% 3.04/0.93 % (3664657)Termination phase: Preprocessing 3
% 3.04/0.93 % (3664657)Time elapsed: 0.036 s
% 3.04/0.93 % (3664657)Peak memory usage: 11 MB
% 3.04/0.93 % (3664657)Instructions burned: 42 (million)
% 3.04/0.93 % (3664662)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=2339514417:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/181Mi)
% 3.04/0.93 % (3664663)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=4009571352:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2995 on theBenchmark for (2995ds/169Mi)
% 3.04/0.93 % (3664651)Instruction limit reached!
% 3.04/0.93 % (3664651)------------------------------
% 3.04/0.93 % (3664651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.93 % (3664651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.93 % (3664651)CaDiCaL version: 2.1.3
% 3.04/0.93 % (3664651)Termination reason: Instruction limit
% 3.04/0.93 % (3664651)Termination phase: Saturation
% 3.04/0.93 % (3664651)Time elapsed: 0.126 s
% 3.04/0.93 % (3664651)Peak memory usage: 14 MB
% 3.04/0.93 % (3664651)Instructions burned: 143 (million)
% 3.04/0.93 % (3664666)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 3.04/0.93 % (3664666)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=2247365283:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2995 on theBenchmark for (2995ds/6Mi)
% 3.04/0.93 % (3664666)Instruction limit reached!
% 3.04/0.93 % (3664666)------------------------------
% 3.04/0.93 % (3664666)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.93 % (3664666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.93 % (3664666)CaDiCaL version: 2.1.3
% 3.04/0.93 % (3664666)Termination reason: Instruction limit
% 3.04/0.93 % (3664666)Termination phase: shuffling
% 3.04/0.93 % (3664666)Time elapsed: 0.006 s
% 3.04/0.93 % (3664666)Peak memory usage: 10 MB
% 3.04/0.93 % (3664666)Instructions burned: 6 (million)
% 3.04/0.93 % (3664626)Instruction limit reached!
% 3.04/0.93 % (3664626)------------------------------
% 3.04/0.93 % (3664626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.93 % (3664626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.93 % (3664626)CaDiCaL version: 2.1.3
% 3.04/0.93 % (3664626)Termination reason: Instruction limit
% 3.04/0.93 % (3664626)Termination phase: Saturation
% 3.04/0.93 % (3664626)Time elapsed: 0.284 s
% 3.04/0.93 % (3664626)Peak memory usage: 15 MB
% 3.04/0.93 % (3664626)Instructions burned: 327 (million)
% 3.04/0.93 % (3664668)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=4107491515:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2995 on theBenchmark for (2995ds/22Mi)
% 3.04/0.93 % (3664669)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=3818906286:i=19:add=on:rtra=on_2995 on theBenchmark for (2995ds/19Mi)
% 3.04/0.93 % (3664656)Instruction limit reached!
% 3.04/0.93 % (3664656)------------------------------
% 3.04/0.93 % (3664656)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.93 % (3664656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.93 % (3664656)CaDiCaL version: 2.1.3
% 3.04/0.93 % (3664656)Termination reason: Instruction limit
% 3.04/0.93 % (3664656)Termination phase: Saturation
% 3.04/0.93 % (3664656)Time elapsed: 0.169 s
% 3.04/0.93 % (3664656)Peak memory usage: 14 MB
% 3.04/0.93 % (3664656)Instructions burned: 193 (million)
% 3.04/0.93 % (3664668)Instruction limit reached!
% 3.04/0.93 % (3664668)------------------------------
% 3.04/0.93 % (3664668)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.93 % (3664668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.93 % (3664668)CaDiCaL version: 2.1.3
% 3.04/0.93 % (3664668)Termination reason: Instruction limit
% 3.04/0.93 % (3664668)Termination phase: Property scanning
% 3.04/0.93 % (3664668)Time elapsed: 0.020 s
% 3.04/0.93 % (3664668)Peak memory usage: 10 MB
% 3.04/0.93 % (3664668)Instructions burned: 22 (million)
% 3.04/0.93 % (3664650) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3664585-3664650"...
% 3.04/0.93 % (3664669)Instruction limit reached!
% 3.04/0.93 % (3664669)------------------------------
% 3.04/0.93 % (3664669)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.93 % (3664669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.93 % (3664669)CaDiCaL version: 2.1.3
% 3.04/0.93 % (3664669)Termination reason: Instruction limit
% 3.04/0.93 % (3664669)Termination phase: shuffling
% 3.04/0.93 % (3664669)Time elapsed: 0.017 s
% 3.04/0.93 % (3664669)Peak memory usage: 10 MB
% 3.04/0.93 % (3664669)Instructions burned: 20 (million)
% 3.04/0.93 % (3664650)...printing done.
% 3.04/0.93 % (3664650)Refutation found. Thanks to Tanya!
% 3.04/0.93 % SZS status Theorem for theBenchmark
% 3.04/0.93 % SZS output start Proof for theBenchmark
% 3.04/0.93 thf(type_def_5, type, product_prod: ($tType * $tType) > $tType).
% 3.04/0.93 thf(type_def_6, type, real: $tType).
% 3.04/0.93 thf(type_def_7, type, set: $tType > $tType).
% 3.04/0.93 thf(type_def_8, type, a: $tType).
% 3.04/0.93 thf(type_def_9, type, sTfun: ($tType * $tType) > $tType).
% 3.04/0.93 thf(func_def_0, type, ordere890947078_space: !>[X0: $tType]:($o)).
% 3.04/0.93 thf(func_def_1, type, type: !>[X0: $tType]:($o)).
% 3.04/0.93 thf(func_def_2, type, one: !>[X0: $tType]:($o)).
% 3.04/0.93 thf(func_def_3, type, plus: !>[X0: $tType]:($o)).
% 3.04/0.93 thf(func_def_4, type, zero: !>[X0: $tType]:($o)).
% 3.04/0.93 thf(func_def_5, type, ord: !>[X0: $tType]:($o)).
% 3.04/0.93 thf(func_def_6, type, neg_numeral: !>[X0: $tType]:($o)).
% 3.04/0.93 thf(func_def_7, type, order: !>[X0: $tType]:($o)).
% 3.04/0.93 thf(func_def_8, type, group_add: !>[X0: $tType]:($o)).
% 3.04/0.93 thf(func_def_9, type, monoid_add: !>[X0: $tType]:($o)).
% 3.04/0.93 thf(func_def_10, type, linorder: !>[X0: $tType]:($o)).
% 3.04/0.93 thf(func_def_11, type, preorder: !>[X0: $tType]:($o)).
% 3.04/0.93 thf(func_def_12, type, zero_neq_one: !>[X0: $tType]:($o)).
% 3.04/0.93 thf(func_def_13, type, zero_less_one: !>[X0: $tType]:($o)).
% 3.04/0.93 thf(func_def_14, type, semigroup_add: !>[X0: $tType]:($o)).
% 3.04/0.93 thf(func_def_15, type, linordered_idom: !>[X0: $tType]:($o)).
% 3.04/0.93 thf(func_def_16, type, comm_monoid_add: !>[X0: $tType]:($o)).
% 3.04/0.93 thf(func_def_17, type, linordered_field: !>[X0: $tType]:($o)).
% 3.04/0.93 thf(func_def_18, type, ab_semigroup_add: !>[X0: $tType]:($o)).
% 3.04/0.93 thf(func_def_19, type, linordered_semidom: !>[X0: $tType]:($o)).
% 3.04/0.93 thf(func_def_20, type, cancel_semigroup_add: !>[X0: $tType]:($o)).
% 3.04/0.93 thf(func_def_21, type, cancel1352612707id_add: !>[X0: $tType]:($o)).
% 3.04/0.93 thf(func_def_22, type, linord219039673up_add: !>[X0: $tType]:($o)).
% 3.04/0.93 thf(func_def_23, type, ordere216010020id_add: !>[X0: $tType]:($o)).
% 3.04/0.93 thf(func_def_24, type, real_V1076094709vector: !>[X0: $tType]:($o)).
% 3.04/0.93 thf(func_def_25, type, ordere779506340up_add: !>[X0: $tType]:($o)).
% 3.04/0.93 thf(func_def_26, type, linord1659791738miring: !>[X0: $tType]:($o)).
% 3.04/0.93 thf(func_def_27, type, canoni770627133id_add: !>[X0: $tType]:($o)).
% 3.04/0.93 thf(func_def_28, type, ordere1818651114id_add: !>[X0: $tType]:($o)).
% 3.04/0.93 thf(func_def_29, type, strict797366125id_add: !>[X0: $tType]:($o)).
% 3.04/0.93 thf(func_def_30, type, real_V55928688vector: !>[X0: $tType]:($o)).
% 3.04/0.93 thf(func_def_31, type, ordere236663937imp_le: !>[X0: $tType]:($o)).
% 3.04/0.93 thf(func_def_32, type, ordere223160158up_add: !>[X0: $tType]:($o)).
% 3.04/0.93 thf(func_def_33, type, strict2144017051up_add: !>[X0: $tType]:($o)).
% 3.04/0.93 thf(func_def_34, type, real_V1587248058vector: !>[X0: $tType]:($o)).
% 3.04/0.93 thf(func_def_35, type, unique1598680935umeral: !>[X0: $tType]:($o)).
% 3.04/0.93 thf(func_def_36, type, ordere516151231imp_le: !>[X0: $tType]:($o)).
% 3.04/0.93 thf(func_def_37, type, unique455577585es_aux: !>[X0: $tType]:((product_prod @ X0 @ X0 > $o))).
% 3.04/0.93 thf(func_def_38, type, one_one: !>[X0: $tType]:(X0)).
% 3.04/0.93 thf(func_def_39, type, plus_plus: !>[X0: $tType]:((X0 > X0 > X0))).
% 3.04/0.93 thf(func_def_40, type, zero_zero: !>[X0: $tType]:(X0)).
% 3.04/0.93 thf(func_def_41, type, ord_less: !>[X0: $tType]:((X0 > X0 > $o))).
% 3.04/0.93 thf(func_def_42, type, ord_less_eq: !>[X0: $tType]:((X0 > X0 > $o))).
% 3.04/0.93 thf(func_def_43, type, prefer1289595409x_pref: !>[X0: $tType]:((set @ product_prod @ X0 @ X0 > $o))).
% 3.04/0.93 thf(func_def_44, type, product_Pair: !>[X0: $tType, X1: $tType]:((X0 > X1 > product_prod @ X0 @ X1))).
% 3.04/0.93 thf(func_def_45, type, product_rec_prod: !>[X0: $tType, X1: $tType, X2: $tType]:(((X0 > X1 > X2) > product_prod @ X0 @ X1 > X2))).
% 3.04/0.93 thf(func_def_46, type, real_V1908273582scaleR: !>[X0: $tType]:((real > X0 > X0))).
% 3.04/0.93 thf(func_def_47, type, collect: !>[X0: $tType]:(((X0 > $o) > set @ X0))).
% 3.04/0.93 thf(func_def_48, type, member: !>[X0: $tType]:((X0 > set @ X0 > $o))).
% 3.04/0.93 thf(func_def_49, type, relation: set @ product_prod @ a @ a).
% 3.04/0.93 thf(func_def_50, type, u: real).
% 3.04/0.93 thf(func_def_51, type, v: real).
% 3.04/0.93 thf(func_def_52, type, x: a).
% 3.04/0.93 thf(func_def_53, type, y: a).
% 3.04/0.93 thf(func_def_55, type, vIMP: ($o > $o > $o)).
% 3.04/0.93 thf(func_def_56, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 3.04/0.93 thf(func_def_57, type, db1: !>[X0: $tType]:(X0)).
% 3.04/0.93 thf(func_def_58, type, db0: !>[X0: $tType]:(X0)).
% 3.04/0.93 thf(func_def_59, type, db2: !>[X0: $tType]:(X0)).
% 3.04/0.93 thf(func_def_60, type, db4: !>[X0: $tType]:(X0)).
% 3.04/0.93 thf(func_def_61, type, db3: !>[X0: $tType]:(X0)).
% 3.04/0.93 thf(func_def_62, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 3.04/0.93 thf(func_def_63, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 3.04/0.93 thf(func_def_66, type, vAND: ($o > $o > $o)).
% 3.04/0.93 thf(func_def_67, type, db7: !>[X0: $tType]:(X0)).
% 3.04/0.93 thf(func_def_68, type, db5: !>[X0: $tType]:(X0)).
% 3.04/0.93 thf(func_def_69, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 3.04/0.93 thf(func_def_70, type, vNOT: ($o > $o)).
% 3.04/0.93 thf(func_def_71, type, vOR: ($o > $o > $o)).
% 3.04/0.93 thf(func_def_72, type, db6: !>[X0: $tType]:(X0)).
% 3.04/0.93 thf(func_def_73, type, db8: !>[X0: $tType]:(X0)).
% 3.04/0.93 thf(func_def_75, type, sK1: !>[X0: $tType]:((X0 > X0))).
% 3.04/0.93 thf(func_def_76, type, sK2: !>[X0: $tType]:((X0 > X0))).
% 3.04/0.93 thf(func_def_77, type, sK3: !>[X0: $tType, X1: $tType]:((product_prod @ X0 @ X1 > X0))).
% 3.04/0.93 thf(func_def_78, type, sK4: !>[X0: $tType, X1: $tType]:((product_prod @ X0 @ X1 > X1))).
% 3.04/0.93 thf(func_def_79, type, sK5: !>[X0: $tType, X1: $tType]:((product_prod @ X1 @ X0 > X1))).
% 3.04/0.93 thf(func_def_80, type, sK6: !>[X0: $tType, X1: $tType]:((product_prod @ X1 @ X0 > X0))).
% 3.04/0.93 thf(func_def_81, type, sK7: !>[X0: $tType]:((X0 > X0 > X0))).
% 3.04/0.93 thf(f6,axiom,(
% 3.04/0.93 (member @ product_prod @ a @ a @ (product_Pair @ a @ a @ x @ y) @ relation)),
% 3.04/0.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_5_assms_I2_J)).
% 3.04/0.93 thf(f7,axiom,(
% 3.04/0.93 ((u != zero_zero @ real) & (u != one_one @ real)) => (member @ product_prod @ a @ a @ (product_Pair @ a @ a @ (plus_plus @ a @ (real_V1908273582scaleR @ a @ u @ x) @ (real_V1908273582scaleR @ a @ v @ y)) @ y) @ relation)),
% 3.04/0.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6__092_060open_062u_A_092_060noteq_062_A0_A_092_060and_062_Au_A_092_060noteq_062_A1_A_092_060longrightarrow_062_Au_A_K_092_060_094sub_062R_Ax_A_L_Av_A_K_092_060_094sub_062R_Ay_A_092_060succeq_062_Ay_092_060close_062)).
% 3.04/0.93 thf(f8,axiom,(
% 3.04/0.93 (u = zero_zero @ real) => (member @ product_prod @ a @ a @ (product_Pair @ a @ a @ (plus_plus @ a @ (real_V1908273582scaleR @ a @ u @ x) @ (real_V1908273582scaleR @ a @ v @ y)) @ y) @ relation)),
% 3.04/0.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7_u__0)).
% 3.04/0.93 thf(f10,axiom,(
% 3.04/0.93 (((plus_plus @ real @ u @ v)) = one_one @ real)),
% 3.04/0.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_9_assms_I5_J)).
% 3.04/0.93 thf(f28,axiom,(
% 3.04/0.93 ! [X0 : $tType] : (cancel1352612707id_add @ X0 => ! [X1 : X0,X2 : X0] : ((X2 = zero_zero @ X0) = (((plus_plus @ X0 @ X1 @ X2)) = X1)))),
% 3.04/0.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_27_add__cancel__left__right)).
% 3.04/0.93 thf(f68,axiom,(
% 3.04/0.93 ! [X0 : $tType] : (comm_monoid_add @ X0 => ! [X1 : X0] : (((plus_plus @ X0 @ X1 @ zero_zero @ X0)) = X1))),
% 3.04/0.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_67_add_Ocomm__neutral)).
% 3.04/0.93 thf(f115,axiom,(
% 3.04/0.93 ! [X0 : $tType] : (real_V1076094709vector @ X0 => ! [X1 : X0] : (((real_V1908273582scaleR @ X0 @ zero_zero @ real @ X1)) = zero_zero @ X0))),
% 3.04/0.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_114_scale__zero__left)).
% 3.04/0.93 thf(f117,axiom,(
% 3.04/0.93 ! [X0 : $tType] : (real_V1076094709vector @ X0 => ! [X1 : X0] : (((real_V1908273582scaleR @ X0 @ one_one @ real @ X1)) = X1))),
% 3.04/0.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_116_scaleR__one)).
% 3.04/0.93 thf(f261,axiom,(
% 3.04/0.93 ! [X0 : $tType] : (real_V1076094709vector @ X0 => comm_monoid_add @ X0)),
% 3.04/0.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p',subcl_Real__Vector__Spaces_Oreal__vector___Groups_Ocomm__monoid__add)).
% 3.04/0.93 thf(f297,axiom,(
% 3.04/0.93 cancel1352612707id_add @ real),
% 3.04/0.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Groups_Ocancel__comm__monoid__add)).
% 3.04/0.93 thf(f340,axiom,(
% 3.04/0.93 real_V1076094709vector @ a),
% 3.04/0.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p',tfree_0)).
% 3.04/0.93 thf(f341,conjecture,(
% 3.04/0.93 (member @ product_prod @ a @ a @ (product_Pair @ a @ a @ (plus_plus @ a @ (real_V1908273582scaleR @ a @ u @ x) @ (real_V1908273582scaleR @ a @ v @ y)) @ y) @ relation)),
% 3.04/0.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0)).
% 3.04/0.93 thf(f342,negated_conjecture,(
% 3.04/0.93 ~(member @ product_prod @ a @ a @ (product_Pair @ a @ a @ (plus_plus @ a @ (real_V1908273582scaleR @ a @ u @ x) @ (real_V1908273582scaleR @ a @ v @ y)) @ y) @ relation)),
% 3.04/0.93 inference(negated_conjecture,[status(cth)],[f341])).
% 3.04/0.93 thf(f381,plain,(
% 3.04/0.93 (one_one @ real = ((plus_plus @ real @ u @ v)))),
% 3.04/0.93 inference(fool_elimination,[],[f10])).
% 3.04/0.93 thf(f390,plain,(
% 3.04/0.93 ! [X0 : $tType] : (real_V1076094709vector @ X0 => ! [X1 : X0] : (((real_V1908273582scaleR @ X0 @ zero_zero @ real @ X1)) = zero_zero @ X0))),
% 3.04/0.93 inference(rectify,[],[f115])).
% 3.04/0.93 thf(f391,plain,(
% 3.04/0.93 ( ! [X0 : $tType] : (($true = ((real_V1076094709vector @ X0 => (!! @ X0 @ (^[Y0 : X0]: (zero_zero @ X0 = (real_V1908273582scaleR @ X0 @ zero_zero @ real @ Y0)))))))) )),
% 3.04/0.93 inference(fool_elimination,[],[f390])).
% 3.04/0.93 thf(f420,plain,(
% 3.04/0.93 ((u != zero_zero @ real) & (u != one_one @ real)) => (member @ product_prod @ a @ a @ (product_Pair @ a @ a @ (plus_plus @ a @ (real_V1908273582scaleR @ a @ u @ x) @ (real_V1908273582scaleR @ a @ v @ y)) @ y) @ relation)),
% 3.04/0.93 inference(rectify,[],[f7])).
% 3.04/0.93 thf(f421,plain,(
% 3.04/0.93 (((((~ (u = one_one @ real)) & (~ (u = zero_zero @ real))) => (member @ product_prod @ a @ a @ (product_Pair @ a @ a @ (plus_plus @ a @ (real_V1908273582scaleR @ a @ u @ x) @ (real_V1908273582scaleR @ a @ v @ y)) @ y) @ relation))) = $true)),
% 3.04/0.93 inference(fool_elimination,[],[f420])).
% 3.04/0.93 thf(f460,plain,(
% 3.04/0.93 ! [X0 : $tType] : (real_V1076094709vector @ X0 => ! [X1 : X0] : (((real_V1908273582scaleR @ X0 @ one_one @ real @ X1)) = X1))),
% 3.04/0.93 inference(rectify,[],[f117])).
% 3.04/0.93 thf(f461,plain,(
% 3.04/0.93 ( ! [X0 : $tType] : ((((real_V1076094709vector @ X0 => (!! @ X0 @ (^[Y0 : X0]: ((real_V1908273582scaleR @ X0 @ one_one @ real @ Y0) = Y0))))) = $true)) )),
% 3.04/0.93 inference(fool_elimination,[],[f460])).
% 3.04/0.93 thf(f482,plain,(
% 3.04/0.93 cancel1352612707id_add @ real),
% 3.04/0.93 inference(rectify,[],[f297])).
% 3.04/0.93 thf(f483,plain,(
% 3.04/0.93 (cancel1352612707id_add @ real = $true)),
% 3.04/0.93 inference(fool_elimination,[],[f482])).
% 3.04/0.93 thf(f486,plain,(
% 3.04/0.93 (member @ product_prod @ a @ a @ (product_Pair @ a @ a @ x @ y) @ relation)),
% 3.04/0.93 inference(rectify,[],[f6])).
% 3.04/0.93 thf(f487,plain,(
% 3.04/0.93 (((member @ product_prod @ a @ a @ (product_Pair @ a @ a @ x @ y) @ relation)) = $true)),
% 3.04/0.93 inference(fool_elimination,[],[f486])).
% 3.04/0.93 thf(f544,plain,(
% 3.04/0.93 ! [X0 : $tType] : (real_V1076094709vector @ X0 => comm_monoid_add @ X0)),
% 3.04/0.93 inference(rectify,[],[f261])).
% 3.04/0.93 thf(f545,plain,(
% 3.04/0.93 ( ! [X0 : $tType] : ((((real_V1076094709vector @ X0 => comm_monoid_add @ X0)) = $true)) )),
% 3.04/0.93 inference(fool_elimination,[],[f544])).
% 3.04/0.93 thf(f638,plain,(
% 3.04/0.93 ~(member @ product_prod @ a @ a @ (product_Pair @ a @ a @ (plus_plus @ a @ (real_V1908273582scaleR @ a @ u @ x) @ (real_V1908273582scaleR @ a @ v @ y)) @ y) @ relation)),
% 3.04/0.93 inference(rectify,[],[f342])).
% 3.04/0.93 thf(f639,plain,(
% 3.04/0.93 ($true = ((~ (member @ product_prod @ a @ a @ (product_Pair @ a @ a @ (plus_plus @ a @ (real_V1908273582scaleR @ a @ u @ x) @ (real_V1908273582scaleR @ a @ v @ y)) @ y) @ relation))))),
% 3.04/0.93 inference(fool_elimination,[],[f638])).
% 3.04/0.93 thf(f662,plain,(
% 3.04/0.93 ! [X0 : $tType] : (cancel1352612707id_add @ X0 => ! [X1 : X0,X2 : X0] : ((X2 = zero_zero @ X0) = (((plus_plus @ X0 @ X1 @ X2)) = X1)))),
% 3.04/0.93 inference(rectify,[],[f28])).
% 3.04/0.93 thf(f663,plain,(
% 3.04/0.93 ( ! [X0 : $tType] : ((((cancel1352612707id_add @ X0 => (!! @ X0 @ (^[Y0 : X0]: (!! @ X0 @ (^[Y1 : X0]: ((zero_zero @ X0 = Y0) = ((plus_plus @ X0 @ Y1 @ Y0) = Y1)))))))) = $true)) )),
% 3.04/0.93 inference(fool_elimination,[],[f662])).
% 3.04/0.93 thf(f710,plain,(
% 3.04/0.93 ! [X0 : $tType] : (comm_monoid_add @ X0 => ! [X1 : X0] : (((plus_plus @ X0 @ X1 @ zero_zero @ X0)) = X1))),
% 3.04/0.93 inference(rectify,[],[f68])).
% 3.04/0.93 thf(f711,plain,(
% 3.04/0.93 ( ! [X0 : $tType] : ((((comm_monoid_add @ X0 => (!! @ X0 @ (^[Y0 : X0]: ((plus_plus @ X0 @ Y0 @ zero_zero @ X0) = Y0))))) = $true)) )),
% 3.04/0.93 inference(fool_elimination,[],[f710])).
% 3.04/0.93 thf(f750,plain,(
% 3.04/0.93 (u = zero_zero @ real) => (member @ product_prod @ a @ a @ (product_Pair @ a @ a @ (plus_plus @ a @ (real_V1908273582scaleR @ a @ u @ x) @ (real_V1908273582scaleR @ a @ v @ y)) @ y) @ relation)),
% 3.04/0.93 inference(rectify,[],[f8])).
% 3.04/0.93 thf(f751,plain,(
% 3.04/0.93 ((((u = zero_zero @ real) => (member @ product_prod @ a @ a @ (product_Pair @ a @ a @ (plus_plus @ a @ (real_V1908273582scaleR @ a @ u @ x) @ (real_V1908273582scaleR @ a @ v @ y)) @ y) @ relation))) = $true)),
% 3.04/0.93 inference(fool_elimination,[],[f750])).
% 3.04/0.93 thf(f850,plain,(
% 3.04/0.93 real_V1076094709vector @ a),
% 3.04/0.93 inference(rectify,[],[f340])).
% 3.04/0.93 thf(f851,plain,(
% 3.04/0.93 (real_V1076094709vector @ a = $true)),
% 3.04/0.93 inference(fool_elimination,[],[f850])).
% 3.04/0.93 thf(f1046,plain,(
% 3.04/0.93 ! [X0 : $tType] : ($true = ((real_V1076094709vector @ X0 => (!! @ X0 @ (^[Y0 : X0]: (zero_zero @ X0 = (real_V1908273582scaleR @ X0 @ zero_zero @ real @ Y0)))))))),
% 3.04/0.93 inference(closure,[],[f391])).
% 3.04/0.93 thf(f1081,plain,(
% 3.04/0.93 ! [X0 : $tType] : (((real_V1076094709vector @ X0 => (!! @ X0 @ (^[Y0 : X0]: ((real_V1908273582scaleR @ X0 @ one_one @ real @ Y0) = Y0))))) = $true)),
% 3.04/0.93 inference(closure,[],[f461])).
% 3.04/0.93 thf(f1119,plain,(
% 3.04/0.93 ! [X0 : $tType] : (((real_V1076094709vector @ X0 => comm_monoid_add @ X0)) = $true)),
% 3.04/0.93 inference(closure,[],[f545])).
% 3.04/0.93 thf(f1176,plain,(
% 3.04/0.93 ! [X0 : $tType] : (((cancel1352612707id_add @ X0 => (!! @ X0 @ (^[Y0 : X0]: (!! @ X0 @ (^[Y1 : X0]: ((zero_zero @ X0 = Y0) = ((plus_plus @ X0 @ Y1 @ Y0) = Y1)))))))) = $true)),
% 3.04/0.93 inference(closure,[],[f663])).
% 3.04/0.93 thf(f1197,plain,(
% 3.04/0.93 ! [X0 : $tType] : (((comm_monoid_add @ X0 => (!! @ X0 @ (^[Y0 : X0]: ((plus_plus @ X0 @ Y0 @ zero_zero @ X0) = Y0))))) = $true)),
% 3.04/0.93 inference(closure,[],[f711])).
% 3.04/0.93 thf(f1387,plain,(
% 3.04/0.93 (real_V1076094709vector @ a = $true)),
% 3.04/0.93 inference(cnf_transformation,[],[f851])).
% 3.04/0.93 thf(f1464,plain,(
% 3.04/0.93 ( ! [X0 : $tType] : ((((real_V1076094709vector @ X0 => comm_monoid_add @ X0)) = $true)) )),
% 3.04/0.93 inference(cnf_transformation,[],[f1119])).
% 3.04/0.93 thf(f1484,plain,(
% 3.04/0.93 ($true = ((~ (member @ product_prod @ a @ a @ (product_Pair @ a @ a @ (plus_plus @ a @ (real_V1908273582scaleR @ a @ u @ x) @ (real_V1908273582scaleR @ a @ v @ y)) @ y) @ relation))))),
% 3.04/0.93 inference(cnf_transformation,[],[f639])).
% 3.04/0.93 thf(f1505,plain,(
% 3.04/0.93 ((((u = zero_zero @ real) => (member @ product_prod @ a @ a @ (product_Pair @ a @ a @ (plus_plus @ a @ (real_V1908273582scaleR @ a @ u @ x) @ (real_V1908273582scaleR @ a @ v @ y)) @ y) @ relation))) = $true)),
% 3.04/0.93 inference(cnf_transformation,[],[f751])).
% 3.04/0.93 thf(f1521,plain,(
% 3.04/0.93 (((member @ product_prod @ a @ a @ (product_Pair @ a @ a @ x @ y) @ relation)) = $true)),
% 3.04/0.93 inference(cnf_transformation,[],[f487])).
% 3.04/0.93 thf(f1540,plain,(
% 3.04/0.93 ( ! [X0 : $tType] : ((((cancel1352612707id_add @ X0 => (!! @ X0 @ (^[Y0 : X0]: (!! @ X0 @ (^[Y1 : X0]: ((zero_zero @ X0 = Y0) = ((plus_plus @ X0 @ Y1 @ Y0) = Y1)))))))) = $true)) )),
% 3.04/0.93 inference(cnf_transformation,[],[f1176])).
% 3.04/0.93 thf(f1541,plain,(
% 3.04/0.93 (cancel1352612707id_add @ real = $true)),
% 3.04/0.93 inference(cnf_transformation,[],[f483])).
% 3.04/0.93 thf(f1544,plain,(
% 3.04/0.93 ( ! [X0 : $tType] : ((((comm_monoid_add @ X0 => (!! @ X0 @ (^[Y0 : X0]: ((plus_plus @ X0 @ Y0 @ zero_zero @ X0) = Y0))))) = $true)) )),
% 3.04/0.93 inference(cnf_transformation,[],[f1197])).
% 3.04/0.93 thf(f1682,plain,(
% 3.04/0.93 ( ! [X0 : $tType] : ((((real_V1076094709vector @ X0 => (!! @ X0 @ (^[Y0 : X0]: ((real_V1908273582scaleR @ X0 @ one_one @ real @ Y0) = Y0))))) = $true)) )),
% 3.04/0.93 inference(cnf_transformation,[],[f1081])).
% 3.04/0.93 thf(f1695,plain,(
% 3.04/0.93 ( ! [X0 : $tType] : (($true = ((real_V1076094709vector @ X0 => (!! @ X0 @ (^[Y0 : X0]: (zero_zero @ X0 = (real_V1908273582scaleR @ X0 @ zero_zero @ real @ Y0)))))))) )),
% 3.04/0.93 inference(cnf_transformation,[],[f1046])).
% 3.04/0.93 thf(f1706,plain,(
% 3.04/0.93 (((((~ (u = one_one @ real)) & (~ (u = zero_zero @ real))) => (member @ product_prod @ a @ a @ (product_Pair @ a @ a @ (plus_plus @ a @ (real_V1908273582scaleR @ a @ u @ x) @ (real_V1908273582scaleR @ a @ v @ y)) @ y) @ relation))) = $true)),
% 3.04/0.93 inference(cnf_transformation,[],[f421])).
% 3.04/0.93 thf(f1708,plain,(
% 3.04/0.93 (one_one @ real = ((plus_plus @ real @ u @ v)))),
% 3.04/0.93 inference(cnf_transformation,[],[f381])).
% 3.04/0.93 thf(f1747,plain,(
% 3.04/0.93 ( ! [X0 : $tType] : ((((!! @ X0 @ (^[Y0 : X0]: ((plus_plus @ X0 @ Y0 @ zero_zero @ X0) = Y0)))) = $true) | (comm_monoid_add @ X0 = $false)) )),
% 3.04/0.93 inference(imp_proxy_clausification,[],[f1544])).
% 3.04/0.93 thf(f1772,plain,(
% 3.04/0.93 ( ! [X0 : $tType] : (($true = ((!! @ X0 @ (^[Y0 : X0]: (!! @ X0 @ (^[Y1 : X0]: ((zero_zero @ X0 = Y0) = ((plus_plus @ X0 @ Y1 @ Y0) = Y1)))))))) | (cancel1352612707id_add @ X0 = $false)) )),
% 3.04/0.93 inference(imp_proxy_clausification,[],[f1540])).
% 3.04/0.93 thf(f1784,plain,(
% 3.04/0.93 (((member @ product_prod @ a @ a @ (product_Pair @ a @ a @ (plus_plus @ a @ (real_V1908273582scaleR @ a @ u @ x) @ (real_V1908273582scaleR @ a @ v @ y)) @ y) @ relation)) = $false)),
% 3.04/0.93 inference(not_proxy_clausification,[],[f1484])).
% 3.04/0.93 thf(f1796,plain,(
% 3.04/0.93 (((member @ product_prod @ a @ a @ (product_Pair @ a @ a @ (plus_plus @ a @ (real_V1908273582scaleR @ a @ u @ x) @ (real_V1908273582scaleR @ a @ v @ y)) @ y) @ relation)) = $true) | (((u = zero_zero @ real)) = $false)),
% 3.04/0.93 inference(imp_proxy_clausification,[],[f1505])).
% 3.04/0.93 thf(f1829,plain,(
% 3.04/0.93 ( ! [X0 : $tType] : ((((!! @ X0 @ (^[Y0 : X0]: ((real_V1908273582scaleR @ X0 @ one_one @ real @ Y0) = Y0)))) = $true) | (real_V1076094709vector @ X0 = $false)) )),
% 3.04/0.93 inference(imp_proxy_clausification,[],[f1682])).
% 3.04/0.93 thf(f1840,plain,(
% 3.04/0.93 ( ! [X0 : $tType] : (($true = ((!! @ X0 @ (^[Y0 : X0]: (zero_zero @ X0 = (real_V1908273582scaleR @ X0 @ zero_zero @ real @ Y0)))))) | (real_V1076094709vector @ X0 = $false)) )),
% 3.04/0.93 inference(imp_proxy_clausification,[],[f1695])).
% 3.04/0.93 thf(f1893,plain,(
% 3.04/0.93 ( ! [X0 : $tType] : ((real_V1076094709vector @ X0 = $false) | (comm_monoid_add @ X0 = $true)) )),
% 3.04/0.93 inference(imp_proxy_clausification,[],[f1464])).
% 3.04/0.93 thf(f1905,plain,(
% 3.04/0.93 ((((~ (u = one_one @ real)) & (~ (u = zero_zero @ real)))) = $false) | (((member @ product_prod @ a @ a @ (product_Pair @ a @ a @ (plus_plus @ a @ (real_V1908273582scaleR @ a @ u @ x) @ (real_V1908273582scaleR @ a @ v @ y)) @ y) @ relation)) = $true)),
% 3.04/0.93 inference(imp_proxy_clausification,[],[f1706])).
% 3.04/0.93 thf(f1994,plain,(
% 3.04/0.93 (((member @ product_prod @ a @ a @ (product_Pair @ a @ a @ (plus_plus @ a @ (real_V1908273582scaleR @ a @ u @ x) @ (real_V1908273582scaleR @ a @ v @ y)) @ y) @ relation)) = $true) | (u != zero_zero @ real)),
% 3.04/0.93 inference(equality_proxy_clausification,[],[f1796])).
% 3.04/0.93 thf(f2018,plain,(
% 3.04/0.93 (((~ (u = one_one @ real))) = $false) | (((~ (u = zero_zero @ real))) = $false) | (((member @ product_prod @ a @ a @ (product_Pair @ a @ a @ (plus_plus @ a @ (real_V1908273582scaleR @ a @ u @ x) @ (real_V1908273582scaleR @ a @ v @ y)) @ y) @ relation)) = $true)),
% 3.04/0.93 inference(and_proxy_clausification,[],[f1905])).
% 3.04/0.93 thf(f2033,definition,(
% 3.04/0.93 spl0_1 <=> (((member @ product_prod @ a @ a @ (product_Pair @ a @ a @ (plus_plus @ a @ (real_V1908273582scaleR @ a @ u @ x) @ (real_V1908273582scaleR @ a @ v @ y)) @ y) @ relation)) = $true)),
% 3.04/0.93 introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition])).
% 3.04/0.93 thf(f2035,plain,(
% 3.04/0.93 (((member @ product_prod @ a @ a @ (product_Pair @ a @ a @ (plus_plus @ a @ (real_V1908273582scaleR @ a @ u @ x) @ (real_V1908273582scaleR @ a @ v @ y)) @ y) @ relation)) = $true) | ~spl0_1),
% 3.04/0.93 inference(avatar_component_clause,[],[f2033])).
% 3.04/0.93 thf(f2037,definition,(
% 3.04/0.93 spl0_2 <=> (u = zero_zero @ real)),
% 3.04/0.93 introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition])).
% 3.04/0.93 thf(f2040,plain,(
% 3.04/0.93 spl0_1 | ~spl0_2),
% 3.04/0.93 inference(avatar_split_clause,[],[f1994,f2037,f2033])).
% 3.04/0.93 thf(f2042,plain,(
% 3.04/0.93 (((u = one_one @ real)) = $true) | (((member @ product_prod @ a @ a @ (product_Pair @ a @ a @ (plus_plus @ a @ (real_V1908273582scaleR @ a @ u @ x) @ (real_V1908273582scaleR @ a @ v @ y)) @ y) @ relation)) = $true) | (((~ (u = zero_zero @ real))) = $false)),
% 3.04/0.93 inference(not_proxy_clausification,[],[f2018])).
% 3.04/0.93 thf(f2043,plain,(
% 3.04/0.93 (((~ (u = zero_zero @ real))) = $false) | (u = one_one @ real) | (((member @ product_prod @ a @ a @ (product_Pair @ a @ a @ (plus_plus @ a @ (real_V1908273582scaleR @ a @ u @ x) @ (real_V1908273582scaleR @ a @ v @ y)) @ y) @ relation)) = $true)),
% 3.04/0.93 inference(equality_proxy_clausification,[],[f2042])).
% 3.04/0.93 thf(f2044,plain,(
% 3.04/0.93 (((u = zero_zero @ real)) = $true) | (((member @ product_prod @ a @ a @ (product_Pair @ a @ a @ (plus_plus @ a @ (real_V1908273582scaleR @ a @ u @ x) @ (real_V1908273582scaleR @ a @ v @ y)) @ y) @ relation)) = $true) | (u = one_one @ real)),
% 3.04/0.93 inference(not_proxy_clausification,[],[f2043])).
% 3.04/0.93 thf(f2045,plain,(
% 3.04/0.93 (u = zero_zero @ real) | (u = one_one @ real) | (((member @ product_prod @ a @ a @ (product_Pair @ a @ a @ (plus_plus @ a @ (real_V1908273582scaleR @ a @ u @ x) @ (real_V1908273582scaleR @ a @ v @ y)) @ y) @ relation)) = $true)),
% 3.04/0.93 inference(equality_proxy_clausification,[],[f2044])).
% 3.04/0.93 thf(f2047,definition,(
% 3.04/0.93 spl0_3 <=> (u = one_one @ real)),
% 3.04/0.93 introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition])).
% 3.04/0.93 thf(f2049,plain,(
% 3.04/0.93 (u = one_one @ real) | ~spl0_3),
% 3.04/0.93 inference(avatar_component_clause,[],[f2047])).
% 3.04/0.93 thf(f2050,plain,(
% 3.04/0.93 spl0_2 | spl0_1 | spl0_3),
% 3.04/0.93 inference(avatar_split_clause,[],[f2045,f2047,f2033,f2037])).
% 3.04/0.93 thf(f2130,plain,(
% 3.04/0.93 (comm_monoid_add @ a = $true) | ($true = $false)),
% 3.04/0.93 inference(superposition,[],[f1893,f1387])).
% 3.04/0.93 thf(f2135,plain,(
% 3.04/0.93 (comm_monoid_add @ a = $true)),
% 3.04/0.93 inference(trivial_inequality_removal,[],[f2130])).
% 3.04/0.93 thf(f2220,plain,(
% 3.04/0.93 (u = ((plus_plus @ real @ u @ v))) | ~spl0_3),
% 3.04/0.93 inference(forward_demodulation,[],[f1708,f2049])).
% 3.04/0.93 thf(f2637,plain,(
% 3.04/0.93 ( ! [X0 : $tType,X1 : X0] : (((((^[Y0 : X0]: ((plus_plus @ X0 @ Y0 @ zero_zero @ X0) = Y0)) @ X1)) = $true) | (comm_monoid_add @ X0 = $false)) )),
% 3.04/0.93 inference(pi_proxy_clausification,[],[f1747])).
% 3.04/0.93 thf(f2638,plain,(
% 3.04/0.93 ( ! [X0 : $tType,X1 : X0] : (((((plus_plus @ X0 @ X1 @ zero_zero @ X0) = X1)) = $true) | (comm_monoid_add @ X0 = $false)) )),
% 3.04/0.93 inference(beta-eta_normalization,[],[f2637])).
% 3.04/0.93 thf(f2639,plain,(
% 3.04/0.93 ( ! [X0 : $tType,X1 : X0] : ((((plus_plus @ X0 @ X1 @ zero_zero @ X0)) = X1) | (comm_monoid_add @ X0 = $false)) )),
% 3.04/0.93 inference(equality_proxy_clausification,[],[f2638])).
% 3.04/0.93 thf(f2736,plain,(
% 3.04/0.93 ( ! [X0 : $tType,X1 : X0] : (($true = (((^[Y0 : X0]: ((real_V1908273582scaleR @ X0 @ one_one @ real @ Y0) = Y0)) @ X1))) | (real_V1076094709vector @ X0 = $false)) )),
% 3.04/0.93 inference(pi_proxy_clausification,[],[f1829])).
% 3.04/0.93 thf(f2737,plain,(
% 3.04/0.93 ( ! [X0 : $tType,X1 : X0] : (((((real_V1908273582scaleR @ X0 @ one_one @ real @ X1) = X1)) = $true) | (real_V1076094709vector @ X0 = $false)) )),
% 3.04/0.93 inference(beta-eta_normalization,[],[f2736])).
% 3.04/0.93 thf(f2753,plain,(
% 3.04/0.93 ( ! [X0 : $tType,X1 : X0] : ((real_V1076094709vector @ X0 = $false) | ((((^[Y0 : X0]: (zero_zero @ X0 = (real_V1908273582scaleR @ X0 @ zero_zero @ real @ Y0))) @ X1)) = $true)) )),
% 3.04/0.93 inference(pi_proxy_clausification,[],[f1840])).
% 3.04/0.93 thf(f2754,plain,(
% 3.04/0.93 ( ! [X0 : $tType,X1 : X0] : ((real_V1076094709vector @ X0 = $false) | (((zero_zero @ X0 = (real_V1908273582scaleR @ X0 @ zero_zero @ real @ X1))) = $true)) )),
% 3.04/0.93 inference(beta-eta_normalization,[],[f2753])).
% 3.04/0.93 thf(f2755,plain,(
% 3.04/0.93 ( ! [X0 : $tType,X1 : X0] : ((zero_zero @ X0 = ((real_V1908273582scaleR @ X0 @ zero_zero @ real @ X1))) | (real_V1076094709vector @ X0 = $false)) )),
% 3.04/0.93 inference(equality_proxy_clausification,[],[f2754])).
% 3.04/0.93 thf(f3074,plain,(
% 3.04/0.93 ( ! [X0 : $tType,X1 : X0] : (($true = (((^[Y0 : X0]: (!! @ X0 @ (^[Y1 : X0]: ((zero_zero @ X0 = Y0) = ((plus_plus @ X0 @ Y1 @ Y0) = Y1))))) @ X1))) | (cancel1352612707id_add @ X0 = $false)) )),
% 3.04/0.93 inference(pi_proxy_clausification,[],[f1772])).
% 3.04/0.93 thf(f3075,plain,(
% 3.04/0.93 ( ! [X0 : $tType,X1 : X0] : ((((!! @ X0 @ (^[Y0 : X0]: ((zero_zero @ X0 = X1) = ((plus_plus @ X0 @ Y0 @ X1) = Y0))))) = $true) | (cancel1352612707id_add @ X0 = $false)) )),
% 3.04/0.93 inference(beta-eta_normalization,[],[f3074])).
% 3.04/0.93 thf(f3076,plain,(
% 3.04/0.93 ( ! [X0 : $tType,X2 : X0,X1 : X0] : ((cancel1352612707id_add @ X0 = $false) | ((((^[Y0 : X0]: ((zero_zero @ X0 = X1) = ((plus_plus @ X0 @ Y0 @ X1) = Y0))) @ X2)) = $true)) )),
% 3.04/0.93 inference(pi_proxy_clausification,[],[f3075])).
% 3.04/0.93 thf(f3077,plain,(
% 3.04/0.93 ( ! [X0 : $tType,X2 : X0,X1 : X0] : ((cancel1352612707id_add @ X0 = $false) | ((((zero_zero @ X0 = X1) = ((plus_plus @ X0 @ X2 @ X1) = X2))) = $true)) )),
% 3.04/0.93 inference(beta-eta_normalization,[],[f3076])).
% 3.04/0.93 thf(f3078,plain,(
% 3.04/0.93 ( ! [X0 : $tType,X2 : X0,X1 : X0] : ((cancel1352612707id_add @ X0 = $false) | ((((plus_plus @ X0 @ X2 @ X1) = X2)) = ((zero_zero @ X0 = X1)))) )),
% 3.04/0.93 inference(equality_proxy_clausification,[],[f3077])).
% 3.04/0.93 thf(f3080,plain,(
% 3.04/0.93 ( ! [X0 : $tType,X2 : X0,X1 : X0] : ((((zero_zero @ X0 = X1)) = $true) | (cancel1352612707id_add @ X0 = $false) | ((((plus_plus @ X0 @ X2 @ X1) = X2)) = $false)) )),
% 3.04/0.93 inference(iff_proxy_clausification,[],[f3078])).
% 3.04/0.93 thf(f3082,plain,(
% 3.04/0.93 ( ! [X0 : $tType,X2 : X0,X1 : X0] : ((zero_zero @ X0 = X1) | ((((plus_plus @ X0 @ X2 @ X1) = X2)) = $false) | (cancel1352612707id_add @ X0 = $false)) )),
% 3.04/0.93 inference(equality_proxy_clausification,[],[f3080])).
% 3.04/0.93 thf(f3084,plain,(
% 3.04/0.93 ( ! [X0 : $tType,X2 : X0,X1 : X0] : ((((plus_plus @ X0 @ X2 @ X1)) != X2) | (cancel1352612707id_add @ X0 = $false) | (zero_zero @ X0 = X1)) )),
% 3.04/0.93 inference(equality_proxy_clausification,[],[f3082])).
% 3.04/0.93 thf(f3310,plain,(
% 3.04/0.93 (cancel1352612707id_add @ real = $false) | (u != u) | (zero_zero @ real = v) | ~spl0_3),
% 3.04/0.93 inference(superposition,[],[f3084,f2220])).
% 3.04/0.93 thf(f3311,plain,(
% 3.04/0.93 (zero_zero @ real = v) | (cancel1352612707id_add @ real = $false) | ~spl0_3),
% 3.04/0.93 inference(trivial_inequality_removal,[],[f3310])).
% 3.04/0.93 thf(f3312,plain,(
% 3.04/0.93 (zero_zero @ real = v) | ($true = $false) | ~spl0_3),
% 3.04/0.93 inference(forward_demodulation,[],[f3311,f1541])).
% 3.04/0.93 thf(f3313,plain,(
% 3.04/0.93 (zero_zero @ real = v) | ~spl0_3),
% 3.04/0.93 inference(trivial_inequality_removal,[],[f3312])).
% 3.04/0.93 thf(f3354,definition,(
% 3.04/0.93 spl0_66 <=> (zero_zero @ real = v)),
% 3.04/0.93 introduced(definition,[new_symbols(definition,[spl0_66])],[avatar_definition])).
% 3.04/0.93 thf(f3355,plain,(
% 3.04/0.93 (zero_zero @ real != v) | spl0_66),
% 3.04/0.93 inference(avatar_component_clause,[],[f3354])).
% 3.04/0.93 thf(f3356,plain,(
% 3.04/0.93 (zero_zero @ real = v) | ~spl0_66),
% 3.04/0.93 inference(avatar_component_clause,[],[f3354])).
% 3.04/0.93 thf(f3488,plain,(
% 3.04/0.93 $false | (~spl0_3 | spl0_66)),
% 3.04/0.93 inference(forward_subsumption_resolution,[],[f3313,f3355])).
% 3.04/0.93 thf(f3489,plain,(
% 3.04/0.93 ~spl0_3 | spl0_66),
% 3.04/0.93 inference(avatar_contradiction_clause,[],[f3488])).
% 3.04/0.93 thf(f3490,plain,(
% 3.04/0.93 ( ! [X0 : $tType,X1 : X0] : ((((real_V1908273582scaleR @ X0 @ one_one @ real @ X1)) = X1) | (real_V1076094709vector @ X0 = $false)) )),
% 3.04/0.93 inference(equality_proxy_clausification,[],[f2737])).
% 3.04/0.93 thf(f3496,plain,(
% 3.04/0.93 ($true = $false) | ~spl0_1),
% 3.04/0.93 inference(forward_demodulation,[],[f2035,f1784])).
% 3.04/0.93 thf(f3497,plain,(
% 3.04/0.93 $false | ~spl0_1),
% 3.04/0.93 inference(trivial_inequality_removal,[],[f3496])).
% 3.04/0.93 thf(f3498,plain,(
% 3.04/0.93 ~spl0_1),
% 3.04/0.93 inference(avatar_contradiction_clause,[],[f3497])).
% 3.04/0.93 thf(f3544,plain,(
% 3.04/0.93 ( ! [X0 : $tType,X1 : X0] : ((zero_zero @ X0 = ((real_V1908273582scaleR @ X0 @ v @ X1))) | (real_V1076094709vector @ X0 = $false)) ) | ~spl0_66),
% 3.04/0.93 inference(superposition,[],[f2755,f3356])).
% 3.04/0.93 thf(f3625,plain,(
% 3.04/0.93 ( ! [X0 : $tType,X1 : X0] : ((((real_V1908273582scaleR @ X0 @ u @ X1)) = X1) | (real_V1076094709vector @ X0 = $false)) ) | ~spl0_3),
% 3.04/0.93 inference(forward_demodulation,[],[f3490,f2049])).
% 3.04/0.93 thf(f3630,plain,(
% 3.04/0.93 (((member @ product_prod @ a @ a @ (product_Pair @ a @ a @ (plus_plus @ a @ x @ (real_V1908273582scaleR @ a @ v @ y)) @ y) @ relation)) = $false) | (real_V1076094709vector @ a = $false) | ~spl0_3),
% 3.04/0.93 inference(superposition,[],[f1784,f3625])).
% 3.04/0.93 thf(f3631,plain,(
% 3.04/0.93 (((member @ product_prod @ a @ a @ (product_Pair @ a @ a @ (plus_plus @ a @ x @ (real_V1908273582scaleR @ a @ v @ y)) @ y) @ relation)) = $false) | ($true = $false) | ~spl0_3),
% 3.04/0.93 inference(forward_demodulation,[],[f3630,f1387])).
% 3.04/0.93 thf(f3632,plain,(
% 3.04/0.93 (((member @ product_prod @ a @ a @ (product_Pair @ a @ a @ (plus_plus @ a @ x @ (real_V1908273582scaleR @ a @ v @ y)) @ y) @ relation)) = $false) | ~spl0_3),
% 3.04/0.93 inference(trivial_inequality_removal,[],[f3631])).
% 3.04/0.93 thf(f5222,definition,(
% 3.04/0.93 spl0_102 <=> (((member @ product_prod @ a @ a @ (product_Pair @ a @ a @ (plus_plus @ a @ x @ zero_zero @ a) @ y) @ relation)) = $false)),
% 3.04/0.93 introduced(definition,[new_symbols(definition,[spl0_102])],[avatar_definition])).
% 3.04/0.93 thf(f5224,plain,(
% 3.04/0.93 (((member @ product_prod @ a @ a @ (product_Pair @ a @ a @ (plus_plus @ a @ x @ zero_zero @ a) @ y) @ relation)) = $false) | ~spl0_102),
% 3.04/0.93 inference(avatar_component_clause,[],[f5222])).
% 3.04/0.93 thf(f5280,plain,(
% 3.04/0.93 (((member @ product_prod @ a @ a @ (product_Pair @ a @ a @ (plus_plus @ a @ x @ zero_zero @ a) @ y) @ relation)) = $false) | (real_V1076094709vector @ a = $false) | (~spl0_3 | ~spl0_66)),
% 3.04/0.93 inference(superposition,[],[f3632,f3544])).
% 3.04/0.93 thf(f5284,plain,(
% 3.04/0.93 ($true = $false) | (((member @ product_prod @ a @ a @ (product_Pair @ a @ a @ (plus_plus @ a @ x @ zero_zero @ a) @ y) @ relation)) = $false) | (~spl0_3 | ~spl0_66)),
% 3.04/0.93 inference(forward_demodulation,[],[f5280,f1387])).
% 3.04/0.93 thf(f5285,plain,(
% 3.04/0.93 (((member @ product_prod @ a @ a @ (product_Pair @ a @ a @ (plus_plus @ a @ x @ zero_zero @ a) @ y) @ relation)) = $false) | (~spl0_3 | ~spl0_66)),
% 3.04/0.93 inference(trivial_inequality_removal,[],[f5284])).
% 3.04/0.93 thf(f5292,plain,(
% 3.04/0.93 spl0_102 | ~spl0_3 | ~spl0_66),
% 3.04/0.93 inference(avatar_split_clause,[],[f5285,f3354,f2047,f5222])).
% 3.04/0.93 thf(f5299,plain,(
% 3.04/0.93 (((member @ product_prod @ a @ a @ (product_Pair @ a @ a @ x @ y) @ relation)) = $false) | (comm_monoid_add @ a = $false) | ~spl0_102),
% 3.04/0.93 inference(superposition,[],[f5224,f2639])).
% 3.04/0.93 thf(f5302,plain,(
% 3.04/0.93 (comm_monoid_add @ a = $false) | ($true = $false) | ~spl0_102),
% 3.04/0.93 inference(forward_demodulation,[],[f5299,f1521])).
% 3.04/0.93 thf(f5303,plain,(
% 3.04/0.93 (comm_monoid_add @ a = $false) | ~spl0_102),
% 3.04/0.93 inference(trivial_inequality_removal,[],[f5302])).
% 3.04/0.93 thf(f5327,plain,(
% 3.04/0.93 ($true = $false) | ~spl0_102),
% 3.04/0.93 inference(superposition,[],[f5303,f2135])).
% 3.04/0.93 thf(f5333,plain,(
% 3.04/0.93 $false | ~spl0_102),
% 3.04/0.93 inference(trivial_inequality_removal,[],[f5327])).
% 3.04/0.93 thf(f5334,plain,(
% 3.04/0.93 ~spl0_102),
% 3.04/0.93 inference(avatar_contradiction_clause,[],[f5333])).
% 3.04/0.93 cnf(s1, plain, spl0_1 | ~spl0_2, inference(sat_conversion,[],[f2040])).
% 3.04/0.93 cnf(s2, plain, spl0_1 | spl0_2 | spl0_3, inference(sat_conversion,[],[f2050])).
% 3.04/0.93 cnf(s120, plain, ~spl0_3 | spl0_66, inference(sat_conversion,[],[f3489])).
% 3.04/0.93 cnf(s121, plain, ~spl0_1, inference(sat_conversion,[],[f3498])).
% 3.04/0.93 cnf(s160, plain, ~spl0_3 | ~spl0_66 | spl0_102, inference(sat_conversion,[],[f5292])).
% 3.04/0.93 cnf(s163, plain, ~spl0_102, inference(sat_conversion,[],[f5334])).
% 3.04/0.93 cnf(s164, plain, ~spl0_3 | ~spl0_66, inference(rat,[],[s160,s163])).
% 3.04/0.93 cnf(s167, plain, spl0_2 | spl0_3, inference(rat,[],[s2,s121])).
% 3.04/0.93 cnf(s168, plain, ~spl0_2, inference(rat,[],[s1,s121])).
% 3.04/0.93 cnf(s170, plain, spl0_3, inference(rat,[],[s167,s168])).
% 3.04/0.93 cnf(s171, plain, ~spl0_66, inference(rat,[],[s164,s170])).
% 3.04/0.93 cnf(s172, plain, $false, inference(rat,[],[s120,s171,s170])).
% 3.04/0.93 thf(f5335,plain,(
% 3.04/0.93 $false),
% 3.04/0.93 inference(avatar_sat_refutation,[],[s172])).
% 3.04/0.93 % SZS output end Proof for theBenchmark
% 3.04/0.93 % (3664650)------------------------------
% 3.04/0.93 % (3664650)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.04/0.93 % (3664650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/0.93 % (3664650)CaDiCaL version: 2.1.3
% 3.04/0.93 % (3664650)Termination reason: Refutation
% 3.04/0.93 % (3664650)Time elapsed: 0.230 s
% 3.04/0.93 % (3664650)Peak memory usage: 16 MB
% 3.04/0.93 % (3664650)Instructions burned: 491 (million)
% 3.04/0.93 % (3664585)Success in time 0.546 s
% 3.04/0.93 % Vampire exiting
%------------------------------------------------------------------------------