%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYO020^1 : TPTP v9.3.1. Released v3.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n019.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:46:18 AM UTC 2026
% Result : Theorem 0.22s 0.29s
% Output : Refutation 0.22s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO020^1 : TPTP v9.3.1. Released v3.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.18 % Computer : n019.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 16:23:26 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 Running higher-order theorem proving
% 0.09/0.23 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.22/0.29 % (996759)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.22/0.29 % (996778)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3760276546:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.22/0.29 % (996778)Refutation not found, incomplete strategy
% 0.22/0.29 % (996778)------------------------------
% 0.22/0.29 % (996778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.29 % (996778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.29 % (996778)CaDiCaL version: 2.1.3
% 0.22/0.29 % (996778)Termination reason: Refutation not found, incomplete strategy
% 0.22/0.29 % (996778)Time elapsed: 0.001 s
% 0.22/0.29 % (996778)Peak memory usage: 12 MB
% 0.22/0.29 % (996778)Instructions burned: 1 (million)
% 0.22/0.29 % (996778)------------------------------
% 0.22/0.29 % (996778)------------------------------
% 0.22/0.29 % (996784)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.29 % (996784)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.29 % (996779)lrs+10_16_si=on:nwc=1.5:random_seed=277014266:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.22/0.29 % (996780)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=2914122008:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.22/0.29 % (996783)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=3367153281:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.22/0.29 % (996782)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=2372455987:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.22/0.29 % (996781)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=4131689956: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.29 % (996784)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=621522781:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.22/0.29 % (996780)Refutation not found, incomplete strategy
% 0.22/0.29 % (996780)------------------------------
% 0.22/0.29 % (996780)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.29 % (996780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.29 % (996780)CaDiCaL version: 2.1.3
% 0.22/0.29 % (996780)Termination reason: Refutation not found, incomplete strategy
% 0.22/0.29 % (996780)Time elapsed: 0.001 s
% 0.22/0.29 % (996780)Peak memory usage: 12 MB
% 0.22/0.29 % (996779)Refutation not found, incomplete strategy
% 0.22/0.29 % (996779)------------------------------
% 0.22/0.29 % (996779)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.29 % (996779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.29 % (996779)CaDiCaL version: 2.1.3
% 0.22/0.29 % (996779)Termination reason: Refutation not found, incomplete strategy
% 0.22/0.29 % (996779)Time elapsed: 0.001 s
% 0.22/0.29 % (996779)Peak memory usage: 12 MB
% 0.22/0.29 % (996779)Instructions burned: 1 (million)
% 0.22/0.29 % (996780)------------------------------
% 0.22/0.29 % (996780)------------------------------
% 0.22/0.29 % (996779)------------------------------
% 0.22/0.29 % (996779)------------------------------
% 0.22/0.29 % (996783) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-996759-996783"...
% 0.22/0.29 % (996781) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-996759-996781"...
% 0.22/0.29 % (996790)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=1190900499:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.22/0.29 % (996784) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-996759-996784"...
% 0.22/0.29 % (996790)Instruction limit reached!
% 0.22/0.29 % (996790)------------------------------
% 0.22/0.29 % (996790)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.29 % (996790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.29 % (996783)...printing done.
% 0.22/0.29 % (996790)CaDiCaL version: 2.1.3
% 0.22/0.29 % (996790)Termination reason: Instruction limit
% 0.22/0.29 % (996790)Termination phase: Saturation
% 0.22/0.29 % (996790)Time elapsed: 0.001 s
% 0.22/0.29 % (996790)Peak memory usage: 12 MB
% 0.22/0.29 % (996790)Instructions burned: 2 (million)
% 0.22/0.29 % (996781)...printing done.
% 0.22/0.29 % (996783)Refutation found. Thanks to Tanya!
% 0.22/0.29 % SZS status Theorem for theBenchmark
% 0.22/0.29 % SZS output start Proof for theBenchmark
% 0.22/0.29 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 0.22/0.29 thf(func_def_0, type, leibeq: ($o > $o > $o)).
% 0.22/0.29 thf(func_def_2, type, vAND: ($o > $o > $o)).
% 0.22/0.29 thf(func_def_3, type, vNOT: ($o > $o)).
% 0.22/0.29 thf(func_def_4, type, vOR: ($o > $o > $o)).
% 0.22/0.29 thf(func_def_7, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 0.22/0.29 thf(func_def_8, type, vIMP: ($o > $o > $o)).
% 0.22/0.29 thf(func_def_9, type, db0: !>[X0: $tType]:(X0)).
% 0.22/0.29 thf(func_def_10, type, db2: !>[X0: $tType]:(X0)).
% 0.22/0.29 thf(func_def_11, type, db1: !>[X0: $tType]:(X0)).
% 0.22/0.29 thf(func_def_12, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 0.22/0.29 thf(func_def_13, type, sK0: $o).
% 0.22/0.29 thf(func_def_14, type, sK1: $o).
% 0.22/0.29 thf(func_def_15, type, sK2: ($o > $o)).
% 0.22/0.29 thf(f1,axiom,(
% 0.22/0.29 (leibeq = (^[X0 : $o, X1 : $o] : (! [X2 : ($o > $o)] : ((X2 @ X0) => (X2 @ X1)))))),
% 0.22/0.29 file('/export/starexec/sandbox/benchmark/theBenchmark.p',leibeq)).
% 0.22/0.29 thf(f2,conjecture,(
% 0.22/0.29 ! [X0 : $o,X1 : $o] : (leibeq @ X0 & X1 @ ~(~X1 | ~X0))),
% 0.22/0.29 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj)).
% 0.22/0.29 thf(f3,negated_conjecture,(
% 0.22/0.29 ~ ! [X0 : $o,X1 : $o] : (leibeq @ X0 & X1 @ ~(~X1 | ~X0))),
% 0.22/0.29 inference(negated_conjecture,[status(cth)],[f2])).
% 0.22/0.29 thf(f4,plain,(
% 0.22/0.29 ~ ! [X0 : $o,X1 : $o] : (leibeq @ X0 & X1 @ ~(~X1 | ~X0))),
% 0.22/0.29 inference(rectify,[],[f3])).
% 0.22/0.29 thf(f5,plain,(
% 0.22/0.29 ~ ! [X0 : $o,X1 : $o] : ($true = ((leibeq @ (X1 & X0) @ (~ ((~ X0) | (~ X1))))))),
% 0.22/0.29 inference(fool_elimination,[],[f4])).
% 0.22/0.29 thf(f6,plain,(
% 0.22/0.29 (leibeq = (^[X0 : $o, X1 : $o] : (! [X2 : ($o > $o)] : ((X2 @ X0) => (X2 @ X1)))))),
% 0.22/0.29 inference(rectify,[],[f1])).
% 0.22/0.29 thf(f7,plain,(
% 0.22/0.29 (leibeq = (^[Y0 : $o]: ((^[Y1 : $o]: (!! @ ($o > $o) @ (^[Y2 : $o > $o]: ((Y2 @ Y0) => (Y2 @ Y1))))))))),
% 0.22/0.29 inference(fool_elimination,[],[f6])).
% 0.22/0.29 thf(f8,plain,(
% 0.22/0.29 ? [X1 : $o,X0 : $o] : ($true != ((leibeq @ (X1 & X0) @ (~ ((~ X0) | (~ X1))))))),
% 0.22/0.29 inference(ennf_transformation,[],[f5])).
% 0.22/0.29 thf(f9,plain,(
% 0.22/0.29 ? [X0 : $o,X1 : $o] : ($true != ((leibeq @ (X0 & X1) @ (~ ((~ X1) | (~ X0))))))),
% 0.22/0.29 inference(rectify,[],[f8])).
% 0.22/0.29 thf(f10,plain,(
% 0.22/0.29 (((leibeq @ (sK0 & sK1) @ (~ ((~ sK1) | (~ sK0))))) != $true)),
% 0.22/0.29 inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(X1,sK1)],[f9])).
% 0.22/0.29 thf(f11,plain,(
% 0.22/0.29 (((leibeq @ (sK0 & sK1) @ (~ ((~ sK1) | (~ sK0))))) != $true)),
% 0.22/0.29 inference(cnf_transformation,[],[f10])).
% 0.22/0.29 thf(f12,plain,(
% 0.22/0.29 (leibeq = (^[Y0 : $o]: ((^[Y1 : $o]: (!! @ ($o > $o) @ (^[Y2 : $o > $o]: ((Y2 @ Y0) => (Y2 @ Y1))))))))),
% 0.22/0.29 inference(cnf_transformation,[],[f7])).
% 0.22/0.29 thf(f14,definition,(
% 0.22/0.29 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 0.22/0.29 introduced(theory,[fool_exhaustiveness_axiom])).
% 0.22/0.29 thf(f15,plain,(
% 0.22/0.29 ((((^[Y0 : $o]: ((^[Y1 : $o]: (!! @ ($o > $o) @ (^[Y2 : $o > $o]: ((Y2 @ Y0) => (Y2 @ Y1))))))) @ (sK0 & sK1) @ (~ ((~ sK1) | (~ sK0))))) != $true)),
% 0.22/0.29 inference(definition_unfolding,[],[f11,f12])).
% 0.22/0.29 thf(f16,plain,(
% 0.22/0.29 ($true != ((!! @ ($o > $o) @ (^[Y0 : $o > $o]: ((Y0 @ (sK0 & sK1)) => (Y0 @ (~ ((~ sK1) | (~ sK0)))))))))),
% 0.22/0.29 inference(beta-eta_normalization,[],[f15])).
% 0.22/0.29 thf(f17,plain,(
% 0.22/0.29 ((((^[Y0 : $o > $o]: ((Y0 @ (sK0 & sK1)) => (Y0 @ (~ ((~ sK1) | (~ sK0)))))) @ sK2)) = $false)),
% 0.22/0.29 inference(sigma_proxy_clausification,[],[f16])).
% 0.22/0.29 thf(f18,plain,(
% 0.22/0.29 ((((sK2 @ (sK0 & sK1)) => (sK2 @ (~ ((~ sK1) | (~ sK0)))))) = $false)),
% 0.22/0.29 inference(beta-eta_normalization,[],[f17])).
% 0.22/0.29 thf(f19,plain,(
% 0.22/0.29 (((sK2 @ (~ ((~ sK1) | (~ sK0))))) = $false)),
% 0.22/0.29 inference(imp_proxy_clausification,[],[f18])).
% 0.22/0.29 thf(f20,plain,(
% 0.22/0.29 (((sK2 @ (sK0 & sK1))) = $true)),
% 0.22/0.29 inference(imp_proxy_clausification,[],[f18])).
% 0.22/0.29 thf(f24,plain,(
% 0.22/0.29 ((((~ sK1) | (~ sK0))) = $false) | (((sK2 @ (~ $true))) = $false)),
% 0.22/0.29 inference(constrained_superposition,[],[f19,f14])).
% 0.22/0.29 thf(f31,plain,(
% 0.22/0.29 (sK1 = $false) | (((sK2 @ (~ ((~ $true) | (~ sK0))))) = $false)),
% 0.22/0.29 inference(constrained_superposition,[],[f19,f14])).
% 0.22/0.29 thf(f32,plain,(
% 0.22/0.29 (sK1 = $false) | ($true = ((sK2 @ (sK0 & $true))))),
% 0.22/0.29 inference(constrained_superposition,[],[f20,f14])).
% 0.22/0.29 thf(f46,plain,(
% 0.22/0.29 (((sK2 @ (~ $true))) = $false) | (((~ sK1)) = $false)),
% 0.22/0.29 inference(or_proxy_clausification,[],[f24])).
% 0.22/0.29 thf(f47,plain,(
% 0.22/0.29 (((sK2 @ (~ $true))) = $false) | ($true = sK1)),
% 0.22/0.29 inference(not_proxy_clausification,[],[f46])).
% 0.22/0.29 thf(f48,plain,(
% 0.22/0.29 ($true = sK1) | (((sK2 @ $false)) = $false)),
% 0.22/0.29 inference(boolean_simplification,[],[f47])).
% 0.22/0.29 thf(f54,plain,(
% 0.22/0.29 (((sK2 @ (~ ($false | (~ sK0))))) = $false) | (sK1 = $false)),
% 0.22/0.29 inference(boolean_simplification,[],[f31])).
% 0.22/0.29 thf(f55,plain,(
% 0.22/0.29 (sK1 = $false) | (((sK2 @ (~ (~ sK0)))) = $false)),
% 0.22/0.29 inference(boolean_simplification,[],[f54])).
% 0.22/0.29 thf(f56,plain,(
% 0.22/0.29 (((sK2 @ sK0)) = $false) | (sK1 = $false)),
% 0.22/0.29 inference(boolean_simplification,[],[f55])).
% 0.22/0.29 thf(f63,plain,(
% 0.22/0.29 (((sK2 @ sK0)) = $true) | (sK1 = $false)),
% 0.22/0.29 inference(boolean_simplification,[],[f32])).
% 0.22/0.29 thf(f65,definition,(
% 0.22/0.29 spl3_1 <=> (((sK2 @ $false)) = $false)),
% 0.22/0.29 introduced(definition,[new_symbols(definition,[spl3_1])],[avatar_definition])).
% 0.22/0.29 thf(f66,plain,(
% 0.22/0.29 (((sK2 @ $false)) = $false) | ~spl3_1),
% 0.22/0.29 inference(avatar_component_clause,[],[f65])).
% 0.22/0.29 thf(f68,definition,(
% 0.22/0.29 spl3_2 <=> ($true = sK1)),
% 0.22/0.29 introduced(definition,[new_symbols(definition,[spl3_2])],[avatar_definition])).
% 0.22/0.29 thf(f69,plain,(
% 0.22/0.29 ($true = sK1) | ~spl3_2),
% 0.22/0.29 inference(avatar_component_clause,[],[f68])).
% 0.22/0.29 thf(f75,definition,(
% 0.22/0.29 spl3_4 <=> (sK1 = $false)),
% 0.22/0.29 introduced(definition,[new_symbols(definition,[spl3_4])],[avatar_definition])).
% 0.22/0.29 thf(f76,plain,(
% 0.22/0.29 (sK1 = $false) | ~spl3_4),
% 0.22/0.29 inference(avatar_component_clause,[],[f75])).
% 0.22/0.29 thf(f81,plain,(
% 0.22/0.29 spl3_1 | spl3_2),
% 0.22/0.29 inference(avatar_split_clause,[],[f48,f68,f65])).
% 0.22/0.29 thf(f88,definition,(
% 0.22/0.29 spl3_7 <=> (((sK2 @ sK0)) = $false)),
% 0.22/0.29 introduced(definition,[new_symbols(definition,[spl3_7])],[avatar_definition])).
% 0.22/0.29 thf(f89,plain,(
% 0.22/0.29 (((sK2 @ sK0)) = $false) | ~spl3_7),
% 0.22/0.29 inference(avatar_component_clause,[],[f88])).
% 0.22/0.29 thf(f90,plain,(
% 0.22/0.29 spl3_4 | spl3_7),
% 0.22/0.29 inference(avatar_split_clause,[],[f56,f88,f75])).
% 0.22/0.29 thf(f104,definition,(
% 0.22/0.29 spl3_11 <=> (((sK2 @ sK0)) = $true)),
% 0.22/0.29 introduced(definition,[new_symbols(definition,[spl3_11])],[avatar_definition])).
% 0.22/0.29 thf(f105,plain,(
% 0.22/0.29 (((sK2 @ sK0)) = $true) | ~spl3_11),
% 0.22/0.29 inference(avatar_component_clause,[],[f104])).
% 0.22/0.29 thf(f106,plain,(
% 0.22/0.29 spl3_11 | spl3_4),
% 0.22/0.29 inference(avatar_split_clause,[],[f63,f75,f104])).
% 0.22/0.29 thf(f107,plain,(
% 0.22/0.29 (((sK2 @ (~ ((~ $false) | (~ sK0))))) = $false) | ~spl3_4),
% 0.22/0.29 inference(backward_demodulation,[],[f19,f76])).
% 0.22/0.29 thf(f110,plain,(
% 0.22/0.29 (((sK2 @ (~ ($true | (~ sK0))))) = $false) | ~spl3_4),
% 0.22/0.29 inference(boolean_simplification,[],[f107])).
% 0.22/0.29 thf(f111,plain,(
% 0.22/0.29 (((sK2 @ (~ $true))) = $false) | ~spl3_4),
% 0.22/0.29 inference(boolean_simplification,[],[f110])).
% 0.22/0.29 thf(f112,plain,(
% 0.22/0.29 (((sK2 @ $false)) = $false) | ~spl3_4),
% 0.22/0.29 inference(boolean_simplification,[],[f111])).
% 0.22/0.29 thf(f119,plain,(
% 0.22/0.29 spl3_1 | ~spl3_4),
% 0.22/0.29 inference(avatar_split_clause,[],[f112,f75,f65])).
% 0.22/0.29 thf(f134,plain,(
% 0.22/0.29 ($true = ((sK2 @ (sK0 & $true)))) | ~spl3_2),
% 0.22/0.29 inference(forward_demodulation,[],[f20,f69])).
% 0.22/0.29 thf(f135,plain,(
% 0.22/0.29 (((sK2 @ sK0)) = $true) | ~spl3_2),
% 0.22/0.29 inference(boolean_simplification,[],[f134])).
% 0.22/0.29 thf(f141,plain,(
% 0.22/0.29 ($true = $false) | (~spl3_7 | ~spl3_11)),
% 0.22/0.29 inference(forward_demodulation,[],[f105,f89])).
% 0.22/0.29 thf(f142,plain,(
% 0.22/0.29 $false | (~spl3_7 | ~spl3_11)),
% 0.22/0.29 inference(trivial_inequality_removal,[],[f141])).
% 0.22/0.29 thf(f143,plain,(
% 0.22/0.29 ~spl3_7 | ~spl3_11),
% 0.22/0.29 inference(avatar_contradiction_clause,[],[f142])).
% 0.22/0.29 thf(f148,plain,(
% 0.22/0.29 ($true = $false) | (~spl3_2 | ~spl3_7)),
% 0.22/0.29 inference(forward_demodulation,[],[f135,f89])).
% 0.22/0.29 thf(f149,plain,(
% 0.22/0.29 $false | (~spl3_2 | ~spl3_7)),
% 0.22/0.29 inference(trivial_inequality_removal,[],[f148])).
% 0.22/0.29 thf(f150,plain,(
% 0.22/0.29 ~spl3_2 | ~spl3_7),
% 0.22/0.29 inference(avatar_contradiction_clause,[],[f149])).
% 0.22/0.29 thf(f155,plain,(
% 0.22/0.29 (((sK2 @ (sK0 & $false))) = $true) | ~spl3_4),
% 0.22/0.29 inference(backward_demodulation,[],[f20,f76])).
% 0.22/0.29 thf(f160,plain,(
% 0.22/0.29 (((sK2 @ $false)) = $true) | ~spl3_4),
% 0.22/0.29 inference(boolean_simplification,[],[f155])).
% 0.22/0.29 thf(f162,plain,(
% 0.22/0.29 ($true = $false) | (~spl3_1 | ~spl3_4)),
% 0.22/0.29 inference(forward_demodulation,[],[f160,f66])).
% 0.22/0.29 thf(f163,plain,(
% 0.22/0.29 $false | (~spl3_1 | ~spl3_4)),
% 0.22/0.29 inference(trivial_inequality_removal,[],[f162])).
% 0.22/0.29 thf(f164,plain,(
% 0.22/0.29 ~spl3_1 | ~spl3_4),
% 0.22/0.29 inference(avatar_contradiction_clause,[],[f163])).
% 0.22/0.29 cnf(s3, plain, spl3_1 | spl3_2, inference(sat_conversion,[],[f81])).
% 0.22/0.29 cnf(s6, plain, spl3_4 | spl3_7, inference(sat_conversion,[],[f90])).
% 0.22/0.29 cnf(s10, plain, spl3_4 | spl3_11, inference(sat_conversion,[],[f106])).
% 0.22/0.29 cnf(s13, plain, spl3_1 | ~spl3_4, inference(sat_conversion,[],[f119])).
% 0.22/0.29 cnf(s16, plain, ~spl3_7 | ~spl3_11, inference(sat_conversion,[],[f143])).
% 0.22/0.29 cnf(s18, plain, ~spl3_2 | ~spl3_7, inference(sat_conversion,[],[f150])).
% 0.22/0.29 cnf(s20, plain, ~spl3_1 | ~spl3_4, inference(sat_conversion,[],[f164])).
% 0.22/0.29 cnf(s22, plain, spl3_1, inference(rat,[],[s18,s6,s3,s13])).
% 0.22/0.29 cnf(s23, plain, ~spl3_4, inference(rat,[],[s20,s22])).
% 0.22/0.29 cnf(s25, plain, spl3_11, inference(rat,[],[s10,s23])).
% 0.22/0.29 cnf(s26, plain, spl3_7, inference(rat,[],[s6,s23])).
% 0.22/0.29 cnf(s31, plain, $false, inference(rat,[],[s16,s25,s26])).
% 0.22/0.29 thf(f168,plain,(
% 0.22/0.29 $false),
% 0.22/0.29 inference(avatar_sat_refutation,[],[s31])).
% 0.22/0.29 % SZS output end Proof for theBenchmark
% 0.22/0.29 % (996783)------------------------------
% 0.22/0.29 % (996783)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.29 % (996783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.29 % (996783)CaDiCaL version: 2.1.3
% 0.22/0.29 % (996783)Termination reason: Refutation
% 0.22/0.29 % (996783)Time elapsed: 0.005 s
% 0.22/0.29 % (996783)Peak memory usage: 13 MB
% 0.22/0.29 % (996783)Instructions burned: 6 (million)
% 0.22/0.29 % (996759)Success in time 0.046 s
% 0.22/0.29 % Vampire exiting
%------------------------------------------------------------------------------