%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NUM016^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n006.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:03 AM UTC 2026
% Result : Theorem 0.21s 0.27s
% Output : Refutation 0.21s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM016^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 % Computer : n006.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Tue Sep 29 11:52:54 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 Running first-order model finding
% 0.09/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.21/0.27 % (615443)Will run a generic schedule for satisfiability detection.
% 0.21/0.27 % (615455)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4179287821:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.21/0.27 % (615450)% WARNING: option uhcvi not known.
% 0.21/0.27 % (615450)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1995025118:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.21/0.27 % (615449)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4060988388_2999 on theBenchmark for (2999ds/0Mi)
% 0.21/0.27 % (615455) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-615443-615455"...
% 0.21/0.27 % (615451)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1177930605:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.21/0.27 % (615450)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.21/0.27 % (615450)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.21/0.27 % Exception at run slice level
% 0.21/0.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.21/0.27 % (615452)dis+10_1_sil=32000:sp=arity:random_seed=4128848579:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.21/0.27 % (615455)...printing done.
% 0.21/0.27 % (615455)Refutation found. Thanks to Tanya!
% 0.21/0.27 % SZS status Theorem for theBenchmark
% 0.21/0.27 % SZS output start Proof for theBenchmark
% 0.21/0.27 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 0.21/0.27 thf(func_def_1, type, factorial_plus_one: ($i > $i)).
% 0.21/0.27 thf(func_def_2, type, less: ($i > $i > $o)).
% 0.21/0.27 thf(func_def_3, type, prime: ($i > $o)).
% 0.21/0.27 thf(func_def_4, type, prime_divisor: ($i > $i)).
% 0.21/0.27 thf(func_def_5, type, divides: ($i > $i > $o)).
% 0.21/0.27 thf(f1,conjecture,(
% 0.21/0.27 ~(! [X0 : $i] : ((less @ (factorial_plus_one @ a) @ X0) | ~(less @ a @ X0) | ~(prime @ X0)) & (prime @ a) & ! [X0 : $i] : ((less @ (prime_divisor @ X0) @ X0) | (prime @ X0)) & ! [X0 : $i] : ((prime @ (prime_divisor @ X0)) | (prime @ X0)) & ! [X0 : $i] : ((divides @ (prime_divisor @ X0) @ X0) | (prime @ X0)) & ! [X0 : $i,X1 : $i] : ((less @ X1 @ X0) | ~(divides @ X0 @ (factorial_plus_one @ X1))) & ! [X0 : $i] : (less @ X0 @ (factorial_plus_one @ X0)) & ! [X0 : $i,X1 : $i] : (~(less @ X1 @ X0) | ~(divides @ X0 @ X1)) & ! [X0 : $i,X1 : $i,X2 : $i] : ((divides @ X0 @ X2) | ~(divides @ X1 @ X2) | ~(divides @ X0 @ X1)) & ! [X0 : $i] : (divides @ X0 @ X0) & ! [X0 : $i,X1 : $i] : (~(less @ X1 @ X0) | ~(less @ X0 @ X1)) & ! [X0 : $i] : ~(less @ X0 @ X0))),
% 0.21/0.27 file('/export/starexec/sandbox/benchmark/theBenchmark.p',cNUM016_1)).
% 0.21/0.27 thf(f2,negated_conjecture,(
% 0.21/0.27 ~ ~(! [X0 : $i] : ((less @ (factorial_plus_one @ a) @ X0) | ~(less @ a @ X0) | ~(prime @ X0)) & (prime @ a) & ! [X0 : $i] : ((less @ (prime_divisor @ X0) @ X0) | (prime @ X0)) & ! [X0 : $i] : ((prime @ (prime_divisor @ X0)) | (prime @ X0)) & ! [X0 : $i] : ((divides @ (prime_divisor @ X0) @ X0) | (prime @ X0)) & ! [X0 : $i,X1 : $i] : ((less @ X1 @ X0) | ~(divides @ X0 @ (factorial_plus_one @ X1))) & ! [X0 : $i] : (less @ X0 @ (factorial_plus_one @ X0)) & ! [X0 : $i,X1 : $i] : (~(less @ X1 @ X0) | ~(divides @ X0 @ X1)) & ! [X0 : $i,X1 : $i,X2 : $i] : ((divides @ X0 @ X2) | ~(divides @ X1 @ X2) | ~(divides @ X0 @ X1)) & ! [X0 : $i] : (divides @ X0 @ X0) & ! [X0 : $i,X1 : $i] : (~(less @ X1 @ X0) | ~(less @ X0 @ X1)) & ! [X0 : $i] : ~(less @ X0 @ X0))),
% 0.21/0.27 inference(negated_conjecture,[status(cth)],[f1])).
% 0.21/0.27 thf(f3,plain,(
% 0.21/0.27 ~ ~(! [X0 : $i] : ((less @ (factorial_plus_one @ a) @ X0) | ~(less @ a @ X0) | ~(prime @ X0)) & (prime @ a) & ! [X1 : $i] : ((less @ (prime_divisor @ X1) @ X1) | (prime @ X1)) & ! [X2 : $i] : ((prime @ (prime_divisor @ X2)) | (prime @ X2)) & ! [X3 : $i] : ((divides @ (prime_divisor @ X3) @ X3) | (prime @ X3)) & ! [X4 : $i,X5 : $i] : ((less @ X5 @ X4) | ~(divides @ X4 @ (factorial_plus_one @ X5))) & ! [X6 : $i] : (less @ X6 @ (factorial_plus_one @ X6)) & ! [X7 : $i,X8 : $i] : (~(less @ X8 @ X7) | ~(divides @ X7 @ X8)) & ! [X9 : $i,X10 : $i,X11 : $i] : ((divides @ X9 @ X11) | ~(divides @ X10 @ X11) | ~(divides @ X9 @ X10)) & ! [X12 : $i] : (divides @ X12 @ X12) & ! [X13 : $i,X14 : $i] : (~(less @ X14 @ X13) | ~(less @ X13 @ X14)) & ! [X15 : $i] : ~(less @ X15 @ X15))),
% 0.21/0.27 inference(rectify,[],[f2])).
% 0.21/0.27 thf(f4,plain,(
% 0.21/0.27 ~ ~(! [X0 : $i] : ((((less @ (factorial_plus_one @ a) @ X0)) = $true) | ~ (((less @ a @ X0)) = $true) | ~ (((prime @ X0)) = $true)) & (((prime @ a)) = $true) & ! [X1 : $i] : ((((less @ (prime_divisor @ X1) @ X1)) = $true) | (((prime @ X1)) = $true)) & ! [X2 : $i] : ((((prime @ (prime_divisor @ X2))) = $true) | (((prime @ X2)) = $true)) & ! [X3 : $i] : ((((divides @ (prime_divisor @ X3) @ X3)) = $true) | (((prime @ X3)) = $true)) & ! [X4 : $i,X5 : $i] : ((((less @ X5 @ X4)) = $true) | ~ (((divides @ X4 @ (factorial_plus_one @ X5))) = $true)) & ! [X6 : $i] : (((less @ X6 @ (factorial_plus_one @ X6))) = $true) & ! [X7 : $i,X8 : $i] : (~ (((less @ X8 @ X7)) = $true) | ~ (((divides @ X7 @ X8)) = $true)) & ! [X9 : $i,X10 : $i,X11 : $i] : ((((divides @ X9 @ X11)) = $true) | ~ (((divides @ X10 @ X11)) = $true) | ~ (((divides @ X9 @ X10)) = $true)) & ! [X12 : $i] : (((divides @ X12 @ X12)) = $true) & ! [X13 : $i,X14 : $i] : (~ (((less @ X14 @ X13)) = $true) | ~ (((less @ X13 @ X14)) = $true)) & ! [X15 : $i] : ~ (((less @ X15 @ X15)) = $true))),
% 0.21/0.27 inference(fool_elimination,[],[f3])).
% 0.21/0.27 thf(f5,plain,(
% 0.21/0.27 ! [X0 : $i] : ((((less @ (factorial_plus_one @ a) @ X0)) = $true) | (((less @ a @ X0)) != $true) | (((prime @ X0)) != $true)) & (((prime @ a)) = $true) & ! [X1 : $i] : ((((less @ (prime_divisor @ X1) @ X1)) = $true) | (((prime @ X1)) = $true)) & ! [X2 : $i] : ((((prime @ (prime_divisor @ X2))) = $true) | (((prime @ X2)) = $true)) & ! [X3 : $i] : ((((divides @ (prime_divisor @ X3) @ X3)) = $true) | (((prime @ X3)) = $true)) & ! [X4 : $i,X5 : $i] : ((((less @ X5 @ X4)) = $true) | (((divides @ X4 @ (factorial_plus_one @ X5))) != $true)) & ! [X6 : $i] : (((less @ X6 @ (factorial_plus_one @ X6))) = $true) & ! [X7 : $i,X8 : $i] : ((((less @ X8 @ X7)) != $true) | (((divides @ X7 @ X8)) != $true)) & ! [X9 : $i,X10 : $i,X11 : $i] : ((((divides @ X9 @ X11)) = $true) | (((divides @ X10 @ X11)) != $true) | (((divides @ X9 @ X10)) != $true)) & ! [X12 : $i] : (((divides @ X12 @ X12)) = $true) & ! [X13 : $i,X14 : $i] : ((((less @ X14 @ X13)) != $true) | (((less @ X13 @ X14)) != $true)) & ! [X15 : $i] : (((less @ X15 @ X15)) != $true)),
% 0.21/0.27 inference(flattening,[],[f4])).
% 0.21/0.27 thf(f6,plain,(
% 0.21/0.27 ( ! [X15 : $i] : ((((less @ X15 @ X15)) != $true)) )),
% 0.21/0.27 inference(cnf_transformation,[],[f5])).
% 0.21/0.27 thf(f7,plain,(
% 0.21/0.27 ( ! [X14 : $i,X13 : $i] : ((((less @ X14 @ X13)) != $true) | (((less @ X13 @ X14)) != $true)) )),
% 0.21/0.27 inference(cnf_transformation,[],[f5])).
% 0.21/0.27 thf(f11,plain,(
% 0.21/0.27 ( ! [X6 : $i] : ((((less @ X6 @ (factorial_plus_one @ X6))) = $true)) )),
% 0.21/0.27 inference(cnf_transformation,[],[f5])).
% 0.21/0.27 thf(f12,plain,(
% 0.21/0.27 ( ! [X4 : $i,X5 : $i] : ((((divides @ X4 @ (factorial_plus_one @ X5))) != $true) | (((less @ X5 @ X4)) = $true)) )),
% 0.21/0.27 inference(cnf_transformation,[],[f5])).
% 0.21/0.27 thf(f13,plain,(
% 0.21/0.27 ( ! [X3 : $i] : ((((divides @ (prime_divisor @ X3) @ X3)) = $true) | (((prime @ X3)) = $true)) )),
% 0.21/0.27 inference(cnf_transformation,[],[f5])).
% 0.21/0.27 thf(f14,plain,(
% 0.21/0.27 ( ! [X2 : $i] : ((((prime @ (prime_divisor @ X2))) = $true) | (((prime @ X2)) = $true)) )),
% 0.21/0.27 inference(cnf_transformation,[],[f5])).
% 0.21/0.27 thf(f15,plain,(
% 0.21/0.27 ( ! [X1 : $i] : ((((less @ (prime_divisor @ X1) @ X1)) = $true) | (((prime @ X1)) = $true)) )),
% 0.21/0.27 inference(cnf_transformation,[],[f5])).
% 0.21/0.27 thf(f17,plain,(
% 0.21/0.27 ( ! [X0 : $i] : ((((prime @ X0)) != $true) | (((less @ a @ X0)) != $true) | (((less @ (factorial_plus_one @ a) @ X0)) = $true)) )),
% 0.21/0.27 inference(cnf_transformation,[],[f5])).
% 0.21/0.27 thf(f19,definition,(
% 0.21/0.27 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 0.21/0.27 introduced(theory,[fool_exhaustiveness_axiom])).
% 0.21/0.27 thf(f21,plain,(
% 0.21/0.27 ( ! [X0 : $i] : (($true != $true) | ($true != ((less @ X0 @ (prime_divisor @ X0)))) | (((prime @ X0)) = $true)) )),
% 0.21/0.27 inference(constrained_superposition,[],[f7,f15])).
% 0.21/0.27 thf(f22,plain,(
% 0.21/0.27 ( ! [X0 : $i] : (($true != ((less @ X0 @ (prime_divisor @ X0)))) | (((prime @ X0)) = $true)) )),
% 0.21/0.27 inference(trivial_inequality_removal,[],[f21])).
% 0.21/0.27 thf(f29,plain,(
% 0.21/0.27 ( ! [X0 : $i] : (($true != $true) | ($true = ((less @ X0 @ (prime_divisor @ (factorial_plus_one @ X0))))) | ($true = ((prime @ (factorial_plus_one @ X0))))) )),
% 0.21/0.27 inference(constrained_superposition,[],[f12,f13])).
% 0.21/0.27 thf(f30,plain,(
% 0.21/0.27 ( ! [X0 : $i] : (($true = ((less @ X0 @ (prime_divisor @ (factorial_plus_one @ X0))))) | ($true = ((prime @ (factorial_plus_one @ X0))))) )),
% 0.21/0.27 inference(trivial_inequality_removal,[],[f29])).
% 0.21/0.27 thf(f47,plain,(
% 0.21/0.27 ( ! [X0 : $i] : (($true != $true) | (((less @ a @ X0)) != $true) | (((less @ (factorial_plus_one @ a) @ X0)) = $true) | (((prime @ X0)) = $false)) )),
% 0.21/0.27 inference(constrained_superposition,[],[f17,f19])).
% 0.21/0.27 thf(f69,plain,(
% 0.21/0.27 ( ! [X0 : $i] : ((((less @ a @ X0)) != $true) | (((less @ (factorial_plus_one @ a) @ X0)) = $true) | (((prime @ X0)) = $false)) )),
% 0.21/0.27 inference(trivial_inequality_removal,[],[f47])).
% 0.21/0.27 thf(f152,plain,(
% 0.21/0.27 ($true != $true) | ($true = ((less @ (factorial_plus_one @ a) @ (factorial_plus_one @ a)))) | ($false = ((prime @ (factorial_plus_one @ a))))),
% 0.21/0.27 inference(constrained_superposition,[],[f69,f11])).
% 0.21/0.27 thf(f153,plain,(
% 0.21/0.27 ($true != $true) | ($true = ((less @ (factorial_plus_one @ a) @ (prime_divisor @ (factorial_plus_one @ a))))) | ($false = ((prime @ (prime_divisor @ (factorial_plus_one @ a))))) | ($true = ((prime @ (factorial_plus_one @ a))))),
% 0.21/0.27 inference(constrained_superposition,[],[f69,f30])).
% 0.21/0.27 thf(f157,plain,(
% 0.21/0.27 ($true = ((less @ (factorial_plus_one @ a) @ (prime_divisor @ (factorial_plus_one @ a))))) | ($false = ((prime @ (prime_divisor @ (factorial_plus_one @ a))))) | ($true = ((prime @ (factorial_plus_one @ a))))),
% 0.21/0.27 inference(trivial_inequality_removal,[],[f153])).
% 0.21/0.27 thf(f158,plain,(
% 0.21/0.27 ($true = ((less @ (factorial_plus_one @ a) @ (factorial_plus_one @ a)))) | ($false = ((prime @ (factorial_plus_one @ a))))),
% 0.21/0.27 inference(trivial_inequality_removal,[],[f152])).
% 0.21/0.27 thf(f159,plain,(
% 0.21/0.27 ($false = ((prime @ (prime_divisor @ (factorial_plus_one @ a))))) | ($true = ((prime @ (factorial_plus_one @ a))))),
% 0.21/0.27 inference(forward_subsumption_resolution,[],[f157,f22])).
% 0.21/0.27 thf(f160,plain,(
% 0.21/0.27 ($false = ((prime @ (factorial_plus_one @ a))))),
% 0.21/0.27 inference(forward_subsumption_resolution,[],[f158,f6])).
% 0.21/0.27 thf(f162,definition,(
% 0.21/0.27 spl0_1 <=> ($true = ((prime @ (factorial_plus_one @ a))))),
% 0.21/0.27 introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition])).
% 0.21/0.27 thf(f164,plain,(
% 0.21/0.27 ($true = ((prime @ (factorial_plus_one @ a)))) | ~spl0_1),
% 0.21/0.27 inference(avatar_component_clause,[],[f162])).
% 0.21/0.27 thf(f166,definition,(
% 0.21/0.27 spl0_2 <=> ($false = ((prime @ (prime_divisor @ (factorial_plus_one @ a)))))),
% 0.21/0.27 introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition])).
% 0.21/0.27 thf(f168,plain,(
% 0.21/0.27 ($false = ((prime @ (prime_divisor @ (factorial_plus_one @ a))))) | ~spl0_2),
% 0.21/0.27 inference(avatar_component_clause,[],[f166])).
% 0.21/0.27 thf(f169,plain,(
% 0.21/0.27 spl0_1 | spl0_2),
% 0.21/0.27 inference(avatar_split_clause,[],[f159,f166,f162])).
% 0.21/0.27 thf(f182,plain,(
% 0.21/0.27 ($true = $false) | ($true = ((prime @ (factorial_plus_one @ a)))) | ~spl0_2),
% 0.21/0.27 inference(constrained_superposition,[],[f168,f14])).
% 0.21/0.27 thf(f188,plain,(
% 0.21/0.27 ($true = ((prime @ (factorial_plus_one @ a)))) | ~spl0_2),
% 0.21/0.27 inference(trivial_inequality_removal,[],[f182])).
% 0.21/0.27 thf(f192,plain,(
% 0.21/0.27 ($true = $false) | ~spl0_2),
% 0.21/0.27 inference(forward_demodulation,[],[f188,f160])).
% 0.21/0.27 thf(f193,plain,(
% 0.21/0.27 $false | ~spl0_2),
% 0.21/0.27 inference(trivial_inequality_removal,[],[f192])).
% 0.21/0.27 thf(f194,plain,(
% 0.21/0.27 ~spl0_2),
% 0.21/0.27 inference(avatar_contradiction_clause,[],[f193])).
% 0.21/0.27 thf(f195,plain,(
% 0.21/0.27 ($true = $false) | ~spl0_1),
% 0.21/0.27 inference(forward_demodulation,[],[f164,f160])).
% 0.21/0.27 thf(f196,plain,(
% 0.21/0.27 $false | ~spl0_1),
% 0.21/0.27 inference(trivial_inequality_removal,[],[f195])).
% 0.21/0.27 thf(f197,plain,(
% 0.21/0.27 ~spl0_1),
% 0.21/0.27 inference(avatar_contradiction_clause,[],[f196])).
% 0.21/0.27 cnf(s1, plain, spl0_1 | spl0_2, inference(sat_conversion,[],[f169])).
% 0.21/0.27 cnf(s3, plain, ~spl0_2, inference(sat_conversion,[],[f194])).
% 0.21/0.27 cnf(s4, plain, ~spl0_1, inference(sat_conversion,[],[f197])).
% 0.21/0.27 cnf(s5, plain, $false, inference(rat,[],[s1,s3,s4])).
% 0.21/0.27 thf(f198,plain,(
% 0.21/0.27 $false),
% 0.21/0.27 inference(avatar_sat_refutation,[],[s5])).
% 0.21/0.27 % SZS output end Proof for theBenchmark
% 0.21/0.27 % (615455)------------------------------
% 0.21/0.27 % (615455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.27 % (615455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.27 % (615455)CaDiCaL version: 2.1.3
% 0.21/0.27 % (615455)Termination reason: Refutation
% 0.21/0.27 % (615455)Time elapsed: 0.006 s
% 0.21/0.27 % (615455)Peak memory usage: 13 MB
% 0.21/0.27 % (615455)Instructions burned: 17 (million)
% 0.21/0.27 % (615443)Success in time 0.041 s
% 0.21/0.27 % Vampire exiting
%------------------------------------------------------------------------------