%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ARI178_1 : TPTP v9.3.1. Released v5.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:34:08 AM UTC 2026
% Result : Theorem 127.53s 18.29s
% Output : Refutation 127.53s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ARI178_1 : TPTP v9.3.1. Released v5.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 % Computer : n006.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 20:43:55 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.22 Running first-order model finding
% 0.08/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.87/0.84 % (162817)Will run a generic schedule for satisfiability detection.
% 3.87/0.84 % (162823)% WARNING: option uhcvi not known.
% 3.87/0.84 % (162823)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3276046728:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 3.87/0.84 % (162822)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2054415278_2999 on theBenchmark for (2999ds/0Mi)
% 3.87/0.84 % (162824)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1985423751:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 3.87/0.84 % (162822)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 3.87/0.84 % (162822)Terminated due to inappropriate strategy.
% 3.87/0.84 % (162822)------------------------------
% 3.87/0.84 % (162822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.87/0.84 % (162825)dis+10_1_sil=32000:sp=arity:random_seed=1453564599:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 3.87/0.84 % (162822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.87/0.84 % (162822)CaDiCaL version: 2.1.3
% 3.87/0.84 % (162822)Termination reason: Inappropriate
% 3.87/0.84 % (162822)Time elapsed: 0.0000 s
% 3.87/0.84 % (162822)Peak memory usage: 10 MB
% 3.87/0.84 % (162826)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3552191389:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 3.87/0.84 % (162828)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=25957119:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 3.87/0.84 % (162827)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=945669076:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 3.87/0.84 % (162822)------------------------------
% 3.87/0.84 % (162822)------------------------------
% 3.87/0.84 % (162836)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2964469867:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 3.87/0.84 % (162836)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 3.87/0.84 % (162836)Terminated due to inappropriate strategy.
% 3.87/0.84 % (162836)------------------------------
% 3.87/0.84 % (162836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.87/0.84 % (162836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.87/0.84 % (162836)CaDiCaL version: 2.1.3
% 3.87/0.84 % (162836)Termination reason: Inappropriate
% 3.87/0.84 % (162836)Time elapsed: 0.0000 s
% 3.87/0.84 % (162836)Peak memory usage: 10 MB
% 3.87/0.84 % (162836)------------------------------
% 3.87/0.84 % (162836)------------------------------
% 3.87/0.84 % (162838)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1833188689:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 3.87/0.84 % (162825)Instruction limit reached!
% 3.87/0.84 % (162825)------------------------------
% 3.87/0.84 % (162825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.87/0.84 % (162825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.87/0.84 % (162825)CaDiCaL version: 2.1.3
% 3.87/0.84 % (162825)Termination reason: Instruction limit
% 3.87/0.84 % (162825)Termination phase: Saturation
% 3.87/0.84 % (162825)Time elapsed: 0.067 s
% 3.87/0.84 % (162825)Peak memory usage: 12 MB
% 3.87/0.84 % (162825)Instructions burned: 109 (million)
% 3.87/0.84 % (162826)Instruction limit reached!
% 3.87/0.84 % (162826)------------------------------
% 3.87/0.84 % (162826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.87/0.84 % (162826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.87/0.84 % (162826)CaDiCaL version: 2.1.3
% 3.87/0.84 % (162826)Termination reason: Instruction limit
% 3.87/0.84 % (162826)Termination phase: Saturation
% 3.87/0.84 % (162826)Time elapsed: 0.072 s
% 3.87/0.84 % (162826)Peak memory usage: 12 MB
% 3.87/0.84 % (162826)Instructions burned: 116 (million)
% 3.87/0.84 % (162827)Instruction limit reached!
% 3.87/0.84 % (162827)------------------------------
% 3.87/0.84 % (162827)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.87/0.84 % (162827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.87/0.84 % (162827)CaDiCaL version: 2.1.3
% 3.87/0.84 % (162827)Termination reason: Instruction limit
% 3.87/0.84 % (162827)Termination phase: Saturation
% 3.87/0.84 % (162827)Time elapsed: 0.078 s
% 3.87/0.84 % (162827)Peak memory usage: 13 MB
% 3.87/0.84 % (162827)Instructions burned: 132 (million)
% 7.43/1.39 % (162840)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=3216548512:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 7.43/1.39 % (162841)ott-21_1_sil=16000:fs=off:random_seed=1563334609:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 7.43/1.39 % (162842)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2830545264:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 7.43/1.39 % (162828)Instruction limit reached!
% 7.43/1.39 % (162828)------------------------------
% 7.43/1.39 % (162828)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.43/1.39 % (162828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.43/1.39 % (162828)CaDiCaL version: 2.1.3
% 7.43/1.39 % (162828)Termination reason: Instruction limit
% 7.43/1.39 % (162828)Termination phase: Saturation
% 7.43/1.39 % (162828)Time elapsed: 0.107 s
% 7.43/1.39 % (162828)Peak memory usage: 13 MB
% 7.43/1.39 % (162828)Instructions burned: 160 (million)
% 7.43/1.39 % (162838)Instruction limit reached!
% 7.43/1.39 % (162838)------------------------------
% 7.43/1.39 % (162838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.43/1.39 % (162838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.43/1.39 % (162838)CaDiCaL version: 2.1.3
% 7.43/1.39 % (162838)Termination reason: Instruction limit
% 7.43/1.39 % (162838)Termination phase: Saturation
% 7.43/1.39 % (162838)Time elapsed: 0.086 s
% 7.43/1.39 % (162838)Peak memory usage: 13 MB
% 7.43/1.39 % (162838)Instructions burned: 131 (million)
% 7.43/1.39 % (162846)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2902422584:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 7.43/1.39 % (162846)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.43/1.39 % (162846)Terminated due to inappropriate strategy.
% 7.43/1.39 % (162846)------------------------------
% 7.43/1.39 % (162846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.43/1.39 % (162846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.43/1.39 % (162846)CaDiCaL version: 2.1.3
% 7.43/1.39 % (162846)Termination reason: Inappropriate
% 7.43/1.39 % (162846)Time elapsed: 0.0000 s
% 7.43/1.39 % (162846)Peak memory usage: 10 MB
% 7.43/1.39 % (162846)------------------------------
% 7.43/1.39 % (162846)------------------------------
% 7.43/1.39 % (162848)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3150233200:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 7.43/1.39 % (162849)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1605695245:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 7.43/1.39 % (162849)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.43/1.39 % (162849)Terminated due to inappropriate strategy.
% 7.43/1.39 % (162849)------------------------------
% 7.43/1.39 % (162849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.43/1.39 % (162849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.43/1.39 % (162849)CaDiCaL version: 2.1.3
% 7.43/1.39 % (162849)Termination reason: Inappropriate
% 7.43/1.39 % (162849)Time elapsed: 0.0000 s
% 7.43/1.39 % (162849)Peak memory usage: 10 MB
% 7.43/1.39 % (162849)------------------------------
% 7.43/1.39 % (162849)------------------------------
% 7.43/1.39 % (162852)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=2880223744:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi)
% 7.43/1.39 % (162841)Instruction limit reached!
% 7.43/1.39 % (162841)------------------------------
% 7.43/1.39 % (162841)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.43/1.39 % (162841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.43/1.39 % (162841)CaDiCaL version: 2.1.3
% 7.43/1.39 % (162841)Termination reason: Instruction limit
% 7.43/1.39 % (162841)Termination phase: Saturation
% 7.43/1.39 % (162841)Time elapsed: 0.082 s
% 7.43/1.39 % (162841)Peak memory usage: 12 MB
% 7.43/1.39 % (162841)Instructions burned: 181 (million)
% 7.43/1.39 % (162854)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=442721182:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 22.79/3.53 % (162842)Instruction limit reached!
% 22.79/3.53 % (162842)------------------------------
% 22.79/3.53 % (162842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.79/3.53 % (162842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.79/3.53 % (162842)CaDiCaL version: 2.1.3
% 22.79/3.53 % (162842)Termination reason: Instruction limit
% 22.79/3.53 % (162842)Termination phase: Saturation
% 22.79/3.53 % (162842)Time elapsed: 0.298 s
% 22.79/3.53 % (162842)Peak memory usage: 14 MB
% 22.79/3.53 % (162842)Instructions burned: 478 (million)
% 22.79/3.53 % (162856)fmb+10_1_sil=64000:random_seed=2286976380:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi)
% 22.79/3.53 % (162856)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 22.79/3.53 % (162856)Terminated due to inappropriate strategy.
% 22.79/3.53 % (162856)------------------------------
% 22.79/3.53 % (162856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.79/3.53 % (162856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.79/3.53 % (162856)CaDiCaL version: 2.1.3
% 22.79/3.53 % (162856)Termination reason: Inappropriate
% 22.79/3.53 % (162856)Time elapsed: 0.0000 s
% 22.79/3.53 % (162856)Peak memory usage: 10 MB
% 22.79/3.53 % (162856)------------------------------
% 22.79/3.53 % (162856)------------------------------
% 22.79/3.53 % (162858)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2320071417:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi)
% 22.79/3.53 % (162840)Instruction limit reached!
% 22.79/3.53 % (162840)------------------------------
% 22.79/3.53 % (162840)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.79/3.53 % (162840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.79/3.53 % (162840)CaDiCaL version: 2.1.3
% 22.79/3.53 % (162840)Termination reason: Instruction limit
% 22.79/3.53 % (162840)Termination phase: Saturation
% 22.79/3.53 % (162840)Time elapsed: 0.351 s
% 22.79/3.53 % (162840)Peak memory usage: 15 MB
% 22.79/3.53 % (162840)Instructions burned: 686 (million)
% 22.79/3.53 % (162858)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 22.79/3.53 % (162858)Terminated due to inappropriate strategy.
% 22.79/3.53 % (162858)------------------------------
% 22.79/3.53 % (162858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.79/3.53 % (162858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.79/3.53 % (162858)CaDiCaL version: 2.1.3
% 22.79/3.53 % (162858)Termination reason: Inappropriate
% 22.79/3.53 % (162858)Time elapsed: 0.0000 s
% 22.79/3.53 % (162858)Peak memory usage: 10 MB
% 22.79/3.53 % (162858)------------------------------
% 22.79/3.53 % (162858)------------------------------
% 22.79/3.53 % (162860)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3558860284:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi)
% 22.79/3.53 % (162860)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 22.79/3.53 % (162860)Terminated due to inappropriate strategy.
% 22.79/3.53 % (162860)------------------------------
% 22.79/3.53 % (162860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.79/3.53 % (162860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.79/3.53 % (162860)CaDiCaL version: 2.1.3
% 22.79/3.53 % (162860)Termination reason: Inappropriate
% 22.79/3.53 % (162860)Time elapsed: 0.0000 s
% 22.79/3.53 % (162860)Peak memory usage: 10 MB
% 22.79/3.53 % (162861)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1270604767:i=5131_2995 on theBenchmark for (2995ds/5131Mi)
% 22.79/3.53 % (162860)------------------------------
% 22.79/3.53 % (162860)------------------------------
% 22.79/3.53 % (162864)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=652955091:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi)
% 22.79/3.53 % (162852)Instruction limit reached!
% 22.79/3.53 % (162852)------------------------------
% 22.79/3.53 % (162852)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.79/3.53 % (162852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.79/3.53 % (162852)CaDiCaL version: 2.1.3
% 22.79/3.53 % (162852)Termination reason: Instruction limit
% 22.79/3.53 % (162852)Termination phase: Saturation
% 22.79/3.53 % (162852)Time elapsed: 0.379 s
% 22.79/3.53 % (162852)Peak memory usage: 16 MB
% 22.79/3.53 % (162852)Instructions burned: 693 (million)
% 22.79/3.53 % (162866)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2271106865:i=6324_2994 on theBenchmark for (2994ds/6324Mi)
% 41.88/6.16 % (162866)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 41.88/6.16 % (162866)Terminated due to inappropriate strategy.
% 41.88/6.16 % (162866)------------------------------
% 41.88/6.16 % (162866)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.88/6.16 % (162866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.88/6.16 % (162866)CaDiCaL version: 2.1.3
% 41.88/6.16 % (162866)Termination reason: Inappropriate
% 41.88/6.16 % (162866)Time elapsed: 0.0000 s
% 41.88/6.16 % (162866)Peak memory usage: 10 MB
% 41.88/6.16 % (162866)------------------------------
% 41.88/6.16 % (162866)------------------------------
% 41.88/6.16 % (162868)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1362702910:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi)
% 41.88/6.16 % (162868)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 41.88/6.16 % (162868)Terminated due to inappropriate strategy.
% 41.88/6.16 % (162868)------------------------------
% 41.88/6.16 % (162868)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.88/6.16 % (162868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.88/6.16 % (162868)CaDiCaL version: 2.1.3
% 41.88/6.16 % (162868)Termination reason: Inappropriate
% 41.88/6.16 % (162868)Time elapsed: 0.0000 s
% 41.88/6.16 % (162868)Peak memory usage: 10 MB
% 41.88/6.16 % (162868)------------------------------
% 41.88/6.16 % (162868)------------------------------
% 41.88/6.16 % (162870)ott-2_1_sil=16000:newcnf=on:random_seed=1125670943:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi)
% 41.88/6.16 % (162854)Instruction limit reached!
% 41.88/6.16 % (162854)------------------------------
% 41.88/6.16 % (162854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.88/6.16 % (162854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.88/6.16 % (162854)CaDiCaL version: 2.1.3
% 41.88/6.16 % (162854)Termination reason: Instruction limit
% 41.88/6.16 % (162854)Termination phase: Saturation
% 41.88/6.16 % (162854)Time elapsed: 0.491 s
% 41.88/6.16 % (162854)Peak memory usage: 21 MB
% 41.88/6.16 % (162854)Instructions burned: 881 (million)
% 41.88/6.16 % (162872)ott+10_1_sil=32000:tgt=ground:random_seed=87033850:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi)
% 41.88/6.16 % (162848)Instruction limit reached!
% 41.88/6.16 % (162848)------------------------------
% 41.88/6.16 % (162848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.88/6.16 % (162848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.88/6.16 % (162848)CaDiCaL version: 2.1.3
% 41.88/6.16 % (162848)Termination reason: Instruction limit
% 41.88/6.16 % (162848)Termination phase: Saturation
% 41.88/6.16 % (162848)Time elapsed: 0.713 s
% 41.88/6.16 % (162848)Peak memory usage: 20 MB
% 41.88/6.16 % (162848)Instructions burned: 1179 (million)
% 41.88/6.16 % (162874)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=302075149:i=54282_2990 on theBenchmark for (2990ds/54282Mi)
% 41.88/6.16 % (162874)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 41.88/6.16 % (162874)Terminated due to inappropriate strategy.
% 41.88/6.16 % (162874)------------------------------
% 41.88/6.16 % (162874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.88/6.16 % (162874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.88/6.16 % (162874)CaDiCaL version: 2.1.3
% 41.88/6.16 % (162874)Termination reason: Inappropriate
% 41.88/6.16 % (162874)Time elapsed: 0.0000 s
% 41.88/6.16 % (162874)Peak memory usage: 10 MB
% 41.88/6.16 % (162874)------------------------------
% 41.88/6.16 % (162874)------------------------------
% 41.88/6.16 % (162876)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1173653006:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi)
% 41.88/6.16 % (162870)Instruction limit reached!
% 41.88/6.16 % (162870)------------------------------
% 41.88/6.16 % (162870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.88/6.16 % (162870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.88/6.16 % (162870)CaDiCaL version: 2.1.3
% 41.88/6.16 % (162870)Termination reason: Instruction limit
% 41.88/6.16 % (162870)Termination phase: Saturation
% 41.88/6.16 % (162870)Time elapsed: 0.517 s
% 41.88/6.16 % (162870)Peak memory usage: 16 MB
% 125.18/18.00 % (162870)Instructions burned: 870 (million)
% 125.18/18.00 % (162878)dis+21_1_sil=32000:sas=cadical:random_seed=1463155898:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi)
% 125.18/18.00 % (162864)Instruction limit reached!
% 125.18/18.00 % (162864)------------------------------
% 125.18/18.00 % (162864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 125.18/18.00 % (162864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.18/18.00 % (162864)CaDiCaL version: 2.1.3
% 125.18/18.00 % (162864)Termination reason: Instruction limit
% 125.18/18.00 % (162864)Termination phase: Saturation
% 125.18/18.00 % (162864)Time elapsed: 0.727 s
% 125.18/18.00 % (162864)Peak memory usage: 24 MB
% 125.18/18.00 % (162864)Instructions burned: 1473 (million)
% 125.18/18.00 % (162880)ott+11_1_sil=16000:gs=on:random_seed=1481936771:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi)
% 125.18/18.00 % (162880)Instruction limit reached!
% 125.18/18.00 % (162880)------------------------------
% 125.18/18.00 % (162880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 125.18/18.00 % (162880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.18/18.00 % (162880)CaDiCaL version: 2.1.3
% 125.18/18.00 % (162880)Termination reason: Instruction limit
% 125.18/18.00 % (162880)Termination phase: Saturation
% 125.18/18.00 % (162880)Time elapsed: 1.288 s
% 125.18/18.00 % (162880)Peak memory usage: 24 MB
% 125.18/18.00 % (162880)Instructions burned: 2252 (million)
% 125.18/18.00 % (162882)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3678887220:fmbsr=1.6:i=67534_2974 on theBenchmark for (2974ds/67534Mi)
% 125.18/18.00 % (162882)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 125.18/18.00 % (162882)Terminated due to inappropriate strategy.
% 125.18/18.00 % (162882)------------------------------
% 125.18/18.00 % (162882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 125.18/18.00 % (162882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.18/18.00 % (162882)CaDiCaL version: 2.1.3
% 125.18/18.00 % (162882)Termination reason: Inappropriate
% 125.18/18.00 % (162882)Time elapsed: 0.001 s
% 125.18/18.00 % (162882)Peak memory usage: 10 MB
% 125.18/18.00 % (162882)------------------------------
% 125.18/18.00 % (162882)------------------------------
% 125.18/18.00 % (162884)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3471501253:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2974 on theBenchmark for (2974ds/4591Mi)
% 125.18/18.00 % (162876)Instruction limit reached!
% 125.18/18.00 % (162876)------------------------------
% 125.18/18.00 % (162876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 125.18/18.00 % (162876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.18/18.00 % (162876)CaDiCaL version: 2.1.3
% 125.18/18.00 % (162876)Termination reason: Instruction limit
% 125.18/18.00 % (162876)Termination phase: Saturation
% 125.18/18.00 % (162876)Time elapsed: 1.944 s
% 125.18/18.00 % (162876)Peak memory usage: 47 MB
% 125.18/18.00 % (162876)Instructions burned: 3513 (million)
% 125.18/18.00 % (162886)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3771732614:i=29340_2971 on theBenchmark for (2971ds/29340Mi)
% 125.18/18.00 % (162861)Instruction limit reached!
% 125.18/18.00 % (162861)------------------------------
% 125.18/18.00 % (162861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 125.18/18.00 % (162861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.18/18.00 % (162861)CaDiCaL version: 2.1.3
% 125.18/18.00 % (162861)Termination reason: Instruction limit
% 125.18/18.00 % (162861)Termination phase: Saturation
% 125.18/18.00 % (162861)Time elapsed: 2.779 s
% 125.18/18.00 % (162861)Peak memory usage: 42 MB
% 125.18/18.00 % (162861)Instructions burned: 5132 (million)
% 125.18/18.00 % (162878)Instruction limit reached!
% 125.18/18.00 % (162878)------------------------------
% 125.18/18.00 % (162878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 125.18/18.00 % (162878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.18/18.00 % (162878)CaDiCaL version: 2.1.3
% 125.18/18.00 % (162878)Termination reason: Instruction limit
% 125.18/18.00 % (162878)Termination phase: Saturation
% 125.18/18.00 % (162878)Time elapsed: 2.116 s
% 125.18/18.00 % (162878)Peak memory usage: 37 MB
% 125.18/18.00 % (162878)Instructions burned: 3773 (million)
% 125.18/18.00 % (162888)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3951604442:i=5211_2967 on theBenchmark for (2967ds/5211Mi)
% 127.53/18.29 % (162890)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=963870772:i=5497:nm=2_2966 on theBenchmark for (2966ds/5497Mi)
% 127.53/18.29 % (162890)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 127.53/18.29 % (162890)Terminated due to inappropriate strategy.
% 127.53/18.29 % (162890)------------------------------
% 127.53/18.29 % (162890)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.53/18.29 % (162890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.53/18.29 % (162890)CaDiCaL version: 2.1.3
% 127.53/18.29 % (162890)Termination reason: Inappropriate
% 127.53/18.29 % (162890)Time elapsed: 0.0000 s
% 127.53/18.29 % (162890)Peak memory usage: 10 MB
% 127.53/18.29 % (162890)------------------------------
% 127.53/18.29 % (162890)------------------------------
% 127.53/18.29 % (162892)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1673338436:fmbsr=2:i=46332_2966 on theBenchmark for (2966ds/46332Mi)
% 127.53/18.29 % (162892)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 127.53/18.29 % (162892)Terminated due to inappropriate strategy.
% 127.53/18.29 % (162892)------------------------------
% 127.53/18.29 % (162892)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.53/18.29 % (162892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.53/18.29 % (162892)CaDiCaL version: 2.1.3
% 127.53/18.29 % (162892)Termination reason: Inappropriate
% 127.53/18.29 % (162892)Time elapsed: 0.001 s
% 127.53/18.29 % (162892)Peak memory usage: 11 MB
% 127.53/18.29 % (162892)------------------------------
% 127.53/18.29 % (162892)------------------------------
% 127.53/18.29 % (162894)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3474935086:i=14071_2966 on theBenchmark for (2966ds/14071Mi)
% 127.53/18.29 % (162894)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 127.53/18.29 % (162894)Terminated due to inappropriate strategy.
% 127.53/18.29 % (162894)------------------------------
% 127.53/18.29 % (162894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.53/18.29 % (162894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.53/18.29 % (162894)CaDiCaL version: 2.1.3
% 127.53/18.29 % (162894)Termination reason: Inappropriate
% 127.53/18.29 % (162894)Time elapsed: 0.0000 s
% 127.53/18.29 % (162894)Peak memory usage: 10 MB
% 127.53/18.29 % (162894)------------------------------
% 127.53/18.29 % (162894)------------------------------
% 127.53/18.29 % (162896)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2067506760:i=22565:add=on:rawr=on_2966 on theBenchmark for (2966ds/22565Mi)
% 127.53/18.29 % (162872)Instruction limit reached!
% 127.53/18.29 % (162872)------------------------------
% 127.53/18.29 % (162872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.53/18.29 % (162872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.53/18.29 % (162872)CaDiCaL version: 2.1.3
% 127.53/18.29 % (162872)Termination reason: Instruction limit
% 127.53/18.29 % (162872)Termination phase: Saturation
% 127.53/18.29 % (162872)Time elapsed: 3.229 s
% 127.53/18.29 % (162872)Peak memory usage: 38 MB
% 127.53/18.29 % (162872)Instructions burned: 5116 (million)
% 127.53/18.29 % (162900)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1561556727:i=8173:av=off_2960 on theBenchmark for (2960ds/8173Mi)
% 127.53/18.29 % (162884)Instruction limit reached!
% 127.53/18.29 % (162884)------------------------------
% 127.53/18.29 % (162884)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.53/18.29 % (162884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.53/18.29 % (162884)CaDiCaL version: 2.1.3
% 127.53/18.29 % (162884)Termination reason: Instruction limit
% 127.53/18.29 % (162884)Termination phase: Saturation
% 127.53/18.29 % (162884)Time elapsed: 2.447 s
% 127.53/18.29 % (162884)Peak memory usage: 34 MB
% 127.53/18.29 % (162884)Instructions burned: 4592 (million)
% 127.53/18.29 % (162902)dis+10_16:1_sil=16000:random_seed=652041351:i=9155:fsr=off_2949 on theBenchmark for (2949ds/9155Mi)
% 127.53/18.29 % (162888)Instruction limit reached!
% 127.53/18.29 % (162888)------------------------------
% 127.53/18.29 % (162888)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.53/18.29 % (162888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.53/18.29 % (162888)CaDiCaL version: 2.1.3
% 127.53/18.29 % (162888)Termination reason: Instruction limit
% 127.53/18.29 % (162888)Termination phase: Saturation
% 127.53/18.29 % (162888)Time elapsed: 2.629 s
% 127.53/18.29 % (162888)Peak memory usage: 50 MB
% 127.53/18.29 % (162888)Instructions burned: 5212 (million)
% 127.53/18.29 % (162904)ott-3_8_sil=64000:random_seed=2952206901:i=20139:bs=on_2940 on theBenchmark for (2940ds/20139Mi)
% 127.53/18.29 % (162900)Instruction limit reached!
% 127.53/18.29 % (162900)------------------------------
% 127.53/18.29 % (162900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.53/18.29 % (162900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.53/18.29 % (162900)CaDiCaL version: 2.1.3
% 127.53/18.29 % (162900)Termination reason: Instruction limit
% 127.53/18.29 % (162900)Termination phase: Saturation
% 127.53/18.29 % (162900)Time elapsed: 5.298 s
% 127.53/18.29 % (162900)Peak memory usage: 54 MB
% 127.53/18.29 % (162900)Instructions burned: 8175 (million)
% 127.53/18.29 % (162906)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2180186572:fmbsr=2:i=32576_2906 on theBenchmark for (2906ds/32576Mi)
% 127.53/18.29 % (162906)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 127.53/18.29 % (162906)Terminated due to inappropriate strategy.
% 127.53/18.29 % (162906)------------------------------
% 127.53/18.29 % (162906)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.53/18.29 % (162906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.53/18.29 % (162906)CaDiCaL version: 2.1.3
% 127.53/18.29 % (162906)Termination reason: Inappropriate
% 127.53/18.29 % (162906)Time elapsed: 0.001 s
% 127.53/18.29 % (162906)Peak memory usage: 10 MB
% 127.53/18.29 % (162906)------------------------------
% 127.53/18.29 % (162906)------------------------------
% 127.53/18.29 % (162908)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=534316037:i=11404_2906 on theBenchmark for (2906ds/11404Mi)
% 127.53/18.29 % (162902)Instruction limit reached!
% 127.53/18.29 % (162902)------------------------------
% 127.53/18.29 % (162902)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.53/18.29 % (162902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.53/18.29 % (162902)CaDiCaL version: 2.1.3
% 127.53/18.29 % (162902)Termination reason: Instruction limit
% 127.53/18.29 % (162902)Termination phase: Saturation
% 127.53/18.29 % (162902)Time elapsed: 4.760 s
% 127.53/18.29 % (162902)Peak memory usage: 55 MB
% 127.53/18.29 % (162902)Instructions burned: 9155 (million)
% 127.53/18.29 % (162910)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=855664439:i=14134_2901 on theBenchmark for (2901ds/14134Mi)
% 127.53/18.29 % (162896)Instruction limit reached!
% 127.53/18.29 % (162896)------------------------------
% 127.53/18.29 % (162896)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.53/18.29 % (162896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.53/18.29 % (162896)CaDiCaL version: 2.1.3
% 127.53/18.29 % (162896)Termination reason: Instruction limit
% 127.53/18.29 % (162896)Termination phase: Saturation
% 127.53/18.29 % (162896)Time elapsed: 9.738 s
% 127.53/18.29 % (162896)Peak memory usage: 234 MB
% 127.53/18.29 % (162896)Instructions burned: 22566 (million)
% 127.53/18.29 % (162912)dis+33_16_sil=32000:sac=on:random_seed=3198297357:i=15851:nm=0_2868 on theBenchmark for (2868ds/15851Mi)
% 127.53/18.29 % (162908)Instruction limit reached!
% 127.53/18.29 % (162908)------------------------------
% 127.53/18.29 % (162908)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.53/18.29 % (162908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.53/18.29 % (162908)CaDiCaL version: 2.1.3
% 127.53/18.29 % (162908)Termination reason: Instruction limit
% 127.53/18.29 % (162908)Termination phase: Saturation
% 127.53/18.29 % (162908)Time elapsed: 8.089 s
% 127.53/18.29 % (162908)Peak memory usage: 56 MB
% 127.53/18.29 % (162908)Instructions burned: 11404 (million)
% 127.53/18.29 % (163345)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2836699082:avsq=on:i=17627:add=on:amm=off_2825 on theBenchmark for (2825ds/17627Mi)
% 127.53/18.29 % (162886)Instruction limit reached!
% 127.53/18.29 % (162886)------------------------------
% 127.53/18.29 % (162886)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.53/18.29 % (162886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.53/18.29 % (162886)CaDiCaL version: 2.1.3
% 127.53/18.29 % (162886)Termination reason: Instruction limit
% 127.53/18.29 % (162886)Termination phase: Saturation
% 127.53/18.29 % (162886)Time elapsed: 14.792 s
% 127.53/18.29 % (162886)Peak memory usage: 397 MB
% 127.53/18.29 % (162886)Instructions burned: 29342 (million)
% 127.53/18.29 % (163347)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2403285338:s2a=on:i=53295_2822 on theBenchmark for (2822ds/53295Mi)
% 127.53/18.29 % (162823) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-162817-162823"...
% 127.53/18.29 % (162823)...printing done.
% 127.53/18.29 % (162823)Refutation found. Thanks to Tanya!
% 127.53/18.29 % SZS status Theorem for theBenchmark
% 127.53/18.29 % SZS output start Proof for theBenchmark
% 127.53/18.29 tff(func_def_7, type, sK0: $int).
% 127.53/18.29 tff(func_def_8, type, sK1: $int).
% 127.53/18.29 tff(func_def_9, type, sK2: $int).
% 127.53/18.29 tff(f1,conjecture,(
% 127.53/18.29 ! [X0 : $int,X1 : $int,X2 : $int] : (($sum($sum($product(2,X0),X1),X2) = 10 & $sum($sum(X0,$product(2,X1)),X2) = 10) => X2 != 0)),
% 127.53/18.29 file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1)).
% 127.53/18.29 tff(f2,negated_conjecture,(
% 127.53/18.29 ~ ! [X0 : $int,X1 : $int,X2 : $int] : (($sum($sum($product(2,X0),X1),X2) = 10 & $sum($sum(X0,$product(2,X1)),X2) = 10) => X2 != 0)),
% 127.53/18.29 inference(negated_conjecture,[status(cth)],[f1])).
% 127.53/18.29 tff(f3,definition,(
% 127.53/18.29 ( ! [X0 : $int,X1 : $int] : ($sum(X0,X1) = $sum(X1,X0)) )),
% 127.53/18.29 introduced(theory,[tha_commutativity])).
% 127.53/18.29 tff(f4,definition,(
% 127.53/18.29 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum(X0,$sum(X1,X2)) = $sum($sum(X0,X1),X2)) )),
% 127.53/18.29 introduced(theory,[tha_associativity])).
% 127.53/18.29 tff(f6,definition,(
% 127.53/18.29 ( ! [X0 : $int,X1 : $int] : ($uminus($sum(X0,X1)) = $sum($uminus(X1),$uminus(X0))) )),
% 127.53/18.29 introduced(theory,[tha_inverse_op_op_inverses])).
% 127.53/18.29 tff(f7,definition,(
% 127.53/18.29 ( ! [X0 : $int] : (0 = $sum(X0,$uminus(X0))) )),
% 127.53/18.29 introduced(theory,[tha_inverse_op_unit])).
% 127.53/18.29 tff(f9,definition,(
% 127.53/18.29 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X1,X2) | ~$less(X0,X1) | $less(X0,X2)) )),
% 127.53/18.29 introduced(theory,[tha_transitivity])).
% 127.53/18.29 tff(f10,definition,(
% 127.53/18.29 ( ! [X0 : $int,X1 : $int] : ($less(X1,X0) | $less(X0,X1) | X0 = X1) )),
% 127.53/18.29 introduced(theory,[tha_order_totality])).
% 127.53/18.29 tff(f11,definition,(
% 127.53/18.29 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($less($sum(X0,X2),$sum(X1,X2)) | ~$less(X0,X1)) )),
% 127.53/18.29 introduced(theory,[tha_order_monotonicity])).
% 127.53/18.29 tff(f12,definition,(
% 127.53/18.29 ( ! [X0 : $int,X1 : $int] : ($less(X1,$sum(X0,1)) | $less(X0,X1)) )),
% 127.53/18.29 introduced(theory,[tha_order_plus_one_dichotomy])).
% 127.53/18.29 tff(f13,definition,(
% 127.53/18.29 ( ! [X0 : $int] : ($uminus($uminus(X0)) = X0) )),
% 127.53/18.29 introduced(theory,[tha_minus_minus_x])).
% 127.53/18.29 tff(f14,definition,(
% 127.53/18.29 ( ! [X0 : $int,X1 : $int] : ($product(X0,X1) = $product(X1,X0)) )),
% 127.53/18.29 introduced(theory,[tha_commutativity])).
% 127.53/18.29 tff(f15,definition,(
% 127.53/18.29 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($product(X0,$product(X1,X2)) = $product($product(X0,X1),X2)) )),
% 127.53/18.29 introduced(theory,[tha_associativity])).
% 127.53/18.29 tff(f16,definition,(
% 127.53/18.29 ( ! [X0 : $int] : ($product(X0,1) = X0) )),
% 127.53/18.29 introduced(theory,[tha_right_identity])).
% 127.53/18.29 tff(f18,definition,(
% 127.53/18.29 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($product(X0,$sum(X1,X2)) = $sum($product(X0,X1),$product(X0,X2))) )),
% 127.53/18.29 introduced(theory,[tha_distributivity])).
% 127.53/18.29 tff(f19,definition,(
% 127.53/18.29 ( ! [X2 : $int,X3 : $int,X0 : $int,X1 : $int] : (0 = X0 | $product(X0,X2) != X1 | $product(X0,X3) != X1 | X2 = X3) )),
% 127.53/18.29 introduced(theory,[tha_divisibility])).
% 127.53/18.29 tff(f20,definition,(
% 127.53/18.29 ( ! [X0 : $int,X1 : $int] : (~$less(X1,$sum(X0,1)) | ~$less(X0,X1)) )),
% 127.53/18.29 introduced(theory,[tha_extra_integer_ordering])).
% 127.53/18.29 tff(f21,plain,(
% 127.53/18.29 ? [X0 : $int,X1 : $int,X2 : $int] : (0 = X2 & ($sum($sum($product(2,X0),X1),X2) = 10 & $sum($sum(X0,$product(2,X1)),X2) = 10))),
% 127.53/18.29 inference(ennf_transformation,[],[f2])).
% 127.53/18.29 tff(f22,plain,(
% 127.53/18.29 ? [X0 : $int,X1 : $int,X2 : $int] : (0 = X2 & $sum($sum($product(2,X0),X1),X2) = 10 & $sum($sum(X0,$product(2,X1)),X2) = 10)),
% 127.53/18.29 inference(flattening,[],[f21])).
% 127.53/18.29 tff(f23,plain,(
% 127.53/18.29 10 = $sum($sum(sK0,$product(2,sK1)),sK2)),
% 127.53/18.29 inference(cnf_transformation,[],[f22])).
% 127.53/18.29 tff(f24,plain,(
% 127.53/18.29 10 = $sum($sum($product(2,sK0),sK1),sK2)),
% 127.53/18.29 inference(cnf_transformation,[],[f22])).
% 127.53/18.29 tff(f25,plain,(
% 127.53/18.29 0 = sK2),
% 127.53/18.29 inference(cnf_transformation,[],[f22])).
% 127.53/18.29 tff(f26,plain,(
% 127.53/18.29 10 = $sum($sum($product(2,sK0),sK1),0)),
% 127.53/18.29 inference(definition_unfolding,[],[f24,f25])).
% 127.53/18.29 tff(f27,plain,(
% 127.53/18.29 10 = $sum($sum(sK0,$product(2,sK1)),0)),
% 127.53/18.29 inference(definition_unfolding,[],[f23,f25])).
% 127.53/18.29 tff(f28,plain,(
% 127.53/18.29 ( ! [X2 : $int,X3 : $int,X0 : $int] : ($product(X0,X2) != $product(X0,X3) | 0 = X0 | X2 = X3) )),
% 127.53/18.29 inference(equality_resolution,[],[f19])).
% 127.53/18.29 tff(f29,plain,(
% 127.53/18.29 10 = $sum(sK0,$product(2,sK1))),
% 127.53/18.29 inference(evaluation,[],[f27])).
% 127.53/18.29 tff(f30,plain,(
% 127.53/18.29 10 = $sum($product(2,sK0),sK1)),
% 127.53/18.29 inference(evaluation,[],[f26])).
% 127.53/18.29 tff(f31,plain,(
% 127.53/18.29 ( ! [X0 : $int] : (0 = $sum($uminus(X0),X0)) )),
% 127.53/18.29 inference(superposition,[],[f7,f13])).
% 127.53/18.29 tff(f32,plain,(
% 127.53/18.29 10 = $sum(sK1,$product(2,sK0))),
% 127.53/18.29 inference(superposition,[],[f3,f30])).
% 127.53/18.29 tff(f49,plain,(
% 127.53/18.29 ( ! [X0 : $int,X1 : $int] : ($less(X1,$sum(1,X0)) | $less(X0,X1)) )),
% 127.53/18.29 inference(superposition,[],[f12,f3])).
% 127.53/18.29 tff(f52,plain,(
% 127.53/18.29 ( ! [X0 : $int,X1 : $int] : (~$less(X0,X1) | ~$less(X1,$sum(1,X0))) )),
% 127.53/18.29 inference(superposition,[],[f20,f3])).
% 127.53/18.29 tff(f59,plain,(
% 127.53/18.29 ( ! [X0 : $int,X1 : $int] : (~$less(X1,X0) | $sum(X1,1) = X0 | $less($sum(X1,1),X0)) )),
% 127.53/18.29 inference(resolution,[],[f10,f20])).
% 127.53/18.29 tff(f60,plain,(
% 127.53/18.29 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X2,X0) | X0 = X1 | $less(X1,X0) | $less(X2,X1)) )),
% 127.53/18.29 inference(resolution,[],[f10,f9])).
% 127.53/18.29 tff(f64,plain,(
% 127.53/18.29 ( ! [X0 : $int,X1 : $int] : ($uminus($sum(X1,$uminus(X0))) = $sum(X0,$uminus(X1))) )),
% 127.53/18.29 inference(superposition,[],[f6,f13])).
% 127.53/18.29 tff(f67,plain,(
% 127.53/18.29 ( ! [X0 : $int,X1 : $int] : ($uminus($sum(X0,X1)) = $sum($uminus(X0),$uminus(X1))) )),
% 127.53/18.29 inference(superposition,[],[f6,f3])).
% 127.53/18.29 tff(f87,plain,(
% 127.53/18.29 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X1,X2) | $less($sum(X0,X1),$sum(X2,X0))) )),
% 127.53/18.29 inference(superposition,[],[f11,f3])).
% 127.53/18.29 tff(f89,plain,(
% 127.53/18.29 ( ! [X0 : $int] : (~$less($product(2,sK0),X0) | $less(10,$sum(X0,sK1))) )),
% 127.53/18.29 inference(superposition,[],[f11,f30])).
% 127.53/18.29 tff(f92,plain,(
% 127.53/18.29 ( ! [X0 : $int] : (~$less(sK1,X0) | $less(10,$sum(X0,$product(2,sK0)))) )),
% 127.53/18.29 inference(superposition,[],[f11,f32])).
% 127.53/18.29 tff(f94,plain,(
% 127.53/18.29 ( ! [X0 : $int,X1 : $int] : (~$less(X0,X1) | $less($sum(X0,$uminus(X1)),0)) )),
% 127.53/18.29 inference(superposition,[],[f11,f7])).
% 127.53/18.29 tff(f99,plain,(
% 127.53/18.29 ( ! [X0 : $int] : (~$less(X0,sK0) | $less($sum(X0,$product(2,sK1)),10)) )),
% 127.53/18.29 inference(superposition,[],[f11,f29])).
% 127.53/18.29 tff(f100,plain,(
% 127.53/18.29 ( ! [X0 : $int] : (~$less(X0,sK1) | $less($sum(X0,$product(2,sK0)),10)) )),
% 127.53/18.29 inference(superposition,[],[f11,f32])).
% 127.53/18.29 tff(f103,plain,(
% 127.53/18.29 ( ! [X0 : $int] : ($less(10,$sum($sum(X0,1),sK1)) | $less(X0,$product(2,sK0))) )),
% 127.53/18.29 inference(resolution,[],[f89,f12])).
% 127.53/18.29 tff(f110,plain,(
% 127.53/18.29 ( ! [X0 : $int] : ($less(10,$sum(sK1,$sum(X0,1))) | $less(X0,$product(2,sK0))) )),
% 127.53/18.29 inference(forward_demodulation,[],[f103,f3])).
% 127.53/18.29 tff(f113,plain,(
% 127.53/18.29 ( ! [X0 : $int,X1 : $int] : ($sum(0,X1) = $sum(X0,$sum($uminus(X0),X1))) )),
% 127.53/18.29 inference(superposition,[],[f4,f7])).
% 127.53/18.29 tff(f114,plain,(
% 127.53/18.29 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum($sum(X0,X1),X2) = $sum(X1,$sum(X0,X2))) )),
% 127.53/18.29 inference(superposition,[],[f4,f3])).
% 127.53/18.29 tff(f116,plain,(
% 127.53/18.29 ( ! [X0 : $int] : ($sum($product(2,sK0),$sum(sK1,X0)) = $sum(10,X0)) )),
% 127.53/18.29 inference(superposition,[],[f4,f30])).
% 127.53/18.29 tff(f118,plain,(
% 127.53/18.29 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum($uminus(X1),$sum($uminus(X0),X2)) = $sum($uminus($sum(X0,X1)),X2)) )),
% 127.53/18.29 inference(superposition,[],[f4,f6])).
% 127.53/18.29 tff(f119,plain,(
% 127.53/18.29 ( ! [X0 : $int] : ($sum(10,X0) = $sum(sK0,$sum($product(2,sK1),X0))) )),
% 127.53/18.29 inference(superposition,[],[f4,f29])).
% 127.53/18.29 tff(f120,plain,(
% 127.53/18.29 ( ! [X0 : $int] : ($sum(10,X0) = $sum(sK1,$sum($product(2,sK0),X0))) )),
% 127.53/18.29 inference(superposition,[],[f4,f32])).
% 127.53/18.29 tff(f122,plain,(
% 127.53/18.29 ( ! [X0 : $int,X1 : $int] : (0 = $sum(X0,$sum(X1,$uminus($sum(X0,X1))))) )),
% 127.53/18.29 inference(superposition,[],[f4,f7])).
% 127.53/18.29 tff(f123,plain,(
% 127.53/18.29 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum(X0,$sum(X1,X2)) = $sum(X1,$sum(X2,X0))) )),
% 127.53/18.29 inference(superposition,[],[f4,f3])).
% 127.53/18.29 tff(f131,plain,(
% 127.53/18.29 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X2,$sum(X0,$sum(X1,1))) | ~$less($sum(X0,X1),X2)) )),
% 127.53/18.29 inference(superposition,[],[f20,f4])).
% 127.53/18.29 tff(f132,plain,(
% 127.53/18.29 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($less(X2,$sum(X0,$sum(X1,1))) | $less($sum(X0,X1),X2)) )),
% 127.53/18.29 inference(superposition,[],[f12,f4])).
% 127.53/18.29 tff(f134,plain,(
% 127.53/18.29 ( ! [X0 : $int,X1 : $int] : ($sum(X0,$sum($uminus(X0),X1)) = X1) )),
% 127.53/18.29 inference(evaluation,[],[f113])).
% 127.53/18.29 tff(f145,plain,(
% 127.53/18.29 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($product(X0,$product(X1,X2)) = $product(X1,$product(X2,X0))) )),
% 127.53/18.29 inference(superposition,[],[f15,f14])).
% 127.53/18.29 tff(f163,plain,(
% 127.53/18.29 ( ! [X0 : $int,X1 : $int] : ($product(X0,$sum(1,X1)) = $sum(X0,$product(X0,X1))) )),
% 127.53/18.29 inference(superposition,[],[f18,f16])).
% 127.53/18.29 tff(f168,plain,(
% 127.53/18.29 ( ! [X0 : $int,X1 : $int] : ($product(X0,$sum(X1,1)) = $sum($product(X0,X1),X0)) )),
% 127.53/18.29 inference(superposition,[],[f18,f16])).
% 127.53/18.29 tff(f170,plain,(
% 127.53/18.29 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($product(X1,$sum(X2,X0)) = $sum($product(X1,X2),$product(X0,X1))) )),
% 127.53/18.29 inference(superposition,[],[f18,f14])).
% 127.53/18.29 tff(f173,plain,(
% 127.53/18.29 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum($product(X0,X1),$product(X0,X2)) = $product(X0,$sum(X2,X1))) )),
% 127.53/18.29 inference(superposition,[],[f18,f3])).
% 127.53/18.29 tff(f175,plain,(
% 127.53/18.29 ( ! [X2 : $int,X3 : $int,X0 : $int,X1 : $int] : ($sum($product(X0,X1),$sum($product(X0,X2),X3)) = $sum($product(X0,$sum(X1,X2)),X3)) )),
% 127.53/18.29 inference(superposition,[],[f4,f18])).
% 127.53/18.29 tff(f186,plain,(
% 127.53/18.29 ( ! [X0 : $int,X1 : $int] : ($product(X0,X1) != X0 | 0 = X0 | 1 = X1) )),
% 127.53/18.29 inference(superposition,[],[f28,f16])).
% 127.53/18.29 tff(f197,plain,(
% 127.53/18.29 ( ! [X0 : $int] : ($less($sum(X0,$product(2,sK1)),10) | $less(sK0,X0) | sK0 = X0) )),
% 127.53/18.29 inference(resolution,[],[f99,f10])).
% 127.53/18.29 tff(f210,plain,(
% 127.53/18.29 $sum(10,$uminus(sK1)) = $sum($product(2,sK0),0)),
% 127.53/18.29 inference(superposition,[],[f116,f7])).
% 127.53/18.29 tff(f216,plain,(
% 127.53/18.29 $product(2,sK0) = $sum(10,$uminus(sK1))),
% 127.53/18.29 inference(evaluation,[],[f210])).
% 127.53/18.29 tff(f220,plain,(
% 127.53/18.29 ( ! [X0 : $int] : ($sum(10,$product(2,X0)) = $sum(sK0,$product(2,$sum(sK1,X0)))) )),
% 127.53/18.29 inference(superposition,[],[f119,f18])).
% 127.53/18.29 tff(f222,plain,(
% 127.53/18.29 $sum(10,$uminus($product(2,sK1))) = $sum(sK0,0)),
% 127.53/18.29 inference(superposition,[],[f119,f7])).
% 127.53/18.29 tff(f223,plain,(
% 127.53/18.29 ( ! [X0 : $int] : ($sum(10,X0) = $sum(sK0,$sum(X0,$product(2,sK1)))) )),
% 127.53/18.29 inference(superposition,[],[f119,f3])).
% 127.53/18.29 tff(f228,plain,(
% 127.53/18.29 sK0 = $sum(10,$uminus($product(2,sK1)))),
% 127.53/18.29 inference(evaluation,[],[f222])).
% 127.53/18.29 tff(f245,plain,(
% 127.53/18.29 ( ! [X0 : $int] : (~$less(X0,0) | ~$less($uminus(1),X0)) )),
% 127.53/18.29 inference(superposition,[],[f20,f31])).
% 127.53/18.29 tff(f246,plain,(
% 127.53/18.29 ( ! [X0 : $int] : ($less(X0,0) | $less($uminus(1),X0)) )),
% 127.53/18.29 inference(superposition,[],[f12,f31])).
% 127.53/18.29 tff(f247,plain,(
% 127.53/18.29 ( ! [X0 : $int] : ($less(X0,0) | $less(-1,X0)) )),
% 127.53/18.29 inference(evaluation,[],[f246])).
% 127.53/18.29 tff(f248,plain,(
% 127.53/18.29 ( ! [X0 : $int] : (~$less(X0,0) | ~$less(-1,X0)) )),
% 127.53/18.29 inference(evaluation,[],[f245])).
% 127.53/18.29 tff(f273,plain,(
% 127.53/18.29 ( ! [X0 : $int,X1 : $int] : (~$less(X0,$sum(1,X1)) | $less(X0,X1) | X0 = X1) )),
% 127.53/18.29 inference(resolution,[],[f52,f10])).
% 127.53/18.29 tff(f287,plain,(
% 127.53/18.29 ( ! [X0 : $int,X1 : $int] : ($uminus(X0) = $sum(X1,$uminus($sum(X0,X1)))) )),
% 127.53/18.29 inference(superposition,[],[f134,f6])).
% 127.53/18.29 tff(f294,plain,(
% 127.53/18.29 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum(X0,$sum(X1,$sum($uminus($sum(X0,X1)),X2))) = X2) )),
% 127.53/18.29 inference(superposition,[],[f134,f4])).
% 127.53/18.29 tff(f356,plain,(
% 127.53/18.29 $sum(sK1,$uminus(10)) = $uminus($product(2,sK0))),
% 127.53/18.29 inference(superposition,[],[f64,f216])).
% 127.53/18.29 tff(f368,plain,(
% 127.53/18.29 $uminus($product(2,sK0)) = $sum(sK1,-10)),
% 127.53/18.29 inference(evaluation,[],[f356])).
% 127.53/18.29 tff(f372,plain,(
% 127.53/18.29 $uminus($product(2,sK0)) = $sum(-10,sK1)),
% 127.53/18.29 inference(forward_demodulation,[],[f368,f3])).
% 127.53/18.29 tff(f453,plain,(
% 127.53/18.29 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($less($sum(X0,X1),$sum($sum(1,X2),X0)) | $less(X2,X1)) )),
% 127.53/18.29 inference(resolution,[],[f87,f49])).
% 127.53/18.29 tff(f464,plain,(
% 127.53/18.29 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($less($sum(X0,X1),$sum(1,$sum(X2,X0))) | $less(X2,X1)) )),
% 127.53/18.29 inference(forward_demodulation,[],[f453,f4])).
% 127.53/18.29 tff(f502,plain,(
% 127.53/18.29 ( ! [X2 : $int,X0 : $int,X1 : $int] : (0 = $sum($product(X0,X1),$sum($product(X0,X2),$uminus($product(X0,$sum(X1,X2)))))) )),
% 127.53/18.29 inference(superposition,[],[f122,f18])).
% 127.53/18.29 tff(f503,plain,(
% 127.53/18.29 ( ! [X0 : $int] : (0 = $sum($product(2,sK0),$sum($sum(sK1,X0),$uminus($sum(10,X0))))) )),
% 127.53/18.29 inference(superposition,[],[f122,f116])).
% 127.53/18.29 tff(f504,plain,(
% 127.53/18.29 0 = $sum($product(2,sK0),$sum(sK1,$uminus(10)))),
% 127.53/18.29 inference(superposition,[],[f122,f30])).
% 127.53/18.29 tff(f514,plain,(
% 127.53/18.29 0 = $sum(sK1,$sum($product(2,sK0),$uminus(10)))),
% 127.53/18.29 inference(superposition,[],[f122,f32])).
% 127.53/18.29 tff(f529,plain,(
% 127.53/18.29 ( ! [X0 : $int] : ($sum(sK0,0) = $sum(10,$sum(X0,$uminus($sum($product(2,sK1),X0))))) )),
% 127.53/18.29 inference(superposition,[],[f119,f122])).
% 127.53/18.29 tff(f536,plain,(
% 127.53/18.29 ( ! [X0 : $int] : ($sum($product(2,sK0),0) = $sum(10,$sum(X0,$uminus($sum(sK1,X0))))) )),
% 127.53/18.29 inference(superposition,[],[f116,f122])).
% 127.53/18.29 tff(f537,plain,(
% 127.53/18.29 ( ! [X0 : $int] : ($product(2,sK0) = $sum(10,$sum(X0,$uminus($sum(sK1,X0))))) )),
% 127.53/18.29 inference(evaluation,[],[f536])).
% 127.53/18.29 tff(f540,plain,(
% 127.53/18.29 ( ! [X0 : $int] : (sK0 = $sum(10,$sum(X0,$uminus($sum($product(2,sK1),X0))))) )),
% 127.53/18.29 inference(evaluation,[],[f529])).
% 127.53/18.29 tff(f542,plain,(
% 127.53/18.29 0 = $sum(sK1,$sum($product(2,sK0),-10))),
% 127.53/18.29 inference(evaluation,[],[f514])).
% 127.53/18.29 tff(f548,plain,(
% 127.53/18.29 0 = $sum($product(2,sK0),$sum(sK1,-10))),
% 127.53/18.29 inference(evaluation,[],[f504])).
% 127.53/18.29 tff(f565,plain,(
% 127.53/18.29 0 = $sum(sK1,$sum(-10,$product(2,sK0)))),
% 127.53/18.29 inference(forward_demodulation,[],[f542,f3])).
% 127.53/18.29 tff(f570,plain,(
% 127.53/18.29 0 = $sum($product(2,sK0),$sum(-10,sK1))),
% 127.53/18.29 inference(forward_demodulation,[],[f548,f3])).
% 127.53/18.29 tff(f571,plain,(
% 127.53/18.29 ( ! [X0 : $int] : (0 = $sum($product(2,sK0),$sum(sK1,$sum(X0,$uminus($sum(10,X0)))))) )),
% 127.53/18.29 inference(forward_demodulation,[],[f503,f4])).
% 127.53/18.29 tff(f619,plain,(
% 127.53/18.29 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum(X2,$sum(X1,$sum($uminus($sum(X1,X2)),X0))) = X0) )),
% 127.53/18.29 inference(superposition,[],[f114,f134])).
% 127.53/18.29 tff(f667,plain,(
% 127.53/18.29 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum(X2,$uminus($sum(X0,X1))) = $sum($uminus(X0),$sum($uminus(X1),X2))) )),
% 127.53/18.29 inference(superposition,[],[f123,f67])).
% 127.53/18.29 tff(f694,plain,(
% 127.53/18.29 ( ! [X2 : $int,X3 : $int,X0 : $int,X1 : $int] : ($sum(X3,$sum(X0,$sum(X1,X2))) = $sum(X2,$sum(X3,$sum(X1,X0)))) )),
% 127.53/18.29 inference(superposition,[],[f123,f114])).
% 127.53/18.29 tff(f701,plain,(
% 127.53/18.29 ( ! [X0 : $int] : ($sum(X0,10) = $sum($product(2,sK1),$sum(X0,sK0))) )),
% 127.53/18.29 inference(superposition,[],[f123,f29])).
% 127.53/18.29 tff(f726,plain,(
% 127.53/18.29 ( ! [X0 : $int,X1 : $int] : ($sum(10,$sum(X0,X1)) = $sum(sK0,$sum(X0,$sum(X1,$product(2,sK1))))) )),
% 127.53/18.29 inference(superposition,[],[f119,f123])).
% 127.53/18.29 tff(f733,plain,(
% 127.53/18.29 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum(X0,X1) = $sum(X2,$sum(X0,$sum(X1,$uminus(X2))))) )),
% 127.53/18.29 inference(superposition,[],[f134,f123])).
% 127.53/18.29 tff(f735,plain,(
% 127.53/18.29 ( ! [X0 : $int,X1 : $int] : ($sum(10,$sum(X0,X1)) = $sum($product(2,sK0),$sum(X0,$sum(X1,sK1)))) )),
% 127.53/18.29 inference(superposition,[],[f116,f123])).
% 127.53/18.29 tff(f951,plain,(
% 127.53/18.29 ( ! [X0 : $int] : ($product(X0,$sum(1,1)) = $sum(X0,X0)) )),
% 127.53/18.29 inference(superposition,[],[f163,f16])).
% 127.53/18.29 tff(f973,plain,(
% 127.53/18.29 ( ! [X0 : $int] : ($sum(X0,X0) = $product(X0,2)) )),
% 127.53/18.29 inference(evaluation,[],[f951])).
% 127.53/18.29 tff(f988,plain,(
% 127.53/18.29 ( ! [X0 : $int,X1 : $int] : ($sum(X0,$product(X0,X1)) = $product(X0,$sum(X1,1))) )),
% 127.53/18.29 inference(superposition,[],[f168,f3])).
% 127.53/18.29 tff(f1031,plain,(
% 127.53/18.29 ( ! [X0 : $int,X1 : $int] : ($product(X0,X1) != X1 | 0 = X1 | 1 = X0) )),
% 127.53/18.29 inference(superposition,[],[f186,f14])).
% 127.53/18.29 tff(f1107,plain,(
% 127.53/18.29 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X1,$sum(X2,$sum(1,X0))) | ~$less($sum(X2,X0),X1)) )),
% 127.53/18.29 inference(superposition,[],[f131,f3])).
% 127.53/18.29 tff(f1123,plain,(
% 127.53/18.29 ( ! [X0 : $int] : (~$less(X0,$sum(10,1)) | ~$less($sum(sK0,$product(2,sK1)),X0)) )),
% 127.53/18.29 inference(superposition,[],[f131,f119])).
% 127.53/18.29 tff(f1124,plain,(
% 127.53/18.29 ( ! [X0 : $int] : (~$less(X0,11) | ~$less($sum(sK0,$product(2,sK1)),X0)) )),
% 127.53/18.29 inference(evaluation,[],[f1123])).
% 127.53/18.29 tff(f1128,plain,(
% 127.53/18.29 ( ! [X0 : $int] : (~$less(X0,11) | ~$less(10,X0)) )),
% 127.53/18.29 inference(forward_demodulation,[],[f1124,f29])).
% 127.53/18.29 tff(f1166,plain,(
% 127.53/18.29 ( ! [X0 : $int] : ($less(X0,$sum(10,1)) | $less($sum(sK0,$product(2,sK1)),X0)) )),
% 127.53/18.29 inference(superposition,[],[f132,f119])).
% 127.53/18.29 tff(f1167,plain,(
% 127.53/18.29 ( ! [X0 : $int] : ($less(X0,11) | $less($sum(sK0,$product(2,sK1)),X0)) )),
% 127.53/18.29 inference(evaluation,[],[f1166])).
% 127.53/18.29 tff(f1171,plain,(
% 127.53/18.29 ( ! [X0 : $int] : ($less(10,X0) | $less(X0,11)) )),
% 127.53/18.29 inference(forward_demodulation,[],[f1167,f29])).
% 127.53/18.29 tff(f1268,plain,(
% 127.53/18.29 ( ! [X0 : $int,X1 : $int] : ($less(X0,11) | $less(X1,X0) | $less(10,X1) | X0 = X1) )),
% 127.53/18.29 inference(resolution,[],[f1171,f60])).
% 127.53/18.29 tff(f1276,plain,(
% 127.53/18.29 ( ! [X0 : $int,X1 : $int] : (~$less(X1,X0) | $less(10,X0) | $less(X1,11)) )),
% 127.53/18.29 inference(resolution,[],[f1171,f9])).
% 127.53/18.29 tff(f1290,plain,(
% 127.53/18.29 $less(10,sK1) | $less(10,$sum(11,$product(2,sK0)))),
% 127.53/18.29 inference(resolution,[],[f1171,f92])).
% 127.53/18.29 tff(f1296,definition,(
% 127.53/18.29 spl3_3 <=> $less(10,$sum(11,$product(2,sK0)))),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_3])],[avatar_definition])).
% 127.53/18.29 tff(f1298,plain,(
% 127.53/18.29 $less(10,$sum(11,$product(2,sK0))) | ~spl3_3),
% 127.53/18.29 inference(avatar_component_clause,[],[f1296])).
% 127.53/18.29 tff(f1300,definition,(
% 127.53/18.29 spl3_4 <=> $less(10,sK1)),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_4])],[avatar_definition])).
% 127.53/18.29 tff(f1302,plain,(
% 127.53/18.29 $less(10,sK1) | ~spl3_4),
% 127.53/18.29 inference(avatar_component_clause,[],[f1300])).
% 127.53/18.29 tff(f1303,plain,(
% 127.53/18.29 spl3_3 | spl3_4),
% 127.53/18.29 inference(avatar_split_clause,[],[f1290,f1300,f1296])).
% 127.53/18.29 tff(f1309,definition,(
% 127.53/18.29 spl3_6 <=> $less(10,sK0)),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_6])],[avatar_definition])).
% 127.53/18.29 tff(f1311,plain,(
% 127.53/18.29 $less(10,sK0) | ~spl3_6),
% 127.53/18.29 inference(avatar_component_clause,[],[f1309])).
% 127.53/18.29 tff(f1318,definition,(
% 127.53/18.29 spl3_8 <=> $less(10,$product(2,sK0))),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_8])],[avatar_definition])).
% 127.53/18.29 tff(f1319,plain,(
% 127.53/18.29 ~$less(10,$product(2,sK0)) | spl3_8),
% 127.53/18.29 inference(avatar_component_clause,[],[f1318])).
% 127.53/18.29 tff(f1320,plain,(
% 127.53/18.29 $less(10,$product(2,sK0)) | ~spl3_8),
% 127.53/18.29 inference(avatar_component_clause,[],[f1318])).
% 127.53/18.29 tff(f1323,plain,(
% 127.53/18.29 ~$less(sK1,$sum(1,10)) | ~spl3_4),
% 127.53/18.29 inference(resolution,[],[f1302,f52])).
% 127.53/18.29 tff(f1334,plain,(
% 127.53/18.29 ~$less(sK1,11) | ~spl3_4),
% 127.53/18.29 inference(evaluation,[],[f1323])).
% 127.53/18.29 tff(f1381,plain,(
% 127.53/18.29 ~$less($product(2,sK0),$sum(1,10)) | ~spl3_8),
% 127.53/18.29 inference(resolution,[],[f1320,f52])).
% 127.53/18.29 tff(f1388,plain,(
% 127.53/18.29 $less($sum(10,$uminus($product(2,sK0))),0) | ~spl3_8),
% 127.53/18.29 inference(resolution,[],[f1320,f94])).
% 127.53/18.29 tff(f1393,plain,(
% 127.53/18.29 $less($sum(10,$sum(-10,sK1)),0) | ~spl3_8),
% 127.53/18.29 inference(forward_demodulation,[],[f1388,f372])).
% 127.53/18.29 tff(f1520,plain,(
% 127.53/18.29 ( ! [X0 : $int] : ($sum(sK0,$product(2,$sum(sK1,X0))) = $sum(10,$product(X0,2))) )),
% 127.53/18.29 inference(superposition,[],[f119,f170])).
% 127.53/18.29 tff(f1557,plain,(
% 127.53/18.29 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($product(X0,$sum(X1,X2)) = $product(X0,$sum(X2,X1))) )),
% 127.53/18.29 inference(superposition,[],[f173,f18])).
% 127.53/18.29 tff(f1709,plain,(
% 127.53/18.29 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum($uminus(X2),$uminus($sum(X0,X1))) = $sum($uminus($sum(X1,X2)),$uminus(X0))) )),
% 127.53/18.29 inference(superposition,[],[f118,f6])).
% 127.53/18.29 tff(f1730,plain,(
% 127.53/18.29 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum($uminus(X0),X2) = $sum(X1,$sum($uminus($sum(X0,X1)),X2))) )),
% 127.53/18.29 inference(superposition,[],[f134,f118])).
% 127.53/18.29 tff(f1770,plain,(
% 127.53/18.29 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($uminus($sum(X0,$sum(X1,X2))) = $sum($uminus(X2),$uminus($sum(X0,X1)))) )),
% 127.53/18.29 inference(forward_demodulation,[],[f1709,f6])).
% 127.53/18.29 tff(f2128,plain,(
% 127.53/18.29 ( ! [X0 : $int] : ($sum($product(2,$sum(X0,sK0)),sK1) = $sum($product(2,X0),10)) )),
% 127.53/18.29 inference(superposition,[],[f175,f30])).
% 127.53/18.29 tff(f2179,plain,(
% 127.53/18.29 ( ! [X0 : $int] : ($sum(10,$product(2,X0)) = $sum($product(2,$sum(X0,sK0)),sK1)) )),
% 127.53/18.29 inference(forward_demodulation,[],[f2128,f3])).
% 127.53/18.29 tff(f2355,plain,(
% 127.53/18.29 $sum(sK1,0) = $sum(10,$sum(-10,sK1))),
% 127.53/18.29 inference(superposition,[],[f120,f570])).
% 127.53/18.29 tff(f2388,plain,(
% 127.53/18.29 sK1 = $sum(10,$sum(-10,sK1))),
% 127.53/18.29 inference(evaluation,[],[f2355])).
% 127.53/18.29 tff(f2440,plain,(
% 127.53/18.29 ~$less(sK0,$sum(1,10)) | ~spl3_6),
% 127.53/18.29 inference(resolution,[],[f1311,f52])).
% 127.53/18.29 tff(f2451,plain,(
% 127.53/18.29 ~$less(sK0,11) | ~spl3_6),
% 127.53/18.29 inference(evaluation,[],[f2440])).
% 127.53/18.29 tff(f3050,plain,(
% 127.53/18.29 ( ! [X0 : $int] : ($less(10,$sum(1,$sum(sK1,X0))) | $less(X0,$product(2,sK0))) )),
% 127.53/18.29 inference(forward_demodulation,[],[f110,f123])).
% 127.53/18.29 tff(f3213,plain,(
% 127.53/18.29 ( ! [X0 : $int] : ($product(2,sK0) = $sum(X0,$sum($uminus($sum(sK1,X0)),10))) )),
% 127.53/18.29 inference(superposition,[],[f123,f537])).
% 127.53/18.29 tff(f3235,plain,(
% 127.53/18.29 ( ! [X0 : $int] : ($product(2,sK0) = $sum(X0,$sum(10,$uminus($sum(sK1,X0))))) )),
% 127.53/18.29 inference(forward_demodulation,[],[f3213,f3])).
% 127.53/18.29 tff(f3453,definition,(
% 127.53/18.29 spl3_31 <=> $less(0,sK0)),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_31])],[avatar_definition])).
% 127.53/18.29 tff(f3455,plain,(
% 127.53/18.29 $less(0,sK0) | ~spl3_31),
% 127.53/18.29 inference(avatar_component_clause,[],[f3453])).
% 127.53/18.29 tff(f3481,definition,(
% 127.53/18.29 spl3_36 <=> $less(1,sK0)),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_36])],[avatar_definition])).
% 127.53/18.29 tff(f3487,definition,(
% 127.53/18.29 spl3_37 <=> $less(2,sK0)),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_37])],[avatar_definition])).
% 127.53/18.29 tff(f3489,plain,(
% 127.53/18.29 $less(2,sK0) | ~spl3_37),
% 127.53/18.29 inference(avatar_component_clause,[],[f3487])).
% 127.53/18.29 tff(f3532,definition,(
% 127.53/18.29 spl3_39 <=> $less(-1,sK0)),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_39])],[avatar_definition])).
% 127.53/18.29 tff(f3536,definition,(
% 127.53/18.29 spl3_40 <=> $less(10,$product(2,sK1))),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_40])],[avatar_definition])).
% 127.53/18.29 tff(f3537,plain,(
% 127.53/18.29 ~$less(10,$product(2,sK1)) | spl3_40),
% 127.53/18.29 inference(avatar_component_clause,[],[f3536])).
% 127.53/18.29 tff(f3538,plain,(
% 127.53/18.29 $less(10,$product(2,sK1)) | ~spl3_40),
% 127.53/18.29 inference(avatar_component_clause,[],[f3536])).
% 127.53/18.29 tff(f3616,definition,(
% 127.53/18.29 spl3_41 <=> sK0 = -10),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_41])],[avatar_definition])).
% 127.53/18.29 tff(f3617,plain,(
% 127.53/18.29 sK0 != -10 | spl3_41),
% 127.53/18.29 inference(avatar_component_clause,[],[f3616])).
% 127.53/18.29 tff(f3618,plain,(
% 127.53/18.29 sK0 = -10 | ~spl3_41),
% 127.53/18.29 inference(avatar_component_clause,[],[f3616])).
% 127.53/18.29 tff(f3635,definition,(
% 127.53/18.29 spl3_45 <=> 2 = sK0),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_45])],[avatar_definition])).
% 127.53/18.29 tff(f3636,plain,(
% 127.53/18.29 2 != sK0 | spl3_45),
% 127.53/18.29 inference(avatar_component_clause,[],[f3635])).
% 127.53/18.29 tff(f3637,plain,(
% 127.53/18.29 2 = sK0 | ~spl3_45),
% 127.53/18.29 inference(avatar_component_clause,[],[f3635])).
% 127.53/18.29 tff(f3669,definition,(
% 127.53/18.29 spl3_47 <=> 1 = sK0),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_47])],[avatar_definition])).
% 127.53/18.29 tff(f3671,plain,(
% 127.53/18.29 1 = sK0 | ~spl3_47),
% 127.53/18.29 inference(avatar_component_clause,[],[f3669])).
% 127.53/18.29 tff(f3675,plain,(
% 127.53/18.29 ~$less(sK0,$sum(1,2)) | ~spl3_37),
% 127.53/18.29 inference(resolution,[],[f3489,f52])).
% 127.53/18.29 tff(f3686,plain,(
% 127.53/18.29 ~$less(sK0,3) | ~spl3_37),
% 127.53/18.29 inference(evaluation,[],[f3675])).
% 127.53/18.29 tff(f3689,definition,(
% 127.53/18.29 spl3_48 <=> $less(3,sK0)),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_48])],[avatar_definition])).
% 127.53/18.29 tff(f3691,plain,(
% 127.53/18.29 $less(3,sK0) | ~spl3_48),
% 127.53/18.29 inference(avatar_component_clause,[],[f3689])).
% 127.53/18.29 tff(f3693,definition,(
% 127.53/18.29 spl3_49 <=> sK0 = 3),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_49])],[avatar_definition])).
% 127.53/18.29 tff(f3695,plain,(
% 127.53/18.29 sK0 = 3 | ~spl3_49),
% 127.53/18.29 inference(avatar_component_clause,[],[f3693])).
% 127.53/18.29 tff(f3733,definition,(
% 127.53/18.29 spl3_52 <=> $less(sK0,2)),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_52])],[avatar_definition])).
% 127.53/18.29 tff(f3735,plain,(
% 127.53/18.29 $less(sK0,2) | ~spl3_52),
% 127.53/18.29 inference(avatar_component_clause,[],[f3733])).
% 127.53/18.29 tff(f3751,plain,(
% 127.53/18.29 $sum(10,$product(2,$product(2,sK0))) = $sum(sK0,$product(2,10))),
% 127.53/18.29 inference(superposition,[],[f220,f32])).
% 127.53/18.29 tff(f3780,plain,(
% 127.53/18.29 $sum(10,$product(2,$product(2,sK0))) = $sum(sK0,20)),
% 127.53/18.29 inference(evaluation,[],[f3751])).
% 127.53/18.29 tff(f3783,plain,(
% 127.53/18.29 $sum(10,$product(2,$product(2,sK0))) = $sum(20,sK0)),
% 127.53/18.29 inference(forward_demodulation,[],[f3780,f3])).
% 127.53/18.29 tff(f3895,plain,(
% 127.53/18.29 $sum(10,$product(2,$uminus(sK0))) = $sum($product(2,0),sK1)),
% 127.53/18.29 inference(superposition,[],[f2179,f31])).
% 127.53/18.29 tff(f3914,plain,(
% 127.53/18.29 sK1 = $sum(10,$product(2,$uminus(sK0)))),
% 127.53/18.29 inference(evaluation,[],[f3895])).
% 127.53/18.29 tff(f4075,plain,(
% 127.53/18.29 ( ! [X0 : $int] : (0 = $sum($product(2,2),$sum(sK1,$sum(X0,$uminus($sum(10,X0)))))) ) | ~spl3_45),
% 127.53/18.29 inference(forward_demodulation,[],[f571,f3637])).
% 127.53/18.29 tff(f4358,definition,(
% 127.53/18.29 spl3_56 <=> 0 = sK0),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_56])],[avatar_definition])).
% 127.53/18.29 tff(f4359,plain,(
% 127.53/18.29 0 != sK0 | spl3_56),
% 127.53/18.29 inference(avatar_component_clause,[],[f4358])).
% 127.53/18.29 tff(f4360,plain,(
% 127.53/18.29 0 = sK0 | ~spl3_56),
% 127.53/18.29 inference(avatar_component_clause,[],[f4358])).
% 127.53/18.29 tff(f4676,definition,(
% 127.53/18.29 spl3_60 <=> sK0 = $product(2,sK0)),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_60])],[avatar_definition])).
% 127.53/18.29 tff(f4677,plain,(
% 127.53/18.29 sK0 != $product(2,sK0) | spl3_60),
% 127.53/18.29 inference(avatar_component_clause,[],[f4676])).
% 127.53/18.29 tff(f4678,plain,(
% 127.53/18.29 sK0 = $product(2,sK0) | ~spl3_60),
% 127.53/18.29 inference(avatar_component_clause,[],[f4676])).
% 127.53/18.29 tff(f4715,definition,(
% 127.53/18.29 spl3_64 <=> $less($product(2,sK0),11)),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_64])],[avatar_definition])).
% 127.53/18.29 tff(f6370,definition,(
% 127.53/18.29 spl3_71 <=> $less($product(2,sK0),sK0)),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_71])],[avatar_definition])).
% 127.53/18.29 tff(f6371,plain,(
% 127.53/18.29 ~$less($product(2,sK0),sK0) | spl3_71),
% 127.53/18.29 inference(avatar_component_clause,[],[f6370])).
% 127.53/18.29 tff(f6372,plain,(
% 127.53/18.29 $less($product(2,sK0),sK0) | ~spl3_71),
% 127.53/18.29 inference(avatar_component_clause,[],[f6370])).
% 127.53/18.29 tff(f6894,plain,(
% 127.53/18.29 $less(-1,sK1) | $less(10,$sum(0,$product(2,sK0)))),
% 127.53/18.29 inference(resolution,[],[f247,f92])).
% 127.53/18.29 tff(f6909,plain,(
% 127.53/18.29 $less(-1,sK1) | $less(10,$product(2,sK0))),
% 127.53/18.29 inference(evaluation,[],[f6894])).
% 127.53/18.29 tff(f6922,plain,(
% 127.53/18.29 $less(-1,sK1) | spl3_8),
% 127.53/18.29 inference(forward_subsumption_resolution,[],[f6909,f1319])).
% 127.53/18.29 tff(f7044,definition,(
% 127.53/18.29 spl3_76 <=> $less(10,$sum(1,$product(2,sK0)))),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_76])],[avatar_definition])).
% 127.53/18.29 tff(f7046,plain,(
% 127.53/18.29 $less(10,$sum(1,$product(2,sK0))) | ~spl3_76),
% 127.53/18.29 inference(avatar_component_clause,[],[f7044])).
% 127.53/18.29 tff(f7200,plain,(
% 127.53/18.29 $sum(10,sK1) = $sum($product(2,sK0),$product(sK1,2))),
% 127.53/18.29 inference(superposition,[],[f116,f973])).
% 127.53/18.29 tff(f7201,plain,(
% 127.53/18.29 $sum(10,$product(2,sK1)) = $sum(sK0,$product(2,$product(sK1,2)))),
% 127.53/18.29 inference(superposition,[],[f220,f973])).
% 127.53/18.29 tff(f7234,plain,(
% 127.53/18.29 $sum(10,$product(2,sK1)) = $sum(sK0,$product(2,$product(2,sK1)))),
% 127.53/18.29 inference(forward_demodulation,[],[f7201,f145])).
% 127.53/18.29 tff(f7235,plain,(
% 127.53/18.29 $sum(10,sK1) = $sum($product(2,sK0),$product(2,sK1))),
% 127.53/18.29 inference(forward_demodulation,[],[f7200,f14])).
% 127.53/18.29 tff(f7378,definition,(
% 127.53/18.29 spl3_87 <=> $less(sK0,$product(2,sK1))),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_87])],[avatar_definition])).
% 127.53/18.29 tff(f7380,plain,(
% 127.53/18.29 $less(sK0,$product(2,sK1)) | ~spl3_87),
% 127.53/18.29 inference(avatar_component_clause,[],[f7378])).
% 127.53/18.29 tff(f8167,plain,(
% 127.53/18.29 sK1 = $sum(-1,1) | $less($sum(-1,1),sK1) | spl3_8),
% 127.53/18.29 inference(resolution,[],[f6922,f59])).
% 127.53/18.29 tff(f8179,definition,(
% 127.53/18.29 spl3_89 <=> 0 = sK1),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_89])],[avatar_definition])).
% 127.53/18.29 tff(f8180,plain,(
% 127.53/18.29 0 != sK1 | spl3_89),
% 127.53/18.29 inference(avatar_component_clause,[],[f8179])).
% 127.53/18.29 tff(f8181,plain,(
% 127.53/18.29 0 = sK1 | ~spl3_89),
% 127.53/18.29 inference(avatar_component_clause,[],[f8179])).
% 127.53/18.29 tff(f9331,definition,(
% 127.53/18.29 spl3_90 <=> $less(1,sK1)),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_90])],[avatar_definition])).
% 127.53/18.29 tff(f9332,plain,(
% 127.53/18.29 ~$less(1,sK1) | spl3_90),
% 127.53/18.29 inference(avatar_component_clause,[],[f9331])).
% 127.53/18.29 tff(f9333,plain,(
% 127.53/18.29 $less(1,sK1) | ~spl3_90),
% 127.53/18.29 inference(avatar_component_clause,[],[f9331])).
% 127.53/18.29 tff(f9339,plain,(
% 127.53/18.29 ~$less($product(2,sK0),11) | ~spl3_8),
% 127.53/18.29 inference(evaluation,[],[f1381])).
% 127.53/18.29 tff(f9342,plain,(
% 127.53/18.29 ~spl3_64 | ~spl3_8),
% 127.53/18.29 inference(avatar_split_clause,[],[f9339,f1318,f4715])).
% 127.53/18.29 tff(f9345,plain,(
% 127.53/18.29 $less(sK1,0) | ~spl3_8),
% 127.53/18.29 inference(forward_demodulation,[],[f1393,f2388])).
% 127.53/18.29 tff(f9352,definition,(
% 127.53/18.29 spl3_93 <=> $less(-1,sK1)),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_93])],[avatar_definition])).
% 127.53/18.29 tff(f9353,plain,(
% 127.53/18.29 ~$less(-1,sK1) | spl3_93),
% 127.53/18.29 inference(avatar_component_clause,[],[f9352])).
% 127.53/18.29 tff(f11071,plain,(
% 127.53/18.29 ~$less(sK0,$sum(1,3)) | ~spl3_48),
% 127.53/18.29 inference(resolution,[],[f3691,f52])).
% 127.53/18.29 tff(f11082,plain,(
% 127.53/18.29 ~$less(sK0,4) | ~spl3_48),
% 127.53/18.29 inference(evaluation,[],[f11071])).
% 127.53/18.29 tff(f11085,definition,(
% 127.53/18.29 spl3_94 <=> $less(4,sK0)),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_94])],[avatar_definition])).
% 127.53/18.29 tff(f11087,plain,(
% 127.53/18.29 $less(4,sK0) | ~spl3_94),
% 127.53/18.29 inference(avatar_component_clause,[],[f11085])).
% 127.53/18.29 tff(f11089,definition,(
% 127.53/18.29 spl3_95 <=> sK0 = 4),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_95])],[avatar_definition])).
% 127.53/18.29 tff(f11091,plain,(
% 127.53/18.29 sK0 = 4 | ~spl3_95),
% 127.53/18.29 inference(avatar_component_clause,[],[f11089])).
% 127.53/18.29 tff(f12017,plain,(
% 127.53/18.29 10 = $sum($product(2,0),sK1) | ~spl3_56),
% 127.53/18.29 inference(superposition,[],[f30,f4360])).
% 127.53/18.29 tff(f12135,plain,(
% 127.53/18.29 10 = sK1 | ~spl3_56),
% 127.53/18.29 inference(evaluation,[],[f12017])).
% 127.53/18.29 tff(f12992,plain,(
% 127.53/18.29 ~$less(-1,sK1) | ~spl3_8),
% 127.53/18.29 inference(resolution,[],[f9345,f248])).
% 127.53/18.29 tff(f13015,plain,(
% 127.53/18.29 ~spl3_93 | ~spl3_8),
% 127.53/18.29 inference(avatar_split_clause,[],[f12992,f1318,f9352])).
% 127.53/18.29 tff(f15196,plain,(
% 127.53/18.29 10 = $sum(sK0,$product(2,0)) | ~spl3_89),
% 127.53/18.29 inference(superposition,[],[f29,f8181])).
% 127.53/18.29 tff(f16391,plain,(
% 127.53/18.29 sK1 = $sum(1,1) | $less($sum(1,1),sK1) | ~spl3_90),
% 127.53/18.29 inference(resolution,[],[f9333,f59])).
% 127.53/18.29 tff(f16408,definition,(
% 127.53/18.29 spl3_100 <=> $less(2,sK1)),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_100])],[avatar_definition])).
% 127.53/18.29 tff(f16410,plain,(
% 127.53/18.29 $less(2,sK1) | ~spl3_100),
% 127.53/18.29 inference(avatar_component_clause,[],[f16408])).
% 127.53/18.29 tff(f16412,definition,(
% 127.53/18.29 spl3_101 <=> 2 = sK1),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_101])],[avatar_definition])).
% 127.53/18.29 tff(f16413,plain,(
% 127.53/18.29 2 != sK1 | spl3_101),
% 127.53/18.29 inference(avatar_component_clause,[],[f16412])).
% 127.53/18.29 tff(f16414,plain,(
% 127.53/18.29 2 = sK1 | ~spl3_101),
% 127.53/18.29 inference(avatar_component_clause,[],[f16412])).
% 127.53/18.29 tff(f18487,plain,(
% 127.53/18.29 $less($product(2,$sum(sK1,1)),10) | $less(sK0,2) | 2 = sK0),
% 127.53/18.29 inference(superposition,[],[f197,f988])).
% 127.53/18.29 tff(f19061,definition,(
% 127.53/18.29 spl3_104 <=> 10 = sK1),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_104])],[avatar_definition])).
% 127.53/18.29 tff(f19062,plain,(
% 127.53/18.29 10 != sK1 | spl3_104),
% 127.53/18.29 inference(avatar_component_clause,[],[f19061])).
% 127.53/18.29 tff(f19063,plain,(
% 127.53/18.29 10 = sK1 | ~spl3_104),
% 127.53/18.29 inference(avatar_component_clause,[],[f19061])).
% 127.53/18.29 tff(f19090,definition,(
% 127.53/18.29 spl3_108 <=> sK0 = sK1),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_108])],[avatar_definition])).
% 127.53/18.29 tff(f19091,plain,(
% 127.53/18.29 sK0 != sK1 | spl3_108),
% 127.53/18.29 inference(avatar_component_clause,[],[f19090])).
% 127.53/18.29 tff(f19092,plain,(
% 127.53/18.29 sK0 = sK1 | ~spl3_108),
% 127.53/18.29 inference(avatar_component_clause,[],[f19090])).
% 127.53/18.29 tff(f20466,plain,(
% 127.53/18.29 $less(10,sK0) | (~spl3_4 | ~spl3_108)),
% 127.53/18.29 inference(superposition,[],[f1302,f19092])).
% 127.53/18.29 tff(f20484,plain,(
% 127.53/18.29 ~$less(1,sK0) | (spl3_90 | ~spl3_108)),
% 127.53/18.29 inference(superposition,[],[f9332,f19092])).
% 127.53/18.29 tff(f20485,plain,(
% 127.53/18.29 ~$less(-1,sK0) | (spl3_93 | ~spl3_108)),
% 127.53/18.29 inference(superposition,[],[f9353,f19092])).
% 127.53/18.29 tff(f20538,plain,(
% 127.53/18.29 ~spl3_39 | spl3_93 | ~spl3_108),
% 127.53/18.29 inference(avatar_split_clause,[],[f20485,f19090,f9352,f3532])).
% 127.53/18.29 tff(f20540,plain,(
% 127.53/18.29 ~spl3_36 | spl3_90 | ~spl3_108),
% 127.53/18.29 inference(avatar_split_clause,[],[f20484,f19090,f9331,f3481])).
% 127.53/18.29 tff(f20544,plain,(
% 127.53/18.29 spl3_6 | ~spl3_4 | ~spl3_108),
% 127.53/18.29 inference(avatar_split_clause,[],[f20466,f19090,f1300,f1309])).
% 127.53/18.29 tff(f20559,definition,(
% 127.53/18.29 spl3_116 <=> 10 = $product(2,sK0)),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_116])],[avatar_definition])).
% 127.53/18.29 tff(f20561,plain,(
% 127.53/18.29 10 = $product(2,sK0) | ~spl3_116),
% 127.53/18.29 inference(avatar_component_clause,[],[f20559])).
% 127.53/18.29 tff(f20623,plain,(
% 127.53/18.29 0 = sK1 | $less(0,sK1) | spl3_8),
% 127.53/18.29 inference(evaluation,[],[f8167])).
% 127.53/18.29 tff(f21028,plain,(
% 127.53/18.29 0 = sK0 | $less(0,sK1) | (spl3_8 | ~spl3_108)),
% 127.53/18.29 inference(forward_demodulation,[],[f20623,f19092])).
% 127.53/18.29 tff(f22156,plain,(
% 127.53/18.29 $less(2,sK0) | (~spl3_100 | ~spl3_108)),
% 127.53/18.29 inference(forward_demodulation,[],[f16410,f19092])).
% 127.53/18.29 tff(f22157,plain,(
% 127.53/18.29 $less($product(2,$sum(sK1,1)),10) | $less(sK0,2) | spl3_45),
% 127.53/18.29 inference(forward_subsumption_resolution,[],[f18487,f3636])).
% 127.53/18.29 tff(f22162,plain,(
% 127.53/18.29 $less(0,sK1) | (spl3_8 | spl3_56 | ~spl3_108)),
% 127.53/18.29 inference(forward_subsumption_resolution,[],[f21028,f4359])).
% 127.53/18.29 tff(f22261,plain,(
% 127.53/18.29 spl3_37 | ~spl3_100 | ~spl3_108),
% 127.53/18.29 inference(avatar_split_clause,[],[f22156,f19090,f16408,f3487])).
% 127.53/18.29 tff(f22262,plain,(
% 127.53/18.29 $less($product(2,$sum(1,sK1)),10) | $less(sK0,2) | spl3_45),
% 127.53/18.29 inference(forward_demodulation,[],[f22157,f1557])).
% 127.53/18.29 tff(f22270,plain,(
% 127.53/18.29 $less(0,sK0) | (spl3_8 | spl3_56 | ~spl3_108)),
% 127.53/18.29 inference(forward_demodulation,[],[f22162,f19092])).
% 127.53/18.29 tff(f22320,plain,(
% 127.53/18.29 $less($product(2,$sum(1,sK0)),10) | $less(sK0,2) | (spl3_45 | ~spl3_108)),
% 127.53/18.29 inference(forward_demodulation,[],[f22262,f19092])).
% 127.53/18.29 tff(f22323,plain,(
% 127.53/18.29 spl3_31 | spl3_8 | spl3_56 | ~spl3_108),
% 127.53/18.29 inference(avatar_split_clause,[],[f22270,f19090,f4358,f1318,f3453])).
% 127.53/18.29 tff(f22335,definition,(
% 127.53/18.29 spl3_120 <=> $less($product(2,$sum(1,sK0)),10)),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_120])],[avatar_definition])).
% 127.53/18.29 tff(f22337,plain,(
% 127.53/18.29 $less($product(2,$sum(1,sK0)),10) | ~spl3_120),
% 127.53/18.29 inference(avatar_component_clause,[],[f22335])).
% 127.53/18.29 tff(f22338,plain,(
% 127.53/18.29 spl3_52 | spl3_120 | spl3_45 | ~spl3_108),
% 127.53/18.29 inference(avatar_split_clause,[],[f22320,f19090,f3635,f22335,f3733])).
% 127.53/18.29 tff(f22393,plain,(
% 127.53/18.29 ( ! [X0 : $int] : (0 = $sum(4,$sum(sK1,$sum(X0,$uminus($sum(10,X0)))))) ) | ~spl3_45),
% 127.53/18.29 inference(evaluation,[],[f4075])).
% 127.53/18.29 tff(f22463,plain,(
% 127.53/18.29 0 = $sum(4,$sum(sK1,$uminus(10))) | ~spl3_45),
% 127.53/18.29 inference(forward_demodulation,[],[f22393,f287])).
% 127.53/18.29 tff(f22464,plain,(
% 127.53/18.29 0 = $sum(4,$sum(sK1,-10)) | ~spl3_45),
% 127.53/18.29 inference(evaluation,[],[f22463])).
% 127.53/18.29 tff(f22582,plain,(
% 127.53/18.29 0 = $sum(4,$sum(-10,sK1)) | ~spl3_45),
% 127.53/18.29 inference(forward_demodulation,[],[f22464,f3])).
% 127.53/18.29 tff(f22901,definition,(
% 127.53/18.29 spl3_124 <=> sK1 = 4),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_124])],[avatar_definition])).
% 127.53/18.29 tff(f22902,plain,(
% 127.53/18.29 sK1 != 4 | spl3_124),
% 127.53/18.29 inference(avatar_component_clause,[],[f22901])).
% 127.53/18.29 tff(f22903,plain,(
% 127.53/18.29 sK1 = 4 | ~spl3_124),
% 127.53/18.29 inference(avatar_component_clause,[],[f22901])).
% 127.53/18.29 tff(f23028,plain,(
% 127.53/18.29 $less(10,2) | (~spl3_6 | ~spl3_45)),
% 127.53/18.29 inference(superposition,[],[f1311,f3637])).
% 127.53/18.29 tff(f23046,plain,(
% 127.53/18.29 $false | (~spl3_6 | ~spl3_45)),
% 127.53/18.29 inference(evaluation,[],[f23028])).
% 127.53/18.29 tff(f23047,plain,(
% 127.53/18.29 ~spl3_6 | ~spl3_45),
% 127.53/18.29 inference(avatar_contradiction_clause,[],[f23046])).
% 127.53/18.29 tff(f23405,plain,(
% 127.53/18.29 ( ! [X0 : $int] : (sK0 = $sum(X0,$sum($uminus($sum(X0,$product(2,sK1))),10))) )),
% 127.53/18.29 inference(superposition,[],[f294,f701])).
% 127.53/18.29 tff(f23708,plain,(
% 127.53/18.29 ( ! [X0 : $int] : (sK0 = $sum(X0,$sum(10,$uminus($sum(X0,$product(2,sK1)))))) )),
% 127.53/18.29 inference(forward_demodulation,[],[f23405,f3])).
% 127.53/18.29 tff(f24066,definition,(
% 127.53/18.29 spl3_127 <=> $less(sK0,0)),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_127])],[avatar_definition])).
% 127.53/18.29 tff(f24067,plain,(
% 127.53/18.29 ~$less(sK0,0) | spl3_127),
% 127.53/18.29 inference(avatar_component_clause,[],[f24066])).
% 127.53/18.29 tff(f24068,plain,(
% 127.53/18.29 $less(sK0,0) | ~spl3_127),
% 127.53/18.29 inference(avatar_component_clause,[],[f24066])).
% 127.53/18.29 tff(f24190,plain,(
% 127.53/18.29 ( ! [X0 : $int] : ($less(10,$sum(1,$sum(X0,sK0))) | $less(X0,$product(2,sK1))) )),
% 127.53/18.29 inference(superposition,[],[f464,f29])).
% 127.53/18.29 tff(f24256,plain,(
% 127.53/18.29 ( ! [X0 : $int] : ($less($sum(sK1,X0),$sum(1,10)) | $less($product(2,sK0),X0)) )),
% 127.53/18.29 inference(superposition,[],[f464,f30])).
% 127.53/18.29 tff(f24324,plain,(
% 127.53/18.29 ( ! [X0 : $int] : ($less($sum(sK1,X0),11) | $less($product(2,sK0),X0)) )),
% 127.53/18.29 inference(evaluation,[],[f24256])).
% 127.53/18.29 tff(f25942,plain,(
% 127.53/18.29 ( ! [X0 : $int] : ($product(2,sK1) = $sum(X0,$sum(10,$uminus($sum(sK0,X0))))) )),
% 127.53/18.29 inference(superposition,[],[f619,f223])).
% 127.53/18.29 tff(f29387,plain,(
% 127.53/18.29 ( ! [X0 : $int,X1 : $int] : (~$less(X1,$sum(10,$sum(1,X0))) | ~$less($sum(sK0,$sum(X0,$product(2,sK1))),X1)) )),
% 127.53/18.29 inference(superposition,[],[f1107,f726])).
% 127.53/18.29 tff(f29415,plain,(
% 127.53/18.29 ( ! [X0 : $int,X1 : $int] : (~$less(X1,$sum(1,$sum(X0,10))) | ~$less($sum(sK0,$sum(X0,$product(2,sK1))),X1)) )),
% 127.53/18.29 inference(forward_demodulation,[],[f29387,f123])).
% 127.53/18.29 tff(f29456,plain,(
% 127.53/18.29 ( ! [X0 : $int,X1 : $int] : (~$less(X1,$sum(1,$sum(X0,10))) | ~$less($sum(10,X0),X1)) )),
% 127.53/18.29 inference(forward_demodulation,[],[f29415,f223])).
% 127.53/18.29 tff(f36072,plain,(
% 127.53/18.29 $less($sum(2,$product(2,sK0)),10) | ~spl3_100),
% 127.53/18.29 inference(resolution,[],[f16410,f100])).
% 127.53/18.29 tff(f36104,plain,(
% 127.53/18.29 $less($product(2,$sum(1,sK0)),10) | ~spl3_100),
% 127.53/18.29 inference(forward_demodulation,[],[f36072,f163])).
% 127.53/18.29 tff(f36312,plain,(
% 127.53/18.29 ( ! [X0 : $int] : ($sum($uminus(X0),$product(2,sK1)) = $sum(10,$uminus($sum(X0,sK0)))) )),
% 127.53/18.29 inference(superposition,[],[f1730,f223])).
% 127.53/18.29 tff(f46462,plain,(
% 127.53/18.29 ( ! [X0 : $int] : (sK0 = $sum(10,$sum(X0,$uminus($sum($product(2,4),X0))))) ) | ~spl3_124),
% 127.53/18.29 inference(superposition,[],[f540,f22903])).
% 127.53/18.29 tff(f46521,plain,(
% 127.53/18.29 0 = $sum(4,$sum(-10,4)) | (~spl3_45 | ~spl3_124)),
% 127.53/18.29 inference(superposition,[],[f22582,f22903])).
% 127.53/18.29 tff(f46529,plain,(
% 127.53/18.29 $false | (~spl3_45 | ~spl3_124)),
% 127.53/18.29 inference(evaluation,[],[f46521])).
% 127.53/18.29 tff(f46530,plain,(
% 127.53/18.29 ~spl3_45 | ~spl3_124),
% 127.53/18.29 inference(avatar_contradiction_clause,[],[f46529])).
% 127.53/18.29 tff(f49728,plain,(
% 127.53/18.29 spl3_120 | ~spl3_100),
% 127.53/18.29 inference(avatar_split_clause,[],[f36104,f16408,f22335])).
% 127.53/18.29 tff(f52877,plain,(
% 127.53/18.29 ( ! [X0 : $int,X1 : $int] : ($sum(10,$sum($uminus(X0),$uminus(X1))) = $sum($product(2,sK0),$sum(sK1,$uminus($sum(X0,X1))))) )),
% 127.53/18.29 inference(superposition,[],[f735,f667])).
% 127.53/18.29 tff(f53022,plain,(
% 127.53/18.29 ( ! [X0 : $int,X1 : $int] : ($sum(10,$uminus($sum(X0,X1))) = $sum(10,$sum($uminus(X0),$uminus(X1)))) )),
% 127.53/18.29 inference(forward_demodulation,[],[f52877,f116])).
% 127.53/18.29 tff(f53185,plain,(
% 127.53/18.29 ( ! [X0 : $int,X1 : $int] : ($sum(10,$uminus($sum(X0,X1))) = $sum(10,$uminus($sum(X1,X0)))) )),
% 127.53/18.29 inference(forward_demodulation,[],[f53022,f6])).
% 127.53/18.29 tff(f54513,plain,(
% 127.53/18.29 $less(-1,sK0) | spl3_127),
% 127.53/18.29 inference(resolution,[],[f24067,f247])).
% 127.53/18.29 tff(f60868,plain,(
% 127.53/18.29 ( ! [X0 : $int] : ($uminus($sum(sK1,$sum($product(2,sK0),X0))) = $sum($uminus(X0),$uminus(10))) )),
% 127.53/18.29 inference(superposition,[],[f1770,f32])).
% 127.53/18.29 tff(f61056,plain,(
% 127.53/18.29 ( ! [X0 : $int] : ($uminus($sum(sK1,$sum($product(2,sK0),X0))) = $sum($uminus(X0),-10)) )),
% 127.53/18.29 inference(evaluation,[],[f60868])).
% 127.53/18.29 tff(f61186,plain,(
% 127.53/18.29 ( ! [X0 : $int] : ($uminus($sum(sK1,$sum($product(2,sK0),X0))) = $sum(-10,$uminus(X0))) )),
% 127.53/18.29 inference(forward_demodulation,[],[f61056,f3])).
% 127.53/18.29 tff(f61366,plain,(
% 127.53/18.29 ( ! [X0 : $int] : ($uminus($sum(10,X0)) = $sum(-10,$uminus(X0))) )),
% 127.53/18.29 inference(forward_demodulation,[],[f61186,f120])).
% 127.53/18.29 tff(f81592,plain,(
% 127.53/18.29 ( ! [X0 : $int] : (0 = $sum(sK1,$sum($uminus($sum(10,X0)),$sum(X0,$product(2,sK0))))) )),
% 127.53/18.29 inference(superposition,[],[f571,f694])).
% 127.53/18.29 tff(f81854,plain,(
% 127.53/18.29 ( ! [X0 : $int] : (0 = $sum(sK1,$sum(X0,$sum($product(2,sK0),$uminus($sum(10,X0)))))) )),
% 127.53/18.29 inference(forward_demodulation,[],[f81592,f123])).
% 127.53/18.29 tff(f82623,plain,(
% 127.53/18.29 ( ! [X0 : $int] : (0 = $sum(sK1,$sum(X0,$sum($product(2,4),$uminus($sum(10,X0)))))) ) | ~spl3_95),
% 127.53/18.29 inference(forward_demodulation,[],[f81854,f11091])).
% 127.53/18.29 tff(f96500,plain,(
% 127.53/18.29 ~$less(sK0,$sum(1,4)) | ~spl3_94),
% 127.53/18.29 inference(resolution,[],[f11087,f52])).
% 127.53/18.29 tff(f96524,plain,(
% 127.53/18.29 ~$less(sK0,5) | ~spl3_94),
% 127.53/18.29 inference(evaluation,[],[f96500])).
% 127.53/18.29 tff(f96529,definition,(
% 127.53/18.29 spl3_152 <=> $less(5,sK0)),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_152])],[avatar_definition])).
% 127.53/18.29 tff(f96531,plain,(
% 127.53/18.29 $less(5,sK0) | ~spl3_152),
% 127.53/18.29 inference(avatar_component_clause,[],[f96529])).
% 127.53/18.29 tff(f96533,definition,(
% 127.53/18.29 spl3_153 <=> sK0 = 5),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_153])],[avatar_definition])).
% 127.53/18.29 tff(f96535,plain,(
% 127.53/18.29 sK0 = 5 | ~spl3_153),
% 127.53/18.29 inference(avatar_component_clause,[],[f96533])).
% 127.53/18.29 tff(f108736,plain,(
% 127.53/18.29 $less(10,$sum(11,$product(2,-10))) | (~spl3_3 | ~spl3_41)),
% 127.53/18.29 inference(superposition,[],[f1298,f3618])).
% 127.53/18.29 tff(f108789,plain,(
% 127.53/18.29 $false | (~spl3_3 | ~spl3_41)),
% 127.53/18.29 inference(evaluation,[],[f108736])).
% 127.53/18.29 tff(f108790,plain,(
% 127.53/18.29 ~spl3_3 | ~spl3_41),
% 127.53/18.29 inference(avatar_contradiction_clause,[],[f108789])).
% 127.53/18.29 tff(f117242,plain,(
% 127.53/18.29 0 = $sum(sK1,$sum(-10,$product(2,5))) | ~spl3_153),
% 127.53/18.29 inference(superposition,[],[f565,f96535])).
% 127.53/18.29 tff(f119849,plain,(
% 127.53/18.29 ~$less(sK0,$sum(1,5)) | ~spl3_152),
% 127.53/18.29 inference(resolution,[],[f96531,f52])).
% 127.53/18.29 tff(f119874,plain,(
% 127.53/18.29 ~$less(sK0,6) | ~spl3_152),
% 127.53/18.29 inference(evaluation,[],[f119849])).
% 127.53/18.29 tff(f119880,definition,(
% 127.53/18.29 spl3_162 <=> $less(6,sK0)),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_162])],[avatar_definition])).
% 127.53/18.29 tff(f119882,plain,(
% 127.53/18.29 $less(6,sK0) | ~spl3_162),
% 127.53/18.29 inference(avatar_component_clause,[],[f119880])).
% 127.53/18.29 tff(f119884,definition,(
% 127.53/18.29 spl3_163 <=> sK0 = 6),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_163])],[avatar_definition])).
% 127.53/18.29 tff(f119885,plain,(
% 127.53/18.29 sK0 != 6 | spl3_163),
% 127.53/18.29 inference(avatar_component_clause,[],[f119884])).
% 127.53/18.29 tff(f119886,plain,(
% 127.53/18.29 sK0 = 6 | ~spl3_163),
% 127.53/18.29 inference(avatar_component_clause,[],[f119884])).
% 127.53/18.29 tff(f120237,plain,(
% 127.53/18.29 spl3_39 | spl3_127),
% 127.53/18.29 inference(avatar_split_clause,[],[f54513,f24066,f3532])).
% 127.53/18.29 tff(f123079,plain,(
% 127.53/18.29 ( ! [X0 : $int] : ($sum(sK1,0) = $sum(10,$sum($product(2,X0),$uminus($product(2,$sum(sK0,X0)))))) )),
% 127.53/18.29 inference(superposition,[],[f120,f502])).
% 127.53/18.29 tff(f123347,plain,(
% 127.53/18.29 ( ! [X0 : $int] : (sK1 = $sum(10,$sum($product(2,X0),$uminus($product(2,$sum(sK0,X0)))))) )),
% 127.53/18.29 inference(evaluation,[],[f123079])).
% 127.53/18.29 tff(f151586,plain,(
% 127.53/18.29 ~$less(sK0,$sum(1,6)) | ~spl3_162),
% 127.53/18.29 inference(resolution,[],[f119882,f52])).
% 127.53/18.29 tff(f151611,plain,(
% 127.53/18.29 ~$less(sK0,7) | ~spl3_162),
% 127.53/18.29 inference(evaluation,[],[f151586])).
% 127.53/18.29 tff(f151617,definition,(
% 127.53/18.29 spl3_172 <=> $less(7,sK0)),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_172])],[avatar_definition])).
% 127.53/18.29 tff(f151619,plain,(
% 127.53/18.29 $less(7,sK0) | ~spl3_172),
% 127.53/18.29 inference(avatar_component_clause,[],[f151617])).
% 127.53/18.29 tff(f151621,definition,(
% 127.53/18.29 spl3_173 <=> sK0 = 7),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_173])],[avatar_definition])).
% 127.53/18.29 tff(f151623,plain,(
% 127.53/18.29 sK0 = 7 | ~spl3_173),
% 127.53/18.29 inference(avatar_component_clause,[],[f151621])).
% 127.53/18.29 tff(f199303,plain,(
% 127.53/18.29 ( ! [X0 : $int] : (sK0 = $sum(10,$sum(X0,$uminus($sum($product(2,10),X0))))) ) | ~spl3_104),
% 127.53/18.29 inference(superposition,[],[f540,f19063])).
% 127.53/18.29 tff(f199330,plain,(
% 127.53/18.29 $less(10,10) | (~spl3_4 | ~spl3_104)),
% 127.53/18.29 inference(superposition,[],[f1302,f19063])).
% 127.53/18.29 tff(f199395,plain,(
% 127.53/18.29 $false | (~spl3_4 | ~spl3_104)),
% 127.53/18.29 inference(evaluation,[],[f199330])).
% 127.53/18.29 tff(f199396,plain,(
% 127.53/18.29 ~spl3_4 | ~spl3_104),
% 127.53/18.29 inference(avatar_contradiction_clause,[],[f199395])).
% 127.53/18.29 tff(f199408,plain,(
% 127.53/18.29 ( ! [X0 : $int] : (sK0 = $sum(10,$sum(X0,$uminus($sum(20,X0))))) ) | ~spl3_104),
% 127.53/18.29 inference(evaluation,[],[f199303])).
% 127.53/18.29 tff(f199434,plain,(
% 127.53/18.29 sK0 = $sum(10,$uminus(20)) | ~spl3_104),
% 127.53/18.29 inference(forward_demodulation,[],[f199408,f287])).
% 127.53/18.29 tff(f199435,plain,(
% 127.53/18.29 sK0 = -10 | ~spl3_104),
% 127.53/18.29 inference(evaluation,[],[f199434])).
% 127.53/18.29 tff(f199443,plain,(
% 127.53/18.29 $false | (spl3_41 | ~spl3_104)),
% 127.53/18.29 inference(forward_subsumption_resolution,[],[f199435,f3617])).
% 127.53/18.29 tff(f199444,plain,(
% 127.53/18.29 spl3_41 | ~spl3_104),
% 127.53/18.29 inference(avatar_contradiction_clause,[],[f199443])).
% 127.53/18.29 tff(f277171,plain,(
% 127.53/18.29 $less($sum(10,$uminus($product(2,sK1))),0) | ~spl3_40),
% 127.53/18.29 inference(resolution,[],[f3538,f94])).
% 127.53/18.29 tff(f277197,plain,(
% 127.53/18.29 $less(sK0,0) | ~spl3_40),
% 127.53/18.29 inference(forward_demodulation,[],[f277171,f228])).
% 127.53/18.29 tff(f278072,plain,(
% 127.53/18.29 sK0 != sK0 | 0 = sK0 | 2 = 1 | ~spl3_60),
% 127.53/18.29 inference(superposition,[],[f1031,f4678])).
% 127.53/18.29 tff(f278275,plain,(
% 127.53/18.29 0 = sK0 | 2 = 1 | ~spl3_60),
% 127.53/18.29 inference(trivial_inequality_removal,[],[f278072])).
% 127.53/18.29 tff(f278276,plain,(
% 127.53/18.29 0 = sK0 | ~spl3_60),
% 127.53/18.29 inference(evaluation,[],[f278275])).
% 127.53/18.29 tff(f278510,plain,(
% 127.53/18.29 $false | (~spl3_56 | spl3_104)),
% 127.53/18.29 inference(forward_subsumption_resolution,[],[f12135,f19062])).
% 127.53/18.29 tff(f278511,plain,(
% 127.53/18.29 ~spl3_56 | spl3_104),
% 127.53/18.29 inference(avatar_contradiction_clause,[],[f278510])).
% 127.53/18.29 tff(f278573,plain,(
% 127.53/18.29 spl3_56 | ~spl3_60),
% 127.53/18.29 inference(avatar_split_clause,[],[f278276,f4676,f4358])).
% 127.53/18.29 tff(f282859,plain,(
% 127.53/18.29 $less(10,$product(2,sK0)) | 10 = $product(2,sK0) | ~spl3_76),
% 127.53/18.29 inference(resolution,[],[f7046,f273])).
% 127.53/18.29 tff(f291317,definition,(
% 127.53/18.29 spl3_344 <=> 10 = sK0),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_344])],[avatar_definition])).
% 127.53/18.29 tff(f291319,plain,(
% 127.53/18.29 10 = sK0 | ~spl3_344),
% 127.53/18.29 inference(avatar_component_clause,[],[f291317])).
% 127.53/18.29 tff(f292226,plain,(
% 127.53/18.29 $less($product(2,$sum(1,10)),10) | (~spl3_120 | ~spl3_344)),
% 127.53/18.29 inference(superposition,[],[f22337,f291319])).
% 127.53/18.29 tff(f292249,plain,(
% 127.53/18.29 $false | (~spl3_120 | ~spl3_344)),
% 127.53/18.29 inference(evaluation,[],[f292226])).
% 127.53/18.29 tff(f292250,plain,(
% 127.53/18.29 ~spl3_120 | ~spl3_344),
% 127.53/18.29 inference(avatar_contradiction_clause,[],[f292249])).
% 127.53/18.29 tff(f297176,plain,(
% 127.53/18.29 $less(10,2) | $less(sK0,11) | ~spl3_52),
% 127.53/18.29 inference(resolution,[],[f1276,f3735])).
% 127.53/18.29 tff(f297178,plain,(
% 127.53/18.29 $less(10,0) | $less(sK0,11) | ~spl3_127),
% 127.53/18.29 inference(resolution,[],[f1276,f24068])).
% 127.53/18.29 tff(f297182,plain,(
% 127.53/18.29 $less(10,0) | $less(sK1,11) | ~spl3_8),
% 127.53/18.29 inference(resolution,[],[f1276,f9345])).
% 127.53/18.29 tff(f297234,plain,(
% 127.53/18.29 $less(sK1,11) | ~spl3_8),
% 127.53/18.29 inference(evaluation,[],[f297182])).
% 127.53/18.29 tff(f297237,plain,(
% 127.53/18.29 $less(sK0,11) | ~spl3_127),
% 127.53/18.29 inference(evaluation,[],[f297178])).
% 127.53/18.29 tff(f297238,plain,(
% 127.53/18.29 $less(sK0,11) | ~spl3_52),
% 127.53/18.29 inference(evaluation,[],[f297176])).
% 127.53/18.29 tff(f297255,plain,(
% 127.53/18.29 $false | (~spl3_4 | ~spl3_8)),
% 127.53/18.29 inference(forward_subsumption_resolution,[],[f297234,f1334])).
% 127.53/18.29 tff(f297256,plain,(
% 127.53/18.29 ~spl3_4 | ~spl3_8),
% 127.53/18.29 inference(avatar_contradiction_clause,[],[f297255])).
% 127.53/18.29 tff(f297261,plain,(
% 127.53/18.29 $false | (~spl3_6 | ~spl3_127)),
% 127.53/18.29 inference(forward_subsumption_resolution,[],[f297237,f2451])).
% 127.53/18.29 tff(f297262,plain,(
% 127.53/18.29 ~spl3_6 | ~spl3_127),
% 127.53/18.29 inference(avatar_contradiction_clause,[],[f297261])).
% 127.53/18.29 tff(f297264,plain,(
% 127.53/18.29 $false | (~spl3_6 | ~spl3_52)),
% 127.53/18.29 inference(forward_subsumption_resolution,[],[f297238,f2451])).
% 127.53/18.29 tff(f297265,plain,(
% 127.53/18.29 ~spl3_6 | ~spl3_52),
% 127.53/18.29 inference(avatar_contradiction_clause,[],[f297264])).
% 127.53/18.29 tff(f297459,plain,(
% 127.53/18.29 2 = sK1 | $less(2,sK1) | ~spl3_90),
% 127.53/18.29 inference(evaluation,[],[f16391])).
% 127.53/18.29 tff(f297709,plain,(
% 127.53/18.29 $less(2,sK1) | (~spl3_90 | spl3_101)),
% 127.53/18.29 inference(forward_subsumption_resolution,[],[f297459,f16413])).
% 127.53/18.29 tff(f297787,plain,(
% 127.53/18.29 spl3_127 | ~spl3_40),
% 127.53/18.29 inference(avatar_split_clause,[],[f277197,f3536,f24066])).
% 127.53/18.29 tff(f297817,plain,(
% 127.53/18.29 spl3_100 | ~spl3_90 | spl3_101),
% 127.53/18.29 inference(avatar_split_clause,[],[f297709,f16412,f9331,f16408])).
% 127.53/18.29 tff(f298366,definition,(
% 127.53/18.29 spl3_386 <=> $less(sK0,11)),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_386])],[avatar_definition])).
% 127.53/18.29 tff(f298368,plain,(
% 127.53/18.29 $less(sK0,11) | ~spl3_386),
% 127.53/18.29 inference(avatar_component_clause,[],[f298366])).
% 127.53/18.29 tff(f298501,plain,(
% 127.53/18.29 $less(3,sK0) | sK0 = 3 | ~spl3_37),
% 127.53/18.29 inference(resolution,[],[f3686,f10])).
% 127.53/18.29 tff(f298761,plain,(
% 127.53/18.29 $less(10,$product(2,sK1)) | $less(sK0,11) | ~spl3_87),
% 127.53/18.29 inference(resolution,[],[f7380,f1276])).
% 127.53/18.29 tff(f298814,plain,(
% 127.53/18.29 0 = $sum(sK1,$sum(-10,10)) | ~spl3_116),
% 127.53/18.29 inference(superposition,[],[f565,f20561])).
% 127.53/18.29 tff(f299191,plain,(
% 127.53/18.29 0 = sK1 | ~spl3_116),
% 127.53/18.29 inference(evaluation,[],[f298814])).
% 127.53/18.29 tff(f299272,plain,(
% 127.53/18.29 $false | (spl3_89 | ~spl3_116)),
% 127.53/18.29 inference(forward_subsumption_resolution,[],[f299191,f8180])).
% 127.53/18.29 tff(f299273,plain,(
% 127.53/18.29 spl3_89 | ~spl3_116),
% 127.53/18.29 inference(avatar_contradiction_clause,[],[f299272])).
% 127.53/18.29 tff(f305275,plain,(
% 127.53/18.29 ~$less(10,sK0) | ~spl3_386),
% 127.53/18.29 inference(resolution,[],[f298368,f1128])).
% 127.53/18.29 tff(f308837,plain,(
% 127.53/18.29 sK0 = $sum(7,1) | $less($sum(7,1),sK0) | ~spl3_172),
% 127.53/18.29 inference(resolution,[],[f151619,f59])).
% 127.53/18.29 tff(f308869,definition,(
% 127.53/18.29 spl3_423 <=> $less(8,sK0)),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_423])],[avatar_definition])).
% 127.53/18.29 tff(f308871,plain,(
% 127.53/18.29 $less(8,sK0) | ~spl3_423),
% 127.53/18.29 inference(avatar_component_clause,[],[f308869])).
% 127.53/18.29 tff(f308873,definition,(
% 127.53/18.29 spl3_424 <=> sK0 = 8),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_424])],[avatar_definition])).
% 127.53/18.29 tff(f308874,plain,(
% 127.53/18.29 sK0 != 8 | spl3_424),
% 127.53/18.29 inference(avatar_component_clause,[],[f308873])).
% 127.53/18.29 tff(f308875,plain,(
% 127.53/18.29 sK0 = 8 | ~spl3_424),
% 127.53/18.29 inference(avatar_component_clause,[],[f308873])).
% 127.53/18.29 tff(f310118,plain,(
% 127.53/18.29 ~$less(10,$product(2,8)) | (spl3_8 | ~spl3_424)),
% 127.53/18.29 inference(superposition,[],[f1319,f308875])).
% 127.53/18.29 tff(f310279,plain,(
% 127.53/18.29 $false | (spl3_8 | ~spl3_424)),
% 127.53/18.29 inference(evaluation,[],[f310118])).
% 127.53/18.29 tff(f310280,plain,(
% 127.53/18.29 spl3_8 | ~spl3_424),
% 127.53/18.29 inference(avatar_contradiction_clause,[],[f310279])).
% 127.53/18.29 tff(f310330,plain,(
% 127.53/18.29 sK0 = $sum(8,1) | $less($sum(8,1),sK0) | ~spl3_423),
% 127.53/18.29 inference(resolution,[],[f308871,f59])).
% 127.53/18.29 tff(f310362,definition,(
% 127.53/18.29 spl3_427 <=> $less(9,sK0)),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_427])],[avatar_definition])).
% 127.53/18.29 tff(f310364,plain,(
% 127.53/18.29 $less(9,sK0) | ~spl3_427),
% 127.53/18.29 inference(avatar_component_clause,[],[f310362])).
% 127.53/18.29 tff(f310366,definition,(
% 127.53/18.29 spl3_428 <=> sK0 = 9),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_428])],[avatar_definition])).
% 127.53/18.29 tff(f310367,plain,(
% 127.53/18.29 sK0 != 9 | spl3_428),
% 127.53/18.29 inference(avatar_component_clause,[],[f310366])).
% 127.53/18.29 tff(f310368,plain,(
% 127.53/18.29 sK0 = 9 | ~spl3_428),
% 127.53/18.29 inference(avatar_component_clause,[],[f310366])).
% 127.53/18.29 tff(f311906,plain,(
% 127.53/18.29 sK0 = $sum(9,1) | $less($sum(9,1),sK0) | ~spl3_427),
% 127.53/18.29 inference(resolution,[],[f310364,f59])).
% 127.53/18.29 tff(f311992,plain,(
% 127.53/18.29 ~$less(10,$product(2,9)) | (spl3_8 | ~spl3_428)),
% 127.53/18.29 inference(superposition,[],[f1319,f310368])).
% 127.53/18.29 tff(f312158,plain,(
% 127.53/18.29 $false | (spl3_8 | ~spl3_428)),
% 127.53/18.29 inference(evaluation,[],[f311992])).
% 127.53/18.29 tff(f312159,plain,(
% 127.53/18.29 spl3_8 | ~spl3_428),
% 127.53/18.29 inference(avatar_contradiction_clause,[],[f312158])).
% 127.53/18.29 tff(f312426,plain,(
% 127.53/18.29 spl3_49 | spl3_48 | ~spl3_37),
% 127.53/18.29 inference(avatar_split_clause,[],[f298501,f3487,f3689,f3693])).
% 127.53/18.29 tff(f312523,plain,(
% 127.53/18.29 sK1 = $sum(10,$product(2,$uminus(3))) | ~spl3_49),
% 127.53/18.29 inference(superposition,[],[f3914,f3695])).
% 127.53/18.29 tff(f312621,plain,(
% 127.53/18.29 sK1 = 4 | ~spl3_49),
% 127.53/18.29 inference(evaluation,[],[f312523])).
% 127.53/18.29 tff(f312671,plain,(
% 127.53/18.29 $false | (~spl3_49 | spl3_124)),
% 127.53/18.29 inference(forward_subsumption_resolution,[],[f312621,f22902])).
% 127.53/18.29 tff(f312672,plain,(
% 127.53/18.29 ~spl3_49 | spl3_124),
% 127.53/18.29 inference(avatar_contradiction_clause,[],[f312671])).
% 127.53/18.29 tff(f313928,definition,(
% 127.53/18.29 spl3_454 <=> $less($sum(10,sK1),10)),
% 127.53/18.29 introduced(definition,[new_symbols(definition,[spl3_454])],[avatar_definition])).
% 127.53/18.29 tff(f361131,plain,(
% 127.53/18.29 $less($sum($product(2,sK0),$product(2,sK1)),10) | ~spl3_71),
% 127.53/18.29 inference(resolution,[],[f6372,f99])).
% 127.53/18.29 tff(f361157,plain,(
% 127.53/18.29 $less(10,sK0) | $less($product(2,sK0),11) | ~spl3_71),
% 127.53/18.29 inference(resolution,[],[f6372,f1276])).
% 127.53/18.29 tff(f361167,plain,(
% 127.53/18.29 $less($sum(10,sK1),10) | ~spl3_71),
% 127.53/18.29 inference(forward_demodulation,[],[f361131,f7235])).
% 127.53/18.29 tff(f361177,plain,(
% 127.53/18.29 spl3_454 | ~spl3_71),
% 127.53/18.29 inference(avatar_split_clause,[],[f361167,f6370,f313928])).
% 127.53/18.29 tff(f422820,plain,(
% 127.53/18.29 $less($product(2,sK0),11) | $less($product(2,sK0),$sum(10,$uminus($sum(sK1,sK1))))),
% 127.53/18.29 inference(superposition,[],[f24324,f3235])).
% 127.53/18.29 tff(f422866,plain,(
% 127.53/18.29 $less($product(2,sK0),$sum(10,$uminus($product(sK1,2)))) | $less($product(2,sK0),11)),
% 127.53/18.29 inference(forward_demodulation,[],[f422820,f973])).
% 127.53/18.29 tff(f423260,plain,(
% 127.53/18.29 $less($product(2,sK0),$sum(10,$uminus($product(2,sK1)))) | $less($product(2,sK0),11)),
% 127.53/18.29 inference(forward_demodulation,[],[f422866,f14])).
% 127.53/18.29 tff(f423527,plain,(
% 127.53/18.29 $less($product(2,sK0),sK0) | $less($product(2,sK0),11)),
% 127.53/18.29 inference(forward_demodulation,[],[f423260,f228])).
% 127.53/18.29 tff(f507867,plain,(
% 127.53/18.29 $less(10,$sum(1,$product(sK0,2))) | $less(sK0,$product(2,sK1))),
% 127.53/18.29 inference(superposition,[],[f24190,f973])).
% 127.53/18.29 tff(f524534,plain,(
% 127.53/18.29 ~$less($sum(10,sK1),10) | $less(10,$product(2,sK0))),
% 127.53/18.29 inference(resolution,[],[f29456,f3050])).
% 127.53/18.29 tff(f524648,plain,(
% 127.53/18.29 spl3_64 | spl3_71),
% 127.53/18.29 inference(avatar_split_clause,[],[f423527,f6370,f4715])).
% 127.53/18.29 tff(f525847,plain,(
% 127.53/18.29 ( ! [X0 : $int] : (0 = $sum(sK1,$sum(X0,$sum(8,$uminus($sum(10,X0)))))) ) | ~spl3_95),
% 127.53/18.29 inference(evaluation,[],[f82623])).
% 127.53/18.29 tff(f526138,plain,(
% 127.53/18.29 ( ! [X0 : $int] : (sK0 = $sum(10,$sum(X0,$uminus($sum(8,X0))))) ) | ~spl3_124),
% 127.53/18.29 inference(evaluation,[],[f46462])).
% 127.53/18.29 tff(f526923,plain,(
% 127.53/18.29 ( ! [X0 : $int] : (0 = $sum(sK1,$sum(X0,$sum(8,$sum(-10,$uminus(X0)))))) ) | ~spl3_95),
% 127.53/18.29 inference(forward_demodulation,[],[f525847,f61366])).
% 127.53/18.29 tff(f527051,plain,(
% 127.53/18.29 sK0 = $sum(10,$uminus(8)) | ~spl3_124),
% 127.53/18.29 inference(forward_demodulation,[],[f526138,f287])).
% 127.53/18.29 tff(f527052,plain,(
% 127.53/18.29 2 = sK0 | ~spl3_124),
% 127.53/18.29 inference(evaluation,[],[f527051])).
% 127.53/18.29 tff(f527980,plain,(
% 127.53/18.29 0 = $sum(sK1,$sum(8,-10)) | ~spl3_95),
% 127.53/18.29 inference(forward_demodulation,[],[f526923,f733])).
% 127.53/18.29 tff(f527981,plain,(
% 127.53/18.29 0 = $sum(sK1,-2) | ~spl3_95),
% 127.53/18.29 inference(evaluation,[],[f527980])).
% 127.53/18.29 tff(f528018,plain,(
% 127.53/18.29 $false | (spl3_45 | ~spl3_124)),
% 127.53/18.29 inference(forward_subsumption_resolution,[],[f527052,f3636])).
% 127.53/18.29 tff(f528019,plain,(
% 127.53/18.29 spl3_45 | ~spl3_124),
% 127.53/18.29 inference(avatar_contradiction_clause,[],[f528018])).
% 127.53/18.29 tff(f528918,plain,(
% 127.53/18.29 0 = sK1 | ~spl3_153),
% 127.53/18.29 inference(evaluation,[],[f117242])).
% 127.53/18.29 tff(f529151,plain,(
% 127.53/18.29 spl3_89 | ~spl3_153),
% 127.53/18.29 inference(avatar_split_clause,[],[f528918,f96533,f8179])).
% 127.53/18.29 tff(f529516,plain,(
% 127.53/18.29 sK0 = $sum(0,1) | $less($sum(0,1),sK0) | ~spl3_31),
% 127.53/18.29 inference(resolution,[],[f3455,f59])).
% 127.53/18.29 tff(f529557,plain,(
% 127.53/18.29 1 = sK0 | $less(1,sK0) | ~spl3_31),
% 127.53/18.29 inference(evaluation,[],[f529516])).
% 127.53/18.29 tff(f530081,plain,(
% 127.53/18.29 $less(sK0,11) | $less(10,$product(2,sK0)) | sK0 = $product(2,sK0) | spl3_71),
% 127.53/18.29 inference(resolution,[],[f6371,f1268])).
% 127.53/18.29 tff(f531738,plain,(
% 127.53/18.29 ( ! [X0 : $int] : (sK0 = $sum(10,$sum(X0,$uminus($sum($product(2,2),X0))))) ) | ~spl3_101),
% 127.53/18.29 inference(superposition,[],[f540,f16414])).
% 127.53/18.29 tff(f532149,plain,(
% 127.53/18.29 ( ! [X0 : $int] : (sK0 = $sum(10,$sum(X0,$uminus($sum(4,X0))))) ) | ~spl3_101),
% 127.53/18.29 inference(evaluation,[],[f531738])).
% 127.53/18.29 tff(f532216,plain,(
% 127.53/18.29 sK0 = $sum(10,$uminus(4)) | ~spl3_101),
% 127.53/18.29 inference(forward_demodulation,[],[f532149,f287])).
% 127.53/18.29 tff(f532217,plain,(
% 127.53/18.29 sK0 = 6 | ~spl3_101),
% 127.53/18.29 inference(evaluation,[],[f532216])).
% 127.53/18.29 tff(f532232,plain,(
% 127.53/18.29 $false | (~spl3_101 | spl3_163)),
% 127.53/18.29 inference(forward_subsumption_resolution,[],[f532217,f119885])).
% 127.53/18.29 tff(f532233,plain,(
% 127.53/18.29 ~spl3_101 | spl3_163),
% 127.53/18.29 inference(avatar_contradiction_clause,[],[f532232])).
% 127.53/18.29 tff(f543188,plain,(
% 127.53/18.29 $less(5,sK0) | sK0 = 5 | ~spl3_94),
% 127.53/18.29 inference(resolution,[],[f96524,f10])).
% 127.53/18.29 tff(f543198,plain,(
% 127.53/18.29 spl3_153 | spl3_152 | ~spl3_94),
% 127.53/18.29 inference(avatar_split_clause,[],[f543188,f11085,f96529,f96533])).
% 127.53/18.29 tff(f558181,plain,(
% 127.53/18.29 $sum(10,$product(2,$product(2,7))) = $sum(20,7) | ~spl3_173),
% 127.53/18.29 inference(superposition,[],[f3783,f151623])).
% 127.53/18.29 tff(f558551,plain,(
% 127.53/18.29 $false | ~spl3_173),
% 127.53/18.29 inference(evaluation,[],[f558181])).
% 127.53/18.29 tff(f558552,plain,(
% 127.53/18.29 ~spl3_173),
% 127.53/18.29 inference(avatar_contradiction_clause,[],[f558551])).
% 127.53/18.29 tff(f558657,plain,(
% 127.53/18.29 sK0 = 8 | $less(8,sK0) | ~spl3_172),
% 127.53/18.29 inference(evaluation,[],[f308837])).
% 127.53/18.29 tff(f558661,plain,(
% 127.53/18.29 sK0 = 9 | $less(9,sK0) | ~spl3_423),
% 127.53/18.29 inference(evaluation,[],[f310330])).
% 127.53/18.29 tff(f558665,plain,(
% 127.53/18.29 10 = sK0 | $less(10,sK0) | ~spl3_427),
% 127.53/18.29 inference(evaluation,[],[f311906])).
% 127.53/18.29 tff(f558716,plain,(
% 127.53/18.29 $less(8,sK0) | (~spl3_172 | spl3_424)),
% 127.53/18.29 inference(forward_subsumption_resolution,[],[f558657,f308874])).
% 127.53/18.29 tff(f558724,plain,(
% 127.53/18.29 $less(9,sK0) | (~spl3_423 | spl3_428)),
% 127.53/18.29 inference(forward_subsumption_resolution,[],[f558661,f310367])).
% 127.53/18.29 tff(f558794,plain,(
% 127.53/18.29 ~spl3_6 | ~spl3_386),
% 127.53/18.29 inference(avatar_split_clause,[],[f305275,f298366,f1309])).
% 127.53/18.29 tff(f559069,plain,(
% 127.53/18.29 spl3_423 | ~spl3_172 | spl3_424),
% 127.53/18.29 inference(avatar_split_clause,[],[f558716,f308873,f151617,f308869])).
% 127.53/18.29 tff(f559072,plain,(
% 127.53/18.29 spl3_427 | ~spl3_423 | spl3_428),
% 127.53/18.29 inference(avatar_split_clause,[],[f558724,f310366,f308869,f310362])).
% 127.53/18.29 tff(f559656,plain,(
% 127.53/18.29 $less(sK0,11) | (spl3_40 | ~spl3_87)),
% 127.53/18.29 inference(forward_subsumption_resolution,[],[f298761,f3537])).
% 127.53/18.29 tff(f559659,plain,(
% 127.53/18.29 $less(sK0,11) | sK0 = $product(2,sK0) | (spl3_8 | spl3_71)),
% 127.53/18.29 inference(forward_subsumption_resolution,[],[f530081,f1319])).
% 127.53/18.29 tff(f559758,plain,(
% 127.53/18.29 spl3_386 | spl3_40 | ~spl3_87),
% 127.53/18.29 inference(avatar_split_clause,[],[f559656,f7378,f3536,f298366])).
% 127.53/18.29 tff(f559761,plain,(
% 127.53/18.29 $less(sK0,11) | (spl3_8 | spl3_60 | spl3_71)),
% 127.53/18.29 inference(forward_subsumption_resolution,[],[f559659,f4677])).
% 127.53/18.29 tff(f559829,plain,(
% 127.53/18.29 spl3_386 | spl3_8 | spl3_60 | spl3_71),
% 127.53/18.29 inference(avatar_split_clause,[],[f559761,f6370,f4676,f1318,f298366])).
% 127.53/18.29 tff(f560622,plain,(
% 127.53/18.29 spl3_36 | spl3_47 | ~spl3_31),
% 127.53/18.29 inference(avatar_split_clause,[],[f529557,f3453,f3669,f3481])).
% 127.53/18.29 tff(f565582,plain,(
% 127.53/18.29 $sum(20,1) = $sum(10,$product(2,$product(2,1))) | ~spl3_47),
% 127.53/18.29 inference(superposition,[],[f3783,f3671])).
% 127.53/18.29 tff(f565934,plain,(
% 127.53/18.29 $false | ~spl3_47),
% 127.53/18.29 inference(evaluation,[],[f565582])).
% 127.53/18.29 tff(f565935,plain,(
% 127.53/18.29 ~spl3_47),
% 127.53/18.29 inference(avatar_contradiction_clause,[],[f565934])).
% 127.53/18.29 tff(f570682,plain,(
% 127.53/18.29 $less(4,sK0) | sK0 = 4 | ~spl3_48),
% 127.53/18.29 inference(resolution,[],[f11082,f10])).
% 127.53/18.29 tff(f577089,plain,(
% 127.53/18.29 $sum(10,$product(2,$product(2,6))) = $sum(20,6) | ~spl3_163),
% 127.53/18.29 inference(superposition,[],[f3783,f119886])).
% 127.53/18.29 tff(f577464,plain,(
% 127.53/18.29 $false | ~spl3_163),
% 127.53/18.29 inference(evaluation,[],[f577089])).
% 127.53/18.29 tff(f577465,plain,(
% 127.53/18.29 ~spl3_163),
% 127.53/18.29 inference(avatar_contradiction_clause,[],[f577464])).
% 127.53/18.29 tff(f577551,plain,(
% 127.53/18.29 10 = sK0 | ~spl3_89),
% 127.53/18.29 inference(evaluation,[],[f15196])).
% 127.53/18.29 tff(f577734,plain,(
% 127.53/18.29 spl3_344 | ~spl3_89),
% 127.53/18.29 inference(avatar_split_clause,[],[f577551,f8179,f291317])).
% 127.53/18.29 tff(f579663,plain,(
% 127.53/18.29 spl3_64 | spl3_6 | ~spl3_71),
% 127.53/18.29 inference(avatar_split_clause,[],[f361157,f6370,f1309,f4715])).
% 127.53/18.29 tff(f580148,plain,(
% 127.53/18.29 spl3_95 | spl3_94 | ~spl3_48),
% 127.53/18.29 inference(avatar_split_clause,[],[f570682,f3689,f11085,f11089])).
% 127.53/18.29 tff(f580168,plain,(
% 127.53/18.29 $less(10,$sum(1,$product(2,sK0))) | $less(sK0,$product(2,sK1))),
% 127.53/18.29 inference(forward_demodulation,[],[f507867,f14])).
% 127.53/18.29 tff(f580416,plain,(
% 127.53/18.29 spl3_8 | ~spl3_454),
% 127.53/18.29 inference(avatar_split_clause,[],[f524534,f313928,f1318])).
% 127.53/18.29 tff(f580464,plain,(
% 127.53/18.29 spl3_116 | spl3_8 | ~spl3_76),
% 127.53/18.29 inference(avatar_split_clause,[],[f282859,f7044,f1318,f20559])).
% 127.53/18.29 tff(f580526,plain,(
% 127.53/18.29 spl3_6 | spl3_344 | ~spl3_427),
% 127.53/18.29 inference(avatar_split_clause,[],[f558665,f310362,f291317,f1309])).
% 127.53/18.29 tff(f580712,plain,(
% 127.53/18.29 spl3_87 | spl3_76),
% 127.53/18.29 inference(avatar_split_clause,[],[f580168,f7044,f7378])).
% 127.53/18.29 tff(f581573,plain,(
% 127.53/18.29 $sum(sK0,$product(2,0)) = $sum(10,$product(-2,2)) | ~spl3_95),
% 127.53/18.29 inference(superposition,[],[f1520,f527981])).
% 127.53/18.29 tff(f581943,plain,(
% 127.53/18.29 sK0 = 6 | ~spl3_95),
% 127.53/18.29 inference(evaluation,[],[f581573])).
% 127.53/18.29 tff(f582004,plain,(
% 127.53/18.29 spl3_163 | ~spl3_95),
% 127.53/18.29 inference(avatar_split_clause,[],[f581943,f11089,f119884])).
% 127.53/18.29 tff(f618018,plain,(
% 127.53/18.29 $less(6,sK0) | sK0 = 6 | ~spl3_152),
% 127.53/18.29 inference(resolution,[],[f119874,f10])).
% 127.53/18.29 tff(f618031,plain,(
% 127.53/18.29 spl3_163 | spl3_162 | ~spl3_152),
% 127.53/18.29 inference(avatar_split_clause,[],[f618018,f96529,f119880,f119884])).
% 127.53/18.30 tff(f642672,plain,(
% 127.53/18.30 $less(7,sK0) | sK0 = 7 | ~spl3_162),
% 127.53/18.30 inference(resolution,[],[f151611,f10])).
% 127.53/18.30 tff(f642685,plain,(
% 127.53/18.30 spl3_173 | spl3_172 | ~spl3_162),
% 127.53/18.30 inference(avatar_split_clause,[],[f642672,f119880,f151617,f151621])).
% 127.53/18.30 tff(f959168,plain,(
% 127.53/18.30 sK1 = $sum(10,$sum($product(2,$sum(10,$uminus($sum(sK0,sK0)))),$uminus($product(2,$product(2,sK1)))))),
% 127.53/18.30 inference(superposition,[],[f123347,f25942])).
% 127.53/18.30 tff(f959820,plain,(
% 127.53/18.30 sK1 = $sum(10,$sum($uminus($product(2,$product(2,sK1))),$product(2,$sum(10,$uminus($sum(sK0,sK0))))))),
% 127.53/18.30 inference(forward_demodulation,[],[f959168,f3])).
% 127.53/18.30 tff(f960002,plain,(
% 127.53/18.30 sK1 = $sum(10,$sum($uminus($product(2,$product(2,sK1))),$product(2,$sum(10,$uminus($product(sK0,2))))))),
% 127.53/18.30 inference(forward_demodulation,[],[f959820,f973])).
% 127.53/18.30 tff(f960085,plain,(
% 127.53/18.30 sK1 = $sum(10,$sum($uminus($product(2,$product(2,sK1))),$product(2,$sum(10,$uminus($product(2,sK0))))))),
% 127.53/18.30 inference(forward_demodulation,[],[f960002,f14])).
% 127.53/18.30 tff(f960140,plain,(
% 127.53/18.30 sK1 = $sum(10,$sum($uminus($product(2,$product(2,sK1))),$product(2,$sum(10,$sum(-10,sK1)))))),
% 127.53/18.30 inference(forward_demodulation,[],[f960085,f372])).
% 127.53/18.30 tff(f960168,plain,(
% 127.53/18.30 sK1 = $sum(10,$sum($uminus($product(2,$product(2,sK1))),$product(2,sK1)))),
% 127.53/18.30 inference(forward_demodulation,[],[f960140,f2388])).
% 127.53/18.30 tff(f960188,plain,(
% 127.53/18.30 sK1 = $sum(10,$sum(10,$uminus($sum($product(2,$product(2,sK1)),sK0))))),
% 127.53/18.30 inference(forward_demodulation,[],[f960168,f36312])).
% 127.53/18.30 tff(f960202,plain,(
% 127.53/18.30 sK1 = $sum(10,$sum(10,$uminus($sum(sK0,$product(2,$product(2,sK1))))))),
% 127.53/18.30 inference(forward_demodulation,[],[f960188,f53185])).
% 127.53/18.30 tff(f960209,plain,(
% 127.53/18.30 sK1 = $sum(10,$sum(10,$uminus($sum(10,$product(2,sK1)))))),
% 127.53/18.30 inference(forward_demodulation,[],[f960202,f7234])).
% 127.53/18.30 tff(f960213,plain,(
% 127.53/18.30 sK0 = sK1),
% 127.53/18.30 inference(forward_demodulation,[],[f960209,f23708])).
% 127.53/18.30 tff(f960217,plain,(
% 127.53/18.30 $false | spl3_108),
% 127.53/18.30 inference(forward_subsumption_resolution,[],[f960213,f19091])).
% 127.53/18.30 tff(f960218,plain,(
% 127.53/18.30 spl3_108),
% 127.53/18.30 inference(avatar_contradiction_clause,[],[f960217])).
% 127.53/18.30 cnf(s4, plain, spl3_3 | spl3_4, inference(sat_conversion,[],[f1303])).
% 127.53/18.30 cnf(s139, plain, ~spl3_8 | ~spl3_64, inference(sat_conversion,[],[f9342])).
% 127.53/18.30 cnf(s184, plain, ~spl3_8 | ~spl3_93, inference(sat_conversion,[],[f13015])).
% 127.53/18.30 cnf(s387, plain, ~spl3_39 | spl3_93 | ~spl3_108, inference(sat_conversion,[],[f20538])).
% 127.53/18.30 cnf(s388, plain, ~spl3_36 | spl3_90 | ~spl3_108, inference(sat_conversion,[],[f20540])).
% 127.53/18.30 cnf(s390, plain, ~spl3_4 | spl3_6 | ~spl3_108, inference(sat_conversion,[],[f20544])).
% 127.53/18.30 cnf(s472, plain, spl3_37 | ~spl3_100 | ~spl3_108, inference(sat_conversion,[],[f22261])).
% 127.53/18.30 cnf(s479, plain, spl3_8 | spl3_31 | spl3_56 | ~spl3_108, inference(sat_conversion,[],[f22323])).
% 127.53/18.30 cnf(s493, plain, spl3_45 | spl3_52 | ~spl3_108 | spl3_120, inference(sat_conversion,[],[f22338])).
% 127.53/18.30 cnf(s595, plain, ~spl3_6 | ~spl3_45, inference(sat_conversion,[],[f23047])).
% 127.53/18.30 cnf(s801, plain, ~spl3_45 | ~spl3_124, inference(sat_conversion,[],[f46530])).
% 127.53/18.30 cnf(s874, plain, ~spl3_100 | spl3_120, inference(sat_conversion,[],[f49728])).
% 127.53/18.30 cnf(s934, plain, ~spl3_3 | ~spl3_41, inference(sat_conversion,[],[f108790])).
% 127.53/18.30 cnf(s989, plain, spl3_39 | spl3_127, inference(sat_conversion,[],[f120237])).
% 127.53/18.30 cnf(s1424, plain, ~spl3_4 | ~spl3_104, inference(sat_conversion,[],[f199396])).
% 127.53/18.30 cnf(s1426, plain, spl3_41 | ~spl3_104, inference(sat_conversion,[],[f199444])).
% 127.53/18.30 cnf(s1682, plain, ~spl3_56 | spl3_104, inference(sat_conversion,[],[f278511])).
% 127.53/18.30 cnf(s1699, plain, spl3_56 | ~spl3_60, inference(sat_conversion,[],[f278573])).
% 127.53/18.30 cnf(s2036, plain, ~spl3_120 | ~spl3_344, inference(sat_conversion,[],[f292250])).
% 127.53/18.30 cnf(s2285, plain, ~spl3_4 | ~spl3_8, inference(sat_conversion,[],[f297256])).
% 127.53/18.30 cnf(s2288, plain, ~spl3_6 | ~spl3_127, inference(sat_conversion,[],[f297262])).
% 127.53/18.30 cnf(s2289, plain, ~spl3_6 | ~spl3_52, inference(sat_conversion,[],[f297265])).
% 127.53/18.30 cnf(s2562, plain, ~spl3_40 | spl3_127, inference(sat_conversion,[],[f297787])).
% 127.53/18.30 cnf(s2729, plain, ~spl3_90 | spl3_100 | spl3_101, inference(sat_conversion,[],[f297817])).
% 127.53/18.30 cnf(s2931, plain, spl3_89 | ~spl3_116, inference(sat_conversion,[],[f299273])).
% 127.53/18.30 cnf(s3058, plain, spl3_8 | ~spl3_424, inference(sat_conversion,[],[f310280])).
% 127.53/18.30 cnf(s3092, plain, spl3_8 | ~spl3_428, inference(sat_conversion,[],[f312159])).
% 127.53/18.30 cnf(s3160, plain, ~spl3_37 | spl3_48 | spl3_49, inference(sat_conversion,[],[f312426])).
% 127.53/18.30 cnf(s3175, plain, ~spl3_49 | spl3_124, inference(sat_conversion,[],[f312672])).
% 127.53/18.30 cnf(s4482, plain, ~spl3_71 | spl3_454, inference(sat_conversion,[],[f361177])).
% 127.53/18.30 cnf(s6637, plain, spl3_64 | spl3_71, inference(sat_conversion,[],[f524648])).
% 127.53/18.30 cnf(s7733, plain, spl3_45 | ~spl3_124, inference(sat_conversion,[],[f528019])).
% 127.53/18.30 cnf(s8131, plain, spl3_89 | ~spl3_153, inference(sat_conversion,[],[f529151])).
% 127.53/18.30 cnf(s8595, plain, ~spl3_101 | spl3_163, inference(sat_conversion,[],[f532233])).
% 127.53/18.30 cnf(s8676, plain, ~spl3_94 | spl3_152 | spl3_153, inference(sat_conversion,[],[f543198])).
% 127.53/18.30 cnf(s8871, plain, ~spl3_173, inference(sat_conversion,[],[f558552])).
% 127.53/18.30 cnf(s8947, plain, ~spl3_6 | ~spl3_386, inference(sat_conversion,[],[f558794])).
% 127.53/18.30 cnf(s9032, plain, ~spl3_172 | spl3_423 | spl3_424, inference(sat_conversion,[],[f559069])).
% 127.53/18.30 cnf(s9038, plain, ~spl3_423 | spl3_427 | spl3_428, inference(sat_conversion,[],[f559072])).
% 127.53/18.30 cnf(s9216, plain, spl3_40 | ~spl3_87 | spl3_386, inference(sat_conversion,[],[f559758])).
% 127.53/18.30 cnf(s9241, plain, spl3_8 | spl3_60 | spl3_71 | spl3_386, inference(sat_conversion,[],[f559829])).
% 127.53/18.30 cnf(s9494, plain, ~spl3_31 | spl3_36 | spl3_47, inference(sat_conversion,[],[f560622])).
% 127.53/18.30 cnf(s9631, plain, ~spl3_47, inference(sat_conversion,[],[f565935])).
% 127.53/18.30 cnf(s10682, plain, ~spl3_163, inference(sat_conversion,[],[f577465])).
% 127.53/18.30 cnf(s10705, plain, ~spl3_89 | spl3_344, inference(sat_conversion,[],[f577734])).
% 127.53/18.30 cnf(s11189, plain, spl3_6 | spl3_64 | ~spl3_71, inference(sat_conversion,[],[f579663])).
% 127.53/18.30 cnf(s11318, plain, ~spl3_48 | spl3_94 | spl3_95, inference(sat_conversion,[],[f580148])).
% 127.53/18.30 cnf(s11379, plain, spl3_8 | ~spl3_454, inference(sat_conversion,[],[f580416])).
% 127.53/18.30 cnf(s11385, plain, spl3_8 | ~spl3_76 | spl3_116, inference(sat_conversion,[],[f580464])).
% 127.53/18.30 cnf(s11402, plain, spl3_6 | spl3_344 | ~spl3_427, inference(sat_conversion,[],[f580526])).
% 127.53/18.30 cnf(s11527, plain, spl3_76 | spl3_87, inference(sat_conversion,[],[f580712])).
% 127.53/18.30 cnf(s11738, plain, ~spl3_95 | spl3_163, inference(sat_conversion,[],[f582004])).
% 127.53/18.30 cnf(s12850, plain, ~spl3_152 | spl3_162 | spl3_163, inference(sat_conversion,[],[f618031])).
% 127.53/18.30 cnf(s12906, plain, ~spl3_162 | spl3_172 | spl3_173, inference(sat_conversion,[],[f642685])).
% 127.53/18.30 cnf(s19662, plain, spl3_108, inference(sat_conversion,[],[f960218])).
% 127.53/18.30 cnf(s20231, plain, ~spl3_95, inference(rat,[],[s11738,s10682])).
% 127.53/18.30 cnf(s20282, plain, ~spl3_31 | spl3_36, inference(rat,[],[s9494,s9631])).
% 127.53/18.30 cnf(s20349, plain, ~spl3_101, inference(rat,[],[s8595,s10682])).
% 127.53/18.30 cnf(s20922, plain, ~spl3_90 | spl3_100, inference(rat,[],[s2729,s20349])).
% 127.53/18.30 cnf(s21191, plain, spl3_45 | spl3_52 | spl3_120, inference(rat,[],[s493,s19662])).
% 127.53/18.30 cnf(s21195, plain, spl3_8 | spl3_31 | spl3_56, inference(rat,[],[s479,s19662])).
% 127.53/18.30 cnf(s21199, plain, spl3_37 | ~spl3_100, inference(rat,[],[s472,s19662])).
% 127.53/18.30 cnf(s21217, plain, ~spl3_4 | spl3_6, inference(rat,[],[s390,s19662])).
% 127.53/18.30 cnf(s21219, plain, ~spl3_36 | spl3_90, inference(rat,[],[s388,s19662])).
% 127.53/18.30 cnf(s21220, plain, ~spl3_39 | spl3_93, inference(rat,[],[s387,s19662])).
% 127.53/18.30 cnf(s21273, plain, ~spl3_4, inference(rat,[],[s9241,s1699,s4482,s8947,s1682,s11379,s21217,s1424,s2285])).
% 127.53/18.30 cnf(s21340, plain, spl3_3, inference(rat,[],[s4,s21273])).
% 127.53/18.30 cnf(s21354, plain, ~spl3_41, inference(rat,[],[s934,s21340])).
% 127.53/18.30 cnf(s21360, plain, ~spl3_104, inference(rat,[],[s1426,s21354])).
% 127.53/18.30 cnf(s21362, plain, ~spl3_56, inference(rat,[],[s1682,s21360])).
% 127.53/18.30 cnf(s21404, plain, ~spl3_6, inference(rat,[],[s2931,s11385,s10705,s184,s11527,s2036,s21220,s9216,s21191,s989,s2562,s595,s2288,s2289,s8947])).
% 127.53/18.30 cnf(s21570, plain, ~spl3_124, inference(rat,[],[s801,s7733])).
% 127.53/18.30 cnf(s21571, plain, ~spl3_49, inference(rat,[],[s3175,s21570])).
% 127.53/18.30 cnf(s21572, plain, spl3_8, inference(rat,[],[s12906,s12850,s9032,s8676,s8131,s9038,s11318,s10705,s11402,s3160,s2036,s21199,s874,s20922,s21219,s20282,s21195,s3058,s3092,s8871,s10682,s20231,s21404,s21571,s21362])).
% 127.53/18.30 cnf(s21596, plain, ~spl3_64, inference(rat,[],[s139,s21572])).
% 127.53/18.30 cnf(s21687, plain, ~spl3_71, inference(rat,[],[s11189,s21404,s21596])).
% 127.53/18.30 cnf(s21710, plain, $false, inference(rat,[],[s6637,s21687,s21596])).
% 127.53/18.30 tff(f960223,plain,(
% 127.53/18.30 $false),
% 127.53/18.30 inference(avatar_sat_refutation,[],[s21710])).
% 127.53/18.30 % SZS output end Proof for theBenchmark
% 127.53/18.30 % (162823)------------------------------
% 127.53/18.30 % (162823)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.53/18.30 % (162823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.53/18.30 % (162823)CaDiCaL version: 2.1.3
% 127.53/18.30 % (162823)Termination reason: Refutation
% 127.53/18.30 % (162823)Time elapsed: 17.944 s
% 127.53/18.30 % (162823)Peak memory usage: 343 MB
% 127.53/18.30 % (162823)Instructions burned: 58074 (million)
% 127.53/18.30 % (162817)Success in time 18.063 s
% 127.53/18.30 % Vampire exiting
%------------------------------------------------------------------------------