%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWX109_1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n015.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:30 PM UTC 2026
% Result : Theorem 7.64s 2.51s
% Output : Refutation 7.64s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWX109_1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.26 % Computer : n015.cluster.edu
% 0.11/0.26 % Model : x86_64 x86_64
% 0.11/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.26 % Memory : 8046.5625MB
% 0.11/0.26 % OS : Linux 6.8.0-71-generic
% 0.11/0.26 % CPULimit : 300
% 0.11/0.26 % WCLimit : 300
% 0.11/0.26 % DateTime : Mon Sep 28 15:04:47 UTC 2026
% 0.11/0.26 % CPUTime :
% 0.11/0.26 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.25/0.30 Running first-order model finding
% 0.25/0.30 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.29/1.26 % (2696055)Will run a generic schedule for satisfiability detection.
% 6.29/1.26 % (2696066)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1254130329:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 6.29/1.26 % (2696061)% WARNING: option uhcvi not known.
% 6.29/1.26 % (2696062)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1361585863:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 6.29/1.26 % (2696060)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=263082410_2999 on theBenchmark for (2999ds/0Mi)
% 6.29/1.26 % (2696064)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3366409872:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 6.29/1.26 % (2696065)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1215612379:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 6.29/1.26 % (2696061)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=93398551:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 6.29/1.26 % (2696063)dis+10_1_sil=32000:sp=arity:random_seed=35562442:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 6.29/1.26 % (2696060)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.29/1.26 % (2696060)Terminated due to inappropriate strategy.
% 6.29/1.26 % (2696060)------------------------------
% 6.29/1.26 % (2696060)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.29/1.26 % (2696060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.26 % (2696060)CaDiCaL version: 2.1.3
% 6.29/1.26 % (2696060)Termination reason: Inappropriate
% 6.29/1.26 % (2696060)Time elapsed: 0.002 s
% 6.29/1.26 % (2696060)Peak memory usage: 10 MB
% 6.29/1.26 % (2696060)Instructions burned: 2 (million)
% 6.29/1.26 % (2696060)------------------------------
% 6.29/1.26 % (2696060)------------------------------
% 6.29/1.26 % (2696075)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3409957172:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 6.29/1.26 % (2696075)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.29/1.26 % (2696075)Terminated due to inappropriate strategy.
% 6.29/1.26 % (2696075)------------------------------
% 6.29/1.26 % (2696075)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.29/1.26 % (2696075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.26 % (2696075)CaDiCaL version: 2.1.3
% 6.29/1.26 % (2696075)Termination reason: Inappropriate
% 6.29/1.26 % (2696075)Time elapsed: 0.002 s
% 6.29/1.26 % (2696075)Peak memory usage: 10 MB
% 6.29/1.26 % (2696075)Instructions burned: 2 (million)
% 6.29/1.26 % (2696075)------------------------------
% 6.29/1.26 % (2696075)------------------------------
% 6.29/1.26 % (2696078)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4076351139:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 6.29/1.26 % (2696066)Instruction limit reached!
% 6.29/1.26 % (2696066)------------------------------
% 6.29/1.26 % (2696066)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.29/1.26 % (2696066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.26 % (2696066)CaDiCaL version: 2.1.3
% 6.29/1.26 % (2696066)Termination reason: Instruction limit
% 6.29/1.26 % (2696066)Termination phase: Saturation
% 6.29/1.26 % (2696066)Time elapsed: 0.081 s
% 6.29/1.26 % (2696066)Peak memory usage: 13 MB
% 6.29/1.26 % (2696066)Instructions burned: 159 (million)
% 6.29/1.26 % (2696080)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=1838470691:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 6.29/1.26 % (2696064)Instruction limit reached!
% 6.29/1.26 % (2696064)------------------------------
% 6.29/1.26 % (2696064)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.29/1.26 % (2696064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.26 % (2696064)CaDiCaL version: 2.1.3
% 6.29/1.26 % (2696064)Termination reason: Instruction limit
% 6.29/1.26 % (2696064)Termination phase: Saturation
% 6.29/1.26 % (2696064)Time elapsed: 0.112 s
% 6.29/1.26 % (2696064)Peak memory usage: 12 MB
% 6.29/1.26 % (2696064)Instructions burned: 117 (million)
% 6.29/1.26 % (2696063)Instruction limit reached!
% 6.29/1.26 % (2696063)------------------------------
% 6.29/1.26 % (2696063)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.77/1.71 % (2696063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.77/1.71 % (2696063)CaDiCaL version: 2.1.3
% 8.77/1.71 % (2696063)Termination reason: Instruction limit
% 8.77/1.71 % (2696063)Termination phase: Saturation
% 8.77/1.71 % (2696063)Time elapsed: 0.111 s
% 8.77/1.71 % (2696063)Peak memory usage: 12 MB
% 8.77/1.71 % (2696063)Instructions burned: 103 (million)
% 8.77/1.71 % (2696065)Instruction limit reached!
% 8.77/1.71 % (2696065)------------------------------
% 8.77/1.71 % (2696065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.77/1.71 % (2696065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.77/1.71 % (2696065)CaDiCaL version: 2.1.3
% 8.77/1.71 % (2696065)Termination reason: Instruction limit
% 8.77/1.71 % (2696065)Termination phase: Saturation
% 8.77/1.71 % (2696065)Time elapsed: 0.130 s
% 8.77/1.71 % (2696065)Peak memory usage: 12 MB
% 8.77/1.71 % (2696065)Instructions burned: 131 (million)
% 8.77/1.71 % (2696083)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=728948498:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 8.77/1.71 % (2696082)ott-21_1_sil=16000:fs=off:random_seed=808420748:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 8.77/1.71 % (2696084)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3983896401:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 8.77/1.71 % (2696084)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 8.77/1.71 % (2696084)Terminated due to inappropriate strategy.
% 8.77/1.71 % (2696084)------------------------------
% 8.77/1.71 % (2696084)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.77/1.71 % (2696084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.77/1.71 % (2696084)CaDiCaL version: 2.1.3
% 8.77/1.71 % (2696084)Termination reason: Inappropriate
% 8.77/1.71 % (2696084)Time elapsed: 0.002 s
% 8.77/1.71 % (2696084)Peak memory usage: 10 MB
% 8.77/1.71 % (2696084)Instructions burned: 1 (million)
% 8.77/1.71 % (2696084)------------------------------
% 8.77/1.71 % (2696084)------------------------------
% 8.77/1.71 % (2696088)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3859241165:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 8.77/1.71 % (2696078)Instruction limit reached!
% 8.77/1.71 % (2696078)------------------------------
% 8.77/1.71 % (2696078)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.77/1.71 % (2696078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.77/1.71 % (2696078)CaDiCaL version: 2.1.3
% 8.77/1.71 % (2696078)Termination reason: Instruction limit
% 8.77/1.71 % (2696078)Termination phase: Saturation
% 8.77/1.71 % (2696078)Time elapsed: 0.142 s
% 8.77/1.71 % (2696078)Peak memory usage: 13 MB
% 8.77/1.71 % (2696078)Instructions burned: 134 (million)
% 8.77/1.71 % (2696090)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=901314240:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 8.77/1.71 % (2696090)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 8.77/1.71 % (2696090)Terminated due to inappropriate strategy.
% 8.77/1.71 % (2696090)------------------------------
% 8.77/1.71 % (2696090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.77/1.71 % (2696090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.77/1.71 % (2696090)CaDiCaL version: 2.1.3
% 8.77/1.71 % (2696090)Termination reason: Inappropriate
% 8.77/1.71 % (2696090)Time elapsed: 0.002 s
% 8.77/1.71 % (2696090)Peak memory usage: 11 MB
% 8.77/1.71 % (2696090)Instructions burned: 1 (million)
% 8.77/1.71 % (2696090)------------------------------
% 8.77/1.71 % (2696090)------------------------------
% 8.77/1.71 % (2696092)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=1039505905: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)
% 8.77/1.71 % (2696082)Instruction limit reached!
% 8.77/1.71 % (2696082)------------------------------
% 8.77/1.71 % (2696082)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.77/1.71 % (2696082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.77/1.71 % (2696082)CaDiCaL version: 2.1.3
% 8.77/1.71 % (2696082)Termination reason: Instruction limit
% 8.77/1.71 % (2696082)Termination phase: Saturation
% 7.64/2.51 % (2696082)Time elapsed: 0.143 s
% 7.64/2.51 % (2696082)Peak memory usage: 12 MB
% 7.64/2.51 % (2696082)Instructions burned: 180 (million)
% 7.64/2.51 % (2696094)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4141154800:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi)
% 7.64/2.51 % (2696080)Instruction limit reached!
% 7.64/2.51 % (2696080)------------------------------
% 7.64/2.51 % (2696080)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.64/2.51 % (2696080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.64/2.51 % (2696080)CaDiCaL version: 2.1.3
% 7.64/2.51 % (2696080)Termination reason: Instruction limit
% 7.64/2.51 % (2696080)Termination phase: Saturation
% 7.64/2.51 % (2696080)Time elapsed: 0.337 s
% 7.64/2.51 % (2696080)Peak memory usage: 18 MB
% 7.64/2.51 % (2696080)Instructions burned: 684 (million)
% 7.64/2.51 % (2696096)fmb+10_1_sil=64000:random_seed=2630445074:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi)
% 7.64/2.51 % (2696096)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.64/2.51 % (2696096)Terminated due to inappropriate strategy.
% 7.64/2.51 % (2696096)------------------------------
% 7.64/2.51 % (2696096)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.64/2.51 % (2696096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.64/2.51 % (2696096)CaDiCaL version: 2.1.3
% 7.64/2.51 % (2696096)Termination reason: Inappropriate
% 7.64/2.51 % (2696096)Time elapsed: 0.002 s
% 7.64/2.51 % (2696096)Peak memory usage: 11 MB
% 7.64/2.51 % (2696096)Instructions burned: 2 (million)
% 7.64/2.51 % (2696096)------------------------------
% 7.64/2.51 % (2696096)------------------------------
% 7.64/2.51 % (2696098)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2478174897:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi)
% 7.64/2.51 % (2696098)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.64/2.51 % (2696098)Terminated due to inappropriate strategy.
% 7.64/2.51 % (2696098)------------------------------
% 7.64/2.51 % (2696098)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.64/2.51 % (2696098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.64/2.51 % (2696098)CaDiCaL version: 2.1.3
% 7.64/2.51 % (2696098)Termination reason: Inappropriate
% 7.64/2.51 % (2696098)Time elapsed: 0.001 s
% 7.64/2.51 % (2696098)Peak memory usage: 10 MB
% 7.64/2.51 % (2696098)Instructions burned: 2 (million)
% 7.64/2.51 % (2696098)------------------------------
% 7.64/2.51 % (2696098)------------------------------
% 7.64/2.51 % (2696100)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3248174137:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi)
% 7.64/2.51 % (2696100)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.64/2.51 % (2696100)Terminated due to inappropriate strategy.
% 7.64/2.51 % (2696100)------------------------------
% 7.64/2.51 % (2696100)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.64/2.51 % (2696100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.64/2.51 % (2696100)CaDiCaL version: 2.1.3
% 7.64/2.51 % (2696100)Termination reason: Inappropriate
% 7.64/2.51 % (2696100)Time elapsed: 0.002 s
% 7.64/2.51 % (2696100)Peak memory usage: 11 MB
% 7.64/2.51 % (2696100)Instructions burned: 1 (million)
% 7.64/2.51 % (2696100)------------------------------
% 7.64/2.51 % (2696100)------------------------------
% 7.64/2.51 % (2696102)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2316922630:i=5131_2994 on theBenchmark for (2994ds/5131Mi)
% 7.64/2.51 % (2696083)Instruction limit reached!
% 7.64/2.51 % (2696083)------------------------------
% 7.64/2.51 % (2696083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.64/2.51 % (2696083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.64/2.51 % (2696083)CaDiCaL version: 2.1.3
% 7.64/2.51 % (2696083)Termination reason: Instruction limit
% 7.64/2.51 % (2696083)Termination phase: Saturation
% 7.64/2.51 % (2696083)Time elapsed: 0.525 s
% 7.64/2.51 % (2696083)Peak memory usage: 14 MB
% 7.64/2.51 % (2696083)Instructions burned: 477 (million)
% 7.64/2.51 % (2696104)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2734755559:i=1472:ins=7:fdi=8:gsp=on_2992 on theBenchmark for (2992ds/1472Mi)
% 7.64/2.51 % (2696092)Instruction limit reached!
% 7.64/2.51 % (2696092)------------------------------
% 7.64/2.51 % (2696092)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.64/2.51 % (2696092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.64/2.51 % (2696092)CaDiCaL version: 2.1.3
% 7.64/2.51 % (2696092)Termination reason: Instruction limit
% 7.64/2.51 % (2696092)Termination phase: Saturation
% 7.64/2.51 % (2696092)Time elapsed: 0.632 s
% 7.64/2.51 % (2696092)Peak memory usage: 17 MB
% 7.64/2.51 % (2696092)Instructions burned: 692 (million)
% 7.64/2.51 % (2696106)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=468848634:i=6324_2990 on theBenchmark for (2990ds/6324Mi)
% 7.64/2.51 % (2696106)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.64/2.51 % (2696106)Terminated due to inappropriate strategy.
% 7.64/2.51 % (2696106)------------------------------
% 7.64/2.51 % (2696106)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.64/2.51 % (2696106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.64/2.51 % (2696106)CaDiCaL version: 2.1.3
% 7.64/2.51 % (2696106)Termination reason: Inappropriate
% 7.64/2.51 % (2696106)Time elapsed: 0.002 s
% 7.64/2.51 % (2696106)Peak memory usage: 10 MB
% 7.64/2.51 % (2696106)Instructions burned: 2 (million)
% 7.64/2.51 % (2696106)------------------------------
% 7.64/2.51 % (2696106)------------------------------
% 7.64/2.51 % (2696108)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1910397563:fmbsr=2.30978:i=2174_2990 on theBenchmark for (2990ds/2174Mi)
% 7.64/2.51 % (2696108)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.64/2.51 % (2696108)Terminated due to inappropriate strategy.
% 7.64/2.51 % (2696108)------------------------------
% 7.64/2.51 % (2696108)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.64/2.51 % (2696108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.64/2.51 % (2696108)CaDiCaL version: 2.1.3
% 7.64/2.51 % (2696108)Termination reason: Inappropriate
% 7.64/2.51 % (2696108)Time elapsed: 0.002 s
% 7.64/2.51 % (2696108)Peak memory usage: 11 MB
% 7.64/2.51 % (2696108)Instructions burned: 1 (million)
% 7.64/2.51 % (2696108)------------------------------
% 7.64/2.51 % (2696108)------------------------------
% 7.64/2.51 % (2696110)ott-2_1_sil=16000:newcnf=on:random_seed=140137608:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2989 on theBenchmark for (2989ds/869Mi)
% 7.64/2.51 % (2696094)Instruction limit reached!
% 7.64/2.51 % (2696094)------------------------------
% 7.64/2.51 % (2696094)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.64/2.51 % (2696094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.64/2.51 % (2696094)CaDiCaL version: 2.1.3
% 7.64/2.51 % (2696094)Termination reason: Instruction limit
% 7.64/2.51 % (2696094)Termination phase: Saturation
% 7.64/2.51 % (2696094)Time elapsed: 0.843 s
% 7.64/2.51 % (2696094)Peak memory usage: 22 MB
% 7.64/2.51 % (2696094)Instructions burned: 879 (million)
% 7.64/2.51 % (2696112)ott+10_1_sil=32000:tgt=ground:random_seed=3255174340:i=5114:av=off_2988 on theBenchmark for (2988ds/5114Mi)
% 7.64/2.51 % (2696088)Instruction limit reached!
% 7.64/2.51 % (2696088)------------------------------
% 7.64/2.51 % (2696088)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.64/2.51 % (2696088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.64/2.51 % (2696088)CaDiCaL version: 2.1.3
% 7.64/2.51 % (2696088)Termination reason: Instruction limit
% 7.64/2.51 % (2696088)Termination phase: Saturation
% 7.64/2.51 % (2696088)Time elapsed: 1.147 s
% 7.64/2.51 % (2696088)Peak memory usage: 19 MB
% 7.64/2.51 % (2696088)Instructions burned: 1180 (million)
% 7.64/2.51 % (2696114)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1264891705:i=54282_2986 on theBenchmark for (2986ds/54282Mi)
% 7.64/2.51 % (2696114)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.64/2.51 % (2696114)Terminated due to inappropriate strategy.
% 7.64/2.51 % (2696114)------------------------------
% 7.64/2.51 % (2696114)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.64/2.51 % (2696114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.64/2.51 % (2696114)CaDiCaL version: 2.1.3
% 7.64/2.51 % (2696114)Termination reason: Inappropriate
% 7.64/2.51 % (2696114)Time elapsed: 0.002 s
% 7.64/2.51 % (2696114)Peak memory usage: 11 MB
% 7.64/2.51 % (2696114)Instructions burned: 2 (million)
% 7.64/2.51 % (2696114)------------------------------
% 7.64/2.51 % (2696114)------------------------------
% 7.64/2.51 % (2696116)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2373473058:i=3512:aac=none_2985 on theBenchmark for (2985ds/3512Mi)
% 7.64/2.51 % (2696110)Instruction limit reached!
% 7.64/2.51 % (2696110)------------------------------
% 7.64/2.51 % (2696110)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.64/2.51 % (2696110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.64/2.51 % (2696110)CaDiCaL version: 2.1.3
% 7.64/2.51 % (2696110)Termination reason: Instruction limit
% 7.64/2.51 % (2696110)Termination phase: Saturation
% 7.64/2.51 % (2696110)Time elapsed: 0.804 s
% 7.64/2.51 % (2696110)Peak memory usage: 16 MB
% 7.64/2.51 % (2696110)Instructions burned: 869 (million)
% 7.64/2.51 % (2696118)dis+21_1_sil=32000:sas=cadical:random_seed=2637360955:i=3773:amm=off_2981 on theBenchmark for (2981ds/3773Mi)
% 7.64/2.51 % (2696104)Instruction limit reached!
% 7.64/2.51 % (2696104)------------------------------
% 7.64/2.51 % (2696104)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.64/2.51 % (2696104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.64/2.51 % (2696104)CaDiCaL version: 2.1.3
% 7.64/2.51 % (2696104)Termination reason: Instruction limit
% 7.64/2.51 % (2696104)Termination phase: Saturation
% 7.64/2.51 % (2696104)Time elapsed: 1.312 s
% 7.64/2.51 % (2696104)Peak memory usage: 23 MB
% 7.64/2.51 % (2696104)Instructions burned: 1472 (million)
% 7.64/2.51 % (2696120)ott+11_1_sil=16000:gs=on:random_seed=2563960128:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2979 on theBenchmark for (2979ds/2251Mi)
% 7.64/2.51 % (2696118) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2696055-2696118"...
% 7.64/2.51 % (2696118)...printing done.
% 7.64/2.51 % (2696118)Refutation found. Thanks to Tanya!
% 7.64/2.51 % SZS status Theorem for theBenchmark
% 7.64/2.51 % SZS output start Proof for theBenchmark
% 7.64/2.51 tff(type_def_5, type, general: $tType).
% 7.64/2.51 tff(type_def_6, type, symbol: $tType).
% 7.64/2.51 tff(func_def_0, type, f__integer__: $int > general).
% 7.64/2.51 tff(func_def_1, type, f__symbolic__: symbol > general).
% 7.64/2.51 tff(func_def_2, type, c__infimum__: general).
% 7.64/2.51 tff(func_def_3, type, c__supremum__: general).
% 7.64/2.51 tff(func_def_9, type, sK1: general > $int).
% 7.64/2.51 tff(func_def_10, type, sK2: general > symbol).
% 7.64/2.51 tff(func_def_11, type, sK3: (general * general) > $int).
% 7.64/2.51 tff(func_def_12, type, sK4: (general * general) > $int).
% 7.64/2.51 tff(func_def_13, type, sK5: (general * general) > general).
% 7.64/2.51 tff(func_def_14, type, sK6: (general * general) > general).
% 7.64/2.51 tff(func_def_15, type, sK7: general).
% 7.64/2.51 tff(func_def_16, type, sK8: general).
% 7.64/2.51 tff(func_def_17, type, sK9: general).
% 7.64/2.51 tff(func_def_18, type, sK10: general).
% 7.64/2.51 tff(func_def_19, type, sK11: $int).
% 7.64/2.51 tff(func_def_20, type, sK12: $int).
% 7.64/2.51 tff(func_def_21, type, sK13: general).
% 7.64/2.51 tff(func_def_22, type, sK14: general).
% 7.64/2.51 tff(pred_def_1, type, p__is_integer__: general > $o).
% 7.64/2.51 tff(pred_def_2, type, p__is_symbolic__: general > $o).
% 7.64/2.51 tff(pred_def_3, type, p__less_equal__: (general * general) > $o).
% 7.64/2.51 tff(pred_def_4, type, p__less__: (general * general) > $o).
% 7.64/2.51 tff(pred_def_5, type, p__greater_equal__: (general * general) > $o).
% 7.64/2.51 tff(pred_def_6, type, p__greater__: (general * general) > $o).
% 7.64/2.51 tff(pred_def_8, type, hq: (general * general) > $o).
% 7.64/2.51 tff(pred_def_9, type, tq: (general * general) > $o).
% 7.64/2.51 tff(pred_def_10, type, hp: (general * general) > $o).
% 7.64/2.51 tff(pred_def_11, type, tp: (general * general) > $o).
% 7.64/2.51 tff(pred_def_13, type, sP0: (general * general * general * general) > $o).
% 7.64/2.51 tff(f18,axiom,(
% 7.64/2.51 ! [X0 : general,X1 : general,X2 : general,X3 : general] : (((X0 = X2 & X1 = X3 & ? [X4 : general,X5 : general] : (X4 = X2 & ? [X6 : $int,X7 : $int] : (X5 = f__integer__($difference(X6,X7)) & f__integer__(X6) = X3 & X7 = 1) & hp(X4,X5))) => hq(X0,X1)) & ((X0 = X2 & X1 = X3 & ? [X4 : general,X5 : general] : (X4 = X2 & ? [X6 : $int,X7 : $int] : (X5 = f__integer__($difference(X6,X7)) & f__integer__(X6) = X3 & X7 = 1) & tp(X4,X5))) => tq(X0,X1)))),
% 7.64/2.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',formula_2_right_0)).
% 7.64/2.51 tff(f19,conjecture,(
% 7.64/2.51 ! [X0 : general,X1 : general,X2 : general,X3 : general] : (((X0 = X2 & ? [X4 : $int,X5 : $int] : (X1 = f__integer__($sum(X4,X5)) & f__integer__(X4) = X3 & X5 = 1) & ? [X6 : general,X7 : general] : (X6 = X2 & X7 = X3 & hp(X6,X7))) => hq(X0,X1)) & ((X0 = X2 & ? [X4 : $int,X5 : $int] : (X1 = f__integer__($sum(X4,X5)) & f__integer__(X4) = X3 & X5 = 1) & ? [X6 : general,X7 : general] : (X6 = X2 & X7 = X3 & tp(X6,X7))) => tq(X0,X1)))),
% 7.64/2.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',formula_3_left_0)).
% 7.64/2.51 tff(f20,negated_conjecture,(
% 7.64/2.51 ~ ! [X0 : general,X1 : general,X2 : general,X3 : general] : (((X0 = X2 & ? [X4 : $int,X5 : $int] : (X1 = f__integer__($sum(X4,X5)) & f__integer__(X4) = X3 & X5 = 1) & ? [X6 : general,X7 : general] : (X6 = X2 & X7 = X3 & hp(X6,X7))) => hq(X0,X1)) & ((X0 = X2 & ? [X4 : $int,X5 : $int] : (X1 = f__integer__($sum(X4,X5)) & f__integer__(X4) = X3 & X5 = 1) & ? [X6 : general,X7 : general] : (X6 = X2 & X7 = X3 & tp(X6,X7))) => tq(X0,X1)))),
% 7.64/2.51 inference(negated_conjecture,[status(cth)],[f19])).
% 7.64/2.51 tff(f22,plain,(
% 7.64/2.51 ! [X0 : general,X1 : general,X2 : general,X3 : general] : (((X0 = X2 & X1 = X3 & ? [X4 : general,X5 : general] : (X4 = X2 & ? [X6 : $int,X7 : $int] : (f__integer__($sum(X6,$uminus(X7))) = X5 & f__integer__(X6) = X3 & X7 = 1) & hp(X4,X5))) => hq(X0,X1)) & ((X0 = X2 & X1 = X3 & ? [X4 : general,X5 : general] : (X4 = X2 & ? [X6 : $int,X7 : $int] : (f__integer__($sum(X6,$uminus(X7))) = X5 & f__integer__(X6) = X3 & X7 = 1) & tp(X4,X5))) => tq(X0,X1)))),
% 7.64/2.51 inference(theory_normalization,[],[f18])).
% 7.64/2.51 tff(f23,definition,(
% 7.64/2.51 ( ! [X0 : $int,X1 : $int] : ($sum(X0,X1) = $sum(X1,X0)) )),
% 7.64/2.51 introduced(theory,[tha_commutativity])).
% 7.64/2.51 tff(f24,definition,(
% 7.64/2.51 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum(X0,$sum(X1,X2)) = $sum($sum(X0,X1),X2)) )),
% 7.64/2.51 introduced(theory,[tha_associativity])).
% 7.64/2.51 tff(f27,definition,(
% 7.64/2.51 ( ! [X0 : $int] : (0 = $sum(X0,$uminus(X0))) )),
% 7.64/2.51 introduced(theory,[tha_inverse_op_unit])).
% 7.64/2.51 tff(f35,plain,(
% 7.64/2.51 ! [X0 : general,X1 : general,X2 : general,X3 : general] : (((X0 = X2 & X1 = X3 & ? [X4 : general,X5 : general] : (X4 = X2 & ? [X6 : $int,X7 : $int] : (f__integer__($sum(X6,$uminus(X7))) = X5 & f__integer__(X6) = X3 & X7 = 1) & hp(X4,X5))) => hq(X0,X1)) & ((X0 = X2 & X1 = X3 & ? [X8 : general,X9 : general] : (X2 = X8 & ? [X10 : $int,X11 : $int] : (f__integer__($sum(X10,$uminus(X11))) = X9 & f__integer__(X10) = X3 & 1 = X11) & tp(X8,X9))) => tq(X0,X1)))),
% 7.64/2.51 inference(rectify,[],[f22])).
% 7.64/2.51 tff(f36,plain,(
% 7.64/2.51 ~ ! [X0 : general,X1 : general,X2 : general,X3 : general] : (((X0 = X2 & ? [X4 : $int,X5 : $int] : (X1 = f__integer__($sum(X4,X5)) & f__integer__(X4) = X3 & X5 = 1) & ? [X6 : general,X7 : general] : (X6 = X2 & X7 = X3 & hp(X6,X7))) => hq(X0,X1)) & ((X0 = X2 & ? [X8 : $int,X9 : $int] : (f__integer__($sum(X8,X9)) = X1 & f__integer__(X8) = X3 & 1 = X9) & ? [X10 : general,X11 : general] : (X2 = X10 & X3 = X11 & tp(X10,X11))) => tq(X0,X1)))),
% 7.64/2.51 inference(rectify,[],[f20])).
% 7.64/2.51 tff(f49,plain,(
% 7.64/2.51 ! [X0 : general,X1 : general,X2 : general,X3 : general] : ((hq(X0,X1) | (X0 != X2 | X1 != X3 | ! [X4 : general,X5 : general] : (X2 != X4 | ! [X6 : $int,X7 : $int] : (f__integer__($sum(X6,$uminus(X7))) != X5 | f__integer__(X6) != X3 | 1 != X7) | ~hp(X4,X5)))) & (tq(X0,X1) | (X0 != X2 | X1 != X3 | ! [X8 : general,X9 : general] : (X2 != X8 | ! [X10 : $int,X11 : $int] : (f__integer__($sum(X10,$uminus(X11))) != X9 | f__integer__(X10) != X3 | 1 != X11) | ~tp(X8,X9)))))),
% 7.64/2.51 inference(ennf_transformation,[],[f35])).
% 7.64/2.51 tff(f50,plain,(
% 7.64/2.51 ! [X0 : general,X1 : general,X2 : general,X3 : general] : ((hq(X0,X1) | X0 != X2 | X1 != X3 | ! [X4 : general,X5 : general] : (X2 != X4 | ! [X6 : $int,X7 : $int] : (f__integer__($sum(X6,$uminus(X7))) != X5 | f__integer__(X6) != X3 | 1 != X7) | ~hp(X4,X5))) & (tq(X0,X1) | X0 != X2 | X1 != X3 | ! [X8 : general,X9 : general] : (X2 != X8 | ! [X10 : $int,X11 : $int] : (f__integer__($sum(X10,$uminus(X11))) != X9 | f__integer__(X10) != X3 | 1 != X11) | ~tp(X8,X9))))),
% 7.64/2.51 inference(flattening,[],[f49])).
% 7.64/2.51 tff(f51,plain,(
% 7.64/2.51 ? [X0 : general,X1 : general,X2 : general,X3 : general] : ((~hq(X0,X1) & (X0 = X2 & ? [X4 : $int,X5 : $int] : (X1 = f__integer__($sum(X4,X5)) & f__integer__(X4) = X3 & X5 = 1) & ? [X6 : general,X7 : general] : (X6 = X2 & X7 = X3 & hp(X6,X7)))) | (~tq(X0,X1) & (X0 = X2 & ? [X8 : $int,X9 : $int] : (f__integer__($sum(X8,X9)) = X1 & f__integer__(X8) = X3 & 1 = X9) & ? [X10 : general,X11 : general] : (X2 = X10 & X3 = X11 & tp(X10,X11)))))),
% 7.64/2.51 inference(ennf_transformation,[],[f36])).
% 7.64/2.51 tff(f52,plain,(
% 7.64/2.51 ? [X0 : general,X1 : general,X2 : general,X3 : general] : ((~hq(X0,X1) & X0 = X2 & ? [X4 : $int,X5 : $int] : (X1 = f__integer__($sum(X4,X5)) & f__integer__(X4) = X3 & X5 = 1) & ? [X6 : general,X7 : general] : (X6 = X2 & X7 = X3 & hp(X6,X7))) | (~tq(X0,X1) & X0 = X2 & ? [X8 : $int,X9 : $int] : (f__integer__($sum(X8,X9)) = X1 & f__integer__(X8) = X3 & 1 = X9) & ? [X10 : general,X11 : general] : (X2 = X10 & X3 = X11 & tp(X10,X11))))),
% 7.64/2.51 inference(flattening,[],[f51])).
% 7.64/2.51 tff(f53,definition,(
% 7.64/2.51 ! [X1 : general,X0 : general,X2 : general,X3 : general] : ((~tq(X0,X1) & X0 = X2 & ? [X8 : $int,X9 : $int] : (f__integer__($sum(X8,X9)) = X1 & f__integer__(X8) = X3 & 1 = X9) & ? [X10 : general,X11 : general] : (X2 = X10 & X3 = X11 & tp(X10,X11))) | ~ sP0(X1,X0,X2,X3))),
% 7.64/2.51 introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction])).
% 7.64/2.51 tff(f54,plain,(
% 7.64/2.51 ? [X0 : general,X1 : general,X2 : general,X3 : general] : ((~hq(X0,X1) & X0 = X2 & ? [X4 : $int,X5 : $int] : (X1 = f__integer__($sum(X4,X5)) & f__integer__(X4) = X3 & X5 = 1) & ? [X6 : general,X7 : general] : (X6 = X2 & X7 = X3 & hp(X6,X7))) | sP0(X1,X0,X2,X3))),
% 7.64/2.51 inference(definition_folding,[],[f52,f53])).
% 7.64/2.51 tff(f60,plain,(
% 7.64/2.51 ! [X1 : general,X0 : general,X2 : general,X3 : general] : ((~tq(X0,X1) & X0 = X2 & ? [X8 : $int,X9 : $int] : (f__integer__($sum(X8,X9)) = X1 & f__integer__(X8) = X3 & 1 = X9) & ? [X10 : general,X11 : general] : (X2 = X10 & X3 = X11 & tp(X10,X11))) | ~sP0(X1,X0,X2,X3))),
% 7.64/2.51 inference(nnf_transformation,[],[f53])).
% 7.64/2.51 tff(f61,plain,(
% 7.64/2.51 ! [X0 : general,X1 : general,X2 : general,X3 : general] : ((~tq(X1,X0) & X1 = X2 & ? [X4 : $int,X5 : $int] : (f__integer__($sum(X4,X5)) = X0 & f__integer__(X4) = X3 & 1 = X5) & ? [X6 : general,X7 : general] : (X2 = X6 & X3 = X7 & tp(X6,X7))) | ~sP0(X0,X1,X2,X3))),
% 7.64/2.51 inference(rectify,[],[f60])).
% 7.64/2.51 tff(f62,plain,(
% 7.64/2.51 ! [X0 : general,X1 : general,X2 : general,X3 : general] : ((~tq(X1,X0) & X1 = X2 & (f__integer__($sum(sK3(X0,X3),sK4(X0,X3))) = X0 & f__integer__(sK3(X0,X3)) = X3 & 1 = sK4(X0,X3)) & (sK5(X2,X3) = X2 & sK6(X2,X3) = X3 & tp(sK5(X2,X3),sK6(X2,X3)))) | ~sP0(X0,X1,X2,X3))),
% 7.64/2.51 inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4,sK5,sK6]),skolemize(X4,sK3(X0,X3)),skolemize(X5,sK4(X0,X3)),skolemize(X6,sK5(X2,X3)),skolemize(X7,sK6(X2,X3))],[f61])).
% 7.64/2.51 tff(f63,plain,(
% 7.64/2.51 (~hq(sK7,sK8) & sK7 = sK9 & (sK8 = f__integer__($sum(sK11,sK12)) & sK10 = f__integer__(sK11) & 1 = sK12) & (sK9 = sK13 & sK10 = sK14 & hp(sK13,sK14))) | sP0(sK8,sK7,sK9,sK10)),
% 7.64/2.51 inference(skolemize,[status(esa),new_symbols(skolem,[sK7,sK8,sK9,sK10,sK11,sK12,sK13,sK14]),skolemize(X0,sK7),skolemize(X1,sK8),skolemize(X2,sK9),skolemize(X3,sK10),skolemize(X4,sK11),skolemize(X5,sK12),skolemize(X6,sK13),skolemize(X7,sK14)],[f54])).
% 7.64/2.51 tff(f83,plain,(
% 7.64/2.51 ( ! [X2 : general,X3 : general,X10 : $int,X0 : general,X11 : $int,X1 : general,X8 : general,X9 : general] : (tq(X0,X1) | X0 != X2 | X1 != X3 | X2 != X8 | f__integer__($sum(X10,$uminus(X11))) != X9 | f__integer__(X10) != X3 | 1 != X11 | ~tp(X8,X9)) )),
% 7.64/2.51 inference(cnf_transformation,[],[f50])).
% 7.64/2.51 tff(f84,plain,(
% 7.64/2.51 ( ! [X2 : general,X3 : general,X0 : general,X1 : general,X6 : $int,X7 : $int,X4 : general,X5 : general] : (hq(X0,X1) | X0 != X2 | X1 != X3 | X2 != X4 | f__integer__($sum(X6,$uminus(X7))) != X5 | f__integer__(X6) != X3 | 1 != X7 | ~hp(X4,X5)) )),
% 7.64/2.51 inference(cnf_transformation,[],[f50])).
% 7.64/2.51 tff(f85,plain,(
% 7.64/2.51 ( ! [X2 : general,X3 : general,X0 : general,X1 : general] : (~sP0(X0,X1,X2,X3) | tp(sK5(X2,X3),sK6(X2,X3))) )),
% 7.64/2.51 inference(cnf_transformation,[],[f62])).
% 7.64/2.51 tff(f86,plain,(
% 7.64/2.51 ( ! [X2 : general,X3 : general,X0 : general,X1 : general] : (~sP0(X0,X1,X2,X3) | sK6(X2,X3) = X3) )),
% 7.64/2.51 inference(cnf_transformation,[],[f62])).
% 7.64/2.51 tff(f87,plain,(
% 7.64/2.51 ( ! [X2 : general,X3 : general,X0 : general,X1 : general] : (~sP0(X0,X1,X2,X3) | sK5(X2,X3) = X2) )),
% 7.64/2.51 inference(cnf_transformation,[],[f62])).
% 7.64/2.51 tff(f88,plain,(
% 7.64/2.51 ( ! [X2 : general,X3 : general,X0 : general,X1 : general] : (~sP0(X0,X1,X2,X3) | 1 = sK4(X0,X3)) )),
% 7.64/2.51 inference(cnf_transformation,[],[f62])).
% 7.64/2.51 tff(f89,plain,(
% 7.64/2.51 ( ! [X2 : general,X3 : general,X0 : general,X1 : general] : (~sP0(X0,X1,X2,X3) | f__integer__(sK3(X0,X3)) = X3) )),
% 7.64/2.51 inference(cnf_transformation,[],[f62])).
% 7.64/2.51 tff(f90,plain,(
% 7.64/2.51 ( ! [X2 : general,X3 : general,X0 : general,X1 : general] : (~sP0(X0,X1,X2,X3) | f__integer__($sum(sK3(X0,X3),sK4(X0,X3))) = X0) )),
% 7.64/2.51 inference(cnf_transformation,[],[f62])).
% 7.64/2.51 tff(f91,plain,(
% 7.64/2.51 ( ! [X2 : general,X3 : general,X0 : general,X1 : general] : (~sP0(X0,X1,X2,X3) | X1 = X2) )),
% 7.64/2.51 inference(cnf_transformation,[],[f62])).
% 7.64/2.51 tff(f92,plain,(
% 7.64/2.51 ( ! [X2 : general,X3 : general,X0 : general,X1 : general] : (~sP0(X0,X1,X2,X3) | ~tq(X1,X0)) )),
% 7.64/2.51 inference(cnf_transformation,[],[f62])).
% 7.64/2.51 tff(f93,plain,(
% 7.64/2.51 hp(sK13,sK14) | sP0(sK8,sK7,sK9,sK10)),
% 7.64/2.51 inference(cnf_transformation,[],[f63])).
% 7.64/2.51 tff(f94,plain,(
% 7.64/2.51 sK10 = sK14 | sP0(sK8,sK7,sK9,sK10)),
% 7.64/2.51 inference(cnf_transformation,[],[f63])).
% 7.64/2.51 tff(f95,plain,(
% 7.64/2.51 sK9 = sK13 | sP0(sK8,sK7,sK9,sK10)),
% 7.64/2.51 inference(cnf_transformation,[],[f63])).
% 7.64/2.51 tff(f96,plain,(
% 7.64/2.51 1 = sK12 | sP0(sK8,sK7,sK9,sK10)),
% 7.64/2.51 inference(cnf_transformation,[],[f63])).
% 7.64/2.51 tff(f97,plain,(
% 7.64/2.51 sK10 = f__integer__(sK11) | sP0(sK8,sK7,sK9,sK10)),
% 7.64/2.51 inference(cnf_transformation,[],[f63])).
% 7.64/2.51 tff(f98,plain,(
% 7.64/2.51 sK8 = f__integer__($sum(sK11,sK12)) | sP0(sK8,sK7,sK9,sK10)),
% 7.64/2.51 inference(cnf_transformation,[],[f63])).
% 7.64/2.51 tff(f99,plain,(
% 7.64/2.51 sK7 = sK9 | sP0(sK8,sK7,sK9,sK10)),
% 7.64/2.51 inference(cnf_transformation,[],[f63])).
% 7.64/2.51 tff(f100,plain,(
% 7.64/2.51 ~hq(sK7,sK8) | sP0(sK8,sK7,sK9,sK10)),
% 7.64/2.51 inference(cnf_transformation,[],[f63])).
% 7.64/2.51 tff(f104,plain,(
% 7.64/2.51 ( ! [X2 : general,X3 : general,X1 : general,X6 : $int,X7 : $int,X4 : general,X5 : general] : (hq(X2,X1) | X1 != X3 | X2 != X4 | f__integer__($sum(X6,$uminus(X7))) != X5 | f__integer__(X6) != X3 | 1 != X7 | ~hp(X4,X5)) )),
% 7.64/2.51 inference(equality_resolution,[],[f84])).
% 7.64/2.51 tff(f105,plain,(
% 7.64/2.51 ( ! [X2 : general,X3 : general,X6 : $int,X7 : $int,X4 : general,X5 : general] : (hq(X2,X3) | X2 != X4 | f__integer__($sum(X6,$uminus(X7))) != X5 | f__integer__(X6) != X3 | 1 != X7 | ~hp(X4,X5)) )),
% 7.64/2.51 inference(equality_resolution,[],[f104])).
% 7.64/2.51 tff(f106,plain,(
% 7.64/2.51 ( ! [X3 : general,X6 : $int,X7 : $int,X4 : general,X5 : general] : (hq(X4,X3) | f__integer__($sum(X6,$uminus(X7))) != X5 | f__integer__(X6) != X3 | 1 != X7 | ~hp(X4,X5)) )),
% 7.64/2.51 inference(equality_resolution,[],[f105])).
% 7.64/2.51 tff(f107,plain,(
% 7.64/2.51 ( ! [X3 : general,X6 : $int,X7 : $int,X4 : general] : (hq(X4,X3) | f__integer__(X6) != X3 | 1 != X7 | ~hp(X4,f__integer__($sum(X6,$uminus(X7))))) )),
% 7.64/2.51 inference(equality_resolution,[],[f106])).
% 7.64/2.51 tff(f108,plain,(
% 7.64/2.51 ( ! [X6 : $int,X7 : $int,X4 : general] : (hq(X4,f__integer__(X6)) | 1 != X7 | ~hp(X4,f__integer__($sum(X6,$uminus(X7))))) )),
% 7.64/2.51 inference(equality_resolution,[],[f107])).
% 7.64/2.51 tff(f109,plain,(
% 7.64/2.51 ( ! [X6 : $int,X4 : general] : (hq(X4,f__integer__(X6)) | ~hp(X4,f__integer__($sum(X6,$uminus(1))))) )),
% 7.64/2.51 inference(equality_resolution,[],[f108])).
% 7.64/2.51 tff(f110,plain,(
% 7.64/2.51 ( ! [X2 : general,X3 : general,X10 : $int,X11 : $int,X1 : general,X8 : general,X9 : general] : (tq(X2,X1) | X1 != X3 | X2 != X8 | f__integer__($sum(X10,$uminus(X11))) != X9 | f__integer__(X10) != X3 | 1 != X11 | ~tp(X8,X9)) )),
% 7.64/2.51 inference(equality_resolution,[],[f83])).
% 7.64/2.51 tff(f111,plain,(
% 7.64/2.51 ( ! [X2 : general,X3 : general,X10 : $int,X11 : $int,X8 : general,X9 : general] : (tq(X2,X3) | X2 != X8 | f__integer__($sum(X10,$uminus(X11))) != X9 | f__integer__(X10) != X3 | 1 != X11 | ~tp(X8,X9)) )),
% 7.64/2.51 inference(equality_resolution,[],[f110])).
% 7.64/2.51 tff(f112,plain,(
% 7.64/2.51 ( ! [X3 : general,X10 : $int,X11 : $int,X8 : general,X9 : general] : (tq(X8,X3) | f__integer__($sum(X10,$uminus(X11))) != X9 | f__integer__(X10) != X3 | 1 != X11 | ~tp(X8,X9)) )),
% 7.64/2.51 inference(equality_resolution,[],[f111])).
% 7.64/2.51 tff(f113,plain,(
% 7.64/2.51 ( ! [X3 : general,X10 : $int,X11 : $int,X8 : general] : (tq(X8,X3) | f__integer__(X10) != X3 | 1 != X11 | ~tp(X8,f__integer__($sum(X10,$uminus(X11))))) )),
% 7.64/2.51 inference(equality_resolution,[],[f112])).
% 7.64/2.51 tff(f114,plain,(
% 7.64/2.51 ( ! [X10 : $int,X11 : $int,X8 : general] : (tq(X8,f__integer__(X10)) | 1 != X11 | ~tp(X8,f__integer__($sum(X10,$uminus(X11))))) )),
% 7.64/2.51 inference(equality_resolution,[],[f113])).
% 7.64/2.51 tff(f115,plain,(
% 7.64/2.51 ( ! [X10 : $int,X8 : general] : (tq(X8,f__integer__(X10)) | ~tp(X8,f__integer__($sum(X10,$uminus(1))))) )),
% 7.64/2.51 inference(equality_resolution,[],[f114])).
% 7.64/2.51 tff(f116,plain,(
% 7.64/2.51 ( ! [X10 : $int,X8 : general] : (~tp(X8,f__integer__($sum(X10,-1))) | tq(X8,f__integer__(X10))) )),
% 7.64/2.51 inference(evaluation,[],[f115])).
% 7.64/2.51 tff(f117,plain,(
% 7.64/2.51 ( ! [X6 : $int,X4 : general] : (~hp(X4,f__integer__($sum(X6,-1))) | hq(X4,f__integer__(X6))) )),
% 7.64/2.51 inference(evaluation,[],[f109])).
% 7.64/2.51 tff(f119,definition,(
% 7.64/2.51 spl15_1 <=> sP0(sK8,sK7,sK9,sK10)),
% 7.64/2.51 introduced(definition,[new_symbols(definition,[spl15_1])],[avatar_definition])).
% 7.64/2.51 tff(f121,plain,(
% 7.64/2.51 sP0(sK8,sK7,sK9,sK10) | ~spl15_1),
% 7.64/2.51 inference(avatar_component_clause,[],[f119])).
% 7.64/2.51 tff(f123,definition,(
% 7.64/2.51 spl15_2 <=> hp(sK13,sK14)),
% 7.64/2.51 introduced(definition,[new_symbols(definition,[spl15_2])],[avatar_definition])).
% 7.64/2.51 tff(f125,plain,(
% 7.64/2.51 hp(sK13,sK14) | ~spl15_2),
% 7.64/2.51 inference(avatar_component_clause,[],[f123])).
% 7.64/2.51 tff(f126,plain,(
% 7.64/2.51 spl15_1 | spl15_2),
% 7.64/2.51 inference(avatar_split_clause,[],[f93,f123,f119])).
% 7.64/2.51 tff(f128,definition,(
% 7.64/2.51 spl15_3 <=> sK10 = sK14),
% 7.64/2.51 introduced(definition,[new_symbols(definition,[spl15_3])],[avatar_definition])).
% 7.64/2.51 tff(f130,plain,(
% 7.64/2.51 sK10 = sK14 | ~spl15_3),
% 7.64/2.51 inference(avatar_component_clause,[],[f128])).
% 7.64/2.51 tff(f131,plain,(
% 7.64/2.51 spl15_1 | spl15_3),
% 7.64/2.51 inference(avatar_split_clause,[],[f94,f128,f119])).
% 7.64/2.51 tff(f133,definition,(
% 7.64/2.51 spl15_4 <=> sK9 = sK13),
% 7.64/2.51 introduced(definition,[new_symbols(definition,[spl15_4])],[avatar_definition])).
% 7.64/2.51 tff(f135,plain,(
% 7.64/2.51 sK9 = sK13 | ~spl15_4),
% 7.64/2.51 inference(avatar_component_clause,[],[f133])).
% 7.64/2.51 tff(f136,plain,(
% 7.64/2.51 spl15_1 | spl15_4),
% 7.64/2.51 inference(avatar_split_clause,[],[f95,f133,f119])).
% 7.64/2.51 tff(f138,definition,(
% 7.64/2.51 spl15_5 <=> 1 = sK12),
% 7.64/2.51 introduced(definition,[new_symbols(definition,[spl15_5])],[avatar_definition])).
% 7.64/2.51 tff(f140,plain,(
% 7.64/2.51 1 = sK12 | ~spl15_5),
% 7.64/2.51 inference(avatar_component_clause,[],[f138])).
% 7.64/2.51 tff(f141,plain,(
% 7.64/2.51 spl15_1 | spl15_5),
% 7.64/2.51 inference(avatar_split_clause,[],[f96,f138,f119])).
% 7.64/2.51 tff(f143,definition,(
% 7.64/2.51 spl15_6 <=> sK10 = f__integer__(sK11)),
% 7.64/2.51 introduced(definition,[new_symbols(definition,[spl15_6])],[avatar_definition])).
% 7.64/2.51 tff(f145,plain,(
% 7.64/2.51 sK10 = f__integer__(sK11) | ~spl15_6),
% 7.64/2.51 inference(avatar_component_clause,[],[f143])).
% 7.64/2.51 tff(f146,plain,(
% 7.64/2.51 spl15_1 | spl15_6),
% 7.64/2.51 inference(avatar_split_clause,[],[f97,f143,f119])).
% 7.64/2.51 tff(f148,definition,(
% 7.64/2.51 spl15_7 <=> sK8 = f__integer__($sum(sK11,sK12))),
% 7.64/2.51 introduced(definition,[new_symbols(definition,[spl15_7])],[avatar_definition])).
% 7.64/2.51 tff(f150,plain,(
% 7.64/2.51 sK8 = f__integer__($sum(sK11,sK12)) | ~spl15_7),
% 7.64/2.51 inference(avatar_component_clause,[],[f148])).
% 7.64/2.51 tff(f151,plain,(
% 7.64/2.51 spl15_1 | spl15_7),
% 7.64/2.51 inference(avatar_split_clause,[],[f98,f148,f119])).
% 7.64/2.51 tff(f153,definition,(
% 7.64/2.51 spl15_8 <=> sK7 = sK9),
% 7.64/2.51 introduced(definition,[new_symbols(definition,[spl15_8])],[avatar_definition])).
% 7.64/2.51 tff(f154,plain,(
% 7.64/2.51 sK7 != sK9 | spl15_8),
% 7.64/2.51 inference(avatar_component_clause,[],[f153])).
% 7.64/2.51 tff(f155,plain,(
% 7.64/2.51 sK7 = sK9 | ~spl15_8),
% 7.64/2.51 inference(avatar_component_clause,[],[f153])).
% 7.64/2.51 tff(f156,plain,(
% 7.64/2.51 spl15_1 | spl15_8),
% 7.64/2.51 inference(avatar_split_clause,[],[f99,f153,f119])).
% 7.64/2.51 tff(f158,definition,(
% 7.64/2.51 spl15_9 <=> hq(sK7,sK8)),
% 7.64/2.51 introduced(definition,[new_symbols(definition,[spl15_9])],[avatar_definition])).
% 7.64/2.51 tff(f160,plain,(
% 7.64/2.51 ~hq(sK7,sK8) | spl15_9),
% 7.64/2.51 inference(avatar_component_clause,[],[f158])).
% 7.64/2.51 tff(f161,plain,(
% 7.64/2.51 spl15_1 | ~spl15_9),
% 7.64/2.51 inference(avatar_split_clause,[],[f100,f158,f119])).
% 7.64/2.51 tff(f162,plain,(
% 7.64/2.51 hp(sK13,sK10) | (~spl15_2 | ~spl15_3)),
% 7.64/2.51 inference(superposition,[],[f125,f130])).
% 7.64/2.51 tff(f165,plain,(
% 7.64/2.51 hp(sK9,sK10) | (~spl15_2 | ~spl15_3 | ~spl15_4)),
% 7.64/2.51 inference(forward_demodulation,[],[f162,f135])).
% 7.64/2.51 tff(f166,plain,(
% 7.64/2.51 hp(sK7,sK10) | (~spl15_2 | ~spl15_3 | ~spl15_4 | ~spl15_8)),
% 7.64/2.51 inference(forward_demodulation,[],[f165,f155])).
% 7.64/2.51 tff(f168,plain,(
% 7.64/2.51 sP0(sK8,sK7,sK7,sK10) | (~spl15_1 | ~spl15_8)),
% 7.64/2.51 inference(forward_demodulation,[],[f121,f155])).
% 7.64/2.51 tff(f169,plain,(
% 7.64/2.51 sK8 = f__integer__($sum(sK11,1)) | (~spl15_5 | ~spl15_7)),
% 7.64/2.51 inference(forward_demodulation,[],[f150,f140])).
% 7.64/2.51 tff(f266,plain,(
% 7.64/2.51 ~tq(sK7,sK8) | (~spl15_1 | ~spl15_8)),
% 7.64/2.51 inference(resolution,[],[f92,f168])).
% 7.64/2.51 tff(f371,plain,(
% 7.64/2.51 sK10 = sK6(sK7,sK10) | (~spl15_1 | ~spl15_8)),
% 7.64/2.51 inference(resolution,[],[f86,f168])).
% 7.64/2.51 tff(f374,plain,(
% 7.64/2.51 sK7 = sK5(sK7,sK10) | (~spl15_1 | ~spl15_8)),
% 7.64/2.51 inference(resolution,[],[f87,f168])).
% 7.64/2.51 tff(f377,plain,(
% 7.64/2.51 1 = sK4(sK8,sK10) | (~spl15_1 | ~spl15_8)),
% 7.64/2.51 inference(resolution,[],[f88,f168])).
% 7.64/2.51 tff(f381,plain,(
% 7.64/2.51 ( ! [X0 : $int,X1 : general] : (~tp(X1,f__integer__($sum(-1,X0))) | tq(X1,f__integer__(X0))) )),
% 7.64/2.51 inference(superposition,[],[f116,f23])).
% 7.64/2.51 tff(f383,plain,(
% 7.64/2.51 ( ! [X0 : $int,X1 : general] : (~hp(X1,f__integer__($sum(-1,X0))) | hq(X1,f__integer__(X0))) )),
% 7.64/2.51 inference(superposition,[],[f117,f23])).
% 7.64/2.51 tff(f386,plain,(
% 7.64/2.51 ( ! [X0 : $int,X1 : $int] : ($sum(0,X1) = $sum(X0,$sum($uminus(X0),X1))) )),
% 7.64/2.51 inference(superposition,[],[f24,f27])).
% 7.64/2.51 tff(f406,plain,(
% 7.64/2.51 ( ! [X0 : $int,X1 : $int] : ($sum(X0,$sum($uminus(X0),X1)) = X1) )),
% 7.64/2.51 inference(evaluation,[],[f386])).
% 7.64/2.51 tff(f425,plain,(
% 7.64/2.51 tp(sK5(sK7,sK10),sK6(sK7,sK10)) | (~spl15_1 | ~spl15_8)),
% 7.64/2.51 inference(resolution,[],[f85,f168])).
% 7.64/2.51 tff(f630,plain,(
% 7.64/2.51 tp(sK5(sK7,sK10),sK10) | (~spl15_1 | ~spl15_8)),
% 7.64/2.51 inference(forward_demodulation,[],[f425,f371])).
% 7.64/2.51 tff(f631,plain,(
% 7.64/2.51 tp(sK7,sK10) | (~spl15_1 | ~spl15_8)),
% 7.64/2.51 inference(forward_demodulation,[],[f630,f374])).
% 7.64/2.51 tff(f1004,plain,(
% 7.64/2.51 ( ! [X0 : $int,X1 : general] : (~tp(X1,f__integer__(X0)) | tq(X1,f__integer__($sum($uminus(-1),X0)))) )),
% 7.64/2.51 inference(superposition,[],[f381,f406])).
% 7.64/2.51 tff(f1008,plain,(
% 7.64/2.51 ( ! [X0 : $int,X1 : general] : (tq(X1,f__integer__($sum(1,X0))) | ~tp(X1,f__integer__(X0))) )),
% 7.64/2.51 inference(evaluation,[],[f1004])).
% 7.64/2.51 tff(f1024,plain,(
% 7.64/2.51 ( ! [X0 : $int,X1 : general] : (~hp(X1,f__integer__(X0)) | hq(X1,f__integer__($sum($uminus(-1),X0)))) )),
% 7.64/2.51 inference(superposition,[],[f383,f406])).
% 7.64/2.51 tff(f1028,plain,(
% 7.64/2.51 ( ! [X0 : $int,X1 : general] : (hq(X1,f__integer__($sum(1,X0))) | ~hp(X1,f__integer__(X0))) )),
% 7.64/2.51 inference(evaluation,[],[f1024])).
% 7.64/2.51 tff(f5540,plain,(
% 7.64/2.51 sK7 = sK9 | ~spl15_1),
% 7.64/2.51 inference(resolution,[],[f121,f91])).
% 7.64/2.51 tff(f5542,plain,(
% 7.64/2.51 $false | (~spl15_1 | spl15_8)),
% 7.64/2.51 inference(forward_subsumption_resolution,[],[f5540,f154])).
% 7.64/2.51 tff(f5543,plain,(
% 7.64/2.51 ~spl15_1 | spl15_8),
% 7.64/2.51 inference(avatar_contradiction_clause,[],[f5542])).
% 7.64/2.51 tff(f6028,plain,(
% 7.64/2.51 sK8 = f__integer__($sum(1,sK11)) | (~spl15_5 | ~spl15_7)),
% 7.64/2.51 inference(forward_demodulation,[],[f169,f23])).
% 7.64/2.51 tff(f6668,plain,(
% 7.64/2.51 ( ! [X0 : general] : (hq(X0,sK8) | ~hp(X0,f__integer__(sK11))) ) | (~spl15_5 | ~spl15_7)),
% 7.64/2.51 inference(superposition,[],[f1028,f6028])).
% 7.64/2.51 tff(f6672,plain,(
% 7.64/2.51 ( ! [X0 : general] : (~hp(X0,sK10) | hq(X0,sK8)) ) | (~spl15_5 | ~spl15_6 | ~spl15_7)),
% 7.64/2.51 inference(forward_demodulation,[],[f6668,f145])).
% 7.64/2.51 tff(f6775,plain,(
% 7.64/2.51 hq(sK7,sK8) | (~spl15_2 | ~spl15_3 | ~spl15_4 | ~spl15_5 | ~spl15_6 | ~spl15_7 | ~spl15_8)),
% 7.64/2.51 inference(resolution,[],[f6672,f166])).
% 7.64/2.51 tff(f6776,plain,(
% 7.64/2.51 $false | (~spl15_2 | ~spl15_3 | ~spl15_4 | ~spl15_5 | ~spl15_6 | ~spl15_7 | ~spl15_8 | spl15_9)),
% 7.64/2.51 inference(forward_subsumption_resolution,[],[f6775,f160])).
% 7.64/2.51 tff(f6777,plain,(
% 7.64/2.51 ~spl15_2 | ~spl15_3 | ~spl15_4 | ~spl15_5 | ~spl15_6 | ~spl15_7 | ~spl15_8 | spl15_9),
% 7.64/2.51 inference(avatar_contradiction_clause,[],[f6776])).
% 7.64/2.51 tff(f6841,plain,(
% 7.64/2.51 sK10 = f__integer__(sK3(sK8,sK10)) | (~spl15_1 | ~spl15_8)),
% 7.64/2.51 inference(resolution,[],[f168,f89])).
% 7.64/2.51 tff(f6842,plain,(
% 7.64/2.51 sK8 = f__integer__($sum(sK3(sK8,sK10),sK4(sK8,sK10))) | (~spl15_1 | ~spl15_8)),
% 7.64/2.51 inference(resolution,[],[f168,f90])).
% 7.64/2.51 tff(f7107,plain,(
% 7.64/2.51 sK8 = f__integer__($sum(sK3(sK8,sK10),1)) | (~spl15_1 | ~spl15_8)),
% 7.64/2.51 inference(forward_demodulation,[],[f6842,f377])).
% 7.64/2.51 tff(f7108,plain,(
% 7.64/2.51 sK8 = f__integer__($sum(1,sK3(sK8,sK10))) | (~spl15_1 | ~spl15_8)),
% 7.64/2.51 inference(forward_demodulation,[],[f7107,f23])).
% 7.64/2.51 tff(f7121,plain,(
% 7.64/2.51 ( ! [X0 : general] : (tq(X0,sK8) | ~tp(X0,f__integer__(sK3(sK8,sK10)))) ) | (~spl15_1 | ~spl15_8)),
% 7.64/2.51 inference(superposition,[],[f1008,f7108])).
% 7.64/2.51 tff(f7147,plain,(
% 7.64/2.51 ( ! [X0 : general] : (~tp(X0,sK10) | tq(X0,sK8)) ) | (~spl15_1 | ~spl15_8)),
% 7.64/2.51 inference(forward_demodulation,[],[f7121,f6841])).
% 7.64/2.51 tff(f9318,plain,(
% 7.64/2.51 tq(sK7,sK8) | (~spl15_1 | ~spl15_8)),
% 7.64/2.51 inference(resolution,[],[f7147,f631])).
% 7.64/2.51 tff(f9319,plain,(
% 7.64/2.51 $false | (~spl15_1 | ~spl15_8)),
% 7.64/2.51 inference(forward_subsumption_resolution,[],[f9318,f266])).
% 7.64/2.51 tff(f9320,plain,(
% 7.64/2.51 ~spl15_1 | ~spl15_8),
% 7.64/2.51 inference(avatar_contradiction_clause,[],[f9319])).
% 7.64/2.51 cnf(s1, plain, spl15_1 | spl15_2, inference(sat_conversion,[],[f126])).
% 7.64/2.51 cnf(s2, plain, spl15_1 | spl15_3, inference(sat_conversion,[],[f131])).
% 7.64/2.51 cnf(s3, plain, spl15_1 | spl15_4, inference(sat_conversion,[],[f136])).
% 7.64/2.51 cnf(s4, plain, spl15_1 | spl15_5, inference(sat_conversion,[],[f141])).
% 7.64/2.51 cnf(s5, plain, spl15_1 | spl15_6, inference(sat_conversion,[],[f146])).
% 7.64/2.51 cnf(s6, plain, spl15_1 | spl15_7, inference(sat_conversion,[],[f151])).
% 7.64/2.51 cnf(s7, plain, spl15_1 | spl15_8, inference(sat_conversion,[],[f156])).
% 7.64/2.51 cnf(s8, plain, spl15_1 | ~spl15_9, inference(sat_conversion,[],[f161])).
% 7.64/2.51 cnf(s116, plain, ~spl15_1 | spl15_8, inference(sat_conversion,[],[f5543])).
% 7.64/2.51 cnf(s294, plain, ~spl15_2 | ~spl15_3 | ~spl15_4 | ~spl15_5 | ~spl15_6 | ~spl15_7 | ~spl15_8 | spl15_9, inference(sat_conversion,[],[f6777])).
% 7.64/2.51 cnf(s657, plain, ~spl15_1 | ~spl15_8, inference(sat_conversion,[],[f9320])).
% 7.64/2.51 cnf(s675, plain, spl15_1, inference(rat,[],[s294,s1,s2,s3,s4,s5,s6,s7,s8])).
% 7.64/2.51 cnf(s676, plain, ~spl15_8, inference(rat,[],[s657,s675])).
% 7.64/2.51 cnf(s677, plain, $false, inference(rat,[],[s116,s676,s675])).
% 7.64/2.51 tff(f9321,plain,(
% 7.64/2.51 $false),
% 7.64/2.51 inference(avatar_sat_refutation,[],[s677])).
% 7.64/2.51 % SZS output end Proof for theBenchmark
% 7.64/2.51 % (2696118)------------------------------
% 7.64/2.51 % (2696118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.64/2.51 % (2696118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.64/2.51 % (2696118)CaDiCaL version: 2.1.3
% 7.64/2.51 % (2696118)Termination reason: Refutation
% 7.64/2.51 % (2696118)Time elapsed: 0.302 s
% 7.64/2.51 % (2696118)Peak memory usage: 15 MB
% 7.64/2.51 % (2696118)Instructions burned: 351 (million)
% 7.64/2.51 % (2696055)Success in time 2.2 s
% 7.64/2.51 % Vampire exiting
%------------------------------------------------------------------------------