%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWX081_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 : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:46:27 PM UTC 2026
% Result : Theorem 7.06s 2.51s
% Output : Refutation 7.06s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX081_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.11/0.23 % Computer : n002.cluster.edu
% 0.11/0.23 % Model : x86_64 x86_64
% 0.11/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.23 % Memory : 8046.5625MB
% 0.11/0.23 % OS : Linux 6.8.0-71-generic
% 0.11/0.23 % CPULimit : 300
% 0.11/0.23 % WCLimit : 300
% 0.11/0.23 % DateTime : Mon Sep 28 15:02:22 UTC 2026
% 0.11/0.23 % CPUTime :
% 0.11/0.23 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.28 Running first-order model finding
% 0.11/0.28 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
% 5.42/1.07 % (417481)Will run a generic schedule for satisfiability detection.
% 5.42/1.07 % (417486)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=489780213_2999 on theBenchmark for (2999ds/0Mi)
% 5.42/1.07 % (417486)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 5.42/1.07 % (417486)Terminated due to inappropriate strategy.
% 5.42/1.07 % (417486)------------------------------
% 5.42/1.07 % (417486)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.42/1.07 % (417486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.42/1.07 % (417486)CaDiCaL version: 2.1.3
% 5.42/1.07 % (417486)Termination reason: Inappropriate
% 5.42/1.07 % (417486)Time elapsed: 0.002 s
% 5.42/1.07 % (417486)Peak memory usage: 11 MB
% 5.42/1.07 % (417486)Instructions burned: 2 (million)
% 5.42/1.07 % (417487)% WARNING: option uhcvi not known.
% 5.42/1.07 % (417486)------------------------------
% 5.42/1.07 % (417486)------------------------------
% 5.42/1.07 % (417487)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3471563435:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 5.42/1.07 % (417488)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1935714433:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 5.42/1.07 % (417490)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3607331307:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 5.42/1.07 % (417491)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=840818423:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 5.42/1.07 % (417489)dis+10_1_sil=32000:sp=arity:random_seed=2423955779:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 5.42/1.07 % (417492)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1174598202:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 5.42/1.07 % (417494)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=755509895:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 5.42/1.07 % (417494)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 5.42/1.07 % (417494)Terminated due to inappropriate strategy.
% 5.42/1.07 % (417494)------------------------------
% 5.42/1.07 % (417494)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.42/1.07 % (417494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.42/1.07 % (417494)CaDiCaL version: 2.1.3
% 5.42/1.07 % (417494)Termination reason: Inappropriate
% 5.42/1.07 % (417494)Time elapsed: 0.001 s
% 5.42/1.07 % (417494)Peak memory usage: 10 MB
% 5.42/1.07 % (417494)Instructions burned: 2 (million)
% 5.42/1.07 % (417494)------------------------------
% 5.42/1.07 % (417494)------------------------------
% 5.42/1.07 % (417502)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=420021085:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 5.42/1.07 % (417489)Instruction limit reached!
% 5.42/1.07 % (417489)------------------------------
% 5.42/1.07 % (417489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.42/1.07 % (417489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.42/1.07 % (417489)CaDiCaL version: 2.1.3
% 5.42/1.07 % (417489)Termination reason: Instruction limit
% 5.42/1.07 % (417489)Termination phase: Saturation
% 5.42/1.07 % (417489)Time elapsed: 0.108 s
% 5.42/1.07 % (417489)Peak memory usage: 13 MB
% 5.42/1.07 % (417489)Instructions burned: 103 (million)
% 5.42/1.07 % (417502)Instruction limit reached!
% 5.42/1.07 % (417502)------------------------------
% 5.42/1.07 % (417502)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.42/1.07 % (417502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.42/1.07 % (417502)CaDiCaL version: 2.1.3
% 5.42/1.07 % (417502)Termination reason: Instruction limit
% 5.42/1.07 % (417502)Termination phase: Saturation
% 5.42/1.07 % (417502)Time elapsed: 0.083 s
% 5.42/1.07 % (417502)Peak memory usage: 13 MB
% 5.42/1.07 % (417502)Instructions burned: 131 (million)
% 5.42/1.07 % (417490)Instruction limit reached!
% 5.42/1.07 % (417490)------------------------------
% 5.42/1.07 % (417490)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.42/1.07 % (417490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.42/1.07 % (417490)CaDiCaL version: 2.1.3
% 5.42/1.07 % (417490)Termination reason: Instruction limit
% 5.42/1.07 % (417490)Termination phase: Saturation
% 8.37/1.94 % (417490)Time elapsed: 0.124 s
% 8.37/1.94 % (417490)Peak memory usage: 13 MB
% 8.37/1.94 % (417490)Instructions burned: 116 (million)
% 8.37/1.94 % (417491)Instruction limit reached!
% 8.37/1.94 % (417491)------------------------------
% 8.37/1.94 % (417491)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.37/1.94 % (417491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.37/1.94 % (417491)CaDiCaL version: 2.1.3
% 8.37/1.94 % (417491)Termination reason: Instruction limit
% 8.37/1.94 % (417491)Termination phase: Saturation
% 8.37/1.94 % (417491)Time elapsed: 0.135 s
% 8.37/1.94 % (417491)Peak memory usage: 13 MB
% 8.37/1.94 % (417491)Instructions burned: 131 (million)
% 8.37/1.94 % (417505)ott-21_1_sil=16000:fs=off:random_seed=1854913069:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 8.37/1.94 % (417504)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=1858759837:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 8.37/1.94 % (417506)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1867462484:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 8.37/1.94 % (417508)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=16574623:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 8.37/1.94 % (417508)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 8.37/1.94 % (417508)Terminated due to inappropriate strategy.
% 8.37/1.94 % (417508)------------------------------
% 8.37/1.94 % (417508)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.37/1.94 % (417508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.37/1.94 % (417508)CaDiCaL version: 2.1.3
% 8.37/1.94 % (417508)Termination reason: Inappropriate
% 8.37/1.94 % (417508)Time elapsed: 0.002 s
% 8.37/1.94 % (417508)Peak memory usage: 10 MB
% 8.37/1.94 % (417508)Instructions burned: 1 (million)
% 8.37/1.94 % (417508)------------------------------
% 8.37/1.94 % (417508)------------------------------
% 8.37/1.94 % (417492)Instruction limit reached!
% 8.37/1.94 % (417492)------------------------------
% 8.37/1.94 % (417492)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.37/1.94 % (417492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.37/1.94 % (417492)CaDiCaL version: 2.1.3
% 8.37/1.94 % (417492)Termination reason: Instruction limit
% 8.37/1.94 % (417492)Termination phase: Saturation
% 8.37/1.94 % (417492)Time elapsed: 0.179 s
% 8.37/1.94 % (417492)Peak memory usage: 13 MB
% 8.37/1.94 % (417492)Instructions burned: 160 (million)
% 8.37/1.94 % (417512)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=663791989:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 8.37/1.94 % (417513)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4164748594:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 8.37/1.94 % (417505)Instruction limit reached!
% 8.37/1.94 % (417505)------------------------------
% 8.37/1.94 % (417505)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.37/1.94 % (417505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.37/1.94 % (417505)CaDiCaL version: 2.1.3
% 8.37/1.94 % (417505)Termination reason: Instruction limit
% 8.37/1.94 % (417505)Termination phase: Saturation
% 8.37/1.94 % (417505)Time elapsed: 0.079 s
% 8.37/1.94 % (417505)Peak memory usage: 12 MB
% 8.37/1.94 % (417505)Instructions burned: 183 (million)
% 8.37/1.94 % (417513)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 8.37/1.94 % (417513)Terminated due to inappropriate strategy.
% 8.37/1.94 % (417513)------------------------------
% 8.37/1.94 % (417513)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.37/1.94 % (417513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.37/1.94 % (417513)CaDiCaL version: 2.1.3
% 8.37/1.94 % (417513)Termination reason: Inappropriate
% 8.37/1.94 % (417513)Time elapsed: 0.003 s
% 8.37/1.94 % (417513)Peak memory usage: 10 MB
% 8.37/1.94 % (417513)Instructions burned: 2 (million)
% 8.37/1.94 % (417513)------------------------------
% 8.37/1.94 % (417513)------------------------------
% 8.37/1.94 % (417516)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=1360321625:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi)
% 7.06/2.51 % (417517)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=731522668:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 7.06/2.51 % (417516)Instruction limit reached!
% 7.06/2.51 % (417516)------------------------------
% 7.06/2.51 % (417516)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.06/2.51 % (417516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.06/2.51 % (417516)CaDiCaL version: 2.1.3
% 7.06/2.51 % (417516)Termination reason: Instruction limit
% 7.06/2.51 % (417516)Termination phase: Saturation
% 7.06/2.51 % (417516)Time elapsed: 0.372 s
% 7.06/2.51 % (417516)Peak memory usage: 19 MB
% 7.06/2.51 % (417516)Instructions burned: 692 (million)
% 7.06/2.51 % (417520)fmb+10_1_sil=64000:random_seed=3067062105:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 7.06/2.51 % (417520)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.06/2.51 % (417520)Terminated due to inappropriate strategy.
% 7.06/2.51 % (417520)------------------------------
% 7.06/2.51 % (417520)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.06/2.51 % (417520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.06/2.51 % (417520)CaDiCaL version: 2.1.3
% 7.06/2.51 % (417520)Termination reason: Inappropriate
% 7.06/2.51 % (417520)Time elapsed: 0.001 s
% 7.06/2.51 % (417520)Peak memory usage: 11 MB
% 7.06/2.51 % (417520)Instructions burned: 2 (million)
% 7.06/2.51 % (417520)------------------------------
% 7.06/2.51 % (417520)------------------------------
% 7.06/2.51 % (417522)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2590333025:i=9515:nm=5_2993 on theBenchmark for (2993ds/9515Mi)
% 7.06/2.51 % (417522)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.06/2.51 % (417522)Terminated due to inappropriate strategy.
% 7.06/2.51 % (417522)------------------------------
% 7.06/2.51 % (417522)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.06/2.51 % (417522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.06/2.51 % (417522)CaDiCaL version: 2.1.3
% 7.06/2.51 % (417522)Termination reason: Inappropriate
% 7.06/2.51 % (417522)Time elapsed: 0.001 s
% 7.06/2.51 % (417522)Peak memory usage: 11 MB
% 7.06/2.51 % (417522)Instructions burned: 2 (million)
% 7.06/2.51 % (417522)------------------------------
% 7.06/2.51 % (417522)------------------------------
% 7.06/2.51 % (417524)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1239669961:fmbsr=1.7:i=920_2993 on theBenchmark for (2993ds/920Mi)
% 7.06/2.51 % (417524)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.06/2.51 % (417524)Terminated due to inappropriate strategy.
% 7.06/2.51 % (417524)------------------------------
% 7.06/2.51 % (417524)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.06/2.51 % (417524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.06/2.51 % (417524)CaDiCaL version: 2.1.3
% 7.06/2.51 % (417524)Termination reason: Inappropriate
% 7.06/2.51 % (417524)Time elapsed: 0.001 s
% 7.06/2.51 % (417524)Peak memory usage: 10 MB
% 7.06/2.51 % (417524)Instructions burned: 2 (million)
% 7.06/2.51 % (417524)------------------------------
% 7.06/2.51 % (417524)------------------------------
% 7.06/2.51 % (417526)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3801913993:i=5131_2992 on theBenchmark for (2992ds/5131Mi)
% 7.06/2.51 % (417506)Instruction limit reached!
% 7.06/2.51 % (417506)------------------------------
% 7.06/2.51 % (417506)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.06/2.51 % (417506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.06/2.51 % (417506)CaDiCaL version: 2.1.3
% 7.06/2.51 % (417506)Termination reason: Instruction limit
% 7.06/2.51 % (417506)Termination phase: Saturation
% 7.06/2.51 % (417506)Time elapsed: 0.551 s
% 7.06/2.51 % (417506)Peak memory usage: 14 MB
% 7.06/2.51 % (417506)Instructions burned: 477 (million)
% 7.06/2.51 % (417528)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3363425673:i=1472:ins=7:fdi=8:gsp=on_2992 on theBenchmark for (2992ds/1472Mi)
% 7.06/2.51 % (417504)Instruction limit reached!
% 7.06/2.51 % (417504)------------------------------
% 7.06/2.51 % (417504)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.06/2.51 % (417504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.06/2.51 % (417504)CaDiCaL version: 2.1.3
% 7.06/2.51 % (417504)Termination reason: Instruction limit
% 7.06/2.51 % (417504)Termination phase: Saturation
% 7.06/2.51 % (417504)Time elapsed: 0.594 s
% 7.06/2.51 % (417504)Peak memory usage: 16 MB
% 7.06/2.51 % (417504)Instructions burned: 685 (million)
% 7.06/2.51 % (417530)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2588619063:i=6324_2992 on theBenchmark for (2992ds/6324Mi)
% 7.06/2.51 % (417530)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.06/2.51 % (417530)Terminated due to inappropriate strategy.
% 7.06/2.51 % (417530)------------------------------
% 7.06/2.51 % (417530)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.06/2.51 % (417530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.06/2.51 % (417530)CaDiCaL version: 2.1.3
% 7.06/2.51 % (417530)Termination reason: Inappropriate
% 7.06/2.51 % (417530)Time elapsed: 0.002 s
% 7.06/2.51 % (417530)Peak memory usage: 11 MB
% 7.06/2.51 % (417530)Instructions burned: 2 (million)
% 7.06/2.51 % (417530)------------------------------
% 7.06/2.51 % (417530)------------------------------
% 7.06/2.51 % (417532)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2449205747:fmbsr=2.30978:i=2174_2991 on theBenchmark for (2991ds/2174Mi)
% 7.06/2.51 % (417532)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.06/2.51 % (417532)Terminated due to inappropriate strategy.
% 7.06/2.51 % (417532)------------------------------
% 7.06/2.51 % (417532)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.06/2.51 % (417532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.06/2.51 % (417532)CaDiCaL version: 2.1.3
% 7.06/2.51 % (417532)Termination reason: Inappropriate
% 7.06/2.51 % (417532)Time elapsed: 0.002 s
% 7.06/2.51 % (417532)Peak memory usage: 10 MB
% 7.06/2.51 % (417532)Instructions burned: 2 (million)
% 7.06/2.51 % (417532)------------------------------
% 7.06/2.51 % (417532)------------------------------
% 7.06/2.51 % (417534)ott-2_1_sil=16000:newcnf=on:random_seed=14355493:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2991 on theBenchmark for (2991ds/869Mi)
% 7.06/2.51 % (417517)Instruction limit reached!
% 7.06/2.51 % (417517)------------------------------
% 7.06/2.51 % (417517)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.06/2.51 % (417517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.06/2.51 % (417517)CaDiCaL version: 2.1.3
% 7.06/2.51 % (417517)Termination reason: Instruction limit
% 7.06/2.51 % (417517)Termination phase: Saturation
% 7.06/2.51 % (417517)Time elapsed: 0.850 s
% 7.06/2.51 % (417517)Peak memory usage: 18 MB
% 7.06/2.51 % (417517)Instructions burned: 879 (million)
% 7.06/2.51 % (417536)ott+10_1_sil=32000:tgt=ground:random_seed=1557868328:i=5114:av=off_2988 on theBenchmark for (2988ds/5114Mi)
% 7.06/2.51 % (417512)Instruction limit reached!
% 7.06/2.51 % (417512)------------------------------
% 7.06/2.51 % (417512)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.06/2.51 % (417512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.06/2.51 % (417512)CaDiCaL version: 2.1.3
% 7.06/2.51 % (417512)Termination reason: Instruction limit
% 7.06/2.51 % (417512)Termination phase: Saturation
% 7.06/2.51 % (417512)Time elapsed: 1.130 s
% 7.06/2.51 % (417512)Peak memory usage: 20 MB
% 7.06/2.51 % (417512)Instructions burned: 1180 (million)
% 7.06/2.51 % (417538)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2791665792:i=54282_2986 on theBenchmark for (2986ds/54282Mi)
% 7.06/2.51 % (417538)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.06/2.51 % (417538)Terminated due to inappropriate strategy.
% 7.06/2.51 % (417538)------------------------------
% 7.06/2.51 % (417538)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.06/2.51 % (417538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.06/2.51 % (417538)CaDiCaL version: 2.1.3
% 7.06/2.51 % (417538)Termination reason: Inappropriate
% 7.06/2.51 % (417538)Time elapsed: 0.002 s
% 7.06/2.51 % (417538)Peak memory usage: 11 MB
% 7.06/2.51 % (417538)Instructions burned: 2 (million)
% 7.06/2.51 % (417538)------------------------------
% 7.06/2.51 % (417538)------------------------------
% 7.06/2.51 % (417540)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3431939447:i=3512:aac=none_2986 on theBenchmark for (2986ds/3512Mi)
% 7.06/2.51 % (417534)Instruction limit reached!
% 7.06/2.51 % (417534)------------------------------
% 7.06/2.51 % (417534)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.06/2.51 % (417534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.06/2.51 % (417534)CaDiCaL version: 2.1.3
% 7.06/2.51 % (417534)Termination reason: Instruction limit
% 7.06/2.51 % (417534)Termination phase: Saturation
% 7.06/2.51 % (417534)Time elapsed: 0.795 s
% 7.06/2.51 % (417534)Peak memory usage: 18 MB
% 7.06/2.51 % (417534)Instructions burned: 870 (million)
% 7.06/2.51 % (417543)dis+21_1_sil=32000:sas=cadical:random_seed=1297245294:i=3773:amm=off_2983 on theBenchmark for (2983ds/3773Mi)
% 7.06/2.51 % (417536) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-417481-417536"...
% 7.06/2.51 % (417536)...printing done.
% 7.06/2.51 % (417536)Refutation found. Thanks to Tanya!
% 7.06/2.51 % SZS status Theorem for theBenchmark
% 7.06/2.51 % SZS output start Proof for theBenchmark
% 7.06/2.51 tff(type_def_5, type, general: $tType).
% 7.06/2.51 tff(type_def_6, type, symbol: $tType).
% 7.06/2.51 tff(func_def_0, type, f__integer__: $int > general).
% 7.06/2.51 tff(func_def_1, type, f__symbolic__: symbol > general).
% 7.06/2.51 tff(func_def_2, type, c__infimum__: general).
% 7.06/2.51 tff(func_def_3, type, c__supremum__: general).
% 7.06/2.51 tff(func_def_10, type, sK0: general > $int).
% 7.06/2.51 tff(func_def_11, type, sK1: general > symbol).
% 7.06/2.51 tff(func_def_12, type, sK2: (general * general * general * general) > general).
% 7.06/2.51 tff(func_def_13, type, sK3: (general * general * general * general) > general).
% 7.06/2.51 tff(func_def_14, type, sK4: (general * general * general * general) > general).
% 7.06/2.51 tff(func_def_15, type, sK5: (general * general * general * general) > general).
% 7.06/2.51 tff(func_def_16, type, sK6: (general * general * general * general) > general).
% 7.06/2.51 tff(func_def_17, type, sK7: (general * general * general * general) > general).
% 7.06/2.51 tff(func_def_18, type, sK8: (general * general * general * general) > $int).
% 7.06/2.51 tff(func_def_19, type, sK9: (general * general * general * general) > $int).
% 7.06/2.51 tff(func_def_20, type, sK10: (general * general * general * general) > $int).
% 7.06/2.51 tff(func_def_21, type, sK11: (general * general * general * general) > $int).
% 7.06/2.51 tff(func_def_22, type, sK12: (general * general * general * general) > general).
% 7.06/2.51 tff(func_def_23, type, sK13: (general * general * general * general) > general).
% 7.06/2.51 tff(func_def_24, type, sK14: (general * general * general * general) > general).
% 7.06/2.51 tff(func_def_25, type, sK15: (general * general * general * general) > general).
% 7.06/2.51 tff(func_def_26, type, sK16: $int).
% 7.06/2.51 tff(func_def_27, type, sK17: $int).
% 7.06/2.51 tff(func_def_28, type, sK18: $int).
% 7.06/2.51 tff(func_def_29, type, sK19: $int).
% 7.06/2.51 tff(func_def_30, type, sF20: $int).
% 7.06/2.51 tff(func_def_31, type, sF21: general).
% 7.06/2.51 tff(func_def_32, type, sF22: general).
% 7.06/2.51 tff(func_def_33, type, sF23: general).
% 7.06/2.51 tff(func_def_34, type, sF24: $int).
% 7.06/2.51 tff(func_def_35, type, sF25: general).
% 7.06/2.51 tff(func_def_36, type, sF26: general).
% 7.06/2.51 tff(func_def_37, type, sF27: general).
% 7.06/2.51 tff(func_def_38, type, sF28: $int).
% 7.06/2.51 tff(func_def_39, type, sF29: $int).
% 7.06/2.51 tff(pred_def_1, type, p__is_integer__: general > $o).
% 7.06/2.51 tff(pred_def_2, type, p__is_symbolic__: general > $o).
% 7.06/2.51 tff(pred_def_3, type, p__less_equal__: (general * general) > $o).
% 7.06/2.51 tff(pred_def_4, type, p__less__: (general * general) > $o).
% 7.06/2.51 tff(pred_def_5, type, p__greater_equal__: (general * general) > $o).
% 7.06/2.51 tff(pred_def_6, type, p__greater__: (general * general) > $o).
% 7.06/2.51 tff(pred_def_8, type, div: (general * general * general * general) > $o).
% 7.06/2.51 tff(f4,axiom,(
% 7.06/2.51 ! [X0 : $int,X1 : $int] : (f__integer__(X0) = f__integer__(X1) <=> X0 = X1)),
% 7.06/2.51 file('/export/starexec/sandbox/benchmark/Axioms/SWV014_0.ax',f__integer__def_ax)).
% 7.06/2.51 tff(f6,axiom,(
% 7.06/2.51 ! [X0 : $int,X1 : $int] : (p__less_equal__(f__integer__(X0),f__integer__(X1)) <=> $lesseq(X0,X1))),
% 7.06/2.51 file('/export/starexec/sandbox/benchmark/Axioms/SWV014_0.ax',numeral_ordering_ax)).
% 7.06/2.51 tff(f7,axiom,(
% 7.06/2.51 ! [X0 : general,X1 : general] : ((p__less_equal__(X0,X1) & p__less_equal__(X1,X0)) => X0 = X1)),
% 7.06/2.51 file('/export/starexec/sandbox/benchmark/Axioms/SWV014_0.ax',antisymmetric_ordering_ax)).
% 7.06/2.51 tff(f8,axiom,(
% 7.06/2.51 ! [X0 : general,X1 : general,X2 : general] : ((p__less_equal__(X0,X1) & p__less_equal__(X1,X2)) => p__less_equal__(X0,X2))),
% 7.06/2.51 file('/export/starexec/sandbox/benchmark/Axioms/SWV014_0.ax',transitive_ordering_ax)).
% 7.06/2.51 tff(f9,axiom,(
% 7.06/2.51 ! [X0 : general,X1 : general] : (p__less_equal__(X0,X1) | p__less_equal__(X1,X0))),
% 7.06/2.51 file('/export/starexec/sandbox/benchmark/Axioms/SWV014_0.ax',strongly_connected_ordering_ax)).
% 7.06/2.51 tff(f10,axiom,(
% 7.06/2.51 ! [X0 : general,X1 : general] : (p__less__(X0,X1) <=> (p__less_equal__(X0,X1) & X0 != X1))),
% 7.06/2.51 file('/export/starexec/sandbox/benchmark/Axioms/SWV014_0.ax',p__less__def_ax)).
% 7.06/2.51 tff(f16,axiom,(
% 7.06/2.51 ! [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))))),
% 7.06/2.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_0_completed_definition_of_div_4)).
% 7.06/2.51 tff(f17,conjecture,(
% 7.06/2.51 ! [X0 : $int,X1 : $int,X2 : $int,X3 : $int] : ((div(f__integer__(X0),f__integer__(X1),f__integer__(X2),f__integer__(X3)) & $less(X3,$difference(X1,1))) => div(f__integer__($sum(X0,1)),f__integer__(X1),f__integer__(X2),f__integer__($sum(X3,1))))),
% 7.06/2.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_1_unnamed_formula)).
% 7.06/2.51 tff(f18,negated_conjecture,(
% 7.06/2.51 ~ ! [X0 : $int,X1 : $int,X2 : $int,X3 : $int] : ((div(f__integer__(X0),f__integer__(X1),f__integer__(X2),f__integer__(X3)) & $less(X3,$difference(X1,1))) => div(f__integer__($sum(X0,1)),f__integer__(X1),f__integer__(X2),f__integer__($sum(X3,1))))),
% 7.06/2.51 inference(negated_conjecture,[status(cth)],[f17])).
% 7.06/2.51 tff(f19,plain,(
% 7.06/2.51 ! [X0 : $int,X1 : $int] : (p__less_equal__(f__integer__(X0),f__integer__(X1)) <=> ~$less(X1,X0))),
% 7.06/2.51 inference(theory_normalization,[],[f6])).
% 7.06/2.51 tff(f20,plain,(
% 7.06/2.51 ~ ! [X0 : $int,X1 : $int,X2 : $int,X3 : $int] : ((div(f__integer__(X0),f__integer__(X1),f__integer__(X2),f__integer__(X3)) & $less(X3,$sum(X1,$uminus(1)))) => div(f__integer__($sum(X0,1)),f__integer__(X1),f__integer__(X2),f__integer__($sum(X3,1))))),
% 7.06/2.51 inference(theory_normalization,[],[f18])).
% 7.06/2.51 tff(f21,definition,(
% 7.06/2.51 ( ! [X0 : $int,X1 : $int] : ($sum(X0,X1) = $sum(X1,X0)) )),
% 7.06/2.51 introduced(theory,[tha_commutativity])).
% 7.06/2.51 tff(f22,definition,(
% 7.06/2.51 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum(X0,$sum(X1,X2)) = $sum($sum(X0,X1),X2)) )),
% 7.06/2.51 introduced(theory,[tha_associativity])).
% 7.06/2.51 tff(f25,definition,(
% 7.06/2.51 ( ! [X0 : $int] : (0 = $sum(X0,$uminus(X0))) )),
% 7.06/2.51 introduced(theory,[tha_inverse_op_unit])).
% 7.06/2.51 tff(f26,definition,(
% 7.06/2.51 ( ! [X0 : $int] : (~$less(X0,X0)) )),
% 7.06/2.51 introduced(theory,[tha_non-reflexivity])).
% 7.06/2.51 tff(f27,definition,(
% 7.06/2.51 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X1,X2) | ~$less(X0,X1) | $less(X0,X2)) )),
% 7.06/2.51 introduced(theory,[tha_transitivity])).
% 7.06/2.51 tff(f28,definition,(
% 7.06/2.51 ( ! [X0 : $int,X1 : $int] : ($less(X1,X0) | $less(X0,X1) | X0 = X1) )),
% 7.06/2.51 introduced(theory,[tha_order_totality])).
% 7.06/2.51 tff(f29,definition,(
% 7.06/2.51 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($less($sum(X0,X2),$sum(X1,X2)) | ~$less(X0,X1)) )),
% 7.06/2.51 introduced(theory,[tha_order_monotonicity])).
% 7.06/2.51 tff(f30,definition,(
% 7.06/2.51 ( ! [X0 : $int,X1 : $int] : ($less(X1,$sum(X0,1)) | $less(X0,X1)) )),
% 7.06/2.51 introduced(theory,[tha_order_plus_one_dichotomy])).
% 7.06/2.51 tff(f38,definition,(
% 7.06/2.51 ( ! [X0 : $int,X1 : $int] : (~$less(X1,$sum(X0,1)) | ~$less(X0,X1)) )),
% 7.06/2.51 introduced(theory,[tha_extra_integer_ordering])).
% 7.06/2.51 tff(f39,plain,(
% 7.06/2.51 ! [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))))),
% 7.06/2.51 inference(rectify,[],[f16])).
% 7.06/2.51 tff(f44,plain,(
% 7.06/2.51 ! [X0 : general,X1 : general] : (X0 = X1 | (~p__less_equal__(X0,X1) | ~p__less_equal__(X1,X0)))),
% 7.06/2.51 inference(ennf_transformation,[],[f7])).
% 7.06/2.51 tff(f45,plain,(
% 7.06/2.51 ! [X0 : general,X1 : general] : (X0 = X1 | ~p__less_equal__(X0,X1) | ~p__less_equal__(X1,X0))),
% 7.06/2.51 inference(flattening,[],[f44])).
% 7.06/2.51 tff(f46,plain,(
% 7.06/2.51 ! [X0 : general,X1 : general,X2 : general] : (p__less_equal__(X0,X2) | (~p__less_equal__(X0,X1) | ~p__less_equal__(X1,X2)))),
% 7.06/2.51 inference(ennf_transformation,[],[f8])).
% 7.06/2.51 tff(f47,plain,(
% 7.06/2.51 ! [X0 : general,X1 : general,X2 : general] : (p__less_equal__(X0,X2) | ~p__less_equal__(X0,X1) | ~p__less_equal__(X1,X2))),
% 7.06/2.51 inference(flattening,[],[f46])).
% 7.06/2.51 tff(f48,plain,(
% 7.06/2.51 ? [X0 : $int,X1 : $int,X2 : $int,X3 : $int] : (~div(f__integer__($sum(X0,1)),f__integer__(X1),f__integer__(X2),f__integer__($sum(X3,1))) & (div(f__integer__(X0),f__integer__(X1),f__integer__(X2),f__integer__(X3)) & $less(X3,$sum(X1,$uminus(1)))))),
% 7.06/2.51 inference(ennf_transformation,[],[f20])).
% 7.06/2.51 tff(f49,plain,(
% 7.06/2.51 ? [X0 : $int,X1 : $int,X2 : $int,X3 : $int] : (~div(f__integer__($sum(X0,1)),f__integer__(X1),f__integer__(X2),f__integer__($sum(X3,1))) & div(f__integer__(X0),f__integer__(X1),f__integer__(X2),f__integer__(X3)) & $less(X3,$sum(X1,$uminus(1))))),
% 7.06/2.51 inference(flattening,[],[f48])).
% 7.06/2.51 tff(f52,plain,(
% 7.06/2.51 ! [X0 : $int,X1 : $int] : ((f__integer__(X0) = f__integer__(X1) | X0 != X1) & (X0 = X1 | f__integer__(X1) != f__integer__(X0)))),
% 7.06/2.51 inference(nnf_transformation,[],[f4])).
% 7.06/2.51 tff(f54,plain,(
% 7.06/2.51 ! [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))))),
% 7.06/2.51 inference(nnf_transformation,[],[f19])).
% 7.06/2.51 tff(f55,plain,(
% 7.06/2.51 ! [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)))),
% 7.06/2.51 inference(nnf_transformation,[],[f10])).
% 7.06/2.51 tff(f56,plain,(
% 7.06/2.51 ! [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)))),
% 7.06/2.51 inference(flattening,[],[f55])).
% 7.06/2.51 tff(f57,plain,(
% 7.06/2.51 ! [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)))),
% 7.06/2.51 inference(nnf_transformation,[],[f39])).
% 7.06/2.51 tff(f58,plain,(
% 7.06/2.51 ! [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)))),
% 7.06/2.51 inference(rectify,[],[f57])).
% 7.06/2.51 tff(f59,plain,(
% 7.06/2.51 ! [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)))),
% 7.06/2.51 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))],[f58])).
% 7.06/2.51 tff(f60,plain,(
% 7.06/2.51 ~div(f__integer__($sum(sK16,1)),f__integer__(sK17),f__integer__(sK18),f__integer__($sum(sK19,1))) & div(f__integer__(sK16),f__integer__(sK17),f__integer__(sK18),f__integer__(sK19)) & $less(sK19,$sum(sK17,$uminus(1)))),
% 7.06/2.51 inference(skolemize,[status(esa),new_symbols(skolem,[sK16,sK17,sK18,sK19]),skolemize(X0,sK16),skolemize(X1,sK17),skolemize(X2,sK18),skolemize(X3,sK19)],[f49])).
% 7.06/2.51 tff(f64,plain,(
% 7.06/2.51 ( ! [X0 : $int,X1 : $int] : (f__integer__(X1) != f__integer__(X0) | X0 = X1) )),
% 7.06/2.51 inference(cnf_transformation,[],[f52])).
% 7.06/2.51 tff(f68,plain,(
% 7.06/2.51 ( ! [X0 : $int,X1 : $int] : (~p__less_equal__(f__integer__(X0),f__integer__(X1)) | ~$less(X1,X0)) )),
% 7.06/2.51 inference(cnf_transformation,[],[f54])).
% 7.06/2.51 tff(f69,plain,(
% 7.06/2.51 ( ! [X0 : $int,X1 : $int] : (p__less_equal__(f__integer__(X0),f__integer__(X1)) | $less(X1,X0)) )),
% 7.06/2.51 inference(cnf_transformation,[],[f54])).
% 7.06/2.51 tff(f70,plain,(
% 7.06/2.51 ( ! [X0 : general,X1 : general] : (~p__less_equal__(X1,X0) | ~p__less_equal__(X0,X1) | X0 = X1) )),
% 7.06/2.51 inference(cnf_transformation,[],[f45])).
% 7.06/2.51 tff(f71,plain,(
% 7.06/2.51 ( ! [X2 : general,X0 : general,X1 : general] : (~p__less_equal__(X1,X2) | ~p__less_equal__(X0,X1) | p__less_equal__(X0,X2)) )),
% 7.06/2.51 inference(cnf_transformation,[],[f47])).
% 7.06/2.51 tff(f72,plain,(
% 7.06/2.51 ( ! [X0 : general,X1 : general] : (p__less_equal__(X0,X1) | p__less_equal__(X1,X0)) )),
% 7.06/2.51 inference(cnf_transformation,[],[f9])).
% 7.06/2.51 tff(f75,plain,(
% 7.06/2.51 ( ! [X0 : general,X1 : general] : (~p__less_equal__(X0,X1) | p__less__(X0,X1) | X0 = X1) )),
% 7.06/2.51 inference(cnf_transformation,[],[f56])).
% 7.06/2.51 tff(f82,plain,(
% 7.06/2.51 ( ! [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)) )),
% 7.06/2.51 inference(cnf_transformation,[],[f59])).
% 7.06/2.51 tff(f83,plain,(
% 7.06/2.51 ( ! [X2 : general,X3 : general,X0 : general,X1 : general] : (~div(X0,X1,X2,X3) | sK5(X0,X1,X2,X3) = sK13(X0,X1,X2,X3)) )),
% 7.06/2.51 inference(cnf_transformation,[],[f59])).
% 7.06/2.51 tff(f84,plain,(
% 7.06/2.51 ( ! [X2 : general,X3 : general,X0 : general,X1 : general] : (~div(X0,X1,X2,X3) | f__integer__(0) = sK12(X0,X1,X2,X3)) )),
% 7.06/2.51 inference(cnf_transformation,[],[f59])).
% 7.06/2.51 tff(f85,plain,(
% 7.06/2.51 ( ! [X2 : general,X3 : general,X0 : general,X1 : general] : (~div(X0,X1,X2,X3) | sK6(X0,X1,X2,X3) = sK7(X0,X1,X2,X3)) )),
% 7.06/2.51 inference(cnf_transformation,[],[f59])).
% 7.06/2.51 tff(f86,plain,(
% 7.06/2.51 ( ! [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))) )),
% 7.06/2.51 inference(cnf_transformation,[],[f59])).
% 7.06/2.51 tff(f87,plain,(
% 7.06/2.51 ( ! [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))) )),
% 7.06/2.51 inference(cnf_transformation,[],[f59])).
% 7.06/2.51 tff(f88,plain,(
% 7.06/2.51 ( ! [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))) )),
% 7.06/2.51 inference(cnf_transformation,[],[f59])).
% 7.06/2.51 tff(f89,plain,(
% 7.06/2.51 ( ! [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))) )),
% 7.06/2.51 inference(cnf_transformation,[],[f59])).
% 7.06/2.51 tff(f90,plain,(
% 7.06/2.51 ( ! [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)))) )),
% 7.06/2.51 inference(cnf_transformation,[],[f59])).
% 7.06/2.51 tff(f91,plain,(
% 7.06/2.51 ( ! [X2 : general,X3 : general,X0 : general,X1 : general] : (~div(X0,X1,X2,X3) | sK2(X0,X1,X2,X3) = sK6(X0,X1,X2,X3)) )),
% 7.06/2.51 inference(cnf_transformation,[],[f59])).
% 7.06/2.51 tff(f92,plain,(
% 7.06/2.51 ( ! [X2 : general,X3 : general,X0 : general,X1 : general] : (~div(X0,X1,X2,X3) | sK5(X0,X1,X2,X3) = X3) )),
% 7.06/2.51 inference(cnf_transformation,[],[f59])).
% 7.06/2.51 tff(f93,plain,(
% 7.06/2.51 ( ! [X2 : general,X3 : general,X0 : general,X1 : general] : (~div(X0,X1,X2,X3) | sK4(X0,X1,X2,X3) = X2) )),
% 7.06/2.51 inference(cnf_transformation,[],[f59])).
% 7.06/2.51 tff(f94,plain,(
% 7.06/2.51 ( ! [X2 : general,X3 : general,X0 : general,X1 : general] : (~div(X0,X1,X2,X3) | sK3(X0,X1,X2,X3) = X1) )),
% 7.06/2.51 inference(cnf_transformation,[],[f59])).
% 7.06/2.51 tff(f95,plain,(
% 7.06/2.51 ( ! [X2 : general,X3 : general,X0 : general,X1 : general] : (~div(X0,X1,X2,X3) | sK2(X0,X1,X2,X3) = X0) )),
% 7.06/2.51 inference(cnf_transformation,[],[f59])).
% 7.06/2.51 tff(f96,plain,(
% 7.06/2.51 ( ! [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)) )),
% 7.06/2.51 inference(cnf_transformation,[],[f59])).
% 7.06/2.51 tff(f97,plain,(
% 7.06/2.51 $less(sK19,$sum(sK17,$uminus(1)))),
% 7.06/2.51 inference(cnf_transformation,[],[f60])).
% 7.06/2.51 tff(f98,plain,(
% 7.06/2.51 div(f__integer__(sK16),f__integer__(sK17),f__integer__(sK18),f__integer__(sK19))),
% 7.06/2.51 inference(cnf_transformation,[],[f60])).
% 7.06/2.51 tff(f99,plain,(
% 7.06/2.51 ~div(f__integer__($sum(sK16,1)),f__integer__(sK17),f__integer__(sK18),f__integer__($sum(sK19,1)))),
% 7.06/2.51 inference(cnf_transformation,[],[f60])).
% 7.06/2.51 tff(f104,plain,(
% 7.06/2.51 ( ! [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)) )),
% 7.06/2.51 inference(equality_resolution,[],[f96])).
% 7.06/2.51 tff(f105,plain,(
% 7.06/2.51 ( ! [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)) )),
% 7.06/2.51 inference(equality_resolution,[],[f104])).
% 7.06/2.51 tff(f106,plain,(
% 7.06/2.51 ( ! [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)) )),
% 7.06/2.51 inference(equality_resolution,[],[f105])).
% 7.06/2.51 tff(f107,plain,(
% 7.06/2.51 ( ! [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)) )),
% 7.06/2.51 inference(equality_resolution,[],[f106])).
% 7.06/2.51 tff(f108,plain,(
% 7.06/2.51 ( ! [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)) )),
% 7.06/2.51 inference(equality_resolution,[],[f107])).
% 7.06/2.51 tff(f109,plain,(
% 7.06/2.51 ( ! [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)) )),
% 7.06/2.51 inference(equality_resolution,[],[f108])).
% 7.06/2.51 tff(f110,plain,(
% 7.06/2.51 ( ! [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)) )),
% 7.06/2.51 inference(equality_resolution,[],[f109])).
% 7.06/2.51 tff(f111,plain,(
% 7.06/2.51 ( ! [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)) )),
% 7.06/2.51 inference(equality_resolution,[],[f110])).
% 7.06/2.51 tff(f112,plain,(
% 7.06/2.51 ( ! [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)) )),
% 7.06/2.51 inference(equality_resolution,[],[f111])).
% 7.06/2.51 tff(f113,plain,(
% 7.06/2.51 ( ! [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)) )),
% 7.06/2.51 inference(equality_resolution,[],[f112])).
% 7.06/2.51 tff(f114,plain,(
% 7.06/2.51 ( ! [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)) )),
% 7.06/2.51 inference(equality_resolution,[],[f113])).
% 7.06/2.51 tff(f115,plain,(
% 7.06/2.51 ( ! [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)) )),
% 7.06/2.51 inference(equality_resolution,[],[f114])).
% 7.06/2.51 tff(f116,plain,(
% 7.06/2.51 ( ! [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)) )),
% 7.06/2.51 inference(equality_resolution,[],[f115])).
% 7.06/2.51 tff(f117,plain,(
% 7.06/2.51 ( ! [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)) )),
% 7.06/2.51 inference(equality_resolution,[],[f116])).
% 7.06/2.51 tff(f118,plain,(
% 7.06/2.51 ( ! [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))) )),
% 7.06/2.51 inference(equality_resolution,[],[f117])).
% 7.06/2.51 tff(f119,definition,(
% 7.06/2.51 sF20 = $sum(sK16,1)),
% 7.06/2.51 introduced(definition,[new_symbols(definition,[sF20])],[function_definition])).
% 7.06/2.51 tff(f120,plain,(
% 7.06/2.51 $sum(sK16,1) = sF20),
% 7.06/2.51 inference(reorient_equations,[],[f119])).
% 7.06/2.51 tff(f121,definition,(
% 7.06/2.51 sF21 = f__integer__(sF20)),
% 7.06/2.51 introduced(definition,[new_symbols(definition,[sF21])],[function_definition])).
% 7.06/2.51 tff(f122,plain,(
% 7.06/2.51 f__integer__(sF20) = sF21),
% 7.06/2.51 inference(reorient_equations,[],[f121])).
% 7.06/2.51 tff(f123,definition,(
% 7.06/2.51 sF22 = f__integer__(sK17)),
% 7.06/2.51 introduced(definition,[new_symbols(definition,[sF22])],[function_definition])).
% 7.06/2.51 tff(f124,plain,(
% 7.06/2.51 f__integer__(sK17) = sF22),
% 7.06/2.51 inference(reorient_equations,[],[f123])).
% 7.06/2.51 tff(f125,definition,(
% 7.06/2.51 sF23 = f__integer__(sK18)),
% 7.06/2.51 introduced(definition,[new_symbols(definition,[sF23])],[function_definition])).
% 7.06/2.51 tff(f126,plain,(
% 7.06/2.51 f__integer__(sK18) = sF23),
% 7.06/2.51 inference(reorient_equations,[],[f125])).
% 7.06/2.51 tff(f127,definition,(
% 7.06/2.51 sF24 = $sum(sK19,1)),
% 7.06/2.51 introduced(definition,[new_symbols(definition,[sF24])],[function_definition])).
% 7.06/2.51 tff(f128,plain,(
% 7.06/2.51 $sum(sK19,1) = sF24),
% 7.06/2.51 inference(reorient_equations,[],[f127])).
% 7.06/2.51 tff(f129,definition,(
% 7.06/2.51 sF25 = f__integer__(sF24)),
% 7.06/2.51 introduced(definition,[new_symbols(definition,[sF25])],[function_definition])).
% 7.06/2.51 tff(f130,plain,(
% 7.06/2.51 f__integer__(sF24) = sF25),
% 7.06/2.51 inference(reorient_equations,[],[f129])).
% 7.06/2.51 tff(f131,plain,(
% 7.06/2.51 ~div(sF21,sF22,sF23,sF25)),
% 7.06/2.51 inference(definition_folding,[],[f99,f130,f128,f126,f124,f122,f120])).
% 7.06/2.51 tff(f132,definition,(
% 7.06/2.51 sF26 = f__integer__(sK16)),
% 7.06/2.51 introduced(definition,[new_symbols(definition,[sF26])],[function_definition])).
% 7.06/2.51 tff(f133,plain,(
% 7.06/2.51 f__integer__(sK16) = sF26),
% 7.06/2.51 inference(reorient_equations,[],[f132])).
% 7.06/2.51 tff(f134,definition,(
% 7.06/2.51 sF27 = f__integer__(sK19)),
% 7.06/2.51 introduced(definition,[new_symbols(definition,[sF27])],[function_definition])).
% 7.06/2.51 tff(f135,plain,(
% 7.06/2.51 f__integer__(sK19) = sF27),
% 7.06/2.51 inference(reorient_equations,[],[f134])).
% 7.06/2.51 tff(f136,plain,(
% 7.06/2.51 div(sF26,sF22,sF23,sF27)),
% 7.06/2.51 inference(definition_folding,[],[f98,f135,f126,f124,f133])).
% 7.06/2.51 tff(f137,definition,(
% 7.06/2.51 sF28 = $uminus(1)),
% 7.06/2.51 introduced(definition,[new_symbols(definition,[sF28])],[function_definition])).
% 7.06/2.51 tff(f138,plain,(
% 7.06/2.51 $uminus(1) = sF28),
% 7.06/2.51 inference(reorient_equations,[],[f137])).
% 7.06/2.51 tff(f139,definition,(
% 7.06/2.51 sF29 = $sum(sK17,sF28)),
% 7.06/2.51 introduced(definition,[new_symbols(definition,[sF29])],[function_definition])).
% 7.06/2.51 tff(f140,plain,(
% 7.06/2.51 $sum(sK17,sF28) = sF29),
% 7.06/2.51 inference(reorient_equations,[],[f139])).
% 7.06/2.51 tff(f141,plain,(
% 7.06/2.51 $less(sK19,sF29)),
% 7.06/2.51 inference(definition_folding,[],[f97,f140,f138])).
% 7.06/2.51 tff(f142,plain,(
% 7.06/2.51 sF28 = -1),
% 7.06/2.51 inference(evaluation,[],[f138])).
% 7.06/2.51 tff(f143,plain,(
% 7.06/2.51 sF20 = $sum(1,sK16)),
% 7.06/2.51 inference(forward_demodulation,[],[f120,f21])).
% 7.06/2.51 tff(f144,plain,(
% 7.06/2.51 sF24 = $sum(1,sK19)),
% 7.06/2.51 inference(forward_demodulation,[],[f128,f21])).
% 7.06/2.51 tff(f145,plain,(
% 7.06/2.51 sF29 = $sum(sK17,-1)),
% 7.06/2.51 inference(forward_demodulation,[],[f140,f142])).
% 7.06/2.51 tff(f146,plain,(
% 7.06/2.51 sF29 = $sum(-1,sK17)),
% 7.06/2.51 inference(forward_demodulation,[],[f145,f21])).
% 7.06/2.51 tff(f187,plain,(
% 7.06/2.51 ( ! [X0 : $int] : ($less(X0,$sum(X0,1))) )),
% 7.06/2.51 inference(resolution,[],[f30,f26])).
% 7.06/2.51 tff(f192,plain,(
% 7.06/2.51 ( ! [X0 : $int,X1 : $int] : (~$less(X1,$sum(1,X0)) | ~$less(X0,X1)) )),
% 7.06/2.51 inference(superposition,[],[f38,f21])).
% 7.06/2.51 tff(f200,plain,(
% 7.06/2.51 ( ! [X0 : $int] : (f__integer__(X0) != sF26 | sK16 = X0) )),
% 7.06/2.51 inference(superposition,[],[f64,f133])).
% 7.06/2.51 tff(f201,plain,(
% 7.06/2.51 ( ! [X0 : $int] : (f__integer__(X0) != sF22 | sK17 = X0) )),
% 7.06/2.51 inference(superposition,[],[f64,f124])).
% 7.06/2.51 tff(f202,plain,(
% 7.06/2.51 ( ! [X0 : $int] : (f__integer__(X0) != sF23 | sK18 = X0) )),
% 7.06/2.51 inference(superposition,[],[f64,f126])).
% 7.06/2.51 tff(f203,plain,(
% 7.06/2.51 ( ! [X0 : $int] : (f__integer__(X0) != sF27 | sK19 = X0) )),
% 7.06/2.51 inference(superposition,[],[f64,f135])).
% 7.06/2.51 tff(f221,plain,(
% 7.06/2.51 ( ! [X0 : $int] : (~p__less_equal__(f__integer__(X0),sF27) | ~$less(sK19,X0)) )),
% 7.06/2.51 inference(superposition,[],[f68,f135])).
% 7.06/2.51 tff(f236,plain,(
% 7.06/2.51 ( ! [X0 : $int] : (p__less_equal__(sF25,f__integer__(X0)) | $less(X0,sF24)) )),
% 7.06/2.51 inference(superposition,[],[f69,f130])).
% 7.06/2.51 tff(f242,plain,(
% 7.06/2.51 ( ! [X0 : $int] : (p__less_equal__(f__integer__(X0),sF25) | $less(sF24,X0)) )),
% 7.06/2.51 inference(superposition,[],[f69,f130])).
% 7.06/2.51 tff(f244,plain,(
% 7.06/2.51 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X0,X1) | $less(X0,$sum(X2,1)) | $less(X2,X1)) )),
% 7.06/2.51 inference(resolution,[],[f27,f30])).
% 7.06/2.51 tff(f292,plain,(
% 7.06/2.51 ( ! [X0 : general,X1 : general] : (p__less__(X0,X1) | X0 = X1 | p__less_equal__(X1,X0)) )),
% 7.06/2.51 inference(resolution,[],[f75,f72])).
% 7.06/2.51 tff(f364,plain,(
% 7.06/2.51 ( ! [X0 : $int] : ($less(sF29,$sum(X0,sK17)) | ~$less(-1,X0)) )),
% 7.06/2.51 inference(superposition,[],[f29,f146])).
% 7.06/2.51 tff(f395,plain,(
% 7.06/2.51 ( ! [X0 : $int,X1 : $int] : ($sum(0,X1) = $sum(X0,$sum($uminus(X0),X1))) )),
% 7.06/2.51 inference(superposition,[],[f22,f25])).
% 7.06/2.51 tff(f400,plain,(
% 7.06/2.51 ( ! [X0 : $int] : ($sum(1,$sum(sK19,X0)) = $sum(sF24,X0)) )),
% 7.06/2.51 inference(superposition,[],[f22,f144])).
% 7.06/2.51 tff(f402,plain,(
% 7.06/2.51 ( ! [X0 : $int] : ($sum(-1,$sum(sK17,X0)) = $sum(sF29,X0)) )),
% 7.06/2.51 inference(superposition,[],[f22,f146])).
% 7.06/2.51 tff(f417,plain,(
% 7.06/2.51 ( ! [X0 : $int,X1 : $int] : ($sum(X0,$sum($uminus(X0),X1)) = X1) )),
% 7.06/2.51 inference(evaluation,[],[f395])).
% 7.06/2.51 tff(f449,plain,(
% 7.06/2.51 sF27 = sK5(sF26,sF22,sF23,sF27)),
% 7.06/2.51 inference(resolution,[],[f92,f136])).
% 7.06/2.51 tff(f450,plain,(
% 7.06/2.51 sF23 = sK4(sF26,sF22,sF23,sF27)),
% 7.06/2.51 inference(resolution,[],[f93,f136])).
% 7.06/2.51 tff(f451,plain,(
% 7.06/2.51 sF22 = sK3(sF26,sF22,sF23,sF27)),
% 7.06/2.51 inference(resolution,[],[f94,f136])).
% 7.06/2.51 tff(f452,plain,(
% 7.06/2.51 sF26 = sK2(sF26,sF22,sF23,sF27)),
% 7.06/2.51 inference(resolution,[],[f95,f136])).
% 7.06/2.51 tff(f480,plain,(
% 7.06/2.51 f__integer__(0) = sK12(sF26,sF22,sF23,sF27)),
% 7.06/2.51 inference(resolution,[],[f84,f136])).
% 7.06/2.51 tff(f517,plain,(
% 7.06/2.51 sK5(sF26,sF22,sF23,sF27) = sK13(sF26,sF22,sF23,sF27)),
% 7.06/2.51 inference(resolution,[],[f83,f136])).
% 7.06/2.51 tff(f518,plain,(
% 7.06/2.51 sF27 = sK13(sF26,sF22,sF23,sF27)),
% 7.06/2.51 inference(forward_demodulation,[],[f517,f449])).
% 7.06/2.51 tff(f522,plain,(
% 7.06/2.51 sK6(sF26,sF22,sF23,sF27) = sK7(sF26,sF22,sF23,sF27)),
% 7.06/2.51 inference(resolution,[],[f85,f136])).
% 7.06/2.51 tff(f527,plain,(
% 7.06/2.51 sK2(sF26,sF22,sF23,sF27) = sK6(sF26,sF22,sF23,sF27)),
% 7.06/2.51 inference(resolution,[],[f91,f136])).
% 7.06/2.51 tff(f528,plain,(
% 7.06/2.51 sF26 = sK6(sF26,sF22,sF23,sF27)),
% 7.06/2.51 inference(forward_demodulation,[],[f527,f452])).
% 7.06/2.51 tff(f529,plain,(
% 7.06/2.51 sK5(sF26,sF22,sF23,sF27) = f__integer__(sK9(sF26,sF22,sF23,sF27))),
% 7.06/2.51 inference(resolution,[],[f86,f136])).
% 7.06/2.51 tff(f530,plain,(
% 7.06/2.51 sF27 = f__integer__(sK9(sF26,sF22,sF23,sF27))),
% 7.06/2.51 inference(forward_demodulation,[],[f529,f449])).
% 7.06/2.51 tff(f539,plain,(
% 7.06/2.51 sK4(sF26,sF22,sF23,sF27) = f__integer__(sK11(sF26,sF22,sF23,sF27))),
% 7.06/2.51 inference(resolution,[],[f87,f136])).
% 7.06/2.51 tff(f540,plain,(
% 7.06/2.51 sF23 = f__integer__(sK11(sF26,sF22,sF23,sF27))),
% 7.06/2.51 inference(forward_demodulation,[],[f539,f450])).
% 7.06/2.51 tff(f541,plain,(
% 7.06/2.51 p__less_equal__(sK12(sF26,sF22,sF23,sF27),sF27) | ~div(sF26,sF22,sF23,sF27)),
% 7.06/2.51 inference(superposition,[],[f82,f518])).
% 7.06/2.51 tff(f542,plain,(
% 7.06/2.51 p__less_equal__(sK12(sF26,sF22,sF23,sF27),sF27)),
% 7.06/2.51 inference(forward_subsumption_resolution,[],[f541,f136])).
% 7.06/2.51 tff(f543,plain,(
% 7.06/2.51 p__less_equal__(f__integer__(0),sF27)),
% 7.06/2.51 inference(forward_demodulation,[],[f542,f480])).
% 7.06/2.51 tff(f544,plain,(
% 7.06/2.51 sK3(sF26,sF22,sF23,sF27) = f__integer__(sK10(sF26,sF22,sF23,sF27))),
% 7.06/2.51 inference(resolution,[],[f88,f136])).
% 7.06/2.51 tff(f545,plain,(
% 7.06/2.51 sF22 = f__integer__(sK10(sF26,sF22,sF23,sF27))),
% 7.06/2.51 inference(forward_demodulation,[],[f544,f451])).
% 7.06/2.51 tff(f548,plain,(
% 7.06/2.51 ( ! [X0 : general] : (~p__less_equal__(X0,f__integer__(0)) | p__less_equal__(X0,sF27)) )),
% 7.06/2.51 inference(resolution,[],[f543,f71])).
% 7.06/2.51 tff(f550,plain,(
% 7.06/2.51 sK8(sF26,sF22,sF23,sF27) = $product(sK10(sF26,sF22,sF23,sF27),sK11(sF26,sF22,sF23,sF27))),
% 7.06/2.51 inference(resolution,[],[f89,f136])).
% 7.06/2.51 tff(f554,plain,(
% 7.06/2.51 sK7(sF26,sF22,sF23,sF27) = f__integer__($sum(sK8(sF26,sF22,sF23,sF27),sK9(sF26,sF22,sF23,sF27)))),
% 7.06/2.51 inference(resolution,[],[f90,f136])).
% 7.06/2.51 tff(f555,plain,(
% 7.06/2.51 sK6(sF26,sF22,sF23,sF27) = f__integer__($sum(sK8(sF26,sF22,sF23,sF27),sK9(sF26,sF22,sF23,sF27)))),
% 7.06/2.51 inference(forward_demodulation,[],[f554,f522])).
% 7.06/2.51 tff(f556,plain,(
% 7.06/2.51 sF26 = f__integer__($sum(sK8(sF26,sF22,sF23,sF27),sK9(sF26,sF22,sF23,sF27)))),
% 7.06/2.51 inference(forward_demodulation,[],[f555,f528])).
% 7.06/2.51 tff(f599,plain,(
% 7.06/2.51 ( ! [X0 : $int,X1 : $int] : (div(f__integer__($sum($product(X0,X1),sF24)),f__integer__(X0),f__integer__(X1),sF25) | ~p__less_equal__(f__integer__(0),sF25) | ~p__less__(sF25,f__integer__(X0))) )),
% 7.06/2.51 inference(superposition,[],[f118,f130])).
% 7.06/2.51 tff(f601,plain,(
% 7.06/2.51 ( ! [X0 : $int,X1 : $int] : (div(f__integer__($sum(sF24,$product(X0,X1))),f__integer__(X0),f__integer__(X1),sF25) | ~p__less_equal__(f__integer__(0),sF25) | ~p__less__(sF25,f__integer__(X0))) )),
% 7.06/2.51 inference(forward_demodulation,[],[f599,f21])).
% 7.06/2.51 tff(f627,plain,(
% 7.06/2.51 ( ! [X0 : general] : (p__less_equal__(f__integer__(0),X0) | p__less_equal__(X0,sF27)) )),
% 7.06/2.51 inference(resolution,[],[f548,f72])).
% 7.06/2.51 tff(f643,plain,(
% 7.06/2.51 ( ! [X0 : $int] : (p__less_equal__(f__integer__(X0),sF27) | ~$less(X0,0)) )),
% 7.06/2.51 inference(resolution,[],[f627,f68])).
% 7.06/2.51 tff(f855,plain,(
% 7.06/2.51 sF22 != sF22 | sK17 = sK10(sF26,sF22,sF23,sF27)),
% 7.06/2.51 inference(superposition,[],[f201,f545])).
% 7.06/2.51 tff(f861,plain,(
% 7.06/2.51 sF22 != sF25 | sK17 = sF24),
% 7.06/2.51 inference(superposition,[],[f201,f130])).
% 7.06/2.51 tff(f862,plain,(
% 7.06/2.51 sK17 = sK10(sF26,sF22,sF23,sF27)),
% 7.06/2.51 inference(trivial_inequality_removal,[],[f855])).
% 7.06/2.51 tff(f870,plain,(
% 7.06/2.51 sF23 != sF23 | sK18 = sK11(sF26,sF22,sF23,sF27)),
% 7.06/2.51 inference(superposition,[],[f202,f540])).
% 7.06/2.51 tff(f876,plain,(
% 7.06/2.51 sK18 = sK11(sF26,sF22,sF23,sF27)),
% 7.06/2.51 inference(trivial_inequality_removal,[],[f870])).
% 7.06/2.51 tff(f883,plain,(
% 7.06/2.51 sF27 != sF27 | sK19 = sK9(sF26,sF22,sF23,sF27)),
% 7.06/2.51 inference(superposition,[],[f203,f530])).
% 7.06/2.51 tff(f891,plain,(
% 7.06/2.51 sK19 = sK9(sF26,sF22,sF23,sF27)),
% 7.06/2.51 inference(trivial_inequality_removal,[],[f883])).
% 7.06/2.51 tff(f895,plain,(
% 7.06/2.51 sK8(sF26,sF22,sF23,sF27) = $product(sK17,sK11(sF26,sF22,sF23,sF27))),
% 7.06/2.51 inference(superposition,[],[f550,f862])).
% 7.06/2.51 tff(f897,plain,(
% 7.06/2.51 sK8(sF26,sF22,sF23,sF27) = $product(sK17,sK18)),
% 7.06/2.51 inference(forward_demodulation,[],[f895,f876])).
% 7.06/2.51 tff(f929,plain,(
% 7.06/2.51 sF26 = f__integer__($sum(sK8(sF26,sF22,sF23,sF27),sK19))),
% 7.06/2.51 inference(superposition,[],[f556,f891])).
% 7.06/2.51 tff(f931,plain,(
% 7.06/2.51 sF26 = f__integer__($sum(sK19,sK8(sF26,sF22,sF23,sF27)))),
% 7.06/2.51 inference(forward_demodulation,[],[f929,f21])).
% 7.06/2.51 tff(f932,plain,(
% 7.06/2.51 sF26 = f__integer__($sum(sK19,$product(sK17,sK18)))),
% 7.06/2.51 inference(forward_demodulation,[],[f931,f897])).
% 7.06/2.51 tff(f1130,plain,(
% 7.06/2.51 ( ! [X0 : $int] : (~$less(sK19,X0) | ~$less(X0,0)) )),
% 7.06/2.51 inference(resolution,[],[f221,f643])).
% 7.06/2.51 tff(f1306,plain,(
% 7.06/2.51 ~$less($sum(sK19,1),0)),
% 7.06/2.51 inference(resolution,[],[f1130,f187])).
% 7.06/2.51 tff(f1316,plain,(
% 7.06/2.51 ~$less($sum(1,sK19),0)),
% 7.06/2.51 inference(forward_demodulation,[],[f1306,f21])).
% 7.06/2.51 tff(f1317,plain,(
% 7.06/2.51 ~$less(sF24,0)),
% 7.06/2.51 inference(forward_demodulation,[],[f1316,f144])).
% 7.06/2.51 tff(f1351,plain,(
% 7.06/2.51 p__less_equal__(sF25,sF22) | $less(sK17,sF24)),
% 7.06/2.51 inference(superposition,[],[f236,f124])).
% 7.06/2.51 tff(f1547,plain,(
% 7.06/2.51 ( ! [X0 : $int] : (~$less(sK19,X0) | ~$less(X0,sF24)) )),
% 7.06/2.51 inference(superposition,[],[f192,f144])).
% 7.06/2.51 tff(f1640,plain,(
% 7.06/2.51 ~$less(-1,1) | ~$less(sK17,sF29)),
% 7.06/2.51 inference(resolution,[],[f364,f192])).
% 7.06/2.51 tff(f1647,plain,(
% 7.06/2.51 ~$less(sK17,sF29)),
% 7.06/2.51 inference(evaluation,[],[f1640])).
% 7.06/2.51 tff(f1868,plain,(
% 7.06/2.51 $sum(sF29,$uminus(sK17)) = $sum(-1,0)),
% 7.06/2.51 inference(superposition,[],[f402,f25])).
% 7.06/2.51 tff(f1872,plain,(
% 7.06/2.51 -1 = $sum(sF29,$uminus(sK17))),
% 7.06/2.51 inference(evaluation,[],[f1868])).
% 7.06/2.51 tff(f2259,plain,(
% 7.06/2.51 ( ! [X0 : $int] : ($less(sK19,$sum(X0,1)) | $less(X0,sF29)) )),
% 7.06/2.51 inference(resolution,[],[f244,f141])).
% 7.06/2.51 tff(f2415,plain,(
% 7.06/2.51 ( ! [X0 : $int] : ($less(sK19,$sum(1,X0)) | $less(X0,sF29)) )),
% 7.06/2.51 inference(superposition,[],[f2259,f21])).
% 7.06/2.51 tff(f2831,plain,(
% 7.06/2.51 sF26 != sF26 | sK16 = $sum(sK19,$product(sK17,sK18))),
% 7.06/2.51 inference(superposition,[],[f200,f932])).
% 7.06/2.51 tff(f2874,plain,(
% 7.06/2.51 sK16 = $sum(sK19,$product(sK17,sK18))),
% 7.06/2.51 inference(trivial_inequality_removal,[],[f2831])).
% 7.06/2.51 tff(f2971,plain,(
% 7.06/2.51 $sum(1,sK16) = $sum(sF24,$product(sK17,sK18))),
% 7.06/2.51 inference(superposition,[],[f400,f2874])).
% 7.06/2.51 tff(f2986,plain,(
% 7.06/2.51 sF20 = $sum(sF24,$product(sK17,sK18))),
% 7.06/2.51 inference(forward_demodulation,[],[f2971,f143])).
% 7.06/2.51 tff(f3044,plain,(
% 7.06/2.51 ( ! [X0 : $int] : ($less(sK19,X0) | $less($sum($uminus(1),X0),sF29)) )),
% 7.06/2.51 inference(superposition,[],[f2415,f417])).
% 7.06/2.51 tff(f3051,plain,(
% 7.06/2.51 ( ! [X0 : $int] : ($less($sum(-1,X0),sF29) | $less(sK19,X0)) )),
% 7.06/2.51 inference(evaluation,[],[f3044])).
% 7.06/2.51 tff(f3215,plain,(
% 7.06/2.51 $less(sF29,sF29) | $less(sK19,sK17)),
% 7.06/2.51 inference(superposition,[],[f3051,f146])).
% 7.06/2.51 tff(f3227,plain,(
% 7.06/2.51 $less(sK19,sK17)),
% 7.06/2.51 inference(forward_subsumption_resolution,[],[f3215,f26])).
% 7.06/2.51 tff(f4765,plain,(
% 7.06/2.51 div(f__integer__(sF20),f__integer__(sK17),f__integer__(sK18),sF25) | ~p__less_equal__(f__integer__(0),sF25) | ~p__less__(sF25,f__integer__(sK17))),
% 7.06/2.51 inference(superposition,[],[f601,f2986])).
% 7.06/2.51 tff(f4799,plain,(
% 7.06/2.51 div(f__integer__(sF20),f__integer__(sK17),sF23,sF25) | ~p__less_equal__(f__integer__(0),sF25) | ~p__less__(sF25,f__integer__(sK17))),
% 7.06/2.51 inference(forward_demodulation,[],[f4765,f126])).
% 7.06/2.51 tff(f4802,plain,(
% 7.06/2.51 div(f__integer__(sF20),sF22,sF23,sF25) | ~p__less_equal__(f__integer__(0),sF25) | ~p__less__(sF25,f__integer__(sK17))),
% 7.06/2.51 inference(forward_demodulation,[],[f4799,f124])).
% 7.06/2.51 tff(f4804,plain,(
% 7.06/2.51 div(sF21,sF22,sF23,sF25) | ~p__less_equal__(f__integer__(0),sF25) | ~p__less__(sF25,f__integer__(sK17))),
% 7.06/2.51 inference(forward_demodulation,[],[f4802,f122])).
% 7.06/2.51 tff(f4806,plain,(
% 7.06/2.51 ~p__less_equal__(f__integer__(0),sF25) | ~p__less__(sF25,f__integer__(sK17))),
% 7.06/2.51 inference(forward_subsumption_resolution,[],[f4804,f131])).
% 7.06/2.51 tff(f4808,plain,(
% 7.06/2.51 ~p__less_equal__(f__integer__(0),sF25) | ~p__less__(sF25,sF22)),
% 7.06/2.51 inference(forward_demodulation,[],[f4806,f124])).
% 7.06/2.51 tff(f4812,plain,(
% 7.06/2.51 ~p__less__(sF25,sF22) | $less(sF24,0)),
% 7.06/2.51 inference(resolution,[],[f4808,f242])).
% 7.06/2.51 tff(f4817,plain,(
% 7.06/2.51 ~p__less__(sF25,sF22)),
% 7.06/2.51 inference(forward_subsumption_resolution,[],[f4812,f1317])).
% 7.06/2.51 tff(f4882,plain,(
% 7.06/2.51 p__less_equal__(sF22,sF25) | sF22 = sF25),
% 7.06/2.51 inference(resolution,[],[f4817,f292])).
% 7.06/2.51 tff(f5012,plain,(
% 7.06/2.51 sF22 = sF25 | ~p__less_equal__(sF25,sF22) | sF22 = sF25),
% 7.06/2.51 inference(resolution,[],[f4882,f70])).
% 7.06/2.51 tff(f5013,plain,(
% 7.06/2.51 ~p__less_equal__(sF25,sF22) | sF22 = sF25),
% 7.06/2.51 inference(duplicate_literal_removal,[],[f5012])).
% 7.06/2.51 tff(f21360,plain,(
% 7.06/2.51 $less(sK17,sF24) | sF22 = sF25),
% 7.06/2.51 inference(resolution,[],[f1351,f5013])).
% 7.06/2.51 tff(f21745,plain,(
% 7.06/2.51 ~$less(sK17,sF24)),
% 7.06/2.51 inference(resolution,[],[f1547,f3227])).
% 7.06/2.51 tff(f21749,plain,(
% 7.06/2.51 ~$less(sF29,sF24)),
% 7.06/2.51 inference(resolution,[],[f1547,f141])).
% 7.06/2.51 tff(f21827,plain,(
% 7.06/2.51 sF22 = sF25),
% 7.06/2.51 inference(resolution,[],[f21745,f21360])).
% 7.06/2.51 tff(f22361,plain,(
% 7.06/2.51 sF22 != sF22 | sK17 = sF24),
% 7.06/2.51 inference(superposition,[],[f861,f21827])).
% 7.06/2.51 tff(f22408,plain,(
% 7.06/2.51 sK17 = sF24),
% 7.06/2.51 inference(trivial_inequality_removal,[],[f22361])).
% 7.06/2.51 tff(f22508,plain,(
% 7.06/2.51 ~$less(sF29,sK17)),
% 7.06/2.51 inference(superposition,[],[f21749,f22408])).
% 7.06/2.51 tff(f22565,plain,(
% 7.06/2.51 $less(sK17,sF29) | sK17 = sF29),
% 7.06/2.51 inference(resolution,[],[f22508,f28])).
% 7.06/2.51 tff(f22566,plain,(
% 7.06/2.51 sK17 = sF29),
% 7.06/2.51 inference(forward_subsumption_resolution,[],[f22565,f1647])).
% 7.06/2.51 tff(f22637,plain,(
% 7.06/2.51 -1 = $sum(sK17,$uminus(sK17))),
% 7.06/2.51 inference(superposition,[],[f1872,f22566])).
% 7.06/2.51 tff(f22670,plain,(
% 7.06/2.51 0 = -1),
% 7.06/2.51 inference(forward_demodulation,[],[f22637,f25])).
% 7.06/2.51 tff(f22671,plain,(
% 7.06/2.51 $false),
% 7.06/2.51 inference(evaluation,[],[f22670])).
% 7.06/2.51 % SZS output end Proof for theBenchmark
% 7.06/2.51 % (417536)------------------------------
% 7.06/2.51 % (417536)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.06/2.51 % (417536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.06/2.51 % (417536)CaDiCaL version: 2.1.3
% 7.06/2.51 % (417536)Termination reason: Refutation
% 7.06/2.51 % (417536)Time elapsed: 1.034 s
% 7.06/2.51 % (417536)Peak memory usage: 21 MB
% 7.06/2.51 % (417536)Instructions burned: 1101 (million)
% 7.06/2.51 % (417481)Success in time 2.211 s
% 7.06/2.51 % Vampire exiting
%------------------------------------------------------------------------------