%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : REL030-1 : 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 : n012.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:56 PM UTC 2026
% Result : Unsatisfiable 6.96s 1.76s
% Output : Refutation 8.73s
% Verified :
% SZS Type : Refutation
% Derivation depth : 51
% Number of leaves : 48
% Syntax : Number of formulae : 332 ( 161 unt; 34 def)
% Number of atoms : 700 ( 274 equ)
% Maximal formula atoms : 15 ( 2 avg)
% Number of connectives : 719 ( 351 ~; 346 |; 0 &)
% ( 22 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 3 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 24 ( 22 usr; 23 prp; 0-2 aty)
% Number of functors : 23 ( 23 usr; 18 con; 0-2 aty)
% Number of variables : 223 ( 0 sgn 223 !; 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(f17,negated_conjecture,
join(sk1,one) = one,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals_14) ).
fof(f18,plain,
one = join(sk1,one),
inference(reorient_equations,[],[f17]) ).
fof(f19,negated_conjecture,
meet(composition(sk1,sk2),complement(sk3)) != meet(composition(sk1,sk2),complement(composition(sk1,sk3))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals_15) ).
fof(f20,plain,
! [X0] : zero = complement(join(complement(X0),complement(complement(X0)))),
inference(definition_unfolding,[],[f16,f6]) ).
fof(f21,plain,
complement(join(complement(composition(sk1,sk2)),complement(complement(sk3)))) != complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),
inference(definition_unfolding,[],[f19,f6,f6]) ).
fof(f22,definition,
sF0 = join(sk1,one),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f23,plain,
join(sk1,one) = sF0,
inference(reorient_equations,[],[f22]) ).
fof(f24,plain,
one = sF0,
inference(definition_folding,[],[f18,f23]) ).
fof(f25,definition,
sF1 = composition(sk1,sk2),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f26,plain,
composition(sk1,sk2) = sF1,
inference(reorient_equations,[],[f25]) ).
fof(f27,definition,
sF2 = complement(sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f28,plain,
complement(sF1) = sF2,
inference(reorient_equations,[],[f27]) ).
fof(f29,definition,
sF3 = complement(sk3),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f30,plain,
complement(sk3) = sF3,
inference(reorient_equations,[],[f29]) ).
fof(f31,definition,
sF4 = complement(sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f32,plain,
complement(sF3) = sF4,
inference(reorient_equations,[],[f31]) ).
fof(f33,definition,
sF5 = join(sF2,sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f34,plain,
join(sF2,sF4) = sF5,
inference(reorient_equations,[],[f33]) ).
fof(f35,definition,
sF6 = complement(sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f36,plain,
complement(sF5) = sF6,
inference(reorient_equations,[],[f35]) ).
fof(f37,definition,
sF7 = composition(sk1,sk3),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f38,plain,
composition(sk1,sk3) = sF7,
inference(reorient_equations,[],[f37]) ).
fof(f39,definition,
sF8 = complement(sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f40,plain,
complement(sF7) = sF8,
inference(reorient_equations,[],[f39]) ).
fof(f41,definition,
sF9 = complement(sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f42,plain,
complement(sF8) = sF9,
inference(reorient_equations,[],[f41]) ).
fof(f43,definition,
sF10 = join(sF2,sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f44,plain,
join(sF2,sF9) = sF10,
inference(reorient_equations,[],[f43]) ).
fof(f45,definition,
sF11 = complement(sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f46,plain,
complement(sF10) = sF11,
inference(reorient_equations,[],[f45]) ).
fof(f47,plain,
sF6 != sF11,
inference(definition_folding,[],[f21,f46,f44,f42,f40,f38,f28,f26,f36,f34,f32,f30,f28,f26]) ).
fof(f48,plain,
! [X0] : composition(X0,sF0) = X0,
inference(forward_demodulation,[],[f8,f24]) ).
fof(f49,plain,
sF0 = join(one,sk1),
inference(forward_demodulation,[],[f23,f1]) ).
fof(f50,plain,
sF5 = join(sF4,sF2),
inference(forward_demodulation,[],[f34,f1]) ).
fof(f51,plain,
sF10 = join(sF9,sF2),
inference(forward_demodulation,[],[f44,f1]) ).
fof(f52,plain,
sF0 = join(sF0,sk1),
inference(forward_demodulation,[],[f49,f24]) ).
fof(f54,definition,
( spl12_1
<=> complement(sF10) = sF11 ),
introduced(definition,[new_symbols(definition,[spl12_1])],[avatar_definition]) ).
fof(f56,plain,
( complement(sF10) = sF11
| ~ spl12_1 ),
inference(avatar_component_clause,[],[f54]) ).
fof(f57,plain,
spl12_1,
inference(avatar_split_clause,[],[f46,f54]) ).
fof(f59,definition,
( spl12_2
<=> complement(sF5) = sF6 ),
introduced(definition,[new_symbols(definition,[spl12_2])],[avatar_definition]) ).
fof(f61,plain,
( complement(sF5) = sF6
| ~ spl12_2 ),
inference(avatar_component_clause,[],[f59]) ).
fof(f62,plain,
spl12_2,
inference(avatar_split_clause,[],[f36,f59]) ).
fof(f69,definition,
( spl12_4
<=> sF0 = join(sF0,sk1) ),
introduced(definition,[new_symbols(definition,[spl12_4])],[avatar_definition]) ).
fof(f71,plain,
( sF0 = join(sF0,sk1)
| ~ spl12_4 ),
inference(avatar_component_clause,[],[f69]) ).
fof(f72,plain,
spl12_4,
inference(avatar_split_clause,[],[f52,f69]) ).
fof(f82,definition,
( spl12_5
<=> sF6 = sF11 ),
introduced(definition,[new_symbols(definition,[spl12_5])],[avatar_definition]) ).
fof(f84,plain,
( sF6 != sF11
| spl12_5 ),
inference(avatar_component_clause,[],[f82]) ).
fof(f85,plain,
~ spl12_5,
inference(avatar_split_clause,[],[f47,f82]) ).
fof(f86,plain,
! [X0,X1] : complement(X1) = join(composition(X0,complement(composition(converse(X0),X1))),complement(X1)),
inference(superposition,[],[f14,f10]) ).
fof(f95,plain,
! [X0,X1] : complement(X1) = join(complement(X1),composition(X0,complement(composition(converse(X0),X1)))),
inference(forward_demodulation,[],[f86,f1]) ).
fof(f97,definition,
( spl12_6
<=> complement(sk3) = sF3 ),
introduced(definition,[new_symbols(definition,[spl12_6])],[avatar_definition]) ).
fof(f99,plain,
( complement(sk3) = sF3
| ~ spl12_6 ),
inference(avatar_component_clause,[],[f97]) ).
fof(f100,plain,
spl12_6,
inference(avatar_split_clause,[],[f30,f97]) ).
fof(f104,definition,
( spl12_7
<=> complement(sF1) = sF2 ),
introduced(definition,[new_symbols(definition,[spl12_7])],[avatar_definition]) ).
fof(f106,plain,
( complement(sF1) = sF2
| ~ spl12_7 ),
inference(avatar_component_clause,[],[f104]) ).
fof(f107,plain,
spl12_7,
inference(avatar_split_clause,[],[f28,f104]) ).
fof(f111,definition,
( spl12_8
<=> complement(sF3) = sF4 ),
introduced(definition,[new_symbols(definition,[spl12_8])],[avatar_definition]) ).
fof(f113,plain,
( complement(sF3) = sF4
| ~ spl12_8 ),
inference(avatar_component_clause,[],[f111]) ).
fof(f114,plain,
spl12_8,
inference(avatar_split_clause,[],[f32,f111]) ).
fof(f118,definition,
( spl12_9
<=> complement(sF8) = sF9 ),
introduced(definition,[new_symbols(definition,[spl12_9])],[avatar_definition]) ).
fof(f120,plain,
( complement(sF8) = sF9
| ~ spl12_9 ),
inference(avatar_component_clause,[],[f118]) ).
fof(f121,plain,
spl12_9,
inference(avatar_split_clause,[],[f42,f118]) ).
fof(f125,definition,
( spl12_10
<=> complement(sF7) = sF8 ),
introduced(definition,[new_symbols(definition,[spl12_10])],[avatar_definition]) ).
fof(f127,plain,
( complement(sF7) = sF8
| ~ spl12_10 ),
inference(avatar_component_clause,[],[f125]) ).
fof(f128,plain,
spl12_10,
inference(avatar_split_clause,[],[f40,f125]) ).
fof(f140,plain,
! [X0,X1] : join(complement(join(complement(X0),complement(X1))),complement(join(complement(X1),X0))) = X1,
inference(superposition,[],[f4,f1]) ).
fof(f150,plain,
! [X0,X1] : join(complement(join(complement(X1),complement(X0))),complement(join(X0,complement(X1)))) = X1,
inference(superposition,[],[f4,f1]) ).
fof(f154,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))) = X0,
inference(superposition,[],[f1,f4]) ).
fof(f172,definition,
( spl12_11
<=> composition(sk1,sk2) = sF1 ),
introduced(definition,[new_symbols(definition,[spl12_11])],[avatar_definition]) ).
fof(f174,plain,
( composition(sk1,sk2) = sF1
| ~ spl12_11 ),
inference(avatar_component_clause,[],[f172]) ).
fof(f175,plain,
spl12_11,
inference(avatar_split_clause,[],[f26,f172]) ).
fof(f184,definition,
( spl12_12
<=> composition(sk1,sk3) = sF7 ),
introduced(definition,[new_symbols(definition,[spl12_12])],[avatar_definition]) ).
fof(f186,plain,
( composition(sk1,sk3) = sF7
| ~ spl12_12 ),
inference(avatar_component_clause,[],[f184]) ).
fof(f187,plain,
spl12_12,
inference(avatar_split_clause,[],[f38,f184]) ).
fof(f196,plain,
! [X0,X1] : join(X0,complement(X0)) = join(X1,complement(X1)),
inference(superposition,[],[f15,f15]) ).
fof(f198,plain,
( top = join(sF1,sF2)
| ~ spl12_7 ),
inference(superposition,[],[f15,f106]) ).
fof(f208,definition,
( spl12_13
<=> sF10 = join(sF9,sF2) ),
introduced(definition,[new_symbols(definition,[spl12_13])],[avatar_definition]) ).
fof(f210,plain,
( sF10 = join(sF9,sF2)
| ~ spl12_13 ),
inference(avatar_component_clause,[],[f208]) ).
fof(f211,plain,
spl12_13,
inference(avatar_split_clause,[],[f51,f208]) ).
fof(f213,definition,
( spl12_14
<=> sF5 = join(sF4,sF2) ),
introduced(definition,[new_symbols(definition,[spl12_14])],[avatar_definition]) ).
fof(f215,plain,
( sF5 = join(sF4,sF2)
| ~ spl12_14 ),
inference(avatar_component_clause,[],[f213]) ).
fof(f216,plain,
spl12_14,
inference(avatar_split_clause,[],[f50,f213]) ).
fof(f231,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(f242,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f1,f2]) ).
fof(f245,plain,
! [X2,X0,X1] : join(X0,X2) = join(complement(join(complement(X0),X1)),join(X2,complement(join(complement(X0),complement(X1))))),
inference(forward_demodulation,[],[f231,f242]) ).
fof(f257,plain,
! [X0,X1] : composition(converse(X1),X0) = converse(composition(converse(X0),X1)),
inference(superposition,[],[f12,f10]) ).
fof(f260,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(f268,plain,
! [X2,X0,X1] : composition(join(converse(X2),converse(X1)),converse(X0)) = join(converse(composition(X0,X2)),converse(composition(X0,X1))),
inference(superposition,[],[f260,f12]) ).
fof(f278,plain,
! [X2,X0,X1] : composition(join(converse(X2),converse(X1)),converse(X0)) = converse(join(composition(X0,X2),composition(X0,X1))),
inference(forward_demodulation,[],[f268,f11]) ).
fof(f281,plain,
! [X2,X0,X1] : converse(join(composition(X0,X2),composition(X0,X1))) = composition(converse(join(X2,X1)),converse(X0)),
inference(forward_demodulation,[],[f278,f11]) ).
fof(f283,plain,
! [X2,X0,X1] : converse(join(composition(X0,X2),composition(X0,X1))) = converse(composition(X0,join(X2,X1))),
inference(forward_demodulation,[],[f281,f12]) ).
fof(f296,plain,
! [X2,X0,X1] : join(composition(X0,X1),composition(X0,X2)) = converse(converse(composition(X0,join(X1,X2)))),
inference(superposition,[],[f10,f283]) ).
fof(f308,plain,
! [X2,X0,X1] : composition(X0,join(X1,X2)) = join(composition(X0,X1),composition(X0,X2)),
inference(forward_demodulation,[],[f296,f10]) ).
fof(f329,plain,
( ! [X0] : composition(sk1,join(sk2,X0)) = join(sF1,composition(sk1,X0))
| ~ spl12_11 ),
inference(superposition,[],[f308,f174]) ).
fof(f405,plain,
zero = complement(top),
inference(superposition,[],[f20,f15]) ).
fof(f406,plain,
! [X0] : join(zero,complement(join(complement(X0),complement(X0)))) = X0,
inference(superposition,[],[f4,f20]) ).
fof(f498,plain,
! [X0] : join(complement(join(complement(X0),complement(X0))),complement(top)) = X0,
inference(superposition,[],[f150,f15]) ).
fof(f518,plain,
! [X0] : join(complement(join(complement(X0),complement(X0))),zero) = X0,
inference(forward_demodulation,[],[f498,f405]) ).
fof(f563,plain,
! [X0] : zero = complement(join(X0,complement(X0))),
inference(superposition,[],[f20,f196]) ).
fof(f663,plain,
! [X0] : complement(X0) = join(zero,complement(join(complement(complement(X0)),X0))),
inference(superposition,[],[f140,f563]) ).
fof(f710,plain,
! [X0] : complement(X0) = join(zero,complement(join(X0,complement(complement(X0))))),
inference(forward_demodulation,[],[f663,f1]) ).
fof(f750,definition,
( spl12_15
<=> zero = complement(top) ),
introduced(definition,[new_symbols(definition,[spl12_15])],[avatar_definition]) ).
fof(f752,plain,
( zero = complement(top)
| ~ spl12_15 ),
inference(avatar_component_clause,[],[f750]) ).
fof(f753,plain,
spl12_15,
inference(avatar_split_clause,[],[f405,f750]) ).
fof(f757,plain,
! [X0] : converse(converse(X0)) = composition(converse(sF0),X0),
inference(superposition,[],[f257,f48]) ).
fof(f775,plain,
! [X0] : composition(converse(sF0),X0) = X0,
inference(forward_demodulation,[],[f757,f10]) ).
fof(f795,plain,
! [X0] : complement(X0) = join(complement(X0),composition(sF0,complement(X0))),
inference(superposition,[],[f95,f775]) ).
fof(f798,plain,
! [X0,X1] : join(X0,composition(X1,X0)) = composition(join(converse(sF0),X1),X0),
inference(superposition,[],[f9,f775]) ).
fof(f807,plain,
sF0 = converse(sF0),
inference(superposition,[],[f48,f775]) ).
fof(f810,plain,
! [X0] : composition(sF0,X0) = X0,
inference(backward_demodulation,[],[f775,f807]) ).
fof(f820,plain,
! [X0,X1] : join(X0,composition(X1,X0)) = composition(join(sF0,X1),X0),
inference(forward_demodulation,[],[f798,f807]) ).
fof(f824,plain,
! [X0] : complement(X0) = join(complement(X0),complement(X0)),
inference(backward_demodulation,[],[f795,f810]) ).
fof(f836,plain,
! [X0] : join(complement(complement(X0)),zero) = X0,
inference(backward_demodulation,[],[f518,f824]) ).
fof(f837,plain,
! [X0] : join(zero,complement(complement(X0))) = X0,
inference(backward_demodulation,[],[f406,f824]) ).
fof(f867,plain,
( sk3 = join(complement(sF3),zero)
| ~ spl12_6 ),
inference(superposition,[],[f836,f99]) ).
fof(f869,plain,
( sF3 = join(complement(sF4),zero)
| ~ spl12_8 ),
inference(superposition,[],[f836,f113]) ).
fof(f870,plain,
( sF5 = join(complement(sF6),zero)
| ~ spl12_2 ),
inference(superposition,[],[f836,f61]) ).
fof(f871,plain,
( sF7 = join(complement(sF8),zero)
| ~ spl12_10 ),
inference(superposition,[],[f836,f127]) ).
fof(f887,plain,
( sF7 = join(zero,complement(sF8))
| ~ spl12_10 ),
inference(forward_demodulation,[],[f871,f1]) ).
fof(f888,plain,
( sF5 = join(zero,complement(sF6))
| ~ spl12_2 ),
inference(forward_demodulation,[],[f870,f1]) ).
fof(f889,plain,
( sF3 = join(zero,complement(sF4))
| ~ spl12_8 ),
inference(forward_demodulation,[],[f869,f1]) ).
fof(f891,plain,
( sk3 = join(zero,complement(sF3))
| ~ spl12_6 ),
inference(forward_demodulation,[],[f867,f1]) ).
fof(f894,plain,
( sF7 = join(zero,sF9)
| ~ spl12_9
| ~ spl12_10 ),
inference(forward_demodulation,[],[f887,f120]) ).
fof(f895,plain,
( sk3 = join(zero,sF4)
| ~ spl12_6
| ~ spl12_8 ),
inference(forward_demodulation,[],[f891,f113]) ).
fof(f901,plain,
( composition(join(sF0,sk1),sk2) = join(sk2,sF1)
| ~ spl12_11 ),
inference(superposition,[],[f820,f174]) ).
fof(f908,plain,
( ! [X0] : composition(sF0,X0) = join(X0,composition(sk1,X0))
| ~ spl12_4 ),
inference(superposition,[],[f820,f71]) ).
fof(f946,plain,
( ! [X0] : join(X0,composition(sk1,X0)) = X0
| ~ spl12_4 ),
inference(forward_demodulation,[],[f908,f810]) ).
fof(f949,plain,
( composition(join(sF0,sk1),sk2) = join(sF1,sk2)
| ~ spl12_11 ),
inference(forward_demodulation,[],[f901,f1]) ).
fof(f960,plain,
( join(sF1,sk2) = composition(sF0,sk2)
| ~ spl12_4
| ~ spl12_11 ),
inference(forward_demodulation,[],[f949,f71]) ).
fof(f966,plain,
( sk2 = join(sF1,sk2)
| ~ spl12_4
| ~ spl12_11 ),
inference(forward_demodulation,[],[f960,f810]) ).
fof(f998,plain,
( ! [X0,X1] : join(X0,X1) = join(X0,join(composition(sk1,X0),X1))
| ~ spl12_4 ),
inference(superposition,[],[f2,f946]) ).
fof(f1019,definition,
( spl12_16
<=> sk2 = join(sF1,sk2) ),
introduced(definition,[new_symbols(definition,[spl12_16])],[avatar_definition]) ).
fof(f1021,plain,
( sk2 = join(sF1,sk2)
| ~ spl12_16 ),
inference(avatar_component_clause,[],[f1019]) ).
fof(f1022,plain,
( spl12_16
| ~ spl12_4
| ~ spl12_11 ),
inference(avatar_split_clause,[],[f966,f172,f69,f1019]) ).
fof(f1096,plain,
! [X0,X1] : join(X0,X1) = join(complement(join(complement(X0),complement(X0))),join(X1,zero)),
inference(superposition,[],[f245,f563]) ).
fof(f1103,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),complement(complement(X1))))) = join(complement(join(complement(X0),X1)),X0),
inference(superposition,[],[f245,f4]) ).
fof(f1106,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,[],[f245,f824]) ).
fof(f1115,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),complement(X1)))) = X0,
inference(forward_demodulation,[],[f1106,f154]) ).
fof(f1118,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),complement(complement(X1))))) = join(X0,complement(join(complement(X0),X1))),
inference(forward_demodulation,[],[f1103,f1]) ).
fof(f1119,plain,
! [X0,X1] : join(X0,X1) = join(complement(complement(X0)),join(X1,zero)),
inference(forward_demodulation,[],[f1096,f824]) ).
fof(f1139,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),X1))) = X0,
inference(forward_demodulation,[],[f1118,f1115]) ).
fof(f1190,plain,
( ! [X0] : join(X0,complement(complement(X0))) = X0
| ~ spl12_4 ),
inference(superposition,[],[f1139,f946]) ).
fof(f1192,plain,
! [X0] : join(X0,zero) = X0,
inference(superposition,[],[f1139,f563]) ).
fof(f1199,plain,
! [X0,X1] : join(complement(complement(X0)),X1) = join(complement(complement(X0)),complement(join(complement(join(complement(complement(X0)),X1)),X0))),
inference(superposition,[],[f140,f1139]) ).
fof(f1212,plain,
! [X0,X1] : join(complement(complement(X0)),X1) = join(complement(complement(X0)),complement(join(X0,complement(join(complement(complement(X0)),X1))))),
inference(forward_demodulation,[],[f1199,f1]) ).
fof(f1222,plain,
! [X0] : complement(complement(X0)) = X0,
inference(backward_demodulation,[],[f836,f1192]) ).
fof(f1223,plain,
! [X0,X1] : join(X0,X1) = join(complement(complement(X0)),X1),
inference(backward_demodulation,[],[f1119,f1192]) ).
fof(f1227,plain,
( ! [X0] : complement(X0) = join(zero,complement(X0))
| ~ spl12_4 ),
inference(backward_demodulation,[],[f710,f1190]) ).
fof(f1247,plain,
! [X0,X1] : join(X0,X1) = join(complement(complement(X0)),complement(join(X0,complement(join(X0,X1))))),
inference(backward_demodulation,[],[f1212,f1223]) ).
fof(f1269,plain,
! [X0] : join(zero,X0) = X0,
inference(backward_demodulation,[],[f837,f1222]) ).
fof(f1293,plain,
( sF3 = complement(sF4)
| ~ spl12_4
| ~ spl12_8 ),
inference(backward_demodulation,[],[f889,f1227]) ).
fof(f1294,plain,
( sF5 = complement(sF6)
| ~ spl12_2
| ~ spl12_4 ),
inference(backward_demodulation,[],[f888,f1227]) ).
fof(f1307,plain,
! [X0,X1] : join(X0,X1) = join(X0,complement(join(X0,complement(join(X0,X1))))),
inference(forward_demodulation,[],[f1247,f1222]) ).
fof(f1321,plain,
( sk3 = sF4
| ~ spl12_6
| ~ spl12_8 ),
inference(backward_demodulation,[],[f895,f1269]) ).
fof(f1322,plain,
( sF7 = sF9
| ~ spl12_9
| ~ spl12_10 ),
inference(backward_demodulation,[],[f894,f1269]) ).
fof(f1355,plain,
( sF10 = join(sF7,sF2)
| ~ spl12_9
| ~ spl12_10
| ~ spl12_13 ),
inference(backward_demodulation,[],[f210,f1322]) ).
fof(f1370,plain,
( sF7 = composition(sk1,sF4)
| ~ spl12_6
| ~ spl12_8
| ~ spl12_12 ),
inference(backward_demodulation,[],[f186,f1321]) ).
fof(f1432,plain,
! [X0,X1] : complement(X0) = join(complement(join(X0,complement(X1))),complement(join(X0,X1))),
inference(superposition,[],[f4,f1222]) ).
fof(f1438,plain,
! [X0,X1] : complement(X0) = join(complement(join(complement(X1),X0)),complement(join(X0,X1))),
inference(superposition,[],[f140,f1222]) ).
fof(f1478,plain,
! [X0,X1] : complement(X0) = join(complement(join(X0,X1)),complement(join(X0,complement(X1)))),
inference(forward_demodulation,[],[f1432,f1]) ).
fof(f1530,plain,
! [X0,X1] : join(X0,X1) = join(join(X0,X1),complement(complement(X0))),
inference(superposition,[],[f1139,f1478]) ).
fof(f1535,plain,
! [X0,X1] : join(X0,X1) = join(complement(complement(X0)),join(X0,X1)),
inference(forward_demodulation,[],[f1530,f1]) ).
fof(f1566,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X1,complement(complement(X0)))),
inference(forward_demodulation,[],[f1535,f242]) ).
fof(f1583,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X1,X0)),
inference(forward_demodulation,[],[f1566,f1222]) ).
fof(f1629,plain,
( ! [X0] : complement(composition(sk1,complement(X0))) = join(complement(complement(X0)),complement(join(composition(sk1,complement(X0)),X0)))
| ~ spl12_4 ),
inference(superposition,[],[f1438,f946]) ).
fof(f1659,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(complement(X0)),complement(join(complement(join(complement(X1),X0)),join(X0,X1)))),
inference(superposition,[],[f4,f1438]) ).
fof(f1672,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(complement(X0)),complement(join(join(X0,X1),complement(join(complement(X1),X0))))),
inference(forward_demodulation,[],[f1659,f1]) ).
fof(f1697,plain,
( ! [X0] : complement(composition(sk1,complement(X0))) = join(complement(complement(X0)),complement(join(X0,composition(sk1,complement(X0)))))
| ~ spl12_4 ),
inference(forward_demodulation,[],[f1629,f1]) ).
fof(f1721,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(complement(X0)),complement(join(X0,join(X1,complement(join(complement(X1),X0)))))),
inference(forward_demodulation,[],[f1672,f2]) ).
fof(f1741,plain,
( ! [X0] : complement(composition(sk1,complement(X0))) = join(X0,complement(join(X0,composition(sk1,complement(X0)))))
| ~ spl12_4 ),
inference(forward_demodulation,[],[f1697,f1222]) ).
fof(f1755,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(complement(X0)),complement(join(X0,X1))),
inference(forward_demodulation,[],[f1721,f1139]) ).
fof(f1780,plain,
! [X0,X1] : join(complement(X1),X0) = join(X0,complement(join(X0,X1))),
inference(forward_demodulation,[],[f1755,f1222]) ).
fof(f1796,plain,
! [X0,X1] : join(X0,X1) = join(X0,complement(join(complement(X1),X0))),
inference(backward_demodulation,[],[f1307,f1780]) ).
fof(f1800,plain,
( ! [X0] : complement(composition(sk1,complement(X0))) = join(complement(composition(sk1,complement(X0))),X0)
| ~ spl12_4 ),
inference(backward_demodulation,[],[f1741,f1780]) ).
fof(f1814,plain,
( ! [X0] : complement(composition(sk1,complement(X0))) = join(X0,complement(composition(sk1,complement(X0))))
| ~ spl12_4 ),
inference(forward_demodulation,[],[f1800,f1]) ).
fof(f1844,plain,
! [X0] : complement(zero) = join(complement(join(complement(X0),zero)),complement(X0)),
inference(superposition,[],[f1438,f1269]) ).
fof(f1852,plain,
top = complement(zero),
inference(superposition,[],[f15,f1269]) ).
fof(f1865,plain,
! [X0] : complement(zero) = join(complement(X0),complement(join(complement(X0),zero))),
inference(forward_demodulation,[],[f1844,f1]) ).
fof(f1871,plain,
! [X0] : complement(zero) = join(complement(zero),complement(X0)),
inference(forward_demodulation,[],[f1865,f1780]) ).
fof(f1873,plain,
! [X0] : top = join(top,complement(X0)),
inference(forward_demodulation,[],[f1871,f1852]) ).
fof(f2042,plain,
! [X0,X1] : join(X1,complement(X0)) = join(X1,complement(join(X0,X1))),
inference(superposition,[],[f1796,f1222]) ).
fof(f2202,plain,
! [X2,X0,X1] : join(composition(X0,X2),complement(composition(X0,X1))) = join(composition(X0,X2),complement(composition(X0,join(X1,X2)))),
inference(superposition,[],[f2042,f308]) ).
fof(f2207,plain,
( join(sk2,complement(sF1)) = join(sk2,complement(sk2))
| ~ spl12_16 ),
inference(superposition,[],[f2042,f1021]) ).
fof(f2208,plain,
( join(sF2,complement(sF4)) = join(sF2,complement(sF5))
| ~ spl12_14 ),
inference(superposition,[],[f2042,f215]) ).
fof(f2247,plain,
( join(sF2,complement(sF4)) = join(sF2,sF6)
| ~ spl12_2
| ~ spl12_14 ),
inference(forward_demodulation,[],[f2208,f61]) ).
fof(f2248,plain,
( top = join(sk2,complement(sF1))
| ~ spl12_16 ),
inference(forward_demodulation,[],[f2207,f15]) ).
fof(f2275,plain,
( join(sF2,sF6) = join(sF2,sF3)
| ~ spl12_2
| ~ spl12_4
| ~ spl12_8
| ~ spl12_14 ),
inference(forward_demodulation,[],[f2247,f1293]) ).
fof(f2276,plain,
( top = join(sk2,sF2)
| ~ spl12_7
| ~ spl12_16 ),
inference(forward_demodulation,[],[f2248,f106]) ).
fof(f2292,plain,
( join(sF2,sF6) = join(sF3,sF2)
| ~ spl12_2
| ~ spl12_4
| ~ spl12_8
| ~ spl12_14 ),
inference(forward_demodulation,[],[f2275,f1]) ).
fof(f2293,plain,
( top = join(sF2,sk2)
| ~ spl12_7
| ~ spl12_16 ),
inference(forward_demodulation,[],[f2276,f1]) ).
fof(f2348,plain,
! [X0] : top = join(top,X0),
inference(superposition,[],[f1873,f1222]) ).
fof(f3897,plain,
( join(sF2,sF4) = join(sF2,sF5)
| ~ spl12_14 ),
inference(superposition,[],[f1583,f215]) ).
fof(f3935,plain,
( join(sF2,sF4) = join(sF5,sF2)
| ~ spl12_14 ),
inference(forward_demodulation,[],[f3897,f1]) ).
fof(f3972,plain,
( join(sF4,sF2) = join(sF5,sF2)
| ~ spl12_14 ),
inference(forward_demodulation,[],[f3935,f1]) ).
fof(f4000,plain,
( sF5 = join(sF5,sF2)
| ~ spl12_14 ),
inference(forward_demodulation,[],[f3972,f215]) ).
fof(f4778,definition,
( spl12_23
<=> sF7 = composition(sk1,sF4) ),
introduced(definition,[new_symbols(definition,[spl12_23])],[avatar_definition]) ).
fof(f4780,plain,
( sF7 = composition(sk1,sF4)
| ~ spl12_23 ),
inference(avatar_component_clause,[],[f4778]) ).
fof(f4781,plain,
( spl12_23
| ~ spl12_6
| ~ spl12_8
| ~ spl12_12 ),
inference(avatar_split_clause,[],[f1370,f184,f111,f97,f4778]) ).
fof(f4804,definition,
( spl12_24
<=> sF5 = join(sF5,sF2) ),
introduced(definition,[new_symbols(definition,[spl12_24])],[avatar_definition]) ).
fof(f4806,plain,
( sF5 = join(sF5,sF2)
| ~ spl12_24 ),
inference(avatar_component_clause,[],[f4804]) ).
fof(f4807,plain,
( spl12_24
| ~ spl12_14 ),
inference(avatar_split_clause,[],[f4000,f213,f4804]) ).
fof(f5014,definition,
( spl12_25
<=> top = join(sF2,sk2) ),
introduced(definition,[new_symbols(definition,[spl12_25])],[avatar_definition]) ).
fof(f5016,plain,
( top = join(sF2,sk2)
| ~ spl12_25 ),
inference(avatar_component_clause,[],[f5014]) ).
fof(f5017,plain,
( spl12_25
| ~ spl12_7
| ~ spl12_16 ),
inference(avatar_split_clause,[],[f2293,f1019,f104,f5014]) ).
fof(f5082,plain,
( ! [X0,X1] : join(X0,composition(sk1,X1)) = join(X0,composition(sk1,join(X0,X1)))
| ~ spl12_4 ),
inference(superposition,[],[f998,f308]) ).
fof(f5188,definition,
( spl12_26
<=> sF10 = join(sF7,sF2) ),
introduced(definition,[new_symbols(definition,[spl12_26])],[avatar_definition]) ).
fof(f5190,plain,
( sF10 = join(sF7,sF2)
| ~ spl12_26 ),
inference(avatar_component_clause,[],[f5188]) ).
fof(f5191,plain,
( spl12_26
| ~ spl12_9
| ~ spl12_10
| ~ spl12_13 ),
inference(avatar_split_clause,[],[f1355,f208,f125,f118,f5188]) ).
fof(f5649,definition,
( spl12_32
<=> sF5 = complement(sF6) ),
introduced(definition,[new_symbols(definition,[spl12_32])],[avatar_definition]) ).
fof(f5651,plain,
( sF5 = complement(sF6)
| ~ spl12_32 ),
inference(avatar_component_clause,[],[f5649]) ).
fof(f5652,plain,
( spl12_32
| ~ spl12_2
| ~ spl12_4 ),
inference(avatar_split_clause,[],[f1294,f69,f59,f5649]) ).
fof(f6201,plain,
( ! [X0,X1] : join(X1,composition(sk1,join(X0,X1))) = join(X1,composition(sk1,X0))
| ~ spl12_4 ),
inference(superposition,[],[f5082,f1]) ).
fof(f6206,plain,
( ! [X0] : join(X0,composition(sk1,complement(X0))) = join(X0,composition(sk1,top))
| ~ spl12_4 ),
inference(superposition,[],[f5082,f15]) ).
fof(f6208,plain,
( ! [X0,X1] : join(X0,composition(sk1,complement(join(X1,X0)))) = join(X0,composition(sk1,join(X0,complement(X1))))
| ~ spl12_4 ),
inference(superposition,[],[f5082,f2042]) ).
fof(f6211,plain,
( ! [X0,X1] : join(X1,composition(sk1,complement(join(X1,X0)))) = join(X1,composition(sk1,join(complement(X0),X1)))
| ~ spl12_4 ),
inference(superposition,[],[f5082,f1780]) ).
fof(f6238,plain,
( join(sF2,composition(sk1,sk2)) = join(sF2,composition(sk1,top))
| ~ spl12_4
| ~ spl12_25 ),
inference(superposition,[],[f5082,f5016]) ).
fof(f6319,plain,
( join(sF2,sF1) = join(sF2,composition(sk1,top))
| ~ spl12_4
| ~ spl12_11
| ~ spl12_25 ),
inference(forward_demodulation,[],[f6238,f174]) ).
fof(f6336,plain,
( ! [X0,X1] : join(X0,composition(sk1,complement(join(X1,X0)))) = join(X0,composition(sk1,complement(X1)))
| ~ spl12_4 ),
inference(forward_demodulation,[],[f6208,f5082]) ).
fof(f6341,plain,
( ! [X0,X1] : join(X1,composition(sk1,complement(join(X1,X0)))) = join(X1,composition(sk1,complement(X0)))
| ~ spl12_4 ),
inference(backward_demodulation,[],[f6211,f6201]) ).
fof(f6360,plain,
( join(sF1,sF2) = join(sF2,composition(sk1,top))
| ~ spl12_4
| ~ spl12_11
| ~ spl12_25 ),
inference(forward_demodulation,[],[f6319,f1]) ).
fof(f6378,plain,
( top = join(sF2,composition(sk1,top))
| ~ spl12_4
| ~ spl12_7
| ~ spl12_11
| ~ spl12_25 ),
inference(forward_demodulation,[],[f6360,f198]) ).
fof(f6847,plain,
! [X2,X0,X1] : join(X1,complement(join(X0,join(X1,X2)))) = join(complement(join(X2,X0)),X1),
inference(superposition,[],[f1780,f242]) ).
fof(f8188,definition,
( spl12_39
<=> join(sF2,sF6) = join(sF3,sF2) ),
introduced(definition,[new_symbols(definition,[spl12_39])],[avatar_definition]) ).
fof(f8190,plain,
( join(sF2,sF6) = join(sF3,sF2)
| ~ spl12_39 ),
inference(avatar_component_clause,[],[f8188]) ).
fof(f8191,plain,
( spl12_39
| ~ spl12_2
| ~ spl12_4
| ~ spl12_8
| ~ spl12_14 ),
inference(avatar_split_clause,[],[f2292,f213,f111,f69,f59,f8188]) ).
fof(f9675,plain,
( ! [X0] : join(complement(join(complement(X0),complement(composition(sk1,complement(complement(X0)))))),complement(join(complement(X0),composition(sk1,top)))) = X0
| ~ spl12_4 ),
inference(superposition,[],[f4,f6206]) ).
fof(f9701,plain,
( ! [X0] : join(X0,complement(join(X0,composition(sk1,complement(X0))))) = join(complement(composition(sk1,top)),X0)
| ~ spl12_4 ),
inference(superposition,[],[f1780,f6206]) ).
fof(f9722,plain,
( ! [X0] : join(complement(composition(sk1,complement(X0))),X0) = join(complement(composition(sk1,top)),X0)
| ~ spl12_4 ),
inference(forward_demodulation,[],[f9701,f1780]) ).
fof(f9735,plain,
( ! [X0] : join(complement(complement(composition(sk1,complement(complement(X0))))),complement(join(complement(X0),composition(sk1,top)))) = X0
| ~ spl12_4 ),
inference(forward_demodulation,[],[f9675,f1814]) ).
fof(f9774,plain,
( ! [X0] : join(X0,complement(composition(sk1,complement(X0)))) = join(complement(composition(sk1,top)),X0)
| ~ spl12_4 ),
inference(forward_demodulation,[],[f9722,f1]) ).
fof(f9783,plain,
( ! [X0] : join(composition(sk1,complement(complement(X0))),complement(join(complement(X0),composition(sk1,top)))) = X0
| ~ spl12_4 ),
inference(forward_demodulation,[],[f9735,f1222]) ).
fof(f9810,plain,
( ! [X0] : complement(composition(sk1,complement(X0))) = join(complement(composition(sk1,top)),X0)
| ~ spl12_4 ),
inference(forward_demodulation,[],[f9774,f1814]) ).
fof(f9814,plain,
( ! [X0] : join(composition(sk1,X0),complement(join(complement(X0),composition(sk1,top)))) = X0
| ~ spl12_4 ),
inference(forward_demodulation,[],[f9783,f1222]) ).
fof(f9877,plain,
( sF1 = join(composition(sk1,sF1),complement(join(sF2,composition(sk1,top))))
| ~ spl12_4
| ~ spl12_7 ),
inference(superposition,[],[f9814,f106]) ).
fof(f9906,plain,
( ! [X0] : complement(composition(sk1,X0)) = join(complement(X0),complement(join(composition(sk1,X0),complement(complement(join(complement(X0),composition(sk1,top)))))))
| ~ spl12_4 ),
inference(superposition,[],[f1478,f9814]) ).
fof(f9925,plain,
( ! [X0] : complement(composition(sk1,X0)) = join(complement(X0),complement(join(composition(sk1,X0),join(complement(X0),composition(sk1,top)))))
| ~ spl12_4 ),
inference(forward_demodulation,[],[f9906,f1222]) ).
fof(f9943,plain,
( sF1 = join(composition(sk1,sF1),complement(top))
| ~ spl12_4
| ~ spl12_7
| ~ spl12_11
| ~ spl12_25 ),
inference(forward_demodulation,[],[f9877,f6378]) ).
fof(f9956,plain,
( ! [X0] : complement(composition(sk1,X0)) = join(complement(join(composition(sk1,top),composition(sk1,X0))),complement(X0))
| ~ spl12_4 ),
inference(forward_demodulation,[],[f9925,f6847]) ).
fof(f9969,plain,
( sF1 = join(complement(top),composition(sk1,sF1))
| ~ spl12_4
| ~ spl12_7
| ~ spl12_11
| ~ spl12_25 ),
inference(forward_demodulation,[],[f9943,f1]) ).
fof(f9979,plain,
( ! [X0] : complement(composition(sk1,X0)) = join(complement(X0),complement(join(composition(sk1,top),composition(sk1,X0))))
| ~ spl12_4 ),
inference(forward_demodulation,[],[f9956,f1]) ).
fof(f9989,plain,
( sF1 = join(zero,composition(sk1,sF1))
| ~ spl12_4
| ~ spl12_7
| ~ spl12_11
| ~ spl12_15
| ~ spl12_25 ),
inference(forward_demodulation,[],[f9969,f752]) ).
fof(f9996,plain,
( ! [X0] : complement(composition(sk1,X0)) = join(complement(X0),complement(composition(sk1,join(top,X0))))
| ~ spl12_4 ),
inference(forward_demodulation,[],[f9979,f308]) ).
fof(f10003,plain,
( sF1 = composition(sk1,sF1)
| ~ spl12_4
| ~ spl12_7
| ~ spl12_11
| ~ spl12_15
| ~ spl12_25 ),
inference(forward_demodulation,[],[f9989,f1269]) ).
fof(f10009,plain,
( ! [X0] : complement(composition(sk1,X0)) = join(complement(X0),complement(composition(sk1,top)))
| ~ spl12_4 ),
inference(forward_demodulation,[],[f9996,f2348]) ).
fof(f10111,plain,
( ! [X0,X1] : join(complement(composition(sk1,X0)),X1) = join(complement(X0),join(complement(composition(sk1,top)),X1))
| ~ spl12_4 ),
inference(superposition,[],[f2,f10009]) ).
fof(f10112,plain,
( ! [X0,X1] : join(X1,complement(composition(sk1,X0))) = join(complement(X0),join(complement(composition(sk1,top)),X1))
| ~ spl12_4 ),
inference(superposition,[],[f242,f10009]) ).
fof(f10125,plain,
( ! [X0] : join(complement(composition(sk1,top)),complement(complement(X0))) = join(complement(composition(sk1,top)),complement(complement(composition(sk1,X0))))
| ~ spl12_4 ),
inference(superposition,[],[f2042,f10009]) ).
fof(f10127,plain,
( ! [X0] : join(complement(composition(sk1,top)),complement(complement(X0))) = complement(composition(sk1,complement(complement(complement(composition(sk1,X0))))))
| ~ spl12_4 ),
inference(forward_demodulation,[],[f10125,f9810]) ).
fof(f10140,plain,
( ! [X0,X1] : join(X1,complement(composition(sk1,X0))) = join(complement(X0),complement(composition(sk1,complement(X1))))
| ~ spl12_4 ),
inference(forward_demodulation,[],[f10112,f9810]) ).
fof(f10141,plain,
( ! [X0,X1] : join(complement(composition(sk1,X0)),X1) = join(complement(X0),complement(composition(sk1,complement(X1))))
| ~ spl12_4 ),
inference(forward_demodulation,[],[f10111,f9810]) ).
fof(f10174,plain,
( ! [X0] : complement(composition(sk1,complement(composition(sk1,X0)))) = join(complement(composition(sk1,top)),complement(complement(X0)))
| ~ spl12_4 ),
inference(forward_demodulation,[],[f10127,f1222]) ).
fof(f10213,plain,
( ! [X0] : complement(composition(sk1,complement(composition(sk1,X0)))) = join(complement(top),complement(composition(sk1,complement(complement(complement(X0))))))
| ~ spl12_4 ),
inference(forward_demodulation,[],[f10174,f10141]) ).
fof(f10243,plain,
( ! [X0] : complement(composition(sk1,complement(composition(sk1,X0)))) = join(complement(top),complement(composition(sk1,complement(X0))))
| ~ spl12_4 ),
inference(forward_demodulation,[],[f10213,f1222]) ).
fof(f10256,plain,
( ! [X0] : complement(composition(sk1,complement(composition(sk1,X0)))) = join(zero,complement(composition(sk1,complement(X0))))
| ~ spl12_4
| ~ spl12_15 ),
inference(forward_demodulation,[],[f10243,f752]) ).
fof(f10267,plain,
( ! [X0] : complement(composition(sk1,complement(X0))) = complement(composition(sk1,complement(composition(sk1,X0))))
| ~ spl12_4
| ~ spl12_15 ),
inference(forward_demodulation,[],[f10256,f1269]) ).
fof(f10776,definition,
( spl12_48
<=> sF1 = composition(sk1,sF1) ),
introduced(definition,[new_symbols(definition,[spl12_48])],[avatar_definition]) ).
fof(f10778,plain,
( sF1 = composition(sk1,sF1)
| ~ spl12_48 ),
inference(avatar_component_clause,[],[f10776]) ).
fof(f10779,plain,
( spl12_48
| ~ spl12_4
| ~ spl12_7
| ~ spl12_11
| ~ spl12_15
| ~ spl12_25 ),
inference(avatar_split_clause,[],[f10003,f5014,f750,f172,f104,f69,f10776]) ).
fof(f10790,plain,
( ! [X0] : join(sF1,composition(sk1,X0)) = composition(sk1,join(sF1,X0))
| ~ spl12_48 ),
inference(superposition,[],[f308,f10778]) ).
fof(f10801,plain,
( ! [X0] : composition(sk1,join(sk2,X0)) = composition(sk1,join(sF1,X0))
| ~ spl12_11
| ~ spl12_48 ),
inference(forward_demodulation,[],[f10790,f329]) ).
fof(f10812,plain,
( ! [X0] : join(sF1,composition(sk1,X0)) = composition(sk1,join(sF1,X0))
| ~ spl12_11
| ~ spl12_48 ),
inference(backward_demodulation,[],[f329,f10801]) ).
fof(f10865,plain,
( ! [X0] : join(composition(sk1,X0),complement(sF1)) = join(composition(sk1,X0),complement(composition(sk1,join(sF1,X0))))
| ~ spl12_11
| ~ spl12_48 ),
inference(superposition,[],[f2042,f10812]) ).
fof(f10867,plain,
( ! [X0] : join(composition(sk1,X0),complement(sF1)) = join(composition(sk1,X0),complement(composition(sk1,sF1)))
| ~ spl12_11
| ~ spl12_48 ),
inference(forward_demodulation,[],[f10865,f2202]) ).
fof(f10894,plain,
( ! [X0] : join(composition(sk1,X0),complement(sF1)) = join(complement(sF1),complement(composition(sk1,complement(composition(sk1,X0)))))
| ~ spl12_4
| ~ spl12_11
| ~ spl12_48 ),
inference(forward_demodulation,[],[f10867,f10140]) ).
fof(f10909,plain,
( ! [X0] : join(composition(sk1,X0),complement(sF1)) = join(complement(sF1),complement(composition(sk1,complement(X0))))
| ~ spl12_4
| ~ spl12_11
| ~ spl12_15
| ~ spl12_48 ),
inference(forward_demodulation,[],[f10894,f10267]) ).
fof(f10920,plain,
( ! [X0] : join(composition(sk1,X0),sF2) = join(sF2,complement(composition(sk1,complement(X0))))
| ~ spl12_4
| ~ spl12_7
| ~ spl12_11
| ~ spl12_15
| ~ spl12_48 ),
inference(forward_demodulation,[],[f10909,f106]) ).
fof(f10927,plain,
( ! [X0] : join(sF2,composition(sk1,X0)) = join(sF2,complement(composition(sk1,complement(X0))))
| ~ spl12_4
| ~ spl12_7
| ~ spl12_11
| ~ spl12_15
| ~ spl12_48 ),
inference(forward_demodulation,[],[f10920,f1]) ).
fof(f16387,plain,
( join(sF2,composition(sk1,complement(sF6))) = join(sF2,composition(sk1,complement(join(sF3,sF2))))
| ~ spl12_4
| ~ spl12_39 ),
inference(superposition,[],[f6341,f8190]) ).
fof(f16532,plain,
( join(sF2,composition(sk1,complement(sF6))) = join(sF2,composition(sk1,complement(sF3)))
| ~ spl12_4
| ~ spl12_39 ),
inference(forward_demodulation,[],[f16387,f6336]) ).
fof(f16632,plain,
( join(sF2,composition(sk1,complement(sF6))) = join(sF2,composition(sk1,sF4))
| ~ spl12_4
| ~ spl12_8
| ~ spl12_39 ),
inference(forward_demodulation,[],[f16532,f113]) ).
fof(f16710,plain,
( join(sF2,sF7) = join(sF2,composition(sk1,complement(sF6)))
| ~ spl12_4
| ~ spl12_8
| ~ spl12_23
| ~ spl12_39 ),
inference(forward_demodulation,[],[f16632,f4780]) ).
fof(f16761,plain,
( join(sF2,sF7) = join(sF2,composition(sk1,sF5))
| ~ spl12_4
| ~ spl12_8
| ~ spl12_23
| ~ spl12_32
| ~ spl12_39 ),
inference(forward_demodulation,[],[f16710,f5651]) ).
fof(f16789,plain,
( join(sF7,sF2) = join(sF2,composition(sk1,sF5))
| ~ spl12_4
| ~ spl12_8
| ~ spl12_23
| ~ spl12_32
| ~ spl12_39 ),
inference(forward_demodulation,[],[f16761,f1]) ).
fof(f16805,plain,
( sF10 = join(sF2,composition(sk1,sF5))
| ~ spl12_4
| ~ spl12_8
| ~ spl12_23
| ~ spl12_26
| ~ spl12_32
| ~ spl12_39 ),
inference(forward_demodulation,[],[f16789,f5190]) ).
fof(f17067,plain,
( ! [X0] : join(X0,complement(sF1)) = join(complement(sF1),complement(composition(sk1,complement(X0))))
| ~ spl12_4
| ~ spl12_48 ),
inference(superposition,[],[f10140,f10778]) ).
fof(f17370,plain,
( ! [X0] : join(X0,sF2) = join(sF2,complement(composition(sk1,complement(X0))))
| ~ spl12_4
| ~ spl12_7
| ~ spl12_48 ),
inference(forward_demodulation,[],[f17067,f106]) ).
fof(f17471,plain,
( ! [X0] : join(X0,sF2) = join(sF2,composition(sk1,X0))
| ~ spl12_4
| ~ spl12_7
| ~ spl12_11
| ~ spl12_15
| ~ spl12_48 ),
inference(forward_demodulation,[],[f17370,f10927]) ).
fof(f17544,plain,
( sF10 = join(sF5,sF2)
| ~ spl12_4
| ~ spl12_7
| ~ spl12_8
| ~ spl12_11
| ~ spl12_15
| ~ spl12_23
| ~ spl12_26
| ~ spl12_32
| ~ spl12_39
| ~ spl12_48 ),
inference(backward_demodulation,[],[f16805,f17471]) ).
fof(f17601,plain,
( sF5 = sF10
| ~ spl12_4
| ~ spl12_7
| ~ spl12_8
| ~ spl12_11
| ~ spl12_15
| ~ spl12_23
| ~ spl12_24
| ~ spl12_26
| ~ spl12_32
| ~ spl12_39
| ~ spl12_48 ),
inference(forward_demodulation,[],[f17544,f4806]) ).
fof(f17636,plain,
( complement(sF5) = sF11
| ~ spl12_1
| ~ spl12_4
| ~ spl12_7
| ~ spl12_8
| ~ spl12_11
| ~ spl12_15
| ~ spl12_23
| ~ spl12_24
| ~ spl12_26
| ~ spl12_32
| ~ spl12_39
| ~ spl12_48 ),
inference(backward_demodulation,[],[f56,f17601]) ).
fof(f17750,plain,
( sF6 = sF11
| ~ spl12_1
| ~ spl12_2
| ~ spl12_4
| ~ spl12_7
| ~ spl12_8
| ~ spl12_11
| ~ spl12_15
| ~ spl12_23
| ~ spl12_24
| ~ spl12_26
| ~ spl12_32
| ~ spl12_39
| ~ spl12_48 ),
inference(forward_demodulation,[],[f17636,f61]) ).
fof(f17766,plain,
( $false
| ~ spl12_1
| ~ spl12_2
| ~ spl12_4
| spl12_5
| ~ spl12_7
| ~ spl12_8
| ~ spl12_11
| ~ spl12_15
| ~ spl12_23
| ~ spl12_24
| ~ spl12_26
| ~ spl12_32
| ~ spl12_39
| ~ spl12_48 ),
inference(forward_subsumption_resolution,[],[f17750,f84]) ).
fof(f17767,plain,
( ~ spl12_1
| ~ spl12_2
| ~ spl12_4
| spl12_5
| ~ spl12_7
| ~ spl12_8
| ~ spl12_11
| ~ spl12_15
| ~ spl12_23
| ~ spl12_24
| ~ spl12_26
| ~ spl12_32
| ~ spl12_39
| ~ spl12_48 ),
inference(avatar_contradiction_clause,[],[f17766]) ).
cnf(s1,plain,
spl12_1,
inference(sat_conversion,[],[f57]) ).
cnf(s2,plain,
spl12_2,
inference(sat_conversion,[],[f62]) ).
cnf(s4,plain,
spl12_4,
inference(sat_conversion,[],[f72]) ).
cnf(s5,plain,
~ spl12_5,
inference(sat_conversion,[],[f85]) ).
cnf(s6,plain,
spl12_6,
inference(sat_conversion,[],[f100]) ).
cnf(s7,plain,
spl12_7,
inference(sat_conversion,[],[f107]) ).
cnf(s8,plain,
spl12_8,
inference(sat_conversion,[],[f114]) ).
cnf(s9,plain,
spl12_9,
inference(sat_conversion,[],[f121]) ).
cnf(s10,plain,
spl12_10,
inference(sat_conversion,[],[f128]) ).
cnf(s11,plain,
spl12_11,
inference(sat_conversion,[],[f175]) ).
cnf(s12,plain,
spl12_12,
inference(sat_conversion,[],[f187]) ).
cnf(s13,plain,
spl12_13,
inference(sat_conversion,[],[f211]) ).
cnf(s14,plain,
spl12_14,
inference(sat_conversion,[],[f216]) ).
cnf(s15,plain,
spl12_15,
inference(sat_conversion,[],[f753]) ).
cnf(s16,plain,
( ~ spl12_4
| ~ spl12_11
| spl12_16 ),
inference(sat_conversion,[],[f1022]) ).
cnf(s23,plain,
( ~ spl12_6
| ~ spl12_8
| ~ spl12_12
| spl12_23 ),
inference(sat_conversion,[],[f4781]) ).
cnf(s24,plain,
( ~ spl12_14
| spl12_24 ),
inference(sat_conversion,[],[f4807]) ).
cnf(s25,plain,
( ~ spl12_7
| ~ spl12_16
| spl12_25 ),
inference(sat_conversion,[],[f5017]) ).
cnf(s26,plain,
( ~ spl12_9
| ~ spl12_10
| ~ spl12_13
| spl12_26 ),
inference(sat_conversion,[],[f5191]) ).
cnf(s32,plain,
( ~ spl12_2
| ~ spl12_4
| spl12_32 ),
inference(sat_conversion,[],[f5652]) ).
cnf(s39,plain,
( ~ spl12_2
| ~ spl12_4
| ~ spl12_8
| ~ spl12_14
| spl12_39 ),
inference(sat_conversion,[],[f8191]) ).
cnf(s48,plain,
( ~ spl12_4
| ~ spl12_7
| ~ spl12_11
| ~ spl12_15
| ~ spl12_25
| spl12_48 ),
inference(sat_conversion,[],[f10779]) ).
cnf(s65,plain,
( ~ spl12_1
| ~ spl12_2
| ~ spl12_4
| spl12_5
| ~ spl12_7
| ~ spl12_8
| ~ spl12_11
| ~ spl12_15
| ~ spl12_23
| ~ spl12_24
| ~ spl12_26
| ~ spl12_32
| ~ spl12_39
| ~ spl12_48 ),
inference(sat_conversion,[],[f17767]) ).
cnf(s67,plain,
spl12_24,
inference(rat,[],[s24,s14]) ).
cnf(s68,plain,
spl12_26,
inference(rat,[],[s26,s10,s13,s9]) ).
cnf(s73,plain,
spl12_23,
inference(rat,[],[s23,s8,s12,s6]) ).
cnf(s84,plain,
spl12_16,
inference(rat,[],[s16,s11,s4]) ).
cnf(s89,plain,
spl12_25,
inference(rat,[],[s25,s7,s84]) ).
cnf(s93,plain,
spl12_48,
inference(rat,[],[s48,s4,s7,s15,s11,s89]) ).
cnf(s96,plain,
spl12_39,
inference(rat,[],[s39,s4,s14,s8,s2]) ).
cnf(s99,plain,
spl12_32,
inference(rat,[],[s32,s4,s2]) ).
cnf(s101,plain,
~ spl12_1,
inference(rat,[],[s65,s93,s96,s2,s68,s67,s73,s15,s11,s8,s7,s5,s4,s99]) ).
cnf(s102,plain,
$false,
inference(rat,[],[s1,s101]) ).
fof(f17793,plain,
$false,
inference(avatar_sat_refutation,[],[s102]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : REL030-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.04/0.32 % Computer : n012.cluster.edu
% 0.04/0.32 % Model : x86_64 x86_64
% 0.04/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.32 % Memory : 8046.5625MB
% 0.04/0.32 % OS : Linux 6.8.0-71-generic
% 0.04/0.32 % CPULimit : 300
% 0.04/0.32 % WCLimit : 300
% 0.04/0.32 % DateTime : Sun Sep 27 22:53:49 UTC 2026
% 0.07/0.32 % CPUTime :
% 0.07/0.32 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.34 Running first-order theorem proving
% 0.07/0.34 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
% 6.96/1.76 % (2845946)Detected a unit-equality problem, will run specialized UEQ schedule.
% 6.96/1.76 % (2845953)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=2868789823:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 6.96/1.76 % (2845957)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=2131458639:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 6.96/1.76 % (2845951)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=4194286338:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 6.96/1.76 % (2845954)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=409221086:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 6.96/1.76 % (2845952)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=2240604006:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 6.96/1.76 % (2845955)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=1231766840:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 6.96/1.76 % (2845956)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=4044251305:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 6.96/1.76 % (2845954)Instruction limit reached!
% 6.96/1.76 % (2845954)------------------------------
% 6.96/1.76 % (2845954)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.96/1.76 % (2845954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.76 % (2845954)CaDiCaL version: 2.1.3
% 6.96/1.76 % (2845954)Termination reason: Instruction limit
% 6.96/1.76 % (2845954)Termination phase: Saturation
% 6.96/1.76 % (2845954)Time elapsed: 0.045 s
% 6.96/1.76 % (2845954)Peak memory usage: 89 MB
% 6.96/1.76 % (2845954)Instructions burned: 139 (million)
% 6.96/1.76 % (2845955)Instruction limit reached!
% 6.96/1.76 % (2845955)------------------------------
% 6.96/1.76 % (2845955)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.96/1.76 % (2845955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.76 % (2845955)CaDiCaL version: 2.1.3
% 6.96/1.76 % (2845955)Termination reason: Instruction limit
% 6.96/1.76 % (2845955)Termination phase: Saturation
% 6.96/1.76 % (2845955)Time elapsed: 0.056 s
% 6.96/1.76 % (2845955)Peak memory usage: 89 MB
% 6.96/1.76 % (2845955)Instructions burned: 181 (million)
% 6.96/1.76 % (2845956)Instruction limit reached!
% 6.96/1.76 % (2845956)------------------------------
% 6.96/1.76 % (2845956)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.96/1.76 % (2845956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.76 % (2845956)CaDiCaL version: 2.1.3
% 6.96/1.76 % (2845956)Termination reason: Instruction limit
% 6.96/1.76 % (2845956)Termination phase: Saturation
% 6.96/1.76 % (2845956)Time elapsed: 0.091 s
% 6.96/1.76 % (2845956)Peak memory usage: 90 MB
% 6.96/1.76 % (2845956)Instructions burned: 259 (million)
% 6.96/1.76 % (2845965)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=328479808:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2998 on theBenchmark for (2998ds/2051Mi)
% 6.96/1.76 % (2845966)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=279948304:i=4948:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/4948Mi)
% 6.96/1.76 % (2845967)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=3735579078:i=215:ep=RSTC_2997 on theBenchmark for (2997ds/215Mi)
% 6.96/1.76 % (2845967)Instruction limit reached!
% 6.96/1.76 % (2845967)------------------------------
% 6.96/1.76 % (2845967)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.96/1.76 % (2845967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.76 % (2845967)CaDiCaL version: 2.1.3
% 6.96/1.76 % (2845967)Termination reason: Instruction limit
% 6.96/1.76 % (2845967)Termination phase: Saturation
% 6.96/1.76 % (2845967)Time elapsed: 0.066 s
% 6.96/1.76 % (2845967)Peak memory usage: 92 MB
% 6.96/1.76 % (2845967)Instructions burned: 215 (million)
% 6.96/1.76 % (2845957)Instruction limit reached!
% 6.96/1.76 % (2845957)------------------------------
% 6.96/1.76 % (2845957)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.96/1.76 % (2845957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.76 % (2845957)CaDiCaL version: 2.1.3
% 6.96/1.76 % (2845957)Termination reason: Instruction limit
% 6.96/1.76 % (2845957)Termination phase: Saturation
% 6.96/1.76 % (2845957)Time elapsed: 0.354 s
% 6.96/1.76 % (2845957)Peak memory usage: 100 MB
% 6.96/1.76 % (2845957)Instructions burned: 1188 (million)
% 6.96/1.76 % (2845971)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=649318564:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2995 on theBenchmark for (2995ds/317Mi)
% 6.96/1.76 % (2845972)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=3633555936:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2995 on theBenchmark for (2995ds/12125Mi)
% 6.96/1.76 % (2845971)Instruction limit reached!
% 6.96/1.76 % (2845971)------------------------------
% 6.96/1.76 % (2845971)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.96/1.76 % (2845971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.76 % (2845971)CaDiCaL version: 2.1.3
% 6.96/1.76 % (2845971)Termination reason: Instruction limit
% 6.96/1.76 % (2845971)Termination phase: Saturation
% 6.96/1.76 % (2845971)Time elapsed: 0.106 s
% 6.96/1.76 % (2845971)Peak memory usage: 93 MB
% 6.96/1.76 % (2845971)Instructions burned: 320 (million)
% 6.96/1.76 % (2845975)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=854534758:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2993 on theBenchmark for (2993ds/2836Mi)
% 6.96/1.76 % (2845965)Instruction limit reached!
% 6.96/1.76 % (2845965)------------------------------
% 6.96/1.76 % (2845965)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.96/1.76 % (2845965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.76 % (2845965)CaDiCaL version: 2.1.3
% 6.96/1.76 % (2845965)Termination reason: Instruction limit
% 6.96/1.76 % (2845965)Termination phase: Saturation
% 6.96/1.76 % (2845965)Time elapsed: 0.736 s
% 6.96/1.76 % (2845965)Peak memory usage: 140 MB
% 6.96/1.76 % (2845965)Instructions burned: 2051 (million)
% 6.96/1.76 % (2845951)First to succeed.
% 6.96/1.76 % (2845951)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2845946"
% 6.96/1.76 % (2845953)Also succeeded, but the first one will report.
% 6.96/1.76 % (2845952)Also succeeded, but the first one will report.
% 6.96/1.76 % (2845977)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=558754424:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2989 on theBenchmark for (2989ds/14534Mi)
% 6.96/1.76 % (2845951)Refutation found. Thanks to Tanya!
% 6.96/1.76 % SZS status Unsatisfiable for theBenchmark
% 6.96/1.76 % SZS output start Proof for theBenchmark
% See solution above
% 8.73/1.86 % (2845951)------------------------------
% 8.73/1.86 % (2845951)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.73/1.86 % (2845951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.73/1.86 % (2845951)CaDiCaL version: 2.1.3
% 8.73/1.86 % (2845951)Termination reason: Refutation
% 8.73/1.86 % (2845951)Time elapsed: 0.909 s
% 8.73/1.86 % (2845951)Peak memory usage: 143 MB
% 8.73/1.86 % (2845951)Instructions burned: 2562 (million)
% 8.73/1.86 % (2845951)------------------------------
% 8.73/1.86 % (2845951)------------------------------
% 8.73/1.86 % (2845946)Success in time 1.217 s
% 8.73/1.86 % Vampire exiting
%------------------------------------------------------------------------------