%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ARI674_1 : TPTP v9.3.1. Released v6.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n012.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 09:35:04 AM UTC 2026
% Result : Theorem 0.06s 0.21s
% Output : Refutation 0.06s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ARI674_1 : TPTP v9.3.1. Released v6.3.0.
% 0.00/0.04 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.06/0.15 % Computer : n012.cluster.edu
% 0.06/0.15 % Model : x86_64 x86_64
% 0.06/0.15 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.15 % Memory : 8046.5625MB
% 0.06/0.15 % OS : Linux 6.8.0-71-generic
% 0.06/0.15 % CPULimit : 300
% 0.06/0.15 % WCLimit : 300
% 0.06/0.15 % DateTime : Mon Sep 28 20:55:19 UTC 2026
% 0.06/0.15 % CPUTime :
% 0.06/0.15 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.06/0.18 Running first-order model finding
% 0.06/0.18 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.06/0.21 % (3754558)Will run a generic schedule for satisfiability detection.
% 0.06/0.21 % (3754566)dis+10_1_sil=32000:sp=arity:random_seed=3057117880:i=103:fgj=on_3000 on theBenchmark for (3000ds/103Mi)
% 0.06/0.21 % (3754564)% WARNING: option uhcvi not known.
% 0.06/0.21 % (3754564)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4014559811:i=135531:add=off:rawr=on_3000 on theBenchmark for (3000ds/135531Mi)
% 0.06/0.21 % (3754568)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3624263340:i=131_3000 on theBenchmark for (3000ds/131Mi)
% 0.06/0.21 % (3754565)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3171397014:i=88024:add=on:rawr=on_3000 on theBenchmark for (3000ds/88024Mi)
% 0.06/0.21 % (3754569)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3553950174:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_3000 on theBenchmark for (3000ds/159Mi)
% 0.06/0.21 % (3754563)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3943894038_3000 on theBenchmark for (3000ds/0Mi)
% 0.06/0.21 % (3754567)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2311169931:i=116_3000 on theBenchmark for (3000ds/116Mi)
% 0.06/0.21 % (3754563)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 0.06/0.21 % (3754563)Terminated due to inappropriate strategy.
% 0.06/0.21 % (3754563)------------------------------
% 0.06/0.21 % (3754563)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.06/0.21 % (3754563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.06/0.21 % (3754563)CaDiCaL version: 2.1.3
% 0.06/0.21 % (3754563)Termination reason: Inappropriate
% 0.06/0.21 % (3754563)Time elapsed: 0.0000 s
% 0.06/0.21 % (3754563)Peak memory usage: 10 MB
% 0.06/0.21 % (3754563)------------------------------
% 0.06/0.21 % (3754563)------------------------------
% 0.06/0.21 % (3754568) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3754558-3754568"...
% 0.06/0.21 % (3754568)...printing done.
% 0.06/0.21 % (3754568)Refutation found. Thanks to Tanya!
% 0.06/0.21 % SZS status Theorem for theBenchmark
% 0.06/0.21 % SZS output start Proof for theBenchmark
% 0.06/0.21 tff(func_def_0, type, a: $int).
% 0.06/0.21 tff(f1,axiom,(
% 0.06/0.21 $lesseq(4,$product(a,a))),
% 0.06/0.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj)).
% 0.06/0.21 tff(f2,conjecture,(
% 0.06/0.21 $lesseq(a,-2) | $lesseq(2,a)),
% 0.06/0.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_001)).
% 0.06/0.21 tff(f3,negated_conjecture,(
% 0.06/0.21 ~($lesseq(a,-2) | $lesseq(2,a))),
% 0.06/0.21 inference(negated_conjecture,[status(cth)],[f2])).
% 0.06/0.21 tff(f4,plain,(
% 0.06/0.21 ~$less($product(a,a),4)),
% 0.06/0.21 inference(theory_normalization,[],[f1])).
% 0.06/0.21 tff(f5,plain,(
% 0.06/0.21 ~(~$less(-2,a) | ~$less(a,2))),
% 0.06/0.21 inference(theory_normalization,[],[f3])).
% 0.06/0.21 tff(f13,definition,(
% 0.06/0.21 ( ! [X0 : $int,X1 : $int] : ($less(X0,X1) | $less(X1,X0) | X0 = X1) )),
% 0.06/0.21 introduced(theory,[tha_order_totality])).
% 0.06/0.21 tff(f23,definition,(
% 0.06/0.21 ( ! [X0 : $int,X1 : $int] : (~$less(X0,X1) | ~$less(X1,$sum(X0,1))) )),
% 0.06/0.21 introduced(theory,[tha_extra_integer_ordering])).
% 0.06/0.21 tff(f24,plain,(
% 0.06/0.21 $less(-2,a) & $less(a,2)),
% 0.06/0.21 inference(ennf_transformation,[],[f5])).
% 0.06/0.21 tff(f25,plain,(
% 0.06/0.21 ~$less($product(a,a),4)),
% 0.06/0.21 inference(cnf_transformation,[],[f4])).
% 0.06/0.21 tff(f26,plain,(
% 0.06/0.21 $less(a,2)),
% 0.06/0.21 inference(cnf_transformation,[],[f24])).
% 0.06/0.21 tff(f27,plain,(
% 0.06/0.21 $less(-2,a)),
% 0.06/0.21 inference(cnf_transformation,[],[f24])).
% 0.06/0.21 tff(f50,plain,(
% 0.06/0.21 ~$less(a,$sum(-2,1))),
% 0.06/0.21 inference(resolution,[],[f23,f27])).
% 0.06/0.21 tff(f54,plain,(
% 0.06/0.21 ~$less(a,-1)),
% 0.06/0.21 inference(evaluation,[],[f50])).
% 0.06/0.21 tff(f65,plain,(
% 0.06/0.21 $less(-1,a) | a = -1),
% 0.06/0.21 inference(resolution,[],[f13,f54])).
% 0.06/0.21 tff(f82,definition,(
% 0.06/0.21 spl0_3 <=> a = -1),
% 0.06/0.21 introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition])).
% 0.06/0.21 tff(f84,plain,(
% 0.06/0.21 a = -1 | ~spl0_3),
% 0.06/0.21 inference(avatar_component_clause,[],[f82])).
% 0.06/0.21 tff(f86,definition,(
% 0.06/0.21 spl0_4 <=> $less(-1,a)),
% 0.06/0.21 introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition])).
% 0.06/0.21 tff(f88,plain,(
% 0.06/0.21 $less(-1,a) | ~spl0_4),
% 0.06/0.21 inference(avatar_component_clause,[],[f86])).
% 0.06/0.21 tff(f91,plain,(
% 0.06/0.21 spl0_3 | spl0_4),
% 0.06/0.21 inference(avatar_split_clause,[],[f65,f86,f82])).
% 0.06/0.21 tff(f94,plain,(
% 0.06/0.21 ~$less($product(-1,-1),4) | ~spl0_3),
% 0.06/0.21 inference(superposition,[],[f25,f84])).
% 0.06/0.21 tff(f97,plain,(
% 0.06/0.21 $false | ~spl0_3),
% 0.06/0.21 inference(evaluation,[],[f94])).
% 0.06/0.21 tff(f98,plain,(
% 0.06/0.21 ~spl0_3),
% 0.06/0.21 inference(avatar_contradiction_clause,[],[f97])).
% 0.06/0.21 tff(f119,plain,(
% 0.06/0.21 ~$less(a,$sum(-1,1)) | ~spl0_4),
% 0.06/0.21 inference(resolution,[],[f88,f23])).
% 0.06/0.21 tff(f120,plain,(
% 0.06/0.21 ~$less(a,0) | ~spl0_4),
% 0.06/0.21 inference(evaluation,[],[f119])).
% 0.06/0.21 tff(f145,plain,(
% 0.06/0.21 $less(0,a) | a = 0 | ~spl0_4),
% 0.06/0.21 inference(resolution,[],[f120,f13])).
% 0.06/0.21 tff(f150,definition,(
% 0.06/0.21 spl0_5 <=> a = 0),
% 0.06/0.21 introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition])).
% 0.06/0.21 tff(f152,plain,(
% 0.06/0.21 a = 0 | ~spl0_5),
% 0.06/0.21 inference(avatar_component_clause,[],[f150])).
% 0.06/0.21 tff(f154,definition,(
% 0.06/0.21 spl0_6 <=> $less(0,a)),
% 0.06/0.21 introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition])).
% 0.06/0.21 tff(f156,plain,(
% 0.06/0.21 $less(0,a) | ~spl0_6),
% 0.06/0.21 inference(avatar_component_clause,[],[f154])).
% 0.06/0.21 tff(f158,plain,(
% 0.06/0.21 spl0_5 | spl0_6 | ~spl0_4),
% 0.06/0.21 inference(avatar_split_clause,[],[f145,f86,f154,f150])).
% 0.06/0.21 tff(f174,plain,(
% 0.06/0.21 ~$less($product(0,0),4) | ~spl0_5),
% 0.06/0.21 inference(superposition,[],[f25,f152])).
% 0.06/0.21 tff(f182,plain,(
% 0.06/0.21 $false | ~spl0_5),
% 0.06/0.21 inference(evaluation,[],[f174])).
% 0.06/0.21 tff(f183,plain,(
% 0.06/0.21 ~spl0_5),
% 0.06/0.21 inference(avatar_contradiction_clause,[],[f182])).
% 0.06/0.21 tff(f216,plain,(
% 0.06/0.21 ~$less(a,$sum(0,1)) | ~spl0_6),
% 0.06/0.21 inference(resolution,[],[f156,f23])).
% 0.06/0.21 tff(f217,plain,(
% 0.06/0.21 ~$less(a,1) | ~spl0_6),
% 0.06/0.21 inference(evaluation,[],[f216])).
% 0.06/0.21 tff(f239,plain,(
% 0.06/0.21 $less(1,a) | a = 1 | ~spl0_6),
% 0.06/0.21 inference(resolution,[],[f217,f13])).
% 0.06/0.21 tff(f243,definition,(
% 0.06/0.21 spl0_7 <=> a = 1),
% 0.06/0.21 introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition])).
% 0.06/0.21 tff(f245,plain,(
% 0.06/0.21 a = 1 | ~spl0_7),
% 0.06/0.21 inference(avatar_component_clause,[],[f243])).
% 0.06/0.21 tff(f247,definition,(
% 0.06/0.21 spl0_8 <=> $less(1,a)),
% 0.06/0.21 introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition])).
% 0.06/0.21 tff(f249,plain,(
% 0.06/0.21 $less(1,a) | ~spl0_8),
% 0.06/0.21 inference(avatar_component_clause,[],[f247])).
% 0.06/0.21 tff(f251,plain,(
% 0.06/0.21 spl0_7 | spl0_8 | ~spl0_6),
% 0.06/0.21 inference(avatar_split_clause,[],[f239,f154,f247,f243])).
% 0.06/0.21 tff(f278,plain,(
% 0.06/0.21 ~$less($product(1,1),4) | ~spl0_7),
% 0.06/0.21 inference(superposition,[],[f25,f245])).
% 0.06/0.21 tff(f292,plain,(
% 0.06/0.21 $false | ~spl0_7),
% 0.06/0.21 inference(evaluation,[],[f278])).
% 0.06/0.21 tff(f293,plain,(
% 0.06/0.21 ~spl0_7),
% 0.06/0.21 inference(avatar_contradiction_clause,[],[f292])).
% 0.06/0.21 tff(f318,plain,(
% 0.06/0.21 ~$less(a,$sum(1,1)) | ~spl0_8),
% 0.06/0.21 inference(resolution,[],[f249,f23])).
% 0.06/0.21 tff(f319,plain,(
% 0.06/0.21 ~$less(a,2) | ~spl0_8),
% 0.06/0.21 inference(evaluation,[],[f318])).
% 0.06/0.21 tff(f320,plain,(
% 0.06/0.21 $false | ~spl0_8),
% 0.06/0.21 inference(forward_subsumption_resolution,[],[f319,f26])).
% 0.06/0.21 tff(f321,plain,(
% 0.06/0.21 ~spl0_8),
% 0.06/0.21 inference(avatar_contradiction_clause,[],[f320])).
% 0.06/0.21 cnf(s4, plain, spl0_3 | spl0_4, inference(sat_conversion,[],[f91])).
% 0.06/0.21 cnf(s5, plain, ~spl0_3, inference(sat_conversion,[],[f98])).
% 0.06/0.21 cnf(s7, plain, ~spl0_4 | spl0_5 | spl0_6, inference(sat_conversion,[],[f158])).
% 0.06/0.21 cnf(s8, plain, ~spl0_5, inference(sat_conversion,[],[f183])).
% 0.06/0.21 cnf(s10, plain, ~spl0_6 | spl0_7 | spl0_8, inference(sat_conversion,[],[f251])).
% 0.06/0.21 cnf(s11, plain, ~spl0_7, inference(sat_conversion,[],[f293])).
% 0.06/0.21 cnf(s12, plain, ~spl0_8, inference(sat_conversion,[],[f321])).
% 0.06/0.21 cnf(s13, plain, ~spl0_6, inference(rat,[],[s10,s12,s11])).
% 0.06/0.21 cnf(s14, plain, ~spl0_4, inference(rat,[],[s7,s13,s8])).
% 0.06/0.21 cnf(s15, plain, $false, inference(rat,[],[s4,s14,s5])).
% 0.06/0.21 tff(f322,plain,(
% 0.06/0.21 $false),
% 0.06/0.21 inference(avatar_sat_refutation,[],[s15])).
% 0.06/0.21 % SZS output end Proof for theBenchmark
% 0.06/0.21 % (3754568)------------------------------
% 0.06/0.21 % (3754568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.06/0.21 % (3754568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.06/0.21 % (3754568)CaDiCaL version: 2.1.3
% 0.06/0.21 % (3754568)Termination reason: Refutation
% 0.06/0.21 % (3754568)Time elapsed: 0.007 s
% 0.06/0.21 % (3754568)Peak memory usage: 12 MB
% 0.06/0.21 % (3754568)Instructions burned: 10 (million)
% 0.06/0.21 % (3754558)Success in time 0.03 s
% 0.06/0.21 % Vampire exiting
%------------------------------------------------------------------------------