%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEV434_8 : TPTP v9.3.1. Released v8.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n005.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 : Tue Sep 29 12:59:16 PM UTC 2026
% Result : Theorem 0.20s 0.50s
% Output : Refutation 0.20s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV434_8 : TPTP v9.3.1. Released v8.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.13/0.41 % Computer : n005.cluster.edu
% 0.13/0.41 % Model : x86_64 x86_64
% 0.13/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.41 % Memory : 8046.5625MB
% 0.13/0.41 % OS : Linux 6.8.0-71-generic
% 0.13/0.41 % CPULimit : 300
% 0.13/0.41 % WCLimit : 300
% 0.13/0.41 % DateTime : Mon Sep 28 06:27:02 UTC 2026
% 0.13/0.41 % CPUTime :
% 0.13/0.41 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.13/0.45 Running first-order model finding
% 0.13/0.45 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.50 % (589982)Will run a generic schedule for satisfiability detection.
% 0.20/0.50 % (589992)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2376945138:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.20/0.50 % (589992) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-589982-589992"...
% 0.20/0.50 % (589992)...printing done.
% 0.20/0.50 % (589992)Refutation found. Thanks to Tanya!
% 0.20/0.50 % SZS status Theorem for theBenchmark
% 0.20/0.50 % SZS output start Proof for theBenchmark
% 0.20/0.50 tff(func_def_0, type, f: $o > $i).
% 0.20/0.50 tff(func_def_3, type, bG0: $o > $o).
% 0.20/0.50 tff(func_def_4, type, sK1: $i > $o).
% 0.20/0.50 tff(f1,axiom,(
% 0.20/0.50 ! [X0 : $i] : ? [X1 : $o] : f(X1) = X0),
% 0.20/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fsurj)).
% 0.20/0.50 tff(f2,conjecture,(
% 0.20/0.50 ! [X0 : $i,X1 : $i,X2 : $i] : (X0 = X1 | X0 = X2 | X1 = X2)),
% 0.20/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',less3)).
% 0.20/0.50 tff(f3,negated_conjecture,(
% 0.20/0.50 ~ ! [X0 : $i,X1 : $i,X2 : $i] : (X0 = X1 | X0 = X2 | X1 = X2)),
% 0.20/0.50 inference(negated_conjecture,[status(cth)],[f2])).
% 0.20/0.50 tff(f4,plain,(
% 0.20/0.50 ! [X0 : $i] : ? [X1 : $o] : f(X1) = X0),
% 0.20/0.50 inference(rectify,[],[f1])).
% 0.20/0.50 tff(f5,definition,(
% 0.20/0.50 ! [X1 : $o] : (($true = X1) <=> ($true = bG0(X1)))),
% 0.20/0.50 introduced(definition,[new_symbols(definition,[bG0])],[fool_formula_definition])).
% 0.20/0.50 tff(f6,plain,(
% 0.20/0.50 ! [X0 : $i] : ? [X1 : $o] : f(bG0(X1)) = X0),
% 0.20/0.50 inference(fool_elimination,[],[f4,f5])).
% 0.20/0.50 tff(f7,plain,(
% 0.20/0.50 ! [X0 : $o] : (($true = X0) <=> ($true = bG0(X0)))),
% 0.20/0.50 inference(rectify,[],[f5])).
% 0.20/0.50 tff(f8,plain,(
% 0.20/0.50 ? [X0 : $i,X1 : $i,X2 : $i] : (X0 != X1 & X0 != X2 & X1 != X2)),
% 0.20/0.50 inference(ennf_transformation,[],[f3])).
% 0.20/0.50 tff(f9,plain,(
% 0.20/0.50 ! [X0 : $o] : ((($true = X0) | ($true != bG0(X0))) & (($true = bG0(X0)) | ($true != X0)))),
% 0.20/0.50 inference(nnf_transformation,[],[f7])).
% 0.20/0.50 tff(f10,plain,(
% 0.20/0.50 ! [X0 : $i] : f(bG0(sK1(X0))) = X0),
% 0.20/0.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X1,sK1(X0))],[f6])).
% 0.20/0.50 tff(f11,plain,(
% 0.20/0.50 sK2 != sK3 & sK2 != sK4 & sK3 != sK4),
% 0.20/0.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4]),skolemize(X0,sK2),skolemize(X1,sK3),skolemize(X2,sK4)],[f8])).
% 0.20/0.50 tff(f12,plain,(
% 0.20/0.50 ( ! [X0 : $o] : (($true != X0) | ($true = bG0(X0))) )),
% 0.20/0.50 inference(cnf_transformation,[],[f9])).
% 0.20/0.50 tff(f13,plain,(
% 0.20/0.50 ( ! [X0 : $o] : (($true != bG0(X0)) | ($true = X0)) )),
% 0.20/0.50 inference(cnf_transformation,[],[f9])).
% 0.20/0.50 tff(f14,plain,(
% 0.20/0.50 ( ! [X0 : $i] : (f(bG0(sK1(X0))) = X0) )),
% 0.20/0.50 inference(cnf_transformation,[],[f10])).
% 0.20/0.50 tff(f15,plain,(
% 0.20/0.50 sK3 != sK4),
% 0.20/0.50 inference(cnf_transformation,[],[f11])).
% 0.20/0.50 tff(f16,plain,(
% 0.20/0.50 sK2 != sK4),
% 0.20/0.50 inference(cnf_transformation,[],[f11])).
% 0.20/0.50 tff(f17,plain,(
% 0.20/0.50 sK2 != sK3),
% 0.20/0.50 inference(cnf_transformation,[],[f11])).
% 0.20/0.50 tff(f19,definition,(
% 0.20/0.50 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 0.20/0.50 introduced(theory,[fool_exhaustiveness_axiom])).
% 0.20/0.50 tff(f22,plain,(
% 0.20/0.50 ( ! [X0 : $i] : ((sK1(X0) = $false) | f(bG0($true)) = X0) )),
% 0.20/0.50 inference(superposition,[],[f14,f19])).
% 0.20/0.50 tff(f23,plain,(
% 0.20/0.50 ( ! [X0 : $i] : ((bG0(sK1(X0)) = $false) | f($true) = X0) )),
% 0.20/0.50 inference(superposition,[],[f14,f19])).
% 0.20/0.50 tff(f26,plain,(
% 0.20/0.50 ($true = bG0($true))),
% 0.20/0.50 inference(equality_resolution,[],[f12])).
% 0.20/0.50 tff(f27,plain,(
% 0.20/0.50 ( ! [X0 : $o] : (($true != $true) | ($true = X0) | (bG0(X0) = $false)) )),
% 0.20/0.50 inference(superposition,[],[f13,f19])).
% 0.20/0.50 tff(f28,plain,(
% 0.20/0.50 ( ! [X0 : $o] : ((bG0(X0) = $false) | ($true = X0)) )),
% 0.20/0.50 inference(trivial_inequality_removal,[],[f27])).
% 0.20/0.50 tff(f31,plain,(
% 0.20/0.50 ( ! [X0 : $i] : (($true = sK1(X0)) | f($false) = X0) )),
% 0.20/0.50 inference(superposition,[],[f14,f28])).
% 0.20/0.50 tff(f119,plain,(
% 0.20/0.50 ( ! [X0 : $i] : (f(bG0($true)) = X0 | f($false) = X0) )),
% 0.20/0.50 inference(superposition,[],[f14,f31])).
% 0.20/0.50 tff(f122,plain,(
% 0.20/0.50 ( ! [X0 : $i] : (f($true) = X0 | f($false) = X0) )),
% 0.20/0.50 inference(forward_demodulation,[],[f119,f26])).
% 0.20/0.50 tff(f128,plain,(
% 0.20/0.50 ( ! [X0 : $i] : (f(bG0($false)) = X0 | f(bG0($true)) = X0) )),
% 0.20/0.50 inference(superposition,[],[f14,f22])).
% 0.20/0.50 tff(f134,plain,(
% 0.20/0.50 ( ! [X0 : $i] : (f(bG0($false)) = X0 | f($true) = X0) )),
% 0.20/0.50 inference(forward_demodulation,[],[f128,f26])).
% 0.20/0.50 tff(f143,plain,(
% 0.20/0.50 sK2 != f($true) | sK4 = f($false)),
% 0.20/0.50 inference(superposition,[],[f16,f122])).
% 0.20/0.50 tff(f144,plain,(
% 0.20/0.50 sK3 != f($true) | sK4 = f($false)),
% 0.20/0.50 inference(superposition,[],[f15,f122])).
% 0.20/0.50 tff(f145,plain,(
% 0.20/0.50 sK2 != f($true) | sK3 = f($false)),
% 0.20/0.50 inference(superposition,[],[f17,f122])).
% 0.20/0.50 tff(f147,plain,(
% 0.20/0.50 ( ! [X0 : $i] : (f($true) != f($false) | f($false) = X0) )),
% 0.20/0.50 inference(equality_factoring,[],[f122])).
% 0.20/0.50 tff(f153,definition,(
% 0.20/0.50 spl5_1 <=> ! [X0 : $i] : f($false) = X0),
% 0.20/0.50 introduced(definition,[new_symbols(definition,[spl5_1])],[avatar_definition])).
% 0.20/0.50 tff(f154,plain,(
% 0.20/0.50 ( ! [X0 : $i] : (f($false) = X0) ) | ~spl5_1),
% 0.20/0.50 inference(avatar_component_clause,[],[f153])).
% 0.20/0.50 tff(f156,definition,(
% 0.20/0.50 spl5_2 <=> f($true) = f($false)),
% 0.20/0.50 introduced(definition,[new_symbols(definition,[spl5_2])],[avatar_definition])).
% 0.20/0.50 tff(f158,plain,(
% 0.20/0.50 f($true) != f($false) | spl5_2),
% 0.20/0.50 inference(avatar_component_clause,[],[f156])).
% 0.20/0.50 tff(f159,plain,(
% 0.20/0.50 spl5_1 | ~spl5_2),
% 0.20/0.50 inference(avatar_split_clause,[],[f147,f156,f153])).
% 0.20/0.50 tff(f162,definition,(
% 0.20/0.50 spl5_3 <=> sK3 = f($false)),
% 0.20/0.50 introduced(definition,[new_symbols(definition,[spl5_3])],[avatar_definition])).
% 0.20/0.50 tff(f164,plain,(
% 0.20/0.50 sK3 = f($false) | ~spl5_3),
% 0.20/0.50 inference(avatar_component_clause,[],[f162])).
% 0.20/0.50 tff(f166,definition,(
% 0.20/0.50 spl5_4 <=> sK2 = f($true)),
% 0.20/0.50 introduced(definition,[new_symbols(definition,[spl5_4])],[avatar_definition])).
% 0.20/0.50 tff(f168,plain,(
% 0.20/0.50 sK2 != f($true) | spl5_4),
% 0.20/0.50 inference(avatar_component_clause,[],[f166])).
% 0.20/0.50 tff(f169,plain,(
% 0.20/0.50 spl5_3 | ~spl5_4),
% 0.20/0.50 inference(avatar_split_clause,[],[f145,f166,f162])).
% 0.20/0.50 tff(f171,definition,(
% 0.20/0.50 spl5_5 <=> sK4 = f($false)),
% 0.20/0.50 introduced(definition,[new_symbols(definition,[spl5_5])],[avatar_definition])).
% 0.20/0.50 tff(f173,plain,(
% 0.20/0.50 sK4 = f($false) | ~spl5_5),
% 0.20/0.50 inference(avatar_component_clause,[],[f171])).
% 0.20/0.50 tff(f175,definition,(
% 0.20/0.50 spl5_6 <=> sK3 = f($true)),
% 0.20/0.50 introduced(definition,[new_symbols(definition,[spl5_6])],[avatar_definition])).
% 0.20/0.50 tff(f177,plain,(
% 0.20/0.50 sK3 != f($true) | spl5_6),
% 0.20/0.50 inference(avatar_component_clause,[],[f175])).
% 0.20/0.50 tff(f178,plain,(
% 0.20/0.50 spl5_5 | ~spl5_6),
% 0.20/0.50 inference(avatar_split_clause,[],[f144,f175,f171])).
% 0.20/0.50 tff(f179,plain,(
% 0.20/0.50 spl5_5 | ~spl5_4),
% 0.20/0.50 inference(avatar_split_clause,[],[f143,f166,f171])).
% 0.20/0.50 tff(f180,plain,(
% 0.20/0.50 ( ! [X0 : $i] : (($false = bG0($false)) | f($true) = X0 | f(bG0($true)) = X0) )),
% 0.20/0.50 inference(superposition,[],[f23,f22])).
% 0.20/0.50 tff(f203,definition,(
% 0.20/0.50 spl5_8 <=> ($false = bG0($false))),
% 0.20/0.50 introduced(definition,[new_symbols(definition,[spl5_8])],[avatar_definition])).
% 0.20/0.50 tff(f205,plain,(
% 0.20/0.50 ($false = bG0($false)) | ~spl5_8),
% 0.20/0.50 inference(avatar_component_clause,[],[f203])).
% 0.20/0.50 tff(f208,plain,(
% 0.20/0.50 ( ! [X0 : $i] : (f($true) = X0 | ($false = bG0($false)) | f($true) = X0) )),
% 0.20/0.50 inference(forward_demodulation,[],[f180,f26])).
% 0.20/0.50 tff(f209,plain,(
% 0.20/0.50 ( ! [X0 : $i] : (f($true) = X0 | ($false = bG0($false))) )),
% 0.20/0.50 inference(duplicate_literal_removal,[],[f208])).
% 0.20/0.50 tff(f211,definition,(
% 0.20/0.50 spl5_9 <=> ! [X0 : $i] : f($true) = X0),
% 0.20/0.50 introduced(definition,[new_symbols(definition,[spl5_9])],[avatar_definition])).
% 0.20/0.50 tff(f212,plain,(
% 0.20/0.50 ( ! [X0 : $i] : (f($true) = X0) ) | ~spl5_9),
% 0.20/0.50 inference(avatar_component_clause,[],[f211])).
% 0.20/0.50 tff(f213,plain,(
% 0.20/0.50 spl5_8 | spl5_9),
% 0.20/0.50 inference(avatar_split_clause,[],[f209,f211,f203])).
% 0.20/0.50 tff(f214,plain,(
% 0.20/0.50 f($true) != f($true) | sK2 = f($false) | spl5_4),
% 0.20/0.50 inference(superposition,[],[f168,f122])).
% 0.20/0.50 tff(f215,plain,(
% 0.20/0.50 sK2 = f($false) | spl5_4),
% 0.20/0.50 inference(trivial_inequality_removal,[],[f214])).
% 0.20/0.50 tff(f217,plain,(
% 0.20/0.50 f($true) != f($true) | sK3 = f($false) | spl5_6),
% 0.20/0.50 inference(superposition,[],[f177,f122])).
% 0.20/0.50 tff(f218,plain,(
% 0.20/0.50 sK3 = f($false) | spl5_6),
% 0.20/0.50 inference(trivial_inequality_removal,[],[f217])).
% 0.20/0.50 tff(f219,plain,(
% 0.20/0.50 spl5_3 | spl5_6),
% 0.20/0.50 inference(avatar_split_clause,[],[f218,f175,f162])).
% 0.20/0.50 tff(f231,plain,(
% 0.20/0.50 sK2 != f($false) | ~spl5_3),
% 0.20/0.50 inference(superposition,[],[f17,f164])).
% 0.20/0.50 tff(f232,plain,(
% 0.20/0.50 $false | (~spl5_3 | spl5_4)),
% 0.20/0.50 inference(forward_subsumption_resolution,[],[f231,f215])).
% 0.20/0.50 tff(f233,plain,(
% 0.20/0.50 ~spl5_3 | spl5_4),
% 0.20/0.50 inference(avatar_contradiction_clause,[],[f232])).
% 0.20/0.50 tff(f246,plain,(
% 0.20/0.50 f($true) != f(bG0($false)) | sK2 = f($true) | spl5_4),
% 0.20/0.50 inference(superposition,[],[f168,f134])).
% 0.20/0.50 tff(f248,plain,(
% 0.20/0.50 sK2 != f(bG0($false)) | sK4 = f($true)),
% 0.20/0.50 inference(superposition,[],[f16,f134])).
% 0.20/0.50 tff(f256,plain,(
% 0.20/0.50 sK2 != f($false) | sK4 = f($true) | ~spl5_8),
% 0.20/0.50 inference(forward_demodulation,[],[f248,f205])).
% 0.20/0.50 tff(f257,plain,(
% 0.20/0.50 f($true) != f(bG0($false)) | spl5_4),
% 0.20/0.50 inference(forward_subsumption_resolution,[],[f246,f168])).
% 0.20/0.50 tff(f259,plain,(
% 0.20/0.50 sK4 = f($true) | (spl5_4 | ~spl5_8)),
% 0.20/0.50 inference(forward_subsumption_resolution,[],[f256,f215])).
% 0.20/0.50 tff(f262,plain,(
% 0.20/0.50 f($true) = f($false) | (spl5_4 | ~spl5_5 | ~spl5_8)),
% 0.20/0.50 inference(forward_demodulation,[],[f259,f173])).
% 0.20/0.50 tff(f263,plain,(
% 0.20/0.50 $false | (spl5_2 | spl5_4 | ~spl5_5 | ~spl5_8)),
% 0.20/0.50 inference(forward_subsumption_resolution,[],[f262,f158])).
% 0.20/0.50 tff(f264,plain,(
% 0.20/0.50 spl5_2 | spl5_4 | ~spl5_5 | ~spl5_8),
% 0.20/0.50 inference(avatar_contradiction_clause,[],[f263])).
% 0.20/0.50 tff(f265,plain,(
% 0.20/0.50 $false | (spl5_4 | ~spl5_9)),
% 0.20/0.50 inference(forward_subsumption_resolution,[],[f257,f212])).
% 0.20/0.50 tff(f266,plain,(
% 0.20/0.50 spl5_4 | ~spl5_9),
% 0.20/0.50 inference(avatar_contradiction_clause,[],[f265])).
% 0.20/0.50 tff(f272,plain,(
% 0.20/0.50 f($true) != f($false) | (~spl5_1 | spl5_4)),
% 0.20/0.50 inference(forward_demodulation,[],[f257,f154])).
% 0.20/0.50 tff(f275,plain,(
% 0.20/0.50 $false | (~spl5_1 | spl5_4)),
% 0.20/0.50 inference(forward_subsumption_resolution,[],[f272,f154])).
% 0.20/0.50 tff(f276,plain,(
% 0.20/0.50 ~spl5_1 | spl5_4),
% 0.20/0.50 inference(avatar_contradiction_clause,[],[f275])).
% 0.20/0.50 tff(f345,plain,(
% 0.20/0.50 sK3 != f($false) | ~spl5_5),
% 0.20/0.50 inference(superposition,[],[f15,f173])).
% 0.20/0.50 tff(f346,plain,(
% 0.20/0.50 $false | (~spl5_3 | ~spl5_5)),
% 0.20/0.50 inference(forward_subsumption_resolution,[],[f345,f164])).
% 0.20/0.50 tff(f347,plain,(
% 0.20/0.50 ~spl5_3 | ~spl5_5),
% 0.20/0.50 inference(avatar_contradiction_clause,[],[f346])).
% 0.20/0.50 cnf(s1, plain, spl5_1 | ~spl5_2, inference(sat_conversion,[],[f159])).
% 0.20/0.50 cnf(s2, plain, spl5_3 | ~spl5_4, inference(sat_conversion,[],[f169])).
% 0.20/0.50 cnf(s3, plain, spl5_5 | ~spl5_6, inference(sat_conversion,[],[f178])).
% 0.20/0.50 cnf(s4, plain, ~spl5_4 | spl5_5, inference(sat_conversion,[],[f179])).
% 0.20/0.50 cnf(s7, plain, spl5_8 | spl5_9, inference(sat_conversion,[],[f213])).
% 0.20/0.50 cnf(s8, plain, spl5_3 | spl5_6, inference(sat_conversion,[],[f219])).
% 0.20/0.50 cnf(s9, plain, ~spl5_3 | spl5_4, inference(sat_conversion,[],[f233])).
% 0.20/0.50 cnf(s10, plain, spl5_2 | spl5_4 | ~spl5_5 | ~spl5_8, inference(sat_conversion,[],[f264])).
% 0.20/0.50 cnf(s11, plain, spl5_4 | ~spl5_9, inference(sat_conversion,[],[f266])).
% 0.20/0.50 cnf(s12, plain, ~spl5_1 | spl5_4, inference(sat_conversion,[],[f276])).
% 0.20/0.50 cnf(s14, plain, ~spl5_3 | ~spl5_5, inference(sat_conversion,[],[f347])).
% 0.20/0.50 cnf(s15, plain, spl5_3 | spl5_2, inference(rat,[],[s7,s10,s11,s3,s2,s8])).
% 0.20/0.50 cnf(s16, plain, ~spl5_3, inference(rat,[],[s4,s9,s14])).
% 0.20/0.50 cnf(s18, plain, ~spl5_4, inference(rat,[],[s2,s16])).
% 0.20/0.50 cnf(s19, plain, spl5_2, inference(rat,[],[s15,s16])).
% 0.20/0.50 cnf(s21, plain, ~spl5_1, inference(rat,[],[s12,s18])).
% 0.20/0.50 cnf(s23, plain, $false, inference(rat,[],[s1,s19,s21])).
% 0.20/0.50 tff(f348,plain,(
% 0.20/0.50 $false),
% 0.20/0.50 inference(avatar_sat_refutation,[],[s23])).
% 0.20/0.50 % SZS output end Proof for theBenchmark
% 0.20/0.50 % (589992)------------------------------
% 0.20/0.50 % (589992)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.50 % (589992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.50 % (589992)CaDiCaL version: 2.1.3
% 0.20/0.50 % (589992)Termination reason: Refutation
% 0.20/0.50 % (589992)Time elapsed: 0.008 s
% 0.20/0.50 % (589992)Peak memory usage: 12 MB
% 0.20/0.50 % (589992)Instructions burned: 12 (million)
% 0.20/0.50 % (589982)Success in time 0.031 s
% 0.20/0.50 % Vampire exiting
%------------------------------------------------------------------------------