%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : FLD049-3 : TPTP v9.3.1. Bugfixed v2.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:49:42 AM UTC 2026
% Result : Unsatisfiable 63.58s 9.29s
% Output : Refutation 63.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 20
% Syntax : Number of formulae : 59 ( 31 unt; 4 def)
% Number of atoms : 105 ( 8 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 93 ( 47 ~; 46 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 10 con; 0-2 aty)
% Number of variables : 37 ( 37 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f6,axiom,
! [X2,X3,X0,X1,X4,X5] :
( ~ product(X4,X5,X2)
| ~ product(X0,X3,X4)
| ~ product(X3,X5,X1)
| product(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/FLD002-0.ax',associativity_multiplication_1) ).
fof(f7,axiom,
! [X2,X3,X0,X1,X4,X5] :
( ~ product(X4,X1,X5)
| ~ product(X3,X4,X0)
| product(X0,X1,X2)
| ~ product(X3,X5,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/FLD002-0.ax',associativity_multiplication_2) ).
fof(f8,axiom,
! [X0] :
( product(multiplicative_identity,X0,X0)
| ~ defined(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/FLD002-0.ax',existence_of_identity_multiplication) ).
fof(f9,axiom,
! [X0] :
( product(multiplicative_inverse(X0),X0,multiplicative_identity)
| sum(additive_identity,X0,additive_identity)
| ~ defined(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/FLD002-0.ax',existence_of_inverse_multiplication) ).
fof(f10,axiom,
! [X2,X0,X1] :
( ~ product(X1,X0,X2)
| product(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/FLD002-0.ax',commutativity_multiplication) ).
fof(f16,axiom,
! [X0,X1] :
( defined(multiply(X0,X1))
| ~ defined(X0)
| ~ defined(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/FLD002-0.ax',well_definedness_of_multiplication) ).
fof(f18,axiom,
! [X0] :
( sum(additive_identity,X0,additive_identity)
| ~ defined(X0)
| defined(multiplicative_inverse(X0)) ),
file('/export/starexec/sandbox/benchmark/Axioms/FLD002-0.ax',well_definedness_of_multiplicative_inverse) ).
fof(f20,axiom,
! [X0,X1] :
( product(X0,X1,multiply(X0,X1))
| ~ defined(X0)
| ~ defined(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/FLD002-0.ax',totality_of_multiplication) ).
fof(f27,axiom,
defined(a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_is_defined) ).
fof(f28,axiom,
defined(b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',b_is_defined) ).
fof(f29,axiom,
defined(c),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_is_defined) ).
fof(f30,axiom,
defined(d),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d_is_defined) ).
fof(f31,negated_conjecture,
~ sum(additive_identity,b,additive_identity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_sum_5) ).
fof(f32,negated_conjecture,
~ sum(additive_identity,d,additive_identity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_sum_6) ).
fof(f33,negated_conjecture,
product(a,multiplicative_inverse(b),multiply(c,multiplicative_inverse(d))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_7) ).
fof(f34,negated_conjecture,
~ product(a,d,multiply(b,c)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_product_8) ).
fof(f35,definition,
sF0 = multiplicative_inverse(b),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f36,plain,
multiplicative_inverse(b) = sF0,
inference(reorient_equations,[],[f35]) ).
fof(f37,definition,
sF1 = multiplicative_inverse(d),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f38,plain,
multiplicative_inverse(d) = sF1,
inference(reorient_equations,[],[f37]) ).
fof(f39,definition,
sF2 = multiply(c,sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f40,plain,
multiply(c,sF1) = sF2,
inference(reorient_equations,[],[f39]) ).
fof(f41,plain,
product(a,sF0,sF2),
inference(definition_folding,[],[f33,f40,f38,f36]) ).
fof(f42,definition,
sF3 = multiply(b,c),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f43,plain,
multiply(b,c) = sF3,
inference(reorient_equations,[],[f42]) ).
fof(f44,plain,
~ product(a,d,sF3),
inference(definition_folding,[],[f34,f43]) ).
fof(f48,plain,
product(sF0,a,sF2),
inference(resolution,[],[f10,f41]) ).
fof(f49,plain,
! [X0] :
( product(X0,multiplicative_identity,X0)
| ~ defined(X0) ),
inference(resolution,[],[f10,f8]) ).
fof(f53,plain,
( defined(sF3)
| ~ defined(b)
| ~ defined(c) ),
inference(superposition,[],[f16,f43]) ).
fof(f54,plain,
( defined(sF3)
| ~ defined(c) ),
inference(forward_subsumption_resolution,[],[f53,f28]) ).
fof(f56,plain,
defined(sF3),
inference(forward_subsumption_resolution,[],[f54,f29]) ).
fof(f58,plain,
( ~ defined(d)
| defined(multiplicative_inverse(d)) ),
inference(resolution,[],[f18,f32]) ).
fof(f60,plain,
defined(multiplicative_inverse(d)),
inference(forward_subsumption_resolution,[],[f58,f30]) ).
fof(f62,plain,
defined(sF1),
inference(forward_demodulation,[],[f60,f38]) ).
fof(f67,plain,
( product(c,sF1,sF2)
| ~ defined(c)
| ~ defined(sF1) ),
inference(superposition,[],[f20,f40]) ).
fof(f68,plain,
( product(b,c,sF3)
| ~ defined(b)
| ~ defined(c) ),
inference(superposition,[],[f20,f43]) ).
fof(f69,plain,
( product(b,c,sF3)
| ~ defined(c) ),
inference(forward_subsumption_resolution,[],[f68,f28]) ).
fof(f70,plain,
( product(c,sF1,sF2)
| ~ defined(sF1) ),
inference(forward_subsumption_resolution,[],[f67,f29]) ).
fof(f71,plain,
product(b,c,sF3),
inference(forward_subsumption_resolution,[],[f69,f29]) ).
fof(f72,plain,
product(c,sF1,sF2),
inference(forward_subsumption_resolution,[],[f70,f62]) ).
fof(f84,plain,
( product(sF0,b,multiplicative_identity)
| sum(additive_identity,b,additive_identity)
| ~ defined(b) ),
inference(superposition,[],[f9,f36]) ).
fof(f85,plain,
( product(sF1,d,multiplicative_identity)
| sum(additive_identity,d,additive_identity)
| ~ defined(d) ),
inference(superposition,[],[f9,f38]) ).
fof(f86,plain,
( product(sF1,d,multiplicative_identity)
| ~ defined(d) ),
inference(forward_subsumption_resolution,[],[f85,f32]) ).
fof(f87,plain,
( product(sF0,b,multiplicative_identity)
| ~ defined(b) ),
inference(forward_subsumption_resolution,[],[f84,f31]) ).
fof(f88,plain,
product(sF1,d,multiplicative_identity),
inference(forward_subsumption_resolution,[],[f86,f30]) ).
fof(f89,plain,
product(sF0,b,multiplicative_identity),
inference(forward_subsumption_resolution,[],[f87,f28]) ).
fof(f101,plain,
product(b,sF0,multiplicative_identity),
inference(resolution,[],[f89,f10]) ).
fof(f128,plain,
! [X2,X3,X0,X1] :
( ~ product(X1,X2,X3)
| ~ product(X0,X1,multiplicative_identity)
| product(X0,X3,X2)
| ~ defined(X2) ),
inference(resolution,[],[f6,f8]) ).
fof(f146,plain,
! [X2,X0,X1] :
( ~ product(X0,sF2,X2)
| product(X1,sF1,X2)
| ~ product(X0,c,X1) ),
inference(resolution,[],[f7,f72]) ).
fof(f151,plain,
! [X2,X0,X1] :
( ~ product(X0,sF1,X1)
| product(X1,d,X2)
| ~ product(X0,multiplicative_identity,X2) ),
inference(resolution,[],[f7,f88]) ).
fof(f392,plain,
! [X0] :
( ~ product(X0,sF0,multiplicative_identity)
| product(X0,sF2,a)
| ~ defined(a) ),
inference(resolution,[],[f128,f48]) ).
fof(f406,plain,
! [X0] :
( ~ product(X0,sF0,multiplicative_identity)
| product(X0,sF2,a) ),
inference(forward_subsumption_resolution,[],[f392,f27]) ).
fof(f506,plain,
product(b,sF2,a),
inference(resolution,[],[f406,f101]) ).
fof(f1146,plain,
! [X0] :
( ~ product(b,c,X0)
| product(X0,sF1,a) ),
inference(resolution,[],[f146,f506]) ).
fof(f1809,plain,
product(sF3,sF1,a),
inference(resolution,[],[f1146,f71]) ).
fof(f1833,plain,
! [X0] :
( ~ product(sF3,multiplicative_identity,X0)
| product(a,d,X0) ),
inference(resolution,[],[f1809,f151]) ).
fof(f24685,plain,
( product(a,d,sF3)
| ~ defined(sF3) ),
inference(resolution,[],[f1833,f49]) ).
fof(f24707,plain,
~ defined(sF3),
inference(forward_subsumption_resolution,[],[f24685,f44]) ).
fof(f24710,plain,
$false,
inference(forward_subsumption_resolution,[],[f24707,f56]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : FLD049-3 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.20 % Computer : n015.cluster.edu
% 0.11/0.20 % Model : x86_64 x86_64
% 0.11/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.20 % Memory : 8046.5625MB
% 0.11/0.20 % OS : Linux 6.8.0-71-generic
% 0.11/0.20 % CPULimit : 300
% 0.11/0.20 % WCLimit : 300
% 0.11/0.20 % DateTime : Tue Sep 29 00:42:32 UTC 2026
% 0.11/0.20 % CPUTime :
% 0.11/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.23 Running first-order model finding
% 0.11/0.23 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 22.35/3.45 % (3201187)Will run a generic schedule for satisfiability detection.
% 22.35/3.45 % (3201209)dis+10_1_sil=32000:sp=arity:random_seed=1844480202:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 22.35/3.45 % (3201207)% WARNING: option uhcvi not known.
% 22.35/3.45 % (3201206)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2626799049_2999 on theBenchmark for (2999ds/0Mi)
% 22.35/3.45 % (3201207)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4244076863:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 22.35/3.45 % (3201208)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3637183127:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 22.35/3.45 % (3201211)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3904662223:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 22.35/3.45 % (3201210)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=193100390:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 22.35/3.45 % TRYING [1]
% 22.35/3.45 % TRYING [2]
% 22.35/3.45 % TRYING [3]
% 22.35/3.45 % (3201212)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1572821751:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 22.35/3.45 % TRYING [4]
% 22.35/3.45 % (3201209)Instruction limit reached!
% 22.35/3.45 % (3201209)------------------------------
% 22.35/3.45 % (3201209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.35/3.45 % (3201209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.35/3.45 % (3201209)CaDiCaL version: 2.1.3
% 22.35/3.45 % (3201209)Termination reason: Instruction limit
% 22.35/3.45 % (3201209)Termination phase: Saturation
% 22.35/3.45 % (3201209)Time elapsed: 0.036 s
% 22.35/3.45 % (3201209)Peak memory usage: 12 MB
% 22.35/3.45 % (3201209)Instructions burned: 104 (million)
% 22.35/3.45 % (3201226)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2947413580:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 22.35/3.45 % TRYING [1]
% 22.35/3.45 % TRYING [2]
% 22.35/3.45 % TRYING [3]
% 22.35/3.45 % TRYING [4]
% 22.35/3.45 % (3201210)Instruction limit reached!
% 22.35/3.45 % (3201210)------------------------------
% 22.35/3.45 % (3201210)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.35/3.45 % (3201210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.35/3.45 % (3201210)CaDiCaL version: 2.1.3
% 22.35/3.45 % (3201210)Termination reason: Instruction limit
% 22.35/3.45 % (3201210)Termination phase: Saturation
% 22.35/3.45 % (3201210)Time elapsed: 0.063 s
% 22.35/3.45 % (3201210)Peak memory usage: 12 MB
% 22.35/3.45 % (3201210)Instructions burned: 117 (million)
% 22.35/3.45 % (3201212)Instruction limit reached!
% 22.35/3.45 % (3201212)------------------------------
% 22.35/3.45 % (3201212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.35/3.45 % (3201212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.35/3.45 % (3201212)CaDiCaL version: 2.1.3
% 22.35/3.45 % (3201212)Termination reason: Instruction limit
% 22.35/3.45 % (3201212)Termination phase: Saturation
% 22.35/3.45 % (3201212)Time elapsed: 0.065 s
% 22.35/3.45 % (3201212)Peak memory usage: 11 MB
% 22.35/3.45 % (3201212)Instructions burned: 161 (million)
% 22.35/3.45 % (3201211)Instruction limit reached!
% 22.35/3.45 % (3201211)------------------------------
% 22.35/3.45 % (3201211)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.35/3.45 % (3201211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.35/3.45 % (3201211)CaDiCaL version: 2.1.3
% 22.35/3.45 % (3201211)Termination reason: Instruction limit
% 22.35/3.45 % (3201211)Termination phase: Saturation
% 22.35/3.45 % (3201211)Time elapsed: 0.078 s
% 22.35/3.45 % (3201211)Peak memory usage: 16 MB
% 22.35/3.45 % (3201211)Instructions burned: 132 (million)
% 22.35/3.45 % (3201236)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2787653469:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 22.35/3.45 % (3201241)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=3725196196:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 22.35/3.45 % TRYING [5]
% 22.35/3.45 % TRYING [5]
% 22.35/3.45 % (3201243)ott-21_1_sil=16000:fs=off:random_seed=774322658:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 22.35/3.45 % (3201236)Instruction limit reached!
% 22.35/3.45 % (3201236)------------------------------
% 22.35/3.45 % (3201236)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.58/9.28 % (3201236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.58/9.28 % (3201236)CaDiCaL version: 2.1.3
% 63.58/9.28 % (3201236)Termination reason: Instruction limit
% 63.58/9.28 % (3201236)Termination phase: Saturation
% 63.58/9.28 % (3201236)Time elapsed: 0.082 s
% 63.58/9.28 % (3201236)Peak memory usage: 16 MB
% 63.58/9.28 % (3201236)Instructions burned: 132 (million)
% 63.58/9.28 % (3201259)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3984401278:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 63.58/9.28 % (3201243)Instruction limit reached!
% 63.58/9.28 % (3201243)------------------------------
% 63.58/9.28 % (3201243)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.58/9.28 % (3201243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.58/9.28 % (3201243)CaDiCaL version: 2.1.3
% 63.58/9.28 % (3201243)Termination reason: Instruction limit
% 63.58/9.28 % (3201243)Termination phase: Saturation
% 63.58/9.28 % (3201243)Time elapsed: 0.099 s
% 63.58/9.28 % (3201243)Peak memory usage: 12 MB
% 63.58/9.28 % (3201243)Instructions burned: 181 (million)
% 63.58/9.28 % (3201261)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=986139778:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 63.58/9.28 % TRYING [1]
% 63.58/9.28 % TRYING [2]
% 63.58/9.28 % TRYING [3]
% 63.58/9.28 % TRYING [4]
% 63.58/9.28 % (3201226)Instruction limit reached!
% 63.58/9.28 % (3201226)------------------------------
% 63.58/9.28 % (3201226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.58/9.28 % (3201226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.58/9.28 % (3201226)CaDiCaL version: 2.1.3
% 63.58/9.28 % (3201226)Termination reason: Instruction limit
% 63.58/9.28 % (3201226)Termination phase: Finite model building SAT solving
% 63.58/9.28 % (3201226)Time elapsed: 0.221 s
% 63.58/9.28 % (3201226)Peak memory usage: 22 MB
% 63.58/9.28 % (3201226)Instructions burned: 715 (million)
% 63.58/9.28 % (3201263)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3763929825:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 63.58/9.28 % TRYING [5]
% 63.58/9.28 % TRYING [6]
% 63.58/9.28 % (3201259)Instruction limit reached!
% 63.58/9.28 % (3201259)------------------------------
% 63.58/9.28 % (3201259)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.58/9.28 % (3201259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.58/9.28 % (3201259)CaDiCaL version: 2.1.3
% 63.58/9.28 % (3201259)Termination reason: Instruction limit
% 63.58/9.28 % (3201259)Termination phase: Saturation
% 63.58/9.28 % (3201259)Time elapsed: 0.303 s
% 63.58/9.28 % (3201259)Peak memory usage: 15 MB
% 63.58/9.28 % (3201259)Instructions burned: 478 (million)
% 63.58/9.28 % (3201265)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2172252120:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 63.58/9.28 % (3201261)Instruction limit reached!
% 63.58/9.28 % (3201261)------------------------------
% 63.58/9.28 % (3201261)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.58/9.28 % (3201261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.58/9.28 % (3201261)CaDiCaL version: 2.1.3
% 63.58/9.28 % (3201261)Termination reason: Instruction limit
% 63.58/9.28 % (3201261)Termination phase: Finite model building SAT solving
% 63.58/9.28 % (3201261)Time elapsed: 0.344 s
% 63.58/9.28 % (3201261)Peak memory usage: 25 MB
% 63.58/9.28 % (3201261)Instructions burned: 866 (million)
% 63.58/9.28 % (3201267)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=3034489960:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2993 on theBenchmark for (2993ds/692Mi)
% 63.58/9.28 % (3201241)Instruction limit reached!
% 63.58/9.28 % (3201241)------------------------------
% 63.58/9.28 % (3201241)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.58/9.28 % (3201241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.58/9.28 % (3201241)CaDiCaL version: 2.1.3
% 63.58/9.28 % (3201241)Termination reason: Instruction limit
% 63.58/9.28 % (3201241)Termination phase: Saturation
% 63.58/9.28 % (3201241)Time elapsed: 0.527 s
% 63.58/9.28 % (3201241)Peak memory usage: 19 MB
% 63.58/9.28 % (3201241)Instructions burned: 686 (million)
% 63.58/9.28 % (3201263)Instruction limit reached!
% 63.58/9.28 % (3201263)------------------------------
% 63.58/9.28 % (3201263)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.58/9.28 % (3201263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.58/9.28 % (3201263)CaDiCaL version: 2.1.3
% 63.58/9.28 % (3201263)Termination reason: Instruction limit
% 63.58/9.28 % (3201263)Termination phase: Saturation
% 63.58/9.28 % (3201263)Time elapsed: 0.369 s
% 63.58/9.28 % (3201263)Peak memory usage: 24 MB
% 63.58/9.28 % (3201263)Instructions burned: 1181 (million)
% 63.58/9.28 % (3201269)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=373584230:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 63.58/9.28 % (3201270)fmb+10_1_sil=64000:random_seed=1970103678:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 63.58/9.28 % TRYING [1]
% 63.58/9.28 % TRYING [2]
% 63.58/9.28 % TRYING [3]
% 63.58/9.28 % TRYING [4]
% 63.58/9.28 % TRYING [14]
% 63.58/9.28 % TRYING [5]
% 63.58/9.28 % TRYING [6]
% 63.58/9.28 % (3201265)Instruction limit reached!
% 63.58/9.28 % (3201265)------------------------------
% 63.58/9.28 % (3201265)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.58/9.28 % (3201265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.58/9.28 % (3201265)CaDiCaL version: 2.1.3
% 63.58/9.28 % (3201265)Termination reason: Instruction limit
% 63.58/9.28 % (3201265)Termination phase: Finite model building constraint generation
% 63.58/9.28 % (3201265)Time elapsed: 0.425 s
% 63.58/9.28 % (3201265)Peak memory usage: 78 MB
% 63.58/9.28 % (3201265)Instructions burned: 890 (million)
% 63.58/9.28 % TRYING [7]
% 63.58/9.28 % (3201283)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3788310413:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 63.58/9.28 % TRYING [20]
% 63.58/9.28 % (3201267)Instruction limit reached!
% 63.58/9.28 % (3201267)------------------------------
% 63.58/9.28 % (3201267)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.58/9.28 % (3201267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.58/9.28 % (3201267)CaDiCaL version: 2.1.3
% 63.58/9.28 % (3201267)Termination reason: Instruction limit
% 63.58/9.28 % (3201267)Termination phase: Saturation
% 63.58/9.28 % (3201267)Time elapsed: 0.549 s
% 63.58/9.28 % (3201267)Peak memory usage: 17 MB
% 63.58/9.28 % (3201267)Instructions burned: 692 (million)
% 63.58/9.28 % (3201293)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3705034408:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 63.58/9.28 % TRYING [8]
% 63.58/9.28 % TRYING [6]
% 63.58/9.28 % (3201269)Instruction limit reached!
% 63.58/9.28 % (3201269)------------------------------
% 63.58/9.28 % (3201269)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.58/9.28 % (3201269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.58/9.28 % (3201269)CaDiCaL version: 2.1.3
% 63.58/9.28 % (3201269)Termination reason: Instruction limit
% 63.58/9.28 % (3201269)Termination phase: Saturation
% 63.58/9.28 % (3201269)Time elapsed: 0.720 s
% 63.58/9.28 % (3201269)Peak memory usage: 16 MB
% 63.58/9.28 % (3201269)Instructions burned: 879 (million)
% 63.58/9.28 % (3201298)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3877992325:i=5131_2985 on theBenchmark for (2985ds/5131Mi)
% 63.58/9.28 % (3201293)Instruction limit reached!
% 63.58/9.28 % (3201293)------------------------------
% 63.58/9.28 % (3201293)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.58/9.28 % (3201293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.58/9.28 % (3201293)CaDiCaL version: 2.1.3
% 63.58/9.28 % (3201293)Termination reason: Instruction limit
% 63.58/9.28 % (3201293)Termination phase: Finite model building constraint generation
% 63.58/9.28 % (3201293)Time elapsed: 0.600 s
% 63.58/9.28 % (3201293)Peak memory usage: 69 MB
% 63.58/9.28 % (3201293)Instructions burned: 921 (million)
% 63.58/9.28 % (3201308)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1852599655:i=1472:ins=7:fdi=8:gsp=on_2981 on theBenchmark for (2981ds/1472Mi)
% 63.58/9.28 % TRYING [8]
% 63.58/9.28 % (3201308)Instruction limit reached!
% 63.58/9.28 % (3201308)------------------------------
% 63.58/9.28 % (3201308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.58/9.28 % (3201308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.58/9.28 % (3201308)CaDiCaL version: 2.1.3
% 63.58/9.28 % (3201308)Termination reason: Instruction limit
% 63.58/9.28 % (3201308)Termination phase: Saturation
% 63.58/9.28 % (3201308)Time elapsed: 1.285 s
% 63.58/9.28 % (3201308)Peak memory usage: 25 MB
% 63.58/9.28 % (3201308)Instructions burned: 1472 (million)
% 63.58/9.28 % (3201324)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3086493265:i=6324_2968 on theBenchmark for (2968ds/6324Mi)
% 63.58/9.29 % TRYING [77]
% 63.58/9.29 % TRYING [9]
% 63.58/9.29 % (3201298)Instruction limit reached!
% 63.58/9.29 % (3201298)------------------------------
% 63.58/9.29 % (3201298)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.58/9.29 % (3201298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.58/9.29 % (3201298)CaDiCaL version: 2.1.3
% 63.58/9.29 % (3201298)Termination reason: Instruction limit
% 63.58/9.29 % (3201298)Termination phase: Saturation
% 63.58/9.29 % (3201298)Time elapsed: 4.072 s
% 63.58/9.29 % (3201298)Peak memory usage: 24 MB
% 63.58/9.29 % (3201298)Instructions burned: 5131 (million)
% 63.58/9.29 % (3201339)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=933382621:fmbsr=2.30978:i=2174_2944 on theBenchmark for (2944ds/2174Mi)
% 63.58/9.29 % TRYING [16]
% 63.58/9.29 % (3201283)Instruction limit reached!
% 63.58/9.29 % (3201283)------------------------------
% 63.58/9.29 % (3201283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.58/9.29 % (3201283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.58/9.29 % (3201283)CaDiCaL version: 2.1.3
% 63.58/9.29 % (3201283)Termination reason: Instruction limit
% 63.58/9.29 % (3201283)Termination phase: Finite model building constraint generation
% 63.58/9.29 % (3201283)Time elapsed: 5.543 s
% 63.58/9.29 % (3201283)Peak memory usage: 533 MB
% 63.58/9.29 % (3201283)Instructions burned: 9516 (million)
% 63.58/9.29 % (3201344)ott-2_1_sil=16000:newcnf=on:random_seed=1711715408:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2933 on theBenchmark for (2933ds/869Mi)
% 63.58/9.29 % (3201339)Instruction limit reached!
% 63.58/9.29 % (3201339)------------------------------
% 63.58/9.29 % (3201339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.58/9.29 % (3201339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.58/9.29 % (3201339)CaDiCaL version: 2.1.3
% 63.58/9.29 % (3201339)Termination reason: Instruction limit
% 63.58/9.29 % (3201339)Termination phase: Finite model building constraint generation
% 63.58/9.29 % (3201339)Time elapsed: 1.342 s
% 63.58/9.29 % (3201339)Peak memory usage: 131 MB
% 63.58/9.29 % (3201339)Instructions burned: 2175 (million)
% 63.58/9.29 % (3201347)ott+10_1_sil=32000:tgt=ground:random_seed=3198694419:i=5114:av=off_2931 on theBenchmark for (2931ds/5114Mi)
% 63.58/9.29 % (3201324)Instruction limit reached!
% 63.58/9.29 % (3201324)------------------------------
% 63.58/9.29 % (3201324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.58/9.29 % (3201324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.58/9.29 % (3201324)CaDiCaL version: 2.1.3
% 63.58/9.29 % (3201324)Termination reason: Instruction limit
% 63.58/9.29 % (3201324)Termination phase: Finite model building constraint generation
% 63.58/9.29 % (3201324)Time elapsed: 4.120 s
% 63.58/9.29 % (3201324)Peak memory usage: 416 MB
% 63.58/9.29 % (3201324)Instructions burned: 6325 (million)
% 63.58/9.29 % (3201352)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2398892651:i=54282_2926 on theBenchmark for (2926ds/54282Mi)
% 63.58/9.29 % TRYING [1]
% 63.58/9.29 % TRYING [2]
% 63.58/9.29 % TRYING [3]
% 63.58/9.29 % TRYING [4]
% 63.58/9.29 % (3201344)Instruction limit reached!
% 63.58/9.29 % (3201344)------------------------------
% 63.58/9.29 % (3201344)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.58/9.29 % (3201344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.58/9.29 % (3201344)CaDiCaL version: 2.1.3
% 63.58/9.29 % (3201344)Termination reason: Instruction limit
% 63.58/9.29 % (3201344)Termination phase: Saturation
% 63.58/9.29 % (3201344)Time elapsed: 0.767 s
% 63.58/9.29 % (3201344)Peak memory usage: 14 MB
% 63.58/9.29 % (3201344)Instructions burned: 869 (million)
% 63.58/9.29 % (3201354)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3644715587:i=3512:aac=none_2925 on theBenchmark for (2925ds/3512Mi)
% 63.58/9.29 % TRYING [5]
% 63.58/9.29 % TRYING [7]
% 63.58/9.29 % (3201347) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3201187-3201347"...
% 63.58/9.29 % (3201347)...printing done.
% 63.58/9.29 % (3201347)Refutation found. Thanks to Tanya!
% 63.58/9.29 % SZS status Unsatisfiable for theBenchmark
% 63.58/9.29 % SZS output start Proof for theBenchmark
% See solution above
% 63.58/9.29 % (3201347)------------------------------
% 63.58/9.29 % (3201347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.58/9.29 % (3201347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.58/9.29 % (3201347)CaDiCaL version: 2.1.3
% 63.58/9.29 % (3201347)Termination reason: Refutation
% 63.58/9.29 % (3201347)Time elapsed: 2.098 s
% 63.58/9.29 % (3201347)Peak memory usage: 27 MB
% 63.58/9.29 % (3201347)Instructions burned: 2151 (million)
% 63.58/9.29 % (3201187)Success in time 9.044 s
% 63.58/9.29 % Vampire exiting
%------------------------------------------------------------------------------