%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR310_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 : n015.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:46:35 AM UTC 2026
% Result : Theorem 18.76s 2.94s
% Output : Refutation 18.76s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR310_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.07/0.19 % Computer : n015.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Tue Sep 29 00:08:17 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.23 Running first-order model finding
% 0.07/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
% 4.57/0.90 % (3162532)Will run a generic schedule for satisfiability detection.
% 4.57/0.90 % (3162545)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3373712741:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.57/0.90 % (3162544)% WARNING: option uhcvi not known.
% 4.57/0.90 % (3162543)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=454922566_2999 on theBenchmark for (2999ds/0Mi)
% 4.57/0.90 % (3162544)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4111062169:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.57/0.90 % (3162547)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2674825891:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.57/0.90 % (3162543)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 4.57/0.90 % (3162543)Terminated due to inappropriate strategy.
% 4.57/0.90 % (3162543)------------------------------
% 4.57/0.90 % (3162543)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.57/0.90 % (3162543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.57/0.90 % (3162543)CaDiCaL version: 2.1.3
% 4.57/0.90 % (3162543)Termination reason: Inappropriate
% 4.57/0.90 % (3162543)Time elapsed: 0.003 s
% 4.57/0.90 % (3162543)Peak memory usage: 10 MB
% 4.57/0.90 % (3162543)Instructions burned: 4 (million)
% 4.57/0.90 % (3162546)dis+10_1_sil=32000:sp=arity:random_seed=781338627:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.57/0.90 % (3162543)------------------------------
% 4.57/0.90 % (3162543)------------------------------
% 4.57/0.90 % (3162548)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=223484648:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.57/0.90 % (3162549)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1490096874:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.57/0.90 % (3162560)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1452121915:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 4.57/0.90 % (3162560)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 4.57/0.90 % (3162560)Terminated due to inappropriate strategy.
% 4.57/0.90 % (3162560)------------------------------
% 4.57/0.90 % (3162560)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.57/0.90 % (3162560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.57/0.90 % (3162560)CaDiCaL version: 2.1.3
% 4.57/0.90 % (3162560)Termination reason: Inappropriate
% 4.57/0.90 % (3162560)Time elapsed: 0.002 s
% 4.57/0.90 % (3162560)Peak memory usage: 10 MB
% 4.57/0.90 % (3162560)Instructions burned: 3 (million)
% 4.57/0.90 % (3162560)------------------------------
% 4.57/0.90 % (3162560)------------------------------
% 4.57/0.90 % (3162571)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=782742412:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 4.57/0.90 % (3162547)Instruction limit reached!
% 4.57/0.90 % (3162547)------------------------------
% 4.57/0.90 % (3162547)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.57/0.90 % (3162547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.57/0.90 % (3162547)CaDiCaL version: 2.1.3
% 4.57/0.90 % (3162547)Termination reason: Instruction limit
% 4.57/0.90 % (3162547)Termination phase: Saturation
% 4.57/0.90 % (3162547)Time elapsed: 0.072 s
% 4.57/0.90 % (3162547)Peak memory usage: 12 MB
% 4.57/0.90 % (3162547)Instructions burned: 116 (million)
% 4.57/0.90 % (3162546)Instruction limit reached!
% 4.57/0.90 % (3162546)------------------------------
% 4.57/0.90 % (3162546)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.57/0.90 % (3162546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.57/0.90 % (3162546)CaDiCaL version: 2.1.3
% 4.57/0.90 % (3162546)Termination reason: Instruction limit
% 4.57/0.90 % (3162546)Termination phase: Saturation
% 4.57/0.90 % (3162546)Time elapsed: 0.069 s
% 4.57/0.90 % (3162546)Peak memory usage: 12 MB
% 4.57/0.90 % (3162546)Instructions burned: 103 (million)
% 4.57/0.90 % (3162582)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=1529721342:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 4.57/0.90 % (3162583)ott-21_1_sil=16000:fs=off:random_seed=2504361593:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 6.47/1.18 % (3162548)Instruction limit reached!
% 6.47/1.18 % (3162548)------------------------------
% 6.47/1.18 % (3162548)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.47/1.18 % (3162548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.47/1.18 % (3162548)CaDiCaL version: 2.1.3
% 6.47/1.18 % (3162548)Termination reason: Instruction limit
% 6.47/1.18 % (3162548)Termination phase: Saturation
% 6.47/1.18 % (3162548)Time elapsed: 0.098 s
% 6.47/1.18 % (3162548)Peak memory usage: 13 MB
% 6.47/1.18 % (3162548)Instructions burned: 131 (million)
% 6.47/1.18 % (3162549)Instruction limit reached!
% 6.47/1.18 % (3162549)------------------------------
% 6.47/1.18 % (3162549)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.47/1.18 % (3162549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.47/1.18 % (3162549)CaDiCaL version: 2.1.3
% 6.47/1.18 % (3162549)Termination reason: Instruction limit
% 6.47/1.18 % (3162549)Termination phase: Saturation
% 6.47/1.18 % (3162549)Time elapsed: 0.099 s
% 6.47/1.18 % (3162549)Peak memory usage: 13 MB
% 6.47/1.18 % (3162549)Instructions burned: 160 (million)
% 6.47/1.18 % (3162587)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3716019926:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 6.47/1.18 % (3162587)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.47/1.18 % (3162587)Terminated due to inappropriate strategy.
% 6.47/1.18 % (3162587)------------------------------
% 6.47/1.18 % (3162587)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.47/1.18 % (3162587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.47/1.18 % (3162587)CaDiCaL version: 2.1.3
% 6.47/1.18 % (3162587)Termination reason: Inappropriate
% 6.47/1.18 % (3162587)Time elapsed: 0.001 s
% 6.47/1.18 % (3162587)Peak memory usage: 10 MB
% 6.47/1.18 % (3162587)Instructions burned: 2 (million)
% 6.47/1.18 % (3162587)------------------------------
% 6.47/1.18 % (3162587)------------------------------
% 6.47/1.18 % (3162586)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2328549631:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 6.47/1.18 % (3162571)Instruction limit reached!
% 6.47/1.18 % (3162571)------------------------------
% 6.47/1.18 % (3162571)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.47/1.18 % (3162571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.47/1.18 % (3162571)CaDiCaL version: 2.1.3
% 6.47/1.18 % (3162571)Termination reason: Instruction limit
% 6.47/1.18 % (3162571)Termination phase: Saturation
% 6.47/1.18 % (3162571)Time elapsed: 0.094 s
% 6.47/1.18 % (3162571)Peak memory usage: 13 MB
% 6.47/1.18 % (3162571)Instructions burned: 131 (million)
% 6.47/1.18 % (3162590)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=560306195:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 6.47/1.18 % (3162591)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1070395941:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 6.47/1.18 % (3162591)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.47/1.18 % (3162591)Terminated due to inappropriate strategy.
% 6.47/1.18 % (3162591)------------------------------
% 6.47/1.18 % (3162591)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.47/1.18 % (3162591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.47/1.18 % (3162591)CaDiCaL version: 2.1.3
% 6.47/1.18 % (3162591)Termination reason: Inappropriate
% 6.47/1.18 % (3162591)Time elapsed: 0.002 s
% 6.47/1.18 % (3162591)Peak memory usage: 10 MB
% 6.47/1.18 % (3162591)Instructions burned: 3 (million)
% 6.47/1.18 % (3162591)------------------------------
% 6.47/1.18 % (3162591)------------------------------
% 6.47/1.18 % (3162594)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=4214272519: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)
% 6.47/1.18 % (3162583)Instruction limit reached!
% 6.47/1.18 % (3162583)------------------------------
% 6.47/1.18 % (3162583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.47/1.18 % (3162583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.47/1.18 % (3162583)CaDiCaL version: 2.1.3
% 6.47/1.18 % (3162583)Termination reason: Instruction limit
% 6.47/1.18 % (3162583)Termination phase: Saturation
% 18.76/2.94 % (3162583)Time elapsed: 0.090 s
% 18.76/2.94 % (3162583)Peak memory usage: 12 MB
% 18.76/2.94 % (3162583)Instructions burned: 186 (million)
% 18.76/2.94 % (3162596)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1550899787:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 18.76/2.94 % (3162582)Instruction limit reached!
% 18.76/2.94 % (3162582)------------------------------
% 18.76/2.94 % (3162582)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.76/2.94 % (3162582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.76/2.94 % (3162582)CaDiCaL version: 2.1.3
% 18.76/2.94 % (3162582)Termination reason: Instruction limit
% 18.76/2.94 % (3162582)Termination phase: Saturation
% 18.76/2.94 % (3162582)Time elapsed: 0.402 s
% 18.76/2.94 % (3162582)Peak memory usage: 18 MB
% 18.76/2.94 % (3162582)Instructions burned: 684 (million)
% 18.76/2.94 % (3162598)fmb+10_1_sil=64000:random_seed=1104014840:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi)
% 18.76/2.94 % (3162598)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 18.76/2.94 % (3162598)Terminated due to inappropriate strategy.
% 18.76/2.94 % (3162598)------------------------------
% 18.76/2.94 % (3162598)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.76/2.94 % (3162598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.76/2.94 % (3162598)CaDiCaL version: 2.1.3
% 18.76/2.94 % (3162598)Termination reason: Inappropriate
% 18.76/2.94 % (3162598)Time elapsed: 0.002 s
% 18.76/2.94 % (3162598)Peak memory usage: 10 MB
% 18.76/2.94 % (3162598)Instructions burned: 4 (million)
% 18.76/2.94 % (3162598)------------------------------
% 18.76/2.94 % (3162598)------------------------------
% 18.76/2.94 % (3162600)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3117984312:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi)
% 18.76/2.94 % (3162600)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 18.76/2.94 % (3162600)Terminated due to inappropriate strategy.
% 18.76/2.94 % (3162600)------------------------------
% 18.76/2.94 % (3162600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.76/2.94 % (3162600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.76/2.94 % (3162600)CaDiCaL version: 2.1.3
% 18.76/2.94 % (3162600)Termination reason: Inappropriate
% 18.76/2.94 % (3162600)Time elapsed: 0.002 s
% 18.76/2.94 % (3162600)Peak memory usage: 10 MB
% 18.76/2.94 % (3162600)Instructions burned: 3 (million)
% 18.76/2.94 % (3162600)------------------------------
% 18.76/2.94 % (3162600)------------------------------
% 18.76/2.94 % (3162594)Instruction limit reached!
% 18.76/2.94 % (3162594)------------------------------
% 18.76/2.94 % (3162594)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.76/2.94 % (3162594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.76/2.94 % (3162594)CaDiCaL version: 2.1.3
% 18.76/2.94 % (3162594)Termination reason: Instruction limit
% 18.76/2.94 % (3162594)Termination phase: Saturation
% 18.76/2.94 % (3162594)Time elapsed: 0.364 s
% 18.76/2.94 % (3162594)Peak memory usage: 16 MB
% 18.76/2.94 % (3162594)Instructions burned: 692 (million)
% 18.76/2.94 % (3162602)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2898075298:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi)
% 18.76/2.94 % (3162602)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 18.76/2.94 % (3162602)Terminated due to inappropriate strategy.
% 18.76/2.94 % (3162602)------------------------------
% 18.76/2.94 % (3162602)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.76/2.94 % (3162602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.76/2.94 % (3162602)CaDiCaL version: 2.1.3
% 18.76/2.94 % (3162602)Termination reason: Inappropriate
% 18.76/2.94 % (3162602)Time elapsed: 0.002 s
% 18.76/2.94 % (3162602)Peak memory usage: 10 MB
% 18.76/2.94 % (3162602)Instructions burned: 3 (million)
% 18.76/2.94 % (3162602)------------------------------
% 18.76/2.94 % (3162602)------------------------------
% 18.76/2.94 % (3162603)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3237433370:i=5131_2994 on theBenchmark for (2994ds/5131Mi)
% 18.76/2.94 % (3162606)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2866708214:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi)
% 18.76/2.94 % (3162586)Instruction limit reached!
% 18.76/2.94 % (3162586)------------------------------
% 18.76/2.94 % (3162586)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.76/2.94 % (3162586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.76/2.94 % (3162586)CaDiCaL version: 2.1.3
% 18.76/2.94 % (3162586)Termination reason: Instruction limit
% 18.76/2.94 % (3162586)Termination phase: Saturation
% 18.76/2.94 % (3162586)Time elapsed: 0.503 s
% 18.76/2.94 % (3162586)Peak memory usage: 14 MB
% 18.76/2.94 % (3162586)Instructions burned: 477 (million)
% 18.76/2.94 % (3162608)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1864506144:i=6324_2993 on theBenchmark for (2993ds/6324Mi)
% 18.76/2.94 % (3162608)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 18.76/2.94 % (3162608)Terminated due to inappropriate strategy.
% 18.76/2.94 % (3162608)------------------------------
% 18.76/2.94 % (3162608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.76/2.94 % (3162608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.76/2.94 % (3162608)CaDiCaL version: 2.1.3
% 18.76/2.94 % (3162608)Termination reason: Inappropriate
% 18.76/2.94 % (3162608)Time elapsed: 0.003 s
% 18.76/2.94 % (3162608)Peak memory usage: 10 MB
% 18.76/2.94 % (3162608)Instructions burned: 4 (million)
% 18.76/2.94 % (3162608)------------------------------
% 18.76/2.94 % (3162608)------------------------------
% 18.76/2.94 % (3162610)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3821273224:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi)
% 18.76/2.94 % (3162610)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 18.76/2.94 % (3162610)Terminated due to inappropriate strategy.
% 18.76/2.94 % (3162610)------------------------------
% 18.76/2.94 % (3162610)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.76/2.94 % (3162610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.76/2.94 % (3162610)CaDiCaL version: 2.1.3
% 18.76/2.94 % (3162610)Termination reason: Inappropriate
% 18.76/2.94 % (3162610)Time elapsed: 0.002 s
% 18.76/2.94 % (3162610)Peak memory usage: 10 MB
% 18.76/2.94 % (3162610)Instructions burned: 3 (million)
% 18.76/2.94 % (3162610)------------------------------
% 18.76/2.94 % (3162610)------------------------------
% 18.76/2.94 % (3162612)ott-2_1_sil=16000:newcnf=on:random_seed=2823069000:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2992 on theBenchmark for (2992ds/869Mi)
% 18.76/2.94 % (3162596)Instruction limit reached!
% 18.76/2.94 % (3162596)------------------------------
% 18.76/2.94 % (3162596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.76/2.94 % (3162596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.76/2.94 % (3162596)CaDiCaL version: 2.1.3
% 18.76/2.94 % (3162596)Termination reason: Instruction limit
% 18.76/2.94 % (3162596)Termination phase: Saturation
% 18.76/2.94 % (3162596)Time elapsed: 0.508 s
% 18.76/2.94 % (3162596)Peak memory usage: 17 MB
% 18.76/2.94 % (3162596)Instructions burned: 880 (million)
% 18.76/2.94 % (3162614)ott+10_1_sil=32000:tgt=ground:random_seed=2463741499:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi)
% 18.76/2.94 % (3162590)Instruction limit reached!
% 18.76/2.94 % (3162590)------------------------------
% 18.76/2.94 % (3162590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.76/2.94 % (3162590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.76/2.94 % (3162590)CaDiCaL version: 2.1.3
% 18.76/2.94 % (3162590)Termination reason: Instruction limit
% 18.76/2.94 % (3162590)Termination phase: Saturation
% 18.76/2.94 % (3162590)Time elapsed: 0.724 s
% 18.76/2.94 % (3162590)Peak memory usage: 19 MB
% 18.76/2.94 % (3162590)Instructions burned: 1180 (million)
% 18.76/2.94 % (3162624)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1769312033:i=54282_2990 on theBenchmark for (2990ds/54282Mi)
% 18.76/2.94 % (3162624)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 18.76/2.94 % (3162624)Terminated due to inappropriate strategy.
% 18.76/2.94 % (3162624)------------------------------
% 18.76/2.94 % (3162624)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.76/2.94 % (3162624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.76/2.94 % (3162624)CaDiCaL version: 2.1.3
% 18.76/2.94 % (3162624)Termination reason: Inappropriate
% 18.76/2.94 % (3162624)Time elapsed: 0.004 s
% 18.76/2.94 % (3162624)Peak memory usage: 10 MB
% 18.76/2.94 % (3162624)Instructions burned: 4 (million)
% 18.76/2.94 % (3162624)------------------------------
% 18.76/2.94 % (3162624)------------------------------
% 18.76/2.94 % (3162626)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2721529756:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi)
% 18.76/2.94 % (3162612)Instruction limit reached!
% 18.76/2.94 % (3162612)------------------------------
% 18.76/2.94 % (3162612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.76/2.94 % (3162612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.76/2.94 % (3162612)CaDiCaL version: 2.1.3
% 18.76/2.94 % (3162612)Termination reason: Instruction limit
% 18.76/2.94 % (3162612)Termination phase: Saturation
% 18.76/2.94 % (3162612)Time elapsed: 0.724 s
% 18.76/2.94 % (3162612)Peak memory usage: 17 MB
% 18.76/2.94 % (3162612)Instructions burned: 870 (million)
% 18.76/2.94 % (3162638)dis+21_1_sil=32000:sas=cadical:random_seed=3246234371:i=3773:amm=off_2985 on theBenchmark for (2985ds/3773Mi)
% 18.76/2.94 % (3162606)Instruction limit reached!
% 18.76/2.94 % (3162606)------------------------------
% 18.76/2.94 % (3162606)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.76/2.94 % (3162606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.76/2.94 % (3162606)CaDiCaL version: 2.1.3
% 18.76/2.94 % (3162606)Termination reason: Instruction limit
% 18.76/2.94 % (3162606)Termination phase: Saturation
% 18.76/2.94 % (3162606)Time elapsed: 0.956 s
% 18.76/2.94 % (3162606)Peak memory usage: 21 MB
% 18.76/2.94 % (3162606)Instructions burned: 1474 (million)
% 18.76/2.94 % (3162649)ott+11_1_sil=16000:gs=on:random_seed=1280045228:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2984 on theBenchmark for (2984ds/2251Mi)
% 18.76/2.94 % (3162638)Instruction limit reached!
% 18.76/2.94 % (3162638)------------------------------
% 18.76/2.94 % (3162638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.76/2.94 % (3162638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.76/2.94 % (3162638)CaDiCaL version: 2.1.3
% 18.76/2.94 % (3162638)Termination reason: Instruction limit
% 18.76/2.94 % (3162638)Termination phase: Saturation
% 18.76/2.94 % (3162638)Time elapsed: 1.052 s
% 18.76/2.94 % (3162638)Peak memory usage: 35 MB
% 18.76/2.94 % (3162638)Instructions burned: 3774 (million)
% 18.76/2.94 % (3162794)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=450200188:fmbsr=1.6:i=67534_2974 on theBenchmark for (2974ds/67534Mi)
% 18.76/2.94 % (3162794)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 18.76/2.94 % (3162794)Terminated due to inappropriate strategy.
% 18.76/2.94 % (3162794)------------------------------
% 18.76/2.94 % (3162794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.76/2.94 % (3162794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.76/2.94 % (3162794)CaDiCaL version: 2.1.3
% 18.76/2.94 % (3162794)Termination reason: Inappropriate
% 18.76/2.94 % (3162794)Time elapsed: 0.001 s
% 18.76/2.94 % (3162794)Peak memory usage: 10 MB
% 18.76/2.94 % (3162794)Instructions burned: 3 (million)
% 18.76/2.94 % (3162794)------------------------------
% 18.76/2.94 % (3162794)------------------------------
% 18.76/2.94 % (3162796)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3248542670:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2974 on theBenchmark for (2974ds/4591Mi)
% 18.76/2.94 % (3162626) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3162532-3162626"...
% 18.76/2.94 % (3162626)...printing done.
% 18.76/2.94 % (3162626)Refutation found. Thanks to Tanya!
% 18.76/2.94 % SZS status Theorem for theBenchmark
% 18.76/2.94 % SZS output start Proof for theBenchmark
% 18.76/2.94 tff(type_def_5, type, time: $tType).
% 18.76/2.94 tff(type_def_6, type, fluent: $tType).
% 18.76/2.94 tff(type_def_7, type, event: $tType).
% 18.76/2.94 tff(func_def_0, type, at_time: $int > time).
% 18.76/2.94 tff(func_def_4, type, waterLevel: $int > fluent).
% 18.76/2.94 tff(func_def_5, type, tapOn: event).
% 18.76/2.94 tff(func_def_6, type, tapOff: event).
% 18.76/2.94 tff(func_def_7, type, overflow: event).
% 18.76/2.94 tff(func_def_8, type, spilling: fluent).
% 18.76/2.94 tff(func_def_9, type, filling: fluent).
% 18.76/2.94 tff(func_def_13, type, sK2: ($int * fluent * $int) > event).
% 18.76/2.94 tff(func_def_14, type, sK3: ($int * fluent * $int) > $int).
% 18.76/2.94 tff(func_def_15, type, sK4: ($int * fluent * $int) > event).
% 18.76/2.94 tff(func_def_16, type, sK5: ($int * fluent * $int) > $int).
% 18.76/2.94 tff(func_def_17, type, sK6: (fluent * $int) > event).
% 18.76/2.94 tff(func_def_18, type, sK7: (fluent * $int) > event).
% 18.76/2.94 tff(func_def_19, type, sK8: (fluent * $int) > event).
% 18.76/2.94 tff(func_def_20, type, sK9: (fluent * $int) > event).
% 18.76/2.94 tff(func_def_21, type, sK10: ($int * event * fluent) > $int).
% 18.76/2.94 tff(func_def_22, type, sK11: ($int * event * fluent) > $int).
% 18.76/2.94 tff(func_def_23, type, sK12: (event * fluent) > $int).
% 18.76/2.94 tff(pred_def_1, type, startedIn: (time * fluent * time) > $o).
% 18.76/2.94 tff(pred_def_2, type, stoppedIn: (time * fluent * time) > $o).
% 18.76/2.94 tff(pred_def_3, type, happens: (event * time) > $o).
% 18.76/2.94 tff(pred_def_4, type, initiates: (event * fluent * time) > $o).
% 18.76/2.94 tff(pred_def_5, type, terminates: (event * fluent * time) > $o).
% 18.76/2.94 tff(pred_def_6, type, releases: (event * fluent * time) > $o).
% 18.76/2.94 tff(pred_def_7, type, trajectory: (fluent * time * fluent * $int) > $o).
% 18.76/2.94 tff(pred_def_8, type, antitrajectory: (fluent * time * fluent * $int) > $o).
% 18.76/2.94 tff(pred_def_9, type, holdsAt: (fluent * time) > $o).
% 18.76/2.94 tff(pred_def_10, type, releasedAt: (fluent * time) > $o).
% 18.76/2.94 tff(pred_def_12, type, sP0: ($int * event * fluent) > $o).
% 18.76/2.94 tff(pred_def_13, type, sP1: ($int * event * fluent) > $o).
% 18.76/2.94 tff(f5,axiom,(
% 18.76/2.94 ! [X0 : fluent,X1 : $int] : ((holdsAt(X0,at_time(X1)) & ~releasedAt(X0,at_time($sum(X1,1))) & ~ ? [X2 : event] : (happens(X2,at_time(X1)) & terminates(X2,X0,at_time(X1)))) => holdsAt(X0,at_time($sum(X1,1))))),
% 18.76/2.94 file('/export/starexec/sandbox/benchmark/Axioms/CSR001_0.ax',keep_holding)).
% 18.76/2.94 tff(f8,axiom,(
% 18.76/2.94 ! [X0 : fluent,X1 : $int] : ((~releasedAt(X0,at_time(X1)) & ~ ? [X2 : event] : (happens(X2,at_time(X1)) & releases(X2,X0,at_time(X1)))) => ~releasedAt(X0,at_time($sum(X1,1))))),
% 18.76/2.94 file('/export/starexec/sandbox/benchmark/Axioms/CSR001_0.ax',keep_not_released)).
% 18.76/2.94 tff(f12,axiom,(
% 18.76/2.94 ! [X0 : event,X1 : $int,X2 : fluent] : ((happens(X0,at_time(X1)) & (initiates(X0,X2,at_time(X1)) | terminates(X0,X2,at_time(X1)))) => ~releasedAt(X2,at_time($sum(X1,1))))),
% 18.76/2.94 file('/export/starexec/sandbox/benchmark/Axioms/CSR001_0.ax',happens_not_released)).
% 18.76/2.94 tff(f14,axiom,(
% 18.76/2.94 tapOn != overflow),
% 18.76/2.94 file('/export/starexec/sandbox/benchmark/Axioms/CSR001_1.ax',tapOn_overflow)).
% 18.76/2.94 tff(f20,axiom,(
% 18.76/2.94 ! [X0 : event,X1 : fluent,X2 : $int] : (initiates(X0,X1,at_time(X2)) <=> ((X0 = tapOn & X1 = filling) | (X0 = overflow & X1 = spilling) | ? [X3 : $int] : (holdsAt(waterLevel(X3),at_time(X2)) & X0 = tapOff & X1 = waterLevel(X3)) | ? [X3 : $int] : (holdsAt(waterLevel(X3),at_time(X2)) & X0 = overflow & X1 = waterLevel(X3))))),
% 18.76/2.94 file('/export/starexec/sandbox/benchmark/Axioms/CSR001_1.ax',initiates_all_defn)).
% 18.76/2.94 tff(f22,axiom,(
% 18.76/2.94 ! [X0 : event,X1 : fluent,X2 : $int] : (releases(X0,X1,at_time(X2)) <=> ? [X3 : $int] : (X0 = tapOn & X1 = waterLevel(X3)))),
% 18.76/2.94 file('/export/starexec/sandbox/benchmark/Axioms/CSR001_1.ax',releases_all_defn)).
% 18.76/2.94 tff(f25,axiom,(
% 18.76/2.94 ! [X0 : event,X1 : $int] : (happens(X0,at_time(X1)) <=> ((X0 = tapOn & X1 = 0) | (holdsAt(waterLevel(3),at_time(X1)) & holdsAt(filling,at_time(X1)) & X0 = overflow)))),
% 18.76/2.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p',happens_all_defn)).
% 18.76/2.94 tff(f32,conjecture,(
% 18.76/2.94 holdsAt(filling,at_time(3)) => (holdsAt(waterLevel(3),at_time(3)) | holdsAt(filling,at_time(4)))),
% 18.76/2.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p',waterLevel_filling)).
% 18.76/2.94 tff(f33,negated_conjecture,(
% 18.76/2.94 ~(holdsAt(filling,at_time(3)) => (holdsAt(waterLevel(3),at_time(3)) | holdsAt(filling,at_time(4))))),
% 18.76/2.94 inference(negated_conjecture,[status(cth)],[f32])).
% 18.76/2.94 tff(f34,definition,(
% 18.76/2.94 ( ! [X0 : $int,X1 : $int] : ($sum(X0,X1) = $sum(X1,X0)) )),
% 18.76/2.94 introduced(theory,[tha_commutativity])).
% 18.76/2.94 tff(f36,definition,(
% 18.76/2.94 ( ! [X0 : $int] : ($sum(X0,0) = X0) )),
% 18.76/2.94 introduced(theory,[tha_right_identity])).
% 18.76/2.94 tff(f46,plain,(
% 18.76/2.94 ! [X0 : event,X1 : fluent,X2 : $int] : (initiates(X0,X1,at_time(X2)) <=> ((X0 = tapOn & X1 = filling) | (X0 = overflow & X1 = spilling) | ? [X3 : $int] : (holdsAt(waterLevel(X3),at_time(X2)) & X0 = tapOff & X1 = waterLevel(X3)) | ? [X4 : $int] : (holdsAt(waterLevel(X4),at_time(X2)) & X0 = overflow & waterLevel(X4) = X1)))),
% 18.76/2.94 inference(rectify,[],[f20])).
% 18.76/2.94 tff(f50,plain,(
% 18.76/2.94 ! [X0 : fluent,X1 : $int] : (holdsAt(X0,at_time($sum(X1,1))) | (~holdsAt(X0,at_time(X1)) | releasedAt(X0,at_time($sum(X1,1))) | ? [X2 : event] : (happens(X2,at_time(X1)) & terminates(X2,X0,at_time(X1)))))),
% 18.76/2.94 inference(ennf_transformation,[],[f5])).
% 18.76/2.94 tff(f51,plain,(
% 18.76/2.94 ! [X0 : fluent,X1 : $int] : (holdsAt(X0,at_time($sum(X1,1))) | ~holdsAt(X0,at_time(X1)) | releasedAt(X0,at_time($sum(X1,1))) | ? [X2 : event] : (happens(X2,at_time(X1)) & terminates(X2,X0,at_time(X1))))),
% 18.76/2.94 inference(flattening,[],[f50])).
% 18.76/2.94 tff(f56,plain,(
% 18.76/2.94 ! [X0 : fluent,X1 : $int] : (~releasedAt(X0,at_time($sum(X1,1))) | (releasedAt(X0,at_time(X1)) | ? [X2 : event] : (happens(X2,at_time(X1)) & releases(X2,X0,at_time(X1)))))),
% 18.76/2.94 inference(ennf_transformation,[],[f8])).
% 18.76/2.94 tff(f57,plain,(
% 18.76/2.94 ! [X0 : fluent,X1 : $int] : (~releasedAt(X0,at_time($sum(X1,1))) | releasedAt(X0,at_time(X1)) | ? [X2 : event] : (happens(X2,at_time(X1)) & releases(X2,X0,at_time(X1))))),
% 18.76/2.94 inference(flattening,[],[f56])).
% 18.76/2.94 tff(f64,plain,(
% 18.76/2.94 ! [X0 : event,X1 : $int,X2 : fluent] : (~releasedAt(X2,at_time($sum(X1,1))) | (~happens(X0,at_time(X1)) | (~initiates(X0,X2,at_time(X1)) & ~terminates(X0,X2,at_time(X1)))))),
% 18.76/2.94 inference(ennf_transformation,[],[f12])).
% 18.76/2.94 tff(f65,plain,(
% 18.76/2.94 ! [X0 : event,X1 : $int,X2 : fluent] : (~releasedAt(X2,at_time($sum(X1,1))) | ~happens(X0,at_time(X1)) | (~initiates(X0,X2,at_time(X1)) & ~terminates(X0,X2,at_time(X1))))),
% 18.76/2.94 inference(flattening,[],[f64])).
% 18.76/2.94 tff(f70,plain,(
% 18.76/2.94 (~holdsAt(waterLevel(3),at_time(3)) & ~holdsAt(filling,at_time(4))) & holdsAt(filling,at_time(3))),
% 18.76/2.94 inference(ennf_transformation,[],[f33])).
% 18.76/2.94 tff(f71,plain,(
% 18.76/2.94 ~holdsAt(waterLevel(3),at_time(3)) & ~holdsAt(filling,at_time(4)) & holdsAt(filling,at_time(3))),
% 18.76/2.94 inference(flattening,[],[f70])).
% 18.76/2.94 tff(f72,definition,(
% 18.76/2.94 ! [X2 : $int,X0 : event,X1 : fluent] : (sP0(X2,X0,X1) <=> ? [X4 : $int] : (holdsAt(waterLevel(X4),at_time(X2)) & X0 = overflow & waterLevel(X4) = X1))),
% 18.76/2.94 introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction])).
% 18.76/2.94 tff(f73,definition,(
% 18.76/2.94 ! [X2 : $int,X0 : event,X1 : fluent] : (sP1(X2,X0,X1) <=> ? [X3 : $int] : (holdsAt(waterLevel(X3),at_time(X2)) & X0 = tapOff & X1 = waterLevel(X3)))),
% 18.76/2.94 introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction])).
% 18.76/2.94 tff(f74,plain,(
% 18.76/2.94 ! [X0 : event,X1 : fluent,X2 : $int] : (initiates(X0,X1,at_time(X2)) <=> ((X0 = tapOn & X1 = filling) | (X0 = overflow & X1 = spilling) | sP1(X2,X0,X1) | sP0(X2,X0,X1)))),
% 18.76/2.94 inference(definition_folding,[],[f46,f73,f72])).
% 18.76/2.94 tff(f81,plain,(
% 18.76/2.94 ! [X0 : fluent,X1 : $int] : (holdsAt(X0,at_time($sum(X1,1))) | ~holdsAt(X0,at_time(X1)) | releasedAt(X0,at_time($sum(X1,1))) | (happens(sK6(X0,X1),at_time(X1)) & terminates(sK6(X0,X1),X0,at_time(X1))))),
% 18.76/2.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(X2,sK6(X0,X1))],[f51])).
% 18.76/2.94 tff(f84,plain,(
% 18.76/2.94 ! [X0 : fluent,X1 : $int] : (~releasedAt(X0,at_time($sum(X1,1))) | releasedAt(X0,at_time(X1)) | (happens(sK9(X0,X1),at_time(X1)) & releases(sK9(X0,X1),X0,at_time(X1))))),
% 18.76/2.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(X2,sK9(X0,X1))],[f57])).
% 18.76/2.94 tff(f92,plain,(
% 18.76/2.94 ! [X0 : event,X1 : fluent,X2 : $int] : ((initiates(X0,X1,at_time(X2)) | ((tapOn != X0 | filling != X1) & (overflow != X0 | spilling != X1) & ~sP1(X2,X0,X1) & ~sP0(X2,X0,X1))) & (((X0 = tapOn & X1 = filling) | (X0 = overflow & X1 = spilling) | sP1(X2,X0,X1) | sP0(X2,X0,X1)) | ~initiates(X0,X1,at_time(X2))))),
% 18.76/2.94 inference(nnf_transformation,[],[f74])).
% 18.76/2.94 tff(f93,plain,(
% 18.76/2.94 ! [X0 : event,X1 : fluent,X2 : $int] : ((initiates(X0,X1,at_time(X2)) | ((tapOn != X0 | filling != X1) & (overflow != X0 | spilling != X1) & ~sP1(X2,X0,X1) & ~sP0(X2,X0,X1))) & ((X0 = tapOn & X1 = filling) | (X0 = overflow & X1 = spilling) | sP1(X2,X0,X1) | sP0(X2,X0,X1) | ~initiates(X0,X1,at_time(X2))))),
% 18.76/2.94 inference(flattening,[],[f92])).
% 18.76/2.94 tff(f96,plain,(
% 18.76/2.94 ! [X0 : event,X1 : fluent,X2 : $int] : ((releases(X0,X1,at_time(X2)) | ! [X3 : $int] : (tapOn != X0 | waterLevel(X3) != X1)) & (? [X3 : $int] : (X0 = tapOn & X1 = waterLevel(X3)) | ~releases(X0,X1,at_time(X2))))),
% 18.76/2.94 inference(nnf_transformation,[],[f22])).
% 18.76/2.94 tff(f97,plain,(
% 18.76/2.94 ! [X0 : event,X1 : fluent,X2 : $int] : ((releases(X0,X1,at_time(X2)) | ! [X3 : $int] : (tapOn != X0 | waterLevel(X3) != X1)) & (? [X4 : $int] : (X0 = tapOn & waterLevel(X4) = X1) | ~releases(X0,X1,at_time(X2))))),
% 18.76/2.94 inference(rectify,[],[f96])).
% 18.76/2.94 tff(f98,plain,(
% 18.76/2.94 ! [X0 : event,X1 : fluent,X2 : $int] : ((releases(X0,X1,at_time(X2)) | ! [X3 : $int] : (tapOn != X0 | waterLevel(X3) != X1)) & ((X0 = tapOn & waterLevel(sK12(X0,X1)) = X1) | ~releases(X0,X1,at_time(X2))))),
% 18.76/2.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(X4,sK12(X0,X1))],[f97])).
% 18.76/2.94 tff(f99,plain,(
% 18.76/2.94 ! [X0 : event,X1 : $int] : ((happens(X0,at_time(X1)) | ((tapOn != X0 | 0 != X1) & (~holdsAt(waterLevel(3),at_time(X1)) | ~holdsAt(filling,at_time(X1)) | overflow != X0))) & (((X0 = tapOn & X1 = 0) | (holdsAt(waterLevel(3),at_time(X1)) & holdsAt(filling,at_time(X1)) & X0 = overflow)) | ~happens(X0,at_time(X1))))),
% 18.76/2.94 inference(nnf_transformation,[],[f25])).
% 18.76/2.94 tff(f100,plain,(
% 18.76/2.94 ! [X0 : event,X1 : $int] : ((happens(X0,at_time(X1)) | ((tapOn != X0 | 0 != X1) & (~holdsAt(waterLevel(3),at_time(X1)) | ~holdsAt(filling,at_time(X1)) | overflow != X0))) & ((X0 = tapOn & X1 = 0) | (holdsAt(waterLevel(3),at_time(X1)) & holdsAt(filling,at_time(X1)) & X0 = overflow) | ~happens(X0,at_time(X1))))),
% 18.76/2.94 inference(flattening,[],[f99])).
% 18.76/2.94 tff(f113,plain,(
% 18.76/2.94 ( ! [X0 : fluent,X1 : $int] : (happens(sK6(X0,X1),at_time(X1)) | ~holdsAt(X0,at_time(X1)) | releasedAt(X0,at_time($sum(X1,1))) | holdsAt(X0,at_time($sum(X1,1)))) )),
% 18.76/2.94 inference(cnf_transformation,[],[f81])).
% 18.76/2.94 tff(f118,plain,(
% 18.76/2.94 ( ! [X0 : fluent,X1 : $int] : (releases(sK9(X0,X1),X0,at_time(X1)) | releasedAt(X0,at_time(X1)) | ~releasedAt(X0,at_time($sum(X1,1)))) )),
% 18.76/2.94 inference(cnf_transformation,[],[f84])).
% 18.76/2.94 tff(f119,plain,(
% 18.76/2.94 ( ! [X0 : fluent,X1 : $int] : (happens(sK9(X0,X1),at_time(X1)) | releasedAt(X0,at_time(X1)) | ~releasedAt(X0,at_time($sum(X1,1)))) )),
% 18.76/2.94 inference(cnf_transformation,[],[f84])).
% 18.76/2.94 tff(f124,plain,(
% 18.76/2.94 ( ! [X2 : fluent,X0 : event,X1 : $int] : (~releasedAt(X2,at_time($sum(X1,1))) | ~initiates(X0,X2,at_time(X1)) | ~happens(X0,at_time(X1))) )),
% 18.76/2.94 inference(cnf_transformation,[],[f65])).
% 18.76/2.94 tff(f126,plain,(
% 18.76/2.94 tapOn != overflow),
% 18.76/2.94 inference(cnf_transformation,[],[f14])).
% 18.76/2.94 tff(f148,plain,(
% 18.76/2.94 ( ! [X2 : $int,X0 : event,X1 : fluent] : (initiates(X0,X1,at_time(X2)) | tapOn != X0 | filling != X1) )),
% 18.76/2.94 inference(cnf_transformation,[],[f93])).
% 18.76/2.94 tff(f156,plain,(
% 18.76/2.94 ( ! [X2 : $int,X0 : event,X1 : fluent] : (~releases(X0,X1,at_time(X2)) | tapOn = X0) )),
% 18.76/2.94 inference(cnf_transformation,[],[f98])).
% 18.76/2.94 tff(f160,plain,(
% 18.76/2.94 ( ! [X0 : event,X1 : $int] : (~happens(X0,at_time(X1)) | overflow = X0 | 0 = X1) )),
% 18.76/2.94 inference(cnf_transformation,[],[f100])).
% 18.76/2.94 tff(f162,plain,(
% 18.76/2.94 ( ! [X0 : event,X1 : $int] : (holdsAt(waterLevel(3),at_time(X1)) | 0 = X1 | ~happens(X0,at_time(X1))) )),
% 18.76/2.94 inference(cnf_transformation,[],[f100])).
% 18.76/2.94 tff(f167,plain,(
% 18.76/2.94 ( ! [X0 : event,X1 : $int] : (happens(X0,at_time(X1)) | tapOn != X0 | 0 != X1) )),
% 18.76/2.94 inference(cnf_transformation,[],[f100])).
% 18.76/2.94 tff(f174,plain,(
% 18.76/2.94 holdsAt(filling,at_time(3))),
% 18.76/2.94 inference(cnf_transformation,[],[f71])).
% 18.76/2.94 tff(f175,plain,(
% 18.76/2.94 ~holdsAt(filling,at_time(4))),
% 18.76/2.94 inference(cnf_transformation,[],[f71])).
% 18.76/2.94 tff(f176,plain,(
% 18.76/2.94 ~holdsAt(waterLevel(3),at_time(3))),
% 18.76/2.94 inference(cnf_transformation,[],[f71])).
% 18.76/2.94 tff(f182,plain,(
% 18.76/2.94 ( ! [X2 : $int,X1 : fluent] : (initiates(tapOn,X1,at_time(X2)) | filling != X1) )),
% 18.76/2.94 inference(equality_resolution,[],[f148])).
% 18.76/2.94 tff(f183,plain,(
% 18.76/2.94 ( ! [X2 : $int] : (initiates(tapOn,filling,at_time(X2))) )),
% 18.76/2.94 inference(equality_resolution,[],[f182])).
% 18.76/2.94 tff(f193,plain,(
% 18.76/2.94 ( ! [X1 : $int] : (happens(tapOn,at_time(X1)) | 0 != X1) )),
% 18.76/2.94 inference(equality_resolution,[],[f167])).
% 18.76/2.94 tff(f194,plain,(
% 18.76/2.94 happens(tapOn,at_time(0))),
% 18.76/2.94 inference(equality_resolution,[],[f193])).
% 18.76/2.94 tff(f426,plain,(
% 18.76/2.94 ( ! [X0 : event] : (0 = 3 | ~happens(X0,at_time(3))) )),
% 18.76/2.94 inference(resolution,[],[f162,f176])).
% 18.76/2.94 tff(f429,plain,(
% 18.76/2.94 ( ! [X0 : event] : (~happens(X0,at_time(3))) )),
% 18.76/2.94 inference(evaluation,[],[f426])).
% 18.76/2.94 tff(f508,plain,(
% 18.76/2.94 ( ! [X2 : event,X0 : $int,X1 : fluent] : (~releasedAt(X1,at_time($sum(1,X0))) | ~initiates(X2,X1,at_time(X0)) | ~happens(X2,at_time(X0))) )),
% 18.76/2.94 inference(superposition,[],[f124,f34])).
% 18.76/2.94 tff(f549,plain,(
% 18.76/2.94 ( ! [X0 : fluent] : (releasedAt(X0,at_time(3)) | ~releasedAt(X0,at_time($sum(3,1)))) )),
% 18.76/2.94 inference(resolution,[],[f119,f429])).
% 18.76/2.94 tff(f552,plain,(
% 18.76/2.94 ( ! [X0 : fluent] : (releasedAt(X0,at_time(3)) | ~releasedAt(X0,at_time(4))) )),
% 18.76/2.94 inference(evaluation,[],[f549])).
% 18.76/2.94 tff(f566,plain,(
% 18.76/2.94 ( ! [X0 : fluent,X1 : $int] : (~releasedAt(X0,at_time($sum(X1,1))) | releasedAt(X0,at_time(X1)) | tapOn = sK9(X0,X1)) )),
% 18.76/2.94 inference(resolution,[],[f118,f156])).
% 18.76/2.94 tff(f646,plain,(
% 18.76/2.94 ( ! [X0 : fluent] : (~holdsAt(X0,at_time(3)) | releasedAt(X0,at_time($sum(3,1))) | holdsAt(X0,at_time($sum(3,1)))) )),
% 18.76/2.94 inference(resolution,[],[f113,f429])).
% 18.76/2.94 tff(f649,plain,(
% 18.76/2.94 ( ! [X0 : fluent] : (releasedAt(X0,at_time(4)) | ~holdsAt(X0,at_time(3)) | holdsAt(X0,at_time(4))) )),
% 18.76/2.94 inference(evaluation,[],[f646])).
% 18.76/2.94 tff(f2439,plain,(
% 18.76/2.94 ( ! [X0 : fluent,X1 : event] : (~initiates(X1,X0,at_time(0)) | ~releasedAt(X0,at_time(1)) | ~happens(X1,at_time(0))) )),
% 18.76/2.94 inference(superposition,[],[f508,f36])).
% 18.76/2.94 tff(f2518,plain,(
% 18.76/2.94 ( ! [X0 : $int,X1 : fluent] : (releasedAt(X1,at_time(X0)) | ~releasedAt(X1,at_time($sum(1,X0))) | tapOn = sK9(X1,X0)) )),
% 18.76/2.94 inference(superposition,[],[f566,f34])).
% 18.76/2.94 tff(f21781,plain,(
% 18.76/2.94 ~releasedAt(filling,at_time(1)) | ~happens(tapOn,at_time(0))),
% 18.76/2.94 inference(resolution,[],[f2439,f183])).
% 18.76/2.94 tff(f21789,plain,(
% 18.76/2.94 ~releasedAt(filling,at_time(1))),
% 18.76/2.94 inference(forward_subsumption_resolution,[],[f21781,f194])).
% 18.76/2.94 tff(f66587,plain,(
% 18.76/2.94 ~releasedAt(filling,at_time($sum(1,1))) | tapOn = sK9(filling,1)),
% 18.76/2.94 inference(resolution,[],[f2518,f21789])).
% 18.76/2.94 tff(f66588,plain,(
% 18.76/2.94 ~releasedAt(filling,at_time(2)) | tapOn = sK9(filling,1)),
% 18.76/2.94 inference(evaluation,[],[f66587])).
% 18.76/2.94 tff(f66594,definition,(
% 18.76/2.94 spl13_7 <=> tapOn = sK9(filling,1)),
% 18.76/2.94 introduced(definition,[new_symbols(definition,[spl13_7])],[avatar_definition])).
% 18.76/2.94 tff(f66595,plain,(
% 18.76/2.94 tapOn = sK9(filling,1) | ~spl13_7),
% 18.76/2.94 inference(avatar_component_clause,[],[f66594])).
% 18.76/2.94 tff(f66597,definition,(
% 18.76/2.94 spl13_8 <=> releasedAt(filling,at_time(2))),
% 18.76/2.94 introduced(definition,[new_symbols(definition,[spl13_8])],[avatar_definition])).
% 18.76/2.94 tff(f66598,plain,(
% 18.76/2.94 ~releasedAt(filling,at_time(2)) | spl13_8),
% 18.76/2.94 inference(avatar_component_clause,[],[f66597])).
% 18.76/2.94 tff(f66599,plain,(
% 18.76/2.94 spl13_7 | ~spl13_8),
% 18.76/2.94 inference(avatar_split_clause,[],[f66588,f66597,f66594])).
% 18.76/2.94 tff(f66619,plain,(
% 18.76/2.94 happens(tapOn,at_time(1)) | releasedAt(filling,at_time(1)) | ~releasedAt(filling,at_time($sum(1,1))) | ~spl13_7),
% 18.76/2.94 inference(superposition,[],[f119,f66595])).
% 18.76/2.94 tff(f66620,plain,(
% 18.76/2.94 happens(tapOn,at_time(1)) | releasedAt(filling,at_time(1)) | ~releasedAt(filling,at_time(2)) | ~spl13_7),
% 18.76/2.94 inference(evaluation,[],[f66619])).
% 18.76/2.94 tff(f66622,plain,(
% 18.76/2.94 happens(tapOn,at_time(1)) | ~releasedAt(filling,at_time(2)) | ~spl13_7),
% 18.76/2.94 inference(forward_subsumption_resolution,[],[f66620,f21789])).
% 18.76/2.94 tff(f66625,definition,(
% 18.76/2.94 spl13_13 <=> happens(tapOn,at_time(1))),
% 18.76/2.94 introduced(definition,[new_symbols(definition,[spl13_13])],[avatar_definition])).
% 18.76/2.94 tff(f66626,plain,(
% 18.76/2.94 happens(tapOn,at_time(1)) | ~spl13_13),
% 18.76/2.94 inference(avatar_component_clause,[],[f66625])).
% 18.76/2.94 tff(f66627,plain,(
% 18.76/2.94 ~spl13_8 | spl13_13 | ~spl13_7),
% 18.76/2.94 inference(avatar_split_clause,[],[f66622,f66594,f66625,f66597])).
% 18.76/2.94 tff(f66650,plain,(
% 18.76/2.94 ~releasedAt(filling,at_time($sum(1,2))) | tapOn = sK9(filling,2) | spl13_8),
% 18.76/2.94 inference(resolution,[],[f66598,f2518])).
% 18.76/2.94 tff(f66651,plain,(
% 18.76/2.94 ~releasedAt(filling,at_time(3)) | tapOn = sK9(filling,2) | spl13_8),
% 18.76/2.94 inference(evaluation,[],[f66650])).
% 18.76/2.94 tff(f66653,definition,(
% 18.76/2.94 spl13_15 <=> tapOn = sK9(filling,2)),
% 18.76/2.94 introduced(definition,[new_symbols(definition,[spl13_15])],[avatar_definition])).
% 18.76/2.94 tff(f66654,plain,(
% 18.76/2.94 tapOn = sK9(filling,2) | ~spl13_15),
% 18.76/2.94 inference(avatar_component_clause,[],[f66653])).
% 18.76/2.94 tff(f66656,definition,(
% 18.76/2.94 spl13_16 <=> releasedAt(filling,at_time(3))),
% 18.76/2.94 introduced(definition,[new_symbols(definition,[spl13_16])],[avatar_definition])).
% 18.76/2.94 tff(f66657,plain,(
% 18.76/2.94 ~releasedAt(filling,at_time(3)) | spl13_16),
% 18.76/2.94 inference(avatar_component_clause,[],[f66656])).
% 18.76/2.94 tff(f66658,plain,(
% 18.76/2.94 spl13_15 | ~spl13_16 | spl13_8),
% 18.76/2.94 inference(avatar_split_clause,[],[f66651,f66597,f66656,f66653])).
% 18.76/2.94 tff(f66970,plain,(
% 18.76/2.94 happens(tapOn,at_time(2)) | releasedAt(filling,at_time(2)) | ~releasedAt(filling,at_time($sum(2,1))) | ~spl13_15),
% 18.76/2.94 inference(superposition,[],[f119,f66654])).
% 18.76/2.94 tff(f66971,plain,(
% 18.76/2.94 happens(tapOn,at_time(2)) | releasedAt(filling,at_time(2)) | ~releasedAt(filling,at_time(3)) | ~spl13_15),
% 18.76/2.94 inference(evaluation,[],[f66970])).
% 18.76/2.94 tff(f66976,definition,(
% 18.76/2.94 spl13_20 <=> happens(tapOn,at_time(2))),
% 18.76/2.94 introduced(definition,[new_symbols(definition,[spl13_20])],[avatar_definition])).
% 18.76/2.94 tff(f66977,plain,(
% 18.76/2.94 happens(tapOn,at_time(2)) | ~spl13_20),
% 18.76/2.94 inference(avatar_component_clause,[],[f66976])).
% 18.76/2.94 tff(f67179,plain,(
% 18.76/2.94 ~releasedAt(filling,at_time(4)) | spl13_16),
% 18.76/2.94 inference(resolution,[],[f66657,f552])).
% 18.76/2.94 tff(f67186,definition,(
% 18.76/2.94 spl13_23 <=> releasedAt(filling,at_time(4))),
% 18.76/2.94 introduced(definition,[new_symbols(definition,[spl13_23])],[avatar_definition])).
% 18.76/2.94 tff(f67187,plain,(
% 18.76/2.94 ~releasedAt(filling,at_time(4)) | spl13_23),
% 18.76/2.94 inference(avatar_component_clause,[],[f67186])).
% 18.76/2.94 tff(f67189,plain,(
% 18.76/2.94 ~spl13_23 | spl13_16),
% 18.76/2.94 inference(avatar_split_clause,[],[f67179,f66656,f67186])).
% 18.76/2.94 tff(f67385,plain,(
% 18.76/2.94 ~holdsAt(filling,at_time(3)) | holdsAt(filling,at_time(4)) | spl13_23),
% 18.76/2.94 inference(resolution,[],[f67187,f649])).
% 18.76/2.94 tff(f67398,plain,(
% 18.76/2.94 holdsAt(filling,at_time(4)) | spl13_23),
% 18.76/2.94 inference(forward_subsumption_resolution,[],[f67385,f174])).
% 18.76/2.94 tff(f67399,plain,(
% 18.76/2.94 $false | spl13_23),
% 18.76/2.94 inference(forward_subsumption_resolution,[],[f67398,f175])).
% 18.76/2.94 tff(f67400,plain,(
% 18.76/2.94 spl13_23),
% 18.76/2.94 inference(avatar_contradiction_clause,[],[f67399])).
% 18.76/2.94 tff(f67401,plain,(
% 18.76/2.94 tapOn = overflow | 0 = 2 | ~spl13_20),
% 18.76/2.94 inference(resolution,[],[f66977,f160])).
% 18.76/2.94 tff(f67403,plain,(
% 18.76/2.94 tapOn = overflow | ~spl13_20),
% 18.76/2.94 inference(evaluation,[],[f67401])).
% 18.76/2.94 tff(f67404,plain,(
% 18.76/2.94 $false | ~spl13_20),
% 18.76/2.94 inference(forward_subsumption_resolution,[],[f67403,f126])).
% 18.76/2.94 tff(f67405,plain,(
% 18.76/2.94 ~spl13_20),
% 18.76/2.94 inference(avatar_contradiction_clause,[],[f67404])).
% 18.76/2.94 tff(f67407,plain,(
% 18.76/2.94 ~spl13_16 | spl13_8 | spl13_20 | ~spl13_15),
% 18.76/2.94 inference(avatar_split_clause,[],[f66971,f66653,f66976,f66597,f66656])).
% 18.76/2.94 tff(f67604,plain,(
% 18.76/2.94 tapOn = overflow | 0 = 1 | ~spl13_13),
% 18.76/2.94 inference(resolution,[],[f66626,f160])).
% 18.76/2.94 tff(f67606,plain,(
% 18.76/2.94 tapOn = overflow | ~spl13_13),
% 18.76/2.94 inference(evaluation,[],[f67604])).
% 18.76/2.94 tff(f67607,plain,(
% 18.76/2.94 $false | ~spl13_13),
% 18.76/2.94 inference(forward_subsumption_resolution,[],[f67606,f126])).
% 18.76/2.94 tff(f67608,plain,(
% 18.76/2.94 ~spl13_13),
% 18.76/2.94 inference(avatar_contradiction_clause,[],[f67607])).
% 18.76/2.94 cnf(s7, plain, spl13_7 | ~spl13_8, inference(sat_conversion,[],[f66599])).
% 18.76/2.94 cnf(s10, plain, ~spl13_7 | ~spl13_8 | spl13_13, inference(sat_conversion,[],[f66627])).
% 18.76/2.94 cnf(s12, plain, spl13_8 | spl13_15 | ~spl13_16, inference(sat_conversion,[],[f66658])).
% 18.76/2.94 cnf(s19, plain, spl13_16 | ~spl13_23, inference(sat_conversion,[],[f67189])).
% 18.76/2.94 cnf(s22, plain, spl13_23, inference(sat_conversion,[],[f67400])).
% 18.76/2.94 cnf(s23, plain, ~spl13_20, inference(sat_conversion,[],[f67405])).
% 18.76/2.94 cnf(s24, plain, spl13_8 | ~spl13_15 | ~spl13_16 | spl13_20, inference(sat_conversion,[],[f67407])).
% 18.76/2.94 cnf(s26, plain, ~spl13_13, inference(sat_conversion,[],[f67608])).
% 18.76/2.94 cnf(s27, plain, spl13_16, inference(rat,[],[s19,s22])).
% 18.76/2.94 cnf(s31, plain, spl13_8 | spl13_15, inference(rat,[],[s12,s27])).
% 18.76/2.94 cnf(s32, plain, ~spl13_7 | ~spl13_8, inference(rat,[],[s10,s26])).
% 18.76/2.94 cnf(s33, plain, spl13_8, inference(rat,[],[s31,s24,s27,s23])).
% 18.76/2.94 cnf(s34, plain, ~spl13_7, inference(rat,[],[s32,s33])).
% 18.76/2.94 cnf(s35, plain, $false, inference(rat,[],[s7,s33,s34])).
% 18.76/2.94 tff(f67609,plain,(
% 18.76/2.94 $false),
% 18.76/2.94 inference(avatar_sat_refutation,[],[s35])).
% 18.76/2.94 % SZS output end Proof for theBenchmark
% 18.76/2.94 % (3162626)------------------------------
% 18.76/2.94 % (3162626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.76/2.94 % (3162626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.76/2.94 % (3162626)CaDiCaL version: 2.1.3
% 18.76/2.94 % (3162626)Termination reason: Refutation
% 18.76/2.94 % (3162626)Time elapsed: 1.714 s
% 18.76/2.94 % (3162626)Peak memory usage: 28 MB
% 18.76/2.94 % (3162626)Instructions burned: 3022 (million)
% 18.76/2.94 % (3162532)Success in time 2.699 s
% 18.76/2.94 % Vampire exiting
%------------------------------------------------------------------------------