%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LAT153-1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n004.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:57 AM UTC 2026
% Result : Unsatisfiable 73.47s 11.06s
% Output : Refutation 73.47s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 20
% Syntax : Number of formulae : 140 ( 140 unt; 10 def)
% Number of atoms : 140 ( 139 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 13 con; 0-2 aty)
% Number of variables : 125 ( 125 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : meet(X0,X0) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/LAT001-0.ax',idempotence_of_meet) ).
fof(f2,axiom,
! [X0] : join(X0,X0) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/LAT001-0.ax',idempotence_of_join) ).
fof(f3,axiom,
! [X0,X1] : meet(X0,join(X0,X1)) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/LAT001-0.ax',absorption1) ).
fof(f4,axiom,
! [X0,X1] : join(X0,meet(X0,X1)) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/LAT001-0.ax',absorption2) ).
fof(f5,axiom,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
file('/export/starexec/sandbox2/benchmark/Axioms/LAT001-0.ax',commutativity_of_meet) ).
fof(f6,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox2/benchmark/Axioms/LAT001-0.ax',commutativity_of_join) ).
fof(f7,axiom,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X1,X2)),
file('/export/starexec/sandbox2/benchmark/Axioms/LAT001-0.ax',associativity_of_meet) ).
fof(f8,axiom,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X0,join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/Axioms/LAT001-0.ax',associativity_of_join) ).
fof(f9,axiom,
! [X2,X3,X0,X1] : meet(X0,join(X1,meet(X2,join(X0,X3)))) = meet(X0,join(X1,meet(X2,join(X3,meet(X2,join(X0,X1)))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',equation_H40) ).
fof(f10,negated_conjecture,
meet(a,join(b,meet(a,c))) != meet(a,join(b,meet(a,join(meet(a,b),meet(c,join(a,b)))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_H7) ).
fof(f11,definition,
sF0 = meet(a,c),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f12,plain,
meet(a,c) = sF0,
inference(reorient_equations,[],[f11]) ).
fof(f13,definition,
sF1 = join(b,sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f14,plain,
join(b,sF0) = sF1,
inference(reorient_equations,[],[f13]) ).
fof(f15,definition,
sF2 = meet(a,sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f16,plain,
meet(a,sF1) = sF2,
inference(reorient_equations,[],[f15]) ).
fof(f17,definition,
sF3 = meet(a,b),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f18,plain,
meet(a,b) = sF3,
inference(reorient_equations,[],[f17]) ).
fof(f19,definition,
sF4 = join(a,b),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f20,plain,
join(a,b) = sF4,
inference(reorient_equations,[],[f19]) ).
fof(f21,definition,
sF5 = meet(c,sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f22,plain,
meet(c,sF4) = sF5,
inference(reorient_equations,[],[f21]) ).
fof(f23,definition,
sF6 = join(sF3,sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f24,plain,
join(sF3,sF5) = sF6,
inference(reorient_equations,[],[f23]) ).
fof(f25,definition,
sF7 = meet(a,sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f26,plain,
meet(a,sF6) = sF7,
inference(reorient_equations,[],[f25]) ).
fof(f27,definition,
sF8 = join(b,sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f28,plain,
join(b,sF7) = sF8,
inference(reorient_equations,[],[f27]) ).
fof(f29,definition,
sF9 = meet(a,sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f30,plain,
meet(a,sF8) = sF9,
inference(reorient_equations,[],[f29]) ).
fof(f31,plain,
sF2 != sF9,
inference(definition_folding,[],[f10,f30,f28,f26,f24,f22,f20,f18,f16,f14,f12]) ).
fof(f33,plain,
a = meet(a,sF4),
inference(superposition,[],[f3,f20]) ).
fof(f34,plain,
b = meet(b,sF1),
inference(superposition,[],[f3,f14]) ).
fof(f35,plain,
b = meet(b,sF8),
inference(superposition,[],[f3,f28]) ).
fof(f49,plain,
! [X0,X1] : join(X1,meet(X0,X1)) = X1,
inference(superposition,[],[f4,f5]) ).
fof(f52,plain,
! [X0,X1] : meet(X1,join(X0,X1)) = X1,
inference(superposition,[],[f3,f6]) ).
fof(f54,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X0,X1)),
inference(superposition,[],[f7,f1]) ).
fof(f57,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X1,meet(X0,X2)),
inference(superposition,[],[f7,f5]) ).
fof(f59,plain,
! [X0] : meet(a,meet(b,X0)) = meet(sF3,X0),
inference(superposition,[],[f7,f18]) ).
fof(f60,plain,
! [X0] : meet(a,meet(c,X0)) = meet(sF0,X0),
inference(superposition,[],[f7,f12]) ).
fof(f62,plain,
! [X0] : meet(a,meet(sF4,X0)) = meet(a,X0),
inference(superposition,[],[f7,f33]) ).
fof(f63,plain,
! [X0] : meet(a,meet(sF6,X0)) = meet(sF7,X0),
inference(superposition,[],[f7,f26]) ).
fof(f67,plain,
! [X0] : meet(c,meet(sF4,X0)) = meet(sF5,X0),
inference(superposition,[],[f7,f22]) ).
fof(f76,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X2,meet(X0,X1)),
inference(superposition,[],[f5,f7]) ).
fof(f82,plain,
! [X2,X0,X1] : join(X0,join(meet(X0,X1),X2)) = join(X0,X2),
inference(superposition,[],[f8,f4]) ).
fof(f84,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X1,join(X0,X2)),
inference(superposition,[],[f8,f6]) ).
fof(f86,plain,
! [X0] : join(a,join(b,X0)) = join(sF4,X0),
inference(superposition,[],[f8,f20]) ).
fof(f88,plain,
! [X0] : join(b,join(sF0,X0)) = join(sF1,X0),
inference(superposition,[],[f8,f14]) ).
fof(f89,plain,
! [X0] : join(b,join(sF7,X0)) = join(sF8,X0),
inference(superposition,[],[f8,f28]) ).
fof(f90,plain,
! [X0] : join(sF3,join(sF5,X0)) = join(sF6,X0),
inference(superposition,[],[f8,f24]) ).
fof(f97,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f6,f8]) ).
fof(f122,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X0,join(X1,meet(X0,join(X1,X2)))))) = meet(X1,join(X2,meet(X0,meet(X0,join(X1,X2))))),
inference(superposition,[],[f9,f2]) ).
fof(f128,plain,
! [X2,X3,X0,X1,X4] : meet(X3,join(X4,meet(meet(X0,X1),join(X3,X2)))) = meet(X3,join(X4,meet(X0,meet(X1,join(X2,meet(meet(X0,X1),join(X3,X4))))))),
inference(superposition,[],[f9,f7]) ).
fof(f141,plain,
! [X2,X3,X0,X1,X4] : meet(X3,join(X4,meet(meet(X0,X1),join(X3,X2)))) = meet(X3,join(X4,meet(X0,meet(X1,join(X2,meet(X0,meet(X1,join(X3,X4)))))))),
inference(forward_demodulation,[],[f128,f7]) ).
fof(f143,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X0,join(X1,meet(X0,join(X1,X2)))))) = meet(X1,join(X2,meet(X0,join(X1,X2)))),
inference(forward_demodulation,[],[f122,f54]) ).
fof(f150,plain,
! [X2,X3,X0,X1,X4] : meet(X3,join(X4,meet(X0,meet(X1,join(X2,meet(X0,meet(X1,join(X3,X4)))))))) = meet(X3,join(X4,meet(X0,meet(X1,join(X3,X2))))),
inference(forward_demodulation,[],[f141,f7]) ).
fof(f152,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X0,join(X1,X2)))) = meet(X1,join(X2,meet(X0,join(X1,X1)))),
inference(forward_demodulation,[],[f143,f9]) ).
fof(f155,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X0,join(X1,X2)))) = meet(X1,join(X2,meet(X0,X1))),
inference(forward_demodulation,[],[f152,f2]) ).
fof(f180,plain,
sF6 = join(sF6,sF7),
inference(superposition,[],[f49,f26]) ).
fof(f200,plain,
! [X0,X1] : meet(X1,X0) = meet(meet(X1,X0),X0),
inference(superposition,[],[f52,f49]) ).
fof(f213,plain,
sF5 = meet(sF5,sF6),
inference(superposition,[],[f52,f24]) ).
fof(f228,plain,
! [X0,X1] : meet(X1,X0) = meet(X0,meet(X1,X0)),
inference(forward_demodulation,[],[f200,f5]) ).
fof(f270,plain,
meet(a,b) = meet(sF3,sF1),
inference(superposition,[],[f59,f34]) ).
fof(f271,plain,
meet(a,b) = meet(sF3,sF8),
inference(superposition,[],[f59,f35]) ).
fof(f289,plain,
sF3 = meet(sF3,sF8),
inference(forward_demodulation,[],[f271,f18]) ).
fof(f290,plain,
meet(a,b) = meet(sF1,sF3),
inference(forward_demodulation,[],[f270,f5]) ).
fof(f294,plain,
sF3 = meet(sF1,sF3),
inference(forward_demodulation,[],[f290,f18]) ).
fof(f300,plain,
meet(sF0,sF4) = meet(a,sF5),
inference(superposition,[],[f60,f22]) ).
fof(f303,plain,
! [X0] : meet(sF0,X0) = meet(a,meet(X0,c)),
inference(superposition,[],[f60,f5]) ).
fof(f323,plain,
! [X0] : join(sF6,X0) = join(sF6,join(sF7,X0)),
inference(superposition,[],[f8,f180]) ).
fof(f353,plain,
! [X0] : meet(sF7,X0) = meet(a,meet(X0,sF6)),
inference(superposition,[],[f63,f5]) ).
fof(f404,plain,
! [X0] : meet(c,sF4) = meet(sF5,join(sF4,X0)),
inference(superposition,[],[f67,f3]) ).
fof(f406,plain,
! [X0] : meet(c,sF4) = meet(sF5,join(X0,sF4)),
inference(superposition,[],[f67,f52]) ).
fof(f413,plain,
! [X0] : sF5 = meet(sF5,join(X0,sF4)),
inference(forward_demodulation,[],[f406,f22]) ).
fof(f415,plain,
! [X0] : sF5 = meet(sF5,join(sF4,X0)),
inference(forward_demodulation,[],[f404,f22]) ).
fof(f468,plain,
join(sF4,sF0) = join(a,sF1),
inference(superposition,[],[f86,f14]) ).
fof(f471,plain,
join(sF4,sF7) = join(a,sF8),
inference(superposition,[],[f86,f28]) ).
fof(f492,plain,
join(a,sF1) = join(sF0,sF4),
inference(forward_demodulation,[],[f468,f6]) ).
fof(f507,plain,
! [X0] : join(b,sF0) = join(sF1,meet(sF0,X0)),
inference(superposition,[],[f88,f4]) ).
fof(f521,plain,
! [X0] : sF1 = join(sF1,meet(sF0,X0)),
inference(forward_demodulation,[],[f507,f14]) ).
fof(f536,plain,
! [X0] : join(sF8,X0) = join(b,join(X0,sF7)),
inference(superposition,[],[f89,f6]) ).
fof(f538,plain,
! [X0] : join(b,sF7) = join(sF8,meet(X0,sF7)),
inference(superposition,[],[f89,f49]) ).
fof(f549,plain,
! [X0] : sF8 = join(sF8,meet(X0,sF7)),
inference(forward_demodulation,[],[f538,f28]) ).
fof(f563,plain,
! [X0] : join(sF6,X0) = join(sF3,join(X0,sF5)),
inference(superposition,[],[f90,f6]) ).
fof(f564,plain,
! [X0] : join(sF3,sF5) = join(sF6,meet(sF5,X0)),
inference(superposition,[],[f90,f4]) ).
fof(f576,plain,
! [X0] : sF6 = join(sF6,meet(sF5,X0)),
inference(forward_demodulation,[],[f564,f24]) ).
fof(f667,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(join(X1,X0),meet(X0,X2)),
inference(superposition,[],[f57,f52]) ).
fof(f748,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(X2,join(X1,X0))),
inference(forward_demodulation,[],[f667,f76]) ).
fof(f1443,plain,
! [X0,X1] : join(join(sF1,X0),X1) = join(join(sF0,X0),join(b,X1)),
inference(superposition,[],[f84,f88]) ).
fof(f1508,plain,
! [X0,X1] : join(join(sF1,X0),X1) = join(sF0,join(X0,join(b,X1))),
inference(forward_demodulation,[],[f1443,f8]) ).
fof(f1529,plain,
! [X0,X1] : join(sF1,join(X0,X1)) = join(sF0,join(X0,join(b,X1))),
inference(forward_demodulation,[],[f1508,f8]) ).
fof(f1880,plain,
! [X0,X1] : join(sF6,join(X1,X0)) = join(sF3,join(X0,join(sF5,X1))),
inference(superposition,[],[f90,f97]) ).
fof(f2008,plain,
sF8 = join(sF8,sF3),
inference(superposition,[],[f49,f289]) ).
fof(f2018,plain,
sF8 = join(sF3,sF8),
inference(forward_demodulation,[],[f2008,f6]) ).
fof(f2212,plain,
! [X0] : join(sF1,X0) = join(sF1,join(sF3,X0)),
inference(superposition,[],[f82,f294]) ).
fof(f5066,plain,
! [X0] : join(X0,sF8) = join(sF3,join(sF8,X0)),
inference(superposition,[],[f97,f2018]) ).
fof(f6244,plain,
! [X2,X3,X0,X1] : meet(X1,join(X2,meet(X0,meet(X3,join(X1,X0))))) = meet(X1,join(X2,meet(X0,meet(X3,X0)))),
inference(superposition,[],[f150,f4]) ).
fof(f6358,plain,
! [X2,X3,X0,X1] : meet(X1,join(X2,meet(X0,meet(X3,join(X1,X0))))) = meet(X1,join(X2,meet(X3,X0))),
inference(forward_demodulation,[],[f6244,f228]) ).
fof(f6425,plain,
! [X2,X3,X0,X1] : meet(X1,join(X2,meet(X3,X0))) = meet(X1,join(X2,meet(X0,X3))),
inference(forward_demodulation,[],[f6358,f748]) ).
fof(f10135,plain,
sF5 = meet(sF5,join(a,sF8)),
inference(superposition,[],[f415,f471]) ).
fof(f10500,plain,
sF5 = meet(sF5,join(a,sF1)),
inference(superposition,[],[f413,f492]) ).
fof(f10726,plain,
sF1 = join(sF1,meet(a,sF5)),
inference(superposition,[],[f521,f300]) ).
fof(f15166,plain,
meet(a,c) = meet(sF0,sF4),
inference(superposition,[],[f62,f303]) ).
fof(f15208,plain,
sF0 = meet(sF0,sF4),
inference(forward_demodulation,[],[f15166,f12]) ).
fof(f15259,plain,
sF0 = meet(a,sF5),
inference(superposition,[],[f300,f15208]) ).
fof(f15976,plain,
meet(a,sF5) = meet(sF7,sF5),
inference(superposition,[],[f353,f213]) ).
fof(f16054,plain,
meet(a,sF5) = meet(sF5,sF7),
inference(forward_demodulation,[],[f15976,f5]) ).
fof(f16084,plain,
sF0 = meet(sF5,sF7),
inference(forward_demodulation,[],[f16054,f15259]) ).
fof(f16348,plain,
sF6 = join(sF6,sF0),
inference(superposition,[],[f576,f16084]) ).
fof(f16351,plain,
sF8 = join(sF8,sF0),
inference(superposition,[],[f549,f16084]) ).
fof(f16352,plain,
sF5 = join(sF5,sF0),
inference(superposition,[],[f4,f16084]) ).
fof(f16378,plain,
sF5 = join(sF0,sF5),
inference(forward_demodulation,[],[f16352,f6]) ).
fof(f16379,plain,
sF8 = join(sF0,sF8),
inference(forward_demodulation,[],[f16351,f6]) ).
fof(f16381,plain,
sF6 = join(sF0,sF6),
inference(forward_demodulation,[],[f16348,f6]) ).
fof(f18921,plain,
join(b,sF5) = join(sF1,sF5),
inference(superposition,[],[f88,f16378]) ).
fof(f19610,plain,
! [X0] : join(X0,sF6) = join(sF0,join(sF6,X0)),
inference(superposition,[],[f97,f16381]) ).
fof(f26133,plain,
meet(a,join(sF8,meet(sF5,a))) = meet(a,join(sF8,sF5)),
inference(superposition,[],[f155,f10135]) ).
fof(f26165,plain,
meet(a,join(sF8,meet(sF5,a))) = meet(a,join(sF5,sF8)),
inference(forward_demodulation,[],[f26133,f6]) ).
fof(f26184,plain,
meet(a,join(sF5,sF8)) = meet(a,join(sF8,meet(a,sF5))),
inference(forward_demodulation,[],[f26165,f6425]) ).
fof(f26194,plain,
meet(a,join(sF5,sF8)) = meet(a,join(sF8,sF0)),
inference(forward_demodulation,[],[f26184,f15259]) ).
fof(f26198,plain,
meet(a,join(sF5,sF8)) = meet(a,join(sF0,sF8)),
inference(forward_demodulation,[],[f26194,f6]) ).
fof(f26199,plain,
meet(a,sF8) = meet(a,join(sF5,sF8)),
inference(forward_demodulation,[],[f26198,f16379]) ).
fof(f26200,plain,
sF9 = meet(a,join(sF5,sF8)),
inference(forward_demodulation,[],[f26199,f30]) ).
fof(f27008,plain,
meet(a,join(sF1,meet(sF5,a))) = meet(a,join(sF1,sF5)),
inference(superposition,[],[f155,f10500]) ).
fof(f27040,plain,
meet(a,join(b,sF5)) = meet(a,join(sF1,meet(sF5,a))),
inference(forward_demodulation,[],[f27008,f18921]) ).
fof(f27059,plain,
meet(a,join(b,sF5)) = meet(a,join(sF1,meet(a,sF5))),
inference(forward_demodulation,[],[f27040,f6425]) ).
fof(f27069,plain,
meet(a,sF1) = meet(a,join(b,sF5)),
inference(forward_demodulation,[],[f27059,f10726]) ).
fof(f27073,plain,
sF2 = meet(a,join(b,sF5)),
inference(forward_demodulation,[],[f27069,f16]) ).
fof(f99115,plain,
join(sF0,join(sF6,b)) = join(sF1,join(sF3,sF5)),
inference(superposition,[],[f1529,f563]) ).
fof(f99274,plain,
join(sF1,sF5) = join(sF0,join(sF6,b)),
inference(forward_demodulation,[],[f99115,f2212]) ).
fof(f99418,plain,
join(b,sF6) = join(sF1,sF5),
inference(forward_demodulation,[],[f99274,f19610]) ).
fof(f99507,plain,
join(b,sF6) = join(b,sF5),
inference(forward_demodulation,[],[f99418,f18921]) ).
fof(f109768,plain,
join(sF6,join(sF7,b)) = join(sF3,join(sF8,sF5)),
inference(superposition,[],[f1880,f536]) ).
fof(f109980,plain,
join(sF5,sF8) = join(sF6,join(sF7,b)),
inference(forward_demodulation,[],[f109768,f5066]) ).
fof(f110123,plain,
join(sF6,b) = join(sF5,sF8),
inference(forward_demodulation,[],[f109980,f323]) ).
fof(f110236,plain,
join(b,sF6) = join(sF5,sF8),
inference(forward_demodulation,[],[f110123,f6]) ).
fof(f110309,plain,
join(b,sF5) = join(sF5,sF8),
inference(forward_demodulation,[],[f110236,f99507]) ).
fof(f110398,plain,
sF9 = meet(a,join(b,sF5)),
inference(superposition,[],[f26200,f110309]) ).
fof(f110494,plain,
sF2 = sF9,
inference(forward_demodulation,[],[f110398,f27073]) ).
fof(f110514,plain,
$false,
inference(forward_subsumption_resolution,[],[f110494,f31]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT153-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.09 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.21/0.49 % Computer : n004.cluster.edu
% 0.21/0.49 % Model : x86_64 x86_64
% 0.21/0.49 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.21/0.49 % Memory : 8046.5625MB
% 0.21/0.49 % OS : Linux 6.8.0-71-generic
% 0.21/0.49 % CPULimit : 300
% 0.21/0.49 % WCLimit : 300
% 0.21/0.49 % DateTime : Sun Sep 27 14:03:08 UTC 2026
% 0.21/0.50 % CPUTime :
% 0.21/0.50 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.25/0.55 Running first-order model finding
% 0.25/0.55 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
% 27.96/4.53 % (3547640)Will run a generic schedule for satisfiability detection.
% 27.96/4.53 % (3547649)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2046978515:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 27.96/4.53 % (3547646)% WARNING: option uhcvi not known.
% 27.96/4.53 % (3547645)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3425046234_2999 on theBenchmark for (2999ds/0Mi)
% 27.96/4.53 % (3547646)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1041250119:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 27.96/4.53 % (3547648)dis+10_1_sil=32000:sp=arity:random_seed=843907408:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 27.96/4.53 % (3547647)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1763071865:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 27.96/4.53 % (3547650)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1805883864:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 27.96/4.53 % (3547651)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=971209297:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 27.96/4.53 % TRYING [1]
% 27.96/4.53 % TRYING [2]
% 27.96/4.53 % TRYING [3]
% 27.96/4.53 % TRYING [4]
% 27.96/4.53 % (3547649)Instruction limit reached!
% 27.96/4.53 % (3547649)------------------------------
% 27.96/4.53 % (3547649)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.96/4.53 % (3547649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.96/4.53 % (3547649)CaDiCaL version: 2.1.3
% 27.96/4.53 % (3547649)Termination reason: Instruction limit
% 27.96/4.53 % (3547649)Termination phase: Saturation
% 27.96/4.53 % (3547649)Time elapsed: 0.058 s
% 27.96/4.53 % (3547649)Peak memory usage: 12 MB
% 27.96/4.53 % (3547649)Instructions burned: 117 (million)
% 27.96/4.53 % TRYING [5]
% 27.96/4.53 % (3547659)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1809904771:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 27.96/4.53 % TRYING [1]
% 27.96/4.53 % TRYING [2]
% 27.96/4.53 % (3547648)Instruction limit reached!
% 27.96/4.53 % (3547648)------------------------------
% 27.96/4.53 % (3547648)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.96/4.53 % (3547648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.96/4.53 % (3547648)CaDiCaL version: 2.1.3
% 27.96/4.53 % (3547648)Termination reason: Instruction limit
% 27.96/4.53 % (3547648)Termination phase: Saturation
% 27.96/4.53 % (3547648)Time elapsed: 0.098 s
% 27.96/4.53 % (3547648)Peak memory usage: 12 MB
% 27.96/4.53 % (3547648)Instructions burned: 103 (million)
% 27.96/4.53 % TRYING [3]
% 27.96/4.53 % TRYING [4]
% 27.96/4.53 % (3547650)Instruction limit reached!
% 27.96/4.53 % (3547650)------------------------------
% 27.96/4.53 % (3547650)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.96/4.53 % (3547650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.96/4.53 % (3547650)CaDiCaL version: 2.1.3
% 27.96/4.53 % (3547650)Termination reason: Instruction limit
% 27.96/4.53 % (3547650)Termination phase: Saturation
% 27.96/4.53 % (3547650)Time elapsed: 0.128 s
% 27.96/4.53 % (3547650)Peak memory usage: 12 MB
% 27.96/4.53 % (3547650)Instructions burned: 131 (million)
% 27.96/4.53 % (3547661)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2666952366:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 27.96/4.53 % (3547651)Instruction limit reached!
% 27.96/4.53 % (3547651)------------------------------
% 27.96/4.53 % (3547651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.96/4.53 % (3547651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.96/4.53 % (3547651)CaDiCaL version: 2.1.3
% 27.96/4.53 % (3547651)Termination reason: Instruction limit
% 27.96/4.53 % (3547651)Termination phase: Saturation
% 27.96/4.53 % (3547651)Time elapsed: 0.157 s
% 27.96/4.53 % (3547651)Peak memory usage: 12 MB
% 27.96/4.53 % (3547651)Instructions burned: 159 (million)
% 27.96/4.53 % (3547662)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=4621846:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 27.96/4.53 % TRYING [5]
% 27.96/4.53 % (3547664)ott-21_1_sil=16000:fs=off:random_seed=1151037443:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 27.96/4.53 % (3547661)Instruction limit reached!
% 27.96/4.53 % (3547661)------------------------------
% 27.96/4.53 % (3547661)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 73.47/11.05 % (3547661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.47/11.05 % (3547661)CaDiCaL version: 2.1.3
% 73.47/11.05 % (3547661)Termination reason: Instruction limit
% 73.47/11.05 % (3547661)Termination phase: Saturation
% 73.47/11.05 % (3547661)Time elapsed: 0.135 s
% 73.47/11.05 % (3547661)Peak memory usage: 12 MB
% 73.47/11.05 % (3547661)Instructions burned: 131 (million)
% 73.47/11.05 % (3547667)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2762578776:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 73.47/11.05 % TRYING [6]
% 73.47/11.05 % (3547664)Instruction limit reached!
% 73.47/11.05 % (3547664)------------------------------
% 73.47/11.05 % (3547664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 73.47/11.05 % (3547664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.47/11.05 % (3547664)CaDiCaL version: 2.1.3
% 73.47/11.05 % (3547664)Termination reason: Instruction limit
% 73.47/11.05 % (3547664)Termination phase: Saturation
% 73.47/11.05 % (3547664)Time elapsed: 0.141 s
% 73.47/11.05 % (3547664)Peak memory usage: 11 MB
% 73.47/11.05 % (3547664)Instructions burned: 181 (million)
% 73.47/11.05 % (3547669)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4171406661:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 73.47/11.05 % TRYING [1]
% 73.47/11.05 % TRYING [2]
% 73.47/11.05 % TRYING [3]
% 73.47/11.05 % TRYING [6]
% 73.47/11.05 % TRYING [4]
% 73.47/11.05 % (3547659)Instruction limit reached!
% 73.47/11.05 % (3547659)------------------------------
% 73.47/11.05 % (3547659)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 73.47/11.05 % (3547659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.47/11.05 % (3547659)CaDiCaL version: 2.1.3
% 73.47/11.05 % (3547659)Termination reason: Instruction limit
% 73.47/11.05 % (3547659)Termination phase: Finite model building constraint generation
% 73.47/11.05 % (3547659)Time elapsed: 0.443 s
% 73.47/11.05 % (3547659)Peak memory usage: 31 MB
% 73.47/11.05 % (3547659)Instructions burned: 714 (million)
% 73.47/11.05 % (3547671)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=56935872:i=1179_2994 on theBenchmark for (2994ds/1179Mi)
% 73.47/11.05 % TRYING [5]
% 73.47/11.05 % (3547667)Instruction limit reached!
% 73.47/11.05 % (3547667)------------------------------
% 73.47/11.05 % (3547667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 73.47/11.05 % (3547667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.47/11.05 % (3547667)CaDiCaL version: 2.1.3
% 73.47/11.05 % (3547667)Termination reason: Instruction limit
% 73.47/11.05 % (3547667)Termination phase: Saturation
% 73.47/11.05 % (3547667)Time elapsed: 0.428 s
% 73.47/11.05 % (3547667)Peak memory usage: 15 MB
% 73.47/11.05 % (3547667)Instructions burned: 477 (million)
% 73.47/11.05 % (3547662)Instruction limit reached!
% 73.47/11.05 % (3547662)------------------------------
% 73.47/11.05 % (3547662)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 73.47/11.05 % (3547662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.47/11.05 % (3547662)CaDiCaL version: 2.1.3
% 73.47/11.05 % (3547662)Termination reason: Instruction limit
% 73.47/11.05 % (3547662)Termination phase: Saturation
% 73.47/11.05 % (3547662)Time elapsed: 0.612 s
% 73.47/11.05 % (3547662)Peak memory usage: 16 MB
% 73.47/11.05 % (3547662)Instructions burned: 684 (million)
% 73.47/11.05 % (3547673)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3599928409:i=889:ins=1_2992 on theBenchmark for (2992ds/889Mi)
% 73.47/11.05 % (3547674)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=1041202869: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)
% 73.47/11.05 % TRYING [7]
% 73.47/11.05 % (3547669)Instruction limit reached!
% 73.47/11.05 % (3547669)------------------------------
% 73.47/11.05 % (3547669)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 73.47/11.05 % (3547669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.47/11.05 % (3547669)CaDiCaL version: 2.1.3
% 73.47/11.05 % (3547669)Termination reason: Instruction limit
% 73.47/11.05 % (3547669)Termination phase: Finite model building SAT solving
% 73.47/11.05 % (3547669)Time elapsed: 0.600 s
% 73.47/11.05 % (3547669)Peak memory usage: 23 MB
% 73.47/11.05 % (3547669)Instructions burned: 865 (million)
% 73.47/11.05 % (3547677)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2508068804:i=879:kws=inv_precedence:fsr=off_2989 on theBenchmark for (2989ds/879Mi)
% 73.47/11.05 % (3547671)Instruction limit reached!
% 73.47/11.05 % (3547671)------------------------------
% 73.47/11.05 % (3547671)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 73.47/11.05 % (3547671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.47/11.05 % (3547671)CaDiCaL version: 2.1.3
% 73.47/11.05 % (3547671)Termination reason: Instruction limit
% 73.47/11.05 % (3547671)Termination phase: Saturation
% 73.47/11.05 % (3547671)Time elapsed: 0.626 s
% 73.47/11.05 % (3547671)Peak memory usage: 25 MB
% 73.47/11.05 % (3547671)Instructions burned: 1180 (million)
% 73.47/11.05 % (3547679)fmb+10_1_sil=64000:random_seed=2378358863:i=22061:nm=2:gsp=on_2987 on theBenchmark for (2987ds/22061Mi)
% 73.47/11.05 % TRYING [1]
% 73.47/11.05 % TRYING [2]
% 73.47/11.05 % TRYING [3]
% 73.47/11.05 % TRYING [4]
% 73.47/11.05 % TRYING [5]
% 73.47/11.05 % (3547674)Instruction limit reached!
% 73.47/11.05 % (3547674)------------------------------
% 73.47/11.05 % (3547674)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 73.47/11.05 % (3547674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.47/11.05 % (3547674)CaDiCaL version: 2.1.3
% 73.47/11.05 % (3547674)Termination reason: Instruction limit
% 73.47/11.05 % (3547674)Termination phase: Saturation
% 73.47/11.05 % (3547674)Time elapsed: 0.670 s
% 73.47/11.05 % (3547674)Peak memory usage: 16 MB
% 73.47/11.05 % (3547674)Instructions burned: 692 (million)
% 73.47/11.05 % (3547681)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1308439406:i=9515:nm=5_2984 on theBenchmark for (2984ds/9515Mi)
% 73.47/11.05 % TRYING [20]
% 73.47/11.05 % (3547673)Instruction limit reached!
% 73.47/11.05 % (3547673)------------------------------
% 73.47/11.05 % (3547673)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 73.47/11.05 % (3547673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.47/11.05 % (3547673)CaDiCaL version: 2.1.3
% 73.47/11.05 % (3547673)Termination reason: Instruction limit
% 73.47/11.05 % (3547673)Termination phase: Finite model building constraint generation
% 73.47/11.05 % (3547673)Time elapsed: 0.814 s
% 73.47/11.05 % (3547673)Peak memory usage: 107 MB
% 73.47/11.05 % (3547673)Instructions burned: 890 (million)
% 73.47/11.05 % (3547683)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=11297158:fmbsr=1.7:i=920_2983 on theBenchmark for (2983ds/920Mi)
% 73.47/11.05 % TRYING [8]
% 73.47/11.05 % TRYING [6]
% 73.47/11.05 % (3547677)Instruction limit reached!
% 73.47/11.05 % (3547677)------------------------------
% 73.47/11.05 % (3547677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 73.47/11.05 % (3547677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.47/11.05 % (3547677)CaDiCaL version: 2.1.3
% 73.47/11.05 % (3547677)Termination reason: Instruction limit
% 73.47/11.05 % (3547677)Termination phase: Saturation
% 73.47/11.05 % (3547677)Time elapsed: 0.791 s
% 73.47/11.05 % (3547677)Peak memory usage: 18 MB
% 73.47/11.05 % (3547677)Instructions burned: 879 (million)
% 73.47/11.05 % (3547685)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2282668523:i=5131_2981 on theBenchmark for (2981ds/5131Mi)
% 73.47/11.05 % (3547683)Instruction limit reached!
% 73.47/11.05 % (3547683)------------------------------
% 73.47/11.05 % (3547683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 73.47/11.05 % (3547683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.47/11.05 % (3547683)CaDiCaL version: 2.1.3
% 73.47/11.05 % (3547683)Termination reason: Instruction limit
% 73.47/11.05 % (3547683)Termination phase: Finite model building constraint generation
% 73.47/11.05 % (3547683)Time elapsed: 0.706 s
% 73.47/11.05 % (3547683)Peak memory usage: 90 MB
% 73.47/11.05 % (3547683)Instructions burned: 921 (million)
% 73.47/11.05 % (3547687)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2858500051:i=1472:ins=7:fdi=8:gsp=on_2975 on theBenchmark for (2975ds/1472Mi)
% 73.47/11.05 % TRYING [7]
% 73.47/11.05 % TRYING [8]
% 73.47/11.05 % (3547687)Instruction limit reached!
% 73.47/11.05 % (3547687)------------------------------
% 73.47/11.05 % (3547687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 73.47/11.05 % (3547687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.47/11.05 % (3547687)CaDiCaL version: 2.1.3
% 73.47/11.05 % (3547687)Termination reason: Instruction limit
% 73.47/11.05 % (3547687)Termination phase: Saturation
% 73.47/11.05 % (3547687)Time elapsed: 1.423 s
% 73.47/11.05 % (3547687)Peak memory usage: 28 MB
% 73.47/11.05 % (3547687)Instructions burned: 1472 (million)
% 73.47/11.05 % (3547689)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3059165800:i=6324_2960 on theBenchmark for (2960ds/6324Mi)
% 73.47/11.05 % (3547689)Cannot represent all propositional literals internally
% 73.47/11.05 % (3547689)Refutation not found, incomplete strategy
% 73.47/11.05 % (3547689)------------------------------
% 73.47/11.05 % (3547689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 73.47/11.05 % (3547689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.47/11.05 % (3547689)CaDiCaL version: 2.1.3
% 73.47/11.05 % (3547689)Termination reason: Refutation not found, incomplete strategy
% 73.47/11.05 % (3547689)Time elapsed: 0.004 s
% 73.47/11.05 % (3547689)Peak memory usage: 10 MB
% 73.47/11.05 % (3547689)Instructions burned: 2 (million)
% 73.47/11.05 % (3547689)------------------------------
% 73.47/11.05 % (3547689)------------------------------
% 73.47/11.05 % (3547691)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2196724365:fmbsr=2.30978:i=2174_2960 on theBenchmark for (2960ds/2174Mi)
% 73.47/11.05 % TRYING [16]
% 73.47/11.05 % TRYING [8]
% 73.47/11.05 % (3547691)Instruction limit reached!
% 73.47/11.05 % (3547691)------------------------------
% 73.47/11.05 % (3547691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 73.47/11.05 % (3547691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.47/11.05 % (3547691)CaDiCaL version: 2.1.3
% 73.47/11.05 % (3547691)Termination reason: Instruction limit
% 73.47/11.05 % (3547691)Termination phase: Finite model building constraint generation
% 73.47/11.05 % (3547691)Time elapsed: 1.484 s
% 73.47/11.05 % (3547691)Peak memory usage: 134 MB
% 73.47/11.05 % (3547691)Instructions burned: 2175 (million)
% 73.47/11.05 % (3547693)ott-2_1_sil=16000:newcnf=on:random_seed=2861188986:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2944 on theBenchmark for (2944ds/869Mi)
% 73.47/11.05 % (3547693)Instruction limit reached!
% 73.47/11.05 % (3547693)------------------------------
% 73.47/11.05 % (3547693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 73.47/11.05 % (3547693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.47/11.05 % (3547693)CaDiCaL version: 2.1.3
% 73.47/11.05 % (3547693)Termination reason: Instruction limit
% 73.47/11.05 % (3547693)Termination phase: Saturation
% 73.47/11.05 % (3547693)Time elapsed: 0.848 s
% 73.47/11.05 % (3547693)Peak memory usage: 20 MB
% 73.47/11.05 % (3547693)Instructions burned: 869 (million)
% 73.47/11.05 % (3547695)ott+10_1_sil=32000:tgt=ground:random_seed=274465423:i=5114:av=off_2935 on theBenchmark for (2935ds/5114Mi)
% 73.47/11.05 % TRYING [9]
% 73.47/11.05 % (3547685)Instruction limit reached!
% 73.47/11.05 % (3547685)------------------------------
% 73.47/11.05 % (3547685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 73.47/11.05 % (3547685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.47/11.05 % (3547685)CaDiCaL version: 2.1.3
% 73.47/11.05 % (3547685)Termination reason: Instruction limit
% 73.47/11.05 % (3547685)Termination phase: Saturation
% 73.47/11.05 % (3547685)Time elapsed: 4.698 s
% 73.47/11.05 % (3547685)Peak memory usage: 49 MB
% 73.47/11.05 % (3547685)Instructions burned: 5131 (million)
% 73.47/11.05 % (3547697)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3304726977:i=54282_2933 on theBenchmark for (2933ds/54282Mi)
% 73.47/11.05 % TRYING [1]
% 73.47/11.05 % TRYING [2]
% 73.47/11.05 % TRYING [3]
% 73.47/11.05 % TRYING [4]
% 73.47/11.05 % TRYING [5]
% 73.47/11.05 % TRYING [6]
% 73.47/11.05 % TRYING [7]
% 73.47/11.05 % (3547681)Instruction limit reached!
% 73.47/11.05 % (3547681)------------------------------
% 73.47/11.05 % (3547681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 73.47/11.06 % (3547681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.47/11.06 % (3547681)CaDiCaL version: 2.1.3
% 73.47/11.06 % (3547681)Termination reason: Instruction limit
% 73.47/11.06 % (3547681)Termination phase: Finite model building constraint generation
% 73.47/11.06 % (3547681)Time elapsed: 6.818 s
% 73.47/11.06 % (3547681)Peak memory usage: 668 MB
% 73.47/11.06 % (3547681)Instructions burned: 9515 (million)
% 73.47/11.06 % (3547699)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2976578226:i=3512:aac=none_2914 on theBenchmark for (2914ds/3512Mi)
% 73.47/11.06 % TRYING [8]
% 73.47/11.06 % TRYING [9]
% 73.47/11.06 % (3547695) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3547640-3547695"...
% 73.47/11.06 % (3547695)...printing done.
% 73.47/11.06 % (3547695)Refutation found. Thanks to Tanya!
% 73.47/11.06 % SZS status Unsatisfiable for theBenchmark
% 73.47/11.06 % SZS output start Proof for theBenchmark
% See solution above
% 73.47/11.06 % (3547695)------------------------------
% 73.47/11.06 % (3547695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 73.47/11.06 % (3547695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.47/11.06 % (3547695)CaDiCaL version: 2.1.3
% 73.47/11.06 % (3547695)Termination reason: Refutation
% 73.47/11.06 % (3547695)Time elapsed: 3.899 s
% 73.47/11.06 % (3547695)Peak memory usage: 50 MB
% 73.47/11.06 % (3547695)Instructions burned: 3910 (million)
% 73.47/11.06 % (3547640)Success in time 10.487 s
% 73.47/11.06 % Vampire exiting
%------------------------------------------------------------------------------