%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : REL005+4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n001.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:13 PM UTC 2026
% Result : Theorem 26.05s 8.86s
% Output : Refutation 26.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 66
% Number of leaves : 17
% Syntax : Number of formulae : 196 ( 173 unt; 2 def)
% Number of atoms : 219 ( 192 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 47 ( 24 ~; 19 |; 2 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 3 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 5 con; 0-2 aty)
% Number of variables : 269 ( 0 sgn 267 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001+0.ax',maddux1_join_commutativity) ).
fof(f2,axiom,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001+0.ax',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/Axioms/REL001+0.ax',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/Axioms/REL001+0.ax',maddux4_definiton_of_meet) ).
fof(f5,axiom,
! [X0,X1,X2] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001+0.ax',composition_associativity) ).
fof(f6,axiom,
! [X0] : composition(X0,one) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/REL001+0.ax',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/Axioms/REL001+0.ax',composition_distributivity) ).
fof(f8,axiom,
! [X0] : converse(converse(X0)) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/REL001+0.ax',converse_idempotence) ).
fof(f9,axiom,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001+0.ax',converse_additivity) ).
fof(f10,axiom,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001+0.ax',converse_multiplicativity) ).
fof(f11,axiom,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001+0.ax',converse_cancellativity) ).
fof(f12,axiom,
! [X0] : top = join(X0,complement(X0)),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001+0.ax',def_top) ).
fof(f13,axiom,
! [X0] : zero = meet(X0,complement(X0)),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001+0.ax',def_zero) ).
fof(f16,axiom,
! [X0,X1,X2] : join(meet(composition(X0,X1),X2),meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2)) = meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001+1.ax',modular_law_2) ).
fof(f17,conjecture,
! [X0,X1] :
( join(converse(meet(X0,X1)),meet(converse(X0),converse(X1))) = meet(converse(X0),converse(X1))
& join(meet(converse(X0),converse(X1)),converse(meet(X0,X1))) = converse(meet(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f18,negated_conjecture,
~ ! [X0,X1] :
( join(converse(meet(X0,X1)),meet(converse(X0),converse(X1))) = meet(converse(X0),converse(X1))
& join(meet(converse(X0),converse(X1)),converse(meet(X0,X1))) = converse(meet(X0,X1)) ),
inference(negated_conjecture,[status(cth)],[f17]) ).
fof(f19,plain,
? [X0,X1] :
( meet(converse(X0),converse(X1)) != join(converse(meet(X0,X1)),meet(converse(X0),converse(X1)))
| converse(meet(X0,X1)) != join(meet(converse(X0),converse(X1)),converse(meet(X0,X1))) ),
inference(ennf_transformation,[],[f18]) ).
fof(f20,plain,
( meet(converse(sK0),converse(sK1)) != join(converse(meet(sK0,sK1)),meet(converse(sK0),converse(sK1)))
| converse(meet(sK0,sK1)) != join(meet(converse(sK0),converse(sK1)),converse(meet(sK0,sK1))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(X1,sK1)],[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(f25,plain,
! [X2,X0,X1] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
inference(cnf_transformation,[],[f5]) ).
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(f36,plain,
! [X2,X0,X1] : meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2) = join(meet(composition(X0,X1),X2),meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2)),
inference(cnf_transformation,[],[f16]) ).
fof(f37,plain,
( meet(converse(sK0),converse(sK1)) != join(converse(meet(sK0,sK1)),meet(converse(sK0),converse(sK1)))
| converse(meet(sK0,sK1)) != join(meet(converse(sK0),converse(sK1)),converse(meet(sK0,sK1))) ),
inference(cnf_transformation,[],[f20]) ).
fof(f38,plain,
! [X0] : zero = complement(join(complement(X0),complement(complement(X0)))),
inference(definition_unfolding,[],[f33,f24]) ).
fof(f41,plain,
! [X2,X0,X1] : complement(join(complement(composition(complement(join(complement(X0),complement(composition(X2,converse(X1))))),X1)),complement(X2))) = join(complement(join(complement(composition(X0,X1)),complement(X2))),complement(join(complement(composition(complement(join(complement(X0),complement(composition(X2,converse(X1))))),X1)),complement(X2)))),
inference(definition_unfolding,[],[f36,f24,f24,f24,f24,f24]) ).
fof(f42,plain,
( complement(join(complement(converse(sK0)),complement(converse(sK1)))) != join(converse(complement(join(complement(sK0),complement(sK1)))),complement(join(complement(converse(sK0)),complement(converse(sK1)))))
| converse(complement(join(complement(sK0),complement(sK1)))) != join(complement(join(complement(converse(sK0)),complement(converse(sK1)))),converse(complement(join(complement(sK0),complement(sK1))))) ),
inference(definition_unfolding,[],[f37,f24,f24,f24,f24,f24,f24]) ).
fof(f44,definition,
( spl2_1
<=> converse(complement(join(complement(sK0),complement(sK1)))) = join(complement(join(complement(converse(sK0)),complement(converse(sK1)))),converse(complement(join(complement(sK0),complement(sK1))))) ),
introduced(definition,[new_symbols(definition,[spl2_1])],[avatar_definition]) ).
fof(f46,plain,
( converse(complement(join(complement(sK0),complement(sK1)))) != join(complement(join(complement(converse(sK0)),complement(converse(sK1)))),converse(complement(join(complement(sK0),complement(sK1)))))
| spl2_1 ),
inference(avatar_component_clause,[],[f44]) ).
fof(f48,definition,
( spl2_2
<=> complement(join(complement(converse(sK0)),complement(converse(sK1)))) = join(converse(complement(join(complement(sK0),complement(sK1)))),complement(join(complement(converse(sK0)),complement(converse(sK1))))) ),
introduced(definition,[new_symbols(definition,[spl2_2])],[avatar_definition]) ).
fof(f50,plain,
( complement(join(complement(converse(sK0)),complement(converse(sK1)))) != join(converse(complement(join(complement(sK0),complement(sK1)))),complement(join(complement(converse(sK0)),complement(converse(sK1)))))
| spl2_2 ),
inference(avatar_component_clause,[],[f48]) ).
fof(f51,plain,
( ~ spl2_1
| ~ spl2_2 ),
inference(avatar_split_clause,[],[f42,f48,f44]) ).
fof(f52,plain,
! [X0,X1] : join(X0,complement(X0)) = join(X1,complement(X1)),
inference(superposition,[],[f32,f32]) ).
fof(f55,plain,
zero = complement(top),
inference(superposition,[],[f38,f32]) ).
fof(f68,plain,
! [X0] : zero = complement(join(X0,complement(X0))),
inference(superposition,[],[f38,f52]) ).
fof(f75,plain,
! [X0] : complement(top) = complement(join(X0,complement(X0))),
inference(superposition,[],[f68,f55]) ).
fof(f105,plain,
! [X0] : top = join(top,complement(join(X0,complement(X0)))),
inference(superposition,[],[f32,f75]) ).
fof(f220,plain,
! [X0] : join(converse(X0),converse(complement(X0))) = converse(top),
inference(superposition,[],[f29,f32]) ).
fof(f234,plain,
! [X0] : converse(top) = join(X0,converse(complement(converse(X0)))),
inference(superposition,[],[f220,f28]) ).
fof(f277,plain,
! [X0] : converse(X0) = composition(converse(one),converse(X0)),
inference(superposition,[],[f30,f26]) ).
fof(f285,plain,
! [X0] : composition(converse(one),X0) = X0,
inference(superposition,[],[f277,f28]) ).
fof(f290,plain,
one = converse(one),
inference(superposition,[],[f285,f26]) ).
fof(f294,plain,
! [X0] : composition(one,X0) = X0,
inference(superposition,[],[f285,f290]) ).
fof(f339,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(top,X1),
inference(superposition,[],[f22,f32]) ).
fof(f340,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X1,join(X0,X2)),
inference(superposition,[],[f22,f21]) ).
fof(f352,plain,
! [X0,X1] : top = join(X0,join(X1,complement(join(X0,X1)))),
inference(superposition,[],[f22,f32]) ).
fof(f353,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X1,join(X2,X0)),
inference(superposition,[],[f22,f21]) ).
fof(f443,plain,
! [X0,X1] : join(top,X0) = join(X1,join(X0,complement(X1))),
inference(superposition,[],[f339,f21]) ).
fof(f450,plain,
! [X0] : join(X0,top) = join(top,complement(complement(X0))),
inference(superposition,[],[f339,f32]) ).
fof(f460,plain,
! [X0,X1] : join(X1,join(complement(X1),X0)) = join(X0,top),
inference(superposition,[],[f339,f21]) ).
fof(f531,plain,
! [X0] : join(top,X0) = join(top,complement(complement(X0))),
inference(superposition,[],[f450,f21]) ).
fof(f541,plain,
! [X0] : join(X0,top) = join(complement(complement(X0)),top),
inference(superposition,[],[f450,f21]) ).
fof(f580,plain,
! [X0] : join(top,X0) = join(complement(complement(X0)),top),
inference(superposition,[],[f531,f21]) ).
fof(f1733,plain,
! [X0,X1] : join(top,X1) = join(complement(X0),join(X0,X1)),
inference(superposition,[],[f340,f32]) ).
fof(f1762,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X1,join(X0,X2)),
inference(superposition,[],[f340,f22]) ).
fof(f1943,plain,
! [X0,X1] : join(top,X0) = join(complement(X1),join(X0,X1)),
inference(superposition,[],[f1733,f21]) ).
fof(f2801,plain,
! [X0,X1] : composition(top,X1) = join(composition(X0,X1),composition(complement(X0),X1)),
inference(superposition,[],[f27,f32]) ).
fof(f3260,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X1,join(X2,X0)),
inference(superposition,[],[f353,f21]) ).
fof(f4598,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(join(X1,X2),X0),
inference(superposition,[],[f3260,f21]) ).
fof(f8664,plain,
! [X0,X1] : complement(X1) = join(complement(X1),composition(converse(X0),complement(composition(X0,X1)))),
inference(forward_demodulation,[],[f31,f21]) ).
fof(f11277,plain,
! [X0,X1] : zero = join(zero,composition(converse(X1),complement(composition(X1,join(complement(X0),complement(complement(X0))))))),
inference(superposition,[],[f8664,f38]) ).
fof(f11298,plain,
! [X0] : complement(X0) = join(complement(X0),complement(composition(one,X0))),
inference(superposition,[],[f8664,f285]) ).
fof(f11301,plain,
! [X2,X0,X1] : join(complement(X0),X2) = join(complement(X0),join(composition(converse(X1),complement(composition(X1,X0))),X2)),
inference(superposition,[],[f22,f8664]) ).
fof(f11351,plain,
! [X0] : complement(X0) = join(complement(X0),complement(X0)),
inference(forward_demodulation,[],[f11298,f294]) ).
fof(f11366,plain,
! [X0,X1] : complement(top) = join(complement(top),composition(converse(X1),complement(composition(X1,join(complement(X0),complement(complement(X0))))))),
inference(forward_demodulation,[],[f11277,f55]) ).
fof(f11397,plain,
! [X0] : join(X0,complement(X0)) = join(complement(X0),top),
inference(superposition,[],[f460,f11351]) ).
fof(f11491,plain,
! [X0] : top = join(complement(X0),join(top,complement(join(X0,complement(X0))))),
inference(superposition,[],[f352,f11397]) ).
fof(f11537,plain,
! [X0] : top = join(complement(X0),top),
inference(forward_demodulation,[],[f11491,f105]) ).
fof(f11596,plain,
! [X0] : top = join(top,X0),
inference(superposition,[],[f11537,f580]) ).
fof(f11597,plain,
! [X0] : top = join(X0,top),
inference(superposition,[],[f11537,f541]) ).
fof(f11728,plain,
top = converse(top),
inference(superposition,[],[f11596,f234]) ).
fof(f12133,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))) = X0,
inference(forward_demodulation,[],[f23,f21]) ).
fof(f13805,plain,
! [X0,X1] : join(complement(X0),X1) = join(complement(join(complement(join(complement(X0),X1)),join(complement(X0),complement(X1)))),complement(X0)),
inference(superposition,[],[f12133,f12133]) ).
fof(f13809,plain,
! [X0] : join(complement(join(complement(X0),complement(X0))),complement(top)) = X0,
inference(superposition,[],[f12133,f32]) ).
fof(f13824,plain,
! [X0,X1] : converse(X0) = join(converse(complement(join(complement(X0),X1))),converse(complement(join(complement(X0),complement(X1))))),
inference(superposition,[],[f29,f12133]) ).
fof(f13879,plain,
! [X0] : join(complement(complement(X0)),complement(top)) = X0,
inference(forward_demodulation,[],[f13809,f11351]) ).
fof(f13883,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,[],[f13805,f21]) ).
fof(f13945,plain,
! [X0,X1] : join(complement(X0),X1) = join(complement(X0),complement(join(complement(X0),join(complement(X1),complement(join(complement(X0),X1)))))),
inference(forward_demodulation,[],[f13883,f353]) ).
fof(f13984,plain,
! [X0] : join(complement(top),complement(complement(X0))) = X0,
inference(superposition,[],[f13879,f21]) ).
fof(f13987,plain,
! [X0] : complement(X0) = join(complement(join(complement(complement(X0)),top)),complement(X0)),
inference(superposition,[],[f12133,f13879]) ).
fof(f14051,plain,
! [X0] : complement(X0) = join(complement(X0),complement(join(complement(complement(X0)),top))),
inference(forward_demodulation,[],[f13987,f21]) ).
fof(f14069,plain,
! [X0] : complement(X0) = join(complement(X0),complement(top)),
inference(forward_demodulation,[],[f14051,f11597]) ).
fof(f14530,plain,
! [X0] : complement(complement(X0)) = X0,
inference(superposition,[],[f14069,f13879]) ).
fof(f14626,plain,
! [X0] : join(X0,complement(top)) = X0,
inference(superposition,[],[f13879,f14530]) ).
fof(f14627,plain,
! [X0] : join(complement(top),X0) = X0,
inference(superposition,[],[f13984,f14530]) ).
fof(f14672,plain,
! [X0] : join(X0,X0) = X0,
inference(superposition,[],[f11351,f14530]) ).
fof(f14750,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X0,X1)),
inference(superposition,[],[f22,f14672]) ).
fof(f14767,plain,
! [X0] : join(complement(X0),X0) = join(top,X0),
inference(superposition,[],[f1943,f14672]) ).
fof(f14856,plain,
! [X0] : join(X0,complement(X0)) = join(top,X0),
inference(forward_demodulation,[],[f14767,f21]) ).
fof(f14879,plain,
! [X0,X1] : join(X1,complement(join(X0,complement(X0)))) = X1,
inference(superposition,[],[f14626,f32]) ).
fof(f15021,plain,
! [X0,X1] : join(complement(join(X0,complement(X0))),X1) = X1,
inference(superposition,[],[f14627,f32]) ).
fof(f15925,plain,
! [X0,X1] : join(X0,complement(X0)) = join(top,X1),
inference(superposition,[],[f14856,f52]) ).
fof(f17485,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),X0) = X0,
inference(superposition,[],[f14750,f12133]) ).
fof(f17668,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),X1))) = X0,
inference(forward_demodulation,[],[f17485,f21]) ).
fof(f19328,plain,
! [X2,X0,X1] : complement(join(complement(X2),complement(composition(complement(join(complement(X0),complement(composition(X2,converse(X1))))),X1)))) = join(complement(join(complement(composition(X0,X1)),complement(X2))),complement(join(complement(X2),complement(composition(complement(join(complement(X0),complement(composition(X2,converse(X1))))),X1))))),
inference(forward_demodulation,[],[f41,f21]) ).
fof(f20185,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X0,X1))),
inference(superposition,[],[f17668,f14530]) ).
fof(f20216,plain,
! [X0,X1] : join(X1,complement(join(X0,complement(X1)))) = X1,
inference(superposition,[],[f17668,f21]) ).
fof(f20289,plain,
! [X0,X1] : join(top,X0) = join(join(complement(X0),X1),X0),
inference(superposition,[],[f443,f17668]) ).
fof(f20363,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(top,X0),
inference(forward_demodulation,[],[f20289,f21]) ).
fof(f21567,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X1,X0))),
inference(superposition,[],[f20216,f14530]) ).
fof(f32025,plain,
! [X2,X0,X1] : join(join(top,X0),X1) = join(join(X1,X0),join(complement(X0),X2)),
inference(superposition,[],[f4598,f20363]) ).
fof(f32212,plain,
! [X2,X0,X1] : join(join(top,X0),X1) = join(complement(X0),join(join(X1,X0),X2)),
inference(forward_demodulation,[],[f32025,f1762]) ).
fof(f32390,plain,
! [X2,X0,X1] : join(join(top,X0),X1) = join(complement(X0),join(X1,join(X0,X2))),
inference(forward_demodulation,[],[f32212,f22]) ).
fof(f32468,plain,
! [X2,X0,X1] : join(top,join(X0,X1)) = join(complement(X0),join(X1,join(X0,X2))),
inference(forward_demodulation,[],[f32390,f22]) ).
fof(f32499,plain,
! [X2,X0,X1] : top = join(complement(X0),join(X1,join(X0,X2))),
inference(forward_demodulation,[],[f32468,f11596]) ).
fof(f35495,plain,
! [X0,X1] : join(top,composition(complement(X1),X0)) = join(complement(composition(X1,X0)),composition(top,X0)),
inference(superposition,[],[f1733,f2801]) ).
fof(f35530,plain,
! [X0,X1] : top = join(complement(composition(X1,X0)),composition(top,X0)),
inference(forward_demodulation,[],[f35495,f11596]) ).
fof(f35766,plain,
! [X0] : top = join(complement(X0),composition(top,X0)),
inference(superposition,[],[f35530,f285]) ).
fof(f35969,plain,
top = composition(top,top),
inference(superposition,[],[f35766,f14627]) ).
fof(f35975,plain,
! [X0] : join(complement(top),complement(join(complement(X0),complement(composition(top,X0))))) = X0,
inference(superposition,[],[f12133,f35766]) ).
fof(f36046,plain,
! [X0] : complement(join(complement(X0),complement(composition(top,X0)))) = X0,
inference(forward_demodulation,[],[f35975,f14627]) ).
fof(f36150,plain,
! [X0] : complement(join(complement(X0),complement(composition(complement(join(complement(top),complement(composition(X0,converse(top))))),top)))) = join(complement(join(complement(top),complement(X0))),complement(join(complement(X0),complement(composition(complement(join(complement(top),complement(composition(X0,converse(top))))),top))))),
inference(superposition,[],[f19328,f35969]) ).
fof(f36152,plain,
! [X0] : complement(join(complement(X0),complement(composition(complement(complement(composition(X0,converse(top)))),top)))) = join(complement(join(complement(top),complement(X0))),complement(join(complement(X0),complement(composition(complement(complement(composition(X0,converse(top)))),top))))),
inference(forward_demodulation,[],[f36150,f14627]) ).
fof(f36169,plain,
! [X0] : complement(join(complement(X0),complement(composition(composition(X0,converse(top)),top)))) = join(complement(join(complement(top),complement(X0))),complement(join(complement(X0),complement(composition(composition(X0,converse(top)),top))))),
inference(forward_demodulation,[],[f36152,f14530]) ).
fof(f36180,plain,
! [X0] : complement(join(complement(X0),complement(composition(X0,composition(converse(top),top))))) = join(complement(join(complement(top),complement(X0))),complement(join(complement(X0),complement(composition(X0,composition(converse(top),top)))))),
inference(forward_demodulation,[],[f36169,f25]) ).
fof(f36185,plain,
! [X0] : complement(join(complement(X0),complement(composition(X0,composition(top,top))))) = join(complement(join(complement(top),complement(X0))),complement(join(complement(X0),complement(composition(X0,composition(top,top)))))),
inference(forward_demodulation,[],[f36180,f11728]) ).
fof(f36188,plain,
! [X0] : complement(join(complement(X0),complement(composition(X0,top)))) = join(complement(join(complement(top),complement(X0))),complement(join(complement(X0),complement(composition(X0,top))))),
inference(forward_demodulation,[],[f36185,f35969]) ).
fof(f36191,plain,
! [X0] : complement(join(complement(X0),complement(composition(X0,top)))) = join(complement(complement(X0)),complement(join(complement(X0),complement(composition(X0,top))))),
inference(forward_demodulation,[],[f36188,f14627]) ).
fof(f36194,plain,
! [X0] : complement(complement(X0)) = complement(join(complement(X0),complement(composition(X0,top)))),
inference(forward_demodulation,[],[f36191,f20185]) ).
fof(f36196,plain,
! [X0] : complement(join(complement(X0),complement(composition(X0,top)))) = X0,
inference(forward_demodulation,[],[f36194,f14530]) ).
fof(f38324,plain,
! [X0] : composition(top,X0) = join(composition(top,X0),X0),
inference(superposition,[],[f20216,f36046]) ).
fof(f38509,plain,
! [X0] : composition(top,X0) = join(X0,composition(top,X0)),
inference(forward_demodulation,[],[f38324,f21]) ).
fof(f38704,plain,
! [X0] : join(X0,complement(X0)) = composition(top,top),
inference(superposition,[],[f38509,f15925]) ).
fof(f38984,plain,
! [X0] : converse(join(X0,complement(X0))) = composition(converse(top),converse(top)),
inference(superposition,[],[f30,f38704]) ).
fof(f38997,plain,
! [X0] : converse(join(X0,complement(X0))) = composition(top,top),
inference(forward_demodulation,[],[f38984,f11728]) ).
fof(f39118,plain,
! [X0] : join(converse(X0),converse(complement(X0))) = composition(top,top),
inference(forward_demodulation,[],[f38997,f29]) ).
fof(f40628,plain,
! [X0] : composition(X0,top) = join(composition(X0,top),X0),
inference(superposition,[],[f20216,f36196]) ).
fof(f40822,plain,
! [X0] : composition(X0,top) = join(X0,composition(X0,top)),
inference(forward_demodulation,[],[f40628,f21]) ).
fof(f56523,plain,
! [X0,X1] : top = join(complement(X0),join(X1,composition(X0,top))),
inference(superposition,[],[f32499,f40822]) ).
fof(f67796,plain,
! [X0,X1] : top = join(complement(top),join(X1,join(converse(X0),converse(complement(X0))))),
inference(superposition,[],[f56523,f39118]) ).
fof(f67816,plain,
! [X0,X1] : top = join(X1,join(converse(X0),converse(complement(X0)))),
inference(forward_demodulation,[],[f67796,f14627]) ).
fof(f76635,plain,
! [X0] : top = join(X0,join(one,converse(complement(one)))),
inference(superposition,[],[f67816,f290]) ).
fof(f77611,plain,
top = join(one,converse(complement(one))),
inference(superposition,[],[f76635,f14627]) ).
fof(f79912,plain,
! [X0,X1] : complement(top) = composition(converse(X1),complement(composition(X1,join(complement(X0),complement(complement(X0)))))),
inference(forward_demodulation,[],[f11366,f14627]) ).
fof(f79913,plain,
! [X0,X1] : complement(top) = composition(converse(X1),complement(composition(X1,join(complement(X0),X0)))),
inference(forward_demodulation,[],[f79912,f14530]) ).
fof(f79914,plain,
! [X0,X1] : complement(top) = composition(converse(X1),complement(composition(X1,join(X0,complement(X0))))),
inference(forward_demodulation,[],[f79913,f21]) ).
fof(f79915,plain,
! [X0,X1] : composition(converse(X1),complement(composition(X1,join(X0,complement(X0))))) = complement(join(one,converse(complement(one)))),
inference(forward_demodulation,[],[f79914,f77611]) ).
fof(f80099,plain,
! [X0,X1] : join(complement(join(X0,complement(X0))),X1) = join(complement(join(X0,complement(X0))),join(complement(join(one,converse(complement(one)))),X1)),
inference(superposition,[],[f11301,f79915]) ).
fof(f80375,plain,
! [X0,X1] : join(complement(join(X0,complement(X0))),X1) = join(complement(join(one,converse(complement(one)))),X1),
inference(forward_demodulation,[],[f80099,f15021]) ).
fof(f80558,plain,
! [X1] : join(complement(join(one,converse(complement(one)))),X1) = X1,
inference(forward_demodulation,[],[f80375,f15021]) ).
fof(f80996,plain,
! [X0] : converse(join(one,converse(complement(one)))) = join(converse(complement(X0)),converse(complement(join(complement(join(one,converse(complement(one)))),complement(X0))))),
inference(superposition,[],[f13824,f80558]) ).
fof(f81408,plain,
! [X0] : join(converse(complement(X0)),converse(complement(complement(X0)))) = converse(join(one,converse(complement(one)))),
inference(forward_demodulation,[],[f80996,f80558]) ).
fof(f81574,plain,
! [X0] : join(converse(complement(X0)),converse(complement(complement(X0)))) = join(converse(one),converse(converse(complement(one)))),
inference(forward_demodulation,[],[f81408,f29]) ).
fof(f81683,plain,
! [X0] : join(converse(complement(X0)),converse(complement(complement(X0)))) = join(converse(one),complement(one)),
inference(forward_demodulation,[],[f81574,f28]) ).
fof(f81760,plain,
! [X0] : join(converse(complement(X0)),converse(complement(complement(X0)))) = join(complement(one),converse(one)),
inference(forward_demodulation,[],[f81683,f21]) ).
fof(f81818,plain,
! [X0] : join(converse(complement(X0)),converse(complement(complement(X0)))) = join(complement(one),one),
inference(forward_demodulation,[],[f81760,f290]) ).
fof(f81852,plain,
! [X0] : join(converse(complement(X0)),converse(complement(complement(X0)))) = join(one,complement(one)),
inference(forward_demodulation,[],[f81818,f21]) ).
fof(f81869,plain,
! [X0] : join(converse(complement(X0)),converse(X0)) = join(one,complement(one)),
inference(forward_demodulation,[],[f81852,f14530]) ).
fof(f81879,plain,
! [X0] : join(converse(X0),converse(complement(X0))) = join(one,complement(one)),
inference(forward_demodulation,[],[f81869,f21]) ).
fof(f87547,plain,
! [X0] : join(X0,converse(complement(converse(X0)))) = join(one,complement(one)),
inference(superposition,[],[f81879,f28]) ).
fof(f87606,plain,
! [X0,X1] : join(X0,complement(X0)) = join(converse(X1),converse(complement(X1))),
inference(superposition,[],[f81879,f52]) ).
fof(f91116,plain,
! [X0,X1] : join(complement(join(complement(X1),complement(X1))),complement(join(converse(X0),converse(complement(X0))))) = X1,
inference(superposition,[],[f12133,f87606]) ).
fof(f91258,plain,
! [X0,X1] : join(complement(complement(X1)),complement(join(converse(X0),converse(complement(X0))))) = X1,
inference(forward_demodulation,[],[f91116,f14672]) ).
fof(f91462,plain,
! [X0,X1] : join(X1,complement(join(converse(X0),converse(complement(X0))))) = X1,
inference(forward_demodulation,[],[f91258,f14530]) ).
fof(f120744,plain,
! [X0,X1] : join(complement(X0),X1) = join(complement(X0),complement(join(complement(X0),complement(X1)))),
inference(forward_demodulation,[],[f13945,f21567]) ).
fof(f121154,plain,
! [X0,X1] : join(X0,X1) = join(X0,complement(join(X0,complement(X1)))),
inference(superposition,[],[f120744,f14530]) ).
fof(f121822,plain,
! [X0,X1] : join(X1,complement(X0)) = join(X1,complement(join(X1,X0))),
inference(superposition,[],[f121154,f14530]) ).
fof(f122685,plain,
! [X0] : join(X0,complement(join(one,complement(one)))) = join(X0,complement(converse(complement(converse(X0))))),
inference(superposition,[],[f121822,f87547]) ).
fof(f122849,plain,
! [X0] : converse(X0) = join(converse(X0),complement(converse(complement(X0)))),
inference(superposition,[],[f121822,f91462]) ).
fof(f123254,plain,
! [X0] : join(X0,complement(converse(complement(converse(X0))))) = X0,
inference(forward_demodulation,[],[f122685,f14879]) ).
fof(f124188,plain,
! [X0] : converse(converse(X0)) = join(converse(converse(X0)),converse(complement(converse(complement(X0))))),
inference(superposition,[],[f29,f122849]) ).
fof(f124243,plain,
! [X0] : join(X0,converse(complement(converse(complement(X0))))) = X0,
inference(forward_demodulation,[],[f124188,f28]) ).
fof(f124648,plain,
! [X0] : complement(converse(complement(converse(complement(X0))))) = join(complement(converse(complement(converse(complement(X0))))),complement(X0)),
inference(superposition,[],[f21567,f124243]) ).
fof(f124722,plain,
! [X0] : complement(converse(complement(converse(complement(X0))))) = join(complement(X0),complement(converse(complement(converse(complement(X0)))))),
inference(forward_demodulation,[],[f124648,f21]) ).
fof(f124798,plain,
! [X0] : complement(X0) = complement(converse(complement(converse(complement(X0))))),
inference(forward_demodulation,[],[f124722,f123254]) ).
fof(f125036,plain,
! [X0,X1] : join(converse(complement(join(complement(X0),X1))),converse(complement(join(complement(X0),complement(X1))))) = converse(converse(complement(converse(complement(X0))))),
inference(superposition,[],[f13824,f124798]) ).
fof(f125301,plain,
! [X0,X1] : complement(converse(complement(X0))) = join(converse(complement(join(complement(X0),X1))),converse(complement(join(complement(X0),complement(X1))))),
inference(forward_demodulation,[],[f125036,f28]) ).
fof(f125480,plain,
! [X0] : converse(X0) = complement(converse(complement(X0))),
inference(forward_demodulation,[],[f125301,f13824]) ).
fof(f126817,plain,
! [X0] : converse(complement(X0)) = complement(converse(X0)),
inference(superposition,[],[f125480,f14530]) ).
fof(f128412,plain,
( complement(converse(join(complement(sK0),complement(sK1)))) != join(complement(join(complement(converse(sK0)),complement(converse(sK1)))),complement(converse(join(complement(sK0),complement(sK1)))))
| spl2_1 ),
inference(superposition,[],[f46,f126817]) ).
fof(f128639,plain,
( complement(join(converse(complement(sK0)),converse(complement(sK1)))) != join(complement(join(complement(converse(sK0)),complement(converse(sK1)))),complement(join(converse(complement(sK0)),converse(complement(sK1)))))
| spl2_1 ),
inference(forward_demodulation,[],[f128412,f29]) ).
fof(f128757,plain,
( complement(join(converse(complement(sK0)),complement(converse(sK1)))) != join(complement(join(complement(converse(sK0)),complement(converse(sK1)))),complement(join(converse(complement(sK0)),complement(converse(sK1)))))
| spl2_1 ),
inference(forward_demodulation,[],[f128639,f126817]) ).
fof(f128845,plain,
( complement(join(complement(converse(sK0)),complement(converse(sK1)))) != join(complement(join(complement(converse(sK0)),complement(converse(sK1)))),complement(join(complement(converse(sK0)),complement(converse(sK1)))))
| spl2_1 ),
inference(forward_demodulation,[],[f128757,f126817]) ).
fof(f128894,plain,
( $false
| spl2_1 ),
inference(forward_subsumption_resolution,[],[f128845,f11351]) ).
fof(f128895,plain,
spl2_1,
inference(avatar_contradiction_clause,[],[f128894]) ).
fof(f129010,plain,
( complement(join(complement(converse(sK0)),complement(converse(sK1)))) != join(complement(join(complement(converse(sK0)),complement(converse(sK1)))),converse(complement(join(complement(sK0),complement(sK1)))))
| spl2_2 ),
inference(forward_demodulation,[],[f50,f21]) ).
fof(f129012,plain,
( complement(join(complement(converse(sK0)),complement(converse(sK1)))) != join(complement(join(complement(converse(sK0)),complement(converse(sK1)))),complement(converse(join(complement(sK0),complement(sK1)))))
| spl2_2 ),
inference(forward_demodulation,[],[f129010,f126817]) ).
fof(f129014,plain,
( complement(join(complement(converse(sK0)),complement(converse(sK1)))) != join(complement(join(complement(converse(sK0)),complement(converse(sK1)))),complement(join(converse(complement(sK0)),converse(complement(sK1)))))
| spl2_2 ),
inference(forward_demodulation,[],[f129012,f29]) ).
fof(f129016,plain,
( complement(join(complement(converse(sK0)),complement(converse(sK1)))) != join(complement(join(complement(converse(sK0)),complement(converse(sK1)))),complement(join(converse(complement(sK0)),complement(converse(sK1)))))
| spl2_2 ),
inference(forward_demodulation,[],[f129014,f126817]) ).
fof(f129017,plain,
( complement(join(complement(converse(sK0)),complement(converse(sK1)))) != join(complement(join(complement(converse(sK0)),complement(converse(sK1)))),complement(join(complement(converse(sK0)),complement(converse(sK1)))))
| spl2_2 ),
inference(forward_demodulation,[],[f129016,f126817]) ).
fof(f129018,plain,
( $false
| spl2_2 ),
inference(forward_subsumption_resolution,[],[f129017,f11351]) ).
fof(f129019,plain,
spl2_2,
inference(avatar_contradiction_clause,[],[f129018]) ).
cnf(s1,plain,
( ~ spl2_1
| ~ spl2_2 ),
inference(sat_conversion,[],[f51]) ).
cnf(s2,plain,
spl2_1,
inference(sat_conversion,[],[f128895]) ).
cnf(s3,plain,
spl2_2,
inference(sat_conversion,[],[f129019]) ).
cnf(s4,plain,
$false,
inference(rat,[],[s1,s3,s2]) ).
fof(f129020,plain,
$false,
inference(avatar_sat_refutation,[],[s4]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL005+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.37 % Computer : n001.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Sun Sep 27 22:55:48 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.40 Running first-order model finding
% 0.12/0.40 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.04/2.46 % (4055964)Will run a generic schedule for satisfiability detection.
% 14.04/2.46 % (4055975)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3665018370:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.04/2.46 % (4055970)% WARNING: option uhcvi not known.
% 14.04/2.46 % (4055969)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1738960572_2999 on theBenchmark for (2999ds/0Mi)
% 14.04/2.46 % (4055971)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3156434211:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.04/2.46 % (4055972)dis+10_1_sil=32000:sp=arity:random_seed=1103402581:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.04/2.46 % (4055973)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3944672313:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.04/2.46 % (4055974)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=542806659:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.04/2.46 % (4055970)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1757109914:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.04/2.46 % TRYING [1]
% 14.04/2.46 % TRYING [2]
% 14.04/2.46 % TRYING [3]
% 14.04/2.46 % (4055975)Instruction limit reached!
% 14.04/2.46 % (4055975)------------------------------
% 14.04/2.46 % (4055975)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.04/2.46 % (4055975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.04/2.46 % (4055975)CaDiCaL version: 2.1.3
% 14.04/2.46 % (4055975)Termination reason: Instruction limit
% 14.04/2.46 % (4055975)Termination phase: Saturation
% 14.04/2.46 % (4055975)Time elapsed: 0.054 s
% 14.04/2.46 % (4055975)Peak memory usage: 13 MB
% 14.04/2.46 % (4055975)Instructions burned: 161 (million)
% 14.04/2.46 % TRYING [4]
% 14.04/2.46 % (4055983)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=247101931:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 14.04/2.46 % (4055972)Instruction limit reached!
% 14.04/2.46 % (4055972)------------------------------
% 14.04/2.46 % (4055972)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.04/2.46 % (4055972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.04/2.46 % (4055972)CaDiCaL version: 2.1.3
% 14.04/2.46 % (4055972)Termination reason: Instruction limit
% 14.04/2.46 % (4055972)Termination phase: Saturation
% 14.04/2.46 % (4055972)Time elapsed: 0.060 s
% 14.04/2.46 % (4055972)Peak memory usage: 13 MB
% 14.04/2.46 % (4055972)Instructions burned: 104 (million)
% 14.04/2.46 % TRYING [1]
% 14.04/2.46 % TRYING [2]
% 14.04/2.46 % TRYING [3]
% 14.04/2.46 % (4055973)Instruction limit reached!
% 14.04/2.46 % (4055973)------------------------------
% 14.04/2.46 % (4055973)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.04/2.46 % (4055973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.04/2.46 % (4055973)CaDiCaL version: 2.1.3
% 14.04/2.46 % (4055973)Termination reason: Instruction limit
% 14.04/2.46 % (4055973)Termination phase: Saturation
% 14.04/2.46 % (4055973)Time elapsed: 0.070 s
% 14.04/2.46 % (4055973)Peak memory usage: 13 MB
% 14.04/2.46 % (4055973)Instructions burned: 117 (million)
% 14.04/2.46 % (4055974)Instruction limit reached!
% 14.04/2.46 % (4055974)------------------------------
% 14.04/2.46 % (4055974)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.04/2.46 % (4055974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.04/2.46 % (4055974)CaDiCaL version: 2.1.3
% 14.04/2.46 % (4055974)Termination reason: Instruction limit
% 14.04/2.46 % (4055974)Termination phase: Saturation
% 14.04/2.46 % (4055974)Time elapsed: 0.078 s
% 14.04/2.46 % (4055974)Peak memory usage: 13 MB
% 14.04/2.46 % (4055974)Instructions burned: 132 (million)
% 14.04/2.46 % (4055985)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=812867080:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 14.04/2.46 % TRYING [4]
% 14.04/2.46 % (4055986)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2899666978:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 14.04/2.46 % (4055987)ott-21_1_sil=16000:fs=off:random_seed=3258444502:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 14.04/2.46 % (4055985)Instruction limit reached!
% 14.04/2.46 % (4055985)------------------------------
% 14.04/2.46 % (4055985)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.04/2.46 % (4055985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.05/5.59 % (4055985)CaDiCaL version: 2.1.3
% 36.05/5.59 % (4055985)Termination reason: Instruction limit
% 36.05/5.59 % (4055985)Termination phase: Saturation
% 36.05/5.59 % (4055985)Time elapsed: 0.083 s
% 36.05/5.59 % (4055985)Peak memory usage: 13 MB
% 36.05/5.59 % (4055985)Instructions burned: 131 (million)
% 36.05/5.59 % TRYING [5]
% 36.05/5.59 % (4055991)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2317405954:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 36.05/5.59 % (4055987)Instruction limit reached!
% 36.05/5.59 % (4055987)------------------------------
% 36.05/5.59 % (4055987)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.05/5.59 % (4055987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.05/5.59 % (4055987)CaDiCaL version: 2.1.3
% 36.05/5.59 % (4055987)Termination reason: Instruction limit
% 36.05/5.59 % (4055987)Termination phase: Saturation
% 36.05/5.59 % (4055987)Time elapsed: 0.088 s
% 36.05/5.59 % (4055987)Peak memory usage: 12 MB
% 36.05/5.59 % (4055987)Instructions burned: 181 (million)
% 36.05/5.59 % (4055993)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1932985502:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 36.05/5.59 % (4055983)Instruction limit reached!
% 36.05/5.59 % (4055983)------------------------------
% 36.05/5.59 % (4055983)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.05/5.59 % (4055983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.05/5.59 % (4055983)CaDiCaL version: 2.1.3
% 36.05/5.59 % (4055983)Termination reason: Instruction limit
% 36.05/5.59 % (4055983)Termination phase: Finite model building constraint generation
% 36.05/5.59 % (4055983)Time elapsed: 0.157 s
% 36.05/5.59 % (4055983)Peak memory usage: 28 MB
% 36.05/5.59 % (4055983)Instructions burned: 714 (million)
% 36.05/5.59 % TRYING [1]
% 36.05/5.59 % TRYING [2]
% 36.05/5.59 % TRYING [5]
% 36.05/5.59 % (4055995)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3459985046:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 36.05/5.59 % TRYING [3]
% 36.05/5.59 % TRYING [4]
% 36.05/5.59 % (4055986)Instruction limit reached!
% 36.05/5.59 % (4055986)------------------------------
% 36.05/5.59 % (4055986)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.05/5.59 % (4055986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.05/5.59 % (4055986)CaDiCaL version: 2.1.3
% 36.05/5.59 % (4055986)Termination reason: Instruction limit
% 36.05/5.59 % (4055986)Termination phase: Saturation
% 36.05/5.59 % (4055986)Time elapsed: 0.342 s
% 36.05/5.59 % (4055986)Peak memory usage: 18 MB
% 36.05/5.59 % (4055986)Instructions burned: 685 (million)
% 36.05/5.59 % (4055991)Instruction limit reached!
% 36.05/5.59 % (4055991)------------------------------
% 36.05/5.59 % (4055991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.05/5.59 % (4055991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.05/5.59 % (4055991)CaDiCaL version: 2.1.3
% 36.05/5.59 % (4055991)Termination reason: Instruction limit
% 36.05/5.59 % (4055991)Termination phase: Saturation
% 36.05/5.59 % (4055991)Time elapsed: 0.256 s
% 36.05/5.59 % (4055991)Peak memory usage: 16 MB
% 36.05/5.59 % (4055991)Instructions burned: 477 (million)
% 36.05/5.59 % (4055997)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1959439576:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 36.05/5.59 % (4055998)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2440073397:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 36.05/5.59 % (4055993)Instruction limit reached!
% 36.05/5.59 % (4055993)------------------------------
% 36.05/5.59 % (4055993)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.05/5.59 % (4055993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.05/5.59 % (4055993)CaDiCaL version: 2.1.3
% 36.05/5.59 % (4055993)Termination reason: Instruction limit
% 36.05/5.59 % (4055993)Termination phase: Finite model building SAT solving
% 36.05/5.59 % (4055993)Time elapsed: 0.301 s
% 36.05/5.59 % (4055993)Peak memory usage: 24 MB
% 36.05/5.59 % (4055993)Instructions burned: 866 (million)
% 36.05/5.59 % (4056001)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1022775587:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 36.05/5.59 % (4055995)Instruction limit reached!
% 36.05/5.59 % (4055995)------------------------------
% 26.05/8.86 % (4055995)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.05/8.86 % (4055995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.05/8.86 % (4055995)CaDiCaL version: 2.1.3
% 26.05/8.86 % (4055995)Termination reason: Instruction limit
% 26.05/8.86 % (4055995)Termination phase: Saturation
% 26.05/8.86 % (4055995)Time elapsed: 0.344 s
% 26.05/8.86 % (4055995)Peak memory usage: 24 MB
% 26.05/8.86 % (4055995)Instructions burned: 1180 (million)
% 26.05/8.86 % (4056003)fmb+10_1_sil=64000:random_seed=3370979769:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 26.05/8.86 % TRYING [1]
% 26.05/8.86 % TRYING [2]
% 26.05/8.86 % TRYING [3]
% 26.05/8.86 % TRYING [4]
% 26.05/8.86 % TRYING [5]
% 26.05/8.86 % (4055998)Instruction limit reached!
% 26.05/8.86 % (4055998)------------------------------
% 26.05/8.86 % (4055998)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.05/8.86 % (4055998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.05/8.86 % (4055998)CaDiCaL version: 2.1.3
% 26.05/8.86 % (4055998)Termination reason: Instruction limit
% 26.05/8.86 % (4055998)Termination phase: Saturation
% 26.05/8.86 % (4055998)Time elapsed: 0.384 s
% 26.05/8.86 % (4055998)Peak memory usage: 18 MB
% 26.05/8.86 % (4055998)Instructions burned: 693 (million)
% 26.05/8.86 % (4056005)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3600869550:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 26.05/8.86 % (4055997)Instruction limit reached!
% 26.05/8.86 % (4055997)------------------------------
% 26.05/8.86 % (4055997)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.05/8.86 % (4055997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.05/8.86 % (4055997)CaDiCaL version: 2.1.3
% 26.05/8.86 % (4055997)Termination reason: Instruction limit
% 26.05/8.86 % (4055997)Termination phase: Finite model building constraint generation
% 26.05/8.86 % (4055997)Time elapsed: 0.414 s
% 26.05/8.86 % (4055997)Peak memory usage: 107 MB
% 26.05/8.86 % (4055997)Instructions burned: 889 (million)
% 26.05/8.86 % TRYING [20]
% 26.05/8.86 % (4056007)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1127746610:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 26.05/8.86 % TRYING [8]
% 26.05/8.86 % TRYING [6]
% 26.05/8.86 % (4056001)Instruction limit reached!
% 26.05/8.86 % (4056001)------------------------------
% 26.05/8.86 % (4056001)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.05/8.86 % (4056001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.05/8.86 % (4056001)CaDiCaL version: 2.1.3
% 26.05/8.86 % (4056001)Termination reason: Instruction limit
% 26.05/8.86 % (4056001)Termination phase: Saturation
% 26.05/8.86 % (4056001)Time elapsed: 0.461 s
% 26.05/8.86 % (4056001)Peak memory usage: 18 MB
% 26.05/8.86 % (4056001)Instructions burned: 879 (million)
% 26.05/8.86 % (4056009)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4098721869:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 26.05/8.86 % (4056007)Instruction limit reached!
% 26.05/8.86 % (4056007)------------------------------
% 26.05/8.86 % (4056007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.05/8.86 % (4056007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.05/8.86 % (4056007)CaDiCaL version: 2.1.3
% 26.05/8.86 % (4056007)Termination reason: Instruction limit
% 26.05/8.86 % (4056007)Termination phase: Finite model building constraint generation
% 26.05/8.86 % (4056007)Time elapsed: 0.320 s
% 26.05/8.86 % (4056007)Peak memory usage: 75 MB
% 26.05/8.86 % (4056007)Instructions burned: 921 (million)
% 26.05/8.86 % (4056011)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=998975603:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 26.05/8.86 % TRYING [6]
% 26.05/8.86 % (4056011)Instruction limit reached!
% 26.05/8.86 % (4056011)------------------------------
% 26.05/8.86 % (4056011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.05/8.86 % (4056011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.05/8.86 % (4056011)CaDiCaL version: 2.1.3
% 26.05/8.86 % (4056011)Termination reason: Instruction limit
% 26.05/8.86 % (4056011)Termination phase: Saturation
% 26.05/8.86 % (4056011)Time elapsed: 0.728 s
% 26.05/8.86 % (4056011)Peak memory usage: 27 MB
% 26.05/8.86 % (4056011)Instructions burned: 1472 (million)
% 26.05/8.86 % (4056013)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4060776792:i=6324_2979 on theBenchmark for (2979ds/6324Mi)
% 26.05/8.86 % (4056013)Cannot represent all propositional literals internally
% 26.05/8.86 % (4056013)Refutation not found, incomplete strategy
% 26.05/8.86 % (4056013)------------------------------
% 26.05/8.86 % (4056013)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.05/8.86 % (4056013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.05/8.86 % (4056013)CaDiCaL version: 2.1.3
% 26.05/8.86 % (4056013)Termination reason: Refutation not found, incomplete strategy
% 26.05/8.86 % (4056013)Time elapsed: 0.008 s
% 26.05/8.86 % (4056013)Peak memory usage: 10 MB
% 26.05/8.86 % (4056013)Instructions burned: 15 (million)
% 26.05/8.86 % (4056013)------------------------------
% 26.05/8.86 % (4056013)------------------------------
% 26.05/8.86 % (4056015)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1292988568:fmbsr=2.30978:i=2174_2979 on theBenchmark for (2979ds/2174Mi)
% 26.05/8.86 % TRYING [16]
% 26.05/8.86 % (4056015)Instruction limit reached!
% 26.05/8.86 % (4056015)------------------------------
% 26.05/8.86 % (4056015)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.05/8.86 % (4056015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.05/8.86 % (4056015)CaDiCaL version: 2.1.3
% 26.05/8.86 % (4056015)Termination reason: Instruction limit
% 26.05/8.86 % (4056015)Termination phase: Finite model building constraint generation
% 26.05/8.86 % (4056015)Time elapsed: 0.739 s
% 26.05/8.86 % (4056015)Peak memory usage: 132 MB
% 26.05/8.86 % (4056015)Instructions burned: 2176 (million)
% 26.05/8.86 % (4056017)ott-2_1_sil=16000:newcnf=on:random_seed=3056820961:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2971 on theBenchmark for (2971ds/869Mi)
% 26.05/8.86 % (4056017)Instruction limit reached!
% 26.05/8.86 % (4056017)------------------------------
% 26.05/8.86 % (4056017)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.05/8.86 % (4056017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.05/8.86 % (4056017)CaDiCaL version: 2.1.3
% 26.05/8.86 % (4056017)Termination reason: Instruction limit
% 26.05/8.86 % (4056017)Termination phase: Saturation
% 26.05/8.86 % (4056017)Time elapsed: 0.515 s
% 26.05/8.86 % (4056017)Peak memory usage: 20 MB
% 26.05/8.86 % (4056017)Instructions burned: 870 (million)
% 26.05/8.86 % (4056019)ott+10_1_sil=32000:tgt=ground:random_seed=3582718042:i=5114:av=off_2966 on theBenchmark for (2966ds/5114Mi)
% 26.05/8.86 % TRYING [7]
% 26.05/8.86 % (4056009)Instruction limit reached!
% 26.05/8.86 % (4056009)------------------------------
% 26.05/8.86 % (4056009)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.05/8.86 % (4056009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.05/8.86 % (4056009)CaDiCaL version: 2.1.3
% 26.05/8.86 % (4056009)Termination reason: Instruction limit
% 26.05/8.86 % (4056009)Termination phase: Saturation
% 26.05/8.86 % (4056009)Time elapsed: 2.757 s
% 26.05/8.86 % (4056009)Peak memory usage: 56 MB
% 26.05/8.86 % (4056009)Instructions burned: 5132 (million)
% 26.05/8.86 % (4056021)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1341773767:i=54282_2961 on theBenchmark for (2961ds/54282Mi)
% 26.05/8.86 % TRYING [1]
% 26.05/8.86 % TRYING [2]
% 26.05/8.86 % TRYING [3]
% 26.05/8.86 % TRYING [4]
% 26.05/8.86 % TRYING [7]
% 26.05/8.86 % TRYING [5]
% 26.05/8.86 % (4056005)Instruction limit reached!
% 26.05/8.86 % (4056005)------------------------------
% 26.05/8.86 % (4056005)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.05/8.86 % (4056005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.05/8.86 % (4056005)CaDiCaL version: 2.1.3
% 26.05/8.86 % (4056005)Termination reason: Instruction limit
% 26.05/8.86 % (4056005)Termination phase: Finite model building constraint generation
% 26.05/8.86 % (4056005)Time elapsed: 3.492 s
% 26.05/8.86 % (4056005)Peak memory usage: 675 MB
% 26.05/8.86 % (4056005)Instructions burned: 9516 (million)
% 26.05/8.86 % (4056060)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2520812686:i=3512:aac=none_2954 on theBenchmark for (2954ds/3512Mi)
% 26.05/8.86 % TRYING [6]
% 26.05/8.86 % (4056003)Instruction limit reached!
% 26.05/8.86 % (4056003)------------------------------
% 26.05/8.86 % (4056003)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.05/8.86 % (4056003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.05/8.86 % (4056003)CaDiCaL version: 2.1.3
% 26.05/8.86 % (4056003)Termination reason: Instruction limit
% 26.05/8.86 % (4056003)Termination phase: Finite model building constraint generation
% 26.05/8.86 % (4056003)Time elapsed: 4.556 s
% 26.05/8.86 % (4056003)Peak memory usage: 252 MB
% 26.05/8.86 % (4056003)Instructions burned: 22061 (million)
% 26.05/8.86 % (4056071)dis+21_1_sil=32000:sas=cadical:random_seed=1339155752:i=3773:amm=off_2947 on theBenchmark for (2947ds/3773Mi)
% 26.05/8.86 % (4056071)Instruction limit reached!
% 26.05/8.86 % (4056071)------------------------------
% 26.05/8.86 % (4056071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.05/8.86 % (4056071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.05/8.86 % (4056071)CaDiCaL version: 2.1.3
% 26.05/8.86 % (4056071)Termination reason: Instruction limit
% 26.05/8.86 % (4056071)Termination phase: Saturation
% 26.05/8.86 % (4056071)Time elapsed: 1.111 s
% 26.05/8.86 % (4056071)Peak memory usage: 43 MB
% 26.05/8.86 % (4056071)Instructions burned: 3775 (million)
% 26.05/8.86 % (4056172)ott+11_1_sil=16000:gs=on:random_seed=3167897549:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2936 on theBenchmark for (2936ds/2251Mi)
% 26.05/8.86 % (4056019)Instruction limit reached!
% 26.05/8.86 % (4056019)------------------------------
% 26.05/8.86 % (4056019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.05/8.86 % (4056019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.05/8.86 % (4056019)CaDiCaL version: 2.1.3
% 26.05/8.86 % (4056019)Termination reason: Instruction limit
% 26.05/8.86 % (4056019)Termination phase: Saturation
% 26.05/8.86 % (4056019)Time elapsed: 3.295 s
% 26.05/8.86 % (4056019)Peak memory usage: 66 MB
% 26.05/8.86 % (4056019)Instructions burned: 5114 (million)
% 26.05/8.86 % (4056060)Instruction limit reached!
% 26.05/8.86 % (4056060)------------------------------
% 26.05/8.86 % (4056060)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.05/8.86 % (4056060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.05/8.86 % (4056060)CaDiCaL version: 2.1.3
% 26.05/8.86 % (4056060)Termination reason: Instruction limit
% 26.05/8.86 % (4056060)Termination phase: Saturation
% 26.05/8.86 % (4056060)Time elapsed: 2.091 s
% 26.05/8.86 % (4056060)Peak memory usage: 40 MB
% 26.05/8.86 % (4056060)Instructions burned: 3512 (million)
% 26.05/8.86 % (4056229)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1419333855:fmbsr=1.6:i=67534_2933 on theBenchmark for (2933ds/67534Mi)
% 26.05/8.86 % (4056230)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2220988344:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2933 on theBenchmark for (2933ds/4591Mi)
% 26.05/8.86 % TRYING [7]
% 26.05/8.86 % (4056172)Instruction limit reached!
% 26.05/8.86 % (4056172)------------------------------
% 26.05/8.86 % (4056172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.05/8.86 % (4056172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.05/8.86 % (4056172)CaDiCaL version: 2.1.3
% 26.05/8.86 % (4056172)Termination reason: Instruction limit
% 26.05/8.86 % (4056172)Termination phase: Saturation
% 26.05/8.86 % (4056172)Time elapsed: 0.739 s
% 26.05/8.86 % (4056172)Peak memory usage: 32 MB
% 26.05/8.86 % (4056172)Instructions burned: 2254 (million)
% 26.05/8.86 % (4056233)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=730817238:i=29340_2929 on theBenchmark for (2929ds/29340Mi)
% 26.05/8.86 % TRYING [7]
% 26.05/8.86 % (4056233) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-4055964-4056233"...
% 26.05/8.86 % (4056233)...printing done.
% 26.05/8.86 % (4056233)Refutation found. Thanks to Tanya!
% 26.05/8.86 % SZS status Theorem for theBenchmark
% 26.05/8.86 % SZS output start Proof for theBenchmark
% See solution above
% 26.05/8.87 % (4056233)------------------------------
% 26.05/8.87 % (4056233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.05/8.87 % (4056233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.05/8.87 % (4056233)CaDiCaL version: 2.1.3
% 26.05/8.87 % (4056233)Termination reason: Refutation
% 26.05/8.87 % (4056233)Time elapsed: 1.270 s
% 26.05/8.87 % (4056233)Peak memory usage: 40 MB
% 26.05/8.87 % (4056233)Instructions burned: 4630 (million)
% 26.05/8.87 % (4055964)Success in time 8.455 s
% 26.05/8.87 % Vampire exiting
%------------------------------------------------------------------------------