%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : PUZ133_2 : 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 : n003.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 12:32:33 PM UTC 2026
% Result : Theorem 11.44s 2.08s
% Output : Refutation 11.44s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ133_2 : TPTP v9.3.1. Released v5.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.37 % Computer : n003.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 22:46:57 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.41 Running first-order model finding
% 0.10/0.41 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
% 2.65/0.93 % (997248)Will run a generic schedule for satisfiability detection.
% 2.65/0.93 % (997253)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3162379166_2999 on theBenchmark for (2999ds/0Mi)
% 2.65/0.93 % (997253)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 2.65/0.93 % (997253)Terminated due to inappropriate strategy.
% 2.65/0.93 % (997253)------------------------------
% 2.65/0.93 % (997253)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.65/0.93 % (997253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.65/0.93 % (997253)CaDiCaL version: 2.1.3
% 2.65/0.93 % (997253)Termination reason: Inappropriate
% 2.65/0.93 % (997253)Time elapsed: 0.0000 s
% 2.65/0.93 % (997253)Peak memory usage: 10 MB
% 2.65/0.93 % (997253)Instructions burned: 1 (million)
% 2.65/0.93 % (997253)------------------------------
% 2.65/0.93 % (997253)------------------------------
% 2.65/0.93 % (997254)% WARNING: option uhcvi not known.
% 2.65/0.93 % (997254)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=549971248:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 2.65/0.93 % (997255)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3259685321:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 2.65/0.93 % (997256)dis+10_1_sil=32000:sp=arity:random_seed=2127410955:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 2.65/0.93 % (997257)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=270342181:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 2.65/0.93 % (997259)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=28115931:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 2.65/0.93 % (997258)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2003021843:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 2.65/0.93 % (997261)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2376721327:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 2.65/0.93 % (997261)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 2.65/0.93 % (997261)Terminated due to inappropriate strategy.
% 2.65/0.93 % (997261)------------------------------
% 2.65/0.93 % (997261)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.65/0.93 % (997261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.65/0.93 % (997261)CaDiCaL version: 2.1.3
% 2.65/0.93 % (997261)Termination reason: Inappropriate
% 2.65/0.93 % (997261)Time elapsed: 0.0000 s
% 2.65/0.93 % (997261)Peak memory usage: 11 MB
% 2.65/0.93 % (997261)Instructions burned: 1 (million)
% 2.65/0.93 % (997261)------------------------------
% 2.65/0.93 % (997261)------------------------------
% 2.65/0.93 % (997269)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2979145737:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 2.65/0.93 % (997256)Instruction limit reached!
% 2.65/0.93 % (997256)------------------------------
% 2.65/0.93 % (997256)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.65/0.93 % (997256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.65/0.93 % (997256)CaDiCaL version: 2.1.3
% 2.65/0.93 % (997256)Termination reason: Instruction limit
% 2.65/0.93 % (997256)Termination phase: Saturation
% 2.65/0.93 % (997256)Time elapsed: 0.062 s
% 2.65/0.93 % (997256)Peak memory usage: 12 MB
% 2.65/0.93 % (997256)Instructions burned: 104 (million)
% 2.65/0.93 % (997269)Instruction limit reached!
% 2.65/0.93 % (997269)------------------------------
% 2.65/0.93 % (997269)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.65/0.93 % (997269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.65/0.93 % (997269)CaDiCaL version: 2.1.3
% 2.65/0.93 % (997269)Termination reason: Instruction limit
% 2.65/0.93 % (997269)Termination phase: Saturation
% 2.65/0.93 % (997269)Time elapsed: 0.047 s
% 2.65/0.93 % (997269)Peak memory usage: 13 MB
% 2.65/0.93 % (997269)Instructions burned: 133 (million)
% 2.65/0.93 % (997257)Instruction limit reached!
% 2.65/0.93 % (997257)------------------------------
% 2.65/0.93 % (997257)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.65/0.93 % (997257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.65/0.93 % (997257)CaDiCaL version: 2.1.3
% 2.65/0.93 % (997257)Termination reason: Instruction limit
% 2.65/0.93 % (997257)Termination phase: Saturation
% 6.96/1.55 % (997257)Time elapsed: 0.068 s
% 6.96/1.55 % (997257)Peak memory usage: 12 MB
% 6.96/1.55 % (997257)Instructions burned: 117 (million)
% 6.96/1.55 % (997272)ott-21_1_sil=16000:fs=off:random_seed=1171290622:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 6.96/1.55 % (997258)Instruction limit reached!
% 6.96/1.55 % (997258)------------------------------
% 6.96/1.55 % (997258)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.96/1.55 % (997258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.55 % (997258)CaDiCaL version: 2.1.3
% 6.96/1.55 % (997258)Termination reason: Instruction limit
% 6.96/1.55 % (997258)Termination phase: Saturation
% 6.96/1.55 % (997258)Time elapsed: 0.075 s
% 6.96/1.55 % (997258)Peak memory usage: 12 MB
% 6.96/1.55 % (997258)Instructions burned: 132 (million)
% 6.96/1.55 % (997271)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=1914624261:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 6.96/1.55 % (997273)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2792802112:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 6.96/1.55 % (997259)Instruction limit reached!
% 6.96/1.55 % (997259)------------------------------
% 6.96/1.55 % (997259)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.96/1.55 % (997259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.55 % (997259)CaDiCaL version: 2.1.3
% 6.96/1.55 % (997259)Termination reason: Instruction limit
% 6.96/1.55 % (997259)Termination phase: Saturation
% 6.96/1.55 % (997259)Time elapsed: 0.089 s
% 6.96/1.55 % (997259)Peak memory usage: 12 MB
% 6.96/1.55 % (997259)Instructions burned: 159 (million)
% 6.96/1.55 % (997275)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3400032560:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 6.96/1.55 % (997275)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.96/1.55 % (997275)Terminated due to inappropriate strategy.
% 6.96/1.55 % (997275)------------------------------
% 6.96/1.55 % (997275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.96/1.55 % (997275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.55 % (997275)CaDiCaL version: 2.1.3
% 6.96/1.55 % (997275)Termination reason: Inappropriate
% 6.96/1.55 % (997275)Time elapsed: 0.001 s
% 6.96/1.55 % (997275)Peak memory usage: 10 MB
% 6.96/1.55 % (997275)Instructions burned: 1 (million)
% 6.96/1.55 % (997275)------------------------------
% 6.96/1.55 % (997275)------------------------------
% 6.96/1.55 % (997278)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1218704138:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 6.96/1.55 % (997280)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3440343958:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 6.96/1.55 % (997280)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.96/1.55 % (997280)Terminated due to inappropriate strategy.
% 6.96/1.55 % (997280)------------------------------
% 6.96/1.55 % (997280)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.96/1.55 % (997280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.55 % (997280)CaDiCaL version: 2.1.3
% 6.96/1.55 % (997280)Termination reason: Inappropriate
% 6.96/1.55 % (997280)Time elapsed: 0.001 s
% 6.96/1.55 % (997280)Peak memory usage: 11 MB
% 6.96/1.55 % (997280)Instructions burned: 1 (million)
% 6.96/1.55 % (997280)------------------------------
% 6.96/1.55 % (997280)------------------------------
% 6.96/1.55 % (997272)Instruction limit reached!
% 6.96/1.55 % (997272)------------------------------
% 6.96/1.55 % (997272)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.96/1.55 % (997272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.55 % (997272)CaDiCaL version: 2.1.3
% 6.96/1.55 % (997272)Termination reason: Instruction limit
% 6.96/1.55 % (997272)Termination phase: Saturation
% 6.96/1.55 % (997272)Time elapsed: 0.043 s
% 6.96/1.55 % (997272)Peak memory usage: 12 MB
% 6.96/1.55 % (997272)Instructions burned: 183 (million)
% 6.96/1.55 % (997284)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=743826485:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi)
% 6.96/1.55 % (997283)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=1608349359: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)
% 11.44/2.08 % (997284)Instruction limit reached!
% 11.44/2.08 % (997284)------------------------------
% 11.44/2.08 % (997284)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.44/2.08 % (997284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.44/2.08 % (997284)CaDiCaL version: 2.1.3
% 11.44/2.08 % (997284)Termination reason: Instruction limit
% 11.44/2.08 % (997284)Termination phase: Saturation
% 11.44/2.08 % (997284)Time elapsed: 0.244 s
% 11.44/2.08 % (997284)Peak memory usage: 17 MB
% 11.44/2.08 % (997284)Instructions burned: 880 (million)
% 11.44/2.08 % (997273)Instruction limit reached!
% 11.44/2.08 % (997273)------------------------------
% 11.44/2.08 % (997273)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.44/2.08 % (997273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.44/2.08 % (997273)CaDiCaL version: 2.1.3
% 11.44/2.08 % (997273)Termination reason: Instruction limit
% 11.44/2.08 % (997273)Termination phase: Saturation
% 11.44/2.08 % (997273)Time elapsed: 0.294 s
% 11.44/2.08 % (997273)Peak memory usage: 13 MB
% 11.44/2.08 % (997273)Instructions burned: 479 (million)
% 11.44/2.08 % (997287)fmb+10_1_sil=64000:random_seed=3445160783:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi)
% 11.44/2.08 % (997287)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 11.44/2.08 % (997287)Terminated due to inappropriate strategy.
% 11.44/2.08 % (997287)------------------------------
% 11.44/2.08 % (997287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.44/2.08 % (997287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.44/2.08 % (997287)CaDiCaL version: 2.1.3
% 11.44/2.08 % (997287)Termination reason: Inappropriate
% 11.44/2.08 % (997287)Time elapsed: 0.0000 s
% 11.44/2.08 % (997287)Peak memory usage: 10 MB
% 11.44/2.08 % (997287)Instructions burned: 1 (million)
% 11.44/2.08 % (997287)------------------------------
% 11.44/2.08 % (997287)------------------------------
% 11.44/2.08 % (997290)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3070680263:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi)
% 11.44/2.08 % (997290)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 11.44/2.08 % (997290)Terminated due to inappropriate strategy.
% 11.44/2.08 % (997290)------------------------------
% 11.44/2.08 % (997290)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.44/2.08 % (997290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.44/2.08 % (997290)CaDiCaL version: 2.1.3
% 11.44/2.08 % (997290)Termination reason: Inappropriate
% 11.44/2.08 % (997290)Time elapsed: 0.0000 s
% 11.44/2.08 % (997290)Peak memory usage: 10 MB
% 11.44/2.08 % (997290)Instructions burned: 1 (million)
% 11.44/2.08 % (997290)------------------------------
% 11.44/2.08 % (997290)------------------------------
% 11.44/2.08 % (997288)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1183822160:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi)
% 11.44/2.08 % (997288)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 11.44/2.08 % (997288)Terminated due to inappropriate strategy.
% 11.44/2.08 % (997288)------------------------------
% 11.44/2.08 % (997288)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.44/2.08 % (997288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.44/2.08 % (997288)CaDiCaL version: 2.1.3
% 11.44/2.08 % (997288)Termination reason: Inappropriate
% 11.44/2.08 % (997288)Time elapsed: 0.001 s
% 11.44/2.08 % (997288)Peak memory usage: 10 MB
% 11.44/2.08 % (997288)Instructions burned: 1 (million)
% 11.44/2.08 % (997288)------------------------------
% 11.44/2.08 % (997288)------------------------------
% 11.44/2.08 % (997292)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2769711628:i=5131_2995 on theBenchmark for (2995ds/5131Mi)
% 11.44/2.08 % (997294)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=233754118:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 11.44/2.08 % (997271)Instruction limit reached!
% 11.44/2.08 % (997271)------------------------------
% 11.44/2.08 % (997271)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.44/2.08 % (997271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.44/2.08 % (997271)CaDiCaL version: 2.1.3
% 11.44/2.08 % (997271)Termination reason: Instruction limit
% 11.44/2.08 % (997271)Termination phase: Saturation
% 11.44/2.08 % (997271)Time elapsed: 0.400 s
% 11.44/2.08 % (997271)Peak memory usage: 17 MB
% 11.44/2.08 % (997271)Instructions burned: 684 (million)
% 11.44/2.08 % (997297)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2252466312:i=6324_2994 on theBenchmark for (2994ds/6324Mi)
% 11.44/2.08 % (997297)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 11.44/2.08 % (997297)Terminated due to inappropriate strategy.
% 11.44/2.08 % (997297)------------------------------
% 11.44/2.08 % (997297)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.44/2.08 % (997297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.44/2.08 % (997297)CaDiCaL version: 2.1.3
% 11.44/2.08 % (997297)Termination reason: Inappropriate
% 11.44/2.08 % (997297)Time elapsed: 0.001 s
% 11.44/2.08 % (997297)Peak memory usage: 10 MB
% 11.44/2.08 % (997297)Instructions burned: 1 (million)
% 11.44/2.08 % (997297)------------------------------
% 11.44/2.08 % (997297)------------------------------
% 11.44/2.08 % (997299)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1046827036:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi)
% 11.44/2.08 % (997299)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 11.44/2.08 % (997299)Terminated due to inappropriate strategy.
% 11.44/2.08 % (997299)------------------------------
% 11.44/2.08 % (997299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.44/2.08 % (997299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.44/2.08 % (997299)CaDiCaL version: 2.1.3
% 11.44/2.08 % (997299)Termination reason: Inappropriate
% 11.44/2.08 % (997299)Time elapsed: 0.001 s
% 11.44/2.08 % (997299)Peak memory usage: 10 MB
% 11.44/2.08 % (997299)Instructions burned: 1 (million)
% 11.44/2.08 % (997299)------------------------------
% 11.44/2.08 % (997299)------------------------------
% 11.44/2.08 % (997301)ott-2_1_sil=16000:newcnf=on:random_seed=226065216:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi)
% 11.44/2.08 % (997283)Instruction limit reached!
% 11.44/2.08 % (997283)------------------------------
% 11.44/2.08 % (997283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.44/2.08 % (997283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.44/2.08 % (997283)CaDiCaL version: 2.1.3
% 11.44/2.08 % (997283)Termination reason: Instruction limit
% 11.44/2.08 % (997283)Termination phase: Saturation
% 11.44/2.08 % (997283)Time elapsed: 0.420 s
% 11.44/2.08 % (997283)Peak memory usage: 17 MB
% 11.44/2.08 % (997283)Instructions burned: 693 (million)
% 11.44/2.08 % (997303)ott+10_1_sil=32000:tgt=ground:random_seed=241319820:i=5114:av=off_2994 on theBenchmark for (2994ds/5114Mi)
% 11.44/2.08 % (997278)Instruction limit reached!
% 11.44/2.08 % (997278)------------------------------
% 11.44/2.08 % (997278)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.44/2.08 % (997278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.44/2.08 % (997278)CaDiCaL version: 2.1.3
% 11.44/2.08 % (997278)Termination reason: Instruction limit
% 11.44/2.08 % (997278)Termination phase: Saturation
% 11.44/2.08 % (997278)Time elapsed: 0.686 s
% 11.44/2.08 % (997278)Peak memory usage: 17 MB
% 11.44/2.08 % (997278)Instructions burned: 1179 (million)
% 11.44/2.08 % (997305)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=489339731:i=54282_2991 on theBenchmark for (2991ds/54282Mi)
% 11.44/2.08 % (997305)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 11.44/2.08 % (997305)Terminated due to inappropriate strategy.
% 11.44/2.08 % (997305)------------------------------
% 11.44/2.08 % (997305)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.44/2.08 % (997305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.44/2.08 % (997305)CaDiCaL version: 2.1.3
% 11.44/2.08 % (997305)Termination reason: Inappropriate
% 11.44/2.08 % (997305)Time elapsed: 0.001 s
% 11.44/2.08 % (997305)Peak memory usage: 10 MB
% 11.44/2.08 % (997305)Instructions burned: 1 (million)
% 11.44/2.08 % (997305)------------------------------
% 11.44/2.08 % (997305)------------------------------
% 11.44/2.08 % (997307)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1736802667:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi)
% 11.44/2.08 % (997301)Instruction limit reached!
% 11.44/2.08 % (997301)------------------------------
% 11.44/2.08 % (997301)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.44/2.08 % (997301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.44/2.08 % (997301)CaDiCaL version: 2.1.3
% 11.44/2.08 % (997301)Termination reason: Instruction limit
% 11.44/2.08 % (997301)Termination phase: Saturation
% 11.44/2.08 % (997301)Time elapsed: 0.555 s
% 11.44/2.08 % (997301)Peak memory usage: 18 MB
% 11.44/2.08 % (997301)Instructions burned: 869 (million)
% 11.44/2.08 % (997309)dis+21_1_sil=32000:sas=cadical:random_seed=1194571240:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi)
% 11.44/2.08 % (997294)Instruction limit reached!
% 11.44/2.08 % (997294)------------------------------
% 11.44/2.08 % (997294)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.44/2.08 % (997294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.44/2.08 % (997294)CaDiCaL version: 2.1.3
% 11.44/2.08 % (997294)Termination reason: Instruction limit
% 11.44/2.08 % (997294)Termination phase: Saturation
% 11.44/2.08 % (997294)Time elapsed: 0.824 s
% 11.44/2.08 % (997294)Peak memory usage: 31 MB
% 11.44/2.08 % (997294)Instructions burned: 1474 (million)
% 11.44/2.08 % (997311)ott+11_1_sil=16000:gs=on:random_seed=681334501:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi)
% 11.44/2.08 % (997309) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-997248-997309"...
% 11.44/2.08 % (997309)...printing done.
% 11.44/2.08 % (997309)Refutation found. Thanks to Tanya!
% 11.44/2.08 % SZS status Theorem for theBenchmark
% 11.44/2.08 % SZS output start Proof for theBenchmark
% 11.44/2.08 tff(func_def_0, type, q: $int > $int).
% 11.44/2.08 tff(func_def_1, type, p: $int > $int).
% 11.44/2.08 tff(func_def_2, type, n: $int).
% 11.44/2.08 tff(func_def_3, type, perm: $int > $int).
% 11.44/2.08 tff(func_def_9, type, sK0: $int).
% 11.44/2.08 tff(func_def_10, type, sK1: $int).
% 11.44/2.08 tff(f1,axiom,(
% 11.44/2.08 queens_p => ! [X0 : $int,X1 : $int] : (($lesseq(1,X0) & $lesseq(X0,n) & $lesseq($sum(1,X0),X1) & $lesseq(X1,n)) => (p(X0) != p(X1) & $sum(p(X0),X0) != $sum(p(X1),X1) & $difference(p(X0),X0) != $difference(p(X1),X1)))),
% 11.44/2.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p',queens_p)).
% 11.44/2.08 tff(f2,axiom,(
% 11.44/2.08 ! [X0 : $int] : perm(X0) = $difference($sum(1,n),X0)),
% 11.44/2.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p',permutation)).
% 11.44/2.08 tff(f3,axiom,(
% 11.44/2.08 ! [X0 : $int,X1 : $int] : (($lesseq(1,X0) & $lesseq(X0,n) & $lesseq($sum(1,X0),X1) & $lesseq(X1,n) & ($lesseq($sum(1,X0),X1) <=> $lesseq($sum(1,perm(X1)),perm(X0)))) => (q(X0) != q(X1) & $sum(q(X0),X0) != $sum(q(X1),X1) & $difference(q(X0),X0) != $difference(q(X1),X1))) => queens_q),
% 11.44/2.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p',queens_q)).
% 11.44/2.08 tff(f4,conjecture,(
% 11.44/2.08 (queens_p & ! [X0 : $int] : q(X0) = p(perm(X0))) => queens_q),
% 11.44/2.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p',queens_sym)).
% 11.44/2.08 tff(f5,negated_conjecture,(
% 11.44/2.08 ~((queens_p & ! [X0 : $int] : q(X0) = p(perm(X0))) => queens_q)),
% 11.44/2.08 inference(negated_conjecture,[status(cth)],[f4])).
% 11.44/2.08 tff(f6,axiom,(
% 11.44/2.08 ! [X0 : $int] : (($lesseq(1,X0) & $lesseq(X0,n)) => ($lesseq(1,perm(X0)) & $lesseq(perm(X0),n)))),
% 11.44/2.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p',permutation_range)).
% 11.44/2.08 tff(f8,plain,(
% 11.44/2.08 queens_p => ! [X0 : $int,X1 : $int] : ((~$less(X0,1) & ~$less(n,X0) & ~$less(X1,$sum(1,X0)) & ~$less(n,X1)) => (p(X0) != p(X1) & $sum(p(X0),X0) != $sum(p(X1),X1) & $sum(p(X0),$uminus(X0)) != $sum(p(X1),$uminus(X1))))),
% 11.44/2.08 inference(theory_normalization,[],[f1])).
% 11.44/2.08 tff(f9,plain,(
% 11.44/2.08 ! [X0 : $int] : perm(X0) = $sum($sum(1,n),$uminus(X0))),
% 11.44/2.08 inference(theory_normalization,[],[f2])).
% 11.44/2.08 tff(f10,plain,(
% 11.44/2.08 ! [X0 : $int,X1 : $int] : ((~$less(X0,1) & ~$less(n,X0) & ~$less(X1,$sum(1,X0)) & ~$less(n,X1) & (~$less(X1,$sum(1,X0)) <=> ~$less(perm(X0),$sum(1,perm(X1))))) => (q(X0) != q(X1) & $sum(q(X0),X0) != $sum(q(X1),X1) & $sum(q(X0),$uminus(X0)) != $sum(q(X1),$uminus(X1)))) => queens_q),
% 11.44/2.08 inference(theory_normalization,[],[f3])).
% 11.44/2.08 tff(f11,plain,(
% 11.44/2.08 ! [X0 : $int] : ((~$less(X0,1) & ~$less(n,X0)) => (~$less(perm(X0),1) & ~$less(n,perm(X0))))),
% 11.44/2.08 inference(theory_normalization,[],[f6])).
% 11.44/2.08 tff(f13,definition,(
% 11.44/2.08 ( ! [X0 : $int,X1 : $int] : ($sum(X0,X1) = $sum(X1,X0)) )),
% 11.44/2.08 introduced(theory,[tha_commutativity])).
% 11.44/2.08 tff(f14,definition,(
% 11.44/2.08 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum(X0,$sum(X1,X2)) = $sum($sum(X0,X1),X2)) )),
% 11.44/2.08 introduced(theory,[tha_associativity])).
% 11.44/2.08 tff(f16,definition,(
% 11.44/2.08 ( ! [X0 : $int,X1 : $int] : ($uminus($sum(X0,X1)) = $sum($uminus(X1),$uminus(X0))) )),
% 11.44/2.08 introduced(theory,[tha_inverse_op_op_inverses])).
% 11.44/2.08 tff(f19,definition,(
% 11.44/2.08 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X1,X2) | ~$less(X0,X1) | $less(X0,X2)) )),
% 11.44/2.08 introduced(theory,[tha_transitivity])).
% 11.44/2.08 tff(f22,definition,(
% 11.44/2.08 ( ! [X0 : $int,X1 : $int] : ($less(X1,$sum(X0,1)) | $less(X0,X1)) )),
% 11.44/2.08 introduced(theory,[tha_order_plus_one_dichotomy])).
% 11.44/2.08 tff(f23,definition,(
% 11.44/2.08 ( ! [X0 : $int] : ($uminus($uminus(X0)) = X0) )),
% 11.44/2.08 introduced(theory,[tha_minus_minus_x])).
% 11.44/2.08 tff(f25,plain,(
% 11.44/2.08 ! [X0 : $int,X1 : $int] : ((p(X0) != p(X1) & $sum(p(X0),X0) != $sum(p(X1),X1) & $sum(p(X0),$uminus(X0)) != $sum(p(X1),$uminus(X1))) | ($less(X0,1) | $less(n,X0) | $less(X1,$sum(1,X0)) | $less(n,X1))) | ~queens_p),
% 11.44/2.08 inference(ennf_transformation,[],[f8])).
% 11.44/2.08 tff(f26,plain,(
% 11.44/2.08 ! [X0 : $int,X1 : $int] : ((p(X0) != p(X1) & $sum(p(X0),X0) != $sum(p(X1),X1) & $sum(p(X0),$uminus(X0)) != $sum(p(X1),$uminus(X1))) | $less(X0,1) | $less(n,X0) | $less(X1,$sum(1,X0)) | $less(n,X1)) | ~queens_p),
% 11.44/2.08 inference(flattening,[],[f25])).
% 11.44/2.08 tff(f27,plain,(
% 11.44/2.08 queens_q | ? [X0 : $int,X1 : $int] : ((q(X0) = q(X1) | $sum(q(X0),X0) = $sum(q(X1),X1) | $sum(q(X0),$uminus(X0)) = $sum(q(X1),$uminus(X1))) & (~$less(X0,1) & ~$less(n,X0) & ~$less(X1,$sum(1,X0)) & ~$less(n,X1) & (~$less(X1,$sum(1,X0)) <=> ~$less(perm(X0),$sum(1,perm(X1))))))),
% 11.44/2.08 inference(ennf_transformation,[],[f10])).
% 11.44/2.08 tff(f28,plain,(
% 11.44/2.08 queens_q | ? [X0 : $int,X1 : $int] : ((q(X0) = q(X1) | $sum(q(X0),X0) = $sum(q(X1),X1) | $sum(q(X0),$uminus(X0)) = $sum(q(X1),$uminus(X1))) & ~$less(X0,1) & ~$less(n,X0) & ~$less(X1,$sum(1,X0)) & ~$less(n,X1) & (~$less(X1,$sum(1,X0)) <=> ~$less(perm(X0),$sum(1,perm(X1)))))),
% 11.44/2.08 inference(flattening,[],[f27])).
% 11.44/2.08 tff(f29,plain,(
% 11.44/2.08 ~queens_q & (queens_p & ! [X0 : $int] : q(X0) = p(perm(X0)))),
% 11.44/2.08 inference(ennf_transformation,[],[f5])).
% 11.44/2.08 tff(f30,plain,(
% 11.44/2.08 ~queens_q & queens_p & ! [X0 : $int] : q(X0) = p(perm(X0))),
% 11.44/2.08 inference(flattening,[],[f29])).
% 11.44/2.08 tff(f31,plain,(
% 11.44/2.08 ! [X0 : $int] : ((~$less(perm(X0),1) & ~$less(n,perm(X0))) | ($less(X0,1) | $less(n,X0)))),
% 11.44/2.08 inference(ennf_transformation,[],[f11])).
% 11.44/2.08 tff(f32,plain,(
% 11.44/2.08 ! [X0 : $int] : ((~$less(perm(X0),1) & ~$less(n,perm(X0))) | $less(X0,1) | $less(n,X0))),
% 11.44/2.08 inference(flattening,[],[f31])).
% 11.44/2.08 tff(f33,plain,(
% 11.44/2.08 queens_q | ? [X0 : $int,X1 : $int] : ((q(X0) = q(X1) | $sum(q(X0),X0) = $sum(q(X1),X1) | $sum(q(X0),$uminus(X0)) = $sum(q(X1),$uminus(X1))) & ~$less(X0,1) & ~$less(n,X0) & ~$less(X1,$sum(1,X0)) & ~$less(n,X1) & ((~$less(X1,$sum(1,X0)) | $less(perm(X0),$sum(1,perm(X1)))) & (~$less(perm(X0),$sum(1,perm(X1))) | $less(X1,$sum(1,X0)))))),
% 11.44/2.08 inference(nnf_transformation,[],[f28])).
% 11.44/2.08 tff(f34,plain,(
% 11.44/2.08 queens_q | ? [X0 : $int,X1 : $int] : ((q(X0) = q(X1) | $sum(q(X0),X0) = $sum(q(X1),X1) | $sum(q(X0),$uminus(X0)) = $sum(q(X1),$uminus(X1))) & ~$less(X0,1) & ~$less(n,X0) & ~$less(X1,$sum(1,X0)) & ~$less(n,X1) & (~$less(X1,$sum(1,X0)) | $less(perm(X0),$sum(1,perm(X1)))) & (~$less(perm(X0),$sum(1,perm(X1))) | $less(X1,$sum(1,X0))))),
% 11.44/2.08 inference(flattening,[],[f33])).
% 11.44/2.08 tff(f35,plain,(
% 11.44/2.08 queens_q | ((q(sK0) = q(sK1) | $sum(q(sK0),sK0) = $sum(q(sK1),sK1) | $sum(q(sK0),$uminus(sK0)) = $sum(q(sK1),$uminus(sK1))) & ~$less(sK0,1) & ~$less(n,sK0) & ~$less(sK1,$sum(1,sK0)) & ~$less(n,sK1) & (~$less(sK1,$sum(1,sK0)) | $less(perm(sK0),$sum(1,perm(sK1)))) & (~$less(perm(sK0),$sum(1,perm(sK1))) | $less(sK1,$sum(1,sK0))))),
% 11.44/2.08 inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(X1,sK1)],[f34])).
% 11.44/2.08 tff(f36,plain,(
% 11.44/2.08 ( ! [X0 : $int,X1 : $int] : ($sum(p(X0),$uminus(X0)) != $sum(p(X1),$uminus(X1)) | $less(X0,1) | $less(n,X0) | $less(X1,$sum(1,X0)) | $less(n,X1) | ~queens_p) )),
% 11.44/2.08 inference(cnf_transformation,[],[f26])).
% 11.44/2.08 tff(f37,plain,(
% 11.44/2.08 ( ! [X0 : $int,X1 : $int] : ($sum(p(X0),X0) != $sum(p(X1),X1) | $less(X0,1) | $less(n,X0) | $less(X1,$sum(1,X0)) | $less(n,X1) | ~queens_p) )),
% 11.44/2.08 inference(cnf_transformation,[],[f26])).
% 11.44/2.08 tff(f38,plain,(
% 11.44/2.08 ( ! [X0 : $int,X1 : $int] : (p(X0) != p(X1) | $less(X0,1) | $less(n,X0) | $less(X1,$sum(1,X0)) | $less(n,X1) | ~queens_p) )),
% 11.44/2.08 inference(cnf_transformation,[],[f26])).
% 11.44/2.08 tff(f39,plain,(
% 11.44/2.08 ( ! [X0 : $int] : (perm(X0) = $sum($sum(1,n),$uminus(X0))) )),
% 11.44/2.08 inference(cnf_transformation,[],[f9])).
% 11.44/2.08 tff(f40,plain,(
% 11.44/2.08 queens_q | ~$less(perm(sK0),$sum(1,perm(sK1))) | $less(sK1,$sum(1,sK0))),
% 11.44/2.08 inference(cnf_transformation,[],[f35])).
% 11.44/2.08 tff(f42,plain,(
% 11.44/2.08 queens_q | ~$less(n,sK1)),
% 11.44/2.08 inference(cnf_transformation,[],[f35])).
% 11.44/2.08 tff(f43,plain,(
% 11.44/2.08 queens_q | ~$less(sK1,$sum(1,sK0))),
% 11.44/2.08 inference(cnf_transformation,[],[f35])).
% 11.44/2.08 tff(f44,plain,(
% 11.44/2.08 queens_q | ~$less(n,sK0)),
% 11.44/2.08 inference(cnf_transformation,[],[f35])).
% 11.44/2.08 tff(f45,plain,(
% 11.44/2.08 queens_q | ~$less(sK0,1)),
% 11.44/2.08 inference(cnf_transformation,[],[f35])).
% 11.44/2.08 tff(f46,plain,(
% 11.44/2.08 queens_q | q(sK0) = q(sK1) | $sum(q(sK0),sK0) = $sum(q(sK1),sK1) | $sum(q(sK0),$uminus(sK0)) = $sum(q(sK1),$uminus(sK1))),
% 11.44/2.08 inference(cnf_transformation,[],[f35])).
% 11.44/2.08 tff(f47,plain,(
% 11.44/2.08 ( ! [X0 : $int] : (q(X0) = p(perm(X0))) )),
% 11.44/2.08 inference(cnf_transformation,[],[f30])).
% 11.44/2.08 tff(f48,plain,(
% 11.44/2.08 queens_p),
% 11.44/2.08 inference(cnf_transformation,[],[f30])).
% 11.44/2.08 tff(f49,plain,(
% 11.44/2.08 ~queens_q),
% 11.44/2.08 inference(cnf_transformation,[],[f30])).
% 11.44/2.08 tff(f50,plain,(
% 11.44/2.08 ( ! [X0 : $int] : (~$less(n,perm(X0)) | $less(X0,1) | $less(n,X0)) )),
% 11.44/2.08 inference(cnf_transformation,[],[f32])).
% 11.44/2.08 tff(f51,plain,(
% 11.44/2.08 ( ! [X0 : $int] : (~$less(perm(X0),1) | $less(X0,1) | $less(n,X0)) )),
% 11.44/2.08 inference(cnf_transformation,[],[f32])).
% 11.44/2.08 tff(f53,plain,(
% 11.44/2.08 ( ! [X0 : $int] : (q(X0) = p($sum($sum(1,n),$uminus(X0)))) )),
% 11.44/2.08 inference(definition_unfolding,[],[f47,f39])).
% 11.44/2.08 tff(f54,plain,(
% 11.44/2.08 queens_q | p($sum($sum(1,n),$uminus(sK0))) = p($sum($sum(1,n),$uminus(sK1))) | $sum(p($sum($sum(1,n),$uminus(sK0))),sK0) = $sum(p($sum($sum(1,n),$uminus(sK1))),sK1) | $sum(p($sum($sum(1,n),$uminus(sK0))),$uminus(sK0)) = $sum(p($sum($sum(1,n),$uminus(sK1))),$uminus(sK1))),
% 11.44/2.08 inference(definition_unfolding,[],[f46,f53,f53,f53,f53,f53,f53])).
% 11.44/2.08 tff(f56,plain,(
% 11.44/2.08 queens_q | ~$less($sum($sum(1,n),$uminus(sK0)),$sum(1,$sum($sum(1,n),$uminus(sK1)))) | $less(sK1,$sum(1,sK0))),
% 11.44/2.08 inference(definition_unfolding,[],[f40,f39,f39])).
% 11.44/2.08 tff(f57,plain,(
% 11.44/2.08 ( ! [X0 : $int] : (~$less($sum($sum(1,n),$uminus(X0)),1) | $less(X0,1) | $less(n,X0)) )),
% 11.44/2.08 inference(definition_unfolding,[],[f51,f39])).
% 11.44/2.08 tff(f58,plain,(
% 11.44/2.08 ( ! [X0 : $int] : (~$less(n,$sum($sum(1,n),$uminus(X0))) | $less(X0,1) | $less(n,X0)) )),
% 11.44/2.08 inference(definition_unfolding,[],[f50,f39])).
% 11.44/2.08 tff(f61,definition,(
% 11.44/2.08 spl2_1 <=> $less(sK1,$sum(1,sK0))),
% 11.44/2.08 introduced(definition,[new_symbols(definition,[spl2_1])],[avatar_definition])).
% 11.44/2.08 tff(f62,plain,(
% 11.44/2.08 ~$less(sK1,$sum(1,sK0)) | spl2_1),
% 11.44/2.08 inference(avatar_component_clause,[],[f61])).
% 11.44/2.08 tff(f65,definition,(
% 11.44/2.08 spl2_2 <=> $less($sum($sum(1,n),$uminus(sK0)),$sum(1,$sum($sum(1,n),$uminus(sK1))))),
% 11.44/2.08 introduced(definition,[new_symbols(definition,[spl2_2])],[avatar_definition])).
% 11.44/2.08 tff(f67,plain,(
% 11.44/2.08 ~$less($sum($sum(1,n),$uminus(sK0)),$sum(1,$sum($sum(1,n),$uminus(sK1)))) | spl2_2),
% 11.44/2.08 inference(avatar_component_clause,[],[f65])).
% 11.44/2.08 tff(f69,definition,(
% 11.44/2.08 spl2_3 <=> queens_q),
% 11.44/2.08 introduced(definition,[new_symbols(definition,[spl2_3])],[avatar_definition])).
% 11.44/2.08 tff(f72,plain,(
% 11.44/2.08 spl2_1 | ~spl2_2 | spl2_3),
% 11.44/2.08 inference(avatar_split_clause,[],[f56,f69,f65,f61])).
% 11.44/2.08 tff(f75,definition,(
% 11.44/2.08 spl2_4 <=> $less(n,sK1)),
% 11.44/2.08 introduced(definition,[new_symbols(definition,[spl2_4])],[avatar_definition])).
% 11.44/2.08 tff(f77,plain,(
% 11.44/2.08 ~$less(n,sK1) | spl2_4),
% 11.44/2.08 inference(avatar_component_clause,[],[f75])).
% 11.44/2.08 tff(f78,plain,(
% 11.44/2.08 ~spl2_4 | spl2_3),
% 11.44/2.08 inference(avatar_split_clause,[],[f42,f69,f75])).
% 11.44/2.08 tff(f79,plain,(
% 11.44/2.08 ~spl2_1 | spl2_3),
% 11.44/2.08 inference(avatar_split_clause,[],[f43,f69,f61])).
% 11.44/2.08 tff(f81,definition,(
% 11.44/2.08 spl2_5 <=> $less(n,sK0)),
% 11.44/2.08 introduced(definition,[new_symbols(definition,[spl2_5])],[avatar_definition])).
% 11.44/2.08 tff(f83,plain,(
% 11.44/2.08 ~$less(n,sK0) | spl2_5),
% 11.44/2.08 inference(avatar_component_clause,[],[f81])).
% 11.44/2.08 tff(f84,plain,(
% 11.44/2.08 ~spl2_5 | spl2_3),
% 11.44/2.08 inference(avatar_split_clause,[],[f44,f69,f81])).
% 11.44/2.08 tff(f86,definition,(
% 11.44/2.08 spl2_6 <=> $less(sK0,1)),
% 11.44/2.08 introduced(definition,[new_symbols(definition,[spl2_6])],[avatar_definition])).
% 11.44/2.08 tff(f88,plain,(
% 11.44/2.08 ~$less(sK0,1) | spl2_6),
% 11.44/2.08 inference(avatar_component_clause,[],[f86])).
% 11.44/2.08 tff(f89,plain,(
% 11.44/2.08 ~spl2_6 | spl2_3),
% 11.44/2.08 inference(avatar_split_clause,[],[f45,f69,f86])).
% 11.44/2.08 tff(f91,definition,(
% 11.44/2.08 spl2_7 <=> $sum(p($sum($sum(1,n),$uminus(sK0))),$uminus(sK0)) = $sum(p($sum($sum(1,n),$uminus(sK1))),$uminus(sK1))),
% 11.44/2.08 introduced(definition,[new_symbols(definition,[spl2_7])],[avatar_definition])).
% 11.44/2.08 tff(f93,plain,(
% 11.44/2.08 $sum(p($sum($sum(1,n),$uminus(sK0))),$uminus(sK0)) = $sum(p($sum($sum(1,n),$uminus(sK1))),$uminus(sK1)) | ~spl2_7),
% 11.44/2.08 inference(avatar_component_clause,[],[f91])).
% 11.44/2.08 tff(f95,definition,(
% 11.44/2.08 spl2_8 <=> $sum(p($sum($sum(1,n),$uminus(sK0))),sK0) = $sum(p($sum($sum(1,n),$uminus(sK1))),sK1)),
% 11.44/2.08 introduced(definition,[new_symbols(definition,[spl2_8])],[avatar_definition])).
% 11.44/2.08 tff(f97,plain,(
% 11.44/2.08 $sum(p($sum($sum(1,n),$uminus(sK0))),sK0) = $sum(p($sum($sum(1,n),$uminus(sK1))),sK1) | ~spl2_8),
% 11.44/2.08 inference(avatar_component_clause,[],[f95])).
% 11.44/2.08 tff(f99,definition,(
% 11.44/2.08 spl2_9 <=> p($sum($sum(1,n),$uminus(sK0))) = p($sum($sum(1,n),$uminus(sK1)))),
% 11.44/2.08 introduced(definition,[new_symbols(definition,[spl2_9])],[avatar_definition])).
% 11.44/2.08 tff(f101,plain,(
% 11.44/2.08 p($sum($sum(1,n),$uminus(sK0))) = p($sum($sum(1,n),$uminus(sK1))) | ~spl2_9),
% 11.44/2.08 inference(avatar_component_clause,[],[f99])).
% 11.44/2.08 tff(f102,plain,(
% 11.44/2.08 spl2_7 | spl2_8 | spl2_9 | spl2_3),
% 11.44/2.08 inference(avatar_split_clause,[],[f54,f69,f99,f95,f91])).
% 11.44/2.08 tff(f104,definition,(
% 11.44/2.08 spl2_10 <=> queens_p),
% 11.44/2.08 introduced(definition,[new_symbols(definition,[spl2_10])],[avatar_definition])).
% 11.44/2.08 tff(f108,definition,(
% 11.44/2.08 spl2_11 <=> ! [X0 : $int,X1 : $int] : ($sum(p(X0),$uminus(X0)) != $sum(p(X1),$uminus(X1)) | $less(n,X1) | $less(X1,$sum(1,X0)) | $less(n,X0) | $less(X0,1))),
% 11.44/2.08 introduced(definition,[new_symbols(definition,[spl2_11])],[avatar_definition])).
% 11.44/2.08 tff(f109,plain,(
% 11.44/2.08 ( ! [X0 : $int,X1 : $int] : ($less(X1,$sum(1,X0)) | $less(n,X1) | $sum(p(X0),$uminus(X0)) != $sum(p(X1),$uminus(X1)) | $less(n,X0) | $less(X0,1)) ) | ~spl2_11),
% 11.44/2.08 inference(avatar_component_clause,[],[f108])).
% 11.44/2.08 tff(f110,plain,(
% 11.44/2.08 ~spl2_10 | spl2_11),
% 11.44/2.08 inference(avatar_split_clause,[],[f36,f108,f104])).
% 11.44/2.08 tff(f112,definition,(
% 11.44/2.08 spl2_12 <=> ! [X0 : $int,X1 : $int] : ($sum(p(X0),X0) != $sum(p(X1),X1) | $less(n,X1) | $less(X1,$sum(1,X0)) | $less(n,X0) | $less(X0,1))),
% 11.44/2.08 introduced(definition,[new_symbols(definition,[spl2_12])],[avatar_definition])).
% 11.44/2.08 tff(f113,plain,(
% 11.44/2.08 ( ! [X0 : $int,X1 : $int] : ($sum(p(X0),X0) != $sum(p(X1),X1) | $less(n,X1) | $less(X1,$sum(1,X0)) | $less(n,X0) | $less(X0,1)) ) | ~spl2_12),
% 11.44/2.08 inference(avatar_component_clause,[],[f112])).
% 11.44/2.08 tff(f114,plain,(
% 11.44/2.08 ~spl2_10 | spl2_12),
% 11.44/2.08 inference(avatar_split_clause,[],[f37,f112,f104])).
% 11.44/2.08 tff(f116,definition,(
% 11.44/2.08 spl2_13 <=> ! [X0 : $int,X1 : $int] : (p(X0) != p(X1) | $less(n,X1) | $less(X1,$sum(1,X0)) | $less(n,X0) | $less(X0,1))),
% 11.44/2.08 introduced(definition,[new_symbols(definition,[spl2_13])],[avatar_definition])).
% 11.44/2.08 tff(f117,plain,(
% 11.44/2.08 ( ! [X0 : $int,X1 : $int] : ($less(X1,$sum(1,X0)) | $less(n,X1) | p(X0) != p(X1) | $less(n,X0) | $less(X0,1)) ) | ~spl2_13),
% 11.44/2.09 inference(avatar_component_clause,[],[f116])).
% 11.44/2.09 tff(f118,plain,(
% 11.44/2.09 ~spl2_10 | spl2_13),
% 11.44/2.09 inference(avatar_split_clause,[],[f38,f116,f104])).
% 11.44/2.09 tff(f119,plain,(
% 11.44/2.09 spl2_10),
% 11.44/2.09 inference(avatar_split_clause,[],[f48,f104])).
% 11.44/2.09 tff(f120,plain,(
% 11.44/2.09 ~spl2_3),
% 11.44/2.09 inference(avatar_split_clause,[],[f49,f69])).
% 11.44/2.09 tff(f139,plain,(
% 11.44/2.09 p($sum($sum(1,n),$uminus(sK0))) = p($sum($uminus(sK1),$sum(1,n))) | ~spl2_9),
% 11.44/2.09 inference(superposition,[],[f101,f13])).
% 11.44/2.09 tff(f144,plain,(
% 11.44/2.09 p($sum($uminus(sK1),$sum(1,n))) = p($sum($uminus(sK0),$sum(1,n))) | ~spl2_9),
% 11.44/2.09 inference(forward_demodulation,[],[f139,f13])).
% 11.44/2.09 tff(f169,plain,(
% 11.44/2.09 ( ! [X0 : $int,X1 : $int] : ($less(X1,$sum(1,X0)) | $less(X0,X1)) )),
% 11.44/2.09 inference(superposition,[],[f22,f13])).
% 11.44/2.09 tff(f193,plain,(
% 11.44/2.09 ( ! [X0 : $int,X1 : $int] : ($uminus($sum($uminus(X0),X1)) = $sum($uminus(X1),X0)) )),
% 11.44/2.09 inference(superposition,[],[f16,f23])).
% 11.44/2.09 tff(f239,plain,(
% 11.44/2.09 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum($sum(X0,X1),X2) = $sum(X1,$sum(X0,X2))) )),
% 11.44/2.09 inference(superposition,[],[f14,f13])).
% 11.44/2.09 tff(f248,plain,(
% 11.44/2.09 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum(X0,$sum(X1,X2)) = $sum(X1,$sum(X2,X0))) )),
% 11.44/2.09 inference(superposition,[],[f14,f13])).
% 11.44/2.09 tff(f275,plain,(
% 11.44/2.09 ( ! [X0 : $int] : (~$less($sum(1,$sum(n,$uminus(X0))),1) | $less(X0,1) | $less(n,X0)) )),
% 11.44/2.09 inference(forward_demodulation,[],[f57,f14])).
% 11.44/2.09 tff(f276,plain,(
% 11.44/2.09 ( ! [X0 : $int] : (~$less(n,$sum(1,$sum(n,$uminus(X0)))) | $less(X0,1) | $less(n,X0)) )),
% 11.44/2.09 inference(forward_demodulation,[],[f58,f14])).
% 11.44/2.09 tff(f283,plain,(
% 11.44/2.09 ( ! [X0 : $int] : (~$less($sum(1,$sum(n,X0)),1) | $less($uminus(X0),1) | $less(n,$uminus(X0))) )),
% 11.44/2.09 inference(superposition,[],[f275,f23])).
% 11.44/2.09 tff(f293,plain,(
% 11.44/2.09 ~$less($sum($sum(1,n),$uminus(sK0)),$sum(1,$sum($uminus(sK1),$sum(1,n)))) | spl2_2),
% 11.44/2.09 inference(forward_demodulation,[],[f67,f13])).
% 11.44/2.09 tff(f294,plain,(
% 11.44/2.09 ~$less($sum($uminus(sK0),$sum(1,n)),$sum(1,$sum($uminus(sK1),$sum(1,n)))) | spl2_2),
% 11.44/2.09 inference(forward_demodulation,[],[f293,f13])).
% 11.44/2.09 tff(f326,plain,(
% 11.44/2.09 $less(n,$sum($uminus(sK0),$sum(1,n))) | p($sum($uminus(sK1),$sum(1,n))) != p($sum($uminus(sK0),$sum(1,n))) | $less(n,$sum($uminus(sK1),$sum(1,n))) | $less($sum($uminus(sK1),$sum(1,n)),1) | (spl2_2 | ~spl2_13)),
% 11.44/2.09 inference(resolution,[],[f117,f294])).
% 11.44/2.09 tff(f335,plain,(
% 11.44/2.09 $less(n,$sum($uminus(sK0),$sum(1,n))) | $less(n,$sum($uminus(sK1),$sum(1,n))) | $less($sum($uminus(sK1),$sum(1,n)),1) | (spl2_2 | ~spl2_9 | ~spl2_13)),
% 11.44/2.09 inference(forward_subsumption_resolution,[],[f326,f144])).
% 11.44/2.09 tff(f340,definition,(
% 11.44/2.09 spl2_16 <=> $less($sum($uminus(sK1),$sum(1,n)),1)),
% 11.44/2.09 introduced(definition,[new_symbols(definition,[spl2_16])],[avatar_definition])).
% 11.44/2.09 tff(f342,plain,(
% 11.44/2.09 $less($sum($uminus(sK1),$sum(1,n)),1) | ~spl2_16),
% 11.44/2.09 inference(avatar_component_clause,[],[f340])).
% 11.44/2.09 tff(f344,definition,(
% 11.44/2.09 spl2_17 <=> $less(n,$sum($uminus(sK1),$sum(1,n)))),
% 11.44/2.09 introduced(definition,[new_symbols(definition,[spl2_17])],[avatar_definition])).
% 11.44/2.09 tff(f346,plain,(
% 11.44/2.09 $less(n,$sum($uminus(sK1),$sum(1,n))) | ~spl2_17),
% 11.44/2.09 inference(avatar_component_clause,[],[f344])).
% 11.44/2.09 tff(f348,definition,(
% 11.44/2.09 spl2_18 <=> $less(n,$sum($uminus(sK0),$sum(1,n)))),
% 11.44/2.09 introduced(definition,[new_symbols(definition,[spl2_18])],[avatar_definition])).
% 11.44/2.09 tff(f349,plain,(
% 11.44/2.09 ~$less(n,$sum($uminus(sK0),$sum(1,n))) | spl2_18),
% 11.44/2.09 inference(avatar_component_clause,[],[f348])).
% 11.44/2.09 tff(f350,plain,(
% 11.44/2.09 $less(n,$sum($uminus(sK0),$sum(1,n))) | ~spl2_18),
% 11.44/2.09 inference(avatar_component_clause,[],[f348])).
% 11.44/2.09 tff(f351,plain,(
% 11.44/2.09 spl2_16 | spl2_17 | spl2_18 | spl2_2 | ~spl2_9 | ~spl2_13),
% 11.44/2.09 inference(avatar_split_clause,[],[f335,f116,f99,f65,f348,f344,f340])).
% 11.44/2.09 tff(f354,plain,(
% 11.44/2.09 ( ! [X0 : $int,X1 : $int] : ($sum(p(X0),X0) != $sum(X1,p(X1)) | $less(n,X1) | $less(X1,$sum(1,X0)) | $less(n,X0) | $less(X0,1)) ) | ~spl2_12),
% 11.44/2.09 inference(forward_demodulation,[],[f113,f13])).
% 11.44/2.09 tff(f355,plain,(
% 11.44/2.09 ( ! [X0 : $int,X1 : $int] : ($less(X1,$sum(1,X0)) | $less(n,X1) | $sum(X1,p(X1)) != $sum(X0,p(X0)) | $less(n,X0) | $less(X0,1)) ) | ~spl2_12),
% 11.44/2.09 inference(forward_demodulation,[],[f354,f13])).
% 11.44/2.09 tff(f361,plain,(
% 11.44/2.09 $less(n,$sum($uminus(sK0),$sum(1,n))) | $sum($sum($uminus(sK0),$sum(1,n)),p($sum($uminus(sK0),$sum(1,n)))) != $sum($sum($uminus(sK1),$sum(1,n)),p($sum($uminus(sK1),$sum(1,n)))) | $less(n,$sum($uminus(sK1),$sum(1,n))) | $less($sum($uminus(sK1),$sum(1,n)),1) | (spl2_2 | ~spl2_12)),
% 11.44/2.09 inference(resolution,[],[f355,f294])).
% 11.44/2.09 tff(f382,plain,(
% 11.44/2.09 $less(n,$sum($uminus(sK0),$sum(1,n))) | $sum(p($sum($uminus(sK1),$sum(1,n))),$uminus($sum($uminus(sK1),$sum(1,n)))) != $sum(p($sum($uminus(sK0),$sum(1,n))),$uminus($sum($uminus(sK0),$sum(1,n)))) | $less(n,$sum($uminus(sK1),$sum(1,n))) | $less($sum($uminus(sK1),$sum(1,n)),1) | (spl2_2 | ~spl2_11)),
% 11.44/2.09 inference(resolution,[],[f109,f294])).
% 11.44/2.09 tff(f853,plain,(
% 11.44/2.09 $less(sK0,sK1) | spl2_1),
% 11.44/2.09 inference(resolution,[],[f169,f62])).
% 11.44/2.09 tff(f2162,plain,(
% 11.44/2.09 $less(n,$sum(1,$sum(n,$uminus(sK0)))) | ~spl2_18),
% 11.44/2.09 inference(superposition,[],[f350,f248])).
% 11.44/2.09 tff(f2817,definition,(
% 11.44/2.09 spl2_60 <=> $less(sK1,1)),
% 11.44/2.09 introduced(definition,[new_symbols(definition,[spl2_60])],[avatar_definition])).
% 11.44/2.09 tff(f2819,plain,(
% 11.44/2.09 $less(sK1,1) | ~spl2_60),
% 11.44/2.09 inference(avatar_component_clause,[],[f2817])).
% 11.44/2.09 tff(f4637,plain,(
% 11.44/2.09 $less(sK0,1) | $less(n,sK0) | ~spl2_18),
% 11.44/2.09 inference(resolution,[],[f2162,f276])).
% 11.44/2.09 tff(f4647,plain,(
% 11.44/2.09 $less(n,sK0) | (spl2_6 | ~spl2_18)),
% 11.44/2.09 inference(forward_subsumption_resolution,[],[f4637,f88])).
% 11.44/2.09 tff(f4650,plain,(
% 11.44/2.09 $false | (spl2_5 | spl2_6 | ~spl2_18)),
% 11.44/2.09 inference(forward_subsumption_resolution,[],[f4647,f83])).
% 11.44/2.09 tff(f4651,plain,(
% 11.44/2.09 spl2_5 | spl2_6 | ~spl2_18),
% 11.44/2.09 inference(avatar_contradiction_clause,[],[f4650])).
% 11.44/2.09 tff(f4652,plain,(
% 11.44/2.09 $less(n,$sum(1,$sum(n,$uminus(sK1)))) | ~spl2_17),
% 11.44/2.09 inference(forward_demodulation,[],[f346,f248])).
% 11.44/2.09 tff(f4653,plain,(
% 11.44/2.09 ~$less(n,$sum(1,$sum(n,$uminus(sK0)))) | spl2_18),
% 11.44/2.09 inference(forward_demodulation,[],[f349,f248])).
% 11.44/2.09 tff(f4654,plain,(
% 11.44/2.09 $less(n,$sum(1,$sum(n,$uminus(sK0)))) | $sum(p($sum($uminus(sK1),$sum(1,n))),$uminus($sum($uminus(sK1),$sum(1,n)))) != $sum(p($sum($uminus(sK0),$sum(1,n))),$uminus($sum($uminus(sK0),$sum(1,n)))) | $less(n,$sum($uminus(sK1),$sum(1,n))) | $less($sum($uminus(sK1),$sum(1,n)),1) | (spl2_2 | ~spl2_11)),
% 11.44/2.09 inference(forward_demodulation,[],[f382,f248])).
% 11.44/2.09 tff(f4655,plain,(
% 11.44/2.09 $less(n,$sum(1,$sum(n,$uminus(sK0)))) | $sum($sum($uminus(sK0),$sum(1,n)),p($sum($uminus(sK0),$sum(1,n)))) != $sum($sum($uminus(sK1),$sum(1,n)),p($sum($uminus(sK1),$sum(1,n)))) | $less(n,$sum($uminus(sK1),$sum(1,n))) | $less($sum($uminus(sK1),$sum(1,n)),1) | (spl2_2 | ~spl2_12)),
% 11.44/2.09 inference(forward_demodulation,[],[f361,f248])).
% 11.44/2.09 tff(f4668,plain,(
% 11.44/2.09 $sum(p($sum($uminus(sK1),$sum(1,n))),$uminus($sum($uminus(sK1),$sum(1,n)))) != $sum(p($sum($uminus(sK0),$sum(1,n))),$sum($uminus($sum(1,n)),sK0)) | $less(n,$sum(1,$sum(n,$uminus(sK0)))) | $less(n,$sum($uminus(sK1),$sum(1,n))) | $less($sum($uminus(sK1),$sum(1,n)),1) | (spl2_2 | ~spl2_11)),
% 11.44/2.09 inference(forward_demodulation,[],[f4654,f193])).
% 11.44/2.09 tff(f4669,plain,(
% 11.44/2.09 $sum($sum($uminus(sK0),$sum(1,n)),p($sum($uminus(sK0),$sum(1,n)))) != $sum($uminus(sK1),$sum($sum(1,n),p($sum($uminus(sK1),$sum(1,n))))) | $less(n,$sum(1,$sum(n,$uminus(sK0)))) | $less(n,$sum($uminus(sK1),$sum(1,n))) | $less($sum($uminus(sK1),$sum(1,n)),1) | (spl2_2 | ~spl2_12)),
% 11.44/2.09 inference(forward_demodulation,[],[f4655,f14])).
% 11.44/2.09 tff(f4682,plain,(
% 11.44/2.09 $sum(p($sum($uminus(sK1),$sum(1,n))),$uminus($sum($uminus(sK1),$sum(1,n)))) != $sum($sum($uminus($sum(1,n)),sK0),p($sum($uminus(sK0),$sum(1,n)))) | $less(n,$sum(1,$sum(n,$uminus(sK0)))) | $less(n,$sum($uminus(sK1),$sum(1,n))) | $less($sum($uminus(sK1),$sum(1,n)),1) | (spl2_2 | ~spl2_11)),
% 11.44/2.09 inference(forward_demodulation,[],[f4668,f13])).
% 11.44/2.09 tff(f4683,plain,(
% 11.44/2.09 $sum($sum($uminus(sK0),$sum(1,n)),p($sum($uminus(sK0),$sum(1,n)))) != $sum($uminus(sK1),$sum(1,$sum(n,p($sum($uminus(sK1),$sum(1,n)))))) | $less(n,$sum(1,$sum(n,$uminus(sK0)))) | $less(n,$sum($uminus(sK1),$sum(1,n))) | $less($sum($uminus(sK1),$sum(1,n)),1) | (spl2_2 | ~spl2_12)),
% 11.44/2.09 inference(forward_demodulation,[],[f4669,f14])).
% 11.44/2.09 tff(f4686,definition,(
% 11.44/2.09 spl2_89 <=> $less(n,$sum(1,$sum(n,$uminus(sK0))))),
% 11.44/2.09 introduced(definition,[new_symbols(definition,[spl2_89])],[avatar_definition])).
% 11.44/2.09 tff(f4687,plain,(
% 11.44/2.09 ~$less(n,$sum(1,$sum(n,$uminus(sK0)))) | spl2_89),
% 11.44/2.09 inference(avatar_component_clause,[],[f4686])).
% 11.44/2.09 tff(f4703,plain,(
% 11.44/2.09 $sum(p($sum($uminus(sK1),$sum(1,n))),$uminus($sum($uminus(sK1),$sum(1,n)))) != $sum($uminus($sum(1,n)),$sum(sK0,p($sum($uminus(sK0),$sum(1,n))))) | $less(n,$sum(1,$sum(n,$uminus(sK0)))) | $less(n,$sum($uminus(sK1),$sum(1,n))) | $less($sum($uminus(sK1),$sum(1,n)),1) | (spl2_2 | ~spl2_11)),
% 11.44/2.09 inference(forward_demodulation,[],[f4682,f14])).
% 11.44/2.09 tff(f4704,plain,(
% 11.44/2.09 $sum($sum($uminus(sK0),$sum(1,n)),p($sum($uminus(sK0),$sum(1,n)))) != $sum(1,$sum($sum(n,p($sum($uminus(sK1),$sum(1,n)))),$uminus(sK1))) | $less(n,$sum(1,$sum(n,$uminus(sK0)))) | $less(n,$sum($uminus(sK1),$sum(1,n))) | $less($sum($uminus(sK1),$sum(1,n)),1) | (spl2_2 | ~spl2_12)),
% 11.44/2.09 inference(forward_demodulation,[],[f4683,f248])).
% 11.44/2.09 tff(f4720,definition,(
% 11.44/2.09 spl2_93 <=> $less(n,$sum(1,$sum(n,$uminus(sK1))))),
% 11.44/2.09 introduced(definition,[new_symbols(definition,[spl2_93])],[avatar_definition])).
% 11.44/2.09 tff(f4722,plain,(
% 11.44/2.09 $less(n,$sum(1,$sum(n,$uminus(sK1)))) | ~spl2_93),
% 11.44/2.09 inference(avatar_component_clause,[],[f4720])).
% 11.44/2.09 tff(f4728,plain,(
% 11.44/2.09 $sum(p($sum($uminus(sK1),$sum(1,n))),$uminus($sum($uminus(sK1),$sum(1,n)))) != $sum(sK0,$sum(p($sum($uminus(sK0),$sum(1,n))),$uminus($sum(1,n)))) | $less(n,$sum(1,$sum(n,$uminus(sK0)))) | $less(n,$sum($uminus(sK1),$sum(1,n))) | $less($sum($uminus(sK1),$sum(1,n)),1) | (spl2_2 | ~spl2_11)),
% 11.44/2.09 inference(forward_demodulation,[],[f4703,f248])).
% 11.44/2.09 tff(f4729,plain,(
% 11.44/2.09 $sum($sum($uminus(sK0),$sum(1,n)),p($sum($uminus(sK0),$sum(1,n)))) != $sum(1,$sum($uminus(sK1),$sum(n,p($sum($uminus(sK1),$sum(1,n)))))) | $less(n,$sum(1,$sum(n,$uminus(sK0)))) | $less(n,$sum($uminus(sK1),$sum(1,n))) | $less($sum($uminus(sK1),$sum(1,n)),1) | (spl2_2 | ~spl2_12)),
% 11.44/2.09 inference(forward_demodulation,[],[f4704,f13])).
% 11.44/2.09 tff(f4737,plain,(
% 11.44/2.09 $sum(p($sum($uminus(sK1),$sum(1,n))),$uminus($sum($uminus(sK1),$sum(1,n)))) != $sum(sK0,$sum($uminus($sum(1,n)),p($sum($uminus(sK0),$sum(1,n))))) | $less(n,$sum(1,$sum(n,$uminus(sK0)))) | $less(n,$sum($uminus(sK1),$sum(1,n))) | $less($sum($uminus(sK1),$sum(1,n)),1) | (spl2_2 | ~spl2_11)),
% 11.44/2.09 inference(forward_demodulation,[],[f4728,f13])).
% 11.44/2.09 tff(f4738,plain,(
% 11.44/2.09 $sum($sum($uminus(sK0),$sum(1,n)),p($sum($uminus(sK0),$sum(1,n)))) != $sum(1,$sum(n,$sum(p($sum($uminus(sK1),$sum(1,n))),$uminus(sK1)))) | $less(n,$sum(1,$sum(n,$uminus(sK0)))) | $less(n,$sum($uminus(sK1),$sum(1,n))) | $less($sum($uminus(sK1),$sum(1,n)),1) | (spl2_2 | ~spl2_12)),
% 11.44/2.09 inference(forward_demodulation,[],[f4729,f248])).
% 11.44/2.09 tff(f4750,plain,(
% 11.44/2.09 $sum($sum($uminus(sK0),$sum(1,n)),p($sum($uminus(sK0),$sum(1,n)))) != $sum(1,$sum(n,$sum($uminus(sK1),p($sum($uminus(sK1),$sum(1,n)))))) | $less(n,$sum(1,$sum(n,$uminus(sK0)))) | $less(n,$sum($uminus(sK1),$sum(1,n))) | $less($sum($uminus(sK1),$sum(1,n)),1) | (spl2_2 | ~spl2_12)),
% 11.44/2.09 inference(forward_demodulation,[],[f4738,f13])).
% 11.44/2.09 tff(f4810,plain,(
% 11.44/2.09 spl2_93 | ~spl2_17),
% 11.44/2.09 inference(avatar_split_clause,[],[f4652,f344,f4720])).
% 11.44/2.09 tff(f4811,plain,(
% 11.44/2.09 ~spl2_89 | spl2_18),
% 11.44/2.09 inference(avatar_split_clause,[],[f4653,f348,f4686])).
% 11.44/2.09 tff(f5566,plain,(
% 11.44/2.09 $less(sK1,1) | $less(n,sK1) | ~spl2_93),
% 11.44/2.09 inference(resolution,[],[f4722,f276])).
% 11.44/2.09 tff(f6152,plain,(
% 11.44/2.09 $sum(p($sum($sum(1,n),$uminus(sK0))),$uminus(sK0)) = $sum($uminus(sK1),p($sum($sum(1,n),$uminus(sK1)))) | ~spl2_7),
% 11.44/2.09 inference(forward_demodulation,[],[f93,f13])).
% 11.44/2.09 tff(f6154,plain,(
% 11.44/2.09 $less($sum(1,$sum(n,$uminus(sK1))),1) | ~spl2_16),
% 11.44/2.09 inference(forward_demodulation,[],[f342,f248])).
% 11.44/2.09 tff(f6239,plain,(
% 11.44/2.09 $sum(p($sum($uminus(sK1),$sum(1,n))),$uminus($sum($uminus(sK1),$sum(1,n)))) != $sum(sK0,$sum($uminus($sum(1,n)),p($sum($uminus(sK0),$sum(1,n))))) | $less(n,$sum($uminus(sK1),$sum(1,n))) | $less($sum($uminus(sK1),$sum(1,n)),1) | (spl2_2 | ~spl2_11 | spl2_89)),
% 11.44/2.09 inference(forward_subsumption_resolution,[],[f4737,f4687])).
% 11.44/2.09 tff(f6240,plain,(
% 11.44/2.09 $sum($sum($uminus(sK0),$sum(1,n)),p($sum($uminus(sK0),$sum(1,n)))) != $sum(1,$sum(n,$sum($uminus(sK1),p($sum($uminus(sK1),$sum(1,n)))))) | $less(n,$sum($uminus(sK1),$sum(1,n))) | $less($sum($uminus(sK1),$sum(1,n)),1) | (spl2_2 | ~spl2_12 | spl2_89)),
% 11.44/2.09 inference(forward_subsumption_resolution,[],[f4750,f4687])).
% 11.44/2.09 tff(f6241,plain,(
% 11.44/2.09 $sum(p($sum($sum(1,n),$uminus(sK0))),$uminus(sK0)) = $sum($uminus(sK1),p($sum($uminus(sK1),$sum(1,n)))) | ~spl2_7),
% 11.44/2.09 inference(forward_demodulation,[],[f6152,f13])).
% 11.44/2.09 tff(f6255,plain,(
% 11.44/2.09 $sum(p($sum($uminus(sK1),$sum(1,n))),$uminus($sum($uminus(sK1),$sum(1,n)))) != $sum(sK0,$sum($uminus($sum(1,n)),p($sum(1,$sum(n,$uminus(sK0)))))) | $less(n,$sum($uminus(sK1),$sum(1,n))) | $less($sum($uminus(sK1),$sum(1,n)),1) | (spl2_2 | ~spl2_11 | spl2_89)),
% 11.44/2.09 inference(forward_demodulation,[],[f6239,f248])).
% 11.44/2.09 tff(f6256,plain,(
% 11.44/2.09 $sum($sum($uminus(sK0),$sum(1,n)),p($sum($uminus(sK0),$sum(1,n)))) != $sum(1,$sum(n,$sum($uminus(sK1),p($sum(1,$sum(n,$uminus(sK1))))))) | $less(n,$sum($uminus(sK1),$sum(1,n))) | $less($sum($uminus(sK1),$sum(1,n)),1) | (spl2_2 | ~spl2_12 | spl2_89)),
% 11.44/2.09 inference(forward_demodulation,[],[f6240,f248])).
% 11.44/2.09 tff(f6257,plain,(
% 11.44/2.09 $sum(p($sum($sum(1,n),$uminus(sK0))),$uminus(sK0)) = $sum($uminus(sK1),p($sum(1,$sum(n,$uminus(sK1))))) | ~spl2_7),
% 11.44/2.09 inference(forward_demodulation,[],[f6241,f248])).
% 11.44/2.09 tff(f6273,plain,(
% 11.44/2.09 $sum(p($sum($uminus(sK1),$sum(1,n))),$sum($uminus($sum(1,n)),sK1)) != $sum(sK0,$sum($uminus($sum(1,n)),p($sum(1,$sum(n,$uminus(sK0)))))) | $less(n,$sum($uminus(sK1),$sum(1,n))) | $less($sum($uminus(sK1),$sum(1,n)),1) | (spl2_2 | ~spl2_11 | spl2_89)),
% 11.44/2.09 inference(forward_demodulation,[],[f6255,f193])).
% 11.44/2.09 tff(f6274,plain,(
% 11.44/2.09 $sum(1,$sum(n,$sum($uminus(sK1),p($sum(1,$sum(n,$uminus(sK1))))))) != $sum($uminus(sK0),$sum($sum(1,n),p($sum($uminus(sK0),$sum(1,n))))) | $less(n,$sum($uminus(sK1),$sum(1,n))) | $less($sum($uminus(sK1),$sum(1,n)),1) | (spl2_2 | ~spl2_12 | spl2_89)),
% 11.44/2.09 inference(forward_demodulation,[],[f6256,f14])).
% 11.44/2.09 tff(f6275,plain,(
% 11.44/2.09 $sum($uminus(sK0),p($sum($sum(1,n),$uminus(sK0)))) = $sum($uminus(sK1),p($sum(1,$sum(n,$uminus(sK1))))) | ~spl2_7),
% 11.44/2.09 inference(forward_demodulation,[],[f6257,f13])).
% 11.44/2.09 tff(f6282,plain,(
% 11.44/2.09 $sum($sum($uminus($sum(1,n)),sK1),p($sum($uminus(sK1),$sum(1,n)))) != $sum(sK0,$sum($uminus($sum(1,n)),p($sum(1,$sum(n,$uminus(sK0)))))) | $less(n,$sum($uminus(sK1),$sum(1,n))) | $less($sum($uminus(sK1),$sum(1,n)),1) | (spl2_2 | ~spl2_11 | spl2_89)),
% 11.44/2.09 inference(forward_demodulation,[],[f6273,f13])).
% 11.44/2.09 tff(f6283,plain,(
% 11.44/2.09 $sum(1,$sum(n,$sum($uminus(sK1),p($sum(1,$sum(n,$uminus(sK1))))))) != $sum($uminus(sK0),$sum(1,$sum(n,p($sum($uminus(sK0),$sum(1,n)))))) | $less(n,$sum($uminus(sK1),$sum(1,n))) | $less($sum($uminus(sK1),$sum(1,n)),1) | (spl2_2 | ~spl2_12 | spl2_89)),
% 11.44/2.09 inference(forward_demodulation,[],[f6274,f14])).
% 11.44/2.09 tff(f6284,plain,(
% 11.44/2.09 $sum($uminus(sK0),p($sum($uminus(sK0),$sum(1,n)))) = $sum($uminus(sK1),p($sum(1,$sum(n,$uminus(sK1))))) | ~spl2_7),
% 11.44/2.09 inference(forward_demodulation,[],[f6275,f13])).
% 11.44/2.09 tff(f6288,plain,(
% 11.44/2.09 $sum($uminus($sum(1,n)),$sum(sK1,p($sum($uminus(sK1),$sum(1,n))))) != $sum(sK0,$sum($uminus($sum(1,n)),p($sum(1,$sum(n,$uminus(sK0)))))) | $less(n,$sum($uminus(sK1),$sum(1,n))) | $less($sum($uminus(sK1),$sum(1,n)),1) | (spl2_2 | ~spl2_11 | spl2_89)),
% 11.44/2.09 inference(forward_demodulation,[],[f6282,f14])).
% 11.44/2.09 tff(f6289,plain,(
% 11.44/2.09 $sum(1,$sum(n,$sum($uminus(sK1),p($sum(1,$sum(n,$uminus(sK1))))))) != $sum(1,$sum($sum(n,p($sum($uminus(sK0),$sum(1,n)))),$uminus(sK0))) | $less(n,$sum($uminus(sK1),$sum(1,n))) | $less($sum($uminus(sK1),$sum(1,n)),1) | (spl2_2 | ~spl2_12 | spl2_89)),
% 11.44/2.09 inference(forward_demodulation,[],[f6283,f248])).
% 11.44/2.09 tff(f6290,plain,(
% 11.44/2.09 $sum($uminus(sK0),p($sum(1,$sum(n,$uminus(sK0))))) = $sum($uminus(sK1),p($sum(1,$sum(n,$uminus(sK1))))) | ~spl2_7),
% 11.44/2.09 inference(forward_demodulation,[],[f6284,f248])).
% 11.44/2.09 tff(f6293,plain,(
% 11.44/2.09 $sum(sK1,$sum(p($sum($uminus(sK1),$sum(1,n))),$uminus($sum(1,n)))) != $sum(sK0,$sum($uminus($sum(1,n)),p($sum(1,$sum(n,$uminus(sK0)))))) | $less(n,$sum($uminus(sK1),$sum(1,n))) | $less($sum($uminus(sK1),$sum(1,n)),1) | (spl2_2 | ~spl2_11 | spl2_89)),
% 11.44/2.09 inference(forward_demodulation,[],[f6288,f248])).
% 11.44/2.09 tff(f6294,plain,(
% 11.44/2.09 $sum(1,$sum(n,$sum($uminus(sK1),p($sum(1,$sum(n,$uminus(sK1))))))) != $sum(1,$sum($uminus(sK0),$sum(n,p($sum($uminus(sK0),$sum(1,n)))))) | $less(n,$sum($uminus(sK1),$sum(1,n))) | $less($sum($uminus(sK1),$sum(1,n)),1) | (spl2_2 | ~spl2_12 | spl2_89)),
% 11.44/2.09 inference(forward_demodulation,[],[f6289,f13])).
% 11.44/2.09 tff(f6301,definition,(
% 11.44/2.09 spl2_163 <=> $less($sum(1,$sum(n,$uminus(sK1))),1)),
% 11.44/2.09 introduced(definition,[new_symbols(definition,[spl2_163])],[avatar_definition])).
% 11.44/2.09 tff(f6303,plain,(
% 11.44/2.09 $less($sum(1,$sum(n,$uminus(sK1))),1) | ~spl2_163),
% 11.44/2.09 inference(avatar_component_clause,[],[f6301])).
% 11.44/2.09 tff(f6305,plain,(
% 11.44/2.09 $sum(sK1,$sum($uminus($sum(1,n)),p($sum($uminus(sK1),$sum(1,n))))) != $sum(sK0,$sum($uminus($sum(1,n)),p($sum(1,$sum(n,$uminus(sK0)))))) | $less(n,$sum($uminus(sK1),$sum(1,n))) | $less($sum($uminus(sK1),$sum(1,n)),1) | (spl2_2 | ~spl2_11 | spl2_89)),
% 11.44/2.09 inference(forward_demodulation,[],[f6293,f13])).
% 11.44/2.09 tff(f6306,plain,(
% 11.44/2.09 $sum(1,$sum(n,$sum($uminus(sK1),p($sum(1,$sum(n,$uminus(sK1))))))) != $sum(1,$sum(n,$sum(p($sum($uminus(sK0),$sum(1,n))),$uminus(sK0)))) | $less(n,$sum($uminus(sK1),$sum(1,n))) | $less($sum($uminus(sK1),$sum(1,n)),1) | (spl2_2 | ~spl2_12 | spl2_89)),
% 11.44/2.09 inference(forward_demodulation,[],[f6294,f248])).
% 11.44/2.09 tff(f6308,plain,(
% 11.44/2.09 $sum(sK1,$sum($uminus($sum(1,n)),p($sum(1,$sum(n,$uminus(sK1)))))) != $sum(sK0,$sum($uminus($sum(1,n)),p($sum(1,$sum(n,$uminus(sK0)))))) | $less(n,$sum($uminus(sK1),$sum(1,n))) | $less($sum($uminus(sK1),$sum(1,n)),1) | (spl2_2 | ~spl2_11 | spl2_89)),
% 11.44/2.09 inference(forward_demodulation,[],[f6305,f248])).
% 11.44/2.09 tff(f6309,plain,(
% 11.44/2.09 $sum(1,$sum(n,$sum($uminus(sK1),p($sum(1,$sum(n,$uminus(sK1))))))) != $sum(1,$sum(n,$sum($uminus(sK0),p($sum($uminus(sK0),$sum(1,n)))))) | $less(n,$sum($uminus(sK1),$sum(1,n))) | $less($sum($uminus(sK1),$sum(1,n)),1) | (spl2_2 | ~spl2_12 | spl2_89)),
% 11.44/2.09 inference(forward_demodulation,[],[f6306,f13])).
% 11.44/2.09 tff(f6311,plain,(
% 11.44/2.09 $less(n,$sum(1,$sum(n,$uminus(sK1)))) | $sum(sK1,$sum($uminus($sum(1,n)),p($sum(1,$sum(n,$uminus(sK1)))))) != $sum(sK0,$sum($uminus($sum(1,n)),p($sum(1,$sum(n,$uminus(sK0)))))) | $less($sum($uminus(sK1),$sum(1,n)),1) | (spl2_2 | ~spl2_11 | spl2_89)),
% 11.44/2.09 inference(forward_demodulation,[],[f6308,f248])).
% 11.44/2.09 tff(f6312,plain,(
% 11.44/2.09 $sum(1,$sum(n,$sum($uminus(sK0),p($sum(1,$sum(n,$uminus(sK0))))))) != $sum(1,$sum(n,$sum($uminus(sK1),p($sum(1,$sum(n,$uminus(sK1))))))) | $less(n,$sum($uminus(sK1),$sum(1,n))) | $less($sum($uminus(sK1),$sum(1,n)),1) | (spl2_2 | ~spl2_12 | spl2_89)),
% 11.44/2.09 inference(forward_demodulation,[],[f6309,f248])).
% 11.44/2.09 tff(f6314,plain,(
% 11.44/2.09 $less($sum(1,$sum(n,$uminus(sK1))),1) | $less(n,$sum(1,$sum(n,$uminus(sK1)))) | $sum(sK1,$sum($uminus($sum(1,n)),p($sum(1,$sum(n,$uminus(sK1)))))) != $sum(sK0,$sum($uminus($sum(1,n)),p($sum(1,$sum(n,$uminus(sK0)))))) | (spl2_2 | ~spl2_11 | spl2_89)),
% 11.44/2.09 inference(forward_demodulation,[],[f6311,f248])).
% 11.44/2.09 tff(f6315,plain,(
% 11.44/2.09 $less(n,$sum(1,$sum(n,$uminus(sK1)))) | $sum(1,$sum(n,$sum($uminus(sK0),p($sum(1,$sum(n,$uminus(sK0))))))) != $sum(1,$sum(n,$sum($uminus(sK1),p($sum(1,$sum(n,$uminus(sK1))))))) | $less($sum($uminus(sK1),$sum(1,n)),1) | (spl2_2 | ~spl2_12 | spl2_89)),
% 11.44/2.09 inference(forward_demodulation,[],[f6312,f248])).
% 11.44/2.09 tff(f6318,definition,(
% 11.44/2.09 spl2_164 <=> $sum(sK1,$sum($uminus($sum(1,n)),p($sum(1,$sum(n,$uminus(sK1)))))) = $sum(sK0,$sum($uminus($sum(1,n)),p($sum(1,$sum(n,$uminus(sK0))))))),
% 11.44/2.09 introduced(definition,[new_symbols(definition,[spl2_164])],[avatar_definition])).
% 11.44/2.09 tff(f6320,plain,(
% 11.44/2.09 $sum(sK1,$sum($uminus($sum(1,n)),p($sum(1,$sum(n,$uminus(sK1)))))) != $sum(sK0,$sum($uminus($sum(1,n)),p($sum(1,$sum(n,$uminus(sK0)))))) | spl2_164),
% 11.44/2.09 inference(avatar_component_clause,[],[f6318])).
% 11.44/2.09 tff(f6321,plain,(
% 11.44/2.09 ~spl2_164 | spl2_93 | spl2_163 | spl2_2 | ~spl2_11 | spl2_89),
% 11.44/2.09 inference(avatar_split_clause,[],[f6314,f4686,f108,f65,f6301,f4720,f6318])).
% 11.44/2.09 tff(f6322,plain,(
% 11.44/2.09 $less($sum(1,$sum(n,$uminus(sK1))),1) | $less(n,$sum(1,$sum(n,$uminus(sK1)))) | $sum(1,$sum(n,$sum($uminus(sK0),p($sum(1,$sum(n,$uminus(sK0))))))) != $sum(1,$sum(n,$sum($uminus(sK1),p($sum(1,$sum(n,$uminus(sK1))))))) | (spl2_2 | ~spl2_12 | spl2_89)),
% 11.44/2.09 inference(forward_demodulation,[],[f6315,f248])).
% 11.44/2.09 tff(f6328,definition,(
% 11.44/2.09 spl2_166 <=> $sum(1,$sum(n,$sum($uminus(sK0),p($sum(1,$sum(n,$uminus(sK0))))))) = $sum(1,$sum(n,$sum($uminus(sK1),p($sum(1,$sum(n,$uminus(sK1)))))))),
% 11.44/2.09 introduced(definition,[new_symbols(definition,[spl2_166])],[avatar_definition])).
% 11.44/2.09 tff(f6330,plain,(
% 11.44/2.09 $sum(1,$sum(n,$sum($uminus(sK0),p($sum(1,$sum(n,$uminus(sK0))))))) != $sum(1,$sum(n,$sum($uminus(sK1),p($sum(1,$sum(n,$uminus(sK1))))))) | spl2_166),
% 11.44/2.09 inference(avatar_component_clause,[],[f6328])).
% 11.44/2.09 tff(f6331,plain,(
% 11.44/2.09 ~spl2_166 | spl2_93 | spl2_163 | spl2_2 | ~spl2_12 | spl2_89),
% 11.44/2.09 inference(avatar_split_clause,[],[f6322,f4686,f112,f65,f6301,f4720,f6328])).
% 11.44/2.09 tff(f6450,plain,(
% 11.44/2.09 $sum(p($sum($sum(1,n),$uminus(sK0))),sK0) = $sum(sK1,p($sum($sum(1,n),$uminus(sK1)))) | ~spl2_8),
% 11.44/2.09 inference(forward_demodulation,[],[f97,f13])).
% 11.44/2.09 tff(f6453,plain,(
% 11.44/2.09 $sum(p($sum($sum(1,n),$uminus(sK0))),sK0) = $sum(sK1,p($sum($uminus(sK1),$sum(1,n)))) | ~spl2_8),
% 11.44/2.09 inference(forward_demodulation,[],[f6450,f13])).
% 11.44/2.09 tff(f6456,plain,(
% 11.44/2.09 $sum(p($sum($sum(1,n),$uminus(sK0))),sK0) = $sum(sK1,p($sum(1,$sum(n,$uminus(sK1))))) | ~spl2_8),
% 11.44/2.09 inference(forward_demodulation,[],[f6453,f248])).
% 11.44/2.09 tff(f6459,plain,(
% 11.44/2.09 $sum(sK0,p($sum($sum(1,n),$uminus(sK0)))) = $sum(sK1,p($sum(1,$sum(n,$uminus(sK1))))) | ~spl2_8),
% 11.44/2.09 inference(forward_demodulation,[],[f6456,f13])).
% 11.44/2.09 tff(f6462,plain,(
% 11.44/2.09 $sum(sK0,p($sum($uminus(sK0),$sum(1,n)))) = $sum(sK1,p($sum(1,$sum(n,$uminus(sK1))))) | ~spl2_8),
% 11.44/2.09 inference(forward_demodulation,[],[f6459,f13])).
% 11.44/2.09 tff(f6464,plain,(
% 11.44/2.09 $sum(sK0,p($sum(1,$sum(n,$uminus(sK0))))) = $sum(sK1,p($sum(1,$sum(n,$uminus(sK1))))) | ~spl2_8),
% 11.44/2.09 inference(forward_demodulation,[],[f6462,f248])).
% 11.44/2.09 tff(f6499,plain,(
% 11.44/2.09 spl2_163 | ~spl2_16),
% 11.44/2.09 inference(avatar_split_clause,[],[f6154,f340,f6301])).
% 11.44/2.09 tff(f7160,plain,(
% 11.44/2.09 ( ! [X0 : $int] : (~$less(X0,sK1) | $less(X0,1)) ) | ~spl2_60),
% 11.44/2.09 inference(resolution,[],[f2819,f19])).
% 11.44/2.09 tff(f7899,plain,(
% 11.44/2.09 $less($uminus($uminus(sK1)),1) | $less(n,$uminus($uminus(sK1))) | ~spl2_163),
% 11.44/2.09 inference(resolution,[],[f6303,f283])).
% 11.44/2.09 tff(f7903,plain,(
% 11.44/2.09 $less(sK1,1) | $less(n,sK1) | ~spl2_163),
% 11.44/2.09 inference(evaluation,[],[f7899])).
% 11.44/2.09 tff(f10611,plain,(
% 11.44/2.09 $less(sK0,1) | (spl2_1 | ~spl2_60)),
% 11.44/2.09 inference(resolution,[],[f853,f7160])).
% 11.44/2.09 tff(f10615,plain,(
% 11.44/2.09 $false | (spl2_1 | spl2_6 | ~spl2_60)),
% 11.44/2.09 inference(forward_subsumption_resolution,[],[f10611,f88])).
% 11.44/2.09 tff(f10616,plain,(
% 11.44/2.09 spl2_1 | spl2_6 | ~spl2_60),
% 11.44/2.09 inference(avatar_contradiction_clause,[],[f10615])).
% 11.44/2.09 tff(f10618,plain,(
% 11.44/2.09 $less(sK1,1) | (spl2_4 | ~spl2_93)),
% 11.44/2.09 inference(forward_subsumption_resolution,[],[f5566,f77])).
% 11.44/2.09 tff(f10622,plain,(
% 11.44/2.09 spl2_60 | spl2_4 | ~spl2_93),
% 11.44/2.09 inference(avatar_split_clause,[],[f10618,f4720,f75,f2817])).
% 11.44/2.09 tff(f10672,plain,(
% 11.44/2.09 $less(sK1,1) | (spl2_4 | ~spl2_163)),
% 11.44/2.09 inference(forward_subsumption_resolution,[],[f7903,f77])).
% 11.44/2.09 tff(f10712,plain,(
% 11.44/2.09 spl2_60 | spl2_4 | ~spl2_163),
% 11.44/2.09 inference(avatar_split_clause,[],[f10672,f6301,f75,f2817])).
% 11.44/2.09 tff(f10930,plain,(
% 11.44/2.09 ( ! [X0 : $int] : ($sum($sum(sK0,p($sum(1,$sum(n,$uminus(sK0))))),X0) = $sum(p($sum(1,$sum(n,$uminus(sK1)))),$sum(sK1,X0))) ) | ~spl2_8),
% 11.44/2.09 inference(superposition,[],[f239,f6464])).
% 11.44/2.09 tff(f10941,plain,(
% 11.44/2.09 ( ! [X0 : $int] : ($sum($sum(sK0,p($sum(1,$sum(n,$uminus(sK0))))),X0) = $sum(sK1,$sum(X0,p($sum(1,$sum(n,$uminus(sK1))))))) ) | ~spl2_8),
% 11.44/2.09 inference(forward_demodulation,[],[f10930,f248])).
% 11.44/2.09 tff(f10944,plain,(
% 11.44/2.09 ( ! [X0 : $int] : ($sum(sK0,$sum(p($sum(1,$sum(n,$uminus(sK0)))),X0)) = $sum(sK1,$sum(X0,p($sum(1,$sum(n,$uminus(sK1))))))) ) | ~spl2_8),
% 11.44/2.09 inference(forward_demodulation,[],[f10941,f14])).
% 11.44/2.09 tff(f11577,plain,(
% 11.44/2.09 $sum(1,$sum(n,$sum($uminus(sK0),p($sum(1,$sum(n,$uminus(sK0))))))) != $sum(1,$sum(n,$sum($uminus(sK0),p($sum(1,$sum(n,$uminus(sK0))))))) | (~spl2_7 | spl2_166)),
% 11.44/2.09 inference(forward_demodulation,[],[f6330,f6290])).
% 11.44/2.09 tff(f11578,plain,(
% 11.44/2.09 $false | (~spl2_7 | spl2_166)),
% 11.44/2.09 inference(trivial_inequality_removal,[],[f11577])).
% 11.44/2.09 tff(f11579,plain,(
% 11.44/2.09 ~spl2_7 | spl2_166),
% 11.44/2.09 inference(avatar_contradiction_clause,[],[f11578])).
% 11.44/2.09 tff(f14143,plain,(
% 11.44/2.09 $sum(sK0,$sum($uminus($sum(1,n)),p($sum(1,$sum(n,$uminus(sK0)))))) != $sum(sK0,$sum(p($sum(1,$sum(n,$uminus(sK0)))),$uminus($sum(1,n)))) | (~spl2_8 | spl2_164)),
% 11.44/2.09 inference(superposition,[],[f6320,f10944])).
% 11.44/2.09 tff(f14179,plain,(
% 11.44/2.09 $sum(sK0,$sum($uminus($sum(1,n)),p($sum(1,$sum(n,$uminus(sK0)))))) != $sum(sK0,$sum($uminus($sum(1,n)),p($sum(1,$sum(n,$uminus(sK0)))))) | (~spl2_8 | spl2_164)),
% 11.44/2.09 inference(forward_demodulation,[],[f14143,f13])).
% 11.44/2.09 tff(f14180,plain,(
% 11.44/2.09 $false | (~spl2_8 | spl2_164)),
% 11.44/2.09 inference(trivial_inequality_removal,[],[f14179])).
% 11.44/2.09 tff(f14181,plain,(
% 11.44/2.09 ~spl2_8 | spl2_164),
% 11.44/2.09 inference(avatar_contradiction_clause,[],[f14180])).
% 11.44/2.09 cnf(s1, plain, spl2_1 | ~spl2_2 | spl2_3, inference(sat_conversion,[],[f72])).
% 11.44/2.09 cnf(s3, plain, spl2_3 | ~spl2_4, inference(sat_conversion,[],[f78])).
% 11.44/2.09 cnf(s4, plain, ~spl2_1 | spl2_3, inference(sat_conversion,[],[f79])).
% 11.44/2.09 cnf(s5, plain, spl2_3 | ~spl2_5, inference(sat_conversion,[],[f84])).
% 11.44/2.09 cnf(s6, plain, spl2_3 | ~spl2_6, inference(sat_conversion,[],[f89])).
% 11.44/2.09 cnf(s7, plain, spl2_3 | spl2_7 | spl2_8 | spl2_9, inference(sat_conversion,[],[f102])).
% 11.44/2.09 cnf(s8, plain, ~spl2_10 | spl2_11, inference(sat_conversion,[],[f110])).
% 11.44/2.09 cnf(s9, plain, ~spl2_10 | spl2_12, inference(sat_conversion,[],[f114])).
% 11.44/2.09 cnf(s10, plain, ~spl2_10 | spl2_13, inference(sat_conversion,[],[f118])).
% 11.44/2.09 cnf(s11, plain, spl2_10, inference(sat_conversion,[],[f119])).
% 11.44/2.09 cnf(s12, plain, ~spl2_3, inference(sat_conversion,[],[f120])).
% 11.44/2.09 cnf(s15, plain, spl2_2 | ~spl2_9 | ~spl2_13 | spl2_16 | spl2_17 | spl2_18, inference(sat_conversion,[],[f351])).
% 11.44/2.09 cnf(s125, plain, spl2_5 | spl2_6 | ~spl2_18, inference(sat_conversion,[],[f4651])).
% 11.44/2.09 cnf(s138, plain, ~spl2_17 | spl2_93, inference(sat_conversion,[],[f4810])).
% 11.44/2.09 cnf(s139, plain, spl2_18 | ~spl2_89, inference(sat_conversion,[],[f4811])).
% 11.44/2.09 cnf(s234, plain, spl2_2 | ~spl2_11 | spl2_89 | spl2_93 | spl2_163 | ~spl2_164, inference(sat_conversion,[],[f6321])).
% 11.44/2.09 cnf(s236, plain, spl2_2 | ~spl2_12 | spl2_89 | spl2_93 | spl2_163 | ~spl2_166, inference(sat_conversion,[],[f6331])).
% 11.44/2.09 cnf(s247, plain, ~spl2_16 | spl2_163, inference(sat_conversion,[],[f6499])).
% 11.44/2.09 cnf(s689, plain, spl2_1 | spl2_6 | ~spl2_60, inference(sat_conversion,[],[f10616])).
% 11.44/2.09 cnf(s691, plain, spl2_4 | spl2_60 | ~spl2_93, inference(sat_conversion,[],[f10622])).
% 11.44/2.09 cnf(s762, plain, spl2_4 | spl2_60 | ~spl2_163, inference(sat_conversion,[],[f10712])).
% 11.44/2.09 cnf(s849, plain, ~spl2_7 | spl2_166, inference(sat_conversion,[],[f11579])).
% 11.44/2.09 cnf(s1181, plain, ~spl2_8 | spl2_164, inference(sat_conversion,[],[f14181])).
% 11.44/2.09 cnf(s1184, plain, spl2_13, inference(rat,[],[s10,s11])).
% 11.44/2.09 cnf(s1185, plain, spl2_12, inference(rat,[],[s9,s11])).
% 11.44/2.09 cnf(s1186, plain, spl2_11, inference(rat,[],[s8,s11])).
% 11.44/2.09 cnf(s1187, plain, spl2_7 | spl2_8 | spl2_9, inference(rat,[],[s7,s12])).
% 11.44/2.09 cnf(s1188, plain, ~spl2_6, inference(rat,[],[s6,s12])).
% 11.44/2.09 cnf(s1189, plain, ~spl2_5, inference(rat,[],[s5,s12])).
% 11.44/2.09 cnf(s1191, plain, ~spl2_18, inference(rat,[],[s125,s1188,s1189])).
% 11.44/2.09 cnf(s1192, plain, ~spl2_89, inference(rat,[],[s139,s1191])).
% 11.44/2.09 cnf(s1193, plain, ~spl2_1, inference(rat,[],[s4,s12])).
% 11.44/2.09 cnf(s1194, plain, ~spl2_60, inference(rat,[],[s689,s1188,s1193])).
% 11.44/2.09 cnf(s1195, plain, ~spl2_4, inference(rat,[],[s3,s12])).
% 11.44/2.09 cnf(s1196, plain, ~spl2_163, inference(rat,[],[s762,s1194,s1195])).
% 11.44/2.09 cnf(s1197, plain, ~spl2_93, inference(rat,[],[s691,s1194,s1195])).
% 11.44/2.09 cnf(s1198, plain, ~spl2_16, inference(rat,[],[s247,s1196])).
% 11.44/2.09 cnf(s1200, plain, ~spl2_17, inference(rat,[],[s138,s1197])).
% 11.44/2.09 cnf(s1201, plain, ~spl2_2, inference(rat,[],[s1,s12,s1193])).
% 11.44/2.09 cnf(s1202, plain, ~spl2_166, inference(rat,[],[s236,s1197,s1196,s1192,s1185,s1201])).
% 11.44/2.09 cnf(s1203, plain, ~spl2_164, inference(rat,[],[s234,s1197,s1196,s1192,s1186,s1201])).
% 11.44/2.09 cnf(s1205, plain, ~spl2_9, inference(rat,[],[s15,s1191,s1200,s1198,s1184,s1201])).
% 11.44/2.09 cnf(s1206, plain, ~spl2_7, inference(rat,[],[s849,s1202])).
% 11.44/2.09 cnf(s1207, plain, ~spl2_8, inference(rat,[],[s1181,s1203])).
% 11.44/2.09 cnf(s1208, plain, $false, inference(rat,[],[s1187,s1205,s1207,s1206])).
% 11.44/2.09 tff(f14194,plain,(
% 11.44/2.09 $false),
% 11.44/2.09 inference(avatar_sat_refutation,[],[s1208])).
% 11.44/2.09 % SZS output end Proof for theBenchmark
% 11.44/2.09 % (997309)------------------------------
% 11.44/2.09 % (997309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.44/2.09 % (997309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.44/2.09 % (997309)CaDiCaL version: 2.1.3
% 11.44/2.09 % (997309)Termination reason: Refutation
% 11.44/2.09 % (997309)Time elapsed: 0.504 s
% 11.44/2.09 % (997309)Peak memory usage: 18 MB
% 11.44/2.09 % (997309)Instructions burned: 922 (million)
% 11.44/2.09 % (997248)Success in time 1.666 s
% 11.44/2.09 % Vampire exiting
%------------------------------------------------------------------------------