%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ARI729_1 : TPTP v9.3.1. Released v6.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:35:09 AM UTC 2026
% Result : Theorem 8.46s 1.84s
% Output : Refutation 8.46s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : ARI729_1 : TPTP v9.3.1. Released v6.3.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.26 % Computer : n001.cluster.edu
% 0.12/0.26 % Model : x86_64 x86_64
% 0.12/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.26 % Memory : 8046.5625MB
% 0.12/0.26 % OS : Linux 6.8.0-71-generic
% 0.12/0.26 % CPULimit : 300
% 0.12/0.26 % WCLimit : 300
% 0.12/0.26 % DateTime : Mon Sep 28 21:07:34 UTC 2026
% 0.12/0.27 % CPUTime :
% 0.12/0.27 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.27/0.31 Running first-order model finding
% 0.27/0.31 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.92/1.18 % (745144)Will run a generic schedule for satisfiability detection.
% 5.92/1.18 % (745149)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3427321374_3000 on theBenchmark for (3000ds/0Mi)
% 5.92/1.18 % (745149)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 5.92/1.18 % (745149)Terminated due to inappropriate strategy.
% 5.92/1.18 % (745149)------------------------------
% 5.92/1.18 % (745149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.92/1.18 % (745149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.92/1.18 % (745149)CaDiCaL version: 2.1.3
% 5.92/1.18 % (745149)Termination reason: Inappropriate
% 5.92/1.18 % (745149)Time elapsed: 0.0000 s
% 5.92/1.18 % (745149)Peak memory usage: 10 MB
% 5.92/1.18 % (745149)------------------------------
% 5.92/1.18 % (745149)------------------------------
% 5.92/1.18 % (745152)dis+10_1_sil=32000:sp=arity:random_seed=3278203393:i=103:fgj=on_3000 on theBenchmark for (3000ds/103Mi)
% 5.92/1.18 % (745150)% WARNING: option uhcvi not known.
% 5.92/1.18 % (745151)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=300925968:i=88024:add=on:rawr=on_3000 on theBenchmark for (3000ds/88024Mi)
% 5.92/1.18 % (745150)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2752697229:i=135531:add=off:rawr=on_3000 on theBenchmark for (3000ds/135531Mi)
% 5.92/1.18 % (745153)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3644482735:i=116_3000 on theBenchmark for (3000ds/116Mi)
% 5.92/1.18 % (745154)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2478149003:i=131_3000 on theBenchmark for (3000ds/131Mi)
% 5.92/1.18 % (745155)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=941686296:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_3000 on theBenchmark for (3000ds/159Mi)
% 5.92/1.18 % (745157)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3631620723:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 5.92/1.18 % (745157)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 5.92/1.18 % (745157)Terminated due to inappropriate strategy.
% 5.92/1.18 % (745157)------------------------------
% 5.92/1.18 % (745157)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.92/1.18 % (745157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.92/1.18 % (745157)CaDiCaL version: 2.1.3
% 5.92/1.18 % (745157)Termination reason: Inappropriate
% 5.92/1.18 % (745157)Time elapsed: 0.001 s
% 5.92/1.18 % (745157)Peak memory usage: 10 MB
% 5.92/1.18 % (745157)------------------------------
% 5.92/1.18 % (745157)------------------------------
% 5.92/1.18 % (745165)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1924317335:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 5.92/1.18 % (745152)Instruction limit reached!
% 5.92/1.18 % (745152)------------------------------
% 5.92/1.18 % (745152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.92/1.18 % (745152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.92/1.18 % (745152)CaDiCaL version: 2.1.3
% 5.92/1.18 % (745152)Termination reason: Instruction limit
% 5.92/1.18 % (745152)Termination phase: Saturation
% 5.92/1.18 % (745152)Time elapsed: 0.108 s
% 5.92/1.18 % (745152)Peak memory usage: 12 MB
% 5.92/1.18 % (745152)Instructions burned: 103 (million)
% 5.92/1.18 % (745153)Instruction limit reached!
% 5.92/1.18 % (745153)------------------------------
% 5.92/1.18 % (745153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.92/1.18 % (745153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.92/1.18 % (745153)CaDiCaL version: 2.1.3
% 5.92/1.18 % (745153)Termination reason: Instruction limit
% 5.92/1.18 % (745153)Termination phase: Saturation
% 5.92/1.18 % (745153)Time elapsed: 0.114 s
% 5.92/1.18 % (745153)Peak memory usage: 12 MB
% 5.92/1.18 % (745153)Instructions burned: 116 (million)
% 5.92/1.18 % (745155)Instruction limit reached!
% 5.92/1.18 % (745155)------------------------------
% 5.92/1.18 % (745155)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.92/1.18 % (745155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.92/1.18 % (745155)CaDiCaL version: 2.1.3
% 5.92/1.18 % (745155)Termination reason: Instruction limit
% 5.92/1.18 % (745155)Termination phase: Saturation
% 5.92/1.18 % (745155)Time elapsed: 0.110 s
% 5.92/1.18 % (745155)Peak memory usage: 13 MB
% 5.92/1.18 % (745155)Instructions burned: 160 (million)
% 7.56/1.69 % (745154)Instruction limit reached!
% 7.56/1.69 % (745154)------------------------------
% 7.56/1.69 % (745154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.56/1.69 % (745154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.56/1.69 % (745154)CaDiCaL version: 2.1.3
% 7.56/1.69 % (745154)Termination reason: Instruction limit
% 7.56/1.69 % (745154)Termination phase: Saturation
% 7.56/1.69 % (745154)Time elapsed: 0.130 s
% 7.56/1.69 % (745154)Peak memory usage: 12 MB
% 7.56/1.69 % (745154)Instructions burned: 131 (million)
% 7.56/1.69 % (745167)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=1645641183:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 7.56/1.69 % (745169)ott-21_1_sil=16000:fs=off:random_seed=291888955:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 7.56/1.69 % (745171)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3577854884:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 7.56/1.69 % (745170)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2528998280:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 7.56/1.69 % (745171)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.56/1.69 % (745171)Terminated due to inappropriate strategy.
% 7.56/1.69 % (745171)------------------------------
% 7.56/1.69 % (745171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.56/1.69 % (745171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.56/1.69 % (745171)CaDiCaL version: 2.1.3
% 7.56/1.69 % (745171)Termination reason: Inappropriate
% 7.56/1.69 % (745171)Time elapsed: 0.0000 s
% 7.56/1.69 % (745171)Peak memory usage: 10 MB
% 7.56/1.69 % (745171)------------------------------
% 7.56/1.69 % (745171)------------------------------
% 7.56/1.69 % (745178)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=307263385:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 7.56/1.69 % (745165)Instruction limit reached!
% 7.56/1.69 % (745165)------------------------------
% 7.56/1.69 % (745165)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.56/1.69 % (745165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.56/1.69 % (745165)CaDiCaL version: 2.1.3
% 7.56/1.69 % (745165)Termination reason: Instruction limit
% 7.56/1.69 % (745165)Termination phase: Saturation
% 7.56/1.69 % (745165)Time elapsed: 0.137 s
% 7.56/1.69 % (745165)Peak memory usage: 13 MB
% 7.56/1.69 % (745165)Instructions burned: 131 (million)
% 7.56/1.69 % (745182)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2965846164:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 7.56/1.69 % (745182)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.56/1.69 % (745182)Terminated due to inappropriate strategy.
% 7.56/1.69 % (745182)------------------------------
% 7.56/1.69 % (745182)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.56/1.69 % (745182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.56/1.69 % (745182)CaDiCaL version: 2.1.3
% 7.56/1.69 % (745182)Termination reason: Inappropriate
% 7.56/1.69 % (745182)Time elapsed: 0.001 s
% 7.56/1.69 % (745182)Peak memory usage: 11 MB
% 7.56/1.69 % (745182)------------------------------
% 7.56/1.69 % (745182)------------------------------
% 7.56/1.69 % (745185)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=1080709039: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.56/1.69 % (745169)Instruction limit reached!
% 7.56/1.69 % (745169)------------------------------
% 7.56/1.69 % (745169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.56/1.69 % (745169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.56/1.69 % (745169)CaDiCaL version: 2.1.3
% 7.56/1.69 % (745169)Termination reason: Instruction limit
% 7.56/1.69 % (745169)Termination phase: Saturation
% 7.56/1.69 % (745169)Time elapsed: 0.147 s
% 7.56/1.69 % (745169)Peak memory usage: 12 MB
% 7.56/1.69 % (745169)Instructions burned: 181 (million)
% 7.56/1.69 % (745187)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=473159346:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi)
% 8.46/1.84 % (745170)Instruction limit reached!
% 8.46/1.84 % (745170)------------------------------
% 8.46/1.84 % (745170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.46/1.84 % (745170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.46/1.84 % (745170)CaDiCaL version: 2.1.3
% 8.46/1.84 % (745170)Termination reason: Instruction limit
% 8.46/1.84 % (745170)Termination phase: Saturation
% 8.46/1.84 % (745170)Time elapsed: 0.501 s
% 8.46/1.84 % (745170)Peak memory usage: 14 MB
% 8.46/1.84 % (745170)Instructions burned: 478 (million)
% 8.46/1.84 % (745195)fmb+10_1_sil=64000:random_seed=864811265:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 8.46/1.84 % (745195)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 8.46/1.84 % (745195)Terminated due to inappropriate strategy.
% 8.46/1.84 % (745195)------------------------------
% 8.46/1.84 % (745195)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.46/1.84 % (745195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.46/1.84 % (745195)CaDiCaL version: 2.1.3
% 8.46/1.84 % (745195)Termination reason: Inappropriate
% 8.46/1.84 % (745195)Time elapsed: 0.001 s
% 8.46/1.84 % (745195)Peak memory usage: 10 MB
% 8.46/1.84 % (745195)------------------------------
% 8.46/1.84 % (745195)------------------------------
% 8.46/1.84 % (745197)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4049434957:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi)
% 8.46/1.84 % (745197)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 8.46/1.84 % (745197)Terminated due to inappropriate strategy.
% 8.46/1.84 % (745197)------------------------------
% 8.46/1.84 % (745197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.46/1.84 % (745197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.46/1.84 % (745197)CaDiCaL version: 2.1.3
% 8.46/1.84 % (745197)Termination reason: Inappropriate
% 8.46/1.84 % (745197)Time elapsed: 0.0000 s
% 8.46/1.84 % (745197)Peak memory usage: 10 MB
% 8.46/1.84 % (745197)------------------------------
% 8.46/1.84 % (745197)------------------------------
% 8.46/1.84 % (745199)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3589624708:fmbsr=1.7:i=920_2992 on theBenchmark for (2992ds/920Mi)
% 8.46/1.84 % (745199)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 8.46/1.84 % (745199)Terminated due to inappropriate strategy.
% 8.46/1.84 % (745199)------------------------------
% 8.46/1.84 % (745199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.46/1.84 % (745199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.46/1.84 % (745199)CaDiCaL version: 2.1.3
% 8.46/1.84 % (745199)Termination reason: Inappropriate
% 8.46/1.84 % (745199)Time elapsed: 0.0000 s
% 8.46/1.84 % (745199)Peak memory usage: 10 MB
% 8.46/1.84 % (745199)------------------------------
% 8.46/1.84 % (745199)------------------------------
% 8.46/1.84 % (745201)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1476380266:i=5131_2992 on theBenchmark for (2992ds/5131Mi)
% 8.46/1.84 % (745167)Instruction limit reached!
% 8.46/1.84 % (745167)------------------------------
% 8.46/1.84 % (745167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.46/1.84 % (745167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.46/1.84 % (745167)CaDiCaL version: 2.1.3
% 8.46/1.84 % (745167)Termination reason: Instruction limit
% 8.46/1.84 % (745167)Termination phase: Saturation
% 8.46/1.84 % (745167)Time elapsed: 0.663 s
% 8.46/1.84 % (745167)Peak memory usage: 16 MB
% 8.46/1.84 % (745167)Instructions burned: 684 (million)
% 8.46/1.84 % (745178)Instruction limit reached!
% 8.46/1.84 % (745178)------------------------------
% 8.46/1.84 % (745178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.46/1.84 % (745178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.46/1.84 % (745178)CaDiCaL version: 2.1.3
% 8.46/1.84 % (745178)Termination reason: Instruction limit
% 8.46/1.84 % (745178)Termination phase: Saturation
% 8.46/1.84 % (745178)Time elapsed: 0.635 s
% 8.46/1.84 % (745178)Peak memory usage: 17 MB
% 8.46/1.84 % (745178)Instructions burned: 1180 (million)
% 8.46/1.84 % (745204)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1453434544:i=6324_2991 on theBenchmark for (2991ds/6324Mi)
% 8.46/1.84 % (745204)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 8.46/1.84 % (745204)Terminated due to inappropriate strategy.
% 8.46/1.84 % (745204)------------------------------
% 8.46/1.84 % (745204)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.46/1.84 % (745204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.46/1.84 % (745204)CaDiCaL version: 2.1.3
% 8.46/1.84 % (745204)Termination reason: Inappropriate
% 8.46/1.84 % (745204)Time elapsed: 0.0000 s
% 8.46/1.84 % (745204)Peak memory usage: 10 MB
% 8.46/1.84 % (745204)------------------------------
% 8.46/1.84 % (745204)------------------------------
% 8.46/1.84 % (745203)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3605790481:i=1472:ins=7:fdi=8:gsp=on_2991 on theBenchmark for (2991ds/1472Mi)
% 8.46/1.84 % (745206)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2025084229:fmbsr=2.30978:i=2174_2991 on theBenchmark for (2991ds/2174Mi)
% 8.46/1.84 % (745206)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 8.46/1.84 % (745206)Terminated due to inappropriate strategy.
% 8.46/1.84 % (745206)------------------------------
% 8.46/1.84 % (745206)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.46/1.84 % (745206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.46/1.84 % (745206)CaDiCaL version: 2.1.3
% 8.46/1.84 % (745206)Termination reason: Inappropriate
% 8.46/1.84 % (745206)Time elapsed: 0.0000 s
% 8.46/1.84 % (745206)Peak memory usage: 10 MB
% 8.46/1.84 % (745206)------------------------------
% 8.46/1.84 % (745206)------------------------------
% 8.46/1.84 % (745209)ott-2_1_sil=16000:newcnf=on:random_seed=1326203933:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2991 on theBenchmark for (2991ds/869Mi)
% 8.46/1.84 % (745185)Instruction limit reached!
% 8.46/1.84 % (745185)------------------------------
% 8.46/1.84 % (745185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.46/1.84 % (745185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.46/1.84 % (745185)CaDiCaL version: 2.1.3
% 8.46/1.84 % (745185)Termination reason: Instruction limit
% 8.46/1.84 % (745185)Termination phase: Saturation
% 8.46/1.84 % (745185)Time elapsed: 0.673 s
% 8.46/1.84 % (745185)Peak memory usage: 18 MB
% 8.46/1.84 % (745185)Instructions burned: 692 (million)
% 8.46/1.84 % (745211)ott+10_1_sil=32000:tgt=ground:random_seed=2304157187:i=5114:av=off_2990 on theBenchmark for (2990ds/5114Mi)
% 8.46/1.84 % (745187)Instruction limit reached!
% 8.46/1.84 % (745187)------------------------------
% 8.46/1.84 % (745187)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.46/1.84 % (745187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.46/1.84 % (745187)CaDiCaL version: 2.1.3
% 8.46/1.84 % (745187)Termination reason: Instruction limit
% 8.46/1.84 % (745187)Termination phase: Saturation
% 8.46/1.84 % (745187)Time elapsed: 0.847 s
% 8.46/1.84 % (745187)Peak memory usage: 18 MB
% 8.46/1.84 % (745187)Instructions burned: 879 (million)
% 8.46/1.84 % (745215)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=530720781:i=54282_2987 on theBenchmark for (2987ds/54282Mi)
% 8.46/1.84 % (745215)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 8.46/1.84 % (745215)Terminated due to inappropriate strategy.
% 8.46/1.84 % (745215)------------------------------
% 8.46/1.84 % (745215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.46/1.84 % (745215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.46/1.84 % (745215)CaDiCaL version: 2.1.3
% 8.46/1.84 % (745215)Termination reason: Inappropriate
% 8.46/1.84 % (745215)Time elapsed: 0.0000 s
% 8.46/1.84 % (745215)Peak memory usage: 11 MB
% 8.46/1.84 % (745215)------------------------------
% 8.46/1.84 % (745215)------------------------------
% 8.46/1.84 % (745217)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=614425287:i=3512:aac=none_2987 on theBenchmark for (2987ds/3512Mi)
% 8.46/1.84 % (745209)Instruction limit reached!
% 8.46/1.84 % (745209)------------------------------
% 8.46/1.84 % (745209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.46/1.84 % (745209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.46/1.84 % (745209)CaDiCaL version: 2.1.3
% 8.46/1.84 % (745209)Termination reason: Instruction limit
% 8.46/1.84 % (745209)Termination phase: Saturation
% 8.46/1.84 % (745209)Time elapsed: 0.463 s
% 8.46/1.84 % (745209)Peak memory usage: 16 MB
% 8.46/1.84 % (745209)Instructions burned: 871 (million)
% 8.46/1.84 % (745221)dis+21_1_sil=32000:sas=cadical:random_seed=1993943685:i=3773:amm=off_2986 on theBenchmark for (2986ds/3773Mi)
% 8.46/1.84 % (745150) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-745144-745150"...
% 8.46/1.84 % (745150)...printing done.
% 8.46/1.84 % (745150)Refutation found. Thanks to Tanya!
% 8.46/1.84 % SZS status Theorem for theBenchmark
% 8.46/1.84 % SZS output start Proof for theBenchmark
% 8.46/1.84 tff(func_def_6, type, sK0: $real).
% 8.46/1.84 tff(func_def_7, type, sK1: $real).
% 8.46/1.84 tff(f1,conjecture,(
% 8.46/1.84 ! [X0 : $real,X1 : $real] : ($floor(X0) = $floor(X1) => $less($difference(X0,X1),1/1))),
% 8.46/1.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove)).
% 8.46/1.84 tff(f2,negated_conjecture,(
% 8.46/1.84 ~ ! [X0 : $real,X1 : $real] : ($floor(X0) = $floor(X1) => $less($difference(X0,X1),1/1))),
% 8.46/1.84 inference(negated_conjecture,[status(cth)],[f1])).
% 8.46/1.84 tff(f3,plain,(
% 8.46/1.84 ~ ! [X0 : $real,X1 : $real] : ($floor(X0) = $floor(X1) => $less($sum(X0,$uminus(X1)),1/1))),
% 8.46/1.84 inference(theory_normalization,[],[f2])).
% 8.46/1.84 tff(f4,definition,(
% 8.46/1.84 ( ! [X0 : $real,X1 : $real] : ($sum(X0,X1) = $sum(X1,X0)) )),
% 8.46/1.84 introduced(theory,[tha_commutativity])).
% 8.46/1.84 tff(f5,definition,(
% 8.46/1.84 ( ! [X2 : $real,X0 : $real,X1 : $real] : ($sum(X0,$sum(X1,X2)) = $sum($sum(X0,X1),X2)) )),
% 8.46/1.84 introduced(theory,[tha_associativity])).
% 8.46/1.84 tff(f8,definition,(
% 8.46/1.84 ( ! [X0 : $real] : (0/1 = $sum(X0,$uminus(X0))) )),
% 8.46/1.84 introduced(theory,[tha_inverse_op_unit])).
% 8.46/1.84 tff(f10,definition,(
% 8.46/1.84 ( ! [X2 : $real,X0 : $real,X1 : $real] : (~$less(X1,X2) | ~$less(X0,X1) | $less(X0,X2)) )),
% 8.46/1.84 introduced(theory,[tha_transitivity])).
% 8.46/1.84 tff(f11,definition,(
% 8.46/1.84 ( ! [X0 : $real,X1 : $real] : ($less(X1,X0) | $less(X0,X1) | X0 = X1) )),
% 8.46/1.84 introduced(theory,[tha_order_totality])).
% 8.46/1.84 tff(f12,definition,(
% 8.46/1.84 ( ! [X2 : $real,X0 : $real,X1 : $real] : ($less($sum(X0,X2),$sum(X1,X2)) | ~$less(X0,X1)) )),
% 8.46/1.84 introduced(theory,[tha_order_monotonicity])).
% 8.46/1.84 tff(f14,definition,(
% 8.46/1.84 ( ! [X0 : $real] : ($uminus($uminus(X0)) = X0) )),
% 8.46/1.84 introduced(theory,[tha_minus_minus_x])).
% 8.46/1.84 tff(f15,definition,(
% 8.46/1.84 ( ! [X0 : $real] : (~$less(X0,$floor(X0))) )),
% 8.46/1.84 introduced(theory,[tha_floor_small])).
% 8.46/1.84 tff(f16,definition,(
% 8.46/1.84 ( ! [X0 : $real] : ($less($sum(X0,$uminus(1/1)),$floor(X0))) )),
% 8.46/1.84 introduced(theory,[tha_floor_big])).
% 8.46/1.84 tff(f17,plain,(
% 8.46/1.84 ? [X0 : $real,X1 : $real] : (~$less($sum(X0,$uminus(X1)),1/1) & $floor(X0) = $floor(X1))),
% 8.46/1.84 inference(ennf_transformation,[],[f3])).
% 8.46/1.84 tff(f18,plain,(
% 8.46/1.84 $floor(sK0) = $floor(sK1)),
% 8.46/1.84 inference(cnf_transformation,[],[f17])).
% 8.46/1.84 tff(f19,plain,(
% 8.46/1.84 ~$less($sum(sK0,$uminus(sK1)),1/1)),
% 8.46/1.84 inference(cnf_transformation,[],[f17])).
% 8.46/1.84 tff(f20,plain,(
% 8.46/1.84 ~$less(sK1,$floor(sK0))),
% 8.46/1.84 inference(superposition,[],[f15,f18])).
% 8.46/1.84 tff(f21,plain,(
% 8.46/1.84 ( ! [X0 : $real] : (0/1 = $sum($uminus(X0),X0)) )),
% 8.46/1.84 inference(superposition,[],[f8,f14])).
% 8.46/1.84 tff(f35,plain,(
% 8.46/1.84 ( ! [X0 : $real] : ($less($sum($uminus(1/1),X0),$floor(X0))) )),
% 8.46/1.84 inference(superposition,[],[f16,f4])).
% 8.46/1.84 tff(f39,plain,(
% 8.46/1.84 ( ! [X0 : $real] : ($less($sum(-1/1,X0),$floor(X0))) )),
% 8.46/1.84 inference(evaluation,[],[f35])).
% 8.46/1.84 tff(f51,plain,(
% 8.46/1.84 $less(1/1,$sum(sK0,$uminus(sK1))) | 1/1 = $sum(sK0,$uminus(sK1))),
% 8.46/1.84 inference(resolution,[],[f11,f19])).
% 8.46/1.84 tff(f57,definition,(
% 8.46/1.84 spl2_1 <=> 1/1 = $sum(sK0,$uminus(sK1))),
% 8.46/1.84 introduced(definition,[new_symbols(definition,[spl2_1])],[avatar_definition])).
% 8.46/1.84 tff(f59,plain,(
% 8.46/1.84 1/1 = $sum(sK0,$uminus(sK1)) | ~spl2_1),
% 8.46/1.84 inference(avatar_component_clause,[],[f57])).
% 8.46/1.84 tff(f61,definition,(
% 8.46/1.84 spl2_2 <=> $less(1/1,$sum(sK0,$uminus(sK1)))),
% 8.46/1.84 introduced(definition,[new_symbols(definition,[spl2_2])],[avatar_definition])).
% 8.46/1.84 tff(f63,plain,(
% 8.46/1.84 $less(1/1,$sum(sK0,$uminus(sK1))) | ~spl2_2),
% 8.46/1.84 inference(avatar_component_clause,[],[f61])).
% 8.46/1.84 tff(f65,plain,(
% 8.46/1.84 spl2_1 | spl2_2),
% 8.46/1.84 inference(avatar_split_clause,[],[f51,f61,f57])).
% 8.46/1.84 tff(f85,plain,(
% 8.46/1.84 ( ! [X2 : $real,X3 : $real,X0 : $real,X1 : $real] : (~$less(X0,X1) | ~$less(X2,$sum(X0,X3)) | $less(X2,$sum(X1,X3))) )),
% 8.46/1.84 inference(resolution,[],[f12,f10])).
% 8.46/1.84 tff(f93,plain,(
% 8.46/1.84 ( ! [X0 : $real,X1 : $real] : ($less($sum(X0,$uminus(X1)),0/1) | ~$less(X0,X1)) )),
% 8.46/1.84 inference(superposition,[],[f12,f8])).
% 8.46/1.84 tff(f94,plain,(
% 8.46/1.84 ( ! [X2 : $real,X0 : $real,X1 : $real] : (~$less(X2,X1) | $less($sum(X2,X0),$sum(X0,X1))) )),
% 8.46/1.84 inference(superposition,[],[f12,f4])).
% 8.46/1.84 tff(f101,plain,(
% 8.46/1.84 ( ! [X0 : $real,X1 : $real] : ($sum(0/1,X1) = $sum(X0,$sum($uminus(X0),X1))) )),
% 8.46/1.84 inference(superposition,[],[f5,f8])).
% 8.46/1.84 tff(f117,plain,(
% 8.46/1.84 ( ! [X0 : $real,X1 : $real] : ($less($sum(X0,$sum(X1,$uminus(1/1))),$floor($sum(X0,X1)))) )),
% 8.46/1.84 inference(superposition,[],[f16,f5])).
% 8.46/1.84 tff(f119,plain,(
% 8.46/1.84 ( ! [X0 : $real,X1 : $real] : ($less($sum(X0,$sum(X1,-1/1)),$floor($sum(X0,X1)))) )),
% 8.46/1.84 inference(evaluation,[],[f117])).
% 8.46/1.84 tff(f121,plain,(
% 8.46/1.84 ( ! [X0 : $real,X1 : $real] : ($sum(X0,$sum($uminus(X0),X1)) = X1) )),
% 8.46/1.84 inference(evaluation,[],[f101])).
% 8.46/1.84 tff(f158,plain,(
% 8.46/1.84 ( ! [X0 : $real,X1 : $real] : ($sum(X1,$sum(X0,$uminus(X1))) = X0) )),
% 8.46/1.84 inference(superposition,[],[f121,f4])).
% 8.46/1.84 tff(f195,plain,(
% 8.46/1.84 ( ! [X2 : $real,X0 : $real,X1 : $real] : (~$less(X2,$sum(X0,$uminus(X1))) | ~$less(X0,X1) | $less(X2,0/1)) )),
% 8.46/1.84 inference(resolution,[],[f93,f10])).
% 8.46/1.84 tff(f348,plain,(
% 8.46/1.84 ( ! [X0 : $real] : ($less($sum(1/1,X0),$sum(X0,$sum(sK0,$uminus(sK1))))) ) | ~spl2_2),
% 8.46/1.84 inference(resolution,[],[f94,f63])).
% 8.46/1.84 tff(f480,plain,(
% 8.46/1.84 ( ! [X0 : $real] : ($less($sum(X0,0/1),$floor($sum(X0,$uminus(-1/1))))) )),
% 8.46/1.84 inference(superposition,[],[f119,f21])).
% 8.46/1.84 tff(f501,plain,(
% 8.46/1.84 ( ! [X0 : $real] : ($less(X0,$floor($sum(X0,1/1)))) )),
% 8.46/1.84 inference(evaluation,[],[f480])).
% 8.46/1.84 tff(f766,plain,(
% 8.46/1.84 ( ! [X2 : $real,X0 : $real,X1 : $real] : (~$less(X0,$sum($sum(-1/1,X1),X2)) | $less(X0,$sum($floor(X1),X2))) )),
% 8.46/1.84 inference(resolution,[],[f85,f39])).
% 8.46/1.84 tff(f789,plain,(
% 8.46/1.84 ( ! [X2 : $real,X0 : $real,X1 : $real] : (~$less(X0,$sum(-1/1,$sum(X1,X2))) | $less(X0,$sum($floor(X1),X2))) )),
% 8.46/1.84 inference(forward_demodulation,[],[f766,f5])).
% 8.46/1.84 tff(f16013,plain,(
% 8.46/1.84 $less($sum(1/1,-1/1),$sum($floor(sK0),$uminus(sK1))) | ~spl2_2),
% 8.46/1.84 inference(resolution,[],[f789,f348])).
% 8.46/1.84 tff(f16090,plain,(
% 8.46/1.84 $less(0/1,$sum($floor(sK0),$uminus(sK1))) | ~spl2_2),
% 8.46/1.84 inference(evaluation,[],[f16013])).
% 8.46/1.84 tff(f25119,plain,(
% 8.46/1.84 ~$less($floor(sK0),sK1) | $less(0/1,0/1) | ~spl2_2),
% 8.46/1.84 inference(resolution,[],[f16090,f195])).
% 8.46/1.84 tff(f25136,plain,(
% 8.46/1.84 ~$less($floor(sK0),sK1) | ~spl2_2),
% 8.46/1.84 inference(evaluation,[],[f25119])).
% 8.46/1.84 tff(f25144,plain,(
% 8.46/1.84 $less(sK1,$floor(sK0)) | sK1 = $floor(sK0) | ~spl2_2),
% 8.46/1.84 inference(resolution,[],[f25136,f11])).
% 8.46/1.84 tff(f25145,plain,(
% 8.46/1.84 sK1 = $floor(sK0) | ~spl2_2),
% 8.46/1.84 inference(forward_subsumption_resolution,[],[f25144,f20])).
% 8.46/1.84 tff(f25379,plain,(
% 8.46/1.84 $less(0/1,$sum(sK1,$uminus(sK1))) | ~spl2_2),
% 8.46/1.84 inference(superposition,[],[f16090,f25145])).
% 8.46/1.84 tff(f25400,plain,(
% 8.46/1.84 $less(0/1,0/1) | ~spl2_2),
% 8.46/1.84 inference(forward_demodulation,[],[f25379,f8])).
% 8.46/1.84 tff(f25401,plain,(
% 8.46/1.84 $false | ~spl2_2),
% 8.46/1.84 inference(evaluation,[],[f25400])).
% 8.46/1.84 tff(f25402,plain,(
% 8.46/1.84 ~spl2_2),
% 8.46/1.84 inference(avatar_contradiction_clause,[],[f25401])).
% 8.46/1.84 tff(f25421,plain,(
% 8.46/1.84 sK0 = $sum(sK1,1/1) | ~spl2_1),
% 8.46/1.84 inference(superposition,[],[f158,f59])).
% 8.46/1.84 tff(f35113,plain,(
% 8.46/1.84 $less(sK1,$floor(sK0)) | ~spl2_1),
% 8.46/1.84 inference(superposition,[],[f501,f25421])).
% 8.46/1.84 tff(f35248,plain,(
% 8.46/1.84 $false | ~spl2_1),
% 8.46/1.84 inference(forward_subsumption_resolution,[],[f35113,f20])).
% 8.46/1.84 tff(f35249,plain,(
% 8.46/1.84 ~spl2_1),
% 8.46/1.84 inference(avatar_contradiction_clause,[],[f35248])).
% 8.46/1.84 cnf(s2, plain, spl2_1 | spl2_2, inference(sat_conversion,[],[f65])).
% 8.46/1.84 cnf(s19, plain, ~spl2_2, inference(sat_conversion,[],[f25402])).
% 8.46/1.84 cnf(s48, plain, ~spl2_1, inference(sat_conversion,[],[f35249])).
% 8.46/1.84 cnf(s52, plain, $false, inference(rat,[],[s2,s19,s48])).
% 8.46/1.84 tff(f35257,plain,(
% 8.46/1.84 $false),
% 8.46/1.84 inference(avatar_sat_refutation,[],[s52])).
% 8.46/1.84 % SZS output end Proof for theBenchmark
% 8.46/1.84 % (745150)------------------------------
% 8.46/1.84 % (745150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.46/1.84 % (745150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.46/1.84 % (745150)CaDiCaL version: 2.1.3
% 8.46/1.84 % (745150)Termination reason: Refutation
% 8.46/1.84 % (745150)Time elapsed: 1.472 s
% 8.46/1.84 % (745150)Peak memory usage: 24 MB
% 8.46/1.84 % (745150)Instructions burned: 1571 (million)
% 8.46/1.84 % (745144)Success in time 1.514 s
% 8.46/1.84 % Vampire exiting
%------------------------------------------------------------------------------