%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : DAT005_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 : 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:47:56 AM UTC 2026
% Result : Theorem 28.51s 4.22s
% Output : Refutation 28.51s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : DAT005_1 : TPTP v9.3.1. Released v5.0.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.00/0.11 % Computer : n012.cluster.edu
% 0.00/0.11 % Model : x86_64 x86_64
% 0.00/0.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.11 % Memory : 8046.5625MB
% 0.00/0.11 % OS : Linux 6.8.0-71-generic
% 0.00/0.11 % CPULimit : 300
% 0.00/0.11 % WCLimit : 300
% 0.00/0.11 % DateTime : Tue Sep 29 00:04:49 UTC 2026
% 0.08/0.12 % CPUTime :
% 0.08/0.12 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.13 Running first-order model finding
% 0.08/0.13 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
% 1.98/0.47 % (3913142)Will run a generic schedule for satisfiability detection.
% 1.98/0.47 % (3913148)% WARNING: option uhcvi not known.
% 1.98/0.47 % (3913149)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=780522903:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.98/0.47 % (3913147)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=509591240_2999 on theBenchmark for (2999ds/0Mi)
% 1.98/0.47 % (3913150)dis+10_1_sil=32000:sp=arity:random_seed=1510304199:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.98/0.47 % (3913148)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2366507909:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.98/0.47 % (3913151)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3928870066:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.98/0.47 % (3913152)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2776657118:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.98/0.47 % (3913153)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4007905963:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.98/0.47 % (3913147)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 1.98/0.47 % (3913147)Terminated due to inappropriate strategy.
% 1.98/0.47 % (3913147)------------------------------
% 1.98/0.47 % (3913147)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.98/0.47 % (3913147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.98/0.47 % (3913147)CaDiCaL version: 2.1.3
% 1.98/0.47 % (3913147)Termination reason: Inappropriate
% 1.98/0.47 % (3913147)Time elapsed: 0.0000 s
% 1.98/0.47 % (3913147)Peak memory usage: 10 MB
% 1.98/0.47 % (3913147)------------------------------
% 1.98/0.47 % (3913147)------------------------------
% 1.98/0.47 % (3913161)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2271246329:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.98/0.47 % (3913161)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 1.98/0.47 % (3913161)Terminated due to inappropriate strategy.
% 1.98/0.47 % (3913161)------------------------------
% 1.98/0.47 % (3913161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.98/0.47 % (3913161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.98/0.47 % (3913161)CaDiCaL version: 2.1.3
% 1.98/0.47 % (3913161)Termination reason: Inappropriate
% 1.98/0.47 % (3913161)Time elapsed: 0.0000 s
% 1.98/0.47 % (3913161)Peak memory usage: 10 MB
% 1.98/0.47 % (3913161)------------------------------
% 1.98/0.47 % (3913161)------------------------------
% 1.98/0.47 % (3913163)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3168865656:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 1.98/0.47 % (3913150)Instruction limit reached!
% 1.98/0.47 % (3913150)------------------------------
% 1.98/0.47 % (3913150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.98/0.47 % (3913150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.98/0.47 % (3913150)CaDiCaL version: 2.1.3
% 1.98/0.47 % (3913150)Termination reason: Instruction limit
% 1.98/0.47 % (3913150)Termination phase: Saturation
% 1.98/0.47 % (3913150)Time elapsed: 0.036 s
% 1.98/0.47 % (3913150)Peak memory usage: 12 MB
% 1.98/0.47 % (3913150)Instructions burned: 106 (million)
% 1.98/0.47 % (3913151)Instruction limit reached!
% 1.98/0.47 % (3913151)------------------------------
% 1.98/0.47 % (3913151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.98/0.47 % (3913151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.98/0.47 % (3913151)CaDiCaL version: 2.1.3
% 1.98/0.47 % (3913151)Termination reason: Instruction limit
% 1.98/0.47 % (3913151)Termination phase: Saturation
% 1.98/0.47 % (3913151)Time elapsed: 0.038 s
% 1.98/0.47 % (3913151)Peak memory usage: 12 MB
% 1.98/0.47 % (3913151)Instructions burned: 116 (million)
% 1.98/0.47 % (3913152)Instruction limit reached!
% 1.98/0.47 % (3913152)------------------------------
% 1.98/0.47 % (3913152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.98/0.47 % (3913152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.98/0.47 % (3913152)CaDiCaL version: 2.1.3
% 1.98/0.47 % (3913152)Termination reason: Instruction limit
% 1.98/0.47 % (3913152)Termination phase: Saturation
% 1.98/0.47 % (3913152)Time elapsed: 0.045 s
% 3.65/0.80 % (3913152)Peak memory usage: 13 MB
% 3.65/0.80 % (3913152)Instructions burned: 131 (million)
% 3.65/0.80 % (3913165)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=821454038:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 3.65/0.80 % (3913166)ott-21_1_sil=16000:fs=off:random_seed=1865102370:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 3.65/0.80 % (3913167)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3787642574:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi)
% 3.65/0.80 % (3913153)Instruction limit reached!
% 3.65/0.80 % (3913153)------------------------------
% 3.65/0.80 % (3913153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.65/0.80 % (3913153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.65/0.80 % (3913153)CaDiCaL version: 2.1.3
% 3.65/0.80 % (3913153)Termination reason: Instruction limit
% 3.65/0.80 % (3913153)Termination phase: Saturation
% 3.65/0.80 % (3913153)Time elapsed: 0.062 s
% 3.65/0.80 % (3913153)Peak memory usage: 13 MB
% 3.65/0.80 % (3913153)Instructions burned: 160 (million)
% 3.65/0.80 % (3913163)Instruction limit reached!
% 3.65/0.80 % (3913163)------------------------------
% 3.65/0.80 % (3913163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.65/0.80 % (3913163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.65/0.80 % (3913163)CaDiCaL version: 2.1.3
% 3.65/0.80 % (3913163)Termination reason: Instruction limit
% 3.65/0.80 % (3913163)Termination phase: Saturation
% 3.65/0.80 % (3913163)Time elapsed: 0.046 s
% 3.65/0.80 % (3913163)Peak memory usage: 12 MB
% 3.65/0.80 % (3913163)Instructions burned: 131 (million)
% 3.65/0.80 % (3913171)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3548027891:fmbsr=1.3:i=865:ins=25_2999 on theBenchmark for (2999ds/865Mi)
% 3.65/0.80 % (3913171)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 3.65/0.80 % (3913171)Terminated due to inappropriate strategy.
% 3.65/0.80 % (3913171)------------------------------
% 3.65/0.80 % (3913171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.65/0.80 % (3913171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.65/0.80 % (3913171)CaDiCaL version: 2.1.3
% 3.65/0.80 % (3913171)Termination reason: Inappropriate
% 3.65/0.80 % (3913171)Time elapsed: 0.0000 s
% 3.65/0.80 % (3913171)Peak memory usage: 10 MB
% 3.65/0.80 % (3913171)------------------------------
% 3.65/0.80 % (3913171)------------------------------
% 3.65/0.80 % (3913172)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2814763128:i=1179_2999 on theBenchmark for (2999ds/1179Mi)
% 3.65/0.80 % (3913174)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2887248697:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 3.65/0.80 % (3913174)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 3.65/0.80 % (3913174)Terminated due to inappropriate strategy.
% 3.65/0.80 % (3913174)------------------------------
% 3.65/0.80 % (3913174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.65/0.80 % (3913174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.65/0.80 % (3913174)CaDiCaL version: 2.1.3
% 3.65/0.80 % (3913174)Termination reason: Inappropriate
% 3.65/0.80 % (3913174)Time elapsed: 0.0000 s
% 3.65/0.80 % (3913174)Peak memory usage: 10 MB
% 3.65/0.80 % (3913174)------------------------------
% 3.65/0.80 % (3913174)------------------------------
% 3.65/0.80 % (3913166)Instruction limit reached!
% 3.65/0.80 % (3913166)------------------------------
% 3.65/0.80 % (3913166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.65/0.80 % (3913166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.65/0.80 % (3913166)CaDiCaL version: 2.1.3
% 3.65/0.80 % (3913166)Termination reason: Instruction limit
% 3.65/0.80 % (3913166)Termination phase: Saturation
% 3.65/0.80 % (3913166)Time elapsed: 0.042 s
% 3.65/0.80 % (3913166)Peak memory usage: 12 MB
% 3.65/0.80 % (3913166)Instructions burned: 183 (million)
% 3.65/0.80 % (3913177)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2271694589:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi)
% 3.65/0.80 % (3913178)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=913089166:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi)
% 11.10/1.90 % (3913167)Instruction limit reached!
% 11.10/1.90 % (3913167)------------------------------
% 11.10/1.90 % (3913167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.10/1.90 % (3913167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.10/1.90 % (3913167)CaDiCaL version: 2.1.3
% 11.10/1.90 % (3913167)Termination reason: Instruction limit
% 11.10/1.90 % (3913167)Termination phase: Saturation
% 11.10/1.90 % (3913167)Time elapsed: 0.151 s
% 11.10/1.90 % (3913167)Peak memory usage: 14 MB
% 11.10/1.90 % (3913167)Instructions burned: 481 (million)
% 11.10/1.90 % (3913181)fmb+10_1_sil=64000:random_seed=195345574:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi)
% 11.10/1.90 % (3913181)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 11.10/1.90 % (3913181)Terminated due to inappropriate strategy.
% 11.10/1.90 % (3913181)------------------------------
% 11.10/1.90 % (3913181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.10/1.90 % (3913181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.10/1.90 % (3913181)CaDiCaL version: 2.1.3
% 11.10/1.90 % (3913181)Termination reason: Inappropriate
% 11.10/1.90 % (3913181)Time elapsed: 0.0000 s
% 11.10/1.90 % (3913181)Peak memory usage: 10 MB
% 11.10/1.90 % (3913181)------------------------------
% 11.10/1.90 % (3913181)------------------------------
% 11.10/1.90 % (3913165)Instruction limit reached!
% 11.10/1.90 % (3913165)------------------------------
% 11.10/1.90 % (3913165)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.10/1.90 % (3913165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.10/1.90 % (3913165)CaDiCaL version: 2.1.3
% 11.10/1.90 % (3913165)Termination reason: Instruction limit
% 11.10/1.90 % (3913165)Termination phase: Saturation
% 11.10/1.90 % (3913165)Time elapsed: 0.184 s
% 11.10/1.90 % (3913165)Peak memory usage: 16 MB
% 11.10/1.90 % (3913165)Instructions burned: 688 (million)
% 11.10/1.90 % (3913183)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3351368227:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi)
% 11.10/1.90 % (3913183)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 11.10/1.90 % (3913183)Terminated due to inappropriate strategy.
% 11.10/1.90 % (3913183)------------------------------
% 11.10/1.90 % (3913183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.10/1.90 % (3913183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.10/1.90 % (3913183)CaDiCaL version: 2.1.3
% 11.10/1.90 % (3913183)Termination reason: Inappropriate
% 11.10/1.90 % (3913183)Time elapsed: 0.0000 s
% 11.10/1.90 % (3913183)Peak memory usage: 10 MB
% 11.10/1.90 % (3913183)------------------------------
% 11.10/1.90 % (3913183)------------------------------
% 11.10/1.90 % (3913184)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3975824915:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi)
% 11.10/1.90 % (3913184)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 11.10/1.90 % (3913184)Terminated due to inappropriate strategy.
% 11.10/1.90 % (3913184)------------------------------
% 11.10/1.90 % (3913184)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.10/1.90 % (3913184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.10/1.90 % (3913184)CaDiCaL version: 2.1.3
% 11.10/1.90 % (3913184)Termination reason: Inappropriate
% 11.10/1.90 % (3913184)Time elapsed: 0.0000 s
% 11.10/1.90 % (3913184)Peak memory usage: 10 MB
% 11.10/1.90 % (3913184)------------------------------
% 11.10/1.90 % (3913184)------------------------------
% 11.10/1.90 % (3913186)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2697150076:i=5131_2997 on theBenchmark for (2997ds/5131Mi)
% 11.10/1.90 % (3913189)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2278678654:i=1472:ins=7:fdi=8:gsp=on_2997 on theBenchmark for (2997ds/1472Mi)
% 11.10/1.90 % (3913177)Instruction limit reached!
% 11.10/1.90 % (3913177)------------------------------
% 11.10/1.90 % (3913177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.10/1.90 % (3913177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.10/1.90 % (3913177)CaDiCaL version: 2.1.3
% 11.10/1.90 % (3913177)Termination reason: Instruction limit
% 18.10/2.80 % (3913177)Termination phase: Saturation
% 18.10/2.80 % (3913177)Time elapsed: 0.208 s
% 18.10/2.80 % (3913177)Peak memory usage: 16 MB
% 18.10/2.80 % (3913177)Instructions burned: 697 (million)
% 18.10/2.80 % (3913191)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1274599857:i=6324_2996 on theBenchmark for (2996ds/6324Mi)
% 18.10/2.80 % (3913191)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 18.10/2.80 % (3913191)Terminated due to inappropriate strategy.
% 18.10/2.80 % (3913191)------------------------------
% 18.10/2.80 % (3913191)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.10/2.80 % (3913191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.10/2.80 % (3913191)CaDiCaL version: 2.1.3
% 18.10/2.80 % (3913191)Termination reason: Inappropriate
% 18.10/2.80 % (3913191)Time elapsed: 0.0000 s
% 18.10/2.80 % (3913191)Peak memory usage: 10 MB
% 18.10/2.80 % (3913191)------------------------------
% 18.10/2.80 % (3913191)------------------------------
% 18.10/2.80 % (3913193)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=984596028:fmbsr=2.30978:i=2174_2996 on theBenchmark for (2996ds/2174Mi)
% 18.10/2.80 % (3913193)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 18.10/2.80 % (3913193)Terminated due to inappropriate strategy.
% 18.10/2.80 % (3913193)------------------------------
% 18.10/2.80 % (3913193)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.10/2.80 % (3913193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.10/2.80 % (3913193)CaDiCaL version: 2.1.3
% 18.10/2.80 % (3913193)Termination reason: Inappropriate
% 18.10/2.80 % (3913193)Time elapsed: 0.0000 s
% 18.10/2.80 % (3913193)Peak memory usage: 10 MB
% 18.10/2.80 % (3913193)------------------------------
% 18.10/2.80 % (3913193)------------------------------
% 18.10/2.80 % (3913195)ott-2_1_sil=16000:newcnf=on:random_seed=4090496627:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2996 on theBenchmark for (2996ds/869Mi)
% 18.10/2.80 % (3913178)Instruction limit reached!
% 18.10/2.80 % (3913178)------------------------------
% 18.10/2.80 % (3913178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.10/2.80 % (3913178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.10/2.80 % (3913178)CaDiCaL version: 2.1.3
% 18.10/2.80 % (3913178)Termination reason: Instruction limit
% 18.10/2.80 % (3913178)Termination phase: Saturation
% 18.10/2.80 % (3913178)Time elapsed: 0.278 s
% 18.10/2.80 % (3913178)Peak memory usage: 18 MB
% 18.10/2.80 % (3913178)Instructions burned: 883 (million)
% 18.10/2.80 % (3913197)ott+10_1_sil=32000:tgt=ground:random_seed=2070377131:i=5114:av=off_2995 on theBenchmark for (2995ds/5114Mi)
% 18.10/2.80 % (3913172)Instruction limit reached!
% 18.10/2.80 % (3913172)------------------------------
% 18.10/2.80 % (3913172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.10/2.80 % (3913172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.10/2.80 % (3913172)CaDiCaL version: 2.1.3
% 18.10/2.80 % (3913172)Termination reason: Instruction limit
% 18.10/2.80 % (3913172)Termination phase: Saturation
% 18.10/2.80 % (3913172)Time elapsed: 0.392 s
% 18.10/2.80 % (3913172)Peak memory usage: 17 MB
% 18.10/2.80 % (3913172)Instructions burned: 1181 (million)
% 18.10/2.80 % (3913199)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1445976125:i=54282_2994 on theBenchmark for (2994ds/54282Mi)
% 18.10/2.80 % (3913199)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 18.10/2.80 % (3913199)Terminated due to inappropriate strategy.
% 18.10/2.80 % (3913199)------------------------------
% 18.10/2.80 % (3913199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.10/2.80 % (3913199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.10/2.80 % (3913199)CaDiCaL version: 2.1.3
% 18.10/2.80 % (3913199)Termination reason: Inappropriate
% 18.10/2.80 % (3913199)Time elapsed: 0.0000 s
% 18.10/2.80 % (3913199)Peak memory usage: 10 MB
% 18.10/2.80 % (3913199)------------------------------
% 18.10/2.80 % (3913199)------------------------------
% 18.10/2.80 % (3913201)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2115380109:i=3512:aac=none_2994 on theBenchmark for (2994ds/3512Mi)
% 18.10/2.80 % (3913195)Instruction limit reached!
% 18.10/2.80 % (3913195)------------------------------
% 18.10/2.80 % (3913195)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.10/2.80 % (3913195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.51/4.22 % (3913195)CaDiCaL version: 2.1.3
% 28.51/4.22 % (3913195)Termination reason: Instruction limit
% 28.51/4.22 % (3913195)Termination phase: Saturation
% 28.51/4.22 % (3913195)Time elapsed: 0.290 s
% 28.51/4.22 % (3913195)Peak memory usage: 15 MB
% 28.51/4.22 % (3913195)Instructions burned: 870 (million)
% 28.51/4.22 % (3913203)dis+21_1_sil=32000:sas=cadical:random_seed=876724425:i=3773:amm=off_2993 on theBenchmark for (2993ds/3773Mi)
% 28.51/4.22 % (3913189)Instruction limit reached!
% 28.51/4.22 % (3913189)------------------------------
% 28.51/4.22 % (3913189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.51/4.22 % (3913189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.51/4.22 % (3913189)CaDiCaL version: 2.1.3
% 28.51/4.22 % (3913189)Termination reason: Instruction limit
% 28.51/4.22 % (3913189)Termination phase: Saturation
% 28.51/4.22 % (3913189)Time elapsed: 0.393 s
% 28.51/4.22 % (3913189)Peak memory usage: 24 MB
% 28.51/4.22 % (3913189)Instructions burned: 1472 (million)
% 28.51/4.22 % (3913205)ott+11_1_sil=16000:gs=on:random_seed=3820769707:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2993 on theBenchmark for (2993ds/2251Mi)
% 28.51/4.22 % (3913205)Instruction limit reached!
% 28.51/4.22 % (3913205)------------------------------
% 28.51/4.22 % (3913205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.51/4.22 % (3913205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.51/4.22 % (3913205)CaDiCaL version: 2.1.3
% 28.51/4.22 % (3913205)Termination reason: Instruction limit
% 28.51/4.22 % (3913205)Termination phase: Saturation
% 28.51/4.22 % (3913205)Time elapsed: 0.606 s
% 28.51/4.22 % (3913205)Peak memory usage: 20 MB
% 28.51/4.22 % (3913205)Instructions burned: 2253 (million)
% 28.51/4.22 % (3913207)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2589960914:fmbsr=1.6:i=67534_2986 on theBenchmark for (2986ds/67534Mi)
% 28.51/4.22 % (3913207)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 28.51/4.22 % (3913207)Terminated due to inappropriate strategy.
% 28.51/4.22 % (3913207)------------------------------
% 28.51/4.22 % (3913207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.51/4.22 % (3913207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.51/4.22 % (3913207)CaDiCaL version: 2.1.3
% 28.51/4.22 % (3913207)Termination reason: Inappropriate
% 28.51/4.22 % (3913207)Time elapsed: 0.0000 s
% 28.51/4.22 % (3913207)Peak memory usage: 10 MB
% 28.51/4.22 % (3913207)------------------------------
% 28.51/4.22 % (3913207)------------------------------
% 28.51/4.22 % (3913209)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=428991802:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2986 on theBenchmark for (2986ds/4591Mi)
% 28.51/4.22 % (3913201)Instruction limit reached!
% 28.51/4.22 % (3913201)------------------------------
% 28.51/4.22 % (3913201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.51/4.22 % (3913201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.51/4.22 % (3913201)CaDiCaL version: 2.1.3
% 28.51/4.22 % (3913201)Termination reason: Instruction limit
% 28.51/4.22 % (3913201)Termination phase: Saturation
% 28.51/4.22 % (3913201)Time elapsed: 0.977 s
% 28.51/4.22 % (3913201)Peak memory usage: 29 MB
% 28.51/4.22 % (3913201)Instructions burned: 3515 (million)
% 28.51/4.22 % (3913211)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=710030698:i=29340_2984 on theBenchmark for (2984ds/29340Mi)
% 28.51/4.22 % (3913186)Instruction limit reached!
% 28.51/4.22 % (3913186)------------------------------
% 28.51/4.22 % (3913186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.51/4.22 % (3913186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.51/4.22 % (3913186)CaDiCaL version: 2.1.3
% 28.51/4.22 % (3913186)Termination reason: Instruction limit
% 28.51/4.22 % (3913186)Termination phase: Saturation
% 28.51/4.22 % (3913186)Time elapsed: 1.455 s
% 28.51/4.22 % (3913186)Peak memory usage: 40 MB
% 28.51/4.22 % (3913186)Instructions burned: 5132 (million)
% 28.51/4.22 % (3913213)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1643071298:i=5211_2982 on theBenchmark for (2982ds/5211Mi)
% 28.51/4.22 % (3913203)Instruction limit reached!
% 28.51/4.22 % (3913203)------------------------------
% 28.51/4.22 % (3913203)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.51/4.22 % (3913203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.51/4.22 % (3913203)CaDiCaL version: 2.1.3
% 28.51/4.22 % (3913203)Termination reason: Instruction limit
% 28.51/4.22 % (3913203)Termination phase: Saturation
% 28.51/4.22 % (3913203)Time elapsed: 1.087 s
% 28.51/4.22 % (3913203)Peak memory usage: 32 MB
% 28.51/4.22 % (3913203)Instructions burned: 3776 (million)
% 28.51/4.22 % (3913215)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3196072733:i=5497:nm=2_2982 on theBenchmark for (2982ds/5497Mi)
% 28.51/4.22 % (3913215)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 28.51/4.22 % (3913215)Terminated due to inappropriate strategy.
% 28.51/4.22 % (3913215)------------------------------
% 28.51/4.22 % (3913215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.51/4.22 % (3913215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.51/4.22 % (3913215)CaDiCaL version: 2.1.3
% 28.51/4.22 % (3913215)Termination reason: Inappropriate
% 28.51/4.22 % (3913215)Time elapsed: 0.0000 s
% 28.51/4.22 % (3913215)Peak memory usage: 10 MB
% 28.51/4.22 % (3913215)------------------------------
% 28.51/4.22 % (3913215)------------------------------
% 28.51/4.22 % (3913217)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=483334682:fmbsr=2:i=46332_2982 on theBenchmark for (2982ds/46332Mi)
% 28.51/4.22 % (3913217)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 28.51/4.22 % (3913217)Terminated due to inappropriate strategy.
% 28.51/4.22 % (3913217)------------------------------
% 28.51/4.22 % (3913217)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.51/4.22 % (3913217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.51/4.22 % (3913217)CaDiCaL version: 2.1.3
% 28.51/4.22 % (3913217)Termination reason: Inappropriate
% 28.51/4.22 % (3913217)Time elapsed: 0.0000 s
% 28.51/4.22 % (3913217)Peak memory usage: 10 MB
% 28.51/4.22 % (3913217)------------------------------
% 28.51/4.22 % (3913217)------------------------------
% 28.51/4.22 % (3913219)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3838322051:i=14071_2982 on theBenchmark for (2982ds/14071Mi)
% 28.51/4.22 % (3913219)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 28.51/4.22 % (3913219)Terminated due to inappropriate strategy.
% 28.51/4.22 % (3913219)------------------------------
% 28.51/4.22 % (3913219)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.51/4.22 % (3913219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.51/4.22 % (3913219)CaDiCaL version: 2.1.3
% 28.51/4.22 % (3913219)Termination reason: Inappropriate
% 28.51/4.22 % (3913219)Time elapsed: 0.0000 s
% 28.51/4.22 % (3913219)Peak memory usage: 10 MB
% 28.51/4.22 % (3913219)------------------------------
% 28.51/4.22 % (3913219)------------------------------
% 28.51/4.22 % (3913221)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1763081360:i=22565:add=on:rawr=on_2982 on theBenchmark for (2982ds/22565Mi)
% 28.51/4.22 % (3913197)Instruction limit reached!
% 28.51/4.22 % (3913197)------------------------------
% 28.51/4.22 % (3913197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.51/4.22 % (3913197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.51/4.22 % (3913197)CaDiCaL version: 2.1.3
% 28.51/4.22 % (3913197)Termination reason: Instruction limit
% 28.51/4.22 % (3913197)Termination phase: Saturation
% 28.51/4.22 % (3913197)Time elapsed: 1.697 s
% 28.51/4.22 % (3913197)Peak memory usage: 29 MB
% 28.51/4.22 % (3913197)Instructions burned: 5114 (million)
% 28.51/4.22 % (3913223)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=482210311:i=8173:av=off_2978 on theBenchmark for (2978ds/8173Mi)
% 28.51/4.22 % (3913209)Instruction limit reached!
% 28.51/4.22 % (3913209)------------------------------
% 28.51/4.22 % (3913209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.51/4.22 % (3913209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.51/4.22 % (3913209)CaDiCaL version: 2.1.3
% 28.51/4.22 % (3913209)Termination reason: Instruction limit
% 28.51/4.22 % (3913209)Termination phase: Saturation
% 28.51/4.22 % (3913209)Time elapsed: 1.318 s
% 28.51/4.22 % (3913209)Peak memory usage: 51 MB
% 28.51/4.22 % (3913209)Instructions burned: 4594 (million)
% 28.51/4.22 % (3913225)dis+10_16:1_sil=16000:random_seed=1711719399:i=9155:fsr=off_2973 on theBenchmark for (2973ds/9155Mi)
% 28.51/4.22 % (3913213)Instruction limit reached!
% 28.51/4.22 % (3913213)------------------------------
% 28.51/4.22 % (3913213)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.51/4.22 % (3913213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.51/4.22 % (3913213)CaDiCaL version: 2.1.3
% 28.51/4.22 % (3913213)Termination reason: Instruction limit
% 28.51/4.22 % (3913213)Termination phase: Saturation
% 28.51/4.22 % (3913213)Time elapsed: 1.496 s
% 28.51/4.22 % (3913213)Peak memory usage: 44 MB
% 28.51/4.22 % (3913213)Instructions burned: 5212 (million)
% 28.51/4.22 % (3913227)ott-3_8_sil=64000:random_seed=250822702:i=20139:bs=on_2967 on theBenchmark for (2967ds/20139Mi)
% 28.51/4.22 % (3913225) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3913142-3913225"...
% 28.51/4.22 % (3913225)...printing done.
% 28.51/4.22 % (3913225)Refutation found. Thanks to Tanya!
% 28.51/4.22 % SZS status Theorem for theBenchmark
% 28.51/4.22 % SZS output start Proof for theBenchmark
% 28.51/4.22 tff(type_def_5, type, array: $tType).
% 28.51/4.22 tff(func_def_0, type, read: (array * $int) > $int).
% 28.51/4.22 tff(func_def_1, type, write: (array * $int * $int) > array).
% 28.51/4.22 tff(func_def_13, type, sK0: array).
% 28.51/4.22 tff(func_def_14, type, sK1: array).
% 28.51/4.22 tff(func_def_15, type, sK2: $int).
% 28.51/4.22 tff(f1,axiom,(
% 28.51/4.22 ! [X0 : array,X1 : $int,X2 : $int] : read(write(X0,X1,X2),X1) = X2),
% 28.51/4.22 file('/export/starexec/sandbox2/benchmark/Axioms/DAT001_0.ax',ax1)).
% 28.51/4.22 tff(f2,axiom,(
% 28.51/4.22 ! [X0 : array,X1 : $int,X2 : $int,X3 : $int] : (X1 = X2 | read(write(X0,X1,X3),X2) = read(X0,X2))),
% 28.51/4.22 file('/export/starexec/sandbox2/benchmark/Axioms/DAT001_0.ax',ax2)).
% 28.51/4.22 tff(f3,conjecture,(
% 28.51/4.22 ! [X0 : array,X1 : array,X2 : $int] : ((X0 = write(write(write(write(X1,3,33),4,444),5,55),4,44) & $lesseq(3,X2) & $lesseq(X2,4)) => ($lesseq(33,read(X0,X2)) & $lesseq(read(X0,X2),44)))),
% 28.51/4.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1)).
% 28.51/4.22 tff(f4,negated_conjecture,(
% 28.51/4.22 ~ ! [X0 : array,X1 : array,X2 : $int] : ((X0 = write(write(write(write(X1,3,33),4,444),5,55),4,44) & $lesseq(3,X2) & $lesseq(X2,4)) => ($lesseq(33,read(X0,X2)) & $lesseq(read(X0,X2),44)))),
% 28.51/4.22 inference(negated_conjecture,[status(cth)],[f3])).
% 28.51/4.22 tff(f5,plain,(
% 28.51/4.22 ~ ! [X0 : array,X1 : array,X2 : $int] : ((X0 = write(write(write(write(X1,3,33),4,444),5,55),4,44) & ~$less(X2,3) & ~$less(4,X2)) => (~$less(read(X0,X2),33) & ~$less(44,read(X0,X2))))),
% 28.51/4.22 inference(theory_normalization,[],[f4])).
% 28.51/4.22 tff(f11,definition,(
% 28.51/4.22 ( ! [X0 : $int] : (~$less(X0,X0)) )),
% 28.51/4.22 introduced(theory,[tha_non-reflexivity])).
% 28.51/4.22 tff(f12,definition,(
% 28.51/4.22 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X1,X2) | ~$less(X0,X1) | $less(X0,X2)) )),
% 28.51/4.22 introduced(theory,[tha_transitivity])).
% 28.51/4.22 tff(f13,definition,(
% 28.51/4.22 ( ! [X0 : $int,X1 : $int] : ($less(X1,X0) | $less(X0,X1) | X0 = X1) )),
% 28.51/4.22 introduced(theory,[tha_order_totality])).
% 28.51/4.22 tff(f17,definition,(
% 28.51/4.22 ( ! [X0 : $int,X1 : $int] : (~$less(X1,$sum(X0,1)) | ~$less(X0,X1)) )),
% 28.51/4.22 introduced(theory,[tha_extra_integer_ordering])).
% 28.51/4.22 tff(f18,plain,(
% 28.51/4.22 ? [X0 : array,X1 : array,X2 : $int] : (($less(read(X0,X2),33) | $less(44,read(X0,X2))) & (X0 = write(write(write(write(X1,3,33),4,444),5,55),4,44) & ~$less(X2,3) & ~$less(4,X2)))),
% 28.51/4.22 inference(ennf_transformation,[],[f5])).
% 28.51/4.22 tff(f19,plain,(
% 28.51/4.22 ? [X0 : array,X1 : array,X2 : $int] : (($less(read(X0,X2),33) | $less(44,read(X0,X2))) & X0 = write(write(write(write(X1,3,33),4,444),5,55),4,44) & ~$less(X2,3) & ~$less(4,X2))),
% 28.51/4.22 inference(flattening,[],[f18])).
% 28.51/4.22 tff(f20,plain,(
% 28.51/4.22 ($less(read(sK0,sK2),33) | $less(44,read(sK0,sK2))) & sK0 = write(write(write(write(sK1,3,33),4,444),5,55),4,44) & ~$less(sK2,3) & ~$less(4,sK2)),
% 28.51/4.22 inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2)],[f19])).
% 28.51/4.22 tff(f21,plain,(
% 28.51/4.22 ( ! [X2 : $int,X0 : array,X1 : $int] : (read(write(X0,X1,X2),X1) = X2) )),
% 28.51/4.22 inference(cnf_transformation,[],[f1])).
% 28.51/4.22 tff(f22,plain,(
% 28.51/4.22 ( ! [X2 : $int,X3 : $int,X0 : array,X1 : $int] : (read(write(X0,X1,X3),X2) = read(X0,X2) | X1 = X2) )),
% 28.51/4.22 inference(cnf_transformation,[],[f2])).
% 28.51/4.22 tff(f23,plain,(
% 28.51/4.22 ~$less(4,sK2)),
% 28.51/4.22 inference(cnf_transformation,[],[f20])).
% 28.51/4.22 tff(f24,plain,(
% 28.51/4.22 ~$less(sK2,3)),
% 28.51/4.22 inference(cnf_transformation,[],[f20])).
% 28.51/4.22 tff(f25,plain,(
% 28.51/4.22 sK0 = write(write(write(write(sK1,3,33),4,444),5,55),4,44)),
% 28.51/4.22 inference(cnf_transformation,[],[f20])).
% 28.51/4.22 tff(f26,plain,(
% 28.51/4.22 $less(read(sK0,sK2),33) | $less(44,read(sK0,sK2))),
% 28.51/4.22 inference(cnf_transformation,[],[f20])).
% 28.51/4.22 tff(f28,definition,(
% 28.51/4.22 spl3_1 <=> $less(44,read(sK0,sK2))),
% 28.51/4.22 introduced(definition,[new_symbols(definition,[spl3_1])],[avatar_definition])).
% 28.51/4.22 tff(f30,plain,(
% 28.51/4.22 $less(44,read(sK0,sK2)) | ~spl3_1),
% 28.51/4.22 inference(avatar_component_clause,[],[f28])).
% 28.51/4.22 tff(f32,definition,(
% 28.51/4.22 spl3_2 <=> $less(read(sK0,sK2),33)),
% 28.51/4.22 introduced(definition,[new_symbols(definition,[spl3_2])],[avatar_definition])).
% 28.51/4.22 tff(f34,plain,(
% 28.51/4.22 $less(read(sK0,sK2),33) | ~spl3_2),
% 28.51/4.22 inference(avatar_component_clause,[],[f32])).
% 28.51/4.22 tff(f35,plain,(
% 28.51/4.22 spl3_1 | spl3_2),
% 28.51/4.22 inference(avatar_split_clause,[],[f26,f32,f28])).
% 28.51/4.22 tff(f47,plain,(
% 28.51/4.22 44 = read(sK0,4)),
% 28.51/4.22 inference(superposition,[],[f21,f25])).
% 28.51/4.22 tff(f50,plain,(
% 28.51/4.22 $less(3,sK2) | 3 = sK2),
% 28.51/4.22 inference(resolution,[],[f13,f24])).
% 28.51/4.22 tff(f51,plain,(
% 28.51/4.22 ( ! [X0 : $int,X1 : $int] : ($less($sum(X1,1),X0) | $sum(X1,1) = X0 | ~$less(X1,X0)) )),
% 28.51/4.22 inference(resolution,[],[f13,f17])).
% 28.51/4.22 tff(f52,plain,(
% 28.51/4.22 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X2,X0) | X0 = X1 | $less(X1,X0) | $less(X2,X1)) )),
% 28.51/4.22 inference(resolution,[],[f13,f12])).
% 28.51/4.22 tff(f53,plain,(
% 28.51/4.22 $less(3,sK2) | 3 = sK2),
% 28.51/4.22 inference(resolution,[],[f13,f24])).
% 28.51/4.22 tff(f58,definition,(
% 28.51/4.22 spl3_3 <=> 3 = sK2),
% 28.51/4.22 introduced(definition,[new_symbols(definition,[spl3_3])],[avatar_definition])).
% 28.51/4.22 tff(f60,plain,(
% 28.51/4.22 3 = sK2 | ~spl3_3),
% 28.51/4.22 inference(avatar_component_clause,[],[f58])).
% 28.51/4.22 tff(f62,definition,(
% 28.51/4.22 spl3_4 <=> $less(3,sK2)),
% 28.51/4.22 introduced(definition,[new_symbols(definition,[spl3_4])],[avatar_definition])).
% 28.51/4.22 tff(f64,plain,(
% 28.51/4.22 $less(3,sK2) | ~spl3_4),
% 28.51/4.22 inference(avatar_component_clause,[],[f62])).
% 28.51/4.22 tff(f65,plain,(
% 28.51/4.22 spl3_3 | spl3_4),
% 28.51/4.22 inference(avatar_split_clause,[],[f53,f62,f58])).
% 28.51/4.22 tff(f66,plain,(
% 28.51/4.22 spl3_3 | spl3_4),
% 28.51/4.22 inference(avatar_split_clause,[],[f50,f62,f58])).
% 28.51/4.22 tff(f115,plain,(
% 28.51/4.22 ( ! [X0 : $int] : (read(write(write(write(sK1,3,33),4,444),5,55),X0) = read(sK0,X0) | 4 = X0) )),
% 28.51/4.22 inference(superposition,[],[f22,f25])).
% 28.51/4.22 tff(f123,plain,(
% 28.51/4.22 ( ! [X0 : $int] : (read(sK0,X0) = read(write(write(sK1,3,33),4,444),X0) | 4 = X0 | 5 = X0) )),
% 28.51/4.22 inference(superposition,[],[f115,f22])).
% 28.51/4.22 tff(f621,plain,(
% 28.51/4.22 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X0,X1) | $sum(X0,1) = X1 | X1 = X2 | $less(X2,X1) | $less($sum(X0,1),X2)) )),
% 28.51/4.22 inference(resolution,[],[f51,f52])).
% 28.51/4.22 tff(f1008,plain,(
% 28.51/4.22 ( ! [X0 : $int] : (read(sK0,X0) = read(write(sK1,3,33),X0) | 4 = X0 | 4 = X0 | 5 = X0) )),
% 28.51/4.22 inference(superposition,[],[f22,f123])).
% 28.51/4.22 tff(f1009,plain,(
% 28.51/4.22 ( ! [X0 : $int] : (read(sK0,X0) = read(write(sK1,3,33),X0) | 4 = X0 | 5 = X0) )),
% 28.51/4.22 inference(duplicate_literal_removal,[],[f1008])).
% 28.51/4.22 tff(f4759,plain,(
% 28.51/4.22 ( ! [X0 : $int] : ($less(X0,read(sK0,sK2)) | ~$less(X0,44)) ) | ~spl3_1),
% 28.51/4.22 inference(resolution,[],[f30,f12])).
% 28.51/4.22 tff(f4764,definition,(
% 28.51/4.22 spl3_15 <=> 33 = read(sK0,sK2)),
% 28.51/4.22 introduced(definition,[new_symbols(definition,[spl3_15])],[avatar_definition])).
% 28.51/4.22 tff(f4765,plain,(
% 28.51/4.22 33 != read(sK0,sK2) | spl3_15),
% 28.51/4.22 inference(avatar_component_clause,[],[f4764])).
% 28.51/4.22 tff(f4766,plain,(
% 28.51/4.22 33 = read(sK0,sK2) | ~spl3_15),
% 28.51/4.22 inference(avatar_component_clause,[],[f4764])).
% 28.51/4.22 tff(f4785,plain,(
% 28.51/4.22 ~$less(read(sK0,sK2),44) | ~spl3_1),
% 28.51/4.22 inference(resolution,[],[f4759,f11])).
% 28.51/4.22 tff(f56566,plain,(
% 28.51/4.22 33 = read(sK0,3) | (~spl3_3 | ~spl3_15)),
% 28.51/4.22 inference(forward_demodulation,[],[f4766,f60])).
% 28.51/4.22 tff(f56599,plain,(
% 28.51/4.22 $less(read(sK0,3),33) | (~spl3_2 | ~spl3_3)),
% 28.51/4.22 inference(forward_demodulation,[],[f34,f60])).
% 28.51/4.22 tff(f56629,plain,(
% 28.51/4.22 ~$less(read(sK0,3),44) | (~spl3_1 | ~spl3_3)),
% 28.51/4.22 inference(forward_demodulation,[],[f4785,f60])).
% 28.51/4.22 tff(f56646,plain,(
% 28.51/4.22 ~$less(33,44) | (~spl3_1 | ~spl3_3 | ~spl3_15)),
% 28.51/4.22 inference(forward_demodulation,[],[f56629,f56566])).
% 28.51/4.22 tff(f56647,plain,(
% 28.51/4.22 $false | (~spl3_1 | ~spl3_3 | ~spl3_15)),
% 28.51/4.22 inference(evaluation,[],[f56646])).
% 28.51/4.22 tff(f56648,plain,(
% 28.51/4.22 ~spl3_1 | ~spl3_3 | ~spl3_15),
% 28.51/4.22 inference(avatar_contradiction_clause,[],[f56647])).
% 28.51/4.22 tff(f56653,plain,(
% 28.51/4.22 33 != read(sK0,3) | (~spl3_3 | spl3_15)),
% 28.51/4.22 inference(forward_demodulation,[],[f4765,f60])).
% 28.51/4.22 tff(f88708,definition,(
% 28.51/4.22 spl3_37 <=> 33 = read(sK0,3)),
% 28.51/4.22 introduced(definition,[new_symbols(definition,[spl3_37])],[avatar_definition])).
% 28.51/4.22 tff(f88710,plain,(
% 28.51/4.22 33 = read(sK0,3) | ~spl3_37),
% 28.51/4.22 inference(avatar_component_clause,[],[f88708])).
% 28.51/4.22 tff(f93866,plain,(
% 28.51/4.22 33 = read(sK0,3) | 3 = 4 | 3 = 5),
% 28.51/4.22 inference(superposition,[],[f21,f1009])).
% 28.51/4.22 tff(f93868,plain,(
% 28.51/4.22 33 = read(sK0,3)),
% 28.51/4.22 inference(evaluation,[],[f93866])).
% 28.51/4.22 tff(f93870,plain,(
% 28.51/4.22 spl3_37),
% 28.51/4.22 inference(avatar_split_clause,[],[f93868,f88708])).
% 28.51/4.22 tff(f98687,plain,(
% 28.51/4.22 $less(33,33) | (~spl3_2 | ~spl3_3 | ~spl3_37)),
% 28.51/4.22 inference(superposition,[],[f56599,f88710])).
% 28.51/4.22 tff(f98688,plain,(
% 28.51/4.22 33 != 33 | (~spl3_3 | spl3_15 | ~spl3_37)),
% 28.51/4.22 inference(superposition,[],[f56653,f88710])).
% 28.51/4.22 tff(f98739,plain,(
% 28.51/4.22 $false | (~spl3_3 | spl3_15 | ~spl3_37)),
% 28.51/4.22 inference(trivial_inequality_removal,[],[f98688])).
% 28.51/4.22 tff(f98740,plain,(
% 28.51/4.22 ~spl3_3 | spl3_15 | ~spl3_37),
% 28.51/4.22 inference(avatar_contradiction_clause,[],[f98739])).
% 28.51/4.22 tff(f98741,plain,(
% 28.51/4.22 $false | (~spl3_2 | ~spl3_3 | ~spl3_37)),
% 28.51/4.22 inference(evaluation,[],[f98687])).
% 28.51/4.22 tff(f98742,plain,(
% 28.51/4.22 ~spl3_2 | ~spl3_3 | ~spl3_37),
% 28.51/4.22 inference(avatar_contradiction_clause,[],[f98741])).
% 28.51/4.22 tff(f98797,plain,(
% 28.51/4.22 ( ! [X0 : $int] : (sK2 = $sum(3,1) | sK2 = X0 | $less(X0,sK2) | $less($sum(3,1),X0)) ) | ~spl3_4),
% 28.51/4.22 inference(resolution,[],[f64,f621])).
% 28.51/4.22 tff(f98807,plain,(
% 28.51/4.22 ( ! [X0 : $int] : (4 = sK2 | sK2 = X0 | $less(X0,sK2) | $less(4,X0)) ) | ~spl3_4),
% 28.51/4.22 inference(evaluation,[],[f98797])).
% 28.51/4.22 tff(f98814,definition,(
% 28.51/4.22 spl3_151 <=> 4 = sK2),
% 28.51/4.22 introduced(definition,[new_symbols(definition,[spl3_151])],[avatar_definition])).
% 28.51/4.22 tff(f98816,plain,(
% 28.51/4.22 4 = sK2 | ~spl3_151),
% 28.51/4.22 inference(avatar_component_clause,[],[f98814])).
% 28.51/4.22 tff(f98819,definition,(
% 28.51/4.22 spl3_152 <=> ! [X0 : $int] : (sK2 = X0 | $less(4,X0) | $less(X0,sK2))),
% 28.51/4.22 introduced(definition,[new_symbols(definition,[spl3_152])],[avatar_definition])).
% 28.51/4.22 tff(f98820,plain,(
% 28.51/4.22 ( ! [X0 : $int] : ($less(4,X0) | $less(X0,sK2) | sK2 = X0) ) | ~spl3_152),
% 28.51/4.22 inference(avatar_component_clause,[],[f98819])).
% 28.51/4.22 tff(f98821,plain,(
% 28.51/4.22 spl3_152 | spl3_151 | ~spl3_4),
% 28.51/4.22 inference(avatar_split_clause,[],[f98807,f62,f98814,f98819])).
% 28.51/4.22 tff(f99229,plain,(
% 28.51/4.22 $less(read(sK0,4),33) | (~spl3_2 | ~spl3_151)),
% 28.51/4.22 inference(superposition,[],[f34,f98816])).
% 28.51/4.22 tff(f99246,plain,(
% 28.51/4.22 $less(44,33) | (~spl3_2 | ~spl3_151)),
% 28.51/4.22 inference(forward_demodulation,[],[f99229,f47])).
% 28.51/4.22 tff(f99247,plain,(
% 28.51/4.22 $false | (~spl3_2 | ~spl3_151)),
% 28.51/4.22 inference(evaluation,[],[f99246])).
% 28.51/4.22 tff(f99248,plain,(
% 28.51/4.22 ~spl3_2 | ~spl3_151),
% 28.51/4.22 inference(avatar_contradiction_clause,[],[f99247])).
% 28.51/4.22 tff(f100368,plain,(
% 28.51/4.22 $less(4,4) | 4 = sK2 | ~spl3_152),
% 28.51/4.22 inference(resolution,[],[f98820,f23])).
% 28.51/4.22 tff(f100379,plain,(
% 28.51/4.22 4 = sK2 | ~spl3_152),
% 28.51/4.22 inference(evaluation,[],[f100368])).
% 28.51/4.22 tff(f100383,plain,(
% 28.51/4.22 spl3_151 | ~spl3_152),
% 28.51/4.22 inference(avatar_split_clause,[],[f100379,f98819,f98814])).
% 28.51/4.22 tff(f100447,plain,(
% 28.51/4.22 $less(44,read(sK0,4)) | (~spl3_1 | ~spl3_151)),
% 28.51/4.22 inference(superposition,[],[f30,f98816])).
% 28.51/4.22 tff(f100463,plain,(
% 28.51/4.22 $less(44,44) | (~spl3_1 | ~spl3_151)),
% 28.51/4.22 inference(forward_demodulation,[],[f100447,f47])).
% 28.51/4.22 tff(f100464,plain,(
% 28.51/4.22 $false | (~spl3_1 | ~spl3_151)),
% 28.51/4.22 inference(evaluation,[],[f100463])).
% 28.51/4.22 tff(f100465,plain,(
% 28.51/4.22 ~spl3_1 | ~spl3_151),
% 28.51/4.22 inference(avatar_contradiction_clause,[],[f100464])).
% 28.51/4.22 cnf(s1, plain, spl3_1 | spl3_2, inference(sat_conversion,[],[f35])).
% 28.51/4.22 cnf(s2, plain, spl3_3 | spl3_4, inference(sat_conversion,[],[f65])).
% 28.51/4.22 cnf(s3, plain, spl3_3 | spl3_4, inference(sat_conversion,[],[f66])).
% 28.51/4.22 cnf(s48, plain, ~spl3_1 | ~spl3_3 | ~spl3_15, inference(sat_conversion,[],[f56648])).
% 28.51/4.22 cnf(s132, plain, spl3_37, inference(sat_conversion,[],[f93870])).
% 28.51/4.22 cnf(s244, plain, ~spl3_3 | spl3_15 | ~spl3_37, inference(sat_conversion,[],[f98740])).
% 28.51/4.22 cnf(s245, plain, ~spl3_2 | ~spl3_3 | ~spl3_37, inference(sat_conversion,[],[f98742])).
% 28.51/4.22 cnf(s251, plain, ~spl3_4 | spl3_151 | spl3_152, inference(sat_conversion,[],[f98821])).
% 28.51/4.22 cnf(s259, plain, ~spl3_2 | ~spl3_151, inference(sat_conversion,[],[f99248])).
% 28.51/4.22 cnf(s269, plain, spl3_151 | ~spl3_152, inference(sat_conversion,[],[f100383])).
% 28.51/4.22 cnf(s280, plain, ~spl3_1 | ~spl3_151, inference(sat_conversion,[],[f100465])).
% 28.51/4.22 cnf(s296, plain, ~spl3_2, inference(rat,[],[s2,s251,s269,s245,s259,s132])).
% 28.51/4.22 cnf(s298, plain, spl3_1, inference(rat,[],[s1,s296])).
% 28.51/4.22 cnf(s299, plain, ~spl3_151, inference(rat,[],[s280,s298])).
% 28.51/4.22 cnf(s301, plain, ~spl3_152, inference(rat,[],[s269,s299])).
% 28.51/4.22 cnf(s302, plain, ~spl3_4, inference(rat,[],[s251,s301,s299])).
% 28.51/4.22 cnf(s303, plain, spl3_3, inference(rat,[],[s3,s302])).
% 28.51/4.22 cnf(s304, plain, spl3_15, inference(rat,[],[s244,s132,s303])).
% 28.51/4.22 cnf(s305, plain, $false, inference(rat,[],[s48,s298,s304,s303])).
% 28.51/4.22 tff(f100466,plain,(
% 28.51/4.22 $false),
% 28.51/4.22 inference(avatar_sat_refutation,[],[s305])).
% 28.51/4.22 % SZS output end Proof for theBenchmark
% 28.51/4.22 % (3913225)------------------------------
% 28.51/4.22 % (3913225)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.51/4.22 % (3913225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.51/4.22 % (3913225)CaDiCaL version: 2.1.3
% 28.51/4.22 % (3913225)Termination reason: Refutation
% 28.51/4.22 % (3913225)Time elapsed: 1.410 s
% 28.51/4.22 % (3913225)Peak memory usage: 35 MB
% 28.51/4.22 % (3913225)Instructions burned: 5158 (million)
% 28.51/4.22 % (3913142)Success in time 4.083 s
% 28.51/4.22 % Vampire exiting
%------------------------------------------------------------------------------