%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LAT005-6 : TPTP v9.3.1. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n014.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 11:47:39 AM UTC 2026
% Result : Unsatisfiable 47.81s 7.28s
% Output : Refutation 47.81s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 19
% Syntax : Number of formulae : 59 ( 35 unt; 0 def)
% Number of atoms : 104 ( 0 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 91 ( 46 ~; 45 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 11 con; 0-0 aty)
% Number of variables : 74 ( 74 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f7,axiom,
! [X2,X0,X1] :
( ~ meet(X0,X1,X2)
| meet(X1,X0,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LAT002-0.ax',commutativity_of_meet) ).
fof(f8,axiom,
! [X2,X0,X1] :
( ~ join(X0,X1,X2)
| join(X1,X0,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LAT002-0.ax',commutativity_of_join) ).
fof(f9,axiom,
! [X2,X0,X1] :
( ~ meet(X0,X1,X2)
| join(X0,X2,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LAT002-0.ax',absorbtion1) ).
fof(f10,axiom,
! [X2,X0,X1] :
( ~ join(X0,X1,X2)
| meet(X0,X2,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LAT002-0.ax',absorbtion2) ).
fof(f11,axiom,
! [X2,X3,X0,X1,X4,X5] :
( ~ meet(X0,X4,X5)
| ~ meet(X1,X3,X4)
| ~ meet(X0,X1,X2)
| meet(X2,X3,X5) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LAT002-0.ax',associativity_of_meet1) ).
fof(f12,axiom,
! [X2,X3,X0,X1,X4,X5] :
( ~ meet(X2,X3,X5)
| ~ meet(X1,X3,X4)
| ~ meet(X0,X1,X2)
| meet(X0,X4,X5) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LAT002-0.ax',associativity_of_meet2) ).
fof(f16,axiom,
! [X2,X3,X0,X1,X4,X5] :
( ~ meet(X0,X1,X0)
| ~ join(X0,X2,X3)
| ~ meet(X2,X1,X4)
| ~ join(X0,X4,X5)
| meet(X1,X3,X5) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LAT002-0.ax',modularity2) ).
fof(f22,axiom,
! [X0] : join(X0,n0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',join_x_and_0) ).
fof(f23,axiom,
! [X0] : meet(X0,n0,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meet_x_and_0) ).
fof(f26,axiom,
! [X2,X3,X0,X1,X4,X5] :
( ~ meet(X0,X1,X1)
| ~ join(X2,X1,X3)
| ~ meet(X0,X2,X4)
| ~ join(X1,X4,X5)
| meet(X0,X3,X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',modularity4) ).
fof(f27,negated_conjecture,
meet(a,b,c),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meet_a_and_b) ).
fof(f29,negated_conjecture,
meet(c,r2,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meet_c_and_r2) ).
fof(f30,negated_conjecture,
meet(r2,b,e),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meet_r2_and_b) ).
fof(f31,negated_conjecture,
join(a,b,c2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',join_a_and_b) ).
fof(f33,negated_conjecture,
meet(c2,r1,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meet_c2_and_r1) ).
fof(f34,negated_conjecture,
meet(r2,a,d),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meet_r2_and_a) ).
fof(f35,negated_conjecture,
join(r1,e,a2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',join_r1_and_e) ).
fof(f36,negated_conjecture,
join(r1,d,b2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',join_r1_and_d) ).
fof(f37,negated_conjecture,
~ meet(a2,b2,r1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meet_a2_and_b2) ).
fof(f45,plain,
meet(b,r2,e),
inference(resolution,[],[f7,f30]) ).
fof(f46,plain,
meet(a,r2,d),
inference(resolution,[],[f7,f34]) ).
fof(f47,plain,
meet(r1,c2,n0),
inference(resolution,[],[f7,f33]) ).
fof(f54,plain,
join(b,a,c2),
inference(resolution,[],[f8,f31]) ).
fof(f57,plain,
join(e,r1,a2),
inference(resolution,[],[f8,f35]) ).
fof(f58,plain,
join(d,r1,b2),
inference(resolution,[],[f8,f36]) ).
fof(f79,plain,
meet(a,c2,a),
inference(resolution,[],[f10,f31]) ).
fof(f83,plain,
meet(r1,b2,r1),
inference(resolution,[],[f10,f36]) ).
fof(f84,plain,
join(a,d,a),
inference(resolution,[],[f46,f9]) ).
fof(f87,plain,
! [X2,X3,X0,X1] :
( ~ meet(X0,X1,n0)
| ~ meet(X2,X0,X3)
| meet(X3,X1,n0) ),
inference(resolution,[],[f11,f23]) ).
fof(f96,plain,
! [X2,X0,X1] :
( ~ meet(X0,X1,b)
| ~ meet(r2,X0,X2)
| meet(X2,X1,e) ),
inference(resolution,[],[f11,f30]) ).
fof(f97,plain,
! [X2,X0,X1] :
( ~ meet(X0,X1,a)
| ~ meet(r2,X0,X2)
| meet(X2,X1,d) ),
inference(resolution,[],[f11,f34]) ).
fof(f112,plain,
! [X2,X0,X1] :
( ~ meet(X2,X0,c)
| ~ meet(X0,r2,X1)
| meet(X2,X1,n0) ),
inference(resolution,[],[f12,f29]) ).
fof(f118,plain,
meet(b,c2,b),
inference(resolution,[],[f54,f10]) ).
fof(f205,plain,
meet(b2,r1,r1),
inference(resolution,[],[f83,f7]) ).
fof(f228,plain,
join(d,a,a),
inference(resolution,[],[f84,f8]) ).
fof(f232,plain,
! [X0] :
( ~ meet(r2,a,X0)
| meet(X0,c2,d) ),
inference(resolution,[],[f97,f79]) ).
fof(f233,plain,
! [X0] :
( ~ meet(r2,b,X0)
| meet(X0,c2,e) ),
inference(resolution,[],[f118,f96]) ).
fof(f264,plain,
! [X0] :
( ~ meet(b,r2,X0)
| meet(a,X0,n0) ),
inference(resolution,[],[f112,f27]) ).
fof(f312,plain,
! [X2,X3,X0,X1] :
( ~ meet(b2,X0,X2)
| ~ join(X0,r1,X1)
| ~ join(r1,X2,X3)
| meet(b2,X1,X3) ),
inference(resolution,[],[f205,f26]) ).
fof(f340,plain,
meet(d,a,d),
inference(resolution,[],[f228,f10]) ).
fof(f960,plain,
meet(d,c2,d),
inference(resolution,[],[f232,f34]) ).
fof(f965,plain,
! [X2,X3,X0,X1] :
( ~ join(d,X2,X3)
| ~ meet(X0,c2,X2)
| ~ join(d,X0,X1)
| meet(c2,X1,X3) ),
inference(resolution,[],[f960,f16]) ).
fof(f1012,plain,
meet(a,e,n0),
inference(resolution,[],[f264,f45]) ).
fof(f1014,plain,
! [X0,X1] :
( ~ meet(X0,a,X1)
| meet(X1,e,n0) ),
inference(resolution,[],[f1012,f87]) ).
fof(f1536,plain,
meet(e,c2,e),
inference(resolution,[],[f233,f30]) ).
fof(f1543,plain,
meet(c2,e,e),
inference(resolution,[],[f1536,f7]) ).
fof(f2642,plain,
meet(d,e,n0),
inference(resolution,[],[f1014,f340]) ).
fof(f2649,plain,
! [X2,X0,X1] :
( ~ meet(X0,e,X1)
| ~ meet(X2,X0,d)
| meet(X2,X1,n0) ),
inference(resolution,[],[f2642,f12]) ).
fof(f3879,plain,
! [X0,X1] :
( ~ meet(X0,c2,n0)
| ~ join(d,X0,X1)
| meet(c2,X1,d) ),
inference(resolution,[],[f965,f22]) ).
fof(f4889,plain,
! [X0] :
( ~ join(d,r1,X0)
| meet(c2,X0,d) ),
inference(resolution,[],[f3879,f47]) ).
fof(f5354,plain,
meet(c2,b2,d),
inference(resolution,[],[f4889,f58]) ).
fof(f5370,plain,
meet(b2,c2,d),
inference(resolution,[],[f5354,f7]) ).
fof(f6013,plain,
! [X0] :
( ~ meet(X0,c2,d)
| meet(X0,e,n0) ),
inference(resolution,[],[f2649,f1543]) ).
fof(f6354,plain,
meet(b2,e,n0),
inference(resolution,[],[f6013,f5370]) ).
fof(f6357,plain,
! [X0,X1] :
( ~ join(r1,n0,X1)
| ~ join(e,r1,X0)
| meet(b2,X0,X1) ),
inference(resolution,[],[f6354,f312]) ).
fof(f7924,plain,
! [X0] :
( ~ join(e,r1,X0)
| meet(b2,X0,r1) ),
inference(resolution,[],[f6357,f22]) ).
fof(f8062,plain,
meet(b2,a2,r1),
inference(resolution,[],[f7924,f57]) ).
fof(f8099,plain,
meet(a2,b2,r1),
inference(resolution,[],[f8062,f7]) ).
fof(f8110,plain,
$false,
inference(global_subsumption,[],[f8099,f37]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT005-6 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.38 % Computer : n014.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 13:55:47 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.41 Running first-order model finding
% 0.11/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 24.63/3.92 % (830809)Will run a generic schedule for satisfiability detection.
% 24.63/3.92 % (830817)dis+10_1_sil=32000:sp=arity:random_seed=2262757374:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 24.63/3.92 % (830815)% WARNING: option uhcvi not known.
% 24.63/3.92 % (830818)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3826795266:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 24.63/3.92 % (830814)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2069775058_2999 on theBenchmark for (2999ds/0Mi)
% 24.63/3.92 % (830816)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=355264227:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 24.63/3.92 % (830819)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2369208494:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 24.63/3.92 % (830815)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2962614810:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 24.63/3.92 % (830820)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=162015694:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 24.63/3.92 % TRYING [1]
% 24.63/3.92 % TRYING [2]
% 24.63/3.92 % TRYING [3]
% 24.63/3.92 % TRYING [4]
% 24.63/3.92 % (830817)Instruction limit reached!
% 24.63/3.92 % (830817)------------------------------
% 24.63/3.92 % (830817)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.63/3.92 % (830817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.63/3.92 % (830817)CaDiCaL version: 2.1.3
% 24.63/3.92 % (830817)Termination reason: Instruction limit
% 24.63/3.92 % (830817)Termination phase: Saturation
% 24.63/3.92 % (830817)Time elapsed: 0.033 s
% 24.63/3.92 % (830817)Peak memory usage: 11 MB
% 24.63/3.92 % (830817)Instructions burned: 106 (million)
% 24.63/3.92 % TRYING [5]
% 24.63/3.92 % (830828)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2248499519:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 24.63/3.92 % TRYING [1]
% 24.63/3.92 % TRYING [2]
% 24.63/3.92 % TRYING [3]
% 24.63/3.92 % TRYING [4]
% 24.63/3.92 % TRYING [5]
% 24.63/3.92 % (830818)Instruction limit reached!
% 24.63/3.92 % (830818)------------------------------
% 24.63/3.92 % (830818)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.63/3.92 % (830818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.63/3.92 % (830818)CaDiCaL version: 2.1.3
% 24.63/3.92 % (830818)Termination reason: Instruction limit
% 24.63/3.92 % (830818)Termination phase: Saturation
% 24.63/3.92 % (830818)Time elapsed: 0.063 s
% 24.63/3.92 % (830818)Peak memory usage: 11 MB
% 24.63/3.92 % (830818)Instructions burned: 117 (million)
% 24.63/3.92 % (830819)Instruction limit reached!
% 24.63/3.92 % (830819)------------------------------
% 24.63/3.92 % (830819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.63/3.92 % (830819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.63/3.92 % (830819)CaDiCaL version: 2.1.3
% 24.63/3.92 % (830819)Termination reason: Instruction limit
% 24.63/3.92 % (830819)Termination phase: Saturation
% 24.63/3.92 % (830819)Time elapsed: 0.071 s
% 24.63/3.92 % (830819)Peak memory usage: 11 MB
% 24.63/3.92 % (830819)Instructions burned: 131 (million)
% 24.63/3.92 % (830831)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=795108776:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 24.63/3.92 % (830832)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=80973697:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 24.63/3.92 % TRYING [6]
% 24.63/3.92 % TRYING [6]
% 24.63/3.92 % (830820)Instruction limit reached!
% 24.63/3.92 % (830820)------------------------------
% 24.63/3.92 % (830820)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.63/3.92 % (830820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.63/3.92 % (830820)CaDiCaL version: 2.1.3
% 24.63/3.92 % (830820)Termination reason: Instruction limit
% 24.63/3.92 % (830820)Termination phase: Saturation
% 24.63/3.92 % (830820)Time elapsed: 0.108 s
% 24.63/3.92 % (830820)Peak memory usage: 13 MB
% 24.63/3.92 % (830820)Instructions burned: 159 (million)
% 24.63/3.92 % (830835)ott-21_1_sil=16000:fs=off:random_seed=3521009140:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 24.63/3.92 % (830831)Instruction limit reached!
% 24.63/3.92 % (830831)------------------------------
% 24.63/3.92 % (830831)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.63/3.92 % (830831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.83/7.06 % (830831)CaDiCaL version: 2.1.3
% 46.83/7.06 % (830831)Termination reason: Instruction limit
% 46.83/7.06 % (830831)Termination phase: Saturation
% 46.83/7.06 % (830831)Time elapsed: 0.079 s
% 46.83/7.06 % (830831)Peak memory usage: 12 MB
% 46.83/7.06 % (830831)Instructions burned: 133 (million)
% 46.83/7.06 % (830828)Instruction limit reached!
% 46.83/7.06 % (830828)------------------------------
% 46.83/7.06 % (830828)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.83/7.06 % (830828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.83/7.06 % (830828)CaDiCaL version: 2.1.3
% 46.83/7.06 % (830828)Termination reason: Instruction limit
% 46.83/7.06 % (830828)Termination phase: Finite model building constraint generation
% 46.83/7.06 % (830828)Time elapsed: 0.140 s
% 46.83/7.06 % (830828)Peak memory usage: 32 MB
% 46.83/7.06 % (830828)Instructions burned: 720 (million)
% 46.83/7.06 % (830837)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1489399782:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 46.83/7.06 % (830838)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1770621011:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 46.83/7.06 % TRYING [1]
% 46.83/7.06 % TRYING [2]
% 46.83/7.06 % TRYING [3]
% 46.83/7.06 % TRYING [4]
% 46.83/7.06 % (830835)Instruction limit reached!
% 46.83/7.06 % (830835)------------------------------
% 46.83/7.06 % (830835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.83/7.06 % (830835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.83/7.06 % (830835)CaDiCaL version: 2.1.3
% 46.83/7.06 % (830835)Termination reason: Instruction limit
% 46.83/7.06 % (830835)Termination phase: Saturation
% 46.83/7.06 % (830835)Time elapsed: 0.090 s
% 46.83/7.06 % (830835)Peak memory usage: 12 MB
% 46.83/7.06 % (830835)Instructions burned: 181 (million)
% 46.83/7.06 % TRYING [5]
% 46.83/7.06 % (830841)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2109265399:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 46.83/7.06 % TRYING [7]
% 46.83/7.06 % TRYING [6]
% 46.83/7.06 % (830838)Instruction limit reached!
% 46.83/7.06 % (830838)------------------------------
% 46.83/7.06 % (830838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.83/7.06 % (830838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.83/7.06 % (830838)CaDiCaL version: 2.1.3
% 46.83/7.06 % (830838)Termination reason: Instruction limit
% 46.83/7.06 % (830838)Termination phase: Finite model building SAT solving
% 46.83/7.06 % (830838)Time elapsed: 0.168 s
% 46.83/7.06 % (830838)Peak memory usage: 28 MB
% 46.83/7.06 % (830838)Instructions burned: 869 (million)
% 46.83/7.06 % (830843)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2460481251:i=889:ins=1_2996 on theBenchmark for (2996ds/889Mi)
% 46.83/7.06 % (830837)Instruction limit reached!
% 46.83/7.06 % (830837)------------------------------
% 46.83/7.06 % (830837)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.83/7.06 % (830837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.83/7.06 % (830837)CaDiCaL version: 2.1.3
% 46.83/7.06 % (830837)Termination reason: Instruction limit
% 46.83/7.06 % (830837)Termination phase: Saturation
% 46.83/7.06 % (830837)Time elapsed: 0.281 s
% 46.83/7.06 % (830837)Peak memory usage: 13 MB
% 46.83/7.06 % (830837)Instructions burned: 477 (million)
% 46.83/7.06 % TRYING [14]
% 46.83/7.06 % (830845)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=1445774313:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 46.83/7.06 % (830832)Instruction limit reached!
% 46.83/7.06 % (830832)------------------------------
% 46.83/7.06 % (830832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.83/7.06 % (830832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.83/7.06 % (830832)CaDiCaL version: 2.1.3
% 46.83/7.06 % (830832)Termination reason: Instruction limit
% 46.83/7.06 % (830832)Termination phase: Saturation
% 46.83/7.06 % (830832)Time elapsed: 0.394 s
% 46.83/7.06 % (830832)Peak memory usage: 15 MB
% 46.83/7.06 % (830832)Instructions burned: 685 (million)
% 46.83/7.06 % (830847)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2156884617:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 46.83/7.06 % (830843)Instruction limit reached!
% 46.83/7.06 % (830843)------------------------------
% 46.83/7.06 % (830843)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.81/7.27 % (830843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.81/7.27 % (830843)CaDiCaL version: 2.1.3
% 47.81/7.27 % (830843)Termination reason: Instruction limit
% 47.81/7.27 % (830843)Termination phase: Finite model building constraint generation
% 47.81/7.27 % (830843)Time elapsed: 0.189 s
% 47.81/7.27 % (830843)Peak memory usage: 83 MB
% 47.81/7.27 % (830843)Instructions burned: 894 (million)
% 47.81/7.27 % (830849)fmb+10_1_sil=64000:random_seed=375608762:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 47.81/7.27 % TRYING [1]
% 47.81/7.27 % TRYING [2]
% 47.81/7.27 % TRYING [3]
% 47.81/7.27 % TRYING [4]
% 47.81/7.27 % TRYING [5]
% 47.81/7.27 % TRYING [8]
% 47.81/7.27 % TRYING [6]
% 47.81/7.27 % (830845)Instruction limit reached!
% 47.81/7.27 % (830845)------------------------------
% 47.81/7.27 % (830845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.81/7.27 % (830845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.81/7.27 % (830845)CaDiCaL version: 2.1.3
% 47.81/7.27 % (830845)Termination reason: Instruction limit
% 47.81/7.27 % (830845)Termination phase: Saturation
% 47.81/7.27 % (830845)Time elapsed: 0.383 s
% 47.81/7.27 % (830845)Peak memory usage: 16 MB
% 47.81/7.27 % (830845)Instructions burned: 693 (million)
% 47.81/7.27 % TRYING [7]
% 47.81/7.27 % (830851)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2564459472:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 47.81/7.27 % TRYING [20]
% 47.81/7.27 % (830841)Instruction limit reached!
% 47.81/7.27 % (830841)------------------------------
% 47.81/7.27 % (830841)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.81/7.27 % (830841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.81/7.27 % (830841)CaDiCaL version: 2.1.3
% 47.81/7.27 % (830841)Termination reason: Instruction limit
% 47.81/7.27 % (830841)Termination phase: Saturation
% 47.81/7.27 % (830841)Time elapsed: 0.719 s
% 47.81/7.27 % (830841)Peak memory usage: 17 MB
% 47.81/7.27 % (830841)Instructions burned: 1179 (million)
% 47.81/7.27 % (830853)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=59741927:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 47.81/7.27 % TRYING [8]
% 47.81/7.27 % (830847)Instruction limit reached!
% 47.81/7.27 % (830847)------------------------------
% 47.81/7.27 % (830847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.81/7.27 % (830847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.81/7.27 % (830847)CaDiCaL version: 2.1.3
% 47.81/7.27 % (830847)Termination reason: Instruction limit
% 47.81/7.27 % (830847)Termination phase: Saturation
% 47.81/7.27 % (830847)Time elapsed: 0.475 s
% 47.81/7.27 % (830847)Peak memory usage: 16 MB
% 47.81/7.27 % (830847)Instructions burned: 880 (million)
% 47.81/7.27 % (830855)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1563468694:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 47.81/7.27 % (830853)Instruction limit reached!
% 47.81/7.27 % (830853)------------------------------
% 47.81/7.27 % (830853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.81/7.27 % (830853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.81/7.27 % (830853)CaDiCaL version: 2.1.3
% 47.81/7.27 % (830853)Termination reason: Instruction limit
% 47.81/7.27 % (830853)Termination phase: Finite model building constraint generation
% 47.81/7.27 % (830853)Time elapsed: 0.343 s
% 47.81/7.27 % (830853)Peak memory usage: 71 MB
% 47.81/7.27 % (830853)Instructions burned: 923 (million)
% 47.81/7.27 % TRYING [9]
% 47.81/7.27 % (830857)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4210298061:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 47.81/7.27 % TRYING [8]
% 47.81/7.27 % (830857)Instruction limit reached!
% 47.81/7.27 % (830857)------------------------------
% 47.81/7.27 % (830857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.81/7.27 % (830857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.81/7.27 % (830857)CaDiCaL version: 2.1.3
% 47.81/7.27 % (830857)Termination reason: Instruction limit
% 47.81/7.27 % (830857)Termination phase: Saturation
% 47.81/7.27 % (830857)Time elapsed: 0.849 s
% 47.81/7.27 % (830857)Peak memory usage: 26 MB
% 47.81/7.27 % (830857)Instructions burned: 1472 (million)
% 47.81/7.27 % (830859)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4249487650:i=6324_2977 on theBenchmark for (2977ds/6324Mi)
% 47.81/7.27 % TRYING [77]
% 47.81/7.27 % TRYING [10]
% 47.81/7.27 % TRYING [9]
% 47.81/7.27 % (830855)Instruction limit reached!
% 47.81/7.27 % (830855)------------------------------
% 47.81/7.27 % (830855)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.81/7.27 % (830855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.81/7.27 % (830855)CaDiCaL version: 2.1.3
% 47.81/7.27 % (830855)Termination reason: Instruction limit
% 47.81/7.27 % (830855)Termination phase: Saturation
% 47.81/7.27 % (830855)Time elapsed: 2.464 s
% 47.81/7.27 % (830855)Peak memory usage: 20 MB
% 47.81/7.27 % (830855)Instructions burned: 5133 (million)
% 47.81/7.27 % (830861)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=665855739:fmbsr=2.30978:i=2174_2964 on theBenchmark for (2964ds/2174Mi)
% 47.81/7.27 % TRYING [16]
% 47.81/7.27 % (830851)Instruction limit reached!
% 47.81/7.27 % (830851)------------------------------
% 47.81/7.27 % (830851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.81/7.27 % (830851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.81/7.27 % (830851)CaDiCaL version: 2.1.3
% 47.81/7.27 % (830851)Termination reason: Instruction limit
% 47.81/7.27 % (830851)Termination phase: Finite model building constraint generation
% 47.81/7.27 % (830851)Time elapsed: 3.266 s
% 47.81/7.27 % (830851)Peak memory usage: 612 MB
% 47.81/7.27 % (830851)Instructions burned: 9518 (million)
% 47.81/7.27 % (830861)Instruction limit reached!
% 47.81/7.27 % (830861)------------------------------
% 47.81/7.27 % (830861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.81/7.27 % (830861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.81/7.27 % (830861)CaDiCaL version: 2.1.3
% 47.81/7.27 % (830861)Termination reason: Instruction limit
% 47.81/7.27 % (830861)Termination phase: Finite model building constraint generation
% 47.81/7.27 % (830861)Time elapsed: 0.720 s
% 47.81/7.27 % (830861)Peak memory usage: 130 MB
% 47.81/7.27 % (830861)Instructions burned: 2174 (million)
% 47.81/7.27 % (830863)ott-2_1_sil=16000:newcnf=on:random_seed=2495370576:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2957 on theBenchmark for (2957ds/869Mi)
% 47.81/7.27 % (830864)ott+10_1_sil=32000:tgt=ground:random_seed=1362413909:i=5114:av=off_2957 on theBenchmark for (2957ds/5114Mi)
% 47.81/7.27 % (830859)Instruction limit reached!
% 47.81/7.27 % (830859)------------------------------
% 47.81/7.27 % (830859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.81/7.27 % (830859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.81/7.27 % (830859)CaDiCaL version: 2.1.3
% 47.81/7.27 % (830859)Termination reason: Instruction limit
% 47.81/7.27 % (830859)Termination phase: Finite model building constraint generation
% 47.81/7.27 % (830859)Time elapsed: 2.177 s
% 47.81/7.27 % (830859)Peak memory usage: 451 MB
% 47.81/7.27 % (830859)Instructions burned: 6326 (million)
% 47.81/7.27 % (830867)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3605620406:i=54282_2955 on theBenchmark for (2955ds/54282Mi)
% 47.81/7.27 % TRYING [1]
% 47.81/7.27 % TRYING [2]
% 47.81/7.27 % TRYING [3]
% 47.81/7.27 % TRYING [4]
% 47.81/7.27 % TRYING [5]
% 47.81/7.27 % TRYING [6]
% 47.81/7.27 % TRYING [11]
% 47.81/7.27 % TRYING [7]
% 47.81/7.27 % (830863)Instruction limit reached!
% 47.81/7.27 % (830863)------------------------------
% 47.81/7.27 % (830863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.81/7.27 % (830863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.81/7.27 % (830863)CaDiCaL version: 2.1.3
% 47.81/7.27 % (830863)Termination reason: Instruction limit
% 47.81/7.27 % (830863)Termination phase: Saturation
% 47.81/7.27 % (830863)Time elapsed: 0.522 s
% 47.81/7.27 % (830863)Peak memory usage: 14 MB
% 47.81/7.27 % (830863)Instructions burned: 869 (million)
% 47.81/7.27 % (830869)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2263019096:i=3512:aac=none_2951 on theBenchmark for (2951ds/3512Mi)
% 47.81/7.27 % TRYING [8]
% 47.81/7.27 % TRYING [10]
% 47.81/7.27 % (830849)Instruction limit reached!
% 47.81/7.27 % (830849)------------------------------
% 47.81/7.27 % (830849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.81/7.27 % (830849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.81/7.27 % (830849)CaDiCaL version: 2.1.3
% 47.81/7.27 % (830849)Termination reason: Instruction limit
% 47.81/7.27 % (830849)Termination phase: Finite model building constraint generation
% 47.81/7.27 % (830849)Time elapsed: 4.832 s
% 47.81/7.27 % (830849)Peak memory usage: 162 MB
% 47.81/7.27 % (830849)Instructions burned: 22063 (million)
% 47.81/7.27 % (830871)dis+21_1_sil=32000:sas=cadical:random_seed=472269055:i=3773:amm=off_2945 on theBenchmark for (2945ds/3773Mi)
% 47.81/7.27 % TRYING [9]
% 47.81/7.27 % (830871)Instruction limit reached!
% 47.81/7.28 % (830871)------------------------------
% 47.81/7.28 % (830871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.81/7.28 % (830871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.81/7.28 % (830871)CaDiCaL version: 2.1.3
% 47.81/7.28 % (830871)Termination reason: Instruction limit
% 47.81/7.28 % (830871)Termination phase: Saturation
% 47.81/7.28 % (830871)Time elapsed: 1.171 s
% 47.81/7.28 % (830871)Peak memory usage: 33 MB
% 47.81/7.28 % (830871)Instructions burned: 3773 (million)
% 47.81/7.28 % (830873)ott+11_1_sil=16000:gs=on:random_seed=3094111262:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2933 on theBenchmark for (2933ds/2251Mi)
% 47.81/7.28 % (830869)Instruction limit reached!
% 47.81/7.28 % (830869)------------------------------
% 47.81/7.28 % (830869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.81/7.28 % (830869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.81/7.28 % (830869)CaDiCaL version: 2.1.3
% 47.81/7.28 % (830869)Termination reason: Instruction limit
% 47.81/7.28 % (830869)Termination phase: Saturation
% 47.81/7.28 % (830869)Time elapsed: 1.860 s
% 47.81/7.28 % (830869)Peak memory usage: 21 MB
% 47.81/7.28 % (830869)Instructions burned: 3512 (million)
% 47.81/7.28 % (830875)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2954796419:fmbsr=1.6:i=67534_2933 on theBenchmark for (2933ds/67534Mi)
% 47.81/7.28 % TRYING [7]
% 47.81/7.28 % (830873) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-830809-830873"...
% 47.81/7.28 % (830873)...printing done.
% 47.81/7.28 % (830873)Refutation found. Thanks to Tanya!
% 47.81/7.28 % SZS status Unsatisfiable for theBenchmark
% 47.81/7.28 % SZS output start Proof for theBenchmark
% See solution above
% 47.81/7.28 % (830873)------------------------------
% 47.81/7.28 % (830873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.81/7.28 % (830873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.81/7.28 % (830873)CaDiCaL version: 2.1.3
% 47.81/7.28 % (830873)Termination reason: Refutation
% 47.81/7.28 % (830873)Time elapsed: 0.142 s
% 47.81/7.28 % (830873)Peak memory usage: 15 MB
% 47.81/7.28 % (830873)Instructions burned: 443 (million)
% 47.81/7.28 % (830809)Success in time 6.851 s
% 47.81/7.28 % Vampire exiting
%------------------------------------------------------------------------------