%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW579_2 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 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 : Tue Sep 29 01:40:28 PM UTC 2026
% Result : Theorem 0.24s 0.35s
% Output : Refutation 0.24s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWW579_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.24 % Computer : n007.cluster.edu
% 0.09/0.24 % Model : x86_64 x86_64
% 0.09/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.24 % Memory : 8046.5625MB
% 0.09/0.24 % OS : Linux 6.8.0-71-generic
% 0.09/0.24 % CPULimit : 300
% 0.09/0.24 % WCLimit : 300
% 0.09/0.24 % DateTime : Mon Sep 28 14:17:55 UTC 2026
% 0.09/0.25 % CPUTime :
% 0.09/0.25 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.24/0.29 Running first-order model finding
% 0.24/0.29 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.24/0.35 % (2411419)Will run a generic schedule for satisfiability detection.
% 0.24/0.35 % (2411428)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=633009496:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.24/0.35 % (2411424)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2094481371_2999 on theBenchmark for (2999ds/0Mi)
% 0.24/0.35 % (2411424)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 0.24/0.35 % (2411424)Terminated due to inappropriate strategy.
% 0.24/0.35 % (2411424)------------------------------
% 0.24/0.35 % (2411424)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.24/0.35 % (2411424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.24/0.35 % (2411424)CaDiCaL version: 2.1.3
% 0.24/0.35 % (2411424)Termination reason: Inappropriate
% 0.24/0.35 % (2411424)Time elapsed: 0.002 s
% 0.24/0.35 % (2411424)Peak memory usage: 11 MB
% 0.24/0.35 % (2411424)Instructions burned: 2 (million)
% 0.24/0.35 % (2411425)% WARNING: option uhcvi not known.
% 0.24/0.35 % (2411424)------------------------------
% 0.24/0.35 % (2411424)------------------------------
% 0.24/0.35 % (2411426)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1241100075:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.24/0.35 % (2411427)dis+10_1_sil=32000:sp=arity:random_seed=4113545457:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.24/0.35 % (2411429)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1066287878:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.24/0.35 % (2411425)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3209333992:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.24/0.35 % (2411428) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2411419-2411428"...
% 0.24/0.35 % (2411430)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4060718365:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.24/0.35 % (2411428)...printing done.
% 0.24/0.35 % (2411428)Refutation found. Thanks to Tanya!
% 0.24/0.35 % SZS status Theorem for theBenchmark
% 0.24/0.35 % SZS output start Proof for theBenchmark
% 0.24/0.35 tff(type_def_5, type, uni: $tType).
% 0.24/0.35 tff(type_def_6, type, ty: $tType).
% 0.24/0.35 tff(type_def_7, type, bool: $tType).
% 0.24/0.35 tff(type_def_8, type, tuple0: $tType).
% 0.24/0.35 tff(func_def_0, type, witness: ty > uni).
% 0.24/0.35 tff(func_def_1, type, int: ty).
% 0.24/0.35 tff(func_def_2, type, real: ty).
% 0.24/0.35 tff(func_def_3, type, bool1: ty).
% 0.24/0.35 tff(func_def_4, type, true: bool).
% 0.24/0.35 tff(func_def_5, type, false: bool).
% 0.24/0.35 tff(func_def_6, type, match_bool: (ty * bool * uni * uni) > uni).
% 0.24/0.35 tff(func_def_7, type, tuple01: ty).
% 0.24/0.35 tff(func_def_8, type, tuple02: tuple0).
% 0.24/0.35 tff(func_def_9, type, qtmark: ty).
% 0.24/0.35 tff(func_def_18, type, min: ($real * $real) > $real).
% 0.24/0.35 tff(func_def_19, type, max: ($real * $real) > $real).
% 0.24/0.35 tff(func_def_25, type, sK0: $real).
% 0.24/0.35 tff(func_def_26, type, sK1: $real).
% 0.24/0.35 tff(func_def_27, type, sK2: $int).
% 0.24/0.35 tff(func_def_28, type, sK3: $real).
% 0.24/0.35 tff(pred_def_1, type, sort: (ty * uni) > $o).
% 0.24/0.35 tff(f17,axiom,(
% 0.24/0.35 ! [X0 : $real,X1 : $real] : (max(X0,X1) = X0 | max(X0,X1) = X1)),
% 0.24/0.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',max_is_some)).
% 0.24/0.35 tff(f20,conjecture,(
% 0.24/0.35 ! [X0 : $real,X1 : $real,X2 : $int,X3 : $real] : (($lesseq(0/1,X0) & $less(0/1,X3) & $lesseq(1,X2) & X1 = $product($to_real(X2),X3)) => (~($less(X0,X1) & $less(1/1,X1)) => ($lesseq($product($to_real(X2),X3),max(X0,1/1)) => ($less(0/1,$quotient(1/1,X3)) => ($lesseq($product($product($to_real(X2),X3),$quotient(1/1,X3)),$product(max(X0,1/1),$quotient(1/1,X3))) => ($lesseq($quotient($product($to_real(X2),X3),X3),$quotient(max(X0,1/1),X3)) => $lesseq($to_real(X2),$quotient(max(X0,1/1),X3))))))))),
% 0.24/0.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wP_parameter_sqrt)).
% 0.24/0.35 tff(f21,negated_conjecture,(
% 0.24/0.35 ~ ! [X0 : $real,X1 : $real,X2 : $int,X3 : $real] : (($lesseq(0/1,X0) & $less(0/1,X3) & $lesseq(1,X2) & X1 = $product($to_real(X2),X3)) => (~($less(X0,X1) & $less(1/1,X1)) => ($lesseq($product($to_real(X2),X3),max(X0,1/1)) => ($less(0/1,$quotient(1/1,X3)) => ($lesseq($product($product($to_real(X2),X3),$quotient(1/1,X3)),$product(max(X0,1/1),$quotient(1/1,X3))) => ($lesseq($quotient($product($to_real(X2),X3),X3),$quotient(max(X0,1/1),X3)) => $lesseq($to_real(X2),$quotient(max(X0,1/1),X3))))))))),
% 0.24/0.35 inference(negated_conjecture,[status(cth)],[f20])).
% 0.24/0.35 tff(f27,plain,(
% 0.24/0.35 ~ ! [X0 : $real,X1 : $real,X2 : $int,X3 : $real] : ((~$less(X0,0/1) & $less(0/1,X3) & ~$less(X2,1) & X1 = $product($to_real(X2),X3)) => (~($less(X0,X1) & $less(1/1,X1)) => (~$less(max(X0,1/1),$product($to_real(X2),X3)) => ($less(0/1,$quotient(1/1,X3)) => (~$less($product(max(X0,1/1),$quotient(1/1,X3)),$product($product($to_real(X2),X3),$quotient(1/1,X3))) => (~$less($quotient(max(X0,1/1),X3),$quotient($product($to_real(X2),X3),X3)) => ~$less($quotient(max(X0,1/1),X3),$to_real(X2))))))))),
% 0.24/0.35 inference(theory_normalization,[],[f21])).
% 0.24/0.35 tff(f64,definition,(
% 0.24/0.35 ( ! [X2 : $real,X1 : $real] : ($quotient($product(X2,X1),X1) = X2 | 0/1 = X1) )),
% 0.24/0.35 introduced(theory,[tha_quotient_multiply])).
% 0.24/0.35 tff(f79,plain,(
% 0.24/0.35 ? [X0 : $real,X1 : $real,X2 : $int,X3 : $real] : (((((($less($quotient(max(X0,1/1),X3),$to_real(X2)) & ~$less($quotient(max(X0,1/1),X3),$quotient($product($to_real(X2),X3),X3))) & ~$less($product(max(X0,1/1),$quotient(1/1,X3)),$product($product($to_real(X2),X3),$quotient(1/1,X3)))) & $less(0/1,$quotient(1/1,X3))) & ~$less(max(X0,1/1),$product($to_real(X2),X3))) & (~$less(X0,X1) | ~$less(1/1,X1))) & (~$less(X0,0/1) & $less(0/1,X3) & ~$less(X2,1) & X1 = $product($to_real(X2),X3)))),
% 0.24/0.35 inference(ennf_transformation,[],[f27])).
% 0.24/0.35 tff(f80,plain,(
% 0.24/0.35 ? [X0 : $real,X1 : $real,X2 : $int,X3 : $real] : ($less($quotient(max(X0,1/1),X3),$to_real(X2)) & ~$less($quotient(max(X0,1/1),X3),$quotient($product($to_real(X2),X3),X3)) & ~$less($product(max(X0,1/1),$quotient(1/1,X3)),$product($product($to_real(X2),X3),$quotient(1/1,X3))) & $less(0/1,$quotient(1/1,X3)) & ~$less(max(X0,1/1),$product($to_real(X2),X3)) & (~$less(X0,X1) | ~$less(1/1,X1)) & ~$less(X0,0/1) & $less(0/1,X3) & ~$less(X2,1) & X1 = $product($to_real(X2),X3))),
% 0.24/0.35 inference(flattening,[],[f79])).
% 0.24/0.35 tff(f98,plain,(
% 0.24/0.35 ( ! [X0 : $real,X1 : $real] : (max(X0,X1) = X1 | max(X0,X1) = X0) )),
% 0.24/0.35 inference(cnf_transformation,[],[f17])).
% 0.24/0.35 tff(f103,plain,(
% 0.24/0.35 sK1 = $product($to_real(sK2),sK3)),
% 0.24/0.35 inference(cnf_transformation,[],[f80])).
% 0.24/0.35 tff(f105,plain,(
% 0.24/0.35 $less(0/1,sK3)),
% 0.24/0.35 inference(cnf_transformation,[],[f80])).
% 0.24/0.35 tff(f110,plain,(
% 0.24/0.35 ~$less($quotient(max(sK0,1/1),sK3),$quotient($product($to_real(sK2),sK3),sK3))),
% 0.24/0.35 inference(cnf_transformation,[],[f80])).
% 0.24/0.35 tff(f111,plain,(
% 0.24/0.35 $less($quotient(max(sK0,1/1),sK3),$to_real(sK2))),
% 0.24/0.35 inference(cnf_transformation,[],[f80])).
% 0.24/0.35 tff(f125,plain,(
% 0.24/0.35 ~$less($quotient(max(sK0,1/1),sK3),$quotient(sK1,sK3))),
% 0.24/0.35 inference(forward_demodulation,[],[f110,f103])).
% 0.24/0.35 tff(f484,plain,(
% 0.24/0.35 $to_real(sK2) = $quotient(sK1,sK3) | 0/1 = sK3),
% 0.24/0.35 inference(superposition,[],[f64,f103])).
% 0.24/0.35 tff(f499,definition,(
% 0.24/0.35 spl4_27 <=> 0/1 = sK3),
% 0.24/0.35 introduced(definition,[new_symbols(definition,[spl4_27])],[avatar_definition])).
% 0.24/0.35 tff(f501,plain,(
% 0.24/0.35 0/1 = sK3 | ~spl4_27),
% 0.24/0.35 inference(avatar_component_clause,[],[f499])).
% 0.24/0.35 tff(f503,definition,(
% 0.24/0.35 spl4_28 <=> $to_real(sK2) = $quotient(sK1,sK3)),
% 0.24/0.35 introduced(definition,[new_symbols(definition,[spl4_28])],[avatar_definition])).
% 0.24/0.35 tff(f505,plain,(
% 0.24/0.35 $to_real(sK2) = $quotient(sK1,sK3) | ~spl4_28),
% 0.24/0.35 inference(avatar_component_clause,[],[f503])).
% 0.24/0.35 tff(f506,plain,(
% 0.24/0.35 spl4_27 | spl4_28),
% 0.24/0.35 inference(avatar_split_clause,[],[f484,f503,f499])).
% 0.24/0.35 tff(f508,plain,(
% 0.24/0.35 $less(0/1,0/1) | ~spl4_27),
% 0.24/0.35 inference(superposition,[],[f105,f501])).
% 0.24/0.35 tff(f515,plain,(
% 0.24/0.35 $false | ~spl4_27),
% 0.24/0.35 inference(evaluation,[],[f508])).
% 0.24/0.35 tff(f516,plain,(
% 0.24/0.35 ~spl4_27),
% 0.24/0.35 inference(avatar_contradiction_clause,[],[f515])).
% 0.24/0.35 tff(f545,plain,(
% 0.24/0.35 ~$less($quotient(sK0,sK3),$quotient(sK1,sK3)) | 1/1 = max(sK0,1/1)),
% 0.24/0.35 inference(superposition,[],[f125,f98])).
% 0.24/0.35 tff(f546,plain,(
% 0.24/0.35 $less($quotient(sK0,sK3),$to_real(sK2)) | 1/1 = max(sK0,1/1)),
% 0.24/0.35 inference(superposition,[],[f111,f98])).
% 0.24/0.35 tff(f573,definition,(
% 0.24/0.35 spl4_31 <=> 1/1 = max(sK0,1/1)),
% 0.24/0.35 introduced(definition,[new_symbols(definition,[spl4_31])],[avatar_definition])).
% 0.24/0.35 tff(f575,plain,(
% 0.24/0.35 1/1 = max(sK0,1/1) | ~spl4_31),
% 0.24/0.35 inference(avatar_component_clause,[],[f573])).
% 0.24/0.35 tff(f584,definition,(
% 0.24/0.35 spl4_33 <=> $less($quotient(sK0,sK3),$to_real(sK2))),
% 0.24/0.35 introduced(definition,[new_symbols(definition,[spl4_33])],[avatar_definition])).
% 0.24/0.35 tff(f587,plain,(
% 0.24/0.35 spl4_31 | spl4_33),
% 0.24/0.35 inference(avatar_split_clause,[],[f546,f584,f573])).
% 0.24/0.35 tff(f588,plain,(
% 0.24/0.35 ~$less($quotient(sK0,sK3),$to_real(sK2)) | 1/1 = max(sK0,1/1) | ~spl4_28),
% 0.24/0.35 inference(forward_demodulation,[],[f545,f505])).
% 0.24/0.35 tff(f590,plain,(
% 0.24/0.35 spl4_31 | ~spl4_33 | ~spl4_28),
% 0.24/0.35 inference(avatar_split_clause,[],[f588,f503,f584,f573])).
% 0.24/0.35 tff(f639,plain,(
% 0.24/0.35 $less($quotient(1/1,sK3),$to_real(sK2)) | ~spl4_31),
% 0.24/0.35 inference(superposition,[],[f111,f575])).
% 0.24/0.35 tff(f641,plain,(
% 0.24/0.35 ~$less($quotient(1/1,sK3),$quotient(sK1,sK3)) | ~spl4_31),
% 0.24/0.35 inference(superposition,[],[f125,f575])).
% 0.24/0.35 tff(f648,plain,(
% 0.24/0.35 ~$less($quotient(1/1,sK3),$to_real(sK2)) | (~spl4_28 | ~spl4_31)),
% 0.24/0.35 inference(forward_demodulation,[],[f641,f505])).
% 0.24/0.35 tff(f650,plain,(
% 0.24/0.35 $false | (~spl4_28 | ~spl4_31)),
% 0.24/0.35 inference(forward_subsumption_resolution,[],[f648,f639])).
% 0.24/0.35 tff(f651,plain,(
% 0.24/0.35 ~spl4_28 | ~spl4_31),
% 0.24/0.35 inference(avatar_contradiction_clause,[],[f650])).
% 0.24/0.35 cnf(s25, plain, spl4_27 | spl4_28, inference(sat_conversion,[],[f506])).
% 0.24/0.35 cnf(s26, plain, ~spl4_27, inference(sat_conversion,[],[f516])).
% 0.24/0.35 cnf(s32, plain, spl4_31 | spl4_33, inference(sat_conversion,[],[f587])).
% 0.24/0.35 cnf(s33, plain, ~spl4_28 | spl4_31 | ~spl4_33, inference(sat_conversion,[],[f590])).
% 0.24/0.35 cnf(s35, plain, ~spl4_28 | ~spl4_31, inference(sat_conversion,[],[f651])).
% 0.24/0.35 cnf(s36, plain, spl4_28, inference(rat,[],[s25,s26])).
% 0.24/0.35 cnf(s37, plain, ~spl4_31, inference(rat,[],[s35,s36])).
% 0.24/0.35 cnf(s38, plain, ~spl4_33, inference(rat,[],[s33,s36,s37])).
% 0.24/0.35 cnf(s40, plain, $false, inference(rat,[],[s32,s38,s37])).
% 0.24/0.35 tff(f652,plain,(
% 0.24/0.35 $false),
% 0.24/0.35 inference(avatar_sat_refutation,[],[s40])).
% 0.24/0.35 % SZS output end Proof for theBenchmark
% 0.24/0.35 % (2411428)------------------------------
% 0.24/0.35 % (2411428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.24/0.35 % (2411428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.24/0.35 % (2411428)CaDiCaL version: 2.1.3
% 0.24/0.35 % (2411428)Termination reason: Refutation
% 0.24/0.35 % (2411428)Time elapsed: 0.015 s
% 0.24/0.35 % (2411428)Peak memory usage: 13 MB
% 0.24/0.35 % (2411428)Instructions burned: 24 (million)
% 0.24/0.35 % (2411419)Success in time 0.039 s
% 0.24/0.35 % Vampire exiting
%------------------------------------------------------------------------------