%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWX083_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 : n026.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 75.78s 10.98s
% Output : Refutation 75.78s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX083_1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.17 % Computer : n026.cluster.edu
% 0.08/0.17 % Model : x86_64 x86_64
% 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.17 % Memory : 8046.5625MB
% 0.08/0.17 % OS : Linux 6.8.0-71-generic
% 0.08/0.17 % CPULimit : 300
% 0.08/0.17 % WCLimit : 300
% 0.08/0.17 % DateTime : Mon Sep 28 15:03:11 UTC 2026
% 0.08/0.17 % CPUTime :
% 0.08/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.21 Running first-order model finding
% 0.08/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.18/0.91 % (3914572)Will run a generic schedule for satisfiability detection.
% 4.18/0.91 % (3914580)dis+10_1_sil=32000:sp=arity:random_seed=3450419823:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.18/0.91 % (3914578)% WARNING: option uhcvi not known.
% 4.18/0.91 % (3914577)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1713760290_2999 on theBenchmark for (2999ds/0Mi)
% 4.18/0.91 % (3914579)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=586776345:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.18/0.91 % (3914578)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1918083708:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.18/0.91 % (3914581)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3719257084:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.18/0.91 % (3914577)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 4.18/0.91 % (3914577)Terminated due to inappropriate strategy.
% 4.18/0.91 % (3914577)------------------------------
% 4.18/0.91 % (3914577)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.18/0.91 % (3914577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.18/0.91 % (3914577)CaDiCaL version: 2.1.3
% 4.18/0.91 % (3914577)Termination reason: Inappropriate
% 4.18/0.91 % (3914577)Time elapsed: 0.002 s
% 4.18/0.91 % (3914577)Peak memory usage: 10 MB
% 4.18/0.91 % (3914577)Instructions burned: 3 (million)
% 4.18/0.91 % (3914577)------------------------------
% 4.18/0.91 % (3914577)------------------------------
% 4.18/0.91 % (3914583)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=583517057:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.18/0.91 % (3914582)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1906573598:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.18/0.91 % (3914589)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1440868108:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 4.18/0.91 % (3914589)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 4.18/0.91 % (3914589)Terminated due to inappropriate strategy.
% 4.18/0.91 % (3914589)------------------------------
% 4.18/0.91 % (3914589)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.18/0.91 % (3914589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.18/0.91 % (3914589)CaDiCaL version: 2.1.3
% 4.18/0.91 % (3914589)Termination reason: Inappropriate
% 4.18/0.91 % (3914589)Time elapsed: 0.002 s
% 4.18/0.91 % (3914589)Peak memory usage: 10 MB
% 4.18/0.91 % (3914589)Instructions burned: 2 (million)
% 4.18/0.91 % (3914580)Instruction limit reached!
% 4.18/0.91 % (3914580)------------------------------
% 4.18/0.91 % (3914580)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.18/0.91 % (3914580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.18/0.91 % (3914580)CaDiCaL version: 2.1.3
% 4.18/0.91 % (3914580)Termination reason: Instruction limit
% 4.18/0.91 % (3914580)Termination phase: Saturation
% 4.18/0.91 % (3914580)Time elapsed: 0.036 s
% 4.18/0.91 % (3914580)Peak memory usage: 13 MB
% 4.18/0.91 % (3914580)Instructions burned: 103 (million)
% 4.18/0.91 % (3914589)------------------------------
% 4.18/0.91 % (3914589)------------------------------
% 4.18/0.91 % (3914593)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1629763313:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 4.18/0.91 % (3914594)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=793464022:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 4.18/0.91 % (3914581)Instruction limit reached!
% 4.18/0.91 % (3914581)------------------------------
% 4.18/0.91 % (3914581)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.18/0.91 % (3914581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.18/0.91 % (3914581)CaDiCaL version: 2.1.3
% 4.18/0.91 % (3914581)Termination reason: Instruction limit
% 4.18/0.91 % (3914581)Termination phase: Saturation
% 4.18/0.91 % (3914581)Time elapsed: 0.077 s
% 4.18/0.91 % (3914581)Peak memory usage: 13 MB
% 4.18/0.91 % (3914581)Instructions burned: 116 (million)
% 4.18/0.91 % (3914593)Instruction limit reached!
% 4.18/0.91 % (3914593)------------------------------
% 4.18/0.91 % (3914593)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.18/1.00 % (3914593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.18/1.00 % (3914593)CaDiCaL version: 2.1.3
% 4.18/1.00 % (3914593)Termination reason: Instruction limit
% 4.18/1.00 % (3914593)Termination phase: Saturation
% 4.18/1.00 % (3914593)Time elapsed: 0.047 s
% 4.18/1.00 % (3914593)Peak memory usage: 13 MB
% 4.18/1.00 % (3914593)Instructions burned: 132 (million)
% 4.18/1.00 % (3914582)Instruction limit reached!
% 4.18/1.00 % (3914582)------------------------------
% 4.18/1.00 % (3914582)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.18/1.00 % (3914582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.18/1.00 % (3914582)CaDiCaL version: 2.1.3
% 4.18/1.00 % (3914582)Termination reason: Instruction limit
% 4.18/1.00 % (3914582)Termination phase: Saturation
% 4.18/1.00 % (3914582)Time elapsed: 0.081 s
% 4.18/1.00 % (3914582)Peak memory usage: 13 MB
% 4.18/1.00 % (3914582)Instructions burned: 132 (million)
% 4.18/1.00 % (3914597)ott-21_1_sil=16000:fs=off:random_seed=2059730666:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 4.18/1.00 % (3914598)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2673431370:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 4.18/1.00 % (3914599)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1224723450:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 4.18/1.00 % (3914599)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 4.18/1.00 % (3914599)Terminated due to inappropriate strategy.
% 4.18/1.00 % (3914599)------------------------------
% 4.18/1.00 % (3914599)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.18/1.00 % (3914599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.18/1.00 % (3914599)CaDiCaL version: 2.1.3
% 4.18/1.00 % (3914599)Termination reason: Inappropriate
% 4.18/1.00 % (3914599)Time elapsed: 0.001 s
% 4.18/1.00 % (3914599)Peak memory usage: 10 MB
% 4.18/1.00 % (3914599)Instructions burned: 2 (million)
% 4.18/1.00 % (3914599)------------------------------
% 4.18/1.00 % (3914599)------------------------------
% 4.18/1.00 % (3914603)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2547153250:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 4.18/1.00 % (3914583)Instruction limit reached!
% 4.18/1.00 % (3914583)------------------------------
% 4.18/1.00 % (3914583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.18/1.00 % (3914583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.18/1.00 % (3914583)CaDiCaL version: 2.1.3
% 4.18/1.00 % (3914583)Termination reason: Instruction limit
% 4.18/1.00 % (3914583)Termination phase: Saturation
% 4.18/1.00 % (3914583)Time elapsed: 0.143 s
% 4.18/1.00 % (3914583)Peak memory usage: 13 MB
% 4.18/1.00 % (3914583)Instructions burned: 160 (million)
% 4.18/1.00 % (3914611)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=397017540:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 4.18/1.00 % (3914611)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 4.18/1.00 % (3914611)Terminated due to inappropriate strategy.
% 4.18/1.00 % (3914611)------------------------------
% 4.18/1.00 % (3914611)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.18/1.00 % (3914611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.18/1.00 % (3914611)CaDiCaL version: 2.1.3
% 4.18/1.00 % (3914611)Termination reason: Inappropriate
% 4.18/1.00 % (3914611)Time elapsed: 0.001 s
% 4.18/1.00 % (3914611)Peak memory usage: 10 MB
% 4.18/1.00 % (3914611)Instructions burned: 2 (million)
% 4.18/1.00 % (3914611)------------------------------
% 4.18/1.00 % (3914611)------------------------------
% 4.18/1.00 % (3914597)Instruction limit reached!
% 4.18/1.00 % (3914597)------------------------------
% 4.18/1.00 % (3914597)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.18/1.00 % (3914597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.18/1.00 % (3914597)CaDiCaL version: 2.1.3
% 4.18/1.00 % (3914597)Termination reason: Instruction limit
% 4.18/1.00 % (3914597)Termination phase: Saturation
% 4.18/1.00 % (3914597)Time elapsed: 0.084 s
% 4.18/1.00 % (3914597)Peak memory usage: 12 MB
% 4.18/1.00 % (3914597)Instructions burned: 180 (million)
% 4.18/1.00 % (3914616)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=1430382120: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)
% 26.02/3.94 % (3914617)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2111750270:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 26.02/3.94 % (3914598)Instruction limit reached!
% 26.02/3.94 % (3914598)------------------------------
% 26.02/3.94 % (3914598)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.02/3.94 % (3914598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.02/3.94 % (3914598)CaDiCaL version: 2.1.3
% 26.02/3.94 % (3914598)Termination reason: Instruction limit
% 26.02/3.94 % (3914598)Termination phase: Saturation
% 26.02/3.94 % (3914598)Time elapsed: 0.173 s
% 26.02/3.94 % (3914598)Peak memory usage: 13 MB
% 26.02/3.94 % (3914598)Instructions burned: 485 (million)
% 26.02/3.94 % (3914652)fmb+10_1_sil=64000:random_seed=3369030300:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi)
% 26.02/3.94 % (3914652)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 26.02/3.94 % (3914652)Terminated due to inappropriate strategy.
% 26.02/3.94 % (3914652)------------------------------
% 26.02/3.94 % (3914652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.02/3.94 % (3914652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.02/3.94 % (3914652)CaDiCaL version: 2.1.3
% 26.02/3.94 % (3914652)Termination reason: Inappropriate
% 26.02/3.94 % (3914652)Time elapsed: 0.001 s
% 26.02/3.94 % (3914652)Peak memory usage: 10 MB
% 26.02/3.94 % (3914652)Instructions burned: 2 (million)
% 26.02/3.94 % (3914652)------------------------------
% 26.02/3.94 % (3914652)------------------------------
% 26.02/3.94 % (3914659)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4069024774:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi)
% 26.02/3.94 % (3914659)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 26.02/3.94 % (3914659)Terminated due to inappropriate strategy.
% 26.02/3.94 % (3914659)------------------------------
% 26.02/3.94 % (3914659)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.02/3.94 % (3914659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.02/3.94 % (3914659)CaDiCaL version: 2.1.3
% 26.02/3.94 % (3914659)Termination reason: Inappropriate
% 26.02/3.94 % (3914659)Time elapsed: 0.001 s
% 26.02/3.94 % (3914659)Peak memory usage: 10 MB
% 26.02/3.94 % (3914659)Instructions burned: 2 (million)
% 26.02/3.94 % (3914659)------------------------------
% 26.02/3.94 % (3914659)------------------------------
% 26.02/3.94 % (3914670)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1075805450:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi)
% 26.02/3.94 % (3914670)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 26.02/3.94 % (3914670)Terminated due to inappropriate strategy.
% 26.02/3.94 % (3914670)------------------------------
% 26.02/3.94 % (3914670)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.02/3.94 % (3914670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.02/3.94 % (3914670)CaDiCaL version: 2.1.3
% 26.02/3.94 % (3914670)Termination reason: Inappropriate
% 26.02/3.94 % (3914670)Time elapsed: 0.001 s
% 26.02/3.94 % (3914670)Peak memory usage: 10 MB
% 26.02/3.94 % (3914670)Instructions burned: 2 (million)
% 26.02/3.94 % (3914670)------------------------------
% 26.02/3.94 % (3914670)------------------------------
% 26.02/3.94 % (3914677)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=369829734:i=5131_2996 on theBenchmark for (2996ds/5131Mi)
% 26.02/3.94 % (3914594)Instruction limit reached!
% 26.02/3.94 % (3914594)------------------------------
% 26.02/3.94 % (3914594)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.02/3.94 % (3914594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.02/3.94 % (3914594)CaDiCaL version: 2.1.3
% 26.02/3.94 % (3914594)Termination reason: Instruction limit
% 26.02/3.94 % (3914594)Termination phase: Saturation
% 26.02/3.94 % (3914594)Time elapsed: 0.377 s
% 26.02/3.94 % (3914594)Peak memory usage: 16 MB
% 26.02/3.94 % (3914594)Instructions burned: 684 (million)
% 26.02/3.94 % (3914711)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3155936037:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 26.02/3.94 % (3914616)Instruction limit reached!
% 26.02/3.94 % (3914616)------------------------------
% 41.23/6.06 % (3914616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.23/6.06 % (3914616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.23/6.06 % (3914616)CaDiCaL version: 2.1.3
% 41.23/6.06 % (3914616)Termination reason: Instruction limit
% 41.23/6.06 % (3914616)Termination phase: Saturation
% 41.23/6.06 % (3914616)Time elapsed: 0.456 s
% 41.23/6.06 % (3914616)Peak memory usage: 18 MB
% 41.23/6.06 % (3914616)Instructions burned: 693 (million)
% 41.23/6.06 % (3914751)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=902574910:i=6324_2993 on theBenchmark for (2993ds/6324Mi)
% 41.23/6.06 % (3914751)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 41.23/6.06 % (3914751)Terminated due to inappropriate strategy.
% 41.23/6.06 % (3914751)------------------------------
% 41.23/6.06 % (3914751)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.23/6.06 % (3914751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.23/6.06 % (3914751)CaDiCaL version: 2.1.3
% 41.23/6.06 % (3914751)Termination reason: Inappropriate
% 41.23/6.06 % (3914751)Time elapsed: 0.002 s
% 41.23/6.06 % (3914751)Peak memory usage: 11 MB
% 41.23/6.06 % (3914751)Instructions burned: 3 (million)
% 41.23/6.06 % (3914751)------------------------------
% 41.23/6.06 % (3914751)------------------------------
% 41.23/6.06 % (3914603)Instruction limit reached!
% 41.23/6.06 % (3914603)------------------------------
% 41.23/6.06 % (3914603)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.23/6.06 % (3914603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.23/6.06 % (3914603)CaDiCaL version: 2.1.3
% 41.23/6.06 % (3914603)Termination reason: Instruction limit
% 41.23/6.06 % (3914603)Termination phase: Saturation
% 41.23/6.06 % (3914603)Time elapsed: 0.553 s
% 41.23/6.06 % (3914603)Peak memory usage: 18 MB
% 41.23/6.06 % (3914603)Instructions burned: 1179 (million)
% 41.23/6.06 % (3914753)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=662269807:fmbsr=2.30978:i=2174_2992 on theBenchmark for (2992ds/2174Mi)
% 41.23/6.06 % (3914753)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 41.23/6.06 % (3914753)Terminated due to inappropriate strategy.
% 41.23/6.06 % (3914753)------------------------------
% 41.23/6.06 % (3914753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.23/6.06 % (3914753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.23/6.06 % (3914753)CaDiCaL version: 2.1.3
% 41.23/6.06 % (3914753)Termination reason: Inappropriate
% 41.23/6.06 % (3914753)Time elapsed: 0.002 s
% 41.23/6.06 % (3914753)Peak memory usage: 10 MB
% 41.23/6.06 % (3914753)Instructions burned: 2 (million)
% 41.23/6.06 % (3914753)------------------------------
% 41.23/6.06 % (3914753)------------------------------
% 41.23/6.06 % (3914754)ott-2_1_sil=16000:newcnf=on:random_seed=1997590610:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2992 on theBenchmark for (2992ds/869Mi)
% 41.23/6.06 % (3914617)Instruction limit reached!
% 41.23/6.06 % (3914617)------------------------------
% 41.23/6.06 % (3914617)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.23/6.06 % (3914617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.23/6.06 % (3914617)CaDiCaL version: 2.1.3
% 41.23/6.06 % (3914617)Termination reason: Instruction limit
% 41.23/6.06 % (3914617)Termination phase: Saturation
% 41.23/6.06 % (3914617)Time elapsed: 0.512 s
% 41.23/6.06 % (3914617)Peak memory usage: 18 MB
% 41.23/6.06 % (3914617)Instructions burned: 880 (million)
% 41.23/6.06 % (3914756)ott+10_1_sil=32000:tgt=ground:random_seed=3883484935:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi)
% 41.23/6.06 % (3914758)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=415369446:i=54282_2992 on theBenchmark for (2992ds/54282Mi)
% 41.23/6.06 % (3914758)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 41.23/6.06 % (3914758)Terminated due to inappropriate strategy.
% 41.23/6.06 % (3914758)------------------------------
% 41.23/6.06 % (3914758)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.23/6.06 % (3914758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.23/6.06 % (3914758)CaDiCaL version: 2.1.3
% 41.23/6.06 % (3914758)Termination reason: Inappropriate
% 41.23/6.06 % (3914758)Time elapsed: 0.002 s
% 41.23/6.06 % (3914758)Peak memory usage: 11 MB
% 41.23/6.06 % (3914758)Instructions burned: 3 (million)
% 75.78/10.98 % (3914758)------------------------------
% 75.78/10.98 % (3914758)------------------------------
% 75.78/10.98 % (3914761)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3577095012:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi)
% 75.78/10.98 % (3914754)Instruction limit reached!
% 75.78/10.98 % (3914754)------------------------------
% 75.78/10.98 % (3914754)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 75.78/10.98 % (3914754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.78/10.98 % (3914754)CaDiCaL version: 2.1.3
% 75.78/10.98 % (3914754)Termination reason: Instruction limit
% 75.78/10.98 % (3914754)Termination phase: Saturation
% 75.78/10.98 % (3914754)Time elapsed: 0.484 s
% 75.78/10.98 % (3914754)Peak memory usage: 18 MB
% 75.78/10.98 % (3914754)Instructions burned: 870 (million)
% 75.78/10.98 % (3914763)dis+21_1_sil=32000:sas=cadical:random_seed=2192618371:i=3773:amm=off_2987 on theBenchmark for (2987ds/3773Mi)
% 75.78/10.98 % (3914711)Instruction limit reached!
% 75.78/10.98 % (3914711)------------------------------
% 75.78/10.98 % (3914711)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 75.78/10.98 % (3914711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.78/10.98 % (3914711)CaDiCaL version: 2.1.3
% 75.78/10.98 % (3914711)Termination reason: Instruction limit
% 75.78/10.98 % (3914711)Termination phase: Saturation
% 75.78/10.98 % (3914711)Time elapsed: 1.114 s
% 75.78/10.98 % (3914711)Peak memory usage: 29 MB
% 75.78/10.98 % (3914711)Instructions burned: 1472 (million)
% 75.78/10.98 % (3914787)ott+11_1_sil=16000:gs=on:random_seed=4235448061:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2983 on theBenchmark for (2983ds/2251Mi)
% 75.78/10.98 % (3914677)Instruction limit reached!
% 75.78/10.98 % (3914677)------------------------------
% 75.78/10.98 % (3914677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 75.78/10.98 % (3914677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.78/10.98 % (3914677)CaDiCaL version: 2.1.3
% 75.78/10.98 % (3914677)Termination reason: Instruction limit
% 75.78/10.98 % (3914677)Termination phase: Saturation
% 75.78/10.98 % (3914677)Time elapsed: 1.496 s
% 75.78/10.98 % (3914677)Peak memory usage: 38 MB
% 75.78/10.98 % (3914677)Instructions burned: 5133 (million)
% 75.78/10.98 % (3914801)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=4176701203:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi)
% 75.78/10.98 % (3914801)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 75.78/10.98 % (3914801)Terminated due to inappropriate strategy.
% 75.78/10.98 % (3914801)------------------------------
% 75.78/10.98 % (3914801)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 75.78/10.98 % (3914801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.78/10.98 % (3914801)CaDiCaL version: 2.1.3
% 75.78/10.98 % (3914801)Termination reason: Inappropriate
% 75.78/10.98 % (3914801)Time elapsed: 0.003 s
% 75.78/10.98 % (3914801)Peak memory usage: 10 MB
% 75.78/10.98 % (3914801)Instructions burned: 2 (million)
% 75.78/10.98 % (3914801)------------------------------
% 75.78/10.98 % (3914801)------------------------------
% 75.78/10.98 % (3914806)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2959490084:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi)
% 75.78/10.98 % (3914761)Instruction limit reached!
% 75.78/10.98 % (3914761)------------------------------
% 75.78/10.98 % (3914761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 75.78/10.98 % (3914761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.78/10.98 % (3914761)CaDiCaL version: 2.1.3
% 75.78/10.98 % (3914761)Termination reason: Instruction limit
% 75.78/10.98 % (3914761)Termination phase: Saturation
% 75.78/10.98 % (3914761)Time elapsed: 1.797 s
% 75.78/10.98 % (3914761)Peak memory usage: 34 MB
% 75.78/10.98 % (3914761)Instructions burned: 3512 (million)
% 75.78/10.98 % (3914842)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3041229546:i=29340_2973 on theBenchmark for (2973ds/29340Mi)
% 75.78/10.98 % (3914787)Instruction limit reached!
% 75.78/10.98 % (3914787)------------------------------
% 75.78/10.98 % (3914787)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 75.78/10.98 % (3914787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.78/10.98 % (3914787)CaDiCaL version: 2.1.3
% 75.78/10.98 % (3914787)Termination reason: Instruction limit
% 75.78/10.98 % (3914787)Termination phase: Saturation
% 75.78/10.98 % (3914787)Time elapsed: 2.083 s
% 75.78/10.98 % (3914787)Peak memory usage: 26 MB
% 75.78/10.98 % (3914787)Instructions burned: 2251 (million)
% 75.78/10.98 % (3914882)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3010814041:i=5211_2962 on theBenchmark for (2962ds/5211Mi)
% 75.78/10.98 % (3914763)Instruction limit reached!
% 75.78/10.98 % (3914763)------------------------------
% 75.78/10.98 % (3914763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 75.78/10.98 % (3914763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.78/10.98 % (3914763)CaDiCaL version: 2.1.3
% 75.78/10.98 % (3914763)Termination reason: Instruction limit
% 75.78/10.98 % (3914763)Termination phase: Saturation
% 75.78/10.98 % (3914763)Time elapsed: 3.124 s
% 75.78/10.98 % (3914763)Peak memory usage: 39 MB
% 75.78/10.98 % (3914763)Instructions burned: 3774 (million)
% 75.78/10.98 % (3914904)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2109837536:i=5497:nm=2_2956 on theBenchmark for (2956ds/5497Mi)
% 75.78/10.98 % (3914904)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 75.78/10.98 % (3914904)Terminated due to inappropriate strategy.
% 75.78/10.98 % (3914904)------------------------------
% 75.78/10.98 % (3914904)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 75.78/10.98 % (3914904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.78/10.98 % (3914904)CaDiCaL version: 2.1.3
% 75.78/10.98 % (3914904)Termination reason: Inappropriate
% 75.78/10.98 % (3914904)Time elapsed: 0.003 s
% 75.78/10.98 % (3914904)Peak memory usage: 11 MB
% 75.78/10.98 % (3914904)Instructions burned: 3 (million)
% 75.78/10.98 % (3914904)------------------------------
% 75.78/10.98 % (3914904)------------------------------
% 75.78/10.98 % (3914906)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2603647860:fmbsr=2:i=46332_2955 on theBenchmark for (2955ds/46332Mi)
% 75.78/10.98 % (3914906)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 75.78/10.98 % (3914906)Terminated due to inappropriate strategy.
% 75.78/10.98 % (3914906)------------------------------
% 75.78/10.98 % (3914906)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 75.78/10.98 % (3914906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.78/10.98 % (3914906)CaDiCaL version: 2.1.3
% 75.78/10.98 % (3914906)Termination reason: Inappropriate
% 75.78/10.98 % (3914906)Time elapsed: 0.002 s
% 75.78/10.98 % (3914906)Peak memory usage: 11 MB
% 75.78/10.98 % (3914906)Instructions burned: 2 (million)
% 75.78/10.98 % (3914906)------------------------------
% 75.78/10.98 % (3914906)------------------------------
% 75.78/10.98 % (3914908)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=815341720:i=14071_2955 on theBenchmark for (2955ds/14071Mi)
% 75.78/10.98 % (3914908)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 75.78/10.98 % (3914908)Terminated due to inappropriate strategy.
% 75.78/10.98 % (3914908)------------------------------
% 75.78/10.98 % (3914908)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 75.78/10.98 % (3914908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.78/10.98 % (3914908)CaDiCaL version: 2.1.3
% 75.78/10.98 % (3914908)Termination reason: Inappropriate
% 75.78/10.98 % (3914908)Time elapsed: 0.003 s
% 75.78/10.98 % (3914908)Peak memory usage: 11 MB
% 75.78/10.98 % (3914908)Instructions burned: 2 (million)
% 75.78/10.98 % (3914908)------------------------------
% 75.78/10.98 % (3914908)------------------------------
% 75.78/10.98 % (3914910)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1739811891:i=22565:add=on:rawr=on_2955 on theBenchmark for (2955ds/22565Mi)
% 75.78/10.98 % (3914756)Instruction limit reached!
% 75.78/10.98 % (3914756)------------------------------
% 75.78/10.98 % (3914756)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 75.78/10.98 % (3914756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.78/10.98 % (3914756)CaDiCaL version: 2.1.3
% 75.78/10.98 % (3914756)Termination reason: Instruction limit
% 75.78/10.98 % (3914756)Termination phase: Saturation
% 75.78/10.98 % (3914756)Time elapsed: 4.673 s
% 75.78/10.98 % (3914756)Peak memory usage: 41 MB
% 75.78/10.98 % (3914756)Instructions burned: 5114 (million)
% 75.78/10.98 % (3914937)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=4249457215:i=8173:av=off_2945 on theBenchmark for (2945ds/8173Mi)
% 75.78/10.98 % (3914806)Instruction limit reached!
% 75.78/10.98 % (3914806)------------------------------
% 75.78/10.98 % (3914806)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 75.78/10.98 % (3914806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.78/10.98 % (3914806)CaDiCaL version: 2.1.3
% 75.78/10.98 % (3914806)Termination reason: Instruction limit
% 75.78/10.98 % (3914806)Termination phase: Saturation
% 75.78/10.98 % (3914806)Time elapsed: 3.915 s
% 75.78/10.98 % (3914806)Peak memory usage: 57 MB
% 75.78/10.98 % (3914806)Instructions burned: 4591 (million)
% 75.78/10.98 % (3914943)dis+10_16:1_sil=16000:random_seed=3293513692:i=9155:fsr=off_2941 on theBenchmark for (2941ds/9155Mi)
% 75.78/10.98 % (3914882)Instruction limit reached!
% 75.78/10.98 % (3914882)------------------------------
% 75.78/10.98 % (3914882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 75.78/10.98 % (3914882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.78/10.98 % (3914882)CaDiCaL version: 2.1.3
% 75.78/10.98 % (3914882)Termination reason: Instruction limit
% 75.78/10.98 % (3914882)Termination phase: Saturation
% 75.78/10.98 % (3914882)Time elapsed: 4.553 s
% 75.78/10.98 % (3914882)Peak memory usage: 52 MB
% 75.78/10.98 % (3914882)Instructions burned: 5212 (million)
% 75.78/10.98 % (3914987)ott-3_8_sil=64000:random_seed=1230255023:i=20139:bs=on_2916 on theBenchmark for (2916ds/20139Mi)
% 75.78/10.98 % (3914987) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3914572-3914987"...
% 75.78/10.98 % (3914987)...printing done.
% 75.78/10.98 % (3914987)Refutation found. Thanks to Tanya!
% 75.78/10.98 % SZS status Theorem for theBenchmark
% 75.78/10.98 % SZS output start Proof for theBenchmark
% 75.78/10.98 tff(type_def_5, type, general: $tType).
% 75.78/10.98 tff(type_def_6, type, symbol: $tType).
% 75.78/10.98 tff(func_def_0, type, f__integer__: $int > general).
% 75.78/10.98 tff(func_def_1, type, f__symbolic__: symbol > general).
% 75.78/10.98 tff(func_def_2, type, c__infimum__: general).
% 75.78/10.98 tff(func_def_3, type, c__supremum__: general).
% 75.78/10.98 tff(func_def_10, type, sK0: general > $int).
% 75.78/10.98 tff(func_def_11, type, sK1: general > symbol).
% 75.78/10.98 tff(func_def_12, type, sK2: (general * general * general * general) > general).
% 75.78/10.98 tff(func_def_13, type, sK3: (general * general * general * general) > general).
% 75.78/10.98 tff(func_def_14, type, sK4: (general * general * general * general) > general).
% 75.78/10.98 tff(func_def_15, type, sK5: (general * general * general * general) > general).
% 75.78/10.98 tff(func_def_16, type, sK6: (general * general * general * general) > general).
% 75.78/10.98 tff(func_def_17, type, sK7: (general * general * general * general) > general).
% 75.78/10.98 tff(func_def_18, type, sK8: (general * general * general * general) > $int).
% 75.78/10.98 tff(func_def_19, type, sK9: (general * general * general * general) > $int).
% 75.78/10.98 tff(func_def_20, type, sK10: (general * general * general * general) > $int).
% 75.78/10.98 tff(func_def_21, type, sK11: (general * general * general * general) > $int).
% 75.78/10.98 tff(func_def_22, type, sK12: (general * general * general * general) > general).
% 75.78/10.98 tff(func_def_23, type, sK13: (general * general * general * general) > general).
% 75.78/10.98 tff(func_def_24, type, sK14: (general * general * general * general) > general).
% 75.78/10.98 tff(func_def_25, type, sK15: (general * general * general * general) > general).
% 75.78/10.98 tff(func_def_26, type, sK16: $int).
% 75.78/10.98 tff(func_def_27, type, sK17: $int).
% 75.78/10.98 tff(func_def_28, type, sK18: $int).
% 75.78/10.98 tff(func_def_29, type, sK19: $int).
% 75.78/10.98 tff(pred_def_1, type, p__is_integer__: general > $o).
% 75.78/10.98 tff(pred_def_2, type, p__is_symbolic__: general > $o).
% 75.78/10.98 tff(pred_def_3, type, p__less_equal__: (general * general) > $o).
% 75.78/10.98 tff(pred_def_4, type, p__less__: (general * general) > $o).
% 75.78/10.98 tff(pred_def_5, type, p__greater_equal__: (general * general) > $o).
% 75.78/10.98 tff(pred_def_6, type, p__greater__: (general * general) > $o).
% 75.78/10.98 tff(pred_def_8, type, div: (general * general * general * general) > $o).
% 75.78/10.98 tff(f6,axiom,(
% 75.78/10.98 ! [X0 : $int,X1 : $int] : (p__less_equal__(f__integer__(X0),f__integer__(X1)) <=> $lesseq(X0,X1))),
% 75.78/10.98 file('/export/starexec/sandbox/benchmark/Axioms/SWV014_0.ax',numeral_ordering_ax)).
% 75.78/10.98 tff(f7,axiom,(
% 75.78/10.98 ! [X0 : general,X1 : general] : ((p__less_equal__(X0,X1) & p__less_equal__(X1,X0)) => X0 = X1)),
% 75.78/10.98 file('/export/starexec/sandbox/benchmark/Axioms/SWV014_0.ax',antisymmetric_ordering_ax)).
% 75.78/10.98 tff(f8,axiom,(
% 75.78/10.98 ! [X0 : general,X1 : general,X2 : general] : ((p__less_equal__(X0,X1) & p__less_equal__(X1,X2)) => p__less_equal__(X0,X2))),
% 75.78/10.98 file('/export/starexec/sandbox/benchmark/Axioms/SWV014_0.ax',transitive_ordering_ax)).
% 75.78/10.98 tff(f10,axiom,(
% 75.78/10.98 ! [X0 : general,X1 : general] : (p__less__(X0,X1) <=> (p__less_equal__(X0,X1) & X0 != X1))),
% 75.78/10.98 file('/export/starexec/sandbox/benchmark/Axioms/SWV014_0.ax',p__less__def_ax)).
% 75.78/10.98 tff(f16,axiom,(
% 75.78/10.98 ! [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))))),
% 75.78/10.98 file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_0_completed_definition_of_div_4)).
% 75.78/10.98 tff(f17,axiom,(
% 75.78/10.98 ! [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))))),
% 75.78/10.98 file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_1_unnamed_formula)).
% 75.78/10.98 tff(f18,axiom,(
% 75.78/10.98 ! [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)))),
% 75.78/10.98 file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_2_unnamed_formula)).
% 75.78/10.98 tff(f19,conjecture,(
% 75.78/10.98 ! [X0 : $int,X1 : $int] : (($greatereq(X0,0) & ($greater(X1,0) => ? [X2 : $int,X3 : $int] : div(f__integer__(X0),f__integer__(X1),f__integer__(X2),f__integer__(X3)))) => ($greater(X1,0) => ? [X2 : $int,X3 : $int] : div(f__integer__($sum(X0,1)),f__integer__(X1),f__integer__(X2),f__integer__(X3))))),
% 75.78/10.98 file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_3_inductive_step)).
% 75.78/10.98 tff(f20,negated_conjecture,(
% 75.78/10.98 ~ ! [X0 : $int,X1 : $int] : (($greatereq(X0,0) & ($greater(X1,0) => ? [X2 : $int,X3 : $int] : div(f__integer__(X0),f__integer__(X1),f__integer__(X2),f__integer__(X3)))) => ($greater(X1,0) => ? [X2 : $int,X3 : $int] : div(f__integer__($sum(X0,1)),f__integer__(X1),f__integer__(X2),f__integer__(X3))))),
% 75.78/10.98 inference(negated_conjecture,[status(cth)],[f19])).
% 75.78/10.98 tff(f21,plain,(
% 75.78/10.98 ! [X0 : $int,X1 : $int] : (p__less_equal__(f__integer__(X0),f__integer__(X1)) <=> ~$less(X1,X0))),
% 75.78/10.98 inference(theory_normalization,[],[f6])).
% 75.78/10.98 tff(f22,plain,(
% 75.78/10.98 ! [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))))),
% 75.78/10.98 inference(theory_normalization,[],[f17])).
% 75.78/10.98 tff(f23,plain,(
% 75.78/10.98 ! [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)))),
% 75.78/10.98 inference(theory_normalization,[],[f18])).
% 75.78/10.98 tff(f24,plain,(
% 75.78/10.98 ~ ! [X0 : $int,X1 : $int] : ((~$less(X0,0) & ($less(0,X1) => ? [X2 : $int,X3 : $int] : div(f__integer__(X0),f__integer__(X1),f__integer__(X2),f__integer__(X3)))) => ($less(0,X1) => ? [X2 : $int,X3 : $int] : div(f__integer__($sum(X0,1)),f__integer__(X1),f__integer__(X2),f__integer__(X3))))),
% 75.78/10.98 inference(theory_normalization,[],[f20])).
% 75.78/10.98 tff(f25,definition,(
% 75.78/10.98 ( ! [X0 : $int,X1 : $int] : ($sum(X0,X1) = $sum(X1,X0)) )),
% 75.78/10.98 introduced(theory,[tha_commutativity])).
% 75.78/10.98 tff(f26,definition,(
% 75.78/10.98 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum(X0,$sum(X1,X2)) = $sum($sum(X0,X1),X2)) )),
% 75.78/10.98 introduced(theory,[tha_associativity])).
% 75.78/10.98 tff(f29,definition,(
% 75.78/10.98 ( ! [X0 : $int] : (0 = $sum(X0,$uminus(X0))) )),
% 75.78/10.98 introduced(theory,[tha_inverse_op_unit])).
% 75.78/10.98 tff(f30,definition,(
% 75.78/10.98 ( ! [X0 : $int] : (~$less(X0,X0)) )),
% 75.78/10.98 introduced(theory,[tha_non-reflexivity])).
% 75.78/10.98 tff(f32,definition,(
% 75.78/10.98 ( ! [X0 : $int,X1 : $int] : ($less(X1,X0) | $less(X0,X1) | X0 = X1) )),
% 75.78/10.98 introduced(theory,[tha_order_totality])).
% 75.78/10.98 tff(f42,definition,(
% 75.78/10.98 ( ! [X0 : $int,X1 : $int] : (~$less(X1,$sum(X0,1)) | ~$less(X0,X1)) )),
% 75.78/10.98 introduced(theory,[tha_extra_integer_ordering])).
% 75.78/10.98 tff(f43,plain,(
% 75.78/10.98 ! [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))))),
% 75.78/10.98 inference(rectify,[],[f16])).
% 75.78/10.98 tff(f44,plain,(
% 75.78/10.98 ~ ! [X0 : $int,X1 : $int] : ((~$less(X0,0) & ($less(0,X1) => ? [X2 : $int,X3 : $int] : div(f__integer__(X0),f__integer__(X1),f__integer__(X2),f__integer__(X3)))) => ($less(0,X1) => ? [X4 : $int,X5 : $int] : div(f__integer__($sum(X0,1)),f__integer__(X1),f__integer__(X4),f__integer__(X5))))),
% 75.78/10.98 inference(rectify,[],[f24])).
% 75.78/10.98 tff(f49,plain,(
% 75.78/10.98 ! [X0 : general,X1 : general] : (X0 = X1 | (~p__less_equal__(X0,X1) | ~p__less_equal__(X1,X0)))),
% 75.78/10.98 inference(ennf_transformation,[],[f7])).
% 75.78/10.98 tff(f50,plain,(
% 75.78/10.98 ! [X0 : general,X1 : general] : (X0 = X1 | ~p__less_equal__(X0,X1) | ~p__less_equal__(X1,X0))),
% 75.78/10.98 inference(flattening,[],[f49])).
% 75.78/10.98 tff(f51,plain,(
% 75.78/10.98 ! [X0 : general,X1 : general,X2 : general] : (p__less_equal__(X0,X2) | (~p__less_equal__(X0,X1) | ~p__less_equal__(X1,X2)))),
% 75.78/10.98 inference(ennf_transformation,[],[f8])).
% 75.78/10.98 tff(f52,plain,(
% 75.78/10.98 ! [X0 : general,X1 : general,X2 : general] : (p__less_equal__(X0,X2) | ~p__less_equal__(X0,X1) | ~p__less_equal__(X1,X2))),
% 75.78/10.98 inference(flattening,[],[f51])).
% 75.78/10.98 tff(f53,plain,(
% 75.78/10.98 ! [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)))))),
% 75.78/10.98 inference(ennf_transformation,[],[f22])).
% 75.78/10.98 tff(f54,plain,(
% 75.78/10.98 ! [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))))),
% 75.78/10.98 inference(flattening,[],[f53])).
% 75.78/10.98 tff(f55,plain,(
% 75.78/10.98 ! [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)))))),
% 75.78/10.98 inference(ennf_transformation,[],[f23])).
% 75.78/10.98 tff(f56,plain,(
% 75.78/10.98 ? [X0 : $int,X1 : $int] : ((! [X4 : $int,X5 : $int] : ~div(f__integer__($sum(X0,1)),f__integer__(X1),f__integer__(X4),f__integer__(X5)) & $less(0,X1)) & (~$less(X0,0) & (? [X2 : $int,X3 : $int] : div(f__integer__(X0),f__integer__(X1),f__integer__(X2),f__integer__(X3)) | ~$less(0,X1))))),
% 75.78/10.98 inference(ennf_transformation,[],[f44])).
% 75.78/10.98 tff(f57,plain,(
% 75.78/10.98 ? [X0 : $int,X1 : $int] : (! [X4 : $int,X5 : $int] : ~div(f__integer__($sum(X0,1)),f__integer__(X1),f__integer__(X4),f__integer__(X5)) & $less(0,X1) & ~$less(X0,0) & (? [X2 : $int,X3 : $int] : div(f__integer__(X0),f__integer__(X1),f__integer__(X2),f__integer__(X3)) | ~$less(0,X1)))),
% 75.78/10.98 inference(flattening,[],[f56])).
% 75.78/10.98 tff(f62,plain,(
% 75.78/10.98 ! [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))))),
% 75.78/10.98 inference(nnf_transformation,[],[f21])).
% 75.78/10.98 tff(f63,plain,(
% 75.78/10.98 ! [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)))),
% 75.78/10.98 inference(nnf_transformation,[],[f10])).
% 75.78/10.98 tff(f64,plain,(
% 75.78/10.98 ! [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)))),
% 75.78/10.98 inference(flattening,[],[f63])).
% 75.78/10.98 tff(f65,plain,(
% 75.78/10.98 ! [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)))),
% 75.78/10.98 inference(nnf_transformation,[],[f43])).
% 75.78/10.98 tff(f66,plain,(
% 75.78/10.98 ! [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)))),
% 75.78/10.98 inference(rectify,[],[f65])).
% 75.78/10.98 tff(f67,plain,(
% 75.78/10.98 ! [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)))),
% 75.78/10.98 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))],[f66])).
% 75.78/10.98 tff(f68,plain,(
% 75.78/10.98 ? [X0 : $int,X1 : $int] : (! [X2 : $int,X3 : $int] : ~div(f__integer__($sum(X0,1)),f__integer__(X1),f__integer__(X2),f__integer__(X3)) & $less(0,X1) & ~$less(X0,0) & (? [X4 : $int,X5 : $int] : div(f__integer__(X0),f__integer__(X1),f__integer__(X4),f__integer__(X5)) | ~$less(0,X1)))),
% 75.78/10.98 inference(rectify,[],[f57])).
% 75.78/10.98 tff(f69,plain,(
% 75.78/10.98 ! [X2 : $int,X3 : $int] : ~div(f__integer__($sum(sK16,1)),f__integer__(sK17),f__integer__(X2),f__integer__(X3)) & $less(0,sK17) & ~$less(sK16,0) & (div(f__integer__(sK16),f__integer__(sK17),f__integer__(sK18),f__integer__(sK19)) | ~$less(0,sK17))),
% 75.78/10.98 inference(skolemize,[status(esa),new_symbols(skolem,[sK16,sK17,sK18,sK19]),skolemize(X0,sK16),skolemize(X1,sK17),skolemize(X4,sK18),skolemize(X5,sK19)],[f68])).
% 75.78/10.98 tff(f78,plain,(
% 75.78/10.98 ( ! [X0 : $int,X1 : $int] : (p__less_equal__(f__integer__(X0),f__integer__(X1)) | $less(X1,X0)) )),
% 75.78/10.98 inference(cnf_transformation,[],[f62])).
% 75.78/10.98 tff(f79,plain,(
% 75.78/10.98 ( ! [X0 : general,X1 : general] : (~p__less_equal__(X1,X0) | ~p__less_equal__(X0,X1) | X0 = X1) )),
% 75.78/10.98 inference(cnf_transformation,[],[f50])).
% 75.78/10.98 tff(f80,plain,(
% 75.78/10.98 ( ! [X2 : general,X0 : general,X1 : general] : (p__less_equal__(X0,X2) | ~p__less_equal__(X0,X1) | ~p__less_equal__(X1,X2)) )),
% 75.78/10.98 inference(cnf_transformation,[],[f52])).
% 75.78/10.98 tff(f82,plain,(
% 75.78/10.98 ( ! [X0 : general,X1 : general] : (X0 != X1 | ~p__less__(X0,X1)) )),
% 75.78/10.98 inference(cnf_transformation,[],[f64])).
% 75.78/10.98 tff(f83,plain,(
% 75.78/10.98 ( ! [X0 : general,X1 : general] : (~p__less__(X0,X1) | p__less_equal__(X0,X1)) )),
% 75.78/10.98 inference(cnf_transformation,[],[f64])).
% 75.78/10.98 tff(f88,plain,(
% 75.78/10.98 ( ! [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)) )),
% 75.78/10.98 inference(cnf_transformation,[],[f67])).
% 75.78/10.98 tff(f89,plain,(
% 75.78/10.98 ( ! [X2 : general,X3 : general,X0 : general,X1 : general] : (~div(X0,X1,X2,X3) | sK3(X0,X1,X2,X3) = sK15(X0,X1,X2,X3)) )),
% 75.78/10.98 inference(cnf_transformation,[],[f67])).
% 75.78/10.98 tff(f90,plain,(
% 75.78/10.98 ( ! [X2 : general,X3 : general,X0 : general,X1 : general] : (~div(X0,X1,X2,X3) | sK5(X0,X1,X2,X3) = sK14(X0,X1,X2,X3)) )),
% 75.78/10.98 inference(cnf_transformation,[],[f67])).
% 75.78/10.98 tff(f101,plain,(
% 75.78/10.98 ( ! [X2 : general,X3 : general,X0 : general,X1 : general] : (~div(X0,X1,X2,X3) | sK5(X0,X1,X2,X3) = X3) )),
% 75.78/10.98 inference(cnf_transformation,[],[f67])).
% 75.78/10.98 tff(f103,plain,(
% 75.78/10.98 ( ! [X2 : general,X3 : general,X0 : general,X1 : general] : (~div(X0,X1,X2,X3) | sK3(X0,X1,X2,X3) = X1) )),
% 75.78/10.98 inference(cnf_transformation,[],[f67])).
% 75.78/10.98 tff(f106,plain,(
% 75.78/10.98 ( ! [X2 : $int,X3 : $int,X0 : $int,X1 : $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)))) )),
% 75.78/10.98 inference(cnf_transformation,[],[f54])).
% 75.78/10.98 tff(f107,plain,(
% 75.78/10.98 ( ! [X2 : $int,X0 : $int,X1 : $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))))) )),
% 75.78/10.98 inference(cnf_transformation,[],[f55])).
% 75.78/10.98 tff(f108,plain,(
% 75.78/10.98 div(f__integer__(sK16),f__integer__(sK17),f__integer__(sK18),f__integer__(sK19)) | ~$less(0,sK17)),
% 75.78/10.98 inference(cnf_transformation,[],[f69])).
% 75.78/10.98 tff(f110,plain,(
% 75.78/10.98 $less(0,sK17)),
% 75.78/10.98 inference(cnf_transformation,[],[f69])).
% 75.78/10.98 tff(f111,plain,(
% 75.78/10.98 ( ! [X2 : $int,X3 : $int] : (~div(f__integer__($sum(sK16,1)),f__integer__(sK17),f__integer__(X2),f__integer__(X3))) )),
% 75.78/10.98 inference(cnf_transformation,[],[f69])).
% 75.78/10.98 tff(f115,plain,(
% 75.78/10.98 ( ! [X1 : general] : (~p__less__(X1,X1)) )),
% 75.78/10.98 inference(equality_resolution,[],[f82])).
% 75.78/10.98 tff(f131,plain,(
% 75.78/10.98 ( ! [X2 : $int,X0 : $int,X1 : $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,-1)))) )),
% 75.78/10.98 inference(evaluation,[],[f107])).
% 75.78/10.98 tff(f132,plain,(
% 75.78/10.98 ( ! [X2 : $int,X3 : $int,X0 : $int,X1 : $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,-1))) )),
% 75.78/10.98 inference(evaluation,[],[f106])).
% 75.78/10.98 tff(f134,definition,(
% 75.78/10.98 spl20_1 <=> $less(0,sK17)),
% 75.78/10.98 introduced(definition,[new_symbols(definition,[spl20_1])],[avatar_definition])).
% 75.78/10.98 tff(f138,definition,(
% 75.78/10.98 spl20_2 <=> div(f__integer__(sK16),f__integer__(sK17),f__integer__(sK18),f__integer__(sK19))),
% 75.78/10.98 introduced(definition,[new_symbols(definition,[spl20_2])],[avatar_definition])).
% 75.78/10.98 tff(f140,plain,(
% 75.78/10.98 div(f__integer__(sK16),f__integer__(sK17),f__integer__(sK18),f__integer__(sK19)) | ~spl20_2),
% 75.78/10.98 inference(avatar_component_clause,[],[f138])).
% 75.78/10.98 tff(f141,plain,(
% 75.78/10.98 ~spl20_1 | spl20_2),
% 75.78/10.98 inference(avatar_split_clause,[],[f108,f138,f134])).
% 75.78/10.98 tff(f142,plain,(
% 75.78/10.98 spl20_1),
% 75.78/10.98 inference(avatar_split_clause,[],[f110,f134])).
% 75.78/10.98 tff(f175,plain,(
% 75.78/10.98 ( ! [X0 : $int,X1 : $int] : (~$less(X1,$sum(1,X0)) | ~$less(X0,X1)) )),
% 75.78/10.98 inference(superposition,[],[f42,f25])).
% 75.78/10.98 tff(f1620,plain,(
% 75.78/10.98 ( ! [X0 : $int,X1 : $int] : ($sum(0,X1) = $sum(X0,$sum($uminus(X0),X1))) )),
% 75.78/10.98 inference(superposition,[],[f26,f29])).
% 75.78/10.98 tff(f1653,plain,(
% 75.78/10.98 ( ! [X0 : $int,X1 : $int] : ($sum(X0,$sum($uminus(X0),X1)) = X1) )),
% 75.78/10.98 inference(evaluation,[],[f1620])).
% 75.78/10.98 tff(f2258,plain,(
% 75.78/10.98 f__integer__(sK19) = sK5(f__integer__(sK16),f__integer__(sK17),f__integer__(sK18),f__integer__(sK19)) | ~spl20_2),
% 75.78/10.98 inference(resolution,[],[f101,f140])).
% 75.78/10.98 tff(f3178,plain,(
% 75.78/10.98 f__integer__(sK17) = sK3(f__integer__(sK16),f__integer__(sK17),f__integer__(sK18),f__integer__(sK19)) | ~spl20_2),
% 75.78/10.98 inference(resolution,[],[f103,f140])).
% 75.78/10.98 tff(f5137,plain,(
% 75.78/10.98 sK3(f__integer__(sK16),f__integer__(sK17),f__integer__(sK18),f__integer__(sK19)) = sK15(f__integer__(sK16),f__integer__(sK17),f__integer__(sK18),f__integer__(sK19)) | ~spl20_2),
% 75.78/10.98 inference(resolution,[],[f89,f140])).
% 75.78/10.98 tff(f5251,plain,(
% 75.78/10.98 sK5(f__integer__(sK16),f__integer__(sK17),f__integer__(sK18),f__integer__(sK19)) = sK14(f__integer__(sK16),f__integer__(sK17),f__integer__(sK18),f__integer__(sK19)) | ~spl20_2),
% 75.78/10.98 inference(resolution,[],[f90,f140])).
% 75.78/10.98 tff(f5391,plain,(
% 75.78/10.98 f__integer__(sK17) = sK15(f__integer__(sK16),f__integer__(sK17),f__integer__(sK18),f__integer__(sK19)) | ~spl20_2),
% 75.78/10.98 inference(forward_demodulation,[],[f5137,f3178])).
% 75.78/10.98 tff(f5392,plain,(
% 75.78/10.98 f__integer__(sK19) = sK14(f__integer__(sK16),f__integer__(sK17),f__integer__(sK18),f__integer__(sK19)) | ~spl20_2),
% 75.78/10.98 inference(forward_demodulation,[],[f5251,f2258])).
% 75.78/10.98 tff(f6456,plain,(
% 75.78/10.98 ( ! [X0 : $int] : (~div(f__integer__(sK16),f__integer__(sK17),f__integer__(X0),f__integer__($sum(sK17,-1)))) )),
% 75.78/10.98 inference(resolution,[],[f131,f111])).
% 75.78/10.98 tff(f6478,plain,(
% 75.78/10.98 ( ! [X0 : $int] : (~div(f__integer__(sK16),f__integer__(sK17),f__integer__(X0),f__integer__($sum(-1,sK17)))) )),
% 75.78/10.98 inference(forward_demodulation,[],[f6456,f25])).
% 75.78/10.98 tff(f6674,plain,(
% 75.78/10.98 ( ! [X0 : $int,X1 : $int] : (~div(f__integer__(sK16),f__integer__(sK17),f__integer__(X0),f__integer__(X1)) | ~$less(X1,$sum(sK17,-1))) )),
% 75.78/10.98 inference(resolution,[],[f132,f111])).
% 75.78/10.98 tff(f7670,plain,(
% 75.78/10.98 ( ! [X0 : $int,X1 : $int] : (~div(f__integer__(sK16),f__integer__(sK17),f__integer__(X0),f__integer__(X1)) | ~$less(X1,$sum(-1,sK17))) )),
% 75.78/10.98 inference(forward_demodulation,[],[f6674,f25])).
% 75.78/10.98 tff(f7847,plain,(
% 75.78/10.98 p__less__(sK14(f__integer__(sK16),f__integer__(sK17),f__integer__(sK18),f__integer__(sK19)),f__integer__(sK17)) | ~div(f__integer__(sK16),f__integer__(sK17),f__integer__(sK18),f__integer__(sK19)) | ~spl20_2),
% 75.78/10.98 inference(superposition,[],[f88,f5391])).
% 75.78/10.98 tff(f7848,plain,(
% 75.78/10.98 p__less__(sK14(f__integer__(sK16),f__integer__(sK17),f__integer__(sK18),f__integer__(sK19)),f__integer__(sK17)) | ~spl20_2),
% 75.78/10.98 inference(forward_subsumption_resolution,[],[f7847,f140])).
% 75.78/10.98 tff(f7849,plain,(
% 75.78/10.98 p__less__(f__integer__(sK19),f__integer__(sK17)) | ~spl20_2),
% 75.78/10.98 inference(forward_demodulation,[],[f7848,f5392])).
% 75.78/10.98 tff(f7912,plain,(
% 75.78/10.98 p__less_equal__(f__integer__(sK19),f__integer__(sK17)) | ~spl20_2),
% 75.78/10.98 inference(resolution,[],[f7849,f83])).
% 75.78/10.98 tff(f7917,plain,(
% 75.78/10.98 ~p__less_equal__(f__integer__(sK17),f__integer__(sK19)) | f__integer__(sK17) = f__integer__(sK19) | ~spl20_2),
% 75.78/10.98 inference(resolution,[],[f7912,f79])).
% 75.78/10.98 tff(f7920,definition,(
% 75.78/10.98 spl20_74 <=> f__integer__(sK17) = f__integer__(sK19)),
% 75.78/10.98 introduced(definition,[new_symbols(definition,[spl20_74])],[avatar_definition])).
% 75.78/10.98 tff(f7922,plain,(
% 75.78/10.98 f__integer__(sK17) = f__integer__(sK19) | ~spl20_74),
% 75.78/10.98 inference(avatar_component_clause,[],[f7920])).
% 75.78/10.98 tff(f7924,definition,(
% 75.78/10.98 spl20_75 <=> p__less_equal__(f__integer__(sK17),f__integer__(sK19))),
% 75.78/10.98 introduced(definition,[new_symbols(definition,[spl20_75])],[avatar_definition])).
% 75.78/10.98 tff(f7926,plain,(
% 75.78/10.98 ~p__less_equal__(f__integer__(sK17),f__integer__(sK19)) | spl20_75),
% 75.78/10.98 inference(avatar_component_clause,[],[f7924])).
% 75.78/10.98 tff(f7928,plain,(
% 75.78/10.98 spl20_74 | ~spl20_75 | ~spl20_2),
% 75.78/10.98 inference(avatar_split_clause,[],[f7917,f138,f7924,f7920])).
% 75.78/10.98 tff(f7930,plain,(
% 75.78/10.98 ( ! [X0 : general] : (~p__less_equal__(f__integer__(sK17),X0) | ~p__less_equal__(X0,f__integer__(sK19))) ) | spl20_75),
% 75.78/10.98 inference(resolution,[],[f7926,f80])).
% 75.78/10.98 tff(f8229,plain,(
% 75.78/10.98 ( ! [X0 : $int] : (~p__less_equal__(f__integer__(X0),f__integer__(sK19)) | $less(X0,sK17)) ) | spl20_75),
% 75.78/10.98 inference(resolution,[],[f7930,f78])).
% 75.78/10.98 tff(f8235,plain,(
% 75.78/10.98 ( ! [X0 : $int] : ($less(sK19,X0) | $less(X0,sK17)) ) | spl20_75),
% 75.78/10.98 inference(resolution,[],[f8229,f78])).
% 75.78/10.98 tff(f8457,plain,(
% 75.78/10.98 ~$less(sK19,$sum(-1,sK17)) | ~spl20_2),
% 75.78/10.98 inference(resolution,[],[f7670,f140])).
% 75.78/10.98 tff(f8485,definition,(
% 75.78/10.98 spl20_97 <=> ! [X0 : $int] : ~div(f__integer__(sK16),f__integer__(sK17),f__integer__(X0),f__integer__(sK19))),
% 75.78/10.98 introduced(definition,[new_symbols(definition,[spl20_97])],[avatar_definition])).
% 75.78/10.98 tff(f8486,plain,(
% 75.78/10.98 ( ! [X0 : $int] : (~div(f__integer__(sK16),f__integer__(sK17),f__integer__(X0),f__integer__(sK19))) ) | ~spl20_97),
% 75.78/10.98 inference(avatar_component_clause,[],[f8485])).
% 75.78/10.98 tff(f8531,plain,(
% 75.78/10.98 $less($sum(-1,sK17),sK19) | sK19 = $sum(-1,sK17) | ~spl20_2),
% 75.78/10.98 inference(resolution,[],[f8457,f32])).
% 75.78/10.98 tff(f8546,definition,(
% 75.78/10.98 spl20_102 <=> sK19 = $sum(-1,sK17)),
% 75.78/10.98 introduced(definition,[new_symbols(definition,[spl20_102])],[avatar_definition])).
% 75.78/10.98 tff(f8548,plain,(
% 75.78/10.98 sK19 = $sum(-1,sK17) | ~spl20_102),
% 75.78/10.98 inference(avatar_component_clause,[],[f8546])).
% 75.78/10.98 tff(f8550,definition,(
% 75.78/10.98 spl20_103 <=> $less($sum(-1,sK17),sK19)),
% 75.78/10.98 introduced(definition,[new_symbols(definition,[spl20_103])],[avatar_definition])).
% 75.78/10.98 tff(f8552,plain,(
% 75.78/10.98 $less($sum(-1,sK17),sK19) | ~spl20_103),
% 75.78/10.98 inference(avatar_component_clause,[],[f8550])).
% 75.78/10.98 tff(f8553,plain,(
% 75.78/10.98 spl20_102 | spl20_103 | ~spl20_2),
% 75.78/10.98 inference(avatar_split_clause,[],[f8531,f138,f8550,f8546])).
% 75.78/10.98 tff(f8556,plain,(
% 75.78/10.98 ( ! [X0 : $int] : (~div(f__integer__(sK16),f__integer__(sK17),f__integer__(X0),f__integer__(sK19))) ) | ~spl20_102),
% 75.78/10.98 inference(superposition,[],[f6478,f8548])).
% 75.78/10.98 tff(f8562,plain,(
% 75.78/10.98 spl20_97 | ~spl20_102),
% 75.78/10.98 inference(avatar_split_clause,[],[f8556,f8546,f8485])).
% 75.78/10.98 tff(f8866,plain,(
% 75.78/10.98 ( ! [X0 : $int] : ($less($sum(1,X0),sK17) | ~$less(X0,sK19)) ) | spl20_75),
% 75.78/10.98 inference(resolution,[],[f8235,f175])).
% 75.78/10.98 tff(f10173,plain,(
% 75.78/10.98 ( ! [X0 : $int] : ($less(X0,sK17) | ~$less($sum($uminus(1),X0),sK19)) ) | spl20_75),
% 75.78/10.98 inference(superposition,[],[f8866,f1653])).
% 75.78/10.98 tff(f10177,plain,(
% 75.78/10.98 ( ! [X0 : $int] : (~$less($sum(-1,X0),sK19) | $less(X0,sK17)) ) | spl20_75),
% 75.78/10.98 inference(evaluation,[],[f10173])).
% 75.78/10.98 tff(f27377,plain,(
% 75.78/10.98 $less(sK17,sK17) | (spl20_75 | ~spl20_103)),
% 75.78/10.98 inference(resolution,[],[f10177,f8552])).
% 75.78/10.98 tff(f27411,plain,(
% 75.78/10.98 $false | (spl20_75 | ~spl20_103)),
% 75.78/10.98 inference(forward_subsumption_resolution,[],[f27377,f30])).
% 75.78/10.98 tff(f27412,plain,(
% 75.78/10.98 spl20_75 | ~spl20_103),
% 75.78/10.98 inference(avatar_contradiction_clause,[],[f27411])).
% 75.78/10.98 tff(f28354,plain,(
% 75.78/10.98 p__less__(f__integer__(sK17),f__integer__(sK17)) | (~spl20_2 | ~spl20_74)),
% 75.78/10.98 inference(superposition,[],[f7849,f7922])).
% 75.78/10.98 tff(f28617,plain,(
% 75.78/10.98 $false | (~spl20_2 | ~spl20_74)),
% 75.78/10.98 inference(forward_subsumption_resolution,[],[f28354,f115])).
% 75.78/10.98 tff(f28618,plain,(
% 75.78/10.98 ~spl20_2 | ~spl20_74),
% 75.78/10.98 inference(avatar_contradiction_clause,[],[f28617])).
% 75.78/10.98 tff(f36010,plain,(
% 75.78/10.98 $false | (~spl20_2 | ~spl20_97)),
% 75.78/10.98 inference(resolution,[],[f8486,f140])).
% 75.78/10.98 tff(f36017,plain,(
% 75.78/10.98 ~spl20_2 | ~spl20_97),
% 75.78/10.98 inference(avatar_contradiction_clause,[],[f36010])).
% 75.78/10.98 cnf(s1, plain, ~spl20_1 | spl20_2, inference(sat_conversion,[],[f141])).
% 75.78/10.98 cnf(s2, plain, spl20_1, inference(sat_conversion,[],[f142])).
% 75.78/10.98 cnf(s125, plain, ~spl20_2 | spl20_74 | ~spl20_75, inference(sat_conversion,[],[f7928])).
% 75.78/10.98 cnf(s163, plain, ~spl20_2 | spl20_102 | spl20_103, inference(sat_conversion,[],[f8553])).
% 75.78/10.98 cnf(s165, plain, spl20_97 | ~spl20_102, inference(sat_conversion,[],[f8562])).
% 75.78/10.98 cnf(s477, plain, spl20_75 | ~spl20_103, inference(sat_conversion,[],[f27412])).
% 75.78/10.98 cnf(s506, plain, ~spl20_2 | ~spl20_74, inference(sat_conversion,[],[f28618])).
% 75.78/10.98 cnf(s635, plain, ~spl20_2 | ~spl20_97, inference(sat_conversion,[],[f36017])).
% 75.78/10.98 cnf(s653, plain, spl20_2, inference(rat,[],[s1,s2])).
% 75.78/10.98 cnf(s654, plain, ~spl20_97, inference(rat,[],[s635,s653])).
% 75.78/10.98 cnf(s655, plain, ~spl20_74, inference(rat,[],[s506,s653])).
% 75.78/10.98 cnf(s662, plain, ~spl20_102, inference(rat,[],[s165,s654])).
% 75.78/10.98 cnf(s663, plain, ~spl20_75, inference(rat,[],[s125,s653,s655])).
% 75.78/10.98 cnf(s667, plain, spl20_103, inference(rat,[],[s163,s653,s662])).
% 75.78/10.98 cnf(s668, plain, $false, inference(rat,[],[s477,s667,s663])).
% 75.78/10.98 tff(f36018,plain,(
% 75.78/10.98 $false),
% 75.78/10.98 inference(avatar_sat_refutation,[],[s668])).
% 75.78/10.98 % SZS output end Proof for theBenchmark
% 75.78/10.98 % (3914987)------------------------------
% 75.78/10.98 % (3914987)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 75.78/10.98 % (3914987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.78/10.98 % (3914987)CaDiCaL version: 2.1.3
% 75.78/10.98 % (3914987)Termination reason: Refutation
% 75.78/10.98 % (3914987)Time elapsed: 2.356 s
% 75.78/10.98 % (3914987)Peak memory usage: 25 MB
% 75.78/10.98 % (3914987)Instructions burned: 2223 (million)
% 75.78/10.98 % (3914572)Success in time 10.761 s
% 75.78/10.98 % Vampire exiting
%------------------------------------------------------------------------------