%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ARI582_1 : TPTP v9.3.1. Released v5.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n020.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:34:54 AM UTC 2026
% Result : Theorem 98.79s 20.28s
% Output : Refutation 98.79s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ARI582_1 : TPTP v9.3.1. Released v5.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.25 % Computer : n020.cluster.edu
% 0.11/0.25 % Model : x86_64 x86_64
% 0.11/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.25 % Memory : 8046.5625MB
% 0.11/0.25 % OS : Linux 6.8.0-71-generic
% 0.11/0.25 % CPULimit : 300
% 0.11/0.25 % WCLimit : 300
% 0.11/0.25 % DateTime : Mon Sep 28 20:53:34 UTC 2026
% 0.11/0.25 % CPUTime :
% 0.11/0.25 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.24/0.30 Running first-order model finding
% 0.24/0.30 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.34/1.29 % (541043)Will run a generic schedule for satisfiability detection.
% 6.34/1.29 % (541051)dis+10_1_sil=32000:sp=arity:random_seed=27170939:i=103:fgj=on_3000 on theBenchmark for (3000ds/103Mi)
% 6.34/1.29 % (541054)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1621911989:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_3000 on theBenchmark for (3000ds/159Mi)
% 6.34/1.29 % (541049)% WARNING: option uhcvi not known.
% 6.34/1.29 % (541050)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2977766341:i=88024:add=on:rawr=on_3000 on theBenchmark for (3000ds/88024Mi)
% 6.34/1.29 % (541048)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3999411913_3000 on theBenchmark for (3000ds/0Mi)
% 6.34/1.29 % (541052)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4146194569:i=116_3000 on theBenchmark for (3000ds/116Mi)
% 6.34/1.29 % (541049)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1469331727:i=135531:add=off:rawr=on_3000 on theBenchmark for (3000ds/135531Mi)
% 6.34/1.29 % (541053)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1639683682:i=131_3000 on theBenchmark for (3000ds/131Mi)
% 6.34/1.29 % (541048)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.34/1.29 % (541048)Terminated due to inappropriate strategy.
% 6.34/1.29 % (541048)------------------------------
% 6.34/1.29 % (541048)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.34/1.29 % (541048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.34/1.29 % (541048)CaDiCaL version: 2.1.3
% 6.34/1.29 % (541048)Termination reason: Inappropriate
% 6.34/1.29 % (541048)Time elapsed: 0.001 s
% 6.34/1.29 % (541048)Peak memory usage: 10 MB
% 6.34/1.29 % (541048)------------------------------
% 6.34/1.29 % (541048)------------------------------
% 6.34/1.29 % (541062)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1394581989:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 6.34/1.29 % (541062)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.34/1.29 % (541062)Terminated due to inappropriate strategy.
% 6.34/1.29 % (541062)------------------------------
% 6.34/1.29 % (541062)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.34/1.29 % (541062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.34/1.29 % (541062)CaDiCaL version: 2.1.3
% 6.34/1.29 % (541062)Termination reason: Inappropriate
% 6.34/1.29 % (541062)Time elapsed: 0.001 s
% 6.34/1.29 % (541062)Peak memory usage: 11 MB
% 6.34/1.29 % (541062)------------------------------
% 6.34/1.29 % (541062)------------------------------
% 6.34/1.29 % (541051)Instruction limit reached!
% 6.34/1.29 % (541051)------------------------------
% 6.34/1.29 % (541051)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.34/1.29 % (541051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.34/1.29 % (541051)CaDiCaL version: 2.1.3
% 6.34/1.29 % (541051)Termination reason: Instruction limit
% 6.34/1.29 % (541051)Termination phase: Saturation
% 6.34/1.29 % (541051)Time elapsed: 0.056 s
% 6.34/1.29 % (541051)Peak memory usage: 12 MB
% 6.34/1.29 % (541051)Instructions burned: 105 (million)
% 6.34/1.29 % (541064)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2547332287:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 6.34/1.29 % (541065)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=281398098:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 6.34/1.29 % (541052)Instruction limit reached!
% 6.34/1.29 % (541052)------------------------------
% 6.34/1.29 % (541052)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.34/1.29 % (541052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.34/1.29 % (541052)CaDiCaL version: 2.1.3
% 6.34/1.29 % (541052)Termination reason: Instruction limit
% 6.34/1.29 % (541052)Termination phase: Saturation
% 6.34/1.29 % (541052)Time elapsed: 0.114 s
% 6.34/1.29 % (541052)Peak memory usage: 12 MB
% 6.34/1.29 % (541052)Instructions burned: 117 (million)
% 6.34/1.29 % (541053)Instruction limit reached!
% 6.34/1.29 % (541053)------------------------------
% 6.34/1.29 % (541053)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.34/1.29 % (541053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.15/2.18 % (541053)CaDiCaL version: 2.1.3
% 13.15/2.18 % (541053)Termination reason: Instruction limit
% 13.15/2.18 % (541053)Termination phase: Saturation
% 13.15/2.18 % (541053)Time elapsed: 0.133 s
% 13.15/2.18 % (541053)Peak memory usage: 13 MB
% 13.15/2.18 % (541053)Instructions burned: 131 (million)
% 13.15/2.18 % (541068)ott-21_1_sil=16000:fs=off:random_seed=4133451193:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 13.15/2.18 % (541064)Instruction limit reached!
% 13.15/2.18 % (541064)------------------------------
% 13.15/2.18 % (541064)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.15/2.18 % (541064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.15/2.18 % (541064)CaDiCaL version: 2.1.3
% 13.15/2.18 % (541064)Termination reason: Instruction limit
% 13.15/2.18 % (541064)Termination phase: Saturation
% 13.15/2.18 % (541064)Time elapsed: 0.088 s
% 13.15/2.18 % (541064)Peak memory usage: 13 MB
% 13.15/2.18 % (541064)Instructions burned: 131 (million)
% 13.15/2.18 % (541069)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=346146063:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 13.15/2.18 % (541054)Instruction limit reached!
% 13.15/2.18 % (541054)------------------------------
% 13.15/2.18 % (541054)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.15/2.18 % (541054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.15/2.18 % (541054)CaDiCaL version: 2.1.3
% 13.15/2.18 % (541054)Termination reason: Instruction limit
% 13.15/2.18 % (541054)Termination phase: Saturation
% 13.15/2.18 % (541054)Time elapsed: 0.172 s
% 13.15/2.18 % (541054)Peak memory usage: 13 MB
% 13.15/2.18 % (541054)Instructions burned: 159 (million)
% 13.15/2.18 % (541071)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=705210806:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 13.15/2.18 % (541071)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 13.15/2.18 % (541071)Terminated due to inappropriate strategy.
% 13.15/2.18 % (541071)------------------------------
% 13.15/2.18 % (541071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.15/2.18 % (541071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.15/2.18 % (541071)CaDiCaL version: 2.1.3
% 13.15/2.18 % (541071)Termination reason: Inappropriate
% 13.15/2.18 % (541071)Time elapsed: 0.0000 s
% 13.15/2.18 % (541071)Peak memory usage: 10 MB
% 13.15/2.18 % (541071)------------------------------
% 13.15/2.18 % (541071)------------------------------
% 13.15/2.18 % (541073)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3527728444:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 13.15/2.18 % (541075)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2598691086:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 13.15/2.18 % (541075)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 13.15/2.18 % (541075)Terminated due to inappropriate strategy.
% 13.15/2.18 % (541075)------------------------------
% 13.15/2.18 % (541075)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.15/2.18 % (541075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.15/2.18 % (541075)CaDiCaL version: 2.1.3
% 13.15/2.18 % (541075)Termination reason: Inappropriate
% 13.15/2.18 % (541075)Time elapsed: 0.001 s
% 13.15/2.18 % (541075)Peak memory usage: 10 MB
% 13.15/2.18 % (541075)------------------------------
% 13.15/2.18 % (541075)------------------------------
% 13.15/2.18 % (541078)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=2571299353:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi)
% 13.15/2.18 % (541068)Instruction limit reached!
% 13.15/2.18 % (541068)------------------------------
% 13.15/2.18 % (541068)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.15/2.18 % (541068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.15/2.18 % (541068)CaDiCaL version: 2.1.3
% 13.15/2.18 % (541068)Termination reason: Instruction limit
% 13.15/2.18 % (541068)Termination phase: Saturation
% 13.15/2.18 % (541068)Time elapsed: 0.150 s
% 13.15/2.18 % (541068)Peak memory usage: 12 MB
% 13.15/2.18 % (541068)Instructions burned: 181 (million)
% 13.15/2.18 % (541080)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=69527340:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi)
% 13.15/2.18 % (541069)Instruction limit reached!
% 38.46/5.74 % (541069)------------------------------
% 38.46/5.74 % (541069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.46/5.74 % (541069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.46/5.74 % (541069)CaDiCaL version: 2.1.3
% 38.46/5.74 % (541069)Termination reason: Instruction limit
% 38.46/5.74 % (541069)Termination phase: Saturation
% 38.46/5.74 % (541069)Time elapsed: 0.289 s
% 38.46/5.74 % (541069)Peak memory usage: 14 MB
% 38.46/5.74 % (541069)Instructions burned: 477 (million)
% 38.46/5.74 % (541082)fmb+10_1_sil=64000:random_seed=4283533503:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi)
% 38.46/5.74 % (541082)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 38.46/5.74 % (541082)Terminated due to inappropriate strategy.
% 38.46/5.74 % (541082)------------------------------
% 38.46/5.74 % (541082)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.46/5.74 % (541082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.46/5.74 % (541082)CaDiCaL version: 2.1.3
% 38.46/5.74 % (541082)Termination reason: Inappropriate
% 38.46/5.74 % (541082)Time elapsed: 0.001 s
% 38.46/5.74 % (541082)Peak memory usage: 11 MB
% 38.46/5.74 % (541082)------------------------------
% 38.46/5.74 % (541082)------------------------------
% 38.46/5.74 % (541084)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=989658121:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi)
% 38.46/5.74 % (541084)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 38.46/5.74 % (541084)Terminated due to inappropriate strategy.
% 38.46/5.74 % (541084)------------------------------
% 38.46/5.74 % (541084)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.46/5.74 % (541084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.46/5.74 % (541084)CaDiCaL version: 2.1.3
% 38.46/5.74 % (541084)Termination reason: Inappropriate
% 38.46/5.74 % (541084)Time elapsed: 0.001 s
% 38.46/5.74 % (541084)Peak memory usage: 11 MB
% 38.46/5.74 % (541084)------------------------------
% 38.46/5.74 % (541084)------------------------------
% 38.46/5.74 % (541086)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3733219346:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi)
% 38.46/5.74 % (541086)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 38.46/5.74 % (541086)Terminated due to inappropriate strategy.
% 38.46/5.74 % (541086)------------------------------
% 38.46/5.74 % (541086)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.46/5.74 % (541086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.46/5.74 % (541086)CaDiCaL version: 2.1.3
% 38.46/5.74 % (541086)Termination reason: Inappropriate
% 38.46/5.74 % (541086)Time elapsed: 0.0000 s
% 38.46/5.74 % (541086)Peak memory usage: 10 MB
% 38.46/5.74 % (541086)------------------------------
% 38.46/5.74 % (541086)------------------------------
% 38.46/5.74 % (541088)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=198279068:i=5131_2994 on theBenchmark for (2994ds/5131Mi)
% 38.46/5.74 % (541065)Instruction limit reached!
% 38.46/5.74 % (541065)------------------------------
% 38.46/5.74 % (541065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.46/5.74 % (541065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.46/5.74 % (541065)CaDiCaL version: 2.1.3
% 38.46/5.74 % (541065)Termination reason: Instruction limit
% 38.46/5.74 % (541065)Termination phase: Saturation
% 38.46/5.74 % (541065)Time elapsed: 0.637 s
% 38.46/5.74 % (541065)Peak memory usage: 17 MB
% 38.46/5.74 % (541065)Instructions burned: 684 (million)
% 38.46/5.74 % (541090)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3163516280:i=1472:ins=7:fdi=8:gsp=on_2992 on theBenchmark for (2992ds/1472Mi)
% 38.46/5.74 % (541078)Instruction limit reached!
% 38.46/5.74 % (541078)------------------------------
% 38.46/5.74 % (541078)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.46/5.74 % (541078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.46/5.74 % (541078)CaDiCaL version: 2.1.3
% 38.46/5.74 % (541078)Termination reason: Instruction limit
% 38.46/5.74 % (541078)Termination phase: Saturation
% 38.46/5.74 % (541078)Time elapsed: 0.679 s
% 38.46/5.74 % (541078)Peak memory usage: 17 MB
% 38.46/5.74 % (541078)Instructions burned: 693 (million)
% 38.46/5.74 % (541092)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2487935510:i=6324_2990 on theBenchmark for (2990ds/6324Mi)
% 65.45/9.52 % (541092)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 65.45/9.52 % (541092)Terminated due to inappropriate strategy.
% 65.45/9.52 % (541092)------------------------------
% 65.45/9.52 % (541092)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 65.45/9.52 % (541092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.45/9.52 % (541092)CaDiCaL version: 2.1.3
% 65.45/9.52 % (541092)Termination reason: Inappropriate
% 65.45/9.52 % (541092)Time elapsed: 0.001 s
% 65.45/9.52 % (541092)Peak memory usage: 11 MB
% 65.45/9.52 % (541092)------------------------------
% 65.45/9.52 % (541092)------------------------------
% 65.45/9.52 % (541094)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2953057402:fmbsr=2.30978:i=2174_2990 on theBenchmark for (2990ds/2174Mi)
% 65.45/9.52 % (541094)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 65.45/9.52 % (541094)Terminated due to inappropriate strategy.
% 65.45/9.52 % (541094)------------------------------
% 65.45/9.52 % (541094)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 65.45/9.52 % (541094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.45/9.52 % (541094)CaDiCaL version: 2.1.3
% 65.45/9.52 % (541094)Termination reason: Inappropriate
% 65.45/9.52 % (541094)Time elapsed: 0.001 s
% 65.45/9.52 % (541094)Peak memory usage: 10 MB
% 65.45/9.52 % (541094)------------------------------
% 65.45/9.52 % (541094)------------------------------
% 65.45/9.52 % (541096)ott-2_1_sil=16000:newcnf=on:random_seed=1778243734:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2989 on theBenchmark for (2989ds/869Mi)
% 65.45/9.52 % (541080)Instruction limit reached!
% 65.45/9.52 % (541080)------------------------------
% 65.45/9.52 % (541080)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 65.45/9.52 % (541080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.45/9.52 % (541080)CaDiCaL version: 2.1.3
% 65.45/9.52 % (541080)Termination reason: Instruction limit
% 65.45/9.52 % (541080)Termination phase: Saturation
% 65.45/9.52 % (541080)Time elapsed: 0.838 s
% 65.45/9.52 % (541080)Peak memory usage: 19 MB
% 65.45/9.52 % (541080)Instructions burned: 880 (million)
% 65.45/9.52 % (541098)ott+10_1_sil=32000:tgt=ground:random_seed=1409811120:i=5114:av=off_2987 on theBenchmark for (2987ds/5114Mi)
% 65.45/9.52 % (541073)Instruction limit reached!
% 65.45/9.52 % (541073)------------------------------
% 65.45/9.52 % (541073)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 65.45/9.52 % (541073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.45/9.52 % (541073)CaDiCaL version: 2.1.3
% 65.45/9.52 % (541073)Termination reason: Instruction limit
% 65.45/9.52 % (541073)Termination phase: Saturation
% 65.45/9.52 % (541073)Time elapsed: 1.022 s
% 65.45/9.52 % (541073)Peak memory usage: 19 MB
% 65.45/9.52 % (541073)Instructions burned: 1180 (million)
% 65.45/9.52 % (541100)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2228461299:i=54282_2987 on theBenchmark for (2987ds/54282Mi)
% 65.45/9.52 % (541100)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 65.45/9.52 % (541100)Terminated due to inappropriate strategy.
% 65.45/9.52 % (541100)------------------------------
% 65.45/9.52 % (541100)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 65.45/9.52 % (541100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.45/9.52 % (541100)CaDiCaL version: 2.1.3
% 65.45/9.52 % (541100)Termination reason: Inappropriate
% 65.45/9.52 % (541100)Time elapsed: 0.001 s
% 65.45/9.52 % (541100)Peak memory usage: 10 MB
% 65.45/9.52 % (541100)------------------------------
% 65.45/9.52 % (541100)------------------------------
% 65.45/9.52 % (541102)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1177377865:i=3512:aac=none_2987 on theBenchmark for (2987ds/3512Mi)
% 65.45/9.52 % (541096)Instruction limit reached!
% 65.45/9.52 % (541096)------------------------------
% 65.45/9.52 % (541096)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 65.45/9.52 % (541096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.45/9.52 % (541096)CaDiCaL version: 2.1.3
% 65.45/9.52 % (541096)Termination reason: Instruction limit
% 65.45/9.52 % (541096)Termination phase: Saturation
% 65.45/9.52 % (541096)Time elapsed: 0.822 s
% 65.45/9.52 % (541096)Peak memory usage: 15 MB
% 98.79/20.28 % (541096)Instructions burned: 869 (million)
% 98.79/20.28 % (541104)dis+21_1_sil=32000:sas=cadical:random_seed=1606005126:i=3773:amm=off_2981 on theBenchmark for (2981ds/3773Mi)
% 98.79/20.28 % (541090)Instruction limit reached!
% 98.79/20.28 % (541090)------------------------------
% 98.79/20.28 % (541090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.79/20.28 % (541090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.79/20.28 % (541090)CaDiCaL version: 2.1.3
% 98.79/20.28 % (541090)Termination reason: Instruction limit
% 98.79/20.28 % (541090)Termination phase: Saturation
% 98.79/20.28 % (541090)Time elapsed: 1.461 s
% 98.79/20.28 % (541090)Peak memory usage: 28 MB
% 98.79/20.28 % (541090)Instructions burned: 1473 (million)
% 98.79/20.28 % (541108)ott+11_1_sil=16000:gs=on:random_seed=3236453387:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2977 on theBenchmark for (2977ds/2251Mi)
% 98.79/20.28 % (541088)Instruction limit reached!
% 98.79/20.28 % (541088)------------------------------
% 98.79/20.28 % (541088)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.79/20.28 % (541088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.79/20.28 % (541088)CaDiCaL version: 2.1.3
% 98.79/20.28 % (541088)Termination reason: Instruction limit
% 98.79/20.28 % (541088)Termination phase: Saturation
% 98.79/20.28 % (541088)Time elapsed: 2.504 s
% 98.79/20.28 % (541088)Peak memory usage: 42 MB
% 98.79/20.28 % (541088)Instructions burned: 5132 (million)
% 98.79/20.28 % (541114)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2341687162:fmbsr=1.6:i=67534_2969 on theBenchmark for (2969ds/67534Mi)
% 98.79/20.28 % (541114)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 98.79/20.28 % (541114)Terminated due to inappropriate strategy.
% 98.79/20.28 % (541114)------------------------------
% 98.79/20.28 % (541114)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.79/20.28 % (541114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.79/20.28 % (541114)CaDiCaL version: 2.1.3
% 98.79/20.28 % (541114)Termination reason: Inappropriate
% 98.79/20.28 % (541114)Time elapsed: 0.001 s
% 98.79/20.28 % (541114)Peak memory usage: 11 MB
% 98.79/20.28 % (541114)------------------------------
% 98.79/20.28 % (541114)------------------------------
% 98.79/20.28 % (541116)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3079024513:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2968 on theBenchmark for (2968ds/4591Mi)
% 98.79/20.28 % (541108)Instruction limit reached!
% 98.79/20.28 % (541108)------------------------------
% 98.79/20.28 % (541108)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.79/20.28 % (541108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.79/20.28 % (541108)CaDiCaL version: 2.1.3
% 98.79/20.28 % (541108)Termination reason: Instruction limit
% 98.79/20.28 % (541108)Termination phase: Saturation
% 98.79/20.28 % (541108)Time elapsed: 2.065 s
% 98.79/20.28 % (541108)Peak memory usage: 23 MB
% 98.79/20.28 % (541108)Instructions burned: 2251 (million)
% 98.79/20.28 % (541132)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=4279362810:i=29340_2956 on theBenchmark for (2956ds/29340Mi)
% 98.79/20.28 % (541102)Instruction limit reached!
% 98.79/20.28 % (541102)------------------------------
% 98.79/20.28 % (541102)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.79/20.28 % (541102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.79/20.28 % (541102)CaDiCaL version: 2.1.3
% 98.79/20.28 % (541102)Termination reason: Instruction limit
% 98.79/20.28 % (541102)Termination phase: Saturation
% 98.79/20.28 % (541102)Time elapsed: 3.265 s
% 98.79/20.28 % (541102)Peak memory usage: 28 MB
% 98.79/20.28 % (541102)Instructions burned: 3512 (million)
% 98.79/20.28 % (541134)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1611153628:i=5211_2954 on theBenchmark for (2954ds/5211Mi)
% 98.79/20.28 % (541116)Instruction limit reached!
% 98.79/20.28 % (541116)------------------------------
% 98.79/20.28 % (541116)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.79/20.28 % (541116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.79/20.28 % (541116)CaDiCaL version: 2.1.3
% 98.79/20.28 % (541116)Termination reason: Instruction limit
% 98.79/20.28 % (541116)Termination phase: Saturation
% 98.79/20.28 % (541116)Time elapsed: 2.286 s
% 98.79/20.28 % (541116)Peak memory usage: 30 MB
% 98.79/20.28 % (541116)Instructions burned: 4593 (million)
% 98.79/20.28 % (541104)Instruction limit reached!
% 98.79/20.28 % (541104)------------------------------
% 98.79/20.28 % (541104)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.79/20.28 % (541104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.79/20.28 % (541104)CaDiCaL version: 2.1.3
% 98.79/20.28 % (541104)Termination reason: Instruction limit
% 98.79/20.28 % (541104)Termination phase: Saturation
% 98.79/20.28 % (541104)Time elapsed: 3.539 s
% 98.79/20.28 % (541104)Peak memory usage: 33 MB
% 98.79/20.28 % (541104)Instructions burned: 3773 (million)
% 98.79/20.28 % (541138)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2748459887:i=5497:nm=2_2945 on theBenchmark for (2945ds/5497Mi)
% 98.79/20.28 % (541138)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 98.79/20.28 % (541138)Terminated due to inappropriate strategy.
% 98.79/20.28 % (541138)------------------------------
% 98.79/20.28 % (541138)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.79/20.28 % (541138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.79/20.28 % (541138)CaDiCaL version: 2.1.3
% 98.79/20.28 % (541138)Termination reason: Inappropriate
% 98.79/20.28 % (541138)Time elapsed: 0.001 s
% 98.79/20.28 % (541138)Peak memory usage: 11 MB
% 98.79/20.28 % (541138)------------------------------
% 98.79/20.28 % (541138)------------------------------
% 98.79/20.28 % (541139)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1987200213:fmbsr=2:i=46332_2945 on theBenchmark for (2945ds/46332Mi)
% 98.79/20.28 % (541139)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 98.79/20.28 % (541139)Terminated due to inappropriate strategy.
% 98.79/20.28 % (541139)------------------------------
% 98.79/20.28 % (541139)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.79/20.28 % (541139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.79/20.28 % (541139)CaDiCaL version: 2.1.3
% 98.79/20.28 % (541139)Termination reason: Inappropriate
% 98.79/20.28 % (541139)Time elapsed: 0.0000 s
% 98.79/20.28 % (541139)Peak memory usage: 10 MB
% 98.79/20.28 % (541139)------------------------------
% 98.79/20.28 % (541139)------------------------------
% 98.79/20.28 % (541141)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=734487958:i=14071_2945 on theBenchmark for (2945ds/14071Mi)
% 98.79/20.28 % (541141)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 98.79/20.28 % (541141)Terminated due to inappropriate strategy.
% 98.79/20.28 % (541141)------------------------------
% 98.79/20.28 % (541141)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.79/20.28 % (541141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.79/20.28 % (541141)CaDiCaL version: 2.1.3
% 98.79/20.28 % (541141)Termination reason: Inappropriate
% 98.79/20.28 % (541141)Time elapsed: 0.0000 s
% 98.79/20.28 % (541141)Peak memory usage: 10 MB
% 98.79/20.28 % (541141)------------------------------
% 98.79/20.28 % (541141)------------------------------
% 98.79/20.28 % (541143)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3817659211:i=22565:add=on:rawr=on_2945 on theBenchmark for (2945ds/22565Mi)
% 98.79/20.28 % (541145)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=893422364:i=8173:av=off_2945 on theBenchmark for (2945ds/8173Mi)
% 98.79/20.28 % (541098)Instruction limit reached!
% 98.79/20.28 % (541098)------------------------------
% 98.79/20.28 % (541098)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.79/20.28 % (541098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.79/20.28 % (541098)CaDiCaL version: 2.1.3
% 98.79/20.28 % (541098)Termination reason: Instruction limit
% 98.79/20.28 % (541098)Termination phase: Saturation
% 98.79/20.28 % (541098)Time elapsed: 5.281 s
% 98.79/20.28 % (541098)Peak memory usage: 38 MB
% 98.79/20.28 % (541098)Instructions burned: 5114 (million)
% 98.79/20.28 % (541148)dis+10_16:1_sil=16000:random_seed=2124782104:i=9155:fsr=off_2934 on theBenchmark for (2934ds/9155Mi)
% 98.79/20.28 % (541134)Instruction limit reached!
% 98.79/20.28 % (541134)------------------------------
% 98.79/20.28 % (541134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.79/20.28 % (541134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.79/20.28 % (541134)CaDiCaL version: 2.1.3
% 98.79/20.28 % (541134)Termination reason: Instruction limit
% 98.79/20.28 % (541134)Termination phase: Saturation
% 98.79/20.28 % (541134)Time elapsed: 4.593 s
% 98.79/20.28 % (541134)Peak memory usage: 41 MB
% 98.79/20.28 % (541134)Instructions burned: 5212 (million)
% 98.79/20.28 % (541164)ott-3_8_sil=64000:random_seed=1313539640:i=20139:bs=on_2907 on theBenchmark for (2907ds/20139Mi)
% 98.79/20.28 % (541148)Instruction limit reached!
% 98.79/20.28 % (541148)------------------------------
% 98.79/20.28 % (541148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.79/20.28 % (541148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.79/20.28 % (541148)CaDiCaL version: 2.1.3
% 98.79/20.28 % (541148)Termination reason: Instruction limit
% 98.79/20.28 % (541148)Termination phase: Saturation
% 98.79/20.28 % (541148)Time elapsed: 7.325 s
% 98.79/20.28 % (541148)Peak memory usage: 52 MB
% 98.79/20.28 % (541148)Instructions burned: 9156 (million)
% 98.79/20.28 % (541145)Instruction limit reached!
% 98.79/20.28 % (541145)------------------------------
% 98.79/20.28 % (541145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.79/20.28 % (541145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.79/20.28 % (541145)CaDiCaL version: 2.1.3
% 98.79/20.28 % (541145)Termination reason: Instruction limit
% 98.79/20.28 % (541145)Termination phase: Saturation
% 98.79/20.28 % (541145)Time elapsed: 8.368 s
% 98.79/20.28 % (541145)Peak memory usage: 52 MB
% 98.79/20.28 % (541145)Instructions burned: 8173 (million)
% 98.79/20.28 % (541178)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2801617787:fmbsr=2:i=32576_2861 on theBenchmark for (2861ds/32576Mi)
% 98.79/20.28 % (541178)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 98.79/20.28 % (541178)Terminated due to inappropriate strategy.
% 98.79/20.28 % (541178)------------------------------
% 98.79/20.28 % (541178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.79/20.28 % (541178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.79/20.28 % (541178)CaDiCaL version: 2.1.3
% 98.79/20.28 % (541178)Termination reason: Inappropriate
% 98.79/20.28 % (541178)Time elapsed: 0.001 s
% 98.79/20.28 % (541178)Peak memory usage: 10 MB
% 98.79/20.28 % (541178)------------------------------
% 98.79/20.28 % (541178)------------------------------
% 98.79/20.28 % (541179)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=4288120545:i=11404_2861 on theBenchmark for (2861ds/11404Mi)
% 98.79/20.28 % (541181)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3384249565:i=14134_2860 on theBenchmark for (2860ds/14134Mi)
% 98.79/20.28 % (541143)Instruction limit reached!
% 98.79/20.28 % (541143)------------------------------
% 98.79/20.28 % (541143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.79/20.28 % (541143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.79/20.28 % (541143)CaDiCaL version: 2.1.3
% 98.79/20.28 % (541143)Termination reason: Instruction limit
% 98.79/20.28 % (541143)Termination phase: Saturation
% 98.79/20.28 % (541143)Time elapsed: 8.785 s
% 98.79/20.28 % (541143)Peak memory usage: 73 MB
% 98.79/20.28 % (541143)Instructions burned: 22566 (million)
% 98.79/20.28 % (541184)dis+33_16_sil=32000:sac=on:random_seed=411532358:i=15851:nm=0_2857 on theBenchmark for (2857ds/15851Mi)
% 98.79/20.28 % (541049) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-541043-541049"...
% 98.79/20.28 % (541049)...printing done.
% 98.79/20.28 % (541049)Refutation found. Thanks to Tanya!
% 98.79/20.28 % SZS status Theorem for theBenchmark
% 98.79/20.28 % SZS output start Proof for theBenchmark
% 98.79/20.28 tff(func_def_6, type, sK0: $int).
% 98.79/20.28 tff(func_def_7, type, sK1: $int).
% 98.79/20.28 tff(f1,conjecture,(
% 98.79/20.28 ! [X0 : $int,X1 : $int] : ($less(X0,X1) => ? [X2 : $int] : ($less($product(X0,2),X2) & $less(X2,$product(X1,2))))),
% 98.79/20.28 file('/export/starexec/sandbox/benchmark/theBenchmark.p',mix_quant_ineq_sys_solvable_3)).
% 98.79/20.28 tff(f2,negated_conjecture,(
% 98.79/20.28 ~ ! [X0 : $int,X1 : $int] : ($less(X0,X1) => ? [X2 : $int] : ($less($product(X0,2),X2) & $less(X2,$product(X1,2))))),
% 98.79/20.28 inference(negated_conjecture,[status(cth)],[f1])).
% 98.79/20.28 tff(f3,definition,(
% 98.79/20.28 ( ! [X0 : $int,X1 : $int] : ($sum(X0,X1) = $sum(X1,X0)) )),
% 98.79/20.28 introduced(theory,[tha_commutativity])).
% 98.79/20.28 tff(f4,definition,(
% 98.79/20.28 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum(X0,$sum(X1,X2)) = $sum($sum(X0,X1),X2)) )),
% 98.79/20.28 introduced(theory,[tha_associativity])).
% 98.79/20.28 tff(f8,definition,(
% 98.79/20.28 ( ! [X0 : $int] : (~$less(X0,X0)) )),
% 98.79/20.28 introduced(theory,[tha_non-reflexivity])).
% 98.79/20.28 tff(f9,definition,(
% 98.79/20.28 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X1,X2) | ~$less(X0,X1) | $less(X0,X2)) )),
% 98.79/20.28 introduced(theory,[tha_transitivity])).
% 98.79/20.28 tff(f10,definition,(
% 98.79/20.28 ( ! [X0 : $int,X1 : $int] : ($less(X0,X1) | $less(X1,X0) | X0 = X1) )),
% 98.79/20.28 introduced(theory,[tha_order_totality])).
% 98.79/20.28 tff(f11,definition,(
% 98.79/20.28 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X0,X1) | $less($sum(X0,X2),$sum(X1,X2))) )),
% 98.79/20.28 introduced(theory,[tha_order_monotonicity])).
% 98.79/20.28 tff(f12,definition,(
% 98.79/20.28 ( ! [X0 : $int,X1 : $int] : ($less(X1,$sum(X0,1)) | $less(X0,X1)) )),
% 98.79/20.28 introduced(theory,[tha_order_plus_one_dichotomy])).
% 98.79/20.28 tff(f14,definition,(
% 98.79/20.28 ( ! [X0 : $int,X1 : $int] : ($product(X0,X1) = $product(X1,X0)) )),
% 98.79/20.28 introduced(theory,[tha_commutativity])).
% 98.79/20.28 tff(f16,definition,(
% 98.79/20.28 ( ! [X0 : $int] : ($product(X0,1) = X0) )),
% 98.79/20.28 introduced(theory,[tha_right_identity])).
% 98.79/20.28 tff(f18,definition,(
% 98.79/20.28 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($product(X0,$sum(X1,X2)) = $sum($product(X0,X1),$product(X0,X2))) )),
% 98.79/20.28 introduced(theory,[tha_distributivity])).
% 98.79/20.28 tff(f20,definition,(
% 98.79/20.28 ( ! [X0 : $int,X1 : $int] : (~$less(X1,$sum(X0,1)) | ~$less(X0,X1)) )),
% 98.79/20.28 introduced(theory,[tha_extra_integer_ordering])).
% 98.79/20.28 tff(f21,plain,(
% 98.79/20.28 ? [X0 : $int,X1 : $int] : (! [X2 : $int] : (~$less($product(X0,2),X2) | ~$less(X2,$product(X1,2))) & $less(X0,X1))),
% 98.79/20.28 inference(ennf_transformation,[],[f2])).
% 98.79/20.28 tff(f22,plain,(
% 98.79/20.28 ( ! [X2 : $int] : (~$less($product(sK0,2),X2) | ~$less(X2,$product(sK1,2))) )),
% 98.79/20.28 inference(cnf_transformation,[],[f21])).
% 98.79/20.28 tff(f23,plain,(
% 98.79/20.28 $less(sK0,sK1)),
% 98.79/20.28 inference(cnf_transformation,[],[f21])).
% 98.79/20.28 tff(f44,plain,(
% 98.79/20.28 ( ! [X0 : $int] : (~$less($product(2,sK0),X0) | ~$less(X0,$product(sK1,2))) )),
% 98.79/20.28 inference(superposition,[],[f22,f14])).
% 98.79/20.28 tff(f47,plain,(
% 98.79/20.28 ( ! [X0 : $int] : (~$less($product(2,sK0),X0) | ~$less(X0,$product(2,sK1))) )),
% 98.79/20.28 inference(forward_demodulation,[],[f44,f14])).
% 98.79/20.28 tff(f51,plain,(
% 98.79/20.28 ( ! [X0 : $int] : ($less(X0,$sum(X0,1))) )),
% 98.79/20.28 inference(resolution,[],[f12,f8])).
% 98.79/20.28 tff(f59,plain,(
% 98.79/20.28 ( ! [X0 : $int,X1 : $int] : (~$less(X0,X1) | ~$less(X1,$sum(1,X0))) )),
% 98.79/20.28 inference(superposition,[],[f20,f3])).
% 98.79/20.28 tff(f96,plain,(
% 98.79/20.28 ( ! [X0 : $int] : ($less($sum(sK0,X0),$sum(sK1,X0))) )),
% 98.79/20.28 inference(resolution,[],[f11,f23])).
% 98.79/20.28 tff(f109,plain,(
% 98.79/20.28 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum(X0,$sum(X1,X2)) = $sum(X1,$sum(X2,X0))) )),
% 98.79/20.28 inference(superposition,[],[f4,f3])).
% 98.79/20.28 tff(f114,plain,(
% 98.79/20.28 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X2,$sum(X0,$sum(X1,1))) | ~$less($sum(X0,X1),X2)) )),
% 98.79/20.28 inference(superposition,[],[f20,f4])).
% 98.79/20.28 tff(f138,plain,(
% 98.79/20.28 ( ! [X0 : $int,X1 : $int] : ($product(X0,$sum(1,X1)) = $sum(X0,$product(X0,X1))) )),
% 98.79/20.28 inference(superposition,[],[f18,f16])).
% 98.79/20.28 tff(f170,plain,(
% 98.79/20.28 ( ! [X0 : $int,X1 : $int] : ($less(X0,$sum(sK1,X1)) | ~$less(X0,$sum(sK0,X1))) )),
% 98.79/20.28 inference(resolution,[],[f96,f9])).
% 98.79/20.28 tff(f204,plain,(
% 98.79/20.28 ~$less($sum($product(2,sK0),1),$product(2,sK1))),
% 98.79/20.28 inference(resolution,[],[f51,f47])).
% 98.79/20.28 tff(f212,plain,(
% 98.79/20.28 ~$less($sum(1,$product(2,sK0)),$product(2,sK1))),
% 98.79/20.28 inference(forward_demodulation,[],[f204,f3])).
% 98.79/20.28 tff(f241,plain,(
% 98.79/20.28 ( ! [X0 : $int] : (~$less($sum(sK1,X0),$sum(1,$sum(sK0,X0)))) )),
% 98.79/20.28 inference(resolution,[],[f59,f96])).
% 98.79/20.28 tff(f583,plain,(
% 98.79/20.28 ( ! [X0 : $int,X1 : $int] : ($less($sum(sK0,$sum(X1,X0)),$sum(X0,$sum(sK1,X1)))) )),
% 98.79/20.28 inference(superposition,[],[f96,f109])).
% 98.79/20.28 tff(f865,plain,(
% 98.79/20.28 ( ! [X0 : $int] : ($product(X0,$sum(1,1)) = $sum(X0,X0)) )),
% 98.79/20.28 inference(superposition,[],[f138,f16])).
% 98.79/20.28 tff(f885,plain,(
% 98.79/20.28 ( ! [X0 : $int] : ($less($sum(sK0,$product(sK1,X0)),$product(sK1,$sum(1,X0)))) )),
% 98.79/20.28 inference(superposition,[],[f96,f138])).
% 98.79/20.28 tff(f887,plain,(
% 98.79/20.28 ( ! [X0 : $int] : ($product(X0,2) = $sum(X0,X0)) )),
% 98.79/20.28 inference(evaluation,[],[f865])).
% 98.79/20.28 tff(f1939,plain,(
% 98.79/20.28 $less($product(2,sK1),$sum(1,$product(2,sK0))) | $product(2,sK1) = $sum(1,$product(2,sK0))),
% 98.79/20.28 inference(resolution,[],[f212,f10])).
% 98.79/20.28 tff(f1942,definition,(
% 98.79/20.28 spl2_18 <=> $product(2,sK1) = $sum(1,$product(2,sK0))),
% 98.79/20.28 introduced(definition,[new_symbols(definition,[spl2_18])],[avatar_definition])).
% 98.79/20.28 tff(f1944,plain,(
% 98.79/20.28 $product(2,sK1) = $sum(1,$product(2,sK0)) | ~spl2_18),
% 98.79/20.28 inference(avatar_component_clause,[],[f1942])).
% 98.79/20.28 tff(f1946,definition,(
% 98.79/20.28 spl2_19 <=> $less($product(2,sK1),$sum(1,$product(2,sK0)))),
% 98.79/20.28 introduced(definition,[new_symbols(definition,[spl2_19])],[avatar_definition])).
% 98.79/20.28 tff(f1950,plain,(
% 98.79/20.28 spl2_18 | spl2_19),
% 98.79/20.28 inference(avatar_split_clause,[],[f1939,f1946,f1942])).
% 98.79/20.28 tff(f1975,plain,(
% 98.79/20.28 ( ! [X0 : $int] : (~$less($sum(sK1,X0),$sum(X0,$sum(1,sK0)))) )),
% 98.79/20.28 inference(superposition,[],[f241,f109])).
% 98.79/20.28 tff(f2486,plain,(
% 98.79/20.28 ( ! [X0 : $int] : (~$less($sum(X0,sK1),$sum(sK0,$sum(1,X0)))) )),
% 98.79/20.28 inference(resolution,[],[f583,f114])).
% 98.79/20.28 tff(f2574,plain,(
% 98.79/20.28 ( ! [X0 : $int] : (~$less($sum(X0,sK1),$sum(1,$sum(X0,sK0)))) )),
% 98.79/20.28 inference(forward_demodulation,[],[f2486,f109])).
% 98.79/20.28 tff(f2641,plain,(
% 98.79/20.28 $less($sum(sK0,sK1),$product(sK1,$sum(1,1)))),
% 98.79/20.28 inference(superposition,[],[f885,f16])).
% 98.79/20.28 tff(f2656,plain,(
% 98.79/20.28 $less($sum(sK0,sK1),$product(sK1,2))),
% 98.79/20.28 inference(evaluation,[],[f2641])).
% 98.79/20.28 tff(f2658,plain,(
% 98.79/20.28 $less($sum(sK0,sK1),$product(2,sK1))),
% 98.79/20.28 inference(forward_demodulation,[],[f2656,f14])).
% 98.79/20.28 tff(f368092,plain,(
% 98.79/20.28 ~$less($sum(sK1,sK1),$sum(sK0,$sum(1,sK0)))),
% 98.79/20.28 inference(resolution,[],[f1975,f170])).
% 98.79/20.28 tff(f368286,plain,(
% 98.79/20.28 ~$less($sum(sK1,sK1),$sum(1,$sum(sK0,sK0)))),
% 98.79/20.28 inference(forward_demodulation,[],[f368092,f109])).
% 98.79/20.28 tff(f368349,plain,(
% 98.79/20.28 ~$less($sum(sK1,sK1),$sum(1,$product(sK0,2)))),
% 98.79/20.28 inference(forward_demodulation,[],[f368286,f887])).
% 98.79/20.28 tff(f368369,plain,(
% 98.79/20.28 ~$less($sum(sK1,sK1),$sum(1,$product(2,sK0)))),
% 98.79/20.28 inference(forward_demodulation,[],[f368349,f14])).
% 98.79/20.28 tff(f368379,plain,(
% 98.79/20.28 ~$less($product(sK1,2),$sum(1,$product(2,sK0)))),
% 98.79/20.28 inference(forward_demodulation,[],[f368369,f887])).
% 98.79/20.28 tff(f368384,plain,(
% 98.79/20.28 ~$less($product(2,sK1),$sum(1,$product(2,sK0)))),
% 98.79/20.28 inference(forward_demodulation,[],[f368379,f14])).
% 98.79/20.28 tff(f368393,plain,(
% 98.79/20.28 ~spl2_19),
% 98.79/20.28 inference(avatar_split_clause,[],[f368384,f1946])).
% 98.79/20.28 tff(f369729,plain,(
% 98.79/20.28 ~$less($sum(sK0,sK1),$sum(1,$product(sK0,2)))),
% 98.79/20.28 inference(superposition,[],[f2574,f887])).
% 98.79/20.28 tff(f369781,plain,(
% 98.79/20.28 ~$less($sum(sK0,sK1),$sum(1,$product(2,sK0)))),
% 98.79/20.28 inference(forward_demodulation,[],[f369729,f14])).
% 98.79/20.28 tff(f369821,plain,(
% 98.79/20.28 ~$less($sum(sK0,sK1),$product(2,sK1)) | ~spl2_18),
% 98.79/20.28 inference(forward_demodulation,[],[f369781,f1944])).
% 98.79/20.28 tff(f369835,plain,(
% 98.79/20.28 $false | ~spl2_18),
% 98.79/20.28 inference(forward_subsumption_resolution,[],[f369821,f2658])).
% 98.79/20.28 tff(f369836,plain,(
% 98.79/20.28 ~spl2_18),
% 98.79/20.28 inference(avatar_contradiction_clause,[],[f369835])).
% 98.79/20.28 cnf(s16, plain, spl2_18 | spl2_19, inference(sat_conversion,[],[f1950])).
% 98.79/20.28 cnf(s9288, plain, ~spl2_19, inference(sat_conversion,[],[f368393])).
% 98.79/20.28 cnf(s9330, plain, ~spl2_18, inference(sat_conversion,[],[f369836])).
% 98.79/20.28 cnf(s9337, plain, $false, inference(rat,[],[s16,s9288,s9330])).
% 98.79/20.28 tff(f369843,plain,(
% 98.79/20.28 $false),
% 98.79/20.28 inference(avatar_sat_refutation,[],[s9337])).
% 98.79/20.28 % SZS output end Proof for theBenchmark
% 98.79/20.28 % (541049)------------------------------
% 98.79/20.28 % (541049)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.79/20.28 % (541049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.79/20.28 % (541049)CaDiCaL version: 2.1.3
% 98.79/20.28 % (541049)Termination reason: Refutation
% 98.79/20.28 % (541049)Time elapsed: 19.788 s
% 98.79/20.28 % (541049)Peak memory usage: 139 MB
% 98.79/20.28 % (541049)Instructions burned: 21941 (million)
% 98.79/20.28 % (541043)Success in time 19.965 s
% 98.79/20.28 % Vampire exiting
%------------------------------------------------------------------------------