%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : REL016-1 : 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 : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:33:44 PM UTC 2026
% Result : Unsatisfiable 5.95s 1.99s
% Output : Refutation 8.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 51
% Syntax : Number of formulae : 244 ( 150 unt; 38 def)
% Number of atoms : 425 ( 189 equ)
% Maximal formula atoms : 9 ( 1 avg)
% Number of connectives : 345 ( 164 ~; 159 |; 0 &)
% ( 22 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 24 ( 22 usr; 23 prp; 0-2 aty)
% Number of functors : 27 ( 27 usr; 22 con; 0-2 aty)
% Number of variables : 142 ( 0 sgn 142 !; 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(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,
meet(composition(sk1,sk2),complement(composition(sk1,sk3))) != meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals_14) ).
fof(f18,plain,
! [X0] : zero = complement(join(complement(X0),complement(complement(X0)))),
inference(definition_unfolding,[],[f16,f6]) ).
fof(f19,plain,
complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))) != complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),
inference(definition_unfolding,[],[f17,f6,f6,f6]) ).
fof(f20,definition,
sF0 = composition(sk1,sk2),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f21,plain,
composition(sk1,sk2) = 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(sk1,sk3),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f25,plain,
composition(sk1,sk3) = sF2,
inference(reorient_equations,[],[f24]) ).
fof(f26,definition,
sF3 = complement(sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f27,plain,
complement(sF2) = sF3,
inference(reorient_equations,[],[f26]) ).
fof(f28,definition,
sF4 = complement(sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f29,plain,
complement(sF3) = sF4,
inference(reorient_equations,[],[f28]) ).
fof(f30,definition,
sF5 = join(sF1,sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f31,plain,
join(sF1,sF4) = sF5,
inference(reorient_equations,[],[f30]) ).
fof(f32,definition,
sF6 = complement(sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f33,plain,
complement(sF5) = sF6,
inference(reorient_equations,[],[f32]) ).
fof(f34,definition,
sF7 = complement(sk2),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f35,plain,
complement(sk2) = sF7,
inference(reorient_equations,[],[f34]) ).
fof(f36,definition,
sF8 = complement(sk3),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f37,plain,
complement(sk3) = sF8,
inference(reorient_equations,[],[f36]) ).
fof(f38,definition,
sF9 = complement(sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f39,plain,
complement(sF8) = sF9,
inference(reorient_equations,[],[f38]) ).
fof(f40,definition,
sF10 = join(sF7,sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f41,plain,
join(sF7,sF9) = sF10,
inference(reorient_equations,[],[f40]) ).
fof(f42,definition,
sF11 = complement(sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f43,plain,
complement(sF10) = sF11,
inference(reorient_equations,[],[f42]) ).
fof(f44,definition,
sF12 = composition(sk1,sF11),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f45,plain,
composition(sk1,sF11) = sF12,
inference(reorient_equations,[],[f44]) ).
fof(f46,definition,
sF13 = complement(sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f47,plain,
complement(sF12) = sF13,
inference(reorient_equations,[],[f46]) ).
fof(f48,definition,
sF14 = join(sF13,sF4),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f49,plain,
join(sF13,sF4) = sF14,
inference(reorient_equations,[],[f48]) ).
fof(f50,definition,
sF15 = complement(sF14),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f51,plain,
complement(sF14) = sF15,
inference(reorient_equations,[],[f50]) ).
fof(f52,plain,
sF6 != sF15,
inference(definition_folding,[],[f19,f51,f49,f29,f27,f25,f47,f45,f43,f41,f39,f37,f35,f33,f31,f29,f27,f25,f23,f21]) ).
fof(f54,definition,
( spl16_1
<=> complement(sF14) = sF15 ),
introduced(definition,[new_symbols(definition,[spl16_1])],[avatar_definition]) ).
fof(f56,plain,
( complement(sF14) = sF15
| ~ spl16_1 ),
inference(avatar_component_clause,[],[f54]) ).
fof(f57,plain,
spl16_1,
inference(avatar_split_clause,[],[f51,f54]) ).
fof(f59,definition,
( spl16_2
<=> complement(sF5) = sF6 ),
introduced(definition,[new_symbols(definition,[spl16_2])],[avatar_definition]) ).
fof(f61,plain,
( complement(sF5) = sF6
| ~ spl16_2 ),
inference(avatar_component_clause,[],[f59]) ).
fof(f62,plain,
spl16_2,
inference(avatar_split_clause,[],[f33,f59]) ).
fof(f75,plain,
! [X0,X1] : join(complement(join(complement(X0),complement(X1))),complement(join(complement(X1),X0))) = X1,
inference(superposition,[],[f4,f1]) ).
fof(f80,plain,
! [X0,X1] : join(complement(join(complement(X1),complement(X0))),complement(join(X0,complement(X1)))) = X1,
inference(superposition,[],[f4,f1]) ).
fof(f103,definition,
( spl16_3
<=> sF6 = sF15 ),
introduced(definition,[new_symbols(definition,[spl16_3])],[avatar_definition]) ).
fof(f105,plain,
( sF6 != sF15
| spl16_3 ),
inference(avatar_component_clause,[],[f103]) ).
fof(f106,plain,
~ spl16_3,
inference(avatar_split_clause,[],[f52,f103]) ).
fof(f108,definition,
( spl16_4
<=> complement(sk3) = sF8 ),
introduced(definition,[new_symbols(definition,[spl16_4])],[avatar_definition]) ).
fof(f110,plain,
( complement(sk3) = sF8
| ~ spl16_4 ),
inference(avatar_component_clause,[],[f108]) ).
fof(f111,plain,
spl16_4,
inference(avatar_split_clause,[],[f37,f108]) ).
fof(f118,definition,
( spl16_5
<=> complement(sk2) = sF7 ),
introduced(definition,[new_symbols(definition,[spl16_5])],[avatar_definition]) ).
fof(f120,plain,
( complement(sk2) = sF7
| ~ spl16_5 ),
inference(avatar_component_clause,[],[f118]) ).
fof(f121,plain,
spl16_5,
inference(avatar_split_clause,[],[f35,f118]) ).
fof(f128,definition,
( spl16_6
<=> complement(sF3) = sF4 ),
introduced(definition,[new_symbols(definition,[spl16_6])],[avatar_definition]) ).
fof(f130,plain,
( complement(sF3) = sF4
| ~ spl16_6 ),
inference(avatar_component_clause,[],[f128]) ).
fof(f131,plain,
spl16_6,
inference(avatar_split_clause,[],[f29,f128]) ).
fof(f139,definition,
( spl16_7
<=> complement(sF0) = sF1 ),
introduced(definition,[new_symbols(definition,[spl16_7])],[avatar_definition]) ).
fof(f141,plain,
( complement(sF0) = sF1
| ~ spl16_7 ),
inference(avatar_component_clause,[],[f139]) ).
fof(f142,plain,
spl16_7,
inference(avatar_split_clause,[],[f23,f139]) ).
fof(f150,definition,
( spl16_8
<=> complement(sF2) = sF3 ),
introduced(definition,[new_symbols(definition,[spl16_8])],[avatar_definition]) ).
fof(f152,plain,
( complement(sF2) = sF3
| ~ spl16_8 ),
inference(avatar_component_clause,[],[f150]) ).
fof(f153,plain,
spl16_8,
inference(avatar_split_clause,[],[f27,f150]) ).
fof(f161,definition,
( spl16_9
<=> complement(sF8) = sF9 ),
introduced(definition,[new_symbols(definition,[spl16_9])],[avatar_definition]) ).
fof(f163,plain,
( complement(sF8) = sF9
| ~ spl16_9 ),
inference(avatar_component_clause,[],[f161]) ).
fof(f164,plain,
spl16_9,
inference(avatar_split_clause,[],[f39,f161]) ).
fof(f172,definition,
( spl16_10
<=> complement(sF12) = sF13 ),
introduced(definition,[new_symbols(definition,[spl16_10])],[avatar_definition]) ).
fof(f174,plain,
( complement(sF12) = sF13
| ~ spl16_10 ),
inference(avatar_component_clause,[],[f172]) ).
fof(f175,plain,
spl16_10,
inference(avatar_split_clause,[],[f47,f172]) ).
fof(f183,definition,
( spl16_11
<=> complement(sF10) = sF11 ),
introduced(definition,[new_symbols(definition,[spl16_11])],[avatar_definition]) ).
fof(f185,plain,
( complement(sF10) = sF11
| ~ spl16_11 ),
inference(avatar_component_clause,[],[f183]) ).
fof(f186,plain,
spl16_11,
inference(avatar_split_clause,[],[f43,f183]) ).
fof(f200,definition,
( spl16_12
<=> composition(sk1,sk2) = sF0 ),
introduced(definition,[new_symbols(definition,[spl16_12])],[avatar_definition]) ).
fof(f202,plain,
( composition(sk1,sk2) = sF0
| ~ spl16_12 ),
inference(avatar_component_clause,[],[f200]) ).
fof(f203,plain,
spl16_12,
inference(avatar_split_clause,[],[f21,f200]) ).
fof(f211,plain,
! [X0,X1] : join(X0,complement(X0)) = join(X1,complement(X1)),
inference(superposition,[],[f15,f15]) ).
fof(f230,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(f237,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f1,f2]) ).
fof(f240,plain,
! [X2,X0,X1] : join(X0,X2) = join(complement(join(complement(X0),X1)),join(X2,complement(join(complement(X0),complement(X1))))),
inference(forward_demodulation,[],[f230,f237]) ).
fof(f246,definition,
( spl16_13
<=> composition(sk1,sk3) = sF2 ),
introduced(definition,[new_symbols(definition,[spl16_13])],[avatar_definition]) ).
fof(f248,plain,
( composition(sk1,sk3) = sF2
| ~ spl16_13 ),
inference(avatar_component_clause,[],[f246]) ).
fof(f249,plain,
spl16_13,
inference(avatar_split_clause,[],[f25,f246]) ).
fof(f269,definition,
( spl16_14
<=> join(sF7,sF9) = sF10 ),
introduced(definition,[new_symbols(definition,[spl16_14])],[avatar_definition]) ).
fof(f271,plain,
( join(sF7,sF9) = sF10
| ~ spl16_14 ),
inference(avatar_component_clause,[],[f269]) ).
fof(f272,plain,
spl16_14,
inference(avatar_split_clause,[],[f41,f269]) ).
fof(f275,definition,
( spl16_15
<=> composition(sk1,sF11) = sF12 ),
introduced(definition,[new_symbols(definition,[spl16_15])],[avatar_definition]) ).
fof(f277,plain,
( composition(sk1,sF11) = sF12
| ~ spl16_15 ),
inference(avatar_component_clause,[],[f275]) ).
fof(f278,plain,
spl16_15,
inference(avatar_split_clause,[],[f45,f275]) ).
fof(f286,definition,
( spl16_16
<=> join(sF1,sF4) = sF5 ),
introduced(definition,[new_symbols(definition,[spl16_16])],[avatar_definition]) ).
fof(f288,plain,
( join(sF1,sF4) = sF5
| ~ spl16_16 ),
inference(avatar_component_clause,[],[f286]) ).
fof(f289,plain,
spl16_16,
inference(avatar_split_clause,[],[f31,f286]) ).
fof(f292,definition,
( spl16_17
<=> join(sF13,sF4) = sF14 ),
introduced(definition,[new_symbols(definition,[spl16_17])],[avatar_definition]) ).
fof(f294,plain,
( join(sF13,sF4) = sF14
| ~ spl16_17 ),
inference(avatar_component_clause,[],[f292]) ).
fof(f295,plain,
spl16_17,
inference(avatar_split_clause,[],[f49,f292]) ).
fof(f310,plain,
! [X0] : join(zero,complement(join(complement(X0),complement(X0)))) = X0,
inference(superposition,[],[f4,f18]) ).
fof(f333,plain,
! [X0,X1] : composition(converse(X1),X0) = converse(composition(converse(X0),X1)),
inference(superposition,[],[f12,f10]) ).
fof(f336,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(f345,plain,
! [X2,X0,X1] : composition(join(converse(X2),converse(X1)),converse(X0)) = join(converse(composition(X0,X2)),converse(composition(X0,X1))),
inference(superposition,[],[f336,f12]) ).
fof(f355,plain,
! [X2,X0,X1] : composition(join(converse(X2),converse(X1)),converse(X0)) = converse(join(composition(X0,X2),composition(X0,X1))),
inference(forward_demodulation,[],[f345,f11]) ).
fof(f358,plain,
! [X2,X0,X1] : converse(join(composition(X0,X2),composition(X0,X1))) = composition(converse(join(X2,X1)),converse(X0)),
inference(forward_demodulation,[],[f355,f11]) ).
fof(f360,plain,
! [X2,X0,X1] : converse(join(composition(X0,X2),composition(X0,X1))) = converse(composition(X0,join(X2,X1))),
inference(forward_demodulation,[],[f358,f12]) ).
fof(f375,plain,
! [X2,X0,X1] : join(composition(X0,X1),composition(X0,X2)) = converse(converse(composition(X0,join(X1,X2)))),
inference(superposition,[],[f10,f360]) ).
fof(f387,plain,
! [X2,X0,X1] : composition(X0,join(X1,X2)) = join(composition(X0,X1),composition(X0,X2)),
inference(forward_demodulation,[],[f375,f10]) ).
fof(f413,plain,
( ! [X0] : composition(sk1,join(X0,sk2)) = join(composition(sk1,X0),sF0)
| ~ spl16_12 ),
inference(superposition,[],[f387,f202]) ).
fof(f415,plain,
( ! [X0] : composition(sk1,join(X0,sF11)) = join(composition(sk1,X0),sF12)
| ~ spl16_15 ),
inference(superposition,[],[f387,f277]) ).
fof(f428,plain,
( ! [X0] : join(sF12,composition(sk1,X0)) = composition(sk1,join(X0,sF11))
| ~ spl16_15 ),
inference(forward_demodulation,[],[f415,f1]) ).
fof(f430,plain,
( ! [X0] : join(sF0,composition(sk1,X0)) = composition(sk1,join(X0,sk2))
| ~ spl16_12 ),
inference(forward_demodulation,[],[f413,f1]) ).
fof(f458,plain,
( sk2 = join(zero,complement(join(sF7,sF7)))
| ~ spl16_5 ),
inference(superposition,[],[f310,f120]) ).
fof(f459,plain,
( sk3 = join(zero,complement(join(sF8,sF8)))
| ~ spl16_4 ),
inference(superposition,[],[f310,f110]) ).
fof(f461,plain,
( sF2 = join(zero,complement(join(sF3,sF3)))
| ~ spl16_8 ),
inference(superposition,[],[f310,f152]) ).
fof(f513,plain,
! [X0,X1] : join(complement(join(X0,complement(X0))),complement(join(complement(X1),complement(X1)))) = X1,
inference(superposition,[],[f4,f211]) ).
fof(f514,plain,
! [X0,X1] : join(complement(join(complement(X1),complement(complement(complement(X1))))),complement(join(X0,complement(X0)))) = X1,
inference(superposition,[],[f4,f211]) ).
fof(f615,plain,
! [X0,X1] : join(complement(X0),X1) = join(complement(X0),complement(join(complement(join(complement(X0),X1)),join(complement(X1),complement(X0))))),
inference(superposition,[],[f75,f75]) ).
fof(f617,plain,
! [X0,X1] : complement(X1) = join(complement(join(X0,complement(X0))),complement(join(complement(complement(X1)),X1))),
inference(superposition,[],[f75,f211]) ).
fof(f646,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = join(complement(X0),complement(join(complement(join(complement(X1),complement(X0))),join(complement(X0),X1)))),
inference(superposition,[],[f4,f75]) ).
fof(f652,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = join(complement(X0),complement(join(join(complement(X0),X1),complement(join(complement(X1),complement(X0)))))),
inference(forward_demodulation,[],[f646,f1]) ).
fof(f665,plain,
! [X0,X1] : complement(X1) = join(complement(join(X0,complement(X0))),complement(join(X1,complement(complement(X1))))),
inference(forward_demodulation,[],[f617,f1]) ).
fof(f667,plain,
! [X0,X1] : join(complement(X0),X1) = join(complement(X0),complement(join(join(complement(X1),complement(X0)),complement(join(complement(X0),X1))))),
inference(forward_demodulation,[],[f615,f1]) ).
fof(f669,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = join(complement(X0),complement(join(complement(X0),join(X1,complement(join(complement(X1),complement(X0))))))),
inference(forward_demodulation,[],[f652,f2]) ).
fof(f674,plain,
! [X0,X1] : join(complement(X0),X1) = join(complement(X0),complement(join(complement(X1),join(complement(X0),complement(join(complement(X0),X1)))))),
inference(forward_demodulation,[],[f667,f2]) ).
fof(f756,plain,
! [X0] : converse(converse(X0)) = composition(converse(one),X0),
inference(superposition,[],[f333,f8]) ).
fof(f772,plain,
! [X0] : composition(converse(one),X0) = X0,
inference(forward_demodulation,[],[f756,f10]) ).
fof(f786,plain,
! [X0] : complement(X0) = join(complement(composition(one,X0)),complement(X0)),
inference(superposition,[],[f14,f772]) ).
fof(f796,plain,
one = converse(one),
inference(superposition,[],[f8,f772]) ).
fof(f799,plain,
! [X0] : composition(one,X0) = X0,
inference(backward_demodulation,[],[f772,f796]) ).
fof(f808,plain,
! [X0] : complement(X0) = join(complement(X0),complement(composition(one,X0))),
inference(forward_demodulation,[],[f786,f1]) ).
fof(f815,plain,
! [X0] : complement(X0) = join(complement(X0),complement(X0)),
inference(forward_demodulation,[],[f808,f799]) ).
fof(f820,plain,
! [X0,X1] : join(complement(join(X0,complement(X0))),complement(complement(X1))) = X1,
inference(backward_demodulation,[],[f513,f815]) ).
fof(f823,plain,
! [X0] : join(zero,complement(complement(X0))) = X0,
inference(backward_demodulation,[],[f310,f815]) ).
fof(f949,plain,
! [X0,X1] : join(X1,complement(join(complement(X0),complement(complement(X1))))) = join(complement(join(complement(X1),X0)),X0),
inference(superposition,[],[f240,f80]) ).
fof(f958,plain,
! [X0,X1] : join(X1,complement(join(complement(X0),complement(complement(X1))))) = join(X0,complement(join(complement(X1),X0))),
inference(forward_demodulation,[],[f949,f1]) ).
fof(f1062,plain,
! [X0,X1] : join(complement(join(X1,complement(X1))),complement(join(complement(X0),complement(complement(complement(X0)))))) = X0,
inference(superposition,[],[f1,f514]) ).
fof(f1063,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_demodulation,[],[f1062,f665]) ).
fof(f1100,plain,
! [X0,X1] : complement(X1) = join(complement(join(X0,complement(X0))),complement(join(X1,X1))),
inference(backward_demodulation,[],[f665,f1063]) ).
fof(f1104,plain,
! [X0,X1] : join(complement(join(X0,complement(X0))),X1) = X1,
inference(backward_demodulation,[],[f820,f1063]) ).
fof(f1107,plain,
! [X0] : join(zero,X0) = X0,
inference(backward_demodulation,[],[f823,f1063]) ).
fof(f1110,plain,
! [X0,X1] : join(X0,complement(join(complement(X1),X0))) = join(X1,complement(join(complement(X0),X1))),
inference(backward_demodulation,[],[f958,f1063]) ).
fof(f1177,plain,
( sF2 = complement(join(sF3,sF3))
| ~ spl16_8 ),
inference(backward_demodulation,[],[f461,f1107]) ).
fof(f1180,plain,
( sk2 = complement(join(sF7,sF7))
| ~ spl16_5 ),
inference(backward_demodulation,[],[f458,f1107]) ).
fof(f1181,plain,
( sk3 = complement(join(sF8,sF8))
| ~ spl16_4 ),
inference(backward_demodulation,[],[f459,f1107]) ).
fof(f1204,plain,
! [X1] : complement(X1) = complement(join(X1,X1)),
inference(forward_demodulation,[],[f1100,f1104]) ).
fof(f1258,plain,
( sF2 = complement(sF3)
| ~ spl16_8 ),
inference(backward_demodulation,[],[f1177,f1204]) ).
fof(f1261,plain,
( sk2 = complement(sF7)
| ~ spl16_5 ),
inference(backward_demodulation,[],[f1180,f1204]) ).
fof(f1262,plain,
( sk3 = complement(sF8)
| ~ spl16_4 ),
inference(backward_demodulation,[],[f1181,f1204]) ).
fof(f1300,plain,
( sk3 = sF9
| ~ spl16_4
| ~ spl16_9 ),
inference(forward_demodulation,[],[f1262,f163]) ).
fof(f1302,plain,
( sF2 = sF4
| ~ spl16_6
| ~ spl16_8 ),
inference(forward_demodulation,[],[f1258,f130]) ).
fof(f1329,plain,
( sF2 = composition(sk1,sF9)
| ~ spl16_4
| ~ spl16_9
| ~ spl16_13 ),
inference(backward_demodulation,[],[f248,f1300]) ).
fof(f1355,plain,
( sF5 = join(sF1,sF2)
| ~ spl16_6
| ~ spl16_8
| ~ spl16_16 ),
inference(backward_demodulation,[],[f288,f1302]) ).
fof(f1357,plain,
( sF14 = join(sF13,sF2)
| ~ spl16_6
| ~ spl16_8
| ~ spl16_17 ),
inference(backward_demodulation,[],[f294,f1302]) ).
fof(f1377,plain,
( sF14 = join(sF2,sF13)
| ~ spl16_6
| ~ spl16_8
| ~ spl16_17 ),
inference(forward_demodulation,[],[f1357,f1]) ).
fof(f1481,plain,
! [X0,X1] : join(X1,complement(join(X0,X1))) = join(complement(X0),complement(join(complement(X1),complement(X0)))),
inference(superposition,[],[f1110,f1063]) ).
fof(f1493,plain,
! [X0,X1] : join(X1,complement(join(complement(X0),X1))) = join(X0,complement(join(X0,complement(X1)))),
inference(superposition,[],[f1110,f1]) ).
fof(f1606,plain,
! [X0] : complement(complement(X0)) = join(X0,X0),
inference(superposition,[],[f1063,f1204]) ).
fof(f1611,plain,
! [X0] : join(X0,X0) = X0,
inference(forward_demodulation,[],[f1606,f1063]) ).
fof(f1652,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X0,X1)),
inference(superposition,[],[f2,f1611]) ).
fof(f1915,definition,
( spl16_22
<=> sF14 = join(sF2,sF13) ),
introduced(definition,[new_symbols(definition,[spl16_22])],[avatar_definition]) ).
fof(f1917,plain,
( sF14 = join(sF2,sF13)
| ~ spl16_22 ),
inference(avatar_component_clause,[],[f1915]) ).
fof(f1918,plain,
( spl16_22
| ~ spl16_6
| ~ spl16_8
| ~ spl16_17 ),
inference(avatar_split_clause,[],[f1377,f292,f150,f128,f1915]) ).
fof(f2080,plain,
! [X0,X1] : join(complement(join(complement(X0),complement(X1))),X0) = X0,
inference(superposition,[],[f1652,f4]) ).
fof(f2106,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),complement(X1)))) = X0,
inference(forward_demodulation,[],[f2080,f1]) ).
fof(f2127,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = join(complement(X0),complement(join(complement(X0),X1))),
inference(backward_demodulation,[],[f669,f2106]) ).
fof(f2139,plain,
! [X0,X1] : join(complement(X0),X1) = join(complement(X0),complement(join(complement(X1),join(complement(X1),complement(X0))))),
inference(backward_demodulation,[],[f674,f2127]) ).
fof(f2160,plain,
! [X0,X1] : join(complement(X0),X1) = join(complement(X0),complement(join(complement(X1),complement(X0)))),
inference(forward_demodulation,[],[f2139,f1652]) ).
fof(f2171,plain,
! [X0,X1] : join(complement(X0),X1) = join(X1,complement(join(X0,X1))),
inference(backward_demodulation,[],[f1481,f2160]) ).
fof(f2179,plain,
! [X0,X1] : join(complement(complement(X0)),X1) = join(X0,complement(join(X0,complement(X1)))),
inference(backward_demodulation,[],[f1493,f2171]) ).
fof(f2203,plain,
! [X0,X1] : join(X0,X1) = join(X0,complement(join(X0,complement(X1)))),
inference(forward_demodulation,[],[f2179,f1063]) ).
fof(f2233,plain,
! [X0,X1] : join(X1,complement(X0)) = join(X1,complement(join(X1,X0))),
inference(superposition,[],[f2203,f1063]) ).
fof(f2649,plain,
( join(complement(sF7),sF9) = join(sF9,complement(sF10))
| ~ spl16_14 ),
inference(superposition,[],[f2171,f271]) ).
fof(f2682,plain,
( join(complement(sF7),sF9) = join(sF9,sF11)
| ~ spl16_11
| ~ spl16_14 ),
inference(forward_demodulation,[],[f2649,f185]) ).
fof(f2704,plain,
( join(sF9,sF11) = join(sF9,complement(sF7))
| ~ spl16_11
| ~ spl16_14 ),
inference(forward_demodulation,[],[f2682,f1]) ).
fof(f2716,plain,
( join(sF9,sF11) = join(sF9,sk2)
| ~ spl16_5
| ~ spl16_11
| ~ spl16_14 ),
inference(forward_demodulation,[],[f2704,f1261]) ).
fof(f3037,definition,
( spl16_25
<=> sF2 = composition(sk1,sF9) ),
introduced(definition,[new_symbols(definition,[spl16_25])],[avatar_definition]) ).
fof(f3039,plain,
( sF2 = composition(sk1,sF9)
| ~ spl16_25 ),
inference(avatar_component_clause,[],[f3037]) ).
fof(f3040,plain,
( spl16_25
| ~ spl16_4
| ~ spl16_9
| ~ spl16_13 ),
inference(avatar_split_clause,[],[f1329,f246,f161,f108,f3037]) ).
fof(f4245,definition,
( spl16_27
<=> sF5 = join(sF1,sF2) ),
introduced(definition,[new_symbols(definition,[spl16_27])],[avatar_definition]) ).
fof(f4247,plain,
( sF5 = join(sF1,sF2)
| ~ spl16_27 ),
inference(avatar_component_clause,[],[f4245]) ).
fof(f4248,plain,
( spl16_27
| ~ spl16_6
| ~ spl16_8
| ~ spl16_16 ),
inference(avatar_split_clause,[],[f1355,f286,f150,f128,f4245]) ).
fof(f5053,definition,
( spl16_29
<=> join(sF9,sF11) = join(sF9,sk2) ),
introduced(definition,[new_symbols(definition,[spl16_29])],[avatar_definition]) ).
fof(f5055,plain,
( join(sF9,sF11) = join(sF9,sk2)
| ~ spl16_29 ),
inference(avatar_component_clause,[],[f5053]) ).
fof(f5056,plain,
( spl16_29
| ~ spl16_5
| ~ spl16_11
| ~ spl16_14 ),
inference(avatar_split_clause,[],[f2716,f269,f183,f118,f5053]) ).
fof(f5058,plain,
( join(sF0,composition(sk1,sF9)) = composition(sk1,join(sF9,sF11))
| ~ spl16_12
| ~ spl16_29 ),
inference(superposition,[],[f430,f5055]) ).
fof(f5078,plain,
( join(sF0,composition(sk1,sF9)) = join(sF12,composition(sk1,sF9))
| ~ spl16_12
| ~ spl16_15
| ~ spl16_29 ),
inference(forward_demodulation,[],[f5058,f428]) ).
fof(f5086,plain,
( join(sF0,sF2) = join(sF12,sF2)
| ~ spl16_12
| ~ spl16_15
| ~ spl16_25
| ~ spl16_29 ),
inference(forward_demodulation,[],[f5078,f3039]) ).
fof(f5093,plain,
( join(sF2,sF12) = join(sF0,sF2)
| ~ spl16_12
| ~ spl16_15
| ~ spl16_25
| ~ spl16_29 ),
inference(forward_demodulation,[],[f5086,f1]) ).
fof(f11249,definition,
( spl16_55
<=> join(sF2,sF12) = join(sF0,sF2) ),
introduced(definition,[new_symbols(definition,[spl16_55])],[avatar_definition]) ).
fof(f11251,plain,
( join(sF2,sF12) = join(sF0,sF2)
| ~ spl16_55 ),
inference(avatar_component_clause,[],[f11249]) ).
fof(f11252,plain,
( spl16_55
| ~ spl16_12
| ~ spl16_15
| ~ spl16_25
| ~ spl16_29 ),
inference(avatar_split_clause,[],[f5093,f5053,f3037,f275,f200,f11249]) ).
fof(f11263,plain,
( join(sF2,complement(sF12)) = join(sF2,complement(join(sF0,sF2)))
| ~ spl16_55 ),
inference(superposition,[],[f2233,f11251]) ).
fof(f11271,plain,
( join(sF2,complement(sF12)) = join(complement(sF0),sF2)
| ~ spl16_55 ),
inference(forward_demodulation,[],[f11263,f2171]) ).
fof(f11280,plain,
( join(sF2,complement(sF12)) = join(sF2,complement(sF0))
| ~ spl16_55 ),
inference(forward_demodulation,[],[f11271,f1]) ).
fof(f11288,plain,
( join(sF2,sF1) = join(sF2,complement(sF12))
| ~ spl16_7
| ~ spl16_55 ),
inference(forward_demodulation,[],[f11280,f141]) ).
fof(f11294,plain,
( join(sF2,sF13) = join(sF2,sF1)
| ~ spl16_7
| ~ spl16_10
| ~ spl16_55 ),
inference(forward_demodulation,[],[f11288,f174]) ).
fof(f11298,plain,
( join(sF1,sF2) = join(sF2,sF13)
| ~ spl16_7
| ~ spl16_10
| ~ spl16_55 ),
inference(forward_demodulation,[],[f11294,f1]) ).
fof(f11301,plain,
( sF14 = join(sF1,sF2)
| ~ spl16_7
| ~ spl16_10
| ~ spl16_22
| ~ spl16_55 ),
inference(forward_demodulation,[],[f11298,f1917]) ).
fof(f11303,plain,
( sF5 = sF14
| ~ spl16_7
| ~ spl16_10
| ~ spl16_22
| ~ spl16_27
| ~ spl16_55 ),
inference(forward_demodulation,[],[f11301,f4247]) ).
fof(f11305,plain,
( complement(sF5) = sF15
| ~ spl16_1
| ~ spl16_7
| ~ spl16_10
| ~ spl16_22
| ~ spl16_27
| ~ spl16_55 ),
inference(backward_demodulation,[],[f56,f11303]) ).
fof(f11381,plain,
( sF6 = sF15
| ~ spl16_1
| ~ spl16_2
| ~ spl16_7
| ~ spl16_10
| ~ spl16_22
| ~ spl16_27
| ~ spl16_55 ),
inference(forward_demodulation,[],[f11305,f61]) ).
fof(f11383,plain,
( $false
| ~ spl16_1
| ~ spl16_2
| spl16_3
| ~ spl16_7
| ~ spl16_10
| ~ spl16_22
| ~ spl16_27
| ~ spl16_55 ),
inference(forward_subsumption_resolution,[],[f11381,f105]) ).
fof(f11384,plain,
( ~ spl16_1
| ~ spl16_2
| spl16_3
| ~ spl16_7
| ~ spl16_10
| ~ spl16_22
| ~ spl16_27
| ~ spl16_55 ),
inference(avatar_contradiction_clause,[],[f11383]) ).
cnf(s1,plain,
spl16_1,
inference(sat_conversion,[],[f57]) ).
cnf(s2,plain,
spl16_2,
inference(sat_conversion,[],[f62]) ).
cnf(s3,plain,
~ spl16_3,
inference(sat_conversion,[],[f106]) ).
cnf(s4,plain,
spl16_4,
inference(sat_conversion,[],[f111]) ).
cnf(s5,plain,
spl16_5,
inference(sat_conversion,[],[f121]) ).
cnf(s6,plain,
spl16_6,
inference(sat_conversion,[],[f131]) ).
cnf(s7,plain,
spl16_7,
inference(sat_conversion,[],[f142]) ).
cnf(s8,plain,
spl16_8,
inference(sat_conversion,[],[f153]) ).
cnf(s9,plain,
spl16_9,
inference(sat_conversion,[],[f164]) ).
cnf(s10,plain,
spl16_10,
inference(sat_conversion,[],[f175]) ).
cnf(s11,plain,
spl16_11,
inference(sat_conversion,[],[f186]) ).
cnf(s12,plain,
spl16_12,
inference(sat_conversion,[],[f203]) ).
cnf(s13,plain,
spl16_13,
inference(sat_conversion,[],[f249]) ).
cnf(s14,plain,
spl16_14,
inference(sat_conversion,[],[f272]) ).
cnf(s15,plain,
spl16_15,
inference(sat_conversion,[],[f278]) ).
cnf(s16,plain,
spl16_16,
inference(sat_conversion,[],[f289]) ).
cnf(s17,plain,
spl16_17,
inference(sat_conversion,[],[f295]) ).
cnf(s22,plain,
( ~ spl16_6
| ~ spl16_8
| ~ spl16_17
| spl16_22 ),
inference(sat_conversion,[],[f1918]) ).
cnf(s25,plain,
( ~ spl16_4
| ~ spl16_9
| ~ spl16_13
| spl16_25 ),
inference(sat_conversion,[],[f3040]) ).
cnf(s27,plain,
( ~ spl16_6
| ~ spl16_8
| ~ spl16_16
| spl16_27 ),
inference(sat_conversion,[],[f4248]) ).
cnf(s29,plain,
( ~ spl16_5
| ~ spl16_11
| ~ spl16_14
| spl16_29 ),
inference(sat_conversion,[],[f5056]) ).
cnf(s55,plain,
( ~ spl16_12
| ~ spl16_15
| ~ spl16_25
| ~ spl16_29
| spl16_55 ),
inference(sat_conversion,[],[f11252]) ).
cnf(s56,plain,
( ~ spl16_1
| ~ spl16_2
| spl16_3
| ~ spl16_7
| ~ spl16_10
| ~ spl16_22
| ~ spl16_27
| ~ spl16_55 ),
inference(sat_conversion,[],[f11384]) ).
cnf(s64,plain,
spl16_27,
inference(rat,[],[s27,s8,s16,s6]) ).
cnf(s66,plain,
spl16_22,
inference(rat,[],[s22,s8,s17,s6]) ).
cnf(s72,plain,
spl16_29,
inference(rat,[],[s29,s11,s14,s5]) ).
cnf(s79,plain,
spl16_25,
inference(rat,[],[s25,s9,s13,s4]) ).
cnf(s81,plain,
spl16_55,
inference(rat,[],[s55,s72,s12,s15,s79]) ).
cnf(s82,plain,
~ spl16_1,
inference(rat,[],[s56,s81,s64,s66,s10,s7,s3,s2]) ).
cnf(s87,plain,
$false,
inference(rat,[],[s1,s82]) ).
fof(f11386,plain,
$false,
inference(avatar_sat_refutation,[],[s87]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL016-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.37 % Computer : n001.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 22:57:17 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.41 Running first-order theorem proving
% 0.12/0.41 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
% 5.95/1.99 % (4057824)Detected a unit-equality problem, will run specialized UEQ schedule.
% 5.95/1.99 % (4057829)lrs+1002_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal:acc=on:s2agt=16:kmz=on:sac=on:random_seed=781642449:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 5.95/1.99 % (4057830)lrs+11_1_ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2484616438:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 5.95/1.99 % (4057832)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=2591611820:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 5.95/1.99 % (4057835)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=1761600637:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 5.95/1.99 % (4057834)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=276741185:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 5.95/1.99 % (4057831)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=620449083:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 5.95/1.99 % (4057833)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=40812442:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 5.95/1.99 % (4057832)Instruction limit reached!
% 5.95/1.99 % (4057832)------------------------------
% 5.95/1.99 % (4057832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.95/1.99 % (4057832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.95/1.99 % (4057832)CaDiCaL version: 2.1.3
% 5.95/1.99 % (4057832)Termination reason: Instruction limit
% 5.95/1.99 % (4057832)Termination phase: Saturation
% 5.95/1.99 % (4057832)Time elapsed: 0.084 s
% 5.95/1.99 % (4057832)Peak memory usage: 89 MB
% 5.95/1.99 % (4057832)Instructions burned: 138 (million)
% 5.95/1.99 % (4057833)Instruction limit reached!
% 5.95/1.99 % (4057833)------------------------------
% 5.95/1.99 % (4057833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.95/1.99 % (4057833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.95/1.99 % (4057833)CaDiCaL version: 2.1.3
% 5.95/1.99 % (4057833)Termination reason: Instruction limit
% 5.95/1.99 % (4057833)Termination phase: Saturation
% 5.95/1.99 % (4057833)Time elapsed: 0.104 s
% 5.95/1.99 % (4057833)Peak memory usage: 89 MB
% 5.95/1.99 % (4057833)Instructions burned: 181 (million)
% 5.95/1.99 % (4057834)Instruction limit reached!
% 5.95/1.99 % (4057834)------------------------------
% 5.95/1.99 % (4057834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.95/1.99 % (4057834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.95/1.99 % (4057834)CaDiCaL version: 2.1.3
% 5.95/1.99 % (4057834)Termination reason: Instruction limit
% 5.95/1.99 % (4057834)Termination phase: Saturation
% 5.95/1.99 % (4057834)Time elapsed: 0.168 s
% 5.95/1.99 % (4057834)Peak memory usage: 91 MB
% 5.95/1.99 % (4057834)Instructions burned: 258 (million)
% 5.95/1.99 % (4057843)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=3652059165:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2997 on theBenchmark for (2997ds/2051Mi)
% 5.95/1.99 % (4057844)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1773027053:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 5.95/1.99 % (4057845)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=1248696569:i=215:ep=RSTC_2996 on theBenchmark for (2996ds/215Mi)
% 5.95/1.99 % (4057845)Instruction limit reached!
% 5.95/1.99 % (4057845)------------------------------
% 5.95/1.99 % (4057845)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.95/1.99 % (4057845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.95/1.99 % (4057845)CaDiCaL version: 2.1.3
% 5.95/1.99 % (4057845)Termination reason: Instruction limit
% 5.95/1.99 % (4057845)Termination phase: Saturation
% 5.95/1.99 % (4057845)Time elapsed: 0.112 s
% 5.95/1.99 % (4057845)Peak memory usage: 90 MB
% 5.95/1.99 % (4057845)Instructions burned: 215 (million)
% 5.95/1.99 % (4057849)lrs+11_1_sil=16000:tgt=full:fde=none:sp=reverse_frequency:lma=off:fs=off:acc=on:bsr=unit_only:rp=on:random_seed=4103787247:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2993 on theBenchmark for (2993ds/317Mi)
% 5.95/1.99 % (4057835)Instruction limit reached!
% 5.95/1.99 % (4057835)------------------------------
% 5.95/1.99 % (4057835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.95/1.99 % (4057835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.95/1.99 % (4057835)CaDiCaL version: 2.1.3
% 5.95/1.99 % (4057835)Termination reason: Instruction limit
% 5.95/1.99 % (4057835)Termination phase: Saturation
% 5.95/1.99 % (4057835)Time elapsed: 0.653 s
% 5.95/1.99 % (4057835)Peak memory usage: 98 MB
% 5.95/1.99 % (4057835)Instructions burned: 1188 (million)
% 5.95/1.99 % (4057829)First to succeed.
% 5.95/1.99 % (4057829)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4057824"
% 5.95/1.99 % (4057851)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=arity:lcm=predicate:urr=on:s2agt=16:br=off:random_seed=3285531657:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2991 on theBenchmark for (2991ds/12125Mi)
% 5.95/1.99 % (4057849)Instruction limit reached!
% 5.95/1.99 % (4057849)------------------------------
% 5.95/1.99 % (4057849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.95/1.99 % (4057849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.95/1.99 % (4057849)CaDiCaL version: 2.1.3
% 5.95/1.99 % (4057849)Termination reason: Instruction limit
% 5.95/1.99 % (4057849)Termination phase: Saturation
% 5.95/1.99 % (4057849)Time elapsed: 0.198 s
% 5.95/1.99 % (4057849)Peak memory usage: 94 MB
% 5.95/1.99 % (4057849)Instructions burned: 317 (million)
% 5.95/1.99 % (4057829)Refutation found. Thanks to Tanya!
% 5.95/1.99 % SZS status Unsatisfiable for theBenchmark
% 5.95/1.99 % SZS output start Proof for theBenchmark
% See solution above
% 8.49/2.18 % (4057829)------------------------------
% 8.49/2.18 % (4057829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.49/2.18 % (4057829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.49/2.18 % (4057829)CaDiCaL version: 2.1.3
% 8.49/2.18 % (4057829)Termination reason: Refutation
% 8.49/2.18 % (4057829)Time elapsed: 0.828 s
% 8.49/2.18 % (4057829)Peak memory usage: 144 MB
% 8.49/2.18 % (4057829)Instructions burned: 2357 (million)
% 8.49/2.18 % (4057829)------------------------------
% 8.49/2.18 % (4057829)------------------------------
% 8.49/2.18 % (4057824)Success in time 1.117 s
% 8.49/2.18 % Vampire exiting
%------------------------------------------------------------------------------