%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : GRP413-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n019.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 10:17:46 AM UTC 2026
% Result : Unsatisfiable 109.86s 15.99s
% Output : Refutation 109.86s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 2
% Syntax : Number of formulae : 45 ( 45 unt; 0 def)
% Number of atoms : 45 ( 44 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 26 ( 26 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 5 avg)
% Maximal term depth : 12 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 139 ( 139 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : multiply(X0,inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X0,inverse(X1))),X2))),X1))) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',single_axiom) ).
fof(f2,negated_conjecture,
multiply(multiply(inverse(b2),b2),a2) != a2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_these_axioms_2) ).
fof(f3,plain,
a2 != multiply(multiply(inverse(b2),b2),a2),
inference(reorient_equations,[],[f2]) ).
fof(f5,plain,
! [X2,X3,X0,X1] : inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),inverse(X3))),X0))),X3)) = multiply(X1,inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X0)),X2))),
inference(superposition,[],[f1,f1]) ).
fof(f23,plain,
! [X2,X3,X0,X1] : inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(X3))),inverse(X1))),multiply(inverse(multiply(X2,inverse(X3))),X0)))),X1)) = X0,
inference(superposition,[],[f5,f1]) ).
fof(f25,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(X2)),X1)))) = X2,
inference(superposition,[],[f1,f5]) ).
fof(f39,plain,
! [X2,X3,X0,X1] : multiply(multiply(multiply(inverse(X3),X3),inverse(multiply(inverse(multiply(multiply(inverse(X2),X2),inverse(X3))),X0))),X3) = multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(multiply(X0,X2)))),
inference(superposition,[],[f25,f1]) ).
fof(f55,plain,
! [X0,X1,X5] : inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,X5)))),X1)) = X5,
inference(superposition,[],[f23,f23]) ).
fof(f88,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,X0)) = multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,X0)),
inference(superposition,[],[f25,f55]) ).
fof(f116,plain,
! [X0,X1,X6,X5] : multiply(inverse(multiply(X1,X0)),multiply(X1,X5)) = multiply(inverse(multiply(X6,X0)),multiply(X6,X5)),
inference(superposition,[],[f88,f23]) ).
fof(f168,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X4,X1)),multiply(X4,X3)) = multiply(X0,multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,X0)))),X3)),
inference(superposition,[],[f116,f55]) ).
fof(f11495,plain,
! [X2,X0,X1] : multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(multiply(inverse(X2),X2),inverse(X1))),multiply(multiply(inverse(X2),X2),inverse(X0))))),X1) = X0,
inference(superposition,[],[f39,f25]) ).
fof(f11516,plain,
! [X2,X0,X1] : multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(multiply(X2,X1)))))) = X2,
inference(superposition,[],[f1,f39]) ).
fof(f15834,plain,
! [X2,X0,X1] : multiply(inverse(X0),X0) = multiply(inverse(multiply(X1,X2)),multiply(X1,X2)),
inference(superposition,[],[f168,f11495]) ).
fof(f16094,plain,
! [X0,X1] : multiply(inverse(X1),X1) = multiply(inverse(X0),X0),
inference(superposition,[],[f15834,f11495]) ).
fof(f16541,plain,
! [X0,X1] : multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(X0),X0))),X1) = X1,
inference(superposition,[],[f11495,f15834]) ).
fof(f17005,plain,
! [X0] : a2 != multiply(multiply(inverse(X0),X0),a2),
inference(superposition,[],[f3,f16094]) ).
fof(f17493,plain,
! [X2,X0,X1] : a2 != multiply(multiply(X0,multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,X0)))),X1)),a2),
inference(superposition,[],[f17005,f55]) ).
fof(f18574,plain,
! [X0,X1] : a2 != multiply(multiply(inverse(X1),multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(X0),X0))),X1)),a2),
inference(superposition,[],[f17493,f15834]) ).
fof(f18661,plain,
! [X2,X0,X1] : a2 != multiply(multiply(inverse(X1),multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(X2),X2))),X1)),a2),
inference(superposition,[],[f18574,f16094]) ).
fof(f18975,plain,
! [X2,X3,X0,X1] : a2 != multiply(multiply(inverse(multiply(X0,X1)),multiply(X0,multiply(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(X3),X3))),X1))),a2),
inference(superposition,[],[f18661,f116]) ).
fof(f20399,plain,
! [X2,X0,X1] : a2 != multiply(multiply(inverse(multiply(inverse(X1),X2)),multiply(inverse(multiply(X0,X1)),multiply(X0,X2))),a2),
inference(superposition,[],[f18975,f168]) ).
fof(f20637,plain,
! [X2,X3,X0,X1,X4] : a2 != multiply(multiply(inverse(multiply(inverse(X3),multiply(X4,X2))),multiply(inverse(multiply(inverse(multiply(X4,X1)),X3)),multiply(inverse(multiply(X0,X1)),multiply(X0,X2)))),a2),
inference(superposition,[],[f20399,f116]) ).
fof(f76824,plain,
! [X2,X0,X1] : multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(X2),X2))),X1) = X1,
inference(superposition,[],[f16541,f16094]) ).
fof(f100607,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X1,X2)),multiply(X1,X0)) = multiply(inverse(X2),X0),
inference(superposition,[],[f168,f76824]) ).
fof(f100866,plain,
! [X2,X3,X0,X1,X4,X5] : a2 != multiply(multiply(inverse(multiply(inverse(X1),multiply(X2,X3))),multiply(inverse(multiply(inverse(multiply(X2,X0)),X1)),multiply(inverse(X0),multiply(multiply(multiply(inverse(X4),X4),inverse(multiply(inverse(X5),X5))),X3)))),a2),
inference(superposition,[],[f20637,f76824]) ).
fof(f101378,plain,
! [X2,X3,X0,X1] : a2 != multiply(multiply(inverse(multiply(inverse(X1),multiply(X2,X3))),multiply(inverse(multiply(inverse(multiply(X2,X0)),X1)),multiply(inverse(X0),X3))),a2),
inference(forward_demodulation,[],[f100866,f76824]) ).
fof(f114027,plain,
! [X2,X0,X1] : multiply(inverse(X1),X2) = multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X1),X2)),
inference(superposition,[],[f100607,f16094]) ).
fof(f132835,plain,
! [X3,X0] : multiply(inverse(multiply(inverse(X3),X3)),X0) = X0,
inference(superposition,[],[f114027,f1]) ).
fof(f138915,plain,
! [X2,X3,X0,X1] : a2 != multiply(multiply(inverse(multiply(inverse(X1),multiply(X2,X0))),multiply(inverse(multiply(inverse(multiply(X2,multiply(inverse(X3),X3))),X1)),X0)),a2),
inference(superposition,[],[f101378,f132835]) ).
fof(f143493,plain,
! [X2,X3,X0,X1,X4,X5] : a2 != multiply(multiply(inverse(multiply(X0,multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,X0)))),X3))),multiply(inverse(multiply(inverse(multiply(X4,multiply(inverse(X5),X5))),multiply(X4,X1))),X3)),a2),
inference(superposition,[],[f138915,f168]) ).
fof(f144066,plain,
! [X2,X3,X0,X1,X5] : a2 != multiply(multiply(inverse(multiply(X0,multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,X0)))),X3))),multiply(inverse(multiply(inverse(multiply(inverse(X5),X5)),X1)),X3)),a2),
inference(forward_demodulation,[],[f143493,f100607]) ).
fof(f144286,plain,
! [X2,X3,X0,X1] : a2 != multiply(multiply(inverse(multiply(X0,multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,X0)))),X3))),multiply(inverse(X1),X3)),a2),
inference(forward_demodulation,[],[f144066,f132835]) ).
fof(f144350,plain,
! [X3,X0,X1] : a2 != multiply(multiply(inverse(multiply(X0,multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(inverse(X1)),X0))),X3))),multiply(inverse(X1),X3)),a2),
inference(forward_demodulation,[],[f144286,f100607]) ).
fof(f161600,plain,
! [X2,X3,X0,X1] : a2 != multiply(multiply(inverse(multiply(X1,multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(inverse(X2)),X1))),X3))),multiply(inverse(X2),X3)),a2),
inference(superposition,[],[f144350,f16094]) ).
fof(f168534,plain,
! [X2,X0,X1,X6] : a2 != multiply(multiply(inverse(multiply(X1,multiply(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(X0),X1))),X6))),multiply(X0,X6)),a2),
inference(superposition,[],[f161600,f23]) ).
fof(f169077,plain,
! [X2,X3,X0,X1] : a2 != multiply(multiply(inverse(multiply(multiply(X1,inverse(multiply(X0,X2))),multiply(X0,X3))),multiply(multiply(X1,inverse(X2)),X3)),a2),
inference(superposition,[],[f168534,f11516]) ).
fof(f169769,plain,
! [X2,X0,X1] : a2 != multiply(multiply(inverse(multiply(inverse(X0),X1)),multiply(multiply(multiply(inverse(X2),X2),inverse(X0)),X1)),a2),
inference(superposition,[],[f169077,f76824]) ).
fof(f170326,plain,
! [X0,X1] : a2 != multiply(multiply(multiply(multiply(inverse(X0),X0),inverse(X1)),X1),a2),
inference(superposition,[],[f169769,f132835]) ).
fof(f170638,plain,
! [X2,X0,X1] : a2 != multiply(multiply(X0,multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,inverse(multiply(X0,X1))))),a2),
inference(superposition,[],[f170326,f11516]) ).
fof(f170666,plain,
! [X0,X1] : a2 != multiply(multiply(X0,multiply(inverse(inverse(X1)),inverse(multiply(X0,X1)))),a2),
inference(forward_demodulation,[],[f170638,f100607]) ).
fof(f170804,plain,
! [X0,X1] : a2 != multiply(multiply(inverse(X1),multiply(inverse(inverse(X1)),inverse(multiply(inverse(X0),X0)))),a2),
inference(superposition,[],[f170666,f16094]) ).
fof(f171244,plain,
! [X0,X4] : a2 != multiply(multiply(X0,multiply(inverse(X0),inverse(multiply(inverse(X4),X4)))),a2),
inference(superposition,[],[f170804,f23]) ).
fof(f171531,plain,
! [X0,X1] : a2 != multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(X0),X0))),a2),
inference(superposition,[],[f171244,f132835]) ).
fof(f171571,plain,
$false,
inference(forward_subsumption_resolution,[],[f171531,f76824]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP413-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.37 % Computer : n019.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 27 10:03:49 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
% 22.27/3.64 % (2852300)Will run a generic schedule for satisfiability detection.
% 22.27/3.64 % (2852313)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3886898887:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 22.27/3.64 % (2852309)% WARNING: option uhcvi not known.
% 22.27/3.64 % (2852308)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1621468860_2999 on theBenchmark for (2999ds/0Mi)
% 22.27/3.64 % (2852310)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2749932723:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 22.27/3.64 % (2852309)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2357650829:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 22.27/3.64 % (2852312)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1362358316:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 22.27/3.64 % (2852311)dis+10_1_sil=32000:sp=arity:random_seed=2798802278:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 22.27/3.64 % (2852314)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4237787234:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 22.27/3.64 % TRYING [1]
% 22.27/3.64 % TRYING [2]
% 22.27/3.64 % TRYING [3]
% 22.27/3.64 % TRYING [4]
% 22.27/3.64 % (2852313)Instruction limit reached!
% 22.27/3.64 % (2852313)------------------------------
% 22.27/3.64 % (2852313)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.27/3.64 % (2852313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.27/3.64 % (2852313)CaDiCaL version: 2.1.3
% 22.27/3.64 % (2852313)Termination reason: Instruction limit
% 22.27/3.64 % (2852313)Termination phase: Saturation
% 22.27/3.64 % (2852313)Time elapsed: 0.039 s
% 22.27/3.64 % (2852313)Peak memory usage: 13 MB
% 22.27/3.64 % (2852313)Instructions burned: 132 (million)
% 22.27/3.64 % (2852322)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=851432790:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 22.27/3.64 % TRYING [1]
% 22.27/3.64 % TRYING [2]
% 22.27/3.64 % TRYING [3]
% 22.27/3.64 % (2852311)Instruction limit reached!
% 22.27/3.64 % (2852311)------------------------------
% 22.27/3.64 % (2852311)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.27/3.64 % (2852311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.27/3.64 % (2852311)CaDiCaL version: 2.1.3
% 22.27/3.64 % (2852311)Termination reason: Instruction limit
% 22.27/3.64 % (2852311)Termination phase: Saturation
% 22.27/3.64 % (2852311)Time elapsed: 0.056 s
% 22.27/3.64 % (2852311)Peak memory usage: 12 MB
% 22.27/3.64 % (2852311)Instructions burned: 106 (million)
% 22.27/3.64 % TRYING [4]
% 22.27/3.64 % (2852312)Instruction limit reached!
% 22.27/3.64 % (2852312)------------------------------
% 22.27/3.64 % (2852312)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.27/3.64 % (2852312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.27/3.64 % (2852312)CaDiCaL version: 2.1.3
% 22.27/3.64 % (2852312)Termination reason: Instruction limit
% 22.27/3.64 % (2852312)Termination phase: Saturation
% 22.27/3.64 % (2852312)Time elapsed: 0.066 s
% 22.27/3.64 % (2852312)Peak memory usage: 12 MB
% 22.27/3.64 % (2852312)Instructions burned: 116 (million)
% 22.27/3.64 % (2852324)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1658381400:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 22.27/3.64 % (2852325)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=3448231671:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 22.27/3.64 % (2852314)Instruction limit reached!
% 22.27/3.64 % (2852314)------------------------------
% 22.27/3.64 % (2852314)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.27/3.64 % (2852314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.27/3.64 % (2852314)CaDiCaL version: 2.1.3
% 22.27/3.64 % (2852314)Termination reason: Instruction limit
% 22.27/3.64 % (2852314)Termination phase: Saturation
% 22.27/3.64 % (2852314)Time elapsed: 0.098 s
% 22.27/3.64 % (2852314)Peak memory usage: 13 MB
% 22.27/3.64 % (2852314)Instructions burned: 160 (million)
% 22.27/3.64 % (2852328)ott-21_1_sil=16000:fs=off:random_seed=2747119004:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 22.27/3.64 % (2852324)Instruction limit reached!
% 22.27/3.64 % (2852324)------------------------------
% 22.27/3.64 % (2852324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.27/3.64 % (2852324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.56/7.47 % (2852324)CaDiCaL version: 2.1.3
% 49.56/7.47 % (2852324)Termination reason: Instruction limit
% 49.56/7.47 % (2852324)Termination phase: Saturation
% 49.56/7.47 % (2852324)Time elapsed: 0.073 s
% 49.56/7.47 % (2852324)Peak memory usage: 12 MB
% 49.56/7.47 % (2852324)Instructions burned: 132 (million)
% 49.56/7.47 % (2852330)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=755073261:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 49.56/7.47 % (2852328)Instruction limit reached!
% 49.56/7.47 % (2852328)------------------------------
% 49.56/7.47 % (2852328)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.56/7.47 % (2852328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.56/7.47 % (2852328)CaDiCaL version: 2.1.3
% 49.56/7.47 % (2852328)Termination reason: Instruction limit
% 49.56/7.47 % (2852328)Termination phase: Saturation
% 49.56/7.47 % (2852328)Time elapsed: 0.096 s
% 49.56/7.47 % (2852328)Peak memory usage: 12 MB
% 49.56/7.47 % (2852328)Instructions burned: 180 (million)
% 49.56/7.47 % (2852336)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=187983948:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 49.56/7.48 % TRYING [1]
% 49.56/7.48 % TRYING [2]
% 49.56/7.48 % TRYING [3]
% 49.56/7.48 % (2852322)Instruction limit reached!
% 49.56/7.48 % (2852322)------------------------------
% 49.56/7.48 % (2852322)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.56/7.48 % (2852322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.56/7.48 % (2852322)CaDiCaL version: 2.1.3
% 49.56/7.48 % (2852322)Termination reason: Instruction limit
% 49.56/7.48 % (2852322)Termination phase: Finite model building SAT solving
% 49.56/7.48 % (2852322)Time elapsed: 0.219 s
% 49.56/7.48 % (2852322)Peak memory usage: 12 MB
% 49.56/7.48 % (2852322)Instructions burned: 717 (million)
% 49.56/7.48 % TRYING [4]
% 49.56/7.48 % (2852347)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=986227204:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 49.56/7.48 % (2852330)Instruction limit reached!
% 49.56/7.48 % (2852330)------------------------------
% 49.56/7.48 % (2852330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.56/7.48 % (2852330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.56/7.48 % (2852330)CaDiCaL version: 2.1.3
% 49.56/7.48 % (2852330)Termination reason: Instruction limit
% 49.56/7.48 % (2852330)Termination phase: Saturation
% 49.56/7.48 % (2852330)Time elapsed: 0.242 s
% 49.56/7.48 % (2852330)Peak memory usage: 15 MB
% 49.56/7.48 % (2852330)Instructions burned: 479 (million)
% 49.56/7.48 % (2852349)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=32324415:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 49.56/7.48 % (2852325)Instruction limit reached!
% 49.56/7.48 % (2852325)------------------------------
% 49.56/7.48 % (2852325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.56/7.48 % (2852325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.56/7.48 % (2852325)CaDiCaL version: 2.1.3
% 49.56/7.48 % (2852325)Termination reason: Instruction limit
% 49.56/7.48 % (2852325)Termination phase: Saturation
% 49.56/7.48 % (2852325)Time elapsed: 0.350 s
% 49.56/7.48 % (2852325)Peak memory usage: 17 MB
% 49.56/7.48 % (2852325)Instructions burned: 684 (million)
% 49.56/7.48 % (2852351)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=2016969195: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)
% 49.56/7.48 % TRYING [14]
% 49.56/7.48 % (2852347)Instruction limit reached!
% 49.56/7.48 % (2852347)------------------------------
% 49.56/7.48 % (2852347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.56/7.48 % (2852347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.56/7.48 % (2852347)CaDiCaL version: 2.1.3
% 49.56/7.48 % (2852347)Termination reason: Instruction limit
% 49.56/7.48 % (2852347)Termination phase: Saturation
% 49.56/7.48 % (2852347)Time elapsed: 0.342 s
% 49.56/7.48 % (2852347)Peak memory usage: 24 MB
% 49.56/7.48 % (2852347)Instructions burned: 1179 (million)
% 49.56/7.48 % (2852353)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=604834228:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 49.56/7.48 % (2852349)Instruction limit reached!
% 49.56/7.48 % (2852349)------------------------------
% 49.56/7.48 % (2852349)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 109.86/15.99 % (2852349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.86/15.99 % (2852349)CaDiCaL version: 2.1.3
% 109.86/15.99 % (2852349)Termination reason: Instruction limit
% 109.86/15.99 % (2852349)Termination phase: Finite model building constraint generation
% 109.86/15.99 % (2852349)Time elapsed: 0.313 s
% 109.86/15.99 % (2852349)Peak memory usage: 81 MB
% 109.86/15.99 % (2852349)Instructions burned: 892 (million)
% 109.86/15.99 % (2852355)fmb+10_1_sil=64000:random_seed=3702292470:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 109.86/15.99 % TRYING [1]
% 109.86/15.99 % TRYING [2]
% 109.86/15.99 % TRYING [3]
% 109.86/15.99 % TRYING [4]
% 109.86/15.99 % (2852336)Instruction limit reached!
% 109.86/15.99 % (2852336)------------------------------
% 109.86/15.99 % (2852336)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 109.86/15.99 % (2852336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.86/15.99 % (2852336)CaDiCaL version: 2.1.3
% 109.86/15.99 % (2852336)Termination reason: Instruction limit
% 109.86/15.99 % (2852336)Termination phase: Finite model building SAT solving
% 109.86/15.99 % (2852336)Time elapsed: 0.596 s
% 109.86/15.99 % (2852336)Peak memory usage: 12 MB
% 109.86/15.99 % (2852336)Instructions burned: 865 (million)
% 109.86/15.99 % (2852351)Instruction limit reached!
% 109.86/15.99 % (2852351)------------------------------
% 109.86/15.99 % (2852351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 109.86/15.99 % (2852351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.86/15.99 % (2852351)CaDiCaL version: 2.1.3
% 109.86/15.99 % (2852351)Termination reason: Instruction limit
% 109.86/15.99 % (2852351)Termination phase: Saturation
% 109.86/15.99 % (2852351)Time elapsed: 0.420 s
% 109.86/15.99 % (2852351)Peak memory usage: 17 MB
% 109.86/15.99 % (2852351)Instructions burned: 692 (million)
% 109.86/15.99 % (2852353)Instruction limit reached!
% 109.86/15.99 % (2852353)------------------------------
% 109.86/15.99 % (2852353)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 109.86/15.99 % (2852353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.86/15.99 % (2852353)CaDiCaL version: 2.1.3
% 109.86/15.99 % (2852353)Termination reason: Instruction limit
% 109.86/15.99 % (2852353)Termination phase: Saturation
% 109.86/15.99 % (2852353)Time elapsed: 0.244 s
% 109.86/15.99 % (2852353)Peak memory usage: 18 MB
% 109.86/15.99 % (2852353)Instructions burned: 880 (million)
% 109.86/15.99 % (2852360)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=632533746:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 109.86/15.99 % TRYING [20]
% 109.86/15.99 % (2852367)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2170601950:i=5131_2990 on theBenchmark for (2990ds/5131Mi)
% 109.86/15.99 % (2852366)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1229678089:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 109.86/15.99 % TRYING [8]
% 109.86/15.99 % (2852366)Instruction limit reached!
% 109.86/15.99 % (2852366)------------------------------
% 109.86/15.99 % (2852366)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 109.86/15.99 % (2852366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.86/15.99 % (2852366)CaDiCaL version: 2.1.3
% 109.86/15.99 % (2852366)Termination reason: Instruction limit
% 109.86/15.99 % (2852366)Termination phase: Finite model building SAT solving
% 109.86/15.99 % (2852366)Time elapsed: 0.689 s
% 109.86/15.99 % (2852366)Peak memory usage: 39 MB
% 109.86/15.99 % (2852366)Instructions burned: 921 (million)
% 109.86/15.99 % (2852384)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1710562951:i=1472:ins=7:fdi=8:gsp=on_2983 on theBenchmark for (2983ds/1472Mi)
% 109.86/15.99 % TRYING [5]
% 109.86/15.99 % (2852384)Instruction limit reached!
% 109.86/15.99 % (2852384)------------------------------
% 109.86/15.99 % (2852384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 109.86/15.99 % (2852384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.86/15.99 % (2852384)CaDiCaL version: 2.1.3
% 109.86/15.99 % (2852384)Termination reason: Instruction limit
% 109.86/15.99 % (2852384)Termination phase: Saturation
% 109.86/15.99 % (2852384)Time elapsed: 1.162 s
% 109.86/15.99 % (2852384)Peak memory usage: 27 MB
% 109.86/15.99 % (2852384)Instructions burned: 1472 (million)
% 109.86/15.99 % (2852392)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1828977665:i=6324_2971 on theBenchmark for (2971ds/6324Mi)
% 109.86/15.99 % TRYING [77]
% 109.86/15.99 % (2852367)Instruction limit reached!
% 109.86/15.99 % (2852367)------------------------------
% 109.86/15.99 % (2852367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 109.86/15.99 % (2852367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.86/15.99 % (2852367)CaDiCaL version: 2.1.3
% 109.86/15.99 % (2852367)Termination reason: Instruction limit
% 109.86/15.99 % (2852367)Termination phase: Saturation
% 109.86/15.99 % (2852367)Time elapsed: 2.291 s
% 109.86/15.99 % (2852367)Peak memory usage: 46 MB
% 109.86/15.99 % (2852367)Instructions burned: 5133 (million)
% 109.86/15.99 % (2852394)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3836830859:fmbsr=2.30978:i=2174_2967 on theBenchmark for (2967ds/2174Mi)
% 109.86/15.99 % TRYING [16]
% 109.86/15.99 % (2852394)Instruction limit reached!
% 109.86/15.99 % (2852394)------------------------------
% 109.86/15.99 % (2852394)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 109.86/15.99 % (2852394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.86/15.99 % (2852394)CaDiCaL version: 2.1.3
% 109.86/15.99 % (2852394)Termination reason: Instruction limit
% 109.86/15.99 % (2852394)Termination phase: Finite model building constraint generation
% 109.86/15.99 % (2852394)Time elapsed: 0.817 s
% 109.86/15.99 % (2852394)Peak memory usage: 153 MB
% 109.86/15.99 % (2852394)Instructions burned: 2176 (million)
% 109.86/15.99 % (2852398)ott-2_1_sil=16000:newcnf=on:random_seed=3886742536:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2959 on theBenchmark for (2959ds/869Mi)
% 109.86/15.99 % (2852398)Instruction limit reached!
% 109.86/15.99 % (2852398)------------------------------
% 109.86/15.99 % (2852398)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 109.86/15.99 % (2852398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.86/15.99 % (2852398)CaDiCaL version: 2.1.3
% 109.86/15.99 % (2852398)Termination reason: Instruction limit
% 109.86/15.99 % (2852398)Termination phase: Saturation
% 109.86/15.99 % (2852398)Time elapsed: 0.447 s
% 109.86/15.99 % (2852398)Peak memory usage: 22 MB
% 109.86/15.99 % (2852398)Instructions burned: 871 (million)
% 109.86/15.99 % (2852401)ott+10_1_sil=32000:tgt=ground:random_seed=162093534:i=5114:av=off_2954 on theBenchmark for (2954ds/5114Mi)
% 109.86/15.99 % (2852392)Instruction limit reached!
% 109.86/15.99 % (2852392)------------------------------
% 109.86/15.99 % (2852392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 109.86/15.99 % (2852392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.86/15.99 % (2852392)CaDiCaL version: 2.1.3
% 109.86/15.99 % (2852392)Termination reason: Instruction limit
% 109.86/15.99 % (2852392)Termination phase: Finite model building constraint generation
% 109.86/15.99 % (2852392)Time elapsed: 3.080 s
% 109.86/15.99 % (2852392)Peak memory usage: 522 MB
% 109.86/15.99 % (2852392)Instructions burned: 6327 (million)
% 109.86/15.99 % TRYING [5]
% 109.86/15.99 % (2852555)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=742840465:i=54282_2940 on theBenchmark for (2940ds/54282Mi)
% 109.86/15.99 % TRYING [1]
% 109.86/15.99 % TRYING [2]
% 109.86/15.99 % TRYING [3]
% 109.86/15.99 % TRYING [4]
% 109.86/15.99 % (2852360)Instruction limit reached!
% 109.86/15.99 % (2852360)------------------------------
% 109.86/15.99 % (2852360)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 109.86/15.99 % (2852360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.86/15.99 % (2852360)CaDiCaL version: 2.1.3
% 109.86/15.99 % (2852360)Termination reason: Instruction limit
% 109.86/15.99 % (2852360)Termination phase: Finite model building constraint generation
% 109.86/15.99 % (2852360)Time elapsed: 5.163 s
% 109.86/15.99 % (2852360)Peak memory usage: 652 MB
% 109.86/15.99 % (2852360)Instructions burned: 9516 (million)
% 109.86/15.99 % (2852401)Instruction limit reached!
% 109.86/15.99 % (2852401)------------------------------
% 109.86/15.99 % (2852401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 109.86/15.99 % (2852401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.86/15.99 % (2852401)CaDiCaL version: 2.1.3
% 109.86/15.99 % (2852401)Termination reason: Instruction limit
% 109.86/15.99 % (2852401)Termination phase: Saturation
% 109.86/15.99 % (2852401)Time elapsed: 1.567 s
% 109.86/15.99 % (2852401)Peak memory usage: 62 MB
% 109.86/15.99 % (2852401)Instructions burned: 5117 (million)
% 109.86/15.99 % (2852557)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=70000423:i=3512:aac=none_2938 on theBenchmark for (2938ds/3512Mi)
% 109.86/15.99 % (2852558)dis+21_1_sil=32000:sas=cadical:random_seed=1016856613:i=3773:amm=off_2938 on theBenchmark for (2938ds/3773Mi)
% 109.86/15.99 % (2852557)Instruction limit reached!
% 109.86/15.99 % (2852557)------------------------------
% 109.86/15.99 % (2852557)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 109.86/15.99 % (2852557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.86/15.99 % (2852557)CaDiCaL version: 2.1.3
% 109.86/15.99 % (2852557)Termination reason: Instruction limit
% 109.86/15.99 % (2852557)Termination phase: Saturation
% 109.86/15.99 % (2852557)Time elapsed: 0.904 s
% 109.86/15.99 % (2852557)Peak memory usage: 40 MB
% 109.86/15.99 % (2852557)Instructions burned: 3512 (million)
% 109.86/15.99 % (2852561)ott+11_1_sil=16000:gs=on:random_seed=4205567098:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2929 on theBenchmark for (2929ds/2251Mi)
% 109.86/15.99 % TRYING [5]
% 109.86/15.99 % (2852561)Instruction limit reached!
% 109.86/15.99 % (2852561)------------------------------
% 109.86/15.99 % (2852561)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 109.86/15.99 % (2852561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.86/15.99 % (2852561)CaDiCaL version: 2.1.3
% 109.86/15.99 % (2852561)Termination reason: Instruction limit
% 109.86/15.99 % (2852561)Termination phase: Saturation
% 109.86/15.99 % (2852561)Time elapsed: 0.628 s
% 109.86/15.99 % (2852561)Peak memory usage: 36 MB
% 109.86/15.99 % (2852561)Instructions burned: 2253 (million)
% 109.86/15.99 % (2852563)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2858325770:fmbsr=1.6:i=67534_2922 on theBenchmark for (2922ds/67534Mi)
% 109.86/15.99 % TRYING [7]
% 109.86/15.99 % (2852558)Instruction limit reached!
% 109.86/15.99 % (2852558)------------------------------
% 109.86/15.99 % (2852558)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 109.86/15.99 % (2852558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.86/15.99 % (2852558)CaDiCaL version: 2.1.3
% 109.86/15.99 % (2852558)Termination reason: Instruction limit
% 109.86/15.99 % (2852558)Termination phase: Saturation
% 109.86/15.99 % (2852558)Time elapsed: 1.819 s
% 109.86/15.99 % (2852558)Peak memory usage: 40 MB
% 109.86/15.99 % (2852558)Instructions burned: 3773 (million)
% 109.86/15.99 % (2852565)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2364020297:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2920 on theBenchmark for (2920ds/4591Mi)
% 109.86/15.99 % (2852565)Instruction limit reached!
% 109.86/15.99 % (2852565)------------------------------
% 109.86/15.99 % (2852565)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 109.86/15.99 % (2852565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.86/15.99 % (2852565)CaDiCaL version: 2.1.3
% 109.86/15.99 % (2852565)Termination reason: Instruction limit
% 109.86/15.99 % (2852565)Termination phase: Saturation
% 109.86/15.99 % (2852565)Time elapsed: 1.774 s
% 109.86/15.99 % (2852565)Peak memory usage: 31 MB
% 109.86/15.99 % (2852565)Instructions burned: 4592 (million)
% 109.86/15.99 % (2852567)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2456141525:i=29340_2902 on theBenchmark for (2902ds/29340Mi)
% 109.86/15.99 % (2852355)Instruction limit reached!
% 109.86/15.99 % (2852355)------------------------------
% 109.86/15.99 % (2852355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 109.86/15.99 % (2852355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.86/15.99 % (2852355)CaDiCaL version: 2.1.3
% 109.86/15.99 % (2852355)Termination reason: Instruction limit
% 109.86/15.99 % (2852355)Termination phase: Finite model building SAT solving
% 109.86/15.99 % (2852355)Time elapsed: 13.173 s
% 109.86/15.99 % (2852355)Peak memory usage: 17 MB
% 109.86/15.99 % (2852355)Instructions burned: 22062 (million)
% 109.86/15.99 % (2852685)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1027781840:i=5211_2860 on theBenchmark for (2860ds/5211Mi)
% 109.86/15.99 % (2852310) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2852300-2852310"...
% 109.86/15.99 % (2852310)...printing done.
% 109.86/15.99 % (2852310)Refutation found. Thanks to Tanya!
% 109.86/15.99 % SZS status Unsatisfiable for theBenchmark
% 109.86/15.99 % SZS output start Proof for theBenchmark
% See solution above
% 109.86/15.99 % (2852310)------------------------------
% 109.86/15.99 % (2852310)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 109.86/15.99 % (2852310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.86/15.99 % (2852310)CaDiCaL version: 2.1.3
% 109.86/15.99 % (2852310)Termination reason: Refutation
% 109.86/15.99 % (2852310)Time elapsed: 15.479 s
% 109.86/15.99 % (2852310)Peak memory usage: 121 MB
% 109.86/15.99 % (2852310)Instructions burned: 38476 (million)
% 109.86/15.99 % (2852300)Success in time 15.579 s
% 109.86/15.99 % Vampire exiting
%------------------------------------------------------------------------------