%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LAT005-5 : TPTP v9.3.1. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n013.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 52.23s 12.06s
% Output : Refutation 52.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 19
% Syntax : Number of formulae : 61 ( 37 unt; 0 def)
% Number of atoms : 105 ( 0 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 89 ( 45 ~; 44 |; 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 : 76 ( 76 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0] : join(n0,X0,X0),
file('/export/starexec/sandbox/benchmark/Axioms/LAT002-0.ax',join_0_and_x) ).
fof(f4,axiom,
! [X0] : meet(n0,X0,n0),
file('/export/starexec/sandbox/benchmark/Axioms/LAT002-0.ax',meet_0_and_x) ).
fof(f7,axiom,
! [X2,X0,X1] :
( ~ meet(X0,X1,X2)
| meet(X1,X0,X2) ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/benchmark/Axioms/LAT002-0.ax',absorbtion1) ).
fof(f10,axiom,
! [X2,X0,X1] :
( ~ join(X0,X1,X2)
| meet(X0,X2,X0) ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/benchmark/Axioms/LAT002-0.ax',associativity_of_meet2) ).
fof(f13,axiom,
! [X2,X3,X0,X1,X4,X5] :
( ~ join(X0,X4,X5)
| ~ join(X1,X3,X4)
| ~ join(X0,X1,X2)
| join(X2,X3,X5) ),
file('/export/starexec/sandbox/benchmark/Axioms/LAT002-0.ax',associativity_of_join1) ).
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/sandbox/benchmark/Axioms/LAT002-0.ax',modularity2) ).
fof(f21,negated_conjecture,
meet(a,b,c),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',meet_a_and_b) ).
fof(f23,negated_conjecture,
meet(c,r2,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',meet_c_and_r2) ).
fof(f24,negated_conjecture,
meet(r2,b,e),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',meet_r2_and_b) ).
fof(f25,negated_conjecture,
join(a,b,c2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',join_a_and_b) ).
fof(f27,negated_conjecture,
meet(c2,r1,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',meet_c2_and_r1) ).
fof(f28,negated_conjecture,
meet(r2,a,d),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',meet_r2_and_a) ).
fof(f29,negated_conjecture,
join(r1,e,a2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',join_r1_and_e) ).
fof(f30,negated_conjecture,
join(r1,d,b2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',join_r1_and_d) ).
fof(f31,negated_conjecture,
~ meet(a2,b2,r1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',meet_a2_and_b2) ).
fof(f34,plain,
! [X0] : meet(X0,n0,n0),
inference(resolution,[],[f7,f4]) ).
fof(f37,plain,
meet(b,r2,e),
inference(resolution,[],[f7,f24]) ).
fof(f38,plain,
meet(a,r2,d),
inference(resolution,[],[f7,f28]) ).
fof(f39,plain,
meet(r1,c2,n0),
inference(resolution,[],[f7,f27]) ).
fof(f43,plain,
! [X0] : join(X0,n0,X0),
inference(resolution,[],[f8,f3]) ).
fof(f48,plain,
join(d,r1,b2),
inference(resolution,[],[f8,f30]) ).
fof(f60,plain,
join(b,e,b),
inference(resolution,[],[f37,f9]) ).
fof(f65,plain,
meet(a,c2,a),
inference(resolution,[],[f10,f25]) ).
fof(f69,plain,
meet(r1,b2,r1),
inference(resolution,[],[f10,f30]) ).
fof(f70,plain,
join(a,d,a),
inference(resolution,[],[f38,f9]) ).
fof(f81,plain,
! [X2,X0,X1] :
( ~ meet(X0,X1,a)
| ~ meet(r2,X0,X2)
| meet(X2,X1,d) ),
inference(resolution,[],[f11,f28]) ).
fof(f94,plain,
! [X2,X0,X1] :
( ~ meet(X2,X0,c)
| ~ meet(X0,r2,X1)
| meet(X2,X1,n0) ),
inference(resolution,[],[f12,f23]) ).
fof(f105,plain,
! [X2,X0,X1] :
( ~ join(a,X0,X2)
| ~ join(X0,X1,b)
| join(X2,X1,c2) ),
inference(resolution,[],[f13,f25]) ).
fof(f170,plain,
! [X2,X3,X0,X1] :
( ~ meet(X0,b2,X2)
| ~ join(r1,X0,X1)
| ~ join(r1,X2,X3)
| meet(b2,X1,X3) ),
inference(resolution,[],[f69,f16]) ).
fof(f189,plain,
join(d,a,a),
inference(resolution,[],[f70,f8]) ).
fof(f192,plain,
! [X0] :
( ~ meet(r2,a,X0)
| meet(X0,c2,d) ),
inference(resolution,[],[f81,f65]) ).
fof(f220,plain,
! [X0] :
( ~ meet(b,r2,X0)
| meet(a,X0,n0) ),
inference(resolution,[],[f94,f21]) ).
fof(f247,plain,
! [X0] :
( ~ join(b,X0,b)
| join(c2,X0,c2) ),
inference(resolution,[],[f105,f25]) ).
fof(f279,plain,
meet(d,a,d),
inference(resolution,[],[f189,f10]) ).
fof(f351,plain,
! [X2,X3,X0,X1] :
( ~ meet(X0,X1,n0)
| ~ meet(X2,X0,X3)
| meet(X3,X1,n0) ),
inference(resolution,[],[f34,f11]) ).
fof(f774,plain,
meet(d,c2,d),
inference(resolution,[],[f192,f28]) ).
fof(f775,plain,
! [X2,X3,X0,X1] :
( ~ join(d,X2,X3)
| ~ meet(X0,c2,X2)
| ~ join(d,X0,X1)
| meet(c2,X1,X3) ),
inference(resolution,[],[f774,f16]) ).
fof(f814,plain,
meet(a,e,n0),
inference(resolution,[],[f220,f37]) ).
fof(f855,plain,
join(c2,e,c2),
inference(resolution,[],[f247,f60]) ).
fof(f870,plain,
join(e,c2,c2),
inference(resolution,[],[f855,f8]) ).
fof(f888,plain,
meet(e,c2,e),
inference(resolution,[],[f870,f10]) ).
fof(f908,plain,
meet(c2,e,e),
inference(resolution,[],[f888,f7]) ).
fof(f1608,plain,
! [X0,X1] :
( ~ meet(X0,a,X1)
| meet(X1,e,n0) ),
inference(resolution,[],[f351,f814]) ).
fof(f2223,plain,
meet(d,e,n0),
inference(resolution,[],[f1608,f279]) ).
fof(f2231,plain,
! [X2,X0,X1] :
( ~ meet(X0,e,X1)
| ~ meet(X2,X0,d)
| meet(X2,X1,n0) ),
inference(resolution,[],[f2223,f12]) ).
fof(f3101,plain,
! [X0,X1] :
( ~ meet(X0,c2,n0)
| ~ join(d,X0,X1)
| meet(c2,X1,d) ),
inference(resolution,[],[f775,f43]) ).
fof(f3865,plain,
! [X0] :
( ~ join(d,r1,X0)
| meet(c2,X0,d) ),
inference(resolution,[],[f3101,f39]) ).
fof(f4161,plain,
meet(c2,b2,d),
inference(resolution,[],[f3865,f48]) ).
fof(f4174,plain,
meet(b2,c2,d),
inference(resolution,[],[f4161,f7]) ).
fof(f4761,plain,
! [X0] :
( ~ meet(X0,c2,d)
| meet(X0,e,n0) ),
inference(resolution,[],[f2231,f908]) ).
fof(f5001,plain,
meet(b2,e,n0),
inference(resolution,[],[f4761,f4174]) ).
fof(f5012,plain,
meet(e,b2,n0),
inference(resolution,[],[f5001,f7]) ).
fof(f5025,plain,
! [X0,X1] :
( ~ join(r1,e,X0)
| ~ join(r1,n0,X1)
| meet(b2,X0,X1) ),
inference(resolution,[],[f5012,f170]) ).
fof(f6801,plain,
! [X0] :
( ~ join(r1,n0,X0)
| meet(b2,a2,X0) ),
inference(resolution,[],[f5025,f29]) ).
fof(f6988,plain,
meet(b2,a2,r1),
inference(resolution,[],[f6801,f43]) ).
fof(f7020,plain,
meet(a2,b2,r1),
inference(resolution,[],[f6988,f7]) ).
fof(f7028,plain,
$false,
inference(global_subsumption,[],[f7020,f31]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT005-5 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.15/0.41 % Computer : n013.cluster.edu
% 0.15/0.41 % Model : x86_64 x86_64
% 0.15/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.41 % Memory : 8046.5625MB
% 0.15/0.41 % OS : Linux 6.8.0-71-generic
% 0.15/0.41 % CPULimit : 300
% 0.15/0.41 % WCLimit : 300
% 0.15/0.41 % DateTime : Sun Sep 27 13:55:21 UTC 2026
% 0.15/0.41 % CPUTime :
% 0.15/0.41 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.15/0.46 Running first-order model finding
% 0.15/0.47 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
% 42.19/6.47 % (244963)Will run a generic schedule for satisfiability detection.
% 42.19/6.47 % (244972)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=464660550:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 42.19/6.47 % (244968)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2825387379_2999 on theBenchmark for (2999ds/0Mi)
% 42.19/6.47 % TRYING [1]
% 42.19/6.47 % TRYING [2]
% 42.19/6.47 % TRYING [3]
% 42.19/6.47 % (244969)% WARNING: option uhcvi not known.
% 42.19/6.47 % TRYING [4]
% 42.19/6.47 % (244969)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1935226496:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 42.19/6.47 % (244970)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=894331091:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 42.19/6.47 % (244971)dis+10_1_sil=32000:sp=arity:random_seed=3421387568:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 42.19/6.47 % (244974)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=639963935:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 42.19/6.47 % (244973)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1726547005:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 42.19/6.47 % TRYING [5]
% 42.19/6.47 % (244972)Instruction limit reached!
% 42.19/6.47 % (244972)------------------------------
% 42.19/6.47 % (244972)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.19/6.47 % (244972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.19/6.47 % (244972)CaDiCaL version: 2.1.3
% 42.19/6.47 % (244972)Termination reason: Instruction limit
% 42.19/6.47 % (244972)Termination phase: Saturation
% 42.19/6.47 % (244972)Time elapsed: 0.051 s
% 42.19/6.47 % (244972)Peak memory usage: 12 MB
% 42.19/6.47 % (244972)Instructions burned: 116 (million)
% 42.19/6.47 % (244982)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3050511893:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 42.19/6.47 % TRYING [1]
% 42.19/6.47 % TRYING [2]
% 42.19/6.47 % TRYING [3]
% 42.19/6.47 % TRYING [4]
% 42.19/6.47 % TRYING [5]
% 42.19/6.47 % (244971)Instruction limit reached!
% 42.19/6.47 % (244971)------------------------------
% 42.19/6.47 % (244971)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.19/6.47 % (244971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.19/6.47 % (244971)CaDiCaL version: 2.1.3
% 42.19/6.47 % (244971)Termination reason: Instruction limit
% 42.19/6.47 % (244971)Termination phase: Saturation
% 42.19/6.47 % (244971)Time elapsed: 0.103 s
% 42.19/6.47 % (244971)Peak memory usage: 11 MB
% 42.19/6.47 % (244971)Instructions burned: 103 (million)
% 42.19/6.47 % TRYING [6]
% 42.19/6.47 % (244973)Instruction limit reached!
% 42.19/6.47 % (244973)------------------------------
% 42.19/6.47 % (244973)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.19/6.47 % (244973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.19/6.47 % (244973)CaDiCaL version: 2.1.3
% 42.19/6.47 % (244973)Termination reason: Instruction limit
% 42.19/6.47 % (244973)Termination phase: Saturation
% 42.19/6.47 % (244973)Time elapsed: 0.117 s
% 42.19/6.47 % (244973)Peak memory usage: 12 MB
% 42.19/6.47 % (244973)Instructions burned: 131 (million)
% 42.19/6.47 % (244984)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2569398833:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 42.19/6.47 % (244985)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=1841437412:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 42.19/6.47 % TRYING [6]
% 42.19/6.47 % (244974)Instruction limit reached!
% 42.19/6.47 % (244974)------------------------------
% 42.19/6.47 % (244974)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.19/6.47 % (244974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.19/6.47 % (244974)CaDiCaL version: 2.1.3
% 42.19/6.47 % (244974)Termination reason: Instruction limit
% 42.19/6.47 % (244974)Termination phase: Saturation
% 42.19/6.47 % (244974)Time elapsed: 0.173 s
% 42.19/6.47 % (244974)Peak memory usage: 12 MB
% 42.19/6.47 % (244974)Instructions burned: 160 (million)
% 42.19/6.47 % (244988)ott-21_1_sil=16000:fs=off:random_seed=1476881530:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 42.19/6.47 % (244984)Instruction limit reached!
% 42.19/6.47 % (244984)------------------------------
% 42.19/6.47 % (244984)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.19/6.47 % (244984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.28/11.30 % (244984)CaDiCaL version: 2.1.3
% 76.28/11.30 % (244984)Termination reason: Instruction limit
% 76.28/11.30 % (244984)Termination phase: Saturation
% 76.28/11.30 % (244984)Time elapsed: 0.129 s
% 76.28/11.30 % (244984)Peak memory usage: 12 MB
% 76.28/11.30 % (244984)Instructions burned: 131 (million)
% 76.28/11.30 % (244990)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2812231678:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 76.28/11.30 % TRYING [7]
% 76.28/11.30 % (244982)Instruction limit reached!
% 76.28/11.30 % (244982)------------------------------
% 76.28/11.30 % (244982)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.28/11.30 % (244982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.28/11.30 % (244982)CaDiCaL version: 2.1.3
% 76.28/11.30 % (244982)Termination reason: Instruction limit
% 76.28/11.30 % (244982)Termination phase: Finite model building constraint generation
% 76.28/11.30 % (244982)Time elapsed: 0.285 s
% 76.28/11.30 % (244982)Peak memory usage: 31 MB
% 76.28/11.30 % (244982)Instructions burned: 716 (million)
% 76.28/11.30 % TRYING [7]
% 76.28/11.30 % (244992)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3578404937:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 76.28/11.30 % TRYING [1]
% 76.28/11.30 % TRYING [2]
% 76.28/11.30 % TRYING [3]
% 76.28/11.30 % (244988)Instruction limit reached!
% 76.28/11.30 % (244988)------------------------------
% 76.28/11.30 % (244988)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.28/11.30 % (244988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.28/11.30 % (244988)CaDiCaL version: 2.1.3
% 76.28/11.30 % (244988)Termination reason: Instruction limit
% 76.28/11.30 % (244988)Termination phase: Saturation
% 76.28/11.30 % (244988)Time elapsed: 0.178 s
% 76.28/11.30 % (244988)Peak memory usage: 12 MB
% 76.28/11.30 % (244988)Instructions burned: 180 (million)
% 76.28/11.30 % TRYING [4]
% 76.28/11.30 % (244994)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1997841834:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 76.28/11.30 % TRYING [5]
% 76.28/11.30 % TRYING [6]
% 76.28/11.30 % (244990)Instruction limit reached!
% 76.28/11.30 % (244990)------------------------------
% 76.28/11.30 % (244990)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.28/11.30 % (244990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.28/11.30 % (244990)CaDiCaL version: 2.1.3
% 76.28/11.30 % (244990)Termination reason: Instruction limit
% 76.28/11.30 % (244990)Termination phase: Saturation
% 76.28/11.30 % (244990)Time elapsed: 0.462 s
% 76.28/11.30 % (244990)Peak memory usage: 13 MB
% 76.28/11.30 % (244990)Instructions burned: 477 (million)
% 76.28/11.30 % (244996)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3280576675:i=889:ins=1_2992 on theBenchmark for (2992ds/889Mi)
% 76.28/11.30 % (244985)Instruction limit reached!
% 76.28/11.30 % (244985)------------------------------
% 76.28/11.30 % (244985)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.28/11.30 % (244985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.28/11.30 % (244985)CaDiCaL version: 2.1.3
% 76.28/11.30 % (244985)Termination reason: Instruction limit
% 76.28/11.30 % (244985)Termination phase: Saturation
% 76.28/11.30 % (244985)Time elapsed: 0.697 s
% 76.28/11.30 % (244985)Peak memory usage: 17 MB
% 76.28/11.30 % (244985)Instructions burned: 685 (million)
% 76.28/11.30 % (244992)Instruction limit reached!
% 76.28/11.30 % (244992)------------------------------
% 76.28/11.30 % (244992)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.28/11.30 % (244992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.28/11.30 % (244992)CaDiCaL version: 2.1.3
% 76.28/11.30 % (244992)Termination reason: Instruction limit
% 76.28/11.30 % (244992)Termination phase: Finite model building SAT solving
% 76.28/11.30 % (244992)Time elapsed: 0.497 s
% 76.28/11.30 % (244992)Peak memory usage: 24 MB
% 76.28/11.30 % (244992)Instructions burned: 866 (million)
% 76.28/11.30 % TRYING [8]
% 76.28/11.30 % (244998)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=367268587:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2991 on theBenchmark for (2991ds/692Mi)
% 76.28/11.30 % (244999)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=775515595:i=879:kws=inv_precedence:fsr=off_2990 on theBenchmark for (2990ds/879Mi)
% 76.28/11.30 % TRYING [14]
% 76.28/11.30 % (244994)Instruction limit reached!
% 76.28/11.30 % (244994)------------------------------
% 76.28/11.30 % (244994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.23/12.06 % (244994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.23/12.06 % (244994)CaDiCaL version: 2.1.3
% 52.23/12.06 % (244994)Termination reason: Instruction limit
% 52.23/12.06 % (244994)Termination phase: Saturation
% 52.23/12.06 % (244994)Time elapsed: 0.627 s
% 52.23/12.06 % (244994)Peak memory usage: 19 MB
% 52.23/12.06 % (244994)Instructions burned: 1180 (million)
% 52.23/12.06 % (245002)fmb+10_1_sil=64000:random_seed=322681374:i=22061:nm=2:gsp=on_2989 on theBenchmark for (2989ds/22061Mi)
% 52.23/12.06 % TRYING [1]
% 52.23/12.06 % TRYING [2]
% 52.23/12.06 % TRYING [3]
% 52.23/12.06 % TRYING [4]
% 52.23/12.06 % TRYING [5]
% 52.23/12.06 % TRYING [6]
% 52.23/12.06 % (244996)Instruction limit reached!
% 52.23/12.06 % (244996)------------------------------
% 52.23/12.06 % (244996)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.23/12.06 % (244996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.23/12.06 % (244996)CaDiCaL version: 2.1.3
% 52.23/12.06 % (244996)Termination reason: Instruction limit
% 52.23/12.06 % (244996)Termination phase: Finite model building constraint generation
% 52.23/12.06 % (244996)Time elapsed: 0.646 s
% 52.23/12.06 % (244996)Peak memory usage: 78 MB
% 52.23/12.06 % (244996)Instructions burned: 889 (million)
% 52.23/12.06 % TRYING [7]
% 52.23/12.06 % (245004)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=759285004:i=9515:nm=5_2985 on theBenchmark for (2985ds/9515Mi)
% 52.23/12.06 % TRYING [20]
% 52.23/12.06 % (244998)Instruction limit reached!
% 52.23/12.06 % (244998)------------------------------
% 52.23/12.06 % (244998)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.23/12.06 % (244998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.23/12.06 % (244998)CaDiCaL version: 2.1.3
% 52.23/12.06 % (244998)Termination reason: Instruction limit
% 52.23/12.06 % (244998)Termination phase: Saturation
% 52.23/12.06 % (244998)Time elapsed: 0.682 s
% 52.23/12.06 % (244998)Peak memory usage: 15 MB
% 52.23/12.06 % (244998)Instructions burned: 693 (million)
% 52.23/12.06 % (245006)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4090654598:fmbsr=1.7:i=920_2984 on theBenchmark for (2984ds/920Mi)
% 52.23/12.06 % TRYING [8]
% 52.23/12.06 % (244999)Instruction limit reached!
% 52.23/12.06 % (244999)------------------------------
% 52.23/12.06 % (244999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.23/12.06 % (244999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.23/12.06 % (244999)CaDiCaL version: 2.1.3
% 52.23/12.06 % (244999)Termination reason: Instruction limit
% 52.23/12.06 % (244999)Termination phase: Saturation
% 52.23/12.06 % (244999)Time elapsed: 0.849 s
% 52.23/12.06 % (244999)Peak memory usage: 17 MB
% 52.23/12.06 % (244999)Instructions burned: 879 (million)
% 52.23/12.06 % TRYING [9]
% 52.23/12.06 % (245008)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1951096352:i=5131_2982 on theBenchmark for (2982ds/5131Mi)
% 52.23/12.06 % TRYING [8]
% 52.23/12.06 % (245006)Instruction limit reached!
% 52.23/12.06 % (245006)------------------------------
% 52.23/12.06 % (245006)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.23/12.06 % (245006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.23/12.06 % (245006)CaDiCaL version: 2.1.3
% 52.23/12.06 % (245006)Termination reason: Instruction limit
% 52.23/12.06 % (245006)Termination phase: Finite model building constraint generation
% 52.23/12.06 % (245006)Time elapsed: 0.689 s
% 52.23/12.06 % (245006)Peak memory usage: 67 MB
% 52.23/12.06 % (245006)Instructions burned: 920 (million)
% 52.23/12.06 % (245010)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2892246676:i=1472:ins=7:fdi=8:gsp=on_2976 on theBenchmark for (2976ds/1472Mi)
% 52.23/12.06 % TRYING [9]
% 52.23/12.06 % TRYING [10]
% 52.23/12.06 % (245010)Instruction limit reached!
% 52.23/12.06 % (245010)------------------------------
% 52.23/12.06 % (245010)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.23/12.06 % (245010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.23/12.06 % (245010)CaDiCaL version: 2.1.3
% 52.23/12.06 % (245010)Termination reason: Instruction limit
% 52.23/12.06 % (245010)Termination phase: Saturation
% 52.23/12.06 % (245010)Time elapsed: 1.432 s
% 52.23/12.06 % (245010)Peak memory usage: 30 MB
% 52.23/12.06 % (245010)Instructions burned: 1473 (million)
% 52.23/12.06 % (245014)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2228423203:i=6324_2961 on theBenchmark for (2961ds/6324Mi)
% 52.23/12.06 % TRYING [77]
% 52.23/12.06 % TRYING [10]
% 52.23/12.06 % (245008)Instruction limit reached!
% 52.23/12.06 % (245008)------------------------------
% 52.23/12.06 % (245008)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.23/12.06 % (245008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.23/12.06 % (245008)CaDiCaL version: 2.1.3
% 52.23/12.06 % (245008)Termination reason: Instruction limit
% 52.23/12.06 % (245008)Termination phase: Saturation
% 52.23/12.06 % (245008)Time elapsed: 4.168 s
% 52.23/12.06 % (245008)Peak memory usage: 19 MB
% 52.23/12.06 % (245008)Instructions burned: 5131 (million)
% 52.23/12.06 % (245016)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3390435088:fmbsr=2.30978:i=2174_2940 on theBenchmark for (2940ds/2174Mi)
% 52.23/12.06 % TRYING [16]
% 52.23/12.06 % TRYING [11]
% 52.23/12.06 % (245016)Instruction limit reached!
% 52.23/12.06 % (245016)------------------------------
% 52.23/12.06 % (245016)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.23/12.06 % (245016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.23/12.06 % (245016)CaDiCaL version: 2.1.3
% 52.23/12.06 % (245016)Termination reason: Instruction limit
% 52.23/12.06 % (245016)Termination phase: Finite model building constraint generation
% 52.23/12.06 % (245016)Time elapsed: 1.498 s
% 52.23/12.06 % (245016)Peak memory usage: 134 MB
% 52.23/12.06 % (245016)Instructions burned: 2174 (million)
% 52.23/12.06 % (245020)ott-2_1_sil=16000:newcnf=on:random_seed=67895342:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2924 on theBenchmark for (2924ds/869Mi)
% 52.23/12.06 % (245004)Instruction limit reached!
% 52.23/12.06 % (245004)------------------------------
% 52.23/12.06 % (245004)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.23/12.06 % (245004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.23/12.06 % (245004)CaDiCaL version: 2.1.3
% 52.23/12.06 % (245004)Termination reason: Instruction limit
% 52.23/12.06 % (245004)Termination phase: Finite model building constraint generation
% 52.23/12.06 % (245004)Time elapsed: 6.680 s
% 52.23/12.06 % (245004)Peak memory usage: 613 MB
% 52.23/12.06 % (245004)Instructions burned: 9516 (million)
% 52.23/12.06 % (245014)Instruction limit reached!
% 52.23/12.06 % (245014)------------------------------
% 52.23/12.06 % (245014)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.23/12.06 % (245014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.23/12.06 % (245014)CaDiCaL version: 2.1.3
% 52.23/12.06 % (245014)Termination reason: Instruction limit
% 52.23/12.06 % (245014)Termination phase: Finite model building constraint generation
% 52.23/12.06 % (245014)Time elapsed: 4.335 s
% 52.23/12.06 % (245014)Peak memory usage: 451 MB
% 52.23/12.06 % (245014)Instructions burned: 6325 (million)
% 52.23/12.06 % (245024)ott+10_1_sil=32000:tgt=ground:random_seed=3908067473:i=5114:av=off_2917 on theBenchmark for (2917ds/5114Mi)
% 52.23/12.06 % (245025)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=281571047:i=54282_2916 on theBenchmark for (2916ds/54282Mi)
% 52.23/12.06 % TRYING [1]
% 52.23/12.06 % TRYING [2]
% 52.23/12.06 % TRYING [3]
% 52.23/12.06 % TRYING [4]
% 52.23/12.06 % TRYING [5]
% 52.23/12.06 % (245020)Instruction limit reached!
% 52.23/12.06 % (245020)------------------------------
% 52.23/12.06 % (245020)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.23/12.06 % (245020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.23/12.06 % (245020)CaDiCaL version: 2.1.3
% 52.23/12.06 % (245020)Termination reason: Instruction limit
% 52.23/12.06 % (245020)Termination phase: Saturation
% 52.23/12.06 % (245020)Time elapsed: 0.857 s
% 52.23/12.06 % (245020)Peak memory usage: 15 MB
% 52.23/12.06 % (245020)Instructions burned: 869 (million)
% 52.23/12.06 % (245028)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1580737229:i=3512:aac=none_2915 on theBenchmark for (2915ds/3512Mi)
% 52.23/12.06 % TRYING [6]
% 52.23/12.06 % TRYING [7]
% 52.23/12.06 % (245002)Instruction limit reached!
% 52.23/12.06 % (245002)------------------------------
% 52.23/12.06 % (245002)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.23/12.06 % (245002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.23/12.06 % (245002)CaDiCaL version: 2.1.3
% 52.23/12.06 % (245002)Termination reason: Instruction limit
% 52.23/12.06 % (245002)Termination phase: Finite model building SAT solving
% 52.23/12.06 % (245002)Time elapsed: 8.062 s
% 52.23/12.06 % (245002)Peak memory usage: 187 MB
% 52.23/12.06 % (245002)Instructions burned: 22062 (million)
% 52.23/12.06 % (245030)dis+21_1_sil=32000:sas=cadical:random_seed=2334672049:i=3773:amm=off_2908 on theBenchmark for (2908ds/3773Mi)
% 52.23/12.06 % TRYING [8]
% 52.23/12.06 % TRYING [9]
% 52.23/12.06 % TRYING [12]
% 52.23/12.06 % (245030)Instruction limit reached!
% 52.23/12.06 % (245030)------------------------------
% 52.23/12.06 % (245030)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.23/12.06 % (245030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.23/12.06 % (245030)CaDiCaL version: 2.1.3
% 52.23/12.06 % (245030)Termination reason: Instruction limit
% 52.23/12.06 % (245030)Termination phase: Saturation
% 52.23/12.06 % (245030)Time elapsed: 2.040 s
% 52.23/12.06 % (245030)Peak memory usage: 33 MB
% 52.23/12.06 % (245030)Instructions burned: 3775 (million)
% 52.23/12.06 % (245032)ott+11_1_sil=16000:gs=on:random_seed=2449284203:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2887 on theBenchmark for (2887ds/2251Mi)
% 52.23/12.06 % (245032) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-244963-245032"...
% 52.23/12.06 % (245032)...printing done.
% 52.23/12.06 % (245032)Refutation found. Thanks to Tanya!
% 52.23/12.06 % SZS status Unsatisfiable for theBenchmark
% 52.23/12.06 % SZS output start Proof for theBenchmark
% See solution above
% 52.23/12.06 % (245032)------------------------------
% 52.23/12.06 % (245032)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.23/12.06 % (245032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.23/12.06 % (245032)CaDiCaL version: 2.1.3
% 52.23/12.06 % (245032)Termination reason: Refutation
% 52.23/12.06 % (245032)Time elapsed: 0.227 s
% 52.23/12.06 % (245032)Peak memory usage: 14 MB
% 52.23/12.06 % (245032)Instructions burned: 363 (million)
% 52.23/12.06 % (244963)Success in time 11.585 s
% 52.23/12.06 % Vampire exiting
%------------------------------------------------------------------------------