%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWX093_1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n014.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 01:46:28 PM UTC 2026
% Result : Theorem 6.68s 1.23s
% Output : Refutation 6.68s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX093_1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.20 % Computer : n014.cluster.edu
% 0.10/0.20 % Model : x86_64 x86_64
% 0.10/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.20 % Memory : 8046.5625MB
% 0.10/0.20 % OS : Linux 6.8.0-71-generic
% 0.10/0.20 % CPULimit : 300
% 0.10/0.20 % WCLimit : 300
% 0.10/0.20 % DateTime : Mon Sep 28 15:00:45 UTC 2026
% 0.10/0.20 % CPUTime :
% 0.10/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.23 Running first-order model finding
% 0.10/0.23 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
% 4.11/0.92 % (1832773)Will run a generic schedule for satisfiability detection.
% 4.11/0.92 % (1832794)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=118514272:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.11/0.92 % (1832790)% WARNING: option uhcvi not known.
% 4.11/0.92 % (1832789)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3584020186_2999 on theBenchmark for (2999ds/0Mi)
% 4.11/0.92 % (1832790)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1504672933:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.11/0.92 % (1832791)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3955185590:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.11/0.92 % (1832792)dis+10_1_sil=32000:sp=arity:random_seed=87169715:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.11/0.92 % (1832793)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=344947723:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.11/0.92 % (1832795)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2111139136:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.11/0.92 % (1832789)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 4.11/0.92 % (1832789)Terminated due to inappropriate strategy.
% 4.11/0.92 % (1832789)------------------------------
% 4.11/0.92 % (1832789)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.11/0.92 % (1832789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.11/0.92 % (1832789)CaDiCaL version: 2.1.3
% 4.11/0.92 % (1832789)Termination reason: Inappropriate
% 4.11/0.92 % (1832789)Time elapsed: 0.002 s
% 4.11/0.92 % (1832789)Peak memory usage: 11 MB
% 4.11/0.92 % (1832789)Instructions burned: 4 (million)
% 4.11/0.92 % (1832789)------------------------------
% 4.11/0.92 % (1832789)------------------------------
% 4.11/0.92 % (1832813)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=726332631:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 4.11/0.92 % (1832813)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 4.11/0.92 % (1832813)Terminated due to inappropriate strategy.
% 4.11/0.92 % (1832813)------------------------------
% 4.11/0.92 % (1832813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.11/0.92 % (1832813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.11/0.92 % (1832813)CaDiCaL version: 2.1.3
% 4.11/0.92 % (1832813)Termination reason: Inappropriate
% 4.11/0.92 % (1832813)Time elapsed: 0.002 s
% 4.11/0.92 % (1832813)Peak memory usage: 10 MB
% 4.11/0.92 % (1832813)Instructions burned: 3 (million)
% 4.11/0.92 % (1832813)------------------------------
% 4.11/0.92 % (1832813)------------------------------
% 4.11/0.92 % (1832794)Instruction limit reached!
% 4.11/0.92 % (1832794)------------------------------
% 4.11/0.92 % (1832794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.11/0.92 % (1832794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.11/0.92 % (1832794)CaDiCaL version: 2.1.3
% 4.11/0.92 % (1832794)Termination reason: Instruction limit
% 4.11/0.92 % (1832794)Termination phase: Saturation
% 4.11/0.92 % (1832794)Time elapsed: 0.046 s
% 4.11/0.92 % (1832794)Peak memory usage: 13 MB
% 4.11/0.92 % (1832794)Instructions burned: 133 (million)
% 4.11/0.92 % (1832822)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=819604862:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 4.11/0.92 % (1832825)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=471926276:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 4.11/0.92 % (1832792)Instruction limit reached!
% 4.11/0.92 % (1832792)------------------------------
% 4.11/0.92 % (1832792)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.11/0.92 % (1832792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.11/0.92 % (1832792)CaDiCaL version: 2.1.3
% 4.11/0.92 % (1832792)Termination reason: Instruction limit
% 4.11/0.92 % (1832792)Termination phase: Saturation
% 4.11/0.92 % (1832792)Time elapsed: 0.068 s
% 4.11/0.92 % (1832792)Peak memory usage: 13 MB
% 4.11/0.92 % (1832792)Instructions burned: 104 (million)
% 4.11/0.92 % (1832793)Instruction limit reached!
% 4.11/0.92 % (1832793)------------------------------
% 4.11/0.92 % (1832793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.60/1.11 % (1832793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.11 % (1832793)CaDiCaL version: 2.1.3
% 5.60/1.11 % (1832793)Termination reason: Instruction limit
% 5.60/1.11 % (1832793)Termination phase: Saturation
% 5.60/1.11 % (1832793)Time elapsed: 0.078 s
% 5.60/1.11 % (1832793)Peak memory usage: 13 MB
% 5.60/1.11 % (1832793)Instructions burned: 117 (million)
% 5.60/1.11 % (1832834)ott-21_1_sil=16000:fs=off:random_seed=1478493594:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 5.60/1.11 % (1832839)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3418975674:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 5.60/1.11 % (1832795)Instruction limit reached!
% 5.60/1.11 % (1832795)------------------------------
% 5.60/1.11 % (1832795)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.60/1.11 % (1832795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.11 % (1832795)CaDiCaL version: 2.1.3
% 5.60/1.11 % (1832795)Termination reason: Instruction limit
% 5.60/1.11 % (1832795)Termination phase: Saturation
% 5.60/1.11 % (1832795)Time elapsed: 0.116 s
% 5.60/1.11 % (1832795)Peak memory usage: 13 MB
% 5.60/1.11 % (1832795)Instructions burned: 159 (million)
% 5.60/1.11 % (1832854)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3692930843:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 5.60/1.11 % (1832854)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 5.60/1.11 % (1832854)Terminated due to inappropriate strategy.
% 5.60/1.11 % (1832854)------------------------------
% 5.60/1.11 % (1832854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.60/1.11 % (1832854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.11 % (1832854)CaDiCaL version: 2.1.3
% 5.60/1.11 % (1832854)Termination reason: Inappropriate
% 5.60/1.11 % (1832854)Time elapsed: 0.003 s
% 5.60/1.11 % (1832854)Peak memory usage: 10 MB
% 5.60/1.11 % (1832854)Instructions burned: 5 (million)
% 5.60/1.11 % (1832822)Instruction limit reached!
% 5.60/1.11 % (1832822)------------------------------
% 5.60/1.11 % (1832822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.60/1.11 % (1832822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.11 % (1832822)CaDiCaL version: 2.1.3
% 5.60/1.11 % (1832822)Termination reason: Instruction limit
% 5.60/1.11 % (1832822)Termination phase: Saturation
% 5.60/1.11 % (1832822)Time elapsed: 0.095 s
% 5.60/1.11 % (1832822)Peak memory usage: 13 MB
% 5.60/1.11 % (1832822)Instructions burned: 131 (million)
% 5.60/1.11 % (1832854)------------------------------
% 5.60/1.11 % (1832854)------------------------------
% 5.60/1.11 % (1832872)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2264431406:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 5.60/1.11 % (1832873)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1779982792:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 5.60/1.11 % (1832873)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 5.60/1.11 % (1832873)Terminated due to inappropriate strategy.
% 5.60/1.11 % (1832873)------------------------------
% 5.60/1.11 % (1832873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.60/1.11 % (1832873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.11 % (1832873)CaDiCaL version: 2.1.3
% 5.60/1.11 % (1832873)Termination reason: Inappropriate
% 5.60/1.11 % (1832873)Time elapsed: 0.002 s
% 5.60/1.11 % (1832873)Peak memory usage: 10 MB
% 5.60/1.11 % (1832873)Instructions burned: 3 (million)
% 5.60/1.11 % (1832873)------------------------------
% 5.60/1.11 % (1832873)------------------------------
% 5.60/1.11 % (1832834)Instruction limit reached!
% 5.60/1.11 % (1832834)------------------------------
% 5.60/1.11 % (1832834)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.60/1.11 % (1832834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.11 % (1832834)CaDiCaL version: 2.1.3
% 5.60/1.11 % (1832834)Termination reason: Instruction limit
% 5.60/1.11 % (1832834)Termination phase: Saturation
% 5.60/1.11 % (1832834)Time elapsed: 0.083 s
% 5.60/1.11 % (1832834)Peak memory usage: 12 MB
% 5.60/1.11 % (1832834)Instructions burned: 181 (million)
% 5.60/1.11 % (1832891)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=1457311924: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)
% 6.68/1.23 % (1832896)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=389386341:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 6.68/1.23 % (1832825)Instruction limit reached!
% 6.68/1.23 % (1832825)------------------------------
% 6.68/1.23 % (1832825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.68/1.23 % (1832825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.68/1.23 % (1832825)CaDiCaL version: 2.1.3
% 6.68/1.23 % (1832825)Termination reason: Instruction limit
% 6.68/1.23 % (1832825)Termination phase: Saturation
% 6.68/1.23 % (1832825)Time elapsed: 0.185 s
% 6.68/1.23 % (1832825)Peak memory usage: 19 MB
% 6.68/1.23 % (1832825)Instructions burned: 684 (million)
% 6.68/1.23 % (1832903)fmb+10_1_sil=64000:random_seed=957059849:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi)
% 6.68/1.23 % (1832903)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.68/1.23 % (1832903)Terminated due to inappropriate strategy.
% 6.68/1.23 % (1832903)------------------------------
% 6.68/1.23 % (1832903)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.68/1.23 % (1832903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.68/1.23 % (1832903)CaDiCaL version: 2.1.3
% 6.68/1.23 % (1832903)Termination reason: Inappropriate
% 6.68/1.23 % (1832903)Time elapsed: 0.001 s
% 6.68/1.23 % (1832903)Peak memory usage: 10 MB
% 6.68/1.23 % (1832903)Instructions burned: 4 (million)
% 6.68/1.23 % (1832903)------------------------------
% 6.68/1.23 % (1832903)------------------------------
% 6.68/1.23 % (1832905)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=626147560:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi)
% 6.68/1.23 % (1832905)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.68/1.23 % (1832905)Terminated due to inappropriate strategy.
% 6.68/1.23 % (1832905)------------------------------
% 6.68/1.23 % (1832905)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.68/1.23 % (1832905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.68/1.23 % (1832905)CaDiCaL version: 2.1.3
% 6.68/1.23 % (1832905)Termination reason: Inappropriate
% 6.68/1.23 % (1832905)Time elapsed: 0.001 s
% 6.68/1.23 % (1832905)Peak memory usage: 10 MB
% 6.68/1.23 % (1832905)Instructions burned: 3 (million)
% 6.68/1.23 % (1832905)------------------------------
% 6.68/1.23 % (1832905)------------------------------
% 6.68/1.23 % (1832907)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2188158816:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi)
% 6.68/1.23 % (1832907)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.68/1.23 % (1832907)Terminated due to inappropriate strategy.
% 6.68/1.23 % (1832907)------------------------------
% 6.68/1.23 % (1832907)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.68/1.23 % (1832907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.68/1.23 % (1832907)CaDiCaL version: 2.1.3
% 6.68/1.23 % (1832907)Termination reason: Inappropriate
% 6.68/1.23 % (1832907)Time elapsed: 0.001 s
% 6.68/1.23 % (1832907)Peak memory usage: 11 MB
% 6.68/1.23 % (1832907)Instructions burned: 3 (million)
% 6.68/1.23 % (1832907)------------------------------
% 6.68/1.23 % (1832907)------------------------------
% 6.68/1.23 % (1832909)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=720445764:i=5131_2996 on theBenchmark for (2996ds/5131Mi)
% 6.68/1.23 % (1832839)Instruction limit reached!
% 6.68/1.23 % (1832839)------------------------------
% 6.68/1.23 % (1832839)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.68/1.23 % (1832839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.68/1.23 % (1832839)CaDiCaL version: 2.1.3
% 6.68/1.23 % (1832839)Termination reason: Instruction limit
% 6.68/1.23 % (1832839)Termination phase: Saturation
% 6.68/1.23 % (1832839)Time elapsed: 0.336 s
% 6.68/1.23 % (1832839)Peak memory usage: 14 MB
% 6.68/1.23 % (1832839)Instructions burned: 478 (million)
% 6.68/1.23 % (1832911)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4019012243:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 6.68/1.23 % (1832891)Instruction limit reached!
% 6.68/1.23 % (1832891)------------------------------
% 6.68/1.23 % (1832891)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.68/1.23 % (1832891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.68/1.23 % (1832891)CaDiCaL version: 2.1.3
% 6.68/1.23 % (1832891)Termination reason: Instruction limit
% 6.68/1.23 % (1832891)Termination phase: Saturation
% 6.68/1.23 % (1832891)Time elapsed: 0.451 s
% 6.68/1.23 % (1832891)Peak memory usage: 19 MB
% 6.68/1.23 % (1832891)Instructions burned: 694 (million)
% 6.68/1.23 % (1832913)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=732474424:i=6324_2993 on theBenchmark for (2993ds/6324Mi)
% 6.68/1.23 % (1832913)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.68/1.23 % (1832913)Terminated due to inappropriate strategy.
% 6.68/1.23 % (1832913)------------------------------
% 6.68/1.23 % (1832913)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.68/1.23 % (1832913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.68/1.23 % (1832913)CaDiCaL version: 2.1.3
% 6.68/1.23 % (1832913)Termination reason: Inappropriate
% 6.68/1.23 % (1832913)Time elapsed: 0.002 s
% 6.68/1.23 % (1832913)Peak memory usage: 11 MB
% 6.68/1.23 % (1832913)Instructions burned: 3 (million)
% 6.68/1.23 % (1832913)------------------------------
% 6.68/1.23 % (1832913)------------------------------
% 6.68/1.23 % (1832915)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3000952625:fmbsr=2.30978:i=2174_2992 on theBenchmark for (2992ds/2174Mi)
% 6.68/1.23 % (1832915)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.68/1.23 % (1832915)Terminated due to inappropriate strategy.
% 6.68/1.23 % (1832915)------------------------------
% 6.68/1.23 % (1832915)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.68/1.23 % (1832915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.68/1.23 % (1832915)CaDiCaL version: 2.1.3
% 6.68/1.23 % (1832915)Termination reason: Inappropriate
% 6.68/1.23 % (1832915)Time elapsed: 0.002 s
% 6.68/1.23 % (1832915)Peak memory usage: 10 MB
% 6.68/1.23 % (1832915)Instructions burned: 3 (million)
% 6.68/1.23 % (1832915)------------------------------
% 6.68/1.23 % (1832915)------------------------------
% 6.68/1.23 % (1832917)ott-2_1_sil=16000:newcnf=on:random_seed=3138098288:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2992 on theBenchmark for (2992ds/869Mi)
% 6.68/1.23 % (1832896)Instruction limit reached!
% 6.68/1.23 % (1832896)------------------------------
% 6.68/1.23 % (1832896)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.68/1.23 % (1832896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.68/1.23 % (1832896)CaDiCaL version: 2.1.3
% 6.68/1.23 % (1832896)Termination reason: Instruction limit
% 6.68/1.23 % (1832896)Termination phase: Saturation
% 6.68/1.23 % (1832896)Time elapsed: 0.509 s
% 6.68/1.23 % (1832896)Peak memory usage: 19 MB
% 6.68/1.23 % (1832896)Instructions burned: 880 (million)
% 6.68/1.23 % (1832919)ott+10_1_sil=32000:tgt=ground:random_seed=76646778:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi)
% 6.68/1.23 % (1832872)Instruction limit reached!
% 6.68/1.23 % (1832872)------------------------------
% 6.68/1.23 % (1832872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.68/1.23 % (1832872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.68/1.23 % (1832872)CaDiCaL version: 2.1.3
% 6.68/1.23 % (1832872)Termination reason: Instruction limit
% 6.68/1.23 % (1832872)Termination phase: Saturation
% 6.68/1.23 % (1832872)Time elapsed: 0.638 s
% 6.68/1.23 % (1832872)Peak memory usage: 17 MB
% 6.68/1.23 % (1832872)Instructions burned: 1180 (million)
% 6.68/1.23 % (1832921)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2053074897:i=54282_2991 on theBenchmark for (2991ds/54282Mi)
% 6.68/1.23 % (1832921)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.68/1.23 % (1832921)Terminated due to inappropriate strategy.
% 6.68/1.23 % (1832921)------------------------------
% 6.68/1.23 % (1832921)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.68/1.23 % (1832921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.68/1.23 % (1832921)CaDiCaL version: 2.1.3
% 6.68/1.23 % (1832921)Termination reason: Inappropriate
% 6.68/1.23 % (1832921)Time elapsed: 0.002 s
% 6.68/1.23 % (1832921)Peak memory usage: 11 MB
% 6.68/1.23 % (1832921)Instructions burned: 4 (million)
% 6.68/1.23 % (1832921)------------------------------
% 6.68/1.23 % (1832921)------------------------------
% 6.68/1.23 % (1832923)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2318129359:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi)
% 6.68/1.23 % (1832919) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1832773-1832919"...
% 6.68/1.23 % (1832919)...printing done.
% 6.68/1.23 % (1832919)Refutation found. Thanks to Tanya!
% 6.68/1.23 % SZS status Theorem for theBenchmark
% 6.68/1.23 % SZS output start Proof for theBenchmark
% 6.68/1.23 tff(type_def_5, type, general: $tType).
% 6.68/1.23 tff(type_def_6, type, symbol: $tType).
% 6.68/1.23 tff(func_def_0, type, f__integer__: $int > general).
% 6.68/1.23 tff(func_def_1, type, f__symbolic__: symbol > general).
% 6.68/1.23 tff(func_def_2, type, c__infimum__: general).
% 6.68/1.23 tff(func_def_3, type, c__supremum__: general).
% 6.68/1.23 tff(func_def_4, type, n_i: $int).
% 6.68/1.23 tff(func_def_10, type, sK3: general > $int).
% 6.68/1.23 tff(func_def_11, type, sK4: general > symbol).
% 6.68/1.23 tff(func_def_12, type, sK5: general > general).
% 6.68/1.23 tff(func_def_13, type, sK6: general > general).
% 6.68/1.23 tff(func_def_14, type, sK7: general > $int).
% 6.68/1.23 tff(func_def_15, type, sK8: general > $int).
% 6.68/1.23 tff(func_def_16, type, sK9: general > general).
% 6.68/1.23 tff(func_def_17, type, sK10: general > general).
% 6.68/1.23 tff(func_def_18, type, sK11: general > $int).
% 6.68/1.23 tff(func_def_19, type, sK12: general > $int).
% 6.68/1.23 tff(func_def_20, type, sK13: general > $int).
% 6.68/1.23 tff(func_def_21, type, sK14: (general * general) > $int).
% 6.68/1.23 tff(func_def_22, type, sK15: (general * general) > $int).
% 6.68/1.23 tff(func_def_23, type, sK16: (general * general) > $int).
% 6.68/1.23 tff(func_def_24, type, sK17: (general * general) > $int).
% 6.68/1.23 tff(func_def_25, type, sK18: (general * general) > $int).
% 6.68/1.23 tff(func_def_26, type, sK19: (general * general) > $int).
% 6.68/1.23 tff(func_def_27, type, sK20: general > general).
% 6.68/1.23 tff(func_def_28, type, sK21: general > general).
% 6.68/1.23 tff(func_def_29, type, sK22: general > general).
% 6.68/1.23 tff(func_def_30, type, sK23: $int > $int).
% 6.68/1.23 tff(func_def_31, type, sK24: $int).
% 6.68/1.23 tff(func_def_32, type, sK25: $int).
% 6.68/1.23 tff(func_def_33, type, sK26: $int).
% 6.68/1.23 tff(func_def_34, type, sK27: general).
% 6.68/1.23 tff(func_def_35, type, sF28: $int).
% 6.68/1.23 tff(func_def_36, type, sF29: general).
% 6.68/1.23 tff(func_def_37, type, sF30: $int).
% 6.68/1.23 tff(func_def_38, type, sF31: $int).
% 6.68/1.23 tff(func_def_39, type, sF32: general).
% 6.68/1.23 tff(func_def_40, type, sF33: $int).
% 6.68/1.23 tff(func_def_41, type, sF34: general).
% 6.68/1.23 tff(pred_def_1, type, p__is_integer__: general > $o).
% 6.68/1.23 tff(pred_def_2, type, p__is_symbolic__: general > $o).
% 6.68/1.23 tff(pred_def_3, type, p__less_equal__: (general * general) > $o).
% 6.68/1.23 tff(pred_def_4, type, p__less__: (general * general) > $o).
% 6.68/1.23 tff(pred_def_5, type, p__greater_equal__: (general * general) > $o).
% 6.68/1.23 tff(pred_def_6, type, p__greater__: (general * general) > $o).
% 6.68/1.23 tff(pred_def_8, type, three: general > $o).
% 6.68/1.23 tff(pred_def_9, type, sqrt: general > $o).
% 6.68/1.23 tff(pred_def_10, type, three_p: general > $o).
% 6.68/1.23 tff(pred_def_11, type, more_than_three: general > $o).
% 6.68/1.23 tff(pred_def_12, type, sqrt: (general * general) > $o).
% 6.68/1.23 tff(pred_def_15, type, sP0: (general * general) > $o).
% 6.68/1.23 tff(pred_def_16, type, sP1: general > $o).
% 6.68/1.23 tff(pred_def_17, type, sP2: general > $o).
% 6.68/1.23 tff(f6,axiom,(
% 6.68/1.23 ! [X0 : $int,X1 : $int] : (p__less_equal__(f__integer__(X0),f__integer__(X1)) <=> $lesseq(X0,X1))),
% 6.68/1.23 file('/export/starexec/sandbox/benchmark/Axioms/SWV014_0.ax',numeral_ordering_ax)).
% 6.68/1.23 tff(f7,axiom,(
% 6.68/1.23 ! [X0 : general,X1 : general] : ((p__less_equal__(X0,X1) & p__less_equal__(X1,X0)) => X0 = X1)),
% 6.68/1.23 file('/export/starexec/sandbox/benchmark/Axioms/SWV014_0.ax',antisymmetric_ordering_ax)).
% 6.68/1.23 tff(f8,axiom,(
% 6.68/1.23 ! [X0 : general,X1 : general,X2 : general] : ((p__less_equal__(X0,X1) & p__less_equal__(X1,X2)) => p__less_equal__(X0,X2))),
% 6.68/1.23 file('/export/starexec/sandbox/benchmark/Axioms/SWV014_0.ax',transitive_ordering_ax)).
% 6.68/1.23 tff(f12,axiom,(
% 6.68/1.23 ! [X0 : general,X1 : general] : (p__greater__(X0,X1) <=> (p__less_equal__(X1,X0) & X0 != X1))),
% 6.68/1.23 file('/export/starexec/sandbox/benchmark/Axioms/SWV014_0.ax',p__greater__def_ax)).
% 6.68/1.23 tff(f25,axiom,(
% 6.68/1.23 ! [X0 : $int,X1 : $int] : (($greatereq(X0,1) & $greatereq(X1,1) & $less(X0,X1)) => $less($product(X0,X0),$product(X1,X1)))),
% 6.68/1.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_9_unnamed_formula)).
% 6.68/1.23 tff(f26,conjecture,(
% 6.68/1.23 ! [X0 : $int,X1 : $int,X2 : general] : (($greatereq(X0,0) & p__less_equal__(f__integer__($product(X0,X0)),X2) & p__greater__(f__integer__($product($sum(X0,1),$sum(X0,1))),X2) & p__less_equal__(f__integer__($product(X1,X1)),X2) & $greatereq(X1,0)) => $lesseq(X1,X0))),
% 6.68/1.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_10_unnamed_formula)).
% 6.68/1.23 tff(f27,negated_conjecture,(
% 6.68/1.23 ~ ! [X0 : $int,X1 : $int,X2 : general] : (($greatereq(X0,0) & p__less_equal__(f__integer__($product(X0,X0)),X2) & p__greater__(f__integer__($product($sum(X0,1),$sum(X0,1))),X2) & p__less_equal__(f__integer__($product(X1,X1)),X2) & $greatereq(X1,0)) => $lesseq(X1,X0))),
% 6.68/1.23 inference(negated_conjecture,[status(cth)],[f26])).
% 6.68/1.23 tff(f28,plain,(
% 6.68/1.23 ! [X0 : $int,X1 : $int] : (p__less_equal__(f__integer__(X0),f__integer__(X1)) <=> ~$less(X1,X0))),
% 6.68/1.23 inference(theory_normalization,[],[f6])).
% 6.68/1.23 tff(f37,plain,(
% 6.68/1.23 ! [X0 : $int,X1 : $int] : ((~$less(X0,1) & ~$less(X1,1) & $less(X0,X1)) => $less($product(X0,X0),$product(X1,X1)))),
% 6.68/1.23 inference(theory_normalization,[],[f25])).
% 6.68/1.23 tff(f38,plain,(
% 6.68/1.23 ~ ! [X0 : $int,X1 : $int,X2 : general] : ((~$less(X0,0) & p__less_equal__(f__integer__($product(X0,X0)),X2) & p__greater__(f__integer__($product($sum(X0,1),$sum(X0,1))),X2) & p__less_equal__(f__integer__($product(X1,X1)),X2) & ~$less(X1,0)) => ~$less(X0,X1))),
% 6.68/1.23 inference(theory_normalization,[],[f27])).
% 6.68/1.23 tff(f39,definition,(
% 6.68/1.23 ( ! [X0 : $int,X1 : $int] : ($sum(X0,X1) = $sum(X1,X0)) )),
% 6.68/1.23 introduced(theory,[tha_commutativity])).
% 6.68/1.23 tff(f41,definition,(
% 6.68/1.23 ( ! [X0 : $int] : ($sum(X0,0) = X0) )),
% 6.68/1.23 introduced(theory,[tha_right_identity])).
% 6.68/1.23 tff(f44,definition,(
% 6.68/1.23 ( ! [X0 : $int] : (~$less(X0,X0)) )),
% 6.68/1.23 introduced(theory,[tha_non-reflexivity])).
% 6.68/1.23 tff(f45,definition,(
% 6.68/1.23 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X1,X2) | ~$less(X0,X1) | $less(X0,X2)) )),
% 6.68/1.23 introduced(theory,[tha_transitivity])).
% 6.68/1.23 tff(f46,definition,(
% 6.68/1.23 ( ! [X0 : $int,X1 : $int] : ($less(X1,X0) | $less(X0,X1) | X0 = X1) )),
% 6.68/1.23 introduced(theory,[tha_order_totality])).
% 6.68/1.23 tff(f48,definition,(
% 6.68/1.23 ( ! [X0 : $int,X1 : $int] : ($less(X1,$sum(X0,1)) | $less(X0,X1)) )),
% 6.68/1.23 introduced(theory,[tha_order_plus_one_dichotomy])).
% 6.68/1.23 tff(f56,definition,(
% 6.68/1.23 ( ! [X0 : $int,X1 : $int] : (~$less(X1,$sum(X0,1)) | ~$less(X0,X1)) )),
% 6.68/1.23 introduced(theory,[tha_extra_integer_ordering])).
% 6.68/1.23 tff(f62,plain,(
% 6.68/1.23 ! [X0 : general,X1 : general] : (p__greater__(X0,X1) => (p__less_equal__(X1,X0) & X0 != X1))),
% 6.68/1.23 inference(unused_predicate_definition_removal,[],[f12])).
% 6.68/1.23 tff(f68,plain,(
% 6.68/1.23 ! [X0 : general,X1 : general] : (X0 = X1 | (~p__less_equal__(X0,X1) | ~p__less_equal__(X1,X0)))),
% 6.68/1.23 inference(ennf_transformation,[],[f7])).
% 6.68/1.23 tff(f69,plain,(
% 6.68/1.23 ! [X0 : general,X1 : general] : (X0 = X1 | ~p__less_equal__(X0,X1) | ~p__less_equal__(X1,X0))),
% 6.68/1.23 inference(flattening,[],[f68])).
% 6.68/1.23 tff(f70,plain,(
% 6.68/1.23 ! [X0 : general,X1 : general,X2 : general] : (p__less_equal__(X0,X2) | (~p__less_equal__(X0,X1) | ~p__less_equal__(X1,X2)))),
% 6.68/1.23 inference(ennf_transformation,[],[f8])).
% 6.68/1.23 tff(f71,plain,(
% 6.68/1.23 ! [X0 : general,X1 : general,X2 : general] : (p__less_equal__(X0,X2) | ~p__less_equal__(X0,X1) | ~p__less_equal__(X1,X2))),
% 6.68/1.23 inference(flattening,[],[f70])).
% 6.68/1.23 tff(f73,plain,(
% 6.68/1.23 ! [X0 : general,X1 : general] : ((p__less_equal__(X1,X0) & X0 != X1) | ~p__greater__(X0,X1))),
% 6.68/1.23 inference(ennf_transformation,[],[f62])).
% 6.68/1.23 tff(f78,plain,(
% 6.68/1.23 ! [X0 : $int,X1 : $int] : ($less($product(X0,X0),$product(X1,X1)) | ($less(X0,1) | $less(X1,1) | ~$less(X0,X1)))),
% 6.68/1.23 inference(ennf_transformation,[],[f37])).
% 6.68/1.23 tff(f79,plain,(
% 6.68/1.23 ! [X0 : $int,X1 : $int] : ($less($product(X0,X0),$product(X1,X1)) | $less(X0,1) | $less(X1,1) | ~$less(X0,X1))),
% 6.68/1.23 inference(flattening,[],[f78])).
% 6.68/1.23 tff(f80,plain,(
% 6.68/1.23 ? [X0 : $int,X1 : $int,X2 : general] : ($less(X0,X1) & (~$less(X0,0) & p__less_equal__(f__integer__($product(X0,X0)),X2) & p__greater__(f__integer__($product($sum(X0,1),$sum(X0,1))),X2) & p__less_equal__(f__integer__($product(X1,X1)),X2) & ~$less(X1,0)))),
% 6.68/1.23 inference(ennf_transformation,[],[f38])).
% 6.68/1.23 tff(f81,plain,(
% 6.68/1.23 ? [X0 : $int,X1 : $int,X2 : general] : ($less(X0,X1) & ~$less(X0,0) & p__less_equal__(f__integer__($product(X0,X0)),X2) & p__greater__(f__integer__($product($sum(X0,1),$sum(X0,1))),X2) & p__less_equal__(f__integer__($product(X1,X1)),X2) & ~$less(X1,0))),
% 6.68/1.23 inference(flattening,[],[f80])).
% 6.68/1.23 tff(f90,plain,(
% 6.68/1.23 ! [X0 : $int,X1 : $int] : ((p__less_equal__(f__integer__(X0),f__integer__(X1)) | $less(X1,X0)) & (~$less(X1,X0) | ~p__less_equal__(f__integer__(X0),f__integer__(X1))))),
% 6.68/1.23 inference(nnf_transformation,[],[f28])).
% 6.68/1.23 tff(f106,plain,(
% 6.68/1.23 $less(sK25,sK26) & ~$less(sK25,0) & p__less_equal__(f__integer__($product(sK25,sK25)),sK27) & p__greater__(f__integer__($product($sum(sK25,1),$sum(sK25,1))),sK27) & p__less_equal__(f__integer__($product(sK26,sK26)),sK27) & ~$less(sK26,0)),
% 6.68/1.23 inference(skolemize,[status(esa),new_symbols(skolem,[sK25,sK26,sK27]),skolemize(X0,sK25),skolemize(X1,sK26),skolemize(X2,sK27)],[f81])).
% 6.68/1.23 tff(f114,plain,(
% 6.68/1.23 ( ! [X0 : $int,X1 : $int] : (~p__less_equal__(f__integer__(X0),f__integer__(X1)) | ~$less(X1,X0)) )),
% 6.68/1.23 inference(cnf_transformation,[],[f90])).
% 6.68/1.23 tff(f115,plain,(
% 6.68/1.23 ( ! [X0 : $int,X1 : $int] : (p__less_equal__(f__integer__(X0),f__integer__(X1)) | $less(X1,X0)) )),
% 6.68/1.23 inference(cnf_transformation,[],[f90])).
% 6.68/1.23 tff(f116,plain,(
% 6.68/1.23 ( ! [X0 : general,X1 : general] : (~p__less_equal__(X1,X0) | ~p__less_equal__(X0,X1) | X0 = X1) )),
% 6.68/1.23 inference(cnf_transformation,[],[f69])).
% 6.68/1.23 tff(f117,plain,(
% 6.68/1.23 ( ! [X2 : general,X0 : general,X1 : general] : (~p__less_equal__(X1,X2) | ~p__less_equal__(X0,X1) | p__less_equal__(X0,X2)) )),
% 6.68/1.23 inference(cnf_transformation,[],[f71])).
% 6.68/1.23 tff(f121,plain,(
% 6.68/1.23 ( ! [X0 : general,X1 : general] : (X0 != X1 | ~p__greater__(X0,X1)) )),
% 6.68/1.23 inference(cnf_transformation,[],[f73])).
% 6.68/1.23 tff(f122,plain,(
% 6.68/1.23 ( ! [X0 : general,X1 : general] : (~p__greater__(X0,X1) | p__less_equal__(X1,X0)) )),
% 6.68/1.23 inference(cnf_transformation,[],[f73])).
% 6.68/1.23 tff(f159,plain,(
% 6.68/1.23 ( ! [X0 : $int,X1 : $int] : ($less($product(X0,X0),$product(X1,X1)) | $less(X0,1) | $less(X1,1) | ~$less(X0,X1)) )),
% 6.68/1.23 inference(cnf_transformation,[],[f79])).
% 6.68/1.23 tff(f161,plain,(
% 6.68/1.23 p__less_equal__(f__integer__($product(sK26,sK26)),sK27)),
% 6.68/1.23 inference(cnf_transformation,[],[f106])).
% 6.68/1.23 tff(f162,plain,(
% 6.68/1.23 p__greater__(f__integer__($product($sum(sK25,1),$sum(sK25,1))),sK27)),
% 6.68/1.23 inference(cnf_transformation,[],[f106])).
% 6.68/1.23 tff(f164,plain,(
% 6.68/1.23 ~$less(sK25,0)),
% 6.68/1.23 inference(cnf_transformation,[],[f106])).
% 6.68/1.23 tff(f165,plain,(
% 6.68/1.23 $less(sK25,sK26)),
% 6.68/1.23 inference(cnf_transformation,[],[f106])).
% 6.68/1.23 tff(f170,plain,(
% 6.68/1.23 ( ! [X1 : general] : (~p__greater__(X1,X1)) )),
% 6.68/1.23 inference(equality_resolution,[],[f121])).
% 6.68/1.23 tff(f176,definition,(
% 6.68/1.23 sF30 = $sum(sK25,1)),
% 6.68/1.23 introduced(definition,[new_symbols(definition,[sF30])],[function_definition])).
% 6.68/1.23 tff(f177,plain,(
% 6.68/1.23 $sum(sK25,1) = sF30),
% 6.68/1.23 inference(reorient_equations,[],[f176])).
% 6.68/1.23 tff(f178,definition,(
% 6.68/1.23 sF31 = $product(sF30,sF30)),
% 6.68/1.23 introduced(definition,[new_symbols(definition,[sF31])],[function_definition])).
% 6.68/1.23 tff(f179,plain,(
% 6.68/1.23 $product(sF30,sF30) = sF31),
% 6.68/1.23 inference(reorient_equations,[],[f178])).
% 6.68/1.23 tff(f180,definition,(
% 6.68/1.23 sF32 = f__integer__(sF31)),
% 6.68/1.23 introduced(definition,[new_symbols(definition,[sF32])],[function_definition])).
% 6.68/1.23 tff(f181,plain,(
% 6.68/1.23 f__integer__(sF31) = sF32),
% 6.68/1.23 inference(reorient_equations,[],[f180])).
% 6.68/1.23 tff(f182,plain,(
% 6.68/1.23 p__greater__(sF32,sK27)),
% 6.68/1.23 inference(definition_folding,[],[f162,f181,f179,f177,f177])).
% 6.68/1.23 tff(f183,definition,(
% 6.68/1.23 sF33 = $product(sK26,sK26)),
% 6.68/1.23 introduced(definition,[new_symbols(definition,[sF33])],[function_definition])).
% 6.68/1.23 tff(f184,plain,(
% 6.68/1.23 $product(sK26,sK26) = sF33),
% 6.68/1.23 inference(reorient_equations,[],[f183])).
% 6.68/1.23 tff(f185,definition,(
% 6.68/1.23 sF34 = f__integer__(sF33)),
% 6.68/1.23 introduced(definition,[new_symbols(definition,[sF34])],[function_definition])).
% 6.68/1.23 tff(f186,plain,(
% 6.68/1.23 f__integer__(sF33) = sF34),
% 6.68/1.23 inference(reorient_equations,[],[f185])).
% 6.68/1.23 tff(f187,plain,(
% 6.68/1.23 p__less_equal__(sF34,sK27)),
% 6.68/1.23 inference(definition_folding,[],[f161,f186,f184])).
% 6.68/1.23 tff(f188,plain,(
% 6.68/1.23 sF30 = $sum(1,sK25)),
% 6.68/1.23 inference(forward_demodulation,[],[f177,f39])).
% 6.68/1.23 tff(f207,plain,(
% 6.68/1.23 p__less_equal__(sK27,sF32)),
% 6.68/1.23 inference(resolution,[],[f122,f182])).
% 6.68/1.23 tff(f259,plain,(
% 6.68/1.23 ( ! [X0 : $int,X1 : $int] : ($less(X1,$sum(1,X0)) | $less(X0,X1)) )),
% 6.68/1.23 inference(superposition,[],[f48,f39])).
% 6.68/1.23 tff(f265,plain,(
% 6.68/1.23 ( ! [X0 : $int,X1 : $int] : (~$less(X1,$sum(1,X0)) | ~$less(X0,X1)) )),
% 6.68/1.23 inference(superposition,[],[f56,f39])).
% 6.68/1.23 tff(f285,plain,(
% 6.68/1.23 ( ! [X0 : $int] : (~p__less_equal__(sF34,f__integer__(X0)) | ~$less(X0,sF33)) )),
% 6.68/1.23 inference(superposition,[],[f114,f186])).
% 6.68/1.23 tff(f297,plain,(
% 6.68/1.23 ( ! [X0 : $int] : (p__less_equal__(f__integer__(X0),sF34) | $less(sF33,X0)) )),
% 6.68/1.23 inference(superposition,[],[f115,f186])).
% 6.68/1.23 tff(f352,plain,(
% 6.68/1.23 ~p__less_equal__(sF32,sK27) | sK27 = sF32),
% 6.68/1.23 inference(resolution,[],[f116,f207])).
% 6.68/1.23 tff(f371,plain,(
% 6.68/1.23 ( ! [X0 : general] : (~p__less_equal__(X0,sF34) | p__less_equal__(X0,sK27)) )),
% 6.68/1.23 inference(resolution,[],[f117,f187])).
% 6.68/1.23 tff(f373,plain,(
% 6.68/1.23 ( ! [X0 : general] : (~p__less_equal__(X0,sK27) | p__less_equal__(X0,sF32)) )),
% 6.68/1.23 inference(resolution,[],[f117,f207])).
% 6.68/1.23 tff(f435,plain,(
% 6.68/1.23 p__less_equal__(sF34,sF32)),
% 6.68/1.23 inference(resolution,[],[f373,f187])).
% 6.68/1.23 tff(f615,plain,(
% 6.68/1.23 ( ! [X0 : $int] : ($less($product(X0,X0),sF33) | $less(X0,1) | $less(sK26,1) | ~$less(X0,sK26)) )),
% 6.68/1.23 inference(superposition,[],[f159,f184])).
% 6.68/1.23 tff(f620,plain,(
% 6.68/1.23 ( ! [X0 : $int] : ($less($product(X0,X0),sF33) | $less(X0,1) | ~$less(X0,sK26)) )),
% 6.68/1.23 inference(forward_subsumption_resolution,[],[f615,f45])).
% 6.68/1.23 tff(f709,plain,(
% 6.68/1.23 ~p__less_equal__(sF34,sF32) | ~$less(sF31,sF33)),
% 6.68/1.23 inference(superposition,[],[f285,f181])).
% 6.68/1.23 tff(f711,plain,(
% 6.68/1.23 ~$less(sF31,sF33)),
% 6.68/1.23 inference(forward_subsumption_resolution,[],[f709,f435])).
% 6.68/1.23 tff(f805,plain,(
% 6.68/1.23 ( ! [X0 : $int] : (p__less_equal__(f__integer__(X0),sK27) | $less(sF33,X0)) )),
% 6.68/1.23 inference(resolution,[],[f297,f371])).
% 6.68/1.23 tff(f827,plain,(
% 6.68/1.23 p__less_equal__(sF32,sK27) | $less(sF33,sF31)),
% 6.68/1.23 inference(superposition,[],[f805,f181])).
% 6.68/1.23 tff(f832,plain,(
% 6.68/1.23 $less(sF33,sF31) | sK27 = sF32),
% 6.68/1.23 inference(resolution,[],[f827,f352])).
% 6.68/1.23 tff(f884,plain,(
% 6.68/1.23 ( ! [X0 : $int] : ($less(X0,sF30) | $less(sK25,X0)) )),
% 6.68/1.23 inference(superposition,[],[f259,f188])).
% 6.68/1.23 tff(f906,plain,(
% 6.68/1.23 ( ! [X0 : $int] : (~$less(sK25,X0) | ~$less(X0,sF30)) )),
% 6.68/1.23 inference(superposition,[],[f265,f188])).
% 6.68/1.23 tff(f907,plain,(
% 6.68/1.23 ( ! [X0 : $int] : (~$less(0,X0) | ~$less(X0,1)) )),
% 6.68/1.23 inference(superposition,[],[f265,f41])).
% 6.68/1.23 tff(f2766,plain,(
% 6.68/1.23 $less(sF31,sF33) | $less(sF30,1) | ~$less(sF30,sK26)),
% 6.68/1.23 inference(superposition,[],[f620,f179])).
% 6.68/1.23 tff(f2768,plain,(
% 6.68/1.23 ~$less(sF30,sK26) | $less(sF30,1)),
% 6.68/1.23 inference(forward_subsumption_resolution,[],[f2766,f711])).
% 6.68/1.23 tff(f2773,plain,(
% 6.68/1.23 $less(sF30,1) | $less(sK26,sF30) | sK26 = sF30),
% 6.68/1.23 inference(resolution,[],[f2768,f46])).
% 6.68/1.23 tff(f6796,plain,(
% 6.68/1.23 $less(0,sF30)),
% 6.68/1.23 inference(resolution,[],[f884,f164])).
% 6.68/1.23 tff(f6876,plain,(
% 6.68/1.23 ~$less(sK26,sF30)),
% 6.68/1.23 inference(resolution,[],[f906,f165])).
% 6.68/1.23 tff(f6911,plain,(
% 6.68/1.23 ~$less(sF30,1)),
% 6.68/1.23 inference(resolution,[],[f907,f6796])).
% 6.68/1.23 tff(f6930,plain,(
% 6.68/1.23 $less(sK26,sF30) | sK26 = sF30),
% 6.68/1.23 inference(resolution,[],[f6911,f2773])).
% 6.68/1.23 tff(f6934,plain,(
% 6.68/1.23 sK26 = sF30),
% 6.68/1.23 inference(forward_subsumption_resolution,[],[f6930,f6876])).
% 6.68/1.23 tff(f7149,plain,(
% 6.68/1.23 $product(sK26,sK26) = sF31),
% 6.68/1.23 inference(superposition,[],[f179,f6934])).
% 6.68/1.23 tff(f7183,plain,(
% 6.68/1.23 sF31 = sF33),
% 6.68/1.23 inference(superposition,[],[f184,f7149])).
% 6.68/1.23 tff(f7275,plain,(
% 6.68/1.23 $less(sF31,sF31) | sK27 = sF32),
% 6.68/1.23 inference(superposition,[],[f832,f7183])).
% 6.68/1.23 tff(f7296,plain,(
% 6.68/1.23 sK27 = sF32),
% 6.68/1.23 inference(forward_subsumption_resolution,[],[f7275,f44])).
% 6.68/1.23 tff(f7409,plain,(
% 6.68/1.23 p__greater__(sK27,sK27)),
% 6.68/1.23 inference(superposition,[],[f182,f7296])).
% 6.68/1.23 tff(f7464,plain,(
% 6.68/1.23 $false),
% 6.68/1.23 inference(forward_subsumption_resolution,[],[f7409,f170])).
% 6.68/1.23 % SZS output end Proof for theBenchmark
% 6.68/1.23 % (1832919)------------------------------
% 6.68/1.23 % (1832919)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.68/1.23 % (1832919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.68/1.23 % (1832919)CaDiCaL version: 2.1.3
% 6.68/1.23 % (1832919)Termination reason: Refutation
% 6.68/1.23 % (1832919)Time elapsed: 0.218 s
% 6.68/1.23 % (1832919)Peak memory usage: 15 MB
% 6.68/1.23 % (1832919)Instructions burned: 359 (million)
% 6.68/1.23 % (1832773)Success in time 0.987 s
% 6.68/1.23 % Vampire exiting
%------------------------------------------------------------------------------