%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : TIM009_1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n016.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 02:33:35 PM UTC 2026
% Result : Theorem 5.58s 1.06s
% Output : Refutation 5.58s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TIM009_1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.19 % Computer : n016.cluster.edu
% 0.11/0.19 % Model : x86_64 x86_64
% 0.11/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.19 % Memory : 8046.5625MB
% 0.11/0.19 % OS : Linux 6.8.0-71-generic
% 0.11/0.19 % CPULimit : 300
% 0.11/0.19 % WCLimit : 300
% 0.11/0.19 % DateTime : Mon Sep 28 18:52:18 UTC 2026
% 0.11/0.20 % CPUTime :
% 0.11/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.23 Running first-order model finding
% 0.11/0.23 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.86/0.76 % (3880140)Will run a generic schedule for satisfiability detection.
% 2.86/0.76 % (3880157)dis+10_1_sil=32000:sp=arity:random_seed=3511888032:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 2.86/0.76 % (3880155)% WARNING: option uhcvi not known.
% 2.86/0.76 % (3880154)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3824449494_2999 on theBenchmark for (2999ds/0Mi)
% 2.86/0.76 % (3880158)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4113991696:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 2.86/0.76 % (3880155)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2764355313:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 2.86/0.76 % (3880159)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=64993849:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 2.86/0.76 % (3880156)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2740656372:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 2.86/0.76 % (3880161)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2390938396:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 2.86/0.76 % (3880154)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 2.86/0.76 % (3880154)Terminated due to inappropriate strategy.
% 2.86/0.76 % (3880154)------------------------------
% 2.86/0.76 % (3880154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.76 % (3880154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.76 % (3880154)CaDiCaL version: 2.1.3
% 2.86/0.76 % (3880154)Termination reason: Inappropriate
% 2.86/0.76 % (3880154)Time elapsed: 0.005 s
% 2.86/0.76 % (3880154)Peak memory usage: 10 MB
% 2.86/0.76 % (3880154)Instructions burned: 8 (million)
% 2.86/0.76 % (3880154)------------------------------
% 2.86/0.76 % (3880154)------------------------------
% 2.86/0.76 % (3880186)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3150364534:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 2.86/0.76 % (3880157)Instruction limit reached!
% 2.86/0.76 % (3880157)------------------------------
% 2.86/0.76 % (3880157)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.76 % (3880157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.76 % (3880157)CaDiCaL version: 2.1.3
% 2.86/0.76 % (3880157)Termination reason: Instruction limit
% 2.86/0.76 % (3880157)Termination phase: Saturation
% 2.86/0.76 % (3880157)Time elapsed: 0.036 s
% 2.86/0.76 % (3880157)Peak memory usage: 13 MB
% 2.86/0.76 % (3880157)Instructions burned: 105 (million)
% 2.86/0.76 % (3880186)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 2.86/0.76 % (3880186)Terminated due to inappropriate strategy.
% 2.86/0.76 % (3880186)------------------------------
% 2.86/0.76 % (3880186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.76 % (3880186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.76 % (3880186)CaDiCaL version: 2.1.3
% 2.86/0.76 % (3880186)Termination reason: Inappropriate
% 2.86/0.76 % (3880186)Time elapsed: 0.003 s
% 2.86/0.76 % (3880186)Peak memory usage: 10 MB
% 2.86/0.76 % (3880186)Instructions burned: 7 (million)
% 2.86/0.76 % (3880186)------------------------------
% 2.86/0.76 % (3880186)------------------------------
% 2.86/0.76 % (3880199)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2723595432:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 2.86/0.76 % (3880200)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=1444508093:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 2.86/0.76 % (3880158)Instruction limit reached!
% 2.86/0.76 % (3880158)------------------------------
% 2.86/0.76 % (3880158)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.76 % (3880158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.76 % (3880158)CaDiCaL version: 2.1.3
% 2.86/0.76 % (3880158)Termination reason: Instruction limit
% 2.86/0.76 % (3880158)Termination phase: Saturation
% 2.86/0.76 % (3880158)Time elapsed: 0.076 s
% 2.86/0.76 % (3880158)Peak memory usage: 13 MB
% 2.86/0.76 % (3880158)Instructions burned: 117 (million)
% 2.86/0.76 % (3880159)Instruction limit reached!
% 2.86/0.76 % (3880159)------------------------------
% 2.86/0.76 % (3880159)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.21/1.01 % (3880159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.21/1.01 % (3880159)CaDiCaL version: 2.1.3
% 4.21/1.01 % (3880159)Termination reason: Instruction limit
% 4.21/1.01 % (3880159)Termination phase: Saturation
% 4.21/1.01 % (3880159)Time elapsed: 0.085 s
% 4.21/1.01 % (3880159)Peak memory usage: 13 MB
% 4.21/1.01 % (3880159)Instructions burned: 132 (million)
% 4.21/1.01 % (3880199)Instruction limit reached!
% 4.21/1.01 % (3880199)------------------------------
% 4.21/1.01 % (3880199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.21/1.01 % (3880199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.21/1.01 % (3880199)CaDiCaL version: 2.1.3
% 4.21/1.01 % (3880199)Termination reason: Instruction limit
% 4.21/1.01 % (3880199)Termination phase: Saturation
% 4.21/1.01 % (3880199)Time elapsed: 0.048 s
% 4.21/1.01 % (3880199)Peak memory usage: 13 MB
% 4.21/1.01 % (3880199)Instructions burned: 132 (million)
% 4.21/1.01 % (3880207)ott-21_1_sil=16000:fs=off:random_seed=3271130814:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 4.21/1.01 % (3880209)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3460936841:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 4.21/1.01 % (3880209)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 4.21/1.01 % (3880209)Terminated due to inappropriate strategy.
% 4.21/1.01 % (3880209)------------------------------
% 4.21/1.01 % (3880209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.21/1.01 % (3880209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.21/1.01 % (3880209)CaDiCaL version: 2.1.3
% 4.21/1.01 % (3880209)Termination reason: Inappropriate
% 4.21/1.01 % (3880209)Time elapsed: 0.001 s
% 4.21/1.01 % (3880209)Peak memory usage: 10 MB
% 4.21/1.01 % (3880209)Instructions burned: 5 (million)
% 4.21/1.01 % (3880209)------------------------------
% 4.21/1.01 % (3880209)------------------------------
% 4.21/1.01 % (3880161)Instruction limit reached!
% 4.21/1.01 % (3880161)------------------------------
% 4.21/1.01 % (3880161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.21/1.01 % (3880161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.21/1.01 % (3880161)CaDiCaL version: 2.1.3
% 4.21/1.01 % (3880161)Termination reason: Instruction limit
% 4.21/1.01 % (3880161)Termination phase: Saturation
% 4.21/1.01 % (3880161)Time elapsed: 0.102 s
% 4.21/1.01 % (3880161)Peak memory usage: 13 MB
% 4.21/1.01 % (3880161)Instructions burned: 160 (million)
% 4.21/1.01 % (3880208)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3974323018:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 4.21/1.01 % (3880212)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4019217282:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 4.21/1.01 % (3880214)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2390627760:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 4.21/1.01 % (3880214)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 4.21/1.01 % (3880214)Terminated due to inappropriate strategy.
% 4.21/1.01 % (3880214)------------------------------
% 4.21/1.01 % (3880214)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.21/1.01 % (3880214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.21/1.01 % (3880214)CaDiCaL version: 2.1.3
% 4.21/1.01 % (3880214)Termination reason: Inappropriate
% 4.21/1.01 % (3880214)Time elapsed: 0.004 s
% 4.21/1.01 % (3880214)Peak memory usage: 10 MB
% 4.21/1.01 % (3880214)Instructions burned: 7 (million)
% 4.21/1.01 % (3880214)------------------------------
% 4.21/1.01 % (3880214)------------------------------
% 4.21/1.01 % (3880217)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=1263084739:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi)
% 4.21/1.01 % (3880207)Instruction limit reached!
% 4.21/1.01 % (3880207)------------------------------
% 4.21/1.01 % (3880207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.21/1.01 % (3880207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.21/1.01 % (3880207)CaDiCaL version: 2.1.3
% 4.21/1.01 % (3880207)Termination reason: Instruction limit
% 4.21/1.01 % (3880207)Termination phase: Saturation
% 5.58/1.06 % (3880207)Time elapsed: 0.087 s
% 5.58/1.06 % (3880207)Peak memory usage: 13 MB
% 5.58/1.06 % (3880207)Instructions burned: 182 (million)
% 5.58/1.06 % (3880219)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1646805635:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 5.58/1.06 % (3880200)Instruction limit reached!
% 5.58/1.06 % (3880200)------------------------------
% 5.58/1.06 % (3880200)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.58/1.06 % (3880200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.58/1.06 % (3880200)CaDiCaL version: 2.1.3
% 5.58/1.06 % (3880200)Termination reason: Instruction limit
% 5.58/1.06 % (3880200)Termination phase: Saturation
% 5.58/1.06 % (3880200)Time elapsed: 0.366 s
% 5.58/1.06 % (3880200)Peak memory usage: 17 MB
% 5.58/1.06 % (3880200)Instructions burned: 685 (million)
% 5.58/1.06 % (3880208)Instruction limit reached!
% 5.58/1.06 % (3880208)------------------------------
% 5.58/1.06 % (3880208)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.58/1.06 % (3880208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.58/1.06 % (3880208)CaDiCaL version: 2.1.3
% 5.58/1.06 % (3880208)Termination reason: Instruction limit
% 5.58/1.06 % (3880208)Termination phase: Saturation
% 5.58/1.06 % (3880208)Time elapsed: 0.320 s
% 5.58/1.06 % (3880208)Peak memory usage: 14 MB
% 5.58/1.06 % (3880208)Instructions burned: 478 (million)
% 5.58/1.06 % (3880221)fmb+10_1_sil=64000:random_seed=590289675:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi)
% 5.58/1.06 % (3880221)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 5.58/1.06 % (3880221)Terminated due to inappropriate strategy.
% 5.58/1.06 % (3880221)------------------------------
% 5.58/1.06 % (3880221)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.58/1.06 % (3880221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.58/1.06 % (3880221)CaDiCaL version: 2.1.3
% 5.58/1.06 % (3880221)Termination reason: Inappropriate
% 5.58/1.06 % (3880221)Time elapsed: 0.004 s
% 5.58/1.06 % (3880221)Peak memory usage: 11 MB
% 5.58/1.06 % (3880221)Instructions burned: 7 (million)
% 5.58/1.06 % (3880221)------------------------------
% 5.58/1.06 % (3880221)------------------------------
% 5.58/1.06 % (3880222)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3761256829:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi)
% 5.58/1.06 % (3880222)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 5.58/1.06 % (3880222)Terminated due to inappropriate strategy.
% 5.58/1.06 % (3880222)------------------------------
% 5.58/1.06 % (3880222)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.58/1.06 % (3880222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.58/1.06 % (3880222)CaDiCaL version: 2.1.3
% 5.58/1.06 % (3880222)Termination reason: Inappropriate
% 5.58/1.06 % (3880222)Time elapsed: 0.003 s
% 5.58/1.06 % (3880222)Peak memory usage: 10 MB
% 5.58/1.06 % (3880222)Instructions burned: 7 (million)
% 5.58/1.06 % (3880222)------------------------------
% 5.58/1.06 % (3880222)------------------------------
% 5.58/1.06 % (3880225)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=140382402:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi)
% 5.58/1.06 % (3880225)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 5.58/1.06 % (3880225)Terminated due to inappropriate strategy.
% 5.58/1.06 % (3880225)------------------------------
% 5.58/1.06 % (3880225)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.58/1.06 % (3880225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.58/1.06 % (3880225)CaDiCaL version: 2.1.3
% 5.58/1.06 % (3880225)Termination reason: Inappropriate
% 5.58/1.06 % (3880225)Time elapsed: 0.003 s
% 5.58/1.06 % (3880225)Peak memory usage: 10 MB
% 5.58/1.06 % (3880225)Instructions burned: 7 (million)
% 5.58/1.06 % (3880226)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=876603231:i=5131_2995 on theBenchmark for (2995ds/5131Mi)
% 5.58/1.06 % (3880225)------------------------------
% 5.58/1.06 % (3880225)------------------------------
% 5.58/1.06 % (3880212)Instruction limit reached!
% 5.58/1.06 % (3880212)------------------------------
% 5.58/1.06 % (3880212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.58/1.06 % (3880212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.58/1.06 % (3880212)CaDiCaL version: 2.1.3
% 5.58/1.06 % (3880212)Termination reason: Instruction limit
% 5.58/1.06 % (3880212)Termination phase: Saturation
% 5.58/1.06 % (3880212)Time elapsed: 0.369 s
% 5.58/1.06 % (3880212)Peak memory usage: 20 MB
% 5.58/1.06 % (3880212)Instructions burned: 1181 (million)
% 5.58/1.06 % (3880229)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1906446948:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi)
% 5.58/1.06 % (3880230)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3643587952:i=6324_2994 on theBenchmark for (2994ds/6324Mi)
% 5.58/1.06 % (3880230)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 5.58/1.06 % (3880230)Terminated due to inappropriate strategy.
% 5.58/1.06 % (3880230)------------------------------
% 5.58/1.06 % (3880230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.58/1.06 % (3880230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.58/1.06 % (3880230)CaDiCaL version: 2.1.3
% 5.58/1.06 % (3880230)Termination reason: Inappropriate
% 5.58/1.06 % (3880230)Time elapsed: 0.002 s
% 5.58/1.06 % (3880230)Peak memory usage: 10 MB
% 5.58/1.06 % (3880230)Instructions burned: 8 (million)
% 5.58/1.06 % (3880230)------------------------------
% 5.58/1.06 % (3880230)------------------------------
% 5.58/1.06 % (3880233)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3419291299:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi)
% 5.58/1.06 % (3880233)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 5.58/1.06 % (3880233)Terminated due to inappropriate strategy.
% 5.58/1.06 % (3880233)------------------------------
% 5.58/1.06 % (3880233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.58/1.06 % (3880233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.58/1.06 % (3880233)CaDiCaL version: 2.1.3
% 5.58/1.06 % (3880233)Termination reason: Inappropriate
% 5.58/1.06 % (3880233)Time elapsed: 0.002 s
% 5.58/1.06 % (3880233)Peak memory usage: 10 MB
% 5.58/1.06 % (3880233)Instructions burned: 7 (million)
% 5.58/1.06 % (3880233)------------------------------
% 5.58/1.06 % (3880233)------------------------------
% 5.58/1.06 % (3880235)ott-2_1_sil=16000:newcnf=on:random_seed=989562716:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi)
% 5.58/1.06 % (3880217)Instruction limit reached!
% 5.58/1.06 % (3880217)------------------------------
% 5.58/1.06 % (3880217)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.58/1.06 % (3880217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.58/1.06 % (3880217)CaDiCaL version: 2.1.3
% 5.58/1.06 % (3880217)Termination reason: Instruction limit
% 5.58/1.06 % (3880217)Termination phase: Saturation
% 5.58/1.06 % (3880217)Time elapsed: 0.396 s
% 5.58/1.06 % (3880217)Peak memory usage: 16 MB
% 5.58/1.06 % (3880217)Instructions burned: 694 (million)
% 5.58/1.06 % (3880237)ott+10_1_sil=32000:tgt=ground:random_seed=2840794420:i=5114:av=off_2994 on theBenchmark for (2994ds/5114Mi)
% 5.58/1.06 % (3880219)Instruction limit reached!
% 5.58/1.06 % (3880219)------------------------------
% 5.58/1.06 % (3880219)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.58/1.06 % (3880219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.58/1.06 % (3880219)CaDiCaL version: 2.1.3
% 5.58/1.06 % (3880219)Termination reason: Instruction limit
% 5.58/1.06 % (3880219)Termination phase: Saturation
% 5.58/1.06 % (3880219)Time elapsed: 0.496 s
% 5.58/1.06 % (3880219)Peak memory usage: 20 MB
% 5.58/1.06 % (3880219)Instructions burned: 880 (million)
% 5.58/1.06 % (3880239)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2072063576:i=54282_2992 on theBenchmark for (2992ds/54282Mi)
% 5.58/1.06 % (3880239)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 5.58/1.06 % (3880239)Terminated due to inappropriate strategy.
% 5.58/1.06 % (3880239)------------------------------
% 5.58/1.06 % (3880239)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.58/1.06 % (3880239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.58/1.06 % (3880239)CaDiCaL version: 2.1.3
% 5.58/1.06 % (3880239)Termination reason: Inappropriate
% 5.58/1.06 % (3880239)Time elapsed: 0.005 s
% 5.58/1.06 % (3880239)Peak memory usage: 10 MB
% 5.58/1.06 % (3880239)Instructions burned: 8 (million)
% 5.58/1.06 % (3880239)------------------------------
% 5.58/1.06 % (3880239)------------------------------
% 5.58/1.06 % (3880241)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4052191401:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi)
% 5.58/1.06 % (3880241) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3880140-3880241"...
% 5.58/1.06 % (3880241)...printing done.
% 5.58/1.06 % (3880241)Refutation found. Thanks to Tanya!
% 5.58/1.06 % SZS status Theorem for theBenchmark
% 5.58/1.06 % SZS output start Proof for theBenchmark
% 5.58/1.06 tff(type_def_5, type, date: $tType).
% 5.58/1.06 tff(type_def_6, type, time: $tType).
% 5.58/1.06 tff(type_def_7, type, day_name: $tType).
% 5.58/1.06 tff(func_def_0, type, ymd: ($int * $int * $int) > date).
% 5.58/1.06 tff(func_def_1, type, dt: ($int * $int * $int * $int * $int) > time).
% 5.58/1.06 tff(func_def_2, type, sunday: day_name).
% 5.58/1.06 tff(func_def_3, type, monday: day_name).
% 5.58/1.06 tff(func_def_4, type, tuesday: day_name).
% 5.58/1.06 tff(func_def_5, type, wednesday: day_name).
% 5.58/1.06 tff(func_def_6, type, thursday: day_name).
% 5.58/1.06 tff(func_def_7, type, friday: day_name).
% 5.58/1.06 tff(func_def_8, type, saturday: day_name).
% 5.58/1.06 tff(pred_def_1, type, is_leap_year: $int > $o).
% 5.58/1.06 tff(pred_def_2, type, is_days_in_month: ($int * $int * $int) > $o).
% 5.58/1.06 tff(pred_def_3, type, is_days_in_year: ($int * $int) > $o).
% 5.58/1.06 tff(pred_def_4, type, calc_date: ($int * $int * $int * date) > $o).
% 5.58/1.06 tff(pred_def_5, type, calc_datetime: ($int * $int * $int * $int * $int * $int * $int * $int * time) > $o).
% 5.58/1.06 tff(pred_def_6, type, normalize_time: ($int * $int * $int * $int * $int * $int * $int) > $o).
% 5.58/1.06 tff(pred_def_7, type, weekday: (date * day_name) > $o).
% 5.58/1.06 tff(pred_def_8, type, zeller_prep: ($int * $int * $int * $int * $int * $int) > $o).
% 5.58/1.06 tff(pred_def_9, type, map_iso: ($int * day_name) > $o).
% 5.58/1.06 tff(pred_def_10, type, map_name_to_int: (day_name * $int) > $o).
% 5.58/1.06 tff(pred_def_11, type, nth_weekday_date: ($int * day_name * $int * $int * date) > $o).
% 5.58/1.06 tff(pred_def_12, type, calc_nth_offset: ($int * $int * $int) > $o).
% 5.58/1.06 tff(pred_def_13, type, valid_day: $int > $o).
% 5.58/1.06 tff(f1,axiom,(
% 5.58/1.06 ! [X0 : $int] : (valid_day(X0) <=> ($greater(X0,0) & $lesseq(X0,31)))),
% 5.58/1.06 file('/export/starexec/sandbox/benchmark/Axioms/TIM001_0.ax',trap_ax)).
% 5.58/1.06 tff(f37,axiom,(
% 5.58/1.06 ! [X0 : $int] : is_days_in_month(1,X0,31)),
% 5.58/1.06 file('/export/starexec/sandbox/benchmark/Axioms/TIM001_0.ax',m1)).
% 5.58/1.06 tff(f49,axiom,(
% 5.58/1.06 ! [X0 : $int,X1 : $int,X2 : $int,X3 : $int] : ((is_days_in_month(X1,X2,X3) & $greater(X0,0) & $lesseq(X0,X3)) => calc_date(X0,X1,X2,ymd(X2,X1,X0)))),
% 5.58/1.06 file('/export/starexec/sandbox/benchmark/Axioms/TIM001_0.ax',rule_base)).
% 5.58/1.06 tff(f50,axiom,(
% 5.58/1.06 ! [X0 : $int,X1 : $int,X2 : $int,X3 : $int,X4 : date] : ((is_days_in_month(X1,X2,X3) & $greater(X0,X3) & X1 != 12) => (calc_date($difference(X0,X3),$sum(X1,1),X2,X4) => calc_date(X0,X1,X2,X4)))),
% 5.58/1.06 file('/export/starexec/sandbox/benchmark/Axioms/TIM001_0.ax',rule_fwd_std)).
% 5.58/1.06 tff(f82,axiom,(
% 5.58/1.06 is_days_in_month(2,2024,29)),
% 5.58/1.06 file('/export/starexec/sandbox/benchmark/Axioms/TIM001_0.ax',hint_leap_2024_feb)).
% 5.58/1.06 tff(f88,conjecture,(
% 5.58/1.06 ? [X0 : $int,X1 : $int,X2 : $int] : (calc_date($sum(30,5),1,2024,ymd(X0,X1,X2)) & X1 = 2 & X2 = 4 & valid_day(X2))),
% 5.58/1.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p',test_month_roll)).
% 5.58/1.06 tff(f89,negated_conjecture,(
% 5.58/1.06 ~ ? [X0 : $int,X1 : $int,X2 : $int] : (calc_date($sum(30,5),1,2024,ymd(X0,X1,X2)) & X1 = 2 & X2 = 4 & valid_day(X2))),
% 5.58/1.06 inference(negated_conjecture,[status(cth)],[f88])).
% 5.58/1.06 tff(f90,plain,(
% 5.58/1.06 ! [X0 : $int] : (valid_day(X0) <=> ($less(0,X0) & ~$less(31,X0)))),
% 5.58/1.06 inference(theory_normalization,[],[f1])).
% 5.58/1.06 tff(f104,plain,(
% 5.58/1.06 ! [X0 : $int,X1 : $int,X2 : $int,X3 : $int] : ((is_days_in_month(X1,X2,X3) & $less(0,X0) & ~$less(X3,X0)) => calc_date(X0,X1,X2,ymd(X2,X1,X0)))),
% 5.58/1.06 inference(theory_normalization,[],[f49])).
% 5.58/1.06 tff(f105,plain,(
% 5.58/1.06 ! [X0 : $int,X1 : $int,X2 : $int,X3 : $int,X4 : date] : ((is_days_in_month(X1,X2,X3) & $less(X3,X0) & X1 != 12) => (calc_date($sum(X0,$uminus(X3)),$sum(X1,1),X2,X4) => calc_date(X0,X1,X2,X4)))),
% 5.58/1.06 inference(theory_normalization,[],[f50])).
% 5.58/1.06 tff(f116,definition,(
% 5.58/1.06 ( ! [X0 : $int,X1 : $int] : ($sum(X0,X1) = $sum(X1,X0)) )),
% 5.58/1.06 introduced(theory,[tha_commutativity])).
% 5.58/1.06 tff(f117,definition,(
% 5.58/1.06 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum(X0,$sum(X1,X2)) = $sum($sum(X0,X1),X2)) )),
% 5.58/1.06 introduced(theory,[tha_associativity])).
% 5.58/1.06 tff(f120,definition,(
% 5.58/1.06 ( ! [X0 : $int] : (0 = $sum(X0,$uminus(X0))) )),
% 5.58/1.06 introduced(theory,[tha_inverse_op_unit])).
% 5.58/1.06 tff(f126,definition,(
% 5.58/1.06 ( ! [X0 : $int] : ($uminus($uminus(X0)) = X0) )),
% 5.58/1.06 introduced(theory,[tha_minus_minus_x])).
% 5.58/1.06 tff(f139,plain,(
% 5.58/1.06 ! [X0 : $int] : (($less(0,X0) & ~$less(31,X0)) => valid_day(X0))),
% 5.58/1.06 inference(unused_predicate_definition_removal,[],[f90])).
% 5.58/1.06 tff(f143,plain,(
% 5.58/1.06 ! [X0 : $int] : (valid_day(X0) | (~$less(0,X0) | $less(31,X0)))),
% 5.58/1.06 inference(ennf_transformation,[],[f139])).
% 5.58/1.06 tff(f144,plain,(
% 5.58/1.06 ! [X0 : $int] : (valid_day(X0) | ~$less(0,X0) | $less(31,X0))),
% 5.58/1.06 inference(flattening,[],[f143])).
% 5.58/1.06 tff(f173,plain,(
% 5.58/1.06 ! [X0 : $int,X1 : $int,X2 : $int,X3 : $int] : (calc_date(X0,X1,X2,ymd(X2,X1,X0)) | (~is_days_in_month(X1,X2,X3) | ~$less(0,X0) | $less(X3,X0)))),
% 5.58/1.06 inference(ennf_transformation,[],[f104])).
% 5.58/1.06 tff(f174,plain,(
% 5.58/1.06 ! [X0 : $int,X1 : $int,X2 : $int,X3 : $int] : (calc_date(X0,X1,X2,ymd(X2,X1,X0)) | ~is_days_in_month(X1,X2,X3) | ~$less(0,X0) | $less(X3,X0))),
% 5.58/1.06 inference(flattening,[],[f173])).
% 5.58/1.06 tff(f175,plain,(
% 5.58/1.06 ! [X0 : $int,X1 : $int,X2 : $int,X3 : $int,X4 : date] : ((calc_date(X0,X1,X2,X4) | ~calc_date($sum(X0,$uminus(X3)),$sum(X1,1),X2,X4)) | (~is_days_in_month(X1,X2,X3) | ~$less(X3,X0) | 12 = X1))),
% 5.58/1.06 inference(ennf_transformation,[],[f105])).
% 5.58/1.06 tff(f176,plain,(
% 5.58/1.06 ! [X0 : $int,X1 : $int,X2 : $int,X3 : $int,X4 : date] : (calc_date(X0,X1,X2,X4) | ~calc_date($sum(X0,$uminus(X3)),$sum(X1,1),X2,X4) | ~is_days_in_month(X1,X2,X3) | ~$less(X3,X0) | 12 = X1)),
% 5.58/1.06 inference(flattening,[],[f175])).
% 5.58/1.06 tff(f206,plain,(
% 5.58/1.06 ! [X0 : $int,X1 : $int,X2 : $int] : (~calc_date($sum(30,5),1,2024,ymd(X0,X1,X2)) | 2 != X1 | 4 != X2 | ~valid_day(X2))),
% 5.58/1.06 inference(ennf_transformation,[],[f89])).
% 5.58/1.06 tff(f208,plain,(
% 5.58/1.06 ( ! [X0 : $int] : (valid_day(X0) | ~$less(0,X0) | $less(31,X0)) )),
% 5.58/1.06 inference(cnf_transformation,[],[f144])).
% 5.58/1.06 tff(f245,plain,(
% 5.58/1.06 ( ! [X0 : $int] : (is_days_in_month(1,X0,31)) )),
% 5.58/1.06 inference(cnf_transformation,[],[f37])).
% 5.58/1.06 tff(f260,plain,(
% 5.58/1.06 ( ! [X2 : $int,X3 : $int,X0 : $int,X1 : $int] : (calc_date(X0,X1,X2,ymd(X2,X1,X0)) | ~is_days_in_month(X1,X2,X3) | ~$less(0,X0) | $less(X3,X0)) )),
% 5.58/1.06 inference(cnf_transformation,[],[f174])).
% 5.58/1.06 tff(f261,plain,(
% 5.58/1.06 ( ! [X2 : $int,X3 : $int,X0 : $int,X1 : $int,X4 : date] : (calc_date(X0,X1,X2,X4) | ~calc_date($sum(X0,$uminus(X3)),$sum(X1,1),X2,X4) | ~is_days_in_month(X1,X2,X3) | ~$less(X3,X0) | 12 = X1) )),
% 5.58/1.06 inference(cnf_transformation,[],[f176])).
% 5.58/1.06 tff(f294,plain,(
% 5.58/1.06 is_days_in_month(2,2024,29)),
% 5.58/1.06 inference(cnf_transformation,[],[f82])).
% 5.58/1.06 tff(f301,plain,(
% 5.58/1.06 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~calc_date($sum(30,5),1,2024,ymd(X0,X1,X2)) | 2 != X1 | 4 != X2 | ~valid_day(X2)) )),
% 5.58/1.06 inference(cnf_transformation,[],[f206])).
% 5.58/1.06 tff(f326,plain,(
% 5.58/1.06 ( ! [X2 : $int,X0 : $int] : (~calc_date($sum(30,5),1,2024,ymd(X0,2,X2)) | 4 != X2 | ~valid_day(X2)) )),
% 5.58/1.06 inference(equality_resolution,[],[f301])).
% 5.58/1.06 tff(f327,plain,(
% 5.58/1.06 ( ! [X0 : $int] : (~calc_date($sum(30,5),1,2024,ymd(X0,2,4)) | ~valid_day(4)) )),
% 5.58/1.06 inference(equality_resolution,[],[f326])).
% 5.58/1.06 tff(f328,plain,(
% 5.58/1.06 ( ! [X0 : $int] : (~calc_date(35,1,2024,ymd(X0,2,4)) | ~valid_day(4)) )),
% 5.58/1.06 inference(evaluation,[],[f327])).
% 5.58/1.06 tff(f352,definition,(
% 5.58/1.06 spl0_1 <=> valid_day(4)),
% 5.58/1.06 introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition])).
% 5.58/1.06 tff(f353,plain,(
% 5.58/1.06 ~valid_day(4) | spl0_1),
% 5.58/1.06 inference(avatar_component_clause,[],[f352])).
% 5.58/1.06 tff(f355,definition,(
% 5.58/1.06 spl0_2 <=> ! [X0 : $int] : ~calc_date(35,1,2024,ymd(X0,2,4))),
% 5.58/1.06 introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition])).
% 5.58/1.06 tff(f356,plain,(
% 5.58/1.06 ( ! [X0 : $int] : (~calc_date(35,1,2024,ymd(X0,2,4))) ) | ~spl0_2),
% 5.58/1.06 inference(avatar_component_clause,[],[f355])).
% 5.58/1.06 tff(f357,plain,(
% 5.58/1.06 ~spl0_1 | spl0_2),
% 5.58/1.06 inference(avatar_split_clause,[],[f328,f355,f352])).
% 5.58/1.06 tff(f398,plain,(
% 5.58/1.06 ~$less(0,4) | $less(31,4) | spl0_1),
% 5.58/1.06 inference(resolution,[],[f208,f353])).
% 5.58/1.06 tff(f399,plain,(
% 5.58/1.06 $false | spl0_1),
% 5.58/1.06 inference(evaluation,[],[f398])).
% 5.58/1.06 tff(f400,plain,(
% 5.58/1.06 spl0_1),
% 5.58/1.06 inference(avatar_contradiction_clause,[],[f399])).
% 5.58/1.06 tff(f754,plain,(
% 5.58/1.06 ( ! [X0 : $int,X1 : $int] : (~calc_date($sum(35,$uminus(X0)),$sum(1,1),2024,ymd(X1,2,4)) | ~is_days_in_month(1,2024,X0) | ~$less(X0,35) | 1 = 12) ) | ~spl0_2),
% 5.58/1.06 inference(resolution,[],[f261,f356])).
% 5.58/1.06 tff(f755,plain,(
% 5.58/1.06 ( ! [X0 : $int,X1 : $int] : (~calc_date($sum(35,$uminus(X0)),2,2024,ymd(X1,2,4)) | ~is_days_in_month(1,2024,X0) | ~$less(X0,35)) ) | ~spl0_2),
% 5.58/1.06 inference(evaluation,[],[f754])).
% 5.58/1.06 tff(f757,plain,(
% 5.58/1.06 ( ! [X0 : $int,X1 : $int] : (~calc_date($sum(35,X0),2,2024,ymd(X1,2,4)) | ~is_days_in_month(1,2024,$uminus(X0)) | ~$less($uminus(X0),35)) ) | ~spl0_2),
% 5.58/1.06 inference(superposition,[],[f755,f126])).
% 5.58/1.06 tff(f765,plain,(
% 5.58/1.06 ( ! [X0 : $int,X1 : $int] : (~calc_date($sum(X0,35),2,2024,ymd(X1,2,4)) | ~is_days_in_month(1,2024,$uminus(X0)) | ~$less($uminus(X0),35)) ) | ~spl0_2),
% 5.58/1.06 inference(superposition,[],[f757,f116])).
% 5.58/1.06 tff(f780,plain,(
% 5.58/1.06 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~calc_date($sum(X0,$sum(X1,35)),2,2024,ymd(X2,2,4)) | ~is_days_in_month(1,2024,$uminus($sum(X0,X1))) | ~$less($uminus($sum(X0,X1)),35)) ) | ~spl0_2),
% 5.58/1.06 inference(superposition,[],[f765,f117])).
% 5.58/1.06 tff(f796,plain,(
% 5.58/1.06 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~calc_date($sum(X1,$sum(35,X0)),2,2024,ymd(X2,2,4)) | ~is_days_in_month(1,2024,$uminus($sum(X1,X0))) | ~$less($uminus($sum(X1,X0)),35)) ) | ~spl0_2),
% 5.58/1.06 inference(superposition,[],[f780,f116])).
% 5.58/1.06 tff(f820,plain,(
% 5.58/1.06 ( ! [X0 : $int,X1 : $int] : (~calc_date($sum(X0,0),2,2024,ymd(X1,2,4)) | ~is_days_in_month(1,2024,$uminus($sum(X0,$uminus(35)))) | ~$less($uminus($sum(X0,$uminus(35))),35)) ) | ~spl0_2),
% 5.58/1.06 inference(superposition,[],[f796,f120])).
% 5.58/1.06 tff(f826,plain,(
% 5.58/1.06 ( ! [X0 : $int,X1 : $int] : (~calc_date(X0,2,2024,ymd(X1,2,4)) | ~is_days_in_month(1,2024,$uminus($sum(X0,-35))) | ~$less($uminus($sum(X0,-35)),35)) ) | ~spl0_2),
% 5.58/1.06 inference(evaluation,[],[f820])).
% 5.58/1.06 tff(f839,plain,(
% 5.58/1.06 ( ! [X0 : $int] : (~is_days_in_month(1,2024,$uminus($sum(4,-35))) | ~$less($uminus($sum(4,-35)),35) | ~is_days_in_month(2,2024,X0) | ~$less(0,4) | $less(X0,4)) ) | ~spl0_2),
% 5.58/1.06 inference(resolution,[],[f826,f260])).
% 5.58/1.06 tff(f844,plain,(
% 5.58/1.06 ( ! [X0 : $int] : (~is_days_in_month(1,2024,31) | ~is_days_in_month(2,2024,X0) | $less(X0,4)) ) | ~spl0_2),
% 5.58/1.06 inference(evaluation,[],[f839])).
% 5.58/1.06 tff(f845,plain,(
% 5.58/1.06 ( ! [X0 : $int] : (~is_days_in_month(2,2024,X0) | $less(X0,4)) ) | ~spl0_2),
% 5.58/1.06 inference(forward_subsumption_resolution,[],[f844,f245])).
% 5.58/1.06 tff(f853,plain,(
% 5.58/1.06 $less(29,4) | ~spl0_2),
% 5.58/1.06 inference(resolution,[],[f845,f294])).
% 5.58/1.06 tff(f855,plain,(
% 5.58/1.06 $false | ~spl0_2),
% 5.58/1.06 inference(evaluation,[],[f853])).
% 5.58/1.06 tff(f856,plain,(
% 5.58/1.06 ~spl0_2),
% 5.58/1.06 inference(avatar_contradiction_clause,[],[f855])).
% 5.58/1.06 cnf(s1, plain, ~spl0_1 | spl0_2, inference(sat_conversion,[],[f357])).
% 5.58/1.06 cnf(s2, plain, spl0_1, inference(sat_conversion,[],[f400])).
% 5.58/1.06 cnf(s4, plain, ~spl0_2, inference(sat_conversion,[],[f856])).
% 5.58/1.06 cnf(s5, plain, $false, inference(rat,[],[s1,s4,s2])).
% 5.58/1.06 tff(f857,plain,(
% 5.58/1.06 $false),
% 5.58/1.06 inference(avatar_sat_refutation,[],[s5])).
% 5.58/1.06 % SZS output end Proof for theBenchmark
% 5.58/1.06 % (3880241)------------------------------
% 5.58/1.06 % (3880241)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.58/1.06 % (3880241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.58/1.06 % (3880241)CaDiCaL version: 2.1.3
% 5.58/1.06 % (3880241)Termination reason: Refutation
% 5.58/1.06 % (3880241)Time elapsed: 0.026 s
% 5.58/1.06 % (3880241)Peak memory usage: 13 MB
% 5.58/1.06 % (3880241)Instructions burned: 37 (million)
% 5.58/1.06 % (3880140)Success in time 0.821 s
% 5.58/1.06 % Vampire exiting
%------------------------------------------------------------------------------