%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : REL033+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n005.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 12:33:58 PM UTC 2026
% Result : Theorem 59.08s 9.97s
% Output : Refutation 64.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 59
% Number of leaves : 23
% Syntax : Number of formulae : 240 ( 236 unt; 10 def)
% Number of atoms : 244 ( 243 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 10 ( 6 ~; 0 |; 2 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 16 con; 0-2 aty)
% Number of variables : 262 ( 259 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maddux1_join_commutativity) ).
fof(f2,axiom,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maddux2_join_associativity) ).
fof(f3,axiom,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maddux3_a_kind_of_de_Morgan) ).
fof(f4,axiom,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maddux4_definiton_of_meet) ).
fof(f6,axiom,
! [X0] : composition(X0,one) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',composition_identity) ).
fof(f7,axiom,
! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',composition_distributivity) ).
fof(f8,axiom,
! [X0] : converse(converse(X0)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_idempotence) ).
fof(f9,axiom,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_additivity) ).
fof(f10,axiom,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_multiplicativity) ).
fof(f11,axiom,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_cancellativity) ).
fof(f12,axiom,
! [X0] : top = join(X0,complement(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',def_top) ).
fof(f13,axiom,
! [X0] : zero = meet(X0,complement(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',def_zero) ).
fof(f14,conjecture,
! [X0,X1,X2] :
( composition(X0,top) = X0
=> composition(meet(X0,X1),X2) = meet(X0,composition(X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f15,negated_conjecture,
~ ! [X0,X1,X2] :
( composition(X0,top) = X0
=> composition(meet(X0,X1),X2) = meet(X0,composition(X1,X2)) ),
inference(negated_conjecture,[status(cth)],[f14]) ).
fof(f16,plain,
? [X0,X1,X2] :
( composition(meet(X0,X1),X2) != meet(X0,composition(X1,X2))
& composition(X0,top) = X0 ),
inference(ennf_transformation,[],[f15]) ).
fof(f17,plain,
( composition(meet(sK0,sK1),sK2) != meet(sK0,composition(sK1,sK2))
& sK0 = composition(sK0,top) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2)],[f16]) ).
fof(f18,plain,
! [X0,X1] : join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f19,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
inference(cnf_transformation,[],[f2]) ).
fof(f20,plain,
! [X0,X1] : join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) = X0,
inference(cnf_transformation,[],[f3]) ).
fof(f21,plain,
! [X0,X1] : complement(join(complement(X0),complement(X1))) = meet(X0,X1),
inference(cnf_transformation,[],[f4]) ).
fof(f23,plain,
! [X0] : composition(X0,one) = X0,
inference(cnf_transformation,[],[f6]) ).
fof(f24,plain,
! [X2,X0,X1] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
inference(cnf_transformation,[],[f7]) ).
fof(f25,plain,
! [X0] : converse(converse(X0)) = X0,
inference(cnf_transformation,[],[f8]) ).
fof(f26,plain,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
inference(cnf_transformation,[],[f9]) ).
fof(f27,plain,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
inference(cnf_transformation,[],[f10]) ).
fof(f28,plain,
! [X0,X1] : complement(X1) = join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)),
inference(cnf_transformation,[],[f11]) ).
fof(f29,plain,
! [X0] : top = join(X0,complement(X0)),
inference(cnf_transformation,[],[f12]) ).
fof(f30,plain,
! [X0] : zero = meet(X0,complement(X0)),
inference(cnf_transformation,[],[f13]) ).
fof(f31,plain,
sK0 = composition(sK0,top),
inference(cnf_transformation,[],[f17]) ).
fof(f32,plain,
composition(meet(sK0,sK1),sK2) != meet(sK0,composition(sK1,sK2)),
inference(cnf_transformation,[],[f17]) ).
fof(f33,plain,
! [X0] : zero = complement(join(complement(X0),complement(complement(X0)))),
inference(definition_unfolding,[],[f30,f21]) ).
fof(f34,plain,
composition(complement(join(complement(sK0),complement(sK1))),sK2) != complement(join(complement(sK0),complement(composition(sK1,sK2)))),
inference(definition_unfolding,[],[f32,f21,f21]) ).
fof(f35,definition,
sF3 = complement(sK0),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f36,plain,
complement(sK0) = sF3,
inference(reorient_equations,[],[f35]) ).
fof(f37,definition,
sF4 = complement(sK1),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f38,plain,
complement(sK1) = sF4,
inference(reorient_equations,[],[f37]) ).
fof(f39,definition,
sF5 = join(sF3,sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f40,plain,
join(sF3,sF4) = sF5,
inference(reorient_equations,[],[f39]) ).
fof(f41,definition,
sF6 = complement(sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f42,plain,
complement(sF5) = sF6,
inference(reorient_equations,[],[f41]) ).
fof(f43,definition,
sF7 = composition(sF6,sK2),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f44,plain,
composition(sF6,sK2) = sF7,
inference(reorient_equations,[],[f43]) ).
fof(f45,definition,
sF8 = composition(sK1,sK2),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f46,plain,
composition(sK1,sK2) = sF8,
inference(reorient_equations,[],[f45]) ).
fof(f47,definition,
sF9 = complement(sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f48,plain,
complement(sF8) = sF9,
inference(reorient_equations,[],[f47]) ).
fof(f49,definition,
sF10 = join(sF3,sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f50,plain,
join(sF3,sF9) = sF10,
inference(reorient_equations,[],[f49]) ).
fof(f51,definition,
sF11 = complement(sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f52,plain,
complement(sF10) = sF11,
inference(reorient_equations,[],[f51]) ).
fof(f53,plain,
sF7 != sF11,
inference(definition_folding,[],[f34,f52,f50,f48,f46,f36,f44,f42,f40,f38,f36]) ).
fof(f54,definition,
sF12 = composition(sK0,top),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f55,plain,
composition(sK0,top) = sF12,
inference(reorient_equations,[],[f54]) ).
fof(f56,plain,
sK0 = sF12,
inference(definition_folding,[],[f31,f55]) ).
fof(f57,plain,
zero = complement(top),
inference(backward_demodulation,[],[f33,f29]) ).
fof(f58,plain,
! [X0,X1] : complement(X1) = join(complement(X1),composition(converse(X0),complement(composition(X0,X1)))),
inference(backward_demodulation,[],[f28,f18]) ).
fof(f59,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))) = X0,
inference(backward_demodulation,[],[f20,f18]) ).
fof(f60,plain,
sK0 = composition(sK0,top),
inference(forward_demodulation,[],[f55,f56]) ).
fof(f62,plain,
! [X0,X1] : converse(join(X1,converse(X0))) = join(converse(X1),X0),
inference(superposition,[],[f26,f25]) ).
fof(f65,plain,
! [X0] : composition(join(sK1,X0),sK2) = join(sF8,composition(X0,sK2)),
inference(superposition,[],[f24,f46]) ).
fof(f73,plain,
! [X0,X1] : converse(composition(converse(X0),X1)) = composition(converse(X1),X0),
inference(superposition,[],[f27,f25]) ).
fof(f75,plain,
! [X2,X0,X1] : composition(join(converse(X1),X2),converse(X0)) = join(converse(composition(X0,X1)),composition(X2,converse(X0))),
inference(superposition,[],[f24,f27]) ).
fof(f110,plain,
! [X0,X1] : join(complement(X0),X1) = join(complement(join(complement(join(complement(X0),X1)),join(complement(X0),complement(X1)))),complement(X0)),
inference(superposition,[],[f59,f59]) ).
fof(f111,plain,
! [X0] : join(complement(join(complement(X0),complement(X0))),complement(top)) = X0,
inference(superposition,[],[f59,f29]) ).
fof(f113,plain,
! [X0,X1] : join(complement(join(complement(X1),X0)),complement(join(complement(X0),complement(X1)))) = X1,
inference(superposition,[],[f59,f18]) ).
fof(f114,plain,
! [X0] : join(complement(top),complement(join(complement(X0),complement(X0)))) = X0,
inference(forward_demodulation,[],[f111,f18]) ).
fof(f115,plain,
! [X0,X1] : join(complement(X0),X1) = join(complement(X0),complement(join(complement(join(complement(X0),X1)),join(complement(X0),complement(X1))))),
inference(forward_demodulation,[],[f110,f18]) ).
fof(f123,plain,
! [X0] : join(zero,complement(join(complement(X0),complement(X0)))) = X0,
inference(forward_demodulation,[],[f114,f57]) ).
fof(f145,plain,
! [X0] : converse(converse(X0)) = composition(converse(one),X0),
inference(superposition,[],[f73,f23]) ).
fof(f153,plain,
! [X0] : composition(converse(one),X0) = X0,
inference(forward_demodulation,[],[f145,f25]) ).
fof(f164,plain,
one = converse(one),
inference(superposition,[],[f23,f153]) ).
fof(f165,plain,
! [X0] : composition(one,X0) = X0,
inference(backward_demodulation,[],[f153,f164]) ).
fof(f190,plain,
! [X0] : complement(X0) = join(complement(X0),composition(one,complement(composition(one,X0)))),
inference(superposition,[],[f58,f164]) ).
fof(f194,plain,
complement(top) = join(complement(top),composition(converse(sK0),complement(sK0))),
inference(superposition,[],[f58,f60]) ).
fof(f199,plain,
complement(top) = join(complement(top),composition(converse(sK0),sF3)),
inference(forward_demodulation,[],[f194,f36]) ).
fof(f202,plain,
! [X0] : complement(X0) = join(complement(X0),complement(composition(one,X0))),
inference(forward_demodulation,[],[f190,f165]) ).
fof(f204,plain,
zero = join(zero,composition(converse(sK0),sF3)),
inference(forward_demodulation,[],[f199,f57]) ).
fof(f206,plain,
! [X0] : complement(X0) = join(complement(X0),complement(X0)),
inference(forward_demodulation,[],[f202,f165]) ).
fof(f208,plain,
! [X0] : join(zero,complement(complement(X0))) = X0,
inference(backward_demodulation,[],[f123,f206]) ).
fof(f219,plain,
! [X2,X0,X1] : join(X0,X2) = join(complement(join(complement(X0),X1)),join(complement(join(complement(X0),complement(X1))),X2)),
inference(superposition,[],[f19,f59]) ).
fof(f221,plain,
! [X2,X3,X0,X1] : join(composition(X0,X2),join(composition(X1,X2),X3)) = join(composition(join(X0,X1),X2),X3),
inference(superposition,[],[f19,f24]) ).
fof(f223,plain,
! [X0,X1] : join(X0,X1) = join(zero,join(complement(complement(X0)),X1)),
inference(superposition,[],[f19,f208]) ).
fof(f224,plain,
! [X0] : join(sF3,join(sF9,X0)) = join(sF10,X0),
inference(superposition,[],[f19,f50]) ).
fof(f231,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f18,f19]) ).
fof(f232,plain,
! [X0,X1] : join(complement(X0),X1) = join(complement(X0),complement(join(complement(X1),join(complement(join(complement(X0),X1)),complement(X0))))),
inference(backward_demodulation,[],[f115,f231]) ).
fof(f234,plain,
! [X0,X1] : join(complement(X0),X1) = join(complement(X0),complement(join(complement(X1),join(complement(X0),complement(join(complement(X0),X1)))))),
inference(forward_demodulation,[],[f232,f18]) ).
fof(f280,plain,
! [X2,X0,X1] : composition(join(converse(X2),converse(X1)),converse(X0)) = join(converse(composition(X0,X2)),converse(composition(X0,X1))),
inference(superposition,[],[f75,f27]) ).
fof(f286,plain,
! [X2,X0,X1] : composition(join(converse(X2),converse(X1)),converse(X0)) = converse(join(composition(X0,X2),composition(X0,X1))),
inference(forward_demodulation,[],[f280,f26]) ).
fof(f296,plain,
! [X2,X0,X1] : converse(join(composition(X0,X2),composition(X0,X1))) = composition(converse(join(X2,X1)),converse(X0)),
inference(forward_demodulation,[],[f286,f26]) ).
fof(f302,plain,
! [X2,X0,X1] : converse(join(composition(X0,X2),composition(X0,X1))) = converse(composition(X0,join(X2,X1))),
inference(forward_demodulation,[],[f296,f27]) ).
fof(f326,plain,
! [X2,X0,X1] : join(composition(X0,X1),composition(X0,X2)) = converse(converse(composition(X0,join(X1,X2)))),
inference(superposition,[],[f25,f302]) ).
fof(f339,plain,
! [X2,X0,X1] : composition(X0,join(X1,X2)) = join(composition(X0,X1),composition(X0,X2)),
inference(forward_demodulation,[],[f326,f25]) ).
fof(f366,plain,
! [X0,X1] : join(X0,composition(X0,X1)) = composition(X0,join(one,X1)),
inference(superposition,[],[f339,f23]) ).
fof(f370,plain,
! [X0] : composition(sK0,join(top,X0)) = join(sK0,composition(sK0,X0)),
inference(superposition,[],[f339,f60]) ).
fof(f384,plain,
! [X2,X3,X0,X1] : join(composition(X0,join(X1,X2)),X3) = join(composition(X0,X1),join(composition(X0,X2),X3)),
inference(superposition,[],[f19,f339]) ).
fof(f460,plain,
! [X0,X1] : join(X0,X1) = join(complement(join(complement(X0),complement(X0))),join(complement(top),X1)),
inference(superposition,[],[f219,f29]) ).
fof(f463,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),complement(complement(X1))))) = join(complement(join(complement(X0),X1)),X0),
inference(superposition,[],[f219,f59]) ).
fof(f464,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))) = join(X0,complement(join(complement(X0),complement(X1)))),
inference(superposition,[],[f219,f206]) ).
fof(f476,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),complement(X1)))) = X0,
inference(forward_demodulation,[],[f464,f59]) ).
fof(f477,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),complement(complement(X1))))) = join(X0,complement(join(complement(X0),X1))),
inference(forward_demodulation,[],[f463,f18]) ).
fof(f478,plain,
! [X0,X1] : join(X0,X1) = join(complement(top),join(X1,complement(join(complement(X0),complement(X0))))),
inference(forward_demodulation,[],[f460,f231]) ).
fof(f492,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),X1))) = X0,
inference(forward_demodulation,[],[f477,f476]) ).
fof(f493,plain,
! [X0,X1] : join(X0,X1) = join(complement(top),join(X1,complement(complement(X0)))),
inference(forward_demodulation,[],[f478,f206]) ).
fof(f503,plain,
! [X0,X1] : join(X0,X1) = join(zero,join(X1,complement(complement(X0)))),
inference(forward_demodulation,[],[f493,f57]) ).
fof(f531,plain,
! [X2,X0,X1] : join(complement(X0),X2) = join(join(complement(X0),X2),complement(join(X0,X1))),
inference(superposition,[],[f492,f219]) ).
fof(f532,plain,
! [X0] : join(X0,complement(top)) = X0,
inference(superposition,[],[f492,f29]) ).
fof(f533,plain,
! [X0] : join(X0,complement(complement(X0))) = X0,
inference(superposition,[],[f492,f492]) ).
fof(f535,plain,
! [X0,X1] : join(X1,complement(join(X0,complement(X1)))) = X1,
inference(superposition,[],[f492,f18]) ).
fof(f552,plain,
! [X0] : join(X0,zero) = X0,
inference(forward_demodulation,[],[f532,f57]) ).
fof(f553,plain,
! [X2,X0,X1] : join(complement(X0),X2) = join(complement(X0),join(X2,complement(join(X0,X1)))),
inference(forward_demodulation,[],[f531,f19]) ).
fof(f564,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(complement(complement(X0)),X1)),
inference(superposition,[],[f19,f533]) ).
fof(f566,plain,
! [X0,X1] : join(X0,X1) = join(complement(join(complement(X0),complement(complement(X0)))),join(complement(complement(X0)),X1)),
inference(superposition,[],[f219,f533]) ).
fof(f576,plain,
! [X0,X1] : join(X0,X1) = join(complement(complement(X0)),join(X1,complement(join(complement(X0),complement(complement(X0)))))),
inference(forward_demodulation,[],[f566,f231]) ).
fof(f578,plain,
! [X0,X1] : join(X0,X1) = join(complement(complement(X0)),X1),
inference(forward_demodulation,[],[f576,f553]) ).
fof(f580,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X0,X1)),
inference(backward_demodulation,[],[f564,f578]) ).
fof(f583,plain,
! [X0,X1] : join(X0,X1) = join(zero,join(X0,X1)),
inference(backward_demodulation,[],[f223,f578]) ).
fof(f593,plain,
! [X0,X1] : join(X0,X1) = join(X1,complement(complement(X0))),
inference(backward_demodulation,[],[f503,f583]) ).
fof(f596,plain,
! [X0] : join(X0,X0) = X0,
inference(backward_demodulation,[],[f533,f593]) ).
fof(f667,plain,
! [X0] : complement(complement(X0)) = join(X0,complement(complement(X0))),
inference(superposition,[],[f593,f596]) ).
fof(f688,plain,
! [X0] : complement(complement(X0)) = join(X0,X0),
inference(forward_demodulation,[],[f667,f593]) ).
fof(f691,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_demodulation,[],[f688,f596]) ).
fof(f694,plain,
top = complement(zero),
inference(superposition,[],[f691,f57]) ).
fof(f695,plain,
sK0 = complement(sF3),
inference(superposition,[],[f691,f36]) ).
fof(f696,plain,
sK1 = complement(sF4),
inference(superposition,[],[f691,f38]) ).
fof(f699,plain,
sF10 = complement(sF11),
inference(superposition,[],[f691,f52]) ).
fof(f706,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X0,X1))),
inference(superposition,[],[f492,f691]) ).
fof(f741,plain,
! [X0,X1] : complement(X1) = join(complement(X1),complement(join(X0,X1))),
inference(superposition,[],[f706,f18]) ).
fof(f751,plain,
complement(sF3) = join(complement(sF3),complement(sF5)),
inference(superposition,[],[f706,f40]) ).
fof(f755,plain,
complement(sF3) = join(complement(sF3),sF6),
inference(forward_demodulation,[],[f751,f42]) ).
fof(f758,plain,
complement(sF3) = join(sF6,complement(sF3)),
inference(forward_demodulation,[],[f755,f18]) ).
fof(f760,plain,
sK0 = join(sF6,sK0),
inference(forward_demodulation,[],[f758,f695]) ).
fof(f762,plain,
sK0 = join(sK0,sF6),
inference(forward_demodulation,[],[f760,f18]) ).
fof(f771,plain,
! [X0] : complement(complement(X0)) = join(complement(complement(X0)),complement(top)),
inference(superposition,[],[f741,f29]) ).
fof(f785,plain,
complement(sF4) = join(complement(sF4),complement(sF5)),
inference(superposition,[],[f741,f40]) ).
fof(f790,plain,
complement(sF4) = join(complement(sF4),sF6),
inference(forward_demodulation,[],[f785,f42]) ).
fof(f796,plain,
! [X0] : complement(complement(X0)) = join(complement(top),complement(complement(X0))),
inference(forward_demodulation,[],[f771,f18]) ).
fof(f797,plain,
complement(sF4) = join(sF6,complement(sF4)),
inference(forward_demodulation,[],[f790,f18]) ).
fof(f803,plain,
! [X0] : join(complement(top),X0) = X0,
inference(forward_demodulation,[],[f796,f691]) ).
fof(f804,plain,
sK1 = join(sF6,sK1),
inference(forward_demodulation,[],[f797,f696]) ).
fof(f808,plain,
! [X0] : join(zero,X0) = X0,
inference(forward_demodulation,[],[f803,f57]) ).
fof(f809,plain,
sK1 = join(sK1,sF6),
inference(forward_demodulation,[],[f804,f18]) ).
fof(f818,plain,
zero = composition(converse(sK0),sF3),
inference(backward_demodulation,[],[f204,f808]) ).
fof(f946,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = join(complement(join(complement(join(complement(X1),complement(X0))),join(complement(X0),X1))),complement(X0)),
inference(superposition,[],[f113,f113]) ).
fof(f968,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = join(complement(X0),complement(join(complement(join(complement(X1),complement(X0))),join(complement(X0),X1)))),
inference(forward_demodulation,[],[f946,f18]) ).
fof(f1001,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = join(complement(X0),complement(join(join(complement(X0),X1),complement(join(complement(X1),complement(X0)))))),
inference(forward_demodulation,[],[f968,f18]) ).
fof(f1022,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = join(complement(X0),complement(join(complement(X0),join(X1,complement(join(complement(X1),complement(X0))))))),
inference(forward_demodulation,[],[f1001,f19]) ).
fof(f1034,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = join(complement(X0),complement(join(complement(X0),X1))),
inference(forward_demodulation,[],[f1022,f492]) ).
fof(f1041,plain,
! [X0,X1] : join(complement(X0),X1) = join(complement(X0),complement(join(complement(X1),join(complement(X1),complement(X0))))),
inference(backward_demodulation,[],[f234,f1034]) ).
fof(f1045,plain,
! [X0,X1] : join(complement(X0),X1) = join(complement(X0),complement(join(complement(X1),complement(X0)))),
inference(forward_demodulation,[],[f1041,f580]) ).
fof(f1050,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = join(complement(X1),complement(join(X0,complement(X1)))),
inference(superposition,[],[f1045,f691]) ).
fof(f1068,plain,
! [X0,X1] : join(complement(join(complement(complement(X0)),X1)),X0) = join(complement(join(complement(complement(X0)),X1)),complement(complement(X0))),
inference(superposition,[],[f1045,f492]) ).
fof(f1069,plain,
! [X0,X1] : join(complement(join(X1,complement(complement(X0)))),X0) = join(complement(join(X1,complement(complement(X0)))),complement(complement(X0))),
inference(superposition,[],[f1045,f535]) ).
fof(f1090,plain,
! [X0,X1] : join(complement(join(X1,complement(complement(X0)))),X0) = join(complement(complement(X0)),complement(join(X1,complement(complement(X0))))),
inference(forward_demodulation,[],[f1069,f18]) ).
fof(f1091,plain,
! [X0,X1] : join(complement(join(complement(complement(X0)),X1)),X0) = join(complement(complement(X0)),complement(join(complement(complement(X0)),X1))),
inference(forward_demodulation,[],[f1068,f18]) ).
fof(f1115,plain,
! [X0,X1] : join(complement(complement(X0)),complement(X1)) = join(complement(join(X1,complement(complement(X0)))),X0),
inference(forward_demodulation,[],[f1090,f1050]) ).
fof(f1116,plain,
! [X0,X1] : join(complement(X1),complement(complement(X0))) = join(complement(join(complement(complement(X0)),X1)),X0),
inference(forward_demodulation,[],[f1091,f1034]) ).
fof(f1130,plain,
! [X0,X1] : join(complement(complement(X0)),complement(X1)) = join(X0,complement(join(X1,complement(complement(X0))))),
inference(forward_demodulation,[],[f1115,f18]) ).
fof(f1131,plain,
! [X0,X1] : join(complement(X1),complement(complement(X0))) = join(X0,complement(join(complement(complement(X0)),X1))),
inference(forward_demodulation,[],[f1116,f18]) ).
fof(f1143,plain,
! [X0,X1] : join(X0,complement(X1)) = join(X0,complement(join(X1,X0))),
inference(forward_demodulation,[],[f1130,f691]) ).
fof(f1144,plain,
! [X0,X1] : join(complement(X1),X0) = join(X0,complement(join(X0,X1))),
inference(forward_demodulation,[],[f1131,f691]) ).
fof(f1173,plain,
! [X0] : join(X0,complement(X0)) = join(complement(zero),X0),
inference(superposition,[],[f1144,f552]) ).
fof(f1186,plain,
join(complement(sF4),sF3) = join(sF3,complement(sF5)),
inference(superposition,[],[f1144,f40]) ).
fof(f1211,plain,
join(complement(sF4),sF3) = join(sF3,sF6),
inference(forward_demodulation,[],[f1186,f42]) ).
fof(f1219,plain,
! [X0] : join(X0,complement(X0)) = join(top,X0),
inference(forward_demodulation,[],[f1173,f694]) ).
fof(f1229,plain,
join(sF3,sF6) = join(sF3,complement(sF4)),
inference(forward_demodulation,[],[f1211,f18]) ).
fof(f1236,plain,
! [X0] : top = join(top,X0),
inference(forward_demodulation,[],[f1219,f29]) ).
fof(f1241,plain,
join(sF3,sF6) = join(sF3,sK1),
inference(forward_demodulation,[],[f1229,f696]) ).
fof(f1249,plain,
! [X0] : composition(sK0,top) = join(sK0,composition(sK0,X0)),
inference(backward_demodulation,[],[f370,f1236]) ).
fof(f1255,plain,
join(sF3,sF6) = join(sK1,sF3),
inference(forward_demodulation,[],[f1241,f18]) ).
fof(f1258,plain,
! [X0] : sK0 = join(sK0,composition(sK0,X0)),
inference(forward_demodulation,[],[f1249,f60]) ).
fof(f1283,plain,
! [X0,X1] : join(X0,complement(X1)) = join(X0,complement(join(X0,X1))),
inference(superposition,[],[f1143,f18]) ).
fof(f1292,plain,
! [X0] : join(X0,complement(X0)) = join(X0,complement(zero)),
inference(superposition,[],[f1143,f808]) ).
fof(f1327,plain,
! [X0] : join(X0,complement(X0)) = join(X0,top),
inference(forward_demodulation,[],[f1292,f694]) ).
fof(f1341,plain,
! [X0] : top = join(X0,top),
inference(forward_demodulation,[],[f1327,f29]) ).
fof(f1469,plain,
composition(converse(sF3),sK0) = converse(zero),
inference(superposition,[],[f73,f818]) ).
fof(f1744,plain,
complement(sK0) = join(complement(sK0),composition(converse(converse(sF3)),complement(converse(zero)))),
inference(superposition,[],[f58,f1469]) ).
fof(f1751,plain,
complement(sK0) = join(complement(sK0),composition(sF3,complement(converse(zero)))),
inference(forward_demodulation,[],[f1744,f25]) ).
fof(f1757,plain,
sF3 = join(sF3,composition(sF3,complement(converse(zero)))),
inference(forward_demodulation,[],[f1751,f36]) ).
fof(f2728,plain,
composition(sK1,sK2) = join(sF8,composition(sF6,sK2)),
inference(superposition,[],[f65,f809]) ).
fof(f2766,plain,
composition(sK1,sK2) = join(sF8,sF7),
inference(forward_demodulation,[],[f2728,f44]) ).
fof(f2772,plain,
composition(sK1,sK2) = join(sF7,sF8),
inference(forward_demodulation,[],[f2766,f18]) ).
fof(f2774,plain,
sF8 = join(sF7,sF8),
inference(forward_demodulation,[],[f2772,f46]) ).
fof(f2781,plain,
complement(sF7) = join(complement(sF7),complement(sF8)),
inference(superposition,[],[f706,f2774]) ).
fof(f2789,plain,
complement(sF7) = join(complement(sF7),sF9),
inference(forward_demodulation,[],[f2781,f48]) ).
fof(f2793,plain,
complement(sF7) = join(sF9,complement(sF7)),
inference(forward_demodulation,[],[f2789,f18]) ).
fof(f3561,plain,
! [X0,X1] : join(sK0,X1) = join(sK0,join(composition(sK0,X0),X1)),
inference(superposition,[],[f19,f1258]) ).
fof(f3630,plain,
! [X0] : composition(X0,top) = join(X0,composition(X0,top)),
inference(superposition,[],[f366,f1341]) ).
fof(f3914,plain,
! [X2,X3,X0,X1] : join(composition(X0,join(X3,X2)),composition(X1,X2)) = join(composition(X0,X3),composition(join(X0,X1),X2)),
inference(superposition,[],[f384,f24]) ).
fof(f5202,plain,
! [X0] : converse(converse(X0)) = join(converse(zero),X0),
inference(superposition,[],[f62,f808]) ).
fof(f5220,plain,
! [X0] : join(converse(zero),X0) = X0,
inference(forward_demodulation,[],[f5202,f25]) ).
fof(f6103,plain,
zero = converse(zero),
inference(superposition,[],[f552,f5220]) ).
fof(f6110,plain,
sF3 = join(sF3,composition(sF3,complement(zero))),
inference(backward_demodulation,[],[f1757,f6103]) ).
fof(f6183,plain,
sF3 = join(sF3,composition(sF3,top)),
inference(forward_demodulation,[],[f6110,f694]) ).
fof(f6220,plain,
sF3 = composition(sF3,top),
inference(forward_demodulation,[],[f6183,f3630]) ).
fof(f7491,plain,
join(sF10,complement(sF7)) = join(sF3,complement(sF7)),
inference(superposition,[],[f224,f2793]) ).
fof(f7557,plain,
! [X2,X0,X1] : join(composition(X0,X1),composition(join(X0,X2),complement(X1))) = join(composition(X0,top),composition(X2,complement(X1))),
inference(superposition,[],[f3914,f29]) ).
fof(f8046,plain,
! [X2,X0,X1] : join(composition(X1,top),composition(X0,complement(X2))) = join(composition(X1,X2),composition(join(X0,X1),complement(X2))),
inference(superposition,[],[f7557,f18]) ).
fof(f8101,plain,
! [X0] : join(composition(sF3,top),composition(sF6,complement(X0))) = join(composition(sF3,X0),composition(join(sK1,sF3),complement(X0))),
inference(superposition,[],[f7557,f1255]) ).
fof(f8166,plain,
! [X0] : join(composition(sF3,X0),composition(join(sK1,sF3),complement(X0))) = join(sF3,composition(sF6,complement(X0))),
inference(forward_demodulation,[],[f8101,f6220]) ).
fof(f8244,plain,
! [X0] : join(sF3,composition(sF6,complement(X0))) = join(composition(sF3,top),composition(sK1,complement(X0))),
inference(forward_demodulation,[],[f8166,f8046]) ).
fof(f8289,plain,
! [X0] : join(sF3,composition(sF6,complement(X0))) = join(sF3,composition(sK1,complement(X0))),
inference(forward_demodulation,[],[f8244,f6220]) ).
fof(f8572,plain,
! [X0] : join(sF3,composition(sF6,X0)) = join(sF3,composition(sK1,X0)),
inference(superposition,[],[f8289,f691]) ).
fof(f16523,plain,
! [X2,X0,X1] : join(composition(X0,X1),top) = join(composition(join(X0,X2),X1),complement(composition(X2,X1))),
inference(superposition,[],[f221,f29]) ).
fof(f16671,plain,
! [X2,X0,X1] : join(composition(X0,X1),top) = join(complement(composition(X2,X1)),composition(join(X0,X2),X1)),
inference(forward_demodulation,[],[f16523,f18]) ).
fof(f16798,plain,
! [X2,X0,X1] : join(top,composition(X0,X1)) = join(complement(composition(X2,X1)),composition(join(X0,X2),X1)),
inference(forward_demodulation,[],[f16671,f18]) ).
fof(f16861,plain,
! [X2,X0,X1] : top = join(complement(composition(X2,X1)),composition(join(X0,X2),X1)),
inference(forward_demodulation,[],[f16798,f1236]) ).
fof(f17024,plain,
! [X0] : top = join(complement(composition(sF6,X0)),composition(sK0,X0)),
inference(superposition,[],[f16861,f762]) ).
fof(f17153,plain,
! [X0] : top = join(composition(sK0,X0),complement(composition(sF6,X0))),
inference(forward_demodulation,[],[f17024,f18]) ).
fof(f30598,plain,
join(complement(sF7),complement(sF10)) = join(complement(sF7),complement(join(sF3,complement(sF7)))),
inference(superposition,[],[f1143,f7491]) ).
fof(f30633,plain,
join(complement(sF7),complement(sF10)) = join(complement(sF7),complement(sF3)),
inference(forward_demodulation,[],[f30598,f1143]) ).
fof(f30658,plain,
join(complement(sF7),complement(sF10)) = join(complement(sF3),complement(sF7)),
inference(forward_demodulation,[],[f30633,f18]) ).
fof(f30670,plain,
join(complement(sF7),complement(sF10)) = join(sK0,complement(sF7)),
inference(forward_demodulation,[],[f30658,f695]) ).
fof(f30678,plain,
join(complement(sF7),sF11) = join(sK0,complement(sF7)),
inference(forward_demodulation,[],[f30670,f52]) ).
fof(f30681,plain,
join(sF11,complement(sF7)) = join(sK0,complement(sF7)),
inference(forward_demodulation,[],[f30678,f18]) ).
fof(f30709,plain,
join(sF11,complement(complement(sF7))) = join(sF11,complement(join(sK0,complement(sF7)))),
inference(superposition,[],[f1283,f30681]) ).
fof(f30737,plain,
join(sF11,sF7) = join(sF11,complement(join(sK0,complement(sF7)))),
inference(forward_demodulation,[],[f30709,f691]) ).
fof(f30765,plain,
join(sF7,sF11) = join(sF11,complement(join(sK0,complement(sF7)))),
inference(forward_demodulation,[],[f30737,f18]) ).
fof(f36427,plain,
! [X0] : join(sK0,top) = join(sK0,complement(composition(sF6,X0))),
inference(superposition,[],[f3561,f17153]) ).
fof(f36516,plain,
! [X0] : join(top,sK0) = join(sK0,complement(composition(sF6,X0))),
inference(forward_demodulation,[],[f36427,f18]) ).
fof(f36568,plain,
! [X0] : top = join(sK0,complement(composition(sF6,X0))),
inference(forward_demodulation,[],[f36516,f1236]) ).
fof(f36992,plain,
top = join(sK0,complement(sF7)),
inference(superposition,[],[f36568,f44]) ).
fof(f37108,plain,
join(sF11,complement(top)) = join(sF7,sF11),
inference(backward_demodulation,[],[f30765,f36992]) ).
fof(f37140,plain,
join(sF11,zero) = join(sF7,sF11),
inference(forward_demodulation,[],[f37108,f57]) ).
fof(f37162,plain,
join(zero,sF11) = join(sF7,sF11),
inference(forward_demodulation,[],[f37140,f18]) ).
fof(f37180,plain,
sF11 = join(sF7,sF11),
inference(forward_demodulation,[],[f37162,f808]) ).
fof(f37204,plain,
complement(sF7) = join(complement(sF7),complement(sF11)),
inference(superposition,[],[f706,f37180]) ).
fof(f37243,plain,
complement(sF7) = join(complement(sF7),sF10),
inference(forward_demodulation,[],[f37204,f699]) ).
fof(f37257,plain,
complement(sF7) = join(sF10,complement(sF7)),
inference(forward_demodulation,[],[f37243,f18]) ).
fof(f37262,plain,
complement(sF7) = join(sF3,complement(sF7)),
inference(backward_demodulation,[],[f7491,f37257]) ).
fof(f38211,plain,
join(sF3,sF7) = join(sF3,composition(sK1,sK2)),
inference(superposition,[],[f8572,f44]) ).
fof(f38310,plain,
join(sF3,sF8) = join(sF3,sF7),
inference(forward_demodulation,[],[f38211,f46]) ).
fof(f38413,plain,
join(sF3,complement(sF8)) = join(sF3,complement(join(sF3,sF7))),
inference(superposition,[],[f1283,f38310]) ).
fof(f38443,plain,
join(sF3,complement(sF8)) = join(complement(sF7),sF3),
inference(forward_demodulation,[],[f38413,f1144]) ).
fof(f38471,plain,
join(sF3,complement(sF8)) = join(sF3,complement(sF7)),
inference(forward_demodulation,[],[f38443,f18]) ).
fof(f38502,plain,
complement(sF7) = join(sF3,complement(sF8)),
inference(forward_demodulation,[],[f38471,f37262]) ).
fof(f38510,plain,
join(sF3,sF9) = complement(sF7),
inference(forward_demodulation,[],[f38502,f48]) ).
fof(f38516,plain,
sF10 = complement(sF7),
inference(forward_demodulation,[],[f38510,f50]) ).
fof(f38606,plain,
sF7 = complement(sF10),
inference(superposition,[],[f691,f38516]) ).
fof(f38634,plain,
sF7 = sF11,
inference(backward_demodulation,[],[f52,f38606]) ).
fof(f38635,plain,
$false,
inference(forward_subsumption_resolution,[],[f38634,f53]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : REL033+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.17/0.45 % Computer : n005.cluster.edu
% 0.17/0.45 % Model : x86_64 x86_64
% 0.17/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.45 % Memory : 8046.5625MB
% 0.17/0.45 % OS : Linux 6.8.0-71-generic
% 0.17/0.45 % CPULimit : 300
% 0.17/0.45 % WCLimit : 300
% 0.17/0.45 % DateTime : Sun Sep 27 22:54:02 UTC 2026
% 0.17/0.45 % CPUTime :
% 0.17/0.46 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.22/0.51 Running first-order theorem proving
% 0.22/0.51 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 22.62/4.18 % (269095)Detected formulas, will run a generic FOF schedule.
% 22.62/4.18 % (269113)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2945897975:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 22.62/4.18 % (269114)dis-21_1_sil=8000:lcm=predicate:random_seed=1075872222:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 22.62/4.18 % (269114)Refutation not found, incomplete strategy
% 22.62/4.18 % (269114)------------------------------
% 22.62/4.18 % (269114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.62/4.18 % (269114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.62/4.18 % (269114)CaDiCaL version: 2.1.3
% 22.62/4.18 % (269114)Termination reason: Refutation not found, incomplete strategy
% 22.62/4.18 % (269114)Time elapsed: 0.001 s
% 22.62/4.18 % (269114)Peak memory usage: 88 MB
% 22.62/4.18 % (269114)Instructions burned: 1 (million)
% 22.62/4.18 % (269112)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2379700535:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 22.62/4.18 % (269111)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2264334026:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 22.62/4.18 % (269109)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=580239294:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 22.62/4.18 % (269110)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=1323207409:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 22.62/4.18 % (269108)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=926516558:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 22.62/4.18 % (269113)Instruction limit reached!
% 22.62/4.18 % (269113)------------------------------
% 22.62/4.18 % (269113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.62/4.18 % (269113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.62/4.18 % (269113)CaDiCaL version: 2.1.3
% 22.62/4.18 % (269113)Termination reason: Instruction limit
% 22.62/4.18 % (269113)Termination phase: Saturation
% 22.62/4.18 % (269113)Time elapsed: 0.138 s
% 22.62/4.18 % (269113)Peak memory usage: 90 MB
% 22.62/4.18 % (269113)Instructions burned: 139 (million)
% 22.62/4.18 % (269111)Instruction limit reached!
% 22.62/4.18 % (269111)------------------------------
% 22.62/4.18 % (269111)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.62/4.18 % (269111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.62/4.18 % (269111)CaDiCaL version: 2.1.3
% 22.62/4.18 % (269111)Termination reason: Instruction limit
% 22.62/4.18 % (269111)Termination phase: Saturation
% 22.62/4.18 % (269111)Time elapsed: 0.105 s
% 22.62/4.18 % (269111)Peak memory usage: 89 MB
% 22.62/4.18 % (269111)Instructions burned: 110 (million)
% 22.62/4.18 % (269112)Instruction limit reached!
% 22.62/4.18 % (269112)------------------------------
% 22.62/4.18 % (269112)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.62/4.18 % (269112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.62/4.18 % (269112)CaDiCaL version: 2.1.3
% 22.62/4.18 % (269112)Termination reason: Instruction limit
% 22.62/4.18 % (269112)Termination phase: Saturation
% 22.62/4.18 % (269112)Time elapsed: 0.110 s
% 22.62/4.18 % (269112)Peak memory usage: 88 MB
% 22.62/4.18 % (269112)Instructions burned: 120 (million)
% 22.62/4.18 % (269114)------------------------------
% 22.62/4.18 % (269114)------------------------------
% 22.62/4.18 % (269122)lrs+10_1_sil=8000:sp=occurrence:random_seed=492340989:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 22.62/4.18 % (269124)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1162749281:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 22.62/4.18 % (269125)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2122054980:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 22.62/4.18 % (269127)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=1293840022:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 22.62/4.18 % (269122)Instruction limit reached!
% 31.63/5.54 % (269122)------------------------------
% 31.63/5.54 % (269122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.63/5.54 % (269122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.63/5.54 % (269122)CaDiCaL version: 2.1.3
% 31.63/5.54 % (269122)Termination reason: Instruction limit
% 31.63/5.54 % (269122)Termination phase: Saturation
% 31.63/5.54 % (269122)Time elapsed: 0.169 s
% 31.63/5.54 % (269122)Peak memory usage: 92 MB
% 31.63/5.54 % (269122)Instructions burned: 287 (million)
% 31.63/5.54 % (269124)Instruction limit reached!
% 31.63/5.54 % (269124)------------------------------
% 31.63/5.54 % (269124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.63/5.54 % (269124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.63/5.54 % (269124)CaDiCaL version: 2.1.3
% 31.63/5.54 % (269124)Termination reason: Instruction limit
% 31.63/5.54 % (269124)Termination phase: Saturation
% 31.63/5.54 % (269124)Time elapsed: 0.152 s
% 31.63/5.54 % (269124)Peak memory usage: 91 MB
% 31.63/5.54 % (269124)Instructions burned: 158 (million)
% 31.63/5.54 % (269132)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1217721054:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 31.63/5.54 % (269127)Instruction limit reached!
% 31.63/5.54 % (269127)------------------------------
% 31.63/5.54 % (269127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.63/5.54 % (269127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.63/5.54 % (269127)CaDiCaL version: 2.1.3
% 31.63/5.54 % (269127)Termination reason: Instruction limit
% 31.63/5.54 % (269127)Termination phase: Saturation
% 31.63/5.54 % (269127)Time elapsed: 0.252 s
% 31.63/5.54 % (269127)Peak memory usage: 92 MB
% 31.63/5.54 % (269127)Instructions burned: 248 (million)
% 31.63/5.54 % (269125)Instruction limit reached!
% 31.63/5.54 % (269125)------------------------------
% 31.63/5.54 % (269125)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.63/5.54 % (269125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.63/5.54 % (269125)CaDiCaL version: 2.1.3
% 31.63/5.54 % (269125)Termination reason: Instruction limit
% 31.63/5.54 % (269125)Termination phase: Saturation
% 31.63/5.54 % (269125)Time elapsed: 0.321 s
% 31.63/5.54 % (269125)Peak memory usage: 92 MB
% 31.63/5.54 % (269125)Instructions burned: 327 (million)
% 31.63/5.54 % (269133)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2864478720:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 31.63/5.54 % (269132)Instruction limit reached!
% 31.63/5.54 % (269132)------------------------------
% 31.63/5.54 % (269132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.63/5.54 % (269132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.63/5.54 % (269132)CaDiCaL version: 2.1.3
% 31.63/5.54 % (269132)Termination reason: Instruction limit
% 31.63/5.54 % (269132)Termination phase: Saturation
% 31.63/5.54 % (269132)Time elapsed: 0.156 s
% 31.63/5.54 % (269132)Peak memory usage: 92 MB
% 31.63/5.54 % (269132)Instructions burned: 294 (million)
% 31.63/5.54 % (269135)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3264563359:cts=off:i=113:fsr=off:ss=included:sgt=4_2991 on theBenchmark for (2991ds/113Mi)
% 31.63/5.54 % (269136)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2597042774:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi)
% 31.63/5.54 % (269136)Refutation not found, incomplete strategy
% 31.63/5.54 % (269136)------------------------------
% 31.63/5.54 % (269136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.63/5.54 % (269136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.63/5.54 % (269136)CaDiCaL version: 2.1.3
% 31.63/5.54 % (269136)Termination reason: Refutation not found, incomplete strategy
% 31.63/5.54 % (269136)Time elapsed: 0.002 s
% 31.63/5.54 % (269136)Peak memory usage: 88 MB
% 31.63/5.54 % (269138)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3282456726:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi)
% 31.63/5.54 % (269135)Instruction limit reached!
% 31.63/5.54 % (269135)------------------------------
% 31.63/5.54 % (269135)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.63/5.54 % (269135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.63/5.54 % (269135)CaDiCaL version: 2.1.3
% 59.08/9.97 % (269135)Termination reason: Instruction limit
% 59.08/9.97 % (269135)Termination phase: Saturation
% 59.08/9.97 % (269135)Time elapsed: 0.108 s
% 59.08/9.97 % (269135)Peak memory usage: 90 MB
% 59.08/9.97 % (269135)Instructions burned: 113 (million)
% 59.08/9.97 % (269138)Instruction limit reached!
% 59.08/9.97 % (269138)------------------------------
% 59.08/9.97 % (269138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.08/9.97 % (269138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.08/9.97 % (269138)CaDiCaL version: 2.1.3
% 59.08/9.97 % (269138)Termination reason: Instruction limit
% 59.08/9.97 % (269138)Termination phase: Saturation
% 59.08/9.97 % (269138)Time elapsed: 0.057 s
% 59.08/9.97 % (269138)Peak memory usage: 89 MB
% 59.08/9.97 % (269138)Instructions burned: 122 (million)
% 59.08/9.97 % (269143)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2794556156:i=437:sd=1:aac=none:ss=included_2988 on theBenchmark for (2988ds/437Mi)
% 59.08/9.97 % (269142)lrs+10_1_sil=8000:sp=occurrence:random_seed=2939446963:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2988 on theBenchmark for (2988ds/907Mi)
% 59.08/9.97 % (269136)------------------------------
% 59.08/9.97 % (269136)------------------------------
% 59.08/9.97 % (269143)Instruction limit reached!
% 59.08/9.97 % (269143)------------------------------
% 59.08/9.97 % (269143)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.08/9.97 % (269143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.08/9.97 % (269143)CaDiCaL version: 2.1.3
% 59.08/9.97 % (269143)Termination reason: Instruction limit
% 59.08/9.97 % (269143)Termination phase: Saturation
% 59.08/9.97 % (269143)Time elapsed: 0.176 s
% 59.08/9.97 % (269143)Peak memory usage: 92 MB
% 59.08/9.97 % (269143)Instructions burned: 437 (million)
% 59.08/9.97 % (269146)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3053477059:i=5202:ss=axioms:sgt=16_2985 on theBenchmark for (2985ds/5202Mi)
% 59.08/9.97 % (269148)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2786373034:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2984 on theBenchmark for (2984ds/134Mi)
% 59.08/9.97 % (269148)Refutation not found, incomplete strategy
% 59.08/9.97 % (269148)------------------------------
% 59.08/9.97 % (269148)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.08/9.97 % (269148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.08/9.97 % (269148)CaDiCaL version: 2.1.3
% 59.08/9.97 % (269148)Termination reason: Refutation not found, incomplete strategy
% 59.08/9.97 % (269148)Time elapsed: 0.002 s
% 59.08/9.97 % (269148)Peak memory usage: 89 MB
% 59.08/9.97 % (269148)Instructions burned: 1 (million)
% 59.08/9.97 % (269148)------------------------------
% 59.08/9.97 % (269148)------------------------------
% 59.08/9.97 % (269142)Instruction limit reached!
% 59.08/9.97 % (269142)------------------------------
% 59.08/9.97 % (269142)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.08/9.97 % (269142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.08/9.97 % (269142)CaDiCaL version: 2.1.3
% 59.08/9.97 % (269142)Termination reason: Instruction limit
% 59.08/9.97 % (269142)Termination phase: Saturation
% 59.08/9.97 % (269142)Time elapsed: 0.850 s
% 59.08/9.97 % (269142)Peak memory usage: 97 MB
% 59.08/9.97 % (269142)Instructions burned: 907 (million)
% 59.08/9.97 % (269155)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3724204957:st=8:i=592:sd=3:ep=RST:ss=axioms_2978 on theBenchmark for (2978ds/592Mi)
% 59.08/9.97 % (269156)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1309494788:st=3:i=13193:sd=3:ss=axioms_2977 on theBenchmark for (2977ds/13193Mi)
% 59.08/9.97 % (269155)Instruction limit reached!
% 59.08/9.97 % (269155)------------------------------
% 59.08/9.97 % (269155)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.08/9.97 % (269155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.08/9.97 % (269155)CaDiCaL version: 2.1.3
% 59.08/9.97 % (269155)Termination reason: Instruction limit
% 59.08/9.97 % (269155)Termination phase: Saturation
% 59.08/9.97 % (269155)Time elapsed: 0.587 s
% 59.08/9.97 % (269155)Peak memory usage: 94 MB
% 59.08/9.97 % (269155)Instructions burned: 592 (million)
% 59.08/9.97 % (269159)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=345485012:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2970 on theBenchmark for (2970ds/125Mi)
% 59.08/9.97 % (269159)Instruction limit reached!
% 59.08/9.97 % (269159)------------------------------
% 59.08/9.97 % (269159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.08/9.97 % (269159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.08/9.97 % (269159)CaDiCaL version: 2.1.3
% 59.08/9.97 % (269159)Termination reason: Instruction limit
% 59.08/9.97 % (269159)Termination phase: Saturation
% 59.08/9.97 % (269159)Time elapsed: 0.134 s
% 59.08/9.97 % (269159)Peak memory usage: 90 MB
% 59.08/9.97 % (269159)Instructions burned: 125 (million)
% 59.08/9.97 % (269133)Instruction limit reached!
% 59.08/9.97 % (269133)------------------------------
% 59.08/9.97 % (269133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.08/9.97 % (269133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.08/9.97 % (269133)CaDiCaL version: 2.1.3
% 59.08/9.97 % (269133)Termination reason: Instruction limit
% 59.08/9.97 % (269133)Termination phase: Saturation
% 59.08/9.97 % (269133)Time elapsed: 2.433 s
% 59.08/9.97 % (269133)Peak memory usage: 141 MB
% 59.08/9.97 % (269133)Instructions burned: 2350 (million)
% 59.08/9.97 % (269163)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2723815202:i=134:gtgl=5:slsql=off:gtg=exists_sym_2967 on theBenchmark for (2967ds/134Mi)
% 59.08/9.97 % (269164)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3195179650:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2966 on theBenchmark for (2966ds/141Mi)
% 59.08/9.97 % (269164)Refutation not found, incomplete strategy
% 59.08/9.97 % (269164)------------------------------
% 59.08/9.97 % (269164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.08/9.97 % (269164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.08/9.97 % (269164)CaDiCaL version: 2.1.3
% 59.08/9.97 % (269164)Termination reason: Refutation not found, incomplete strategy
% 59.08/9.97 % (269164)Time elapsed: 0.002 s
% 59.08/9.97 % (269164)Peak memory usage: 88 MB
% 59.08/9.97 % (269163)Instruction limit reached!
% 59.08/9.97 % (269163)------------------------------
% 59.08/9.97 % (269163)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.08/9.97 % (269163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.08/9.97 % (269163)CaDiCaL version: 2.1.3
% 59.08/9.97 % (269163)Termination reason: Instruction limit
% 59.08/9.97 % (269163)Termination phase: Saturation
% 59.08/9.97 % (269163)Time elapsed: 0.126 s
% 59.08/9.97 % (269163)Peak memory usage: 89 MB
% 59.08/9.97 % (269163)Instructions burned: 134 (million)
% 59.08/9.97 % (269167)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1542824410:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2963 on theBenchmark for (2963ds/431Mi)
% 59.08/9.97 % (269167)Refutation not found, incomplete strategy
% 59.08/9.97 % (269167)------------------------------
% 59.08/9.97 % (269167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.08/9.97 % (269167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.08/9.97 % (269167)CaDiCaL version: 2.1.3
% 59.08/9.97 % (269167)Termination reason: Refutation not found, incomplete strategy
% 59.08/9.97 % (269167)Time elapsed: 0.002 s
% 59.08/9.97 % (269167)Peak memory usage: 88 MB
% 59.08/9.97 % (269164)------------------------------
% 59.08/9.97 % (269164)------------------------------
% 59.08/9.97 % (269169)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=1661288153:i=6060:aac=none:ins=25_2960 on theBenchmark for (2960ds/6060Mi)
% 59.08/9.97 % (269167)------------------------------
% 59.08/9.97 % (269167)------------------------------
% 59.08/9.97 % (269146)Instruction limit reached!
% 59.08/9.97 % (269146)------------------------------
% 59.08/9.97 % (269146)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.08/9.97 % (269146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.08/9.97 % (269146)CaDiCaL version: 2.1.3
% 59.08/9.97 % (269146)Termination reason: Instruction limit
% 59.08/9.97 % (269146)Termination phase: Saturation
% 59.08/9.97 % (269146)Time elapsed: 2.864 s
% 59.08/9.97 % (269146)Peak memory usage: 164 MB
% 59.08/9.97 % (269146)Instructions burned: 5203 (million)
% 59.08/9.97 % (269173)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=2733537798:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2957 on theBenchmark for (2957ds/150Mi)
% 59.08/9.97 % (269173)Instruction limit reached!
% 59.08/9.97 % (269173)------------------------------
% 59.08/9.97 % (269173)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.08/9.97 % (269173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.08/9.97 % (269173)CaDiCaL version: 2.1.3
% 59.08/9.97 % (269173)Termination reason: Instruction limit
% 59.08/9.97 % (269173)Termination phase: Saturation
% 59.08/9.97 % (269173)Time elapsed: 0.124 s
% 59.08/9.97 % (269173)Peak memory usage: 90 MB
% 59.08/9.97 % (269173)Instructions burned: 151 (million)
% 59.08/9.97 % (269174)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1626358194:i=14155:bd=all_2955 on theBenchmark for (2955ds/14155Mi)
% 59.08/9.97 % (269178)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2960049546:i=667:av=off:fsr=off_2953 on theBenchmark for (2953ds/667Mi)
% 59.08/9.97 % (269178)Instruction limit reached!
% 59.08/9.97 % (269178)------------------------------
% 59.08/9.97 % (269178)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.08/9.97 % (269178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.08/9.97 % (269178)CaDiCaL version: 2.1.3
% 59.08/9.97 % (269178)Termination reason: Instruction limit
% 59.08/9.97 % (269178)Termination phase: Saturation
% 59.08/9.97 % (269178)Time elapsed: 0.493 s
% 59.08/9.97 % (269178)Peak memory usage: 89 MB
% 59.08/9.97 % (269178)Instructions burned: 667 (million)
% 59.08/9.97 % (269181)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=2735640118:s2a=on:i=185:s2at=1.8:fdi=4_2946 on theBenchmark for (2946ds/185Mi)
% 59.08/9.97 % (269181)Instruction limit reached!
% 59.08/9.97 % (269181)------------------------------
% 59.08/9.97 % (269181)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.08/9.97 % (269181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.08/9.97 % (269181)CaDiCaL version: 2.1.3
% 59.08/9.97 % (269181)Termination reason: Instruction limit
% 59.08/9.97 % (269181)Termination phase: Saturation
% 59.08/9.97 % (269181)Time elapsed: 0.178 s
% 59.08/9.97 % (269181)Peak memory usage: 90 MB
% 59.08/9.97 % (269181)Instructions burned: 186 (million)
% 59.08/9.97 % (269183)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2877467451:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2942 on theBenchmark for (2942ds/193Mi)
% 59.08/9.97 % (269183)Instruction limit reached!
% 59.08/9.97 % (269183)------------------------------
% 59.08/9.97 % (269183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.08/9.97 % (269183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.08/9.97 % (269183)CaDiCaL version: 2.1.3
% 59.08/9.97 % (269183)Termination reason: Instruction limit
% 59.08/9.97 % (269183)Termination phase: Saturation
% 59.08/9.97 % (269183)Time elapsed: 0.179 s
% 59.08/9.97 % (269183)Peak memory usage: 90 MB
% 59.08/9.97 % (269183)Instructions burned: 193 (million)
% 59.08/9.97 % (269185)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=795625302:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2938 on theBenchmark for (2938ds/4850Mi)
% 59.08/9.97 % (269185)Refutation not found, incomplete strategy
% 59.08/9.97 % (269185)------------------------------
% 59.08/9.97 % (269185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.08/9.97 % (269185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.08/9.97 % (269185)CaDiCaL version: 2.1.3
% 59.08/9.97 % (269185)Termination reason: Refutation not found, incomplete strategy
% 59.08/9.97 % (269185)Time elapsed: 0.002 s
% 59.08/9.97 % (269185)Peak memory usage: 88 MB
% 59.08/9.97 % (269185)------------------------------
% 59.08/9.97 % (269185)------------------------------
% 59.08/9.97 % (269191)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3146378325:i=12111:sd=1:ss=included_2931 on theBenchmark for (2931ds/12111Mi)
% 59.08/9.97 % (269174)First to succeed.
% 59.08/9.97 % (269174)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-269095"
% 59.08/9.97 % (269174)Refutation found. Thanks to Tanya!
% 59.08/9.97 % SZS status Theorem for theBenchmark
% 59.08/9.97 % SZS output start Proof for theBenchmark
% See solution above
% 64.19/10.23 % (269174)------------------------------
% 64.19/10.23 % (269174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.19/10.23 % (269174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.19/10.23 % (269174)CaDiCaL version: 2.1.3
% 64.19/10.23 % (269174)Termination reason: Refutation
% 64.19/10.23 % (269174)Time elapsed: 3.783 s
% 64.19/10.23 % (269174)Peak memory usage: 168 MB
% 64.19/10.23 % (269174)Instructions burned: 5215 (million)
% 64.19/10.23 % (269174)------------------------------
% 64.19/10.23 % (269174)------------------------------
% 64.19/10.23 % (269095)Success in time 8.943 s
% 64.19/10.23 % Vampire exiting
%------------------------------------------------------------------------------