%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYO524_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 02:31:24 PM UTC 2026
% Result : Theorem 2.91s 1.03s
% Output : Refutation 2.91s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SYO524_1 : TPTP v9.3.1. Released v5.0.0.
% 0.00/0.10 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.28/0.32 % Computer : n016.cluster.edu
% 0.28/0.32 % Model : x86_64 x86_64
% 0.28/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.28/0.32 % Memory : 8046.5625MB
% 0.28/0.32 % OS : Linux 6.8.0-71-generic
% 0.28/0.33 % CPULimit : 300
% 0.28/0.33 % WCLimit : 300
% 0.28/0.33 % DateTime : Mon Sep 28 17:52:04 UTC 2026
% 0.28/0.33 % CPUTime :
% 0.28/0.33 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.28/0.39 Running first-order model finding
% 0.28/0.39 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
% 2.91/1.03 % (3836824)Will run a generic schedule for satisfiability detection.
% 2.91/1.03 % (3836834)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1817785857:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 2.91/1.03 % (3836830)% WARNING: option uhcvi not known.
% 2.91/1.03 % (3836835)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3675280021:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 2.91/1.03 % (3836832)dis+10_1_sil=32000:sp=arity:random_seed=2015051911:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 2.91/1.03 % (3836833)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=35717285:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 2.91/1.03 % (3836830)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=443882107:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 2.91/1.03 % (3836831)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3744017935:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 2.91/1.03 % (3836829)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1304105331_2999 on theBenchmark for (2999ds/0Mi)
% 2.91/1.03 % (3836829)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 2.91/1.03 % (3836829)Terminated due to inappropriate strategy.
% 2.91/1.03 % (3836829)------------------------------
% 2.91/1.03 % (3836829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.91/1.03 % (3836829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.91/1.03 % (3836829)CaDiCaL version: 2.1.3
% 2.91/1.03 % (3836829)Termination reason: Inappropriate
% 2.91/1.03 % (3836829)Time elapsed: 0.001 s
% 2.91/1.03 % (3836829)Peak memory usage: 10 MB
% 2.91/1.03 % (3836829)------------------------------
% 2.91/1.03 % (3836829)------------------------------
% 2.91/1.03 % (3836843)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1274947318:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 2.91/1.03 % (3836843)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 2.91/1.03 % (3836843)Terminated due to inappropriate strategy.
% 2.91/1.03 % (3836843)------------------------------
% 2.91/1.03 % (3836843)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.91/1.03 % (3836843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.91/1.03 % (3836843)CaDiCaL version: 2.1.3
% 2.91/1.03 % (3836843)Termination reason: Inappropriate
% 2.91/1.03 % (3836843)Time elapsed: 0.001 s
% 2.91/1.03 % (3836843)Peak memory usage: 10 MB
% 2.91/1.03 % (3836843)------------------------------
% 2.91/1.03 % (3836843)------------------------------
% 2.91/1.03 % (3836834)Instruction limit reached!
% 2.91/1.03 % (3836834)------------------------------
% 2.91/1.03 % (3836834)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.91/1.03 % (3836834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.91/1.03 % (3836834)CaDiCaL version: 2.1.3
% 2.91/1.03 % (3836834)Termination reason: Instruction limit
% 2.91/1.03 % (3836834)Termination phase: Saturation
% 2.91/1.03 % (3836834)Time elapsed: 0.070 s
% 2.91/1.03 % (3836834)Peak memory usage: 13 MB
% 2.91/1.03 % (3836834)Instructions burned: 131 (million)
% 2.91/1.03 % (3836846)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=2949006149:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 2.91/1.03 % (3836845)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=28819790:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 2.91/1.03 % (3836832)Instruction limit reached!
% 2.91/1.03 % (3836832)------------------------------
% 2.91/1.03 % (3836832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.91/1.03 % (3836832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.91/1.03 % (3836832)CaDiCaL version: 2.1.3
% 2.91/1.03 % (3836832)Termination reason: Instruction limit
% 2.91/1.03 % (3836832)Termination phase: Saturation
% 2.91/1.03 % (3836832)Time elapsed: 0.104 s
% 2.91/1.03 % (3836832)Peak memory usage: 12 MB
% 2.91/1.03 % (3836832)Instructions burned: 103 (million)
% 2.91/1.03 % (3836833)Instruction limit reached!
% 2.91/1.03 % (3836833)------------------------------
% 2.91/1.03 % (3836833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.91/1.03 % (3836833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.91/1.03 % (3836833)CaDiCaL version: 2.1.3
% 2.91/1.03 % (3836833)Termination reason: Instruction limit
% 2.91/1.03 % (3836833)Termination phase: Saturation
% 2.91/1.03 % (3836833)Time elapsed: 0.112 s
% 2.91/1.03 % (3836833)Peak memory usage: 12 MB
% 2.91/1.03 % (3836833)Instructions burned: 116 (million)
% 2.91/1.03 % (3836849)ott-21_1_sil=16000:fs=off:random_seed=2364944689:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 2.91/1.03 % (3836850)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2134895190:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 2.91/1.03 % (3836835)Instruction limit reached!
% 2.91/1.03 % (3836835)------------------------------
% 2.91/1.03 % (3836835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.91/1.03 % (3836835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.91/1.03 % (3836835)CaDiCaL version: 2.1.3
% 2.91/1.03 % (3836835)Termination reason: Instruction limit
% 2.91/1.03 % (3836835)Termination phase: Saturation
% 2.91/1.03 % (3836835)Time elapsed: 0.179 s
% 2.91/1.03 % (3836835)Peak memory usage: 13 MB
% 2.91/1.03 % (3836835)Instructions burned: 159 (million)
% 2.91/1.03 % (3836853)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1639727992:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 2.91/1.03 % (3836853)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 2.91/1.03 % (3836853)Terminated due to inappropriate strategy.
% 2.91/1.03 % (3836853)------------------------------
% 2.91/1.03 % (3836853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.91/1.03 % (3836853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.91/1.03 % (3836853)CaDiCaL version: 2.1.3
% 2.91/1.03 % (3836853)Termination reason: Inappropriate
% 2.91/1.03 % (3836853)Time elapsed: 0.001 s
% 2.91/1.03 % (3836853)Peak memory usage: 10 MB
% 2.91/1.03 % (3836853)------------------------------
% 2.91/1.03 % (3836853)------------------------------
% 2.91/1.03 % (3836845)Instruction limit reached!
% 2.91/1.03 % (3836845)------------------------------
% 2.91/1.03 % (3836845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.91/1.03 % (3836845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.91/1.03 % (3836845)CaDiCaL version: 2.1.3
% 2.91/1.03 % (3836845)Termination reason: Instruction limit
% 2.91/1.03 % (3836845)Termination phase: Saturation
% 2.91/1.03 % (3836845)Time elapsed: 0.156 s
% 2.91/1.03 % (3836845)Peak memory usage: 13 MB
% 2.91/1.03 % (3836845)Instructions burned: 132 (million)
% 2.91/1.03 % (3836855)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1108309907:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 2.91/1.03 % (3836849)Instruction limit reached!
% 2.91/1.03 % (3836849)------------------------------
% 2.91/1.03 % (3836849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.91/1.03 % (3836849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.91/1.03 % (3836849)CaDiCaL version: 2.1.3
% 2.91/1.03 % (3836849)Termination reason: Instruction limit
% 2.91/1.03 % (3836849)Termination phase: Saturation
% 2.91/1.03 % (3836849)Time elapsed: 0.152 s
% 2.91/1.03 % (3836849)Peak memory usage: 12 MB
% 2.91/1.03 % (3836849)Instructions burned: 181 (million)
% 2.91/1.03 % (3836856)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1581053201:i=889:ins=1_2996 on theBenchmark for (2996ds/889Mi)
% 2.91/1.03 % (3836856)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 2.91/1.03 % (3836856)Terminated due to inappropriate strategy.
% 2.91/1.03 % (3836856)------------------------------
% 2.91/1.03 % (3836856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.91/1.03 % (3836856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.91/1.03 % (3836856)CaDiCaL version: 2.1.3
% 2.91/1.03 % (3836856)Termination reason: Inappropriate
% 2.91/1.03 % (3836856)Time elapsed: 0.001 s
% 2.91/1.03 % (3836856)Peak memory usage: 10 MB
% 2.91/1.03 % (3836856)------------------------------
% 2.91/1.03 % (3836856)------------------------------
% 2.91/1.03 % (3836858)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=2878534737:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi)
% 2.91/1.03 % (3836860)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2858429979:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi)
% 2.91/1.03 % (3836846)Instruction limit reached!
% 2.91/1.03 % (3836846)------------------------------
% 2.91/1.03 % (3836846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.91/1.03 % (3836846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.91/1.03 % (3836846)CaDiCaL version: 2.1.3
% 2.91/1.03 % (3836846)Termination reason: Instruction limit
% 2.91/1.03 % (3836846)Termination phase: Saturation
% 2.91/1.03 % (3836846)Time elapsed: 0.307 s
% 2.91/1.03 % (3836846)Peak memory usage: 17 MB
% 2.91/1.03 % (3836846)Instructions burned: 685 (million)
% 2.91/1.03 % (3836863)fmb+10_1_sil=64000:random_seed=2827421724:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi)
% 2.91/1.03 % (3836863)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 2.91/1.03 % (3836863)Terminated due to inappropriate strategy.
% 2.91/1.03 % (3836863)------------------------------
% 2.91/1.03 % (3836863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.91/1.03 % (3836863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.91/1.03 % (3836863)CaDiCaL version: 2.1.3
% 2.91/1.03 % (3836863)Termination reason: Inappropriate
% 2.91/1.03 % (3836863)Time elapsed: 0.0000 s
% 2.91/1.03 % (3836863)Peak memory usage: 10 MB
% 2.91/1.03 % (3836863)------------------------------
% 2.91/1.03 % (3836863)------------------------------
% 2.91/1.03 % (3836865)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4245236504:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi)
% 2.91/1.03 % (3836865)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 2.91/1.03 % (3836865)Terminated due to inappropriate strategy.
% 2.91/1.03 % (3836865)------------------------------
% 2.91/1.03 % (3836865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.91/1.03 % (3836865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.91/1.03 % (3836865)CaDiCaL version: 2.1.3
% 2.91/1.03 % (3836865)Termination reason: Inappropriate
% 2.91/1.03 % (3836865)Time elapsed: 0.0000 s
% 2.91/1.03 % (3836865)Peak memory usage: 10 MB
% 2.91/1.03 % (3836865)------------------------------
% 2.91/1.03 % (3836865)------------------------------
% 2.91/1.03 % (3836867)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3011957055:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi)
% 2.91/1.03 % (3836867)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 2.91/1.03 % (3836867)Terminated due to inappropriate strategy.
% 2.91/1.03 % (3836867)------------------------------
% 2.91/1.03 % (3836867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.91/1.03 % (3836867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.91/1.03 % (3836867)CaDiCaL version: 2.1.3
% 2.91/1.03 % (3836867)Termination reason: Inappropriate
% 2.91/1.03 % (3836867)Time elapsed: 0.001 s
% 2.91/1.03 % (3836867)Peak memory usage: 10 MB
% 2.91/1.03 % (3836867)------------------------------
% 2.91/1.03 % (3836867)------------------------------
% 2.91/1.03 % (3836850) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3836824-3836850"...
% 2.91/1.03 % (3836850)...printing done.
% 2.91/1.03 % (3836850)Refutation found. Thanks to Tanya!
% 2.91/1.03 % SZS status Theorem for theBenchmark
% 2.91/1.03 % SZS output start Proof for theBenchmark
% 2.91/1.03 tff(func_def_0, type, f: $int > $int).
% 2.91/1.03 tff(f1,conjecture,(
% 2.91/1.03 (! [X0 : $int] : $lesseq(f($sum(X0,1)),f($sum(X0,2))) & $lesseq(f(7),3)) => $lesseq(f(4),3)),
% 2.91/1.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1)).
% 2.91/1.03 tff(f2,negated_conjecture,(
% 2.91/1.03 ~((! [X0 : $int] : $lesseq(f($sum(X0,1)),f($sum(X0,2))) & $lesseq(f(7),3)) => $lesseq(f(4),3))),
% 2.91/1.03 inference(negated_conjecture,[status(cth)],[f1])).
% 2.91/1.03 tff(f3,plain,(
% 2.91/1.03 ~((! [X0 : $int] : ~$less(f($sum(X0,2)),f($sum(X0,1))) & ~$less(3,f(7))) => ~$less(3,f(4)))),
% 2.91/1.03 inference(theory_normalization,[],[f2])).
% 2.91/1.03 tff(f4,definition,(
% 2.91/1.03 ( ! [X0 : $int,X1 : $int] : ($sum(X0,X1) = $sum(X1,X0)) )),
% 2.91/1.03 introduced(theory,[tha_commutativity])).
% 2.91/1.03 tff(f5,definition,(
% 2.91/1.03 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum(X0,$sum(X1,X2)) = $sum($sum(X0,X1),X2)) )),
% 2.91/1.03 introduced(theory,[tha_associativity])).
% 2.91/1.03 tff(f8,definition,(
% 2.91/1.03 ( ! [X0 : $int] : (0 = $sum(X0,$uminus(X0))) )),
% 2.91/1.03 introduced(theory,[tha_inverse_op_unit])).
% 2.91/1.03 tff(f10,definition,(
% 2.91/1.03 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X1,X2) | ~$less(X0,X1) | $less(X0,X2)) )),
% 2.91/1.03 introduced(theory,[tha_transitivity])).
% 2.91/1.03 tff(f11,definition,(
% 2.91/1.03 ( ! [X0 : $int,X1 : $int] : ($less(X1,X0) | $less(X0,X1) | X0 = X1) )),
% 2.91/1.03 introduced(theory,[tha_order_totality])).
% 2.91/1.03 tff(f16,plain,(
% 2.91/1.03 $less(3,f(4)) & (! [X0 : $int] : ~$less(f($sum(X0,2)),f($sum(X0,1))) & ~$less(3,f(7)))),
% 2.91/1.03 inference(ennf_transformation,[],[f3])).
% 2.91/1.03 tff(f17,plain,(
% 2.91/1.03 $less(3,f(4)) & ! [X0 : $int] : ~$less(f($sum(X0,2)),f($sum(X0,1))) & ~$less(3,f(7))),
% 2.91/1.03 inference(flattening,[],[f16])).
% 2.91/1.03 tff(f18,plain,(
% 2.91/1.03 ~$less(3,f(7))),
% 2.91/1.03 inference(cnf_transformation,[],[f17])).
% 2.91/1.03 tff(f19,plain,(
% 2.91/1.03 ( ! [X0 : $int] : (~$less(f($sum(X0,2)),f($sum(X0,1)))) )),
% 2.91/1.03 inference(cnf_transformation,[],[f17])).
% 2.91/1.03 tff(f20,plain,(
% 2.91/1.03 $less(3,f(4))),
% 2.91/1.03 inference(cnf_transformation,[],[f17])).
% 2.91/1.03 tff(f163,plain,(
% 2.91/1.03 ( ! [X0 : $int] : ($less(X0,f(4)) | ~$less(X0,3)) )),
% 2.91/1.03 inference(resolution,[],[f10,f20])).
% 2.91/1.03 tff(f632,plain,(
% 2.91/1.03 ( ! [X0 : $int,X1 : $int] : ($sum(0,X1) = $sum(X0,$sum($uminus(X0),X1))) )),
% 2.91/1.03 inference(superposition,[],[f5,f8])).
% 2.91/1.03 tff(f655,plain,(
% 2.91/1.03 ( ! [X0 : $int,X1 : $int] : ($sum(X0,$sum($uminus(X0),X1)) = X1) )),
% 2.91/1.03 inference(evaluation,[],[f632])).
% 2.91/1.03 tff(f801,plain,(
% 2.91/1.03 ( ! [X0 : $int,X1 : $int] : (~$less(f($sum(X0,$sum(X1,2))),f($sum($sum(X0,X1),1)))) )),
% 2.91/1.03 inference(superposition,[],[f19,f5])).
% 2.91/1.03 tff(f804,plain,(
% 2.91/1.03 ( ! [X0 : $int,X1 : $int] : (~$less(f($sum($sum(X0,X1),2)),f($sum(X0,$sum(X1,1))))) )),
% 2.91/1.03 inference(superposition,[],[f19,f5])).
% 2.91/1.03 tff(f805,plain,(
% 2.91/1.03 ( ! [X0 : $int,X1 : $int] : (~$less(f($sum(2,$sum(X0,X1))),f($sum(X0,$sum(X1,1))))) )),
% 2.91/1.03 inference(forward_demodulation,[],[f804,f4])).
% 2.91/1.03 tff(f806,plain,(
% 2.91/1.03 ( ! [X0 : $int,X1 : $int] : (~$less(f($sum(X0,$sum(X1,2))),f($sum(1,$sum(X0,X1))))) )),
% 2.91/1.03 inference(forward_demodulation,[],[f801,f4])).
% 2.91/1.03 tff(f855,plain,(
% 2.91/1.03 ( ! [X0 : $int,X1 : $int] : (~$less(f($sum(2,$sum(X0,X1))),f($sum(X1,$sum(X0,1))))) )),
% 2.91/1.03 inference(superposition,[],[f805,f4])).
% 2.91/1.03 tff(f859,plain,(
% 2.91/1.03 ( ! [X0 : $int,X1 : $int] : (~$less(f($sum(2,$sum(X1,X0))),f($sum(X1,$sum(1,X0))))) )),
% 2.91/1.03 inference(superposition,[],[f805,f4])).
% 2.91/1.03 tff(f983,plain,(
% 2.91/1.03 ( ! [X0 : $int] : (~$less(f($sum(2,$sum(X0,$uminus(1)))),f($sum(X0,0)))) )),
% 2.91/1.03 inference(superposition,[],[f859,f8])).
% 2.91/1.03 tff(f989,plain,(
% 2.91/1.03 ( ! [X0 : $int] : (~$less(f($sum(2,$sum(X0,-1))),f(X0))) )),
% 2.91/1.03 inference(evaluation,[],[f983])).
% 2.91/1.03 tff(f1236,plain,(
% 2.91/1.03 ( ! [X0 : $int] : (~$less(f($sum($uminus(1),$sum(X0,2))),f(X0))) )),
% 2.91/1.03 inference(superposition,[],[f806,f655])).
% 2.91/1.03 tff(f1245,plain,(
% 2.91/1.03 ( ! [X0 : $int] : (~$less(f(X0),f($sum(X0,$sum($uminus(2),1))))) )),
% 2.91/1.03 inference(superposition,[],[f855,f655])).
% 2.91/1.03 tff(f1256,plain,(
% 2.91/1.03 ( ! [X0 : $int] : (~$less(f(X0),f($sum(X0,-1)))) )),
% 2.91/1.03 inference(evaluation,[],[f1245])).
% 2.91/1.03 tff(f1264,plain,(
% 2.91/1.03 ( ! [X0 : $int] : (~$less(f($sum(-1,$sum(X0,2))),f(X0))) )),
% 2.91/1.03 inference(evaluation,[],[f1236])).
% 2.91/1.03 tff(f1294,plain,(
% 2.91/1.03 ( ! [X0 : $int] : (~$less(f(X0),f($sum(-1,X0)))) )),
% 2.91/1.03 inference(superposition,[],[f1256,f4])).
% 2.91/1.03 tff(f1368,plain,(
% 2.91/1.03 ~$less(f($sum(2,$sum(4,-1))),3)),
% 2.91/1.03 inference(resolution,[],[f163,f989])).
% 2.91/1.03 tff(f1373,plain,(
% 2.91/1.03 ~$less(f(5),3)),
% 2.91/1.03 inference(evaluation,[],[f1368])).
% 2.91/1.03 tff(f1374,plain,(
% 2.91/1.03 $less(3,f(5)) | 3 = f(5)),
% 2.91/1.03 inference(resolution,[],[f1373,f11])).
% 2.91/1.03 tff(f1564,plain,(
% 2.91/1.03 ( ! [X0 : $int] : (~$less(f($sum($uminus(-1),X0)),f(X0))) )),
% 2.91/1.03 inference(superposition,[],[f1294,f655])).
% 2.91/1.03 tff(f1568,plain,(
% 2.91/1.03 ( ! [X0 : $int] : (~$less(f($sum(1,X0)),f(X0))) )),
% 2.91/1.03 inference(evaluation,[],[f1564])).
% 2.91/1.03 tff(f1577,plain,(
% 2.91/1.03 ( ! [X0 : $int] : (~$less(f($sum(X0,1)),f(X0))) )),
% 2.91/1.03 inference(superposition,[],[f1568,f4])).
% 2.91/1.03 tff(f1967,definition,(
% 2.91/1.03 spl0_35 <=> 3 = f(5)),
% 2.91/1.03 introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition])).
% 2.91/1.03 tff(f1969,plain,(
% 2.91/1.03 3 = f(5) | ~spl0_35),
% 2.91/1.03 inference(avatar_component_clause,[],[f1967])).
% 2.91/1.03 tff(f1971,definition,(
% 2.91/1.03 spl0_36 <=> $less(3,f(5))),
% 2.91/1.03 introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition])).
% 2.91/1.03 tff(f1973,plain,(
% 2.91/1.03 $less(3,f(5)) | ~spl0_36),
% 2.91/1.03 inference(avatar_component_clause,[],[f1971])).
% 2.91/1.03 tff(f1974,plain,(
% 2.91/1.03 spl0_35 | spl0_36),
% 2.91/1.03 inference(avatar_split_clause,[],[f1374,f1971,f1967])).
% 2.91/1.03 tff(f1979,plain,(
% 2.91/1.03 ~$less(3,f($sum(-1,5))) | ~spl0_35),
% 2.91/1.03 inference(superposition,[],[f1294,f1969])).
% 2.91/1.03 tff(f1982,plain,(
% 2.91/1.03 ~$less(3,f(4)) | ~spl0_35),
% 2.91/1.03 inference(evaluation,[],[f1979])).
% 2.91/1.03 tff(f1987,plain,(
% 2.91/1.03 $false | ~spl0_35),
% 2.91/1.03 inference(forward_subsumption_resolution,[],[f1982,f20])).
% 2.91/1.03 tff(f1988,plain,(
% 2.91/1.03 ~spl0_35),
% 2.91/1.03 inference(avatar_contradiction_clause,[],[f1987])).
% 2.91/1.03 tff(f1991,plain,(
% 2.91/1.03 ( ! [X0 : $int] : ($less(X0,f(5)) | ~$less(X0,3)) ) | ~spl0_36),
% 2.91/1.03 inference(resolution,[],[f1973,f10])).
% 2.91/1.03 tff(f1996,plain,(
% 2.91/1.03 ~$less(f($sum(5,1)),3) | ~spl0_36),
% 2.91/1.03 inference(resolution,[],[f1991,f1577])).
% 2.91/1.03 tff(f1999,plain,(
% 2.91/1.03 ~$less(f(6),3) | ~spl0_36),
% 2.91/1.03 inference(evaluation,[],[f1996])).
% 2.91/1.03 tff(f2008,plain,(
% 2.91/1.03 $less(3,f(6)) | 3 = f(6) | ~spl0_36),
% 2.91/1.03 inference(resolution,[],[f1999,f11])).
% 2.91/1.03 tff(f8902,definition,(
% 2.91/1.03 spl0_54 <=> 3 = f(6)),
% 2.91/1.03 introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition])).
% 2.91/1.03 tff(f8904,plain,(
% 2.91/1.03 3 = f(6) | ~spl0_54),
% 2.91/1.03 inference(avatar_component_clause,[],[f8902])).
% 2.91/1.03 tff(f8906,definition,(
% 2.91/1.03 spl0_55 <=> $less(3,f(6))),
% 2.91/1.03 introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition])).
% 2.91/1.03 tff(f8908,plain,(
% 2.91/1.03 $less(3,f(6)) | ~spl0_55),
% 2.91/1.03 inference(avatar_component_clause,[],[f8906])).
% 2.91/1.03 tff(f8909,plain,(
% 2.91/1.03 spl0_54 | spl0_55 | ~spl0_36),
% 2.91/1.03 inference(avatar_split_clause,[],[f2008,f1971,f8906,f8902])).
% 2.91/1.03 tff(f9103,plain,(
% 2.91/1.03 ~$less(3,f($sum(6,-1))) | ~spl0_54),
% 2.91/1.03 inference(superposition,[],[f1256,f8904])).
% 2.91/1.03 tff(f9104,plain,(
% 2.91/1.03 ~$less(3,f(5)) | ~spl0_54),
% 2.91/1.03 inference(evaluation,[],[f9103])).
% 2.91/1.03 tff(f9150,plain,(
% 2.91/1.03 $false | (~spl0_36 | ~spl0_54)),
% 2.91/1.03 inference(forward_subsumption_resolution,[],[f9104,f1973])).
% 2.91/1.03 tff(f9151,plain,(
% 2.91/1.03 ~spl0_36 | ~spl0_54),
% 2.91/1.03 inference(avatar_contradiction_clause,[],[f9150])).
% 2.91/1.03 tff(f9182,plain,(
% 2.91/1.03 ( ! [X0 : $int] : ($less(X0,f(6)) | ~$less(X0,3)) ) | ~spl0_55),
% 2.91/1.03 inference(resolution,[],[f8908,f10])).
% 2.91/1.03 tff(f9470,plain,(
% 2.91/1.03 ~$less(f($sum(-1,$sum(6,2))),3) | ~spl0_55),
% 2.91/1.03 inference(resolution,[],[f9182,f1264])).
% 2.91/1.03 tff(f9475,plain,(
% 2.91/1.03 ~$less(f(7),3) | ~spl0_55),
% 2.91/1.03 inference(evaluation,[],[f9470])).
% 2.91/1.03 tff(f9490,plain,(
% 2.91/1.03 $less(3,f(7)) | f(7) = 3 | ~spl0_55),
% 2.91/1.03 inference(resolution,[],[f9475,f11])).
% 2.91/1.03 tff(f9491,plain,(
% 2.91/1.03 f(7) = 3 | ~spl0_55),
% 2.91/1.03 inference(forward_subsumption_resolution,[],[f9490,f18])).
% 2.91/1.03 tff(f9523,plain,(
% 2.91/1.03 ~$less(3,f($sum(-1,7))) | ~spl0_55),
% 2.91/1.03 inference(superposition,[],[f1294,f9491])).
% 2.91/1.03 tff(f9526,plain,(
% 2.91/1.03 ~$less(3,f(6)) | ~spl0_55),
% 2.91/1.03 inference(evaluation,[],[f9523])).
% 2.91/1.03 tff(f9532,plain,(
% 2.91/1.03 $false | ~spl0_55),
% 2.91/1.03 inference(forward_subsumption_resolution,[],[f9526,f8908])).
% 2.91/1.03 tff(f9533,plain,(
% 2.91/1.03 ~spl0_55),
% 2.91/1.03 inference(avatar_contradiction_clause,[],[f9532])).
% 2.91/1.03 cnf(s57, plain, spl0_35 | spl0_36, inference(sat_conversion,[],[f1974])).
% 2.91/1.03 cnf(s59, plain, ~spl0_35, inference(sat_conversion,[],[f1988])).
% 2.91/1.03 cnf(s107, plain, ~spl0_36 | spl0_54 | spl0_55, inference(sat_conversion,[],[f8909])).
% 2.91/1.03 cnf(s111, plain, ~spl0_36 | ~spl0_54, inference(sat_conversion,[],[f9151])).
% 2.91/1.03 cnf(s119, plain, ~spl0_55, inference(sat_conversion,[],[f9533])).
% 2.91/1.03 cnf(s120, plain, ~spl0_36 | spl0_54, inference(rat,[],[s107,s119])).
% 2.91/1.03 cnf(s121, plain, spl0_36, inference(rat,[],[s57,s59])).
% 2.91/1.03 cnf(s122, plain, ~spl0_54, inference(rat,[],[s111,s121])).
% 2.91/1.03 cnf(s123, plain, $false, inference(rat,[],[s120,s122,s121])).
% 2.91/1.03 tff(f9534,plain,(
% 2.91/1.03 $false),
% 2.91/1.03 inference(avatar_sat_refutation,[],[s123])).
% 2.91/1.03 % SZS output end Proof for theBenchmark
% 2.91/1.03 % (3836850)------------------------------
% 2.91/1.03 % (3836850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.91/1.03 % (3836850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.91/1.03 % (3836850)CaDiCaL version: 2.1.3
% 2.91/1.03 % (3836850)Termination reason: Refutation
% 2.91/1.03 % (3836850)Time elapsed: 0.409 s
% 2.91/1.03 % (3836850)Peak memory usage: 15 MB
% 2.91/1.03 % (3836850)Instructions burned: 385 (million)
% 2.91/1.03 % (3836824)Success in time 0.627 s
% 2.91/1.03 % Vampire exiting
%------------------------------------------------------------------------------