%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : REL031+1 : 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 : n007.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 94.08s 35.28s
% Output : Refutation 94.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 63
% Number of leaves : 14
% Syntax : Number of formulae : 151 ( 146 unt; 0 def)
% Number of atoms : 161 ( 160 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 : 186 ( 182 !; 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(f14,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(f15,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)],[f14]) ).
fof(f16,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,[],[f15]) ).
fof(f17,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,[],[f16]) ).
fof(f18,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)],[f17]) ).
fof(f19,plain,
! [X0,X1] : join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f20,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
inference(cnf_transformation,[],[f2]) ).
fof(f21,plain,
! [X0,X1] : join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) = X0,
inference(cnf_transformation,[],[f3]) ).
fof(f22,plain,
! [X0,X1] : complement(join(complement(X0),complement(X1))) = meet(X0,X1),
inference(cnf_transformation,[],[f4]) ).
fof(f23,plain,
! [X2,X0,X1] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
inference(cnf_transformation,[],[f5]) ).
fof(f24,plain,
! [X0] : composition(X0,one) = X0,
inference(cnf_transformation,[],[f6]) ).
fof(f25,plain,
! [X2,X0,X1] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
inference(cnf_transformation,[],[f7]) ).
fof(f26,plain,
! [X0] : converse(converse(X0)) = X0,
inference(cnf_transformation,[],[f8]) ).
fof(f27,plain,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
inference(cnf_transformation,[],[f9]) ).
fof(f28,plain,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
inference(cnf_transformation,[],[f10]) ).
fof(f29,plain,
! [X0,X1] : complement(X1) = join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)),
inference(cnf_transformation,[],[f11]) ).
fof(f30,plain,
! [X0] : top = join(X0,complement(X0)),
inference(cnf_transformation,[],[f12]) ).
fof(f31,plain,
! [X0] : zero = meet(X0,complement(X0)),
inference(cnf_transformation,[],[f13]) ).
fof(f32,plain,
one = join(composition(converse(sK1),sK1),one),
inference(cnf_transformation,[],[f18]) ).
fof(f33,plain,
one = join(composition(converse(sK0),sK0),one),
inference(cnf_transformation,[],[f18]) ).
fof(f34,plain,
one != join(composition(converse(composition(sK0,sK1)),composition(sK0,sK1)),one),
inference(cnf_transformation,[],[f18]) ).
fof(f35,plain,
! [X0] : zero = complement(join(complement(X0),complement(complement(X0)))),
inference(definition_unfolding,[],[f31,f22]) ).
fof(f36,plain,
one = join(one,composition(converse(sK1),sK1)),
inference(superposition,[],[f19,f32]) ).
fof(f37,plain,
one = join(one,composition(converse(sK0),sK0)),
inference(superposition,[],[f19,f33]) ).
fof(f40,plain,
one != join(one,composition(converse(composition(sK0,sK1)),composition(sK0,sK1))),
inference(superposition,[],[f34,f19]) ).
fof(f46,plain,
zero = complement(top),
inference(forward_demodulation,[],[f35,f30]) ).
fof(f48,plain,
! [X0,X1] : converse(join(converse(X0),X1)) = join(X0,converse(X1)),
inference(superposition,[],[f27,f26]) ).
fof(f49,plain,
! [X0,X1] : converse(join(X1,converse(X0))) = join(converse(X1),X0),
inference(superposition,[],[f27,f26]) ).
fof(f55,plain,
! [X0,X1] : converse(composition(converse(X0),X1)) = composition(converse(X1),X0),
inference(superposition,[],[f28,f26]) ).
fof(f59,plain,
! [X0] : join(X0,converse(complement(converse(X0)))) = converse(top),
inference(superposition,[],[f48,f30]) ).
fof(f215,plain,
! [X0] : converse(converse(X0)) = composition(converse(one),X0),
inference(superposition,[],[f55,f24]) ).
fof(f231,plain,
! [X0] : composition(converse(one),X0) = X0,
inference(forward_demodulation,[],[f215,f26]) ).
fof(f236,plain,
one = converse(one),
inference(superposition,[],[f231,f24]) ).
fof(f243,plain,
! [X0] : composition(one,X0) = X0,
inference(superposition,[],[f231,f236]) ).
fof(f266,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(top,X1),
inference(superposition,[],[f20,f30]) ).
fof(f271,plain,
! [X0] : join(one,X0) = join(composition(converse(sK1),sK1),join(one,X0)),
inference(superposition,[],[f20,f32]) ).
fof(f273,plain,
! [X0] : join(one,X0) = join(one,join(composition(converse(sK1),sK1),X0)),
inference(superposition,[],[f20,f36]) ).
fof(f303,plain,
! [X0] : join(one,X0) = join(join(one,X0),composition(converse(sK1),sK1)),
inference(superposition,[],[f19,f271]) ).
fof(f304,plain,
! [X0] : join(one,X0) = join(one,join(X0,composition(converse(sK1),sK1))),
inference(forward_demodulation,[],[f303,f20]) ).
fof(f399,plain,
! [X0,X1] : join(join(one,X0),X1) = join(one,join(join(X0,composition(converse(sK1),sK1)),X1)),
inference(superposition,[],[f20,f304]) ).
fof(f400,plain,
! [X0,X1] : join(join(one,X0),X1) = join(one,join(X0,join(composition(converse(sK1),sK1),X1))),
inference(forward_demodulation,[],[f399,f20]) ).
fof(f403,plain,
! [X0,X1] : join(one,join(X0,X1)) = join(one,join(X0,join(composition(converse(sK1),sK1),X1))),
inference(forward_demodulation,[],[f400,f20]) ).
fof(f1120,plain,
! [X0,X1] : join(one,join(join(composition(converse(sK1),sK1),X0),X1)) = join(one,join(X1,X0)),
inference(superposition,[],[f403,f19]) ).
fof(f1159,plain,
! [X0,X1] : join(one,join(composition(converse(sK1),sK1),join(X0,X1))) = join(one,join(X1,X0)),
inference(forward_demodulation,[],[f1120,f20]) ).
fof(f1165,plain,
! [X0,X1] : join(one,join(X0,X1)) = join(one,join(X1,X0)),
inference(forward_demodulation,[],[f1159,f273]) ).
fof(f1169,plain,
! [X2,X0,X1] : join(one,join(X2,join(X0,X1))) = join(one,join(X0,join(X1,X2))),
inference(superposition,[],[f1165,f20]) ).
fof(f1204,plain,
! [X0,X1] : join(one,join(converse(X1),converse(X0))) = join(one,converse(join(X0,X1))),
inference(superposition,[],[f1165,f27]) ).
fof(f1259,plain,
! [X0,X1] : join(one,converse(join(X0,X1))) = join(one,converse(join(X1,X0))),
inference(forward_demodulation,[],[f1204,f27]) ).
fof(f1271,plain,
! [X2,X0,X1] : join(one,converse(join(X2,join(X0,X1)))) = join(one,converse(join(X0,join(X1,X2)))),
inference(superposition,[],[f1259,f20]) ).
fof(f1401,plain,
! [X0,X1] : join(one,join(X0,top)) = join(one,join(X1,join(complement(X1),X0))),
inference(superposition,[],[f1169,f30]) ).
fof(f1404,plain,
! [X0,X1] : join(one,join(X0,converse(top))) = join(one,join(X1,join(converse(complement(converse(X1))),X0))),
inference(superposition,[],[f1169,f59]) ).
fof(f1993,plain,
! [X0] : join(one,join(X0,top)) = join(one,join(complement(complement(X0)),top)),
inference(superposition,[],[f1401,f30]) ).
fof(f2076,plain,
! [X0] : join(one,join(X0,top)) = join(one,join(top,complement(complement(X0)))),
inference(forward_demodulation,[],[f1993,f1165]) ).
fof(f18438,plain,
! [X0,X1] : join(one,converse(join(X0,top))) = join(one,converse(join(X1,join(complement(X1),X0)))),
inference(superposition,[],[f1271,f30]) ).
fof(f20834,plain,
! [X0] : join(one,converse(join(X0,top))) = join(one,converse(join(complement(complement(X0)),top))),
inference(superposition,[],[f18438,f30]) ).
fof(f21036,plain,
! [X0] : join(one,converse(join(X0,top))) = join(one,converse(join(top,complement(complement(X0))))),
inference(forward_demodulation,[],[f20834,f1259]) ).
fof(f30751,plain,
! [X0] : join(one,join(X0,converse(top))) = join(one,join(one,join(converse(complement(one)),X0))),
inference(superposition,[],[f1404,f236]) ).
fof(f32937,plain,
join(one,join(one,converse(top))) = join(one,join(converse(complement(converse(converse(complement(one))))),converse(top))),
inference(superposition,[],[f30751,f59]) ).
fof(f33115,plain,
join(one,join(one,converse(top))) = join(one,join(converse(top),converse(complement(converse(converse(complement(one))))))),
inference(forward_demodulation,[],[f32937,f1165]) ).
fof(f33166,plain,
join(one,join(one,converse(top))) = join(one,converse(join(top,complement(converse(converse(complement(one))))))),
inference(forward_demodulation,[],[f33115,f27]) ).
fof(f33195,plain,
join(one,join(one,converse(top))) = join(one,converse(join(top,complement(complement(one))))),
inference(forward_demodulation,[],[f33166,f26]) ).
fof(f33218,plain,
join(one,join(one,converse(top))) = join(one,converse(join(one,top))),
inference(forward_demodulation,[],[f33195,f21036]) ).
fof(f33306,plain,
join(converse(one),join(one,top)) = converse(join(one,join(one,converse(top)))),
inference(superposition,[],[f49,f33218]) ).
fof(f33340,plain,
join(one,join(one,top)) = converse(join(one,join(one,converse(top)))),
inference(forward_demodulation,[],[f33306,f236]) ).
fof(f39382,plain,
! [X0] : join(one,composition(X0,sK1)) = join(one,composition(join(converse(sK1),X0),sK1)),
inference(superposition,[],[f273,f25]) ).
fof(f39610,plain,
! [X0] : join(one,composition(converse(X0),sK1)) = join(one,composition(converse(join(sK1,X0)),sK1)),
inference(superposition,[],[f39382,f27]) ).
fof(f108708,plain,
! [X0,X1] : complement(X1) = join(complement(X1),composition(converse(X0),complement(composition(X0,X1)))),
inference(forward_demodulation,[],[f29,f19]) ).
fof(f115290,plain,
! [X0,X1] : join(one,join(X0,complement(X0))) = join(one,join(composition(converse(X1),complement(composition(X1,X0))),top)),
inference(superposition,[],[f1401,f108708]) ).
fof(f115424,plain,
! [X0,X1] : join(one,join(X0,complement(X0))) = join(one,join(top,composition(converse(X1),complement(composition(X1,X0))))),
inference(forward_demodulation,[],[f115290,f1165]) ).
fof(f115469,plain,
! [X0,X1] : join(one,top) = join(one,join(top,composition(converse(X1),complement(composition(X1,X0))))),
inference(forward_demodulation,[],[f115424,f30]) ).
fof(f115513,plain,
! [X0] : join(one,top) = join(one,join(top,complement(composition(one,X0)))),
inference(superposition,[],[f115469,f231]) ).
fof(f115588,plain,
! [X0] : join(one,top) = join(one,join(top,complement(X0))),
inference(forward_demodulation,[],[f115513,f243]) ).
fof(f115650,plain,
! [X0] : join(one,top) = join(one,join(X0,top)),
inference(superposition,[],[f115588,f2076]) ).
fof(f115906,plain,
! [X0] : join(one,top) = join(one,join(top,X0)),
inference(superposition,[],[f115650,f19]) ).
fof(f116334,plain,
join(one,top) = join(one,converse(top)),
inference(superposition,[],[f115906,f59]) ).
fof(f116735,plain,
join(one,join(one,top)) = converse(join(one,join(one,top))),
inference(superposition,[],[f33340,f116334]) ).
fof(f116815,plain,
join(one,top) = converse(join(one,top)),
inference(forward_demodulation,[],[f116735,f115650]) ).
fof(f117036,plain,
converse(top) = join(join(one,top),converse(complement(join(one,top)))),
inference(superposition,[],[f59,f116815]) ).
fof(f117073,plain,
converse(top) = join(one,join(top,converse(complement(join(one,top))))),
inference(forward_demodulation,[],[f117036,f20]) ).
fof(f117100,plain,
converse(top) = join(one,top),
inference(forward_demodulation,[],[f117073,f115906]) ).
fof(f117134,plain,
converse(top) = converse(converse(top)),
inference(superposition,[],[f116815,f117100]) ).
fof(f117152,plain,
converse(top) = join(one,converse(top)),
inference(superposition,[],[f115650,f117100]) ).
fof(f117240,plain,
top = converse(top),
inference(forward_demodulation,[],[f117134,f26]) ).
fof(f117804,plain,
top = join(one,top),
inference(forward_demodulation,[],[f117152,f117240]) ).
fof(f117831,plain,
! [X0] : join(top,X0) = join(one,join(top,X0)),
inference(superposition,[],[f20,f117804]) ).
fof(f117904,plain,
! [X0] : join(top,X0) = join(one,top),
inference(forward_demodulation,[],[f117831,f115906]) ).
fof(f117955,plain,
! [X0] : converse(top) = join(top,X0),
inference(forward_demodulation,[],[f117904,f117100]) ).
fof(f117991,plain,
! [X0] : top = join(top,X0),
inference(forward_demodulation,[],[f117955,f117240]) ).
fof(f122155,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))) = X0,
inference(forward_demodulation,[],[f21,f19]) ).
fof(f130631,plain,
! [X0,X1] : join(complement(join(X0,complement(X1))),complement(join(complement(X1),complement(X0)))) = X1,
inference(superposition,[],[f122155,f19]) ).
fof(f130634,plain,
! [X0] : join(complement(converse(top)),complement(join(complement(X0),complement(converse(complement(converse(complement(X0)))))))) = X0,
inference(superposition,[],[f122155,f59]) ).
fof(f130637,plain,
! [X0] : join(complement(join(complement(X0),top)),complement(join(complement(X0),zero))) = X0,
inference(superposition,[],[f122155,f46]) ).
fof(f130733,plain,
! [X0] : join(complement(join(complement(X0),top)),complement(join(zero,complement(X0)))) = X0,
inference(forward_demodulation,[],[f130637,f19]) ).
fof(f130735,plain,
! [X0] : join(complement(top),complement(join(complement(X0),complement(converse(complement(converse(complement(X0)))))))) = X0,
inference(forward_demodulation,[],[f130634,f117240]) ).
fof(f130773,plain,
! [X0] : join(complement(join(zero,complement(X0))),complement(join(complement(X0),top))) = X0,
inference(forward_demodulation,[],[f130733,f19]) ).
fof(f130775,plain,
! [X0] : join(zero,complement(join(complement(X0),complement(converse(complement(converse(complement(X0)))))))) = X0,
inference(forward_demodulation,[],[f130735,f46]) ).
fof(f130796,plain,
! [X0] : join(complement(join(zero,complement(X0))),complement(join(top,complement(X0)))) = X0,
inference(forward_demodulation,[],[f130773,f19]) ).
fof(f130810,plain,
! [X0] : join(complement(join(top,complement(X0))),complement(join(zero,complement(X0)))) = X0,
inference(forward_demodulation,[],[f130796,f19]) ).
fof(f130818,plain,
! [X0] : join(complement(top),complement(join(zero,complement(X0)))) = X0,
inference(forward_demodulation,[],[f130810,f117991]) ).
fof(f130820,plain,
! [X0] : join(zero,complement(join(zero,complement(X0)))) = X0,
inference(forward_demodulation,[],[f130818,f46]) ).
fof(f130974,plain,
zero = join(zero,complement(top)),
inference(superposition,[],[f130820,f30]) ).
fof(f131096,plain,
zero = join(zero,zero),
inference(forward_demodulation,[],[f130974,f46]) ).
fof(f131143,plain,
! [X0] : join(zero,X0) = join(zero,join(zero,X0)),
inference(superposition,[],[f20,f131096]) ).
fof(f131230,plain,
! [X0] : join(zero,X0) = X0,
inference(superposition,[],[f131143,f130820]) ).
fof(f131459,plain,
! [X0] : join(X0,zero) = X0,
inference(superposition,[],[f131230,f19]) ).
fof(f131480,plain,
! [X0] : complement(join(zero,complement(X0))) = X0,
inference(superposition,[],[f130820,f131230]) ).
fof(f132136,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_demodulation,[],[f131480,f131230]) ).
fof(f133056,plain,
! [X0,X1] : join(X0,composition(converse(X1),complement(composition(X1,complement(X0))))) = X0,
inference(superposition,[],[f108708,f132136]) ).
fof(f142444,plain,
! [X0] : join(X0,complement(composition(one,complement(X0)))) = X0,
inference(superposition,[],[f133056,f231]) ).
fof(f142838,plain,
! [X0] : join(X0,complement(complement(X0))) = X0,
inference(forward_demodulation,[],[f142444,f243]) ).
fof(f142967,plain,
! [X0] : join(X0,X0) = X0,
inference(forward_demodulation,[],[f142838,f132136]) ).
fof(f143073,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X0,X1)),
inference(superposition,[],[f20,f142967]) ).
fof(f144038,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),X0) = X0,
inference(superposition,[],[f143073,f122155]) ).
fof(f145966,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),X1))) = X0,
inference(forward_demodulation,[],[f144038,f19]) ).
fof(f151204,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X0,X1))),
inference(superposition,[],[f145966,f132136]) ).
fof(f153949,plain,
! [X0] : complement(join(complement(X0),complement(converse(complement(converse(complement(X0))))))) = X0,
inference(forward_demodulation,[],[f130775,f131230]) ).
fof(f163484,plain,
! [X0,X1] : top = join(X0,join(complement(X0),X1)),
inference(forward_demodulation,[],[f266,f117991]) ).
fof(f163495,plain,
! [X0,X1] : top = join(join(complement(X0),X1),X0),
inference(superposition,[],[f163484,f122155]) ).
fof(f164430,plain,
! [X0,X1] : top = join(complement(X0),join(X1,X0)),
inference(forward_demodulation,[],[f163495,f20]) ).
fof(f165725,plain,
! [X2,X0,X1] : top = join(complement(composition(X1,X2)),composition(join(X0,X1),X2)),
inference(superposition,[],[f164430,f25]) ).
fof(f348199,plain,
! [X0] : top = join(complement(composition(composition(converse(sK0),sK0),X0)),composition(one,X0)),
inference(superposition,[],[f165725,f37]) ).
fof(f349126,plain,
! [X0] : top = join(composition(one,X0),complement(composition(composition(converse(sK0),sK0),X0))),
inference(forward_demodulation,[],[f348199,f19]) ).
fof(f349922,plain,
! [X0] : top = join(composition(one,X0),complement(composition(converse(sK0),composition(sK0,X0)))),
inference(forward_demodulation,[],[f349126,f23]) ).
fof(f350449,plain,
! [X0] : top = join(X0,complement(composition(converse(sK0),composition(sK0,X0)))),
inference(forward_demodulation,[],[f349922,f243]) ).
fof(f982872,plain,
! [X0,X1] : join(X1,complement(X0)) = join(complement(join(join(complement(X0),complement(X1)),complement(join(X1,complement(X0))))),complement(X0)),
inference(superposition,[],[f130631,f130631]) ).
fof(f983380,plain,
! [X0,X1] : join(X1,complement(X0)) = join(complement(X0),complement(join(join(complement(X0),complement(X1)),complement(join(X1,complement(X0)))))),
inference(forward_demodulation,[],[f982872,f19]) ).
fof(f983727,plain,
! [X0,X1] : join(X1,complement(X0)) = join(complement(X0),complement(join(complement(X0),join(complement(X1),complement(join(X1,complement(X0))))))),
inference(forward_demodulation,[],[f983380,f20]) ).
fof(f983911,plain,
! [X0,X1] : join(X1,complement(X0)) = join(complement(X0),complement(join(complement(X0),complement(X1)))),
inference(forward_demodulation,[],[f983727,f151204]) ).
fof(f1086032,plain,
! [X0,X1] : join(X1,X0) = join(X0,complement(join(X0,complement(X1)))),
inference(superposition,[],[f983911,f153949]) ).
fof(f1087275,plain,
! [X0] : join(X0,complement(top)) = join(composition(converse(sK0),composition(sK0,X0)),X0),
inference(superposition,[],[f1086032,f350449]) ).
fof(f1088440,plain,
! [X0] : join(X0,complement(top)) = join(X0,composition(converse(sK0),composition(sK0,X0))),
inference(forward_demodulation,[],[f1087275,f19]) ).
fof(f1088789,plain,
! [X0] : join(X0,zero) = join(X0,composition(converse(sK0),composition(sK0,X0))),
inference(forward_demodulation,[],[f1088440,f46]) ).
fof(f1088965,plain,
! [X0] : join(X0,composition(converse(sK0),composition(sK0,X0))) = X0,
inference(forward_demodulation,[],[f1088789,f131459]) ).
fof(f1089679,plain,
join(one,composition(converse(sK1),sK1)) = join(one,composition(converse(composition(converse(sK0),composition(sK0,sK1))),sK1)),
inference(superposition,[],[f39610,f1088965]) ).
fof(f1089680,plain,
join(one,composition(converse(sK1),sK1)) = join(one,composition(composition(converse(composition(sK0,sK1)),sK0),sK1)),
inference(forward_demodulation,[],[f1089679,f55]) ).
fof(f1090024,plain,
join(one,composition(converse(sK1),sK1)) = join(one,composition(converse(composition(sK0,sK1)),composition(sK0,sK1))),
inference(forward_demodulation,[],[f1089680,f23]) ).
fof(f1090189,plain,
one = join(one,composition(converse(composition(sK0,sK1)),composition(sK0,sK1))),
inference(forward_demodulation,[],[f1090024,f36]) ).
fof(f1090241,plain,
$false,
inference(forward_subsumption_resolution,[],[f1090189,f40]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL031+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.38 % Computer : n007.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 22:52:38 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.15/0.44 Running first-order model finding
% 0.15/0.44 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
% 29.48/4.69 % (1863819)Will run a generic schedule for satisfiability detection.
% 29.48/4.69 % (1863824)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2193775535_2999 on theBenchmark for (2999ds/0Mi)
% 29.48/4.69 % TRYING [1]
% 29.48/4.69 % TRYING [2]
% 29.48/4.69 % TRYING [3]
% 29.48/4.69 % (1863825)% WARNING: option uhcvi not known.
% 29.48/4.69 % TRYING [4]
% 29.48/4.69 % (1863825)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3642328180:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 29.48/4.69 % (1863827)dis+10_1_sil=32000:sp=arity:random_seed=370595303:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 29.48/4.69 % (1863828)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=570624278:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 29.48/4.69 % (1863830)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=492994532:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 29.48/4.69 % (1863826)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2086133912:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 29.48/4.69 % (1863829)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3964102960:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 29.48/4.69 % TRYING [5]
% 29.48/4.69 % (1863827)Instruction limit reached!
% 29.48/4.69 % (1863827)------------------------------
% 29.48/4.69 % (1863827)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.48/4.69 % (1863827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.48/4.69 % (1863827)CaDiCaL version: 2.1.3
% 29.48/4.69 % (1863827)Termination reason: Instruction limit
% 29.48/4.69 % (1863827)Termination phase: Saturation
% 29.48/4.69 % (1863827)Time elapsed: 0.109 s
% 29.48/4.69 % (1863827)Peak memory usage: 12 MB
% 29.48/4.69 % (1863827)Instructions burned: 107 (million)
% 29.48/4.69 % (1863828)Instruction limit reached!
% 29.48/4.69 % (1863828)------------------------------
% 29.48/4.69 % (1863828)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.48/4.69 % (1863828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.48/4.69 % (1863828)CaDiCaL version: 2.1.3
% 29.48/4.69 % (1863828)Termination reason: Instruction limit
% 29.48/4.69 % (1863828)Termination phase: Saturation
% 29.48/4.69 % (1863828)Time elapsed: 0.125 s
% 29.48/4.69 % (1863828)Peak memory usage: 12 MB
% 29.48/4.69 % (1863828)Instructions burned: 116 (million)
% 29.48/4.69 % (1863829)Instruction limit reached!
% 29.48/4.69 % (1863829)------------------------------
% 29.48/4.69 % (1863829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.48/4.69 % (1863829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.48/4.69 % (1863829)CaDiCaL version: 2.1.3
% 29.48/4.69 % (1863829)Termination reason: Instruction limit
% 29.48/4.69 % (1863829)Termination phase: Saturation
% 29.48/4.69 % (1863829)Time elapsed: 0.137 s
% 29.48/4.69 % (1863829)Peak memory usage: 12 MB
% 29.48/4.69 % (1863829)Instructions burned: 131 (million)
% 29.48/4.69 % (1863838)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3016678547:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 29.48/4.69 % TRYING [1]
% 29.48/4.69 % TRYING [2]
% 29.48/4.69 % (1863830)Instruction limit reached!
% 29.48/4.69 % (1863830)------------------------------
% 29.48/4.69 % (1863830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.48/4.69 % (1863830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.48/4.69 % (1863830)CaDiCaL version: 2.1.3
% 29.48/4.69 % (1863830)Termination reason: Instruction limit
% 29.48/4.69 % (1863830)Termination phase: Saturation
% 29.48/4.69 % (1863830)Time elapsed: 0.162 s
% 29.48/4.69 % (1863830)Peak memory usage: 13 MB
% 29.48/4.69 % (1863830)Instructions burned: 160 (million)
% 29.48/4.69 % TRYING [3]
% 29.48/4.69 % (1863839)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1178226179:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 29.48/4.69 % TRYING [4]
% 29.48/4.69 % (1863840)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=4064973550:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 29.48/4.69 % TRYING [6]
% 29.48/4.69 % (1863842)ott-21_1_sil=16000:fs=off:random_seed=1890870591:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 29.48/4.69 % TRYING [5]
% 29.48/4.69 % (1863839)Instruction limit reached!
% 29.48/4.69 % (1863839)------------------------------
% 29.48/4.69 % (1863839)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 69.98/10.32 % (1863839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.98/10.32 % (1863839)CaDiCaL version: 2.1.3
% 69.98/10.32 % (1863839)Termination reason: Instruction limit
% 69.98/10.32 % (1863839)Termination phase: Saturation
% 69.98/10.32 % (1863839)Time elapsed: 0.148 s
% 69.98/10.32 % (1863839)Peak memory usage: 13 MB
% 69.98/10.32 % (1863839)Instructions burned: 131 (million)
% 69.98/10.32 % (1863846)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2978261377:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 69.98/10.32 % (1863842)Instruction limit reached!
% 69.98/10.32 % (1863842)------------------------------
% 69.98/10.32 % (1863842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 69.98/10.32 % (1863842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.98/10.32 % (1863842)CaDiCaL version: 2.1.3
% 69.98/10.32 % (1863842)Termination reason: Instruction limit
% 69.98/10.32 % (1863842)Termination phase: Saturation
% 69.98/10.32 % (1863842)Time elapsed: 0.157 s
% 69.98/10.32 % (1863842)Peak memory usage: 12 MB
% 69.98/10.32 % (1863842)Instructions burned: 180 (million)
% 69.98/10.32 % (1863848)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=707787470:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi)
% 69.98/10.32 % TRYING [1]
% 69.98/10.32 % TRYING [2]
% 69.98/10.32 % TRYING [3]
% 69.98/10.32 % TRYING [4]
% 69.98/10.32 % TRYING [5]
% 69.98/10.32 % TRYING [6]
% 69.98/10.32 % (1863838)Instruction limit reached!
% 69.98/10.32 % (1863838)------------------------------
% 69.98/10.32 % (1863838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 69.98/10.32 % (1863838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.98/10.32 % (1863838)CaDiCaL version: 2.1.3
% 69.98/10.32 % (1863838)Termination reason: Instruction limit
% 69.98/10.32 % (1863838)Termination phase: Finite model building constraint generation
% 69.98/10.32 % (1863838)Time elapsed: 0.606 s
% 69.98/10.32 % (1863838)Peak memory usage: 23 MB
% 69.98/10.32 % (1863838)Instructions burned: 714 (million)
% 69.98/10.32 % (1863840)Instruction limit reached!
% 69.98/10.32 % (1863840)------------------------------
% 69.98/10.32 % (1863840)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 69.98/10.32 % (1863840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.98/10.32 % (1863840)CaDiCaL version: 2.1.3
% 69.98/10.32 % (1863840)Termination reason: Instruction limit
% 69.98/10.32 % (1863840)Termination phase: Saturation
% 69.98/10.32 % (1863840)Time elapsed: 0.627 s
% 69.98/10.32 % (1863840)Peak memory usage: 17 MB
% 69.98/10.32 % (1863840)Instructions burned: 684 (million)
% 69.98/10.32 % (1863850)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=138507071:i=1179_2991 on theBenchmark for (2991ds/1179Mi)
% 69.98/10.32 % TRYING [7]
% 69.98/10.32 % (1863846)Instruction limit reached!
% 69.98/10.32 % (1863846)------------------------------
% 69.98/10.32 % (1863846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 69.98/10.32 % (1863846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.98/10.32 % (1863846)CaDiCaL version: 2.1.3
% 69.98/10.32 % (1863846)Termination reason: Instruction limit
% 69.98/10.32 % (1863846)Termination phase: Saturation
% 69.98/10.32 % (1863846)Time elapsed: 0.456 s
% 69.98/10.32 % (1863846)Peak memory usage: 15 MB
% 69.98/10.32 % (1863846)Instructions burned: 478 (million)
% 69.98/10.32 % TRYING [6]
% 69.98/10.32 % (1863851)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1038263921:i=889:ins=1_2991 on theBenchmark for (2991ds/889Mi)
% 69.98/10.32 % (1863853)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=664355697:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2991 on theBenchmark for (2991ds/692Mi)
% 69.98/10.32 % (1863848)Instruction limit reached!
% 69.98/10.32 % (1863848)------------------------------
% 69.98/10.32 % (1863848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 69.98/10.32 % (1863848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.98/10.32 % (1863848)CaDiCaL version: 2.1.3
% 69.98/10.32 % (1863848)Termination reason: Instruction limit
% 69.98/10.32 % (1863848)Termination phase: Finite model building SAT solving
% 69.98/10.32 % (1863848)Time elapsed: 0.607 s
% 69.98/10.32 % (1863848)Peak memory usage: 22 MB
% 69.98/10.32 % (1863848)Instructions burned: 867 (million)
% 69.98/10.32 % TRYING [14]
% 69.98/10.32 % (1863856)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2931884616:i=879:kws=inv_precedence:fsr=off_2989 on theBenchmark for (2989ds/879Mi)
% 143.81/20.74 % (1863853)Instruction limit reached!
% 143.81/20.74 % (1863853)------------------------------
% 143.81/20.74 % (1863853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 143.81/20.74 % (1863853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.81/20.74 % (1863853)CaDiCaL version: 2.1.3
% 143.81/20.74 % (1863853)Termination reason: Instruction limit
% 143.81/20.74 % (1863853)Termination phase: Saturation
% 143.81/20.74 % (1863853)Time elapsed: 0.656 s
% 143.81/20.74 % (1863853)Peak memory usage: 16 MB
% 143.81/20.74 % (1863853)Instructions burned: 693 (million)
% 143.81/20.74 % (1863851)Instruction limit reached!
% 143.81/20.74 % (1863851)------------------------------
% 143.81/20.74 % (1863851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 143.81/20.74 % (1863851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.81/20.74 % (1863851)CaDiCaL version: 2.1.3
% 143.81/20.74 % (1863851)Termination reason: Instruction limit
% 143.81/20.74 % (1863851)Termination phase: Finite model building constraint generation
% 143.81/20.74 % (1863851)Time elapsed: 0.672 s
% 143.81/20.74 % (1863851)Peak memory usage: 82 MB
% 143.81/20.74 % (1863851)Instructions burned: 889 (million)
% 143.81/20.74 % (1863858)fmb+10_1_sil=64000:random_seed=3349739970:i=22061:nm=2:gsp=on_2984 on theBenchmark for (2984ds/22061Mi)
% 143.81/20.74 % TRYING [1]
% 143.81/20.74 % TRYING [2]
% 143.81/20.74 % TRYING [3]
% 143.81/20.74 % (1863859)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1509668266:i=9515:nm=5_2984 on theBenchmark for (2984ds/9515Mi)
% 143.81/20.74 % TRYING [20]
% 143.81/20.74 % TRYING [4]
% 143.81/20.74 % TRYING [5]
% 143.81/20.74 % (1863856)Instruction limit reached!
% 143.81/20.74 % (1863856)------------------------------
% 143.81/20.74 % (1863856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 143.81/20.74 % (1863856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.81/20.74 % (1863856)CaDiCaL version: 2.1.3
% 143.81/20.74 % (1863856)Termination reason: Instruction limit
% 143.81/20.74 % (1863856)Termination phase: Saturation
% 143.81/20.74 % (1863856)Time elapsed: 0.804 s
% 143.81/20.74 % (1863856)Peak memory usage: 18 MB
% 143.81/20.74 % (1863856)Instructions burned: 880 (million)
% 143.81/20.74 % (1863862)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3645938603:fmbsr=1.7:i=920_2980 on theBenchmark for (2980ds/920Mi)
% 143.81/20.74 % TRYING [8]
% 143.81/20.74 % (1863850)Instruction limit reached!
% 143.81/20.74 % (1863850)------------------------------
% 143.81/20.74 % (1863850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 143.81/20.74 % (1863850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.81/20.74 % (1863850)CaDiCaL version: 2.1.3
% 143.81/20.74 % TRYING [6]
% 143.81/20.74 % (1863850)Termination reason: Instruction limit
% 143.81/20.74 % (1863850)Termination phase: Saturation
% 143.81/20.74 % (1863850)Time elapsed: 1.187 s
% 143.81/20.74 % (1863850)Peak memory usage: 23 MB
% 143.81/20.74 % (1863850)Instructions burned: 1179 (million)
% 143.81/20.74 % (1863864)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4071505952:i=5131_2979 on theBenchmark for (2979ds/5131Mi)
% 143.81/20.74 % (1863862)Instruction limit reached!
% 143.81/20.74 % (1863862)------------------------------
% 143.81/20.74 % (1863862)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 143.81/20.74 % (1863862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.81/20.74 % (1863862)CaDiCaL version: 2.1.3
% 143.81/20.74 % (1863862)Termination reason: Instruction limit
% 143.81/20.74 % (1863862)Termination phase: Finite model building SAT solving
% 143.81/20.74 % (1863862)Time elapsed: 0.716 s
% 143.81/20.74 % (1863862)Peak memory usage: 65 MB
% 143.81/20.74 % (1863862)Instructions burned: 921 (million)
% 143.81/20.74 % (1863866)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1996579731:i=1472:ins=7:fdi=8:gsp=on_2972 on theBenchmark for (2972ds/1472Mi)
% 143.81/20.74 % TRYING [7]
% 143.81/20.74 % (1863866)Instruction limit reached!
% 143.81/20.74 % (1863866)------------------------------
% 143.81/20.74 % (1863866)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 143.81/20.74 % (1863866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.81/20.74 % (1863866)CaDiCaL version: 2.1.3
% 143.81/20.74 % (1863866)Termination reason: Instruction limit
% 143.81/20.74 % (1863866)Termination phase: Saturation
% 143.81/20.74 % (1863866)Time elapsed: 1.422 s
% 143.81/20.74 % (1863866)Peak memory usage: 26 MB
% 143.81/20.74 % (1863866)Instructions burned: 1472 (million)
% 143.81/20.74 % (1863877)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3145412318:i=6324_2958 on theBenchmark for (2958ds/6324Mi)
% 94.08/35.28 % TRYING [77]
% 94.08/35.28 % TRYING [8]
% 94.08/35.28 % TRYING [8]
% 94.08/35.28 % (1863864)Instruction limit reached!
% 94.08/35.28 % (1863864)------------------------------
% 94.08/35.28 % (1863864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.08/35.28 % (1863864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.08/35.28 % (1863864)CaDiCaL version: 2.1.3
% 94.08/35.28 % (1863864)Termination reason: Instruction limit
% 94.08/35.28 % (1863864)Termination phase: Saturation
% 94.08/35.28 % (1863864)Time elapsed: 4.567 s
% 94.08/35.28 % (1863864)Peak memory usage: 51 MB
% 94.08/35.28 % (1863864)Instructions burned: 5131 (million)
% 94.08/35.28 % (1863972)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1532205675:fmbsr=2.30978:i=2174_2933 on theBenchmark for (2933ds/2174Mi)
% 94.08/35.28 % TRYING [16]
% 94.08/35.28 % (1863859)Instruction limit reached!
% 94.08/35.28 % (1863859)------------------------------
% 94.08/35.28 % (1863859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.08/35.28 % (1863859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.08/35.28 % (1863859)CaDiCaL version: 2.1.3
% 94.08/35.28 % (1863859)Termination reason: Instruction limit
% 94.08/35.28 % (1863859)Termination phase: Finite model building constraint generation
% 94.08/35.28 % (1863859)Time elapsed: 5.772 s
% 94.08/35.28 % (1863859)Peak memory usage: 671 MB
% 94.08/35.28 % (1863859)Instructions burned: 9518 (million)
% 94.08/35.28 % (1863972)Instruction limit reached!
% 94.08/35.28 % (1863972)------------------------------
% 94.08/35.28 % (1863972)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.08/35.28 % (1863972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.08/35.28 % (1863972)CaDiCaL version: 2.1.3
% 94.08/35.28 % (1863972)Termination reason: Instruction limit
% 94.08/35.28 % (1863972)Termination phase: Finite model building constraint generation
% 94.08/35.28 % (1863972)Time elapsed: 0.742 s
% 94.08/35.28 % (1863972)Peak memory usage: 135 MB
% 94.08/35.28 % (1863972)Instructions burned: 2177 (million)
% 94.08/35.28 % (1864035)ott-2_1_sil=16000:newcnf=on:random_seed=3483870140:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2925 on theBenchmark for (2925ds/869Mi)
% 94.08/35.28 % (1864037)ott+10_1_sil=32000:tgt=ground:random_seed=2768618918:i=5114:av=off_2924 on theBenchmark for (2924ds/5114Mi)
% 94.08/35.28 % (1863877)Instruction limit reached!
% 94.08/35.28 % (1863877)------------------------------
% 94.08/35.28 % (1863877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.08/35.28 % (1863877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.08/35.28 % (1863877)CaDiCaL version: 2.1.3
% 94.08/35.28 % (1863877)Termination reason: Instruction limit
% 94.08/35.28 % (1863877)Termination phase: Finite model building constraint generation
% 94.08/35.28 % (1863877)Time elapsed: 3.414 s
% 94.08/35.28 % (1863877)Peak memory usage: 515 MB
% 94.08/35.28 % (1863877)Instructions burned: 6324 (million)
% 94.08/35.28 % (1864039)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3940123290:i=54282_2922 on theBenchmark for (2922ds/54282Mi)
% 94.08/35.28 % TRYING [1]
% 94.08/35.28 % TRYING [2]
% 94.08/35.28 % TRYING [3]
% 94.08/35.28 % TRYING [4]
% 94.08/35.28 % TRYING [5]
% 94.08/35.28 % TRYING [6]
% 94.08/35.28 % (1864035)Instruction limit reached!
% 94.08/35.28 % (1864035)------------------------------
% 94.08/35.28 % (1864035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.08/35.28 % (1864035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.08/35.28 % (1864035)CaDiCaL version: 2.1.3
% 94.08/35.28 % (1864035)Termination reason: Instruction limit
% 94.08/35.28 % (1864035)Termination phase: Saturation
% 94.08/35.28 % (1864035)Time elapsed: 0.490 s
% 94.08/35.28 % (1864035)Peak memory usage: 18 MB
% 94.08/35.28 % (1864035)Instructions burned: 870 (million)
% 94.08/35.28 % (1864041)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2795174400:i=3512:aac=none_2920 on theBenchmark for (2920ds/3512Mi)
% 94.08/35.28 % TRYING [7]
% 94.08/35.28 % (1864041)Instruction limit reached!
% 94.08/35.28 % (1864041)------------------------------
% 94.08/35.28 % (1864041)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.08/35.28 % (1864041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.08/35.28 % (1864041)CaDiCaL version: 2.1.3
% 94.08/35.28 % (1864041)Termination reason: Instruction limit
% 94.08/35.28 % (1864041)Termination phase: Saturation
% 94.08/35.28 % (1864041)Time elapsed: 1.830 s
% 94.08/35.28 % (1864041)Peak memory usage: 41 MB
% 94.08/35.28 % (1864041)Instructions burned: 3514 (million)
% 94.08/35.28 % (1864043)dis+21_1_sil=32000:sas=cadical:random_seed=1107302849:i=3773:amm=off_2901 on theBenchmark for (2901ds/3773Mi)
% 94.08/35.28 % (1864037)Instruction limit reached!
% 94.08/35.28 % (1864037)------------------------------
% 94.08/35.28 % (1864037)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.08/35.28 % (1864037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.08/35.28 % (1864037)CaDiCaL version: 2.1.3
% 94.08/35.28 % (1864037)Termination reason: Instruction limit
% 94.08/35.28 % (1864037)Termination phase: Saturation
% 94.08/35.28 % (1864037)Time elapsed: 2.909 s
% 94.08/35.28 % (1864037)Peak memory usage: 59 MB
% 94.08/35.28 % (1864037)Instructions burned: 5114 (million)
% 94.08/35.28 % (1864045)ott+11_1_sil=16000:gs=on:random_seed=3441841367:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2895 on theBenchmark for (2895ds/2251Mi)
% 94.08/35.28 % TRYING [9]
% 94.08/35.28 % (1864045)Instruction limit reached!
% 94.08/35.28 % (1864045)------------------------------
% 94.08/35.28 % (1864045)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.08/35.28 % (1864045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.08/35.28 % (1864045)CaDiCaL version: 2.1.3
% 94.08/35.28 % (1864045)Termination reason: Instruction limit
% 94.08/35.28 % (1864045)Termination phase: Saturation
% 94.08/35.28 % (1864045)Time elapsed: 1.179 s
% 94.08/35.28 % (1864045)Peak memory usage: 24 MB
% 94.08/35.28 % (1864045)Instructions burned: 2252 (million)
% 94.08/35.28 % (1864047)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=462027132:fmbsr=1.6:i=67534_2883 on theBenchmark for (2883ds/67534Mi)
% 94.08/35.28 % TRYING [7]
% 94.08/35.28 % (1864043)Instruction limit reached!
% 94.08/35.28 % (1864043)------------------------------
% 94.08/35.28 % (1864043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.08/35.28 % (1864043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.08/35.28 % (1864043)CaDiCaL version: 2.1.3
% 94.08/35.28 % (1864043)Termination reason: Instruction limit
% 94.08/35.28 % (1864043)Termination phase: Saturation
% 94.08/35.28 % (1864043)Time elapsed: 1.979 s
% 94.08/35.28 % (1864043)Peak memory usage: 42 MB
% 94.08/35.28 % (1864043)Instructions burned: 3773 (million)
% 94.08/35.28 % (1864049)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3076859600:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2881 on theBenchmark for (2881ds/4591Mi)
% 94.08/35.28 % TRYING [8]
% 94.08/35.28 % (1864049)Instruction limit reached!
% 94.08/35.28 % (1864049)------------------------------
% 94.08/35.28 % (1864049)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.08/35.28 % (1864049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.08/35.28 % (1864049)CaDiCaL version: 2.1.3
% 94.08/35.28 % (1864049)Termination reason: Instruction limit
% 94.08/35.28 % (1864049)Termination phase: Saturation
% 94.08/35.28 % (1864049)Time elapsed: 1.996 s
% 94.08/35.28 % (1864049)Peak memory usage: 35 MB
% 94.08/35.28 % (1864049)Instructions burned: 4591 (million)
% 94.08/35.28 % (1864051)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2284257906:i=29340_2861 on theBenchmark for (2861ds/29340Mi)
% 94.08/35.28 % TRYING [8]
% 94.08/35.28 % TRYING [9]
% 94.08/35.28 % (1863858)Instruction limit reached!
% 94.08/35.28 % (1863858)------------------------------
% 94.08/35.28 % (1863858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.08/35.28 % (1863858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.08/35.28 % (1863858)CaDiCaL version: 2.1.3
% 94.08/35.28 % (1863858)Termination reason: Instruction limit
% 94.08/35.28 % (1863858)Termination phase: Finite model building SAT solving
% 94.08/35.28 % (1863858)Time elapsed: 14.299 s
% 94.08/35.28 % (1863858)Peak memory usage: 101 MB
% 94.08/35.28 % (1863858)Instructions burned: 22065 (million)
% 94.08/35.28 % (1864191)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=461355885:i=5211_2840 on theBenchmark for (2840ds/5211Mi)
% 94.08/35.28 % (1864191)Instruction limit reached!
% 94.08/35.28 % (1864191)------------------------------
% 94.08/35.28 % (1864191)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.08/35.28 % (1864191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.08/35.28 % (1864191)CaDiCaL version: 2.1.3
% 94.08/35.28 % (1864191)Termination reason: Instruction limit
% 94.08/35.28 % (1864191)Termination phase: Saturation
% 94.08/35.28 % (1864191)Time elapsed: 4.274 s
% 94.08/35.28 % (1864191)Peak memory usage: 50 MB
% 94.08/35.28 % (1864191)Instructions burned: 5211 (million)
% 94.08/35.28 % (1864351)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2953910079:i=5497:nm=2_2797 on theBenchmark for (2797ds/5497Mi)
% 94.08/35.28 % TRYING [17]
% 94.08/35.28 % (1864351)Instruction limit reached!
% 94.08/35.28 % (1864351)------------------------------
% 94.08/35.28 % (1864351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.08/35.28 % (1864351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.08/35.28 % (1864351)CaDiCaL version: 2.1.3
% 94.08/35.28 % (1864351)Termination reason: Instruction limit
% 94.08/35.28 % (1864351)Termination phase: Finite model building constraint generation
% 94.08/35.28 % (1864351)Time elapsed: 4.069 s
% 94.08/35.28 % (1864351)Peak memory usage: 392 MB
% 94.08/35.28 % (1864351)Instructions burned: 5498 (million)
% 94.08/35.28 % (1864361)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=29816890:fmbsr=2:i=46332_2755 on theBenchmark for (2755ds/46332Mi)
% 94.08/35.28 % TRYING [15]
% 94.08/35.28 % TRYING [9]
% 94.08/35.28 % TRYING [9]
% 94.08/35.28 % (1863826) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1863819-1863826"...
% 94.08/35.28 % (1863826)...printing done.
% 94.08/35.28 % (1863826)Refutation found. Thanks to Tanya!
% 94.08/35.28 % SZS status Theorem for theBenchmark
% 94.08/35.28 % SZS output start Proof for theBenchmark
% See solution above
% 94.08/35.29 % (1863826)------------------------------
% 94.08/35.29 % (1863826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.08/35.29 % (1863826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.08/35.29 % (1863826)CaDiCaL version: 2.1.3
% 94.08/35.29 % (1863826)Termination reason: Refutation
% 94.08/35.29 % (1863826)Time elapsed: 34.448 s
% 94.08/35.29 % (1863826)Peak memory usage: 254 MB
% 94.08/35.29 % (1863826)Instructions burned: 52436 (million)
% 94.08/35.29 % (1863819)Success in time 34.827 s
% 94.08/35.29 % Vampire exiting
%------------------------------------------------------------------------------