%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWX087_1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:46:28 PM UTC 2026
% Result : Theorem 12.88s 2.11s
% Output : Refutation 12.88s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX087_1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 % Computer : n013.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 15:00:06 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.21 Running first-order model finding
% 0.09/0.21 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
% 3.40/0.76 % (1246339)Will run a generic schedule for satisfiability detection.
% 3.40/0.76 % (1246345)% WARNING: option uhcvi not known.
% 3.40/0.76 % (1246345)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3276791511:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 3.40/0.76 % (1246344)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2080303717_2999 on theBenchmark for (2999ds/0Mi)
% 3.40/0.76 % (1246346)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2423603627:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 3.40/0.76 % (1246347)dis+10_1_sil=32000:sp=arity:random_seed=131070410:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 3.40/0.76 % (1246348)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4206958747:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 3.40/0.76 % (1246350)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=946775416:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 3.40/0.76 % (1246349)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1540536919:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 3.40/0.76 % (1246344)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 3.40/0.76 % (1246344)Terminated due to inappropriate strategy.
% 3.40/0.76 % (1246344)------------------------------
% 3.40/0.76 % (1246344)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.40/0.76 % (1246344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.40/0.76 % (1246344)CaDiCaL version: 2.1.3
% 3.40/0.76 % (1246344)Termination reason: Inappropriate
% 3.40/0.76 % (1246344)Time elapsed: 0.003 s
% 3.40/0.76 % (1246344)Peak memory usage: 11 MB
% 3.40/0.76 % (1246344)Instructions burned: 4 (million)
% 3.40/0.76 % (1246344)------------------------------
% 3.40/0.76 % (1246344)------------------------------
% 3.40/0.76 % (1246358)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3916453625:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 3.40/0.76 % (1246358)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 3.40/0.76 % (1246358)Terminated due to inappropriate strategy.
% 3.40/0.76 % (1246358)------------------------------
% 3.40/0.76 % (1246358)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.40/0.76 % (1246358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.40/0.76 % (1246358)CaDiCaL version: 2.1.3
% 3.40/0.76 % (1246358)Termination reason: Inappropriate
% 3.40/0.76 % (1246358)Time elapsed: 0.002 s
% 3.40/0.76 % (1246358)Peak memory usage: 11 MB
% 3.40/0.76 % (1246358)Instructions burned: 3 (million)
% 3.40/0.76 % (1246358)------------------------------
% 3.40/0.76 % (1246358)------------------------------
% 3.40/0.76 % (1246360)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3186425666:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 3.40/0.76 % (1246347)Instruction limit reached!
% 3.40/0.76 % (1246347)------------------------------
% 3.40/0.76 % (1246347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.40/0.76 % (1246347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.40/0.76 % (1246347)CaDiCaL version: 2.1.3
% 3.40/0.76 % (1246347)Termination reason: Instruction limit
% 3.40/0.76 % (1246347)Termination phase: Saturation
% 3.40/0.76 % (1246347)Time elapsed: 0.067 s
% 3.40/0.76 % (1246347)Peak memory usage: 13 MB
% 3.40/0.76 % (1246347)Instructions burned: 104 (million)
% 3.40/0.76 % (1246348)Instruction limit reached!
% 3.40/0.76 % (1246348)------------------------------
% 3.40/0.76 % (1246348)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.40/0.76 % (1246348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.40/0.76 % (1246348)CaDiCaL version: 2.1.3
% 3.40/0.76 % (1246348)Termination reason: Instruction limit
% 3.40/0.76 % (1246348)Termination phase: Saturation
% 3.40/0.76 % (1246348)Time elapsed: 0.070 s
% 3.40/0.76 % (1246348)Peak memory usage: 12 MB
% 3.40/0.76 % (1246348)Instructions burned: 117 (million)
% 3.40/0.76 % (1246349)Instruction limit reached!
% 3.40/0.76 % (1246349)------------------------------
% 3.40/0.76 % (1246349)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.40/0.76 % (1246349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.40/0.76 % (1246349)CaDiCaL version: 2.1.3
% 3.40/0.76 % (1246349)Termination reason: Instruction limit
% 6.52/1.15 % (1246349)Termination phase: Saturation
% 6.52/1.15 % (1246349)Time elapsed: 0.086 s
% 6.52/1.15 % (1246349)Peak memory usage: 13 MB
% 6.52/1.15 % (1246349)Instructions burned: 132 (million)
% 6.52/1.15 % (1246362)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=2999147801:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 6.52/1.15 % (1246363)ott-21_1_sil=16000:fs=off:random_seed=4083317143:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 6.52/1.15 % (1246365)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2515805993:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 6.52/1.15 % (1246350)Instruction limit reached!
% 6.52/1.15 % (1246350)------------------------------
% 6.52/1.15 % (1246350)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.52/1.15 % (1246350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.52/1.15 % (1246350)CaDiCaL version: 2.1.3
% 6.52/1.15 % (1246350)Termination reason: Instruction limit
% 6.52/1.15 % (1246350)Termination phase: Saturation
% 6.52/1.15 % (1246350)Time elapsed: 0.108 s
% 6.52/1.15 % (1246350)Peak memory usage: 14 MB
% 6.52/1.15 % (1246350)Instructions burned: 159 (million)
% 6.52/1.15 % (1246368)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1306380625:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 6.52/1.15 % (1246368)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.52/1.15 % (1246368)Terminated due to inappropriate strategy.
% 6.52/1.15 % (1246368)------------------------------
% 6.52/1.15 % (1246368)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.52/1.15 % (1246368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.52/1.15 % (1246368)CaDiCaL version: 2.1.3
% 6.52/1.15 % (1246368)Termination reason: Inappropriate
% 6.52/1.15 % (1246368)Time elapsed: 0.002 s
% 6.52/1.15 % (1246368)Peak memory usage: 10 MB
% 6.52/1.15 % (1246368)Instructions burned: 3 (million)
% 6.52/1.15 % (1246368)------------------------------
% 6.52/1.15 % (1246368)------------------------------
% 6.52/1.15 % (1246360)Instruction limit reached!
% 6.52/1.15 % (1246360)------------------------------
% 6.52/1.15 % (1246360)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.52/1.15 % (1246360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.52/1.15 % (1246360)CaDiCaL version: 2.1.3
% 6.52/1.15 % (1246360)Termination reason: Instruction limit
% 6.52/1.15 % (1246360)Termination phase: Saturation
% 6.52/1.15 % (1246360)Time elapsed: 0.087 s
% 6.52/1.15 % (1246360)Peak memory usage: 13 MB
% 6.52/1.15 % (1246360)Instructions burned: 131 (million)
% 6.52/1.15 % (1246370)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1808862384:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 6.52/1.15 % (1246371)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3950563125:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 6.52/1.15 % (1246371)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.52/1.15 % (1246371)Terminated due to inappropriate strategy.
% 6.52/1.15 % (1246371)------------------------------
% 6.52/1.15 % (1246371)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.52/1.15 % (1246371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.52/1.15 % (1246371)CaDiCaL version: 2.1.3
% 6.52/1.15 % (1246371)Termination reason: Inappropriate
% 6.52/1.15 % (1246371)Time elapsed: 0.002 s
% 6.52/1.15 % (1246371)Peak memory usage: 10 MB
% 6.52/1.15 % (1246371)Instructions burned: 3 (million)
% 6.52/1.15 % (1246371)------------------------------
% 6.52/1.15 % (1246371)------------------------------
% 6.52/1.15 % (1246363)Instruction limit reached!
% 6.52/1.15 % (1246363)------------------------------
% 6.52/1.15 % (1246363)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.52/1.15 % (1246363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.52/1.15 % (1246363)CaDiCaL version: 2.1.3
% 6.52/1.15 % (1246363)Termination reason: Instruction limit
% 6.52/1.15 % (1246363)Termination phase: Saturation
% 6.52/1.15 % (1246363)Time elapsed: 0.081 s
% 6.52/1.15 % (1246363)Peak memory usage: 12 MB
% 6.52/1.15 % (1246363)Instructions burned: 181 (million)
% 6.52/1.15 % (1246374)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=1198575879: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)
% 12.88/2.11 % (1246375)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4173587690:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 12.88/2.11 % (1246365)Instruction limit reached!
% 12.88/2.11 % (1246365)------------------------------
% 12.88/2.11 % (1246365)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.88/2.11 % (1246365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.88/2.11 % (1246365)CaDiCaL version: 2.1.3
% 12.88/2.11 % (1246365)Termination reason: Instruction limit
% 12.88/2.11 % (1246365)Termination phase: Saturation
% 12.88/2.11 % (1246365)Time elapsed: 0.296 s
% 12.88/2.11 % (1246365)Peak memory usage: 14 MB
% 12.88/2.11 % (1246365)Instructions burned: 478 (million)
% 12.88/2.11 % (1246378)fmb+10_1_sil=64000:random_seed=282068216:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi)
% 12.88/2.11 % (1246378)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 12.88/2.11 % (1246378)Terminated due to inappropriate strategy.
% 12.88/2.11 % (1246378)------------------------------
% 12.88/2.11 % (1246378)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.88/2.11 % (1246378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.88/2.11 % (1246378)CaDiCaL version: 2.1.3
% 12.88/2.11 % (1246378)Termination reason: Inappropriate
% 12.88/2.11 % (1246378)Time elapsed: 0.002 s
% 12.88/2.11 % (1246378)Peak memory usage: 10 MB
% 12.88/2.11 % (1246378)Instructions burned: 4 (million)
% 12.88/2.11 % (1246378)------------------------------
% 12.88/2.11 % (1246378)------------------------------
% 12.88/2.11 % (1246380)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1773176565:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi)
% 12.88/2.11 % (1246380)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 12.88/2.11 % (1246380)Terminated due to inappropriate strategy.
% 12.88/2.11 % (1246380)------------------------------
% 12.88/2.11 % (1246380)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.88/2.11 % (1246380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.88/2.11 % (1246380)CaDiCaL version: 2.1.3
% 12.88/2.11 % (1246380)Termination reason: Inappropriate
% 12.88/2.11 % (1246380)Time elapsed: 0.002 s
% 12.88/2.11 % (1246380)Peak memory usage: 10 MB
% 12.88/2.11 % (1246380)Instructions burned: 3 (million)
% 12.88/2.11 % (1246380)------------------------------
% 12.88/2.11 % (1246380)------------------------------
% 12.88/2.11 % (1246382)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2761289749:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi)
% 12.88/2.11 % (1246382)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 12.88/2.11 % (1246382)Terminated due to inappropriate strategy.
% 12.88/2.11 % (1246382)------------------------------
% 12.88/2.11 % (1246382)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.88/2.11 % (1246382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.88/2.11 % (1246382)CaDiCaL version: 2.1.3
% 12.88/2.11 % (1246382)Termination reason: Inappropriate
% 12.88/2.11 % (1246382)Time elapsed: 0.002 s
% 12.88/2.11 % (1246382)Peak memory usage: 10 MB
% 12.88/2.11 % (1246382)Instructions burned: 3 (million)
% 12.88/2.11 % (1246382)------------------------------
% 12.88/2.11 % (1246382)------------------------------
% 12.88/2.11 % (1246362)Instruction limit reached!
% 12.88/2.11 % (1246362)------------------------------
% 12.88/2.11 % (1246362)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.88/2.11 % (1246362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.88/2.11 % (1246362)CaDiCaL version: 2.1.3
% 12.88/2.11 % (1246362)Termination reason: Instruction limit
% 12.88/2.11 % (1246362)Termination phase: Saturation
% 12.88/2.11 % (1246362)Time elapsed: 0.401 s
% 12.88/2.11 % (1246362)Peak memory usage: 18 MB
% 12.88/2.11 % (1246362)Instructions burned: 684 (million)
% 12.88/2.11 % (1246384)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1285557695:i=5131_2994 on theBenchmark for (2994ds/5131Mi)
% 12.88/2.11 % (1246385)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4274762067:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi)
% 12.88/2.11 % (1246374)Instruction limit reached!
% 12.88/2.11 % (1246374)------------------------------
% 12.88/2.11 % (1246374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.88/2.11 % (1246374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.88/2.11 % (1246374)CaDiCaL version: 2.1.3
% 12.88/2.11 % (1246374)Termination reason: Instruction limit
% 12.88/2.11 % (1246374)Termination phase: Saturation
% 12.88/2.11 % (1246374)Time elapsed: 0.339 s
% 12.88/2.11 % (1246374)Peak memory usage: 16 MB
% 12.88/2.11 % (1246374)Instructions burned: 693 (million)
% 12.88/2.11 % (1246388)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3649369177:i=6324_2994 on theBenchmark for (2994ds/6324Mi)
% 12.88/2.11 % (1246388)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 12.88/2.11 % (1246388)Terminated due to inappropriate strategy.
% 12.88/2.11 % (1246388)------------------------------
% 12.88/2.11 % (1246388)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.88/2.11 % (1246388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.88/2.11 % (1246388)CaDiCaL version: 2.1.3
% 12.88/2.11 % (1246388)Termination reason: Inappropriate
% 12.88/2.11 % (1246388)Time elapsed: 0.003 s
% 12.88/2.11 % (1246388)Peak memory usage: 11 MB
% 12.88/2.11 % (1246388)Instructions burned: 4 (million)
% 12.88/2.11 % (1246388)------------------------------
% 12.88/2.11 % (1246388)------------------------------
% 12.88/2.11 % (1246390)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3370919603:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi)
% 12.88/2.11 % (1246390)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 12.88/2.11 % (1246390)Terminated due to inappropriate strategy.
% 12.88/2.11 % (1246390)------------------------------
% 12.88/2.11 % (1246390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.88/2.11 % (1246390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.88/2.11 % (1246390)CaDiCaL version: 2.1.3
% 12.88/2.11 % (1246390)Termination reason: Inappropriate
% 12.88/2.11 % (1246390)Time elapsed: 0.002 s
% 12.88/2.11 % (1246390)Peak memory usage: 10 MB
% 12.88/2.11 % (1246390)Instructions burned: 3 (million)
% 12.88/2.11 % (1246390)------------------------------
% 12.88/2.11 % (1246390)------------------------------
% 12.88/2.11 % (1246392)ott-2_1_sil=16000:newcnf=on:random_seed=3496941353:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi)
% 12.88/2.11 % (1246375)Instruction limit reached!
% 12.88/2.11 % (1246375)------------------------------
% 12.88/2.11 % (1246375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.88/2.11 % (1246375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.88/2.11 % (1246375)CaDiCaL version: 2.1.3
% 12.88/2.11 % (1246375)Termination reason: Instruction limit
% 12.88/2.11 % (1246375)Termination phase: Saturation
% 12.88/2.11 % (1246375)Time elapsed: 0.524 s
% 12.88/2.11 % (1246375)Peak memory usage: 20 MB
% 12.88/2.11 % (1246375)Instructions burned: 880 (million)
% 12.88/2.11 % (1246394)ott+10_1_sil=32000:tgt=ground:random_seed=2206595668:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi)
% 12.88/2.11 % (1246370)Instruction limit reached!
% 12.88/2.11 % (1246370)------------------------------
% 12.88/2.11 % (1246370)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.88/2.11 % (1246370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.88/2.11 % (1246370)CaDiCaL version: 2.1.3
% 12.88/2.11 % (1246370)Termination reason: Instruction limit
% 12.88/2.11 % (1246370)Termination phase: Saturation
% 12.88/2.11 % (1246370)Time elapsed: 0.722 s
% 12.88/2.11 % (1246370)Peak memory usage: 18 MB
% 12.88/2.11 % (1246370)Instructions burned: 1180 (million)
% 12.88/2.11 % (1246396)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3872449656:i=54282_2990 on theBenchmark for (2990ds/54282Mi)
% 12.88/2.11 % (1246396)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 12.88/2.11 % (1246396)Terminated due to inappropriate strategy.
% 12.88/2.11 % (1246396)------------------------------
% 12.88/2.11 % (1246396)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.88/2.11 % (1246396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.88/2.11 % (1246396)CaDiCaL version: 2.1.3
% 12.88/2.11 % (1246396)Termination reason: Inappropriate
% 12.88/2.11 % (1246396)Time elapsed: 0.003 s
% 12.88/2.11 % (1246396)Peak memory usage: 11 MB
% 12.88/2.11 % (1246396)Instructions burned: 4 (million)
% 12.88/2.11 % (1246396)------------------------------
% 12.88/2.11 % (1246396)------------------------------
% 12.88/2.11 % (1246398)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3768198882:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi)
% 12.88/2.11 % (1246392)Instruction limit reached!
% 12.88/2.11 % (1246392)------------------------------
% 12.88/2.11 % (1246392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.88/2.11 % (1246392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.88/2.11 % (1246392)CaDiCaL version: 2.1.3
% 12.88/2.11 % (1246392)Termination reason: Instruction limit
% 12.88/2.11 % (1246392)Termination phase: Saturation
% 12.88/2.11 % (1246392)Time elapsed: 0.471 s
% 12.88/2.11 % (1246392)Peak memory usage: 17 MB
% 12.88/2.11 % (1246392)Instructions burned: 870 (million)
% 12.88/2.11 % (1246400)dis+21_1_sil=32000:sas=cadical:random_seed=1265001552:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi)
% 12.88/2.11 % (1246385)Instruction limit reached!
% 12.88/2.11 % (1246385)------------------------------
% 12.88/2.11 % (1246385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.88/2.11 % (1246385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.88/2.11 % (1246385)CaDiCaL version: 2.1.3
% 12.88/2.11 % (1246385)Termination reason: Instruction limit
% 12.88/2.11 % (1246385)Termination phase: Saturation
% 12.88/2.11 % (1246385)Time elapsed: 0.776 s
% 12.88/2.11 % (1246385)Peak memory usage: 24 MB
% 12.88/2.11 % (1246385)Instructions burned: 1473 (million)
% 12.88/2.11 % (1246402)ott+11_1_sil=16000:gs=on:random_seed=1031796656:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2986 on theBenchmark for (2986ds/2251Mi)
% 12.88/2.11 % (1246345) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1246339-1246345"...
% 12.88/2.11 % (1246345)...printing done.
% 12.88/2.11 % (1246345)Refutation found. Thanks to Tanya!
% 12.88/2.11 % SZS status Theorem for theBenchmark
% 12.88/2.11 % SZS output start Proof for theBenchmark
% 12.88/2.11 tff(type_def_5, type, general: $tType).
% 12.88/2.11 tff(type_def_6, type, symbol: $tType).
% 12.88/2.11 tff(func_def_0, type, f__integer__: $int > general).
% 12.88/2.11 tff(func_def_1, type, f__symbolic__: symbol > general).
% 12.88/2.11 tff(func_def_2, type, c__infimum__: general).
% 12.88/2.11 tff(func_def_3, type, c__supremum__: general).
% 12.88/2.11 tff(func_def_4, type, h_i: $int).
% 12.88/2.11 tff(func_def_10, type, sK0: general > $int).
% 12.88/2.11 tff(func_def_11, type, sK1: general > symbol).
% 12.88/2.11 tff(func_def_12, type, sK2: (general * general) > general).
% 12.88/2.11 tff(func_def_13, type, sK3: (general * general) > general).
% 12.88/2.11 tff(func_def_14, type, sK4: (general * general) > general).
% 12.88/2.11 tff(func_def_15, type, sK5: (general * general) > general).
% 12.88/2.11 tff(func_def_16, type, sK6: (general * general) > general).
% 12.88/2.11 tff(func_def_17, type, sK7: (general * general) > general).
% 12.88/2.11 tff(func_def_18, type, sK8: (general * general * general) > general).
% 12.88/2.11 tff(func_def_19, type, sK9: (general * general * general) > general).
% 12.88/2.11 tff(func_def_20, type, sK10: (general * general * general) > general).
% 12.88/2.11 tff(func_def_21, type, sK11: (general * general * general) > general).
% 12.88/2.11 tff(func_def_22, type, sK12: (general * general * general) > general).
% 12.88/2.11 tff(func_def_23, type, sK13: (general * general * general) > general).
% 12.88/2.11 tff(func_def_24, type, sK14: (general * general * general) > general).
% 12.88/2.11 tff(func_def_25, type, sK15: (general * general * general) > general).
% 12.88/2.11 tff(func_def_26, type, sK17: (general * general * general) > general).
% 12.88/2.11 tff(func_def_27, type, sK18: (general * general * general) > general).
% 12.88/2.11 tff(func_def_28, type, sK19: (general * general * general) > general).
% 12.88/2.11 tff(func_def_29, type, sK20: (general * general * general) > general).
% 12.88/2.11 tff(func_def_30, type, sK21: (general * general * general) > general).
% 12.88/2.11 tff(func_def_31, type, sK22: (general * general * general) > $int).
% 12.88/2.11 tff(func_def_32, type, sK23: (general * general * general) > $int).
% 12.88/2.11 tff(func_def_33, type, sK24: (general * general * general) > general).
% 12.88/2.11 tff(func_def_34, type, sK25: (general * general * general) > general).
% 12.88/2.11 tff(func_def_35, type, sK26: (general * general * general) > general).
% 12.88/2.11 tff(func_def_36, type, sK27: (general * general * general) > $int).
% 12.88/2.11 tff(func_def_37, type, sK28: (general * general * general) > $int).
% 12.88/2.11 tff(func_def_38, type, sK31: (general * general) > general).
% 12.88/2.11 tff(func_def_39, type, sK32: (general * general) > general).
% 12.88/2.11 tff(func_def_40, type, sK33: (general * general * general) > $int).
% 12.88/2.11 tff(func_def_41, type, sK34: (general * general * general) > $int).
% 12.88/2.11 tff(func_def_42, type, sK35: (general * general * general) > $int).
% 12.88/2.11 tff(func_def_43, type, sK36: (general * general * general) > $int).
% 12.88/2.11 tff(func_def_44, type, sK37: (general * general * general) > $int).
% 12.88/2.11 tff(func_def_45, type, sK38: general).
% 12.88/2.11 tff(func_def_46, type, sK39: general).
% 12.88/2.11 tff(pred_def_1, type, p__is_integer__: general > $o).
% 12.88/2.11 tff(pred_def_2, type, p__is_symbolic__: general > $o).
% 12.88/2.11 tff(pred_def_3, type, p__less_equal__: (general * general) > $o).
% 12.88/2.11 tff(pred_def_4, type, p__less__: (general * general) > $o).
% 12.88/2.11 tff(pred_def_5, type, p__greater_equal__: (general * general) > $o).
% 12.88/2.11 tff(pred_def_6, type, p__greater__: (general * general) > $o).
% 12.88/2.11 tff(pred_def_8, type, in0: (general * general) > $o).
% 12.88/2.11 tff(pred_def_9, type, person: general > $o).
% 12.88/2.11 tff(pred_def_10, type, goto: (general * general * general) > $o).
% 12.88/2.11 tff(pred_def_11, type, go: (general * general) > $o).
% 12.88/2.11 tff(pred_def_12, type, in_building: (general * general) > $o).
% 12.88/2.11 tff(pred_def_13, type, in: (general * general * general) > $o).
% 12.88/2.11 tff(pred_def_14, type, in_building_p: (general * general) > $o).
% 12.88/2.11 tff(pred_def_17, type, sP16: (general * general * general * general * general) > $o).
% 12.88/2.11 tff(pred_def_18, type, sP29: (general * general * general * general * general * general) > $o).
% 12.88/2.11 tff(pred_def_19, type, sP30: ($int * $int * general * general) > $o).
% 12.88/2.11 tff(f6,axiom,(
% 12.88/2.11 ! [X0 : $int,X1 : $int] : (p__less_equal__(f__integer__(X0),f__integer__(X1)) <=> $lesseq(X0,X1))),
% 12.88/2.11 file('/export/starexec/sandbox/benchmark/Axioms/SWV014_0.ax',numeral_ordering_ax)).
% 12.88/2.11 tff(f7,axiom,(
% 12.88/2.11 ! [X0 : general,X1 : general] : ((p__less_equal__(X0,X1) & p__less_equal__(X1,X0)) => X0 = X1)),
% 12.88/2.11 file('/export/starexec/sandbox/benchmark/Axioms/SWV014_0.ax',antisymmetric_ordering_ax)).
% 12.88/2.11 tff(f9,axiom,(
% 12.88/2.11 ! [X0 : general,X1 : general] : (p__less_equal__(X0,X1) | p__less_equal__(X1,X0))),
% 12.88/2.11 file('/export/starexec/sandbox/benchmark/Axioms/SWV014_0.ax',strongly_connected_ordering_ax)).
% 12.88/2.11 tff(f17,axiom,(
% 12.88/2.11 ! [X0 : general,X1 : general] : (in0(X0,X1) => person(X0))),
% 12.88/2.11 file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_1_unnamed_formula)).
% 12.88/2.11 tff(f18,axiom,(
% 12.88/2.11 ! [X0 : general,X1 : general,X2 : general] : (goto(X0,X1,X2) => person(X0))),
% 12.88/2.11 file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_2_unnamed_formula)).
% 12.88/2.11 tff(f24,axiom,(
% 12.88/2.11 ! [X0 : general,X1 : general,X2 : general] : (in(X0,X1,X2) <=> (? [X3 : general,X4 : general] : (X0 = X3 & X1 = X4 & X2 = f__integer__(0) & ? [X5 : general,X6 : general] : (X5 = X3 & X6 = X4 & in0(X5,X6))) | ? [X3 : general,X4 : general,X7 : general] : (X0 = X3 & X1 = X4 & ? [X8 : $int,X9 : $int] : (X2 = f__integer__($sum(X8,X9)) & f__integer__(X8) = X7 & X9 = 1) & ? [X5 : general,X6 : general,X10 : general] : (X5 = X3 & X6 = X4 & X10 = X7 & goto(X5,X6,X10))) | ? [X3 : general,X4 : general,X7 : general] : (X0 = X3 & X1 = X4 & ? [X8 : $int,X9 : $int] : (X2 = f__integer__($sum(X8,X9)) & f__integer__(X8) = X7 & X9 = 1) & ? [X5 : general,X6 : general,X10 : general] : (X5 = X3 & X6 = X4 & X10 = X7 & in(X5,X6,X10)) & ? [X5 : general,X6 : general] : (X5 = X7 & ? [X8 : $int,X9 : $int,X11 : $int] : (X8 = 0 & ? [X8 : $int,X12 : $int] : (X9 = $difference(X8,X12) & X8 = h_i & X12 = 1) & X6 = f__integer__(X11) & $lesseq(X8,X11) & $lesseq(X11,X9)) & X5 = X6) & in(X0,X1,X2))))),
% 12.88/2.11 file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_8_completed_definition_of_in_3)).
% 12.88/2.11 tff(f25,conjecture,(
% 12.88/2.11 ! [X0 : general,X1 : general] : (in(X0,X1,f__integer__(0)) => person(X0))),
% 12.88/2.11 file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_9_base_case)).
% 12.88/2.11 tff(f26,negated_conjecture,(
% 12.88/2.11 ~ ! [X0 : general,X1 : general] : (in(X0,X1,f__integer__(0)) => person(X0))),
% 12.88/2.11 inference(negated_conjecture,[status(cth)],[f25])).
% 12.88/2.11 tff(f27,plain,(
% 12.88/2.11 ! [X0 : $int,X1 : $int] : (p__less_equal__(f__integer__(X0),f__integer__(X1)) <=> ~$less(X1,X0))),
% 12.88/2.11 inference(theory_normalization,[],[f6])).
% 12.88/2.11 tff(f30,plain,(
% 12.88/2.11 ! [X0 : general,X1 : general,X2 : general] : (in(X0,X1,X2) <=> (? [X3 : general,X4 : general] : (X0 = X3 & X1 = X4 & X2 = f__integer__(0) & ? [X5 : general,X6 : general] : (X5 = X3 & X6 = X4 & in0(X5,X6))) | ? [X3 : general,X4 : general,X7 : general] : (X0 = X3 & X1 = X4 & ? [X8 : $int,X9 : $int] : (X2 = f__integer__($sum(X8,X9)) & f__integer__(X8) = X7 & X9 = 1) & ? [X5 : general,X6 : general,X10 : general] : (X5 = X3 & X6 = X4 & X10 = X7 & goto(X5,X6,X10))) | ? [X3 : general,X4 : general,X7 : general] : (X0 = X3 & X1 = X4 & ? [X8 : $int,X9 : $int] : (X2 = f__integer__($sum(X8,X9)) & f__integer__(X8) = X7 & X9 = 1) & ? [X5 : general,X6 : general,X10 : general] : (X5 = X3 & X6 = X4 & X10 = X7 & in(X5,X6,X10)) & ? [X5 : general,X6 : general] : (X5 = X7 & ? [X8 : $int,X9 : $int,X11 : $int] : (X8 = 0 & ? [X8 : $int,X12 : $int] : ($sum(X8,$uminus(X12)) = X9 & X8 = h_i & X12 = 1) & X6 = f__integer__(X11) & ~$less(X11,X8) & ~$less(X9,X11)) & X5 = X6) & in(X0,X1,X2))))),
% 12.88/2.11 inference(theory_normalization,[],[f24])).
% 12.88/2.11 tff(f31,definition,(
% 12.88/2.11 ( ! [X0 : $int,X1 : $int] : ($sum(X0,X1) = $sum(X1,X0)) )),
% 12.88/2.11 introduced(theory,[tha_commutativity])).
% 12.88/2.11 tff(f36,definition,(
% 12.88/2.11 ( ! [X0 : $int] : (~$less(X0,X0)) )),
% 12.88/2.11 introduced(theory,[tha_non-reflexivity])).
% 12.88/2.11 tff(f40,definition,(
% 12.88/2.11 ( ! [X0 : $int,X1 : $int] : ($less(X1,$sum(X0,1)) | $less(X0,X1)) )),
% 12.88/2.11 introduced(theory,[tha_order_plus_one_dichotomy])).
% 12.88/2.11 tff(f45,plain,(
% 12.88/2.11 ! [X0 : general,X1 : general,X2 : general] : (in(X0,X1,X2) <=> (? [X3 : general,X4 : general] : (X0 = X3 & X1 = X4 & X2 = f__integer__(0) & ? [X5 : general,X6 : general] : (X5 = X3 & X6 = X4 & in0(X5,X6))) | ? [X7 : general,X8 : general,X9 : general] : (X0 = X7 & X1 = X8 & ? [X10 : $int,X11 : $int] : (f__integer__($sum(X10,X11)) = X2 & f__integer__(X10) = X9 & 1 = X11) & ? [X12 : general,X13 : general,X14 : general] : (X7 = X12 & X8 = X13 & X9 = X14 & goto(X12,X13,X14))) | ? [X15 : general,X16 : general,X17 : general] : (X0 = X15 & X1 = X16 & ? [X18 : $int,X19 : $int] : (f__integer__($sum(X18,X19)) = X2 & f__integer__(X18) = X17 & 1 = X19) & ? [X20 : general,X21 : general,X22 : general] : (X15 = X20 & X16 = X21 & X17 = X22 & in(X20,X21,X22)) & ? [X23 : general,X24 : general] : (X17 = X23 & ? [X25 : $int,X26 : $int,X27 : $int] : (0 = X25 & ? [X28 : $int,X29 : $int] : ($sum(X28,$uminus(X29)) = X26 & h_i = X28 & 1 = X29) & f__integer__(X27) = X24 & ~$less(X27,X25) & ~$less(X26,X27)) & X23 = X24) & in(X0,X1,X2))))),
% 12.88/2.11 inference(rectify,[],[f30])).
% 12.88/2.11 tff(f52,plain,(
% 12.88/2.11 ! [X0 : general,X1 : general] : (X0 = X1 | (~p__less_equal__(X0,X1) | ~p__less_equal__(X1,X0)))),
% 12.88/2.11 inference(ennf_transformation,[],[f7])).
% 12.88/2.11 tff(f53,plain,(
% 12.88/2.11 ! [X0 : general,X1 : general] : (X0 = X1 | ~p__less_equal__(X0,X1) | ~p__less_equal__(X1,X0))),
% 12.88/2.11 inference(flattening,[],[f52])).
% 12.88/2.11 tff(f57,plain,(
% 12.88/2.11 ! [X0 : general,X1 : general] : (person(X0) | ~in0(X0,X1))),
% 12.88/2.11 inference(ennf_transformation,[],[f17])).
% 12.88/2.11 tff(f58,plain,(
% 12.88/2.11 ! [X0 : general,X1 : general,X2 : general] : (person(X0) | ~goto(X0,X1,X2))),
% 12.88/2.11 inference(ennf_transformation,[],[f18])).
% 12.88/2.11 tff(f64,plain,(
% 12.88/2.11 ? [X0 : general,X1 : general] : (~person(X0) & in(X0,X1,f__integer__(0)))),
% 12.88/2.11 inference(ennf_transformation,[],[f26])).
% 12.88/2.11 tff(f72,plain,(
% 12.88/2.11 ( ! [X0 : $int,X1 : $int] : (p__less_equal__(f__integer__(X0),f__integer__(X1)) | $less(X1,X0)) )),
% 12.88/2.11 inference(cnf_transformation,[],[f27])).
% 12.88/2.11 tff(f73,plain,(
% 12.88/2.11 ( ! [X0 : $int,X1 : $int] : (~$less(X1,X0) | ~p__less_equal__(f__integer__(X0),f__integer__(X1))) )),
% 12.88/2.11 inference(cnf_transformation,[],[f27])).
% 12.88/2.11 tff(f74,plain,(
% 12.88/2.11 ( ! [X0 : general,X1 : general] : (~p__less_equal__(X0,X1) | ~p__less_equal__(X1,X0) | X0 = X1) )),
% 12.88/2.11 inference(cnf_transformation,[],[f53])).
% 12.88/2.11 tff(f76,plain,(
% 12.88/2.11 ( ! [X0 : general,X1 : general] : (p__less_equal__(X1,X0) | p__less_equal__(X0,X1)) )),
% 12.88/2.11 inference(cnf_transformation,[],[f9])).
% 12.88/2.11 tff(f83,plain,(
% 12.88/2.11 ( ! [X0 : general,X1 : general] : (~in0(X0,X1) | person(X0)) )),
% 12.88/2.11 inference(cnf_transformation,[],[f57])).
% 12.88/2.11 tff(f84,plain,(
% 12.88/2.11 ( ! [X2 : general,X0 : general,X1 : general] : (~goto(X0,X1,X2) | person(X0)) )),
% 12.88/2.11 inference(cnf_transformation,[],[f58])).
% 12.88/2.11 tff(f106,plain,(
% 12.88/2.11 ( ! [X2 : general,X0 : general,X1 : general] : (~in(X0,X1,X2) | sP29(sK26(X0,X1,X2),sK25(X0,X1,X2),sK24(X0,X1,X2),sK13(X0,X1,X2),sK12(X0,X1,X2),sK11(X0,X1,X2)) | sP16(sK15(X0,X1,X2),sK14(X0,X1,X2),X2,X1,X0) | ~$less(sK35(X0,X1,X2),sK33(X0,X1,X2))) )),
% 12.88/2.11 inference(cnf_transformation,[],[f45])).
% 12.88/2.11 tff(f107,plain,(
% 12.88/2.11 ( ! [X2 : general,X0 : general,X1 : general] : (~in(X0,X1,X2) | sP29(sK26(X0,X1,X2),sK25(X0,X1,X2),sK24(X0,X1,X2),sK13(X0,X1,X2),sK12(X0,X1,X2),sK11(X0,X1,X2)) | sP16(sK15(X0,X1,X2),sK14(X0,X1,X2),X2,X1,X0) | sK18(X0,X1,X2) = f__integer__(sK35(X0,X1,X2))) )),
% 12.88/2.11 inference(cnf_transformation,[],[f45])).
% 12.88/2.11 tff(f108,plain,(
% 12.88/2.11 ( ! [X2 : general,X0 : general,X1 : general] : (~in(X0,X1,X2) | sP29(sK26(X0,X1,X2),sK25(X0,X1,X2),sK24(X0,X1,X2),sK13(X0,X1,X2),sK12(X0,X1,X2),sK11(X0,X1,X2)) | sP16(sK15(X0,X1,X2),sK14(X0,X1,X2),X2,X1,X0) | 0 = sK33(X0,X1,X2)) )),
% 12.88/2.11 inference(cnf_transformation,[],[f45])).
% 12.88/2.11 tff(f114,plain,(
% 12.88/2.11 ( ! [X2 : general,X0 : general,X1 : general] : (~$less(sK35(X0,X1,X2),sK33(X0,X1,X2)) | sK12(X0,X1,X2) = X1 | sP16(sK15(X0,X1,X2),sK14(X0,X1,X2),X2,X1,X0) | ~in(X0,X1,X2)) )),
% 12.88/2.11 inference(cnf_transformation,[],[f45])).
% 12.88/2.11 tff(f115,plain,(
% 12.88/2.11 ( ! [X2 : general,X0 : general,X1 : general] : (~in(X0,X1,X2) | sK12(X0,X1,X2) = X1 | sP16(sK15(X0,X1,X2),sK14(X0,X1,X2),X2,X1,X0) | sK18(X0,X1,X2) = f__integer__(sK35(X0,X1,X2))) )),
% 12.88/2.11 inference(cnf_transformation,[],[f45])).
% 12.88/2.11 tff(f116,plain,(
% 12.88/2.11 ( ! [X2 : general,X0 : general,X1 : general] : (~in(X0,X1,X2) | sK12(X0,X1,X2) = X1 | sP16(sK15(X0,X1,X2),sK14(X0,X1,X2),X2,X1,X0) | 0 = sK33(X0,X1,X2)) )),
% 12.88/2.11 inference(cnf_transformation,[],[f45])).
% 12.88/2.11 tff(f118,plain,(
% 12.88/2.11 ( ! [X2 : general,X0 : general,X1 : general] : (~$less(sK35(X0,X1,X2),sK33(X0,X1,X2)) | sK11(X0,X1,X2) = X0 | sP16(sK15(X0,X1,X2),sK14(X0,X1,X2),X2,X1,X0) | ~in(X0,X1,X2)) )),
% 12.88/2.11 inference(cnf_transformation,[],[f45])).
% 12.88/2.11 tff(f119,plain,(
% 12.88/2.11 ( ! [X2 : general,X0 : general,X1 : general] : (~in(X0,X1,X2) | sK11(X0,X1,X2) = X0 | sP16(sK15(X0,X1,X2),sK14(X0,X1,X2),X2,X1,X0) | sK18(X0,X1,X2) = f__integer__(sK35(X0,X1,X2))) )),
% 12.88/2.11 inference(cnf_transformation,[],[f45])).
% 12.88/2.11 tff(f120,plain,(
% 12.88/2.11 ( ! [X2 : general,X0 : general,X1 : general] : (~in(X0,X1,X2) | sK11(X0,X1,X2) = X0 | sP16(sK15(X0,X1,X2),sK14(X0,X1,X2),X2,X1,X0) | 0 = sK33(X0,X1,X2)) )),
% 12.88/2.11 inference(cnf_transformation,[],[f45])).
% 12.88/2.11 tff(f121,plain,(
% 12.88/2.11 ( ! [X2 : general,X3 : general,X0 : general,X1 : general,X4 : general] : (in0(sK31(X3,X4),sK32(X3,X4)) | ~sP16(X4,X3,X2,X1,X0)) )),
% 12.88/2.11 inference(cnf_transformation,[],[f45])).
% 12.88/2.11 tff(f122,plain,(
% 12.88/2.11 ( ! [X2 : general,X3 : general,X0 : general,X1 : general,X4 : general] : (~sP16(X4,X3,X2,X1,X0) | sK32(X3,X4) = X4) )),
% 12.88/2.11 inference(cnf_transformation,[],[f45])).
% 12.88/2.11 tff(f123,plain,(
% 12.88/2.11 ( ! [X2 : general,X3 : general,X0 : general,X1 : general,X4 : general] : (~sP16(X4,X3,X2,X1,X0) | sK31(X3,X4) = X3) )),
% 12.88/2.11 inference(cnf_transformation,[],[f45])).
% 12.88/2.11 tff(f130,plain,(
% 12.88/2.11 ( ! [X8 : general,X9 : general,X7 : general,X14 : general,X12 : general,X13 : general] : (goto(X12,X13,X14) | ~sP29(X14,X13,X12,X9,X8,X7)) )),
% 12.88/2.11 inference(cnf_transformation,[],[f45])).
% 12.88/2.11 tff(f132,plain,(
% 12.88/2.11 ( ! [X8 : general,X9 : general,X7 : general,X14 : general,X12 : general,X13 : general] : (~sP29(X14,X13,X12,X9,X8,X7) | X8 = X13) )),
% 12.88/2.11 inference(cnf_transformation,[],[f45])).
% 12.88/2.11 tff(f133,plain,(
% 12.88/2.11 ( ! [X8 : general,X9 : general,X7 : general,X14 : general,X12 : general,X13 : general] : (~sP29(X14,X13,X12,X9,X8,X7) | X7 = X12) )),
% 12.88/2.11 inference(cnf_transformation,[],[f45])).
% 12.88/2.11 tff(f134,plain,(
% 12.88/2.11 ( ! [X2 : general,X0 : general,X1 : general] : (~in(X0,X1,X2) | sK11(X0,X1,X2) = X0 | sP16(sK15(X0,X1,X2),sK14(X0,X1,X2),X2,X1,X0) | 1 = sK23(X0,X1,X2)) )),
% 12.88/2.11 inference(cnf_transformation,[],[f45])).
% 12.88/2.11 tff(f135,plain,(
% 12.88/2.11 ( ! [X2 : general,X0 : general,X1 : general] : (~in(X0,X1,X2) | sK11(X0,X1,X2) = X0 | sP16(sK15(X0,X1,X2),sK14(X0,X1,X2),X2,X1,X0) | sK10(X0,X1,X2) = f__integer__(sK22(X0,X1,X2))) )),
% 12.88/2.11 inference(cnf_transformation,[],[f45])).
% 12.88/2.11 tff(f136,plain,(
% 12.88/2.11 ( ! [X2 : general,X0 : general,X1 : general] : (~in(X0,X1,X2) | sK11(X0,X1,X2) = X0 | sP16(sK15(X0,X1,X2),sK14(X0,X1,X2),X2,X1,X0) | f__integer__($sum(sK22(X0,X1,X2),sK23(X0,X1,X2))) = X2) )),
% 12.88/2.11 inference(cnf_transformation,[],[f45])).
% 12.88/2.11 tff(f137,plain,(
% 12.88/2.11 ( ! [X2 : general,X0 : general,X1 : general] : (~in(X0,X1,X2) | sK12(X0,X1,X2) = X1 | sP16(sK15(X0,X1,X2),sK14(X0,X1,X2),X2,X1,X0) | 1 = sK23(X0,X1,X2)) )),
% 12.88/2.11 inference(cnf_transformation,[],[f45])).
% 12.88/2.11 tff(f138,plain,(
% 12.88/2.11 ( ! [X2 : general,X0 : general,X1 : general] : (~in(X0,X1,X2) | sK12(X0,X1,X2) = X1 | sP16(sK15(X0,X1,X2),sK14(X0,X1,X2),X2,X1,X0) | sK10(X0,X1,X2) = f__integer__(sK22(X0,X1,X2))) )),
% 12.88/2.11 inference(cnf_transformation,[],[f45])).
% 12.88/2.11 tff(f139,plain,(
% 12.88/2.11 ( ! [X2 : general,X0 : general,X1 : general] : (~in(X0,X1,X2) | sK12(X0,X1,X2) = X1 | sP16(sK15(X0,X1,X2),sK14(X0,X1,X2),X2,X1,X0) | f__integer__($sum(sK22(X0,X1,X2),sK23(X0,X1,X2))) = X2) )),
% 12.88/2.11 inference(cnf_transformation,[],[f45])).
% 12.88/2.11 tff(f143,plain,(
% 12.88/2.11 ( ! [X2 : general,X0 : general,X1 : general] : (~in(X0,X1,X2) | sP29(sK26(X0,X1,X2),sK25(X0,X1,X2),sK24(X0,X1,X2),sK13(X0,X1,X2),sK12(X0,X1,X2),sK11(X0,X1,X2)) | sP16(sK15(X0,X1,X2),sK14(X0,X1,X2),X2,X1,X0) | 1 = sK23(X0,X1,X2)) )),
% 12.88/2.11 inference(cnf_transformation,[],[f45])).
% 12.88/2.11 tff(f144,plain,(
% 12.88/2.11 ( ! [X2 : general,X0 : general,X1 : general] : (~in(X0,X1,X2) | sP29(sK26(X0,X1,X2),sK25(X0,X1,X2),sK24(X0,X1,X2),sK13(X0,X1,X2),sK12(X0,X1,X2),sK11(X0,X1,X2)) | sP16(sK15(X0,X1,X2),sK14(X0,X1,X2),X2,X1,X0) | sK10(X0,X1,X2) = f__integer__(sK22(X0,X1,X2))) )),
% 12.88/2.11 inference(cnf_transformation,[],[f45])).
% 12.88/2.11 tff(f145,plain,(
% 12.88/2.11 ( ! [X2 : general,X0 : general,X1 : general] : (~in(X0,X1,X2) | sP29(sK26(X0,X1,X2),sK25(X0,X1,X2),sK24(X0,X1,X2),sK13(X0,X1,X2),sK12(X0,X1,X2),sK11(X0,X1,X2)) | sP16(sK15(X0,X1,X2),sK14(X0,X1,X2),X2,X1,X0) | f__integer__($sum(sK22(X0,X1,X2),sK23(X0,X1,X2))) = X2) )),
% 12.88/2.11 inference(cnf_transformation,[],[f45])).
% 12.88/2.11 tff(f162,plain,(
% 12.88/2.11 ( ! [X2 : general,X0 : general,X1 : general] : (~in(X0,X1,X2) | sK11(X0,X1,X2) = X0 | sP16(sK15(X0,X1,X2),sK14(X0,X1,X2),X2,X1,X0) | sK17(X0,X1,X2) = sK18(X0,X1,X2)) )),
% 12.88/2.11 inference(cnf_transformation,[],[f45])).
% 12.88/2.11 tff(f163,plain,(
% 12.88/2.11 ( ! [X2 : general,X0 : general,X1 : general] : (~in(X0,X1,X2) | sK11(X0,X1,X2) = X0 | sP16(sK15(X0,X1,X2),sK14(X0,X1,X2),X2,X1,X0) | sK10(X0,X1,X2) = sK17(X0,X1,X2)) )),
% 12.88/2.11 inference(cnf_transformation,[],[f45])).
% 12.88/2.11 tff(f164,plain,(
% 12.88/2.11 ( ! [X2 : general,X0 : general,X1 : general] : (~in(X0,X1,X2) | sK12(X0,X1,X2) = X1 | sP16(sK15(X0,X1,X2),sK14(X0,X1,X2),X2,X1,X0) | sK17(X0,X1,X2) = sK18(X0,X1,X2)) )),
% 12.88/2.11 inference(cnf_transformation,[],[f45])).
% 12.88/2.11 tff(f165,plain,(
% 12.88/2.11 ( ! [X2 : general,X0 : general,X1 : general] : (~in(X0,X1,X2) | sK12(X0,X1,X2) = X1 | sP16(sK15(X0,X1,X2),sK14(X0,X1,X2),X2,X1,X0) | sK10(X0,X1,X2) = sK17(X0,X1,X2)) )),
% 12.88/2.11 inference(cnf_transformation,[],[f45])).
% 12.88/2.11 tff(f168,plain,(
% 12.88/2.11 ( ! [X2 : general,X0 : general,X1 : general] : (~in(X0,X1,X2) | sP29(sK26(X0,X1,X2),sK25(X0,X1,X2),sK24(X0,X1,X2),sK13(X0,X1,X2),sK12(X0,X1,X2),sK11(X0,X1,X2)) | sP16(sK15(X0,X1,X2),sK14(X0,X1,X2),X2,X1,X0) | sK17(X0,X1,X2) = sK18(X0,X1,X2)) )),
% 12.88/2.11 inference(cnf_transformation,[],[f45])).
% 12.88/2.11 tff(f169,plain,(
% 12.88/2.11 ( ! [X2 : general,X0 : general,X1 : general] : (~in(X0,X1,X2) | sP29(sK26(X0,X1,X2),sK25(X0,X1,X2),sK24(X0,X1,X2),sK13(X0,X1,X2),sK12(X0,X1,X2),sK11(X0,X1,X2)) | sP16(sK15(X0,X1,X2),sK14(X0,X1,X2),X2,X1,X0) | sK10(X0,X1,X2) = sK17(X0,X1,X2)) )),
% 12.88/2.11 inference(cnf_transformation,[],[f45])).
% 12.88/2.11 tff(f171,plain,(
% 12.88/2.11 ( ! [X2 : general,X3 : general,X0 : general,X1 : general,X4 : general] : (~sP16(X4,X3,X2,X1,X0) | X1 = X4) )),
% 12.88/2.11 inference(cnf_transformation,[],[f45])).
% 12.88/2.11 tff(f172,plain,(
% 12.88/2.11 ( ! [X2 : general,X3 : general,X0 : general,X1 : general,X4 : general] : (~sP16(X4,X3,X2,X1,X0) | X0 = X3) )),
% 12.88/2.11 inference(cnf_transformation,[],[f45])).
% 12.88/2.11 tff(f183,plain,(
% 12.88/2.11 in(sK38,sK39,f__integer__(0))),
% 12.88/2.11 inference(cnf_transformation,[],[f64])).
% 12.88/2.11 tff(f184,plain,(
% 12.88/2.11 ~person(sK38)),
% 12.88/2.11 inference(cnf_transformation,[],[f64])).
% 12.88/2.11 tff(f219,plain,(
% 12.88/2.11 ( ! [X0 : general,X1 : general] : (in0(X0,X1) | ~person(X0)) )),
% 12.88/2.11 inference(consistent_polarity_flipping,[],[f83])).
% 12.88/2.11 tff(f220,plain,(
% 12.88/2.11 ( ! [X2 : general,X0 : general,X1 : general] : (goto(X0,X1,X2) | ~person(X0)) )),
% 12.88/2.11 inference(consistent_polarity_flipping,[],[f84])).
% 12.88/2.11 tff(f234,plain,(
% 12.88/2.11 ( ! [X8 : general,X9 : general,X7 : general,X14 : general,X12 : general,X13 : general] : (~sP29(X14,X13,X12,X9,X8,X7) | ~goto(X12,X13,X14)) )),
% 12.88/2.11 inference(consistent_polarity_flipping,[],[f130])).
% 12.88/2.11 tff(f241,plain,(
% 12.88/2.11 ( ! [X2 : general,X3 : general,X0 : general,X1 : general,X4 : general] : (~in0(sK31(X3,X4),sK32(X3,X4)) | ~sP16(X4,X3,X2,X1,X0)) )),
% 12.88/2.11 inference(consistent_polarity_flipping,[],[f121])).
% 12.88/2.11 tff(f249,plain,(
% 12.88/2.11 person(sK38)),
% 12.88/2.11 inference(consistent_polarity_flipping,[],[f184])).
% 12.88/2.11 tff(f251,plain,(
% 12.88/2.11 ( ! [X0 : general] : (p__less_equal__(X0,X0)) )),
% 12.88/2.11 inference(factoring,[],[f76])).
% 12.88/2.11 tff(f259,plain,(
% 12.88/2.11 ( ! [X0 : $int] : ($less(X0,$sum(X0,1))) )),
% 12.88/2.11 inference(resolution,[],[f40,f36])).
% 12.88/2.11 tff(f268,plain,(
% 12.88/2.11 ( ! [X0 : $int] : ($less(X0,$sum(1,X0))) )),
% 12.88/2.11 inference(superposition,[],[f259,f31])).
% 12.88/2.11 tff(f270,plain,(
% 12.88/2.11 ( ! [X0 : $int] : (~p__less_equal__(f__integer__($sum(1,X0)),f__integer__(X0))) )),
% 12.88/2.11 inference(resolution,[],[f268,f73])).
% 12.88/2.11 tff(f324,plain,(
% 12.88/2.11 ( ! [X0 : $int,X1 : $int] : (~p__less_equal__(f__integer__(X0),f__integer__(X1)) | f__integer__(X1) = f__integer__(X0) | $less(X0,X1)) )),
% 12.88/2.11 inference(resolution,[],[f74,f72])).
% 12.88/2.11 tff(f458,plain,(
% 12.88/2.11 ( ! [X0 : $int] : (p__less_equal__(f__integer__(X0),f__integer__($sum(1,X0)))) )),
% 12.88/2.11 inference(resolution,[],[f270,f76])).
% 12.88/2.11 tff(f512,definition,(
% 12.88/2.11 spl40_6 <=> sP16(sK15(sK38,sK39,f__integer__(0)),sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38)),
% 12.88/2.11 introduced(definition,[new_symbols(definition,[spl40_6])],[avatar_definition])).
% 12.88/2.11 tff(f513,plain,(
% 12.88/2.11 ~sP16(sK15(sK38,sK39,f__integer__(0)),sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38) | spl40_6),
% 12.88/2.11 inference(avatar_component_clause,[],[f512])).
% 12.88/2.11 tff(f514,plain,(
% 12.88/2.11 sP16(sK15(sK38,sK39,f__integer__(0)),sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38) | ~spl40_6),
% 12.88/2.11 inference(avatar_component_clause,[],[f512])).
% 12.88/2.11 tff(f516,definition,(
% 12.88/2.11 spl40_7 <=> sK38 = sK11(sK38,sK39,f__integer__(0))),
% 12.88/2.11 introduced(definition,[new_symbols(definition,[spl40_7])],[avatar_definition])).
% 12.88/2.11 tff(f518,plain,(
% 12.88/2.11 sK38 = sK11(sK38,sK39,f__integer__(0)) | ~spl40_7),
% 12.88/2.11 inference(avatar_component_clause,[],[f516])).
% 12.88/2.11 tff(f531,plain,(
% 12.88/2.11 sK39 = sK12(sK38,sK39,f__integer__(0)) | sP16(sK15(sK38,sK39,f__integer__(0)),sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38) | 0 = sK33(sK38,sK39,f__integer__(0))),
% 12.88/2.11 inference(resolution,[],[f116,f183])).
% 12.88/2.11 tff(f534,definition,(
% 12.88/2.11 spl40_8 <=> 0 = sK33(sK38,sK39,f__integer__(0))),
% 12.88/2.11 introduced(definition,[new_symbols(definition,[spl40_8])],[avatar_definition])).
% 12.88/2.11 tff(f536,plain,(
% 12.88/2.11 0 = sK33(sK38,sK39,f__integer__(0)) | ~spl40_8),
% 12.88/2.11 inference(avatar_component_clause,[],[f534])).
% 12.88/2.11 tff(f538,definition,(
% 12.88/2.11 spl40_9 <=> sK39 = sK12(sK38,sK39,f__integer__(0))),
% 12.88/2.11 introduced(definition,[new_symbols(definition,[spl40_9])],[avatar_definition])).
% 12.88/2.11 tff(f540,plain,(
% 12.88/2.11 sK39 = sK12(sK38,sK39,f__integer__(0)) | ~spl40_9),
% 12.88/2.11 inference(avatar_component_clause,[],[f538])).
% 12.88/2.11 tff(f541,plain,(
% 12.88/2.11 spl40_8 | spl40_6 | spl40_9),
% 12.88/2.11 inference(avatar_split_clause,[],[f531,f538,f512,f534])).
% 12.88/2.11 tff(f542,plain,(
% 12.88/2.11 sK38 = sK11(sK38,sK39,f__integer__(0)) | sP16(sK15(sK38,sK39,f__integer__(0)),sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38) | 0 = sK33(sK38,sK39,f__integer__(0))),
% 12.88/2.11 inference(resolution,[],[f120,f183])).
% 12.88/2.11 tff(f544,plain,(
% 12.88/2.11 spl40_8 | spl40_6 | spl40_7),
% 12.88/2.11 inference(avatar_split_clause,[],[f542,f516,f512,f534])).
% 12.88/2.11 tff(f549,plain,(
% 12.88/2.11 sK38 = sK14(sK38,sK39,f__integer__(0)) | ~spl40_6),
% 12.88/2.11 inference(resolution,[],[f514,f172])).
% 12.88/2.11 tff(f550,plain,(
% 12.88/2.11 sK39 = sK15(sK38,sK39,f__integer__(0)) | ~spl40_6),
% 12.88/2.11 inference(resolution,[],[f514,f171])).
% 12.88/2.11 tff(f552,plain,(
% 12.88/2.11 sP16(sK39,sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38) | ~spl40_6),
% 12.88/2.11 inference(superposition,[],[f514,f550])).
% 12.88/2.11 tff(f553,plain,(
% 12.88/2.11 sP16(sK39,sK38,f__integer__(0),sK39,sK38) | ~spl40_6),
% 12.88/2.11 inference(forward_demodulation,[],[f552,f549])).
% 12.88/2.11 tff(f554,plain,(
% 12.88/2.11 sK38 = sK11(sK38,sK39,f__integer__(0)) | sP16(sK15(sK38,sK39,f__integer__(0)),sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38) | 1 = sK23(sK38,sK39,f__integer__(0))),
% 12.88/2.11 inference(resolution,[],[f134,f183])).
% 12.88/2.11 tff(f556,plain,(
% 12.88/2.11 sK39 = sK12(sK38,sK39,f__integer__(0)) | sP16(sK15(sK38,sK39,f__integer__(0)),sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38) | 1 = sK23(sK38,sK39,f__integer__(0))),
% 12.88/2.11 inference(resolution,[],[f137,f183])).
% 12.88/2.11 tff(f564,plain,(
% 12.88/2.11 sK38 = sK31(sK38,sK39) | ~spl40_6),
% 12.88/2.11 inference(resolution,[],[f553,f123])).
% 12.88/2.11 tff(f565,plain,(
% 12.88/2.11 sK39 = sK32(sK38,sK39) | ~spl40_6),
% 12.88/2.11 inference(resolution,[],[f553,f122])).
% 12.88/2.11 tff(f580,definition,(
% 12.88/2.11 spl40_10 <=> ! [X2 : general,X0 : general,X1 : general] : ~sP16(sK39,sK38,X0,X1,X2)),
% 12.88/2.11 introduced(definition,[new_symbols(definition,[spl40_10])],[avatar_definition])).
% 12.88/2.11 tff(f581,plain,(
% 12.88/2.11 ( ! [X2 : general,X0 : general,X1 : general] : (~sP16(sK39,sK38,X0,X1,X2)) ) | ~spl40_10),
% 12.88/2.11 inference(avatar_component_clause,[],[f580])).
% 12.88/2.11 tff(f587,plain,(
% 12.88/2.11 ( ! [X2 : general,X0 : general,X1 : general] : (~in0(sK31(sK38,sK39),sK39) | ~sP16(sK39,sK38,X0,X1,X2)) ) | ~spl40_6),
% 12.88/2.11 inference(superposition,[],[f241,f565])).
% 12.88/2.11 tff(f588,plain,(
% 12.88/2.11 ( ! [X2 : general,X0 : general,X1 : general] : (~in0(sK38,sK39) | ~sP16(sK39,sK38,X0,X1,X2)) ) | ~spl40_6),
% 12.88/2.11 inference(forward_demodulation,[],[f587,f564])).
% 12.88/2.11 tff(f590,definition,(
% 12.88/2.11 spl40_12 <=> in0(sK38,sK39)),
% 12.88/2.11 introduced(definition,[new_symbols(definition,[spl40_12])],[avatar_definition])).
% 12.88/2.11 tff(f591,plain,(
% 12.88/2.11 in0(sK38,sK39) | ~spl40_12),
% 12.88/2.11 inference(avatar_component_clause,[],[f590])).
% 12.88/2.11 tff(f592,plain,(
% 12.88/2.11 ~in0(sK38,sK39) | spl40_12),
% 12.88/2.11 inference(avatar_component_clause,[],[f590])).
% 12.88/2.11 tff(f594,plain,(
% 12.88/2.11 ~person(sK38) | spl40_12),
% 12.88/2.11 inference(resolution,[],[f592,f219])).
% 12.88/2.11 tff(f595,plain,(
% 12.88/2.11 $false | spl40_12),
% 12.88/2.11 inference(forward_subsumption_resolution,[],[f594,f249])).
% 12.88/2.11 tff(f596,plain,(
% 12.88/2.11 spl40_12),
% 12.88/2.11 inference(avatar_contradiction_clause,[],[f595])).
% 12.88/2.11 tff(f598,definition,(
% 12.88/2.11 spl40_13 <=> 1 = sK23(sK38,sK39,f__integer__(0))),
% 12.88/2.11 introduced(definition,[new_symbols(definition,[spl40_13])],[avatar_definition])).
% 12.88/2.11 tff(f600,plain,(
% 12.88/2.11 1 = sK23(sK38,sK39,f__integer__(0)) | ~spl40_13),
% 12.88/2.11 inference(avatar_component_clause,[],[f598])).
% 12.88/2.11 tff(f601,plain,(
% 12.88/2.11 spl40_13 | spl40_6 | spl40_7),
% 12.88/2.11 inference(avatar_split_clause,[],[f554,f516,f512,f598])).
% 12.88/2.11 tff(f602,plain,(
% 12.88/2.11 spl40_13 | spl40_6 | spl40_9),
% 12.88/2.11 inference(avatar_split_clause,[],[f556,f538,f512,f598])).
% 12.88/2.11 tff(f644,definition,(
% 12.88/2.11 spl40_18 <=> $less(sK35(sK38,sK39,f__integer__(0)),0)),
% 12.88/2.11 introduced(definition,[new_symbols(definition,[spl40_18])],[avatar_definition])).
% 12.88/2.11 tff(f646,plain,(
% 12.88/2.11 ~$less(sK35(sK38,sK39,f__integer__(0)),0) | spl40_18),
% 12.88/2.11 inference(avatar_component_clause,[],[f644])).
% 12.88/2.11 tff(f675,plain,(
% 12.88/2.11 sK38 = sK11(sK38,sK39,f__integer__(0)) | sP16(sK15(sK38,sK39,f__integer__(0)),sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38) | sK17(sK38,sK39,f__integer__(0)) = sK18(sK38,sK39,f__integer__(0))),
% 12.88/2.11 inference(resolution,[],[f162,f183])).
% 12.88/2.11 tff(f677,plain,(
% 12.88/2.11 sK38 = sK11(sK38,sK39,f__integer__(0)) | sP16(sK15(sK38,sK39,f__integer__(0)),sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38) | sK10(sK38,sK39,f__integer__(0)) = sK17(sK38,sK39,f__integer__(0))),
% 12.88/2.11 inference(resolution,[],[f163,f183])).
% 12.88/2.11 tff(f679,plain,(
% 12.88/2.11 sK39 = sK12(sK38,sK39,f__integer__(0)) | sP16(sK15(sK38,sK39,f__integer__(0)),sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38) | sK17(sK38,sK39,f__integer__(0)) = sK18(sK38,sK39,f__integer__(0))),
% 12.88/2.11 inference(resolution,[],[f164,f183])).
% 12.88/2.11 tff(f689,plain,(
% 12.88/2.11 sK39 = sK12(sK38,sK39,f__integer__(0)) | sP16(sK15(sK38,sK39,f__integer__(0)),sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38) | sK10(sK38,sK39,f__integer__(0)) = sK17(sK38,sK39,f__integer__(0))),
% 12.88/2.11 inference(resolution,[],[f165,f183])).
% 12.88/2.11 tff(f699,plain,(
% 12.88/2.11 sK39 = sK12(sK38,sK39,f__integer__(0)) | sP16(sK15(sK38,sK39,f__integer__(0)),sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38) | sK18(sK38,sK39,f__integer__(0)) = f__integer__(sK35(sK38,sK39,f__integer__(0)))),
% 12.88/2.11 inference(resolution,[],[f115,f183])).
% 12.88/2.11 tff(f701,plain,(
% 12.88/2.11 sK38 = sK11(sK38,sK39,f__integer__(0)) | sP16(sK15(sK38,sK39,f__integer__(0)),sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38) | sK18(sK38,sK39,f__integer__(0)) = f__integer__(sK35(sK38,sK39,f__integer__(0)))),
% 12.88/2.11 inference(resolution,[],[f119,f183])).
% 12.88/2.11 tff(f703,plain,(
% 12.88/2.11 sK38 = sK11(sK38,sK39,f__integer__(0)) | sP16(sK15(sK38,sK39,f__integer__(0)),sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38) | sK10(sK38,sK39,f__integer__(0)) = f__integer__(sK22(sK38,sK39,f__integer__(0)))),
% 12.88/2.11 inference(resolution,[],[f135,f183])).
% 12.88/2.11 tff(f710,plain,(
% 12.88/2.11 sK39 = sK12(sK38,sK39,f__integer__(0)) | sP16(sK15(sK38,sK39,f__integer__(0)),sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38) | sK10(sK38,sK39,f__integer__(0)) = f__integer__(sK22(sK38,sK39,f__integer__(0)))),
% 12.88/2.11 inference(resolution,[],[f138,f183])).
% 12.88/2.11 tff(f712,plain,(
% 12.88/2.11 sK38 = sK11(sK38,sK39,f__integer__(0)) | sP16(sK15(sK38,sK39,f__integer__(0)),sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38) | f__integer__(0) = f__integer__($sum(sK22(sK38,sK39,f__integer__(0)),sK23(sK38,sK39,f__integer__(0))))),
% 12.88/2.11 inference(resolution,[],[f136,f183])).
% 12.88/2.11 tff(f738,plain,(
% 12.88/2.11 sK39 = sK12(sK38,sK39,f__integer__(0)) | sP16(sK15(sK38,sK39,f__integer__(0)),sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38) | f__integer__(0) = f__integer__($sum(sK22(sK38,sK39,f__integer__(0)),sK23(sK38,sK39,f__integer__(0))))),
% 12.88/2.11 inference(resolution,[],[f139,f183])).
% 12.88/2.11 tff(f899,definition,(
% 12.88/2.11 spl40_29 <=> sP29(sK26(sK38,sK39,f__integer__(0)),sK25(sK38,sK39,f__integer__(0)),sK24(sK38,sK39,f__integer__(0)),sK13(sK38,sK39,f__integer__(0)),sK39,sK38)),
% 12.88/2.11 introduced(definition,[new_symbols(definition,[spl40_29])],[avatar_definition])).
% 12.88/2.11 tff(f900,plain,(
% 12.88/2.11 ~sP29(sK26(sK38,sK39,f__integer__(0)),sK25(sK38,sK39,f__integer__(0)),sK24(sK38,sK39,f__integer__(0)),sK13(sK38,sK39,f__integer__(0)),sK39,sK38) | spl40_29),
% 12.88/2.11 inference(avatar_component_clause,[],[f899])).
% 12.88/2.11 tff(f901,plain,(
% 12.88/2.11 sP29(sK26(sK38,sK39,f__integer__(0)),sK25(sK38,sK39,f__integer__(0)),sK24(sK38,sK39,f__integer__(0)),sK13(sK38,sK39,f__integer__(0)),sK39,sK38) | ~spl40_29),
% 12.88/2.11 inference(avatar_component_clause,[],[f899])).
% 12.88/2.11 tff(f904,plain,(
% 12.88/2.11 ( ! [X2 : general,X0 : general,X1 : general] : (~sP16(sK39,sK38,X0,X1,X2)) ) | (~spl40_6 | ~spl40_12)),
% 12.88/2.11 inference(forward_subsumption_resolution,[],[f588,f591])).
% 12.88/2.11 tff(f907,plain,(
% 12.88/2.11 spl40_10 | ~spl40_6 | ~spl40_12),
% 12.88/2.11 inference(avatar_split_clause,[],[f904,f590,f512,f580])).
% 12.88/2.11 tff(f917,plain,(
% 12.88/2.11 $false | (~spl40_6 | ~spl40_10)),
% 12.88/2.11 inference(forward_subsumption_resolution,[],[f553,f581])).
% 12.88/2.11 tff(f918,plain,(
% 12.88/2.11 ~spl40_6 | ~spl40_10),
% 12.88/2.11 inference(avatar_contradiction_clause,[],[f917])).
% 12.88/2.11 tff(f925,plain,(
% 12.88/2.11 sP29(sK26(sK38,sK39,f__integer__(0)),sK25(sK38,sK39,f__integer__(0)),sK24(sK38,sK39,f__integer__(0)),sK13(sK38,sK39,f__integer__(0)),sK12(sK38,sK39,f__integer__(0)),sK11(sK38,sK39,f__integer__(0))) | sP16(sK15(sK38,sK39,f__integer__(0)),sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38) | 0 = sK33(sK38,sK39,f__integer__(0))),
% 12.88/2.11 inference(resolution,[],[f108,f183])).
% 12.88/2.11 tff(f957,plain,(
% 12.88/2.11 sP29(sK26(sK38,sK39,f__integer__(0)),sK25(sK38,sK39,f__integer__(0)),sK24(sK38,sK39,f__integer__(0)),sK13(sK38,sK39,f__integer__(0)),sK12(sK38,sK39,f__integer__(0)),sK11(sK38,sK39,f__integer__(0))) | sP16(sK15(sK38,sK39,f__integer__(0)),sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38) | 1 = sK23(sK38,sK39,f__integer__(0))),
% 12.88/2.11 inference(resolution,[],[f143,f183])).
% 12.88/2.11 tff(f959,plain,(
% 12.88/2.11 sP29(sK26(sK38,sK39,f__integer__(0)),sK25(sK38,sK39,f__integer__(0)),sK24(sK38,sK39,f__integer__(0)),sK13(sK38,sK39,f__integer__(0)),sK12(sK38,sK39,f__integer__(0)),sK38) | sP16(sK15(sK38,sK39,f__integer__(0)),sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38) | 1 = sK23(sK38,sK39,f__integer__(0)) | ~spl40_7),
% 12.88/2.11 inference(forward_demodulation,[],[f957,f518])).
% 12.88/2.11 tff(f960,plain,(
% 12.88/2.11 sP29(sK26(sK38,sK39,f__integer__(0)),sK25(sK38,sK39,f__integer__(0)),sK24(sK38,sK39,f__integer__(0)),sK13(sK38,sK39,f__integer__(0)),sK39,sK38) | sP16(sK15(sK38,sK39,f__integer__(0)),sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38) | 1 = sK23(sK38,sK39,f__integer__(0)) | (~spl40_7 | ~spl40_9)),
% 12.88/2.11 inference(forward_demodulation,[],[f959,f540])).
% 12.88/2.11 tff(f961,plain,(
% 12.88/2.11 spl40_13 | spl40_6 | spl40_29 | ~spl40_7 | ~spl40_9),
% 12.88/2.11 inference(avatar_split_clause,[],[f960,f538,f516,f899,f512,f598])).
% 12.88/2.11 tff(f984,plain,(
% 12.88/2.11 sP29(sK26(sK38,sK39,f__integer__(0)),sK25(sK38,sK39,f__integer__(0)),sK24(sK38,sK39,f__integer__(0)),sK13(sK38,sK39,f__integer__(0)),sK12(sK38,sK39,f__integer__(0)),sK11(sK38,sK39,f__integer__(0))) | sP16(sK15(sK38,sK39,f__integer__(0)),sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38) | ~$less(sK35(sK38,sK39,f__integer__(0)),sK33(sK38,sK39,f__integer__(0)))),
% 12.88/2.11 inference(resolution,[],[f106,f183])).
% 12.88/2.11 tff(f986,plain,(
% 12.88/2.11 sP29(sK26(sK38,sK39,f__integer__(0)),sK25(sK38,sK39,f__integer__(0)),sK24(sK38,sK39,f__integer__(0)),sK13(sK38,sK39,f__integer__(0)),sK12(sK38,sK39,f__integer__(0)),sK38) | sP16(sK15(sK38,sK39,f__integer__(0)),sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38) | ~$less(sK35(sK38,sK39,f__integer__(0)),sK33(sK38,sK39,f__integer__(0))) | ~spl40_7),
% 12.88/2.11 inference(forward_demodulation,[],[f984,f518])).
% 12.88/2.11 tff(f987,plain,(
% 12.88/2.11 sP29(sK26(sK38,sK39,f__integer__(0)),sK25(sK38,sK39,f__integer__(0)),sK24(sK38,sK39,f__integer__(0)),sK13(sK38,sK39,f__integer__(0)),sK39,sK38) | sP16(sK15(sK38,sK39,f__integer__(0)),sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38) | ~$less(sK35(sK38,sK39,f__integer__(0)),sK33(sK38,sK39,f__integer__(0))) | (~spl40_7 | ~spl40_9)),
% 12.88/2.11 inference(forward_demodulation,[],[f986,f540])).
% 12.88/2.11 tff(f988,plain,(
% 12.88/2.11 ~$less(sK35(sK38,sK39,f__integer__(0)),0) | sP29(sK26(sK38,sK39,f__integer__(0)),sK25(sK38,sK39,f__integer__(0)),sK24(sK38,sK39,f__integer__(0)),sK13(sK38,sK39,f__integer__(0)),sK39,sK38) | sP16(sK15(sK38,sK39,f__integer__(0)),sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38) | (~spl40_7 | ~spl40_8 | ~spl40_9)),
% 12.88/2.11 inference(forward_demodulation,[],[f987,f536])).
% 12.88/2.11 tff(f1023,plain,(
% 12.88/2.11 sP29(sK26(sK38,sK39,f__integer__(0)),sK25(sK38,sK39,f__integer__(0)),sK24(sK38,sK39,f__integer__(0)),sK13(sK38,sK39,f__integer__(0)),sK12(sK38,sK39,f__integer__(0)),sK11(sK38,sK39,f__integer__(0))) | sP16(sK15(sK38,sK39,f__integer__(0)),sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38) | sK17(sK38,sK39,f__integer__(0)) = sK18(sK38,sK39,f__integer__(0))),
% 12.88/2.11 inference(resolution,[],[f168,f183])).
% 12.88/2.11 tff(f1025,plain,(
% 12.88/2.11 sP29(sK26(sK38,sK39,f__integer__(0)),sK25(sK38,sK39,f__integer__(0)),sK24(sK38,sK39,f__integer__(0)),sK13(sK38,sK39,f__integer__(0)),sK12(sK38,sK39,f__integer__(0)),sK38) | sP16(sK15(sK38,sK39,f__integer__(0)),sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38) | sK17(sK38,sK39,f__integer__(0)) = sK18(sK38,sK39,f__integer__(0)) | ~spl40_7),
% 12.88/2.11 inference(forward_demodulation,[],[f1023,f518])).
% 12.88/2.11 tff(f1026,plain,(
% 12.88/2.11 sP29(sK26(sK38,sK39,f__integer__(0)),sK25(sK38,sK39,f__integer__(0)),sK24(sK38,sK39,f__integer__(0)),sK13(sK38,sK39,f__integer__(0)),sK39,sK38) | sP16(sK15(sK38,sK39,f__integer__(0)),sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38) | sK17(sK38,sK39,f__integer__(0)) = sK18(sK38,sK39,f__integer__(0)) | (~spl40_7 | ~spl40_9)),
% 12.88/2.11 inference(forward_demodulation,[],[f1025,f540])).
% 12.88/2.11 tff(f1028,definition,(
% 12.88/2.11 spl40_34 <=> sK17(sK38,sK39,f__integer__(0)) = sK18(sK38,sK39,f__integer__(0))),
% 12.88/2.12 introduced(definition,[new_symbols(definition,[spl40_34])],[avatar_definition])).
% 12.88/2.12 tff(f1030,plain,(
% 12.88/2.12 sK17(sK38,sK39,f__integer__(0)) = sK18(sK38,sK39,f__integer__(0)) | ~spl40_34),
% 12.88/2.12 inference(avatar_component_clause,[],[f1028])).
% 12.88/2.12 tff(f1031,plain,(
% 12.88/2.12 spl40_34 | spl40_6 | spl40_29 | ~spl40_7 | ~spl40_9),
% 12.88/2.12 inference(avatar_split_clause,[],[f1026,f538,f516,f899,f512,f1028])).
% 12.88/2.12 tff(f1032,plain,(
% 12.88/2.12 sP29(sK26(sK38,sK39,f__integer__(0)),sK25(sK38,sK39,f__integer__(0)),sK24(sK38,sK39,f__integer__(0)),sK13(sK38,sK39,f__integer__(0)),sK12(sK38,sK39,f__integer__(0)),sK11(sK38,sK39,f__integer__(0))) | sP16(sK15(sK38,sK39,f__integer__(0)),sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38) | sK10(sK38,sK39,f__integer__(0)) = sK17(sK38,sK39,f__integer__(0))),
% 12.88/2.12 inference(resolution,[],[f169,f183])).
% 12.88/2.12 tff(f1034,plain,(
% 12.88/2.12 sP29(sK26(sK38,sK39,f__integer__(0)),sK25(sK38,sK39,f__integer__(0)),sK24(sK38,sK39,f__integer__(0)),sK13(sK38,sK39,f__integer__(0)),sK12(sK38,sK39,f__integer__(0)),sK38) | sP16(sK15(sK38,sK39,f__integer__(0)),sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38) | sK10(sK38,sK39,f__integer__(0)) = sK17(sK38,sK39,f__integer__(0)) | ~spl40_7),
% 12.88/2.12 inference(forward_demodulation,[],[f1032,f518])).
% 12.88/2.12 tff(f1035,plain,(
% 12.88/2.12 sP29(sK26(sK38,sK39,f__integer__(0)),sK25(sK38,sK39,f__integer__(0)),sK24(sK38,sK39,f__integer__(0)),sK13(sK38,sK39,f__integer__(0)),sK39,sK38) | sP16(sK15(sK38,sK39,f__integer__(0)),sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38) | sK10(sK38,sK39,f__integer__(0)) = sK17(sK38,sK39,f__integer__(0)) | (~spl40_7 | ~spl40_9)),
% 12.88/2.12 inference(forward_demodulation,[],[f1034,f540])).
% 12.88/2.12 tff(f1037,definition,(
% 12.88/2.12 spl40_35 <=> sK10(sK38,sK39,f__integer__(0)) = sK17(sK38,sK39,f__integer__(0))),
% 12.88/2.12 introduced(definition,[new_symbols(definition,[spl40_35])],[avatar_definition])).
% 12.88/2.12 tff(f1039,plain,(
% 12.88/2.12 sK10(sK38,sK39,f__integer__(0)) = sK17(sK38,sK39,f__integer__(0)) | ~spl40_35),
% 12.88/2.12 inference(avatar_component_clause,[],[f1037])).
% 12.88/2.12 tff(f1040,plain,(
% 12.88/2.12 spl40_35 | spl40_6 | spl40_29 | ~spl40_7 | ~spl40_9),
% 12.88/2.12 inference(avatar_split_clause,[],[f1035,f538,f516,f899,f512,f1037])).
% 12.88/2.12 tff(f1041,plain,(
% 12.88/2.12 sP29(sK26(sK38,sK39,f__integer__(0)),sK25(sK38,sK39,f__integer__(0)),sK24(sK38,sK39,f__integer__(0)),sK13(sK38,sK39,f__integer__(0)),sK12(sK38,sK39,f__integer__(0)),sK11(sK38,sK39,f__integer__(0))) | sP16(sK15(sK38,sK39,f__integer__(0)),sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38) | sK18(sK38,sK39,f__integer__(0)) = f__integer__(sK35(sK38,sK39,f__integer__(0)))),
% 12.88/2.12 inference(resolution,[],[f107,f183])).
% 12.88/2.12 tff(f1043,plain,(
% 12.88/2.12 sP29(sK26(sK38,sK39,f__integer__(0)),sK25(sK38,sK39,f__integer__(0)),sK24(sK38,sK39,f__integer__(0)),sK13(sK38,sK39,f__integer__(0)),sK12(sK38,sK39,f__integer__(0)),sK38) | sP16(sK15(sK38,sK39,f__integer__(0)),sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38) | sK18(sK38,sK39,f__integer__(0)) = f__integer__(sK35(sK38,sK39,f__integer__(0))) | ~spl40_7),
% 12.88/2.12 inference(forward_demodulation,[],[f1041,f518])).
% 12.88/2.12 tff(f1044,plain,(
% 12.88/2.12 sP29(sK26(sK38,sK39,f__integer__(0)),sK25(sK38,sK39,f__integer__(0)),sK24(sK38,sK39,f__integer__(0)),sK13(sK38,sK39,f__integer__(0)),sK39,sK38) | sP16(sK15(sK38,sK39,f__integer__(0)),sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38) | sK18(sK38,sK39,f__integer__(0)) = f__integer__(sK35(sK38,sK39,f__integer__(0))) | (~spl40_7 | ~spl40_9)),
% 12.88/2.12 inference(forward_demodulation,[],[f1043,f540])).
% 12.88/2.12 tff(f1046,definition,(
% 12.88/2.12 spl40_36 <=> sK18(sK38,sK39,f__integer__(0)) = f__integer__(sK35(sK38,sK39,f__integer__(0)))),
% 12.88/2.12 introduced(definition,[new_symbols(definition,[spl40_36])],[avatar_definition])).
% 12.88/2.12 tff(f1048,plain,(
% 12.88/2.12 sK18(sK38,sK39,f__integer__(0)) = f__integer__(sK35(sK38,sK39,f__integer__(0))) | ~spl40_36),
% 12.88/2.12 inference(avatar_component_clause,[],[f1046])).
% 12.88/2.12 tff(f1049,plain,(
% 12.88/2.12 spl40_36 | spl40_6 | spl40_29 | ~spl40_7 | ~spl40_9),
% 12.88/2.12 inference(avatar_split_clause,[],[f1044,f538,f516,f899,f512,f1046])).
% 12.88/2.12 tff(f1050,plain,(
% 12.88/2.12 sP29(sK26(sK38,sK39,f__integer__(0)),sK25(sK38,sK39,f__integer__(0)),sK24(sK38,sK39,f__integer__(0)),sK13(sK38,sK39,f__integer__(0)),sK12(sK38,sK39,f__integer__(0)),sK11(sK38,sK39,f__integer__(0))) | sP16(sK15(sK38,sK39,f__integer__(0)),sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38) | sK10(sK38,sK39,f__integer__(0)) = f__integer__(sK22(sK38,sK39,f__integer__(0)))),
% 12.88/2.12 inference(resolution,[],[f144,f183])).
% 12.88/2.12 tff(f1052,plain,(
% 12.88/2.12 sP29(sK26(sK38,sK39,f__integer__(0)),sK25(sK38,sK39,f__integer__(0)),sK24(sK38,sK39,f__integer__(0)),sK13(sK38,sK39,f__integer__(0)),sK12(sK38,sK39,f__integer__(0)),sK38) | sP16(sK15(sK38,sK39,f__integer__(0)),sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38) | sK10(sK38,sK39,f__integer__(0)) = f__integer__(sK22(sK38,sK39,f__integer__(0))) | ~spl40_7),
% 12.88/2.12 inference(forward_demodulation,[],[f1050,f518])).
% 12.88/2.12 tff(f1053,plain,(
% 12.88/2.12 sP29(sK26(sK38,sK39,f__integer__(0)),sK25(sK38,sK39,f__integer__(0)),sK24(sK38,sK39,f__integer__(0)),sK13(sK38,sK39,f__integer__(0)),sK39,sK38) | sP16(sK15(sK38,sK39,f__integer__(0)),sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38) | sK10(sK38,sK39,f__integer__(0)) = f__integer__(sK22(sK38,sK39,f__integer__(0))) | (~spl40_7 | ~spl40_9)),
% 12.88/2.12 inference(forward_demodulation,[],[f1052,f540])).
% 12.88/2.12 tff(f1055,definition,(
% 12.88/2.12 spl40_37 <=> sK10(sK38,sK39,f__integer__(0)) = f__integer__(sK22(sK38,sK39,f__integer__(0)))),
% 12.88/2.12 introduced(definition,[new_symbols(definition,[spl40_37])],[avatar_definition])).
% 12.88/2.12 tff(f1057,plain,(
% 12.88/2.12 sK10(sK38,sK39,f__integer__(0)) = f__integer__(sK22(sK38,sK39,f__integer__(0))) | ~spl40_37),
% 12.88/2.12 inference(avatar_component_clause,[],[f1055])).
% 12.88/2.12 tff(f1058,plain,(
% 12.88/2.12 spl40_37 | spl40_6 | spl40_29 | ~spl40_7 | ~spl40_9),
% 12.88/2.12 inference(avatar_split_clause,[],[f1053,f538,f516,f899,f512,f1055])).
% 12.88/2.12 tff(f1059,plain,(
% 12.88/2.12 sP29(sK26(sK38,sK39,f__integer__(0)),sK25(sK38,sK39,f__integer__(0)),sK24(sK38,sK39,f__integer__(0)),sK13(sK38,sK39,f__integer__(0)),sK12(sK38,sK39,f__integer__(0)),sK11(sK38,sK39,f__integer__(0))) | sP16(sK15(sK38,sK39,f__integer__(0)),sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38) | f__integer__(0) = f__integer__($sum(sK22(sK38,sK39,f__integer__(0)),sK23(sK38,sK39,f__integer__(0))))),
% 12.88/2.12 inference(resolution,[],[f145,f183])).
% 12.88/2.12 tff(f1061,plain,(
% 12.88/2.12 sP29(sK26(sK38,sK39,f__integer__(0)),sK25(sK38,sK39,f__integer__(0)),sK24(sK38,sK39,f__integer__(0)),sK13(sK38,sK39,f__integer__(0)),sK12(sK38,sK39,f__integer__(0)),sK38) | sP16(sK15(sK38,sK39,f__integer__(0)),sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38) | f__integer__(0) = f__integer__($sum(sK22(sK38,sK39,f__integer__(0)),sK23(sK38,sK39,f__integer__(0)))) | ~spl40_7),
% 12.88/2.12 inference(forward_demodulation,[],[f1059,f518])).
% 12.88/2.12 tff(f1062,plain,(
% 12.88/2.12 sP29(sK26(sK38,sK39,f__integer__(0)),sK25(sK38,sK39,f__integer__(0)),sK24(sK38,sK39,f__integer__(0)),sK13(sK38,sK39,f__integer__(0)),sK39,sK38) | sP16(sK15(sK38,sK39,f__integer__(0)),sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38) | f__integer__(0) = f__integer__($sum(sK22(sK38,sK39,f__integer__(0)),sK23(sK38,sK39,f__integer__(0)))) | (~spl40_7 | ~spl40_9)),
% 12.88/2.12 inference(forward_demodulation,[],[f1061,f540])).
% 12.88/2.12 tff(f1064,definition,(
% 12.88/2.12 spl40_38 <=> f__integer__(0) = f__integer__($sum(sK22(sK38,sK39,f__integer__(0)),sK23(sK38,sK39,f__integer__(0))))),
% 12.88/2.12 introduced(definition,[new_symbols(definition,[spl40_38])],[avatar_definition])).
% 12.88/2.12 tff(f1065,plain,(
% 12.88/2.12 f__integer__(0) != f__integer__($sum(sK22(sK38,sK39,f__integer__(0)),sK23(sK38,sK39,f__integer__(0)))) | spl40_38),
% 12.88/2.12 inference(avatar_component_clause,[],[f1064])).
% 12.88/2.12 tff(f1066,plain,(
% 12.88/2.12 f__integer__(0) = f__integer__($sum(sK22(sK38,sK39,f__integer__(0)),sK23(sK38,sK39,f__integer__(0)))) | ~spl40_38),
% 12.88/2.12 inference(avatar_component_clause,[],[f1064])).
% 12.88/2.12 tff(f1067,plain,(
% 12.88/2.12 spl40_38 | spl40_6 | spl40_29 | ~spl40_7 | ~spl40_9),
% 12.88/2.12 inference(avatar_split_clause,[],[f1062,f538,f516,f899,f512,f1064])).
% 12.88/2.12 tff(f1104,plain,(
% 12.88/2.12 ~goto(sK24(sK38,sK39,f__integer__(0)),sK25(sK38,sK39,f__integer__(0)),sK26(sK38,sK39,f__integer__(0))) | ~spl40_29),
% 12.88/2.12 inference(resolution,[],[f901,f234])).
% 12.88/2.12 tff(f1105,plain,(
% 12.88/2.12 sK38 = sK24(sK38,sK39,f__integer__(0)) | ~spl40_29),
% 12.88/2.12 inference(resolution,[],[f901,f133])).
% 12.88/2.12 tff(f1106,plain,(
% 12.88/2.12 sK39 = sK25(sK38,sK39,f__integer__(0)) | ~spl40_29),
% 12.88/2.12 inference(resolution,[],[f901,f132])).
% 12.88/2.12 tff(f1943,plain,(
% 12.88/2.12 ( ! [X0 : $int,X1 : $int] : ($less(X1,X0) | $less(X0,X1) | f__integer__(X1) = f__integer__(X0)) )),
% 12.88/2.12 inference(resolution,[],[f324,f72])).
% 12.88/2.12 tff(f3240,plain,(
% 12.88/2.12 ~goto(sK24(sK38,sK39,f__integer__(0)),sK39,sK26(sK38,sK39,f__integer__(0))) | ~spl40_29),
% 12.88/2.12 inference(forward_demodulation,[],[f1104,f1106])).
% 12.88/2.12 tff(f3241,plain,(
% 12.88/2.12 ~goto(sK38,sK39,sK26(sK38,sK39,f__integer__(0))) | ~spl40_29),
% 12.88/2.12 inference(forward_demodulation,[],[f3240,f1105])).
% 12.88/2.12 tff(f3242,plain,(
% 12.88/2.12 ~person(sK38) | ~spl40_29),
% 12.88/2.12 inference(resolution,[],[f3241,f220])).
% 12.88/2.12 tff(f3243,plain,(
% 12.88/2.12 $false | ~spl40_29),
% 12.88/2.12 inference(forward_subsumption_resolution,[],[f3242,f249])).
% 12.88/2.12 tff(f3244,plain,(
% 12.88/2.12 ~spl40_29),
% 12.88/2.12 inference(avatar_contradiction_clause,[],[f3243])).
% 12.88/2.12 tff(f3263,definition,(
% 12.88/2.12 spl40_46 <=> $less(0,sK35(sK38,sK39,f__integer__(0)))),
% 12.88/2.12 introduced(definition,[new_symbols(definition,[spl40_46])],[avatar_definition])).
% 12.88/2.12 tff(f3265,plain,(
% 12.88/2.12 $less(0,sK35(sK38,sK39,f__integer__(0))) | ~spl40_46),
% 12.88/2.12 inference(avatar_component_clause,[],[f3263])).
% 12.88/2.12 tff(f3292,plain,(
% 12.88/2.12 ~p__less_equal__(f__integer__(sK35(sK38,sK39,f__integer__(0))),f__integer__(0)) | ~spl40_46),
% 12.88/2.12 inference(resolution,[],[f3265,f73])).
% 12.88/2.12 tff(f3311,plain,(
% 12.88/2.12 sK17(sK38,sK39,f__integer__(0)) = f__integer__(sK35(sK38,sK39,f__integer__(0))) | (~spl40_34 | ~spl40_36)),
% 12.88/2.12 inference(forward_demodulation,[],[f1048,f1030])).
% 12.88/2.12 tff(f3312,plain,(
% 12.88/2.12 sK10(sK38,sK39,f__integer__(0)) = f__integer__(sK35(sK38,sK39,f__integer__(0))) | (~spl40_34 | ~spl40_35 | ~spl40_36)),
% 12.88/2.12 inference(forward_demodulation,[],[f3311,f1039])).
% 12.88/2.12 tff(f3627,plain,(
% 12.88/2.12 f__integer__(0) = f__integer__($sum(sK22(sK38,sK39,f__integer__(0)),1)) | (~spl40_13 | ~spl40_38)),
% 12.88/2.12 inference(forward_demodulation,[],[f1066,f600])).
% 12.88/2.12 tff(f3628,plain,(
% 12.88/2.12 f__integer__(0) = f__integer__($sum(1,sK22(sK38,sK39,f__integer__(0)))) | (~spl40_13 | ~spl40_38)),
% 12.88/2.12 inference(forward_demodulation,[],[f3627,f31])).
% 12.88/2.12 tff(f3630,plain,(
% 12.88/2.12 p__less_equal__(f__integer__(sK22(sK38,sK39,f__integer__(0))),f__integer__(0)) | (~spl40_13 | ~spl40_38)),
% 12.88/2.12 inference(superposition,[],[f458,f3628])).
% 12.88/2.12 tff(f3631,plain,(
% 12.88/2.12 ~p__less_equal__(f__integer__(0),f__integer__(sK22(sK38,sK39,f__integer__(0)))) | (~spl40_13 | ~spl40_38)),
% 12.88/2.12 inference(superposition,[],[f270,f3628])).
% 12.88/2.12 tff(f3678,plain,(
% 12.88/2.12 ~p__less_equal__(f__integer__(0),sK10(sK38,sK39,f__integer__(0))) | (~spl40_13 | ~spl40_37 | ~spl40_38)),
% 12.88/2.12 inference(forward_demodulation,[],[f3631,f1057])).
% 12.88/2.12 tff(f3679,plain,(
% 12.88/2.12 p__less_equal__(sK10(sK38,sK39,f__integer__(0)),f__integer__(0)) | (~spl40_13 | ~spl40_37 | ~spl40_38)),
% 12.88/2.12 inference(forward_demodulation,[],[f3630,f1057])).
% 12.88/2.12 tff(f4443,definition,(
% 12.88/2.12 spl40_101 <=> f__integer__(0) = sK10(sK38,sK39,f__integer__(0))),
% 12.88/2.12 introduced(definition,[new_symbols(definition,[spl40_101])],[avatar_definition])).
% 12.88/2.12 tff(f4444,plain,(
% 12.88/2.12 f__integer__(0) = sK10(sK38,sK39,f__integer__(0)) | ~spl40_101),
% 12.88/2.12 inference(avatar_component_clause,[],[f4443])).
% 12.88/2.12 tff(f4506,definition,(
% 12.88/2.12 spl40_104 <=> p__less_equal__(sK10(sK38,sK39,f__integer__(0)),f__integer__(0))),
% 12.88/2.12 introduced(definition,[new_symbols(definition,[spl40_104])],[avatar_definition])).
% 12.88/2.12 tff(f4528,definition,(
% 12.88/2.12 spl40_106 <=> p__less_equal__(f__integer__(0),sK10(sK38,sK39,f__integer__(0)))),
% 12.88/2.12 introduced(definition,[new_symbols(definition,[spl40_106])],[avatar_definition])).
% 12.88/2.12 tff(f4529,plain,(
% 12.88/2.12 ~p__less_equal__(f__integer__(0),sK10(sK38,sK39,f__integer__(0))) | spl40_106),
% 12.88/2.12 inference(avatar_component_clause,[],[f4528])).
% 12.88/2.12 tff(f4699,plain,(
% 12.88/2.12 sP29(sK26(sK38,sK39,f__integer__(0)),sK25(sK38,sK39,f__integer__(0)),sK24(sK38,sK39,f__integer__(0)),sK13(sK38,sK39,f__integer__(0)),sK12(sK38,sK39,f__integer__(0)),sK11(sK38,sK39,f__integer__(0))) | 0 = sK33(sK38,sK39,f__integer__(0)) | spl40_6),
% 12.88/2.12 inference(forward_subsumption_resolution,[],[f925,f513])).
% 12.88/2.12 tff(f4716,plain,(
% 12.88/2.12 sP29(sK26(sK38,sK39,f__integer__(0)),sK25(sK38,sK39,f__integer__(0)),sK24(sK38,sK39,f__integer__(0)),sK13(sK38,sK39,f__integer__(0)),sK12(sK38,sK39,f__integer__(0)),sK38) | 0 = sK33(sK38,sK39,f__integer__(0)) | (spl40_6 | ~spl40_7)),
% 12.88/2.12 inference(forward_demodulation,[],[f4699,f518])).
% 12.88/2.12 tff(f4733,plain,(
% 12.88/2.12 sP29(sK26(sK38,sK39,f__integer__(0)),sK25(sK38,sK39,f__integer__(0)),sK24(sK38,sK39,f__integer__(0)),sK13(sK38,sK39,f__integer__(0)),sK39,sK38) | 0 = sK33(sK38,sK39,f__integer__(0)) | (spl40_6 | ~spl40_7 | ~spl40_9)),
% 12.88/2.12 inference(forward_demodulation,[],[f4716,f540])).
% 12.88/2.12 tff(f4743,plain,(
% 12.88/2.12 0 = sK33(sK38,sK39,f__integer__(0)) | (spl40_6 | ~spl40_7 | ~spl40_9 | spl40_29)),
% 12.88/2.12 inference(forward_subsumption_resolution,[],[f4733,f900])).
% 12.88/2.12 tff(f4750,plain,(
% 12.88/2.12 spl40_8 | spl40_6 | ~spl40_7 | ~spl40_9 | spl40_29),
% 12.88/2.12 inference(avatar_split_clause,[],[f4743,f899,f538,f516,f512,f534])).
% 12.88/2.12 tff(f4763,plain,(
% 12.88/2.12 ~$less(sK35(sK38,sK39,f__integer__(0)),0) | sP16(sK15(sK38,sK39,f__integer__(0)),sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38) | (~spl40_7 | ~spl40_8 | ~spl40_9 | spl40_29)),
% 12.88/2.12 inference(forward_subsumption_resolution,[],[f988,f900])).
% 12.88/2.12 tff(f4780,plain,(
% 12.88/2.12 ~$less(sK35(sK38,sK39,f__integer__(0)),0) | (spl40_6 | ~spl40_7 | ~spl40_8 | ~spl40_9 | spl40_29)),
% 12.88/2.12 inference(forward_subsumption_resolution,[],[f4763,f513])).
% 12.88/2.12 tff(f4856,plain,(
% 12.88/2.12 ~$less(sK35(sK38,sK39,f__integer__(0)),0) | sK38 = sK11(sK38,sK39,f__integer__(0)) | sP16(sK15(sK38,sK39,f__integer__(0)),sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38) | ~in(sK38,sK39,f__integer__(0)) | ~spl40_8),
% 12.88/2.12 inference(superposition,[],[f118,f536])).
% 12.88/2.12 tff(f4857,plain,(
% 12.88/2.12 ~$less(sK35(sK38,sK39,f__integer__(0)),0) | sK39 = sK12(sK38,sK39,f__integer__(0)) | sP16(sK15(sK38,sK39,f__integer__(0)),sK14(sK38,sK39,f__integer__(0)),f__integer__(0),sK39,sK38) | ~in(sK38,sK39,f__integer__(0)) | ~spl40_8),
% 12.88/2.12 inference(superposition,[],[f114,f536])).
% 12.88/2.12 tff(f5116,plain,(
% 12.88/2.12 ~spl40_18 | spl40_6 | ~spl40_7 | ~spl40_8 | ~spl40_9 | spl40_29),
% 12.88/2.12 inference(avatar_split_clause,[],[f4780,f899,f538,f534,f516,f512,f644])).
% 12.88/2.12 tff(f10153,plain,(
% 12.88/2.12 $less(0,sK35(sK38,sK39,f__integer__(0))) | f__integer__(0) = f__integer__(sK35(sK38,sK39,f__integer__(0))) | spl40_18),
% 12.88/2.12 inference(resolution,[],[f1943,f646])).
% 12.88/2.12 tff(f59880,plain,(
% 12.88/2.12 f__integer__(0) = sK10(sK38,sK39,f__integer__(0)) | $less(0,sK35(sK38,sK39,f__integer__(0))) | (spl40_18 | ~spl40_34 | ~spl40_35 | ~spl40_36)),
% 12.88/2.12 inference(forward_demodulation,[],[f10153,f3312])).
% 12.88/2.12 tff(f59882,plain,(
% 12.88/2.12 spl40_46 | spl40_101 | spl40_18 | ~spl40_34 | ~spl40_35 | ~spl40_36),
% 12.88/2.12 inference(avatar_split_clause,[],[f59880,f1046,f1037,f1028,f644,f4443,f3263])).
% 12.88/2.12 tff(f93932,plain,(
% 12.88/2.12 ~p__less_equal__(f__integer__(0),f__integer__(0)) | (~spl40_101 | spl40_106)),
% 12.88/2.12 inference(forward_demodulation,[],[f4529,f4444])).
% 12.88/2.12 tff(f93933,plain,(
% 12.88/2.12 $false | (~spl40_101 | spl40_106)),
% 12.88/2.12 inference(forward_subsumption_resolution,[],[f93932,f251])).
% 12.88/2.12 tff(f93934,plain,(
% 12.88/2.12 ~spl40_101 | spl40_106),
% 12.88/2.12 inference(avatar_contradiction_clause,[],[f93933])).
% 12.88/2.12 tff(f95358,plain,(
% 12.88/2.12 ~p__less_equal__(sK10(sK38,sK39,f__integer__(0)),f__integer__(0)) | (~spl40_34 | ~spl40_35 | ~spl40_36 | ~spl40_46)),
% 12.88/2.12 inference(forward_demodulation,[],[f3292,f3312])).
% 12.88/2.12 tff(f95529,plain,(
% 12.88/2.12 ~spl40_104 | ~spl40_34 | ~spl40_35 | ~spl40_36 | ~spl40_46),
% 12.88/2.12 inference(avatar_split_clause,[],[f95358,f3263,f1046,f1037,f1028,f4506])).
% 12.88/2.12 tff(f98494,plain,(
% 12.88/2.12 sK39 = sK12(sK38,sK39,f__integer__(0)) | sK18(sK38,sK39,f__integer__(0)) = f__integer__(sK35(sK38,sK39,f__integer__(0))) | spl40_6),
% 12.88/2.12 inference(forward_subsumption_resolution,[],[f699,f513])).
% 12.88/2.12 tff(f98495,plain,(
% 12.88/2.12 sK39 = sK12(sK38,sK39,f__integer__(0)) | sK10(sK38,sK39,f__integer__(0)) = f__integer__(sK22(sK38,sK39,f__integer__(0))) | spl40_6),
% 12.88/2.12 inference(forward_subsumption_resolution,[],[f710,f513])).
% 12.88/2.12 tff(f98496,plain,(
% 12.88/2.12 sK39 = sK12(sK38,sK39,f__integer__(0)) | f__integer__(0) = f__integer__($sum(sK22(sK38,sK39,f__integer__(0)),sK23(sK38,sK39,f__integer__(0)))) | spl40_6),
% 12.88/2.12 inference(forward_subsumption_resolution,[],[f738,f513])).
% 12.88/2.12 tff(f98563,plain,(
% 12.88/2.12 spl40_37 | spl40_9 | spl40_6),
% 12.88/2.12 inference(avatar_split_clause,[],[f98495,f512,f538,f1055])).
% 12.88/2.12 tff(f98564,plain,(
% 12.88/2.12 f__integer__(0) = f__integer__($sum(sK22(sK38,sK39,f__integer__(0)),1)) | sK39 = sK12(sK38,sK39,f__integer__(0)) | (spl40_6 | ~spl40_13)),
% 12.88/2.12 inference(forward_demodulation,[],[f98496,f600])).
% 12.88/2.12 tff(f98605,plain,(
% 12.88/2.12 f__integer__(0) = f__integer__($sum(1,sK22(sK38,sK39,f__integer__(0)))) | sK39 = sK12(sK38,sK39,f__integer__(0)) | (spl40_6 | ~spl40_13)),
% 12.88/2.12 inference(forward_demodulation,[],[f98564,f31])).
% 12.88/2.12 tff(f98642,plain,(
% 12.88/2.12 ~spl40_106 | ~spl40_13 | ~spl40_37 | ~spl40_38),
% 12.88/2.12 inference(avatar_split_clause,[],[f3678,f1064,f1055,f598,f4528])).
% 12.88/2.12 tff(f98643,plain,(
% 12.88/2.12 spl40_104 | ~spl40_13 | ~spl40_37 | ~spl40_38),
% 12.88/2.12 inference(avatar_split_clause,[],[f3679,f1064,f1055,f598,f4506])).
% 12.88/2.12 tff(f99214,plain,(
% 12.88/2.12 f__integer__(0) != f__integer__($sum(sK22(sK38,sK39,f__integer__(0)),1)) | (~spl40_13 | spl40_38)),
% 12.88/2.12 inference(forward_demodulation,[],[f1065,f600])).
% 12.88/2.12 tff(f99343,definition,(
% 12.88/2.12 spl40_770 <=> f__integer__(0) = f__integer__($sum(1,sK22(sK38,sK39,f__integer__(0))))),
% 12.88/2.12 introduced(definition,[new_symbols(definition,[spl40_770])],[avatar_definition])).
% 12.88/2.12 tff(f99571,plain,(
% 12.88/2.12 f__integer__(0) != f__integer__($sum(1,sK22(sK38,sK39,f__integer__(0)))) | (~spl40_13 | spl40_38)),
% 12.88/2.12 inference(forward_demodulation,[],[f99214,f31])).
% 12.88/2.12 tff(f99667,plain,(
% 12.88/2.12 ~spl40_770 | ~spl40_13 | spl40_38),
% 12.88/2.12 inference(avatar_split_clause,[],[f99571,f1064,f598,f99343])).
% 12.88/2.12 tff(f100074,plain,(
% 12.88/2.12 ~$less(sK35(sK38,sK39,f__integer__(0)),0) | sK39 = sK12(sK38,sK39,f__integer__(0)) | ~in(sK38,sK39,f__integer__(0)) | (spl40_6 | ~spl40_8)),
% 12.88/2.12 inference(forward_subsumption_resolution,[],[f4857,f513])).
% 12.88/2.12 tff(f100075,plain,(
% 12.88/2.12 sK39 = sK12(sK38,sK39,f__integer__(0)) | sK10(sK38,sK39,f__integer__(0)) = sK17(sK38,sK39,f__integer__(0)) | spl40_6),
% 12.88/2.12 inference(forward_subsumption_resolution,[],[f689,f513])).
% 12.88/2.12 tff(f100077,plain,(
% 12.88/2.12 sK39 = sK12(sK38,sK39,f__integer__(0)) | sK17(sK38,sK39,f__integer__(0)) = sK18(sK38,sK39,f__integer__(0)) | spl40_6),
% 12.88/2.12 inference(forward_subsumption_resolution,[],[f679,f513])).
% 12.88/2.12 tff(f100080,plain,(
% 12.88/2.12 spl40_9 | spl40_770 | spl40_6 | ~spl40_13),
% 12.88/2.12 inference(avatar_split_clause,[],[f98605,f598,f512,f99343,f538])).
% 12.88/2.12 tff(f100086,plain,(
% 12.88/2.12 spl40_36 | spl40_9 | spl40_6),
% 12.88/2.12 inference(avatar_split_clause,[],[f98494,f512,f538,f1046])).
% 12.88/2.12 tff(f100089,plain,(
% 12.88/2.12 sK38 = sK11(sK38,sK39,f__integer__(0)) | sK17(sK38,sK39,f__integer__(0)) = sK18(sK38,sK39,f__integer__(0)) | spl40_6),
% 12.88/2.12 inference(forward_subsumption_resolution,[],[f675,f513])).
% 12.88/2.12 tff(f100090,plain,(
% 12.88/2.12 sK38 = sK11(sK38,sK39,f__integer__(0)) | sK10(sK38,sK39,f__integer__(0)) = sK17(sK38,sK39,f__integer__(0)) | spl40_6),
% 12.88/2.12 inference(forward_subsumption_resolution,[],[f677,f513])).
% 12.88/2.12 tff(f100091,plain,(
% 12.88/2.12 sK38 = sK11(sK38,sK39,f__integer__(0)) | sK18(sK38,sK39,f__integer__(0)) = f__integer__(sK35(sK38,sK39,f__integer__(0))) | spl40_6),
% 12.88/2.12 inference(forward_subsumption_resolution,[],[f701,f513])).
% 12.88/2.12 tff(f100092,plain,(
% 12.88/2.12 sK38 = sK11(sK38,sK39,f__integer__(0)) | sK10(sK38,sK39,f__integer__(0)) = f__integer__(sK22(sK38,sK39,f__integer__(0))) | spl40_6),
% 12.88/2.12 inference(forward_subsumption_resolution,[],[f703,f513])).
% 12.88/2.12 tff(f100093,plain,(
% 12.88/2.12 sK38 = sK11(sK38,sK39,f__integer__(0)) | f__integer__(0) = f__integer__($sum(sK22(sK38,sK39,f__integer__(0)),sK23(sK38,sK39,f__integer__(0)))) | spl40_6),
% 12.88/2.12 inference(forward_subsumption_resolution,[],[f712,f513])).
% 12.88/2.12 tff(f100110,plain,(
% 12.88/2.12 ~$less(sK35(sK38,sK39,f__integer__(0)),0) | sK38 = sK11(sK38,sK39,f__integer__(0)) | ~in(sK38,sK39,f__integer__(0)) | (spl40_6 | ~spl40_8)),
% 12.88/2.12 inference(forward_subsumption_resolution,[],[f4856,f513])).
% 12.88/2.12 tff(f100149,plain,(
% 12.88/2.12 ~$less(sK35(sK38,sK39,f__integer__(0)),0) | sK39 = sK12(sK38,sK39,f__integer__(0)) | (spl40_6 | ~spl40_8)),
% 12.88/2.12 inference(forward_subsumption_resolution,[],[f100074,f183])).
% 12.88/2.12 tff(f100150,plain,(
% 12.88/2.12 spl40_35 | spl40_9 | spl40_6),
% 12.88/2.12 inference(avatar_split_clause,[],[f100075,f512,f538,f1037])).
% 12.88/2.12 tff(f100151,plain,(
% 12.88/2.12 spl40_34 | spl40_9 | spl40_6),
% 12.88/2.12 inference(avatar_split_clause,[],[f100077,f512,f538,f1028])).
% 12.88/2.12 tff(f100155,plain,(
% 12.88/2.12 spl40_34 | spl40_7 | spl40_6),
% 12.88/2.12 inference(avatar_split_clause,[],[f100089,f512,f516,f1028])).
% 12.88/2.12 tff(f100156,plain,(
% 12.88/2.12 spl40_35 | spl40_7 | spl40_6),
% 12.88/2.12 inference(avatar_split_clause,[],[f100090,f512,f516,f1037])).
% 12.88/2.12 tff(f100157,plain,(
% 12.88/2.12 spl40_36 | spl40_7 | spl40_6),
% 12.88/2.12 inference(avatar_split_clause,[],[f100091,f512,f516,f1046])).
% 12.88/2.12 tff(f100158,plain,(
% 12.88/2.12 spl40_37 | spl40_7 | spl40_6),
% 12.88/2.12 inference(avatar_split_clause,[],[f100092,f512,f516,f1055])).
% 12.88/2.12 tff(f100159,plain,(
% 12.88/2.12 f__integer__(0) = f__integer__($sum(sK22(sK38,sK39,f__integer__(0)),1)) | sK38 = sK11(sK38,sK39,f__integer__(0)) | (spl40_6 | ~spl40_13)),
% 12.88/2.12 inference(forward_demodulation,[],[f100093,f600])).
% 12.88/2.12 tff(f100178,plain,(
% 12.88/2.12 ~$less(sK35(sK38,sK39,f__integer__(0)),0) | sK38 = sK11(sK38,sK39,f__integer__(0)) | (spl40_6 | ~spl40_8)),
% 12.88/2.12 inference(forward_subsumption_resolution,[],[f100110,f183])).
% 12.88/2.12 tff(f100194,plain,(
% 12.88/2.12 spl40_9 | ~spl40_18 | spl40_6 | ~spl40_8),
% 12.88/2.12 inference(avatar_split_clause,[],[f100149,f534,f512,f644,f538])).
% 12.88/2.12 tff(f100196,plain,(
% 12.88/2.12 f__integer__(0) = f__integer__($sum(1,sK22(sK38,sK39,f__integer__(0)))) | sK38 = sK11(sK38,sK39,f__integer__(0)) | (spl40_6 | ~spl40_13)),
% 12.88/2.12 inference(forward_demodulation,[],[f100159,f31])).
% 12.88/2.12 tff(f100207,plain,(
% 12.88/2.12 spl40_7 | ~spl40_18 | spl40_6 | ~spl40_8),
% 12.88/2.12 inference(avatar_split_clause,[],[f100178,f534,f512,f644,f516])).
% 12.88/2.12 tff(f100220,plain,(
% 12.88/2.12 spl40_7 | spl40_770 | spl40_6 | ~spl40_13),
% 12.88/2.12 inference(avatar_split_clause,[],[f100196,f598,f512,f99343,f516])).
% 12.88/2.12 cnf(s6, plain, spl40_6 | spl40_8 | spl40_9, inference(sat_conversion,[],[f541])).
% 12.88/2.12 cnf(s7, plain, spl40_6 | spl40_7 | spl40_8, inference(sat_conversion,[],[f544])).
% 12.88/2.12 cnf(s10, plain, spl40_12, inference(sat_conversion,[],[f596])).
% 12.88/2.12 cnf(s11, plain, spl40_6 | spl40_7 | spl40_13, inference(sat_conversion,[],[f601])).
% 12.88/2.12 cnf(s12, plain, spl40_6 | spl40_9 | spl40_13, inference(sat_conversion,[],[f602])).
% 12.88/2.12 cnf(s32, plain, ~spl40_6 | spl40_10 | ~spl40_12, inference(sat_conversion,[],[f907])).
% 12.88/2.12 cnf(s36, plain, ~spl40_6 | ~spl40_10, inference(sat_conversion,[],[f918])).
% 12.88/2.12 cnf(s42, plain, spl40_6 | ~spl40_7 | ~spl40_9 | spl40_13 | spl40_29, inference(sat_conversion,[],[f961])).
% 12.88/2.12 cnf(s49, plain, spl40_6 | ~spl40_7 | ~spl40_9 | spl40_29 | spl40_34, inference(sat_conversion,[],[f1031])).
% 12.88/2.12 cnf(s50, plain, spl40_6 | ~spl40_7 | ~spl40_9 | spl40_29 | spl40_35, inference(sat_conversion,[],[f1040])).
% 12.88/2.12 cnf(s51, plain, spl40_6 | ~spl40_7 | ~spl40_9 | spl40_29 | spl40_36, inference(sat_conversion,[],[f1049])).
% 12.88/2.12 cnf(s52, plain, spl40_6 | ~spl40_7 | ~spl40_9 | spl40_29 | spl40_37, inference(sat_conversion,[],[f1058])).
% 12.88/2.12 cnf(s53, plain, spl40_6 | ~spl40_7 | ~spl40_9 | spl40_29 | spl40_38, inference(sat_conversion,[],[f1067])).
% 12.88/2.12 cnf(s59, plain, ~spl40_29, inference(sat_conversion,[],[f3244])).
% 12.88/2.12 cnf(s199, plain, spl40_6 | ~spl40_7 | spl40_8 | ~spl40_9 | spl40_29, inference(sat_conversion,[],[f4750])).
% 12.88/2.12 cnf(s247, plain, spl40_6 | ~spl40_7 | ~spl40_8 | ~spl40_9 | ~spl40_18 | spl40_29, inference(sat_conversion,[],[f5116])).
% 12.88/2.12 cnf(s591, plain, spl40_18 | ~spl40_34 | ~spl40_35 | ~spl40_36 | spl40_46 | spl40_101, inference(sat_conversion,[],[f59882])).
% 12.88/2.12 cnf(s1319, plain, ~spl40_101 | spl40_106, inference(sat_conversion,[],[f93934])).
% 12.88/2.12 cnf(s1698, plain, ~spl40_34 | ~spl40_35 | ~spl40_36 | ~spl40_46 | ~spl40_104, inference(sat_conversion,[],[f95529])).
% 12.88/2.12 cnf(s2355, plain, spl40_6 | spl40_9 | spl40_37, inference(sat_conversion,[],[f98563])).
% 12.88/2.12 cnf(s2361, plain, ~spl40_13 | ~spl40_37 | ~spl40_38 | ~spl40_106, inference(sat_conversion,[],[f98642])).
% 12.88/2.12 cnf(s2362, plain, ~spl40_13 | ~spl40_37 | ~spl40_38 | spl40_104, inference(sat_conversion,[],[f98643])).
% 12.88/2.12 cnf(s2795, plain, ~spl40_13 | spl40_38 | ~spl40_770, inference(sat_conversion,[],[f99667])).
% 12.88/2.12 cnf(s3211, plain, spl40_6 | spl40_9 | ~spl40_13 | spl40_770, inference(sat_conversion,[],[f100080])).
% 12.88/2.12 cnf(s3216, plain, spl40_6 | spl40_9 | spl40_36, inference(sat_conversion,[],[f100086])).
% 12.88/2.12 cnf(s3230, plain, spl40_6 | spl40_9 | spl40_35, inference(sat_conversion,[],[f100150])).
% 12.88/2.12 cnf(s3231, plain, spl40_6 | spl40_9 | spl40_34, inference(sat_conversion,[],[f100151])).
% 12.88/2.12 cnf(s3232, plain, spl40_6 | spl40_7 | spl40_34, inference(sat_conversion,[],[f100155])).
% 12.88/2.12 cnf(s3233, plain, spl40_6 | spl40_7 | spl40_35, inference(sat_conversion,[],[f100156])).
% 12.88/2.12 cnf(s3234, plain, spl40_6 | spl40_7 | spl40_36, inference(sat_conversion,[],[f100157])).
% 12.88/2.12 cnf(s3235, plain, spl40_6 | spl40_7 | spl40_37, inference(sat_conversion,[],[f100158])).
% 12.88/2.12 cnf(s3241, plain, spl40_6 | ~spl40_8 | spl40_9 | ~spl40_18, inference(sat_conversion,[],[f100194])).
% 12.88/2.12 cnf(s3246, plain, spl40_6 | spl40_7 | ~spl40_8 | ~spl40_18, inference(sat_conversion,[],[f100207])).
% 12.88/2.12 cnf(s3251, plain, spl40_6 | spl40_7 | ~spl40_13 | spl40_770, inference(sat_conversion,[],[f100220])).
% 12.88/2.12 cnf(s3259, plain, spl40_6 | ~spl40_7 | ~spl40_9 | spl40_38, inference(rat,[],[s53,s59])).
% 12.88/2.12 cnf(s3260, plain, spl40_6 | ~spl40_7 | ~spl40_9 | spl40_37, inference(rat,[],[s52,s59])).
% 12.88/2.12 cnf(s3261, plain, spl40_6 | ~spl40_7 | ~spl40_9 | spl40_36, inference(rat,[],[s51,s59])).
% 12.88/2.12 cnf(s3262, plain, spl40_6 | ~spl40_7 | ~spl40_9 | spl40_35, inference(rat,[],[s50,s59])).
% 12.88/2.12 cnf(s3263, plain, spl40_6 | ~spl40_7 | ~spl40_9 | spl40_34, inference(rat,[],[s49,s59])).
% 12.88/2.12 cnf(s3270, plain, spl40_6 | ~spl40_7 | ~spl40_9 | spl40_13, inference(rat,[],[s42,s59])).
% 12.88/2.12 cnf(s3278, plain, spl40_9 | spl40_6, inference(rat,[],[s591,s1319,s1698,s2361,s2362,s3241,s2795,s3211,s6,s12,s2355,s3216,s3230,s3231])).
% 12.88/2.12 cnf(s3281, plain, ~spl40_6, inference(rat,[],[s32,s36,s10])).
% 12.88/2.12 cnf(s3283, plain, spl40_9, inference(rat,[],[s3278,s3281])).
% 12.88/2.12 cnf(s3284, plain, ~spl40_7, inference(rat,[],[s591,s1319,s1698,s2361,s2362,s247,s3263,s3262,s3261,s3259,s3260,s199,s3270,s3281,s3283,s59])).
% 12.88/2.12 cnf(s3285, plain, spl40_37, inference(rat,[],[s3235,s3281,s3284])).
% 12.88/2.12 cnf(s3286, plain, spl40_36, inference(rat,[],[s3234,s3281,s3284])).
% 12.88/2.12 cnf(s3287, plain, spl40_35, inference(rat,[],[s3233,s3281,s3284])).
% 12.88/2.12 cnf(s3288, plain, spl40_34, inference(rat,[],[s3232,s3281,s3284])).
% 12.88/2.12 cnf(s3292, plain, spl40_13, inference(rat,[],[s11,s3281,s3284])).
% 12.88/2.12 cnf(s3293, plain, spl40_8, inference(rat,[],[s7,s3281,s3284])).
% 12.88/2.12 cnf(s3296, plain, spl40_770, inference(rat,[],[s3251,s3284,s3281,s3292])).
% 12.88/2.12 cnf(s3297, plain, spl40_38, inference(rat,[],[s2795,s3296,s3292])).
% 12.88/2.12 cnf(s3298, plain, ~spl40_18, inference(rat,[],[s3246,s3284,s3281,s3293])).
% 12.88/2.12 cnf(s3308, plain, spl40_104, inference(rat,[],[s2362,s3292,s3285,s3297])).
% 12.88/2.12 cnf(s3309, plain, ~spl40_106, inference(rat,[],[s2361,s3292,s3285,s3297])).
% 12.88/2.12 cnf(s3381, plain, ~spl40_46, inference(rat,[],[s1698,s3286,s3288,s3287,s3308])).
% 12.88/2.12 cnf(s3382, plain, ~spl40_101, inference(rat,[],[s1319,s3309])).
% 12.88/2.12 cnf(s3387, plain, $false, inference(rat,[],[s591,s3298,s3288,s3286,s3287,s3382,s3381])).
% 12.88/2.12 tff(f100231,plain,(
% 12.88/2.12 $false),
% 12.88/2.12 inference(avatar_sat_refutation,[],[s3387])).
% 12.88/2.12 % SZS output end Proof for theBenchmark
% 12.88/2.12 % (1246345)------------------------------
% 12.88/2.12 % (1246345)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.88/2.12 % (1246345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.88/2.12 % (1246345)CaDiCaL version: 2.1.3
% 12.88/2.12 % (1246345)Termination reason: Refutation
% 12.88/2.12 % (1246345)Time elapsed: 1.856 s
% 12.88/2.12 % (1246345)Peak memory usage: 48 MB
% 12.88/2.12 % (1246345)Instructions burned: 6801 (million)
% 12.88/2.12 % (1246339)Success in time 1.891 s
% 12.88/2.12 % Vampire exiting
%------------------------------------------------------------------------------