%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWX082_1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:46:27 PM UTC 2026
% Result : Theorem 10.18s 2.00s
% Output : Refutation 10.18s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX082_1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.17 % Computer : n020.cluster.edu
% 0.07/0.17 % Model : x86_64 x86_64
% 0.07/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.17 % Memory : 8046.5625MB
% 0.07/0.17 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Mon Sep 28 15:00:34 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.21 Running first-order model finding
% 0.07/0.21 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.02/0.84 % (223767)Will run a generic schedule for satisfiability detection.
% 4.02/0.84 % (223775)dis+10_1_sil=32000:sp=arity:random_seed=1464190957:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.02/0.84 % (223773)% WARNING: option uhcvi not known.
% 4.02/0.84 % (223772)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1089178709_2999 on theBenchmark for (2999ds/0Mi)
% 4.02/0.84 % (223776)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4062557328:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.02/0.84 % (223773)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=950674011:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.02/0.84 % (223774)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3915956003:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.02/0.84 % (223777)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2218308597:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.02/0.84 % (223778)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=808765351:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.02/0.84 % (223772)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 4.02/0.84 % (223772)Terminated due to inappropriate strategy.
% 4.02/0.84 % (223772)------------------------------
% 4.02/0.84 % (223772)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.02/0.84 % (223772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.02/0.84 % (223772)CaDiCaL version: 2.1.3
% 4.02/0.84 % (223772)Termination reason: Inappropriate
% 4.02/0.84 % (223772)Time elapsed: 0.002 s
% 4.02/0.84 % (223772)Peak memory usage: 10 MB
% 4.02/0.84 % (223772)Instructions burned: 2 (million)
% 4.02/0.84 % (223772)------------------------------
% 4.02/0.84 % (223772)------------------------------
% 4.02/0.84 % (223786)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2764488314:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 4.02/0.84 % (223786)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 4.02/0.84 % (223786)Terminated due to inappropriate strategy.
% 4.02/0.84 % (223786)------------------------------
% 4.02/0.84 % (223786)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.02/0.84 % (223786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.02/0.84 % (223786)CaDiCaL version: 2.1.3
% 4.02/0.84 % (223786)Termination reason: Inappropriate
% 4.02/0.84 % (223786)Time elapsed: 0.001 s
% 4.02/0.84 % (223786)Peak memory usage: 11 MB
% 4.02/0.84 % (223786)Instructions burned: 2 (million)
% 4.02/0.84 % (223786)------------------------------
% 4.02/0.84 % (223786)------------------------------
% 4.02/0.84 % (223775)Instruction limit reached!
% 4.02/0.84 % (223775)------------------------------
% 4.02/0.84 % (223775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.02/0.84 % (223775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.02/0.84 % (223775)CaDiCaL version: 2.1.3
% 4.02/0.84 % (223775)Termination reason: Instruction limit
% 4.02/0.84 % (223775)Termination phase: Saturation
% 4.02/0.84 % (223775)Time elapsed: 0.036 s
% 4.02/0.84 % (223775)Peak memory usage: 12 MB
% 4.02/0.84 % (223775)Instructions burned: 103 (million)
% 4.02/0.84 % (223789)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=2043434131:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 4.02/0.84 % (223788)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=946264329:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 4.02/0.84 % (223776)Instruction limit reached!
% 4.02/0.84 % (223776)------------------------------
% 4.02/0.84 % (223776)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.02/0.84 % (223776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.02/0.84 % (223776)CaDiCaL version: 2.1.3
% 4.02/0.84 % (223776)Termination reason: Instruction limit
% 4.02/0.84 % (223776)Termination phase: Saturation
% 4.02/0.84 % (223776)Time elapsed: 0.073 s
% 4.02/0.84 % (223776)Peak memory usage: 12 MB
% 4.02/0.84 % (223776)Instructions burned: 118 (million)
% 4.02/0.84 % (223777)Instruction limit reached!
% 4.02/0.84 % (223777)------------------------------
% 4.02/0.84 % (223777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.05/1.40 % (223777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.05/1.40 % (223777)CaDiCaL version: 2.1.3
% 8.05/1.40 % (223777)Termination reason: Instruction limit
% 8.05/1.40 % (223777)Termination phase: Saturation
% 8.05/1.40 % (223777)Time elapsed: 0.079 s
% 8.05/1.40 % (223777)Peak memory usage: 13 MB
% 8.05/1.40 % (223777)Instructions burned: 133 (million)
% 8.05/1.40 % (223792)ott-21_1_sil=16000:fs=off:random_seed=2214057229:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 8.05/1.40 % (223793)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1966218243:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 8.05/1.40 % (223778)Instruction limit reached!
% 8.05/1.40 % (223778)------------------------------
% 8.05/1.40 % (223778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.05/1.40 % (223778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.05/1.40 % (223778)CaDiCaL version: 2.1.3
% 8.05/1.40 % (223778)Termination reason: Instruction limit
% 8.05/1.40 % (223778)Termination phase: Saturation
% 8.05/1.40 % (223778)Time elapsed: 0.099 s
% 8.05/1.40 % (223778)Peak memory usage: 13 MB
% 8.05/1.40 % (223778)Instructions burned: 160 (million)
% 8.05/1.40 % (223796)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1841484462:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 8.05/1.40 % (223796)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 8.05/1.40 % (223796)Terminated due to inappropriate strategy.
% 8.05/1.40 % (223796)------------------------------
% 8.05/1.40 % (223796)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.05/1.40 % (223796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.05/1.40 % (223796)CaDiCaL version: 2.1.3
% 8.05/1.40 % (223796)Termination reason: Inappropriate
% 8.05/1.40 % (223796)Time elapsed: 0.001 s
% 8.05/1.40 % (223796)Peak memory usage: 10 MB
% 8.05/1.40 % (223796)Instructions burned: 1 (million)
% 8.05/1.40 % (223796)------------------------------
% 8.05/1.40 % (223796)------------------------------
% 8.05/1.40 % (223788)Instruction limit reached!
% 8.05/1.40 % (223788)------------------------------
% 8.05/1.40 % (223788)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.05/1.40 % (223788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.05/1.40 % (223788)CaDiCaL version: 2.1.3
% 8.05/1.40 % (223788)Termination reason: Instruction limit
% 8.05/1.40 % (223788)Termination phase: Saturation
% 8.05/1.40 % (223788)Time elapsed: 0.082 s
% 8.05/1.40 % (223788)Peak memory usage: 13 MB
% 8.05/1.40 % (223788)Instructions burned: 132 (million)
% 8.05/1.40 % (223798)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1879152421:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 8.05/1.40 % (223799)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1755024439:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 8.05/1.40 % (223799)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 8.05/1.40 % (223799)Terminated due to inappropriate strategy.
% 8.05/1.40 % (223799)------------------------------
% 8.05/1.40 % (223799)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.05/1.40 % (223799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.05/1.40 % (223799)CaDiCaL version: 2.1.3
% 8.05/1.40 % (223799)Termination reason: Inappropriate
% 8.05/1.40 % (223799)Time elapsed: 0.001 s
% 8.05/1.40 % (223799)Peak memory usage: 10 MB
% 8.05/1.40 % (223799)Instructions burned: 2 (million)
% 8.05/1.40 % (223799)------------------------------
% 8.05/1.40 % (223799)------------------------------
% 8.05/1.40 % (223802)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=1550568072: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)
% 8.05/1.40 % (223792)Instruction limit reached!
% 8.05/1.40 % (223792)------------------------------
% 8.05/1.40 % (223792)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.05/1.40 % (223792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.05/1.40 % (223792)CaDiCaL version: 2.1.3
% 8.05/1.40 % (223792)Termination reason: Instruction limit
% 8.05/1.40 % (223792)Termination phase: Saturation
% 8.05/1.40 % (223792)Time elapsed: 0.083 s
% 8.05/1.40 % (223792)Peak memory usage: 12 MB
% 8.05/1.40 % (223792)Instructions burned: 181 (million)
% 10.18/2.00 % (223804)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3145230714:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 10.18/2.00 % (223789)Instruction limit reached!
% 10.18/2.00 % (223789)------------------------------
% 10.18/2.00 % (223789)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.18/2.00 % (223789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.18/2.00 % (223789)CaDiCaL version: 2.1.3
% 10.18/2.00 % (223789)Termination reason: Instruction limit
% 10.18/2.00 % (223789)Termination phase: Saturation
% 10.18/2.00 % (223789)Time elapsed: 0.167 s
% 10.18/2.00 % (223789)Peak memory usage: 15 MB
% 10.18/2.00 % (223789)Instructions burned: 684 (million)
% 10.18/2.00 % (223806)fmb+10_1_sil=64000:random_seed=4214623395:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi)
% 10.18/2.00 % (223806)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 10.18/2.00 % (223806)Terminated due to inappropriate strategy.
% 10.18/2.00 % (223806)------------------------------
% 10.18/2.00 % (223806)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.18/2.00 % (223806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.18/2.00 % (223806)CaDiCaL version: 2.1.3
% 10.18/2.00 % (223806)Termination reason: Inappropriate
% 10.18/2.00 % (223806)Time elapsed: 0.001 s
% 10.18/2.00 % (223806)Peak memory usage: 11 MB
% 10.18/2.00 % (223806)Instructions burned: 2 (million)
% 10.18/2.00 % (223806)------------------------------
% 10.18/2.00 % (223806)------------------------------
% 10.18/2.00 % (223808)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1968785330:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi)
% 10.18/2.00 % (223808)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 10.18/2.00 % (223808)Terminated due to inappropriate strategy.
% 10.18/2.00 % (223808)------------------------------
% 10.18/2.00 % (223808)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.18/2.00 % (223808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.18/2.00 % (223808)CaDiCaL version: 2.1.3
% 10.18/2.00 % (223808)Termination reason: Inappropriate
% 10.18/2.00 % (223808)Time elapsed: 0.001 s
% 10.18/2.00 % (223808)Peak memory usage: 10 MB
% 10.18/2.00 % (223808)Instructions burned: 2 (million)
% 10.18/2.00 % (223808)------------------------------
% 10.18/2.00 % (223808)------------------------------
% 10.18/2.00 % (223810)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1104856680:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi)
% 10.18/2.00 % (223810)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 10.18/2.00 % (223810)Terminated due to inappropriate strategy.
% 10.18/2.00 % (223810)------------------------------
% 10.18/2.00 % (223810)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.18/2.00 % (223810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.18/2.00 % (223810)CaDiCaL version: 2.1.3
% 10.18/2.00 % (223810)Termination reason: Inappropriate
% 10.18/2.00 % (223810)Time elapsed: 0.0000 s
% 10.18/2.00 % (223810)Peak memory usage: 10 MB
% 10.18/2.00 % (223810)Instructions burned: 2 (million)
% 10.18/2.00 % (223810)------------------------------
% 10.18/2.00 % (223810)------------------------------
% 10.18/2.00 % (223812)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3641036139:i=5131_2997 on theBenchmark for (2997ds/5131Mi)
% 10.18/2.00 % (223793)Instruction limit reached!
% 10.18/2.00 % (223793)------------------------------
% 10.18/2.00 % (223793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.18/2.00 % (223793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.18/2.00 % (223793)CaDiCaL version: 2.1.3
% 10.18/2.00 % (223793)Termination reason: Instruction limit
% 10.18/2.00 % (223793)Termination phase: Saturation
% 10.18/2.00 % (223793)Time elapsed: 0.322 s
% 10.18/2.00 % (223793)Peak memory usage: 14 MB
% 10.18/2.00 % (223793)Instructions burned: 477 (million)
% 10.18/2.00 % (223814)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2145207719:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 10.18/2.00 % (223802)Instruction limit reached!
% 10.18/2.00 % (223802)------------------------------
% 10.18/2.00 % (223802)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.18/2.00 % (223802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.18/2.00 % (223802)CaDiCaL version: 2.1.3
% 10.18/2.00 % (223802)Termination reason: Instruction limit
% 10.18/2.00 % (223802)Termination phase: Saturation
% 10.18/2.00 % (223802)Time elapsed: 0.423 s
% 10.18/2.00 % (223802)Peak memory usage: 22 MB
% 10.18/2.00 % (223802)Instructions burned: 694 (million)
% 10.18/2.00 % (223816)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=793342735:i=6324_2993 on theBenchmark for (2993ds/6324Mi)
% 10.18/2.00 % (223816)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 10.18/2.00 % (223816)Terminated due to inappropriate strategy.
% 10.18/2.00 % (223816)------------------------------
% 10.18/2.00 % (223816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.18/2.00 % (223816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.18/2.00 % (223816)CaDiCaL version: 2.1.3
% 10.18/2.00 % (223816)Termination reason: Inappropriate
% 10.18/2.00 % (223816)Time elapsed: 0.002 s
% 10.18/2.00 % (223816)Peak memory usage: 10 MB
% 10.18/2.00 % (223816)Instructions burned: 2 (million)
% 10.18/2.00 % (223816)------------------------------
% 10.18/2.00 % (223816)------------------------------
% 10.18/2.00 % (223818)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1437177276:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi)
% 10.18/2.00 % (223818)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 10.18/2.00 % (223818)Terminated due to inappropriate strategy.
% 10.18/2.00 % (223818)------------------------------
% 10.18/2.00 % (223818)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.18/2.00 % (223818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.18/2.00 % (223818)CaDiCaL version: 2.1.3
% 10.18/2.00 % (223818)Termination reason: Inappropriate
% 10.18/2.00 % (223818)Time elapsed: 0.001 s
% 10.18/2.00 % (223818)Peak memory usage: 11 MB
% 10.18/2.00 % (223818)Instructions burned: 2 (million)
% 10.18/2.00 % (223818)------------------------------
% 10.18/2.00 % (223818)------------------------------
% 10.18/2.00 % (223820)ott-2_1_sil=16000:newcnf=on:random_seed=2685505790:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi)
% 10.18/2.00 % (223804)Instruction limit reached!
% 10.18/2.00 % (223804)------------------------------
% 10.18/2.00 % (223804)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.18/2.00 % (223804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.18/2.00 % (223804)CaDiCaL version: 2.1.3
% 10.18/2.00 % (223804)Termination reason: Instruction limit
% 10.18/2.00 % (223804)Termination phase: Saturation
% 10.18/2.00 % (223804)Time elapsed: 0.497 s
% 10.18/2.00 % (223804)Peak memory usage: 18 MB
% 10.18/2.00 % (223804)Instructions burned: 880 (million)
% 10.18/2.00 % (223822)ott+10_1_sil=32000:tgt=ground:random_seed=2736053861:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi)
% 10.18/2.00 % (223798)Instruction limit reached!
% 10.18/2.00 % (223798)------------------------------
% 10.18/2.00 % (223798)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.18/2.00 % (223798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.18/2.00 % (223798)CaDiCaL version: 2.1.3
% 10.18/2.00 % (223798)Termination reason: Instruction limit
% 10.18/2.00 % (223798)Termination phase: Saturation
% 10.18/2.00 % (223798)Time elapsed: 0.622 s
% 10.18/2.00 % (223798)Peak memory usage: 21 MB
% 10.18/2.00 % (223798)Instructions burned: 1180 (million)
% 10.18/2.00 % (223824)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=576271850:i=54282_2992 on theBenchmark for (2992ds/54282Mi)
% 10.18/2.00 % (223824)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 10.18/2.00 % (223824)Terminated due to inappropriate strategy.
% 10.18/2.00 % (223824)------------------------------
% 10.18/2.00 % (223824)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.18/2.00 % (223824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.18/2.00 % (223824)CaDiCaL version: 2.1.3
% 10.18/2.00 % (223824)Termination reason: Inappropriate
% 10.18/2.00 % (223824)Time elapsed: 0.002 s
% 10.18/2.00 % (223824)Peak memory usage: 11 MB
% 10.18/2.00 % (223824)Instructions burned: 2 (million)
% 10.18/2.00 % (223824)------------------------------
% 10.18/2.00 % (223824)------------------------------
% 10.18/2.00 % (223826)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4213879515:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi)
% 10.18/2.00 % (223820)Instruction limit reached!
% 10.18/2.00 % (223820)------------------------------
% 10.18/2.00 % (223820)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.18/2.00 % (223820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.18/2.00 % (223820)CaDiCaL version: 2.1.3
% 10.18/2.00 % (223820)Termination reason: Instruction limit
% 10.18/2.00 % (223820)Termination phase: Saturation
% 10.18/2.00 % (223820)Time elapsed: 0.495 s
% 10.18/2.00 % (223820)Peak memory usage: 19 MB
% 10.18/2.00 % (223820)Instructions burned: 871 (million)
% 10.18/2.00 % (223828)dis+21_1_sil=32000:sas=cadical:random_seed=1951295819:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi)
% 10.18/2.00 % (223814)Instruction limit reached!
% 10.18/2.00 % (223814)------------------------------
% 10.18/2.00 % (223814)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.18/2.00 % (223814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.18/2.00 % (223814)CaDiCaL version: 2.1.3
% 10.18/2.00 % (223814)Termination reason: Instruction limit
% 10.18/2.00 % (223814)Termination phase: Saturation
% 10.18/2.00 % (223814)Time elapsed: 0.854 s
% 10.18/2.00 % (223814)Peak memory usage: 29 MB
% 10.18/2.00 % (223814)Instructions burned: 1472 (million)
% 10.18/2.00 % (223830)ott+11_1_sil=16000:gs=on:random_seed=2039748478:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2986 on theBenchmark for (2986ds/2251Mi)
% 10.18/2.00 % (223812)Instruction limit reached!
% 10.18/2.00 % (223812)------------------------------
% 10.18/2.00 % (223812)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.18/2.00 % (223812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.18/2.00 % (223812)CaDiCaL version: 2.1.3
% 10.18/2.00 % (223812)Termination reason: Instruction limit
% 10.18/2.00 % (223812)Termination phase: Saturation
% 10.18/2.00 % (223812)Time elapsed: 1.299 s
% 10.18/2.00 % (223812)Peak memory usage: 32 MB
% 10.18/2.00 % (223812)Instructions burned: 5133 (million)
% 10.18/2.00 % (223832)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1302497964:fmbsr=1.6:i=67534_2984 on theBenchmark for (2984ds/67534Mi)
% 10.18/2.00 % (223832)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 10.18/2.00 % (223832)Terminated due to inappropriate strategy.
% 10.18/2.00 % (223832)------------------------------
% 10.18/2.00 % (223832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.18/2.00 % (223832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.18/2.00 % (223832)CaDiCaL version: 2.1.3
% 10.18/2.00 % (223832)Termination reason: Inappropriate
% 10.18/2.00 % (223832)Time elapsed: 0.001 s
% 10.18/2.00 % (223832)Peak memory usage: 10 MB
% 10.18/2.00 % (223832)Instructions burned: 2 (million)
% 10.18/2.00 % (223832)------------------------------
% 10.18/2.00 % (223832)------------------------------
% 10.18/2.00 % (223834)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3412278021:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2984 on theBenchmark for (2984ds/4591Mi)
% 10.18/2.00 % (223822) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-223767-223822"...
% 10.18/2.00 % (223822)...printing done.
% 10.18/2.00 % (223822)Refutation found. Thanks to Tanya!
% 10.18/2.00 % SZS status Theorem for theBenchmark
% 10.18/2.00 % SZS output start Proof for theBenchmark
% 10.18/2.00 tff(type_def_5, type, general: $tType).
% 10.18/2.00 tff(type_def_6, type, symbol: $tType).
% 10.18/2.00 tff(func_def_0, type, f__integer__: $int > general).
% 10.18/2.00 tff(func_def_1, type, f__symbolic__: symbol > general).
% 10.18/2.00 tff(func_def_2, type, c__infimum__: general).
% 10.18/2.00 tff(func_def_3, type, c__supremum__: general).
% 10.18/2.00 tff(func_def_10, type, sK0: general > $int).
% 10.18/2.00 tff(func_def_11, type, sK1: general > symbol).
% 10.18/2.00 tff(func_def_12, type, sK2: (general * general * general * general) > general).
% 10.18/2.00 tff(func_def_13, type, sK3: (general * general * general * general) > general).
% 10.18/2.00 tff(func_def_14, type, sK4: (general * general * general * general) > general).
% 10.18/2.00 tff(func_def_15, type, sK5: (general * general * general * general) > general).
% 10.18/2.00 tff(func_def_16, type, sK6: (general * general * general * general) > general).
% 10.18/2.00 tff(func_def_17, type, sK7: (general * general * general * general) > general).
% 10.18/2.00 tff(func_def_18, type, sK8: (general * general * general * general) > $int).
% 10.18/2.00 tff(func_def_19, type, sK9: (general * general * general * general) > $int).
% 10.18/2.00 tff(func_def_20, type, sK10: (general * general * general * general) > $int).
% 10.18/2.00 tff(func_def_21, type, sK11: (general * general * general * general) > $int).
% 10.18/2.00 tff(func_def_22, type, sK12: (general * general * general * general) > general).
% 10.18/2.00 tff(func_def_23, type, sK13: (general * general * general * general) > general).
% 10.18/2.00 tff(func_def_24, type, sK14: (general * general * general * general) > general).
% 10.18/2.00 tff(func_def_25, type, sK15: (general * general * general * general) > general).
% 10.18/2.00 tff(func_def_26, type, sK16: $int).
% 10.18/2.00 tff(func_def_27, type, sK17: $int).
% 10.18/2.00 tff(func_def_28, type, sK18: $int).
% 10.18/2.00 tff(func_def_29, type, sF19: $int).
% 10.18/2.00 tff(func_def_30, type, sF20: general).
% 10.18/2.00 tff(func_def_31, type, sF21: general).
% 10.18/2.00 tff(func_def_32, type, sF22: $int).
% 10.18/2.00 tff(func_def_33, type, sF23: general).
% 10.18/2.00 tff(func_def_34, type, sF24: general).
% 10.18/2.00 tff(func_def_35, type, sF25: general).
% 10.18/2.00 tff(func_def_36, type, sF26: general).
% 10.18/2.00 tff(func_def_37, type, sF27: $int).
% 10.18/2.00 tff(func_def_38, type, sF28: $int).
% 10.18/2.00 tff(func_def_39, type, sF29: general).
% 10.18/2.00 tff(pred_def_1, type, p__is_integer__: general > $o).
% 10.18/2.00 tff(pred_def_2, type, p__is_symbolic__: general > $o).
% 10.18/2.00 tff(pred_def_3, type, p__less_equal__: (general * general) > $o).
% 10.18/2.00 tff(pred_def_4, type, p__less__: (general * general) > $o).
% 10.18/2.00 tff(pred_def_5, type, p__greater_equal__: (general * general) > $o).
% 10.18/2.00 tff(pred_def_6, type, p__greater__: (general * general) > $o).
% 10.18/2.00 tff(pred_def_8, type, div: (general * general * general * general) > $o).
% 10.18/2.00 tff(f4,axiom,(
% 10.18/2.00 ! [X0 : $int,X1 : $int] : (f__integer__(X0) = f__integer__(X1) <=> X0 = X1)),
% 10.18/2.00 file('/export/starexec/sandbox/benchmark/Axioms/SWV014_0.ax',f__integer__def_ax)).
% 10.18/2.00 tff(f6,axiom,(
% 10.18/2.00 ! [X0 : $int,X1 : $int] : (p__less_equal__(f__integer__(X0),f__integer__(X1)) <=> $lesseq(X0,X1))),
% 10.18/2.00 file('/export/starexec/sandbox/benchmark/Axioms/SWV014_0.ax',numeral_ordering_ax)).
% 10.18/2.00 tff(f8,axiom,(
% 10.18/2.00 ! [X0 : general,X1 : general,X2 : general] : ((p__less_equal__(X0,X1) & p__less_equal__(X1,X2)) => p__less_equal__(X0,X2))),
% 10.18/2.00 file('/export/starexec/sandbox/benchmark/Axioms/SWV014_0.ax',transitive_ordering_ax)).
% 10.18/2.00 tff(f9,axiom,(
% 10.18/2.00 ! [X0 : general,X1 : general] : (p__less_equal__(X0,X1) | p__less_equal__(X1,X0))),
% 10.18/2.00 file('/export/starexec/sandbox/benchmark/Axioms/SWV014_0.ax',strongly_connected_ordering_ax)).
% 10.18/2.00 tff(f10,axiom,(
% 10.18/2.00 ! [X0 : general,X1 : general] : (p__less__(X0,X1) <=> (p__less_equal__(X0,X1) & X0 != X1))),
% 10.18/2.00 file('/export/starexec/sandbox/benchmark/Axioms/SWV014_0.ax',p__less__def_ax)).
% 10.18/2.00 tff(f16,axiom,(
% 10.18/2.00 ! [X0 : general,X1 : general,X2 : general,X3 : general] : (div(X0,X1,X2,X3) <=> ? [X4 : general,X5 : general,X6 : general,X7 : general] : (X0 = X4 & X1 = X5 & X2 = X6 & X3 = X7 & ? [X8 : general,X9 : general] : (X8 = X4 & ? [X10 : $int,X11 : $int] : (X9 = f__integer__($sum(X10,X11)) & ? [X12 : $int,X11 : $int] : (X10 = $product(X12,X11) & f__integer__(X12) = X5 & f__integer__(X11) = X6) & f__integer__(X11) = X7) & X8 = X9) & ? [X8 : general,X9 : general] : (X8 = f__integer__(0) & X9 = X7 & p__less_equal__(X8,X9)) & ? [X8 : general,X9 : general] : (X8 = X7 & X9 = X5 & p__less__(X8,X9))))),
% 10.18/2.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_0_completed_definition_of_div_4)).
% 10.18/2.00 tff(f18,conjecture,(
% 10.18/2.00 ! [X0 : $int,X1 : $int,X2 : $int] : (div(f__integer__(X0),f__integer__(X1),f__integer__(X2),f__integer__($difference(X1,1))) => div(f__integer__($sum(X0,1)),f__integer__(X1),f__integer__($sum(X2,1)),f__integer__(0)))),
% 10.18/2.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_2_unnamed_formula)).
% 10.18/2.00 tff(f19,negated_conjecture,(
% 10.18/2.00 ~ ! [X0 : $int,X1 : $int,X2 : $int] : (div(f__integer__(X0),f__integer__(X1),f__integer__(X2),f__integer__($difference(X1,1))) => div(f__integer__($sum(X0,1)),f__integer__(X1),f__integer__($sum(X2,1)),f__integer__(0)))),
% 10.18/2.00 inference(negated_conjecture,[status(cth)],[f18])).
% 10.18/2.00 tff(f20,plain,(
% 10.18/2.00 ! [X0 : $int,X1 : $int] : (p__less_equal__(f__integer__(X0),f__integer__(X1)) <=> ~$less(X1,X0))),
% 10.18/2.00 inference(theory_normalization,[],[f6])).
% 10.18/2.00 tff(f22,plain,(
% 10.18/2.00 ~ ! [X0 : $int,X1 : $int,X2 : $int] : (div(f__integer__(X0),f__integer__(X1),f__integer__(X2),f__integer__($sum(X1,$uminus(1)))) => div(f__integer__($sum(X0,1)),f__integer__(X1),f__integer__($sum(X2,1)),f__integer__(0)))),
% 10.18/2.00 inference(theory_normalization,[],[f19])).
% 10.18/2.00 tff(f23,definition,(
% 10.18/2.00 ( ! [X0 : $int,X1 : $int] : ($sum(X0,X1) = $sum(X1,X0)) )),
% 10.18/2.00 introduced(theory,[tha_commutativity])).
% 10.18/2.00 tff(f24,definition,(
% 10.18/2.00 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum(X0,$sum(X1,X2)) = $sum($sum(X0,X1),X2)) )),
% 10.18/2.00 introduced(theory,[tha_associativity])).
% 10.18/2.00 tff(f26,definition,(
% 10.18/2.00 ( ! [X0 : $int,X1 : $int] : ($uminus($sum(X0,X1)) = $sum($uminus(X1),$uminus(X0))) )),
% 10.18/2.00 introduced(theory,[tha_inverse_op_op_inverses])).
% 10.18/2.00 tff(f27,definition,(
% 10.18/2.00 ( ! [X0 : $int] : (0 = $sum(X0,$uminus(X0))) )),
% 10.18/2.00 introduced(theory,[tha_inverse_op_unit])).
% 10.18/2.00 tff(f28,definition,(
% 10.18/2.00 ( ! [X0 : $int] : (~$less(X0,X0)) )),
% 10.18/2.00 introduced(theory,[tha_non-reflexivity])).
% 10.18/2.00 tff(f32,definition,(
% 10.18/2.00 ( ! [X0 : $int,X1 : $int] : ($less(X1,$sum(X0,1)) | $less(X0,X1)) )),
% 10.18/2.00 introduced(theory,[tha_order_plus_one_dichotomy])).
% 10.18/2.00 tff(f33,definition,(
% 10.18/2.00 ( ! [X0 : $int] : ($uminus($uminus(X0)) = X0) )),
% 10.18/2.00 introduced(theory,[tha_minus_minus_x])).
% 10.18/2.00 tff(f34,definition,(
% 10.18/2.00 ( ! [X0 : $int,X1 : $int] : ($product(X0,X1) = $product(X1,X0)) )),
% 10.18/2.00 introduced(theory,[tha_commutativity])).
% 10.18/2.00 tff(f36,definition,(
% 10.18/2.00 ( ! [X0 : $int] : ($product(X0,1) = X0) )),
% 10.18/2.00 introduced(theory,[tha_right_identity])).
% 10.18/2.00 tff(f38,definition,(
% 10.18/2.00 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($product(X0,$sum(X1,X2)) = $sum($product(X0,X1),$product(X0,X2))) )),
% 10.18/2.00 introduced(theory,[tha_distributivity])).
% 10.18/2.00 tff(f41,plain,(
% 10.18/2.00 ! [X0 : general,X1 : general,X2 : general,X3 : general] : (div(X0,X1,X2,X3) <=> ? [X4 : general,X5 : general,X6 : general,X7 : general] : (X0 = X4 & X1 = X5 & X2 = X6 & X3 = X7 & ? [X8 : general,X9 : general] : (X8 = X4 & ? [X10 : $int,X11 : $int] : (X9 = f__integer__($sum(X10,X11)) & ? [X12 : $int,X13 : $int] : ($product(X12,X13) = X10 & f__integer__(X12) = X5 & f__integer__(X13) = X6) & f__integer__(X11) = X7) & X8 = X9) & ? [X14 : general,X15 : general] : (f__integer__(0) = X14 & X7 = X15 & p__less_equal__(X14,X15)) & ? [X16 : general,X17 : general] : (X7 = X16 & X5 = X17 & p__less__(X16,X17))))),
% 10.18/2.00 inference(rectify,[],[f16])).
% 10.18/2.00 tff(f48,plain,(
% 10.18/2.00 ! [X0 : general,X1 : general,X2 : general] : (p__less_equal__(X0,X2) | (~p__less_equal__(X0,X1) | ~p__less_equal__(X1,X2)))),
% 10.18/2.00 inference(ennf_transformation,[],[f8])).
% 10.18/2.00 tff(f49,plain,(
% 10.18/2.00 ! [X0 : general,X1 : general,X2 : general] : (p__less_equal__(X0,X2) | ~p__less_equal__(X0,X1) | ~p__less_equal__(X1,X2))),
% 10.18/2.00 inference(flattening,[],[f48])).
% 10.18/2.00 tff(f52,plain,(
% 10.18/2.00 ? [X0 : $int,X1 : $int,X2 : $int] : (~div(f__integer__($sum(X0,1)),f__integer__(X1),f__integer__($sum(X2,1)),f__integer__(0)) & div(f__integer__(X0),f__integer__(X1),f__integer__(X2),f__integer__($sum(X1,$uminus(1)))))),
% 10.18/2.00 inference(ennf_transformation,[],[f22])).
% 10.18/2.00 tff(f55,plain,(
% 10.18/2.00 ! [X0 : $int,X1 : $int] : ((f__integer__(X0) = f__integer__(X1) | X0 != X1) & (X0 = X1 | f__integer__(X1) != f__integer__(X0)))),
% 10.18/2.00 inference(nnf_transformation,[],[f4])).
% 10.18/2.00 tff(f57,plain,(
% 10.18/2.00 ! [X0 : $int,X1 : $int] : ((p__less_equal__(f__integer__(X0),f__integer__(X1)) | $less(X1,X0)) & (~$less(X1,X0) | ~p__less_equal__(f__integer__(X0),f__integer__(X1))))),
% 10.18/2.00 inference(nnf_transformation,[],[f20])).
% 10.18/2.00 tff(f58,plain,(
% 10.18/2.00 ! [X0 : general,X1 : general] : ((p__less__(X0,X1) | (~p__less_equal__(X0,X1) | X0 = X1)) & ((p__less_equal__(X0,X1) & X0 != X1) | ~p__less__(X0,X1)))),
% 10.18/2.00 inference(nnf_transformation,[],[f10])).
% 10.18/2.00 tff(f59,plain,(
% 10.18/2.00 ! [X0 : general,X1 : general] : ((p__less__(X0,X1) | ~p__less_equal__(X0,X1) | X0 = X1) & ((p__less_equal__(X0,X1) & X0 != X1) | ~p__less__(X0,X1)))),
% 10.18/2.00 inference(flattening,[],[f58])).
% 10.18/2.00 tff(f60,plain,(
% 10.18/2.00 ! [X0 : general,X1 : general,X2 : general,X3 : general] : ((div(X0,X1,X2,X3) | ! [X4 : general,X5 : general,X6 : general,X7 : general] : (X0 != X4 | X1 != X5 | X2 != X6 | X3 != X7 | ! [X8 : general,X9 : general] : (X4 != X8 | ! [X10 : $int,X11 : $int] : (f__integer__($sum(X10,X11)) != X9 | ! [X12 : $int,X13 : $int] : ($product(X12,X13) != X10 | f__integer__(X12) != X5 | f__integer__(X13) != X6) | f__integer__(X11) != X7) | X8 != X9) | ! [X14 : general,X15 : general] : (f__integer__(0) != X14 | X7 != X15 | ~p__less_equal__(X14,X15)) | ! [X16 : general,X17 : general] : (X7 != X16 | X5 != X17 | ~p__less__(X16,X17)))) & (? [X4 : general,X5 : general,X6 : general,X7 : general] : (X0 = X4 & X1 = X5 & X2 = X6 & X3 = X7 & ? [X8 : general,X9 : general] : (X8 = X4 & ? [X10 : $int,X11 : $int] : (X9 = f__integer__($sum(X10,X11)) & ? [X12 : $int,X13 : $int] : ($product(X12,X13) = X10 & f__integer__(X12) = X5 & f__integer__(X13) = X6) & f__integer__(X11) = X7) & X8 = X9) & ? [X14 : general,X15 : general] : (f__integer__(0) = X14 & X7 = X15 & p__less_equal__(X14,X15)) & ? [X16 : general,X17 : general] : (X7 = X16 & X5 = X17 & p__less__(X16,X17))) | ~div(X0,X1,X2,X3)))),
% 10.18/2.00 inference(nnf_transformation,[],[f41])).
% 10.18/2.00 tff(f61,plain,(
% 10.18/2.00 ! [X0 : general,X1 : general,X2 : general,X3 : general] : ((div(X0,X1,X2,X3) | ! [X4 : general,X5 : general,X6 : general,X7 : general] : (X0 != X4 | X1 != X5 | X2 != X6 | X3 != X7 | ! [X8 : general,X9 : general] : (X4 != X8 | ! [X10 : $int,X11 : $int] : (f__integer__($sum(X10,X11)) != X9 | ! [X12 : $int,X13 : $int] : ($product(X12,X13) != X10 | f__integer__(X12) != X5 | f__integer__(X13) != X6) | f__integer__(X11) != X7) | X8 != X9) | ! [X14 : general,X15 : general] : (f__integer__(0) != X14 | X7 != X15 | ~p__less_equal__(X14,X15)) | ! [X16 : general,X17 : general] : (X7 != X16 | X5 != X17 | ~p__less__(X16,X17)))) & (? [X18 : general,X19 : general,X20 : general,X21 : general] : (X0 = X18 & X1 = X19 & X2 = X20 & X3 = X21 & ? [X22 : general,X23 : general] : (X18 = X22 & ? [X24 : $int,X25 : $int] : (f__integer__($sum(X24,X25)) = X23 & ? [X26 : $int,X27 : $int] : ($product(X26,X27) = X24 & f__integer__(X26) = X19 & f__integer__(X27) = X20) & f__integer__(X25) = X21) & X22 = X23) & ? [X28 : general,X29 : general] : (f__integer__(0) = X28 & X21 = X29 & p__less_equal__(X28,X29)) & ? [X30 : general,X31 : general] : (X21 = X30 & X19 = X31 & p__less__(X30,X31))) | ~div(X0,X1,X2,X3)))),
% 10.18/2.00 inference(rectify,[],[f60])).
% 10.18/2.00 tff(f62,plain,(
% 10.18/2.00 ! [X0 : general,X1 : general,X2 : general,X3 : general] : ((div(X0,X1,X2,X3) | ! [X4 : general,X5 : general,X6 : general,X7 : general] : (X0 != X4 | X1 != X5 | X2 != X6 | X3 != X7 | ! [X8 : general,X9 : general] : (X4 != X8 | ! [X10 : $int,X11 : $int] : (f__integer__($sum(X10,X11)) != X9 | ! [X12 : $int,X13 : $int] : ($product(X12,X13) != X10 | f__integer__(X12) != X5 | f__integer__(X13) != X6) | f__integer__(X11) != X7) | X8 != X9) | ! [X14 : general,X15 : general] : (f__integer__(0) != X14 | X7 != X15 | ~p__less_equal__(X14,X15)) | ! [X16 : general,X17 : general] : (X7 != X16 | X5 != X17 | ~p__less__(X16,X17)))) & ((sK2(X0,X1,X2,X3) = X0 & sK3(X0,X1,X2,X3) = X1 & sK4(X0,X1,X2,X3) = X2 & sK5(X0,X1,X2,X3) = X3 & (sK2(X0,X1,X2,X3) = sK6(X0,X1,X2,X3) & (sK7(X0,X1,X2,X3) = f__integer__($sum(sK8(X0,X1,X2,X3),sK9(X0,X1,X2,X3))) & (sK8(X0,X1,X2,X3) = $product(sK10(X0,X1,X2,X3),sK11(X0,X1,X2,X3)) & sK3(X0,X1,X2,X3) = f__integer__(sK10(X0,X1,X2,X3)) & sK4(X0,X1,X2,X3) = f__integer__(sK11(X0,X1,X2,X3))) & sK5(X0,X1,X2,X3) = f__integer__(sK9(X0,X1,X2,X3))) & sK6(X0,X1,X2,X3) = sK7(X0,X1,X2,X3)) & (f__integer__(0) = sK12(X0,X1,X2,X3) & sK5(X0,X1,X2,X3) = sK13(X0,X1,X2,X3) & p__less_equal__(sK12(X0,X1,X2,X3),sK13(X0,X1,X2,X3))) & (sK5(X0,X1,X2,X3) = sK14(X0,X1,X2,X3) & sK3(X0,X1,X2,X3) = sK15(X0,X1,X2,X3) & p__less__(sK14(X0,X1,X2,X3),sK15(X0,X1,X2,X3)))) | ~div(X0,X1,X2,X3)))),
% 10.18/2.00 inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4,sK5,sK6,sK7,sK8,sK9,sK10,sK11,sK12,sK13,sK14,sK15]),skolemize(X18,sK2(X0,X1,X2,X3)),skolemize(X19,sK3(X0,X1,X2,X3)),skolemize(X20,sK4(X0,X1,X2,X3)),skolemize(X21,sK5(X0,X1,X2,X3)),skolemize(X22,sK6(X0,X1,X2,X3)),skolemize(X23,sK7(X0,X1,X2,X3)),skolemize(X24,sK8(X0,X1,X2,X3)),skolemize(X25,sK9(X0,X1,X2,X3)),skolemize(X26,sK10(X0,X1,X2,X3)),skolemize(X27,sK11(X0,X1,X2,X3)),skolemize(X28,sK12(X0,X1,X2,X3)),skolemize(X29,sK13(X0,X1,X2,X3)),skolemize(X30,sK14(X0,X1,X2,X3)),skolemize(X31,sK15(X0,X1,X2,X3))],[f61])).
% 10.18/2.00 tff(f63,plain,(
% 10.18/2.00 ~div(f__integer__($sum(sK16,1)),f__integer__(sK17),f__integer__($sum(sK18,1)),f__integer__(0)) & div(f__integer__(sK16),f__integer__(sK17),f__integer__(sK18),f__integer__($sum(sK17,$uminus(1))))),
% 10.18/2.00 inference(skolemize,[status(esa),new_symbols(skolem,[sK16,sK17,sK18]),skolemize(X0,sK16),skolemize(X1,sK17),skolemize(X2,sK18)],[f52])).
% 10.18/2.00 tff(f67,plain,(
% 10.18/2.00 ( ! [X0 : $int,X1 : $int] : (f__integer__(X1) != f__integer__(X0) | X0 = X1) )),
% 10.18/2.00 inference(cnf_transformation,[],[f55])).
% 10.18/2.00 tff(f71,plain,(
% 10.18/2.00 ( ! [X0 : $int,X1 : $int] : (~p__less_equal__(f__integer__(X0),f__integer__(X1)) | ~$less(X1,X0)) )),
% 10.18/2.00 inference(cnf_transformation,[],[f57])).
% 10.18/2.00 tff(f72,plain,(
% 10.18/2.00 ( ! [X0 : $int,X1 : $int] : (p__less_equal__(f__integer__(X0),f__integer__(X1)) | $less(X1,X0)) )),
% 10.18/2.00 inference(cnf_transformation,[],[f57])).
% 10.18/2.00 tff(f74,plain,(
% 10.18/2.00 ( ! [X2 : general,X0 : general,X1 : general] : (~p__less_equal__(X1,X2) | ~p__less_equal__(X0,X1) | p__less_equal__(X0,X2)) )),
% 10.18/2.00 inference(cnf_transformation,[],[f49])).
% 10.18/2.00 tff(f75,plain,(
% 10.18/2.00 ( ! [X0 : general,X1 : general] : (p__less_equal__(X0,X1) | p__less_equal__(X1,X0)) )),
% 10.18/2.00 inference(cnf_transformation,[],[f9])).
% 10.18/2.00 tff(f77,plain,(
% 10.18/2.00 ( ! [X0 : general,X1 : general] : (~p__less__(X0,X1) | p__less_equal__(X0,X1)) )),
% 10.18/2.00 inference(cnf_transformation,[],[f59])).
% 10.18/2.00 tff(f78,plain,(
% 10.18/2.00 ( ! [X0 : general,X1 : general] : (~p__less_equal__(X0,X1) | p__less__(X0,X1) | X0 = X1) )),
% 10.18/2.00 inference(cnf_transformation,[],[f59])).
% 10.18/2.00 tff(f82,plain,(
% 10.18/2.00 ( ! [X2 : general,X3 : general,X0 : general,X1 : general] : (p__less__(sK14(X0,X1,X2,X3),sK15(X0,X1,X2,X3)) | ~div(X0,X1,X2,X3)) )),
% 10.18/2.00 inference(cnf_transformation,[],[f62])).
% 10.18/2.00 tff(f83,plain,(
% 10.18/2.00 ( ! [X2 : general,X3 : general,X0 : general,X1 : general] : (~div(X0,X1,X2,X3) | sK3(X0,X1,X2,X3) = sK15(X0,X1,X2,X3)) )),
% 10.18/2.00 inference(cnf_transformation,[],[f62])).
% 10.18/2.00 tff(f84,plain,(
% 10.18/2.00 ( ! [X2 : general,X3 : general,X0 : general,X1 : general] : (~div(X0,X1,X2,X3) | sK5(X0,X1,X2,X3) = sK14(X0,X1,X2,X3)) )),
% 10.18/2.00 inference(cnf_transformation,[],[f62])).
% 10.18/2.00 tff(f85,plain,(
% 10.18/2.00 ( ! [X2 : general,X3 : general,X0 : general,X1 : general] : (p__less_equal__(sK12(X0,X1,X2,X3),sK13(X0,X1,X2,X3)) | ~div(X0,X1,X2,X3)) )),
% 10.18/2.00 inference(cnf_transformation,[],[f62])).
% 10.18/2.00 tff(f86,plain,(
% 10.18/2.00 ( ! [X2 : general,X3 : general,X0 : general,X1 : general] : (~div(X0,X1,X2,X3) | sK5(X0,X1,X2,X3) = sK13(X0,X1,X2,X3)) )),
% 10.18/2.00 inference(cnf_transformation,[],[f62])).
% 10.18/2.00 tff(f87,plain,(
% 10.18/2.00 ( ! [X2 : general,X3 : general,X0 : general,X1 : general] : (~div(X0,X1,X2,X3) | f__integer__(0) = sK12(X0,X1,X2,X3)) )),
% 10.18/2.00 inference(cnf_transformation,[],[f62])).
% 10.18/2.00 tff(f88,plain,(
% 10.18/2.00 ( ! [X2 : general,X3 : general,X0 : general,X1 : general] : (~div(X0,X1,X2,X3) | sK6(X0,X1,X2,X3) = sK7(X0,X1,X2,X3)) )),
% 10.18/2.00 inference(cnf_transformation,[],[f62])).
% 10.18/2.00 tff(f89,plain,(
% 10.18/2.00 ( ! [X2 : general,X3 : general,X0 : general,X1 : general] : (~div(X0,X1,X2,X3) | sK5(X0,X1,X2,X3) = f__integer__(sK9(X0,X1,X2,X3))) )),
% 10.18/2.00 inference(cnf_transformation,[],[f62])).
% 10.18/2.00 tff(f90,plain,(
% 10.18/2.00 ( ! [X2 : general,X3 : general,X0 : general,X1 : general] : (~div(X0,X1,X2,X3) | sK4(X0,X1,X2,X3) = f__integer__(sK11(X0,X1,X2,X3))) )),
% 10.18/2.00 inference(cnf_transformation,[],[f62])).
% 10.18/2.00 tff(f91,plain,(
% 10.18/2.00 ( ! [X2 : general,X3 : general,X0 : general,X1 : general] : (~div(X0,X1,X2,X3) | sK3(X0,X1,X2,X3) = f__integer__(sK10(X0,X1,X2,X3))) )),
% 10.18/2.00 inference(cnf_transformation,[],[f62])).
% 10.18/2.00 tff(f92,plain,(
% 10.18/2.00 ( ! [X2 : general,X3 : general,X0 : general,X1 : general] : (~div(X0,X1,X2,X3) | sK8(X0,X1,X2,X3) = $product(sK10(X0,X1,X2,X3),sK11(X0,X1,X2,X3))) )),
% 10.18/2.00 inference(cnf_transformation,[],[f62])).
% 10.18/2.00 tff(f93,plain,(
% 10.18/2.00 ( ! [X2 : general,X3 : general,X0 : general,X1 : general] : (~div(X0,X1,X2,X3) | sK7(X0,X1,X2,X3) = f__integer__($sum(sK8(X0,X1,X2,X3),sK9(X0,X1,X2,X3)))) )),
% 10.18/2.00 inference(cnf_transformation,[],[f62])).
% 10.18/2.00 tff(f94,plain,(
% 10.18/2.00 ( ! [X2 : general,X3 : general,X0 : general,X1 : general] : (~div(X0,X1,X2,X3) | sK2(X0,X1,X2,X3) = sK6(X0,X1,X2,X3)) )),
% 10.18/2.00 inference(cnf_transformation,[],[f62])).
% 10.18/2.00 tff(f95,plain,(
% 10.18/2.00 ( ! [X2 : general,X3 : general,X0 : general,X1 : general] : (~div(X0,X1,X2,X3) | sK5(X0,X1,X2,X3) = X3) )),
% 10.18/2.00 inference(cnf_transformation,[],[f62])).
% 10.18/2.00 tff(f96,plain,(
% 10.18/2.00 ( ! [X2 : general,X3 : general,X0 : general,X1 : general] : (~div(X0,X1,X2,X3) | sK4(X0,X1,X2,X3) = X2) )),
% 10.18/2.00 inference(cnf_transformation,[],[f62])).
% 10.18/2.00 tff(f97,plain,(
% 10.18/2.00 ( ! [X2 : general,X3 : general,X0 : general,X1 : general] : (~div(X0,X1,X2,X3) | sK3(X0,X1,X2,X3) = X1) )),
% 10.18/2.00 inference(cnf_transformation,[],[f62])).
% 10.18/2.00 tff(f98,plain,(
% 10.18/2.00 ( ! [X2 : general,X3 : general,X0 : general,X1 : general] : (~div(X0,X1,X2,X3) | sK2(X0,X1,X2,X3) = X0) )),
% 10.18/2.00 inference(cnf_transformation,[],[f62])).
% 10.18/2.00 tff(f99,plain,(
% 10.18/2.00 ( ! [X2 : general,X3 : general,X10 : $int,X0 : general,X11 : $int,X1 : general,X8 : general,X6 : general,X9 : general,X7 : general,X14 : general,X4 : general,X16 : general,X17 : general,X15 : general,X5 : general,X12 : $int,X13 : $int] : (div(X0,X1,X2,X3) | X0 != X4 | X1 != X5 | X2 != X6 | X3 != X7 | X4 != X8 | f__integer__($sum(X10,X11)) != X9 | $product(X12,X13) != X10 | f__integer__(X12) != X5 | f__integer__(X13) != X6 | f__integer__(X11) != X7 | X8 != X9 | f__integer__(0) != X14 | X7 != X15 | ~p__less_equal__(X14,X15) | X7 != X16 | X5 != X17 | ~p__less__(X16,X17)) )),
% 10.18/2.00 inference(cnf_transformation,[],[f62])).
% 10.18/2.00 tff(f101,plain,(
% 10.18/2.00 div(f__integer__(sK16),f__integer__(sK17),f__integer__(sK18),f__integer__($sum(sK17,$uminus(1))))),
% 10.18/2.00 inference(cnf_transformation,[],[f63])).
% 10.18/2.00 tff(f102,plain,(
% 10.18/2.00 ~div(f__integer__($sum(sK16,1)),f__integer__(sK17),f__integer__($sum(sK18,1)),f__integer__(0))),
% 10.18/2.00 inference(cnf_transformation,[],[f63])).
% 10.18/2.00 tff(f107,plain,(
% 10.18/2.00 ( ! [X2 : general,X3 : general,X10 : $int,X11 : $int,X1 : general,X8 : general,X6 : general,X9 : general,X7 : general,X14 : general,X4 : general,X16 : general,X17 : general,X15 : general,X5 : general,X12 : $int,X13 : $int] : (div(X4,X1,X2,X3) | X1 != X5 | X2 != X6 | X3 != X7 | X4 != X8 | f__integer__($sum(X10,X11)) != X9 | $product(X12,X13) != X10 | f__integer__(X12) != X5 | f__integer__(X13) != X6 | f__integer__(X11) != X7 | X8 != X9 | f__integer__(0) != X14 | X7 != X15 | ~p__less_equal__(X14,X15) | X7 != X16 | X5 != X17 | ~p__less__(X16,X17)) )),
% 10.18/2.00 inference(equality_resolution,[],[f99])).
% 10.18/2.00 tff(f108,plain,(
% 10.18/2.00 ( ! [X2 : general,X3 : general,X10 : $int,X11 : $int,X8 : general,X6 : general,X9 : general,X7 : general,X14 : general,X4 : general,X16 : general,X17 : general,X15 : general,X5 : general,X12 : $int,X13 : $int] : (div(X4,X5,X2,X3) | X2 != X6 | X3 != X7 | X4 != X8 | f__integer__($sum(X10,X11)) != X9 | $product(X12,X13) != X10 | f__integer__(X12) != X5 | f__integer__(X13) != X6 | f__integer__(X11) != X7 | X8 != X9 | f__integer__(0) != X14 | X7 != X15 | ~p__less_equal__(X14,X15) | X7 != X16 | X5 != X17 | ~p__less__(X16,X17)) )),
% 10.18/2.00 inference(equality_resolution,[],[f107])).
% 10.18/2.00 tff(f109,plain,(
% 10.18/2.00 ( ! [X3 : general,X10 : $int,X11 : $int,X8 : general,X6 : general,X9 : general,X7 : general,X14 : general,X4 : general,X16 : general,X17 : general,X15 : general,X5 : general,X12 : $int,X13 : $int] : (div(X4,X5,X6,X3) | X3 != X7 | X4 != X8 | f__integer__($sum(X10,X11)) != X9 | $product(X12,X13) != X10 | f__integer__(X12) != X5 | f__integer__(X13) != X6 | f__integer__(X11) != X7 | X8 != X9 | f__integer__(0) != X14 | X7 != X15 | ~p__less_equal__(X14,X15) | X7 != X16 | X5 != X17 | ~p__less__(X16,X17)) )),
% 10.18/2.00 inference(equality_resolution,[],[f108])).
% 10.18/2.00 tff(f110,plain,(
% 10.18/2.00 ( ! [X10 : $int,X11 : $int,X8 : general,X6 : general,X9 : general,X7 : general,X14 : general,X4 : general,X16 : general,X17 : general,X15 : general,X5 : general,X12 : $int,X13 : $int] : (div(X4,X5,X6,X7) | X4 != X8 | f__integer__($sum(X10,X11)) != X9 | $product(X12,X13) != X10 | f__integer__(X12) != X5 | f__integer__(X13) != X6 | f__integer__(X11) != X7 | X8 != X9 | f__integer__(0) != X14 | X7 != X15 | ~p__less_equal__(X14,X15) | X7 != X16 | X5 != X17 | ~p__less__(X16,X17)) )),
% 10.18/2.00 inference(equality_resolution,[],[f109])).
% 10.18/2.00 tff(f111,plain,(
% 10.18/2.00 ( ! [X10 : $int,X11 : $int,X8 : general,X6 : general,X9 : general,X7 : general,X14 : general,X16 : general,X17 : general,X15 : general,X5 : general,X12 : $int,X13 : $int] : (div(X8,X5,X6,X7) | f__integer__($sum(X10,X11)) != X9 | $product(X12,X13) != X10 | f__integer__(X12) != X5 | f__integer__(X13) != X6 | f__integer__(X11) != X7 | X8 != X9 | f__integer__(0) != X14 | X7 != X15 | ~p__less_equal__(X14,X15) | X7 != X16 | X5 != X17 | ~p__less__(X16,X17)) )),
% 10.18/2.00 inference(equality_resolution,[],[f110])).
% 10.18/2.00 tff(f112,plain,(
% 10.18/2.00 ( ! [X10 : $int,X11 : $int,X8 : general,X6 : general,X7 : general,X14 : general,X16 : general,X17 : general,X15 : general,X5 : general,X12 : $int,X13 : $int] : (div(X8,X5,X6,X7) | $product(X12,X13) != X10 | f__integer__(X12) != X5 | f__integer__(X13) != X6 | f__integer__(X11) != X7 | f__integer__($sum(X10,X11)) != X8 | f__integer__(0) != X14 | X7 != X15 | ~p__less_equal__(X14,X15) | X7 != X16 | X5 != X17 | ~p__less__(X16,X17)) )),
% 10.18/2.00 inference(equality_resolution,[],[f111])).
% 10.18/2.00 tff(f113,plain,(
% 10.18/2.00 ( ! [X11 : $int,X8 : general,X6 : general,X7 : general,X14 : general,X16 : general,X17 : general,X15 : general,X5 : general,X12 : $int,X13 : $int] : (div(X8,X5,X6,X7) | f__integer__(X12) != X5 | f__integer__(X13) != X6 | f__integer__(X11) != X7 | f__integer__($sum($product(X12,X13),X11)) != X8 | f__integer__(0) != X14 | X7 != X15 | ~p__less_equal__(X14,X15) | X7 != X16 | X5 != X17 | ~p__less__(X16,X17)) )),
% 10.18/2.00 inference(equality_resolution,[],[f112])).
% 10.18/2.00 tff(f114,plain,(
% 10.18/2.00 ( ! [X11 : $int,X8 : general,X6 : general,X7 : general,X14 : general,X16 : general,X17 : general,X15 : general,X12 : $int,X13 : $int] : (div(X8,f__integer__(X12),X6,X7) | f__integer__(X13) != X6 | f__integer__(X11) != X7 | f__integer__($sum($product(X12,X13),X11)) != X8 | f__integer__(0) != X14 | X7 != X15 | ~p__less_equal__(X14,X15) | X7 != X16 | f__integer__(X12) != X17 | ~p__less__(X16,X17)) )),
% 10.18/2.00 inference(equality_resolution,[],[f113])).
% 10.18/2.00 tff(f115,plain,(
% 10.18/2.00 ( ! [X11 : $int,X8 : general,X7 : general,X14 : general,X16 : general,X17 : general,X15 : general,X12 : $int,X13 : $int] : (div(X8,f__integer__(X12),f__integer__(X13),X7) | f__integer__(X11) != X7 | f__integer__($sum($product(X12,X13),X11)) != X8 | f__integer__(0) != X14 | X7 != X15 | ~p__less_equal__(X14,X15) | X7 != X16 | f__integer__(X12) != X17 | ~p__less__(X16,X17)) )),
% 10.18/2.00 inference(equality_resolution,[],[f114])).
% 10.18/2.00 tff(f116,plain,(
% 10.18/2.00 ( ! [X11 : $int,X8 : general,X16 : general,X14 : general,X17 : general,X15 : general,X12 : $int,X13 : $int] : (div(X8,f__integer__(X12),f__integer__(X13),f__integer__(X11)) | f__integer__($sum($product(X12,X13),X11)) != X8 | f__integer__(0) != X14 | f__integer__(X11) != X15 | ~p__less_equal__(X14,X15) | f__integer__(X11) != X16 | f__integer__(X12) != X17 | ~p__less__(X16,X17)) )),
% 10.18/2.00 inference(equality_resolution,[],[f115])).
% 10.18/2.00 tff(f117,plain,(
% 10.18/2.00 ( ! [X11 : $int,X16 : general,X14 : general,X17 : general,X15 : general,X12 : $int,X13 : $int] : (div(f__integer__($sum($product(X12,X13),X11)),f__integer__(X12),f__integer__(X13),f__integer__(X11)) | f__integer__(0) != X14 | f__integer__(X11) != X15 | ~p__less_equal__(X14,X15) | f__integer__(X11) != X16 | f__integer__(X12) != X17 | ~p__less__(X16,X17)) )),
% 10.18/2.00 inference(equality_resolution,[],[f116])).
% 10.18/2.00 tff(f118,plain,(
% 10.18/2.00 ( ! [X11 : $int,X16 : general,X17 : general,X15 : general,X12 : $int,X13 : $int] : (div(f__integer__($sum($product(X12,X13),X11)),f__integer__(X12),f__integer__(X13),f__integer__(X11)) | f__integer__(X11) != X15 | ~p__less_equal__(f__integer__(0),X15) | f__integer__(X11) != X16 | f__integer__(X12) != X17 | ~p__less__(X16,X17)) )),
% 10.18/2.00 inference(equality_resolution,[],[f117])).
% 10.18/2.00 tff(f119,plain,(
% 10.18/2.00 ( ! [X11 : $int,X16 : general,X17 : general,X12 : $int,X13 : $int] : (div(f__integer__($sum($product(X12,X13),X11)),f__integer__(X12),f__integer__(X13),f__integer__(X11)) | ~p__less_equal__(f__integer__(0),f__integer__(X11)) | f__integer__(X11) != X16 | f__integer__(X12) != X17 | ~p__less__(X16,X17)) )),
% 10.18/2.00 inference(equality_resolution,[],[f118])).
% 10.18/2.00 tff(f120,plain,(
% 10.18/2.00 ( ! [X11 : $int,X17 : general,X12 : $int,X13 : $int] : (div(f__integer__($sum($product(X12,X13),X11)),f__integer__(X12),f__integer__(X13),f__integer__(X11)) | ~p__less_equal__(f__integer__(0),f__integer__(X11)) | f__integer__(X12) != X17 | ~p__less__(f__integer__(X11),X17)) )),
% 10.18/2.00 inference(equality_resolution,[],[f119])).
% 10.18/2.00 tff(f121,plain,(
% 10.18/2.00 ( ! [X11 : $int,X12 : $int,X13 : $int] : (div(f__integer__($sum($product(X12,X13),X11)),f__integer__(X12),f__integer__(X13),f__integer__(X11)) | ~p__less_equal__(f__integer__(0),f__integer__(X11)) | ~p__less__(f__integer__(X11),f__integer__(X12))) )),
% 10.18/2.00 inference(equality_resolution,[],[f120])).
% 10.18/2.00 tff(f122,definition,(
% 10.18/2.00 sF19 = $sum(sK16,1)),
% 10.18/2.00 introduced(definition,[new_symbols(definition,[sF19])],[function_definition])).
% 10.18/2.00 tff(f123,plain,(
% 10.18/2.00 $sum(sK16,1) = sF19),
% 10.18/2.00 inference(reorient_equations,[],[f122])).
% 10.18/2.00 tff(f124,definition,(
% 10.18/2.00 sF20 = f__integer__(sF19)),
% 10.18/2.00 introduced(definition,[new_symbols(definition,[sF20])],[function_definition])).
% 10.18/2.00 tff(f125,plain,(
% 10.18/2.00 f__integer__(sF19) = sF20),
% 10.18/2.00 inference(reorient_equations,[],[f124])).
% 10.18/2.00 tff(f126,definition,(
% 10.18/2.00 sF21 = f__integer__(sK17)),
% 10.18/2.00 introduced(definition,[new_symbols(definition,[sF21])],[function_definition])).
% 10.18/2.00 tff(f127,plain,(
% 10.18/2.00 f__integer__(sK17) = sF21),
% 10.18/2.00 inference(reorient_equations,[],[f126])).
% 10.18/2.00 tff(f128,definition,(
% 10.18/2.00 sF22 = $sum(sK18,1)),
% 10.18/2.00 introduced(definition,[new_symbols(definition,[sF22])],[function_definition])).
% 10.18/2.00 tff(f129,plain,(
% 10.18/2.00 $sum(sK18,1) = sF22),
% 10.18/2.00 inference(reorient_equations,[],[f128])).
% 10.18/2.00 tff(f130,definition,(
% 10.18/2.00 sF23 = f__integer__(sF22)),
% 10.18/2.00 introduced(definition,[new_symbols(definition,[sF23])],[function_definition])).
% 10.18/2.00 tff(f131,plain,(
% 10.18/2.00 f__integer__(sF22) = sF23),
% 10.18/2.00 inference(reorient_equations,[],[f130])).
% 10.18/2.00 tff(f132,definition,(
% 10.18/2.00 sF24 = f__integer__(0)),
% 10.18/2.00 introduced(definition,[new_symbols(definition,[sF24])],[function_definition])).
% 10.18/2.00 tff(f133,plain,(
% 10.18/2.00 f__integer__(0) = sF24),
% 10.18/2.00 inference(reorient_equations,[],[f132])).
% 10.18/2.00 tff(f134,plain,(
% 10.18/2.00 ~div(sF20,sF21,sF23,sF24)),
% 10.18/2.00 inference(definition_folding,[],[f102,f133,f131,f129,f127,f125,f123])).
% 10.18/2.00 tff(f135,definition,(
% 10.18/2.00 sF25 = f__integer__(sK16)),
% 10.18/2.00 introduced(definition,[new_symbols(definition,[sF25])],[function_definition])).
% 10.18/2.00 tff(f136,plain,(
% 10.18/2.00 f__integer__(sK16) = sF25),
% 10.18/2.00 inference(reorient_equations,[],[f135])).
% 10.18/2.00 tff(f137,definition,(
% 10.18/2.00 sF26 = f__integer__(sK18)),
% 10.18/2.00 introduced(definition,[new_symbols(definition,[sF26])],[function_definition])).
% 10.18/2.00 tff(f138,plain,(
% 10.18/2.00 f__integer__(sK18) = sF26),
% 10.18/2.00 inference(reorient_equations,[],[f137])).
% 10.18/2.00 tff(f139,definition,(
% 10.18/2.00 sF27 = $uminus(1)),
% 10.18/2.00 introduced(definition,[new_symbols(definition,[sF27])],[function_definition])).
% 10.18/2.00 tff(f140,plain,(
% 10.18/2.00 $uminus(1) = sF27),
% 10.18/2.00 inference(reorient_equations,[],[f139])).
% 10.18/2.00 tff(f141,definition,(
% 10.18/2.00 sF28 = $sum(sK17,sF27)),
% 10.18/2.00 introduced(definition,[new_symbols(definition,[sF28])],[function_definition])).
% 10.18/2.00 tff(f142,plain,(
% 10.18/2.00 $sum(sK17,sF27) = sF28),
% 10.18/2.00 inference(reorient_equations,[],[f141])).
% 10.18/2.00 tff(f143,definition,(
% 10.18/2.00 sF29 = f__integer__(sF28)),
% 10.18/2.00 introduced(definition,[new_symbols(definition,[sF29])],[function_definition])).
% 10.18/2.00 tff(f144,plain,(
% 10.18/2.00 f__integer__(sF28) = sF29),
% 10.18/2.00 inference(reorient_equations,[],[f143])).
% 10.18/2.00 tff(f145,plain,(
% 10.18/2.00 div(sF25,sF21,sF26,sF29)),
% 10.18/2.00 inference(definition_folding,[],[f101,f144,f142,f140,f138,f127,f136])).
% 10.18/2.00 tff(f147,plain,(
% 10.18/2.00 sF27 = -1),
% 10.18/2.00 inference(evaluation,[],[f140])).
% 10.18/2.00 tff(f148,plain,(
% 10.18/2.00 sF19 = $sum(1,sK16)),
% 10.18/2.00 inference(forward_demodulation,[],[f123,f23])).
% 10.18/2.00 tff(f149,plain,(
% 10.18/2.00 sF22 = $sum(1,sK18)),
% 10.18/2.00 inference(forward_demodulation,[],[f129,f23])).
% 10.18/2.00 tff(f150,plain,(
% 10.18/2.00 sF28 = $sum(sK17,-1)),
% 10.18/2.00 inference(forward_demodulation,[],[f142,f147])).
% 10.18/2.00 tff(f151,plain,(
% 10.18/2.00 sF28 = $sum(-1,sK17)),
% 10.18/2.00 inference(forward_demodulation,[],[f150,f23])).
% 10.18/2.00 tff(f168,plain,(
% 10.18/2.00 ( ! [X0 : general] : (p__less_equal__(X0,X0)) )),
% 10.18/2.00 inference(factoring,[],[f75])).
% 10.18/2.00 tff(f198,plain,(
% 10.18/2.00 ( ! [X0 : $int,X1 : $int] : ($less(X1,$sum(1,X0)) | $less(X0,X1)) )),
% 10.18/2.00 inference(superposition,[],[f32,f23])).
% 10.18/2.00 tff(f210,plain,(
% 10.18/2.00 ( ! [X0 : $int] : (f__integer__(X0) != sF25 | sK16 = X0) )),
% 10.18/2.00 inference(superposition,[],[f67,f136])).
% 10.18/2.00 tff(f211,plain,(
% 10.18/2.00 ( ! [X0 : $int] : (f__integer__(X0) != sF21 | sK17 = X0) )),
% 10.18/2.00 inference(superposition,[],[f67,f127])).
% 10.18/2.00 tff(f212,plain,(
% 10.18/2.00 ( ! [X0 : $int] : (f__integer__(X0) != sF26 | sK18 = X0) )),
% 10.18/2.00 inference(superposition,[],[f67,f138])).
% 10.18/2.00 tff(f215,plain,(
% 10.18/2.00 ( ! [X0 : $int] : (f__integer__(X0) != sF29 | sF28 = X0) )),
% 10.18/2.00 inference(superposition,[],[f67,f144])).
% 10.18/2.00 tff(f225,plain,(
% 10.18/2.00 ( ! [X0 : $int] : (~p__less_equal__(sF21,f__integer__(X0)) | ~$less(X0,sK17)) )),
% 10.18/2.00 inference(superposition,[],[f71,f127])).
% 10.18/2.00 tff(f236,plain,(
% 10.18/2.00 ( ! [X0 : $int] : (~p__less_equal__(f__integer__(X0),sF29) | ~$less(sF28,X0)) )),
% 10.18/2.00 inference(superposition,[],[f71,f144])).
% 10.18/2.00 tff(f245,plain,(
% 10.18/2.00 ( ! [X0 : $int] : (p__less_equal__(f__integer__(X0),sF24) | $less(0,X0)) )),
% 10.18/2.00 inference(superposition,[],[f72,f133])).
% 10.18/2.00 tff(f320,plain,(
% 10.18/2.00 ( ! [X0 : $int,X1 : $int] : ($uminus($sum($uminus(X0),X1)) = $sum($uminus(X1),X0)) )),
% 10.18/2.00 inference(superposition,[],[f26,f33])).
% 10.18/2.00 tff(f370,plain,(
% 10.18/2.00 ( ! [X0 : $int,X1 : $int] : ($sum(0,X1) = $sum(X0,$sum($uminus(X0),X1))) )),
% 10.18/2.00 inference(superposition,[],[f24,f27])).
% 10.18/2.00 tff(f374,plain,(
% 10.18/2.00 ( ! [X0 : $int] : ($sum(1,$sum(sK16,X0)) = $sum(sF19,X0)) )),
% 10.18/2.00 inference(superposition,[],[f24,f148])).
% 10.18/2.00 tff(f377,plain,(
% 10.18/2.00 ( ! [X0 : $int] : ($sum(-1,$sum(sK17,X0)) = $sum(sF28,X0)) )),
% 10.18/2.00 inference(superposition,[],[f24,f151])).
% 10.18/2.00 tff(f390,plain,(
% 10.18/2.00 ( ! [X0 : $int,X1 : $int] : ($sum(X0,$sum($uminus(X0),X1)) = X1) )),
% 10.18/2.00 inference(evaluation,[],[f370])).
% 10.18/2.00 tff(f421,plain,(
% 10.18/2.00 sF29 = sK5(sF25,sF21,sF26,sF29)),
% 10.18/2.00 inference(resolution,[],[f95,f145])).
% 10.18/2.00 tff(f422,plain,(
% 10.18/2.00 sF26 = sK4(sF25,sF21,sF26,sF29)),
% 10.18/2.00 inference(resolution,[],[f96,f145])).
% 10.18/2.00 tff(f423,plain,(
% 10.18/2.00 sF21 = sK3(sF25,sF21,sF26,sF29)),
% 10.18/2.00 inference(resolution,[],[f97,f145])).
% 10.18/2.00 tff(f424,plain,(
% 10.18/2.00 sF25 = sK2(sF25,sF21,sF26,sF29)),
% 10.18/2.00 inference(resolution,[],[f98,f145])).
% 10.18/2.00 tff(f425,plain,(
% 10.18/2.00 ( ! [X0 : $int,X1 : $int] : ($product(X0,$sum(1,X1)) = $sum(X0,$product(X0,X1))) )),
% 10.18/2.00 inference(superposition,[],[f38,f36])).
% 10.18/2.00 tff(f450,plain,(
% 10.18/2.00 f__integer__(0) = sK12(sF25,sF21,sF26,sF29)),
% 10.18/2.00 inference(resolution,[],[f87,f145])).
% 10.18/2.00 tff(f451,plain,(
% 10.18/2.00 sF24 = sK12(sF25,sF21,sF26,sF29)),
% 10.18/2.00 inference(forward_demodulation,[],[f450,f133])).
% 10.18/2.00 tff(f469,plain,(
% 10.18/2.00 sK3(sF25,sF21,sF26,sF29) = sK15(sF25,sF21,sF26,sF29)),
% 10.18/2.00 inference(resolution,[],[f83,f145])).
% 10.18/2.00 tff(f470,plain,(
% 10.18/2.00 sF21 = sK15(sF25,sF21,sF26,sF29)),
% 10.18/2.00 inference(forward_demodulation,[],[f469,f423])).
% 10.18/2.00 tff(f473,plain,(
% 10.18/2.00 sK5(sF25,sF21,sF26,sF29) = sK14(sF25,sF21,sF26,sF29)),
% 10.18/2.00 inference(resolution,[],[f84,f145])).
% 10.18/2.00 tff(f474,plain,(
% 10.18/2.00 sF29 = sK14(sF25,sF21,sF26,sF29)),
% 10.18/2.00 inference(forward_demodulation,[],[f473,f421])).
% 10.18/2.00 tff(f475,plain,(
% 10.18/2.00 p__less__(sF29,sK15(sF25,sF21,sF26,sF29)) | ~div(sF25,sF21,sF26,sF29)),
% 10.18/2.00 inference(superposition,[],[f82,f474])).
% 10.18/2.00 tff(f476,plain,(
% 10.18/2.00 p__less__(sF29,sK15(sF25,sF21,sF26,sF29))),
% 10.18/2.00 inference(forward_subsumption_resolution,[],[f475,f145])).
% 10.18/2.00 tff(f477,plain,(
% 10.18/2.00 p__less__(sF29,sF21)),
% 10.18/2.00 inference(forward_demodulation,[],[f476,f470])).
% 10.18/2.00 tff(f483,plain,(
% 10.18/2.00 p__less_equal__(sF29,sF21)),
% 10.18/2.00 inference(resolution,[],[f477,f77])).
% 10.18/2.00 tff(f484,plain,(
% 10.18/2.00 sK5(sF25,sF21,sF26,sF29) = sK13(sF25,sF21,sF26,sF29)),
% 10.18/2.00 inference(resolution,[],[f86,f145])).
% 10.18/2.00 tff(f485,plain,(
% 10.18/2.00 sF29 = sK13(sF25,sF21,sF26,sF29)),
% 10.18/2.00 inference(forward_demodulation,[],[f484,f421])).
% 10.18/2.00 tff(f487,plain,(
% 10.18/2.00 ( ! [X0 : general] : (~p__less_equal__(X0,sF29) | p__less_equal__(X0,sF21)) )),
% 10.18/2.00 inference(resolution,[],[f483,f74])).
% 10.18/2.00 tff(f489,plain,(
% 10.18/2.00 sK6(sF25,sF21,sF26,sF29) = sK7(sF25,sF21,sF26,sF29)),
% 10.18/2.00 inference(resolution,[],[f88,f145])).
% 10.18/2.00 tff(f494,plain,(
% 10.18/2.00 sK2(sF25,sF21,sF26,sF29) = sK6(sF25,sF21,sF26,sF29)),
% 10.18/2.00 inference(resolution,[],[f94,f145])).
% 10.18/2.00 tff(f495,plain,(
% 10.18/2.00 sF25 = sK6(sF25,sF21,sF26,sF29)),
% 10.18/2.00 inference(forward_demodulation,[],[f494,f424])).
% 10.18/2.00 tff(f496,plain,(
% 10.18/2.00 sK5(sF25,sF21,sF26,sF29) = f__integer__(sK9(sF25,sF21,sF26,sF29))),
% 10.18/2.00 inference(resolution,[],[f89,f145])).
% 10.18/2.00 tff(f497,plain,(
% 10.18/2.00 sF29 = f__integer__(sK9(sF25,sF21,sF26,sF29))),
% 10.18/2.00 inference(forward_demodulation,[],[f496,f421])).
% 10.18/2.00 tff(f506,plain,(
% 10.18/2.00 sK4(sF25,sF21,sF26,sF29) = f__integer__(sK11(sF25,sF21,sF26,sF29))),
% 10.18/2.00 inference(resolution,[],[f90,f145])).
% 10.18/2.00 tff(f507,plain,(
% 10.18/2.00 sF26 = f__integer__(sK11(sF25,sF21,sF26,sF29))),
% 10.18/2.00 inference(forward_demodulation,[],[f506,f422])).
% 10.18/2.00 tff(f508,plain,(
% 10.18/2.00 p__less_equal__(sK12(sF25,sF21,sF26,sF29),sF29) | ~div(sF25,sF21,sF26,sF29)),
% 10.18/2.00 inference(superposition,[],[f85,f485])).
% 10.18/2.00 tff(f509,plain,(
% 10.18/2.00 p__less_equal__(sK12(sF25,sF21,sF26,sF29),sF29)),
% 10.18/2.00 inference(forward_subsumption_resolution,[],[f508,f145])).
% 10.18/2.00 tff(f510,plain,(
% 10.18/2.00 p__less_equal__(sF24,sF29)),
% 10.18/2.00 inference(forward_demodulation,[],[f509,f451])).
% 10.18/2.00 tff(f511,plain,(
% 10.18/2.00 sK3(sF25,sF21,sF26,sF29) = f__integer__(sK10(sF25,sF21,sF26,sF29))),
% 10.18/2.00 inference(resolution,[],[f91,f145])).
% 10.18/2.00 tff(f512,plain,(
% 10.18/2.00 sF21 = f__integer__(sK10(sF25,sF21,sF26,sF29))),
% 10.18/2.00 inference(forward_demodulation,[],[f511,f423])).
% 10.18/2.00 tff(f513,plain,(
% 10.18/2.00 p__less_equal__(sF24,sF21)),
% 10.18/2.00 inference(resolution,[],[f510,f487])).
% 10.18/2.00 tff(f515,plain,(
% 10.18/2.00 ( ! [X0 : general] : (~p__less_equal__(X0,sF24) | p__less_equal__(X0,sF29)) )),
% 10.18/2.00 inference(resolution,[],[f510,f74])).
% 10.18/2.00 tff(f517,plain,(
% 10.18/2.00 sK8(sF25,sF21,sF26,sF29) = $product(sK10(sF25,sF21,sF26,sF29),sK11(sF25,sF21,sF26,sF29))),
% 10.18/2.00 inference(resolution,[],[f92,f145])).
% 10.18/2.00 tff(f518,plain,(
% 10.18/2.00 p__less__(sF24,sF21) | sF21 = sF24),
% 10.18/2.00 inference(resolution,[],[f513,f78])).
% 10.18/2.00 tff(f521,plain,(
% 10.18/2.00 sK7(sF25,sF21,sF26,sF29) = f__integer__($sum(sK8(sF25,sF21,sF26,sF29),sK9(sF25,sF21,sF26,sF29)))),
% 10.18/2.00 inference(resolution,[],[f93,f145])).
% 10.18/2.00 tff(f522,plain,(
% 10.18/2.00 sK6(sF25,sF21,sF26,sF29) = f__integer__($sum(sK8(sF25,sF21,sF26,sF29),sK9(sF25,sF21,sF26,sF29)))),
% 10.18/2.00 inference(forward_demodulation,[],[f521,f489])).
% 10.18/2.00 tff(f523,plain,(
% 10.18/2.00 sF25 = f__integer__($sum(sK8(sF25,sF21,sF26,sF29),sK9(sF25,sF21,sF26,sF29)))),
% 10.18/2.00 inference(forward_demodulation,[],[f522,f495])).
% 10.18/2.00 tff(f564,plain,(
% 10.18/2.00 ( ! [X0 : $int,X1 : $int] : (div(f__integer__($sum($product(X0,X1),0)),f__integer__(X0),f__integer__(X1),sF24) | ~p__less_equal__(sF24,sF24) | ~p__less__(sF24,f__integer__(X0))) )),
% 10.18/2.00 inference(superposition,[],[f121,f133])).
% 10.18/2.00 tff(f571,plain,(
% 10.18/2.00 ( ! [X0 : $int,X1 : $int] : (div(f__integer__($product(X0,X1)),f__integer__(X0),f__integer__(X1),sF24) | ~p__less_equal__(sF24,sF24) | ~p__less__(sF24,f__integer__(X0))) )),
% 10.18/2.00 inference(evaluation,[],[f564])).
% 10.18/2.00 tff(f581,plain,(
% 10.18/2.00 ( ! [X0 : $int,X1 : $int] : (div(f__integer__($product(X0,X1)),f__integer__(X0),f__integer__(X1),sF24) | ~p__less__(sF24,f__integer__(X0))) )),
% 10.18/2.00 inference(forward_subsumption_resolution,[],[f571,f168])).
% 10.18/2.00 tff(f1018,plain,(
% 10.18/2.00 sF21 != sF21 | sK17 = sK10(sF25,sF21,sF26,sF29)),
% 10.18/2.00 inference(superposition,[],[f211,f512])).
% 10.18/2.00 tff(f1025,plain,(
% 10.18/2.00 sK17 = sK10(sF25,sF21,sF26,sF29)),
% 10.18/2.00 inference(trivial_inequality_removal,[],[f1018])).
% 10.18/2.00 tff(f1033,plain,(
% 10.18/2.00 sF26 != sF26 | sK18 = sK11(sF25,sF21,sF26,sF29)),
% 10.18/2.00 inference(superposition,[],[f212,f507])).
% 10.18/2.00 tff(f1039,plain,(
% 10.18/2.00 sK18 = sK11(sF25,sF21,sF26,sF29)),
% 10.18/2.00 inference(trivial_inequality_removal,[],[f1033])).
% 10.18/2.00 tff(f1042,plain,(
% 10.18/2.00 sK8(sF25,sF21,sF26,sF29) = $product(sK10(sF25,sF21,sF26,sF29),sK18)),
% 10.18/2.00 inference(superposition,[],[f517,f1039])).
% 10.18/2.00 tff(f1044,plain,(
% 10.18/2.00 sK8(sF25,sF21,sF26,sF29) = $product(sK18,sK10(sF25,sF21,sF26,sF29))),
% 10.18/2.00 inference(forward_demodulation,[],[f1042,f34])).
% 10.18/2.00 tff(f1045,plain,(
% 10.18/2.00 sK8(sF25,sF21,sF26,sF29) = $product(sK18,sK17)),
% 10.18/2.00 inference(forward_demodulation,[],[f1044,f1025])).
% 10.18/2.00 tff(f1046,plain,(
% 10.18/2.00 sK8(sF25,sF21,sF26,sF29) = $product(sK17,sK18)),
% 10.18/2.00 inference(forward_demodulation,[],[f1045,f34])).
% 10.18/2.00 tff(f1107,plain,(
% 10.18/2.00 sF29 != sF29 | sF28 = sK9(sF25,sF21,sF26,sF29)),
% 10.18/2.00 inference(superposition,[],[f215,f497])).
% 10.18/2.00 tff(f1115,plain,(
% 10.18/2.00 sF28 = sK9(sF25,sF21,sF26,sF29)),
% 10.18/2.00 inference(trivial_inequality_removal,[],[f1107])).
% 10.18/2.00 tff(f1119,plain,(
% 10.18/2.00 sF25 = f__integer__($sum(sK8(sF25,sF21,sF26,sF29),sF28))),
% 10.18/2.00 inference(superposition,[],[f523,f1115])).
% 10.18/2.00 tff(f1121,plain,(
% 10.18/2.00 sF25 = f__integer__($sum(sF28,sK8(sF25,sF21,sF26,sF29)))),
% 10.18/2.00 inference(forward_demodulation,[],[f1119,f23])).
% 10.18/2.00 tff(f1122,plain,(
% 10.18/2.00 sF25 = f__integer__($sum(sF28,$product(sK17,sK18)))),
% 10.18/2.00 inference(forward_demodulation,[],[f1121,f1046])).
% 10.18/2.00 tff(f1163,plain,(
% 10.18/2.00 ~$less(0,sK17) | ~p__less_equal__(sF21,sF24)),
% 10.18/2.00 inference(superposition,[],[f225,f133])).
% 10.18/2.00 tff(f1312,plain,(
% 10.18/2.00 sF25 != sF25 | sK16 = $sum(sF28,$product(sK17,sK18))),
% 10.18/2.00 inference(superposition,[],[f210,f1122])).
% 10.18/2.00 tff(f1331,plain,(
% 10.18/2.00 sK16 = $sum(sF28,$product(sK17,sK18))),
% 10.18/2.00 inference(trivial_inequality_removal,[],[f1312])).
% 10.18/2.00 tff(f1687,plain,(
% 10.18/2.00 ( ! [X0 : $int] : (p__less_equal__(f__integer__(X0),sF29) | $less(0,X0)) )),
% 10.18/2.00 inference(resolution,[],[f245,f515])).
% 10.18/2.00 tff(f1751,plain,(
% 10.18/2.00 ( ! [X0 : $int] : (~$less(sF28,X0) | $less(0,X0)) )),
% 10.18/2.00 inference(resolution,[],[f1687,f236])).
% 10.18/2.00 tff(f1877,plain,(
% 10.18/2.00 ( ! [X0 : $int] : ($less(0,$sum(1,X0)) | $less(X0,sF28)) )),
% 10.18/2.00 inference(resolution,[],[f198,f1751])).
% 10.18/2.00 tff(f2020,plain,(
% 10.18/2.00 ( ! [X0 : $int,X1 : $int] : ($uminus(X0) = $sum(X1,$uminus($sum(X0,X1)))) )),
% 10.18/2.00 inference(superposition,[],[f390,f26])).
% 10.18/2.00 tff(f2146,plain,(
% 10.18/2.00 $sum(1,0) = $sum(sF19,$uminus(sK16))),
% 10.18/2.00 inference(superposition,[],[f374,f27])).
% 10.18/2.00 tff(f2153,plain,(
% 10.18/2.00 1 = $sum(sF19,$uminus(sK16))),
% 10.18/2.00 inference(evaluation,[],[f2146])).
% 10.18/2.00 tff(f2252,plain,(
% 10.18/2.00 ( ! [X0 : $int,X1 : $int] : ($uminus(X0) = $sum($uminus($sum($uminus($uminus(X1)),X0)),X1)) )),
% 10.18/2.00 inference(superposition,[],[f320,f390])).
% 10.18/2.00 tff(f2266,plain,(
% 10.18/2.00 ( ! [X0 : $int,X1 : $int] : ($uminus(X0) = $sum($uminus($sum(X1,X0)),X1)) )),
% 10.18/2.00 inference(evaluation,[],[f2252])).
% 10.18/2.00 tff(f2273,plain,(
% 10.18/2.00 ( ! [X0 : $int,X1 : $int] : ($uminus(X0) = $sum(X1,$uminus($sum(X1,X0)))) )),
% 10.18/2.00 inference(forward_demodulation,[],[f2266,f23])).
% 10.18/2.00 tff(f2957,plain,(
% 10.18/2.00 ( ! [X0 : $int] : ($less(0,X0) | $less($sum($uminus(1),X0),sF28)) )),
% 10.18/2.00 inference(superposition,[],[f1877,f390])).
% 10.18/2.00 tff(f2965,plain,(
% 10.18/2.00 ( ! [X0 : $int] : ($less($sum(-1,X0),sF28) | $less(0,X0)) )),
% 10.18/2.00 inference(evaluation,[],[f2957])).
% 10.18/2.00 tff(f3058,plain,(
% 10.18/2.00 ( ! [X0 : $int] : ($product(X0,sF22) = $sum(X0,$product(X0,sK18))) )),
% 10.18/2.00 inference(superposition,[],[f425,f149])).
% 10.18/2.00 tff(f4967,plain,(
% 10.18/2.00 $less(sF28,sF28) | $less(0,sK17)),
% 10.18/2.00 inference(superposition,[],[f2965,f151])).
% 10.18/2.00 tff(f4980,plain,(
% 10.18/2.00 $less(0,sK17)),
% 10.18/2.00 inference(forward_subsumption_resolution,[],[f4967,f28])).
% 10.18/2.00 tff(f27145,plain,(
% 10.18/2.00 ~p__less_equal__(sF21,sF24)),
% 10.18/2.00 inference(resolution,[],[f1163,f4980])).
% 10.18/2.00 tff(f30776,plain,(
% 10.18/2.00 $uminus(sF19) = $sum($uminus(sK16),$uminus(1))),
% 10.18/2.00 inference(superposition,[],[f2020,f2153])).
% 10.18/2.00 tff(f30932,plain,(
% 10.18/2.00 $uminus(sF19) = $sum($uminus(sK16),-1)),
% 10.18/2.00 inference(evaluation,[],[f30776])).
% 10.18/2.00 tff(f30972,plain,(
% 10.18/2.00 $uminus(sF19) = $sum(-1,$uminus(sK16))),
% 10.18/2.00 inference(forward_demodulation,[],[f30932,f23])).
% 10.18/2.00 tff(f33529,plain,(
% 10.18/2.00 $sum(sF28,$product(sK17,sK18)) = $sum(-1,$product(sK17,sF22))),
% 10.18/2.00 inference(superposition,[],[f377,f3058])).
% 10.18/2.00 tff(f33630,plain,(
% 10.18/2.00 sK16 = $sum(-1,$product(sK17,sF22))),
% 10.18/2.00 inference(forward_demodulation,[],[f33529,f1331])).
% 10.18/2.00 tff(f34192,plain,(
% 10.18/2.00 $sum(-1,$uminus(sK16)) = $uminus($product(sK17,sF22))),
% 10.18/2.00 inference(superposition,[],[f2273,f33630])).
% 10.18/2.00 tff(f34205,plain,(
% 10.18/2.00 $uminus(sF19) = $uminus($product(sK17,sF22))),
% 10.18/2.00 inference(forward_demodulation,[],[f34192,f30972])).
% 10.18/2.00 tff(f36702,plain,(
% 10.18/2.00 $product(sK17,sF22) = $uminus($uminus(sF19))),
% 10.18/2.00 inference(superposition,[],[f33,f34205])).
% 10.18/2.00 tff(f36726,plain,(
% 10.18/2.00 sF19 = $product(sK17,sF22)),
% 10.18/2.00 inference(evaluation,[],[f36702])).
% 10.18/2.00 tff(f36909,plain,(
% 10.18/2.00 div(f__integer__(sF19),f__integer__(sK17),f__integer__(sF22),sF24) | ~p__less__(sF24,f__integer__(sK17))),
% 10.18/2.00 inference(superposition,[],[f581,f36726])).
% 10.18/2.00 tff(f36986,plain,(
% 10.18/2.00 div(f__integer__(sF19),f__integer__(sK17),sF23,sF24) | ~p__less__(sF24,f__integer__(sK17))),
% 10.18/2.00 inference(forward_demodulation,[],[f36909,f131])).
% 10.18/2.00 tff(f37035,plain,(
% 10.18/2.00 div(f__integer__(sF19),sF21,sF23,sF24) | ~p__less__(sF24,f__integer__(sK17))),
% 10.18/2.00 inference(forward_demodulation,[],[f36986,f127])).
% 10.18/2.00 tff(f37070,plain,(
% 10.18/2.00 div(sF20,sF21,sF23,sF24) | ~p__less__(sF24,f__integer__(sK17))),
% 10.18/2.00 inference(forward_demodulation,[],[f37035,f125])).
% 10.18/2.00 tff(f37085,plain,(
% 10.18/2.00 ~p__less__(sF24,f__integer__(sK17))),
% 10.18/2.00 inference(forward_subsumption_resolution,[],[f37070,f134])).
% 10.18/2.00 tff(f37093,plain,(
% 10.18/2.00 ~p__less__(sF24,sF21)),
% 10.18/2.00 inference(forward_demodulation,[],[f37085,f127])).
% 10.18/2.00 tff(f37250,plain,(
% 10.18/2.00 sF21 = sF24),
% 10.18/2.00 inference(resolution,[],[f37093,f518])).
% 10.18/2.00 tff(f37510,plain,(
% 10.18/2.00 ~p__less_equal__(sF21,sF21)),
% 10.18/2.00 inference(superposition,[],[f27145,f37250])).
% 10.18/2.00 tff(f37533,plain,(
% 10.18/2.00 $false),
% 10.18/2.00 inference(forward_subsumption_resolution,[],[f37510,f168])).
% 10.18/2.00 % SZS output end Proof for theBenchmark
% 10.18/2.00 % (223822)------------------------------
% 10.18/2.00 % (223822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.18/2.00 % (223822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.18/2.00 % (223822)CaDiCaL version: 2.1.3
% 10.18/2.00 % (223822)Termination reason: Refutation
% 10.18/2.00 % (223822)Time elapsed: 1.024 s
% 10.18/2.00 % (223822)Peak memory usage: 25 MB
% 10.18/2.00 % (223822)Instructions burned: 1852 (million)
% 10.18/2.00 % (223767)Success in time 1.776 s
% 10.18/2.00 % Vampire exiting
%------------------------------------------------------------------------------