%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : REL031+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n016.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:34 PM UTC 2026
% Result : Theorem 117.77s 33.26s
% Output : Refutation 117.77s
% Verified :
% SZS Type : Refutation
% Derivation depth : 83
% Number of leaves : 14
% Syntax : Number of formulae : 191 ( 186 unt; 0 def)
% Number of atoms : 201 ( 200 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 16 ( 6 ~; 0 |; 8 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 5 con; 0-2 aty)
% Number of variables : 268 ( 264 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/Axioms/REL001+0.ax',composition_associativity) ).
fof(f6,axiom,
! [X0] : composition(X0,one) = X0,
file('/export/starexec/sandbox/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/sandbox/benchmark/Axioms/REL001+0.ax',composition_distributivity) ).
fof(f8,axiom,
! [X0] : converse(converse(X0)) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',converse_idempotence) ).
fof(f9,axiom,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',converse_additivity) ).
fof(f10,axiom,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
file('/export/starexec/sandbox/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/sandbox/benchmark/Axioms/REL001+0.ax',converse_cancellativity) ).
fof(f12,axiom,
! [X0] : top = join(X0,complement(X0)),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',def_top) ).
fof(f13,axiom,
! [X0] : zero = meet(X0,complement(X0)),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',def_zero) ).
fof(f17,conjecture,
! [X0,X1] :
( ( join(composition(converse(X0),X0),one) = one
& join(composition(converse(X1),X1),one) = one )
=> join(composition(converse(composition(X0,X1)),composition(X0,X1)),one) = one ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f18,negated_conjecture,
~ ! [X0,X1] :
( ( join(composition(converse(X0),X0),one) = one
& join(composition(converse(X1),X1),one) = one )
=> join(composition(converse(composition(X0,X1)),composition(X0,X1)),one) = one ),
inference(negated_conjecture,[status(cth)],[f17]) ).
fof(f19,plain,
? [X0,X1] :
( one != join(composition(converse(composition(X0,X1)),composition(X0,X1)),one)
& join(composition(converse(X0),X0),one) = one
& join(composition(converse(X1),X1),one) = one ),
inference(ennf_transformation,[],[f18]) ).
fof(f20,plain,
? [X0,X1] :
( one != join(composition(converse(composition(X0,X1)),composition(X0,X1)),one)
& join(composition(converse(X0),X0),one) = one
& join(composition(converse(X1),X1),one) = one ),
inference(flattening,[],[f19]) ).
fof(f21,plain,
( one != join(composition(converse(composition(sK0,sK1)),composition(sK0,sK1)),one)
& one = join(composition(converse(sK0),sK0),one)
& one = join(composition(converse(sK1),sK1),one) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(X1,sK1)],[f20]) ).
fof(f22,plain,
! [X0,X1] : join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f23,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
inference(cnf_transformation,[],[f2]) ).
fof(f24,plain,
! [X0,X1] : join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) = X0,
inference(cnf_transformation,[],[f3]) ).
fof(f25,plain,
! [X0,X1] : complement(join(complement(X0),complement(X1))) = meet(X0,X1),
inference(cnf_transformation,[],[f4]) ).
fof(f26,plain,
! [X2,X0,X1] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
inference(cnf_transformation,[],[f5]) ).
fof(f27,plain,
! [X0] : composition(X0,one) = X0,
inference(cnf_transformation,[],[f6]) ).
fof(f28,plain,
! [X2,X0,X1] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
inference(cnf_transformation,[],[f7]) ).
fof(f29,plain,
! [X0] : converse(converse(X0)) = X0,
inference(cnf_transformation,[],[f8]) ).
fof(f30,plain,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
inference(cnf_transformation,[],[f9]) ).
fof(f31,plain,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
inference(cnf_transformation,[],[f10]) ).
fof(f32,plain,
! [X0,X1] : complement(X1) = join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)),
inference(cnf_transformation,[],[f11]) ).
fof(f33,plain,
! [X0] : top = join(X0,complement(X0)),
inference(cnf_transformation,[],[f12]) ).
fof(f34,plain,
! [X0] : zero = meet(X0,complement(X0)),
inference(cnf_transformation,[],[f13]) ).
fof(f38,plain,
one = join(composition(converse(sK1),sK1),one),
inference(cnf_transformation,[],[f21]) ).
fof(f39,plain,
one = join(composition(converse(sK0),sK0),one),
inference(cnf_transformation,[],[f21]) ).
fof(f40,plain,
one != join(composition(converse(composition(sK0,sK1)),composition(sK0,sK1)),one),
inference(cnf_transformation,[],[f21]) ).
fof(f41,plain,
! [X0] : zero = complement(join(complement(X0),complement(complement(X0)))),
inference(definition_unfolding,[],[f34,f25]) ).
fof(f45,plain,
one = join(one,composition(converse(sK1),sK1)),
inference(superposition,[],[f22,f38]) ).
fof(f46,plain,
one = join(one,composition(converse(sK0),sK0)),
inference(superposition,[],[f22,f39]) ).
fof(f49,plain,
one != join(one,composition(converse(composition(sK0,sK1)),composition(sK0,sK1))),
inference(superposition,[],[f40,f22]) ).
fof(f55,plain,
zero = complement(top),
inference(forward_demodulation,[],[f41,f33]) ).
fof(f57,plain,
! [X0,X1] : converse(join(converse(X0),X1)) = join(X0,converse(X1)),
inference(superposition,[],[f30,f29]) ).
fof(f58,plain,
! [X0,X1] : converse(join(X1,converse(X0))) = join(converse(X1),X0),
inference(superposition,[],[f30,f29]) ).
fof(f59,plain,
! [X0,X1] : join(converse(X0),converse(X1)) = converse(join(X1,X0)),
inference(superposition,[],[f30,f22]) ).
fof(f64,plain,
! [X0,X1] : converse(composition(converse(X0),X1)) = composition(converse(X1),X0),
inference(superposition,[],[f31,f29]) ).
fof(f68,plain,
! [X0] : join(X0,converse(complement(converse(X0)))) = converse(top),
inference(superposition,[],[f57,f33]) ).
fof(f69,plain,
! [X0,X1] : join(X1,converse(X0)) = converse(join(X0,converse(X1))),
inference(superposition,[],[f57,f22]) ).
fof(f114,plain,
! [X0,X1] : converse(join(X0,X1)) = converse(join(X1,X0)),
inference(superposition,[],[f59,f30]) ).
fof(f224,plain,
! [X0] : converse(converse(X0)) = composition(converse(one),X0),
inference(superposition,[],[f64,f27]) ).
fof(f240,plain,
! [X0] : composition(converse(one),X0) = X0,
inference(forward_demodulation,[],[f224,f29]) ).
fof(f245,plain,
one = converse(one),
inference(superposition,[],[f240,f27]) ).
fof(f252,plain,
! [X0] : composition(one,X0) = X0,
inference(superposition,[],[f240,f245]) ).
fof(f264,plain,
converse(top) = join(one,converse(complement(one))),
inference(superposition,[],[f68,f245]) ).
fof(f473,plain,
! [X0] : join(one,X0) = join(composition(converse(sK1),sK1),join(one,X0)),
inference(superposition,[],[f23,f38]) ).
fof(f475,plain,
! [X0] : join(one,X0) = join(one,join(composition(converse(sK1),sK1),X0)),
inference(superposition,[],[f23,f45]) ).
fof(f499,plain,
top = join(composition(converse(sK1),sK1),top),
inference(superposition,[],[f473,f33]) ).
fof(f509,plain,
! [X0] : join(one,X0) = join(join(one,X0),composition(converse(sK1),sK1)),
inference(superposition,[],[f22,f473]) ).
fof(f510,plain,
! [X0] : join(one,X0) = join(one,join(X0,composition(converse(sK1),sK1))),
inference(forward_demodulation,[],[f509,f23]) ).
fof(f518,plain,
top = join(top,composition(converse(sK1),sK1)),
inference(forward_demodulation,[],[f499,f22]) ).
fof(f524,plain,
! [X0] : join(top,X0) = join(top,join(composition(converse(sK1),sK1),X0)),
inference(superposition,[],[f23,f518]) ).
fof(f633,plain,
! [X0,X1] : join(join(one,X0),X1) = join(one,join(join(X0,composition(converse(sK1),sK1)),X1)),
inference(superposition,[],[f23,f510]) ).
fof(f634,plain,
! [X0,X1] : join(join(one,X0),X1) = join(one,join(X0,join(composition(converse(sK1),sK1),X1))),
inference(forward_demodulation,[],[f633,f23]) ).
fof(f638,plain,
! [X0,X1] : join(one,join(X0,X1)) = join(one,join(X0,join(composition(converse(sK1),sK1),X1))),
inference(forward_demodulation,[],[f634,f23]) ).
fof(f673,plain,
! [X0] : join(top,X0) = join(top,join(X0,composition(converse(sK1),sK1))),
inference(superposition,[],[f524,f22]) ).
fof(f697,plain,
! [X0,X1] : join(join(top,X0),X1) = join(top,join(join(X0,composition(converse(sK1),sK1)),X1)),
inference(superposition,[],[f23,f673]) ).
fof(f698,plain,
! [X0,X1] : join(join(top,X0),X1) = join(top,join(X0,join(composition(converse(sK1),sK1),X1))),
inference(forward_demodulation,[],[f697,f23]) ).
fof(f701,plain,
! [X0,X1] : join(top,join(X0,X1)) = join(top,join(X0,join(composition(converse(sK1),sK1),X1))),
inference(forward_demodulation,[],[f698,f23]) ).
fof(f1617,plain,
! [X0,X1] : join(one,join(join(composition(converse(sK1),sK1),X0),X1)) = join(one,join(X1,X0)),
inference(superposition,[],[f638,f22]) ).
fof(f1658,plain,
! [X0,X1] : join(one,join(composition(converse(sK1),sK1),join(X0,X1))) = join(one,join(X1,X0)),
inference(forward_demodulation,[],[f1617,f23]) ).
fof(f1664,plain,
! [X0,X1] : join(one,join(X0,X1)) = join(one,join(X1,X0)),
inference(forward_demodulation,[],[f1658,f475]) ).
fof(f1668,plain,
! [X2,X0,X1] : join(one,join(X2,join(X0,X1))) = join(one,join(X0,join(X1,X2))),
inference(superposition,[],[f1664,f23]) ).
fof(f1918,plain,
! [X0,X1] : join(one,join(X0,top)) = join(one,join(X1,join(complement(X1),X0))),
inference(superposition,[],[f1668,f33]) ).
fof(f2535,plain,
! [X0] : join(one,join(X0,top)) = join(one,join(complement(complement(X0)),top)),
inference(superposition,[],[f1918,f33]) ).
fof(f2538,plain,
! [X0] : join(one,join(X0,converse(top))) = join(one,join(converse(complement(converse(complement(X0)))),top)),
inference(superposition,[],[f1918,f68]) ).
fof(f2619,plain,
! [X0] : join(one,join(X0,converse(top))) = join(one,join(top,converse(complement(converse(complement(X0)))))),
inference(forward_demodulation,[],[f2538,f1664]) ).
fof(f2620,plain,
! [X0] : join(one,join(X0,top)) = join(one,join(top,complement(complement(X0)))),
inference(forward_demodulation,[],[f2535,f1664]) ).
fof(f6325,plain,
! [X0,X1] : join(top,join(join(composition(converse(sK1),sK1),X0),X1)) = join(top,join(X1,X0)),
inference(superposition,[],[f701,f22]) ).
fof(f6438,plain,
! [X0,X1] : join(top,join(composition(converse(sK1),sK1),join(X0,X1))) = join(top,join(X1,X0)),
inference(forward_demodulation,[],[f6325,f23]) ).
fof(f6455,plain,
! [X0,X1] : join(top,join(X0,X1)) = join(top,join(X1,X0)),
inference(forward_demodulation,[],[f6438,f524]) ).
fof(f6463,plain,
! [X2,X0,X1] : join(top,join(X2,join(X0,X1))) = join(top,join(X0,join(X1,X2))),
inference(superposition,[],[f6455,f23]) ).
fof(f7385,plain,
! [X0,X1] : join(top,join(X0,top)) = join(top,join(X1,join(complement(X1),X0))),
inference(superposition,[],[f6463,f33]) ).
fof(f7456,plain,
! [X0] : join(top,join(X0,converse(top))) = join(top,join(one,join(converse(complement(one)),X0))),
inference(superposition,[],[f6463,f264]) ).
fof(f16991,plain,
! [X0] : join(one,composition(X0,sK1)) = join(one,composition(join(converse(sK1),X0),sK1)),
inference(superposition,[],[f475,f28]) ).
fof(f17096,plain,
! [X0,X1] : complement(X1) = join(complement(X1),composition(converse(X0),complement(composition(X0,X1)))),
inference(forward_demodulation,[],[f32,f22]) ).
fof(f17098,plain,
! [X0] : join(one,composition(converse(X0),sK1)) = join(one,composition(converse(join(sK1,X0)),sK1)),
inference(superposition,[],[f16991,f30]) ).
fof(f19193,plain,
! [X0,X1] : join(one,join(X0,complement(X0))) = join(one,join(composition(converse(X1),complement(composition(X1,X0))),top)),
inference(superposition,[],[f1918,f17096]) ).
fof(f19233,plain,
! [X0,X1] : join(one,join(X0,complement(X0))) = join(one,join(top,composition(converse(X1),complement(composition(X1,X0))))),
inference(forward_demodulation,[],[f19193,f1664]) ).
fof(f19248,plain,
! [X0,X1] : join(one,top) = join(one,join(top,composition(converse(X1),complement(composition(X1,X0))))),
inference(forward_demodulation,[],[f19233,f33]) ).
fof(f19362,plain,
! [X0] : join(one,top) = join(one,join(top,complement(composition(one,X0)))),
inference(superposition,[],[f19248,f240]) ).
fof(f19393,plain,
! [X0] : join(one,top) = join(one,join(top,complement(X0))),
inference(forward_demodulation,[],[f19362,f252]) ).
fof(f19410,plain,
! [X0] : join(one,top) = join(one,join(X0,top)),
inference(superposition,[],[f19393,f2620]) ).
fof(f19494,plain,
! [X0] : join(one,top) = join(one,join(top,X0)),
inference(superposition,[],[f19410,f22]) ).
fof(f19496,plain,
! [X0,X1] : join(one,top) = join(one,join(X0,join(X1,top))),
inference(superposition,[],[f19410,f23]) ).
fof(f19679,plain,
! [X0] : join(one,top) = join(one,join(X0,converse(top))),
inference(superposition,[],[f19494,f2619]) ).
fof(f19889,plain,
join(top,join(one,top)) = join(top,join(converse(top),converse(top))),
inference(superposition,[],[f7456,f19679]) ).
fof(f19962,plain,
join(top,join(one,top)) = join(top,converse(join(top,top))),
inference(forward_demodulation,[],[f19889,f30]) ).
fof(f20547,plain,
! [X0] : join(top,join(one,top)) = join(top,join(join(X0,top),top)),
inference(superposition,[],[f7385,f19496]) ).
fof(f20592,plain,
! [X0] : join(top,join(one,top)) = join(top,join(top,join(X0,top))),
inference(forward_demodulation,[],[f20547,f6455]) ).
fof(f21457,plain,
converse(join(top,join(one,top))) = join(converse(top),join(top,top)),
inference(superposition,[],[f58,f19962]) ).
fof(f24926,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))) = X0,
inference(forward_demodulation,[],[f24,f22]) ).
fof(f25098,plain,
converse(top) = join(join(top,join(one,top)),converse(complement(join(converse(top),join(top,top))))),
inference(superposition,[],[f68,f21457]) ).
fof(f25105,plain,
converse(top) = join(top,join(join(one,top),converse(complement(join(converse(top),join(top,top)))))),
inference(forward_demodulation,[],[f25098,f23]) ).
fof(f25114,plain,
converse(top) = join(top,join(one,join(top,converse(complement(join(converse(top),join(top,top))))))),
inference(forward_demodulation,[],[f25105,f23]) ).
fof(f25121,plain,
converse(top) = join(top,join(one,top)),
inference(forward_demodulation,[],[f25114,f19494]) ).
fof(f25133,plain,
converse(top) = join(top,converse(top)),
inference(superposition,[],[f20592,f25121]) ).
fof(f25162,plain,
! [X0] : join(converse(top),X0) = join(top,join(join(one,top),X0)),
inference(superposition,[],[f23,f25121]) ).
fof(f25187,plain,
! [X0] : join(converse(top),X0) = join(top,join(one,join(top,X0))),
inference(forward_demodulation,[],[f25162,f23]) ).
fof(f25215,plain,
! [X0] : join(converse(top),X0) = join(top,join(one,top)),
inference(forward_demodulation,[],[f25187,f19494]) ).
fof(f25227,plain,
! [X0] : converse(top) = join(converse(top),X0),
inference(forward_demodulation,[],[f25215,f25121]) ).
fof(f25259,plain,
converse(top) = converse(converse(top)),
inference(superposition,[],[f69,f25133]) ).
fof(f25284,plain,
top = converse(top),
inference(forward_demodulation,[],[f25259,f29]) ).
fof(f25472,plain,
! [X0] : top = join(top,X0),
inference(forward_demodulation,[],[f25227,f25284]) ).
fof(f31755,plain,
! [X0] : join(complement(converse(top)),complement(join(complement(X0),complement(converse(complement(converse(complement(X0)))))))) = X0,
inference(superposition,[],[f24926,f68]) ).
fof(f31758,plain,
! [X0] : join(complement(join(complement(X0),top)),complement(join(complement(X0),zero))) = X0,
inference(superposition,[],[f24926,f55]) ).
fof(f31807,plain,
! [X0] : join(complement(join(complement(X0),top)),complement(join(zero,complement(X0)))) = X0,
inference(forward_demodulation,[],[f31758,f22]) ).
fof(f31809,plain,
! [X0] : join(complement(top),complement(join(complement(X0),complement(converse(complement(converse(complement(X0)))))))) = X0,
inference(forward_demodulation,[],[f31755,f25284]) ).
fof(f31847,plain,
! [X0] : join(complement(join(zero,complement(X0))),complement(join(complement(X0),top))) = X0,
inference(forward_demodulation,[],[f31807,f22]) ).
fof(f31849,plain,
! [X0] : join(zero,complement(join(complement(X0),complement(converse(complement(converse(complement(X0)))))))) = X0,
inference(forward_demodulation,[],[f31809,f55]) ).
fof(f31862,plain,
! [X0] : join(complement(join(zero,complement(X0))),complement(join(top,complement(X0)))) = X0,
inference(forward_demodulation,[],[f31847,f22]) ).
fof(f31872,plain,
! [X0] : join(complement(join(top,complement(X0))),complement(join(zero,complement(X0)))) = X0,
inference(forward_demodulation,[],[f31862,f22]) ).
fof(f31874,plain,
! [X0] : join(complement(top),complement(join(zero,complement(X0)))) = X0,
inference(forward_demodulation,[],[f31872,f25472]) ).
fof(f31875,plain,
! [X0] : join(zero,complement(join(zero,complement(X0)))) = X0,
inference(forward_demodulation,[],[f31874,f55]) ).
fof(f31928,plain,
zero = join(zero,complement(top)),
inference(superposition,[],[f31875,f33]) ).
fof(f31964,plain,
zero = join(zero,zero),
inference(forward_demodulation,[],[f31928,f55]) ).
fof(f31977,plain,
! [X0] : join(zero,X0) = join(zero,join(zero,X0)),
inference(superposition,[],[f23,f31964]) ).
fof(f32002,plain,
! [X0] : join(zero,X0) = X0,
inference(superposition,[],[f31977,f31875]) ).
fof(f32108,plain,
! [X0] : join(X0,zero) = X0,
inference(superposition,[],[f32002,f22]) ).
fof(f32117,plain,
! [X0] : complement(join(zero,complement(X0))) = X0,
inference(superposition,[],[f31875,f32002]) ).
fof(f32441,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_demodulation,[],[f32117,f32002]) ).
fof(f32873,plain,
! [X0,X1] : complement(X0) = join(complement(join(X0,X1)),complement(join(X0,complement(X1)))),
inference(superposition,[],[f24926,f32441]) ).
fof(f42107,plain,
! [X0] : complement(join(complement(X0),complement(converse(complement(converse(complement(X0))))))) = X0,
inference(forward_demodulation,[],[f31849,f32002]) ).
fof(f47421,plain,
! [X0] : complement(X0) = complement(join(X0,complement(converse(complement(converse(X0)))))),
inference(superposition,[],[f42107,f32441]) ).
fof(f48211,plain,
! [X0] : complement(join(complement(X0),complement(converse(complement(converse(complement(X0))))))) = join(X0,complement(converse(complement(converse(X0))))),
inference(superposition,[],[f42107,f47421]) ).
fof(f48217,plain,
! [X0] : join(X0,complement(converse(complement(converse(X0))))) = X0,
inference(forward_demodulation,[],[f48211,f42107]) ).
fof(f48343,plain,
! [X0] : converse(X0) = join(converse(X0),complement(converse(complement(X0)))),
inference(superposition,[],[f48217,f29]) ).
fof(f48435,plain,
! [X0] : converse(converse(X0)) = join(X0,converse(complement(converse(complement(converse(converse(X0))))))),
inference(superposition,[],[f57,f48217]) ).
fof(f48524,plain,
! [X0] : join(X0,converse(complement(converse(complement(X0))))) = X0,
inference(forward_demodulation,[],[f48435,f29]) ).
fof(f48878,plain,
! [X0] : complement(X0) = join(complement(X0),converse(complement(converse(X0)))),
inference(superposition,[],[f48524,f32441]) ).
fof(f53536,plain,
! [X0] : converse(complement(X0)) = join(converse(complement(X0)),complement(converse(X0))),
inference(superposition,[],[f48343,f32441]) ).
fof(f53637,plain,
! [X0] : converse(complement(X0)) = join(complement(converse(X0)),converse(complement(X0))),
inference(forward_demodulation,[],[f53536,f22]) ).
fof(f64454,plain,
! [X0] : converse(complement(converse(X0))) = join(complement(X0),converse(complement(converse(X0)))),
inference(superposition,[],[f53637,f29]) ).
fof(f64550,plain,
! [X0] : complement(X0) = converse(complement(converse(X0))),
inference(forward_demodulation,[],[f64454,f48878]) ).
fof(f64640,plain,
! [X0,X1] : converse(complement(converse(join(X0,X1)))) = complement(join(X1,X0)),
inference(superposition,[],[f64550,f114]) ).
fof(f64671,plain,
! [X0] : join(X0,complement(complement(X0))) = X0,
inference(superposition,[],[f48524,f64550]) ).
fof(f64739,plain,
! [X0] : join(X0,X0) = X0,
inference(forward_demodulation,[],[f64671,f32441]) ).
fof(f64754,plain,
! [X0,X1] : complement(join(X0,X1)) = complement(join(X1,X0)),
inference(forward_demodulation,[],[f64640,f64550]) ).
fof(f64792,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X0,X1)),
inference(superposition,[],[f23,f64739]) ).
fof(f65717,plain,
! [X0,X1] : top = join(join(X1,X0),complement(join(X0,X1))),
inference(superposition,[],[f33,f64754]) ).
fof(f65812,plain,
! [X0,X1] : top = join(X1,join(X0,complement(join(X0,X1)))),
inference(forward_demodulation,[],[f65717,f23]) ).
fof(f65933,plain,
! [X0,X1] : join(X0,X1) = join(X1,join(X0,X1)),
inference(superposition,[],[f64792,f22]) ).
fof(f65988,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),X0) = X0,
inference(superposition,[],[f64792,f24926]) ).
fof(f67035,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),X1))) = X0,
inference(forward_demodulation,[],[f65988,f22]) ).
fof(f69040,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X0,X1))),
inference(superposition,[],[f67035,f32441]) ).
fof(f69096,plain,
! [X0,X1] : join(X1,complement(join(X0,complement(X1)))) = X1,
inference(superposition,[],[f67035,f22]) ).
fof(f69572,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X1,X0))),
inference(superposition,[],[f69096,f32441]) ).
fof(f69586,plain,
! [X2,X0,X1] : join(X2,complement(join(X0,join(X1,complement(X2))))) = X2,
inference(superposition,[],[f69096,f23]) ).
fof(f74500,plain,
! [X0,X1] : join(X0,X1) = join(join(X0,X1),complement(complement(X0))),
inference(superposition,[],[f69096,f69040]) ).
fof(f74537,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X1,complement(complement(X0)))),
inference(forward_demodulation,[],[f74500,f23]) ).
fof(f74713,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X1,X0)),
inference(forward_demodulation,[],[f74537,f32441]) ).
fof(f74907,plain,
! [X0,X1] : join(join(X0,X1),join(X0,X1)) = join(join(X0,X1),X0),
inference(superposition,[],[f74713,f64792]) ).
fof(f76151,plain,
! [X0,X1] : join(join(X0,X1),join(X0,X1)) = join(X0,join(X1,X0)),
inference(forward_demodulation,[],[f74907,f23]) ).
fof(f76579,plain,
! [X0,X1] : join(X1,X0) = join(join(X0,X1),join(X0,X1)),
inference(forward_demodulation,[],[f76151,f65933]) ).
fof(f76933,plain,
! [X0,X1] : join(X1,X0) = join(X0,join(X1,join(X0,X1))),
inference(forward_demodulation,[],[f76579,f23]) ).
fof(f77193,plain,
! [X0,X1] : join(X1,X0) = join(X0,join(X0,X1)),
inference(forward_demodulation,[],[f76933,f65933]) ).
fof(f78367,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X1,join(join(X1,X0),X2)),
inference(superposition,[],[f23,f77193]) ).
fof(f78864,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X1,join(X1,join(X0,X2))),
inference(forward_demodulation,[],[f78367,f23]) ).
fof(f79498,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X1,join(X0,X2)),
inference(forward_demodulation,[],[f78864,f64792]) ).
fof(f91043,plain,
! [X2,X0,X1] : join(X0,complement(join(X2,join(complement(X0),X1)))) = X0,
inference(superposition,[],[f69586,f22]) ).
fof(f97773,plain,
! [X0,X1] : top = join(join(complement(X0),X1),X0),
inference(superposition,[],[f65812,f91043]) ).
fof(f98074,plain,
! [X0,X1] : top = join(complement(X0),join(X1,X0)),
inference(forward_demodulation,[],[f97773,f23]) ).
fof(f98610,plain,
! [X2,X0,X1] : top = join(complement(composition(X1,X2)),composition(join(X0,X1),X2)),
inference(superposition,[],[f98074,f28]) ).
fof(f148675,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X1,join(X0,X2)),
inference(superposition,[],[f79498,f23]) ).
fof(f148677,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X1,X0)),
inference(superposition,[],[f79498,f22]) ).
fof(f160588,plain,
! [X2,X0,X1] : join(X2,join(X0,X1)) = join(X1,join(X2,X0)),
inference(superposition,[],[f148675,f22]) ).
fof(f174802,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X0,join(X2,X1)),
inference(superposition,[],[f160588,f148677]) ).
fof(f319981,plain,
! [X0] : top = join(complement(composition(composition(converse(sK0),sK0),X0)),composition(one,X0)),
inference(superposition,[],[f98610,f46]) ).
fof(f320581,plain,
! [X0] : top = join(composition(one,X0),complement(composition(composition(converse(sK0),sK0),X0))),
inference(forward_demodulation,[],[f319981,f22]) ).
fof(f321217,plain,
! [X0] : top = join(composition(one,X0),complement(composition(converse(sK0),composition(sK0,X0)))),
inference(forward_demodulation,[],[f320581,f26]) ).
fof(f321474,plain,
! [X0] : top = join(X0,complement(composition(converse(sK0),composition(sK0,X0)))),
inference(forward_demodulation,[],[f321217,f252]) ).
fof(f1109731,plain,
! [X0,X1] : join(X0,X1) = join(complement(complement(X0)),complement(join(complement(join(X0,X1)),complement(complement(join(X0,complement(X1))))))),
inference(superposition,[],[f24926,f32873]) ).
fof(f1110185,plain,
! [X0,X1] : join(X0,X1) = join(complement(complement(X0)),complement(join(complement(join(X0,X1)),join(X0,complement(X1))))),
inference(forward_demodulation,[],[f1109731,f32441]) ).
fof(f1111372,plain,
! [X0,X1] : join(X0,X1) = join(complement(complement(X0)),complement(join(X0,join(complement(join(X0,X1)),complement(X1))))),
inference(forward_demodulation,[],[f1110185,f148675]) ).
fof(f1112333,plain,
! [X0,X1] : join(X0,X1) = join(complement(complement(X0)),complement(join(X0,join(complement(X1),complement(join(X0,X1)))))),
inference(forward_demodulation,[],[f1111372,f174802]) ).
fof(f1112824,plain,
! [X0,X1] : join(X0,X1) = join(complement(complement(X0)),complement(join(X0,complement(X1)))),
inference(forward_demodulation,[],[f1112333,f69572]) ).
fof(f1113007,plain,
! [X0,X1] : join(X0,X1) = join(X0,complement(join(X0,complement(X1)))),
inference(forward_demodulation,[],[f1112824,f32441]) ).
fof(f1113200,plain,
! [X0] : join(X0,complement(top)) = join(X0,composition(converse(sK0),composition(sK0,X0))),
inference(superposition,[],[f1113007,f321474]) ).
fof(f1114384,plain,
! [X0] : join(X0,zero) = join(X0,composition(converse(sK0),composition(sK0,X0))),
inference(forward_demodulation,[],[f1113200,f55]) ).
fof(f1114704,plain,
! [X0] : join(X0,composition(converse(sK0),composition(sK0,X0))) = X0,
inference(forward_demodulation,[],[f1114384,f32108]) ).
fof(f1115458,plain,
join(one,composition(converse(sK1),sK1)) = join(one,composition(converse(composition(converse(sK0),composition(sK0,sK1))),sK1)),
inference(superposition,[],[f17098,f1114704]) ).
fof(f1115459,plain,
join(one,composition(converse(sK1),sK1)) = join(one,composition(composition(converse(composition(sK0,sK1)),sK0),sK1)),
inference(forward_demodulation,[],[f1115458,f64]) ).
fof(f1115759,plain,
join(one,composition(converse(sK1),sK1)) = join(one,composition(converse(composition(sK0,sK1)),composition(sK0,sK1))),
inference(forward_demodulation,[],[f1115459,f26]) ).
fof(f1115885,plain,
one = join(one,composition(converse(composition(sK0,sK1)),composition(sK0,sK1))),
inference(forward_demodulation,[],[f1115759,f45]) ).
fof(f1115923,plain,
$false,
inference(forward_subsumption_resolution,[],[f1115885,f49]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL031+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.13/0.37 % Computer : n016.cluster.edu
% 0.13/0.37 % Model : x86_64 x86_64
% 0.13/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.37 % Memory : 8046.5625MB
% 0.13/0.37 % OS : Linux 6.8.0-71-generic
% 0.13/0.37 % CPULimit : 300
% 0.13/0.37 % WCLimit : 300
% 0.13/0.37 % DateTime : Sun Sep 27 22:59:30 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.13/0.41 Running first-order model finding
% 0.13/0.41 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.75/3.02 % (3085573)Will run a generic schedule for satisfiability detection.
% 16.75/3.02 % (3085588)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1931369512:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 16.75/3.02 % (3085583)% WARNING: option uhcvi not known.
% 16.75/3.02 % (3085582)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1578991520_2999 on theBenchmark for (2999ds/0Mi)
% 16.75/3.02 % (3085586)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4214439332:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 16.75/3.02 % (3085585)dis+10_1_sil=32000:sp=arity:random_seed=4279433256:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 16.75/3.02 % (3085583)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3430588163:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 16.75/3.02 % (3085587)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3186770564:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 16.75/3.02 % TRYING [1]
% 16.75/3.02 % TRYING [2]
% 16.75/3.02 % (3085584)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=321804500:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 16.75/3.02 % TRYING [3]
% 16.75/3.02 % TRYING [4]
% 16.75/3.02 % (3085588)Instruction limit reached!
% 16.75/3.02 % (3085588)------------------------------
% 16.75/3.02 % (3085588)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.75/3.02 % (3085588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.75/3.02 % (3085588)CaDiCaL version: 2.1.3
% 16.75/3.02 % (3085588)Termination reason: Instruction limit
% 16.75/3.02 % (3085588)Termination phase: Saturation
% 16.75/3.02 % (3085588)Time elapsed: 0.052 s
% 16.75/3.02 % (3085588)Peak memory usage: 12 MB
% 16.75/3.02 % (3085588)Instructions burned: 162 (million)
% 16.75/3.02 % (3085601)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=643461407:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 16.75/3.02 % (3085585)Instruction limit reached!
% 16.75/3.02 % (3085585)------------------------------
% 16.75/3.02 % (3085585)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.75/3.02 % (3085585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.75/3.02 % (3085585)CaDiCaL version: 2.1.3
% 16.75/3.02 % (3085585)Termination reason: Instruction limit
% 16.75/3.02 % (3085585)Termination phase: Saturation
% 16.75/3.02 % (3085585)Time elapsed: 0.059 s
% 16.75/3.02 % (3085585)Peak memory usage: 12 MB
% 16.75/3.02 % (3085585)Instructions burned: 104 (million)
% 16.75/3.02 % TRYING [1]
% 16.75/3.02 % TRYING [2]
% 16.75/3.02 % TRYING [3]
% 16.75/3.02 % (3085586)Instruction limit reached!
% 16.75/3.02 % (3085586)------------------------------
% 16.75/3.02 % (3085586)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.75/3.02 % (3085586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.75/3.02 % (3085586)CaDiCaL version: 2.1.3
% 16.75/3.02 % (3085586)Termination reason: Instruction limit
% 16.75/3.02 % (3085586)Termination phase: Saturation
% 16.75/3.02 % (3085586)Time elapsed: 0.071 s
% 16.75/3.02 % (3085586)Peak memory usage: 13 MB
% 16.75/3.02 % (3085586)Instructions burned: 117 (million)
% 16.75/3.02 % (3085587)Instruction limit reached!
% 16.75/3.02 % (3085587)------------------------------
% 16.75/3.02 % (3085587)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.75/3.02 % (3085587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.75/3.02 % (3085587)CaDiCaL version: 2.1.3
% 16.75/3.02 % (3085587)Termination reason: Instruction limit
% 16.75/3.02 % (3085587)Termination phase: Saturation
% 16.75/3.02 % (3085587)Time elapsed: 0.078 s
% 16.75/3.02 % (3085587)Peak memory usage: 13 MB
% 16.75/3.02 % (3085587)Instructions burned: 132 (million)
% 16.75/3.02 % (3085603)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3135283032:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 16.75/3.02 % TRYING [4]
% 16.75/3.02 % (3085604)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=3967182670:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 16.75/3.02 % (3085606)ott-21_1_sil=16000:fs=off:random_seed=3438323661:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 16.75/3.02 % TRYING [5]
% 16.75/3.02 % (3085606)Instruction limit reached!
% 16.75/3.02 % (3085606)------------------------------
% 16.75/3.02 % (3085606)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.23/5.43 % (3085606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.23/5.43 % (3085606)CaDiCaL version: 2.1.3
% 35.23/5.43 % (3085606)Termination reason: Instruction limit
% 35.23/5.43 % (3085606)Termination phase: Saturation
% 35.23/5.43 % (3085606)Time elapsed: 0.088 s
% 35.23/5.43 % (3085606)Peak memory usage: 12 MB
% 35.23/5.43 % (3085606)Instructions burned: 182 (million)
% 35.23/5.43 % (3085609)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1079567596:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 35.23/5.43 % (3085601)Instruction limit reached!
% 35.23/5.43 % (3085601)------------------------------
% 35.23/5.43 % (3085601)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.23/5.43 % (3085601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.23/5.43 % (3085601)CaDiCaL version: 2.1.3
% 35.23/5.43 % (3085601)Termination reason: Instruction limit
% 35.23/5.43 % (3085601)Termination phase: Finite model building constraint generation
% 35.23/5.43 % (3085601)Time elapsed: 0.154 s
% 35.23/5.43 % (3085601)Peak memory usage: 28 MB
% 35.23/5.43 % (3085601)Instructions burned: 715 (million)
% 35.23/5.43 % TRYING [5]
% 35.23/5.43 % (3085611)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3333943382:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 35.23/5.43 % (3085603)Instruction limit reached!
% 35.23/5.43 % (3085603)------------------------------
% 35.23/5.43 % (3085603)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.23/5.43 % (3085603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.23/5.43 % (3085603)CaDiCaL version: 2.1.3
% 35.23/5.43 % (3085603)Termination reason: Instruction limit
% 35.23/5.43 % (3085603)Termination phase: Saturation
% 35.23/5.43 % (3085603)Time elapsed: 0.144 s
% 35.23/5.43 % (3085603)Peak memory usage: 13 MB
% 35.23/5.43 % (3085603)Instructions burned: 132 (million)
% 35.23/5.43 % TRYING [1]
% 35.23/5.43 % TRYING [2]
% 35.23/5.43 % TRYING [3]
% 35.23/5.43 % (3085613)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1480742208:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 35.23/5.43 % TRYING [4]
% 35.23/5.43 % (3085611)Instruction limit reached!
% 35.23/5.43 % (3085611)------------------------------
% 35.23/5.43 % (3085611)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.23/5.43 % (3085611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.23/5.43 % (3085611)CaDiCaL version: 2.1.3
% 35.23/5.43 % (3085611)Termination reason: Instruction limit
% 35.23/5.43 % (3085611)Termination phase: Finite model building SAT solving
% 35.23/5.43 % (3085611)Time elapsed: 0.159 s
% 35.23/5.43 % (3085611)Peak memory usage: 24 MB
% 35.23/5.43 % (3085611)Instructions burned: 866 (million)
% 35.23/5.43 % (3085615)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3614202085:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 35.23/5.43 % (3085604)Instruction limit reached!
% 35.23/5.43 % (3085604)------------------------------
% 35.23/5.43 % (3085604)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.23/5.43 % (3085604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.23/5.43 % (3085604)CaDiCaL version: 2.1.3
% 35.23/5.43 % (3085604)Termination reason: Instruction limit
% 35.23/5.43 % (3085604)Termination phase: Saturation
% 35.23/5.43 % (3085604)Time elapsed: 0.343 s
% 35.23/5.43 % (3085604)Peak memory usage: 16 MB
% 35.23/5.43 % (3085604)Instructions burned: 685 (million)
% 35.23/5.43 % (3085617)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=318364343: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)
% 35.23/5.43 % (3085609)Instruction limit reached!
% 35.23/5.43 % (3085609)------------------------------
% 35.23/5.43 % (3085609)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.23/5.43 % (3085609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.23/5.43 % (3085609)CaDiCaL version: 2.1.3
% 35.23/5.43 % (3085609)Termination reason: Instruction limit
% 35.23/5.43 % (3085609)Termination phase: Saturation
% 35.23/5.43 % (3085609)Time elapsed: 0.253 s
% 35.23/5.43 % (3085609)Peak memory usage: 16 MB
% 35.23/5.43 % (3085609)Instructions burned: 477 (million)
% 35.23/5.43 % (3085619)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3341038964:i=879:kws=inv_precedence:fsr=off_2995 on theBenchmark for (2995ds/879Mi)
% 35.23/5.43 % (3085615)Instruction limit reached!
% 35.23/5.43 % (3085615)------------------------------
% 84.88/12.47 % (3085615)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 84.88/12.47 % (3085615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.88/12.47 % (3085615)CaDiCaL version: 2.1.3
% 84.88/12.47 % (3085615)Termination reason: Instruction limit
% 84.88/12.47 % (3085615)Termination phase: Finite model building constraint generation
% 84.88/12.47 % (3085615)Time elapsed: 0.230 s
% 84.88/12.47 % (3085615)Peak memory usage: 107 MB
% 84.88/12.47 % (3085615)Instructions burned: 891 (million)
% 84.88/12.47 % (3085623)fmb+10_1_sil=64000:random_seed=1340422842:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 84.88/12.47 % TRYING [1]
% 84.88/12.47 % TRYING [2]
% 84.88/12.47 % TRYING [3]
% 84.88/12.47 % TRYING [4]
% 84.88/12.47 % TRYING [6]
% 84.88/12.47 % (3085617)Instruction limit reached!
% 84.88/12.47 % (3085617)------------------------------
% 84.88/12.47 % (3085617)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 84.88/12.47 % (3085617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.88/12.47 % (3085617)CaDiCaL version: 2.1.3
% 84.88/12.47 % (3085617)Termination reason: Instruction limit
% 84.88/12.47 % (3085617)Termination phase: Saturation
% 84.88/12.47 % (3085617)Time elapsed: 0.472 s
% 84.88/12.47 % (3085617)Peak memory usage: 17 MB
% 84.88/12.47 % (3085617)Instructions burned: 693 (million)
% 84.88/12.47 % (3085639)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1358117328:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 84.88/12.47 % TRYING [20]
% 84.88/12.47 % TRYING [5]
% 84.88/12.47 % (3085613)Instruction limit reached!
% 84.88/12.47 % (3085613)------------------------------
% 84.88/12.47 % (3085613)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 84.88/12.47 % (3085613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.88/12.47 % (3085613)CaDiCaL version: 2.1.3
% 84.88/12.47 % (3085613)Termination reason: Instruction limit
% 84.88/12.47 % (3085613)Termination phase: Saturation
% 84.88/12.47 % (3085613)Time elapsed: 0.829 s
% 84.88/12.47 % (3085613)Peak memory usage: 26 MB
% 84.88/12.47 % (3085613)Instructions burned: 1179 (million)
% 84.88/12.47 % (3085642)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1429669259:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 84.88/12.47 % (3085619)Instruction limit reached!
% 84.88/12.47 % (3085619)------------------------------
% 84.88/12.47 % (3085619)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 84.88/12.47 % (3085619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.88/12.47 % (3085619)CaDiCaL version: 2.1.3
% 84.88/12.47 % (3085619)Termination reason: Instruction limit
% 84.88/12.47 % (3085619)Termination phase: Saturation
% 84.88/12.47 % (3085619)Time elapsed: 0.631 s
% 84.88/12.47 % (3085619)Peak memory usage: 18 MB
% 84.88/12.47 % (3085619)Instructions burned: 879 (million)
% 84.88/12.47 % TRYING [8]
% 84.88/12.47 % (3085645)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3768233067:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 84.88/12.47 % (3085642)Instruction limit reached!
% 84.88/12.47 % (3085642)------------------------------
% 84.88/12.47 % (3085642)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 84.88/12.47 % (3085642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.88/12.47 % (3085642)CaDiCaL version: 2.1.3
% 84.88/12.47 % (3085642)Termination reason: Instruction limit
% 84.88/12.47 % (3085642)Termination phase: Finite model building constraint generation
% 84.88/12.47 % (3085642)Time elapsed: 0.573 s
% 84.88/12.47 % (3085642)Peak memory usage: 75 MB
% 84.88/12.47 % (3085642)Instructions burned: 920 (million)
% 84.88/12.47 % (3085651)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2771605627:i=1472:ins=7:fdi=8:gsp=on_2982 on theBenchmark for (2982ds/1472Mi)
% 84.88/12.47 % TRYING [6]
% 84.88/12.47 % (3085651)Instruction limit reached!
% 84.88/12.47 % (3085651)------------------------------
% 84.88/12.47 % (3085651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 84.88/12.47 % (3085651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.88/12.47 % (3085651)CaDiCaL version: 2.1.3
% 84.88/12.47 % (3085651)Termination reason: Instruction limit
% 84.88/12.47 % (3085651)Termination phase: Saturation
% 84.88/12.47 % (3085651)Time elapsed: 0.822 s
% 84.88/12.47 % (3085651)Peak memory usage: 26 MB
% 84.88/12.47 % (3085651)Instructions burned: 1473 (million)
% 84.88/12.47 % (3085752)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2191406824:i=6324_2974 on theBenchmark for (2974ds/6324Mi)
% 84.88/12.47 % (3085752)Cannot represent all propositional literals internally
% 117.77/33.26 % (3085752)Refutation not found, incomplete strategy
% 117.77/33.26 % (3085752)------------------------------
% 117.77/33.26 % (3085752)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.77/33.26 % (3085752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.77/33.26 % (3085752)CaDiCaL version: 2.1.3
% 117.77/33.26 % (3085752)Termination reason: Refutation not found, incomplete strategy
% 117.77/33.26 % (3085752)Time elapsed: 0.008 s
% 117.77/33.26 % (3085752)Peak memory usage: 10 MB
% 117.77/33.26 % (3085752)Instructions burned: 14 (million)
% 117.77/33.26 % (3085752)------------------------------
% 117.77/33.26 % (3085752)------------------------------
% 117.77/33.26 % (3085762)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2204949068:fmbsr=2.30978:i=2174_2973 on theBenchmark for (2973ds/2174Mi)
% 117.77/33.26 % TRYING [16]
% 117.77/33.26 % (3085762)Instruction limit reached!
% 117.77/33.26 % (3085762)------------------------------
% 117.77/33.26 % (3085762)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.77/33.26 % (3085762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.77/33.26 % (3085762)CaDiCaL version: 2.1.3
% 117.77/33.26 % (3085762)Termination reason: Instruction limit
% 117.77/33.26 % (3085762)Termination phase: Finite model building constraint generation
% 117.77/33.26 % (3085762)Time elapsed: 0.735 s
% 117.77/33.26 % (3085762)Peak memory usage: 132 MB
% 117.77/33.26 % (3085762)Instructions burned: 2175 (million)
% 117.77/33.26 % (3085811)ott-2_1_sil=16000:newcnf=on:random_seed=1303567488:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2966 on theBenchmark for (2966ds/869Mi)
% 117.77/33.26 % (3085811)Instruction limit reached!
% 117.77/33.26 % (3085811)------------------------------
% 117.77/33.26 % (3085811)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.77/33.26 % (3085811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.77/33.26 % (3085811)CaDiCaL version: 2.1.3
% 117.77/33.26 % (3085811)Termination reason: Instruction limit
% 117.77/33.26 % (3085811)Termination phase: Saturation
% 117.77/33.26 % (3085811)Time elapsed: 0.523 s
% 117.77/33.26 % (3085811)Peak memory usage: 22 MB
% 117.77/33.26 % (3085811)Instructions burned: 871 (million)
% 117.77/33.26 % (3085813)ott+10_1_sil=32000:tgt=ground:random_seed=181604095:i=5114:av=off_2960 on theBenchmark for (2960ds/5114Mi)
% 117.77/33.26 % TRYING [7]
% 117.77/33.26 % (3085645)Instruction limit reached!
% 117.77/33.26 % (3085645)------------------------------
% 117.77/33.26 % (3085645)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.77/33.26 % (3085645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.77/33.26 % (3085645)CaDiCaL version: 2.1.3
% 117.77/33.26 % (3085645)Termination reason: Instruction limit
% 117.77/33.26 % (3085645)Termination phase: Saturation
% 117.77/33.26 % (3085645)Time elapsed: 3.111 s
% 117.77/33.26 % (3085645)Peak memory usage: 55 MB
% 117.77/33.26 % (3085645)Instructions burned: 5132 (million)
% 117.77/33.26 % (3085815)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=361632647:i=54282_2957 on theBenchmark for (2957ds/54282Mi)
% 117.77/33.26 % TRYING [1]
% 117.77/33.26 % TRYING [2]
% 117.77/33.26 % TRYING [3]
% 117.77/33.26 % TRYING [4]
% 117.77/33.26 % TRYING [5]
% 117.77/33.26 % (3085639)Instruction limit reached!
% 117.77/33.26 % (3085639)------------------------------
% 117.77/33.26 % (3085639)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.77/33.26 % (3085639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.77/33.26 % (3085639)CaDiCaL version: 2.1.3
% 117.77/33.26 % (3085639)Termination reason: Instruction limit
% 117.77/33.26 % (3085639)Termination phase: Finite model building constraint generation
% 117.77/33.26 % (3085639)Time elapsed: 3.867 s
% 117.77/33.26 % (3085639)Peak memory usage: 675 MB
% 117.77/33.26 % (3085639)Instructions burned: 9518 (million)
% 117.77/33.26 % TRYING [7]
% 117.77/33.26 % (3085817)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3432686906:i=3512:aac=none_2950 on theBenchmark for (2950ds/3512Mi)
% 117.77/33.26 % (3085623)Instruction limit reached!
% 117.77/33.26 % (3085623)------------------------------
% 117.77/33.26 % (3085623)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.77/33.26 % (3085623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.77/33.26 % (3085623)CaDiCaL version: 2.1.3
% 117.77/33.26 % (3085623)Termination reason: Instruction limit
% 117.77/33.26 % (3085623)Termination phase: Finite model building constraint generation
% 117.77/33.26 % (3085623)Time elapsed: 4.326 s
% 117.77/33.26 % (3085623)Peak memory usage: 142 MB
% 117.77/33.26 % (3085623)Instructions burned: 22064 (million)
% 117.77/33.26 % (3085819)dis+21_1_sil=32000:sas=cadical:random_seed=1030828689:i=3773:amm=off_2949 on theBenchmark for (2949ds/3773Mi)
% 117.77/33.26 % TRYING [6]
% 117.77/33.26 % (3085819)Instruction limit reached!
% 117.77/33.26 % (3085819)------------------------------
% 117.77/33.26 % (3085819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.77/33.26 % (3085819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.77/33.26 % (3085819)CaDiCaL version: 2.1.3
% 117.77/33.26 % (3085819)Termination reason: Instruction limit
% 117.77/33.26 % (3085819)Termination phase: Saturation
% 117.77/33.26 % (3085819)Time elapsed: 1.064 s
% 117.77/33.26 % (3085819)Peak memory usage: 43 MB
% 117.77/33.26 % (3085819)Instructions burned: 3775 (million)
% 117.77/33.26 % (3085821)ott+11_1_sil=16000:gs=on:random_seed=1211701193:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2939 on theBenchmark for (2939ds/2251Mi)
% 117.77/33.26 % (3085821)Instruction limit reached!
% 117.77/33.26 % (3085821)------------------------------
% 117.77/33.26 % (3085821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.77/33.26 % (3085821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.77/33.26 % (3085821)CaDiCaL version: 2.1.3
% 117.77/33.26 % (3085821)Termination reason: Instruction limit
% 117.77/33.26 % (3085821)Termination phase: Saturation
% 117.77/33.26 % (3085821)Time elapsed: 0.659 s
% 117.77/33.26 % (3085821)Peak memory usage: 28 MB
% 117.77/33.26 % (3085821)Instructions burned: 2254 (million)
% 117.77/33.26 % (3085823)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3278450909:fmbsr=1.6:i=67534_2932 on theBenchmark for (2932ds/67534Mi)
% 117.77/33.26 % TRYING [7]
% 117.77/33.26 % (3085817)Instruction limit reached!
% 117.77/33.26 % (3085817)------------------------------
% 117.77/33.26 % (3085817)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.77/33.26 % (3085817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.77/33.26 % (3085817)CaDiCaL version: 2.1.3
% 117.77/33.26 % (3085817)Termination reason: Instruction limit
% 117.77/33.26 % (3085817)Termination phase: Saturation
% 117.77/33.26 % (3085817)Time elapsed: 1.863 s
% 117.77/33.26 % (3085817)Peak memory usage: 41 MB
% 117.77/33.26 % (3085817)Instructions burned: 3512 (million)
% 117.77/33.26 % (3085825)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3098411405:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2931 on theBenchmark for (2931ds/4591Mi)
% 117.77/33.26 % (3085813)Instruction limit reached!
% 117.77/33.26 % (3085813)------------------------------
% 117.77/33.26 % (3085813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.77/33.26 % (3085813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.77/33.26 % (3085813)CaDiCaL version: 2.1.3
% 117.77/33.26 % (3085813)Termination reason: Instruction limit
% 117.77/33.26 % (3085813)Termination phase: Saturation
% 117.77/33.26 % (3085813)Time elapsed: 3.070 s
% 117.77/33.26 % (3085813)Peak memory usage: 65 MB
% 117.77/33.26 % (3085813)Instructions burned: 5114 (million)
% 117.77/33.26 % (3085827)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=822534012:i=29340_2929 on theBenchmark for (2929ds/29340Mi)
% 117.77/33.26 % TRYING [7]
% 117.77/33.26 % (3085825)Instruction limit reached!
% 117.77/33.26 % (3085825)------------------------------
% 117.77/33.26 % (3085825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.77/33.26 % (3085825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.77/33.26 % (3085825)CaDiCaL version: 2.1.3
% 117.77/33.26 % (3085825)Termination reason: Instruction limit
% 117.77/33.26 % (3085825)Termination phase: Saturation
% 117.77/33.26 % (3085825)Time elapsed: 2.319 s
% 117.77/33.26 % (3085825)Peak memory usage: 61 MB
% 117.77/33.26 % (3085825)Instructions burned: 4591 (million)
% 117.77/33.26 % (3085829)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2322956873:i=5211_2908 on theBenchmark for (2908ds/5211Mi)
% 117.77/33.26 % (3085829)Instruction limit reached!
% 117.77/33.26 % (3085829)------------------------------
% 117.77/33.26 % (3085829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.77/33.26 % (3085829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.77/33.26 % (3085829)CaDiCaL version: 2.1.3
% 117.77/33.26 % (3085829)Termination reason: Instruction limit
% 117.77/33.26 % (3085829)Termination phase: Saturation
% 117.77/33.26 % (3085829)Time elapsed: 2.821 s
% 117.77/33.26 % (3085829)Peak memory usage: 49 MB
% 117.77/33.26 % (3085829)Instructions burned: 5213 (million)
% 117.77/33.26 % (3085831)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1840573965:i=5497:nm=2_2879 on theBenchmark for (2879ds/5497Mi)
% 117.77/33.26 % TRYING [17]
% 117.77/33.26 % (3085831)Instruction limit reached!
% 117.77/33.26 % (3085831)------------------------------
% 117.77/33.26 % (3085831)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.77/33.26 % (3085831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.77/33.26 % (3085831)CaDiCaL version: 2.1.3
% 117.77/33.26 % (3085831)Termination reason: Instruction limit
% 117.77/33.26 % (3085831)Termination phase: Finite model building constraint generation
% 117.77/33.26 % (3085831)Time elapsed: 1.940 s
% 117.77/33.26 % (3085831)Peak memory usage: 394 MB
% 117.77/33.26 % (3085831)Instructions burned: 5497 (million)
% 117.77/33.26 % (3085833)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=4241568885:fmbsr=2:i=46332_2859 on theBenchmark for (2859ds/46332Mi)
% 117.77/33.26 % TRYING [15]
% 117.77/33.26 % (3085827)Instruction limit reached!
% 117.77/33.26 % (3085827)------------------------------
% 117.77/33.26 % (3085827)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.77/33.26 % (3085827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.77/33.26 % (3085827)CaDiCaL version: 2.1.3
% 117.77/33.26 % (3085827)Termination reason: Instruction limit
% 117.77/33.26 % (3085827)Termination phase: Saturation
% 117.77/33.26 % (3085827)Time elapsed: 19.213 s
% 117.77/33.26 % (3085827)Peak memory usage: 166 MB
% 117.77/33.26 % (3085827)Instructions burned: 29340 (million)
% 117.77/33.26 % (3086149)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=204055039:i=14071_2737 on theBenchmark for (2737ds/14071Mi)
% 117.77/33.26 % TRYING [12]
% 117.77/33.26 % TRYING [8]
% 117.77/33.26 % (3085584) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3085573-3085584"...
% 117.77/33.26 % (3085584)...printing done.
% 117.77/33.26 % (3085584)Refutation found. Thanks to Tanya!
% 117.77/33.26 % SZS status Theorem for theBenchmark
% 117.77/33.26 % SZS output start Proof for theBenchmark
% See solution above
% 117.77/33.26 % (3085584)------------------------------
% 117.77/33.26 % (3085584)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.77/33.26 % (3085584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.77/33.26 % (3085584)CaDiCaL version: 2.1.3
% 117.77/33.26 % (3085584)Termination reason: Refutation
% 117.77/33.26 % (3085584)Time elapsed: 32.324 s
% 117.77/33.26 % (3085584)Peak memory usage: 258 MB
% 117.77/33.26 % (3085584)Instructions burned: 55560 (million)
% 117.77/33.26 % (3085573)Success in time 32.837 s
% 117.77/33.26 % Vampire exiting
%------------------------------------------------------------------------------