%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM925^1 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n007.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:19:02 AM UTC 2026
% Result : Theorem 0.22s 0.32s
% Output : Refutation 0.22s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM925^1 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.18 % Computer : n007.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Tue Sep 29 13:03:41 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.22 Running higher-order theorem proving
% 0.09/0.24 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.22/0.31 % (3327917)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.22/0.31 % (3327942)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=3894587880:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.22/0.31 % (3327944)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.22/0.31 % (3327944)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.22/0.31 % (3327938)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3024503725:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.22/0.31 % (3327940)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=2582072682:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.22/0.31 % (3327939)lrs+10_16_si=on:nwc=1.5:random_seed=3762092876:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.22/0.31 % (3327943)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=703908479:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.22/0.31 % (3327942)Instruction limit reached!
% 0.22/0.31 % (3327942)------------------------------
% 0.22/0.31 % (3327942)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.31 % (3327942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.31 % (3327942)CaDiCaL version: 2.1.3
% 0.22/0.31 % (3327942)Termination reason: Instruction limit
% 0.22/0.31 % (3327942)Termination phase: Saturation
% 0.22/0.31 % (3327942)Time elapsed: 0.007 s
% 0.22/0.31 % (3327942)Peak memory usage: 12 MB
% 0.22/0.31 % (3327942)Instructions burned: 26 (million)
% 0.22/0.31 % (3327941)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=4204970070: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.22/0.31 % (3327944)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=587770346:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.22/0.31 % (3327940)Instruction limit reached!
% 0.22/0.31 % (3327940)------------------------------
% 0.22/0.31 % (3327940)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.31 % (3327940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.31 % (3327940)CaDiCaL version: 2.1.3
% 0.22/0.31 % (3327940)Termination reason: Instruction limit
% 0.22/0.31 % (3327940)Termination phase: Property scanning
% 0.22/0.31 % (3327940)Time elapsed: 0.002 s
% 0.22/0.31 % (3327940)Peak memory usage: 10 MB
% 0.22/0.31 % (3327940)Instructions burned: 5 (million)
% 0.22/0.31 % (3327939)Instruction limit reached!
% 0.22/0.31 % (3327939)------------------------------
% 0.22/0.31 % (3327939)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.31 % (3327939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.31 % (3327939)CaDiCaL version: 2.1.3
% 0.22/0.31 % (3327939)Termination reason: Instruction limit
% 0.22/0.31 % (3327939)Termination phase: Saturation
% 0.22/0.31 % (3327939)Time elapsed: 0.008 s
% 0.22/0.31 % (3327939)Peak memory usage: 12 MB
% 0.22/0.31 % (3327939)Instructions burned: 18 (million)
% 0.22/0.31 % (3327965)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=855842496:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.22/0.31 % (3327965)Instruction limit reached!
% 0.22/0.31 % (3327965)------------------------------
% 0.22/0.31 % (3327965)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.31 % (3327965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.31 % (3327965)CaDiCaL version: 2.1.3
% 0.22/0.31 % (3327965)Termination reason: Instruction limit
% 0.22/0.31 % (3327965)Termination phase: Property scanning
% 0.22/0.31 % (3327965)Time elapsed: 0.001 s
% 0.22/0.31 % (3327965)Peak memory usage: 10 MB
% 0.22/0.31 % (3327965)Instructions burned: 4 (million)
% 0.22/0.31 % (3327941) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3327917-3327941"...
% 0.22/0.31 % (3327941)...printing done.
% 0.22/0.32 % (3327943) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3327917-3327943"...
% 0.22/0.32 % (3327968)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=2199837612:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.22/0.32 % (3327941)Refutation found. Thanks to Tanya!
% 0.22/0.32 % SZS status Theorem for theBenchmark
% 0.22/0.32 % SZS output start Proof for theBenchmark
% 0.22/0.32 thf(type_def_5, type, int: $tType).
% 0.22/0.32 thf(type_def_6, type, nat: $tType).
% 0.22/0.32 thf(type_def_7, type, sTfun: ($tType * $tType) > $tType).
% 0.22/0.32 thf(func_def_0, type, one_one_int: int).
% 0.22/0.32 thf(func_def_1, type, one_one_nat: nat).
% 0.22/0.32 thf(func_def_2, type, plus_plus_int: (int > int > int)).
% 0.22/0.32 thf(func_def_3, type, plus_plus_nat: (nat > nat > nat)).
% 0.22/0.32 thf(func_def_4, type, zero_zero_int: int).
% 0.22/0.32 thf(func_def_5, type, zero_zero_nat: nat).
% 0.22/0.32 thf(func_def_6, type, bit0: (int > int)).
% 0.22/0.32 thf(func_def_7, type, bit1: (int > int)).
% 0.22/0.32 thf(func_def_8, type, pls: int).
% 0.22/0.32 thf(func_def_9, type, number_number_of_int: (int > int)).
% 0.22/0.32 thf(func_def_10, type, number_number_of_nat: (int > nat)).
% 0.22/0.32 thf(func_def_11, type, semiri1621563631at_int: (nat > int)).
% 0.22/0.32 thf(func_def_12, type, semiri984289939at_nat: (nat > nat)).
% 0.22/0.32 thf(func_def_13, type, ord_less_int: (int > int > $o)).
% 0.22/0.32 thf(func_def_14, type, ord_less_nat: (nat > nat > $o)).
% 0.22/0.32 thf(func_def_15, type, power_power_int: (int > nat > int)).
% 0.22/0.32 thf(func_def_16, type, power_power_nat: (nat > nat > nat)).
% 0.22/0.32 thf(func_def_17, type, n: nat).
% 0.22/0.32 thf(func_def_18, type, t: int).
% 0.22/0.32 thf(func_def_23, type, inv_bit1_1: (int > int)).
% 0.22/0.32 thf(func_def_24, type, inv_bit0_2: (int > int)).
% 0.22/0.32 thf(func_def_25, type, inv_semiri1621563631at_int_3: (int > nat)).
% 0.22/0.32 thf(f1,axiom,(
% 0.22/0.32 (ord_less_int @ zero_zero_int @ (plus_plus_int @ one_one_int @ (semiri1621563631at_int @ n)))),
% 0.22/0.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_0_n1pos)).
% 0.22/0.32 thf(f6,axiom,(
% 0.22/0.32 (((power_power_int @ zero_zero_int @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))) = zero_zero_int)),
% 0.22/0.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_5_zero__power2)).
% 0.22/0.32 thf(f17,axiom,(
% 0.22/0.32 (one_one_int = ((number_number_of_int @ (bit1 @ pls))))),
% 0.22/0.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_16_semiring__norm_I110_J)).
% 0.22/0.32 thf(f63,axiom,(
% 0.22/0.32 ~(ord_less_int @ pls @ zero_zero_int)),
% 0.22/0.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_62_bin__less__0__simps_I1_J)).
% 0.22/0.32 thf(f79,axiom,(
% 0.22/0.32 (pls = zero_zero_int)),
% 0.22/0.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_78_Pls__def)).
% 0.22/0.32 thf(f93,axiom,(
% 0.22/0.32 ! [X1 : int,X0 : int] : ((((power_power_int @ X0 @ (number_number_of_nat @ X1))) = zero_zero_int) <=> ((((number_number_of_nat @ X1)) != zero_zero_nat) & (X0 = zero_zero_int)))),
% 0.22/0.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_92_power__eq__0__iff__number__of)).
% 0.22/0.32 thf(f107,conjecture,(
% 0.22/0.32 (((power_power_int @ (plus_plus_int @ one_one_int @ (semiri1621563631at_int @ n)) @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))) != zero_zero_int)),
% 0.22/0.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0)).
% 0.22/0.32 thf(f108,negated_conjecture,(
% 0.22/0.32 ~ (((power_power_int @ (plus_plus_int @ one_one_int @ (semiri1621563631at_int @ n)) @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))) != zero_zero_int)),
% 0.22/0.32 inference(negated_conjecture,[status(cth)],[f107])).
% 0.22/0.32 thf(f135,plain,(
% 0.22/0.32 ~(ord_less_int @ pls @ zero_zero_int)),
% 0.22/0.32 inference(rectify,[],[f63])).
% 0.22/0.32 thf(f136,plain,(
% 0.22/0.32 ~ (((ord_less_int @ pls @ zero_zero_int)) = $true)),
% 0.22/0.32 inference(fool_elimination,[],[f135])).
% 0.22/0.32 thf(f159,plain,(
% 0.22/0.32 (ord_less_int @ zero_zero_int @ (plus_plus_int @ one_one_int @ (semiri1621563631at_int @ n)))),
% 0.22/0.32 inference(rectify,[],[f1])).
% 0.22/0.32 thf(f160,plain,(
% 0.22/0.32 (((ord_less_int @ zero_zero_int @ (plus_plus_int @ one_one_int @ (semiri1621563631at_int @ n)))) = $true)),
% 0.22/0.32 inference(fool_elimination,[],[f159])).
% 0.22/0.32 thf(f183,plain,(
% 0.22/0.32 (((ord_less_int @ pls @ zero_zero_int)) != $true)),
% 0.22/0.32 inference(flattening,[],[f136])).
% 0.22/0.32 thf(f185,plain,(
% 0.22/0.32 (zero_zero_int = ((power_power_int @ (plus_plus_int @ one_one_int @ (semiri1621563631at_int @ n)) @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))))),
% 0.22/0.32 inference(flattening,[],[f108])).
% 0.22/0.32 thf(f211,plain,(
% 0.22/0.32 ! [X1 : int,X0 : int] : (((((power_power_int @ X0 @ (number_number_of_nat @ X1))) = zero_zero_int) | ((zero_zero_nat = ((number_number_of_nat @ X1))) | (zero_zero_int != X0))) & (((((number_number_of_nat @ X1)) != zero_zero_nat) & (X0 = zero_zero_int)) | (zero_zero_int != ((power_power_int @ X0 @ (number_number_of_nat @ X1))))))),
% 0.22/0.32 inference(nnf_transformation,[],[f93])).
% 0.22/0.32 thf(f212,plain,(
% 0.22/0.32 ! [X1 : int,X0 : int] : (((((power_power_int @ X0 @ (number_number_of_nat @ X1))) = zero_zero_int) | (zero_zero_nat = ((number_number_of_nat @ X1))) | (zero_zero_int != X0)) & (((((number_number_of_nat @ X1)) != zero_zero_nat) & (X0 = zero_zero_int)) | (zero_zero_int != ((power_power_int @ X0 @ (number_number_of_nat @ X1))))))),
% 0.22/0.32 inference(flattening,[],[f211])).
% 0.22/0.32 thf(f213,plain,(
% 0.22/0.32 ! [X0 : int,X1 : int] : (((zero_zero_int = ((power_power_int @ X1 @ (number_number_of_nat @ X0)))) | (zero_zero_nat = ((number_number_of_nat @ X0))) | (zero_zero_int != X1)) & (((zero_zero_nat != ((number_number_of_nat @ X0))) & (zero_zero_int = X1)) | (zero_zero_int != ((power_power_int @ X1 @ (number_number_of_nat @ X0))))))),
% 0.22/0.32 inference(rectify,[],[f212])).
% 0.22/0.32 thf(f243,plain,(
% 0.22/0.32 (zero_zero_int = ((power_power_int @ zero_zero_int @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))))),
% 0.22/0.32 inference(cnf_transformation,[],[f6])).
% 0.22/0.32 thf(f260,plain,(
% 0.22/0.32 (zero_zero_int = pls)),
% 0.22/0.32 inference(cnf_transformation,[],[f79])).
% 0.22/0.32 thf(f284,plain,(
% 0.22/0.32 (one_one_int = ((number_number_of_int @ (bit1 @ pls))))),
% 0.22/0.32 inference(cnf_transformation,[],[f17])).
% 0.22/0.32 thf(f305,plain,(
% 0.22/0.32 ( ! [X0 : int,X1 : int] : ((zero_zero_int != ((power_power_int @ X1 @ (number_number_of_nat @ X0)))) | (zero_zero_int = X1)) )),
% 0.22/0.32 inference(cnf_transformation,[],[f213])).
% 0.22/0.32 thf(f343,plain,(
% 0.22/0.32 (((ord_less_int @ zero_zero_int @ (plus_plus_int @ one_one_int @ (semiri1621563631at_int @ n)))) = $true)),
% 0.22/0.32 inference(cnf_transformation,[],[f160])).
% 0.22/0.32 thf(f349,plain,(
% 0.22/0.32 (zero_zero_int = ((power_power_int @ (plus_plus_int @ one_one_int @ (semiri1621563631at_int @ n)) @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))))),
% 0.22/0.32 inference(cnf_transformation,[],[f185])).
% 0.22/0.32 thf(f353,plain,(
% 0.22/0.32 (((ord_less_int @ pls @ zero_zero_int)) != $true)),
% 0.22/0.32 inference(cnf_transformation,[],[f183])).
% 0.22/0.32 thf(f463,definition,(
% 0.22/0.32 spl0_8 <=> (one_one_int = ((number_number_of_int @ (bit1 @ pls))))),
% 0.22/0.32 introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition])).
% 0.22/0.32 thf(f465,plain,(
% 0.22/0.32 (one_one_int = ((number_number_of_int @ (bit1 @ pls)))) | ~spl0_8),
% 0.22/0.32 inference(avatar_component_clause,[],[f463])).
% 0.22/0.32 thf(f466,plain,(
% 0.22/0.32 spl0_8),
% 0.22/0.32 inference(avatar_split_clause,[],[f284,f463])).
% 0.22/0.32 thf(f473,definition,(
% 0.22/0.32 spl0_10 <=> (zero_zero_int = ((power_power_int @ zero_zero_int @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))))),
% 0.22/0.32 introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition])).
% 0.22/0.32 thf(f476,plain,(
% 0.22/0.32 spl0_10),
% 0.22/0.32 inference(avatar_split_clause,[],[f243,f473])).
% 0.22/0.32 thf(f478,definition,(
% 0.22/0.32 spl0_11 <=> (((ord_less_int @ zero_zero_int @ (plus_plus_int @ one_one_int @ (semiri1621563631at_int @ n)))) = $true)),
% 0.22/0.32 introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition])).
% 0.22/0.32 thf(f481,plain,(
% 0.22/0.32 spl0_11),
% 0.22/0.32 inference(avatar_split_clause,[],[f343,f478])).
% 0.22/0.32 thf(f488,definition,(
% 0.22/0.32 spl0_13 <=> (zero_zero_int = ((power_power_int @ (plus_plus_int @ one_one_int @ (semiri1621563631at_int @ n)) @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))))),
% 0.22/0.32 introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition])).
% 0.22/0.32 thf(f490,plain,(
% 0.22/0.32 (zero_zero_int = ((power_power_int @ (plus_plus_int @ one_one_int @ (semiri1621563631at_int @ n)) @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))))) | ~spl0_13),
% 0.22/0.32 inference(avatar_component_clause,[],[f488])).
% 0.22/0.32 thf(f491,plain,(
% 0.22/0.32 spl0_13),
% 0.22/0.32 inference(avatar_split_clause,[],[f349,f488])).
% 0.22/0.32 thf(f528,definition,(
% 0.22/0.32 spl0_21 <=> (((ord_less_int @ pls @ zero_zero_int)) = $true)),
% 0.22/0.32 introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition])).
% 0.22/0.32 thf(f531,plain,(
% 0.22/0.32 ~spl0_21),
% 0.22/0.32 inference(avatar_split_clause,[],[f353,f528])).
% 0.22/0.32 thf(f543,definition,(
% 0.22/0.32 spl0_24 <=> (zero_zero_int = pls)),
% 0.22/0.32 introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition])).
% 0.22/0.32 thf(f545,plain,(
% 0.22/0.32 (zero_zero_int = pls) | ~spl0_24),
% 0.22/0.32 inference(avatar_component_clause,[],[f543])).
% 0.22/0.32 thf(f546,plain,(
% 0.22/0.32 spl0_24),
% 0.22/0.32 inference(avatar_split_clause,[],[f260,f543])).
% 0.22/0.32 thf(f677,plain,(
% 0.22/0.32 ( ! [X0 : int,X1 : int] : ((pls != ((power_power_int @ X1 @ (number_number_of_nat @ X0)))) | (zero_zero_int = X1)) ) | ~spl0_24),
% 0.22/0.32 inference(forward_demodulation,[],[f305,f545])).
% 0.22/0.32 thf(f678,plain,(
% 0.22/0.32 ( ! [X0 : int,X1 : int] : ((pls != ((power_power_int @ X1 @ (number_number_of_nat @ X0)))) | (pls = X1)) ) | ~spl0_24),
% 0.22/0.32 inference(forward_demodulation,[],[f677,f545])).
% 0.22/0.32 thf(f684,plain,(
% 0.22/0.32 (zero_zero_int != pls) | (((plus_plus_int @ one_one_int @ (semiri1621563631at_int @ n))) = pls) | (~spl0_13 | ~spl0_24)),
% 0.22/0.32 inference(superposition,[],[f678,f490])).
% 0.22/0.32 thf(f687,plain,(
% 0.22/0.32 (((plus_plus_int @ one_one_int @ (semiri1621563631at_int @ n))) = pls) | (~spl0_13 | ~spl0_24)),
% 0.22/0.32 inference(forward_subsumption_resolution,[],[f684,f545])).
% 0.22/0.32 thf(f689,definition,(
% 0.22/0.32 spl0_40 <=> (pls = ((plus_plus_int @ (number_number_of_int @ (bit1 @ pls)) @ (semiri1621563631at_int @ n))))),
% 0.22/0.32 introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition])).
% 0.22/0.32 thf(f693,plain,(
% 0.22/0.32 (pls = ((plus_plus_int @ (number_number_of_int @ (bit1 @ pls)) @ (semiri1621563631at_int @ n)))) | (~spl0_8 | ~spl0_13 | ~spl0_24)),
% 0.22/0.32 inference(forward_demodulation,[],[f687,f465])).
% 0.22/0.32 thf(f694,plain,(
% 0.22/0.32 spl0_40 | ~spl0_8 | ~spl0_13 | ~spl0_24),
% 0.22/0.32 inference(avatar_split_clause,[],[f693,f543,f488,f463,f689])).
% 0.22/0.32 thf(f698,definition,(
% 0.22/0.32 (one_one_int != ((number_number_of_int @ (bit1 @ pls)))) | (pls != ((plus_plus_int @ (number_number_of_int @ (bit1 @ pls)) @ (semiri1621563631at_int @ n)))) | (zero_zero_int != pls) | (zero_zero_int != ((power_power_int @ zero_zero_int @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))))) | (((ord_less_int @ zero_zero_int @ (plus_plus_int @ one_one_int @ (semiri1621563631at_int @ n)))) != $true) | (((ord_less_int @ pls @ zero_zero_int)) = $true)),
% 0.22/0.32 introduced(theory,[theory_tautology_sat_conflict])).
% 0.22/0.32 cnf(s8, plain, spl0_8, inference(sat_conversion,[],[f466])).
% 0.22/0.32 cnf(s10, plain, spl0_10, inference(sat_conversion,[],[f476])).
% 0.22/0.32 cnf(s11, plain, spl0_11, inference(sat_conversion,[],[f481])).
% 0.22/0.32 cnf(s14, plain, spl0_13, inference(sat_conversion,[],[f491])).
% 0.22/0.32 cnf(s25, plain, ~spl0_21, inference(sat_conversion,[],[f531])).
% 0.22/0.32 cnf(s33, plain, spl0_24, inference(sat_conversion,[],[f546])).
% 0.22/0.32 cnf(s56, plain, ~spl0_8 | ~spl0_13 | ~spl0_24 | spl0_40, inference(sat_conversion,[],[f694])).
% 0.22/0.32 cnf(s60, plain, ~spl0_8 | ~spl0_10 | ~spl0_11 | spl0_21 | ~spl0_24 | ~spl0_40, inference(sat_conversion,[],[f698])).
% 0.22/0.32 cnf(s62, plain, ~spl0_40, inference(rat,[],[s60,s10,s33,s25,s11,s8])).
% 0.22/0.32 cnf(s63, plain, $false, inference(rat,[],[s56,s14,s33,s62,s8])).
% 0.22/0.32 thf(f699,plain,(
% 0.22/0.32 $false),
% 0.22/0.32 inference(avatar_sat_refutation,[],[s63])).
% 0.22/0.32 % SZS output end Proof for theBenchmark
% 0.22/0.32 % (3327941)------------------------------
% 0.22/0.32 % (3327941)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.32 % (3327941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.32 % (3327941)CaDiCaL version: 2.1.3
% 0.22/0.32 % (3327941)Termination reason: Refutation
% 0.22/0.32 % (3327941)Time elapsed: 0.019 s
% 0.22/0.32 % (3327941)Peak memory usage: 13 MB
% 0.22/0.32 % (3327941)Instructions burned: 34 (million)
% 0.22/0.32 % (3327917)Success in time 0.063 s
% 0.22/0.32 % Vampire exiting
%------------------------------------------------------------------------------