%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWX073_1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:46:26 PM UTC 2026
% Result : Theorem 184.43s 41.41s
% Output : Refutation 184.43s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX073_1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.25 % Computer : n002.cluster.edu
% 0.11/0.25 % Model : x86_64 x86_64
% 0.11/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.25 % Memory : 8046.5625MB
% 0.11/0.25 % OS : Linux 6.8.0-71-generic
% 0.11/0.25 % CPULimit : 300
% 0.11/0.25 % WCLimit : 300
% 0.11/0.25 % DateTime : Mon Sep 28 15:02:52 UTC 2026
% 0.11/0.25 % CPUTime :
% 0.11/0.25 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.29 Running first-order model finding
% 0.11/0.29 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.07/1.19 % (419171)Will run a generic schedule for satisfiability detection.
% 6.07/1.19 % (419180)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=793195952:i=116_3000 on theBenchmark for (3000ds/116Mi)
% 6.07/1.19 % (419179)dis+10_1_sil=32000:sp=arity:random_seed=1409591442:i=103:fgj=on_3000 on theBenchmark for (3000ds/103Mi)
% 6.07/1.19 % (419181)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1372835733:i=131_3000 on theBenchmark for (3000ds/131Mi)
% 6.07/1.19 % (419176)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3138366102_3000 on theBenchmark for (3000ds/0Mi)
% 6.07/1.19 % (419178)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=925857439:i=88024:add=on:rawr=on_3000 on theBenchmark for (3000ds/88024Mi)
% 6.07/1.19 % (419176)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.07/1.19 % (419176)Terminated due to inappropriate strategy.
% 6.07/1.19 % (419176)------------------------------
% 6.07/1.19 % (419176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.07/1.19 % (419176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.07/1.19 % (419176)CaDiCaL version: 2.1.3
% 6.07/1.19 % (419176)Termination reason: Inappropriate
% 6.07/1.19 % (419176)Time elapsed: 0.002 s
% 6.07/1.19 % (419176)Peak memory usage: 11 MB
% 6.07/1.19 % (419176)Instructions burned: 1 (million)
% 6.07/1.19 % (419176)------------------------------
% 6.07/1.19 % (419176)------------------------------
% 6.07/1.19 % (419177)% WARNING: option uhcvi not known.
% 6.07/1.19 % (419189)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3788695724:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 6.07/1.19 % (419189)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.07/1.19 % (419189)Terminated due to inappropriate strategy.
% 6.07/1.19 % (419189)------------------------------
% 6.07/1.19 % (419189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.07/1.19 % (419189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.07/1.19 % (419189)CaDiCaL version: 2.1.3
% 6.07/1.19 % (419189)Termination reason: Inappropriate
% 6.07/1.19 % (419189)Time elapsed: 0.001 s
% 6.07/1.19 % (419189)Peak memory usage: 11 MB
% 6.07/1.19 % (419189)Instructions burned: 1 (million)
% 6.07/1.19 % (419189)------------------------------
% 6.07/1.19 % (419189)------------------------------
% 6.07/1.19 % (419182)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2464657709:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_3000 on theBenchmark for (3000ds/159Mi)
% 6.07/1.19 % (419177)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3987647326:i=135531:add=off:rawr=on_3000 on theBenchmark for (3000ds/135531Mi)
% 6.07/1.19 % (419191)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3461527502:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 6.07/1.19 % (419180)Instruction limit reached!
% 6.07/1.19 % (419180)------------------------------
% 6.07/1.19 % (419180)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.07/1.19 % (419180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.07/1.19 % (419180)CaDiCaL version: 2.1.3
% 6.07/1.19 % (419180)Termination reason: Instruction limit
% 6.07/1.19 % (419180)Termination phase: Saturation
% 6.07/1.19 % (419180)Time elapsed: 0.097 s
% 6.07/1.19 % (419180)Peak memory usage: 12 MB
% 6.07/1.19 % (419180)Instructions burned: 117 (million)
% 6.07/1.19 % (419179)Instruction limit reached!
% 6.07/1.19 % (419179)------------------------------
% 6.07/1.19 % (419179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.07/1.19 % (419179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.07/1.19 % (419179)CaDiCaL version: 2.1.3
% 6.07/1.19 % (419179)Termination reason: Instruction limit
% 6.07/1.19 % (419179)Termination phase: Saturation
% 6.07/1.19 % (419179)Time elapsed: 0.108 s
% 6.07/1.19 % (419179)Peak memory usage: 12 MB
% 6.07/1.19 % (419179)Instructions burned: 103 (million)
% 6.07/1.19 % (419181)Instruction limit reached!
% 6.07/1.19 % (419181)------------------------------
% 6.07/1.19 % (419181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.07/1.19 % (419181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.07/1.19 % (419181)CaDiCaL version: 2.1.3
% 6.07/1.19 % (419181)Termination reason: Instruction limit
% 6.07/1.19 % (419181)Termination phase: Saturation
% 9.21/1.96 % (419181)Time elapsed: 0.119 s
% 9.21/1.96 % (419181)Peak memory usage: 13 MB
% 9.21/1.96 % (419181)Instructions burned: 131 (million)
% 9.21/1.96 % (419200)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=1436143733:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 9.21/1.96 % (419203)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3648975983:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 9.21/1.96 % (419182)Instruction limit reached!
% 9.21/1.96 % (419182)------------------------------
% 9.21/1.96 % (419182)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.21/1.96 % (419182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.21/1.96 % (419182)CaDiCaL version: 2.1.3
% 9.21/1.96 % (419182)Termination reason: Instruction limit
% 9.21/1.96 % (419182)Termination phase: Saturation
% 9.21/1.96 % (419182)Time elapsed: 0.112 s
% 9.21/1.96 % (419182)Peak memory usage: 13 MB
% 9.21/1.96 % (419182)Instructions burned: 161 (million)
% 9.21/1.96 % (419209)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=476115114:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 9.21/1.96 % (419201)ott-21_1_sil=16000:fs=off:random_seed=2151749381:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 9.21/1.96 % (419209)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 9.21/1.96 % (419209)Terminated due to inappropriate strategy.
% 9.21/1.96 % (419209)------------------------------
% 9.21/1.96 % (419209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.21/1.96 % (419209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.21/1.96 % (419209)CaDiCaL version: 2.1.3
% 9.21/1.96 % (419209)Termination reason: Inappropriate
% 9.21/1.96 % (419209)Time elapsed: 0.001 s
% 9.21/1.96 % (419209)Peak memory usage: 10 MB
% 9.21/1.96 % (419209)Instructions burned: 1 (million)
% 9.21/1.96 % (419209)------------------------------
% 9.21/1.96 % (419209)------------------------------
% 9.21/1.96 % (419212)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2276711325:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 9.21/1.96 % (419191)Instruction limit reached!
% 9.21/1.96 % (419191)------------------------------
% 9.21/1.96 % (419191)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.21/1.96 % (419191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.21/1.96 % (419191)CaDiCaL version: 2.1.3
% 9.21/1.96 % (419191)Termination reason: Instruction limit
% 9.21/1.96 % (419191)Termination phase: Saturation
% 9.21/1.96 % (419191)Time elapsed: 0.137 s
% 9.21/1.96 % (419191)Peak memory usage: 13 MB
% 9.21/1.96 % (419191)Instructions burned: 131 (million)
% 9.21/1.96 % (419215)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2506056889:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 9.21/1.96 % (419215)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 9.21/1.96 % (419215)Terminated due to inappropriate strategy.
% 9.21/1.96 % (419215)------------------------------
% 9.21/1.96 % (419215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.21/1.96 % (419215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.21/1.96 % (419215)CaDiCaL version: 2.1.3
% 9.21/1.96 % (419215)Termination reason: Inappropriate
% 9.21/1.96 % (419215)Time elapsed: 0.001 s
% 9.21/1.96 % (419215)Peak memory usage: 11 MB
% 9.21/1.96 % (419215)Instructions burned: 1 (million)
% 9.21/1.96 % (419215)------------------------------
% 9.21/1.96 % (419215)------------------------------
% 9.21/1.96 % (419219)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=2854082123:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi)
% 9.21/1.96 % (419201)Instruction limit reached!
% 9.21/1.96 % (419201)------------------------------
% 9.21/1.96 % (419201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.21/1.96 % (419201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.21/1.96 % (419201)CaDiCaL version: 2.1.3
% 9.21/1.96 % (419201)Termination reason: Instruction limit
% 9.21/1.96 % (419201)Termination phase: Saturation
% 9.21/1.96 % (419201)Time elapsed: 0.136 s
% 9.21/1.96 % (419201)Peak memory usage: 12 MB
% 9.21/1.96 % (419201)Instructions burned: 181 (million)
% 31.15/4.88 % (419223)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1736381068:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi)
% 31.15/4.88 % (419203)Instruction limit reached!
% 31.15/4.88 % (419203)------------------------------
% 31.15/4.88 % (419203)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.15/4.88 % (419203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.15/4.88 % (419203)CaDiCaL version: 2.1.3
% 31.15/4.88 % (419203)Termination reason: Instruction limit
% 31.15/4.88 % (419203)Termination phase: Saturation
% 31.15/4.88 % (419203)Time elapsed: 0.248 s
% 31.15/4.88 % (419203)Peak memory usage: 14 MB
% 31.15/4.88 % (419203)Instructions burned: 478 (million)
% 31.15/4.88 % (419230)fmb+10_1_sil=64000:random_seed=615741295:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi)
% 31.15/4.88 % (419230)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 31.15/4.88 % (419230)Terminated due to inappropriate strategy.
% 31.15/4.88 % (419230)------------------------------
% 31.15/4.88 % (419230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.15/4.88 % (419230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.15/4.88 % (419230)CaDiCaL version: 2.1.3
% 31.15/4.88 % (419230)Termination reason: Inappropriate
% 31.15/4.88 % (419230)Time elapsed: 0.0000 s
% 31.15/4.88 % (419230)Peak memory usage: 10 MB
% 31.15/4.88 % (419230)Instructions burned: 1 (million)
% 31.15/4.88 % (419230)------------------------------
% 31.15/4.88 % (419230)------------------------------
% 31.15/4.88 % (419232)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2972597307:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi)
% 31.15/4.88 % (419232)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 31.15/4.88 % (419232)Terminated due to inappropriate strategy.
% 31.15/4.88 % (419232)------------------------------
% 31.15/4.88 % (419232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.15/4.88 % (419232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.15/4.88 % (419232)CaDiCaL version: 2.1.3
% 31.15/4.88 % (419232)Termination reason: Inappropriate
% 31.15/4.88 % (419232)Time elapsed: 0.0000 s
% 31.15/4.88 % (419232)Peak memory usage: 10 MB
% 31.15/4.88 % (419232)Instructions burned: 1 (million)
% 31.15/4.88 % (419232)------------------------------
% 31.15/4.88 % (419232)------------------------------
% 31.15/4.88 % (419234)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=542493045:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi)
% 31.15/4.88 % (419234)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 31.15/4.88 % (419234)Terminated due to inappropriate strategy.
% 31.15/4.88 % (419234)------------------------------
% 31.15/4.88 % (419234)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.15/4.88 % (419234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.15/4.88 % (419234)CaDiCaL version: 2.1.3
% 31.15/4.88 % (419234)Termination reason: Inappropriate
% 31.15/4.88 % (419234)Time elapsed: 0.001 s
% 31.15/4.88 % (419234)Peak memory usage: 10 MB
% 31.15/4.88 % (419234)Instructions burned: 1 (million)
% 31.15/4.88 % (419234)------------------------------
% 31.15/4.88 % (419234)------------------------------
% 31.15/4.88 % (419237)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=629463321:i=5131_2995 on theBenchmark for (2995ds/5131Mi)
% 31.15/4.88 % (419200)Instruction limit reached!
% 31.15/4.88 % (419200)------------------------------
% 31.15/4.88 % (419200)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.15/4.88 % (419200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.15/4.88 % (419200)CaDiCaL version: 2.1.3
% 31.15/4.88 % (419200)Termination reason: Instruction limit
% 31.15/4.88 % (419200)Termination phase: Saturation
% 31.15/4.88 % (419200)Time elapsed: 0.634 s
% 31.15/4.88 % (419200)Peak memory usage: 18 MB
% 31.15/4.88 % (419200)Instructions burned: 684 (million)
% 31.15/4.88 % (419256)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=952829475:i=1472:ins=7:fdi=8:gsp=on_2992 on theBenchmark for (2992ds/1472Mi)
% 31.15/4.88 % (419219)Instruction limit reached!
% 31.15/4.88 % (419219)------------------------------
% 31.15/4.88 % (419219)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.15/4.88 % (419219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.91/6.29 % (419219)CaDiCaL version: 2.1.3
% 41.91/6.29 % (419219)Termination reason: Instruction limit
% 41.91/6.29 % (419219)Termination phase: Saturation
% 41.91/6.29 % (419219)Time elapsed: 0.592 s
% 41.91/6.29 % (419219)Peak memory usage: 16 MB
% 41.91/6.29 % (419219)Instructions burned: 693 (million)
% 41.91/6.29 % (419262)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=916963920:i=6324_2991 on theBenchmark for (2991ds/6324Mi)
% 41.91/6.29 % (419262)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 41.91/6.29 % (419262)Terminated due to inappropriate strategy.
% 41.91/6.29 % (419262)------------------------------
% 41.91/6.29 % (419262)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.91/6.29 % (419262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.91/6.29 % (419262)CaDiCaL version: 2.1.3
% 41.91/6.29 % (419262)Termination reason: Inappropriate
% 41.91/6.29 % (419262)Time elapsed: 0.002 s
% 41.91/6.29 % (419262)Peak memory usage: 10 MB
% 41.91/6.29 % (419262)Instructions burned: 1 (million)
% 41.91/6.29 % (419262)------------------------------
% 41.91/6.29 % (419262)------------------------------
% 41.91/6.29 % (419265)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3520556707:fmbsr=2.30978:i=2174_2990 on theBenchmark for (2990ds/2174Mi)
% 41.91/6.29 % (419265)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 41.91/6.29 % (419265)Terminated due to inappropriate strategy.
% 41.91/6.29 % (419265)------------------------------
% 41.91/6.29 % (419265)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.91/6.29 % (419265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.91/6.29 % (419265)CaDiCaL version: 2.1.3
% 41.91/6.29 % (419265)Termination reason: Inappropriate
% 41.91/6.29 % (419265)Time elapsed: 0.001 s
% 41.91/6.29 % (419265)Peak memory usage: 11 MB
% 41.91/6.29 % (419265)Instructions burned: 1 (million)
% 41.91/6.29 % (419265)------------------------------
% 41.91/6.29 % (419265)------------------------------
% 41.91/6.29 % (419267)ott-2_1_sil=16000:newcnf=on:random_seed=4098039814:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2990 on theBenchmark for (2990ds/869Mi)
% 41.91/6.29 % (419223)Instruction limit reached!
% 41.91/6.29 % (419223)------------------------------
% 41.91/6.29 % (419223)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.91/6.29 % (419223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.91/6.29 % (419223)CaDiCaL version: 2.1.3
% 41.91/6.29 % (419223)Termination reason: Instruction limit
% 41.91/6.29 % (419223)Termination phase: Saturation
% 41.91/6.29 % (419223)Time elapsed: 0.695 s
% 41.91/6.29 % (419223)Peak memory usage: 20 MB
% 41.91/6.29 % (419223)Instructions burned: 879 (million)
% 41.91/6.29 % (419272)ott+10_1_sil=32000:tgt=ground:random_seed=2835314053:i=5114:av=off_2989 on theBenchmark for (2989ds/5114Mi)
% 41.91/6.29 % (419212)Instruction limit reached!
% 41.91/6.29 % (419212)------------------------------
% 41.91/6.29 % (419212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.91/6.29 % (419212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.91/6.29 % (419212)CaDiCaL version: 2.1.3
% 41.91/6.29 % (419212)Termination reason: Instruction limit
% 41.91/6.29 % (419212)Termination phase: Saturation
% 41.91/6.29 % (419212)Time elapsed: 1.099 s
% 41.91/6.29 % (419212)Peak memory usage: 18 MB
% 41.91/6.29 % (419212)Instructions burned: 1180 (million)
% 41.91/6.29 % (419286)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1822988373:i=54282_2986 on theBenchmark for (2986ds/54282Mi)
% 41.91/6.29 % (419286)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 41.91/6.29 % (419286)Terminated due to inappropriate strategy.
% 41.91/6.29 % (419286)------------------------------
% 41.91/6.29 % (419286)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.91/6.29 % (419286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.91/6.29 % (419286)CaDiCaL version: 2.1.3
% 41.91/6.29 % (419286)Termination reason: Inappropriate
% 41.91/6.29 % (419286)Time elapsed: 0.002 s
% 41.91/6.29 % (419286)Peak memory usage: 11 MB
% 41.91/6.29 % (419286)Instructions burned: 1 (million)
% 41.91/6.29 % (419286)------------------------------
% 41.91/6.29 % (419286)------------------------------
% 41.91/6.29 % (419288)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4169854846:i=3512:aac=none_2986 on theBenchmark for (2986ds/3512Mi)
% 41.91/6.29 % (419267)Instruction limit reached!
% 125.11/17.94 % (419267)------------------------------
% 125.11/17.94 % (419267)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 125.11/17.94 % (419267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.11/17.94 % (419267)CaDiCaL version: 2.1.3
% 125.11/17.94 % (419267)Termination reason: Instruction limit
% 125.11/17.94 % (419267)Termination phase: Saturation
% 125.11/17.94 % (419267)Time elapsed: 0.689 s
% 125.11/17.94 % (419267)Peak memory usage: 17 MB
% 125.11/17.94 % (419267)Instructions burned: 870 (million)
% 125.11/17.94 % (419299)dis+21_1_sil=32000:sas=cadical:random_seed=2045989014:i=3773:amm=off_2983 on theBenchmark for (2983ds/3773Mi)
% 125.11/17.94 % (419256)Instruction limit reached!
% 125.11/17.94 % (419256)------------------------------
% 125.11/17.94 % (419256)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 125.11/17.94 % (419256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.11/17.94 % (419256)CaDiCaL version: 2.1.3
% 125.11/17.94 % (419256)Termination reason: Instruction limit
% 125.11/17.94 % (419256)Termination phase: Saturation
% 125.11/17.94 % (419256)Time elapsed: 1.201 s
% 125.11/17.94 % (419256)Peak memory usage: 22 MB
% 125.11/17.94 % (419256)Instructions burned: 1472 (million)
% 125.11/17.94 % (419310)ott+11_1_sil=16000:gs=on:random_seed=2602411957:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2979 on theBenchmark for (2979ds/2251Mi)
% 125.11/17.94 % (419237)Instruction limit reached!
% 125.11/17.94 % (419237)------------------------------
% 125.11/17.94 % (419237)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 125.11/17.94 % (419237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.11/17.94 % (419237)CaDiCaL version: 2.1.3
% 125.11/17.94 % (419237)Termination reason: Instruction limit
% 125.11/17.94 % (419237)Termination phase: Saturation
% 125.11/17.94 % (419237)Time elapsed: 2.199 s
% 125.11/17.94 % (419237)Peak memory usage: 41 MB
% 125.11/17.94 % (419237)Instructions burned: 5131 (million)
% 125.11/17.94 % (419329)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2597912188:fmbsr=1.6:i=67534_2973 on theBenchmark for (2973ds/67534Mi)
% 125.11/17.94 % (419329)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 125.11/17.94 % (419329)Terminated due to inappropriate strategy.
% 125.11/17.94 % (419329)------------------------------
% 125.11/17.94 % (419329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 125.11/17.94 % (419329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.11/17.94 % (419329)CaDiCaL version: 2.1.3
% 125.11/17.94 % (419329)Termination reason: Inappropriate
% 125.11/17.94 % (419329)Time elapsed: 0.001 s
% 125.11/17.94 % (419329)Peak memory usage: 10 MB
% 125.11/17.94 % (419329)Instructions burned: 1 (million)
% 125.11/17.94 % (419329)------------------------------
% 125.11/17.94 % (419329)------------------------------
% 125.11/17.94 % (419331)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2531509455:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2972 on theBenchmark for (2972ds/4591Mi)
% 125.11/17.94 % (419310)Instruction limit reached!
% 125.11/17.94 % (419310)------------------------------
% 125.11/17.94 % (419310)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 125.11/17.94 % (419310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.11/17.94 % (419310)CaDiCaL version: 2.1.3
% 125.11/17.94 % (419310)Termination reason: Instruction limit
% 125.11/17.94 % (419310)Termination phase: Saturation
% 125.11/17.94 % (419310)Time elapsed: 1.692 s
% 125.11/17.94 % (419310)Peak memory usage: 19 MB
% 125.11/17.94 % (419310)Instructions burned: 2251 (million)
% 125.11/17.94 % (419358)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2077512930:i=29340_2962 on theBenchmark for (2962ds/29340Mi)
% 125.11/17.94 % (419288)Instruction limit reached!
% 125.11/17.94 % (419288)------------------------------
% 125.11/17.94 % (419288)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 125.11/17.94 % (419288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.11/17.94 % (419288)CaDiCaL version: 2.1.3
% 125.11/17.94 % (419288)Termination reason: Instruction limit
% 125.11/17.94 % (419288)Termination phase: Saturation
% 125.11/17.94 % (419288)Time elapsed: 2.974 s
% 125.11/17.94 % (419288)Peak memory usage: 29 MB
% 125.11/17.94 % (419288)Instructions burned: 3513 (million)
% 125.11/17.94 % (419374)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=92951158:i=5211_2956 on theBenchmark for (2956ds/5211Mi)
% 125.11/17.94 % (419331)Instruction limit reached!
% 148.43/21.20 % (419331)------------------------------
% 148.43/21.20 % (419331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 148.43/21.20 % (419331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.43/21.20 % (419331)CaDiCaL version: 2.1.3
% 148.43/21.20 % (419331)Termination reason: Instruction limit
% 148.43/21.20 % (419331)Termination phase: Saturation
% 148.43/21.20 % (419331)Time elapsed: 1.852 s
% 148.43/21.20 % (419331)Peak memory usage: 24 MB
% 148.43/21.20 % (419331)Instructions burned: 4595 (million)
% 148.43/21.20 % (419380)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=586625919:i=5497:nm=2_2954 on theBenchmark for (2954ds/5497Mi)
% 148.43/21.20 % (419380)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 148.43/21.20 % (419380)Terminated due to inappropriate strategy.
% 148.43/21.20 % (419380)------------------------------
% 148.43/21.20 % (419380)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 148.43/21.20 % (419380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.43/21.20 % (419380)CaDiCaL version: 2.1.3
% 148.43/21.20 % (419380)Termination reason: Inappropriate
% 148.43/21.20 % (419380)Time elapsed: 0.001 s
% 148.43/21.20 % (419380)Peak memory usage: 11 MB
% 148.43/21.20 % (419380)Instructions burned: 1 (million)
% 148.43/21.20 % (419380)------------------------------
% 148.43/21.20 % (419380)------------------------------
% 148.43/21.20 % (419382)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2360057561:fmbsr=2:i=46332_2953 on theBenchmark for (2953ds/46332Mi)
% 148.43/21.20 % (419382)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 148.43/21.20 % (419382)Terminated due to inappropriate strategy.
% 148.43/21.20 % (419382)------------------------------
% 148.43/21.20 % (419382)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 148.43/21.20 % (419382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.43/21.20 % (419382)CaDiCaL version: 2.1.3
% 148.43/21.20 % (419382)Termination reason: Inappropriate
% 148.43/21.20 % (419382)Time elapsed: 0.001 s
% 148.43/21.20 % (419382)Peak memory usage: 10 MB
% 148.43/21.20 % (419382)Instructions burned: 1 (million)
% 148.43/21.20 % (419382)------------------------------
% 148.43/21.20 % (419382)------------------------------
% 148.43/21.20 % (419384)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=736942415:i=14071_2953 on theBenchmark for (2953ds/14071Mi)
% 148.43/21.20 % (419384)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 148.43/21.20 % (419384)Terminated due to inappropriate strategy.
% 148.43/21.20 % (419384)------------------------------
% 148.43/21.20 % (419384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 148.43/21.20 % (419384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.43/21.20 % (419384)CaDiCaL version: 2.1.3
% 148.43/21.20 % (419384)Termination reason: Inappropriate
% 148.43/21.20 % (419384)Time elapsed: 0.001 s
% 148.43/21.20 % (419384)Peak memory usage: 10 MB
% 148.43/21.20 % (419384)Instructions burned: 1 (million)
% 148.43/21.20 % (419384)------------------------------
% 148.43/21.20 % (419384)------------------------------
% 148.43/21.20 % (419386)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=932389160:i=22565:add=on:rawr=on_2953 on theBenchmark for (2953ds/22565Mi)
% 148.43/21.20 % (419299)Instruction limit reached!
% 148.43/21.20 % (419299)------------------------------
% 148.43/21.20 % (419299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 148.43/21.20 % (419299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.43/21.20 % (419299)CaDiCaL version: 2.1.3
% 148.43/21.20 % (419299)Termination reason: Instruction limit
% 148.43/21.20 % (419299)Termination phase: Saturation
% 148.43/21.20 % (419299)Time elapsed: 3.221 s
% 148.43/21.20 % (419299)Peak memory usage: 30 MB
% 148.43/21.20 % (419299)Instructions burned: 3774 (million)
% 148.43/21.20 % (419392)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=528683261:i=8173:av=off_2950 on theBenchmark for (2950ds/8173Mi)
% 148.43/21.20 % (419272)Instruction limit reached!
% 148.43/21.20 % (419272)------------------------------
% 148.43/21.20 % (419272)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 148.43/21.20 % (419272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.43/21.20 % (419272)CaDiCaL version: 2.1.3
% 148.43/21.20 % (419272)Termination reason: Instruction limit
% 148.43/21.20 % (419272)Termination phase: Saturation
% 148.43/21.20 % (419272)Time elapsed: 4.882 s
% 159.87/22.87 % (419272)Peak memory usage: 28 MB
% 159.87/22.87 % (419272)Instructions burned: 5115 (million)
% 159.87/22.87 % (419410)dis+10_16:1_sil=16000:random_seed=522608257:i=9155:fsr=off_2940 on theBenchmark for (2940ds/9155Mi)
% 159.87/22.87 % (419374)Instruction limit reached!
% 159.87/22.87 % (419374)------------------------------
% 159.87/22.87 % (419374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 159.87/22.87 % (419374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.87/22.87 % (419374)CaDiCaL version: 2.1.3
% 159.87/22.87 % (419374)Termination reason: Instruction limit
% 159.87/22.87 % (419374)Termination phase: Saturation
% 159.87/22.87 % (419374)Time elapsed: 4.651 s
% 159.87/22.87 % (419374)Peak memory usage: 44 MB
% 159.87/22.87 % (419374)Instructions burned: 5211 (million)
% 159.87/22.87 % (419446)ott-3_8_sil=64000:random_seed=797421475:i=20139:bs=on_2909 on theBenchmark for (2909ds/20139Mi)
% 159.87/22.87 % (419392)Instruction limit reached!
% 159.87/22.87 % (419392)------------------------------
% 159.87/22.87 % (419392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 159.87/22.87 % (419392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.87/22.87 % (419392)CaDiCaL version: 2.1.3
% 159.87/22.87 % (419392)Termination reason: Instruction limit
% 159.87/22.87 % (419392)Termination phase: Saturation
% 159.87/22.87 % (419392)Time elapsed: 8.132 s
% 159.87/22.87 % (419392)Peak memory usage: 39 MB
% 159.87/22.87 % (419392)Instructions burned: 8173 (million)
% 159.87/22.87 % (419461)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1851161894:fmbsr=2:i=32576_2868 on theBenchmark for (2868ds/32576Mi)
% 159.87/22.87 % (419461)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 159.87/22.87 % (419461)Terminated due to inappropriate strategy.
% 159.87/22.87 % (419461)------------------------------
% 159.87/22.87 % (419461)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 159.87/22.87 % (419461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.87/22.87 % (419461)CaDiCaL version: 2.1.3
% 159.87/22.87 % (419461)Termination reason: Inappropriate
% 159.87/22.87 % (419461)Time elapsed: 0.001 s
% 159.87/22.87 % (419461)Peak memory usage: 11 MB
% 159.87/22.87 % (419461)Instructions burned: 1 (million)
% 159.87/22.87 % (419461)------------------------------
% 159.87/22.87 % (419461)------------------------------
% 159.87/22.87 % (419463)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3871909966:i=11404_2868 on theBenchmark for (2868ds/11404Mi)
% 159.87/22.87 % (419410)Instruction limit reached!
% 159.87/22.87 % (419410)------------------------------
% 159.87/22.87 % (419410)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 159.87/22.87 % (419410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.87/22.87 % (419410)CaDiCaL version: 2.1.3
% 159.87/22.87 % (419410)Termination reason: Instruction limit
% 159.87/22.87 % (419410)Termination phase: Saturation
% 159.87/22.87 % (419410)Time elapsed: 7.753 s
% 159.87/22.87 % (419410)Peak memory usage: 49 MB
% 159.87/22.87 % (419410)Instructions burned: 9156 (million)
% 159.87/22.87 % (419618)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=617445366:i=14134_2862 on theBenchmark for (2862ds/14134Mi)
% 159.87/22.87 % (419358)Instruction limit reached!
% 159.87/22.87 % (419358)------------------------------
% 159.87/22.87 % (419358)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 159.87/22.87 % (419358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.87/22.87 % (419358)CaDiCaL version: 2.1.3
% 159.87/22.87 % (419358)Termination reason: Instruction limit
% 159.87/22.87 % (419358)Termination phase: Saturation
% 159.87/22.87 % (419358)Time elapsed: 12.348 s
% 159.87/22.87 % (419358)Peak memory usage: 323 MB
% 159.87/22.87 % (419358)Instructions burned: 29342 (million)
% 159.87/22.87 % (419620)dis+33_16_sil=32000:sac=on:random_seed=3110241613:i=15851:nm=0_2838 on theBenchmark for (2838ds/15851Mi)
% 159.87/22.87 % (419386)Instruction limit reached!
% 159.87/22.87 % (419386)------------------------------
% 159.87/22.87 % (419386)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 159.87/22.87 % (419386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.87/22.87 % (419386)CaDiCaL version: 2.1.3
% 159.87/22.87 % (419386)Termination reason: Instruction limit
% 159.87/22.87 % (419386)Termination phase: Saturation
% 159.87/22.87 % (419386)Time elapsed: 12.941 s
% 159.87/22.87 % (419386)Peak memory usage: 71 MB
% 159.87/22.87 % (419386)Instructions burned: 22566 (million)
% 159.87/22.87 % (419623)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=688437322:avsq=on:i=17627:add=on:amm=off_2823 on theBenchmark for (2823ds/17627Mi)
% 188.18/26.86 % (419463)Instruction limit reached!
% 188.18/26.86 % (419463)------------------------------
% 188.18/26.86 % (419463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 188.18/26.86 % (419463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 188.18/26.86 % (419463)CaDiCaL version: 2.1.3
% 188.18/26.86 % (419463)Termination reason: Instruction limit
% 188.18/26.86 % (419463)Termination phase: Saturation
% 188.18/26.86 % (419463)Time elapsed: 7.473 s
% 188.18/26.86 % (419463)Peak memory usage: 43 MB
% 188.18/26.86 % (419463)Instructions burned: 11405 (million)
% 188.18/26.86 % (419625)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=4137596913:s2a=on:i=53295_2793 on theBenchmark for (2793ds/53295Mi)
% 188.18/26.86 % (419620)Instruction limit reached!
% 188.18/26.86 % (419620)------------------------------
% 188.18/26.86 % (419620)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 188.18/26.86 % (419620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 188.18/26.86 % (419620)CaDiCaL version: 2.1.3
% 188.18/26.86 % (419620)Termination reason: Instruction limit
% 188.18/26.86 % (419620)Termination phase: Saturation
% 188.18/26.86 % (419620)Time elapsed: 4.581 s
% 188.18/26.86 % (419620)Peak memory usage: 162 MB
% 188.18/26.86 % (419620)Instructions burned: 15851 (million)
% 188.18/26.86 % (419627)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3990916919:i=26857:ins=20_2792 on theBenchmark for (2792ds/26857Mi)
% 188.18/26.86 % (419627)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 188.18/26.86 % (419627)Terminated due to inappropriate strategy.
% 188.18/26.86 % (419627)------------------------------
% 188.18/26.86 % (419627)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 188.18/26.86 % (419627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 188.18/26.86 % (419627)CaDiCaL version: 2.1.3
% 188.18/26.86 % (419627)Termination reason: Inappropriate
% 188.18/26.86 % (419627)Time elapsed: 0.0000 s
% 188.18/26.86 % (419627)Peak memory usage: 10 MB
% 188.18/26.86 % (419627)Instructions burned: 1 (million)
% 188.18/26.86 % (419627)------------------------------
% 188.18/26.86 % (419627)------------------------------
% 188.18/26.86 % (419629)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3041389972:i=28120:bs=on:fsr=off_2792 on theBenchmark for (2792ds/28120Mi)
% 188.18/26.86 % (419446)Instruction limit reached!
% 188.18/26.86 % (419446)------------------------------
% 188.18/26.86 % (419446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 188.18/26.86 % (419446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 188.18/26.86 % (419446)CaDiCaL version: 2.1.3
% 188.18/26.86 % (419446)Termination reason: Instruction limit
% 188.18/26.86 % (419446)Termination phase: Saturation
% 188.18/26.86 % (419446)Time elapsed: 11.764 s
% 188.18/26.86 % (419446)Peak memory usage: 53 MB
% 188.18/26.86 % (419446)Instructions burned: 20141 (million)
% 188.18/26.86 % (419631)fmb+10_1_sil=256000:fmbss=7:random_seed=4140252035:fmbsr=1.6:i=182295_2791 on theBenchmark for (2791ds/182295Mi)
% 188.18/26.86 % (419631)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 188.18/26.86 % (419631)Terminated due to inappropriate strategy.
% 188.18/26.86 % (419631)------------------------------
% 188.18/26.86 % (419631)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 188.18/26.86 % (419631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 188.18/26.86 % (419631)CaDiCaL version: 2.1.3
% 188.18/26.86 % (419631)Termination reason: Inappropriate
% 188.18/26.86 % (419631)Time elapsed: 0.001 s
% 188.18/26.86 % (419631)Peak memory usage: 10 MB
% 188.18/26.86 % (419631)Instructions burned: 1 (million)
% 188.18/26.86 % (419631)------------------------------
% 188.18/26.86 % (419631)------------------------------
% 188.18/26.86 % (419633)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2650611290:i=44625:gsp=on_2791 on theBenchmark for (2791ds/44625Mi)
% 188.18/26.86 % (419633)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 188.18/26.86 % (419633)Terminated due to inappropriate strategy.
% 188.18/26.86 % (419633)------------------------------
% 188.18/26.86 % (419633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 188.18/26.86 % (419633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 188.18/26.86 % (419633)CaDiCaL version: 2.1.3
% 188.18/26.86 % (419633)Termination reason: Inappropriate
% 196.06/27.96 % (419633)Time elapsed: 0.002 s
% 196.06/27.96 % (419633)Peak memory usage: 11 MB
% 196.06/27.96 % (419633)Instructions burned: 2 (million)
% 196.06/27.96 % (419633)------------------------------
% 196.06/27.96 % (419633)------------------------------
% 196.06/27.96 % (419635)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1430184468:i=160505_2790 on theBenchmark for (2790ds/160505Mi)
% 196.06/27.96 % (419635)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 196.06/27.96 % (419635)Terminated due to inappropriate strategy.
% 196.06/27.96 % (419635)------------------------------
% 196.06/27.96 % (419635)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 196.06/27.96 % (419635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 196.06/27.96 % (419635)CaDiCaL version: 2.1.3
% 196.06/27.96 % (419635)Termination reason: Inappropriate
% 196.06/27.96 % (419635)Time elapsed: 0.001 s
% 196.06/27.96 % (419635)Peak memory usage: 10 MB
% 196.06/27.96 % (419635)Instructions burned: 1 (million)
% 196.06/27.96 % (419635)------------------------------
% 196.06/27.96 % (419635)------------------------------
% 196.06/27.96 % (419637)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1000721327:fmbsr=1.3:i=225729_2790 on theBenchmark for (2790ds/225729Mi)
% 196.06/27.96 % (419637)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 196.06/27.96 % (419637)Terminated due to inappropriate strategy.
% 196.06/27.96 % (419637)------------------------------
% 196.06/27.96 % (419637)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 196.06/27.96 % (419637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 196.06/27.96 % (419637)CaDiCaL version: 2.1.3
% 196.06/27.96 % (419637)Termination reason: Inappropriate
% 196.06/27.96 % (419637)Time elapsed: 0.001 s
% 196.06/27.96 % (419637)Peak memory usage: 10 MB
% 196.06/27.96 % (419637)Instructions burned: 1 (million)
% 196.06/27.96 % (419637)------------------------------
% 196.06/27.96 % (419637)------------------------------
% 196.06/27.96 % (419639)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=558633745:fmbsr=2:i=185024:ins=7_2790 on theBenchmark for (2790ds/185024Mi)
% 196.06/27.96 % (419639)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 196.06/27.96 % (419639)Terminated due to inappropriate strategy.
% 196.06/27.96 % (419639)------------------------------
% 196.06/27.96 % (419639)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 196.06/27.96 % (419639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 196.06/27.96 % (419639)CaDiCaL version: 2.1.3
% 196.06/27.96 % (419639)Termination reason: Inappropriate
% 196.06/27.96 % (419639)Time elapsed: 0.001 s
% 196.06/27.96 % (419639)Peak memory usage: 10 MB
% 196.06/27.96 % (419639)Instructions burned: 1 (million)
% 196.06/27.96 % (419639)------------------------------
% 196.06/27.96 % (419639)------------------------------
% 196.06/27.96 % (419641)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=242318376:rtra=on_2790 on theBenchmark for (2790ds/0Mi)
% 196.06/27.96 % (419641)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 196.06/27.96 % (419641)Terminated due to inappropriate strategy.
% 196.06/27.96 % (419641)------------------------------
% 196.06/27.96 % (419641)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 196.06/27.96 % (419641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 196.06/27.96 % (419641)CaDiCaL version: 2.1.3
% 196.06/27.96 % (419641)Termination reason: Inappropriate
% 196.06/27.96 % (419641)Time elapsed: 0.001 s
% 196.06/27.96 % (419641)Peak memory usage: 11 MB
% 196.06/27.96 % (419641)Instructions burned: 1 (million)
% 196.06/27.96 % (419641)------------------------------
% 196.06/27.96 % (419641)------------------------------
% 196.06/27.96 % (419643)% WARNING: option uhcvi not known.
% 196.06/27.96 % (419643)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=903148314:i=271062:add=off:rtra=on:rawr=on_2790 on theBenchmark for (2790ds/271062Mi)
% 196.06/27.96 % (419618)Instruction limit reached!
% 196.06/27.96 % (419618)------------------------------
% 196.06/27.96 % (419618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 196.06/27.96 % (419618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 196.06/27.96 % (419618)CaDiCaL version: 2.1.3
% 196.06/27.96 % (419618)Termination reason: Instruction limit
% 196.06/27.96 % (419618)Termination phase: Saturation
% 196.06/27.96 % (419618)Time elapsed: 8.751 s
% 196.06/27.96 % (419618)Peak memory usage: 59 MB
% 196.06/27.96 % (419618)Instructions burned: 14135 (million)
% 196.06/27.96 % (419645)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3779218236:i=176048:add=on:rtra=on:rawr=on_2774 on theBenchmark for (2774ds/176048Mi)
% 202.42/28.85 % (419629)Instruction limit reached!
% 202.42/28.85 % (419629)------------------------------
% 202.42/28.85 % (419629)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 202.42/28.85 % (419629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.42/28.85 % (419629)CaDiCaL version: 2.1.3
% 202.42/28.85 % (419629)Termination reason: Instruction limit
% 202.42/28.85 % (419629)Termination phase: Saturation
% 202.42/28.85 % (419629)Time elapsed: 5.340 s
% 202.42/28.85 % (419629)Peak memory usage: 19 MB
% 202.42/28.85 % (419629)Instructions burned: 28122 (million)
% 202.42/28.85 % (419647)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1987764869:i=206:fgj=on:rtra=on_2738 on theBenchmark for (2738ds/206Mi)
% 202.42/28.85 % (419647)Instruction limit reached!
% 202.42/28.85 % (419647)------------------------------
% 202.42/28.85 % (419647)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 202.42/28.85 % (419647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.42/28.85 % (419647)CaDiCaL version: 2.1.3
% 202.42/28.85 % (419647)Termination reason: Instruction limit
% 202.42/28.85 % (419647)Termination phase: Saturation
% 202.42/28.85 % (419647)Time elapsed: 0.073 s
% 202.42/28.85 % (419647)Peak memory usage: 13 MB
% 202.42/28.85 % (419647)Instructions burned: 208 (million)
% 202.42/28.85 % (419649)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=296726185:i=232:rtra=on_2737 on theBenchmark for (2737ds/232Mi)
% 202.42/28.85 % (419649)Instruction limit reached!
% 202.42/28.85 % (419649)------------------------------
% 202.42/28.85 % (419649)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 202.42/28.85 % (419649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.42/28.85 % (419649)CaDiCaL version: 2.1.3
% 202.42/28.85 % (419649)Termination reason: Instruction limit
% 202.42/28.85 % (419649)Termination phase: Saturation
% 202.42/28.85 % (419649)Time elapsed: 0.078 s
% 202.42/28.85 % (419649)Peak memory usage: 13 MB
% 202.42/28.85 % (419649)Instructions burned: 232 (million)
% 202.42/28.85 % (419651)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1941600774:i=262:rtra=on_2736 on theBenchmark for (2736ds/262Mi)
% 202.42/28.85 % (419651)Instruction limit reached!
% 202.42/28.85 % (419651)------------------------------
% 202.42/28.85 % (419651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 202.42/28.85 % (419651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.42/28.85 % (419651)CaDiCaL version: 2.1.3
% 202.42/28.85 % (419651)Termination reason: Instruction limit
% 202.42/28.85 % (419651)Termination phase: Saturation
% 202.42/28.85 % (419651)Time elapsed: 0.091 s
% 202.42/28.85 % (419651)Peak memory usage: 13 MB
% 202.42/28.85 % (419651)Instructions burned: 262 (million)
% 202.42/28.85 % (419653)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3565661859:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2735 on theBenchmark for (2735ds/318Mi)
% 202.42/28.85 % (419653)Instruction limit reached!
% 202.42/28.85 % (419653)------------------------------
% 202.42/28.85 % (419653)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 202.42/28.85 % (419653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.42/28.85 % (419653)CaDiCaL version: 2.1.3
% 202.42/28.85 % (419653)Termination reason: Instruction limit
% 202.42/28.85 % (419653)Termination phase: Saturation
% 202.42/28.85 % (419653)Time elapsed: 0.119 s
% 202.42/28.85 % (419653)Peak memory usage: 15 MB
% 202.42/28.85 % (419653)Instructions burned: 318 (million)
% 202.42/28.85 % (419655)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=351581858:i=1428:nm=2:rtra=on_2734 on theBenchmark for (2734ds/1428Mi)
% 202.42/28.85 % (419655)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 202.42/28.85 % (419655)Terminated due to inappropriate strategy.
% 202.42/28.85 % (419655)------------------------------
% 202.42/28.85 % (419655)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 202.42/28.85 % (419655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.42/28.85 % (419655)CaDiCaL version: 2.1.3
% 202.42/28.85 % (419655)Termination reason: Inappropriate
% 202.42/28.85 % (419655)Time elapsed: 0.001 s
% 202.42/28.85 % (419655)Peak memory usage: 10 MB
% 202.42/28.85 % (419655)Instructions burned: 1 (million)
% 202.42/28.85 % (419655)------------------------------
% 202.42/28.85 % (419655)------------------------------
% 224.52/31.95 % (419657)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=4048858784:i=262:bd=preordered:rtra=on:fsd=on_2734 on theBenchmark for (2734ds/262Mi)
% 224.52/31.95 % (419657)Instruction limit reached!
% 224.52/31.95 % (419657)------------------------------
% 224.52/31.95 % (419657)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 224.52/31.95 % (419657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 224.52/31.95 % (419657)CaDiCaL version: 2.1.3
% 224.52/31.95 % (419657)Termination reason: Instruction limit
% 224.52/31.95 % (419657)Termination phase: Saturation
% 224.52/31.95 % (419657)Time elapsed: 0.098 s
% 224.52/31.95 % (419657)Peak memory usage: 14 MB
% 224.52/31.95 % (419657)Instructions burned: 264 (million)
% 224.52/31.95 % (419659)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:si=on:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1171451987:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2733 on theBenchmark for (2733ds/1368Mi)
% 224.52/31.95 % (419659)Instruction limit reached!
% 224.52/31.95 % (419659)------------------------------
% 224.52/31.95 % (419659)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 224.52/31.95 % (419659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 224.52/31.95 % (419659)CaDiCaL version: 2.1.3
% 224.52/31.95 % (419659)Termination reason: Instruction limit
% 224.52/31.95 % (419659)Termination phase: Saturation
% 224.52/31.95 % (419659)Time elapsed: 0.404 s
% 224.52/31.95 % (419659)Peak memory usage: 28 MB
% 224.52/31.95 % (419659)Instructions burned: 1369 (million)
% 224.52/31.95 % (419661)ott-21_1_sil=16000:si=on:fs=off:random_seed=2062778778:i=360:av=off:fsr=off:rtra=on_2729 on theBenchmark for (2729ds/360Mi)
% 224.52/31.95 % (419661)Instruction limit reached!
% 224.52/31.95 % (419661)------------------------------
% 224.52/31.95 % (419661)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 224.52/31.95 % (419661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 224.52/31.95 % (419661)CaDiCaL version: 2.1.3
% 224.52/31.95 % (419661)Termination reason: Instruction limit
% 224.52/31.95 % (419661)Termination phase: Saturation
% 224.52/31.95 % (419661)Time elapsed: 0.087 s
% 224.52/31.95 % (419661)Peak memory usage: 13 MB
% 224.52/31.95 % (419661)Instructions burned: 362 (million)
% 224.52/31.95 % (419663)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3723542535:i=954:bd=all:rtra=on_2728 on theBenchmark for (2728ds/954Mi)
% 224.52/31.95 % (419663)Instruction limit reached!
% 224.52/31.95 % (419663)------------------------------
% 224.52/31.95 % (419663)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 224.52/31.95 % (419663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 224.52/31.95 % (419663)CaDiCaL version: 2.1.3
% 224.52/31.95 % (419663)Termination reason: Instruction limit
% 224.52/31.95 % (419663)Termination phase: Saturation
% 224.52/31.95 % (419663)Time elapsed: 0.348 s
% 224.52/31.95 % (419663)Peak memory usage: 17 MB
% 224.52/31.95 % (419663)Instructions burned: 954 (million)
% 224.52/31.95 % (419665)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=269963210:fmbsr=1.3:i=1730:ins=25:rtra=on_2724 on theBenchmark for (2724ds/1730Mi)
% 224.52/31.95 % (419665)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 224.52/31.95 % (419665)Terminated due to inappropriate strategy.
% 224.52/31.95 % (419665)------------------------------
% 224.52/31.95 % (419665)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 224.52/31.95 % (419665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 224.52/31.95 % (419665)CaDiCaL version: 2.1.3
% 224.52/31.95 % (419665)Termination reason: Inappropriate
% 224.52/31.95 % (419665)Time elapsed: 0.0000 s
% 224.52/31.95 % (419665)Peak memory usage: 10 MB
% 224.52/31.95 % (419665)Instructions burned: 1 (million)
% 224.52/31.95 % (419665)------------------------------
% 224.52/31.95 % (419665)------------------------------
% 224.52/31.95 % (419667)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=42792349:i=2358:rtra=on_2724 on theBenchmark for (2724ds/2358Mi)
% 224.52/31.95 % (419623)Instruction limit reached!
% 224.52/31.95 % (419623)------------------------------
% 224.52/31.95 % (419623)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 224.52/31.95 % (419623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 224.52/31.95 % (419623)CaDiCaL version: 2.1.3
% 224.52/31.95 % (419623)Termination reason: Instruction limit
% 224.52/31.95 % (419623)Termination phase: Saturation
% 184.43/41.41 % (419623)Time elapsed: 10.022 s
% 184.43/41.41 % (419623)Peak memory usage: 124 MB
% 184.43/41.41 % (419623)Instructions burned: 17627 (million)
% 184.43/41.41 % (419669)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=1126249664:i=1778:ins=1:rtra=on_2723 on theBenchmark for (2723ds/1778Mi)
% 184.43/41.41 % (419669)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 184.43/41.41 % (419669)Terminated due to inappropriate strategy.
% 184.43/41.41 % (419669)------------------------------
% 184.43/41.41 % (419669)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.43/41.41 % (419669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.43/41.41 % (419669)CaDiCaL version: 2.1.3
% 184.43/41.41 % (419669)Termination reason: Inappropriate
% 184.43/41.41 % (419669)Time elapsed: 0.001 s
% 184.43/41.41 % (419669)Peak memory usage: 10 MB
% 184.43/41.41 % (419669)Instructions burned: 1 (million)
% 184.43/41.41 % (419669)------------------------------
% 184.43/41.41 % (419669)------------------------------
% 184.43/41.41 % (419671)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:si=on:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3570382000:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2722 on theBenchmark for (2722ds/1384Mi)
% 184.43/41.41 % (419667)Instruction limit reached!
% 184.43/41.41 % (419667)------------------------------
% 184.43/41.41 % (419667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.43/41.41 % (419667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.43/41.41 % (419667)CaDiCaL version: 2.1.3
% 184.43/41.41 % (419667)Termination reason: Instruction limit
% 184.43/41.41 % (419667)Termination phase: Saturation
% 184.43/41.41 % (419667)Time elapsed: 0.884 s
% 184.43/41.41 % (419667)Peak memory usage: 23 MB
% 184.43/41.41 % (419667)Instructions burned: 2360 (million)
% 184.43/41.41 % (419795)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1126472988:i=1758:kws=inv_precedence:fsr=off:rtra=on_2715 on theBenchmark for (2715ds/1758Mi)
% 184.43/41.41 % (419671)Instruction limit reached!
% 184.43/41.41 % (419671)------------------------------
% 184.43/41.41 % (419671)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.43/41.41 % (419671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.43/41.41 % (419671)CaDiCaL version: 2.1.3
% 184.43/41.41 % (419671)Termination reason: Instruction limit
% 184.43/41.41 % (419671)Termination phase: Saturation
% 184.43/41.41 % (419671)Time elapsed: 0.755 s
% 184.43/41.41 % (419671)Peak memory usage: 21 MB
% 184.43/41.41 % (419671)Instructions burned: 1385 (million)
% 184.43/41.41 % (419797)fmb+10_1_sil=64000:si=on:random_seed=374137316:i=44122:nm=2:rtra=on:gsp=on_2715 on theBenchmark for (2715ds/44122Mi)
% 184.43/41.41 % (419797)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 184.43/41.41 % (419797)Terminated due to inappropriate strategy.
% 184.43/41.41 % (419797)------------------------------
% 184.43/41.41 % (419797)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.43/41.41 % (419797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.43/41.41 % (419797)CaDiCaL version: 2.1.3
% 184.43/41.41 % (419797)Termination reason: Inappropriate
% 184.43/41.41 % (419797)Time elapsed: 0.002 s
% 184.43/41.41 % (419797)Peak memory usage: 11 MB
% 184.43/41.41 % (419797)Instructions burned: 1 (million)
% 184.43/41.41 % (419797)------------------------------
% 184.43/41.41 % (419797)------------------------------
% 184.43/41.41 % (419799)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=805220268:i=19030:nm=5:rtra=on_2714 on theBenchmark for (2714ds/19030Mi)
% 184.43/41.41 % (419799)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 184.43/41.41 % (419799)Terminated due to inappropriate strategy.
% 184.43/41.41 % (419799)------------------------------
% 184.43/41.41 % (419799)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.43/41.41 % (419799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.43/41.41 % (419799)CaDiCaL version: 2.1.3
% 184.43/41.41 % (419799)Termination reason: Inappropriate
% 184.43/41.41 % (419799)Time elapsed: 0.001 s
% 184.43/41.41 % (419799)Peak memory usage: 10 MB
% 184.43/41.41 % (419799)Instructions burned: 1 (million)
% 184.43/41.41 % (419799)------------------------------
% 184.43/41.41 % (419799)------------------------------
% 184.43/41.41 % (419801)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=3747975773:fmbsr=1.7:i=1840:rtra=on_2714 on theBenchmark for (2714ds/1840Mi)
% 184.43/41.41 % (419801)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 184.43/41.41 % (419801)Terminated due to inappropriate strategy.
% 184.43/41.41 % (419801)------------------------------
% 184.43/41.41 % (419801)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.43/41.41 % (419801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.43/41.41 % (419801)CaDiCaL version: 2.1.3
% 184.43/41.41 % (419801)Termination reason: Inappropriate
% 184.43/41.41 % (419801)Time elapsed: 0.001 s
% 184.43/41.41 % (419801)Peak memory usage: 10 MB
% 184.43/41.41 % (419801)Instructions burned: 1 (million)
% 184.43/41.41 % (419801)------------------------------
% 184.43/41.41 % (419801)------------------------------
% 184.43/41.41 % (419803)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=113169011:i=10262:rtra=on_2714 on theBenchmark for (2714ds/10262Mi)
% 184.43/41.41 % (419795)Instruction limit reached!
% 184.43/41.41 % (419795)------------------------------
% 184.43/41.41 % (419795)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.43/41.41 % (419795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.43/41.41 % (419795)CaDiCaL version: 2.1.3
% 184.43/41.41 % (419795)Termination reason: Instruction limit
% 184.43/41.41 % (419795)Termination phase: Saturation
% 184.43/41.41 % (419795)Time elapsed: 0.573 s
% 184.43/41.41 % (419795)Peak memory usage: 27 MB
% 184.43/41.41 % (419795)Instructions burned: 1759 (million)
% 184.43/41.41 % (419883)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1170187309:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2709 on theBenchmark for (2709ds/2944Mi)
% 184.43/41.41 % (419883)Instruction limit reached!
% 184.43/41.41 % (419883)------------------------------
% 184.43/41.41 % (419883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.43/41.41 % (419883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.43/41.41 % (419883)CaDiCaL version: 2.1.3
% 184.43/41.41 % (419883)Termination reason: Instruction limit
% 184.43/41.41 % (419883)Termination phase: Saturation
% 184.43/41.41 % (419883)Time elapsed: 1.534 s
% 184.43/41.41 % (419883)Peak memory usage: 31 MB
% 184.43/41.41 % (419883)Instructions burned: 2944 (million)
% 184.43/41.41 % (419989)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=2967541880:i=12648:rtra=on_2694 on theBenchmark for (2694ds/12648Mi)
% 184.43/41.41 % (419989)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 184.43/41.41 % (419989)Terminated due to inappropriate strategy.
% 184.43/41.41 % (419989)------------------------------
% 184.43/41.41 % (419989)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.43/41.41 % (419989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.43/41.41 % (419989)CaDiCaL version: 2.1.3
% 184.43/41.41 % (419989)Termination reason: Inappropriate
% 184.43/41.41 % (419989)Time elapsed: 0.002 s
% 184.43/41.41 % (419989)Peak memory usage: 11 MB
% 184.43/41.41 % (419989)Instructions burned: 1 (million)
% 184.43/41.41 % (419989)------------------------------
% 184.43/41.41 % (419989)------------------------------
% 184.43/41.41 % (419991)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2702069059:fmbsr=2.30978:i=4348:rtra=on_2693 on theBenchmark for (2693ds/4348Mi)
% 184.43/41.41 % (419991)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 184.43/41.41 % (419991)Terminated due to inappropriate strategy.
% 184.43/41.41 % (419991)------------------------------
% 184.43/41.41 % (419991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.43/41.41 % (419991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.43/41.41 % (419991)CaDiCaL version: 2.1.3
% 184.43/41.41 % (419991)Termination reason: Inappropriate
% 184.43/41.41 % (419991)Time elapsed: 0.002 s
% 184.43/41.41 % (419991)Peak memory usage: 11 MB
% 184.43/41.41 % (419991)Instructions burned: 1 (million)
% 184.43/41.41 % (419991)------------------------------
% 184.43/41.41 % (419991)------------------------------
% 184.43/41.41 % (419994)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=1555847309:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2693 on theBenchmark for (2693ds/1738Mi)
% 184.43/41.41 % (419994)Instruction limit reached!
% 184.43/41.41 % (419994)------------------------------
% 184.43/41.41 % (419994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.43/41.41 % (419994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.43/41.41 % (419994)CaDiCaL version: 2.1.3
% 184.43/41.41 % (419994)Termination reason: Instruction limit
% 184.43/41.41 % (419994)Termination phase: Saturation
% 184.43/41.41 % (419994)Time elapsed: 0.976 s
% 184.43/41.41 % (419994)Peak memory usage: 20 MB
% 184.43/41.41 % (419994)Instructions burned: 1740 (million)
% 184.43/41.41 % (420001)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=1542459395:i=10228:av=off:rtra=on_2683 on theBenchmark for (2683ds/10228Mi)
% 184.43/41.41 % (420001)Instruction limit reached!
% 184.43/41.41 % (420001)------------------------------
% 184.43/41.41 % (420001)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.43/41.41 % (420001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.43/41.41 % (420001)CaDiCaL version: 2.1.3
% 184.43/41.41 % (420001)Termination reason: Instruction limit
% 184.43/41.41 % (420001)Termination phase: Saturation
% 184.43/41.41 % (420001)Time elapsed: 6.147 s
% 184.43/41.41 % (420001)Peak memory usage: 37 MB
% 184.43/41.41 % (420001)Instructions burned: 10228 (million)
% 184.43/41.41 % (420025)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=3322192887:i=108564:rtra=on_2621 on theBenchmark for (2621ds/108564Mi)
% 184.43/41.41 % (420025)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 184.43/41.41 % (420025)Terminated due to inappropriate strategy.
% 184.43/41.41 % (420025)------------------------------
% 184.43/41.41 % (420025)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.43/41.41 % (420025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.43/41.41 % (420025)CaDiCaL version: 2.1.3
% 184.43/41.41 % (420025)Termination reason: Inappropriate
% 184.43/41.41 % (420025)Time elapsed: 0.002 s
% 184.43/41.41 % (420025)Peak memory usage: 11 MB
% 184.43/41.41 % (420025)Instructions burned: 1 (million)
% 184.43/41.41 % (420025)------------------------------
% 184.43/41.41 % (420025)------------------------------
% 184.43/41.41 % (420027)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=3030539615:i=7024:aac=none:rtra=on_2621 on theBenchmark for (2621ds/7024Mi)
% 184.43/41.41 % (419803)Instruction limit reached!
% 184.43/41.41 % (419803)------------------------------
% 184.43/41.41 % (419803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.43/41.41 % (419803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.43/41.41 % (419803)CaDiCaL version: 2.1.3
% 184.43/41.41 % (419803)Termination reason: Instruction limit
% 184.43/41.41 % (419803)Termination phase: Saturation
% 184.43/41.41 % (419803)Time elapsed: 9.648 s
% 184.43/41.41 % (419803)Peak memory usage: 56 MB
% 184.43/41.41 % (419803)Instructions burned: 10262 (million)
% 184.43/41.41 % (420029)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=3198641745:i=7546:rtra=on:amm=off_2617 on theBenchmark for (2617ds/7546Mi)
% 184.43/41.41 % (419643) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-419171-419643"...
% 184.43/41.41 % (419643)...printing done.
% 184.43/41.41 % (419643)Refutation found. Thanks to Tanya!
% 184.43/41.41 % SZS status Theorem for theBenchmark
% 184.43/41.41 % SZS output start Proof for theBenchmark
% 184.43/41.41 tff(type_def_5, type, general: $tType).
% 184.43/41.41 tff(type_def_6, type, symbol: $tType).
% 184.43/41.41 tff(func_def_0, type, f__integer__: $int > general).
% 184.43/41.41 tff(func_def_1, type, f__symbolic__: symbol > general).
% 184.43/41.41 tff(func_def_2, type, c__infimum__: general).
% 184.43/41.41 tff(func_def_3, type, c__supremum__: general).
% 184.43/41.41 tff(func_def_11, type, sK0: general).
% 184.43/41.41 tff(func_def_12, type, sK1: general).
% 184.43/41.41 tff(func_def_13, type, sK2: general).
% 184.43/41.41 tff(func_def_14, type, sK3: general).
% 184.43/41.41 tff(func_def_15, type, sK4: general).
% 184.43/41.41 tff(func_def_16, type, sK5: general).
% 184.43/41.41 tff(func_def_17, type, sK6: general).
% 184.43/41.41 tff(func_def_18, type, sK7: general).
% 184.43/41.41 tff(func_def_19, type, sK8: general).
% 184.43/41.41 tff(func_def_20, type, sK9: general).
% 184.43/41.41 tff(func_def_21, type, sK10: general > symbol).
% 184.43/41.41 tff(func_def_22, type, sK11: general > $int).
% 184.43/41.41 tff(pred_def_1, type, p__is_integer__: general > $o).
% 184.43/41.41 tff(pred_def_2, type, p__is_symbolic__: general > $o).
% 184.43/41.41 tff(pred_def_3, type, p__less_equal__: (general * general) > $o).
% 184.43/41.41 tff(pred_def_4, type, p__less__: (general * general) > $o).
% 184.43/41.41 tff(pred_def_5, type, p__greater_equal__: (general * general) > $o).
% 184.43/41.41 tff(pred_def_6, type, p__greater__: (general * general) > $o).
% 184.43/41.41 tff(pred_def_8, type, hp: general > $o).
% 184.43/41.41 tff(pred_def_9, type, tp: general > $o).
% 184.43/41.41 tff(f1,axiom,(
% 184.43/41.41 ! [X0 : general] : (p__is_integer__(X0) <=> ? [X1 : $int] : X0 = f__integer__(X1))),
% 184.43/41.41 file('/export/starexec/sandbox2/benchmark/Axioms/SWV014_0.ax',p__is_integer__def_ax)).
% 184.43/41.41 tff(f2,axiom,(
% 184.43/41.41 ! [X0 : general] : (? [X1 : symbol] : X0 = f__symbolic__(X1) <=> p__is_symbolic__(X0))),
% 184.43/41.41 file('/export/starexec/sandbox2/benchmark/Axioms/SWV014_0.ax',p__is_symbolic__def_ax)).
% 184.43/41.41 tff(f3,axiom,(
% 184.43/41.41 ! [X0 : general] : (X0 = c__supremum__ | p__is_integer__(X0) | p__is_symbolic__(X0) | X0 = c__infimum__)),
% 184.43/41.41 file('/export/starexec/sandbox2/benchmark/Axioms/SWV014_0.ax',general_universe_ax)).
% 184.43/41.41 tff(f6,axiom,(
% 184.43/41.41 ! [X1 : $int,X0 : $int] : (p__less_equal__(f__integer__(X0),f__integer__(X1)) <=> $lesseq(X0,X1))),
% 184.43/41.41 file('/export/starexec/sandbox2/benchmark/Axioms/SWV014_0.ax',numeral_ordering_ax)).
% 184.43/41.41 tff(f7,axiom,(
% 184.43/41.41 ! [X1 : general,X0 : general] : ((p__less_equal__(X0,X1) & p__less_equal__(X1,X0)) => X0 = X1)),
% 184.43/41.41 file('/export/starexec/sandbox2/benchmark/Axioms/SWV014_0.ax',antisymmetric_ordering_ax)).
% 184.43/41.41 tff(f8,axiom,(
% 184.43/41.41 ! [X0 : general,X1 : general,X2 : general] : ((p__less_equal__(X1,X2) & p__less_equal__(X0,X1)) => p__less_equal__(X0,X2))),
% 184.43/41.41 file('/export/starexec/sandbox2/benchmark/Axioms/SWV014_0.ax',transitive_ordering_ax)).
% 184.43/41.41 tff(f9,axiom,(
% 184.43/41.41 ! [X1 : general,X0 : general] : (p__less_equal__(X1,X0) | p__less_equal__(X0,X1))),
% 184.43/41.41 file('/export/starexec/sandbox2/benchmark/Axioms/SWV014_0.ax',strongly_connected_ordering_ax)).
% 184.43/41.41 tff(f10,axiom,(
% 184.43/41.41 ! [X1 : general,X0 : general] : (p__less__(X0,X1) <=> (X0 != X1 & p__less_equal__(X0,X1)))),
% 184.43/41.41 file('/export/starexec/sandbox2/benchmark/Axioms/SWV014_0.ax',p__less__def_ax)).
% 184.43/41.41 tff(f11,axiom,(
% 184.43/41.41 ! [X0 : general,X1 : general] : (p__less_equal__(X1,X0) <=> p__greater_equal__(X0,X1))),
% 184.43/41.41 file('/export/starexec/sandbox2/benchmark/Axioms/SWV014_0.ax',p__greater_equal__def_ax)).
% 184.43/41.41 tff(f12,axiom,(
% 184.43/41.41 ! [X0 : general,X1 : general] : ((X0 != X1 & p__less_equal__(X1,X0)) <=> p__greater__(X0,X1))),
% 184.43/41.41 file('/export/starexec/sandbox2/benchmark/Axioms/SWV014_0.ax',p__greater__def_ax)).
% 184.43/41.41 tff(f13,axiom,(
% 184.43/41.41 ! [X0 : $int] : p__less__(c__infimum__,f__integer__(X0))),
% 184.43/41.41 file('/export/starexec/sandbox2/benchmark/Axioms/SWV014_0.ax',minimal_element_ax)).
% 184.43/41.41 tff(f14,axiom,(
% 184.43/41.41 ! [X1 : symbol,X0 : $int] : p__less__(f__integer__(X0),f__symbolic__(X1))),
% 184.43/41.41 file('/export/starexec/sandbox2/benchmark/Axioms/SWV014_0.ax',numerals_less_than_symbols_ax)).
% 184.43/41.41 tff(f15,axiom,(
% 184.43/41.41 ! [X0 : symbol] : p__less__(f__symbolic__(X0),c__supremum__)),
% 184.43/41.41 file('/export/starexec/sandbox2/benchmark/Axioms/SWV014_0.ax',maximal_element_ax)).
% 184.43/41.41 tff(f16,axiom,(
% 184.43/41.41 ! [X0 : general] : (hp(X0) => tp(X0))),
% 184.43/41.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',formula_0_transition_axiom_0)).
% 184.43/41.41 tff(f17,axiom,(
% 184.43/41.41 ! [X0 : general] : ((($true & X0 = f__integer__(4)) => hp(X0)) & ((X0 = f__integer__(4) & $true) => tp(X0)))),
% 184.43/41.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',formula_1_right_0)).
% 184.43/41.41 tff(f18,conjecture,(
% 184.43/41.41 ! [X0 : general,X1 : general] : (((? [X3 : general,X2 : general] : (p__less__(X2,X3) & X2 = X1 & X3 = f__integer__(5)) & X0 = X1 & ? [X2 : general,X3 : general] : (X3 = f__integer__(3) & X2 = X1 & p__greater__(X2,X3))) => hp(X0)) & ((X0 = X1 & ? [X2 : general,X3 : general] : (X3 = f__integer__(5) & X2 = X1 & p__less__(X2,X3)) & ? [X2 : general,X3 : general] : (X3 = f__integer__(3) & p__greater__(X2,X3) & X2 = X1)) => tp(X0)))),
% 184.43/41.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',formula_2_left_0)).
% 184.43/41.41 tff(f19,negated_conjecture,(
% 184.43/41.41 ~ ! [X0 : general,X1 : general] : (((? [X3 : general,X2 : general] : (p__less__(X2,X3) & X2 = X1 & X3 = f__integer__(5)) & X0 = X1 & ? [X2 : general,X3 : general] : (X3 = f__integer__(3) & X2 = X1 & p__greater__(X2,X3))) => hp(X0)) & ((X0 = X1 & ? [X2 : general,X3 : general] : (X3 = f__integer__(5) & X2 = X1 & p__less__(X2,X3)) & ? [X2 : general,X3 : general] : (X3 = f__integer__(3) & p__greater__(X2,X3) & X2 = X1)) => tp(X0)))),
% 184.43/41.41 inference(negated_conjecture,[status(cth)],[f18])).
% 184.43/41.41 tff(f20,plain,(
% 184.43/41.41 ! [X1 : $int,X0 : $int] : (p__less_equal__(f__integer__(X0),f__integer__(X1)) <=> ~$less(X1,X0))),
% 184.43/41.41 inference(theory_normalization,[],[f6])).
% 184.43/41.41 tff(f21,definition,(
% 184.43/41.41 ( ! [X0 : $int,X1 : $int] : ($sum(X1,X0) = $sum(X0,X1)) )),
% 184.43/41.41 introduced(theory,[tha_commutativity])).
% 184.43/41.41 tff(f22,definition,(
% 184.43/41.41 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum(X0,$sum(X1,X2)) = $sum($sum(X0,X1),X2)) )),
% 184.43/41.41 introduced(theory,[tha_associativity])).
% 184.43/41.41 tff(f23,definition,(
% 184.43/41.41 ( ! [X0 : $int] : ($sum(X0,0) = X0) )),
% 184.43/41.41 introduced(theory,[tha_right_identity])).
% 184.43/41.41 tff(f26,definition,(
% 184.43/41.41 ( ! [X0 : $int] : (~$less(X0,X0)) )),
% 184.43/41.41 introduced(theory,[tha_non-reflexivity])).
% 184.43/41.41 tff(f27,definition,(
% 184.43/41.41 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X0,X1) | ~$less(X1,X2) | $less(X0,X2)) )),
% 184.43/41.41 introduced(theory,[tha_transitivity])).
% 184.43/41.41 tff(f28,definition,(
% 184.43/41.41 ( ! [X0 : $int,X1 : $int] : ($less(X1,X0) | $less(X0,X1) | X0 = X1) )),
% 184.43/41.41 introduced(theory,[tha_order_totality])).
% 184.43/41.41 tff(f29,definition,(
% 184.43/41.41 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X0,X1) | $less($sum(X0,X2),$sum(X1,X2))) )),
% 184.43/41.41 introduced(theory,[tha_order_monotonicity])).
% 184.43/41.41 tff(f30,definition,(
% 184.43/41.41 ( ! [X0 : $int,X1 : $int] : ($less(X1,$sum(X0,1)) | $less(X0,X1)) )),
% 184.43/41.41 introduced(theory,[tha_order_plus_one_dichotomy])).
% 184.43/41.41 tff(f32,definition,(
% 184.43/41.41 ( ! [X0 : $int,X1 : $int] : (~$less(X0,X1) | ~$less(X1,$sum(X0,1))) )),
% 184.43/41.41 introduced(theory,[tha_extra_integer_ordering])).
% 184.43/41.41 tff(f33,plain,(
% 184.43/41.41 ! [X1 : general,X0 : general] : (p__less__(X1,X0) <=> (X0 != X1 & p__less_equal__(X1,X0)))),
% 184.43/41.41 inference(rectify,[],[f10])).
% 184.43/41.41 tff(f34,plain,(
% 184.43/41.41 ! [X0 : general,X1 : general] : (p__less_equal__(X0,X1) | p__less_equal__(X1,X0))),
% 184.43/41.41 inference(rectify,[],[f9])).
% 184.43/41.41 tff(f35,plain,(
% 184.43/41.41 ! [X1 : $int,X0 : $int] : (p__less_equal__(f__integer__(X1),f__integer__(X0)) <=> ~$less(X0,X1))),
% 184.43/41.41 inference(rectify,[],[f20])).
% 184.43/41.41 tff(f36,plain,(
% 184.43/41.41 ! [X1 : general,X0 : general] : ((p__less_equal__(X0,X1) & p__less_equal__(X1,X0)) => X0 = X1)),
% 184.43/41.41 inference(rectify,[],[f7])).
% 184.43/41.41 tff(f37,plain,(
% 184.43/41.41 ~ ! [X0 : general,X1 : general] : (((? [X6 : general,X7 : general] : (p__less__(X6,X7) & f__integer__(5) = X7 & X1 = X6) & ? [X9 : general,X8 : general] : (X1 = X8 & p__greater__(X8,X9) & f__integer__(3) = X9) & X0 = X1) => tp(X0)) & ((? [X3 : general,X2 : general] : (p__less__(X2,X3) & X2 = X1 & X3 = f__integer__(5)) & X0 = X1 & ? [X4 : general,X5 : general] : (f__integer__(3) = X5 & p__greater__(X4,X5) & X1 = X4)) => hp(X0)))),
% 184.43/41.41 inference(rectify,[],[f19])).
% 184.43/41.41 tff(f38,plain,(
% 184.43/41.41 ! [X0 : general,X1 : general] : (p__greater__(X0,X1) => (X0 != X1 & p__less_equal__(X1,X0)))),
% 184.43/41.41 inference(unused_predicate_definition_removal,[],[f12])).
% 184.43/41.41 tff(f39,plain,(
% 184.43/41.41 ! [X1 : general,X0 : general] : (p__less__(X1,X0) => (X0 != X1 & p__less_equal__(X1,X0)))),
% 184.43/41.41 inference(unused_predicate_definition_removal,[],[f33])).
% 184.43/41.41 tff(f40,plain,(
% 184.43/41.41 ! [X0 : general] : (p__is_symbolic__(X0) => ? [X1 : symbol] : X0 = f__symbolic__(X1))),
% 184.43/41.41 inference(unused_predicate_definition_removal,[],[f2])).
% 184.43/41.41 tff(f41,plain,(
% 184.43/41.41 ! [X0 : general] : (p__is_integer__(X0) => ? [X1 : $int] : X0 = f__integer__(X1))),
% 184.43/41.41 inference(unused_predicate_definition_removal,[],[f1])).
% 184.43/41.41 tff(f42,plain,(
% 184.43/41.41 ! [X0 : general,X1 : general] : ((X0 != X1 & p__less_equal__(X1,X0)) | ~p__less__(X1,X0))),
% 184.43/41.41 inference(ennf_transformation,[],[f39])).
% 184.43/41.41 tff(f43,plain,(
% 184.43/41.41 ? [X0 : general,X1 : general] : ((~tp(X0) & (? [X6 : general,X7 : general] : (p__less__(X6,X7) & f__integer__(5) = X7 & X1 = X6) & ? [X9 : general,X8 : general] : (X1 = X8 & p__greater__(X8,X9) & f__integer__(3) = X9) & X0 = X1)) | (~hp(X0) & (? [X3 : general,X2 : general] : (p__less__(X2,X3) & X2 = X1 & X3 = f__integer__(5)) & X0 = X1 & ? [X4 : general,X5 : general] : (f__integer__(3) = X5 & p__greater__(X4,X5) & X1 = X4))))),
% 184.43/41.41 inference(ennf_transformation,[],[f37])).
% 184.43/41.41 tff(f44,plain,(
% 184.43/41.41 ? [X1 : general,X0 : general] : ((? [X9 : general,X8 : general] : (X1 = X8 & p__greater__(X8,X9) & f__integer__(3) = X9) & X0 = X1 & ? [X6 : general,X7 : general] : (p__less__(X6,X7) & f__integer__(5) = X7 & X1 = X6) & ~tp(X0)) | (? [X3 : general,X2 : general] : (p__less__(X2,X3) & X2 = X1 & X3 = f__integer__(5)) & ? [X4 : general,X5 : general] : (f__integer__(3) = X5 & p__greater__(X4,X5) & X1 = X4) & ~hp(X0) & X0 = X1))),
% 184.43/41.41 inference(flattening,[],[f43])).
% 184.43/41.41 tff(f45,plain,(
% 184.43/41.41 ! [X0 : general] : ((hp(X0) | ($false | f__integer__(4) != X0)) & (tp(X0) | (f__integer__(4) != X0 | $false)))),
% 184.43/41.41 inference(ennf_transformation,[],[f17])).
% 184.43/41.41 tff(f46,plain,(
% 184.43/41.41 ! [X0 : general] : ((f__integer__(4) != X0 | $false | tp(X0)) & ($false | f__integer__(4) != X0 | hp(X0)))),
% 184.43/41.41 inference(flattening,[],[f45])).
% 184.43/41.41 tff(f47,plain,(
% 184.43/41.41 ! [X0 : general,X1 : general,X2 : general] : (p__less_equal__(X0,X2) | (~p__less_equal__(X1,X2) | ~p__less_equal__(X0,X1)))),
% 184.43/41.41 inference(ennf_transformation,[],[f8])).
% 184.43/41.41 tff(f48,plain,(
% 184.43/41.41 ! [X1 : general,X0 : general,X2 : general] : (p__less_equal__(X0,X2) | ~p__less_equal__(X0,X1) | ~p__less_equal__(X1,X2))),
% 184.43/41.41 inference(flattening,[],[f47])).
% 184.43/41.41 tff(f49,plain,(
% 184.43/41.41 ! [X1 : general,X0 : general] : (~p__greater__(X0,X1) | (X0 != X1 & p__less_equal__(X1,X0)))),
% 184.43/41.41 inference(ennf_transformation,[],[f38])).
% 184.43/41.41 tff(f50,plain,(
% 184.43/41.41 ! [X0 : general] : (~p__is_symbolic__(X0) | ? [X1 : symbol] : X0 = f__symbolic__(X1))),
% 184.43/41.41 inference(ennf_transformation,[],[f40])).
% 184.43/41.41 tff(f51,plain,(
% 184.43/41.41 ! [X0 : general] : (~p__is_integer__(X0) | ? [X1 : $int] : X0 = f__integer__(X1))),
% 184.43/41.41 inference(ennf_transformation,[],[f41])).
% 184.43/41.41 tff(f52,plain,(
% 184.43/41.41 ! [X1 : general,X0 : general] : (X0 = X1 | (~p__less_equal__(X0,X1) | ~p__less_equal__(X1,X0)))),
% 184.43/41.41 inference(ennf_transformation,[],[f36])).
% 184.43/41.41 tff(f53,plain,(
% 184.43/41.41 ! [X1 : general,X0 : general] : (X0 = X1 | ~p__less_equal__(X1,X0) | ~p__less_equal__(X0,X1))),
% 184.43/41.41 inference(flattening,[],[f52])).
% 184.43/41.41 tff(f54,plain,(
% 184.43/41.41 ! [X0 : general] : (~hp(X0) | tp(X0))),
% 184.43/41.41 inference(ennf_transformation,[],[f16])).
% 184.43/41.41 tff(f57,plain,(
% 184.43/41.41 ( ! [X0 : general,X1 : general] : (p__less_equal__(X1,X0) | p__less_equal__(X0,X1)) )),
% 184.43/41.41 inference(cnf_transformation,[],[f34])).
% 184.43/41.41 tff(f58,plain,(
% 184.43/41.41 ( ! [X2 : general,X0 : general,X1 : general] : (~p__less_equal__(X1,X2) | ~p__less_equal__(X0,X1) | p__less_equal__(X0,X2)) )),
% 184.43/41.41 inference(cnf_transformation,[],[f48])).
% 184.43/41.41 tff(f59,plain,(
% 184.43/41.41 ( ! [X0 : general] : (hp(X0) | f__integer__(4) != X0) )),
% 184.43/41.41 inference(cnf_transformation,[],[f46])).
% 184.43/41.41 tff(f61,plain,(
% 184.43/41.41 ( ! [X0 : general] : (~hp(X0) | tp(X0)) )),
% 184.43/41.41 inference(cnf_transformation,[],[f54])).
% 184.43/41.41 tff(f62,plain,(
% 184.43/41.41 ( ! [X0 : general,X1 : general] : (p__less_equal__(X1,X0) | ~p__less__(X1,X0)) )),
% 184.43/41.41 inference(cnf_transformation,[],[f42])).
% 184.43/41.41 tff(f63,plain,(
% 184.43/41.41 ( ! [X0 : general,X1 : general] : (~p__less__(X1,X0) | X0 != X1) )),
% 184.43/41.41 inference(cnf_transformation,[],[f42])).
% 184.43/41.41 tff(f64,plain,(
% 184.43/41.41 ( ! [X0 : general,X1 : general] : (~p__greater_equal__(X0,X1) | p__less_equal__(X1,X0)) )),
% 184.43/41.41 inference(cnf_transformation,[],[f11])).
% 184.43/41.41 tff(f65,plain,(
% 184.43/41.41 ( ! [X0 : general,X1 : general] : (~p__less_equal__(X1,X0) | p__greater_equal__(X0,X1)) )),
% 184.43/41.41 inference(cnf_transformation,[],[f11])).
% 184.43/41.41 tff(f66,plain,(
% 184.43/41.41 ( ! [X0 : $int,X1 : $int] : (p__less_equal__(f__integer__(X1),f__integer__(X0)) | $less(X0,X1)) )),
% 184.43/41.41 inference(cnf_transformation,[],[f35])).
% 184.43/41.41 tff(f67,plain,(
% 184.43/41.41 ( ! [X0 : $int,X1 : $int] : (~$less(X0,X1) | ~p__less_equal__(f__integer__(X1),f__integer__(X0))) )),
% 184.43/41.41 inference(cnf_transformation,[],[f35])).
% 184.43/41.41 tff(f74,plain,(
% 184.43/41.41 f__integer__(3) = sK8 | f__integer__(3) = sK3),
% 184.43/41.41 inference(cnf_transformation,[],[f44])).
% 184.43/41.41 tff(f75,plain,(
% 184.43/41.41 f__integer__(3) = sK3 | p__greater__(sK9,sK8)),
% 184.43/41.41 inference(cnf_transformation,[],[f44])).
% 184.43/41.41 tff(f76,plain,(
% 184.43/41.41 f__integer__(3) = sK3 | sK0 = sK9),
% 184.43/41.41 inference(cnf_transformation,[],[f44])).
% 184.43/41.41 tff(f77,plain,(
% 184.43/41.41 f__integer__(3) = sK8 | p__greater__(sK2,sK3)),
% 184.43/41.41 inference(cnf_transformation,[],[f44])).
% 184.43/41.41 tff(f78,plain,(
% 184.43/41.41 p__greater__(sK9,sK8) | p__greater__(sK2,sK3)),
% 184.43/41.41 inference(cnf_transformation,[],[f44])).
% 184.43/41.41 tff(f79,plain,(
% 184.43/41.41 p__greater__(sK2,sK3) | sK0 = sK9),
% 184.43/41.41 inference(cnf_transformation,[],[f44])).
% 184.43/41.41 tff(f80,plain,(
% 184.43/41.41 sK0 = sK2 | f__integer__(3) = sK8),
% 184.43/41.41 inference(cnf_transformation,[],[f44])).
% 184.43/41.41 tff(f81,plain,(
% 184.43/41.41 sK0 = sK2 | p__greater__(sK9,sK8)),
% 184.43/41.41 inference(cnf_transformation,[],[f44])).
% 184.43/41.41 tff(f82,plain,(
% 184.43/41.41 sK0 = sK2 | sK0 = sK9),
% 184.43/41.41 inference(cnf_transformation,[],[f44])).
% 184.43/41.41 tff(f83,plain,(
% 184.43/41.41 f__integer__(3) = sK8 | p__less__(sK5,sK4)),
% 184.43/41.41 inference(cnf_transformation,[],[f44])).
% 184.43/41.41 tff(f85,plain,(
% 184.43/41.41 p__less__(sK5,sK4) | sK0 = sK9),
% 184.43/41.41 inference(cnf_transformation,[],[f44])).
% 184.43/41.41 tff(f86,plain,(
% 184.43/41.41 sK5 = sK0 | f__integer__(3) = sK8),
% 184.43/41.41 inference(cnf_transformation,[],[f44])).
% 184.43/41.41 tff(f88,plain,(
% 184.43/41.41 sK5 = sK0 | sK0 = sK9),
% 184.43/41.41 inference(cnf_transformation,[],[f44])).
% 184.43/41.41 tff(f89,plain,(
% 184.43/41.41 f__integer__(5) = sK4 | f__integer__(3) = sK8),
% 184.43/41.41 inference(cnf_transformation,[],[f44])).
% 184.43/41.41 tff(f91,plain,(
% 184.43/41.41 f__integer__(5) = sK4 | sK0 = sK9),
% 184.43/41.41 inference(cnf_transformation,[],[f44])).
% 184.43/41.41 tff(f98,plain,(
% 184.43/41.41 f__integer__(3) = sK3 | sK0 = sK6),
% 184.43/41.41 inference(cnf_transformation,[],[f44])).
% 184.43/41.41 tff(f99,plain,(
% 184.43/41.41 f__integer__(3) = sK3 | f__integer__(5) = sK7),
% 184.43/41.41 inference(cnf_transformation,[],[f44])).
% 184.43/41.41 tff(f100,plain,(
% 184.43/41.41 p__less__(sK6,sK7) | f__integer__(3) = sK3),
% 184.43/41.41 inference(cnf_transformation,[],[f44])).
% 184.43/41.41 tff(f101,plain,(
% 184.43/41.41 p__greater__(sK2,sK3) | sK0 = sK6),
% 184.43/41.41 inference(cnf_transformation,[],[f44])).
% 184.43/41.41 tff(f102,plain,(
% 184.43/41.41 p__greater__(sK2,sK3) | f__integer__(5) = sK7),
% 184.43/41.41 inference(cnf_transformation,[],[f44])).
% 184.43/41.41 tff(f103,plain,(
% 184.43/41.41 p__less__(sK6,sK7) | p__greater__(sK2,sK3)),
% 184.43/41.41 inference(cnf_transformation,[],[f44])).
% 184.43/41.41 tff(f104,plain,(
% 184.43/41.41 sK0 = sK2 | sK0 = sK6),
% 184.43/41.41 inference(cnf_transformation,[],[f44])).
% 184.43/41.41 tff(f105,plain,(
% 184.43/41.41 sK0 = sK2 | f__integer__(5) = sK7),
% 184.43/41.41 inference(cnf_transformation,[],[f44])).
% 184.43/41.41 tff(f106,plain,(
% 184.43/41.41 sK0 = sK2 | p__less__(sK6,sK7)),
% 184.43/41.41 inference(cnf_transformation,[],[f44])).
% 184.43/41.41 tff(f107,plain,(
% 184.43/41.41 p__less__(sK5,sK4) | sK0 = sK6),
% 184.43/41.41 inference(cnf_transformation,[],[f44])).
% 184.43/41.41 tff(f108,plain,(
% 184.43/41.41 p__less__(sK5,sK4) | f__integer__(5) = sK7),
% 184.43/41.41 inference(cnf_transformation,[],[f44])).
% 184.43/41.41 tff(f109,plain,(
% 184.43/41.41 p__less__(sK5,sK4) | p__less__(sK6,sK7)),
% 184.43/41.41 inference(cnf_transformation,[],[f44])).
% 184.43/41.41 tff(f110,plain,(
% 184.43/41.41 sK5 = sK0 | sK0 = sK6),
% 184.43/41.41 inference(cnf_transformation,[],[f44])).
% 184.43/41.41 tff(f111,plain,(
% 184.43/41.41 sK5 = sK0 | f__integer__(5) = sK7),
% 184.43/41.41 inference(cnf_transformation,[],[f44])).
% 184.43/41.41 tff(f112,plain,(
% 184.43/41.41 sK5 = sK0 | p__less__(sK6,sK7)),
% 184.43/41.41 inference(cnf_transformation,[],[f44])).
% 184.43/41.41 tff(f113,plain,(
% 184.43/41.41 f__integer__(5) = sK4 | sK0 = sK6),
% 184.43/41.41 inference(cnf_transformation,[],[f44])).
% 184.43/41.41 tff(f114,plain,(
% 184.43/41.41 f__integer__(5) = sK7 | f__integer__(5) = sK4),
% 184.43/41.41 inference(cnf_transformation,[],[f44])).
% 184.43/41.41 tff(f115,plain,(
% 184.43/41.41 f__integer__(5) = sK4 | p__less__(sK6,sK7)),
% 184.43/41.41 inference(cnf_transformation,[],[f44])).
% 184.43/41.41 tff(f128,plain,(
% 184.43/41.41 ~tp(sK1) | ~hp(sK1)),
% 184.43/41.41 inference(cnf_transformation,[],[f44])).
% 184.43/41.41 tff(f131,plain,(
% 184.43/41.41 sK0 = sK1),
% 184.43/41.41 inference(cnf_transformation,[],[f44])).
% 184.43/41.41 tff(f132,plain,(
% 184.43/41.41 ( ! [X0 : general,X1 : general] : (~p__greater__(X0,X1) | p__less_equal__(X1,X0)) )),
% 184.43/41.41 inference(cnf_transformation,[],[f49])).
% 184.43/41.41 tff(f133,plain,(
% 184.43/41.41 ( ! [X0 : general,X1 : general] : (X0 != X1 | ~p__greater__(X0,X1)) )),
% 184.43/41.41 inference(cnf_transformation,[],[f49])).
% 184.43/41.41 tff(f134,plain,(
% 184.43/41.41 ( ! [X0 : general] : (c__supremum__ = X0 | c__infimum__ = X0 | p__is_integer__(X0) | p__is_symbolic__(X0)) )),
% 184.43/41.41 inference(cnf_transformation,[],[f3])).
% 184.43/41.41 tff(f135,plain,(
% 184.43/41.41 ( ! [X0 : general,X1 : general] : (~p__less_equal__(X0,X1) | X0 = X1 | ~p__less_equal__(X1,X0)) )),
% 184.43/41.41 inference(cnf_transformation,[],[f53])).
% 184.43/41.41 tff(f136,plain,(
% 184.43/41.41 ( ! [X0 : general] : (f__symbolic__(sK10(X0)) = X0 | ~p__is_symbolic__(X0)) )),
% 184.43/41.41 inference(cnf_transformation,[],[f50])).
% 184.43/41.41 tff(f137,plain,(
% 184.43/41.41 ( ! [X0 : symbol] : (p__less__(f__symbolic__(X0),c__supremum__)) )),
% 184.43/41.41 inference(cnf_transformation,[],[f15])).
% 184.43/41.41 tff(f138,plain,(
% 184.43/41.41 ( ! [X0 : general] : (~p__is_integer__(X0) | f__integer__(sK11(X0)) = X0) )),
% 184.43/41.41 inference(cnf_transformation,[],[f51])).
% 184.43/41.41 tff(f141,plain,(
% 184.43/41.41 ( ! [X0 : $int,X1 : symbol] : (p__less__(f__integer__(X0),f__symbolic__(X1))) )),
% 184.43/41.41 inference(cnf_transformation,[],[f14])).
% 184.43/41.41 tff(f142,plain,(
% 184.43/41.41 ( ! [X0 : $int] : (p__less__(c__infimum__,f__integer__(X0))) )),
% 184.43/41.41 inference(cnf_transformation,[],[f13])).
% 184.43/41.41 tff(f153,plain,(
% 184.43/41.41 f__integer__(5) = sK4 | sK6 = sK1),
% 184.43/41.41 inference(definition_unfolding,[],[f113,f131])).
% 184.43/41.41 tff(f154,plain,(
% 184.43/41.41 p__less__(sK6,sK7) | sK5 = sK1),
% 184.43/41.41 inference(definition_unfolding,[],[f112,f131])).
% 184.43/41.41 tff(f155,plain,(
% 184.43/41.41 sK5 = sK1 | f__integer__(5) = sK7),
% 184.43/41.41 inference(definition_unfolding,[],[f111,f131])).
% 184.43/41.41 tff(f156,plain,(
% 184.43/41.41 sK6 = sK1 | sK5 = sK1),
% 184.43/41.41 inference(definition_unfolding,[],[f110,f131,f131])).
% 184.43/41.41 tff(f157,plain,(
% 184.43/41.41 p__less__(sK5,sK4) | sK6 = sK1),
% 184.43/41.41 inference(definition_unfolding,[],[f107,f131])).
% 184.43/41.41 tff(f158,plain,(
% 184.43/41.41 p__less__(sK6,sK7) | sK2 = sK1),
% 184.43/41.41 inference(definition_unfolding,[],[f106,f131])).
% 184.43/41.41 tff(f159,plain,(
% 184.43/41.41 sK2 = sK1 | f__integer__(5) = sK7),
% 184.43/41.41 inference(definition_unfolding,[],[f105,f131])).
% 184.43/41.41 tff(f160,plain,(
% 184.43/41.41 sK2 = sK1 | sK6 = sK1),
% 184.43/41.41 inference(definition_unfolding,[],[f104,f131,f131])).
% 184.43/41.41 tff(f161,plain,(
% 184.43/41.41 sK6 = sK1 | p__greater__(sK2,sK3)),
% 184.43/41.41 inference(definition_unfolding,[],[f101,f131])).
% 184.43/41.41 tff(f162,plain,(
% 184.43/41.41 f__integer__(3) = sK3 | sK6 = sK1),
% 184.43/41.41 inference(definition_unfolding,[],[f98,f131])).
% 184.43/41.41 tff(f167,plain,(
% 184.43/41.41 sK9 = sK1 | f__integer__(5) = sK4),
% 184.43/41.41 inference(definition_unfolding,[],[f91,f131])).
% 184.43/41.41 tff(f168,plain,(
% 184.43/41.41 sK5 = sK1 | sK9 = sK1),
% 184.43/41.41 inference(definition_unfolding,[],[f88,f131,f131])).
% 184.43/41.41 tff(f170,plain,(
% 184.43/41.41 f__integer__(3) = sK8 | sK5 = sK1),
% 184.43/41.41 inference(definition_unfolding,[],[f86,f131])).
% 184.43/41.41 tff(f171,plain,(
% 184.43/41.41 p__less__(sK5,sK4) | sK9 = sK1),
% 184.43/41.41 inference(definition_unfolding,[],[f85,f131])).
% 184.43/41.41 tff(f172,plain,(
% 184.43/41.41 sK9 = sK1 | sK2 = sK1),
% 184.43/41.41 inference(definition_unfolding,[],[f82,f131,f131])).
% 184.43/41.41 tff(f173,plain,(
% 184.43/41.41 sK2 = sK1 | p__greater__(sK9,sK8)),
% 184.43/41.41 inference(definition_unfolding,[],[f81,f131])).
% 184.43/41.41 tff(f174,plain,(
% 184.43/41.41 f__integer__(3) = sK8 | sK2 = sK1),
% 184.43/41.41 inference(definition_unfolding,[],[f80,f131])).
% 184.43/41.41 tff(f175,plain,(
% 184.43/41.41 sK9 = sK1 | p__greater__(sK2,sK3)),
% 184.43/41.41 inference(definition_unfolding,[],[f79,f131])).
% 184.43/41.41 tff(f176,plain,(
% 184.43/41.41 sK9 = sK1 | f__integer__(3) = sK3),
% 184.43/41.41 inference(definition_unfolding,[],[f76,f131])).
% 184.43/41.41 tff(f183,plain,(
% 184.43/41.41 hp(f__integer__(4))),
% 184.43/41.41 inference(equality_resolution,[],[f59])).
% 184.43/41.41 tff(f184,plain,(
% 184.43/41.41 ( ! [X1 : general] : (~p__less__(X1,X1)) )),
% 184.43/41.41 inference(equality_resolution,[],[f63])).
% 184.43/41.41 tff(f185,plain,(
% 184.43/41.41 ( ! [X1 : general] : (~p__greater__(X1,X1)) )),
% 184.43/41.41 inference(equality_resolution,[],[f133])).
% 184.43/41.41 tff(f187,plain,(
% 184.43/41.41 ~p__less__(sK6,sK7) | p__greater__(sK2,sK3)),
% 184.43/41.41 inference(consistent_polarity_flipping,[],[f103])).
% 184.43/41.41 tff(f188,plain,(
% 184.43/41.41 ( ! [X0 : general,X1 : general] : (p__less_equal__(X1,X0) | p__less__(X1,X0)) )),
% 184.43/41.41 inference(consistent_polarity_flipping,[],[f62])).
% 184.43/41.41 tff(f189,plain,(
% 184.43/41.41 ( ! [X0 : general] : (p__is_symbolic__(X0) | f__symbolic__(sK10(X0)) = X0) )),
% 184.43/41.41 inference(consistent_polarity_flipping,[],[f136])).
% 184.43/41.41 tff(f190,plain,(
% 184.43/41.41 f__integer__(3) = sK3 | ~p__less__(sK6,sK7)),
% 184.43/41.41 inference(consistent_polarity_flipping,[],[f100])).
% 184.43/41.41 tff(f191,plain,(
% 184.43/41.41 ( ! [X1 : general] : (p__less__(X1,X1)) )),
% 184.43/41.41 inference(consistent_polarity_flipping,[],[f184])).
% 184.43/41.41 tff(f192,plain,(
% 184.43/41.41 ~p__less__(sK5,sK4) | ~p__less__(sK6,sK7)),
% 184.43/41.41 inference(consistent_polarity_flipping,[],[f109])).
% 184.43/41.41 tff(f193,plain,(
% 184.43/41.41 f__integer__(5) = sK7 | ~p__less__(sK5,sK4)),
% 184.43/41.41 inference(consistent_polarity_flipping,[],[f108])).
% 184.43/41.41 tff(f195,plain,(
% 184.43/41.41 ~p__less__(sK6,sK7) | sK2 = sK1),
% 184.43/41.41 inference(consistent_polarity_flipping,[],[f158])).
% 184.43/41.41 tff(f196,plain,(
% 184.43/41.41 ~hp(f__integer__(4))),
% 184.43/41.41 inference(consistent_polarity_flipping,[],[f183])).
% 184.43/41.41 tff(f198,plain,(
% 184.43/41.41 hp(sK1) | ~tp(sK1)),
% 184.43/41.41 inference(consistent_polarity_flipping,[],[f128])).
% 184.43/41.41 tff(f199,plain,(
% 184.43/41.41 ( ! [X0 : general] : (tp(X0) | hp(X0)) )),
% 184.43/41.41 inference(consistent_polarity_flipping,[],[f61])).
% 184.43/41.41 tff(f201,plain,(
% 184.43/41.41 ~p__less__(sK5,sK4) | sK9 = sK1),
% 184.43/41.41 inference(consistent_polarity_flipping,[],[f171])).
% 184.43/41.41 tff(f202,plain,(
% 184.43/41.41 ( ! [X0 : symbol] : (~p__less__(f__symbolic__(X0),c__supremum__)) )),
% 184.43/41.41 inference(consistent_polarity_flipping,[],[f137])).
% 184.43/41.41 tff(f203,plain,(
% 184.43/41.41 f__integer__(5) = sK4 | ~p__less__(sK6,sK7)),
% 184.43/41.41 inference(consistent_polarity_flipping,[],[f115])).
% 184.43/41.41 tff(f204,plain,(
% 184.43/41.41 ( ! [X0 : $int,X1 : symbol] : (~p__less__(f__integer__(X0),f__symbolic__(X1))) )),
% 184.43/41.41 inference(consistent_polarity_flipping,[],[f141])).
% 184.43/41.41 tff(f205,plain,(
% 184.43/41.41 ~p__less__(sK6,sK7) | sK5 = sK1),
% 184.43/41.41 inference(consistent_polarity_flipping,[],[f154])).
% 184.43/41.41 tff(f209,plain,(
% 184.43/41.41 ( ! [X0 : $int] : (~p__less__(c__infimum__,f__integer__(X0))) )),
% 184.43/41.41 inference(consistent_polarity_flipping,[],[f142])).
% 184.43/41.41 tff(f212,plain,(
% 184.43/41.41 ~p__less__(sK5,sK4) | f__integer__(3) = sK8),
% 184.43/41.41 inference(consistent_polarity_flipping,[],[f83])).
% 184.43/41.41 tff(f216,plain,(
% 184.43/41.41 ~p__less__(sK5,sK4) | sK6 = sK1),
% 184.43/41.41 inference(consistent_polarity_flipping,[],[f157])).
% 184.43/41.41 tff(f217,plain,(
% 184.43/41.41 ( ! [X0 : general] : (~p__is_symbolic__(X0) | c__supremum__ = X0 | c__infimum__ = X0 | p__is_integer__(X0)) )),
% 184.43/41.41 inference(consistent_polarity_flipping,[],[f134])).
% 184.43/41.41 tff(f219,definition,(
% 184.43/41.41 spl12_1 <=> tp(sK1)),
% 184.43/41.41 introduced(definition,[new_symbols(definition,[spl12_1])],[avatar_definition])).
% 184.43/41.41 tff(f221,plain,(
% 184.43/41.41 ~tp(sK1) | spl12_1),
% 184.43/41.41 inference(avatar_component_clause,[],[f219])).
% 184.43/41.41 tff(f223,definition,(
% 184.43/41.41 spl12_2 <=> p__greater__(sK2,sK3)),
% 184.43/41.41 introduced(definition,[new_symbols(definition,[spl12_2])],[avatar_definition])).
% 184.43/41.41 tff(f225,plain,(
% 184.43/41.41 p__greater__(sK2,sK3) | ~spl12_2),
% 184.43/41.41 inference(avatar_component_clause,[],[f223])).
% 184.43/41.41 tff(f228,definition,(
% 184.43/41.41 spl12_3 <=> f__integer__(5) = sK4),
% 184.43/41.41 introduced(definition,[new_symbols(definition,[spl12_3])],[avatar_definition])).
% 184.43/41.41 tff(f230,plain,(
% 184.43/41.41 f__integer__(5) = sK4 | ~spl12_3),
% 184.43/41.41 inference(avatar_component_clause,[],[f228])).
% 184.43/41.41 tff(f232,definition,(
% 184.43/41.41 spl12_4 <=> sK6 = sK1),
% 184.43/41.41 introduced(definition,[new_symbols(definition,[spl12_4])],[avatar_definition])).
% 184.43/41.41 tff(f234,plain,(
% 184.43/41.41 sK6 = sK1 | ~spl12_4),
% 184.43/41.41 inference(avatar_component_clause,[],[f232])).
% 184.43/41.41 tff(f235,plain,(
% 184.43/41.41 spl12_3 | spl12_4),
% 184.43/41.41 inference(avatar_split_clause,[],[f153,f232,f228])).
% 184.43/41.41 tff(f237,definition,(
% 184.43/41.41 spl12_5 <=> hp(sK1)),
% 184.43/41.41 introduced(definition,[new_symbols(definition,[spl12_5])],[avatar_definition])).
% 184.43/41.41 tff(f239,plain,(
% 184.43/41.41 hp(sK1) | ~spl12_5),
% 184.43/41.41 inference(avatar_component_clause,[],[f237])).
% 184.43/41.41 tff(f240,plain,(
% 184.43/41.41 ~spl12_1 | spl12_5),
% 184.43/41.41 inference(avatar_split_clause,[],[f198,f237,f219])).
% 184.43/41.41 tff(f242,definition,(
% 184.43/41.41 spl12_6 <=> sK5 = sK1),
% 184.43/41.41 introduced(definition,[new_symbols(definition,[spl12_6])],[avatar_definition])).
% 184.43/41.41 tff(f244,plain,(
% 184.43/41.41 sK5 = sK1 | ~spl12_6),
% 184.43/41.41 inference(avatar_component_clause,[],[f242])).
% 184.43/41.41 tff(f245,plain,(
% 184.43/41.41 spl12_6 | spl12_4),
% 184.43/41.41 inference(avatar_split_clause,[],[f156,f232,f242])).
% 184.43/41.41 tff(f247,definition,(
% 184.43/41.41 spl12_7 <=> f__integer__(5) = sK7),
% 184.43/41.41 introduced(definition,[new_symbols(definition,[spl12_7])],[avatar_definition])).
% 184.43/41.41 tff(f249,plain,(
% 184.43/41.41 f__integer__(5) = sK7 | ~spl12_7),
% 184.43/41.41 inference(avatar_component_clause,[],[f247])).
% 184.43/41.41 tff(f250,plain,(
% 184.43/41.41 spl12_2 | spl12_7),
% 184.43/41.41 inference(avatar_split_clause,[],[f102,f247,f223])).
% 184.43/41.41 tff(f252,definition,(
% 184.43/41.41 spl12_8 <=> f__integer__(3) = sK8),
% 184.43/41.41 introduced(definition,[new_symbols(definition,[spl12_8])],[avatar_definition])).
% 184.43/41.41 tff(f254,plain,(
% 184.43/41.41 f__integer__(3) = sK8 | ~spl12_8),
% 184.43/41.41 inference(avatar_component_clause,[],[f252])).
% 184.43/41.41 tff(f255,plain,(
% 184.43/41.41 spl12_3 | spl12_8),
% 184.43/41.41 inference(avatar_split_clause,[],[f89,f252,f228])).
% 184.43/41.41 tff(f257,definition,(
% 184.43/41.41 spl12_9 <=> p__less__(sK6,sK7)),
% 184.43/41.41 introduced(definition,[new_symbols(definition,[spl12_9])],[avatar_definition])).
% 184.43/41.41 tff(f259,plain,(
% 184.43/41.41 ~p__less__(sK6,sK7) | spl12_9),
% 184.43/41.41 inference(avatar_component_clause,[],[f257])).
% 184.43/41.41 tff(f260,plain,(
% 184.43/41.41 spl12_2 | ~spl12_9),
% 184.43/41.41 inference(avatar_split_clause,[],[f187,f257,f223])).
% 184.43/41.41 tff(f262,definition,(
% 184.43/41.41 spl12_10 <=> sK9 = sK1),
% 184.43/41.41 introduced(definition,[new_symbols(definition,[spl12_10])],[avatar_definition])).
% 184.43/41.41 tff(f264,plain,(
% 184.43/41.41 sK9 = sK1 | ~spl12_10),
% 184.43/41.41 inference(avatar_component_clause,[],[f262])).
% 184.43/41.41 tff(f265,plain,(
% 184.43/41.41 spl12_2 | spl12_10),
% 184.43/41.41 inference(avatar_split_clause,[],[f175,f262,f223])).
% 184.43/41.41 tff(f267,definition,(
% 184.43/41.41 spl12_11 <=> f__integer__(3) = sK3),
% 184.43/41.41 introduced(definition,[new_symbols(definition,[spl12_11])],[avatar_definition])).
% 184.43/41.41 tff(f269,plain,(
% 184.43/41.41 f__integer__(3) = sK3 | ~spl12_11),
% 184.43/41.41 inference(avatar_component_clause,[],[f267])).
% 184.43/41.41 tff(f270,plain,(
% 184.43/41.41 spl12_11 | spl12_8),
% 184.43/41.41 inference(avatar_split_clause,[],[f74,f252,f267])).
% 184.43/41.41 tff(f272,definition,(
% 184.43/41.41 spl12_12 <=> p__greater__(sK9,sK8)),
% 184.43/41.41 introduced(definition,[new_symbols(definition,[spl12_12])],[avatar_definition])).
% 184.43/41.41 tff(f274,plain,(
% 184.43/41.41 p__greater__(sK9,sK8) | ~spl12_12),
% 184.43/41.41 inference(avatar_component_clause,[],[f272])).
% 184.43/41.41 tff(f277,definition,(
% 184.43/41.41 spl12_13 <=> sK2 = sK1),
% 184.43/41.41 introduced(definition,[new_symbols(definition,[spl12_13])],[avatar_definition])).
% 184.43/41.41 tff(f279,plain,(
% 184.43/41.41 sK2 = sK1 | ~spl12_13),
% 184.43/41.41 inference(avatar_component_clause,[],[f277])).
% 184.43/41.41 tff(f280,plain,(
% 184.43/41.41 spl12_13 | spl12_4),
% 184.43/41.41 inference(avatar_split_clause,[],[f160,f232,f277])).
% 184.43/41.41 tff(f281,plain,(
% 184.43/41.41 spl12_4 | spl12_2),
% 184.43/41.42 inference(avatar_split_clause,[],[f161,f223,f232])).
% 184.43/41.42 tff(f282,plain,(
% 184.43/41.42 spl12_13 | ~spl12_9),
% 184.43/41.42 inference(avatar_split_clause,[],[f195,f257,f277])).
% 184.43/41.42 tff(f284,plain,(
% 184.43/41.42 spl12_11 | spl12_4),
% 184.43/41.42 inference(avatar_split_clause,[],[f162,f232,f267])).
% 184.43/41.42 tff(f286,definition,(
% 184.43/41.42 spl12_14 <=> p__less__(sK5,sK4)),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_14])],[avatar_definition])).
% 184.43/41.42 tff(f288,plain,(
% 184.43/41.42 ~p__less__(sK5,sK4) | spl12_14),
% 184.43/41.42 inference(avatar_component_clause,[],[f286])).
% 184.43/41.42 tff(f289,plain,(
% 184.43/41.42 ~spl12_14 | spl12_8),
% 184.43/41.42 inference(avatar_split_clause,[],[f212,f252,f286])).
% 184.43/41.42 tff(f290,plain,(
% 184.43/41.42 spl12_6 | spl12_7),
% 184.43/41.42 inference(avatar_split_clause,[],[f155,f247,f242])).
% 184.43/41.42 tff(f292,plain,(
% 184.43/41.42 ~spl12_9 | spl12_6),
% 184.43/41.42 inference(avatar_split_clause,[],[f205,f242,f257])).
% 184.43/41.42 tff(f293,plain,(
% 184.43/41.42 spl12_7 | spl12_3),
% 184.43/41.42 inference(avatar_split_clause,[],[f114,f228,f247])).
% 184.43/41.42 tff(f294,plain,(
% 184.43/41.42 spl12_13 | spl12_12),
% 184.43/41.42 inference(avatar_split_clause,[],[f173,f272,f277])).
% 184.43/41.42 tff(f297,plain,(
% 184.43/41.42 spl12_10 | spl12_11),
% 184.43/41.42 inference(avatar_split_clause,[],[f176,f267,f262])).
% 184.43/41.42 tff(f298,plain,(
% 184.43/41.42 spl12_10 | spl12_3),
% 184.43/41.42 inference(avatar_split_clause,[],[f167,f228,f262])).
% 184.43/41.42 tff(f300,plain,(
% 184.43/41.42 spl12_8 | spl12_2),
% 184.43/41.42 inference(avatar_split_clause,[],[f77,f223,f252])).
% 184.43/41.42 tff(f302,plain,(
% 184.43/41.42 ~spl12_14 | ~spl12_9),
% 184.43/41.42 inference(avatar_split_clause,[],[f192,f257,f286])).
% 184.43/41.42 tff(f303,plain,(
% 184.43/41.42 spl12_13 | spl12_7),
% 184.43/41.42 inference(avatar_split_clause,[],[f159,f247,f277])).
% 184.43/41.42 tff(f304,plain,(
% 184.43/41.42 spl12_10 | spl12_6),
% 184.43/41.42 inference(avatar_split_clause,[],[f168,f242,f262])).
% 184.43/41.42 tff(f305,plain,(
% 184.43/41.42 spl12_2 | spl12_12),
% 184.43/41.42 inference(avatar_split_clause,[],[f78,f272,f223])).
% 184.43/41.42 tff(f307,plain,(
% 184.43/41.42 spl12_11 | ~spl12_9),
% 184.43/41.42 inference(avatar_split_clause,[],[f190,f257,f267])).
% 184.43/41.42 tff(f309,plain,(
% 184.43/41.42 spl12_4 | ~spl12_14),
% 184.43/41.42 inference(avatar_split_clause,[],[f216,f286,f232])).
% 184.43/41.42 tff(f310,plain,(
% 184.43/41.42 spl12_7 | spl12_11),
% 184.43/41.42 inference(avatar_split_clause,[],[f99,f267,f247])).
% 184.43/41.42 tff(f312,plain,(
% 184.43/41.42 spl12_12 | spl12_11),
% 184.43/41.42 inference(avatar_split_clause,[],[f75,f267,f272])).
% 184.43/41.42 tff(f316,plain,(
% 184.43/41.42 spl12_10 | spl12_13),
% 184.43/41.42 inference(avatar_split_clause,[],[f172,f277,f262])).
% 184.43/41.42 tff(f318,plain,(
% 184.43/41.42 spl12_10 | ~spl12_14),
% 184.43/41.42 inference(avatar_split_clause,[],[f201,f286,f262])).
% 184.43/41.42 tff(f319,plain,(
% 184.43/41.42 spl12_8 | spl12_13),
% 184.43/41.42 inference(avatar_split_clause,[],[f174,f277,f252])).
% 184.43/41.42 tff(f320,plain,(
% 184.43/41.42 spl12_7 | ~spl12_14),
% 184.43/41.42 inference(avatar_split_clause,[],[f193,f286,f247])).
% 184.43/41.42 tff(f321,plain,(
% 184.43/41.42 spl12_8 | spl12_6),
% 184.43/41.42 inference(avatar_split_clause,[],[f170,f242,f252])).
% 184.43/41.42 tff(f322,plain,(
% 184.43/41.42 spl12_3 | ~spl12_9),
% 184.43/41.42 inference(avatar_split_clause,[],[f203,f257,f228])).
% 184.43/41.42 tff(f323,plain,(
% 184.43/41.42 ~p__less__(sK1,sK7) | (~spl12_4 | spl12_9)),
% 184.43/41.42 inference(forward_demodulation,[],[f259,f234])).
% 184.43/41.42 tff(f324,plain,(
% 184.43/41.42 p__greater__(sK1,sK8) | (~spl12_10 | ~spl12_12)),
% 184.43/41.42 inference(forward_demodulation,[],[f274,f264])).
% 184.43/41.42 tff(f325,plain,(
% 184.43/41.42 hp(sK1) | spl12_1),
% 184.43/41.42 inference(resolution,[],[f199,f221])).
% 184.43/41.42 tff(f326,plain,(
% 184.43/41.42 spl12_5 | spl12_1),
% 184.43/41.42 inference(avatar_split_clause,[],[f325,f219,f237])).
% 184.43/41.42 tff(f328,plain,(
% 184.43/41.42 ~p__less__(c__infimum__,sK8) | ~spl12_8),
% 184.43/41.42 inference(superposition,[],[f209,f254])).
% 184.43/41.42 tff(f329,plain,(
% 184.43/41.42 ( ! [X0 : symbol] : (~p__less__(sK7,f__symbolic__(X0))) ) | ~spl12_7),
% 184.43/41.42 inference(superposition,[],[f204,f249])).
% 184.43/41.42 tff(f330,plain,(
% 184.43/41.42 ( ! [X0 : symbol] : (~p__less__(sK8,f__symbolic__(X0))) ) | ~spl12_8),
% 184.43/41.42 inference(superposition,[],[f204,f254])).
% 184.43/41.42 tff(f332,plain,(
% 184.43/41.42 ( ! [X0 : general] : (p__less_equal__(X0,X0)) )),
% 184.43/41.42 inference(factoring,[],[f57])).
% 184.43/41.42 tff(f335,plain,(
% 184.43/41.42 p__less_equal__(sK8,sK1) | (~spl12_10 | ~spl12_12)),
% 184.43/41.42 inference(resolution,[],[f132,f324])).
% 184.43/41.42 tff(f343,plain,(
% 184.43/41.42 ( ! [X0 : $int] : ($less(X0,$sum(X0,1))) )),
% 184.43/41.42 inference(resolution,[],[f30,f26])).
% 184.43/41.42 tff(f344,plain,(
% 184.43/41.42 ( ! [X0 : $int,X1 : $int] : ($less(X1,$sum(1,X0)) | $less(X0,X1)) )),
% 184.43/41.42 inference(superposition,[],[f30,f21])).
% 184.43/41.42 tff(f348,plain,(
% 184.43/41.42 ( ! [X0 : $int,X1 : $int] : (p__greater_equal__(f__integer__(X0),f__integer__(X1)) | $less(X0,X1)) )),
% 184.43/41.42 inference(resolution,[],[f66,f65])).
% 184.43/41.42 tff(f349,plain,(
% 184.43/41.42 ( ! [X0 : $int] : (p__less_equal__(sK7,f__integer__(X0)) | $less(X0,5)) ) | ~spl12_7),
% 184.43/41.42 inference(superposition,[],[f66,f249])).
% 184.43/41.42 tff(f350,plain,(
% 184.43/41.42 ( ! [X0 : $int] : (p__less_equal__(sK8,f__integer__(X0)) | $less(X0,3)) ) | ~spl12_8),
% 184.43/41.42 inference(superposition,[],[f66,f254])).
% 184.43/41.42 tff(f352,plain,(
% 184.43/41.42 ( ! [X0 : $int] : (p__less_equal__(f__integer__(X0),sK8) | $less(3,X0)) ) | ~spl12_8),
% 184.43/41.42 inference(superposition,[],[f66,f254])).
% 184.43/41.42 tff(f358,plain,(
% 184.43/41.42 ( ! [X0 : $int,X1 : $int] : (~p__less_equal__(f__integer__($sum(X0,1)),f__integer__(X1)) | $less(X0,X1)) )),
% 184.43/41.42 inference(resolution,[],[f67,f30])).
% 184.43/41.42 tff(f370,plain,(
% 184.43/41.42 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less($sum(X0,1),X1) | $less(X2,X1) | $less(X0,X2)) )),
% 184.43/41.42 inference(resolution,[],[f27,f30])).
% 184.43/41.42 tff(f372,plain,(
% 184.43/41.42 ( ! [X0 : $int,X1 : $int] : (~p__less_equal__(f__integer__(X1),f__integer__(X0)) | X0 = X1 | $less(X1,X0)) )),
% 184.43/41.42 inference(resolution,[],[f28,f67])).
% 184.43/41.42 tff(f373,plain,(
% 184.43/41.42 ( ! [X0 : $int,X1 : $int] : (~$less(X1,$sum(X0,1)) | X0 = X1 | $less(X1,X0)) )),
% 184.43/41.42 inference(resolution,[],[f28,f32])).
% 184.43/41.42 tff(f381,plain,(
% 184.43/41.42 ( ! [X2 : general,X0 : general,X1 : general] : (~p__less_equal__(X0,X1) | p__less_equal__(X0,X2) | p__less__(X1,X2)) )),
% 184.43/41.42 inference(resolution,[],[f58,f188])).
% 184.43/41.42 tff(f382,plain,(
% 184.43/41.42 ( ! [X2 : general,X0 : general,X1 : general] : (~p__less_equal__(X0,X1) | p__less_equal__(X2,X1) | p__less_equal__(X0,X2)) )),
% 184.43/41.42 inference(resolution,[],[f58,f57])).
% 184.43/41.42 tff(f384,plain,(
% 184.43/41.42 ( ! [X2 : $int,X0 : general,X1 : $int] : (~p__less_equal__(X0,f__integer__(X1)) | $less(X2,X1) | p__less_equal__(X0,f__integer__(X2))) )),
% 184.43/41.42 inference(resolution,[],[f58,f66])).
% 184.43/41.42 tff(f388,plain,(
% 184.43/41.42 ( ! [X0 : general] : (~p__less_equal__(X0,sK8) | p__less_equal__(X0,sK1)) ) | (~spl12_10 | ~spl12_12)),
% 184.43/41.42 inference(resolution,[],[f58,f335])).
% 184.43/41.42 tff(f391,plain,(
% 184.43/41.42 ( ! [X0 : general,X1 : general] : (~p__less_equal__(X1,X0) | p__less__(X0,X1) | X0 = X1) )),
% 184.43/41.42 inference(resolution,[],[f135,f188])).
% 184.43/41.42 tff(f394,plain,(
% 184.43/41.42 ( ! [X0 : $int,X1 : $int] : (~p__less_equal__(f__integer__(X1),f__integer__(X0)) | $less(X1,X0) | f__integer__(X1) = f__integer__(X0)) )),
% 184.43/41.42 inference(resolution,[],[f135,f66])).
% 184.43/41.42 tff(f398,plain,(
% 184.43/41.42 sK8 = sK1 | ~p__less_equal__(sK1,sK8) | (~spl12_10 | ~spl12_12)),
% 184.43/41.42 inference(resolution,[],[f135,f335])).
% 184.43/41.42 tff(f402,definition,(
% 184.43/41.42 spl12_15 <=> p__less_equal__(sK7,sK8)),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_15])],[avatar_definition])).
% 184.43/41.42 tff(f404,plain,(
% 184.43/41.42 ~p__less_equal__(sK7,sK8) | spl12_15),
% 184.43/41.42 inference(avatar_component_clause,[],[f402])).
% 184.43/41.42 tff(f411,definition,(
% 184.43/41.42 spl12_17 <=> sK8 = sK1),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_17])],[avatar_definition])).
% 184.43/41.42 tff(f412,plain,(
% 184.43/41.42 sK8 != sK1 | spl12_17),
% 184.43/41.42 inference(avatar_component_clause,[],[f411])).
% 184.43/41.42 tff(f413,plain,(
% 184.43/41.42 sK8 = sK1 | ~spl12_17),
% 184.43/41.42 inference(avatar_component_clause,[],[f411])).
% 184.43/41.42 tff(f415,definition,(
% 184.43/41.42 spl12_18 <=> p__less_equal__(sK1,sK8)),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_18])],[avatar_definition])).
% 184.43/41.42 tff(f417,plain,(
% 184.43/41.42 ~p__less_equal__(sK1,sK8) | spl12_18),
% 184.43/41.42 inference(avatar_component_clause,[],[f415])).
% 184.43/41.42 tff(f418,plain,(
% 184.43/41.42 spl12_17 | ~spl12_18 | ~spl12_10 | ~spl12_12),
% 184.43/41.42 inference(avatar_split_clause,[],[f398,f272,f262,f415,f411])).
% 184.43/41.42 tff(f431,plain,(
% 184.43/41.42 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($less($sum(X0,X1),$sum($sum(X2,1),X1)) | $less(X2,X0)) )),
% 184.43/41.42 inference(resolution,[],[f29,f30])).
% 184.43/41.42 tff(f436,plain,(
% 184.43/41.42 ( ! [X0 : general] : (p__is_integer__(X0) | f__symbolic__(sK10(X0)) = X0 | c__infimum__ = X0 | c__supremum__ = X0) )),
% 184.43/41.42 inference(resolution,[],[f217,f189])).
% 184.43/41.42 tff(f465,plain,(
% 184.43/41.42 ( ! [X0 : $int] : (~p__less_equal__(sK8,f__integer__(X0)) | f__integer__(X0) = sK8 | $less(3,X0)) ) | ~spl12_8),
% 184.43/41.42 inference(resolution,[],[f352,f135])).
% 184.43/41.42 tff(f481,plain,(
% 184.43/41.42 ( ! [X0 : $int] : (~p__less_equal__(f__integer__($sum(X0,1)),f__integer__(X0))) )),
% 184.43/41.42 inference(resolution,[],[f343,f67])).
% 184.43/41.42 tff(f483,plain,(
% 184.43/41.42 ( ! [X0 : $int] : ($less(X0,$sum(1,X0))) )),
% 184.43/41.42 inference(superposition,[],[f343,f21])).
% 184.43/41.42 tff(f510,plain,(
% 184.43/41.42 ( ! [X0 : $int] : ($less(0,X0) | $less(X0,1)) )),
% 184.43/41.42 inference(superposition,[],[f344,f23])).
% 184.43/41.42 tff(f548,plain,(
% 184.43/41.42 ( ! [X2 : general,X0 : general,X1 : general] : (p__less__(X0,X2) | p__less__(X2,X1) | p__less_equal__(X0,X1)) )),
% 184.43/41.42 inference(resolution,[],[f381,f188])).
% 184.43/41.42 tff(f570,plain,(
% 184.43/41.42 ( ! [X0 : general,X1 : $int] : (p__less_equal__(f__integer__(X1),X0) | $less(3,X1) | p__less_equal__(X0,sK8)) ) | ~spl12_8),
% 184.43/41.42 inference(resolution,[],[f382,f352])).
% 184.43/41.42 tff(f589,plain,(
% 184.43/41.42 sK8 = sK1 | p__less__(sK1,sK8) | (~spl12_10 | ~spl12_12)),
% 184.43/41.42 inference(resolution,[],[f391,f335])).
% 184.43/41.42 tff(f623,plain,(
% 184.43/41.42 ( ! [X0 : $int] : (~p__less_equal__(f__integer__($sum(X0,1)),sK7) | $less(X0,5)) ) | ~spl12_7),
% 184.43/41.42 inference(superposition,[],[f358,f249])).
% 184.43/41.42 tff(f785,plain,(
% 184.43/41.42 ( ! [X0 : $int] : (~p__less_equal__(f__integer__(X0),sK8) | $less(X0,3) | 3 = X0) ) | ~spl12_8),
% 184.43/41.42 inference(superposition,[],[f372,f254])).
% 184.43/41.42 tff(f791,plain,(
% 184.43/41.42 ( ! [X0 : $int,X1 : $int] : (~$less(X1,$sum(1,X0)) | X0 = X1 | $less(X1,X0)) )),
% 184.43/41.42 inference(superposition,[],[f373,f21])).
% 184.43/41.42 tff(f802,plain,(
% 184.43/41.42 ( ! [X0 : $int,X1 : $int] : (p__less_equal__(sK8,f__integer__(X0)) | $less(X1,3) | $less(X0,X1)) ) | ~spl12_8),
% 184.43/41.42 inference(resolution,[],[f384,f350])).
% 184.43/41.42 tff(f973,plain,(
% 184.43/41.42 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($less($sum(X0,X1),$sum(X2,$sum(1,X1))) | $less(X2,X0)) )),
% 184.43/41.42 inference(forward_demodulation,[],[f431,f22])).
% 184.43/41.42 tff(f1003,plain,(
% 184.43/41.42 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($less(X2,$sum(X0,$sum(1,1))) | $less(X0,X1) | $less(X1,X2)) )),
% 184.43/41.42 inference(resolution,[],[f973,f370])).
% 184.43/41.42 tff(f1038,plain,(
% 184.43/41.42 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($less(X1,X2) | $less(X2,$sum(X0,2)) | $less(X0,X1)) )),
% 184.43/41.42 inference(evaluation,[],[f1003])).
% 184.43/41.42 tff(f1101,plain,(
% 184.43/41.42 ( ! [X0 : general] : (f__symbolic__(sK10(X0)) = X0 | c__infimum__ = X0 | f__integer__(sK11(X0)) = X0 | c__supremum__ = X0) )),
% 184.43/41.42 inference(resolution,[],[f436,f138])).
% 184.43/41.42 tff(f1251,definition,(
% 184.43/41.42 spl12_19 <=> c__infimum__ = sK8),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_19])],[avatar_definition])).
% 184.43/41.42 tff(f1252,plain,(
% 184.43/41.42 c__infimum__ != sK8 | spl12_19),
% 184.43/41.42 inference(avatar_component_clause,[],[f1251])).
% 184.43/41.42 tff(f1253,plain,(
% 184.43/41.42 c__infimum__ = sK8 | ~spl12_19),
% 184.43/41.42 inference(avatar_component_clause,[],[f1251])).
% 184.43/41.42 tff(f1271,plain,(
% 184.43/41.42 ~p__less__(sK8,sK8) | (~spl12_8 | ~spl12_19)),
% 184.43/41.42 inference(superposition,[],[f328,f1253])).
% 184.43/41.42 tff(f1274,plain,(
% 184.43/41.42 $false | (~spl12_8 | ~spl12_19)),
% 184.43/41.42 inference(forward_subsumption_resolution,[],[f1271,f191])).
% 184.43/41.42 tff(f1275,plain,(
% 184.43/41.42 ~spl12_8 | ~spl12_19),
% 184.43/41.42 inference(avatar_contradiction_clause,[],[f1274])).
% 184.43/41.42 tff(f1320,definition,(
% 184.43/41.42 spl12_23 <=> p__less_equal__(sK8,sK7)),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_23])],[avatar_definition])).
% 184.43/41.42 tff(f1322,plain,(
% 184.43/41.42 p__less_equal__(sK8,sK7) | ~spl12_23),
% 184.43/41.42 inference(avatar_component_clause,[],[f1320])).
% 184.43/41.42 tff(f1327,plain,(
% 184.43/41.42 p__less_equal__(sK3,sK2) | ~spl12_2),
% 184.43/41.42 inference(resolution,[],[f225,f132])).
% 184.43/41.42 tff(f1329,plain,(
% 184.43/41.42 ~p__less__(sK1,sK4) | (~spl12_6 | spl12_14)),
% 184.43/41.42 inference(forward_demodulation,[],[f288,f244])).
% 184.43/41.42 tff(f1336,plain,(
% 184.43/41.42 ( ! [X0 : symbol] : (~p__less__(sK4,f__symbolic__(X0))) ) | ~spl12_3),
% 184.43/41.42 inference(superposition,[],[f204,f230])).
% 184.43/41.42 tff(f1338,plain,(
% 184.43/41.42 ( ! [X0 : $int] : (p__greater_equal__(f__integer__(X0),sK4) | $less(X0,5)) ) | ~spl12_3),
% 184.43/41.42 inference(superposition,[],[f348,f230])).
% 184.43/41.42 tff(f1358,plain,(
% 184.43/41.42 p__less_equal__(sK3,sK1) | (~spl12_2 | ~spl12_13)),
% 184.43/41.42 inference(forward_demodulation,[],[f1327,f279])).
% 184.43/41.42 tff(f1361,plain,(
% 184.43/41.42 ( ! [X0 : $int] : (p__less_equal__(f__integer__(X0),sK3) | $less(3,X0)) ) | ~spl12_11),
% 184.43/41.42 inference(superposition,[],[f66,f269])).
% 184.43/41.42 tff(f1365,plain,(
% 184.43/41.42 ~p__less__(c__infimum__,sK3) | ~spl12_11),
% 184.43/41.42 inference(superposition,[],[f209,f269])).
% 184.43/41.42 tff(f1367,plain,(
% 184.43/41.42 ( ! [X0 : $int] : (p__greater_equal__(sK3,f__integer__(X0)) | $less(3,X0)) ) | ~spl12_11),
% 184.43/41.42 inference(superposition,[],[f348,f269])).
% 184.43/41.42 tff(f1377,plain,(
% 184.43/41.42 ( ! [X0 : $int] : (~p__less_equal__(sK3,f__integer__(X0)) | f__integer__(X0) = sK3 | $less(3,X0)) ) | ~spl12_11),
% 184.43/41.42 inference(superposition,[],[f394,f269])).
% 184.43/41.42 tff(f1400,plain,(
% 184.43/41.42 ( ! [X0 : general] : (p__less_equal__(sK3,X0) | p__less_equal__(X0,sK1)) ) | (~spl12_2 | ~spl12_13)),
% 184.43/41.42 inference(resolution,[],[f1358,f382])).
% 184.43/41.42 tff(f1403,plain,(
% 184.43/41.42 ( ! [X0 : general] : (~p__less_equal__(X0,sK3) | p__less_equal__(X0,sK1)) ) | (~spl12_2 | ~spl12_13)),
% 184.43/41.42 inference(resolution,[],[f1358,f58])).
% 184.43/41.42 tff(f1406,definition,(
% 184.43/41.42 spl12_25 <=> sK3 = sK1),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_25])],[avatar_definition])).
% 184.43/41.42 tff(f1408,plain,(
% 184.43/41.42 sK3 = sK1 | ~spl12_25),
% 184.43/41.42 inference(avatar_component_clause,[],[f1406])).
% 184.43/41.42 tff(f1410,definition,(
% 184.43/41.42 spl12_26 <=> p__less_equal__(sK1,sK3)),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_26])],[avatar_definition])).
% 184.43/41.42 tff(f1468,definition,(
% 184.43/41.42 spl12_28 <=> ! [X0 : $int] : ($less(5,X0) | $less(X0,3))),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_28])],[avatar_definition])).
% 184.43/41.42 tff(f1469,plain,(
% 184.43/41.42 ( ! [X0 : $int] : ($less(5,X0) | $less(X0,3)) ) | ~spl12_28),
% 184.43/41.42 inference(avatar_component_clause,[],[f1468])).
% 184.43/41.42 tff(f1480,plain,(
% 184.43/41.42 ( ! [X0 : $int,X1 : general] : (~p__less_equal__(X1,f__integer__(X0)) | $less(3,X0) | p__less_equal__(X1,sK3)) ) | ~spl12_11),
% 184.43/41.42 inference(resolution,[],[f1361,f58])).
% 184.43/41.42 tff(f1509,plain,(
% 184.43/41.42 ( ! [X0 : general] : (p__less_equal__(sK3,X0) | ~p__less_equal__(sK1,X0) | sK1 = X0) ) | (~spl12_2 | ~spl12_13)),
% 184.43/41.42 inference(resolution,[],[f1400,f135])).
% 184.43/41.42 tff(f1527,plain,(
% 184.43/41.42 ( ! [X0 : $int] : ($less(3,X0) | p__less_equal__(f__integer__(X0),sK1)) ) | (~spl12_2 | ~spl12_11 | ~spl12_13)),
% 184.43/41.42 inference(resolution,[],[f1403,f1361])).
% 184.43/41.42 tff(f1693,definition,(
% 184.43/41.42 spl12_31 <=> ! [X0 : $int] : $less(X0,5)),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_31])],[avatar_definition])).
% 184.43/41.42 tff(f1694,plain,(
% 184.43/41.42 ( ! [X0 : $int] : ($less(X0,5)) ) | ~spl12_31),
% 184.43/41.42 inference(avatar_component_clause,[],[f1693])).
% 184.43/41.42 tff(f1909,definition,(
% 184.43/41.42 spl12_44 <=> ! [X0 : $int] : (p__less_equal__(f__integer__(X0),sK1) | $less(3,X0))),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_44])],[avatar_definition])).
% 184.43/41.42 tff(f1910,plain,(
% 184.43/41.42 ( ! [X0 : $int] : (p__less_equal__(f__integer__(X0),sK1) | $less(3,X0)) ) | ~spl12_44),
% 184.43/41.42 inference(avatar_component_clause,[],[f1909])).
% 184.43/41.42 tff(f1986,plain,(
% 184.43/41.42 ( ! [X0 : $int,X1 : general] : (p__less__(X1,f__integer__(X0)) | $less(3,X0) | p__less_equal__(X1,sK3)) ) | ~spl12_11),
% 184.43/41.42 inference(resolution,[],[f1480,f188])).
% 184.43/41.42 tff(f2049,definition,(
% 184.43/41.42 spl12_58 <=> p__less__(sK1,sK8)),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_58])],[avatar_definition])).
% 184.43/41.42 tff(f2051,plain,(
% 184.43/41.42 p__less__(sK1,sK8) | ~spl12_58),
% 184.43/41.42 inference(avatar_component_clause,[],[f2049])).
% 184.43/41.42 tff(f2052,plain,(
% 184.43/41.42 spl12_58 | spl12_17 | ~spl12_10 | ~spl12_12),
% 184.43/41.42 inference(avatar_split_clause,[],[f589,f272,f262,f411,f2049])).
% 184.43/41.42 tff(f2059,plain,(
% 184.43/41.42 p__greater__(sK1,sK1) | (~spl12_10 | ~spl12_12 | ~spl12_17)),
% 184.43/41.42 inference(superposition,[],[f324,f413])).
% 184.43/41.42 tff(f2069,plain,(
% 184.43/41.42 $false | (~spl12_10 | ~spl12_12 | ~spl12_17)),
% 184.43/41.42 inference(forward_subsumption_resolution,[],[f2059,f185])).
% 184.43/41.42 tff(f2070,plain,(
% 184.43/41.42 ~spl12_10 | ~spl12_12 | ~spl12_17),
% 184.43/41.42 inference(avatar_contradiction_clause,[],[f2069])).
% 184.43/41.42 tff(f2174,plain,(
% 184.43/41.42 ( ! [X0 : $int] : (~p__less_equal__(f__integer__($sum(1,X0)),f__integer__(X0))) )),
% 184.43/41.42 inference(resolution,[],[f483,f67])).
% 184.43/41.42 tff(f2227,plain,(
% 184.43/41.42 ( ! [X0 : $int] : (~p__less_equal__(f__integer__(1),f__integer__(X0)) | $less(0,X0)) )),
% 184.43/41.42 inference(resolution,[],[f510,f67])).
% 184.43/41.42 tff(f2837,plain,(
% 184.43/41.42 ( ! [X0 : symbol,X1 : general] : (p__less__(X1,f__symbolic__(X0)) | p__less_equal__(X1,c__supremum__)) )),
% 184.43/41.42 inference(resolution,[],[f548,f202])).
% 184.43/41.42 tff(f2865,plain,(
% 184.43/41.42 ( ! [X0 : $int,X1 : general] : (p__less__(f__integer__($sum(X0,1)),X1) | p__less__(X1,sK7) | $less(X0,5)) ) | ~spl12_7),
% 184.43/41.42 inference(resolution,[],[f548,f623])).
% 184.43/41.42 tff(f2867,plain,(
% 184.43/41.42 ( ! [X0 : general] : (p__less__(sK1,X0) | p__less__(X0,sK8)) ) | spl12_18),
% 184.43/41.42 inference(resolution,[],[f548,f417])).
% 184.43/41.42 tff(f3080,definition,(
% 184.43/41.42 spl12_68 <=> c__infimum__ = sK3),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_68])],[avatar_definition])).
% 184.43/41.42 tff(f3081,plain,(
% 184.43/41.42 c__infimum__ != sK3 | spl12_68),
% 184.43/41.42 inference(avatar_component_clause,[],[f3080])).
% 184.43/41.42 tff(f3082,plain,(
% 184.43/41.42 c__infimum__ = sK3 | ~spl12_68),
% 184.43/41.42 inference(avatar_component_clause,[],[f3080])).
% 184.43/41.42 tff(f3578,plain,(
% 184.43/41.42 ~p__less__(sK3,sK3) | (~spl12_11 | ~spl12_68)),
% 184.43/41.42 inference(superposition,[],[f1365,f3082])).
% 184.43/41.42 tff(f3582,plain,(
% 184.43/41.42 $false | (~spl12_11 | ~spl12_68)),
% 184.43/41.42 inference(forward_subsumption_resolution,[],[f3578,f191])).
% 184.43/41.42 tff(f3583,plain,(
% 184.43/41.42 ~spl12_11 | ~spl12_68),
% 184.43/41.42 inference(avatar_contradiction_clause,[],[f3582])).
% 184.43/41.42 tff(f5681,plain,(
% 184.43/41.42 ( ! [X0 : $int,X1 : $int] : ($less(1,X1) | $less(X0,2) | $less(X1,X0) | 2 = X0) )),
% 184.43/41.42 inference(resolution,[],[f1038,f791])).
% 184.43/41.42 tff(f23572,definition,(
% 184.43/41.42 spl12_81 <=> p__less_equal__(sK1,sK4)),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_81])],[avatar_definition])).
% 184.43/41.42 tff(f23573,plain,(
% 184.43/41.42 p__less_equal__(sK1,sK4) | ~spl12_81),
% 184.43/41.42 inference(avatar_component_clause,[],[f23572])).
% 184.43/41.42 tff(f23574,plain,(
% 184.43/41.42 ~p__less_equal__(sK1,sK4) | spl12_81),
% 184.43/41.42 inference(avatar_component_clause,[],[f23572])).
% 184.43/41.42 tff(f23576,definition,(
% 184.43/41.42 spl12_82 <=> sK4 = sK1),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_82])],[avatar_definition])).
% 184.43/41.42 tff(f23578,plain,(
% 184.43/41.42 sK4 = sK1 | ~spl12_82),
% 184.43/41.42 inference(avatar_component_clause,[],[f23576])).
% 184.43/41.42 tff(f23593,definition,(
% 184.43/41.42 spl12_84 <=> p__less_equal__(sK4,sK1)),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_84])],[avatar_definition])).
% 184.43/41.42 tff(f23594,plain,(
% 184.43/41.42 ~p__less_equal__(sK4,sK1) | spl12_84),
% 184.43/41.42 inference(avatar_component_clause,[],[f23593])).
% 184.43/41.42 tff(f33024,plain,(
% 184.43/41.42 sK4 = sK1 | p__less__(sK4,sK1) | ~spl12_81),
% 184.43/41.42 inference(resolution,[],[f23573,f391])).
% 184.43/41.42 tff(f33031,definition,(
% 184.43/41.42 spl12_86 <=> p__less__(sK4,sK1)),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_86])],[avatar_definition])).
% 184.43/41.42 tff(f33033,plain,(
% 184.43/41.42 p__less__(sK4,sK1) | ~spl12_86),
% 184.43/41.42 inference(avatar_component_clause,[],[f33031])).
% 184.43/41.42 tff(f33034,plain,(
% 184.43/41.42 spl12_86 | spl12_82 | ~spl12_81),
% 184.43/41.42 inference(avatar_split_clause,[],[f33024,f23572,f23576,f33031])).
% 184.43/41.42 tff(f36074,plain,(
% 184.43/41.42 ~p__less__(sK1,sK1) | (~spl12_6 | spl12_14 | ~spl12_82)),
% 184.43/41.42 inference(superposition,[],[f1329,f23578])).
% 184.43/41.42 tff(f36122,plain,(
% 184.43/41.42 $false | (~spl12_6 | spl12_14 | ~spl12_82)),
% 184.43/41.42 inference(forward_subsumption_resolution,[],[f36074,f191])).
% 184.43/41.42 tff(f36123,plain,(
% 184.43/41.42 ~spl12_6 | spl12_14 | ~spl12_82),
% 184.43/41.42 inference(avatar_contradiction_clause,[],[f36122])).
% 184.43/41.42 tff(f36131,plain,(
% 184.43/41.42 ( ! [X0 : general] : (p__less__(sK4,X0) | p__less__(X0,sK1)) ) | spl12_84),
% 184.43/41.42 inference(resolution,[],[f23594,f548])).
% 184.43/41.42 tff(f48273,plain,(
% 184.43/41.42 ( ! [X0 : general] : (~p__less__(sK7,X0) | c__infimum__ = X0 | f__integer__(sK11(X0)) = X0 | c__supremum__ = X0) ) | ~spl12_7),
% 184.43/41.42 inference(superposition,[],[f329,f1101])).
% 184.43/41.42 tff(f48274,plain,(
% 184.43/41.42 ( ! [X0 : general] : (~p__less__(sK4,X0) | c__infimum__ = X0 | c__supremum__ = X0 | f__integer__(sK11(X0)) = X0) ) | ~spl12_3),
% 184.43/41.42 inference(superposition,[],[f1336,f1101])).
% 184.43/41.42 tff(f67643,plain,(
% 184.43/41.42 spl12_44 | ~spl12_2 | ~spl12_11 | ~spl12_13),
% 184.43/41.42 inference(avatar_split_clause,[],[f1527,f277,f267,f223,f1909])).
% 184.43/41.42 tff(f67672,plain,(
% 184.43/41.42 p__less_equal__(sK3,sK1) | $less(3,3) | (~spl12_11 | ~spl12_44)),
% 184.43/41.42 inference(superposition,[],[f1910,f269])).
% 184.43/41.42 tff(f67993,plain,(
% 184.43/41.42 sK3 = sK1 | ~p__less_equal__(sK1,sK3) | p__less_equal__(sK3,sK1) | (~spl12_2 | ~spl12_13)),
% 184.43/41.42 inference(resolution,[],[f1509,f1403])).
% 184.43/41.42 tff(f69334,plain,(
% 184.43/41.42 ( ! [X0 : $int] : (p__less_equal__(c__infimum__,sK3) | $less(3,X0)) ) | ~spl12_11),
% 184.43/41.42 inference(resolution,[],[f1986,f209])).
% 184.43/41.42 tff(f69340,definition,(
% 184.43/41.42 spl12_113 <=> p__less_equal__(c__infimum__,sK3)),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_113])],[avatar_definition])).
% 184.43/41.42 tff(f69342,plain,(
% 184.43/41.42 p__less_equal__(c__infimum__,sK3) | ~spl12_113),
% 184.43/41.42 inference(avatar_component_clause,[],[f69340])).
% 184.43/41.42 tff(f69344,definition,(
% 184.43/41.42 spl12_114 <=> ! [X0 : $int] : $less(3,X0)),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_114])],[avatar_definition])).
% 184.43/41.42 tff(f69345,plain,(
% 184.43/41.42 ( ! [X0 : $int] : ($less(3,X0)) ) | ~spl12_114),
% 184.43/41.42 inference(avatar_component_clause,[],[f69344])).
% 184.43/41.42 tff(f69393,plain,(
% 184.43/41.42 $false | ~spl12_114),
% 184.43/41.42 inference(resolution,[],[f69345,f26])).
% 184.43/41.42 tff(f69406,plain,(
% 184.43/41.42 ~spl12_114),
% 184.43/41.42 inference(avatar_contradiction_clause,[],[f69393])).
% 184.43/41.42 tff(f69416,plain,(
% 184.43/41.42 ~p__less_equal__(sK3,c__infimum__) | c__infimum__ = sK3 | ~spl12_113),
% 184.43/41.42 inference(resolution,[],[f69342,f135])).
% 184.43/41.42 tff(f69421,plain,(
% 184.43/41.42 ~p__less_equal__(sK3,c__infimum__) | (spl12_68 | ~spl12_113)),
% 184.43/41.42 inference(forward_subsumption_resolution,[],[f69416,f3081])).
% 184.43/41.42 tff(f69434,definition,(
% 184.43/41.42 spl12_116 <=> c__infimum__ = sK1),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_116])],[avatar_definition])).
% 184.43/41.42 tff(f69435,plain,(
% 184.43/41.42 c__infimum__ != sK1 | spl12_116),
% 184.43/41.42 inference(avatar_component_clause,[],[f69434])).
% 184.43/41.42 tff(f69436,plain,(
% 184.43/41.42 c__infimum__ = sK1 | ~spl12_116),
% 184.43/41.42 inference(avatar_component_clause,[],[f69434])).
% 184.43/41.42 tff(f72069,plain,(
% 184.43/41.42 $false | ~spl12_31),
% 184.43/41.42 inference(resolution,[],[f1694,f26])).
% 184.43/41.42 tff(f72083,plain,(
% 184.43/41.42 ~spl12_31),
% 184.43/41.42 inference(avatar_contradiction_clause,[],[f72069])).
% 184.43/41.42 tff(f73358,plain,(
% 184.43/41.42 $less(5,3) | ~spl12_28),
% 184.43/41.42 inference(resolution,[],[f1469,f26])).
% 184.43/41.42 tff(f73378,plain,(
% 184.43/41.42 $false | ~spl12_28),
% 184.43/41.42 inference(evaluation,[],[f73358])).
% 184.43/41.42 tff(f73379,plain,(
% 184.43/41.42 ~spl12_28),
% 184.43/41.42 inference(avatar_contradiction_clause,[],[f73378])).
% 184.43/41.42 tff(f73875,definition,(
% 184.43/41.42 spl12_229 <=> c__supremum__ = sK8),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_229])],[avatar_definition])).
% 184.43/41.42 tff(f73877,plain,(
% 184.43/41.42 c__supremum__ = sK8 | ~spl12_229),
% 184.43/41.42 inference(avatar_component_clause,[],[f73875])).
% 184.43/41.42 tff(f74828,definition,(
% 184.43/41.42 spl12_263 <=> c__supremum__ = sK1),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_263])],[avatar_definition])).
% 184.43/41.42 tff(f74830,plain,(
% 184.43/41.42 c__supremum__ = sK1 | ~spl12_263),
% 184.43/41.42 inference(avatar_component_clause,[],[f74828])).
% 184.43/41.42 tff(f75344,plain,(
% 184.43/41.42 ( ! [X0 : symbol] : (~p__less__(f__symbolic__(X0),sK1)) ) | ~spl12_263),
% 184.43/41.42 inference(superposition,[],[f202,f74830])).
% 184.43/41.42 tff(f75771,plain,(
% 184.43/41.42 ( ! [X0 : symbol] : (p__less__(sK4,f__symbolic__(X0))) ) | (spl12_84 | ~spl12_263)),
% 184.43/41.42 inference(resolution,[],[f75344,f36131])).
% 184.43/41.42 tff(f75779,plain,(
% 184.43/41.42 $false | (~spl12_3 | spl12_84 | ~spl12_263)),
% 184.43/41.42 inference(forward_subsumption_resolution,[],[f75771,f1336])).
% 184.43/41.42 tff(f75780,plain,(
% 184.43/41.42 ~spl12_3 | spl12_84 | ~spl12_263),
% 184.43/41.42 inference(avatar_contradiction_clause,[],[f75779])).
% 184.43/41.42 tff(f77957,plain,(
% 184.43/41.42 p__less__(sK1,sK4) | spl12_81),
% 184.43/41.42 inference(resolution,[],[f23574,f188])).
% 184.43/41.42 tff(f77962,plain,(
% 184.43/41.42 $false | (~spl12_6 | spl12_14 | spl12_81)),
% 184.43/41.42 inference(forward_subsumption_resolution,[],[f77957,f1329])).
% 184.43/41.42 tff(f77963,plain,(
% 184.43/41.42 ~spl12_6 | spl12_14 | spl12_81),
% 184.43/41.42 inference(avatar_contradiction_clause,[],[f77962])).
% 184.43/41.42 tff(f78099,plain,(
% 184.43/41.42 c__infimum__ = sK1 | f__integer__(sK11(sK1)) = sK1 | c__supremum__ = sK1 | (~spl12_3 | ~spl12_86)),
% 184.43/41.42 inference(resolution,[],[f48274,f33033])).
% 184.43/41.42 tff(f78173,definition,(
% 184.43/41.42 spl12_350 <=> f__integer__(sK11(sK1)) = sK1),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_350])],[avatar_definition])).
% 184.43/41.42 tff(f78175,plain,(
% 184.43/41.42 f__integer__(sK11(sK1)) = sK1 | ~spl12_350),
% 184.43/41.42 inference(avatar_component_clause,[],[f78173])).
% 184.43/41.42 tff(f82109,definition,(
% 184.43/41.42 spl12_436 <=> f__integer__(1) = sK1),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_436])],[avatar_definition])).
% 184.43/41.42 tff(f82111,plain,(
% 184.43/41.42 f__integer__(1) = sK1 | ~spl12_436),
% 184.43/41.42 inference(avatar_component_clause,[],[f82109])).
% 184.43/41.42 tff(f88134,plain,(
% 184.43/41.42 p__less_equal__(sK7,c__supremum__) | ~spl12_7),
% 184.43/41.42 inference(resolution,[],[f2837,f329])).
% 184.43/41.42 tff(f88271,definition,(
% 184.43/41.42 spl12_512 <=> p__less_equal__(sK8,sK1)),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_512])],[avatar_definition])).
% 184.43/41.42 tff(f88272,plain,(
% 184.43/41.42 p__less_equal__(sK8,sK1) | ~spl12_512),
% 184.43/41.42 inference(avatar_component_clause,[],[f88271])).
% 184.43/41.42 tff(f88273,plain,(
% 184.43/41.42 ~p__less_equal__(sK8,sK1) | spl12_512),
% 184.43/41.42 inference(avatar_component_clause,[],[f88271])).
% 184.43/41.42 tff(f88304,plain,(
% 184.43/41.42 p__less_equal__(sK1,sK8) | spl12_512),
% 184.43/41.42 inference(resolution,[],[f88273,f57])).
% 184.43/41.42 tff(f88438,plain,(
% 184.43/41.42 spl12_18 | spl12_512),
% 184.43/41.42 inference(avatar_split_clause,[],[f88304,f88271,f415])).
% 184.43/41.42 tff(f95640,definition,(
% 184.43/41.42 spl12_644 <=> $less(sK11(sK8),3)),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_644])],[avatar_definition])).
% 184.43/41.42 tff(f95641,plain,(
% 184.43/41.42 ~$less(sK11(sK8),3) | spl12_644),
% 184.43/41.42 inference(avatar_component_clause,[],[f95640])).
% 184.43/41.42 tff(f95642,plain,(
% 184.43/41.42 $less(sK11(sK8),3) | ~spl12_644),
% 184.43/41.42 inference(avatar_component_clause,[],[f95640])).
% 184.43/41.42 tff(f95851,definition,(
% 184.43/41.42 spl12_691 <=> p__less_equal__(f__integer__(1),sK8)),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_691])],[avatar_definition])).
% 184.43/41.42 tff(f95852,plain,(
% 184.43/41.42 p__less_equal__(f__integer__(1),sK8) | ~spl12_691),
% 184.43/41.42 inference(avatar_component_clause,[],[f95851])).
% 184.43/41.42 tff(f95853,plain,(
% 184.43/41.42 ~p__less_equal__(f__integer__(1),sK8) | spl12_691),
% 184.43/41.42 inference(avatar_component_clause,[],[f95851])).
% 184.43/41.42 tff(f96129,definition,(
% 184.43/41.42 spl12_745 <=> f__integer__(sK11(sK8)) = sK8),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_745])],[avatar_definition])).
% 184.43/41.42 tff(f96131,plain,(
% 184.43/41.42 f__integer__(sK11(sK8)) = sK8 | ~spl12_745),
% 184.43/41.42 inference(avatar_component_clause,[],[f96129])).
% 184.43/41.42 tff(f97263,plain,(
% 184.43/41.42 $less(sK11(sK1),5) | p__less_equal__(sK7,sK1) | (~spl12_7 | ~spl12_350)),
% 184.43/41.42 inference(superposition,[],[f349,f78175])).
% 184.43/41.42 tff(f97298,plain,(
% 184.43/41.42 $less(sK11(sK1),5) | p__greater_equal__(sK1,sK4) | (~spl12_3 | ~spl12_350)),
% 184.43/41.42 inference(superposition,[],[f1338,f78175])).
% 184.43/41.42 tff(f97308,plain,(
% 184.43/41.42 p__greater_equal__(sK3,sK1) | $less(3,sK11(sK1)) | (~spl12_11 | ~spl12_350)),
% 184.43/41.42 inference(superposition,[],[f1367,f78175])).
% 184.43/41.42 tff(f97311,plain,(
% 184.43/41.42 ~p__less_equal__(sK3,sK1) | $less(3,sK11(sK1)) | sK3 = sK1 | (~spl12_11 | ~spl12_350)),
% 184.43/41.42 inference(superposition,[],[f1377,f78175])).
% 184.43/41.42 tff(f97411,plain,(
% 184.43/41.42 ~p__less_equal__(f__integer__(1),sK1) | $less(0,sK11(sK1)) | ~spl12_350),
% 184.43/41.42 inference(superposition,[],[f2227,f78175])).
% 184.43/41.42 tff(f97503,definition,(
% 184.43/41.42 spl12_769 <=> p__greater_equal__(sK1,sK4)),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_769])],[avatar_definition])).
% 184.43/41.42 tff(f97504,plain,(
% 184.43/41.42 ~p__greater_equal__(sK1,sK4) | spl12_769),
% 184.43/41.42 inference(avatar_component_clause,[],[f97503])).
% 184.43/41.42 tff(f97505,plain,(
% 184.43/41.42 p__greater_equal__(sK1,sK4) | ~spl12_769),
% 184.43/41.42 inference(avatar_component_clause,[],[f97503])).
% 184.43/41.42 tff(f97512,definition,(
% 184.43/41.42 spl12_771 <=> $less(sK11(sK1),5)),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_771])],[avatar_definition])).
% 184.43/41.42 tff(f97514,plain,(
% 184.43/41.42 $less(sK11(sK1),5) | ~spl12_771),
% 184.43/41.42 inference(avatar_component_clause,[],[f97512])).
% 184.43/41.42 tff(f97562,definition,(
% 184.43/41.42 spl12_782 <=> $less(3,sK11(sK1))),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_782])],[avatar_definition])).
% 184.43/41.42 tff(f97564,plain,(
% 184.43/41.42 $less(3,sK11(sK1)) | ~spl12_782),
% 184.43/41.42 inference(avatar_component_clause,[],[f97562])).
% 184.43/41.42 tff(f97597,definition,(
% 184.43/41.42 spl12_788 <=> 3 = sK11(sK1)),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_788])],[avatar_definition])).
% 184.43/41.42 tff(f97599,plain,(
% 184.43/41.42 3 = sK11(sK1) | ~spl12_788),
% 184.43/41.42 inference(avatar_component_clause,[],[f97597])).
% 184.43/41.42 tff(f97677,definition,(
% 184.43/41.42 spl12_804 <=> p__greater_equal__(sK3,sK1)),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_804])],[avatar_definition])).
% 184.43/41.42 tff(f97679,plain,(
% 184.43/41.42 p__greater_equal__(sK3,sK1) | ~spl12_804),
% 184.43/41.42 inference(avatar_component_clause,[],[f97677])).
% 184.43/41.42 tff(f98053,plain,(
% 184.43/41.42 ~p__less_equal__(sK3,sK1) | (spl12_68 | ~spl12_113 | ~spl12_116)),
% 184.43/41.42 inference(superposition,[],[f69421,f69436])).
% 184.43/41.42 tff(f98079,plain,(
% 184.43/41.42 $false | (~spl12_2 | ~spl12_13 | spl12_68 | ~spl12_113 | ~spl12_116)),
% 184.43/41.42 inference(forward_subsumption_resolution,[],[f98053,f1358])).
% 184.43/41.42 tff(f98080,plain,(
% 184.43/41.42 ~spl12_2 | ~spl12_13 | spl12_68 | ~spl12_113 | ~spl12_116),
% 184.43/41.42 inference(avatar_contradiction_clause,[],[f98079])).
% 184.43/41.42 tff(f98110,definition,(
% 184.43/41.42 spl12_831 <=> $less(sK11(sK1),3)),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_831])],[avatar_definition])).
% 184.43/41.42 tff(f98111,plain,(
% 184.43/41.42 ~$less(sK11(sK1),3) | spl12_831),
% 184.43/41.42 inference(avatar_component_clause,[],[f98110])).
% 184.43/41.42 tff(f98112,plain,(
% 184.43/41.42 $less(sK11(sK1),3) | ~spl12_831),
% 184.43/41.42 inference(avatar_component_clause,[],[f98110])).
% 184.43/41.42 tff(f98174,plain,(
% 184.43/41.42 $less(3,sK11(sK1)) | sK3 = sK1 | (~spl12_2 | ~spl12_11 | ~spl12_13 | ~spl12_350)),
% 184.43/41.42 inference(forward_subsumption_resolution,[],[f97311,f1358])).
% 184.43/41.42 tff(f98209,plain,(
% 184.43/41.42 sK3 = sK1 | ~p__less_equal__(sK1,sK3) | (~spl12_2 | ~spl12_13)),
% 184.43/41.42 inference(forward_subsumption_resolution,[],[f67993,f135])).
% 184.43/41.42 tff(f98291,plain,(
% 184.43/41.42 spl12_25 | spl12_782 | ~spl12_2 | ~spl12_11 | ~spl12_13 | ~spl12_350),
% 184.43/41.42 inference(avatar_split_clause,[],[f98174,f78173,f277,f267,f223,f97562,f1406])).
% 184.43/41.42 tff(f98297,plain,(
% 184.43/41.42 spl12_25 | ~spl12_26 | ~spl12_2 | ~spl12_13),
% 184.43/41.42 inference(avatar_split_clause,[],[f98209,f277,f223,f1410,f1406])).
% 184.43/41.42 tff(f98337,plain,(
% 184.43/41.42 p__greater__(sK2,sK1) | (~spl12_2 | ~spl12_25)),
% 184.43/41.42 inference(superposition,[],[f225,f1408])).
% 184.43/41.42 tff(f98506,plain,(
% 184.43/41.42 p__greater__(sK1,sK1) | (~spl12_2 | ~spl12_13 | ~spl12_25)),
% 184.43/41.42 inference(forward_demodulation,[],[f98337,f279])).
% 184.43/41.42 tff(f98521,plain,(
% 184.43/41.42 $false | (~spl12_2 | ~spl12_13 | ~spl12_25)),
% 184.43/41.42 inference(forward_subsumption_resolution,[],[f98506,f185])).
% 184.43/41.42 tff(f98522,plain,(
% 184.43/41.42 ~spl12_2 | ~spl12_13 | ~spl12_25),
% 184.43/41.42 inference(avatar_contradiction_clause,[],[f98521])).
% 184.43/41.42 tff(f102849,plain,(
% 184.43/41.42 ~$less(sK11(sK1),$sum(3,1)) | ~spl12_782),
% 184.43/41.42 inference(resolution,[],[f97564,f32])).
% 184.43/41.42 tff(f102854,plain,(
% 184.43/41.42 ~$less(sK11(sK1),4) | ~spl12_782),
% 184.43/41.42 inference(evaluation,[],[f102849])).
% 184.43/41.42 tff(f103109,plain,(
% 184.43/41.42 3 = sK11(sK1) | $less(3,sK11(sK1)) | spl12_831),
% 184.43/41.42 inference(resolution,[],[f98111,f28])).
% 184.43/41.42 tff(f103245,plain,(
% 184.43/41.42 $less(4,sK11(sK1)) | 4 = sK11(sK1) | ~spl12_782),
% 184.43/41.42 inference(resolution,[],[f102854,f28])).
% 184.43/41.42 tff(f103265,definition,(
% 184.43/41.42 spl12_852 <=> 4 = sK11(sK1)),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_852])],[avatar_definition])).
% 184.43/41.42 tff(f103266,plain,(
% 184.43/41.42 4 != sK11(sK1) | spl12_852),
% 184.43/41.42 inference(avatar_component_clause,[],[f103265])).
% 184.43/41.42 tff(f103267,plain,(
% 184.43/41.42 4 = sK11(sK1) | ~spl12_852),
% 184.43/41.42 inference(avatar_component_clause,[],[f103265])).
% 184.43/41.42 tff(f103274,definition,(
% 184.43/41.42 spl12_854 <=> $less(4,sK11(sK1))),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_854])],[avatar_definition])).
% 184.43/41.42 tff(f103276,plain,(
% 184.43/41.42 $less(4,sK11(sK1)) | ~spl12_854),
% 184.43/41.42 inference(avatar_component_clause,[],[f103274])).
% 184.43/41.42 tff(f103601,definition,(
% 184.43/41.42 spl12_861 <=> sK11(sK1) = 1),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_861])],[avatar_definition])).
% 184.43/41.42 tff(f103602,plain,(
% 184.43/41.42 sK11(sK1) != 1 | spl12_861),
% 184.43/41.42 inference(avatar_component_clause,[],[f103601])).
% 184.43/41.42 tff(f103603,plain,(
% 184.43/41.42 sK11(sK1) = 1 | ~spl12_861),
% 184.43/41.42 inference(avatar_component_clause,[],[f103601])).
% 184.43/41.42 tff(f103609,definition,(
% 184.43/41.42 spl12_863 <=> $less(1,sK11(sK1))),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_863])],[avatar_definition])).
% 184.43/41.42 tff(f103611,plain,(
% 184.43/41.42 $less(1,sK11(sK1)) | ~spl12_863),
% 184.43/41.42 inference(avatar_component_clause,[],[f103609])).
% 184.43/41.42 tff(f107957,plain,(
% 184.43/41.42 ~$less(sK11(sK1),$sum(4,1)) | ~spl12_854),
% 184.43/41.42 inference(resolution,[],[f103276,f32])).
% 184.43/41.42 tff(f107964,plain,(
% 184.43/41.42 ~$less(sK11(sK1),5) | ~spl12_854),
% 184.43/41.42 inference(evaluation,[],[f107957])).
% 184.43/41.42 tff(f107966,plain,(
% 184.43/41.42 $false | (~spl12_771 | ~spl12_854)),
% 184.43/41.42 inference(forward_subsumption_resolution,[],[f107964,f97514])).
% 184.43/41.42 tff(f107967,plain,(
% 184.43/41.42 ~spl12_771 | ~spl12_854),
% 184.43/41.42 inference(avatar_contradiction_clause,[],[f107966])).
% 184.43/41.42 tff(f108974,plain,(
% 184.43/41.42 ~p__less_equal__(f__integer__(3),f__integer__(sK11(sK8))) | ~spl12_644),
% 184.43/41.42 inference(resolution,[],[f95642,f67])).
% 184.43/41.42 tff(f110262,definition,(
% 184.43/41.42 spl12_879 <=> p__less_equal__(sK8,f__integer__(1))),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_879])],[avatar_definition])).
% 184.43/41.42 tff(f112979,definition,(
% 184.43/41.42 spl12_885 <=> $less(1,sK11(sK8))),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_885])],[avatar_definition])).
% 184.43/41.42 tff(f112981,plain,(
% 184.43/41.42 $less(1,sK11(sK8)) | ~spl12_885),
% 184.43/41.42 inference(avatar_component_clause,[],[f112979])).
% 184.43/41.42 tff(f114456,plain,(
% 184.43/41.42 p__less_equal__(sK8,f__integer__(1)) | spl12_691),
% 184.43/41.42 inference(resolution,[],[f95853,f57])).
% 184.43/41.42 tff(f114491,plain,(
% 184.43/41.42 spl12_879 | spl12_691),
% 184.43/41.42 inference(avatar_split_clause,[],[f114456,f95851,f110262])).
% 184.43/41.42 tff(f115613,plain,(
% 184.43/41.42 ~p__less_equal__(f__integer__(sK11(sK8)),f__integer__(1)) | ~spl12_885),
% 184.43/41.42 inference(resolution,[],[f112981,f67])).
% 184.43/41.42 tff(f115621,plain,(
% 184.43/41.42 ~p__less_equal__(sK8,f__integer__(1)) | (~spl12_745 | ~spl12_885)),
% 184.43/41.42 inference(forward_demodulation,[],[f115613,f96131])).
% 184.43/41.42 tff(f116197,plain,(
% 184.43/41.42 f__integer__(4) = sK1 | (~spl12_350 | ~spl12_852)),
% 184.43/41.42 inference(forward_demodulation,[],[f78175,f103267])).
% 184.43/41.42 tff(f116200,plain,(
% 184.43/41.42 ~hp(sK1) | (~spl12_350 | ~spl12_852)),
% 184.43/41.42 inference(superposition,[],[f196,f116197])).
% 184.43/41.42 tff(f116570,plain,(
% 184.43/41.42 $false | (~spl12_5 | ~spl12_350 | ~spl12_852)),
% 184.43/41.42 inference(forward_subsumption_resolution,[],[f116200,f239])).
% 184.43/41.42 tff(f116571,plain,(
% 184.43/41.42 ~spl12_5 | ~spl12_350 | ~spl12_852),
% 184.43/41.42 inference(avatar_contradiction_clause,[],[f116570])).
% 184.43/41.42 tff(f117018,plain,(
% 184.43/41.42 ~p__less__(c__infimum__,sK8) | ~spl12_8),
% 184.43/41.42 inference(superposition,[],[f209,f254])).
% 184.43/41.42 tff(f117296,plain,(
% 184.43/41.42 p__less_equal__(f__integer__(1),sK1) | (~spl12_10 | ~spl12_12 | ~spl12_691)),
% 184.43/41.42 inference(resolution,[],[f388,f95852])).
% 184.43/41.42 tff(f118216,plain,(
% 184.43/41.42 ~p__less__(sK1,sK8) | (~spl12_8 | ~spl12_116)),
% 184.43/41.42 inference(forward_demodulation,[],[f117018,f69436])).
% 184.43/41.42 tff(f118242,plain,(
% 184.43/41.42 $false | (~spl12_8 | ~spl12_58 | ~spl12_116)),
% 184.43/41.42 inference(forward_subsumption_resolution,[],[f118216,f2051])).
% 184.43/41.42 tff(f118243,plain,(
% 184.43/41.42 ~spl12_8 | ~spl12_58 | ~spl12_116),
% 184.43/41.42 inference(avatar_contradiction_clause,[],[f118242])).
% 184.43/41.42 tff(f118596,plain,(
% 184.43/41.42 p__less_equal__(sK3,sK1) | (~spl12_11 | ~spl12_44)),
% 184.43/41.42 inference(evaluation,[],[f67672])).
% 184.43/41.42 tff(f118776,definition,(
% 184.43/41.42 spl12_952 <=> p__less_equal__(sK3,sK1)),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_952])],[avatar_definition])).
% 184.43/41.42 tff(f118850,definition,(
% 184.43/41.42 spl12_959 <=> $less(0,sK11(sK1))),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_959])],[avatar_definition])).
% 184.43/41.42 tff(f118852,plain,(
% 184.43/41.42 $less(0,sK11(sK1)) | ~spl12_959),
% 184.43/41.42 inference(avatar_component_clause,[],[f118850])).
% 184.43/41.42 tff(f119391,plain,(
% 184.43/41.42 spl12_804 | spl12_782 | ~spl12_11 | ~spl12_350),
% 184.43/41.42 inference(avatar_split_clause,[],[f97308,f78173,f267,f97562,f97677])).
% 184.43/41.42 tff(f119862,plain,(
% 184.43/41.42 spl12_952 | ~spl12_11 | ~spl12_44),
% 184.43/41.42 inference(avatar_split_clause,[],[f118596,f1909,f267,f118776])).
% 184.43/41.42 tff(f119936,plain,(
% 184.43/41.42 spl12_25 | ~spl12_952 | spl12_782 | ~spl12_11 | ~spl12_350),
% 184.43/41.42 inference(avatar_split_clause,[],[f97311,f78173,f267,f97562,f118776,f1406])).
% 184.43/41.42 tff(f119973,plain,(
% 184.43/41.42 spl12_113 | spl12_114 | ~spl12_11),
% 184.43/41.42 inference(avatar_split_clause,[],[f69334,f267,f69344,f69340])).
% 184.43/41.42 tff(f120024,definition,(
% 184.43/41.42 spl12_1023 <=> p__less_equal__(f__integer__(1),sK1)),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_1023])],[avatar_definition])).
% 184.43/41.42 tff(f120700,plain,(
% 184.43/41.42 ( ! [X0 : general] : (~p__less__(sK8,X0) | c__supremum__ = X0 | c__infimum__ = X0 | f__integer__(sK11(X0)) = X0) ) | ~spl12_8),
% 184.43/41.42 inference(superposition,[],[f330,f1101])).
% 184.43/41.42 tff(f120823,plain,(
% 184.43/41.42 ~p__less_equal__(f__integer__(3),sK8) | (~spl12_644 | ~spl12_745)),
% 184.43/41.42 inference(forward_demodulation,[],[f108974,f96131])).
% 184.43/41.42 tff(f120898,plain,(
% 184.43/41.42 ~p__less_equal__(sK8,sK8) | (~spl12_8 | ~spl12_644 | ~spl12_745)),
% 184.43/41.42 inference(forward_demodulation,[],[f120823,f254])).
% 184.43/41.42 tff(f120920,plain,(
% 184.43/41.42 $false | (~spl12_8 | ~spl12_644 | ~spl12_745)),
% 184.43/41.42 inference(forward_subsumption_resolution,[],[f120898,f332])).
% 184.43/41.42 tff(f120921,plain,(
% 184.43/41.42 ~spl12_8 | ~spl12_644 | ~spl12_745),
% 184.43/41.42 inference(avatar_contradiction_clause,[],[f120920])).
% 184.43/41.42 tff(f121007,plain,(
% 184.43/41.42 ( ! [X0 : $int] : (p__less_equal__(f__integer__(X0),sK8) | $less(3,$sum(X0,1))) ) | ~spl12_8),
% 184.43/41.42 inference(resolution,[],[f570,f481])).
% 184.43/41.42 tff(f121269,plain,(
% 184.43/41.42 ~p__less_equal__(sK7,sK8) | 3 = 5 | $less(5,3) | (~spl12_7 | ~spl12_8)),
% 184.43/41.42 inference(superposition,[],[f785,f249])).
% 184.43/41.42 tff(f121272,plain,(
% 184.43/41.42 ~p__less_equal__(sK7,sK8) | (~spl12_7 | ~spl12_8)),
% 184.43/41.42 inference(evaluation,[],[f121269])).
% 184.43/41.42 tff(f121304,plain,(
% 184.43/41.42 ( ! [X0 : $int] : ($less(5,X0) | $less(X0,3) | p__less_equal__(sK8,sK7)) ) | (~spl12_7 | ~spl12_8)),
% 184.43/41.42 inference(superposition,[],[f802,f249])).
% 184.43/41.42 tff(f121730,plain,(
% 184.43/41.42 ~spl12_879 | ~spl12_745 | ~spl12_885),
% 184.43/41.42 inference(avatar_split_clause,[],[f115621,f112979,f96129,f110262])).
% 184.43/41.42 tff(f121779,plain,(
% 184.43/41.42 spl12_1023 | ~spl12_10 | ~spl12_12 | ~spl12_691),
% 184.43/41.42 inference(avatar_split_clause,[],[f117296,f95851,f272,f262,f120024])).
% 184.43/41.42 tff(f127964,plain,(
% 184.43/41.42 f__integer__(sK11(sK8)) = sK8 | c__supremum__ = sK8 | c__infimum__ = sK8 | ~spl12_8),
% 184.43/41.42 inference(resolution,[],[f120700,f191])).
% 184.43/41.42 tff(f132744,plain,(
% 184.43/41.42 ~$less(sK11(sK1),$sum(1,1)) | ~spl12_863),
% 184.43/41.42 inference(resolution,[],[f103611,f32])).
% 184.43/41.42 tff(f132749,plain,(
% 184.43/41.42 ~$less(sK11(sK1),2) | ~spl12_863),
% 184.43/41.42 inference(evaluation,[],[f132744])).
% 184.43/41.42 tff(f132757,plain,(
% 184.43/41.42 ~$less(sK11(sK1),$sum(0,1)) | ~spl12_959),
% 184.43/41.42 inference(resolution,[],[f118852,f32])).
% 184.43/41.42 tff(f132763,plain,(
% 184.43/41.42 ~$less(sK11(sK1),1) | ~spl12_959),
% 184.43/41.42 inference(evaluation,[],[f132757])).
% 184.43/41.42 tff(f132794,plain,(
% 184.43/41.42 $less(2,sK11(sK1)) | 2 = sK11(sK1) | ~spl12_863),
% 184.43/41.42 inference(resolution,[],[f132749,f28])).
% 184.43/41.42 tff(f132811,definition,(
% 184.43/41.42 spl12_1302 <=> 2 = sK11(sK1)),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_1302])],[avatar_definition])).
% 184.43/41.42 tff(f132813,plain,(
% 184.43/41.42 2 = sK11(sK1) | ~spl12_1302),
% 184.43/41.42 inference(avatar_component_clause,[],[f132811])).
% 184.43/41.42 tff(f132819,definition,(
% 184.43/41.42 spl12_1304 <=> $less(2,sK11(sK1))),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_1304])],[avatar_definition])).
% 184.43/41.42 tff(f132821,plain,(
% 184.43/41.42 $less(2,sK11(sK1)) | ~spl12_1304),
% 184.43/41.42 inference(avatar_component_clause,[],[f132819])).
% 184.43/41.42 tff(f133027,plain,(
% 184.43/41.42 sK11(sK1) = 1 | $less(1,sK11(sK1)) | ~spl12_959),
% 184.43/41.42 inference(resolution,[],[f132763,f28])).
% 184.43/41.42 tff(f135149,plain,(
% 184.43/41.42 ~$less(sK11(sK1),$sum(2,1)) | ~spl12_1304),
% 184.43/41.42 inference(resolution,[],[f132821,f32])).
% 184.43/41.42 tff(f135154,plain,(
% 184.43/41.42 ~$less(sK11(sK1),3) | ~spl12_1304),
% 184.43/41.42 inference(evaluation,[],[f135149])).
% 184.43/41.42 tff(f135158,plain,(
% 184.43/41.42 $false | (~spl12_831 | ~spl12_1304)),
% 184.43/41.42 inference(forward_subsumption_resolution,[],[f135154,f98112])).
% 184.43/41.42 tff(f135159,plain,(
% 184.43/41.42 ~spl12_831 | ~spl12_1304),
% 184.43/41.42 inference(avatar_contradiction_clause,[],[f135158])).
% 184.43/41.42 tff(f167310,plain,(
% 184.43/41.42 sK4 = sK1 | ~p__less_equal__(sK4,sK1) | ~spl12_81),
% 184.43/41.42 inference(resolution,[],[f23573,f135])).
% 184.43/41.42 tff(f167336,plain,(
% 184.43/41.42 p__less_equal__(sK4,sK1) | ~spl12_769),
% 184.43/41.42 inference(resolution,[],[f97505,f64])).
% 184.43/41.42 tff(f196936,plain,(
% 184.43/41.42 f__integer__(1) = sK1 | (~spl12_350 | ~spl12_861)),
% 184.43/41.42 inference(forward_demodulation,[],[f78175,f103603])).
% 184.43/41.42 tff(f196937,plain,(
% 184.43/41.42 spl12_436 | ~spl12_350 | ~spl12_861),
% 184.43/41.42 inference(avatar_split_clause,[],[f196936,f103601,f78173,f82109])).
% 184.43/41.42 tff(f197199,plain,(
% 184.43/41.42 $less(3,$sum(1,1)) | p__less_equal__(sK1,sK8) | (~spl12_8 | ~spl12_436)),
% 184.43/41.42 inference(superposition,[],[f121007,f82111])).
% 184.43/41.42 tff(f197279,plain,(
% 184.43/41.42 p__less_equal__(sK1,sK8) | (~spl12_8 | ~spl12_436)),
% 184.43/41.42 inference(evaluation,[],[f197199])).
% 184.43/41.42 tff(f197368,plain,(
% 184.43/41.42 $false | (~spl12_8 | spl12_18 | ~spl12_436)),
% 184.43/41.42 inference(forward_subsumption_resolution,[],[f197279,f417])).
% 184.43/41.42 tff(f197369,plain,(
% 184.43/41.42 ~spl12_8 | spl12_18 | ~spl12_436),
% 184.43/41.42 inference(avatar_contradiction_clause,[],[f197368])).
% 184.43/41.42 tff(f215449,plain,(
% 184.43/41.42 f__integer__(2) = sK1 | (~spl12_350 | ~spl12_1302)),
% 184.43/41.42 inference(forward_demodulation,[],[f78175,f132813])).
% 184.43/41.42 tff(f215915,plain,(
% 184.43/41.42 ~p__less_equal__(f__integer__($sum(1,2)),sK1) | (~spl12_350 | ~spl12_1302)),
% 184.43/41.42 inference(superposition,[],[f2174,f215449])).
% 184.43/41.42 tff(f216131,plain,(
% 184.43/41.42 ~p__less_equal__(f__integer__(3),sK1) | (~spl12_350 | ~spl12_1302)),
% 184.43/41.42 inference(evaluation,[],[f215915])).
% 184.43/41.42 tff(f216234,plain,(
% 184.43/41.42 ~p__less_equal__(sK8,sK1) | (~spl12_8 | ~spl12_350 | ~spl12_1302)),
% 184.43/41.42 inference(forward_demodulation,[],[f216131,f254])).
% 184.43/41.42 tff(f216268,plain,(
% 184.43/41.42 $false | (~spl12_8 | ~spl12_350 | ~spl12_512 | ~spl12_1302)),
% 184.43/41.42 inference(forward_subsumption_resolution,[],[f216234,f88272])).
% 184.43/41.42 tff(f216269,plain,(
% 184.43/41.42 ~spl12_8 | ~spl12_350 | ~spl12_512 | ~spl12_1302),
% 184.43/41.42 inference(avatar_contradiction_clause,[],[f216268])).
% 184.43/41.42 tff(f216274,plain,(
% 184.43/41.42 ~$less(sK11(sK1),5) | ~spl12_854),
% 184.43/41.42 inference(evaluation,[],[f107957])).
% 184.43/41.42 tff(f216298,plain,(
% 184.43/41.42 ~spl12_771 | ~spl12_854),
% 184.43/41.42 inference(avatar_split_clause,[],[f216274,f103274,f97512])).
% 184.43/41.42 tff(f216313,plain,(
% 184.43/41.42 $less(4,sK11(sK1)) | (~spl12_782 | spl12_852)),
% 184.43/41.42 inference(forward_subsumption_resolution,[],[f103245,f103266])).
% 184.43/41.42 tff(f216434,plain,(
% 184.43/41.42 ~spl12_831 | ~spl12_1304),
% 184.43/41.42 inference(avatar_split_clause,[],[f135154,f132819,f98110])).
% 184.43/41.42 tff(f216437,plain,(
% 184.43/41.42 ~spl12_84 | spl12_82 | ~spl12_81),
% 184.43/41.42 inference(avatar_split_clause,[],[f167310,f23572,f23576,f23593])).
% 184.43/41.42 tff(f216510,plain,(
% 184.43/41.42 spl12_84 | ~spl12_769),
% 184.43/41.42 inference(avatar_split_clause,[],[f167336,f97503,f23593])).
% 184.43/41.42 tff(f216557,plain,(
% 184.43/41.42 spl12_854 | ~spl12_782 | spl12_852),
% 184.43/41.42 inference(avatar_split_clause,[],[f216313,f103265,f97562,f103274])).
% 184.43/41.42 tff(f216931,definition,(
% 184.43/41.42 spl12_1633 <=> p__less_equal__(sK7,sK1)),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_1633])],[avatar_definition])).
% 184.43/41.42 tff(f216932,plain,(
% 184.43/41.42 ~p__less_equal__(sK7,sK1) | spl12_1633),
% 184.43/41.42 inference(avatar_component_clause,[],[f216931])).
% 184.43/41.42 tff(f216933,plain,(
% 184.43/41.42 p__less_equal__(sK7,sK1) | ~spl12_1633),
% 184.43/41.42 inference(avatar_component_clause,[],[f216931])).
% 184.43/41.42 tff(f217052,definition,(
% 184.43/41.42 spl12_1648 <=> sK7 = sK1),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_1648])],[avatar_definition])).
% 184.43/41.42 tff(f217053,plain,(
% 184.43/41.42 sK7 = sK1 | ~spl12_1648),
% 184.43/41.42 inference(avatar_component_clause,[],[f217052])).
% 184.43/41.42 tff(f217284,definition,(
% 184.43/41.42 spl12_1669 <=> ! [X1 : symbol] : p__less__(f__symbolic__(X1),sK7)),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_1669])],[avatar_definition])).
% 184.43/41.42 tff(f217285,plain,(
% 184.43/41.42 ( ! [X1 : symbol] : (p__less__(f__symbolic__(X1),sK7)) ) | ~spl12_1669),
% 184.43/41.42 inference(avatar_component_clause,[],[f217284])).
% 184.43/41.42 tff(f217340,plain,(
% 184.43/41.42 ~spl12_15 | ~spl12_7 | ~spl12_8),
% 184.43/41.42 inference(avatar_split_clause,[],[f121272,f252,f247,f402])).
% 184.43/41.42 tff(f217362,plain,(
% 184.43/41.42 spl12_28 | spl12_23 | ~spl12_7 | ~spl12_8),
% 184.43/41.42 inference(avatar_split_clause,[],[f121304,f252,f247,f1320,f1468])).
% 184.43/41.42 tff(f217558,plain,(
% 184.43/41.42 f__integer__(sK11(sK8)) = sK8 | c__supremum__ = sK8 | (~spl12_8 | spl12_19)),
% 184.43/41.42 inference(forward_subsumption_resolution,[],[f127964,f1252])).
% 184.43/41.42 tff(f217588,plain,(
% 184.43/41.42 spl12_745 | spl12_229 | ~spl12_8 | spl12_19),
% 184.43/41.42 inference(avatar_split_clause,[],[f217558,f1251,f252,f73875,f96129])).
% 184.43/41.42 tff(f217729,plain,(
% 184.43/41.42 $less(1,sK11(sK1)) | (spl12_861 | ~spl12_959)),
% 184.43/41.42 inference(forward_subsumption_resolution,[],[f133027,f103602])).
% 184.43/41.42 tff(f217973,plain,(
% 184.43/41.42 spl12_863 | spl12_861 | ~spl12_959),
% 184.43/41.42 inference(avatar_split_clause,[],[f217729,f118850,f103601,f103609])).
% 184.43/41.42 tff(f218955,plain,(
% 184.43/41.42 ~p__less_equal__(c__supremum__,sK7) | c__supremum__ = sK7 | ~spl12_7),
% 184.43/41.42 inference(resolution,[],[f88134,f135])).
% 184.43/41.42 tff(f218958,plain,(
% 184.43/41.42 c__supremum__ = sK7 | p__less__(c__supremum__,sK7) | ~spl12_7),
% 184.43/41.42 inference(resolution,[],[f88134,f391])).
% 184.43/41.42 tff(f218971,definition,(
% 184.43/41.42 spl12_1723 <=> c__supremum__ = sK7),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_1723])],[avatar_definition])).
% 184.43/41.42 tff(f218973,plain,(
% 184.43/41.42 c__supremum__ = sK7 | ~spl12_1723),
% 184.43/41.42 inference(avatar_component_clause,[],[f218971])).
% 184.43/41.42 tff(f218976,definition,(
% 184.43/41.42 spl12_1724 <=> p__less_equal__(c__supremum__,sK7)),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_1724])],[avatar_definition])).
% 184.43/41.42 tff(f218978,plain,(
% 184.43/41.42 ~p__less_equal__(c__supremum__,sK7) | spl12_1724),
% 184.43/41.42 inference(avatar_component_clause,[],[f218976])).
% 184.43/41.42 tff(f218979,plain,(
% 184.43/41.42 ~spl12_1724 | spl12_1723 | ~spl12_7),
% 184.43/41.42 inference(avatar_split_clause,[],[f218955,f247,f218971,f218976])).
% 184.43/41.42 tff(f218981,definition,(
% 184.43/41.42 spl12_1725 <=> p__less__(c__supremum__,sK7)),
% 184.43/41.42 introduced(definition,[new_symbols(definition,[spl12_1725])],[avatar_definition])).
% 184.43/41.42 tff(f218983,plain,(
% 184.43/41.42 p__less__(c__supremum__,sK7) | ~spl12_1725),
% 184.43/41.42 inference(avatar_component_clause,[],[f218981])).
% 184.43/41.42 tff(f218984,plain,(
% 184.43/41.42 spl12_1725 | spl12_1723 | ~spl12_7),
% 184.43/41.42 inference(avatar_split_clause,[],[f218958,f247,f218971,f218981])).
% 184.43/41.42 tff(f218996,plain,(
% 184.43/41.42 p__less__(sK1,sK7) | sK7 = sK1 | ~spl12_1633),
% 184.43/41.42 inference(resolution,[],[f216933,f391])).
% 184.43/41.42 tff(f219016,plain,(
% 184.43/41.42 sK7 = sK1 | (~spl12_4 | spl12_9 | ~spl12_1633)),
% 184.43/41.42 inference(forward_subsumption_resolution,[],[f218996,f323])).
% 184.43/41.42 tff(f219018,plain,(
% 184.43/41.42 spl12_1648 | ~spl12_4 | spl12_9 | ~spl12_1633),
% 184.43/41.42 inference(avatar_split_clause,[],[f219016,f216931,f257,f232,f217052])).
% 184.43/41.42 tff(f219684,plain,(
% 184.43/41.42 ( ! [X0 : symbol,X1 : $int] : (p__less__(f__symbolic__(X0),sK7) | $less(X1,5)) ) | ~spl12_7),
% 184.43/41.42 inference(resolution,[],[f2865,f204])).
% 184.43/41.42 tff(f219703,plain,(
% 184.43/41.42 spl12_1669 | spl12_31 | ~spl12_7),
% 184.43/41.42 inference(avatar_split_clause,[],[f219684,f247,f1693,f217284])).
% 184.43/41.42 tff(f219726,plain,(
% 184.43/41.42 ~p__less__(sK1,sK1) | (~spl12_4 | spl12_9 | ~spl12_1648)),
% 184.43/41.42 inference(superposition,[],[f323,f217053])).
% 184.43/41.42 tff(f219786,plain,(
% 184.43/41.42 $false | (~spl12_4 | spl12_9 | ~spl12_1648)),
% 184.43/41.42 inference(forward_subsumption_resolution,[],[f219726,f191])).
% 184.43/41.42 tff(f219787,plain,(
% 184.43/41.42 ~spl12_4 | spl12_9 | ~spl12_1648),
% 184.43/41.42 inference(avatar_contradiction_clause,[],[f219786])).
% 184.43/41.42 tff(f219988,plain,(
% 184.43/41.42 p__less__(sK7,sK1) | spl12_1633),
% 184.43/41.42 inference(resolution,[],[f216932,f188])).
% 184.43/41.42 tff(f224755,plain,(
% 184.43/41.42 ( ! [X0 : symbol] : (~p__less__(f__symbolic__(X0),sK7)) ) | ~spl12_1723),
% 184.43/41.42 inference(superposition,[],[f202,f218973])).
% 184.43/41.42 tff(f224934,plain,(
% 184.43/41.42 c__infimum__ = sK1 | f__integer__(sK11(sK1)) = sK1 | c__supremum__ = sK1 | (~spl12_7 | spl12_1633)),
% 184.43/41.42 inference(resolution,[],[f48273,f219988])).
% 184.43/41.42 tff(f224968,plain,(
% 184.43/41.42 p__less__(sK1,sK7) | c__supremum__ = sK8 | c__infimum__ = sK8 | f__integer__(sK11(sK8)) = sK8 | (~spl12_7 | spl12_18)),
% 184.43/41.42 inference(resolution,[],[f48273,f2867])).
% 184.43/41.42 tff(f224969,plain,(
% 184.43/41.42 c__supremum__ = sK1 | f__integer__(sK11(sK1)) = sK1 | (~spl12_7 | spl12_116 | spl12_1633)),
% 184.43/41.42 inference(forward_subsumption_resolution,[],[f224934,f69435])).
% 184.43/41.42 tff(f224984,plain,(
% 184.43/41.42 f__integer__(sK11(sK8)) = sK8 | c__supremum__ = sK8 | c__infimum__ = sK8 | (~spl12_4 | ~spl12_7 | spl12_9 | spl12_18)),
% 184.43/41.42 inference(forward_subsumption_resolution,[],[f224968,f323])).
% 184.43/41.42 tff(f225030,plain,(
% 184.43/41.42 spl12_263 | spl12_350 | ~spl12_7 | spl12_116 | spl12_1633),
% 184.43/41.42 inference(avatar_split_clause,[],[f224969,f216931,f69434,f247,f78173,f74828])).
% 184.43/41.42 tff(f225460,plain,(
% 184.43/41.42 p__less_equal__(sK7,sK1) | (~spl12_7 | ~spl12_263)),
% 184.43/41.42 inference(superposition,[],[f88134,f74830])).
% 184.43/41.42 tff(f225473,plain,(
% 184.43/41.42 p__less__(sK1,sK7) | (~spl12_263 | ~spl12_1725)),
% 184.43/41.42 inference(superposition,[],[f218983,f74830])).
% 184.43/41.42 tff(f225476,plain,(
% 184.43/41.42 $false | (~spl12_7 | ~spl12_263 | spl12_1633)),
% 184.43/41.42 inference(forward_subsumption_resolution,[],[f225460,f216932])).
% 184.43/41.42 tff(f225477,plain,(
% 184.43/41.42 ~spl12_7 | ~spl12_263 | spl12_1633),
% 184.43/41.42 inference(avatar_contradiction_clause,[],[f225476])).
% 184.43/41.42 tff(f225478,plain,(
% 184.43/41.42 $false | (~spl12_4 | spl12_9 | ~spl12_263 | ~spl12_1725)),
% 184.43/41.42 inference(forward_subsumption_resolution,[],[f225473,f323])).
% 184.43/41.42 tff(f225479,plain,(
% 184.43/41.42 ~spl12_4 | spl12_9 | ~spl12_263 | ~spl12_1725),
% 184.43/41.42 inference(avatar_contradiction_clause,[],[f225478])).
% 184.43/41.42 tff(f226150,plain,(
% 184.43/41.42 ~spl12_1023 | spl12_959 | ~spl12_350),
% 184.43/41.42 inference(avatar_split_clause,[],[f97411,f78173,f118850,f120024])).
% 184.43/41.42 tff(f226985,plain,(
% 184.43/41.42 f__integer__(sK11(sK1)) = sK1 | c__supremum__ = sK1 | (~spl12_3 | ~spl12_86 | spl12_116)),
% 184.43/41.42 inference(forward_subsumption_resolution,[],[f78099,f69435])).
% 184.43/41.42 tff(f227075,plain,(
% 184.43/41.42 $less(sK11(sK1),5) | (~spl12_7 | ~spl12_350 | spl12_1633)),
% 184.43/41.42 inference(forward_subsumption_resolution,[],[f97263,f216932])).
% 184.43/41.42 tff(f228039,plain,(
% 184.43/41.42 spl12_782 | spl12_788 | spl12_831),
% 184.43/41.42 inference(avatar_split_clause,[],[f103109,f98110,f97597,f97562])).
% 184.43/41.42 tff(f228095,plain,(
% 184.43/41.42 spl12_1302 | spl12_1304 | ~spl12_863),
% 184.43/41.42 inference(avatar_split_clause,[],[f132794,f103609,f132819,f132811])).
% 184.43/41.42 tff(f228180,plain,(
% 184.43/41.42 $less(sK11(sK1),5) | (~spl12_3 | ~spl12_350 | spl12_769)),
% 184.43/41.42 inference(forward_subsumption_resolution,[],[f97298,f97504])).
% 184.43/41.42 tff(f228310,plain,(
% 184.43/41.42 spl12_263 | spl12_350 | ~spl12_3 | ~spl12_86 | spl12_116),
% 184.43/41.42 inference(avatar_split_clause,[],[f226985,f69434,f33031,f228,f78173,f74828])).
% 184.43/41.42 tff(f228321,plain,(
% 184.43/41.42 spl12_771 | ~spl12_7 | ~spl12_350 | spl12_1633),
% 184.43/41.42 inference(avatar_split_clause,[],[f227075,f216931,f78173,f247,f97512])).
% 184.43/41.42 tff(f228434,plain,(
% 184.43/41.42 spl12_771 | ~spl12_3 | ~spl12_350 | spl12_769),
% 184.43/41.42 inference(avatar_split_clause,[],[f228180,f97503,f78173,f228,f97512])).
% 184.43/41.42 tff(f261351,plain,(
% 184.43/41.42 p__less_equal__(sK1,sK3) | ~spl12_804),
% 184.43/41.42 inference(resolution,[],[f97679,f64])).
% 184.43/41.42 tff(f261352,plain,(
% 184.43/41.42 spl12_26 | ~spl12_804),
% 184.43/41.42 inference(avatar_split_clause,[],[f261351,f97677,f1410])).
% 184.43/41.42 tff(f280441,plain,(
% 184.43/41.42 $less(1,sK11(sK8)) | 3 = 2 | $less(3,2) | spl12_644),
% 184.43/41.42 inference(resolution,[],[f95641,f5681])).
% 184.43/41.42 tff(f280455,plain,(
% 184.43/41.42 $less(1,sK11(sK8)) | spl12_644),
% 184.43/41.42 inference(evaluation,[],[f280441])).
% 184.43/41.42 tff(f280465,plain,(
% 184.43/41.42 spl12_885 | spl12_644),
% 184.43/41.42 inference(avatar_split_clause,[],[f280455,f95640,f112979])).
% 184.43/41.42 tff(f310208,plain,(
% 184.43/41.42 $false | (~spl12_1669 | ~spl12_1723)),
% 184.43/41.42 inference(forward_subsumption_resolution,[],[f224755,f217285])).
% 184.43/41.42 tff(f310209,plain,(
% 184.43/41.42 ~spl12_1669 | ~spl12_1723),
% 184.43/41.42 inference(avatar_contradiction_clause,[],[f310208])).
% 184.43/41.42 tff(f361180,plain,(
% 184.43/41.42 f__integer__(3) = sK1 | (~spl12_350 | ~spl12_788)),
% 184.43/41.42 inference(forward_demodulation,[],[f78175,f97599])).
% 184.43/41.42 tff(f370689,plain,(
% 184.43/41.42 sK8 = sK1 | ~p__less_equal__(sK8,sK1) | $less(3,3) | (~spl12_8 | ~spl12_350 | ~spl12_788)),
% 184.43/41.42 inference(superposition,[],[f465,f361180])).
% 184.43/41.42 tff(f370983,plain,(
% 184.43/41.42 sK8 = sK1 | ~p__less_equal__(sK8,sK1) | (~spl12_8 | ~spl12_350 | ~spl12_788)),
% 184.43/41.42 inference(evaluation,[],[f370689])).
% 184.43/41.42 tff(f371031,plain,(
% 184.43/41.42 ~p__less_equal__(sK8,sK1) | (~spl12_8 | spl12_17 | ~spl12_350 | ~spl12_788)),
% 184.43/41.42 inference(forward_subsumption_resolution,[],[f370983,f412])).
% 184.43/41.42 tff(f371045,plain,(
% 184.43/41.42 $false | (~spl12_8 | spl12_17 | ~spl12_350 | ~spl12_512 | ~spl12_788)),
% 184.43/41.42 inference(forward_subsumption_resolution,[],[f371031,f88272])).
% 184.43/41.42 tff(f371046,plain,(
% 184.43/41.42 ~spl12_8 | spl12_17 | ~spl12_350 | ~spl12_512 | ~spl12_788),
% 184.43/41.42 inference(avatar_contradiction_clause,[],[f371045])).
% 184.43/41.42 tff(f371298,plain,(
% 184.43/41.42 f__integer__(sK11(sK8)) = sK8 | c__supremum__ = sK8 | (~spl12_4 | ~spl12_7 | spl12_9 | spl12_18 | spl12_19)),
% 184.43/41.42 inference(forward_subsumption_resolution,[],[f224984,f1252])).
% 184.43/41.42 tff(f371416,plain,(
% 184.43/41.42 spl12_745 | spl12_229 | ~spl12_4 | ~spl12_7 | spl12_9 | spl12_18 | spl12_19),
% 184.43/41.42 inference(avatar_split_clause,[],[f371298,f1251,f415,f257,f247,f232,f73875,f96129])).
% 184.43/41.42 tff(f424935,plain,(
% 184.43/41.42 p__less_equal__(sK7,sK8) | (~spl12_7 | ~spl12_229)),
% 184.43/41.42 inference(superposition,[],[f88134,f73877])).
% 184.43/41.42 tff(f424943,plain,(
% 184.43/41.42 ~p__less_equal__(sK8,sK7) | (~spl12_229 | spl12_1724)),
% 184.43/41.42 inference(superposition,[],[f218978,f73877])).
% 184.43/41.42 tff(f424951,plain,(
% 184.43/41.42 $false | (~spl12_23 | ~spl12_229 | spl12_1724)),
% 184.43/41.42 inference(forward_subsumption_resolution,[],[f424943,f1322])).
% 184.43/41.42 tff(f424952,plain,(
% 184.43/41.42 ~spl12_23 | ~spl12_229 | spl12_1724),
% 184.43/41.42 inference(avatar_contradiction_clause,[],[f424951])).
% 184.43/41.42 tff(f424960,plain,(
% 184.43/41.42 $false | (~spl12_7 | spl12_15 | ~spl12_229)),
% 184.43/41.42 inference(forward_subsumption_resolution,[],[f424935,f404])).
% 184.43/41.42 tff(f424961,plain,(
% 184.43/41.42 ~spl12_7 | spl12_15 | ~spl12_229),
% 184.43/41.42 inference(avatar_contradiction_clause,[],[f424960])).
% 184.43/41.42 cnf(s2, plain, spl12_3 | spl12_4, inference(sat_conversion,[],[f235])).
% 184.43/41.42 cnf(s3, plain, ~spl12_1 | spl12_5, inference(sat_conversion,[],[f240])).
% 184.43/41.42 cnf(s4, plain, spl12_4 | spl12_6, inference(sat_conversion,[],[f245])).
% 184.43/41.42 cnf(s5, plain, spl12_2 | spl12_7, inference(sat_conversion,[],[f250])).
% 184.43/41.42 cnf(s6, plain, spl12_3 | spl12_8, inference(sat_conversion,[],[f255])).
% 184.43/41.42 cnf(s7, plain, spl12_2 | ~spl12_9, inference(sat_conversion,[],[f260])).
% 184.43/41.42 cnf(s8, plain, spl12_2 | spl12_10, inference(sat_conversion,[],[f265])).
% 184.43/41.42 cnf(s9, plain, spl12_8 | spl12_11, inference(sat_conversion,[],[f270])).
% 184.43/41.42 cnf(s11, plain, spl12_4 | spl12_13, inference(sat_conversion,[],[f280])).
% 184.43/41.42 cnf(s12, plain, spl12_2 | spl12_4, inference(sat_conversion,[],[f281])).
% 184.43/41.42 cnf(s13, plain, ~spl12_9 | spl12_13, inference(sat_conversion,[],[f282])).
% 184.43/41.42 cnf(s15, plain, spl12_4 | spl12_11, inference(sat_conversion,[],[f284])).
% 184.43/41.42 cnf(s16, plain, spl12_8 | ~spl12_14, inference(sat_conversion,[],[f289])).
% 184.43/41.42 cnf(s17, plain, spl12_6 | spl12_7, inference(sat_conversion,[],[f290])).
% 184.43/41.42 cnf(s19, plain, spl12_6 | ~spl12_9, inference(sat_conversion,[],[f292])).
% 184.43/41.42 cnf(s20, plain, spl12_3 | spl12_7, inference(sat_conversion,[],[f293])).
% 184.43/41.42 cnf(s21, plain, spl12_12 | spl12_13, inference(sat_conversion,[],[f294])).
% 184.43/41.42 cnf(s24, plain, spl12_10 | spl12_11, inference(sat_conversion,[],[f297])).
% 184.43/41.42 cnf(s25, plain, spl12_3 | spl12_10, inference(sat_conversion,[],[f298])).
% 184.43/41.42 cnf(s27, plain, spl12_2 | spl12_8, inference(sat_conversion,[],[f300])).
% 184.43/41.42 cnf(s29, plain, ~spl12_9 | ~spl12_14, inference(sat_conversion,[],[f302])).
% 184.43/41.42 cnf(s30, plain, spl12_7 | spl12_13, inference(sat_conversion,[],[f303])).
% 184.43/41.42 cnf(s31, plain, spl12_6 | spl12_10, inference(sat_conversion,[],[f304])).
% 184.43/41.42 cnf(s32, plain, spl12_2 | spl12_12, inference(sat_conversion,[],[f305])).
% 184.43/41.42 cnf(s34, plain, ~spl12_9 | spl12_11, inference(sat_conversion,[],[f307])).
% 184.43/41.42 cnf(s36, plain, spl12_4 | ~spl12_14, inference(sat_conversion,[],[f309])).
% 184.43/41.42 cnf(s37, plain, spl12_7 | spl12_11, inference(sat_conversion,[],[f310])).
% 184.43/41.42 cnf(s39, plain, spl12_11 | spl12_12, inference(sat_conversion,[],[f312])).
% 184.43/41.42 cnf(s43, plain, spl12_10 | spl12_13, inference(sat_conversion,[],[f316])).
% 184.43/41.42 cnf(s45, plain, spl12_10 | ~spl12_14, inference(sat_conversion,[],[f318])).
% 184.43/41.42 cnf(s46, plain, spl12_8 | spl12_13, inference(sat_conversion,[],[f319])).
% 184.43/41.42 cnf(s47, plain, spl12_7 | ~spl12_14, inference(sat_conversion,[],[f320])).
% 184.43/41.42 cnf(s48, plain, spl12_6 | spl12_8, inference(sat_conversion,[],[f321])).
% 184.43/41.42 cnf(s49, plain, spl12_3 | ~spl12_9, inference(sat_conversion,[],[f322])).
% 184.43/41.42 cnf(s50, plain, spl12_1 | spl12_5, inference(sat_conversion,[],[f326])).
% 184.43/41.42 cnf(s52, plain, ~spl12_10 | ~spl12_12 | spl12_17 | ~spl12_18, inference(sat_conversion,[],[f418])).
% 184.43/41.42 cnf(s55, plain, ~spl12_8 | ~spl12_19, inference(sat_conversion,[],[f1275])).
% 184.43/41.42 cnf(s105, plain, ~spl12_10 | ~spl12_12 | spl12_17 | spl12_58, inference(sat_conversion,[],[f2052])).
% 184.43/41.42 cnf(s112, plain, ~spl12_10 | ~spl12_12 | ~spl12_17, inference(sat_conversion,[],[f2070])).
% 184.43/41.42 cnf(s137, plain, ~spl12_11 | ~spl12_68, inference(sat_conversion,[],[f3583])).
% 184.43/41.42 cnf(s193, plain, ~spl12_81 | spl12_82 | spl12_86, inference(sat_conversion,[],[f33034])).
% 184.43/41.42 cnf(s195, plain, ~spl12_6 | spl12_14 | ~spl12_82, inference(sat_conversion,[],[f36123])).
% 184.43/41.42 cnf(s221, plain, ~spl12_2 | ~spl12_11 | ~spl12_13 | spl12_44, inference(sat_conversion,[],[f67643])).
% 184.43/41.42 cnf(s266, plain, ~spl12_114, inference(sat_conversion,[],[f69406])).
% 184.43/41.42 cnf(s323, plain, ~spl12_31, inference(sat_conversion,[],[f72083])).
% 184.43/41.42 cnf(s425, plain, ~spl12_28, inference(sat_conversion,[],[f73379])).
% 184.43/41.42 cnf(s628, plain, ~spl12_3 | spl12_84 | ~spl12_263, inference(sat_conversion,[],[f75780])).
% 184.43/41.42 cnf(s824, plain, ~spl12_6 | spl12_14 | spl12_81, inference(sat_conversion,[],[f77963])).
% 184.43/41.42 cnf(s1493, plain, spl12_18 | spl12_512, inference(sat_conversion,[],[f88438])).
% 184.43/41.42 cnf(s2288, plain, ~spl12_2 | ~spl12_13 | spl12_68 | ~spl12_113 | ~spl12_116, inference(sat_conversion,[],[f98080])).
% 184.43/41.42 cnf(s2431, plain, ~spl12_2 | ~spl12_11 | ~spl12_13 | spl12_25 | ~spl12_350 | spl12_782, inference(sat_conversion,[],[f98291])).
% 184.43/41.42 cnf(s2439, plain, ~spl12_2 | ~spl12_13 | spl12_25 | ~spl12_26, inference(sat_conversion,[],[f98297])).
% 184.43/41.42 cnf(s2483, plain, ~spl12_2 | ~spl12_13 | ~spl12_25, inference(sat_conversion,[],[f98522])).
% 184.43/41.42 cnf(s2991, plain, ~spl12_771 | ~spl12_854, inference(sat_conversion,[],[f107967])).
% 184.43/41.42 cnf(s3371, plain, spl12_691 | spl12_879, inference(sat_conversion,[],[f114491])).
% 184.43/41.42 cnf(s3495, plain, ~spl12_5 | ~spl12_350 | ~spl12_852, inference(sat_conversion,[],[f116571])).
% 184.43/41.42 cnf(s3959, plain, ~spl12_8 | ~spl12_58 | ~spl12_116, inference(sat_conversion,[],[f118243])).
% 184.43/41.42 cnf(s4406, plain, ~spl12_11 | ~spl12_350 | spl12_782 | spl12_804, inference(sat_conversion,[],[f119391])).
% 184.43/41.42 cnf(s4728, plain, ~spl12_11 | ~spl12_44 | spl12_952, inference(sat_conversion,[],[f119862])).
% 184.43/41.42 cnf(s4785, plain, ~spl12_11 | spl12_25 | ~spl12_350 | spl12_782 | ~spl12_952, inference(sat_conversion,[],[f119936])).
% 184.43/41.42 cnf(s4816, plain, ~spl12_11 | spl12_113 | spl12_114, inference(sat_conversion,[],[f119973])).
% 184.43/41.42 cnf(s5302, plain, ~spl12_8 | ~spl12_644 | ~spl12_745, inference(sat_conversion,[],[f120921])).
% 184.43/41.42 cnf(s5459, plain, ~spl12_745 | ~spl12_879 | ~spl12_885, inference(sat_conversion,[],[f121730])).
% 184.43/41.42 cnf(s5500, plain, ~spl12_10 | ~spl12_12 | ~spl12_691 | spl12_1023, inference(sat_conversion,[],[f121779])).
% 184.43/41.42 cnf(s6767, plain, ~spl12_831 | ~spl12_1304, inference(sat_conversion,[],[f135159])).
% 184.43/41.42 cnf(s8752, plain, ~spl12_350 | spl12_436 | ~spl12_861, inference(sat_conversion,[],[f196937])).
% 184.43/41.42 cnf(s8792, plain, ~spl12_8 | spl12_18 | ~spl12_436, inference(sat_conversion,[],[f197369])).
% 184.43/41.42 cnf(s9335, plain, ~spl12_8 | ~spl12_350 | ~spl12_512 | ~spl12_1302, inference(sat_conversion,[],[f216269])).
% 184.43/41.42 cnf(s9343, plain, ~spl12_771 | ~spl12_854, inference(sat_conversion,[],[f216298])).
% 184.43/41.42 cnf(s9374, plain, ~spl12_831 | ~spl12_1304, inference(sat_conversion,[],[f216434])).
% 184.43/41.42 cnf(s9375, plain, ~spl12_81 | spl12_82 | ~spl12_84, inference(sat_conversion,[],[f216437])).
% 184.43/41.42 cnf(s9401, plain, spl12_84 | ~spl12_769, inference(sat_conversion,[],[f216510])).
% 184.43/41.42 cnf(s9421, plain, ~spl12_782 | spl12_852 | spl12_854, inference(sat_conversion,[],[f216557])).
% 184.43/41.42 cnf(s9776, plain, ~spl12_7 | ~spl12_8 | ~spl12_15, inference(sat_conversion,[],[f217340])).
% 184.43/41.42 cnf(s9797, plain, ~spl12_7 | ~spl12_8 | spl12_23 | spl12_28, inference(sat_conversion,[],[f217362])).
% 184.43/41.42 cnf(s9920, plain, ~spl12_8 | spl12_19 | spl12_229 | spl12_745, inference(sat_conversion,[],[f217588])).
% 184.43/41.42 cnf(s10150, plain, spl12_861 | spl12_863 | ~spl12_959, inference(sat_conversion,[],[f217973])).
% 184.43/41.42 cnf(s10413, plain, ~spl12_7 | spl12_1723 | ~spl12_1724, inference(sat_conversion,[],[f218979])).
% 184.43/41.42 cnf(s10414, plain, ~spl12_7 | spl12_1723 | spl12_1725, inference(sat_conversion,[],[f218984])).
% 184.43/41.42 cnf(s10424, plain, ~spl12_4 | spl12_9 | ~spl12_1633 | spl12_1648, inference(sat_conversion,[],[f219018])).
% 184.43/41.42 cnf(s10504, plain, ~spl12_7 | spl12_31 | spl12_1669, inference(sat_conversion,[],[f219703])).
% 184.43/41.42 cnf(s10515, plain, ~spl12_4 | spl12_9 | ~spl12_1648, inference(sat_conversion,[],[f219787])).
% 184.43/41.42 cnf(s11319, plain, ~spl12_7 | spl12_116 | spl12_263 | spl12_350 | spl12_1633, inference(sat_conversion,[],[f225030])).
% 184.43/41.42 cnf(s11356, plain, ~spl12_7 | ~spl12_263 | spl12_1633, inference(sat_conversion,[],[f225477])).
% 184.43/41.42 cnf(s11357, plain, ~spl12_4 | spl12_9 | ~spl12_263 | ~spl12_1725, inference(sat_conversion,[],[f225479])).
% 184.43/41.42 cnf(s11379, plain, ~spl12_350 | spl12_959 | ~spl12_1023, inference(sat_conversion,[],[f226150])).
% 184.43/41.42 cnf(s13117, plain, spl12_782 | spl12_788 | spl12_831, inference(sat_conversion,[],[f228039])).
% 184.43/41.42 cnf(s13171, plain, ~spl12_863 | spl12_1302 | spl12_1304, inference(sat_conversion,[],[f228095])).
% 184.43/41.42 cnf(s13457, plain, ~spl12_3 | ~spl12_86 | spl12_116 | spl12_263 | spl12_350, inference(sat_conversion,[],[f228310])).
% 184.43/41.42 cnf(s13478, plain, ~spl12_7 | ~spl12_350 | spl12_771 | spl12_1633, inference(sat_conversion,[],[f228321])).
% 184.43/41.42 cnf(s13725, plain, ~spl12_3 | ~spl12_350 | spl12_769 | spl12_771, inference(sat_conversion,[],[f228434])).
% 184.43/41.42 cnf(s14635, plain, spl12_26 | ~spl12_804, inference(sat_conversion,[],[f261352])).
% 184.43/41.42 cnf(s14857, plain, spl12_644 | spl12_885, inference(sat_conversion,[],[f280465])).
% 184.43/41.42 cnf(s15184, plain, ~spl12_1669 | ~spl12_1723, inference(sat_conversion,[],[f310209])).
% 184.43/41.42 cnf(s15380, plain, ~spl12_8 | spl12_17 | ~spl12_350 | ~spl12_512 | ~spl12_788, inference(sat_conversion,[],[f371046])).
% 184.43/41.42 cnf(s15650, plain, ~spl12_4 | ~spl12_7 | spl12_9 | spl12_18 | spl12_19 | spl12_229 | spl12_745, inference(sat_conversion,[],[f371416])).
% 184.43/41.42 cnf(s16061, plain, ~spl12_23 | ~spl12_229 | spl12_1724, inference(sat_conversion,[],[f424952])).
% 184.43/41.42 cnf(s16066, plain, ~spl12_7 | spl12_15 | ~spl12_229, inference(sat_conversion,[],[f424961])).
% 184.43/41.42 cnf(s16095, plain, spl12_2 | ~spl12_5, inference(rat,[],[s10150,s13171,s11379,s9374,s5500,s13117,s3371,s9421,s5459,s9343,s14857,s3495,s13478,s5302,s15380,s9335,s8752,s11319,s15650,s1493,s8792,s3959,s16066,s11356,s52,s105,s9776,s10424,s10515,s112,s55,s5,s7,s8,s12,s27,s32])).
% 184.43/41.42 cnf(s16096, plain, ~spl12_12 | ~spl12_10 | spl12_263 | spl12_1633 | ~spl12_8 | ~spl12_7 | ~spl12_5, inference(rat,[],[s6767,s13117,s13171,s9421,s10150,s9343,s11379,s3495,s13478,s15380,s9335,s8752,s11319,s1493,s8792,s3959,s52,s105,s5500,s112,s3371,s5459,s14857,s5302,s9920,s16061,s9797,s10413,s15184,s10504,s55,s323,s425])).
% 184.43/41.42 cnf(s16097, plain, spl12_12 | spl12_263 | spl12_1633 | ~spl12_7 | ~spl12_5, inference(rat,[],[s2991,s9421,s3495,s13478,s4785,s11319,s4728,s2288,s2483,s221,s137,s4816,s21,s39,s16095,s266])).
% 184.43/41.42 cnf(s16098, plain, spl12_9 | ~spl12_8 | ~spl12_7 | ~spl12_4 | ~spl12_5, inference(rat,[],[s2991,s9421,s3495,s13725,s4785,s13457,s9401,s4728,s2288,s193,s9375,s221,s137,s4816,s195,s824,s2483,s24,s25,s31,s43,s45,s16096,s16097,s11357,s10424,s10515,s16095,s10414,s15184,s10504,s266,s323])).
% 184.43/41.42 cnf(s16099, plain, ~spl12_9 | ~spl12_5, inference(rat,[],[s9421,s9343,s2431,s3495,s13725,s13457,s628,s9401,s193,s9375,s2288,s2483,s195,s824,s137,s4816,s13,s19,s29,s34,s49,s16095,s266])).
% 184.43/41.42 cnf(s16100, plain, ~spl12_7 | ~spl12_4 | ~spl12_5, inference(rat,[],[s9421,s9343,s2431,s3495,s13725,s13457,s9401,s2288,s193,s9375,s137,s4816,s2483,s195,s824,s6,s9,s16,s46,s48,s11356,s16098,s16095,s10424,s10515,s16099,s266])).
% 184.43/41.42 cnf(s16101, plain, spl12_7 | ~spl12_5, inference(rat,[],[s2991,s9421,s3495,s13725,s4406,s13457,s628,s9401,s14635,s193,s9375,s2439,s2288,s195,s824,s2483,s137,s4816,s17,s20,s30,s37,s47,s16095,s266])).
% 184.43/41.42 cnf(s16102, plain, ~spl12_5, inference(rat,[],[s2991,s9421,s3495,s13725,s4406,s13457,s628,s9401,s14635,s193,s9375,s2439,s2288,s195,s824,s2483,s137,s4816,s2,s4,s11,s15,s36,s16100,s16101,s16095,s266])).
% 184.43/41.42 cnf(s16103, plain, spl12_1, inference(rat,[],[s50,s16102])).
% 184.43/41.42 cnf(s16110, plain, $false, inference(rat,[],[s3,s16102,s16103])).
% 184.43/41.42 tff(f424966,plain,(
% 184.43/41.42 $false),
% 184.43/41.42 inference(avatar_sat_refutation,[],[s16110])).
% 184.43/41.42 % SZS output end Proof for theBenchmark
% 184.43/41.42 % (419643)------------------------------
% 184.43/41.42 % (419643)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 184.43/41.42 % (419643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.43/41.42 % (419643)CaDiCaL version: 2.1.3
% 184.43/41.42 % (419643)Termination reason: Refutation
% 184.43/41.42 % (419643)Time elapsed: 19.760 s
% 184.43/41.42 % (419643)Peak memory usage: 131 MB
% 184.43/41.42 % (419643)Instructions burned: 24704 (million)
% 184.43/41.42 % (419171)Success in time 41.115 s
% 184.43/41.42 % Vampire exiting
%------------------------------------------------------------------------------