%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : REL050-2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n020.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:09 PM UTC 2026
% Result : Unsatisfiable 24.71s 4.65s
% Output : Refutation 25.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 43
% Number of leaves : 21
% Syntax : Number of formulae : 190 ( 169 unt; 7 def)
% Number of atoms : 212 ( 183 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 46 ( 24 ~; 20 |; 0 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 3 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 9 con; 0-2 aty)
% Number of variables : 231 ( 0 sgn 231 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maddux1_join_commutativity_1) ).
fof(f2,axiom,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maddux2_join_associativity_2) ).
fof(f3,axiom,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maddux3_a_kind_of_de_Morgan_3) ).
fof(f4,plain,
! [X0,X1] : join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) = X0,
inference(reorient_equations,[],[f3]) ).
fof(f5,axiom,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maddux4_definiton_of_meet_4) ).
fof(f6,plain,
! [X0,X1] : complement(join(complement(X0),complement(X1))) = meet(X0,X1),
inference(reorient_equations,[],[f5]) ).
fof(f7,axiom,
! [X2,X0,X1] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',composition_associativity_5) ).
fof(f8,axiom,
! [X0] : composition(X0,one) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',composition_identity_6) ).
fof(f9,axiom,
! [X2,X0,X1] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',composition_distributivity_7) ).
fof(f10,axiom,
! [X0] : converse(converse(X0)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_idempotence_8) ).
fof(f11,axiom,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_additivity_9) ).
fof(f12,axiom,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_multiplicativity_10) ).
fof(f13,axiom,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_cancellativity_11) ).
fof(f14,plain,
! [X0,X1] : complement(X1) = join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)),
inference(reorient_equations,[],[f13]) ).
fof(f15,axiom,
! [X0] : top = join(X0,complement(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',def_top_12) ).
fof(f16,axiom,
! [X0] : zero = meet(X0,complement(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',def_zero_13) ).
fof(f17,negated_conjecture,
( join(complement(composition(sk1,top)),composition(complement(composition(sk1,top)),top)) != composition(complement(composition(sk1,top)),top)
| join(composition(complement(composition(sk1,top)),top),complement(composition(sk1,top))) != complement(composition(sk1,top)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals_14) ).
fof(f18,plain,
( composition(complement(composition(sk1,top)),top) != join(complement(composition(sk1,top)),composition(complement(composition(sk1,top)),top))
| complement(composition(sk1,top)) != join(composition(complement(composition(sk1,top)),top),complement(composition(sk1,top))) ),
inference(reorient_equations,[],[f17]) ).
fof(f19,plain,
! [X0] : zero = complement(join(complement(X0),complement(complement(X0)))),
inference(definition_unfolding,[],[f16,f6]) ).
fof(f20,definition,
sF0 = composition(sk1,top),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f21,plain,
composition(sk1,top) = sF0,
inference(reorient_equations,[],[f20]) ).
fof(f22,definition,
sF1 = complement(sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f23,plain,
complement(sF0) = sF1,
inference(reorient_equations,[],[f22]) ).
fof(f24,definition,
sF2 = composition(sF1,top),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f25,plain,
composition(sF1,top) = sF2,
inference(reorient_equations,[],[f24]) ).
fof(f26,definition,
sF3 = join(sF1,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f27,plain,
join(sF1,sF2) = sF3,
inference(reorient_equations,[],[f26]) ).
fof(f28,definition,
sF4 = join(sF2,sF1),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f29,plain,
join(sF2,sF1) = sF4,
inference(reorient_equations,[],[f28]) ).
fof(f30,plain,
( sF2 != sF3
| sF1 != sF4 ),
inference(definition_folding,[],[f18,f29,f23,f21,f25,f23,f21,f23,f21,f27,f25,f23,f21,f23,f21,f25,f23,f21]) ).
fof(f32,definition,
( spl5_1
<=> sF1 = sF4 ),
introduced(definition,[new_symbols(definition,[spl5_1])],[avatar_definition]) ).
fof(f34,plain,
( sF1 != sF4
| spl5_1 ),
inference(avatar_component_clause,[],[f32]) ).
fof(f36,definition,
( spl5_2
<=> sF2 = sF3 ),
introduced(definition,[new_symbols(definition,[spl5_2])],[avatar_definition]) ).
fof(f37,plain,
( sF2 = sF3
| ~ spl5_2 ),
inference(avatar_component_clause,[],[f36]) ).
fof(f39,plain,
( ~ spl5_1
| ~ spl5_2 ),
inference(avatar_split_clause,[],[f30,f36,f32]) ).
fof(f40,plain,
zero = complement(top),
inference(backward_demodulation,[],[f19,f15]) ).
fof(f41,plain,
sF3 = join(sF2,sF1),
inference(forward_demodulation,[],[f27,f1]) ).
fof(f42,plain,
sF3 = sF4,
inference(backward_demodulation,[],[f29,f41]) ).
fof(f43,plain,
( sF1 != sF3
| spl5_1 ),
inference(forward_demodulation,[],[f34,f42]) ).
fof(f55,plain,
! [X0,X1] : converse(join(converse(X0),X1)) = join(X0,converse(X1)),
inference(superposition,[],[f11,f10]) ).
fof(f56,plain,
! [X0,X1] : converse(join(X1,converse(X0))) = join(converse(X1),X0),
inference(superposition,[],[f11,f10]) ).
fof(f63,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(top,X1),
inference(superposition,[],[f2,f15]) ).
fof(f67,plain,
! [X0] : join(sF2,join(sF1,X0)) = join(sF3,X0),
inference(superposition,[],[f2,f41]) ).
fof(f72,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f1,f2]) ).
fof(f77,plain,
! [X0,X1] : join(complement(X0),complement(X1)) = join(complement(X0),complement(join(complement(join(complement(X0),complement(X1))),join(complement(X0),X1)))),
inference(superposition,[],[f4,f4]) ).
fof(f81,plain,
! [X0] : sF0 = join(complement(join(sF1,complement(X0))),complement(join(sF1,X0))),
inference(superposition,[],[f4,f23]) ).
fof(f88,plain,
! [X2,X0,X1] : join(X0,X2) = join(complement(join(complement(X0),complement(X1))),join(complement(join(complement(X0),X1)),X2)),
inference(superposition,[],[f2,f4]) ).
fof(f90,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))) = X0,
inference(superposition,[],[f1,f4]) ).
fof(f91,plain,
! [X2,X0,X1] : join(X0,X2) = join(complement(join(complement(X0),X1)),join(X2,complement(join(complement(X0),complement(X1))))),
inference(forward_demodulation,[],[f88,f72]) ).
fof(f96,plain,
! [X0] : sF0 = join(complement(join(sF1,X0)),complement(join(sF1,complement(X0)))),
inference(forward_demodulation,[],[f81,f1]) ).
fof(f100,plain,
! [X0,X1] : join(complement(X0),complement(X1)) = join(complement(X0),complement(join(join(complement(X0),X1),complement(join(complement(X0),complement(X1)))))),
inference(forward_demodulation,[],[f77,f1]) ).
fof(f104,plain,
! [X0,X1] : join(complement(X0),complement(X1)) = join(complement(X0),complement(join(complement(X0),join(X1,complement(join(complement(X0),complement(X1))))))),
inference(forward_demodulation,[],[f100,f2]) ).
fof(f105,plain,
! [X0,X1] : converse(composition(X1,converse(X0))) = composition(X0,converse(X1)),
inference(superposition,[],[f12,f10]) ).
fof(f106,plain,
! [X0,X1] : converse(composition(converse(X0),X1)) = composition(converse(X1),X0),
inference(superposition,[],[f12,f10]) ).
fof(f108,plain,
! [X2,X0,X1] : composition(join(converse(X1),X2),converse(X0)) = join(converse(composition(X0,X1)),composition(X2,converse(X0))),
inference(superposition,[],[f9,f12]) ).
fof(f109,plain,
! [X0,X1] : complement(X1) = join(composition(X0,complement(composition(converse(X0),X1))),complement(X1)),
inference(superposition,[],[f14,f10]) ).
fof(f116,plain,
! [X2,X0,X1] : join(complement(X0),X2) = join(composition(converse(X1),complement(composition(X1,X0))),join(complement(X0),X2)),
inference(superposition,[],[f2,f14]) ).
fof(f119,plain,
! [X2,X0,X1] : join(complement(X0),X2) = join(complement(X0),join(X2,composition(converse(X1),complement(composition(X1,X0))))),
inference(forward_demodulation,[],[f116,f72]) ).
fof(f124,plain,
! [X0,X1] : complement(X1) = join(complement(X1),composition(X0,complement(composition(converse(X0),X1)))),
inference(forward_demodulation,[],[f109,f1]) ).
fof(f129,plain,
! [X0] : zero = join(composition(converse(X0),complement(composition(X0,top))),zero),
inference(superposition,[],[f14,f40]) ).
fof(f136,plain,
! [X0] : zero = join(zero,composition(converse(X0),complement(composition(X0,top)))),
inference(forward_demodulation,[],[f129,f1]) ).
fof(f153,plain,
! [X2,X0,X1] : join(X0,X1) = join(complement(complement(X0)),join(X1,complement(join(complement(X0),complement(composition(X2,complement(composition(converse(X2),X0)))))))),
inference(superposition,[],[f91,f124]) ).
fof(f166,plain,
! [X0,X1] : join(X0,join(complement(X0),complement(X1))) = join(complement(join(complement(X0),X1)),top),
inference(superposition,[],[f91,f15]) ).
fof(f170,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),complement(complement(X1))))) = join(complement(join(complement(X0),X1)),X0),
inference(superposition,[],[f91,f4]) ).
fof(f177,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),complement(complement(X1))))) = join(X0,complement(join(complement(X0),X1))),
inference(forward_demodulation,[],[f170,f1]) ).
fof(f178,plain,
! [X0,X1] : join(X0,join(complement(X0),complement(X1))) = join(top,complement(join(complement(X0),X1))),
inference(forward_demodulation,[],[f166,f1]) ).
fof(f186,plain,
! [X0,X1] : join(top,complement(join(complement(X0),X1))) = join(top,complement(X1)),
inference(forward_demodulation,[],[f178,f63]) ).
fof(f199,plain,
! [X2,X0,X1] : composition(join(converse(X2),converse(X1)),converse(X0)) = join(converse(composition(X0,X2)),converse(composition(X0,X1))),
inference(superposition,[],[f108,f12]) ).
fof(f205,plain,
! [X2,X0,X1] : composition(join(converse(X2),converse(X1)),converse(X0)) = converse(join(composition(X0,X2),composition(X0,X1))),
inference(forward_demodulation,[],[f199,f11]) ).
fof(f208,plain,
! [X2,X0,X1] : converse(join(composition(X0,X2),composition(X0,X1))) = composition(converse(join(X2,X1)),converse(X0)),
inference(forward_demodulation,[],[f205,f11]) ).
fof(f210,plain,
! [X2,X0,X1] : converse(join(composition(X0,X2),composition(X0,X1))) = converse(composition(X0,join(X2,X1))),
inference(forward_demodulation,[],[f208,f12]) ).
fof(f223,plain,
! [X2,X0,X1] : join(composition(X0,X1),composition(X0,X2)) = converse(converse(composition(X0,join(X1,X2)))),
inference(superposition,[],[f10,f210]) ).
fof(f236,plain,
! [X2,X0,X1] : composition(X0,join(X1,X2)) = join(composition(X0,X1),composition(X0,X2)),
inference(forward_demodulation,[],[f223,f10]) ).
fof(f258,plain,
! [X0,X1] : composition(X0,join(one,X1)) = join(X0,composition(X0,X1)),
inference(superposition,[],[f236,f8]) ).
fof(f259,plain,
! [X0] : composition(sF1,join(X0,top)) = join(composition(sF1,X0),sF2),
inference(superposition,[],[f236,f25]) ).
fof(f260,plain,
! [X0] : composition(sk1,join(X0,top)) = join(composition(sk1,X0),sF0),
inference(superposition,[],[f236,f21]) ).
fof(f267,plain,
! [X2,X3,X0,X1] : join(composition(X0,join(X1,X2)),X3) = join(composition(X0,X1),join(composition(X0,X2),X3)),
inference(superposition,[],[f2,f236]) ).
fof(f271,plain,
! [X0] : join(sF0,composition(sk1,X0)) = composition(sk1,join(X0,top)),
inference(forward_demodulation,[],[f260,f1]) ).
fof(f272,plain,
! [X0] : join(sF2,composition(sF1,X0)) = composition(sF1,join(X0,top)),
inference(forward_demodulation,[],[f259,f1]) ).
fof(f276,plain,
join(sF2,sF1) = composition(sF1,join(one,top)),
inference(superposition,[],[f272,f8]) ).
fof(f278,plain,
sF3 = composition(sF1,join(one,top)),
inference(forward_demodulation,[],[f276,f41]) ).
fof(f295,plain,
! [X0] : composition(sk1,composition(top,X0)) = composition(sF0,X0),
inference(superposition,[],[f7,f21]) ).
fof(f316,plain,
! [X0] : join(top,X0) = join(top,join(zero,X0)),
inference(superposition,[],[f63,f40]) ).
fof(f322,plain,
! [X0] : join(X0,top) = join(top,complement(complement(X0))),
inference(superposition,[],[f63,f15]) ).
fof(f338,plain,
! [X0] : join(top,X0) = join(zero,join(X0,top)),
inference(forward_demodulation,[],[f316,f72]) ).
fof(f346,plain,
! [X0,X1] : join(top,complement(complement(X0))) = join(top,complement(composition(X1,complement(composition(converse(X1),X0))))),
inference(superposition,[],[f186,f124]) ).
fof(f350,plain,
! [X0] : join(top,complement(top)) = join(top,complement(complement(complement(X0)))),
inference(superposition,[],[f186,f15]) ).
fof(f357,plain,
! [X0] : join(complement(X0),top) = join(top,complement(top)),
inference(forward_demodulation,[],[f350,f322]) ).
fof(f359,plain,
! [X0,X1] : join(X0,top) = join(top,complement(composition(X1,complement(composition(converse(X1),X0))))),
inference(forward_demodulation,[],[f346,f322]) ).
fof(f362,plain,
! [X0] : top = join(complement(X0),top),
inference(forward_demodulation,[],[f357,f15]) ).
fof(f366,plain,
! [X0] : top = join(top,complement(X0)),
inference(forward_demodulation,[],[f362,f1]) ).
fof(f376,plain,
! [X0] : top = join(X0,top),
inference(backward_demodulation,[],[f359,f366]) ).
fof(f380,plain,
! [X0] : composition(sk1,top) = join(sF0,composition(sk1,X0)),
inference(backward_demodulation,[],[f271,f376]) ).
fof(f385,plain,
! [X0] : join(top,X0) = join(zero,top),
inference(backward_demodulation,[],[f338,f376]) ).
fof(f388,plain,
composition(sF1,top) = sF3,
inference(backward_demodulation,[],[f278,f376]) ).
fof(f394,plain,
sF2 = sF3,
inference(backward_demodulation,[],[f25,f388]) ).
fof(f396,plain,
! [X0] : top = join(top,X0),
inference(forward_demodulation,[],[f385,f376]) ).
fof(f401,plain,
! [X0] : sF0 = join(sF0,composition(sk1,X0)),
inference(forward_demodulation,[],[f380,f21]) ).
fof(f404,plain,
spl5_2,
inference(avatar_split_clause,[],[f394,f36]) ).
fof(f423,plain,
( sF3 = join(sF3,sF1)
| ~ spl5_2 ),
inference(backward_demodulation,[],[f41,f37]) ).
fof(f426,plain,
( ! [X0] : join(sF3,X0) = join(sF3,join(sF1,X0))
| ~ spl5_2 ),
inference(backward_demodulation,[],[f67,f37]) ).
fof(f459,plain,
! [X0] : converse(converse(X0)) = composition(converse(one),X0),
inference(superposition,[],[f106,f8]) ).
fof(f479,plain,
! [X0] : composition(converse(one),X0) = X0,
inference(forward_demodulation,[],[f459,f10]) ).
fof(f494,plain,
! [X0] : complement(X0) = join(complement(X0),composition(one,complement(X0))),
inference(superposition,[],[f124,f479]) ).
fof(f504,plain,
one = converse(one),
inference(superposition,[],[f8,f479]) ).
fof(f508,plain,
! [X0] : composition(one,X0) = X0,
inference(backward_demodulation,[],[f479,f504]) ).
fof(f520,plain,
! [X0] : complement(X0) = join(complement(X0),complement(X0)),
inference(backward_demodulation,[],[f494,f508]) ).
fof(f586,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))) = join(X0,complement(join(complement(X0),complement(X1)))),
inference(superposition,[],[f91,f520]) ).
fof(f588,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),complement(X1)))) = X0,
inference(forward_demodulation,[],[f586,f90]) ).
fof(f593,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),X1))) = X0,
inference(backward_demodulation,[],[f177,f588]) ).
fof(f613,plain,
! [X2,X0,X1] : join(complement(X0),X2) = join(join(complement(X0),X2),complement(join(X0,X1))),
inference(superposition,[],[f593,f91]) ).
fof(f615,plain,
! [X0,X1] : join(X1,complement(join(X0,complement(X1)))) = X1,
inference(superposition,[],[f593,f1]) ).
fof(f616,plain,
! [X0] : join(X0,complement(top)) = X0,
inference(superposition,[],[f593,f15]) ).
fof(f619,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),X0) = join(X0,X0),
inference(superposition,[],[f91,f593]) ).
fof(f630,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),X1))) = join(X0,X0),
inference(forward_demodulation,[],[f619,f1]) ).
fof(f633,plain,
! [X0] : join(X0,zero) = X0,
inference(forward_demodulation,[],[f616,f40]) ).
fof(f635,plain,
! [X0,X1] : join(complement(X0),complement(X1)) = join(complement(X0),complement(join(complement(X0),X1))),
inference(backward_demodulation,[],[f104,f615]) ).
fof(f636,plain,
! [X2,X0,X1] : join(complement(X0),X2) = join(complement(X0),join(X2,complement(join(X0,X1)))),
inference(forward_demodulation,[],[f613,f2]) ).
fof(f642,plain,
! [X0] : join(X0,X0) = X0,
inference(forward_demodulation,[],[f630,f593]) ).
fof(f643,plain,
! [X0,X1] : join(X0,X1) = join(complement(complement(X0)),X1),
inference(backward_demodulation,[],[f153,f636]) ).
fof(f688,plain,
! [X0,X1] : complement(X0) = join(complement(join(complement(complement(X0)),complement(X1))),complement(join(X0,X1))),
inference(superposition,[],[f4,f643]) ).
fof(f695,plain,
! [X0,X1] : complement(complement(X0)) = join(X0,complement(join(complement(complement(complement(X0))),X1))),
inference(superposition,[],[f593,f643]) ).
fof(f696,plain,
! [X0,X1] : complement(complement(X0)) = join(X0,complement(join(complement(X0),X1))),
inference(forward_demodulation,[],[f695,f643]) ).
fof(f700,plain,
! [X0,X1] : complement(X0) = join(complement(join(X0,X1)),complement(join(complement(complement(X0)),complement(X1)))),
inference(forward_demodulation,[],[f688,f1]) ).
fof(f707,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_demodulation,[],[f696,f593]) ).
fof(f709,plain,
! [X0,X1] : complement(X0) = join(complement(join(X0,X1)),complement(join(X0,complement(X1)))),
inference(forward_demodulation,[],[f700,f643]) ).
fof(f720,plain,
sF0 = complement(sF1),
inference(backward_demodulation,[],[f96,f709]) ).
fof(f731,plain,
! [X0] : join(complement(X0),complement(complement(complement(X0)))) = join(complement(X0),complement(top)),
inference(superposition,[],[f635,f15]) ).
fof(f741,plain,
! [X0] : join(complement(X0),complement(complement(complement(X0)))) = join(complement(X0),zero),
inference(forward_demodulation,[],[f731,f40]) ).
fof(f747,plain,
! [X0] : join(complement(X0),complement(complement(complement(X0)))) = join(zero,complement(X0)),
inference(forward_demodulation,[],[f741,f1]) ).
fof(f751,plain,
! [X0] : join(complement(X0),complement(X0)) = join(zero,complement(X0)),
inference(forward_demodulation,[],[f747,f707]) ).
fof(f754,plain,
! [X0] : complement(X0) = join(zero,complement(X0)),
inference(forward_demodulation,[],[f751,f642]) ).
fof(f771,plain,
top = complement(zero),
inference(superposition,[],[f15,f754]) ).
fof(f786,plain,
! [X0,X1] : join(X0,complement(X1)) = join(X0,complement(join(X0,X1))),
inference(superposition,[],[f635,f707]) ).
fof(f787,plain,
! [X0] : join(zero,X0) = X0,
inference(superposition,[],[f754,f707]) ).
fof(f788,plain,
! [X0] : zero = composition(converse(X0),complement(composition(X0,top))),
inference(backward_demodulation,[],[f136,f787]) ).
fof(f933,plain,
! [X0] : sF1 = join(sF1,complement(join(sF0,X0))),
inference(superposition,[],[f593,f720]) ).
fof(f1610,plain,
! [X0] : composition(X0,top) = join(X0,composition(X0,complement(one))),
inference(superposition,[],[f258,f15]) ).
fof(f1734,plain,
top = composition(top,top),
inference(superposition,[],[f396,f1610]) ).
fof(f1822,plain,
! [X0] : converse(top) = join(X0,converse(complement(converse(X0)))),
inference(superposition,[],[f55,f15]) ).
fof(f2334,plain,
! [X2,X3,X0,X1] : join(composition(X0,join(X3,X2)),composition(X1,X2)) = join(composition(X0,X3),composition(join(X0,X1),X2)),
inference(superposition,[],[f267,f9]) ).
fof(f3151,plain,
( ! [X0] : join(sF3,sF1) = join(sF3,complement(join(complement(sF1),X0)))
| ~ spl5_2 ),
inference(superposition,[],[f426,f593]) ).
fof(f3202,plain,
( ! [X0] : join(sF3,sF1) = join(sF3,complement(join(sF0,X0)))
| ~ spl5_2 ),
inference(forward_demodulation,[],[f3151,f720]) ).
fof(f3218,plain,
( ! [X0] : sF3 = join(sF3,complement(join(sF0,X0)))
| ~ spl5_2 ),
inference(forward_demodulation,[],[f3202,f423]) ).
fof(f3286,plain,
! [X0] : converse(top) = join(converse(top),X0),
inference(superposition,[],[f56,f396]) ).
fof(f3368,plain,
top = converse(top),
inference(superposition,[],[f376,f3286]) ).
fof(f3372,plain,
! [X0] : top = join(X0,converse(complement(converse(X0)))),
inference(backward_demodulation,[],[f1822,f3368]) ).
fof(f3432,plain,
! [X0] : composition(converse(X0),top) = converse(composition(top,X0)),
inference(superposition,[],[f106,f3368]) ).
fof(f3519,plain,
! [X0] : join(X0,complement(top)) = join(X0,complement(converse(complement(converse(X0))))),
inference(superposition,[],[f786,f3372]) ).
fof(f3554,plain,
! [X0] : join(X0,zero) = join(X0,complement(converse(complement(converse(X0))))),
inference(forward_demodulation,[],[f3519,f40]) ).
fof(f3578,plain,
! [X0] : join(X0,complement(converse(complement(converse(X0))))) = X0,
inference(forward_demodulation,[],[f3554,f633]) ).
fof(f3607,plain,
! [X2,X0,X1] : join(composition(X0,X1),composition(join(X0,X2),complement(X1))) = join(composition(X0,top),composition(X2,complement(X1))),
inference(superposition,[],[f2334,f15]) ).
fof(f5128,plain,
! [X0,X1] : composition(sk1,join(composition(top,X0),X1)) = join(composition(sF0,X0),composition(sk1,X1)),
inference(superposition,[],[f236,f295]) ).
fof(f5361,plain,
! [X0,X1] : join(composition(sF0,top),composition(composition(sk1,X1),complement(X0))) = join(composition(sF0,X0),composition(sF0,complement(X0))),
inference(superposition,[],[f3607,f401]) ).
fof(f5402,plain,
! [X0,X1] : join(composition(sF0,top),composition(composition(sk1,X1),complement(X0))) = composition(sF0,join(X0,complement(X0))),
inference(forward_demodulation,[],[f5361,f236]) ).
fof(f5460,plain,
! [X0,X1] : composition(sF0,top) = join(composition(sF0,top),composition(composition(sk1,X1),complement(X0))),
inference(forward_demodulation,[],[f5402,f15]) ).
fof(f5499,plain,
! [X0,X1] : composition(sF0,top) = join(composition(sF0,top),composition(sk1,composition(X1,complement(X0)))),
inference(forward_demodulation,[],[f5460,f7]) ).
fof(f5523,plain,
! [X0,X1] : composition(sF0,top) = composition(sk1,join(composition(top,top),composition(X1,complement(X0)))),
inference(forward_demodulation,[],[f5499,f5128]) ).
fof(f5534,plain,
! [X0,X1] : composition(sF0,top) = composition(sk1,join(top,composition(X1,complement(X0)))),
inference(forward_demodulation,[],[f5523,f1734]) ).
fof(f5544,plain,
composition(sk1,top) = composition(sF0,top),
inference(forward_demodulation,[],[f5534,f396]) ).
fof(f5547,plain,
sF0 = composition(sF0,top),
inference(forward_demodulation,[],[f5544,f21]) ).
fof(f5554,plain,
zero = composition(converse(sF0),complement(sF0)),
inference(superposition,[],[f788,f5547]) ).
fof(f5585,plain,
zero = composition(converse(sF0),sF1),
inference(forward_demodulation,[],[f5554,f23]) ).
fof(f5969,plain,
! [X0] : converse(converse(X0)) = join(X0,converse(complement(converse(complement(converse(converse(X0))))))),
inference(superposition,[],[f55,f3578]) ).
fof(f5976,plain,
! [X0] : join(X0,converse(complement(converse(complement(X0))))) = X0,
inference(forward_demodulation,[],[f5969,f10]) ).
fof(f7128,plain,
zero = converse(complement(converse(complement(zero)))),
inference(superposition,[],[f787,f5976]) ).
fof(f7135,plain,
zero = converse(complement(converse(top))),
inference(forward_demodulation,[],[f7128,f771]) ).
fof(f7158,plain,
zero = converse(complement(top)),
inference(forward_demodulation,[],[f7135,f3368]) ).
fof(f7212,plain,
zero = converse(zero),
inference(forward_demodulation,[],[f7158,f40]) ).
fof(f7659,plain,
converse(zero) = composition(converse(sF1),sF0),
inference(superposition,[],[f106,f5585]) ).
fof(f7695,plain,
zero = composition(converse(sF1),sF0),
inference(forward_demodulation,[],[f7659,f7212]) ).
fof(f13383,plain,
! [X0] : join(complement(sF0),X0) = join(complement(sF0),join(X0,composition(converse(converse(sF1)),complement(zero)))),
inference(superposition,[],[f119,f7695]) ).
fof(f13412,plain,
! [X0] : join(complement(sF0),X0) = join(complement(sF0),join(X0,composition(converse(converse(sF1)),top))),
inference(forward_demodulation,[],[f13383,f771]) ).
fof(f13431,plain,
! [X0] : join(complement(sF0),X0) = join(complement(sF0),join(X0,converse(composition(top,converse(sF1))))),
inference(forward_demodulation,[],[f13412,f3432]) ).
fof(f13442,plain,
! [X0] : join(complement(sF0),X0) = join(complement(sF0),join(X0,composition(sF1,converse(top)))),
inference(forward_demodulation,[],[f13431,f105]) ).
fof(f13447,plain,
! [X0] : join(complement(sF0),X0) = join(complement(sF0),join(X0,composition(sF1,top))),
inference(forward_demodulation,[],[f13442,f3368]) ).
fof(f13450,plain,
! [X0] : join(complement(sF0),X0) = join(complement(sF0),join(X0,sF3)),
inference(forward_demodulation,[],[f13447,f388]) ).
fof(f13453,plain,
! [X0] : join(complement(sF0),X0) = join(sF3,join(complement(sF0),X0)),
inference(forward_demodulation,[],[f13450,f72]) ).
fof(f13457,plain,
! [X0] : join(sF1,X0) = join(sF3,join(sF1,X0)),
inference(forward_demodulation,[],[f13453,f23]) ).
fof(f13459,plain,
( ! [X0] : join(sF1,X0) = join(sF3,X0)
| ~ spl5_2 ),
inference(forward_demodulation,[],[f13457,f426]) ).
fof(f13539,plain,
( ! [X0] : sF1 = join(sF3,complement(join(sF0,X0)))
| ~ spl5_2 ),
inference(backward_demodulation,[],[f933,f13459]) ).
fof(f13586,plain,
( sF1 = sF3
| ~ spl5_2 ),
inference(forward_demodulation,[],[f13539,f3218]) ).
fof(f13640,plain,
( $false
| spl5_1
| ~ spl5_2 ),
inference(forward_subsumption_resolution,[],[f13586,f43]) ).
fof(f13641,plain,
( spl5_1
| ~ spl5_2 ),
inference(avatar_contradiction_clause,[],[f13640]) ).
cnf(s1,plain,
( ~ spl5_1
| ~ spl5_2 ),
inference(sat_conversion,[],[f39]) ).
cnf(s2,plain,
spl5_2,
inference(sat_conversion,[],[f404]) ).
cnf(s7,plain,
( spl5_1
| ~ spl5_2 ),
inference(sat_conversion,[],[f13641]) ).
cnf(s8,plain,
spl5_1,
inference(rat,[],[s7,s2]) ).
cnf(s9,plain,
$false,
inference(rat,[],[s1,s2,s8]) ).
fof(f13690,plain,
$false,
inference(avatar_sat_refutation,[],[s9]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL050-2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.15/0.41 % Computer : n020.cluster.edu
% 0.15/0.41 % Model : x86_64 x86_64
% 0.15/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.41 % Memory : 8046.5625MB
% 0.15/0.41 % OS : Linux 6.8.0-71-generic
% 0.15/0.41 % CPULimit : 300
% 0.15/0.41 % WCLimit : 300
% 0.15/0.41 % DateTime : Sun Sep 27 22:58:04 UTC 2026
% 0.15/0.41 % CPUTime :
% 0.15/0.41 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.23/0.48 Running first-order theorem proving
% 0.23/0.48 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 17.58/3.69 % (3864231)Input is clausal, will run a generic CNF schedule.
% 17.58/3.69 % (3864240)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1066419980:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 17.58/3.69 % (3864242)dis-21_1_sil=8000:lcm=predicate:random_seed=3913846207:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 17.58/3.69 % (3864242)Refutation not found, incomplete strategy
% 17.58/3.69 % (3864242)------------------------------
% 17.58/3.69 % (3864242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.58/3.69 % (3864242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.58/3.69 % (3864242)CaDiCaL version: 2.1.3
% 17.58/3.69 % (3864242)Termination reason: Refutation not found, incomplete strategy
% 17.58/3.69 % (3864242)Time elapsed: 0.002 s
% 17.58/3.69 % (3864242)Peak memory usage: 88 MB
% 17.58/3.69 % (3864242)Instructions burned: 1 (million)
% 17.58/3.69 % (3864241)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=769528439:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 17.58/3.69 % (3864238)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1102986151:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 17.58/3.69 % (3864237)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3259265885:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 17.58/3.69 % (3864239)lrs+10_1_sil=8000:sp=occurrence:random_seed=1289108069:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 17.58/3.69 % (3864236)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=3352982455:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 17.58/3.69 % (3864240)Instruction limit reached!
% 17.58/3.69 % (3864240)------------------------------
% 17.58/3.69 % (3864240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.58/3.69 % (3864240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.58/3.69 % (3864240)CaDiCaL version: 2.1.3
% 17.58/3.69 % (3864240)Termination reason: Instruction limit
% 17.58/3.69 % (3864240)Termination phase: Saturation
% 17.58/3.69 % (3864240)Time elapsed: 0.116 s
% 17.58/3.69 % (3864240)Peak memory usage: 89 MB
% 17.58/3.69 % (3864240)Instructions burned: 115 (million)
% 17.58/3.69 % (3864239)Instruction limit reached!
% 17.58/3.69 % (3864239)------------------------------
% 17.58/3.69 % (3864239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.58/3.69 % (3864239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.58/3.69 % (3864239)CaDiCaL version: 2.1.3
% 17.58/3.69 % (3864239)Termination reason: Instruction limit
% 17.58/3.69 % (3864239)Termination phase: Saturation
% 17.58/3.69 % (3864239)Time elapsed: 0.102 s
% 17.58/3.69 % (3864239)Peak memory usage: 89 MB
% 17.58/3.69 % (3864239)Instructions burned: 107 (million)
% 17.58/3.69 % (3864241)Instruction limit reached!
% 17.58/3.69 % (3864241)------------------------------
% 17.58/3.69 % (3864241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.58/3.69 % (3864241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.58/3.69 % (3864241)CaDiCaL version: 2.1.3
% 17.58/3.69 % (3864241)Termination reason: Instruction limit
% 17.58/3.69 % (3864241)Termination phase: Saturation
% 17.58/3.69 % (3864241)Time elapsed: 0.163 s
% 17.58/3.69 % (3864241)Peak memory usage: 90 MB
% 17.58/3.69 % (3864241)Instructions burned: 181 (million)
% 17.58/3.69 % (3864242)------------------------------
% 17.58/3.69 % (3864242)------------------------------
% 17.58/3.69 % (3864251)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1941858204:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 17.58/3.69 % (3864250)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=1160881686:i=143:sd=2:aac=none:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/143Mi)
% 17.58/3.69 % (3864250)Refutation not found, incomplete strategy
% 17.58/3.69 % (3864250)------------------------------
% 17.58/3.69 % (3864250)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.58/3.69 % (3864250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.71/4.65 % (3864250)CaDiCaL version: 2.1.3
% 24.71/4.65 % (3864250)Termination reason: Refutation not found, incomplete strategy
% 24.71/4.65 % (3864250)Time elapsed: 0.003 s
% 24.71/4.65 % (3864250)Peak memory usage: 88 MB
% 24.71/4.65 % (3864250)Instructions burned: 1 (million)
% 24.71/4.65 % (3864251)Instruction limit reached!
% 24.71/4.65 % (3864251)------------------------------
% 24.71/4.65 % (3864251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.71/4.65 % (3864251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.71/4.65 % (3864251)CaDiCaL version: 2.1.3
% 24.71/4.65 % (3864251)Termination reason: Instruction limit
% 24.71/4.65 % (3864251)Termination phase: Saturation
% 24.71/4.65 % (3864251)Time elapsed: 0.108 s
% 24.71/4.65 % (3864251)Peak memory usage: 92 MB
% 24.71/4.65 % (3864251)Instructions burned: 190 (million)
% 24.71/4.65 % (3864252)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1693218358:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 24.71/4.65 % (3864253)lrs+10_64_to=lpo:sil=8000:random_seed=545789266:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 24.71/4.65 % (3864252)Instruction limit reached!
% 24.71/4.65 % (3864252)------------------------------
% 24.71/4.65 % (3864252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.71/4.65 % (3864252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.71/4.65 % (3864252)CaDiCaL version: 2.1.3
% 24.71/4.65 % (3864252)Termination reason: Instruction limit
% 24.71/4.65 % (3864252)Termination phase: Saturation
% 24.71/4.65 % (3864252)Time elapsed: 0.204 s
% 24.71/4.65 % (3864252)Peak memory usage: 91 MB
% 24.71/4.65 % (3864252)Instructions burned: 220 (million)
% 24.71/4.65 % (3864253)Instruction limit reached!
% 24.71/4.65 % (3864253)------------------------------
% 24.71/4.65 % (3864253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.71/4.65 % (3864253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.71/4.65 % (3864253)CaDiCaL version: 2.1.3
% 24.71/4.65 % (3864253)Termination reason: Instruction limit
% 24.71/4.65 % (3864253)Termination phase: Saturation
% 24.71/4.65 % (3864253)Time elapsed: 0.127 s
% 24.71/4.65 % (3864253)Peak memory usage: 89 MB
% 24.71/4.65 % (3864253)Instructions burned: 126 (million)
% 24.71/4.65 % (3864256)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=538586192:avsq=on:i=194:fgj=on:bd=preordered_2993 on theBenchmark for (2993ds/194Mi)
% 24.71/4.65 % (3864250)------------------------------
% 24.71/4.65 % (3864250)------------------------------
% 24.71/4.65 % (3864256)Instruction limit reached!
% 24.71/4.65 % (3864256)------------------------------
% 24.71/4.65 % (3864256)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.71/4.65 % (3864256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.71/4.65 % (3864256)CaDiCaL version: 2.1.3
% 24.71/4.65 % (3864256)Termination reason: Instruction limit
% 24.71/4.65 % (3864256)Termination phase: Saturation
% 24.71/4.65 % (3864256)Time elapsed: 0.114 s
% 24.71/4.65 % (3864256)Peak memory usage: 90 MB
% 24.71/4.65 % (3864256)Instructions burned: 196 (million)
% 24.71/4.65 % (3864259)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3367437313:i=157:gtg=all_2991 on theBenchmark for (2991ds/157Mi)
% 24.71/4.65 % (3864260)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=4194025228:i=3394:sd=4:ss=included:sgt=64_2991 on theBenchmark for (2991ds/3394Mi)
% 24.71/4.65 % (3864262)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=1835537386:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2990 on theBenchmark for (2990ds/106Mi)
% 24.71/4.65 % (3864263)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=82531826:i=107_2989 on theBenchmark for (2989ds/107Mi)
% 24.71/4.65 % (3864263)Refutation not found, incomplete strategy
% 24.71/4.65 % (3864263)------------------------------
% 24.71/4.65 % (3864263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.71/4.65 % (3864263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.71/4.65 % (3864263)CaDiCaL version: 2.1.3
% 24.71/4.65 % (3864263)Termination reason: Refutation not found, incomplete strategy
% 24.71/4.65 % (3864263)Time elapsed: 0.002 s
% 24.71/4.65 % (3864263)Peak memory usage: 88 MB
% 24.71/4.65 % (3864263)Instructions burned: 1 (million)
% 24.71/4.65 % (3864259)Instruction limit reached!
% 24.71/4.65 % (3864259)------------------------------
% 24.71/4.65 % (3864259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.71/4.65 % (3864259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.71/4.65 % (3864259)CaDiCaL version: 2.1.3
% 24.71/4.65 % (3864259)Termination reason: Instruction limit
% 24.71/4.65 % (3864259)Termination phase: Saturation
% 24.71/4.65 % (3864259)Time elapsed: 0.168 s
% 24.71/4.65 % (3864259)Peak memory usage: 91 MB
% 24.71/4.65 % (3864259)Instructions burned: 157 (million)
% 24.71/4.65 % (3864262)Instruction limit reached!
% 24.71/4.65 % (3864262)------------------------------
% 24.71/4.65 % (3864262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.71/4.65 % (3864262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.71/4.65 % (3864262)CaDiCaL version: 2.1.3
% 24.71/4.65 % (3864262)Termination reason: Instruction limit
% 24.71/4.65 % (3864262)Termination phase: Saturation
% 24.71/4.65 % (3864262)Time elapsed: 0.103 s
% 24.71/4.65 % (3864262)Peak memory usage: 89 MB
% 24.71/4.65 % (3864262)Instructions burned: 106 (million)
% 24.71/4.65 % (3864268)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1980257267:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2986 on theBenchmark for (2986ds/242Mi)
% 24.71/4.65 % (3864269)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2750056194:cond=fast:i=5208:av=off_2986 on theBenchmark for (2986ds/5208Mi)
% 24.71/4.65 % (3864263)------------------------------
% 24.71/4.65 % (3864263)------------------------------
% 24.71/4.65 % (3864268)Instruction limit reached!
% 24.71/4.65 % (3864268)------------------------------
% 24.71/4.65 % (3864268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.71/4.65 % (3864268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.71/4.65 % (3864268)CaDiCaL version: 2.1.3
% 24.71/4.65 % (3864268)Termination reason: Instruction limit
% 24.71/4.65 % (3864268)Termination phase: Saturation
% 24.71/4.65 % (3864268)Time elapsed: 0.214 s
% 24.71/4.65 % (3864268)Peak memory usage: 89 MB
% 24.71/4.65 % (3864268)Instructions burned: 243 (million)
% 24.71/4.65 % (3864272)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=4157516124:i=134:sd=2:doe=on:ss=axioms:sgt=14_2982 on theBenchmark for (2982ds/134Mi)
% 24.71/4.65 % (3864273)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=4048392696:i=499:bd=all_2981 on theBenchmark for (2981ds/499Mi)
% 24.71/4.65 % (3864272)Instruction limit reached!
% 24.71/4.65 % (3864272)------------------------------
% 24.71/4.65 % (3864272)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.71/4.65 % (3864272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.71/4.65 % (3864272)CaDiCaL version: 2.1.3
% 24.71/4.65 % (3864272)Termination reason: Instruction limit
% 24.71/4.65 % (3864272)Termination phase: Saturation
% 24.71/4.65 % (3864272)Time elapsed: 0.127 s
% 24.71/4.65 % (3864272)Peak memory usage: 89 MB
% 24.71/4.65 % (3864272)Instructions burned: 134 (million)
% 24.71/4.65 % (3864273)Instruction limit reached!
% 24.71/4.65 % (3864273)------------------------------
% 24.71/4.65 % (3864273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.71/4.65 % (3864273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.71/4.65 % (3864273)CaDiCaL version: 2.1.3
% 24.71/4.65 % (3864273)Termination reason: Instruction limit
% 24.71/4.65 % (3864273)Termination phase: Saturation
% 24.71/4.65 % (3864273)Time elapsed: 0.187 s
% 24.71/4.65 % (3864273)Peak memory usage: 94 MB
% 24.71/4.65 % (3864273)Instructions burned: 501 (million)
% 24.71/4.65 % (3864278)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2447281425:i=191:fgj=on:bd=all_2978 on theBenchmark for (2978ds/191Mi)
% 24.71/4.65 % (3864279)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=70023959:i=264:kws=precedence:fsr=off_2977 on theBenchmark for (2977ds/264Mi)
% 24.71/4.65 % (3864278)Instruction limit reached!
% 24.71/4.65 % (3864278)------------------------------
% 24.71/4.65 % (3864278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.71/4.65 % (3864278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.71/4.65 % (3864278)CaDiCaL version: 2.1.3
% 24.71/4.65 % (3864278)Termination reason: Instruction limit
% 24.71/4.65 % (3864278)Termination phase: Saturation
% 24.71/4.65 % (3864278)Time elapsed: 0.185 s
% 24.71/4.65 % (3864278)Peak memory usage: 90 MB
% 24.71/4.65 % (3864278)Instructions burned: 191 (million)
% 24.71/4.65 % (3864279)Instruction limit reached!
% 24.71/4.65 % (3864279)------------------------------
% 24.71/4.65 % (3864279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.71/4.65 % (3864279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.71/4.65 % (3864279)CaDiCaL version: 2.1.3
% 24.71/4.65 % (3864279)Termination reason: Instruction limit
% 24.71/4.65 % (3864279)Termination phase: Saturation
% 24.71/4.65 % (3864279)Time elapsed: 0.146 s
% 24.71/4.65 % (3864279)Peak memory usage: 92 MB
% 24.71/4.65 % (3864279)Instructions burned: 264 (million)
% 24.71/4.65 % (3864282)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2589543129:cond=on:i=156:bs=on:gtg=exists_all:er=known_2974 on theBenchmark for (2974ds/156Mi)
% 24.71/4.65 % (3864283)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=1811308841:i=3256:kws=precedence:bd=preordered:av=off_2973 on theBenchmark for (2973ds/3256Mi)
% 24.71/4.65 % (3864282)Instruction limit reached!
% 24.71/4.65 % (3864282)------------------------------
% 24.71/4.65 % (3864282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.71/4.65 % (3864282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.71/4.65 % (3864282)CaDiCaL version: 2.1.3
% 24.71/4.65 % (3864282)Termination reason: Instruction limit
% 24.71/4.65 % (3864282)Termination phase: Saturation
% 24.71/4.65 % (3864282)Time elapsed: 0.141 s
% 24.71/4.65 % (3864282)Peak memory usage: 89 MB
% 24.71/4.65 % (3864282)Instructions burned: 156 (million)
% 24.71/4.65 % (3864238)First to succeed.
% 24.71/4.65 % (3864238)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3864231"
% 24.71/4.65 % (3864286)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=4002493705:i=537:av=off:ss=included_2970 on theBenchmark for (2970ds/537Mi)
% 24.71/4.65 % (3864238)Refutation found. Thanks to Tanya!
% 24.71/4.65 % SZS status Unsatisfiable for theBenchmark
% 24.71/4.65 % SZS output start Proof for theBenchmark
% See solution above
% 25.78/4.92 % (3864238)------------------------------
% 25.78/4.92 % (3864238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.78/4.92 % (3864238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.78/4.92 % (3864238)CaDiCaL version: 2.1.3
% 25.78/4.92 % (3864238)Termination reason: Refutation
% 25.78/4.92 % (3864238)Time elapsed: 2.828 s
% 25.78/4.92 % (3864238)Peak memory usage: 145 MB
% 25.78/4.92 % (3864238)Instructions burned: 2622 (million)
% 25.78/4.92 % (3864238)------------------------------
% 25.78/4.92 % (3864238)------------------------------
% 25.78/4.92 % (3864231)Success in time 3.513 s
% 25.78/4.92 % Vampire exiting
%------------------------------------------------------------------------------