%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR031+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n017.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:44:26 AM UTC 2026
% Result : Theorem 40.26s 7.53s
% Output : Refutation 40.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 5
% Syntax : Number of formulae : 22 ( 10 unt; 0 def)
% Number of atoms : 34 ( 0 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 28 ( 16 ~; 9 |; 1 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 2 ( 2 usr; 2 con; 0-0 aty)
% Number of variables : 20 ( 20 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4028,axiom,
! [X0] :
~ ( collection(X0)
& individual(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+3.ax',ax3_4028) ).
fof(f7072,axiom,
! [X0,X1] :
( disjointwith(X0,X1)
=> collection(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+3.ax',ax3_7072) ).
fof(f20191,axiom,
individual(c_tptptptpcol_16_8398),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+3.ax',ax3_20191) ).
fof(f41386,axiom,
! [X0,X1] :
( disjointwith(X0,X1)
=> disjointwith(X1,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+3.ax',ax3_41386) ).
fof(f44217,conjecture,
~ disjointwith(c_tptptptpcol_16_8398,c_tptpcol_16_18488),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',query181) ).
fof(f44218,negated_conjecture,
~ ~ disjointwith(c_tptptptpcol_16_8398,c_tptpcol_16_18488),
inference(negated_conjecture,[status(cth)],[f44217]) ).
fof(f44219,plain,
disjointwith(c_tptptptpcol_16_8398,c_tptpcol_16_18488),
inference(flattening,[],[f44218]) ).
fof(f47682,plain,
! [X0] :
( ~ collection(X0)
| ~ individual(X0) ),
inference(ennf_transformation,[],[f4028]) ).
fof(f48441,plain,
! [X0,X1] :
( collection(X1)
| ~ disjointwith(X0,X1) ),
inference(ennf_transformation,[],[f7072]) ).
fof(f64064,plain,
! [X0,X1] :
( disjointwith(X1,X0)
| ~ disjointwith(X0,X1) ),
inference(ennf_transformation,[],[f41386]) ).
fof(f70265,plain,
! [X0] :
( ~ individual(X0)
| ~ collection(X0) ),
inference(cnf_transformation,[],[f47682]) ).
fof(f73248,plain,
! [X0,X1] :
( ~ disjointwith(X0,X1)
| collection(X1) ),
inference(cnf_transformation,[],[f48441]) ).
fof(f86126,plain,
individual(c_tptptptpcol_16_8398),
inference(cnf_transformation,[],[f20191]) ).
fof(f105733,plain,
! [X0,X1] :
( ~ disjointwith(X0,X1)
| disjointwith(X1,X0) ),
inference(cnf_transformation,[],[f64064]) ).
fof(f108041,plain,
disjointwith(c_tptptptpcol_16_8398,c_tptpcol_16_18488),
inference(cnf_transformation,[],[f44219]) ).
fof(f108868,plain,
! [X0] :
( collection(X0)
| individual(X0) ),
inference(consistent_polarity_flipping,[],[f70265]) ).
fof(f109519,plain,
! [X0,X1] :
( ~ collection(X1)
| ~ disjointwith(X0,X1) ),
inference(consistent_polarity_flipping,[],[f73248]) ).
fof(f112274,plain,
~ individual(c_tptptptpcol_16_8398),
inference(consistent_polarity_flipping,[],[f86126]) ).
fof(f146457,plain,
! [X0,X1] :
( ~ disjointwith(X0,X1)
| individual(X1) ),
inference(resolution,[],[f109519,f108868]) ).
fof(f147830,plain,
disjointwith(c_tptpcol_16_18488,c_tptptptpcol_16_8398),
inference(resolution,[],[f105733,f108041]) ).
fof(f197277,plain,
individual(c_tptptptpcol_16_8398),
inference(resolution,[],[f146457,f147830]) ).
fof(f197278,plain,
$false,
inference(forward_subsumption_resolution,[],[f197277,f112274]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : CSR031+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.10 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.28/0.31 % Computer : n017.cluster.edu
% 0.28/0.31 % Model : x86_64 x86_64
% 0.28/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.28/0.31 % Memory : 8046.5625MB
% 0.28/0.31 % OS : Linux 6.8.0-71-generic
% 0.28/0.32 % CPULimit : 300
% 0.28/0.32 % WCLimit : 300
% 0.28/0.32 % DateTime : Mon Sep 28 22:07:06 UTC 2026
% 0.28/0.32 % CPUTime :
% 0.28/0.32 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.28/0.38 Running first-order model finding
% 0.28/0.38 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
% 18.53/7.44 % (4092674)Will run a generic schedule for satisfiability detection.
% 18.53/7.44 % (4092681)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=174553877:i=88024:add=on:rawr=on_2984 on theBenchmark for (2984ds/88024Mi)
% 18.53/7.44 % (4092680)% WARNING: option uhcvi not known.
% 18.53/7.44 % (4092679)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3152222359_2984 on theBenchmark for (2984ds/0Mi)
% 18.53/7.44 % (4092680)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2421006843:i=135531:add=off:rawr=on_2984 on theBenchmark for (2984ds/135531Mi)
% 18.53/7.44 % (4092682)dis+10_1_sil=32000:sp=arity:random_seed=3973596317:i=103:fgj=on_2984 on theBenchmark for (2984ds/103Mi)
% 18.53/7.44 % (4092683)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1189331832:i=116_2984 on theBenchmark for (2984ds/116Mi)
% 18.53/7.44 % (4092684)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3728501234:i=131_2984 on theBenchmark for (2984ds/131Mi)
% 18.53/7.44 % (4092685)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3331608988:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2984 on theBenchmark for (2984ds/159Mi)
% 18.53/7.44 % (4092682)Instruction limit reached!
% 18.53/7.44 % (4092682)------------------------------
% 18.53/7.44 % (4092682)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.53/7.44 % (4092682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.53/7.44 % (4092682)CaDiCaL version: 2.1.3
% 18.53/7.44 % (4092682)Termination reason: Instruction limit
% 18.53/7.44 % (4092682)Termination phase: Preprocessing 2
% 18.53/7.44 % (4092682)Time elapsed: 0.147 s
% 18.53/7.44 % (4092682)Peak memory usage: 61 MB
% 18.53/7.44 % (4092682)Instructions burned: 104 (million)
% 18.53/7.44 % (4092683)Instruction limit reached!
% 18.53/7.44 % (4092683)------------------------------
% 18.53/7.44 % (4092683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.53/7.44 % (4092683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.53/7.44 % (4092683)CaDiCaL version: 2.1.3
% 18.53/7.44 % (4092683)Termination reason: Instruction limit
% 18.53/7.44 % (4092683)Termination phase: Preprocessing 2
% 18.53/7.44 % (4092683)Time elapsed: 0.165 s
% 18.53/7.44 % (4092683)Peak memory usage: 61 MB
% 18.53/7.44 % (4092683)Instructions burned: 116 (million)
% 18.53/7.44 % (4092684)Instruction limit reached!
% 18.53/7.44 % (4092684)------------------------------
% 18.53/7.44 % (4092684)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.53/7.44 % (4092684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.53/7.44 % (4092684)CaDiCaL version: 2.1.3
% 18.53/7.44 % (4092684)Termination reason: Instruction limit
% 18.53/7.44 % (4092684)Termination phase: Preprocessing 2
% 18.53/7.44 % (4092684)Time elapsed: 0.178 s
% 18.53/7.44 % (4092684)Peak memory usage: 61 MB
% 18.53/7.44 % (4092684)Instructions burned: 131 (million)
% 18.53/7.44 % (4092693)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3955916303:i=714:nm=2_2982 on theBenchmark for (2982ds/714Mi)
% 18.53/7.44 % (4092694)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3175755409:i=131:bd=preordered:fsd=on_2981 on theBenchmark for (2981ds/131Mi)
% 18.53/7.44 % (4092695)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=2562517555:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2981 on theBenchmark for (2981ds/684Mi)
% 18.53/7.44 % (4092685)Instruction limit reached!
% 18.53/7.44 % (4092685)------------------------------
% 18.53/7.44 % (4092685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.53/7.44 % (4092685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.53/7.44 % (4092685)CaDiCaL version: 2.1.3
% 18.53/7.44 % (4092685)Termination reason: Instruction limit
% 18.53/7.44 % (4092685)Termination phase: Naming
% 18.53/7.44 % (4092685)Time elapsed: 0.209 s
% 18.53/7.44 % (4092685)Peak memory usage: 62 MB
% 18.53/7.44 % (4092685)Instructions burned: 160 (million)
% 18.53/7.44 % (4092699)ott-21_1_sil=16000:fs=off:random_seed=4008000387:i=180:av=off:fsr=off_2981 on theBenchmark for (2981ds/180Mi)
% 18.53/7.44 % (4092694)Instruction limit reached!
% 18.53/7.44 % (4092694)------------------------------
% 18.53/7.44 % (4092694)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.53/7.44 % (4092694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.26/7.53 % (4092694)CaDiCaL version: 2.1.3
% 40.26/7.53 % (4092694)Termination reason: Instruction limit
% 40.26/7.53 % (4092694)Termination phase: Preprocessing 2
% 40.26/7.53 % (4092694)Time elapsed: 0.170 s
% 40.26/7.53 % (4092694)Peak memory usage: 61 MB
% 40.26/7.53 % (4092694)Instructions burned: 131 (million)
% 40.26/7.53 % (4092701)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1042950922:i=477:bd=all_2979 on theBenchmark for (2979ds/477Mi)
% 40.26/7.53 % (4092699)Instruction limit reached!
% 40.26/7.53 % (4092699)------------------------------
% 40.26/7.53 % (4092699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.26/7.53 % (4092699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.26/7.53 % (4092699)CaDiCaL version: 2.1.3
% 40.26/7.53 % (4092699)Termination reason: Instruction limit
% 40.26/7.53 % (4092699)Termination phase: Preprocessing 3
% 40.26/7.53 % (4092699)Time elapsed: 0.209 s
% 40.26/7.53 % (4092699)Peak memory usage: 62 MB
% 40.26/7.53 % (4092699)Instructions burned: 180 (million)
% 40.26/7.53 % (4092703)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1764309736:fmbsr=1.3:i=865:ins=25_2978 on theBenchmark for (2978ds/865Mi)
% 40.26/7.53 % (4092693)Instruction limit reached!
% 40.26/7.53 % (4092693)------------------------------
% 40.26/7.53 % (4092693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.26/7.53 % (4092693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.26/7.53 % (4092693)CaDiCaL version: 2.1.3
% 40.26/7.53 % (4092693)Termination reason: Instruction limit
% 40.26/7.53 % (4092693)Termination phase: Finite model building preprocessing
% 40.26/7.53 % (4092693)Time elapsed: 0.713 s
% 40.26/7.53 % (4092693)Peak memory usage: 68 MB
% 40.26/7.53 % (4092693)Instructions burned: 714 (million)
% 40.26/7.53 % (4092695)Instruction limit reached!
% 40.26/7.53 % (4092695)------------------------------
% 40.26/7.53 % (4092695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.26/7.53 % (4092695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.26/7.53 % (4092695)CaDiCaL version: 2.1.3
% 40.26/7.53 % (4092695)Termination reason: Instruction limit
% 40.26/7.53 % (4092695)Termination phase: Property scanning
% 40.26/7.53 % (4092695)Time elapsed: 0.734 s
% 40.26/7.53 % (4092695)Peak memory usage: 73 MB
% 40.26/7.53 % (4092695)Instructions burned: 684 (million)
% 40.26/7.53 % (4092701)Instruction limit reached!
% 40.26/7.53 % (4092701)------------------------------
% 40.26/7.53 % (4092701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.26/7.53 % (4092701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.26/7.53 % (4092701)CaDiCaL version: 2.1.3
% 40.26/7.53 % (4092701)Termination reason: Instruction limit
% 40.26/7.53 % (4092701)Termination phase: Property scanning
% 40.26/7.53 % (4092701)Time elapsed: 0.518 s
% 40.26/7.53 % (4092701)Peak memory usage: 67 MB
% 40.26/7.53 % (4092701)Instructions burned: 478 (million)
% 40.26/7.53 % (4092705)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3872143187:i=1179_2974 on theBenchmark for (2974ds/1179Mi)
% 40.26/7.53 % (4092706)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1685994675:i=889:ins=1_2973 on theBenchmark for (2973ds/889Mi)
% 40.26/7.53 % (4092707)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=2368642747:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2973 on theBenchmark for (2973ds/692Mi)
% 40.26/7.53 % (4092703)Instruction limit reached!
% 40.26/7.53 % (4092703)------------------------------
% 40.26/7.53 % (4092703)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.26/7.53 % (4092703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.26/7.53 % (4092703)CaDiCaL version: 2.1.3
% 40.26/7.53 % (4092703)Termination reason: Instruction limit
% 40.26/7.53 % (4092703)Termination phase: Finite model building preprocessing
% 40.26/7.53 % (4092703)Time elapsed: 0.873 s
% 40.26/7.53 % (4092703)Peak memory usage: 86 MB
% 40.26/7.53 % (4092703)Instructions burned: 865 (million)
% 40.26/7.53 % (4092711)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3459692594:i=879:kws=inv_precedence:fsr=off_2969 on theBenchmark for (2969ds/879Mi)
% 40.26/7.53 % (4092707)Instruction limit reached!
% 40.26/7.53 % (4092707)------------------------------
% 40.26/7.53 % (4092707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.26/7.53 % (4092707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.26/7.53 % (4092707)CaDiCaL version: 2.1.3
% 40.26/7.53 % (4092707)Termination reason: Instruction limit
% 40.26/7.53 % (4092707)Termination phase: Property scanning
% 40.26/7.53 % (4092707)Time elapsed: 0.758 s
% 40.26/7.53 % (4092707)Peak memory usage: 76 MB
% 40.26/7.53 % (4092707)Instructions burned: 692 (million)
% 40.26/7.53 % (4092713)fmb+10_1_sil=64000:random_seed=640429658:i=22061:nm=2:gsp=on_2965 on theBenchmark for (2965ds/22061Mi)
% 40.26/7.53 % (4092706)Instruction limit reached!
% 40.26/7.53 % (4092706)------------------------------
% 40.26/7.53 % (4092706)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.26/7.53 % (4092706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.26/7.53 % (4092706)CaDiCaL version: 2.1.3
% 40.26/7.53 % (4092706)Termination reason: Instruction limit
% 40.26/7.53 % (4092706)Termination phase: Finite model building preprocessing
% 40.26/7.53 % (4092706)Time elapsed: 0.919 s
% 40.26/7.53 % (4092706)Peak memory usage: 86 MB
% 40.26/7.53 % (4092706)Instructions burned: 890 (million)
% 40.26/7.53 % (4092715)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2722290882:i=9515:nm=5_2964 on theBenchmark for (2964ds/9515Mi)
% 40.26/7.53 % (4092705)Instruction limit reached!
% 40.26/7.53 % (4092705)------------------------------
% 40.26/7.53 % (4092705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.26/7.53 % (4092705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.26/7.53 % (4092705)CaDiCaL version: 2.1.3
% 40.26/7.53 % (4092705)Termination reason: Instruction limit
% 40.26/7.53 % (4092705)Termination phase: Saturation
% 40.26/7.53 % (4092705)Time elapsed: 1.196 s
% 40.26/7.53 % (4092705)Peak memory usage: 81 MB
% 40.26/7.53 % (4092705)Instructions burned: 1179 (million)
% 40.26/7.53 % (4092717)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2047149970:fmbsr=1.7:i=920_2961 on theBenchmark for (2961ds/920Mi)
% 40.26/7.53 % (4092711)Instruction limit reached!
% 40.26/7.53 % (4092711)------------------------------
% 40.26/7.53 % (4092711)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.26/7.53 % (4092711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.26/7.53 % (4092711)CaDiCaL version: 2.1.3
% 40.26/7.53 % (4092711)Termination reason: Instruction limit
% 40.26/7.53 % (4092711)Termination phase: Saturation
% 40.26/7.53 % (4092711)Time elapsed: 0.945 s
% 40.26/7.53 % (4092711)Peak memory usage: 91 MB
% 40.26/7.53 % (4092711)Instructions burned: 879 (million)
% 40.26/7.53 % (4092719)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2695542932:i=5131_2958 on theBenchmark for (2958ds/5131Mi)
% 40.26/7.53 % TRYING [1]
% 40.26/7.53 % TRYING [2]
% 40.26/7.53 % (4092717)Instruction limit reached!
% 40.26/7.53 % (4092717)------------------------------
% 40.26/7.53 % (4092717)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.26/7.53 % (4092717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.26/7.53 % (4092717)CaDiCaL version: 2.1.3
% 40.26/7.53 % (4092717)Termination reason: Instruction limit
% 40.26/7.53 % (4092717)Termination phase: Finite model building preprocessing
% 40.26/7.53 % (4092717)Time elapsed: 0.923 s
% 40.26/7.53 % (4092717)Peak memory usage: 78 MB
% 40.26/7.53 % (4092717)Instructions burned: 921 (million)
% 40.26/7.53 % (4092721)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3037525091:i=1472:ins=7:fdi=8:gsp=on_2951 on theBenchmark for (2951ds/1472Mi)
% 40.26/7.53 % TRYING [3]
% 40.26/7.53 % TRYING [1]
% 40.26/7.53 % TRYING [20]
% 40.26/7.53 % (4092721)Instruction limit reached!
% 40.26/7.53 % (4092721)------------------------------
% 40.26/7.53 % (4092721)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.26/7.53 % (4092721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.26/7.53 % (4092721)CaDiCaL version: 2.1.3
% 40.26/7.53 % (4092721)Termination reason: Instruction limit
% 40.26/7.53 % (4092721)Termination phase: Saturation
% 40.26/7.53 % (4092721)Time elapsed: 1.373 s
% 40.26/7.53 % (4092721)Peak memory usage: 82 MB
% 40.26/7.53 % (4092721)Instructions burned: 1472 (million)
% 40.26/7.53 % (4092723)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2792803595:i=6324_2937 on theBenchmark for (2937ds/6324Mi)
% 40.26/7.53 % (4092680) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-4092674-4092680"...
% 40.26/7.53 % (4092680)...printing done.
% 40.26/7.53 % (4092680)Refutation found. Thanks to Tanya!
% 40.26/7.53 % SZS status Theorem for theBenchmark
% 40.26/7.53 % SZS output start Proof for theBenchmark
% See solution above
% 40.26/7.53 % (4092680)------------------------------
% 40.26/7.53 % (4092680)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.26/7.53 % (4092680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.26/7.53 % (4092680)CaDiCaL version: 2.1.3
% 40.26/7.53 % (4092680)Termination reason: Refutation
% 40.26/7.53 % (4092680)Time elapsed: 5.232 s
% 40.26/7.53 % (4092680)Peak memory usage: 128 MB
% 40.26/7.53 % (4092680)Instructions burned: 4910 (million)
% 40.26/7.53 % (4092674)Success in time 7.047 s
% 40.26/7.53 % Vampire exiting
%------------------------------------------------------------------------------