%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ARI615_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 : n002.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:58 AM UTC 2026
% Result : Theorem 117.33s 19.59s
% Output : Refutation 117.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ARI615_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.08/0.19 % Computer : n002.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 20:56:22 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.22 Running first-order model finding
% 0.08/0.22 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.37/0.90 % (749859)Will run a generic schedule for satisfiability detection.
% 4.37/0.90 % (749866)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1653185638:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.37/0.90 % (749865)% WARNING: option uhcvi not known.
% 4.37/0.90 % (749864)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=527496903_2999 on theBenchmark for (2999ds/0Mi)
% 4.37/0.90 % (749865)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3450881268:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.37/0.90 % (749867)dis+10_1_sil=32000:sp=arity:random_seed=1333541732:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.37/0.90 % (749868)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1324023300:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.37/0.90 % (749864)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 4.37/0.90 % (749864)Terminated due to inappropriate strategy.
% 4.37/0.90 % (749864)------------------------------
% 4.37/0.90 % (749864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.37/0.90 % (749864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.37/0.90 % (749864)CaDiCaL version: 2.1.3
% 4.37/0.90 % (749864)Termination reason: Inappropriate
% 4.37/0.90 % (749864)Time elapsed: 0.0000 s
% 4.37/0.90 % (749864)Peak memory usage: 10 MB
% 4.37/0.90 % (749869)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1858620680:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.37/0.90 % (749870)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=18116355:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.37/0.90 % (749864)------------------------------
% 4.37/0.90 % (749864)------------------------------
% 4.37/0.90 % (749878)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3965980451:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 4.37/0.90 % (749878)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 4.37/0.90 % (749878)Terminated due to inappropriate strategy.
% 4.37/0.90 % (749878)------------------------------
% 4.37/0.90 % (749878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.37/0.90 % (749878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.37/0.90 % (749878)CaDiCaL version: 2.1.3
% 4.37/0.90 % (749878)Termination reason: Inappropriate
% 4.37/0.90 % (749878)Time elapsed: 0.0000 s
% 4.37/0.90 % (749878)Peak memory usage: 10 MB
% 4.37/0.90 % (749878)------------------------------
% 4.37/0.90 % (749878)------------------------------
% 4.37/0.90 % (749880)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1962917850:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 4.37/0.90 % (749867)Instruction limit reached!
% 4.37/0.90 % (749867)------------------------------
% 4.37/0.90 % (749867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.37/0.90 % (749867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.37/0.90 % (749867)CaDiCaL version: 2.1.3
% 4.37/0.90 % (749867)Termination reason: Instruction limit
% 4.37/0.90 % (749867)Termination phase: Saturation
% 4.37/0.90 % (749867)Time elapsed: 0.068 s
% 4.37/0.90 % (749867)Peak memory usage: 12 MB
% 4.37/0.90 % (749867)Instructions burned: 103 (million)
% 4.37/0.90 % (749868)Instruction limit reached!
% 4.37/0.90 % (749868)------------------------------
% 4.37/0.90 % (749868)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.37/0.90 % (749868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.37/0.90 % (749868)CaDiCaL version: 2.1.3
% 4.37/0.90 % (749868)Termination reason: Instruction limit
% 4.37/0.90 % (749868)Termination phase: Saturation
% 4.37/0.90 % (749868)Time elapsed: 0.071 s
% 4.37/0.90 % (749868)Peak memory usage: 12 MB
% 4.37/0.90 % (749868)Instructions burned: 116 (million)
% 4.37/0.90 % (749869)Instruction limit reached!
% 4.37/0.90 % (749869)------------------------------
% 4.37/0.90 % (749869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.37/0.90 % (749869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.37/0.90 % (749869)CaDiCaL version: 2.1.3
% 4.37/0.90 % (749869)Termination reason: Instruction limit
% 4.37/0.90 % (749869)Termination phase: Saturation
% 4.37/0.90 % (749869)Time elapsed: 0.087 s
% 4.37/0.90 % (749882)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=2501691553:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 8.08/1.45 % (749869)Peak memory usage: 12 MB
% 8.08/1.45 % (749869)Instructions burned: 132 (million)
% 8.08/1.45 % (749883)ott-21_1_sil=16000:fs=off:random_seed=2978106460:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 8.08/1.45 % (749885)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2009153344:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 8.08/1.45 % (749870)Instruction limit reached!
% 8.08/1.45 % (749870)------------------------------
% 8.08/1.45 % (749870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.08/1.45 % (749870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.08/1.45 % (749870)CaDiCaL version: 2.1.3
% 8.08/1.45 % (749870)Termination reason: Instruction limit
% 8.08/1.45 % (749870)Termination phase: Saturation
% 8.08/1.45 % (749870)Time elapsed: 0.112 s
% 8.08/1.45 % (749870)Peak memory usage: 14 MB
% 8.08/1.45 % (749870)Instructions burned: 159 (million)
% 8.08/1.45 % (749880)Instruction limit reached!
% 8.08/1.45 % (749880)------------------------------
% 8.08/1.45 % (749880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.08/1.45 % (749880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.08/1.45 % (749880)CaDiCaL version: 2.1.3
% 8.08/1.45 % (749880)Termination reason: Instruction limit
% 8.08/1.45 % (749880)Termination phase: Saturation
% 8.08/1.45 % (749880)Time elapsed: 0.089 s
% 8.08/1.45 % (749880)Peak memory usage: 13 MB
% 8.08/1.45 % (749880)Instructions burned: 131 (million)
% 8.08/1.45 % (749888)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2598563337:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 8.08/1.45 % (749888)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 8.08/1.45 % (749888)Terminated due to inappropriate strategy.
% 8.08/1.45 % (749888)------------------------------
% 8.08/1.45 % (749888)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.08/1.45 % (749888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.08/1.45 % (749888)CaDiCaL version: 2.1.3
% 8.08/1.45 % (749888)Termination reason: Inappropriate
% 8.08/1.45 % (749888)Time elapsed: 0.0000 s
% 8.08/1.45 % (749888)Peak memory usage: 10 MB
% 8.08/1.45 % (749888)------------------------------
% 8.08/1.45 % (749888)------------------------------
% 8.08/1.45 % (749889)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1475745803:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 8.08/1.45 % (749891)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=786898377:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 8.08/1.45 % (749891)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 8.08/1.45 % (749891)Terminated due to inappropriate strategy.
% 8.08/1.45 % (749891)------------------------------
% 8.08/1.45 % (749891)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.08/1.45 % (749891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.08/1.45 % (749891)CaDiCaL version: 2.1.3
% 8.08/1.45 % (749891)Termination reason: Inappropriate
% 8.08/1.45 % (749891)Time elapsed: 0.0000 s
% 8.08/1.45 % (749891)Peak memory usage: 10 MB
% 8.08/1.45 % (749891)------------------------------
% 8.08/1.45 % (749891)------------------------------
% 8.08/1.45 % (749883)Instruction limit reached!
% 8.08/1.45 % (749883)------------------------------
% 8.08/1.45 % (749883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.08/1.45 % (749883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.08/1.45 % (749883)CaDiCaL version: 2.1.3
% 8.08/1.45 % (749883)Termination reason: Instruction limit
% 8.08/1.45 % (749883)Termination phase: Saturation
% 8.08/1.45 % (749883)Time elapsed: 0.078 s
% 8.08/1.45 % (749883)Peak memory usage: 12 MB
% 8.08/1.45 % (749883)Instructions burned: 181 (million)
% 8.08/1.45 % (749894)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=3391286096:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi)
% 8.08/1.45 % (749895)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1867213584:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 23.43/3.61 % (749882)Instruction limit reached!
% 23.43/3.61 % (749882)------------------------------
% 23.43/3.61 % (749882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.43/3.61 % (749882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.43/3.61 % (749882)CaDiCaL version: 2.1.3
% 23.43/3.61 % (749882)Termination reason: Instruction limit
% 23.43/3.61 % (749882)Termination phase: Saturation
% 23.43/3.61 % (749882)Time elapsed: 0.305 s
% 23.43/3.61 % (749882)Peak memory usage: 15 MB
% 23.43/3.61 % (749882)Instructions burned: 686 (million)
% 23.43/3.61 % (749898)fmb+10_1_sil=64000:random_seed=8690662:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi)
% 23.43/3.61 % (749898)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 23.43/3.61 % (749898)Terminated due to inappropriate strategy.
% 23.43/3.61 % (749898)------------------------------
% 23.43/3.61 % (749898)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.43/3.61 % (749898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.43/3.61 % (749898)CaDiCaL version: 2.1.3
% 23.43/3.61 % (749898)Termination reason: Inappropriate
% 23.43/3.61 % (749898)Time elapsed: 0.0000 s
% 23.43/3.61 % (749898)Peak memory usage: 10 MB
% 23.43/3.61 % (749898)------------------------------
% 23.43/3.61 % (749898)------------------------------
% 23.43/3.61 % (749900)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1264705865:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi)
% 23.43/3.61 % (749900)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 23.43/3.61 % (749900)Terminated due to inappropriate strategy.
% 23.43/3.61 % (749900)------------------------------
% 23.43/3.61 % (749900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.43/3.61 % (749900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.43/3.61 % (749900)CaDiCaL version: 2.1.3
% 23.43/3.61 % (749900)Termination reason: Inappropriate
% 23.43/3.61 % (749900)Time elapsed: 0.0000 s
% 23.43/3.61 % (749900)Peak memory usage: 10 MB
% 23.43/3.61 % (749900)------------------------------
% 23.43/3.61 % (749900)------------------------------
% 23.43/3.61 % (749885)Instruction limit reached!
% 23.43/3.61 % (749885)------------------------------
% 23.43/3.61 % (749885)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.43/3.61 % (749885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.43/3.61 % (749885)CaDiCaL version: 2.1.3
% 23.43/3.61 % (749885)Termination reason: Instruction limit
% 23.43/3.61 % (749885)Termination phase: Saturation
% 23.43/3.61 % (749885)Time elapsed: 0.334 s
% 23.43/3.61 % (749885)Peak memory usage: 14 MB
% 23.43/3.61 % (749885)Instructions burned: 477 (million)
% 23.43/3.61 % (749902)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3391182244:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi)
% 23.43/3.61 % (749902)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 23.43/3.61 % (749902)Terminated due to inappropriate strategy.
% 23.43/3.61 % (749902)------------------------------
% 23.43/3.61 % (749902)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.43/3.61 % (749902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.43/3.61 % (749902)CaDiCaL version: 2.1.3
% 23.43/3.61 % (749902)Termination reason: Inappropriate
% 23.43/3.61 % (749902)Time elapsed: 0.0000 s
% 23.43/3.61 % (749902)Peak memory usage: 10 MB
% 23.43/3.61 % (749902)------------------------------
% 23.43/3.61 % (749902)------------------------------
% 23.43/3.61 % (749903)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2209587820:i=5131_2995 on theBenchmark for (2995ds/5131Mi)
% 23.43/3.61 % (749905)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=371029197:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 23.43/3.61 % (749894)Instruction limit reached!
% 23.43/3.61 % (749894)------------------------------
% 23.43/3.61 % (749894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.43/3.61 % (749894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.43/3.61 % (749894)CaDiCaL version: 2.1.3
% 23.43/3.61 % (749894)Termination reason: Instruction limit
% 23.43/3.61 % (749894)Termination phase: Saturation
% 23.43/3.61 % (749894)Time elapsed: 0.442 s
% 23.43/3.61 % (749894)Peak memory usage: 19 MB
% 23.43/3.61 % (749894)Instructions burned: 693 (million)
% 23.43/3.61 % (749908)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1501850306:i=6324_2993 on theBenchmark for (2993ds/6324Mi)
% 42.34/6.28 % (749908)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 42.34/6.28 % (749908)Terminated due to inappropriate strategy.
% 42.34/6.28 % (749908)------------------------------
% 42.34/6.28 % (749908)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.34/6.28 % (749908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.34/6.28 % (749908)CaDiCaL version: 2.1.3
% 42.34/6.28 % (749908)Termination reason: Inappropriate
% 42.34/6.28 % (749908)Time elapsed: 0.0000 s
% 42.34/6.28 % (749908)Peak memory usage: 10 MB
% 42.34/6.28 % (749908)------------------------------
% 42.34/6.28 % (749908)------------------------------
% 42.34/6.28 % (749910)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4198977352:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi)
% 42.34/6.28 % (749910)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 42.34/6.28 % (749910)Terminated due to inappropriate strategy.
% 42.34/6.28 % (749910)------------------------------
% 42.34/6.28 % (749910)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.34/6.28 % (749910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.34/6.28 % (749910)CaDiCaL version: 2.1.3
% 42.34/6.28 % (749910)Termination reason: Inappropriate
% 42.34/6.28 % (749910)Time elapsed: 0.0000 s
% 42.34/6.28 % (749910)Peak memory usage: 10 MB
% 42.34/6.28 % (749910)------------------------------
% 42.34/6.28 % (749910)------------------------------
% 42.34/6.28 % (749912)ott-2_1_sil=16000:newcnf=on:random_seed=2030802844:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi)
% 42.34/6.28 % (749895)Instruction limit reached!
% 42.34/6.28 % (749895)------------------------------
% 42.34/6.28 % (749895)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.34/6.28 % (749895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.34/6.28 % (749895)CaDiCaL version: 2.1.3
% 42.34/6.28 % (749895)Termination reason: Instruction limit
% 42.34/6.28 % (749895)Termination phase: Saturation
% 42.34/6.28 % (749895)Time elapsed: 0.513 s
% 42.34/6.28 % (749895)Peak memory usage: 21 MB
% 42.34/6.28 % (749895)Instructions burned: 879 (million)
% 42.34/6.28 % (749914)ott+10_1_sil=32000:tgt=ground:random_seed=3935620920:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi)
% 42.34/6.28 % (749889)Instruction limit reached!
% 42.34/6.28 % (749889)------------------------------
% 42.34/6.28 % (749889)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.34/6.28 % (749889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.34/6.28 % (749889)CaDiCaL version: 2.1.3
% 42.34/6.28 % (749889)Termination reason: Instruction limit
% 42.34/6.28 % (749889)Termination phase: Saturation
% 42.34/6.28 % (749889)Time elapsed: 0.747 s
% 42.34/6.28 % (749889)Peak memory usage: 19 MB
% 42.34/6.28 % (749889)Instructions burned: 1180 (million)
% 42.34/6.28 % (749916)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=4074453110:i=54282_2990 on theBenchmark for (2990ds/54282Mi)
% 42.34/6.28 % (749916)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 42.34/6.28 % (749916)Terminated due to inappropriate strategy.
% 42.34/6.28 % (749916)------------------------------
% 42.34/6.28 % (749916)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.34/6.28 % (749916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.34/6.28 % (749916)CaDiCaL version: 2.1.3
% 42.34/6.28 % (749916)Termination reason: Inappropriate
% 42.34/6.28 % (749916)Time elapsed: 0.0000 s
% 42.34/6.28 % (749916)Peak memory usage: 10 MB
% 42.34/6.28 % (749916)------------------------------
% 42.34/6.28 % (749916)------------------------------
% 42.34/6.28 % (749918)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2667519110:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi)
% 42.34/6.28 % (749905)Instruction limit reached!
% 42.34/6.28 % (749905)------------------------------
% 42.34/6.28 % (749905)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.34/6.28 % (749905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.34/6.28 % (749905)CaDiCaL version: 2.1.3
% 42.34/6.28 % (749905)Termination reason: Instruction limit
% 42.34/6.28 % (749905)Termination phase: Saturation
% 42.34/6.28 % (749905)Time elapsed: 0.713 s
% 42.34/6.28 % (749905)Peak memory usage: 25 MB
% 117.33/19.59 % (749905)Instructions burned: 1473 (million)
% 117.33/19.59 % (749920)dis+21_1_sil=32000:sas=cadical:random_seed=1329894598:i=3773:amm=off_2987 on theBenchmark for (2987ds/3773Mi)
% 117.33/19.59 % (749912)Instruction limit reached!
% 117.33/19.59 % (749912)------------------------------
% 117.33/19.59 % (749912)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.33/19.59 % (749912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.33/19.59 % (749912)CaDiCaL version: 2.1.3
% 117.33/19.59 % (749912)Termination reason: Instruction limit
% 117.33/19.59 % (749912)Termination phase: Saturation
% 117.33/19.59 % (749912)Time elapsed: 0.565 s
% 117.33/19.59 % (749912)Peak memory usage: 17 MB
% 117.33/19.59 % (749912)Instructions burned: 870 (million)
% 117.33/19.59 % (749922)ott+11_1_sil=16000:gs=on:random_seed=1378821396:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi)
% 117.33/19.59 % (749922)Instruction limit reached!
% 117.33/19.59 % (749922)------------------------------
% 117.33/19.59 % (749922)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.33/19.59 % (749922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.33/19.59 % (749922)CaDiCaL version: 2.1.3
% 117.33/19.59 % (749922)Termination reason: Instruction limit
% 117.33/19.59 % (749922)Termination phase: Saturation
% 117.33/19.59 % (749922)Time elapsed: 1.249 s
% 117.33/19.59 % (749922)Peak memory usage: 22 MB
% 117.33/19.59 % (749922)Instructions burned: 2251 (million)
% 117.33/19.59 % (749924)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=4202417983:fmbsr=1.6:i=67534_2974 on theBenchmark for (2974ds/67534Mi)
% 117.33/19.59 % (749924)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 117.33/19.59 % (749924)Terminated due to inappropriate strategy.
% 117.33/19.59 % (749924)------------------------------
% 117.33/19.59 % (749924)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.33/19.59 % (749924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.33/19.59 % (749924)CaDiCaL version: 2.1.3
% 117.33/19.59 % (749924)Termination reason: Inappropriate
% 117.33/19.59 % (749924)Time elapsed: 0.0000 s
% 117.33/19.59 % (749924)Peak memory usage: 10 MB
% 117.33/19.59 % (749924)------------------------------
% 117.33/19.59 % (749924)------------------------------
% 117.33/19.59 % (749926)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1735145993:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2974 on theBenchmark for (2974ds/4591Mi)
% 117.33/19.59 % (749918)Instruction limit reached!
% 117.33/19.59 % (749918)------------------------------
% 117.33/19.59 % (749918)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.33/19.59 % (749918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.33/19.59 % (749918)CaDiCaL version: 2.1.3
% 117.33/19.59 % (749918)Termination reason: Instruction limit
% 117.33/19.59 % (749918)Termination phase: Saturation
% 117.33/19.59 % (749918)Time elapsed: 1.974 s
% 117.33/19.59 % (749918)Peak memory usage: 30 MB
% 117.33/19.59 % (749918)Instructions burned: 3513 (million)
% 117.33/19.59 % (749928)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3124608178:i=29340_2970 on theBenchmark for (2970ds/29340Mi)
% 117.33/19.59 % (749920)Instruction limit reached!
% 117.33/19.59 % (749920)------------------------------
% 117.33/19.59 % (749920)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.33/19.59 % (749920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.33/19.59 % (749920)CaDiCaL version: 2.1.3
% 117.33/19.59 % (749920)Termination reason: Instruction limit
% 117.33/19.59 % (749920)Termination phase: Saturation
% 117.33/19.59 % (749920)Time elapsed: 2.072 s
% 117.33/19.59 % (749920)Peak memory usage: 29 MB
% 117.33/19.59 % (749920)Instructions burned: 3774 (million)
% 117.33/19.59 % (749930)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2980962802:i=5211_2966 on theBenchmark for (2966ds/5211Mi)
% 117.33/19.59 % (749903)Instruction limit reached!
% 117.33/19.59 % (749903)------------------------------
% 117.33/19.59 % (749903)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.33/19.59 % (749903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.33/19.59 % (749903)CaDiCaL version: 2.1.3
% 117.33/19.59 % (749903)Termination reason: Instruction limit
% 117.33/19.59 % (749903)Termination phase: Saturation
% 117.33/19.59 % (749903)Time elapsed: 2.880 s
% 117.33/19.59 % (749903)Peak memory usage: 39 MB
% 117.33/19.59 % (749903)Instructions burned: 5133 (million)
% 117.33/19.59 % (749932)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=456353327:i=5497:nm=2_2966 on theBenchmark for (2966ds/5497Mi)
% 117.33/19.59 % (749932)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 117.33/19.59 % (749932)Terminated due to inappropriate strategy.
% 117.33/19.59 % (749932)------------------------------
% 117.33/19.59 % (749932)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.33/19.59 % (749932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.33/19.59 % (749932)CaDiCaL version: 2.1.3
% 117.33/19.59 % (749932)Termination reason: Inappropriate
% 117.33/19.59 % (749932)Time elapsed: 0.0000 s
% 117.33/19.59 % (749932)Peak memory usage: 10 MB
% 117.33/19.59 % (749932)------------------------------
% 117.33/19.59 % (749932)------------------------------
% 117.33/19.59 % (749934)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=570704133:fmbsr=2:i=46332_2965 on theBenchmark for (2965ds/46332Mi)
% 117.33/19.59 % (749934)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 117.33/19.59 % (749934)Terminated due to inappropriate strategy.
% 117.33/19.59 % (749934)------------------------------
% 117.33/19.59 % (749934)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.33/19.59 % (749934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.33/19.59 % (749934)CaDiCaL version: 2.1.3
% 117.33/19.59 % (749934)Termination reason: Inappropriate
% 117.33/19.59 % (749934)Time elapsed: 0.0000 s
% 117.33/19.59 % (749934)Peak memory usage: 10 MB
% 117.33/19.59 % (749934)------------------------------
% 117.33/19.59 % (749934)------------------------------
% 117.33/19.59 % (749936)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=4016665293:i=14071_2965 on theBenchmark for (2965ds/14071Mi)
% 117.33/19.59 % (749936)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 117.33/19.59 % (749936)Terminated due to inappropriate strategy.
% 117.33/19.59 % (749936)------------------------------
% 117.33/19.59 % (749936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.33/19.59 % (749936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.33/19.59 % (749936)CaDiCaL version: 2.1.3
% 117.33/19.59 % (749936)Termination reason: Inappropriate
% 117.33/19.59 % (749936)Time elapsed: 0.0000 s
% 117.33/19.59 % (749936)Peak memory usage: 10 MB
% 117.33/19.59 % (749936)------------------------------
% 117.33/19.59 % (749936)------------------------------
% 117.33/19.59 % (749938)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1067661109:i=22565:add=on:rawr=on_2965 on theBenchmark for (2965ds/22565Mi)
% 117.33/19.59 % (749914)Instruction limit reached!
% 117.33/19.59 % (749914)------------------------------
% 117.33/19.59 % (749914)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.33/19.59 % (749914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.33/19.59 % (749914)CaDiCaL version: 2.1.3
% 117.33/19.59 % (749914)Termination reason: Instruction limit
% 117.33/19.59 % (749914)Termination phase: Saturation
% 117.33/19.59 % (749914)Time elapsed: 3.272 s
% 117.33/19.59 % (749914)Peak memory usage: 36 MB
% 117.33/19.59 % (749914)Instructions burned: 5114 (million)
% 117.33/19.59 % (749940)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=786816456:i=8173:av=off_2959 on theBenchmark for (2959ds/8173Mi)
% 117.33/19.59 % (749926)Instruction limit reached!
% 117.33/19.59 % (749926)------------------------------
% 117.33/19.59 % (749926)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.33/19.59 % (749926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.33/19.59 % (749926)CaDiCaL version: 2.1.3
% 117.33/19.59 % (749926)Termination reason: Instruction limit
% 117.33/19.59 % (749926)Termination phase: Saturation
% 117.33/19.59 % (749926)Time elapsed: 2.336 s
% 117.33/19.59 % (749926)Peak memory usage: 52 MB
% 117.33/19.59 % (749926)Instructions burned: 4591 (million)
% 117.33/19.59 % (749942)dis+10_16:1_sil=16000:random_seed=4206270540:i=9155:fsr=off_2950 on theBenchmark for (2950ds/9155Mi)
% 117.33/19.59 % (749930)Instruction limit reached!
% 117.33/19.59 % (749930)------------------------------
% 117.33/19.59 % (749930)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.33/19.59 % (749930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.33/19.59 % (749930)CaDiCaL version: 2.1.3
% 117.33/19.59 % (749930)Termination reason: Instruction limit
% 117.33/19.59 % (749930)Termination phase: Saturation
% 117.33/19.59 % (749930)Time elapsed: 2.712 s
% 117.33/19.59 % (749930)Peak memory usage: 53 MB
% 117.33/19.59 % (749930)Instructions burned: 5212 (million)
% 117.33/19.59 % (749944)ott-3_8_sil=64000:random_seed=201927713:i=20139:bs=on_2939 on theBenchmark for (2939ds/20139Mi)
% 117.33/19.59 % (749940)Instruction limit reached!
% 117.33/19.59 % (749940)------------------------------
% 117.33/19.59 % (749940)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.33/19.59 % (749940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.33/19.59 % (749940)CaDiCaL version: 2.1.3
% 117.33/19.59 % (749940)Termination reason: Instruction limit
% 117.33/19.59 % (749940)Termination phase: Saturation
% 117.33/19.59 % (749940)Time elapsed: 5.199 s
% 117.33/19.59 % (749940)Peak memory usage: 51 MB
% 117.33/19.59 % (749940)Instructions burned: 8173 (million)
% 117.33/19.59 % (749946)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2412091901:fmbsr=2:i=32576_2907 on theBenchmark for (2907ds/32576Mi)
% 117.33/19.59 % (749946)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 117.33/19.59 % (749946)Terminated due to inappropriate strategy.
% 117.33/19.59 % (749946)------------------------------
% 117.33/19.59 % (749946)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.33/19.59 % (749946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.33/19.59 % (749946)CaDiCaL version: 2.1.3
% 117.33/19.59 % (749946)Termination reason: Inappropriate
% 117.33/19.59 % (749946)Time elapsed: 0.0000 s
% 117.33/19.59 % (749946)Peak memory usage: 10 MB
% 117.33/19.59 % (749946)------------------------------
% 117.33/19.59 % (749946)------------------------------
% 117.33/19.59 % (749948)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2782371026:i=11404_2907 on theBenchmark for (2907ds/11404Mi)
% 117.33/19.59 % (749942)Instruction limit reached!
% 117.33/19.59 % (749942)------------------------------
% 117.33/19.59 % (749942)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.33/19.59 % (749942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.33/19.59 % (749942)CaDiCaL version: 2.1.3
% 117.33/19.59 % (749942)Termination reason: Instruction limit
% 117.33/19.59 % (749942)Termination phase: Saturation
% 117.33/19.59 % (749942)Time elapsed: 4.869 s
% 117.33/19.59 % (749942)Peak memory usage: 53 MB
% 117.33/19.59 % (749942)Instructions burned: 9156 (million)
% 117.33/19.59 % (749950)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1152710869:i=14134_2901 on theBenchmark for (2901ds/14134Mi)
% 117.33/19.59 % (749938)Instruction limit reached!
% 117.33/19.59 % (749938)------------------------------
% 117.33/19.59 % (749938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.33/19.59 % (749938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.33/19.59 % (749938)CaDiCaL version: 2.1.3
% 117.33/19.59 % (749938)Termination reason: Instruction limit
% 117.33/19.59 % (749938)Termination phase: Saturation
% 117.33/19.59 % (749938)Time elapsed: 10.218 s
% 117.33/19.59 % (749938)Peak memory usage: 18 MB
% 117.33/19.59 % (749938)Instructions burned: 22566 (million)
% 117.33/19.59 % (749953)dis+33_16_sil=32000:sac=on:random_seed=1175424093:i=15851:nm=0_2863 on theBenchmark for (2863ds/15851Mi)
% 117.33/19.59 % (749948)Instruction limit reached!
% 117.33/19.59 % (749948)------------------------------
% 117.33/19.59 % (749948)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.33/19.59 % (749948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.33/19.59 % (749948)CaDiCaL version: 2.1.3
% 117.33/19.59 % (749948)Termination reason: Instruction limit
% 117.33/19.59 % (749948)Termination phase: Saturation
% 117.33/19.59 % (749948)Time elapsed: 8.506 s
% 117.33/19.59 % (749948)Peak memory usage: 50 MB
% 117.33/19.59 % (749948)Instructions burned: 11404 (million)
% 117.33/19.59 % (750280)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=270789361:avsq=on:i=17627:add=on:amm=off_2821 on theBenchmark for (2821ds/17627Mi)
% 117.33/19.59 % (749865) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-749859-749865"...
% 117.33/19.59 % (749865)...printing done.
% 117.33/19.59 % (749865)Refutation found. Thanks to Tanya!
% 117.33/19.59 % SZS status Theorem for theBenchmark
% 117.33/19.59 % SZS output start Proof for theBenchmark
% 117.33/19.59 tff(func_def_4, type, sK0: $int).
% 117.33/19.59 tff(func_def_5, type, sK1: $int).
% 117.33/19.59 tff(func_def_6, type, sK2: $int).
% 117.33/19.59 tff(func_def_7, type, sK3: $int).
% 117.33/19.59 tff(pred_def_1, type, p: ($int * $int * $int) > $o).
% 117.33/19.59 tff(f1,conjecture,(
% 117.33/19.59 ! [X0 : $int,X1 : $int,X2 : $int] : (($lesseq($sum(X1,$uminus(X2)),X0) & $lesseq(X0,$sum(X1,X2))) <=> p(X0,X1,X2)) => ! [X0 : $int,X1 : $int,X2 : $int,X3 : $int] : ($lesseq(X2,X3) => (p(X0,X1,X2) => p(X0,X1,X3)))),
% 117.33/19.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p',interv_with_smaller_radius_contained)).
% 117.33/19.59 tff(f2,negated_conjecture,(
% 117.33/19.59 ~(! [X0 : $int,X1 : $int,X2 : $int] : (($lesseq($sum(X1,$uminus(X2)),X0) & $lesseq(X0,$sum(X1,X2))) <=> p(X0,X1,X2)) => ! [X0 : $int,X1 : $int,X2 : $int,X3 : $int] : ($lesseq(X2,X3) => (p(X0,X1,X2) => p(X0,X1,X3))))),
% 117.33/19.59 inference(negated_conjecture,[status(cth)],[f1])).
% 117.33/19.59 tff(f3,plain,(
% 117.33/19.59 ~(! [X0 : $int,X1 : $int,X2 : $int] : ((~$less(X0,$sum(X1,$uminus(X2))) & ~$less($sum(X1,X2),X0)) <=> p(X0,X1,X2)) => ! [X0 : $int,X1 : $int,X2 : $int,X3 : $int] : (~$less(X3,X2) => (p(X0,X1,X2) => p(X0,X1,X3))))),
% 117.33/19.59 inference(theory_normalization,[],[f2])).
% 117.33/19.59 tff(f4,definition,(
% 117.33/19.59 ( ! [X0 : $int,X1 : $int] : ($sum(X0,X1) = $sum(X1,X0)) )),
% 117.33/19.59 introduced(theory,[tha_commutativity])).
% 117.33/19.59 tff(f5,definition,(
% 117.33/19.59 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum(X0,$sum(X1,X2)) = $sum($sum(X0,X1),X2)) )),
% 117.33/19.59 introduced(theory,[tha_associativity])).
% 117.33/19.59 tff(f7,definition,(
% 117.33/19.59 ( ! [X0 : $int,X1 : $int] : ($uminus($sum(X0,X1)) = $sum($uminus(X1),$uminus(X0))) )),
% 117.33/19.59 introduced(theory,[tha_inverse_op_op_inverses])).
% 117.33/19.59 tff(f8,definition,(
% 117.33/19.59 ( ! [X0 : $int] : (0 = $sum(X0,$uminus(X0))) )),
% 117.33/19.59 introduced(theory,[tha_inverse_op_unit])).
% 117.33/19.59 tff(f9,definition,(
% 117.33/19.59 ( ! [X0 : $int] : (~$less(X0,X0)) )),
% 117.33/19.59 introduced(theory,[tha_non-reflexivity])).
% 117.33/19.59 tff(f10,definition,(
% 117.33/19.59 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X1,X2) | ~$less(X0,X1) | $less(X0,X2)) )),
% 117.33/19.59 introduced(theory,[tha_transitivity])).
% 117.33/19.59 tff(f11,definition,(
% 117.33/19.59 ( ! [X0 : $int,X1 : $int] : ($less(X0,X1) | $less(X1,X0) | X0 = X1) )),
% 117.33/19.59 introduced(theory,[tha_order_totality])).
% 117.33/19.59 tff(f12,definition,(
% 117.33/19.59 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X0,X1) | $less($sum(X0,X2),$sum(X1,X2))) )),
% 117.33/19.59 introduced(theory,[tha_order_monotonicity])).
% 117.33/19.59 tff(f13,definition,(
% 117.33/19.59 ( ! [X0 : $int,X1 : $int] : ($less(X1,$sum(X0,1)) | $less(X0,X1)) )),
% 117.33/19.59 introduced(theory,[tha_order_plus_one_dichotomy])).
% 117.33/19.59 tff(f15,definition,(
% 117.33/19.59 ( ! [X0 : $int,X1 : $int] : (~$less(X1,$sum(X0,1)) | ~$less(X0,X1)) )),
% 117.33/19.59 introduced(theory,[tha_extra_integer_ordering])).
% 117.33/19.59 tff(f16,plain,(
% 117.33/19.59 ~(! [X0 : $int,X1 : $int,X2 : $int] : ((~$less(X0,$sum(X1,$uminus(X2))) & ~$less($sum(X1,X2),X0)) <=> p(X0,X1,X2)) => ! [X3 : $int,X4 : $int,X5 : $int,X6 : $int] : (~$less(X6,X5) => (p(X3,X4,X5) => p(X3,X4,X6))))),
% 117.33/19.59 inference(rectify,[],[f3])).
% 117.33/19.59 tff(f17,plain,(
% 117.33/19.59 ? [X3 : $int,X4 : $int,X5 : $int,X6 : $int] : ((~p(X3,X4,X6) & p(X3,X4,X5)) & ~$less(X6,X5)) & ! [X0 : $int,X1 : $int,X2 : $int] : ((~$less(X0,$sum(X1,$uminus(X2))) & ~$less($sum(X1,X2),X0)) <=> p(X0,X1,X2))),
% 117.33/19.59 inference(ennf_transformation,[],[f16])).
% 117.33/19.59 tff(f18,plain,(
% 117.33/19.59 ? [X3 : $int,X4 : $int,X5 : $int,X6 : $int] : (~p(X3,X4,X6) & p(X3,X4,X5) & ~$less(X6,X5)) & ! [X0 : $int,X1 : $int,X2 : $int] : ((~$less(X0,$sum(X1,$uminus(X2))) & ~$less($sum(X1,X2),X0)) <=> p(X0,X1,X2))),
% 117.33/19.59 inference(flattening,[],[f17])).
% 117.33/19.59 tff(f19,plain,(
% 117.33/19.59 ( ! [X2 : $int,X0 : $int,X1 : $int] : (p(X0,X1,X2) | $less($sum(X1,X2),X0) | $less(X0,$sum(X1,$uminus(X2)))) )),
% 117.33/19.59 inference(cnf_transformation,[],[f18])).
% 117.33/19.59 tff(f20,plain,(
% 117.33/19.59 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less($sum(X1,X2),X0) | ~p(X0,X1,X2)) )),
% 117.33/19.59 inference(cnf_transformation,[],[f18])).
% 117.33/19.59 tff(f21,plain,(
% 117.33/19.59 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X0,$sum(X1,$uminus(X2))) | ~p(X0,X1,X2)) )),
% 117.33/19.59 inference(cnf_transformation,[],[f18])).
% 117.33/19.59 tff(f22,plain,(
% 117.33/19.59 ~$less(sK3,sK2)),
% 117.33/19.59 inference(cnf_transformation,[],[f18])).
% 117.33/19.59 tff(f23,plain,(
% 117.33/19.59 p(sK0,sK1,sK2)),
% 117.33/19.59 inference(cnf_transformation,[],[f18])).
% 117.33/19.59 tff(f24,plain,(
% 117.33/19.59 ~p(sK0,sK1,sK3)),
% 117.33/19.59 inference(cnf_transformation,[],[f18])).
% 117.33/19.59 tff(f25,plain,(
% 117.33/19.59 $less($sum(sK1,sK3),sK0) | $less(sK0,$sum(sK1,$uminus(sK3)))),
% 117.33/19.59 inference(resolution,[],[f19,f24])).
% 117.33/19.59 tff(f27,definition,(
% 117.33/19.59 spl4_1 <=> $less(sK0,$sum(sK1,$uminus(sK3)))),
% 117.33/19.59 introduced(definition,[new_symbols(definition,[spl4_1])],[avatar_definition])).
% 117.33/19.59 tff(f29,plain,(
% 117.33/19.59 $less(sK0,$sum(sK1,$uminus(sK3))) | ~spl4_1),
% 117.33/19.59 inference(avatar_component_clause,[],[f27])).
% 117.33/19.59 tff(f31,definition,(
% 117.33/19.59 spl4_2 <=> $less($sum(sK1,sK3),sK0)),
% 117.33/19.59 introduced(definition,[new_symbols(definition,[spl4_2])],[avatar_definition])).
% 117.33/19.59 tff(f33,plain,(
% 117.33/19.59 $less($sum(sK1,sK3),sK0) | ~spl4_2),
% 117.33/19.59 inference(avatar_component_clause,[],[f31])).
% 117.33/19.59 tff(f34,plain,(
% 117.33/19.59 spl4_1 | spl4_2),
% 117.33/19.59 inference(avatar_split_clause,[],[f25,f31,f27])).
% 117.33/19.59 tff(f42,plain,(
% 117.33/19.59 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~p(X2,X1,X0) | ~$less($sum(X0,X1),X2)) )),
% 117.33/19.59 inference(superposition,[],[f20,f4])).
% 117.33/19.59 tff(f43,plain,(
% 117.33/19.59 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~p(X2,X1,X0) | ~$less(X2,$sum($uminus(X0),X1))) )),
% 117.33/19.59 inference(superposition,[],[f21,f4])).
% 117.33/19.59 tff(f53,plain,(
% 117.33/19.59 ( ! [X0 : $int,X1 : $int] : (~$less(X1,$sum(1,X0)) | ~$less(X0,X1)) )),
% 117.33/19.59 inference(superposition,[],[f15,f4])).
% 117.33/19.59 tff(f55,plain,(
% 117.33/19.59 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X0,X1) | $less(X0,$sum(X2,1)) | $less(X2,X1)) )),
% 117.33/19.59 inference(resolution,[],[f10,f13])).
% 117.33/19.59 tff(f57,plain,(
% 117.33/19.59 ( ! [X0 : $int] : (~$less(X0,$sum(sK1,sK3)) | $less(X0,sK0)) ) | ~spl4_2),
% 117.33/19.59 inference(resolution,[],[f33,f10])).
% 117.33/19.59 tff(f67,plain,(
% 117.33/19.59 $less(sK2,sK3) | sK2 = sK3),
% 117.33/19.59 inference(resolution,[],[f11,f22])).
% 117.33/19.59 tff(f77,definition,(
% 117.33/19.59 spl4_3 <=> sK2 = sK3),
% 117.33/19.59 introduced(definition,[new_symbols(definition,[spl4_3])],[avatar_definition])).
% 117.33/19.59 tff(f79,plain,(
% 117.33/19.59 sK2 = sK3 | ~spl4_3),
% 117.33/19.59 inference(avatar_component_clause,[],[f77])).
% 117.33/19.59 tff(f81,definition,(
% 117.33/19.59 spl4_4 <=> $less(sK2,sK3)),
% 117.33/19.59 introduced(definition,[new_symbols(definition,[spl4_4])],[avatar_definition])).
% 117.33/19.59 tff(f83,plain,(
% 117.33/19.59 $less(sK2,sK3) | ~spl4_4),
% 117.33/19.59 inference(avatar_component_clause,[],[f81])).
% 117.33/19.59 tff(f85,plain,(
% 117.33/19.59 spl4_3 | spl4_4),
% 117.33/19.59 inference(avatar_split_clause,[],[f67,f81,f77])).
% 117.33/19.59 tff(f87,plain,(
% 117.33/19.59 ~p(sK0,sK1,sK2) | ~spl4_3),
% 117.33/19.59 inference(superposition,[],[f24,f79])).
% 117.33/19.59 tff(f89,plain,(
% 117.33/19.59 $false | ~spl4_3),
% 117.33/19.59 inference(forward_subsumption_resolution,[],[f87,f23])).
% 117.33/19.59 tff(f90,plain,(
% 117.33/19.59 ~spl4_3),
% 117.33/19.59 inference(avatar_contradiction_clause,[],[f89])).
% 117.33/19.59 tff(f94,plain,(
% 117.33/19.59 ( ! [X0 : $int,X1 : $int] : ($uminus($sum(X0,X1)) = $sum($uminus(X0),$uminus(X1))) )),
% 117.33/19.59 inference(superposition,[],[f7,f4])).
% 117.33/19.59 tff(f110,plain,(
% 117.33/19.59 ( ! [X0 : $int,X1 : $int] : ($sum(0,X1) = $sum(X0,$sum($uminus(X0),X1))) )),
% 117.33/19.59 inference(superposition,[],[f5,f8])).
% 117.33/19.59 tff(f117,plain,(
% 117.33/19.59 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum(X0,$sum(X1,X2)) = $sum(X1,$sum(X2,X0))) )),
% 117.33/19.59 inference(superposition,[],[f5,f4])).
% 117.33/19.59 tff(f127,plain,(
% 117.33/19.59 ( ! [X0 : $int,X1 : $int] : ($sum(X0,$sum($uminus(X0),X1)) = X1) )),
% 117.33/19.59 inference(evaluation,[],[f110])).
% 117.33/19.59 tff(f130,plain,(
% 117.33/19.59 ( ! [X0 : $int] : ($less($sum(sK2,X0),$sum(sK3,X0))) ) | ~spl4_4),
% 117.33/19.59 inference(resolution,[],[f83,f12])).
% 117.33/19.59 tff(f134,plain,(
% 117.33/19.59 ~$less($sum(sK2,sK1),sK0)),
% 117.33/19.59 inference(resolution,[],[f42,f23])).
% 117.33/19.59 tff(f136,plain,(
% 117.33/19.59 ~$less($sum(sK1,sK2),sK0)),
% 117.33/19.59 inference(forward_demodulation,[],[f134,f4])).
% 117.33/19.59 tff(f163,plain,(
% 117.33/19.59 ( ! [X0 : $int] : ($less($sum(sK2,X0),$sum(X0,sK3))) ) | ~spl4_4),
% 117.33/19.59 inference(superposition,[],[f130,f4])).
% 117.33/19.59 tff(f173,plain,(
% 117.33/19.59 ~$less(sK0,$sum($uminus(sK2),sK1))),
% 117.33/19.59 inference(resolution,[],[f43,f23])).
% 117.33/19.59 tff(f175,plain,(
% 117.33/19.59 ~$less(sK0,$sum(sK1,$uminus(sK2)))),
% 117.33/19.59 inference(forward_demodulation,[],[f173,f4])).
% 117.33/19.59 tff(f243,definition,(
% 117.33/19.59 spl4_9 <=> $less($sum(sK1,$uminus(sK2)),sK0)),
% 117.33/19.59 introduced(definition,[new_symbols(definition,[spl4_9])],[avatar_definition])).
% 117.33/19.59 tff(f244,plain,(
% 117.33/19.59 ~$less($sum(sK1,$uminus(sK2)),sK0) | spl4_9),
% 117.33/19.59 inference(avatar_component_clause,[],[f243])).
% 117.33/19.59 tff(f245,plain,(
% 117.33/19.59 $less($sum(sK1,$uminus(sK2)),sK0) | ~spl4_9),
% 117.33/19.59 inference(avatar_component_clause,[],[f243])).
% 117.33/19.59 tff(f247,definition,(
% 117.33/19.59 spl4_10 <=> sK0 = $sum(sK1,$uminus(sK2))),
% 117.33/19.59 introduced(definition,[new_symbols(definition,[spl4_10])],[avatar_definition])).
% 117.33/19.59 tff(f249,plain,(
% 117.33/19.59 sK0 = $sum(sK1,$uminus(sK2)) | ~spl4_10),
% 117.33/19.59 inference(avatar_component_clause,[],[f247])).
% 117.33/19.59 tff(f311,plain,(
% 117.33/19.59 ( ! [X0 : $int] : (~$less(X0,$sum(sK1,$uminus(sK2))) | $less(X0,sK0)) ) | ~spl4_9),
% 117.33/19.59 inference(resolution,[],[f245,f10])).
% 117.33/19.59 tff(f334,plain,(
% 117.33/19.59 ( ! [X0 : $int,X1 : $int] : ($sum(X1,$sum(X0,$uminus(X1))) = X0) )),
% 117.33/19.59 inference(superposition,[],[f127,f4])).
% 117.33/19.59 tff(f349,plain,(
% 117.33/19.59 ( ! [X0 : $int] : ($less($sum(sK2,$sum($uminus(sK3),X0)),X0)) ) | ~spl4_4),
% 117.33/19.59 inference(superposition,[],[f130,f127])).
% 117.33/19.59 tff(f439,plain,(
% 117.33/19.59 ( ! [X0 : $int,X1 : $int] : ($uminus(X1) = $sum(X0,$uminus($sum(X0,X1)))) )),
% 117.33/19.59 inference(superposition,[],[f127,f94])).
% 117.33/19.59 tff(f694,plain,(
% 117.33/19.59 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum(X0,X1) = $sum(X2,$sum(X0,$sum(X1,$uminus(X2))))) )),
% 117.33/19.59 inference(superposition,[],[f127,f117])).
% 117.33/19.59 tff(f1081,plain,(
% 117.33/19.59 $less($sum(sK2,sK1),sK0) | (~spl4_2 | ~spl4_4)),
% 117.33/19.59 inference(resolution,[],[f57,f163])).
% 117.33/19.59 tff(f1086,plain,(
% 117.33/19.59 $less($sum(sK1,sK2),sK0) | (~spl4_2 | ~spl4_4)),
% 117.33/19.59 inference(forward_demodulation,[],[f1081,f4])).
% 117.33/19.59 tff(f1087,plain,(
% 117.33/19.59 $false | (~spl4_2 | ~spl4_4)),
% 117.33/19.59 inference(forward_subsumption_resolution,[],[f1086,f136])).
% 117.33/19.59 tff(f1088,plain,(
% 117.33/19.59 ~spl4_2 | ~spl4_4),
% 117.33/19.59 inference(avatar_contradiction_clause,[],[f1087])).
% 117.33/19.59 tff(f1093,plain,(
% 117.33/19.59 ( ! [X0 : $int] : ($less(X0,$sum(sK1,$uminus(sK3))) | $less(sK0,$sum(X0,1))) ) | ~spl4_1),
% 117.33/19.59 inference(resolution,[],[f29,f55])).
% 117.33/19.59 tff(f1094,plain,(
% 117.33/19.59 ( ! [X0 : $int] : ($less($sum(sK0,X0),$sum($sum(sK1,$uminus(sK3)),X0))) ) | ~spl4_1),
% 117.33/19.59 inference(resolution,[],[f29,f12])).
% 117.33/19.59 tff(f1096,plain,(
% 117.33/19.59 ( ! [X0 : $int] : ($less($sum(sK0,X0),$sum(sK1,$sum($uminus(sK3),X0)))) ) | ~spl4_1),
% 117.33/19.59 inference(forward_demodulation,[],[f1094,f5])).
% 117.33/19.59 tff(f1476,plain,(
% 117.33/19.59 $less(sK0,$sum($sum(sK1,$uminus(sK3)),1)) | ~spl4_1),
% 117.33/19.59 inference(resolution,[],[f1093,f9])).
% 117.33/19.59 tff(f1494,plain,(
% 117.33/19.59 $less(sK0,$sum(1,$sum(sK1,$uminus(sK3)))) | ~spl4_1),
% 117.33/19.59 inference(forward_demodulation,[],[f1476,f4])).
% 117.33/19.59 tff(f3343,plain,(
% 117.33/19.59 ( ! [X0 : $int] : ($less($sum(sK0,$sum(X0,$uminus($uminus(sK3)))),$sum(sK1,X0))) ) | ~spl4_1),
% 117.33/19.59 inference(superposition,[],[f1096,f334])).
% 117.33/19.59 tff(f3375,plain,(
% 117.33/19.59 ( ! [X0 : $int] : ($less($sum(sK0,$sum(X0,sK3)),$sum(sK1,X0))) ) | ~spl4_1),
% 117.33/19.59 inference(evaluation,[],[f3343])).
% 117.33/19.59 tff(f59529,plain,(
% 117.33/19.59 $less(sK0,$sum(sK1,$uminus(sK2))) | sK0 = $sum(sK1,$uminus(sK2)) | spl4_9),
% 117.33/19.59 inference(resolution,[],[f244,f11])).
% 117.33/19.59 tff(f59548,plain,(
% 117.33/19.59 sK0 = $sum(sK1,$uminus(sK2)) | spl4_9),
% 117.33/19.59 inference(forward_subsumption_resolution,[],[f59529,f175])).
% 117.33/19.59 tff(f59550,plain,(
% 117.33/19.59 spl4_10 | spl4_9),
% 117.33/19.59 inference(avatar_split_clause,[],[f59548,f243,f247])).
% 117.33/19.59 tff(f59625,plain,(
% 117.33/19.59 $uminus($uminus(sK2)) = $sum(sK1,$uminus(sK0)) | ~spl4_10),
% 117.33/19.59 inference(superposition,[],[f439,f249])).
% 117.33/19.59 tff(f59729,plain,(
% 117.33/19.59 sK2 = $sum(sK1,$uminus(sK0)) | ~spl4_10),
% 117.33/19.59 inference(evaluation,[],[f59625])).
% 117.33/19.59 tff(f92962,plain,(
% 117.33/19.59 ~$less($sum(sK1,$uminus(sK3)),sK0) | ~spl4_1),
% 117.33/19.59 inference(resolution,[],[f1494,f53])).
% 117.33/19.59 tff(f94500,plain,(
% 117.33/19.59 $less($sum(sK2,$sum($uminus(sK3),$sum(sK1,$uminus(sK2)))),sK0) | (~spl4_4 | ~spl4_9)),
% 117.33/19.59 inference(resolution,[],[f311,f349])).
% 117.33/19.59 tff(f94518,plain,(
% 117.33/19.59 $less($sum($uminus(sK3),sK1),sK0) | (~spl4_4 | ~spl4_9)),
% 117.33/19.59 inference(forward_demodulation,[],[f94500,f694])).
% 117.33/19.59 tff(f94525,plain,(
% 117.33/19.59 $less($sum(sK1,$uminus(sK3)),sK0) | (~spl4_4 | ~spl4_9)),
% 117.33/19.59 inference(forward_demodulation,[],[f94518,f4])).
% 117.33/19.59 tff(f145813,definition,(
% 117.33/19.59 spl4_727 <=> $less($sum(sK1,$uminus(sK3)),sK0)),
% 117.33/19.59 introduced(definition,[new_symbols(definition,[spl4_727])],[avatar_definition])).
% 117.33/19.59 tff(f238609,plain,(
% 117.33/19.59 $less($sum(sK0,$sum($uminus(sK0),sK3)),sK2) | (~spl4_1 | ~spl4_10)),
% 117.33/19.59 inference(superposition,[],[f3375,f59729])).
% 117.33/19.59 tff(f239208,plain,(
% 117.33/19.59 $less(sK3,sK2) | (~spl4_1 | ~spl4_10)),
% 117.33/19.59 inference(forward_demodulation,[],[f238609,f127])).
% 117.33/19.59 tff(f239317,plain,(
% 117.33/19.59 $false | (~spl4_1 | ~spl4_10)),
% 117.33/19.59 inference(forward_subsumption_resolution,[],[f239208,f22])).
% 117.33/19.59 tff(f239318,plain,(
% 117.33/19.59 ~spl4_1 | ~spl4_10),
% 117.33/19.59 inference(avatar_contradiction_clause,[],[f239317])).
% 117.33/19.59 tff(f239521,plain,(
% 117.33/19.59 spl4_727 | ~spl4_4 | ~spl4_9),
% 117.33/19.59 inference(avatar_split_clause,[],[f94525,f243,f81,f145813])).
% 117.33/19.59 tff(f583422,plain,(
% 117.33/19.59 ~spl4_727 | ~spl4_1),
% 117.33/19.59 inference(avatar_split_clause,[],[f92962,f27,f145813])).
% 117.33/19.59 cnf(s1, plain, spl4_1 | spl4_2, inference(sat_conversion,[],[f34])).
% 117.33/19.59 cnf(s3, plain, spl4_3 | spl4_4, inference(sat_conversion,[],[f85])).
% 117.33/19.59 cnf(s4, plain, ~spl4_3, inference(sat_conversion,[],[f90])).
% 117.33/19.59 cnf(s11, plain, ~spl4_2 | ~spl4_4, inference(sat_conversion,[],[f1088])).
% 117.33/19.59 cnf(s245, plain, spl4_9 | spl4_10, inference(sat_conversion,[],[f59550])).
% 117.33/19.59 cnf(s2600, plain, ~spl4_1 | ~spl4_10, inference(sat_conversion,[],[f239318])).
% 117.33/19.59 cnf(s2613, plain, ~spl4_4 | ~spl4_9 | spl4_727, inference(sat_conversion,[],[f239521])).
% 117.33/19.59 cnf(s6498, plain, ~spl4_1 | ~spl4_727, inference(sat_conversion,[],[f583422])).
% 117.33/19.59 cnf(s6553, plain, spl4_4, inference(rat,[],[s3,s4])).
% 117.33/19.59 cnf(s6556, plain, ~spl4_2, inference(rat,[],[s11,s6553])).
% 117.33/19.59 cnf(s6563, plain, spl4_1, inference(rat,[],[s1,s6556])).
% 117.33/19.59 cnf(s6564, plain, ~spl4_727, inference(rat,[],[s6498,s6563])).
% 117.33/19.59 cnf(s6566, plain, ~spl4_10, inference(rat,[],[s2600,s6563])).
% 117.33/19.59 cnf(s6570, plain, ~spl4_9, inference(rat,[],[s2613,s6553,s6564])).
% 117.33/19.59 cnf(s6571, plain, $false, inference(rat,[],[s245,s6566,s6570])).
% 117.33/19.59 tff(f583423,plain,(
% 117.33/19.59 $false),
% 117.33/19.59 inference(avatar_sat_refutation,[],[s6571])).
% 117.33/19.59 % SZS output end Proof for theBenchmark
% 117.33/19.59 % (749865)------------------------------
% 117.33/19.59 % (749865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.33/19.59 % (749865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.33/19.59 % (749865)CaDiCaL version: 2.1.3
% 117.33/19.59 % (749865)Termination reason: Refutation
% 117.33/19.59 % (749865)Time elapsed: 19.216 s
% 117.33/19.59 % (749865)Peak memory usage: 167 MB
% 117.33/19.59 % (749865)Instructions burned: 32233 (million)
% 117.33/19.59 % (749859)Success in time 19.356 s
% 117.33/19.59 % Vampire exiting
%------------------------------------------------------------------------------