%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : DAT017_1 : TPTP v9.3.1. Released v5.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n016.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:47:58 AM UTC 2026
% Result : Theorem 0.19s 0.27s
% Output : Refutation 0.19s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : DAT017_1 : TPTP v9.3.1. Released v5.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 % Computer : n016.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Tue Sep 29 00:10:19 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.22 Running first-order model finding
% 0.08/0.22 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.19/0.27 % (4167500)Will run a generic schedule for satisfiability detection.
% 0.19/0.27 % (4167514)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1545384514:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.19/0.27 % (4167510)% WARNING: option uhcvi not known.
% 0.19/0.27 % (4167514) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-4167500-4167514"...
% 0.19/0.27 % (4167509)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1549186590_2999 on theBenchmark for (2999ds/0Mi)
% 0.19/0.27 % (4167513)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3575336432:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.19/0.27 % (4167511)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3789947468:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.19/0.27 % (4167510)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1919629414:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.19/0.27 % (4167514)...printing done.
% 0.19/0.27 % (4167509)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 0.19/0.27 % (4167509)Terminated due to inappropriate strategy.
% 0.19/0.27 % (4167509)------------------------------
% 0.19/0.27 % (4167509)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.27 % (4167509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.27 % (4167509)CaDiCaL version: 2.1.3
% 0.19/0.27 % (4167509)Termination reason: Inappropriate
% 0.19/0.27 % (4167509)Time elapsed: 0.0000 s
% 0.19/0.27 % (4167509)Peak memory usage: 10 MB
% 0.19/0.27 % (4167512)dis+10_1_sil=32000:sp=arity:random_seed=3454622435:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.19/0.27 % (4167515)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=457189557:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.19/0.27 % (4167514)Refutation found. Thanks to Tanya!
% 0.19/0.27 % SZS status Theorem for theBenchmark
% 0.19/0.27 % SZS output start Proof for theBenchmark
% 0.19/0.27 tff(type_def_5, type, array: $tType).
% 0.19/0.27 tff(func_def_0, type, read: (array * $int) > $int).
% 0.19/0.27 tff(func_def_1, type, write: (array * $int * $int) > array).
% 0.19/0.27 tff(func_def_6, type, sK0: array).
% 0.19/0.27 tff(func_def_7, type, sK1: array).
% 0.19/0.27 tff(func_def_8, type, sK2: $int).
% 0.19/0.27 tff(func_def_9, type, sK3: $int).
% 0.19/0.27 tff(func_def_10, type, sK4: $int).
% 0.19/0.27 tff(f1,axiom,(
% 0.19/0.27 ! [X0 : array,X1 : $int,X2 : $int] : read(write(X0,X1,X2),X1) = X2),
% 0.19/0.27 file('/export/starexec/sandbox2/benchmark/Axioms/DAT001_0.ax',ax1)).
% 0.19/0.27 tff(f2,axiom,(
% 0.19/0.27 ! [X0 : array,X1 : $int,X2 : $int,X3 : $int] : (X1 = X2 | read(write(X0,X1,X3),X2) = read(X0,X2))),
% 0.19/0.27 file('/export/starexec/sandbox2/benchmark/Axioms/DAT001_0.ax',ax2)).
% 0.19/0.27 tff(f3,conjecture,(
% 0.19/0.27 ! [X0 : array,X1 : array,X2 : $int,X3 : $int,X4 : $int] : ((read(X1,X2) != read(X1,X3) & X0 = write(write(write(X1,X3,0),X4,$sum(read(X1,X4),1)),X2,0)) => ? [X5 : $int] : read(X0,X5) != read(X1,X5))),
% 0.19/0.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1)).
% 0.19/0.27 tff(f4,negated_conjecture,(
% 0.19/0.27 ~ ! [X0 : array,X1 : array,X2 : $int,X3 : $int,X4 : $int] : ((read(X1,X2) != read(X1,X3) & X0 = write(write(write(X1,X3,0),X4,$sum(read(X1,X4),1)),X2,0)) => ? [X5 : $int] : read(X0,X5) != read(X1,X5))),
% 0.19/0.27 inference(negated_conjecture,[status(cth)],[f3])).
% 0.19/0.27 tff(f5,definition,(
% 0.19/0.27 ( ! [X0 : $int,X1 : $int] : ($sum(X0,X1) = $sum(X1,X0)) )),
% 0.19/0.27 introduced(theory,[tha_commutativity])).
% 0.19/0.27 tff(f10,definition,(
% 0.19/0.27 ( ! [X0 : $int] : (~$less(X0,X0)) )),
% 0.19/0.27 introduced(theory,[tha_non-reflexivity])).
% 0.19/0.27 tff(f14,definition,(
% 0.19/0.27 ( ! [X0 : $int,X1 : $int] : ($less(X0,X1) | $less(X1,$sum(X0,1))) )),
% 0.19/0.27 introduced(theory,[tha_order_plus_one_dichotomy])).
% 0.19/0.27 tff(f16,definition,(
% 0.19/0.27 ( ! [X0 : $int,X1 : $int] : (~$less(X0,X1) | ~$less(X1,$sum(X0,1))) )),
% 0.19/0.27 introduced(theory,[tha_extra_integer_ordering])).
% 0.19/0.27 tff(f17,plain,(
% 0.19/0.27 ? [X0 : array,X1 : array,X2 : $int,X3 : $int,X4 : $int] : (! [X5 : $int] : read(X0,X5) = read(X1,X5) & (read(X1,X2) != read(X1,X3) & X0 = write(write(write(X1,X3,0),X4,$sum(read(X1,X4),1)),X2,0)))),
% 0.19/0.27 inference(ennf_transformation,[],[f4])).
% 0.19/0.27 tff(f18,plain,(
% 0.19/0.27 ? [X0 : array,X1 : array,X2 : $int,X3 : $int,X4 : $int] : (! [X5 : $int] : read(X0,X5) = read(X1,X5) & read(X1,X2) != read(X1,X3) & X0 = write(write(write(X1,X3,0),X4,$sum(read(X1,X4),1)),X2,0))),
% 0.19/0.27 inference(flattening,[],[f17])).
% 0.19/0.27 tff(f19,plain,(
% 0.19/0.27 ! [X5 : $int] : read(sK0,X5) = read(sK1,X5) & read(sK1,sK2) != read(sK1,sK3) & sK0 = write(write(write(sK1,sK3,0),sK4,$sum(read(sK1,sK4),1)),sK2,0)),
% 0.19/0.27 inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3),skolemize(X4,sK4)],[f18])).
% 0.19/0.27 tff(f20,plain,(
% 0.19/0.27 ( ! [X2 : $int,X0 : array,X1 : $int] : (read(write(X0,X1,X2),X1) = X2) )),
% 0.19/0.27 inference(cnf_transformation,[],[f1])).
% 0.19/0.27 tff(f21,plain,(
% 0.19/0.27 ( ! [X2 : $int,X3 : $int,X0 : array,X1 : $int] : (read(write(X0,X1,X3),X2) = read(X0,X2) | X1 = X2) )),
% 0.19/0.27 inference(cnf_transformation,[],[f2])).
% 0.19/0.27 tff(f22,plain,(
% 0.19/0.27 sK0 = write(write(write(sK1,sK3,0),sK4,$sum(read(sK1,sK4),1)),sK2,0)),
% 0.19/0.27 inference(cnf_transformation,[],[f19])).
% 0.19/0.27 tff(f23,plain,(
% 0.19/0.27 read(sK1,sK2) != read(sK1,sK3)),
% 0.19/0.27 inference(cnf_transformation,[],[f19])).
% 0.19/0.27 tff(f24,plain,(
% 0.19/0.27 ( ! [X5 : $int] : (read(sK0,X5) = read(sK1,X5)) )),
% 0.19/0.27 inference(cnf_transformation,[],[f19])).
% 0.19/0.27 tff(f25,plain,(
% 0.19/0.27 read(sK1,sK2) != read(sK0,sK3)),
% 0.19/0.27 inference(superposition,[],[f23,f24])).
% 0.19/0.27 tff(f26,plain,(
% 0.19/0.27 read(sK0,sK3) != read(sK0,sK2)),
% 0.19/0.27 inference(forward_demodulation,[],[f25,f24])).
% 0.19/0.27 tff(f27,plain,(
% 0.19/0.27 sK0 = write(write(write(sK1,sK3,0),sK4,$sum(read(sK0,sK4),1)),sK2,0)),
% 0.19/0.27 inference(superposition,[],[f22,f24])).
% 0.19/0.27 tff(f28,plain,(
% 0.19/0.27 sK0 = write(write(write(sK1,sK3,0),sK4,$sum(1,read(sK0,sK4))),sK2,0)),
% 0.19/0.27 inference(forward_demodulation,[],[f27,f5])).
% 0.19/0.27 tff(f39,plain,(
% 0.19/0.27 ( ! [X0 : $int] : ($less(X0,$sum(X0,1))) )),
% 0.19/0.27 inference(resolution,[],[f14,f10])).
% 0.19/0.27 tff(f46,plain,(
% 0.19/0.27 ( ! [X0 : $int] : ($less(X0,$sum(1,X0))) )),
% 0.19/0.27 inference(superposition,[],[f39,f5])).
% 0.19/0.27 tff(f48,plain,(
% 0.19/0.27 0 = read(sK0,sK2)),
% 0.19/0.27 inference(superposition,[],[f20,f28])).
% 0.19/0.27 tff(f53,plain,(
% 0.19/0.27 ( ! [X0 : $int] : (~$less($sum(1,X0),$sum(X0,1))) )),
% 0.19/0.27 inference(resolution,[],[f46,f16])).
% 0.19/0.27 tff(f151,plain,(
% 0.19/0.27 ( ! [X0 : $int] : (read(sK0,X0) = read(write(write(sK1,sK3,0),sK4,$sum(1,read(sK0,sK4))),X0) | sK2 = X0) )),
% 0.19/0.28 inference(superposition,[],[f21,f28])).
% 0.19/0.28 tff(f154,plain,(
% 0.19/0.28 read(sK0,sK4) = $sum(1,read(sK0,sK4)) | sK2 = sK4),
% 0.19/0.28 inference(superposition,[],[f151,f20])).
% 0.19/0.28 tff(f157,plain,(
% 0.19/0.28 ( ! [X0 : $int] : (read(sK0,X0) = read(write(sK1,sK3,0),X0) | sK4 = X0 | sK2 = X0) )),
% 0.19/0.28 inference(superposition,[],[f21,f151])).
% 0.19/0.28 tff(f159,definition,(
% 0.19/0.28 spl5_1 <=> sK2 = sK4),
% 0.19/0.28 introduced(definition,[new_symbols(definition,[spl5_1])],[avatar_definition])).
% 0.19/0.28 tff(f161,plain,(
% 0.19/0.28 sK2 = sK4 | ~spl5_1),
% 0.19/0.28 inference(avatar_component_clause,[],[f159])).
% 0.19/0.28 tff(f163,definition,(
% 0.19/0.28 spl5_2 <=> read(sK0,sK4) = $sum(1,read(sK0,sK4))),
% 0.19/0.28 introduced(definition,[new_symbols(definition,[spl5_2])],[avatar_definition])).
% 0.19/0.28 tff(f165,plain,(
% 0.19/0.28 read(sK0,sK4) = $sum(1,read(sK0,sK4)) | ~spl5_2),
% 0.19/0.28 inference(avatar_component_clause,[],[f163])).
% 0.19/0.28 tff(f167,plain,(
% 0.19/0.28 spl5_1 | spl5_2),
% 0.19/0.28 inference(avatar_split_clause,[],[f154,f163,f159])).
% 0.19/0.28 tff(f203,plain,(
% 0.19/0.28 ~$less(read(sK0,sK4),$sum(read(sK0,sK4),1)) | ~spl5_2),
% 0.19/0.28 inference(superposition,[],[f53,f165])).
% 0.19/0.28 tff(f211,plain,(
% 0.19/0.28 $false | ~spl5_2),
% 0.19/0.28 inference(forward_subsumption_resolution,[],[f203,f39])).
% 0.19/0.28 tff(f212,plain,(
% 0.19/0.28 ~spl5_2),
% 0.19/0.28 inference(avatar_contradiction_clause,[],[f211])).
% 0.19/0.28 tff(f285,plain,(
% 0.19/0.28 ( ! [X0 : $int] : (sK2 = X0 | read(sK0,X0) = read(write(sK1,sK3,0),X0) | sK2 = X0) ) | ~spl5_1),
% 0.19/0.28 inference(superposition,[],[f161,f157])).
% 0.19/0.28 tff(f290,plain,(
% 0.19/0.28 ( ! [X0 : $int] : (read(sK0,X0) = read(write(sK1,sK3,0),X0) | sK2 = X0) ) | ~spl5_1),
% 0.19/0.28 inference(duplicate_literal_removal,[],[f285])).
% 0.19/0.28 tff(f309,plain,(
% 0.19/0.28 0 = read(sK0,sK3) | sK2 = sK3 | ~spl5_1),
% 0.19/0.28 inference(superposition,[],[f290,f20])).
% 0.19/0.28 tff(f314,definition,(
% 0.19/0.28 spl5_3 <=> sK2 = sK3),
% 0.19/0.28 introduced(definition,[new_symbols(definition,[spl5_3])],[avatar_definition])).
% 0.19/0.28 tff(f316,plain,(
% 0.19/0.28 sK2 = sK3 | ~spl5_3),
% 0.19/0.28 inference(avatar_component_clause,[],[f314])).
% 0.19/0.28 tff(f318,definition,(
% 0.19/0.28 spl5_4 <=> 0 = read(sK0,sK3)),
% 0.19/0.28 introduced(definition,[new_symbols(definition,[spl5_4])],[avatar_definition])).
% 0.19/0.28 tff(f319,plain,(
% 0.19/0.28 0 != read(sK0,sK3) | spl5_4),
% 0.19/0.28 inference(avatar_component_clause,[],[f318])).
% 0.19/0.28 tff(f320,plain,(
% 0.19/0.28 0 = read(sK0,sK3) | ~spl5_4),
% 0.19/0.28 inference(avatar_component_clause,[],[f318])).
% 0.19/0.28 tff(f322,plain,(
% 0.19/0.28 spl5_3 | spl5_4 | ~spl5_1),
% 0.19/0.28 inference(avatar_split_clause,[],[f309,f159,f318,f314])).
% 0.19/0.28 tff(f334,plain,(
% 0.19/0.28 0 != read(sK0,sK2) | ~spl5_4),
% 0.19/0.28 inference(superposition,[],[f26,f320])).
% 0.19/0.28 tff(f335,plain,(
% 0.19/0.28 $false | ~spl5_4),
% 0.19/0.28 inference(forward_subsumption_resolution,[],[f334,f48])).
% 0.19/0.28 tff(f336,plain,(
% 0.19/0.28 ~spl5_4),
% 0.19/0.28 inference(avatar_contradiction_clause,[],[f335])).
% 0.19/0.28 tff(f337,plain,(
% 0.19/0.28 0 != read(sK0,sK2) | (~spl5_3 | spl5_4)),
% 0.19/0.28 inference(forward_demodulation,[],[f319,f316])).
% 0.19/0.28 tff(f338,plain,(
% 0.19/0.28 $false | (~spl5_3 | spl5_4)),
% 0.19/0.28 inference(forward_subsumption_resolution,[],[f337,f48])).
% 0.19/0.28 tff(f339,plain,(
% 0.19/0.28 ~spl5_3 | spl5_4),
% 0.19/0.28 inference(avatar_contradiction_clause,[],[f338])).
% 0.19/0.28 cnf(s2, plain, spl5_1 | spl5_2, inference(sat_conversion,[],[f167])).
% 0.19/0.28 cnf(s4, plain, ~spl5_2, inference(sat_conversion,[],[f212])).
% 0.19/0.28 cnf(s6, plain, ~spl5_1 | spl5_3 | spl5_4, inference(sat_conversion,[],[f322])).
% 0.19/0.28 cnf(s7, plain, ~spl5_4, inference(sat_conversion,[],[f336])).
% 0.19/0.28 cnf(s8, plain, ~spl5_3 | spl5_4, inference(sat_conversion,[],[f339])).
% 0.19/0.28 cnf(s9, plain, ~spl5_3, inference(rat,[],[s8,s7])).
% 0.19/0.28 cnf(s10, plain, ~spl5_1, inference(rat,[],[s6,s7,s9])).
% 0.19/0.28 cnf(s11, plain, $false, inference(rat,[],[s2,s4,s10])).
% 0.19/0.28 tff(f340,plain,(
% 0.19/0.28 $false),
% 0.19/0.28 inference(avatar_sat_refutation,[],[s11])).
% 0.19/0.28 % SZS output end Proof for theBenchmark
% 0.19/0.28 % (4167514)------------------------------
% 0.19/0.28 % (4167514)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.28 % (4167514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.28 % (4167514)CaDiCaL version: 2.1.3
% 0.19/0.28 % (4167514)Termination reason: Refutation
% 0.19/0.28 % (4167514)Time elapsed: 0.007 s
% 0.19/0.28 % (4167514)Peak memory usage: 13 MB
% 0.19/0.28 % (4167514)Instructions burned: 15 (million)
% 0.19/0.28 % (4167500)Success in time 0.044 s
% 0.19/0.28 % Vampire exiting
%------------------------------------------------------------------------------