%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : REL043+2 : 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 : n026.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:34:06 PM UTC 2026
% Result : Theorem 17.80s 3.57s
% Output : Refutation 18.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 21
% Syntax : Number of formulae : 166 ( 162 unt; 7 def)
% Number of atoms : 170 ( 169 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 9 ( 5 ~; 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 : 18 ( 18 usr; 13 con; 0-2 aty)
% Number of variables : 197 ( 194 !; 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,axiom,
! [X0,X1,X2] : join(meet(composition(X0,X1),X2),composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2)))) = composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dedekind_law) ).
fof(f17,conjecture,
! [X0,X1,X2] :
( join(composition(X0,converse(X1)),X2) = X2
=> join(composition(complement(X2),X1),complement(X0)) = complement(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f18,negated_conjecture,
~ ! [X0,X1,X2] :
( join(composition(X0,converse(X1)),X2) = X2
=> join(composition(complement(X2),X1),complement(X0)) = complement(X0) ),
inference(negated_conjecture,[status(cth)],[f17]) ).
fof(f19,plain,
? [X0,X1,X2] :
( complement(X0) != join(composition(complement(X2),X1),complement(X0))
& join(composition(X0,converse(X1)),X2) = X2 ),
inference(ennf_transformation,[],[f18]) ).
fof(f20,plain,
( complement(sK0) != join(composition(complement(sK2),sK1),complement(sK0))
& sK2 = join(composition(sK0,converse(sK1)),sK2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2)],[f19]) ).
fof(f21,plain,
! [X0,X1] : join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f22,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
inference(cnf_transformation,[],[f2]) ).
fof(f23,plain,
! [X0,X1] : join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) = X0,
inference(cnf_transformation,[],[f3]) ).
fof(f24,plain,
! [X0,X1] : complement(join(complement(X0),complement(X1))) = meet(X0,X1),
inference(cnf_transformation,[],[f4]) ).
fof(f26,plain,
! [X0] : composition(X0,one) = X0,
inference(cnf_transformation,[],[f6]) ).
fof(f27,plain,
! [X2,X0,X1] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
inference(cnf_transformation,[],[f7]) ).
fof(f28,plain,
! [X0] : converse(converse(X0)) = X0,
inference(cnf_transformation,[],[f8]) ).
fof(f29,plain,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
inference(cnf_transformation,[],[f9]) ).
fof(f30,plain,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
inference(cnf_transformation,[],[f10]) ).
fof(f31,plain,
! [X0,X1] : complement(X1) = join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)),
inference(cnf_transformation,[],[f11]) ).
fof(f32,plain,
! [X0] : top = join(X0,complement(X0)),
inference(cnf_transformation,[],[f12]) ).
fof(f33,plain,
! [X0] : zero = meet(X0,complement(X0)),
inference(cnf_transformation,[],[f13]) ).
fof(f34,plain,
! [X2,X0,X1] : composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2))) = join(meet(composition(X0,X1),X2),composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2)))),
inference(cnf_transformation,[],[f14]) ).
fof(f37,plain,
sK2 = join(composition(sK0,converse(sK1)),sK2),
inference(cnf_transformation,[],[f20]) ).
fof(f38,plain,
complement(sK0) != join(composition(complement(sK2),sK1),complement(sK0)),
inference(cnf_transformation,[],[f20]) ).
fof(f39,plain,
! [X0] : zero = complement(join(complement(X0),complement(complement(X0)))),
inference(definition_unfolding,[],[f33,f24]) ).
fof(f40,plain,
! [X2,X0,X1] : composition(complement(join(complement(X0),complement(composition(X2,converse(X1))))),complement(join(complement(X1),complement(composition(converse(X0),X2))))) = join(complement(join(complement(composition(X0,X1)),complement(X2))),composition(complement(join(complement(X0),complement(composition(X2,converse(X1))))),complement(join(complement(X1),complement(composition(converse(X0),X2)))))),
inference(definition_unfolding,[],[f34,f24,f24,f24,f24,f24]) ).
fof(f43,definition,
sF3 = complement(sK0),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f44,plain,
complement(sK0) = sF3,
inference(reorient_equations,[],[f43]) ).
fof(f45,definition,
sF4 = complement(sK2),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f46,plain,
complement(sK2) = sF4,
inference(reorient_equations,[],[f45]) ).
fof(f47,definition,
sF5 = composition(sF4,sK1),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f48,plain,
composition(sF4,sK1) = sF5,
inference(reorient_equations,[],[f47]) ).
fof(f49,definition,
sF6 = join(sF5,sF3),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f50,plain,
join(sF5,sF3) = sF6,
inference(reorient_equations,[],[f49]) ).
fof(f51,plain,
sF3 != sF6,
inference(definition_folding,[],[f38,f50,f44,f48,f46,f44]) ).
fof(f52,definition,
sF7 = converse(sK1),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f53,plain,
converse(sK1) = sF7,
inference(reorient_equations,[],[f52]) ).
fof(f54,definition,
sF8 = composition(sK0,sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f55,plain,
composition(sK0,sF7) = sF8,
inference(reorient_equations,[],[f54]) ).
fof(f56,definition,
sF9 = join(sF8,sK2),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f57,plain,
join(sF8,sK2) = sF9,
inference(reorient_equations,[],[f56]) ).
fof(f58,plain,
sK2 = sF9,
inference(definition_folding,[],[f37,f57,f55,f53]) ).
fof(f59,plain,
sK2 = join(sF8,sK2),
inference(forward_demodulation,[],[f57,f58]) ).
fof(f67,plain,
! [X0,X1] : converse(join(converse(X0),X1)) = join(X0,converse(X1)),
inference(superposition,[],[f29,f28]) ).
fof(f69,plain,
! [X0,X1] : converse(join(X1,converse(X0))) = join(converse(X1),X0),
inference(superposition,[],[f29,f28]) ).
fof(f73,plain,
! [X0,X1] : converse(composition(converse(X0),X1)) = composition(converse(X1),X0),
inference(superposition,[],[f30,f28]) ).
fof(f83,plain,
! [X0,X1] : join(complement(join(complement(X0),complement(X1))),complement(join(complement(X1),X0))) = X1,
inference(superposition,[],[f23,f21]) ).
fof(f85,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))) = X0,
inference(superposition,[],[f23,f21]) ).
fof(f107,plain,
! [X2,X0,X1] : composition(join(converse(X1),X2),converse(X0)) = join(converse(composition(X0,X1)),composition(X2,converse(X0))),
inference(superposition,[],[f27,f30]) ).
fof(f201,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(top,X1),
inference(superposition,[],[f22,f32]) ).
fof(f203,plain,
! [X2,X0,X1] : join(X0,X2) = join(complement(join(complement(X0),complement(X1))),join(complement(join(complement(X0),X1)),X2)),
inference(superposition,[],[f22,f23]) ).
fof(f216,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f21,f22]) ).
fof(f270,plain,
! [X0] : converse(converse(X0)) = composition(converse(one),X0),
inference(superposition,[],[f73,f26]) ).
fof(f280,plain,
! [X0] : composition(converse(one),X0) = X0,
inference(forward_demodulation,[],[f270,f28]) ).
fof(f294,plain,
one = converse(one),
inference(superposition,[],[f26,f280]) ).
fof(f298,plain,
! [X0] : composition(one,X0) = X0,
inference(superposition,[],[f280,f294]) ).
fof(f309,plain,
! [X0] : complement(X0) = join(composition(converse(one),complement(X0)),complement(X0)),
inference(superposition,[],[f31,f298]) ).
fof(f312,plain,
! [X0] : complement(X0) = join(complement(X0),complement(X0)),
inference(forward_demodulation,[],[f309,f280]) ).
fof(f324,plain,
! [X0,X1] : join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) = join(X0,complement(join(complement(X0),X1))),
inference(superposition,[],[f203,f312]) ).
fof(f328,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),X1))) = X0,
inference(forward_demodulation,[],[f324,f23]) ).
fof(f342,plain,
! [X0,X1] : join(X1,complement(join(X0,complement(X1)))) = X1,
inference(superposition,[],[f328,f21]) ).
fof(f344,plain,
! [X0] : join(X0,complement(complement(X0))) = X0,
inference(superposition,[],[f328,f328]) ).
fof(f372,plain,
! [X2,X0,X1] : join(X1,X0) = join(complement(join(complement(X0),X2)),join(X1,X0)),
inference(superposition,[],[f216,f328]) ).
fof(f482,plain,
! [X0] : join(X0,converse(complement(converse(X0)))) = converse(top),
inference(superposition,[],[f67,f32]) ).
fof(f515,plain,
! [X0] : join(X0,complement(converse(top))) = X0,
inference(superposition,[],[f328,f482]) ).
fof(f645,plain,
zero = complement(top),
inference(superposition,[],[f39,f32]) ).
fof(f649,plain,
! [X0] : join(complement(join(complement(X0),complement(X0))),zero) = X0,
inference(superposition,[],[f85,f39]) ).
fof(f651,plain,
! [X0] : join(X0,zero) = X0,
inference(superposition,[],[f328,f39]) ).
fof(f659,plain,
! [X0,X1] : zero = join(composition(converse(X1),complement(composition(X1,join(complement(X0),complement(complement(X0)))))),zero),
inference(superposition,[],[f31,f39]) ).
fof(f685,plain,
! [X1] : zero = join(composition(converse(X1),complement(composition(X1,top))),zero),
inference(forward_demodulation,[],[f659,f32]) ).
fof(f693,plain,
! [X0] : complement(join(complement(X0),complement(X0))) = X0,
inference(forward_demodulation,[],[f649,f651]) ).
fof(f709,plain,
! [X1] : zero = composition(converse(X1),complement(composition(X1,top))),
inference(forward_demodulation,[],[f685,f651]) ).
fof(f711,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_demodulation,[],[f693,f312]) ).
fof(f715,plain,
! [X0] : join(complement(X0),complement(complement(X0))) = complement(zero),
inference(superposition,[],[f711,f39]) ).
fof(f716,plain,
sK0 = complement(sF3),
inference(superposition,[],[f711,f44]) ).
fof(f717,plain,
sK2 = complement(sF4),
inference(superposition,[],[f711,f46]) ).
fof(f723,plain,
! [X0] : top = join(complement(X0),X0),
inference(superposition,[],[f32,f711]) ).
fof(f726,plain,
! [X0,X1] : complement(X0) = join(complement(join(complement(X1),X0)),complement(join(X0,X1))),
inference(superposition,[],[f83,f711]) ).
fof(f735,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X0,X1))),
inference(superposition,[],[f328,f711]) ).
fof(f739,plain,
top = complement(zero),
inference(forward_demodulation,[],[f715,f32]) ).
fof(f745,plain,
! [X0,X1] : complement(X1) = join(complement(X1),complement(join(X0,X1))),
inference(superposition,[],[f735,f21]) ).
fof(f871,plain,
! [X0] : complement(X0) = join(complement(join(complement(complement(complement(X0))),X0)),complement(X0)),
inference(superposition,[],[f726,f344]) ).
fof(f900,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(join(complement(join(complement(X1),X0)),join(X0,X1))),complement(complement(X0))),
inference(superposition,[],[f85,f726]) ).
fof(f901,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(complement(X0)),complement(join(complement(join(complement(X1),X0)),join(X0,X1)))),
inference(superposition,[],[f23,f726]) ).
fof(f922,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(complement(X0)),complement(join(X0,X1))),
inference(forward_demodulation,[],[f901,f372]) ).
fof(f923,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(join(complement(join(complement(X1),X0)),join(X0,X1))),X0),
inference(forward_demodulation,[],[f900,f711]) ).
fof(f941,plain,
! [X0] : complement(X0) = join(complement(join(complement(X0),X0)),complement(X0)),
inference(forward_demodulation,[],[f871,f711]) ).
fof(f964,plain,
! [X0,X1] : join(complement(X1),X0) = join(X0,complement(join(X0,X1))),
inference(forward_demodulation,[],[f922,f711]) ).
fof(f965,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(join(X0,X1)),X0),
inference(forward_demodulation,[],[f923,f372]) ).
fof(f970,plain,
! [X0] : complement(X0) = join(complement(top),complement(X0)),
inference(forward_demodulation,[],[f941,f723]) ).
fof(f984,plain,
! [X0] : complement(X0) = join(zero,complement(X0)),
inference(forward_demodulation,[],[f970,f645]) ).
fof(f991,plain,
! [X0] : join(zero,X0) = X0,
inference(superposition,[],[f984,f711]) ).
fof(f992,plain,
sF3 = join(zero,sF3),
inference(superposition,[],[f984,f44]) ).
fof(f1000,plain,
! [X0] : zero = complement(join(complement(zero),X0)),
inference(superposition,[],[f328,f984]) ).
fof(f1006,plain,
! [X0] : complement(zero) = join(complement(zero),complement(complement(X0))),
inference(superposition,[],[f735,f984]) ).
fof(f1007,plain,
! [X0] : complement(zero) = join(complement(zero),X0),
inference(forward_demodulation,[],[f1006,f711]) ).
fof(f1011,plain,
! [X0] : zero = complement(join(top,X0)),
inference(forward_demodulation,[],[f1000,f739]) ).
fof(f1014,plain,
! [X0] : top = join(top,X0),
inference(forward_demodulation,[],[f1007,f739]) ).
fof(f1033,plain,
top = converse(top),
inference(superposition,[],[f482,f1014]) ).
fof(f1071,plain,
complement(sF3) = join(complement(sF3),complement(sF6)),
inference(superposition,[],[f745,f50]) ).
fof(f1105,plain,
sK0 = join(sK0,complement(sF6)),
inference(forward_demodulation,[],[f1071,f716]) ).
fof(f1211,plain,
! [X0,X1] : join(complement(X0),X1) = join(X1,complement(join(X0,X1))),
inference(superposition,[],[f964,f21]) ).
fof(f1219,plain,
! [X0] : join(X0,complement(converse(top))) = join(complement(converse(complement(converse(X0)))),X0),
inference(superposition,[],[f964,f482]) ).
fof(f1226,plain,
! [X0,X1] : join(complement(complement(join(X0,X1))),complement(join(complement(X1),X0))) = join(complement(join(complement(X1),X0)),complement(complement(X0))),
inference(superposition,[],[f964,f726]) ).
fof(f1293,plain,
! [X0,X1] : join(complement(complement(join(X0,X1))),complement(join(complement(X1),X0))) = join(complement(join(complement(X1),X0)),X0),
inference(forward_demodulation,[],[f1226,f711]) ).
fof(f1300,plain,
! [X0] : join(complement(converse(complement(converse(X0)))),X0) = X0,
inference(forward_demodulation,[],[f1219,f515]) ).
fof(f1317,plain,
! [X0,X1] : join(join(X0,X1),complement(join(complement(X1),X0))) = join(complement(join(complement(X1),X0)),X0),
inference(forward_demodulation,[],[f1293,f711]) ).
fof(f1331,plain,
! [X0,X1] : join(X0,join(X1,complement(join(complement(X1),X0)))) = join(complement(join(complement(X1),X0)),X0),
inference(forward_demodulation,[],[f1317,f22]) ).
fof(f1339,plain,
! [X0,X1] : join(X0,X1) = join(complement(join(complement(X1),X0)),X0),
inference(forward_demodulation,[],[f1331,f328]) ).
fof(f2274,plain,
join(complement(sF5),sF3) = join(sF3,complement(sF6)),
inference(superposition,[],[f1211,f50]) ).
fof(f2452,plain,
! [X2,X0,X1] : composition(join(converse(X2),converse(X1)),converse(X0)) = join(converse(composition(X0,X2)),converse(composition(X0,X1))),
inference(superposition,[],[f107,f30]) ).
fof(f2477,plain,
! [X2,X0,X1] : composition(join(converse(X2),converse(X1)),converse(X0)) = converse(join(composition(X0,X2),composition(X0,X1))),
inference(forward_demodulation,[],[f2452,f29]) ).
fof(f2496,plain,
! [X2,X0,X1] : converse(join(composition(X0,X2),composition(X0,X1))) = composition(converse(join(X2,X1)),converse(X0)),
inference(forward_demodulation,[],[f2477,f29]) ).
fof(f2504,plain,
! [X2,X0,X1] : converse(join(composition(X0,X2),composition(X0,X1))) = converse(composition(X0,join(X2,X1))),
inference(forward_demodulation,[],[f2496,f30]) ).
fof(f2529,plain,
! [X2,X0,X1] : join(composition(X0,X1),composition(X0,X2)) = converse(converse(composition(X0,join(X1,X2)))),
inference(superposition,[],[f28,f2504]) ).
fof(f2547,plain,
! [X2,X0,X1] : composition(X0,join(X1,X2)) = join(composition(X0,X1),composition(X0,X2)),
inference(forward_demodulation,[],[f2529,f28]) ).
fof(f2779,plain,
! [X0,X1] : join(complement(join(complement(X1),X0)),X1) = join(X1,complement(join(top,X0))),
inference(superposition,[],[f964,f201]) ).
fof(f2808,plain,
! [X0,X1] : join(X1,zero) = join(complement(join(complement(X1),X0)),X1),
inference(forward_demodulation,[],[f2779,f1011]) ).
fof(f2862,plain,
! [X0,X1] : join(complement(join(complement(X1),X0)),X1) = X1,
inference(forward_demodulation,[],[f2808,f651]) ).
fof(f2906,plain,
! [X0,X1] : complement(X0) = join(complement(join(X0,X1)),complement(X0)),
inference(superposition,[],[f2862,f711]) ).
fof(f3081,plain,
complement(sF8) = join(complement(sK2),complement(sF8)),
inference(superposition,[],[f2906,f59]) ).
fof(f3146,plain,
complement(sF8) = join(sF4,complement(sF8)),
inference(forward_demodulation,[],[f3081,f46]) ).
fof(f3429,plain,
join(complement(sF4),complement(sF8)) = join(complement(sF8),complement(complement(sF8))),
inference(superposition,[],[f1211,f3146]) ).
fof(f3432,plain,
top = join(complement(sF4),complement(sF8)),
inference(forward_demodulation,[],[f3429,f32]) ).
fof(f3443,plain,
top = join(sK2,complement(sF8)),
inference(forward_demodulation,[],[f3432,f717]) ).
fof(f5047,plain,
! [X0,X1] : composition(converse(X0),join(X1,complement(composition(X0,top)))) = join(composition(converse(X0),X1),zero),
inference(superposition,[],[f2547,f709]) ).
fof(f5050,plain,
! [X0,X1] : composition(converse(X0),X1) = composition(converse(X0),join(X1,complement(composition(X0,top)))),
inference(forward_demodulation,[],[f5047,f651]) ).
fof(f5862,plain,
sF6 = join(sF6,complement(sK0)),
inference(superposition,[],[f342,f1105]) ).
fof(f5885,plain,
sF6 = join(sF6,sF3),
inference(forward_demodulation,[],[f5862,f44]) ).
fof(f6233,plain,
! [X0] : join(converse(complement(converse(complement(X0)))),X0) = join(complement(converse(top)),converse(complement(converse(complement(X0))))),
inference(superposition,[],[f1339,f482]) ).
fof(f6351,plain,
! [X0] : join(converse(complement(converse(complement(X0)))),X0) = join(complement(top),converse(complement(converse(complement(X0))))),
inference(forward_demodulation,[],[f6233,f1033]) ).
fof(f6435,plain,
! [X0] : join(converse(complement(converse(complement(X0)))),X0) = join(zero,converse(complement(converse(complement(X0))))),
inference(forward_demodulation,[],[f6351,f645]) ).
fof(f6481,plain,
! [X0] : converse(complement(converse(complement(X0)))) = join(converse(complement(converse(complement(X0)))),X0),
inference(forward_demodulation,[],[f6435,f991]) ).
fof(f10342,plain,
! [X0] : converse(converse(X0)) = join(converse(complement(converse(complement(converse(converse(X0)))))),X0),
inference(superposition,[],[f69,f1300]) ).
fof(f10345,plain,
! [X0] : join(converse(complement(converse(complement(X0)))),X0) = X0,
inference(forward_demodulation,[],[f10342,f28]) ).
fof(f10379,plain,
! [X0] : converse(complement(converse(complement(X0)))) = X0,
inference(forward_demodulation,[],[f10345,f6481]) ).
fof(f10570,plain,
zero = converse(complement(converse(top))),
inference(superposition,[],[f10379,f739]) ).
fof(f10597,plain,
zero = converse(complement(top)),
inference(forward_demodulation,[],[f10570,f1033]) ).
fof(f10601,plain,
zero = converse(zero),
inference(forward_demodulation,[],[f10597,f645]) ).
fof(f10923,plain,
! [X0] : composition(complement(join(complement(sF4),complement(composition(X0,converse(sK1))))),complement(join(complement(sK1),complement(composition(converse(sF4),X0))))) = join(complement(join(complement(sF5),complement(X0))),composition(complement(join(complement(sF4),complement(composition(X0,converse(sK1))))),complement(join(complement(sK1),complement(composition(converse(sF4),X0)))))),
inference(superposition,[],[f40,f48]) ).
fof(f11156,plain,
! [X0] : composition(complement(join(complement(sF4),complement(composition(X0,sF7)))),complement(join(complement(sK1),complement(composition(converse(sF4),X0))))) = join(complement(join(complement(sF5),complement(X0))),composition(complement(join(complement(sF4),complement(composition(X0,sF7)))),complement(join(complement(sK1),complement(composition(converse(sF4),X0)))))),
inference(forward_demodulation,[],[f10923,f53]) ).
fof(f11227,plain,
! [X0] : composition(complement(join(sK2,complement(composition(X0,sF7)))),complement(join(complement(sK1),complement(composition(converse(sF4),X0))))) = join(complement(join(complement(sF5),complement(X0))),composition(complement(join(sK2,complement(composition(X0,sF7)))),complement(join(complement(sK1),complement(composition(converse(sF4),X0)))))),
inference(forward_demodulation,[],[f11156,f717]) ).
fof(f16458,plain,
! [X0] : composition(converse(X0),complement(composition(X0,top))) = composition(converse(X0),zero),
inference(superposition,[],[f5050,f991]) ).
fof(f16495,plain,
! [X0] : zero = composition(converse(X0),zero),
inference(forward_demodulation,[],[f16458,f709]) ).
fof(f19411,plain,
composition(complement(join(sK2,complement(sF8))),complement(join(complement(sK1),complement(composition(converse(sF4),sK0))))) = join(complement(join(complement(sF5),complement(sK0))),composition(complement(join(sK2,complement(sF8))),complement(join(complement(sK1),complement(composition(converse(sF4),sK0)))))),
inference(superposition,[],[f11227,f55]) ).
fof(f19488,plain,
composition(complement(top),complement(join(complement(sK1),complement(composition(converse(sF4),sK0))))) = join(complement(join(complement(sF5),complement(sK0))),composition(complement(top),complement(join(complement(sK1),complement(composition(converse(sF4),sK0)))))),
inference(forward_demodulation,[],[f19411,f3443]) ).
fof(f19527,plain,
composition(zero,complement(join(complement(sK1),complement(composition(converse(sF4),sK0))))) = join(complement(join(complement(sF5),complement(sK0))),composition(zero,complement(join(complement(sK1),complement(composition(converse(sF4),sK0)))))),
inference(forward_demodulation,[],[f19488,f645]) ).
fof(f19549,plain,
composition(zero,complement(join(complement(sK1),complement(composition(converse(sF4),sK0))))) = join(complement(join(complement(sF5),sF3)),composition(zero,complement(join(complement(sK1),complement(composition(converse(sF4),sK0)))))),
inference(forward_demodulation,[],[f19527,f44]) ).
fof(f19563,plain,
composition(zero,complement(join(complement(sK1),complement(composition(converse(sF4),sK0))))) = join(complement(join(sF3,complement(sF6))),composition(zero,complement(join(complement(sK1),complement(composition(converse(sF4),sK0)))))),
inference(forward_demodulation,[],[f19549,f2274]) ).
fof(f25669,plain,
! [X0] : converse(zero) = composition(converse(zero),X0),
inference(superposition,[],[f73,f16495]) ).
fof(f25701,plain,
! [X0] : zero = composition(zero,X0),
inference(forward_demodulation,[],[f25669,f10601]) ).
fof(f25747,plain,
zero = join(complement(join(sF3,complement(sF6))),zero),
inference(superposition,[],[f19563,f25701]) ).
fof(f25810,plain,
zero = complement(join(sF3,complement(sF6))),
inference(forward_demodulation,[],[f25747,f651]) ).
fof(f25880,plain,
join(zero,sF3) = join(complement(complement(sF6)),sF3),
inference(superposition,[],[f965,f25810]) ).
fof(f26051,plain,
join(zero,sF3) = join(sF6,sF3),
inference(forward_demodulation,[],[f25880,f711]) ).
fof(f26128,plain,
sF6 = join(zero,sF3),
inference(forward_demodulation,[],[f26051,f5885]) ).
fof(f26174,plain,
sF3 = sF6,
inference(forward_demodulation,[],[f26128,f992]) ).
fof(f26199,plain,
$false,
inference(forward_subsumption_resolution,[],[f26174,f51]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : REL043+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.39 % Computer : n026.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sun Sep 27 22:59:27 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.15/0.44 Running first-order theorem proving
% 0.15/0.44 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
% 12.96/2.92 % (3305202)Detected formulas, will run a generic FOF schedule.
% 12.96/2.92 % (3305225)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=187567915:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 12.96/2.92 % (3305226)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=4052171843:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 12.96/2.92 % (3305227)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=562267325:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 12.96/2.92 % (3305228)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=657642237:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 12.96/2.92 % (3305229)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=874283110:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 12.96/2.92 % (3305224)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=4003822050:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 12.96/2.92 % (3305230)dis-21_1_sil=8000:lcm=predicate:random_seed=534996886: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)
% 12.96/2.92 % (3305230)Refutation not found, incomplete strategy
% 12.96/2.92 % (3305230)------------------------------
% 12.96/2.92 % (3305230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.96/2.92 % (3305230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.96/2.92 % (3305230)CaDiCaL version: 2.1.3
% 12.96/2.92 % (3305230)Termination reason: Refutation not found, incomplete strategy
% 12.96/2.92 % (3305230)Time elapsed: 0.003 s
% 12.96/2.92 % (3305230)Peak memory usage: 88 MB
% 12.96/2.92 % (3305230)Instructions burned: 1 (million)
% 12.96/2.92 % (3305227)Instruction limit reached!
% 12.96/2.92 % (3305227)------------------------------
% 12.96/2.92 % (3305227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.96/2.92 % (3305227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.96/2.92 % (3305227)CaDiCaL version: 2.1.3
% 12.96/2.92 % (3305227)Termination reason: Instruction limit
% 12.96/2.92 % (3305227)Termination phase: Saturation
% 12.96/2.92 % (3305227)Time elapsed: 0.085 s
% 12.96/2.92 % (3305227)Peak memory usage: 89 MB
% 12.96/2.92 % (3305227)Instructions burned: 109 (million)
% 12.96/2.92 % (3305228)Instruction limit reached!
% 12.96/2.92 % (3305228)------------------------------
% 12.96/2.92 % (3305228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.96/2.92 % (3305228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.96/2.92 % (3305228)CaDiCaL version: 2.1.3
% 12.96/2.92 % (3305228)Termination reason: Instruction limit
% 12.96/2.92 % (3305228)Termination phase: Saturation
% 12.96/2.92 % (3305228)Time elapsed: 0.109 s
% 12.96/2.92 % (3305228)Peak memory usage: 89 MB
% 12.96/2.92 % (3305228)Instructions burned: 120 (million)
% 12.96/2.92 % (3305229)Instruction limit reached!
% 12.96/2.92 % (3305229)------------------------------
% 12.96/2.92 % (3305229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.96/2.92 % (3305229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.96/2.92 % (3305229)CaDiCaL version: 2.1.3
% 12.96/2.92 % (3305229)Termination reason: Instruction limit
% 12.96/2.92 % (3305229)Termination phase: Saturation
% 12.96/2.92 % (3305229)Time elapsed: 0.136 s
% 12.96/2.92 % (3305229)Peak memory usage: 89 MB
% 12.96/2.92 % (3305229)Instructions burned: 141 (million)
% 12.96/2.92 % (3305242)lrs+10_1_sil=8000:sp=occurrence:random_seed=2063893107:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 12.96/2.92 % (3305243)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3765233182:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 12.96/2.92 % (3305244)lrs+1011_1_sil=32000:sp=occurrence:random_seed=807754618:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 12.96/2.92 % (3305230)------------------------------
% 12.96/2.92 % (3305230)------------------------------
% 12.96/2.92 % (3305243)Instruction limit reached!
% 12.96/2.92 % (3305243)------------------------------
% 12.96/2.92 % (3305243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.80/3.57 % (3305243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.80/3.57 % (3305243)CaDiCaL version: 2.1.3
% 17.80/3.57 % (3305243)Termination reason: Instruction limit
% 17.80/3.57 % (3305243)Termination phase: Saturation
% 17.80/3.57 % (3305243)Time elapsed: 0.159 s
% 17.80/3.57 % (3305243)Peak memory usage: 90 MB
% 17.80/3.57 % (3305243)Instructions burned: 157 (million)
% 17.80/3.57 % (3305251)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=3834832851:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi)
% 17.80/3.57 % (3305242)Instruction limit reached!
% 17.80/3.57 % (3305242)------------------------------
% 17.80/3.57 % (3305242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.80/3.57 % (3305242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.80/3.57 % (3305242)CaDiCaL version: 2.1.3
% 17.80/3.57 % (3305242)Termination reason: Instruction limit
% 17.80/3.57 % (3305242)Termination phase: Saturation
% 17.80/3.57 % (3305242)Time elapsed: 0.286 s
% 17.80/3.57 % (3305242)Peak memory usage: 91 MB
% 17.80/3.57 % (3305242)Instructions burned: 286 (million)
% 17.80/3.57 % (3305244)Instruction limit reached!
% 17.80/3.57 % (3305244)------------------------------
% 17.80/3.57 % (3305244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.80/3.57 % (3305244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.80/3.57 % (3305244)CaDiCaL version: 2.1.3
% 17.80/3.57 % (3305244)Termination reason: Instruction limit
% 17.80/3.57 % (3305244)Termination phase: Saturation
% 17.80/3.57 % (3305244)Time elapsed: 0.321 s
% 17.80/3.57 % (3305244)Peak memory usage: 91 MB
% 17.80/3.57 % (3305244)Instructions burned: 328 (million)
% 17.80/3.57 % (3305252)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=546602008:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 17.80/3.57 % (3305251)Instruction limit reached!
% 17.80/3.57 % (3305251)------------------------------
% 17.80/3.57 % (3305251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.80/3.57 % (3305251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.80/3.57 % (3305251)CaDiCaL version: 2.1.3
% 17.80/3.57 % (3305251)Termination reason: Instruction limit
% 17.80/3.57 % (3305251)Termination phase: Saturation
% 17.80/3.57 % (3305251)Time elapsed: 0.113 s
% 17.80/3.57 % (3305251)Peak memory usage: 92 MB
% 17.80/3.57 % (3305251)Instructions burned: 251 (million)
% 17.80/3.57 % (3305255)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2144424455:i=2350_2991 on theBenchmark for (2991ds/2350Mi)
% 17.80/3.57 % (3305258)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2972238955:i=127:av=off:fsr=off:sup=off_2990 on theBenchmark for (2990ds/127Mi)
% 17.80/3.57 % (3305258)Refutation not found, incomplete strategy
% 17.80/3.57 % (3305258)------------------------------
% 17.80/3.57 % (3305258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.80/3.57 % (3305258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.80/3.57 % (3305258)CaDiCaL version: 2.1.3
% 17.80/3.57 % (3305258)Termination reason: Refutation not found, incomplete strategy
% 17.80/3.57 % (3305258)Time elapsed: 0.001 s
% 17.80/3.57 % (3305258)Peak memory usage: 87 MB
% 17.80/3.57 % (3305258)Instructions burned: 1 (million)
% 17.80/3.57 % (3305256)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=213341005:cts=off:i=113:fsr=off:ss=included:sgt=4_2991 on theBenchmark for (2991ds/113Mi)
% 17.80/3.57 % (3305252)Instruction limit reached!
% 17.80/3.57 % (3305252)------------------------------
% 17.80/3.57 % (3305252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.80/3.57 % (3305252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.80/3.57 % (3305252)CaDiCaL version: 2.1.3
% 17.80/3.57 % (3305252)Termination reason: Instruction limit
% 17.80/3.57 % (3305252)Termination phase: Saturation
% 17.80/3.57 % (3305252)Time elapsed: 0.164 s
% 17.80/3.57 % (3305252)Peak memory usage: 89 MB
% 17.80/3.57 % (3305252)Instructions burned: 294 (million)
% 17.80/3.57 % (3305256)Instruction limit reached!
% 17.80/3.57 % (3305256)------------------------------
% 17.80/3.57 % (3305256)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.80/3.57 % (3305256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.80/3.57 % (3305256)CaDiCaL version: 2.1.3
% 17.80/3.57 % (3305256)Termination reason: Instruction limit
% 17.80/3.57 % (3305256)Termination phase: Saturation
% 17.80/3.57 % (3305256)Time elapsed: 0.065 s
% 17.80/3.57 % (3305256)Peak memory usage: 89 MB
% 17.80/3.57 % (3305256)Instructions burned: 114 (million)
% 17.80/3.57 % (3305258)------------------------------
% 17.80/3.57 % (3305258)------------------------------
% 17.80/3.57 % (3305262)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2316950443:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2989 on theBenchmark for (2989ds/114Mi)
% 17.80/3.57 % (3305263)lrs+10_1_sil=8000:sp=occurrence:random_seed=2236051302:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2989 on theBenchmark for (2989ds/907Mi)
% 17.80/3.57 % (3305264)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1093287304:i=437:sd=1:aac=none:ss=included_2988 on theBenchmark for (2988ds/437Mi)
% 17.80/3.57 % (3305262)Instruction limit reached!
% 17.80/3.57 % (3305262)------------------------------
% 17.80/3.57 % (3305262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.80/3.57 % (3305262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.80/3.57 % (3305262)CaDiCaL version: 2.1.3
% 17.80/3.57 % (3305262)Termination reason: Instruction limit
% 17.80/3.57 % (3305262)Termination phase: Saturation
% 17.80/3.57 % (3305262)Time elapsed: 0.067 s
% 17.80/3.57 % (3305262)Peak memory usage: 89 MB
% 17.80/3.57 % (3305262)Instructions burned: 115 (million)
% 17.80/3.57 % (3305264)Instruction limit reached!
% 17.80/3.57 % (3305264)------------------------------
% 17.80/3.57 % (3305264)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.80/3.57 % (3305264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.80/3.57 % (3305264)CaDiCaL version: 2.1.3
% 17.80/3.57 % (3305264)Termination reason: Instruction limit
% 17.80/3.57 % (3305264)Termination phase: Saturation
% 17.80/3.57 % (3305264)Time elapsed: 0.117 s
% 17.80/3.57 % (3305264)Peak memory usage: 90 MB
% 17.80/3.57 % (3305264)Instructions burned: 437 (million)
% 17.80/3.57 % (3305270)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2093068784:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2986 on theBenchmark for (2986ds/134Mi)
% 17.80/3.57 % (3305269)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1987613063:i=5202:ss=axioms:sgt=16_2987 on theBenchmark for (2987ds/5202Mi)
% 17.80/3.57 % (3305270)Refutation not found, incomplete strategy
% 17.80/3.57 % (3305270)------------------------------
% 17.80/3.57 % (3305270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.80/3.57 % (3305270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.80/3.57 % (3305270)CaDiCaL version: 2.1.3
% 17.80/3.57 % (3305270)Termination reason: Refutation not found, incomplete strategy
% 17.80/3.57 % (3305270)Time elapsed: 0.001 s
% 17.80/3.57 % (3305270)Peak memory usage: 89 MB
% 17.80/3.57 % (3305270)Instructions burned: 1 (million)
% 17.80/3.57 % (3305270)------------------------------
% 17.80/3.57 % (3305270)------------------------------
% 17.80/3.57 % (3305344)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1787570355:st=8:i=592:sd=3:ep=RST:ss=axioms_2984 on theBenchmark for (2984ds/592Mi)
% 17.80/3.57 % (3305263)Instruction limit reached!
% 17.80/3.57 % (3305263)------------------------------
% 17.80/3.57 % (3305263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.80/3.57 % (3305263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.80/3.57 % (3305263)CaDiCaL version: 2.1.3
% 17.80/3.57 % (3305263)Termination reason: Instruction limit
% 17.80/3.57 % (3305263)Termination phase: Saturation
% 17.80/3.57 % (3305263)Time elapsed: 0.537 s
% 17.80/3.57 % (3305263)Peak memory usage: 98 MB
% 17.80/3.57 % (3305263)Instructions burned: 909 (million)
% 17.80/3.57 % (3305344)Instruction limit reached!
% 17.80/3.57 % (3305344)------------------------------
% 17.80/3.57 % (3305344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.80/3.57 % (3305344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.80/3.57 % (3305344)CaDiCaL version: 2.1.3
% 17.80/3.57 % (3305344)Termination reason: Instruction limit
% 17.80/3.57 % (3305344)Termination phase: Saturation
% 17.80/3.57 % (3305344)Time elapsed: 0.158 s
% 17.80/3.57 % (3305344)Peak memory usage: 91 MB
% 17.80/3.57 % (3305344)Instructions burned: 592 (million)
% 17.80/3.57 % (3305380)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1347645546:st=3:i=13193:sd=3:ss=axioms_2982 on theBenchmark for (2982ds/13193Mi)
% 17.80/3.57 % (3305386)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=4080791107:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2981 on theBenchmark for (2981ds/125Mi)
% 17.80/3.57 % (3305386)Instruction limit reached!
% 17.80/3.57 % (3305386)------------------------------
% 17.80/3.57 % (3305386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.80/3.57 % (3305386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.80/3.57 % (3305386)CaDiCaL version: 2.1.3
% 17.80/3.57 % (3305386)Termination reason: Instruction limit
% 17.80/3.57 % (3305386)Termination phase: Saturation
% 17.80/3.57 % (3305386)Time elapsed: 0.044 s
% 17.80/3.57 % (3305386)Peak memory usage: 91 MB
% 17.80/3.57 % (3305386)Instructions burned: 126 (million)
% 17.80/3.57 % (3305431)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2140121289:i=134:gtgl=5:slsql=off:gtg=exists_sym_2980 on theBenchmark for (2980ds/134Mi)
% 17.80/3.57 % (3305431)Instruction limit reached!
% 17.80/3.57 % (3305431)------------------------------
% 17.80/3.57 % (3305431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.80/3.57 % (3305431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.80/3.57 % (3305431)CaDiCaL version: 2.1.3
% 17.80/3.57 % (3305431)Termination reason: Instruction limit
% 17.80/3.57 % (3305431)Termination phase: Saturation
% 17.80/3.57 % (3305431)Time elapsed: 0.044 s
% 17.80/3.57 % (3305431)Peak memory usage: 90 MB
% 17.80/3.57 % (3305431)Instructions burned: 137 (million)
% 17.80/3.57 % (3305433)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3139372067:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/141Mi)
% 17.80/3.57 % (3305433)Refutation not found, incomplete strategy
% 17.80/3.57 % (3305433)------------------------------
% 17.80/3.57 % (3305433)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.80/3.57 % (3305433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.80/3.57 % (3305433)CaDiCaL version: 2.1.3
% 17.80/3.57 % (3305433)Termination reason: Refutation not found, incomplete strategy
% 17.80/3.57 % (3305433)Time elapsed: 0.001 s
% 17.80/3.57 % (3305433)Peak memory usage: 88 MB
% 17.80/3.57 % (3305433)Instructions burned: 1 (million)
% 17.80/3.57 % (3305224)First to succeed.
% 17.80/3.57 % (3305224)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3305202"
% 17.80/3.57 % (3305433)------------------------------
% 17.80/3.57 % (3305433)------------------------------
% 17.80/3.57 % (3305435)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1163086202:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2976 on theBenchmark for (2976ds/431Mi)
% 17.80/3.57 % (3305435)Refutation not found, incomplete strategy
% 17.80/3.57 % (3305435)------------------------------
% 17.80/3.57 % (3305435)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.80/3.57 % (3305435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.80/3.57 % (3305435)CaDiCaL version: 2.1.3
% 17.80/3.57 % (3305435)Termination reason: Refutation not found, incomplete strategy
% 17.80/3.57 % (3305435)Time elapsed: 0.001 s
% 17.80/3.57 % (3305435)Peak memory usage: 88 MB
% 17.80/3.57 % (3305435)Instructions burned: 1 (million)
% 17.80/3.57 % (3305255)Instruction limit reached!
% 17.80/3.57 % (3305255)------------------------------
% 17.80/3.57 % (3305255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.80/3.57 % (3305255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.80/3.57 % (3305255)CaDiCaL version: 2.1.3
% 17.80/3.57 % (3305255)Termination reason: Instruction limit
% 17.80/3.57 % (3305255)Termination phase: Saturation
% 17.80/3.57 % (3305255)Time elapsed: 1.469 s
% 17.80/3.57 % (3305255)Peak memory usage: 141 MB
% 17.80/3.57 % (3305255)Instructions burned: 2351 (million)
% 17.80/3.57 % (3305224)Refutation found. Thanks to Tanya!
% 17.80/3.57 % SZS status Theorem for theBenchmark
% 17.80/3.57 % SZS output start Proof for theBenchmark
% See solution above
% 18.42/3.66 % (3305224)------------------------------
% 18.42/3.66 % (3305224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.42/3.66 % (3305224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.42/3.66 % (3305224)CaDiCaL version: 2.1.3
% 18.42/3.66 % (3305224)Termination reason: Refutation
% 18.42/3.66 % (3305224)Time elapsed: 2.028 s
% 18.42/3.66 % (3305224)Peak memory usage: 146 MB
% 18.42/3.66 % (3305224)Instructions burned: 2822 (million)
% 18.42/3.66 % (3305224)------------------------------
% 18.42/3.66 % (3305224)------------------------------
% 18.42/3.66 % (3305202)Success in time 2.512 s
% 18.42/3.66 % Vampire exiting
%------------------------------------------------------------------------------