%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : REL028-2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n017.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:54 PM UTC 2026
% Result : Unsatisfiable 15.97s 3.18s
% Output : Refutation 16.50s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 38
% Syntax : Number of formulae : 217 ( 103 unt; 23 def)
% Number of atoms : 438 ( 173 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 431 ( 210 ~; 205 |; 0 &)
% ( 16 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 18 ( 16 usr; 17 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 12 con; 0-2 aty)
% Number of variables : 136 ( 0 sgn 136 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p',composition_distributivity_7) ).
fof(f10,axiom,
! [X0] : converse(converse(X0)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',converse_idempotence_8) ).
fof(f11,axiom,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',converse_additivity_9) ).
fof(f12,axiom,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p',def_top_12) ).
fof(f16,axiom,
! [X0] : zero = meet(X0,complement(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',def_zero_13) ).
fof(f23,negated_conjecture,
join(sk1,one) = one,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals_17) ).
fof(f24,plain,
one = join(sk1,one),
inference(reorient_equations,[],[f23]) ).
fof(f25,negated_conjecture,
join(sk2,one) = one,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals_18) ).
fof(f26,plain,
one = join(sk2,one),
inference(reorient_equations,[],[f25]) ).
fof(f27,negated_conjecture,
composition(sk1,sk2) != meet(sk1,sk2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals_19) ).
fof(f28,plain,
! [X0] : zero = complement(join(complement(X0),complement(complement(X0)))),
inference(definition_unfolding,[],[f16,f6]) ).
fof(f32,plain,
composition(sk1,sk2) != complement(join(complement(sk1),complement(sk2))),
inference(definition_unfolding,[],[f27,f6]) ).
fof(f33,definition,
sF0 = join(sk1,one),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f34,plain,
join(sk1,one) = sF0,
inference(reorient_equations,[],[f33]) ).
fof(f35,plain,
one = sF0,
inference(definition_folding,[],[f24,f34]) ).
fof(f36,definition,
sF1 = join(sk2,one),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f37,plain,
join(sk2,one) = sF1,
inference(reorient_equations,[],[f36]) ).
fof(f38,plain,
one = sF1,
inference(definition_folding,[],[f26,f37]) ).
fof(f39,definition,
sF2 = composition(sk1,sk2),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f40,plain,
composition(sk1,sk2) = sF2,
inference(reorient_equations,[],[f39]) ).
fof(f41,definition,
sF3 = complement(sk1),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f42,plain,
complement(sk1) = sF3,
inference(reorient_equations,[],[f41]) ).
fof(f43,definition,
sF4 = complement(sk2),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f44,plain,
complement(sk2) = sF4,
inference(reorient_equations,[],[f43]) ).
fof(f45,definition,
sF5 = join(sF3,sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f46,plain,
join(sF3,sF4) = sF5,
inference(reorient_equations,[],[f45]) ).
fof(f47,definition,
sF6 = complement(sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f48,plain,
complement(sF5) = sF6,
inference(reorient_equations,[],[f47]) ).
fof(f49,plain,
sF2 != sF6,
inference(definition_folding,[],[f32,f48,f46,f44,f42,f40]) ).
fof(f50,plain,
sF0 = sF1,
inference(forward_demodulation,[],[f35,f38]) ).
fof(f51,plain,
zero = complement(top),
inference(backward_demodulation,[],[f28,f15]) ).
fof(f52,plain,
! [X0] : composition(X0,sF1) = X0,
inference(forward_demodulation,[],[f8,f38]) ).
fof(f53,plain,
sF0 = join(sk1,sF1),
inference(forward_demodulation,[],[f34,f38]) ).
fof(f54,plain,
sF1 = join(sk2,sF1),
inference(forward_demodulation,[],[f37,f38]) ).
fof(f56,plain,
! [X0] : composition(X0,sF0) = X0,
inference(forward_demodulation,[],[f52,f50]) ).
fof(f57,plain,
sF0 = join(sF1,sk1),
inference(forward_demodulation,[],[f53,f1]) ).
fof(f58,plain,
sF1 = join(sF1,sk2),
inference(forward_demodulation,[],[f54,f1]) ).
fof(f59,plain,
sF0 = join(sF0,sk1),
inference(forward_demodulation,[],[f57,f50]) ).
fof(f60,plain,
sF0 = join(sF0,sk2),
inference(forward_demodulation,[],[f58,f50]) ).
fof(f73,definition,
( spl7_2
<=> complement(sF5) = sF6 ),
introduced(definition,[new_symbols(definition,[spl7_2])],[avatar_definition]) ).
fof(f75,plain,
( complement(sF5) = sF6
| ~ spl7_2 ),
inference(avatar_component_clause,[],[f73]) ).
fof(f76,plain,
spl7_2,
inference(avatar_split_clause,[],[f48,f73]) ).
fof(f87,plain,
! [X0,X1] : join(complement(join(complement(X0),complement(X1))),complement(join(complement(X1),X0))) = X1,
inference(superposition,[],[f4,f1]) ).
fof(f89,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))) = X0,
inference(superposition,[],[f4,f1]) ).
fof(f91,plain,
! [X0,X1] : join(complement(join(complement(X1),X0)),complement(join(complement(X0),complement(X1)))) = X1,
inference(forward_demodulation,[],[f87,f1]) ).
fof(f103,definition,
( spl7_3
<=> composition(sk1,sk2) = sF2 ),
introduced(definition,[new_symbols(definition,[spl7_3])],[avatar_definition]) ).
fof(f105,plain,
( composition(sk1,sk2) = sF2
| ~ spl7_3 ),
inference(avatar_component_clause,[],[f103]) ).
fof(f106,plain,
spl7_3,
inference(avatar_split_clause,[],[f40,f103]) ).
fof(f111,plain,
! [X0,X1] : complement(X1) = join(composition(X0,complement(composition(converse(X0),X1))),complement(X1)),
inference(superposition,[],[f14,f10]) ).
fof(f120,plain,
! [X0,X1] : complement(X1) = join(complement(X1),composition(X0,complement(composition(converse(X0),X1)))),
inference(forward_demodulation,[],[f111,f1]) ).
fof(f128,definition,
( spl7_5
<=> zero = complement(top) ),
introduced(definition,[new_symbols(definition,[spl7_5])],[avatar_definition]) ).
fof(f130,plain,
( zero = complement(top)
| ~ spl7_5 ),
inference(avatar_component_clause,[],[f128]) ).
fof(f131,plain,
spl7_5,
inference(avatar_split_clause,[],[f51,f128]) ).
fof(f133,definition,
( spl7_6
<=> complement(sk1) = sF3 ),
introduced(definition,[new_symbols(definition,[spl7_6])],[avatar_definition]) ).
fof(f135,plain,
( complement(sk1) = sF3
| ~ spl7_6 ),
inference(avatar_component_clause,[],[f133]) ).
fof(f136,plain,
spl7_6,
inference(avatar_split_clause,[],[f42,f133]) ).
fof(f144,definition,
( spl7_7
<=> complement(sk2) = sF4 ),
introduced(definition,[new_symbols(definition,[spl7_7])],[avatar_definition]) ).
fof(f146,plain,
( complement(sk2) = sF4
| ~ spl7_7 ),
inference(avatar_component_clause,[],[f144]) ).
fof(f147,plain,
spl7_7,
inference(avatar_split_clause,[],[f44,f144]) ).
fof(f155,definition,
( spl7_8
<=> sF2 = sF6 ),
introduced(definition,[new_symbols(definition,[spl7_8])],[avatar_definition]) ).
fof(f157,plain,
( sF2 != sF6
| spl7_8 ),
inference(avatar_component_clause,[],[f155]) ).
fof(f158,plain,
~ spl7_8,
inference(avatar_split_clause,[],[f49,f155]) ).
fof(f168,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f1,f2]) ).
fof(f187,definition,
( spl7_9
<=> join(sF3,sF4) = sF5 ),
introduced(definition,[new_symbols(definition,[spl7_9])],[avatar_definition]) ).
fof(f189,plain,
( join(sF3,sF4) = sF5
| ~ spl7_9 ),
inference(avatar_component_clause,[],[f187]) ).
fof(f190,plain,
spl7_9,
inference(avatar_split_clause,[],[f46,f187]) ).
fof(f199,plain,
! [X0] : join(complement(join(complement(X0),complement(complement(complement(X0))))),complement(top)) = X0,
inference(superposition,[],[f4,f15]) ).
fof(f200,plain,
! [X0] : join(complement(top),complement(join(complement(X0),complement(complement(complement(X0)))))) = X0,
inference(forward_demodulation,[],[f199,f1]) ).
fof(f204,plain,
( ! [X0] : join(zero,complement(join(complement(X0),complement(complement(complement(X0)))))) = X0
| ~ spl7_5 ),
inference(forward_demodulation,[],[f200,f130]) ).
fof(f243,definition,
( spl7_10
<=> sF0 = join(sF0,sk1) ),
introduced(definition,[new_symbols(definition,[spl7_10])],[avatar_definition]) ).
fof(f245,plain,
( sF0 = join(sF0,sk1)
| ~ spl7_10 ),
inference(avatar_component_clause,[],[f243]) ).
fof(f246,plain,
spl7_10,
inference(avatar_split_clause,[],[f59,f243]) ).
fof(f255,definition,
( spl7_11
<=> sF0 = join(sF0,sk2) ),
introduced(definition,[new_symbols(definition,[spl7_11])],[avatar_definition]) ).
fof(f257,plain,
( sF0 = join(sF0,sk2)
| ~ spl7_11 ),
inference(avatar_component_clause,[],[f255]) ).
fof(f258,plain,
spl7_11,
inference(avatar_split_clause,[],[f60,f255]) ).
fof(f275,plain,
! [X0] : complement(X0) = join(complement(join(complement(complement(X0)),X0)),complement(top)),
inference(superposition,[],[f91,f15]) ).
fof(f286,plain,
! [X0] : complement(X0) = join(complement(top),complement(join(complement(complement(X0)),X0))),
inference(forward_demodulation,[],[f275,f1]) ).
fof(f300,plain,
! [X0] : complement(X0) = join(complement(top),complement(join(X0,complement(complement(X0))))),
inference(forward_demodulation,[],[f286,f1]) ).
fof(f306,plain,
( ! [X0] : complement(X0) = join(zero,complement(join(X0,complement(complement(X0)))))
| ~ spl7_5 ),
inference(forward_demodulation,[],[f300,f130]) ).
fof(f310,plain,
( ! [X0] : complement(complement(X0)) = X0
| ~ spl7_5 ),
inference(backward_demodulation,[],[f204,f306]) ).
fof(f321,plain,
( sk1 = complement(sF3)
| ~ spl7_5
| ~ spl7_6 ),
inference(superposition,[],[f310,f135]) ).
fof(f322,plain,
( sk2 = complement(sF4)
| ~ spl7_5
| ~ spl7_7 ),
inference(superposition,[],[f310,f146]) ).
fof(f328,plain,
( ! [X0,X1] : complement(X0) = join(complement(join(X0,X1)),complement(join(X0,complement(X1))))
| ~ spl7_5 ),
inference(superposition,[],[f89,f310]) ).
fof(f331,plain,
( ! [X0,X1] : complement(X0) = join(complement(join(X0,X1)),complement(join(complement(X1),X0)))
| ~ spl7_5 ),
inference(superposition,[],[f91,f310]) ).
fof(f344,plain,
( ! [X0,X1] : complement(X1) = join(complement(join(X0,X1)),complement(join(X1,complement(X0))))
| ~ spl7_5 ),
inference(superposition,[],[f328,f1]) ).
fof(f419,definition,
( spl7_12
<=> sk1 = complement(sF3) ),
introduced(definition,[new_symbols(definition,[spl7_12])],[avatar_definition]) ).
fof(f421,plain,
( sk1 = complement(sF3)
| ~ spl7_12 ),
inference(avatar_component_clause,[],[f419]) ).
fof(f422,plain,
( spl7_12
| ~ spl7_5
| ~ spl7_6 ),
inference(avatar_split_clause,[],[f321,f133,f128,f419]) ).
fof(f424,definition,
( spl7_13
<=> sk2 = complement(sF4) ),
introduced(definition,[new_symbols(definition,[spl7_13])],[avatar_definition]) ).
fof(f426,plain,
( sk2 = complement(sF4)
| ~ spl7_13 ),
inference(avatar_component_clause,[],[f424]) ).
fof(f427,plain,
( spl7_13
| ~ spl7_5
| ~ spl7_7 ),
inference(avatar_split_clause,[],[f322,f144,f128,f424]) ).
fof(f429,plain,
! [X0,X1] : composition(converse(X1),X0) = converse(composition(converse(X0),X1)),
inference(superposition,[],[f12,f10]) ).
fof(f432,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(f439,plain,
! [X2,X0,X1] : composition(join(converse(X2),converse(X1)),converse(X0)) = join(converse(composition(X0,X2)),converse(composition(X0,X1))),
inference(superposition,[],[f432,f12]) ).
fof(f450,plain,
! [X2,X0,X1] : composition(join(converse(X2),converse(X1)),converse(X0)) = converse(join(composition(X0,X2),composition(X0,X1))),
inference(forward_demodulation,[],[f439,f11]) ).
fof(f453,plain,
! [X2,X0,X1] : converse(join(composition(X0,X2),composition(X0,X1))) = composition(converse(join(X2,X1)),converse(X0)),
inference(forward_demodulation,[],[f450,f11]) ).
fof(f455,plain,
! [X2,X0,X1] : converse(join(composition(X0,X2),composition(X0,X1))) = converse(composition(X0,join(X2,X1))),
inference(forward_demodulation,[],[f453,f12]) ).
fof(f466,plain,
! [X2,X0,X1] : join(composition(X0,X1),composition(X0,X2)) = converse(converse(composition(X0,join(X1,X2)))),
inference(superposition,[],[f10,f455]) ).
fof(f478,plain,
! [X2,X0,X1] : composition(X0,join(X1,X2)) = join(composition(X0,X1),composition(X0,X2)),
inference(forward_demodulation,[],[f466,f10]) ).
fof(f519,plain,
( ! [X0,X1] : complement(X1) = join(complement(join(X0,X1)),complement(join(complement(X0),X1)))
| ~ spl7_5 ),
inference(superposition,[],[f331,f1]) ).
fof(f543,plain,
( ! [X0,X1] : join(X0,X1) = join(complement(complement(X0)),complement(join(complement(join(X0,X1)),join(complement(X1),X0))))
| ~ spl7_5 ),
inference(superposition,[],[f4,f331]) ).
fof(f552,plain,
( ! [X0,X1] : join(X0,X1) = join(complement(complement(X0)),complement(join(X0,join(complement(join(X0,X1)),complement(X1)))))
| ~ spl7_5 ),
inference(forward_demodulation,[],[f543,f168]) ).
fof(f570,plain,
( ! [X0,X1] : join(X0,X1) = join(complement(complement(X0)),complement(join(X0,join(complement(X1),complement(join(X0,X1))))))
| ~ spl7_5 ),
inference(forward_demodulation,[],[f552,f1]) ).
fof(f585,plain,
( ! [X0,X1] : join(X0,X1) = join(X0,complement(join(X0,join(complement(X1),complement(join(X0,X1))))))
| ~ spl7_5 ),
inference(forward_demodulation,[],[f570,f310]) ).
fof(f999,plain,
! [X0] : converse(converse(X0)) = composition(converse(sF0),X0),
inference(superposition,[],[f429,f56]) ).
fof(f1017,plain,
! [X0] : composition(converse(sF0),X0) = X0,
inference(forward_demodulation,[],[f999,f10]) ).
fof(f1132,plain,
! [X0] : complement(X0) = join(complement(X0),composition(sF0,complement(X0))),
inference(superposition,[],[f120,f1017]) ).
fof(f1135,plain,
! [X0,X1] : join(X0,composition(X1,X0)) = composition(join(converse(sF0),X1),X0),
inference(superposition,[],[f9,f1017]) ).
fof(f1146,plain,
sF0 = converse(sF0),
inference(superposition,[],[f56,f1017]) ).
fof(f1151,plain,
! [X0] : composition(sF0,X0) = X0,
inference(backward_demodulation,[],[f1017,f1146]) ).
fof(f1163,plain,
! [X0,X1] : join(X0,composition(X1,X0)) = composition(join(sF0,X1),X0),
inference(forward_demodulation,[],[f1135,f1146]) ).
fof(f1167,plain,
! [X0] : complement(X0) = join(complement(X0),complement(X0)),
inference(backward_demodulation,[],[f1132,f1151]) ).
fof(f1263,plain,
( composition(join(sF0,sk1),sk2) = join(sk2,sF2)
| ~ spl7_3 ),
inference(superposition,[],[f1163,f105]) ).
fof(f1272,plain,
( ! [X0] : composition(sF0,X0) = join(X0,composition(sk1,X0))
| ~ spl7_10 ),
inference(superposition,[],[f1163,f245]) ).
fof(f1327,plain,
( ! [X0] : join(X0,composition(sk1,X0)) = X0
| ~ spl7_10 ),
inference(forward_demodulation,[],[f1272,f1151]) ).
fof(f1332,plain,
( composition(join(sF0,sk1),sk2) = join(sF2,sk2)
| ~ spl7_3 ),
inference(forward_demodulation,[],[f1263,f1]) ).
fof(f1349,plain,
( composition(sF0,sk2) = join(sF2,sk2)
| ~ spl7_3
| ~ spl7_10 ),
inference(forward_demodulation,[],[f1332,f245]) ).
fof(f1358,plain,
( sk2 = join(sF2,sk2)
| ~ spl7_3
| ~ spl7_10 ),
inference(forward_demodulation,[],[f1349,f1151]) ).
fof(f1363,plain,
( ! [X0] : join(X0,X0) = X0
| ~ spl7_5 ),
inference(superposition,[],[f1167,f310]) ).
fof(f1474,plain,
( ! [X0,X1] : join(X0,X1) = join(X0,join(X0,X1))
| ~ spl7_5 ),
inference(superposition,[],[f2,f1363]) ).
fof(f1574,plain,
( ! [X0,X1] : join(X0,X1) = join(X0,join(composition(sk1,X0),X1))
| ~ spl7_10 ),
inference(superposition,[],[f2,f1327]) ).
fof(f1694,plain,
( ! [X0,X1] : join(X0,composition(sk1,X1)) = join(X0,composition(sk1,join(X0,X1)))
| ~ spl7_10 ),
inference(superposition,[],[f1574,f478]) ).
fof(f1854,plain,
( ! [X0] : join(X0,composition(sk1,complement(X0))) = join(X0,composition(sk1,top))
| ~ spl7_10 ),
inference(superposition,[],[f1694,f15]) ).
fof(f2553,plain,
( ! [X0,X1] : complement(complement(join(X0,complement(X1)))) = join(complement(complement(X0)),complement(join(complement(complement(join(X1,X0))),complement(join(X0,complement(X1))))))
| ~ spl7_5 ),
inference(superposition,[],[f519,f344]) ).
fof(f2556,plain,
( ! [X0,X1] : complement(complement(join(X0,complement(X1)))) = join(complement(complement(X0)),complement(join(join(X1,X0),complement(join(X0,complement(X1))))))
| ~ spl7_5 ),
inference(forward_demodulation,[],[f2553,f310]) ).
fof(f2605,plain,
( ! [X0,X1] : complement(complement(join(X0,complement(X1)))) = join(complement(complement(X0)),complement(join(X1,join(X0,complement(join(X0,complement(X1)))))))
| ~ spl7_5 ),
inference(forward_demodulation,[],[f2556,f2]) ).
fof(f2638,plain,
( ! [X0,X1] : complement(complement(join(X0,complement(X1)))) = join(X0,complement(join(X1,join(X0,complement(join(X0,complement(X1)))))))
| ~ spl7_5 ),
inference(forward_demodulation,[],[f2605,f310]) ).
fof(f2663,plain,
( ! [X0,X1] : join(X0,complement(X1)) = join(X0,complement(join(X1,join(X0,complement(join(X0,complement(X1)))))))
| ~ spl7_5 ),
inference(forward_demodulation,[],[f2638,f310]) ).
fof(f2693,plain,
( ! [X0,X1] : join(X1,X0) = join(X0,join(X1,X0))
| ~ spl7_5 ),
inference(superposition,[],[f168,f1363]) ).
fof(f3074,plain,
( ! [X0,X1] : complement(X0) = join(complement(join(X1,X0)),complement(X0))
| ~ spl7_5 ),
inference(superposition,[],[f1474,f344]) ).
fof(f3132,plain,
( ! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X1,X0)))
| ~ spl7_5 ),
inference(forward_demodulation,[],[f3074,f1]) ).
fof(f3150,plain,
( ! [X0,X1] : join(X0,X1) = join(X0,complement(join(X0,complement(X1))))
| ~ spl7_5 ),
inference(backward_demodulation,[],[f585,f3132]) ).
fof(f3157,plain,
( ! [X0,X1] : join(X0,complement(X1)) = join(X0,complement(join(X1,join(X0,X1))))
| ~ spl7_5 ),
inference(backward_demodulation,[],[f2663,f3150]) ).
fof(f3164,plain,
( ! [X0,X1] : join(X0,complement(X1)) = join(X0,complement(join(X0,X1)))
| ~ spl7_5 ),
inference(forward_demodulation,[],[f3157,f2693]) ).
fof(f3402,plain,
( ! [X0,X1] : join(X1,complement(X0)) = join(X1,complement(join(X0,X1)))
| ~ spl7_5 ),
inference(superposition,[],[f3164,f1]) ).
fof(f3436,plain,
( join(sF0,complement(sk2)) = join(sF0,complement(sF0))
| ~ spl7_5
| ~ spl7_11 ),
inference(superposition,[],[f3164,f257]) ).
fof(f3491,plain,
( top = join(sF0,complement(sk2))
| ~ spl7_5
| ~ spl7_11 ),
inference(forward_demodulation,[],[f3436,f15]) ).
fof(f3537,plain,
( top = join(sF0,sF4)
| ~ spl7_5
| ~ spl7_7
| ~ spl7_11 ),
inference(forward_demodulation,[],[f3491,f146]) ).
fof(f3570,plain,
( top = join(sF4,sF0)
| ~ spl7_5
| ~ spl7_7
| ~ spl7_11 ),
inference(forward_demodulation,[],[f3537,f1]) ).
fof(f4169,plain,
( join(sF4,complement(sF3)) = join(sF4,complement(sF5))
| ~ spl7_5
| ~ spl7_9 ),
inference(superposition,[],[f3402,f189]) ).
fof(f4226,plain,
( join(sF4,complement(sF3)) = join(sF4,sF6)
| ~ spl7_2
| ~ spl7_5
| ~ spl7_9 ),
inference(forward_demodulation,[],[f4169,f75]) ).
fof(f4269,plain,
( join(sF4,sk1) = join(sF4,sF6)
| ~ spl7_2
| ~ spl7_5
| ~ spl7_9
| ~ spl7_12 ),
inference(forward_demodulation,[],[f4226,f421]) ).
fof(f4777,definition,
( spl7_18
<=> top = join(sF4,sF0) ),
introduced(definition,[new_symbols(definition,[spl7_18])],[avatar_definition]) ).
fof(f4779,plain,
( top = join(sF4,sF0)
| ~ spl7_18 ),
inference(avatar_component_clause,[],[f4777]) ).
fof(f4780,plain,
( spl7_18
| ~ spl7_5
| ~ spl7_7
| ~ spl7_11 ),
inference(avatar_split_clause,[],[f3570,f255,f144,f128,f4777]) ).
fof(f4791,plain,
( join(sF4,composition(sk1,sF0)) = join(sF4,composition(sk1,top))
| ~ spl7_10
| ~ spl7_18 ),
inference(superposition,[],[f1694,f4779]) ).
fof(f4796,plain,
( join(sF4,sk1) = join(sF4,composition(sk1,top))
| ~ spl7_10
| ~ spl7_18 ),
inference(forward_demodulation,[],[f4791,f56]) ).
fof(f4807,plain,
( join(sF4,sF6) = join(sF4,composition(sk1,top))
| ~ spl7_2
| ~ spl7_5
| ~ spl7_9
| ~ spl7_10
| ~ spl7_12
| ~ spl7_18 ),
inference(forward_demodulation,[],[f4796,f4269]) ).
fof(f4826,definition,
( spl7_19
<=> sk2 = join(sF2,sk2) ),
introduced(definition,[new_symbols(definition,[spl7_19])],[avatar_definition]) ).
fof(f4828,plain,
( sk2 = join(sF2,sk2)
| ~ spl7_19 ),
inference(avatar_component_clause,[],[f4826]) ).
fof(f4829,plain,
( spl7_19
| ~ spl7_3
| ~ spl7_10 ),
inference(avatar_split_clause,[],[f1358,f243,f103,f4826]) ).
fof(f4834,plain,
( complement(sF2) = join(complement(sk2),complement(join(complement(sk2),sF2)))
| ~ spl7_5
| ~ spl7_19 ),
inference(superposition,[],[f331,f4828]) ).
fof(f4840,plain,
( complement(sF2) = join(complement(sk2),complement(sF2))
| ~ spl7_5
| ~ spl7_19 ),
inference(forward_demodulation,[],[f4834,f3164]) ).
fof(f4844,plain,
( complement(sF2) = join(complement(sF2),complement(sk2))
| ~ spl7_5
| ~ spl7_19 ),
inference(forward_demodulation,[],[f4840,f1]) ).
fof(f4846,plain,
( complement(sF2) = join(complement(sF2),sF4)
| ~ spl7_5
| ~ spl7_7
| ~ spl7_19 ),
inference(forward_demodulation,[],[f4844,f146]) ).
fof(f4848,plain,
( complement(sF2) = join(sF4,complement(sF2))
| ~ spl7_5
| ~ spl7_7
| ~ spl7_19 ),
inference(forward_demodulation,[],[f4846,f1]) ).
fof(f5301,plain,
( join(sF4,composition(sk1,top)) = join(sF4,composition(sk1,sk2))
| ~ spl7_10
| ~ spl7_13 ),
inference(superposition,[],[f1854,f426]) ).
fof(f5370,plain,
( join(sF4,composition(sk1,top)) = join(sF4,sF2)
| ~ spl7_3
| ~ spl7_10
| ~ spl7_13 ),
inference(forward_demodulation,[],[f5301,f105]) ).
fof(f5396,plain,
( join(sF4,sF6) = join(sF4,sF2)
| ~ spl7_2
| ~ spl7_3
| ~ spl7_5
| ~ spl7_9
| ~ spl7_10
| ~ spl7_12
| ~ spl7_13
| ~ spl7_18 ),
inference(forward_demodulation,[],[f5370,f4807]) ).
fof(f5414,plain,
( join(sF4,sk1) = join(sF4,sF2)
| ~ spl7_2
| ~ spl7_3
| ~ spl7_5
| ~ spl7_9
| ~ spl7_10
| ~ spl7_12
| ~ spl7_13
| ~ spl7_18 ),
inference(backward_demodulation,[],[f4269,f5396]) ).
fof(f8773,definition,
( spl7_24
<=> complement(sF2) = join(sF4,complement(sF2)) ),
introduced(definition,[new_symbols(definition,[spl7_24])],[avatar_definition]) ).
fof(f8775,plain,
( complement(sF2) = join(sF4,complement(sF2))
| ~ spl7_24 ),
inference(avatar_component_clause,[],[f8773]) ).
fof(f8776,plain,
( spl7_24
| ~ spl7_5
| ~ spl7_7
| ~ spl7_19 ),
inference(avatar_split_clause,[],[f4848,f4826,f144,f128,f8773]) ).
fof(f16510,definition,
( spl7_40
<=> join(sF4,sk1) = join(sF4,sF2) ),
introduced(definition,[new_symbols(definition,[spl7_40])],[avatar_definition]) ).
fof(f16512,plain,
( join(sF4,sk1) = join(sF4,sF2)
| ~ spl7_40 ),
inference(avatar_component_clause,[],[f16510]) ).
fof(f16513,plain,
( spl7_40
| ~ spl7_2
| ~ spl7_3
| ~ spl7_5
| ~ spl7_9
| ~ spl7_10
| ~ spl7_12
| ~ spl7_13
| ~ spl7_18 ),
inference(avatar_split_clause,[],[f5414,f4777,f424,f419,f243,f187,f128,f103,f73,f16510]) ).
fof(f16529,plain,
( join(sF4,complement(sk1)) = join(sF4,complement(join(sF4,sF2)))
| ~ spl7_5
| ~ spl7_40 ),
inference(superposition,[],[f3164,f16512]) ).
fof(f16545,plain,
( join(sF4,complement(sF2)) = join(sF4,complement(sk1))
| ~ spl7_5
| ~ spl7_40 ),
inference(forward_demodulation,[],[f16529,f3164]) ).
fof(f16560,plain,
( join(sF4,sF3) = join(sF4,complement(sF2))
| ~ spl7_5
| ~ spl7_6
| ~ spl7_40 ),
inference(forward_demodulation,[],[f16545,f135]) ).
fof(f16571,plain,
( complement(sF2) = join(sF4,sF3)
| ~ spl7_5
| ~ spl7_6
| ~ spl7_24
| ~ spl7_40 ),
inference(forward_demodulation,[],[f16560,f8775]) ).
fof(f16578,plain,
( join(sF3,sF4) = complement(sF2)
| ~ spl7_5
| ~ spl7_6
| ~ spl7_24
| ~ spl7_40 ),
inference(forward_demodulation,[],[f16571,f1]) ).
fof(f16582,plain,
( sF5 = complement(sF2)
| ~ spl7_5
| ~ spl7_6
| ~ spl7_9
| ~ spl7_24
| ~ spl7_40 ),
inference(forward_demodulation,[],[f16578,f189]) ).
fof(f16727,definition,
( spl7_41
<=> sF5 = complement(sF2) ),
introduced(definition,[new_symbols(definition,[spl7_41])],[avatar_definition]) ).
fof(f16729,plain,
( sF5 = complement(sF2)
| ~ spl7_41 ),
inference(avatar_component_clause,[],[f16727]) ).
fof(f16730,plain,
( spl7_41
| ~ spl7_5
| ~ spl7_6
| ~ spl7_9
| ~ spl7_24
| ~ spl7_40 ),
inference(avatar_split_clause,[],[f16582,f16510,f8773,f187,f133,f128,f16727]) ).
fof(f16731,plain,
( ! [X0] : sF2 = join(complement(join(sF5,complement(X0))),complement(join(sF5,X0)))
| ~ spl7_41 ),
inference(superposition,[],[f4,f16729]) ).
fof(f16783,plain,
( ! [X0] : sF2 = join(complement(join(sF5,X0)),complement(join(sF5,complement(X0))))
| ~ spl7_41 ),
inference(forward_demodulation,[],[f16731,f1]) ).
fof(f16792,plain,
( sF2 = complement(sF5)
| ~ spl7_5
| ~ spl7_41 ),
inference(forward_demodulation,[],[f16783,f328]) ).
fof(f16795,plain,
( sF2 = sF6
| ~ spl7_2
| ~ spl7_5
| ~ spl7_41 ),
inference(forward_demodulation,[],[f16792,f75]) ).
fof(f16800,plain,
( $false
| ~ spl7_2
| ~ spl7_5
| spl7_8
| ~ spl7_41 ),
inference(forward_subsumption_resolution,[],[f16795,f157]) ).
fof(f16801,plain,
( ~ spl7_2
| ~ spl7_5
| spl7_8
| ~ spl7_41 ),
inference(avatar_contradiction_clause,[],[f16800]) ).
cnf(s2,plain,
spl7_2,
inference(sat_conversion,[],[f76]) ).
cnf(s3,plain,
spl7_3,
inference(sat_conversion,[],[f106]) ).
cnf(s5,plain,
spl7_5,
inference(sat_conversion,[],[f131]) ).
cnf(s6,plain,
spl7_6,
inference(sat_conversion,[],[f136]) ).
cnf(s7,plain,
spl7_7,
inference(sat_conversion,[],[f147]) ).
cnf(s8,plain,
~ spl7_8,
inference(sat_conversion,[],[f158]) ).
cnf(s9,plain,
spl7_9,
inference(sat_conversion,[],[f190]) ).
cnf(s10,plain,
spl7_10,
inference(sat_conversion,[],[f246]) ).
cnf(s11,plain,
spl7_11,
inference(sat_conversion,[],[f258]) ).
cnf(s12,plain,
( ~ spl7_5
| ~ spl7_6
| spl7_12 ),
inference(sat_conversion,[],[f422]) ).
cnf(s13,plain,
( ~ spl7_5
| ~ spl7_7
| spl7_13 ),
inference(sat_conversion,[],[f427]) ).
cnf(s18,plain,
( ~ spl7_5
| ~ spl7_7
| ~ spl7_11
| spl7_18 ),
inference(sat_conversion,[],[f4780]) ).
cnf(s19,plain,
( ~ spl7_3
| ~ spl7_10
| spl7_19 ),
inference(sat_conversion,[],[f4829]) ).
cnf(s24,plain,
( ~ spl7_5
| ~ spl7_7
| ~ spl7_19
| spl7_24 ),
inference(sat_conversion,[],[f8776]) ).
cnf(s40,plain,
( ~ spl7_2
| ~ spl7_3
| ~ spl7_5
| ~ spl7_9
| ~ spl7_10
| ~ spl7_12
| ~ spl7_13
| ~ spl7_18
| spl7_40 ),
inference(sat_conversion,[],[f16513]) ).
cnf(s41,plain,
( ~ spl7_5
| ~ spl7_6
| ~ spl7_9
| ~ spl7_24
| ~ spl7_40
| spl7_41 ),
inference(sat_conversion,[],[f16730]) ).
cnf(s43,plain,
( ~ spl7_2
| ~ spl7_5
| spl7_8
| ~ spl7_41 ),
inference(sat_conversion,[],[f16801]) ).
cnf(s52,plain,
spl7_18,
inference(rat,[],[s18,s7,s11,s5]) ).
cnf(s55,plain,
spl7_13,
inference(rat,[],[s13,s7,s5]) ).
cnf(s56,plain,
spl7_12,
inference(rat,[],[s12,s6,s5]) ).
cnf(s61,plain,
spl7_19,
inference(rat,[],[s19,s10,s3]) ).
cnf(s64,plain,
spl7_24,
inference(rat,[],[s24,s5,s7,s61]) ).
cnf(s68,plain,
~ spl7_41,
inference(rat,[],[s43,s5,s8,s2]) ).
cnf(s69,plain,
spl7_40,
inference(rat,[],[s40,s3,s52,s55,s56,s10,s9,s5,s2]) ).
cnf(s72,plain,
$false,
inference(rat,[],[s41,s64,s5,s6,s9,s68,s69]) ).
fof(f16803,plain,
$false,
inference(avatar_sat_refutation,[],[s72]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL028-2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.38 % Computer : n017.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Sun Sep 27 22:48:51 UTC 2026
% 0.13/0.39 % CPUTime :
% 0.13/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.42 Running first-order theorem proving
% 0.13/0.42 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 15.97/3.18 % (3040838)Detected a unit-equality problem, will run specialized UEQ schedule.
% 15.97/3.18 % (3040868)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=584566982:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 15.97/3.18 % (3040872)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=3085391033:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 15.97/3.18 % (3040869)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=1168205222:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 15.97/3.18 % (3040871)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=2529048230:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 15.97/3.18 % (3040873)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=3856156372:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 15.97/3.18 % (3040874)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=3872938655:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 15.97/3.18 % (3040870)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=2592775790:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 15.97/3.18 % (3040871)Instruction limit reached!
% 15.97/3.18 % (3040871)------------------------------
% 15.97/3.18 % (3040871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.97/3.18 % (3040871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.97/3.18 % (3040871)CaDiCaL version: 2.1.3
% 15.97/3.18 % (3040871)Termination reason: Instruction limit
% 15.97/3.18 % (3040871)Termination phase: Saturation
% 15.97/3.18 % (3040871)Time elapsed: 0.137 s
% 15.97/3.18 % (3040871)Peak memory usage: 89 MB
% 15.97/3.18 % (3040871)Instructions burned: 136 (million)
% 15.97/3.18 % (3040872)Instruction limit reached!
% 15.97/3.18 % (3040872)------------------------------
% 15.97/3.18 % (3040872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.97/3.18 % (3040872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.97/3.18 % (3040872)CaDiCaL version: 2.1.3
% 15.97/3.18 % (3040872)Termination reason: Instruction limit
% 15.97/3.18 % (3040872)Termination phase: Saturation
% 15.97/3.18 % (3040872)Time elapsed: 0.179 s
% 15.97/3.18 % (3040872)Peak memory usage: 89 MB
% 15.97/3.18 % (3040872)Instructions burned: 182 (million)
% 15.97/3.18 % (3040873)Instruction limit reached!
% 15.97/3.18 % (3040873)------------------------------
% 15.97/3.18 % (3040873)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.97/3.18 % (3040873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.97/3.18 % (3040873)CaDiCaL version: 2.1.3
% 15.97/3.18 % (3040873)Termination reason: Instruction limit
% 15.97/3.18 % (3040873)Termination phase: Saturation
% 15.97/3.18 % (3040873)Time elapsed: 0.242 s
% 15.97/3.18 % (3040873)Peak memory usage: 90 MB
% 15.97/3.18 % (3040873)Instructions burned: 257 (million)
% 15.97/3.18 % (3040887)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=2837502610:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2996 on theBenchmark for (2996ds/2051Mi)
% 15.97/3.18 % (3040888)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1921640002:i=4948:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/4948Mi)
% 15.97/3.18 % (3040892)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=840660554:i=215:ep=RSTC_2995 on theBenchmark for (2995ds/215Mi)
% 15.97/3.18 % (3040892)Instruction limit reached!
% 15.97/3.18 % (3040892)------------------------------
% 15.97/3.18 % (3040892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.97/3.18 % (3040892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.97/3.18 % (3040892)CaDiCaL version: 2.1.3
% 15.97/3.18 % (3040892)Termination reason: Instruction limit
% 15.97/3.18 % (3040892)Termination phase: Saturation
% 15.97/3.18 % (3040892)Time elapsed: 0.174 s
% 15.97/3.18 % (3040892)Peak memory usage: 92 MB
% 15.97/3.18 % (3040892)Instructions burned: 215 (million)
% 15.97/3.18 % (3040899)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=3487579097:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2992 on theBenchmark for (2992ds/317Mi)
% 15.97/3.18 % (3040874)Instruction limit reached!
% 15.97/3.18 % (3040874)------------------------------
% 15.97/3.18 % (3040874)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.97/3.18 % (3040874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.97/3.18 % (3040874)CaDiCaL version: 2.1.3
% 15.97/3.18 % (3040874)Termination reason: Instruction limit
% 15.97/3.18 % (3040874)Termination phase: Saturation
% 15.97/3.18 % (3040874)Time elapsed: 1.101 s
% 15.97/3.18 % (3040874)Peak memory usage: 101 MB
% 15.97/3.18 % (3040874)Instructions burned: 1187 (million)
% 15.97/3.18 % (3040899)Instruction limit reached!
% 15.97/3.18 % (3040899)------------------------------
% 15.97/3.18 % (3040899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.97/3.18 % (3040899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.97/3.18 % (3040899)CaDiCaL version: 2.1.3
% 15.97/3.18 % (3040899)Termination reason: Instruction limit
% 15.97/3.18 % (3040899)Termination phase: Saturation
% 15.97/3.18 % (3040899)Time elapsed: 0.318 s
% 15.97/3.18 % (3040899)Peak memory usage: 92 MB
% 15.97/3.18 % (3040899)Instructions burned: 318 (million)
% 15.97/3.18 % (3040905)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=4264028717:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2986 on theBenchmark for (2986ds/12125Mi)
% 15.97/3.18 % (3040906)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=331946049:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2986 on theBenchmark for (2986ds/2836Mi)
% 15.97/3.18 % (3040868)First to succeed.
% 15.97/3.18 % (3040868)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3040838"
% 15.97/3.18 % (3040868)Refutation found. Thanks to Tanya!
% 15.97/3.18 % SZS status Unsatisfiable for theBenchmark
% 15.97/3.18 % SZS output start Proof for theBenchmark
% See solution above
% 16.50/3.42 % (3040868)------------------------------
% 16.50/3.42 % (3040868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.50/3.42 % (3040868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.50/3.42 % (3040868)CaDiCaL version: 2.1.3
% 16.50/3.42 % (3040868)Termination reason: Refutation
% 16.50/3.42 % (3040868)Time elapsed: 1.793 s
% 16.50/3.42 % (3040868)Peak memory usage: 157 MB
% 16.50/3.42 % (3040868)Instructions burned: 3445 (million)
% 16.50/3.42 % (3040868)------------------------------
% 16.50/3.42 % (3040868)------------------------------
% 16.50/3.42 % (3040838)Success in time 2.215 s
% 16.50/3.42 % Vampire exiting
%------------------------------------------------------------------------------