%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : REL029-3 : 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 : n003.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:55 PM UTC 2026
% Result : Unsatisfiable 17.76s 3.37s
% Output : Refutation 18.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 80
% Number of leaves : 75
% Syntax : Number of formulae : 888 ( 198 unt; 56 def)
% Number of atoms : 2869 ( 770 equ)
% Maximal formula atoms : 21 ( 3 avg)
% Number of connectives : 3923 (1942 ~;1938 |; 0 &)
% ( 43 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 4 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 45 ( 43 usr; 44 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 19 con; 0-2 aty)
% Number of variables : 724 ( 0 sgn 724 !; 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(f7,axiom,
! [X2,X0,X1] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',composition_associativity_5) ).
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,axiom,
! [X2,X0,X1] : join(meet(composition(X0,X1),X2),composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2)))) = composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dedekind_law_14) ).
fof(f18,plain,
! [X2,X0,X1] : composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2))) = join(meet(composition(X0,X1),X2),composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2)))),
inference(reorient_equations,[],[f17]) ).
fof(f19,axiom,
! [X2,X0,X1] : join(meet(composition(X0,X1),X2),meet(composition(X0,meet(X1,composition(converse(X0),X2))),X2)) = meet(composition(X0,meet(X1,composition(converse(X0),X2))),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',modular_law_1_15) ).
fof(f20,plain,
! [X2,X0,X1] : meet(composition(X0,meet(X1,composition(converse(X0),X2))),X2) = join(meet(composition(X0,X1),X2),meet(composition(X0,meet(X1,composition(converse(X0),X2))),X2)),
inference(reorient_equations,[],[f19]) ).
fof(f21,axiom,
! [X2,X0,X1] : join(meet(composition(X0,X1),X2),meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2)) = meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',modular_law_2_16) ).
fof(f22,plain,
! [X2,X0,X1] : meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2) = join(meet(composition(X0,X1),X2),meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2)),
inference(reorient_equations,[],[f21]) ).
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,
meet(composition(sk1,sk3),composition(sk2,sk3)) != composition(meet(sk1,sk2),sk3),
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(f29,plain,
! [X2,X0,X1] : composition(complement(join(complement(X0),complement(composition(X2,converse(X1))))),complement(join(complement(X1),complement(composition(converse(X0),X2))))) = join(complement(join(complement(composition(X0,X1)),complement(X2))),composition(complement(join(complement(X0),complement(composition(X2,converse(X1))))),complement(join(complement(X1),complement(composition(converse(X0),X2)))))),
inference(definition_unfolding,[],[f18,f6,f6,f6,f6,f6]) ).
fof(f30,plain,
! [X2,X0,X1] : complement(join(complement(composition(X0,complement(join(complement(X1),complement(composition(converse(X0),X2)))))),complement(X2))) = join(complement(join(complement(composition(X0,X1)),complement(X2))),complement(join(complement(composition(X0,complement(join(complement(X1),complement(composition(converse(X0),X2)))))),complement(X2)))),
inference(definition_unfolding,[],[f20,f6,f6,f6,f6,f6]) ).
fof(f31,plain,
! [X2,X0,X1] : complement(join(complement(composition(complement(join(complement(X0),complement(composition(X2,converse(X1))))),X1)),complement(X2))) = join(complement(join(complement(composition(X0,X1)),complement(X2))),complement(join(complement(composition(complement(join(complement(X0),complement(composition(X2,converse(X1))))),X1)),complement(X2)))),
inference(definition_unfolding,[],[f22,f6,f6,f6,f6,f6]) ).
fof(f32,plain,
complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))) != composition(complement(join(complement(sk1),complement(sk2))),sk3),
inference(definition_unfolding,[],[f27,f6,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,sk3),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f40,plain,
composition(sk1,sk3) = sF2,
inference(reorient_equations,[],[f39]) ).
fof(f41,definition,
sF3 = complement(sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f42,plain,
complement(sF2) = sF3,
inference(reorient_equations,[],[f41]) ).
fof(f43,definition,
sF4 = composition(sk2,sk3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f44,plain,
composition(sk2,sk3) = sF4,
inference(reorient_equations,[],[f43]) ).
fof(f45,definition,
sF5 = complement(sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f46,plain,
complement(sF4) = sF5,
inference(reorient_equations,[],[f45]) ).
fof(f47,definition,
sF6 = join(sF3,sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f48,plain,
join(sF3,sF5) = sF6,
inference(reorient_equations,[],[f47]) ).
fof(f49,definition,
sF7 = complement(sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f50,plain,
complement(sF6) = sF7,
inference(reorient_equations,[],[f49]) ).
fof(f51,definition,
sF8 = complement(sk1),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f52,plain,
complement(sk1) = sF8,
inference(reorient_equations,[],[f51]) ).
fof(f53,definition,
sF9 = complement(sk2),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f54,plain,
complement(sk2) = sF9,
inference(reorient_equations,[],[f53]) ).
fof(f55,definition,
sF10 = join(sF8,sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f56,plain,
join(sF8,sF9) = sF10,
inference(reorient_equations,[],[f55]) ).
fof(f57,definition,
sF11 = complement(sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f58,plain,
complement(sF10) = sF11,
inference(reorient_equations,[],[f57]) ).
fof(f59,definition,
sF12 = composition(sF11,sk3),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f60,plain,
composition(sF11,sk3) = sF12,
inference(reorient_equations,[],[f59]) ).
fof(f61,plain,
sF7 != sF12,
inference(definition_folding,[],[f32,f60,f58,f56,f54,f52,f50,f48,f46,f44,f42,f40]) ).
fof(f62,plain,
sF0 = sF1,
inference(forward_demodulation,[],[f35,f38]) ).
fof(f63,plain,
zero = complement(top),
inference(backward_demodulation,[],[f28,f15]) ).
fof(f64,plain,
! [X0] : composition(X0,sF1) = X0,
inference(forward_demodulation,[],[f8,f38]) ).
fof(f65,plain,
sF0 = join(sk1,sF1),
inference(forward_demodulation,[],[f34,f38]) ).
fof(f66,plain,
sF1 = join(sk2,sF1),
inference(forward_demodulation,[],[f37,f38]) ).
fof(f68,plain,
! [X0] : composition(X0,sF0) = X0,
inference(forward_demodulation,[],[f64,f62]) ).
fof(f69,plain,
sF0 = join(sF1,sk1),
inference(forward_demodulation,[],[f65,f1]) ).
fof(f70,plain,
sF1 = join(sF1,sk2),
inference(forward_demodulation,[],[f66,f1]) ).
fof(f71,plain,
sF0 = join(sF0,sk1),
inference(forward_demodulation,[],[f69,f62]) ).
fof(f72,plain,
sF0 = join(sF0,sk2),
inference(forward_demodulation,[],[f70,f62]) ).
fof(f81,plain,
! [X2,X0,X1] : join(composition(X0,X1),composition(X2,X1)) = composition(join(X2,X0),X1),
inference(superposition,[],[f9,f1]) ).
fof(f82,plain,
! [X2,X0,X1] : composition(join(X0,X2),X1) = composition(join(X2,X0),X1),
inference(forward_demodulation,[],[f81,f9]) ).
fof(f88,plain,
! [X0,X1] : join(complement(join(complement(X0),complement(X1))),complement(join(complement(X1),X0))) = X1,
inference(superposition,[],[f4,f1]) ).
fof(f99,plain,
! [X0,X1] : join(complement(join(complement(X1),X0)),complement(join(complement(X0),complement(X1)))) = X1,
inference(forward_demodulation,[],[f88,f1]) ).
fof(f105,definition,
( spl13_2
<=> complement(sF6) = sF7 ),
introduced(definition,[new_symbols(definition,[spl13_2])],[avatar_definition]) ).
fof(f107,plain,
( complement(sF6) = sF7
| ~ spl13_2 ),
inference(avatar_component_clause,[],[f105]) ).
fof(f108,plain,
spl13_2,
inference(avatar_split_clause,[],[f50,f105]) ).
fof(f119,plain,
! [X0,X1] : complement(X1) = join(composition(X0,complement(composition(converse(X0),X1))),complement(X1)),
inference(superposition,[],[f14,f10]) ).
fof(f126,plain,
! [X0,X1] : complement(X1) = join(complement(X1),composition(X0,complement(composition(converse(X0),X1)))),
inference(forward_demodulation,[],[f119,f1]) ).
fof(f128,definition,
( spl13_4
<=> composition(sF11,sk3) = sF12 ),
introduced(definition,[new_symbols(definition,[spl13_4])],[avatar_definition]) ).
fof(f130,plain,
( composition(sF11,sk3) = sF12
| ~ spl13_4 ),
inference(avatar_component_clause,[],[f128]) ).
fof(f131,plain,
spl13_4,
inference(avatar_split_clause,[],[f60,f128]) ).
fof(f134,plain,
( ! [X0] : composition(join(sF11,X0),sk3) = join(sF12,composition(X0,sk3))
| ~ spl13_4 ),
inference(superposition,[],[f9,f130]) ).
fof(f139,definition,
( spl13_5
<=> complement(sk2) = sF9 ),
introduced(definition,[new_symbols(definition,[spl13_5])],[avatar_definition]) ).
fof(f141,plain,
( complement(sk2) = sF9
| ~ spl13_5 ),
inference(avatar_component_clause,[],[f139]) ).
fof(f142,plain,
spl13_5,
inference(avatar_split_clause,[],[f54,f139]) ).
fof(f144,definition,
( spl13_6
<=> sF7 = sF12 ),
introduced(definition,[new_symbols(definition,[spl13_6])],[avatar_definition]) ).
fof(f146,plain,
( sF7 != sF12
| spl13_6 ),
inference(avatar_component_clause,[],[f144]) ).
fof(f147,plain,
~ spl13_6,
inference(avatar_split_clause,[],[f61,f144]) ).
fof(f149,definition,
( spl13_7
<=> complement(sk1) = sF8 ),
introduced(definition,[new_symbols(definition,[spl13_7])],[avatar_definition]) ).
fof(f151,plain,
( complement(sk1) = sF8
| ~ spl13_7 ),
inference(avatar_component_clause,[],[f149]) ).
fof(f152,plain,
spl13_7,
inference(avatar_split_clause,[],[f52,f149]) ).
fof(f166,definition,
( spl13_8
<=> complement(sF2) = sF3 ),
introduced(definition,[new_symbols(definition,[spl13_8])],[avatar_definition]) ).
fof(f168,plain,
( complement(sF2) = sF3
| ~ spl13_8 ),
inference(avatar_component_clause,[],[f166]) ).
fof(f169,plain,
spl13_8,
inference(avatar_split_clause,[],[f42,f166]) ).
fof(f181,definition,
( spl13_9
<=> complement(sF10) = sF11 ),
introduced(definition,[new_symbols(definition,[spl13_9])],[avatar_definition]) ).
fof(f183,plain,
( complement(sF10) = sF11
| ~ spl13_9 ),
inference(avatar_component_clause,[],[f181]) ).
fof(f184,plain,
spl13_9,
inference(avatar_split_clause,[],[f58,f181]) ).
fof(f196,definition,
( spl13_10
<=> complement(sF4) = sF5 ),
introduced(definition,[new_symbols(definition,[spl13_10])],[avatar_definition]) ).
fof(f198,plain,
( complement(sF4) = sF5
| ~ spl13_10 ),
inference(avatar_component_clause,[],[f196]) ).
fof(f199,plain,
spl13_10,
inference(avatar_split_clause,[],[f46,f196]) ).
fof(f213,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(f214,plain,
! [X2,X3,X0,X1] : join(composition(X0,X2),join(composition(X1,X2),X3)) = join(composition(join(X0,X1),X2),X3),
inference(superposition,[],[f2,f9]) ).
fof(f219,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f1,f2]) ).
fof(f221,plain,
! [X2,X0,X1] : join(X0,X2) = join(complement(join(complement(X0),X1)),join(X2,complement(join(complement(X0),complement(X1))))),
inference(forward_demodulation,[],[f213,f219]) ).
fof(f226,plain,
! [X0,X1] : converse(join(converse(X0),X1)) = join(X0,converse(X1)),
inference(superposition,[],[f11,f10]) ).
fof(f227,plain,
! [X0,X1] : converse(join(X1,converse(X0))) = join(converse(X1),X0),
inference(superposition,[],[f11,f10]) ).
fof(f244,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(top,X1),
inference(superposition,[],[f2,f15]) ).
fof(f247,plain,
! [X0] : join(complement(join(complement(X0),complement(complement(complement(X0))))),complement(top)) = X0,
inference(superposition,[],[f4,f15]) ).
fof(f248,plain,
! [X0] : join(complement(top),complement(join(complement(X0),complement(complement(complement(X0)))))) = X0,
inference(forward_demodulation,[],[f247,f1]) ).
fof(f252,plain,
! [X0] : join(zero,complement(join(complement(X0),complement(complement(complement(X0)))))) = X0,
inference(forward_demodulation,[],[f248,f63]) ).
fof(f254,definition,
( spl13_11
<=> zero = complement(top) ),
introduced(definition,[new_symbols(definition,[spl13_11])],[avatar_definition]) ).
fof(f256,plain,
( zero = complement(top)
| ~ spl13_11 ),
inference(avatar_component_clause,[],[f254]) ).
fof(f257,plain,
spl13_11,
inference(avatar_split_clause,[],[f63,f254]) ).
fof(f259,definition,
( spl13_12
<=> join(sF8,sF9) = sF10 ),
introduced(definition,[new_symbols(definition,[spl13_12])],[avatar_definition]) ).
fof(f261,plain,
( join(sF8,sF9) = sF10
| ~ spl13_12 ),
inference(avatar_component_clause,[],[f259]) ).
fof(f262,plain,
spl13_12,
inference(avatar_split_clause,[],[f56,f259]) ).
fof(f263,plain,
( ! [X0] : join(sF8,join(sF9,X0)) = join(sF10,X0)
| ~ spl13_12 ),
inference(superposition,[],[f2,f261]) ).
fof(f265,definition,
( spl13_13
<=> join(sF3,sF5) = sF6 ),
introduced(definition,[new_symbols(definition,[spl13_13])],[avatar_definition]) ).
fof(f267,plain,
( join(sF3,sF5) = sF6
| ~ spl13_13 ),
inference(avatar_component_clause,[],[f265]) ).
fof(f268,plain,
spl13_13,
inference(avatar_split_clause,[],[f48,f265]) ).
fof(f269,plain,
( ! [X0] : join(sF3,join(sF5,X0)) = join(sF6,X0)
| ~ spl13_13 ),
inference(superposition,[],[f2,f267]) ).
fof(f271,definition,
( spl13_14
<=> composition(sk1,sk3) = sF2 ),
introduced(definition,[new_symbols(definition,[spl13_14])],[avatar_definition]) ).
fof(f273,plain,
( composition(sk1,sk3) = sF2
| ~ spl13_14 ),
inference(avatar_component_clause,[],[f271]) ).
fof(f274,plain,
spl13_14,
inference(avatar_split_clause,[],[f40,f271]) ).
fof(f283,definition,
( spl13_15
<=> composition(sk2,sk3) = sF4 ),
introduced(definition,[new_symbols(definition,[spl13_15])],[avatar_definition]) ).
fof(f285,plain,
( composition(sk2,sk3) = sF4
| ~ spl13_15 ),
inference(avatar_component_clause,[],[f283]) ).
fof(f286,plain,
spl13_15,
inference(avatar_split_clause,[],[f44,f283]) ).
fof(f294,plain,
! [X0,X1] : composition(X0,converse(X1)) = converse(composition(X1,converse(X0))),
inference(superposition,[],[f12,f10]) ).
fof(f295,plain,
! [X0,X1] : composition(converse(X1),X0) = converse(composition(converse(X0),X1)),
inference(superposition,[],[f12,f10]) ).
fof(f296,plain,
! [X0,X1] : complement(converse(X0)) = join(composition(converse(converse(X1)),complement(converse(composition(X0,X1)))),complement(converse(X0))),
inference(superposition,[],[f14,f12]) ).
fof(f297,plain,
! [X2,X0,X1] : composition(join(X2,converse(X1)),converse(X0)) = join(composition(X2,converse(X0)),converse(composition(X0,X1))),
inference(superposition,[],[f9,f12]) ).
fof(f298,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(f299,plain,
! [X0,X1] : complement(converse(X0)) = join(complement(converse(X0)),composition(converse(converse(X1)),complement(converse(composition(X0,X1))))),
inference(forward_demodulation,[],[f296,f1]) ).
fof(f300,plain,
! [X0,X1] : complement(converse(X0)) = join(complement(converse(X0)),composition(X1,complement(converse(composition(X0,X1))))),
inference(forward_demodulation,[],[f299,f10]) ).
fof(f306,plain,
! [X2,X0,X1] : composition(join(converse(X2),converse(X1)),converse(X0)) = join(converse(composition(X0,X2)),converse(composition(X0,X1))),
inference(superposition,[],[f298,f12]) ).
fof(f316,plain,
! [X2,X0,X1] : composition(join(converse(X2),converse(X1)),converse(X0)) = converse(join(composition(X0,X2),composition(X0,X1))),
inference(forward_demodulation,[],[f306,f11]) ).
fof(f319,plain,
! [X2,X0,X1] : converse(join(composition(X0,X2),composition(X0,X1))) = composition(converse(join(X2,X1)),converse(X0)),
inference(forward_demodulation,[],[f316,f11]) ).
fof(f321,plain,
! [X2,X0,X1] : converse(join(composition(X0,X2),composition(X0,X1))) = converse(composition(X0,join(X2,X1))),
inference(forward_demodulation,[],[f319,f12]) ).
fof(f334,plain,
! [X2,X0,X1] : join(composition(X0,X1),composition(X0,X2)) = converse(converse(composition(X0,join(X1,X2)))),
inference(superposition,[],[f10,f321]) ).
fof(f346,plain,
! [X2,X0,X1] : composition(X0,join(X1,X2)) = join(composition(X0,X1),composition(X0,X2)),
inference(forward_demodulation,[],[f334,f10]) ).
fof(f368,plain,
( ! [X0] : composition(sF11,join(sk3,X0)) = join(sF12,composition(sF11,X0))
| ~ spl13_4 ),
inference(superposition,[],[f346,f130]) ).
fof(f394,plain,
! [X0,X1] : composition(X0,join(sF0,X1)) = join(X0,composition(X0,X1)),
inference(superposition,[],[f346,f68]) ).
fof(f482,definition,
( spl13_16
<=> sF0 = join(sF0,sk1) ),
introduced(definition,[new_symbols(definition,[spl13_16])],[avatar_definition]) ).
fof(f484,plain,
( sF0 = join(sF0,sk1)
| ~ spl13_16 ),
inference(avatar_component_clause,[],[f482]) ).
fof(f485,plain,
spl13_16,
inference(avatar_split_clause,[],[f71,f482]) ).
fof(f487,plain,
( ! [X0] : composition(X0,sF0) = join(X0,composition(X0,sk1))
| ~ spl13_16 ),
inference(superposition,[],[f394,f484]) ).
fof(f539,plain,
( ! [X0] : join(X0,composition(X0,sk1)) = X0
| ~ spl13_16 ),
inference(forward_demodulation,[],[f487,f68]) ).
fof(f573,definition,
( spl13_17
<=> sF0 = join(sF0,sk2) ),
introduced(definition,[new_symbols(definition,[spl13_17])],[avatar_definition]) ).
fof(f575,plain,
( sF0 = join(sF0,sk2)
| ~ spl13_17 ),
inference(avatar_component_clause,[],[f573]) ).
fof(f576,plain,
spl13_17,
inference(avatar_split_clause,[],[f72,f573]) ).
fof(f577,plain,
( ! [X0] : composition(X0,sF0) = join(X0,composition(X0,sk2))
| ~ spl13_17 ),
inference(superposition,[],[f394,f575]) ).
fof(f579,plain,
( ! [X0] : join(X0,composition(X0,sk2)) = X0
| ~ spl13_17 ),
inference(forward_demodulation,[],[f577,f68]) ).
fof(f625,plain,
! [X0] : complement(X0) = join(complement(join(complement(complement(X0)),X0)),complement(top)),
inference(superposition,[],[f99,f15]) ).
fof(f633,plain,
! [X0] : complement(X0) = join(complement(top),complement(join(complement(complement(X0)),X0))),
inference(forward_demodulation,[],[f625,f1]) ).
fof(f654,plain,
! [X0] : complement(X0) = join(complement(top),complement(join(X0,complement(complement(X0))))),
inference(forward_demodulation,[],[f633,f1]) ).
fof(f661,plain,
( ! [X0] : complement(X0) = join(zero,complement(join(X0,complement(complement(X0)))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f654,f256]) ).
fof(f667,plain,
( ! [X0] : complement(complement(X0)) = X0
| ~ spl13_11 ),
inference(backward_demodulation,[],[f252,f661]) ).
fof(f670,plain,
( ! [X0] : complement(X0) = join(zero,complement(join(X0,X0)))
| ~ spl13_11 ),
inference(backward_demodulation,[],[f661,f667]) ).
fof(f677,plain,
( sk1 = complement(sF8)
| ~ spl13_7
| ~ spl13_11 ),
inference(superposition,[],[f667,f151]) ).
fof(f678,plain,
( sk2 = complement(sF9)
| ~ spl13_5
| ~ spl13_11 ),
inference(superposition,[],[f667,f141]) ).
fof(f679,plain,
( sF2 = complement(sF3)
| ~ spl13_8
| ~ spl13_11 ),
inference(superposition,[],[f667,f168]) ).
fof(f680,plain,
( sF4 = complement(sF5)
| ~ spl13_10
| ~ spl13_11 ),
inference(superposition,[],[f667,f198]) ).
fof(f683,plain,
( ! [X0,X1] : complement(X0) = join(complement(join(X0,complement(X1))),complement(join(X0,X1)))
| ~ spl13_11 ),
inference(superposition,[],[f4,f667]) ).
fof(f688,plain,
( ! [X0,X1] : complement(X0) = join(complement(join(X0,X1)),complement(join(complement(X1),X0)))
| ~ spl13_11 ),
inference(superposition,[],[f99,f667]) ).
fof(f694,plain,
( ! [X0,X1] : complement(X0) = join(complement(join(X0,X1)),complement(join(X0,complement(X1))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f683,f1]) ).
fof(f703,plain,
( ! [X0,X1] : complement(X1) = join(complement(join(X0,X1)),complement(join(X1,complement(X0))))
| ~ spl13_11 ),
inference(superposition,[],[f694,f1]) ).
fof(f713,plain,
( ! [X2,X0,X1] : complement(composition(X0,X1)) = join(complement(composition(X0,join(X1,X2))),complement(join(composition(X0,X1),complement(composition(X0,X2)))))
| ~ spl13_11 ),
inference(superposition,[],[f694,f346]) ).
fof(f792,plain,
( ! [X0,X1] : complement(X1) = join(complement(join(X0,X1)),complement(join(complement(X0),X1)))
| ~ spl13_11 ),
inference(superposition,[],[f688,f1]) ).
fof(f828,plain,
( ! [X0,X1] : join(X0,X1) = join(complement(complement(X0)),complement(join(complement(join(X0,X1)),join(complement(X1),X0))))
| ~ spl13_11 ),
inference(superposition,[],[f4,f688]) ).
fof(f837,plain,
( ! [X0,X1] : join(X0,X1) = join(complement(complement(X0)),complement(join(X0,join(complement(join(X0,X1)),complement(X1)))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f828,f219]) ).
fof(f864,plain,
( ! [X0,X1] : join(X0,X1) = join(complement(complement(X0)),complement(join(X0,join(complement(X1),complement(join(X0,X1))))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f837,f1]) ).
fof(f882,plain,
( ! [X0,X1] : join(X0,X1) = join(X0,complement(join(X0,join(complement(X1),complement(join(X0,X1))))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f864,f667]) ).
fof(f934,plain,
( complement(sk1) = join(complement(sF0),complement(join(sk1,complement(sF0))))
| ~ spl13_11
| ~ spl13_16 ),
inference(superposition,[],[f703,f484]) ).
fof(f937,plain,
( complement(sF9) = join(complement(sF10),complement(join(sF9,complement(sF8))))
| ~ spl13_11
| ~ spl13_12 ),
inference(superposition,[],[f703,f261]) ).
fof(f955,plain,
( ! [X0,X1] : complement(complement(join(X0,complement(X1)))) = join(complement(join(complement(join(X0,complement(X1))),join(X1,X0))),complement(complement(X0)))
| ~ spl13_11 ),
inference(superposition,[],[f688,f703]) ).
fof(f965,plain,
( ! [X0,X1] : complement(complement(join(X0,complement(X1)))) = join(complement(complement(X0)),complement(join(complement(join(X0,complement(X1))),join(X1,X0))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f955,f1]) ).
fof(f975,plain,
( complement(sF9) = join(complement(sF10),complement(join(sF9,sk1)))
| ~ spl13_7
| ~ spl13_11
| ~ spl13_12 ),
inference(forward_demodulation,[],[f937,f677]) ).
fof(f978,plain,
( sF8 = join(complement(sF0),complement(join(sk1,complement(sF0))))
| ~ spl13_7
| ~ spl13_11
| ~ spl13_16 ),
inference(forward_demodulation,[],[f934,f151]) ).
fof(f991,plain,
( ! [X0,X1] : complement(complement(join(X0,complement(X1)))) = join(complement(complement(X0)),complement(join(join(X1,X0),complement(join(X0,complement(X1))))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f965,f1]) ).
fof(f999,plain,
( complement(sF9) = join(sF11,complement(join(sF9,sk1)))
| ~ spl13_7
| ~ spl13_9
| ~ spl13_11
| ~ spl13_12 ),
inference(forward_demodulation,[],[f975,f183]) ).
fof(f1009,plain,
( ! [X0,X1] : complement(complement(join(X0,complement(X1)))) = join(complement(complement(X0)),complement(join(X1,join(X0,complement(join(X0,complement(X1)))))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f991,f2]) ).
fof(f1015,plain,
( sk2 = join(sF11,complement(join(sF9,sk1)))
| ~ spl13_5
| ~ spl13_7
| ~ spl13_9
| ~ spl13_11
| ~ spl13_12 ),
inference(forward_demodulation,[],[f999,f678]) ).
fof(f1025,plain,
( ! [X0,X1] : complement(complement(join(X0,complement(X1)))) = join(X0,complement(join(X1,join(X0,complement(join(X0,complement(X1)))))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f1009,f667]) ).
fof(f1038,plain,
( ! [X0,X1] : join(X0,complement(X1)) = join(X0,complement(join(X1,join(X0,complement(join(X0,complement(X1)))))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f1025,f667]) ).
fof(f1044,definition,
( spl13_18
<=> sk1 = complement(sF8) ),
introduced(definition,[new_symbols(definition,[spl13_18])],[avatar_definition]) ).
fof(f1046,plain,
( sk1 = complement(sF8)
| ~ spl13_18 ),
inference(avatar_component_clause,[],[f1044]) ).
fof(f1047,plain,
( spl13_18
| ~ spl13_7
| ~ spl13_11 ),
inference(avatar_split_clause,[],[f677,f254,f149,f1044]) ).
fof(f1049,definition,
( spl13_19
<=> sk2 = complement(sF9) ),
introduced(definition,[new_symbols(definition,[spl13_19])],[avatar_definition]) ).
fof(f1051,plain,
( sk2 = complement(sF9)
| ~ spl13_19 ),
inference(avatar_component_clause,[],[f1049]) ).
fof(f1052,plain,
( spl13_19
| ~ spl13_5
| ~ spl13_11 ),
inference(avatar_split_clause,[],[f678,f254,f139,f1049]) ).
fof(f1056,plain,
! [X0] : converse(converse(X0)) = composition(converse(sF0),X0),
inference(superposition,[],[f295,f68]) ).
fof(f1072,plain,
! [X0] : composition(converse(sF0),X0) = X0,
inference(forward_demodulation,[],[f1056,f10]) ).
fof(f1095,plain,
! [X0,X1] : join(X0,X1) = join(complement(top),join(X1,complement(join(complement(X0),complement(complement(complement(X0))))))),
inference(superposition,[],[f221,f15]) ).
fof(f1121,plain,
! [X0,X1] : join(X0,join(complement(X0),complement(X1))) = join(complement(join(complement(X0),X1)),top),
inference(superposition,[],[f221,f15]) ).
fof(f1128,plain,
( ! [X0,X1] : join(X0,complement(join(X1,complement(X0)))) = join(complement(join(complement(X0),X1)),complement(complement(X0)))
| ~ spl13_11 ),
inference(superposition,[],[f221,f703]) ).
fof(f1143,plain,
( ! [X0,X1] : join(X0,complement(join(X1,complement(X0)))) = join(complement(complement(X0)),complement(join(complement(X0),X1)))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f1128,f1]) ).
fof(f1149,plain,
! [X0,X1] : join(X0,join(complement(X0),complement(X1))) = join(top,complement(join(complement(X0),X1))),
inference(forward_demodulation,[],[f1121,f1]) ).
fof(f1171,plain,
( ! [X0,X1] : join(X0,X1) = join(complement(top),join(X1,complement(join(complement(X0),complement(X0)))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f1095,f667]) ).
fof(f1182,plain,
( ! [X0,X1] : join(X0,complement(join(X1,complement(X0)))) = join(X0,complement(join(complement(X0),X1)))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f1143,f667]) ).
fof(f1184,plain,
! [X0,X1] : join(top,complement(join(complement(X0),X1))) = join(top,complement(X1)),
inference(forward_demodulation,[],[f1149,f244]) ).
fof(f1196,plain,
( ! [X0,X1] : join(X0,X1) = join(zero,join(X1,complement(join(complement(X0),complement(X0)))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f1171,f256]) ).
fof(f1275,plain,
( ! [X0] : complement(complement(join(X0,X0))) = join(complement(complement(X0)),complement(join(complement(join(X0,X0)),complement(zero))))
| ~ spl13_11 ),
inference(superposition,[],[f703,f670]) ).
fof(f1278,plain,
( ! [X0,X1] : join(complement(X0),X1) = join(zero,join(complement(join(X0,X0)),X1))
| ~ spl13_11 ),
inference(superposition,[],[f2,f670]) ).
fof(f1282,plain,
( ! [X0] : complement(complement(join(X0,X0))) = join(X0,complement(join(complement(join(X0,X0)),complement(zero))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f1275,f667]) ).
fof(f1287,plain,
( ! [X0] : join(X0,X0) = join(X0,complement(join(complement(join(X0,X0)),complement(zero))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f1282,f667]) ).
fof(f1332,plain,
( ! [X0,X1] : join(top,complement(join(complement(X1),X0))) = join(join(X0,X1),complement(X0))
| ~ spl13_11 ),
inference(superposition,[],[f244,f688]) ).
fof(f1334,plain,
( ! [X0,X1] : join(top,complement(join(X0,complement(X1)))) = join(join(X1,X0),complement(X0))
| ~ spl13_11 ),
inference(superposition,[],[f244,f703]) ).
fof(f1337,plain,
! [X0,X1] : join(top,X0) = join(X1,join(X0,complement(X1))),
inference(superposition,[],[f244,f1]) ).
fof(f1345,plain,
( ! [X0,X1] : complement(join(complement(X1),X0)) = join(complement(join(top,X0)),complement(join(join(complement(X1),X0),complement(X1))))
| ~ spl13_11 ),
inference(superposition,[],[f703,f244]) ).
fof(f1357,plain,
( ! [X0,X1] : complement(join(complement(X1),X0)) = join(complement(join(top,X0)),complement(join(complement(X1),join(X0,complement(X1)))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f1345,f2]) ).
fof(f1363,plain,
( ! [X0,X1] : join(X1,join(X0,complement(X0))) = join(top,complement(join(X0,complement(X1))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f1334,f2]) ).
fof(f1365,plain,
( ! [X0,X1] : join(top,complement(join(complement(X1),X0))) = join(X0,join(X1,complement(X0)))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f1332,f2]) ).
fof(f1373,plain,
( ! [X0,X1] : join(X1,top) = join(top,complement(join(X0,complement(X1))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f1363,f15]) ).
fof(f1375,plain,
( ! [X0,X1] : join(top,X1) = join(top,complement(join(complement(X1),X0)))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f1365,f1337]) ).
fof(f1379,plain,
( ! [X0,X1] : join(top,X1) = join(top,complement(X0))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f1375,f1184]) ).
fof(f1384,plain,
( ! [X0] : zero = join(composition(converse(X0),complement(composition(X0,top))),zero)
| ~ spl13_11 ),
inference(superposition,[],[f14,f256]) ).
fof(f1388,plain,
( top = complement(zero)
| ~ spl13_11 ),
inference(superposition,[],[f667,f256]) ).
fof(f1393,plain,
( ! [X0] : join(X0,X0) = join(X0,complement(join(complement(join(X0,X0)),top)))
| ~ spl13_11 ),
inference(backward_demodulation,[],[f1287,f1388]) ).
fof(f1395,plain,
( ! [X0] : zero = join(zero,composition(converse(X0),complement(composition(X0,top))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f1384,f1]) ).
fof(f1398,plain,
( ! [X0] : join(X0,X0) = join(X0,complement(join(top,complement(join(X0,X0)))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f1393,f1]) ).
fof(f1405,plain,
! [X0] : complement(X0) = join(complement(X0),composition(sF0,complement(X0))),
inference(superposition,[],[f126,f1072]) ).
fof(f1408,plain,
! [X0,X1] : composition(join(X1,converse(sF0)),X0) = join(composition(X1,X0),X0),
inference(superposition,[],[f9,f1072]) ).
fof(f1409,plain,
! [X0,X1] : join(X0,composition(X1,X0)) = composition(join(converse(sF0),X1),X0),
inference(superposition,[],[f9,f1072]) ).
fof(f1420,plain,
sF0 = converse(sF0),
inference(superposition,[],[f68,f1072]) ).
fof(f1425,plain,
! [X0] : composition(sF0,X0) = X0,
inference(backward_demodulation,[],[f1072,f1420]) ).
fof(f1437,plain,
! [X0,X1] : join(X0,composition(X1,X0)) = composition(join(sF0,X1),X0),
inference(forward_demodulation,[],[f1409,f1420]) ).
fof(f1438,plain,
! [X0,X1] : join(X0,composition(X1,X0)) = composition(join(X1,converse(sF0)),X0),
inference(forward_demodulation,[],[f1408,f1]) ).
fof(f1441,plain,
! [X0] : complement(X0) = join(complement(X0),complement(X0)),
inference(backward_demodulation,[],[f1405,f1425]) ).
fof(f1451,plain,
! [X0,X1] : join(X0,composition(X1,X0)) = composition(join(X1,sF0),X0),
inference(forward_demodulation,[],[f1438,f1420]) ).
fof(f1453,plain,
( ! [X0,X1] : join(X0,X1) = join(zero,join(X1,complement(complement(X0))))
| ~ spl13_11 ),
inference(backward_demodulation,[],[f1196,f1441]) ).
fof(f1458,plain,
( ! [X0,X1] : join(X0,X1) = join(zero,join(X1,X0))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f1453,f667]) ).
fof(f1461,plain,
( ! [X0,X1] : join(complement(X0),X1) = join(X1,complement(join(X0,X0)))
| ~ spl13_11 ),
inference(backward_demodulation,[],[f1278,f1458]) ).
fof(f1462,plain,
( ! [X0] : join(X0,X0) = join(X0,complement(join(complement(X0),top)))
| ~ spl13_11 ),
inference(backward_demodulation,[],[f1398,f1461]) ).
fof(f1463,plain,
( ! [X0] : complement(X0) = join(complement(X0),zero)
| ~ spl13_11 ),
inference(backward_demodulation,[],[f670,f1461]) ).
fof(f1465,plain,
( ! [X0] : complement(X0) = join(zero,complement(X0))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f1463,f1]) ).
fof(f1466,plain,
( ! [X0] : join(X0,X0) = join(X0,complement(join(top,complement(X0))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f1462,f1182]) ).
fof(f1477,plain,
( composition(join(sF0,sF11),sk3) = join(sk3,sF12)
| ~ spl13_4 ),
inference(superposition,[],[f1437,f130]) ).
fof(f1478,plain,
( composition(join(sF0,sk1),sk3) = join(sk3,sF2)
| ~ spl13_14 ),
inference(superposition,[],[f1437,f273]) ).
fof(f1487,plain,
( ! [X0] : composition(sF0,X0) = join(X0,composition(sk1,X0))
| ~ spl13_16 ),
inference(superposition,[],[f1437,f484]) ).
fof(f1488,plain,
( ! [X0] : composition(sF0,X0) = join(X0,composition(sk2,X0))
| ~ spl13_17 ),
inference(superposition,[],[f1437,f575]) ).
fof(f1539,plain,
( ! [X0] : join(X0,composition(sk2,X0)) = X0
| ~ spl13_17 ),
inference(forward_demodulation,[],[f1488,f1425]) ).
fof(f1540,plain,
( ! [X0] : join(X0,composition(sk1,X0)) = X0
| ~ spl13_16 ),
inference(forward_demodulation,[],[f1487,f1425]) ).
fof(f1545,plain,
( composition(join(sF0,sk1),sk3) = join(sF2,sk3)
| ~ spl13_14 ),
inference(forward_demodulation,[],[f1478,f1]) ).
fof(f1546,plain,
( composition(join(sF0,sF11),sk3) = join(sF12,sk3)
| ~ spl13_4 ),
inference(forward_demodulation,[],[f1477,f1]) ).
fof(f1562,plain,
( join(sF2,sk3) = composition(sF0,sk3)
| ~ spl13_14
| ~ spl13_16 ),
inference(forward_demodulation,[],[f1545,f484]) ).
fof(f1563,plain,
( join(sF12,sk3) = composition(join(sF11,sF0),sk3)
| ~ spl13_4 ),
inference(forward_demodulation,[],[f1546,f82]) ).
fof(f1573,plain,
( sk3 = join(sF2,sk3)
| ~ spl13_14
| ~ spl13_16 ),
inference(forward_demodulation,[],[f1562,f1425]) ).
fof(f1577,plain,
( ! [X0] : join(zero,X0) = X0
| ~ spl13_11 ),
inference(superposition,[],[f1465,f667]) ).
fof(f1591,plain,
( ! [X0] : complement(complement(X0)) = join(complement(complement(X0)),complement(join(complement(X0),complement(zero))))
| ~ spl13_11 ),
inference(superposition,[],[f703,f1465]) ).
fof(f1598,plain,
( ! [X0] : complement(complement(X0)) = join(complement(complement(X0)),complement(join(complement(X0),top)))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f1591,f1388]) ).
fof(f1604,plain,
( ! [X0] : zero = composition(converse(X0),complement(composition(X0,top)))
| ~ spl13_11 ),
inference(backward_demodulation,[],[f1395,f1577]) ).
fof(f1607,plain,
( ! [X0] : complement(complement(X0)) = join(complement(complement(X0)),complement(join(top,complement(X0))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f1598,f1]) ).
fof(f1612,plain,
( ! [X0] : join(X0,complement(join(top,complement(X0)))) = X0
| ~ spl13_11 ),
inference(forward_demodulation,[],[f1607,f667]) ).
fof(f1615,plain,
( ! [X0] : join(X0,X0) = X0
| ~ spl13_11 ),
inference(forward_demodulation,[],[f1612,f1466]) ).
fof(f1621,plain,
( ! [X0] : join(X0,complement(join(top,complement(X0)))) = X0
| ~ spl13_11 ),
inference(backward_demodulation,[],[f1466,f1615]) ).
fof(f1631,plain,
( ! [X0,X1] : join(X0,X1) = join(X0,join(X0,X1))
| ~ spl13_11 ),
inference(superposition,[],[f2,f1615]) ).
fof(f1637,plain,
( ! [X0] : join(X0,complement(X0)) = join(top,complement(X0))
| ~ spl13_11 ),
inference(superposition,[],[f244,f1615]) ).
fof(f1649,plain,
( ! [X0] : top = join(top,complement(X0))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f1637,f15]) ).
fof(f1664,plain,
( ! [X0] : join(X0,complement(top)) = X0
| ~ spl13_11 ),
inference(backward_demodulation,[],[f1621,f1649]) ).
fof(f1665,plain,
( ! [X1] : top = join(top,X1)
| ~ spl13_11 ),
inference(backward_demodulation,[],[f1379,f1649]) ).
fof(f1667,plain,
( ! [X1] : top = join(X1,top)
| ~ spl13_11 ),
inference(backward_demodulation,[],[f1373,f1649]) ).
fof(f1691,plain,
( ! [X0,X1] : complement(join(complement(X1),X0)) = join(complement(top),complement(join(complement(X1),join(X0,complement(X1)))))
| ~ spl13_11 ),
inference(backward_demodulation,[],[f1357,f1665]) ).
fof(f1700,plain,
( ! [X0] : join(X0,zero) = X0
| ~ spl13_11 ),
inference(forward_demodulation,[],[f1664,f256]) ).
fof(f1713,plain,
( ! [X0,X1] : complement(join(complement(X1),X0)) = join(zero,complement(join(complement(X1),join(X0,complement(X1)))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f1691,f256]) ).
fof(f1723,plain,
( ! [X0,X1] : complement(join(complement(X1),X0)) = complement(join(complement(X1),join(X0,complement(X1))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f1713,f1577]) ).
fof(f1874,plain,
( ! [X0] : complement(composition(sk1,X0)) = join(complement(X0),complement(join(composition(sk1,X0),complement(X0))))
| ~ spl13_11
| ~ spl13_16 ),
inference(superposition,[],[f703,f1540]) ).
fof(f1877,plain,
( ! [X0,X1] : join(X0,X1) = join(X0,join(composition(sk1,X0),X1))
| ~ spl13_16 ),
inference(superposition,[],[f2,f1540]) ).
fof(f1879,plain,
( ! [X0] : complement(composition(sk1,complement(X0))) = join(complement(join(composition(sk1,complement(X0)),X0)),complement(complement(X0)))
| ~ spl13_11
| ~ spl13_16 ),
inference(superposition,[],[f688,f1540]) ).
fof(f1888,plain,
( ! [X0] : complement(composition(sk1,complement(X0))) = join(complement(complement(X0)),complement(join(composition(sk1,complement(X0)),X0)))
| ~ spl13_11
| ~ spl13_16 ),
inference(forward_demodulation,[],[f1879,f1]) ).
fof(f1890,plain,
( ! [X0] : complement(composition(sk1,X0)) = join(complement(X0),complement(join(complement(X0),composition(sk1,X0))))
| ~ spl13_11
| ~ spl13_16 ),
inference(forward_demodulation,[],[f1874,f1]) ).
fof(f1901,plain,
( ! [X0] : complement(composition(sk1,complement(X0))) = join(complement(complement(X0)),complement(join(X0,composition(sk1,complement(X0)))))
| ~ spl13_11
| ~ spl13_16 ),
inference(forward_demodulation,[],[f1888,f1]) ).
fof(f1904,plain,
( ! [X0] : complement(composition(sk1,complement(X0))) = join(X0,complement(join(X0,composition(sk1,complement(X0)))))
| ~ spl13_11
| ~ spl13_16 ),
inference(forward_demodulation,[],[f1901,f667]) ).
fof(f1916,plain,
( ! [X0] : complement(composition(sk2,X0)) = join(complement(X0),complement(join(composition(sk2,X0),complement(X0))))
| ~ spl13_11
| ~ spl13_17 ),
inference(superposition,[],[f703,f1539]) ).
fof(f1919,plain,
( ! [X0,X1] : join(X0,X1) = join(X0,join(composition(sk2,X0),X1))
| ~ spl13_17 ),
inference(superposition,[],[f2,f1539]) ).
fof(f1921,plain,
( ! [X0] : complement(composition(sk2,complement(X0))) = join(complement(join(composition(sk2,complement(X0)),X0)),complement(complement(X0)))
| ~ spl13_11
| ~ spl13_17 ),
inference(superposition,[],[f688,f1539]) ).
fof(f1930,plain,
( ! [X0] : complement(composition(sk2,complement(X0))) = join(complement(complement(X0)),complement(join(composition(sk2,complement(X0)),X0)))
| ~ spl13_11
| ~ spl13_17 ),
inference(forward_demodulation,[],[f1921,f1]) ).
fof(f1932,plain,
( ! [X0] : complement(composition(sk2,X0)) = join(complement(X0),complement(join(complement(X0),composition(sk2,X0))))
| ~ spl13_11
| ~ spl13_17 ),
inference(forward_demodulation,[],[f1916,f1]) ).
fof(f1943,plain,
( ! [X0] : complement(composition(sk2,complement(X0))) = join(complement(complement(X0)),complement(join(X0,composition(sk2,complement(X0)))))
| ~ spl13_11
| ~ spl13_17 ),
inference(forward_demodulation,[],[f1930,f1]) ).
fof(f1946,plain,
( ! [X0] : complement(composition(sk2,complement(X0))) = join(X0,complement(join(X0,composition(sk2,complement(X0)))))
| ~ spl13_11
| ~ spl13_17 ),
inference(forward_demodulation,[],[f1943,f667]) ).
fof(f1949,plain,
( ! [X0,X1] : join(X1,composition(X0,X1)) = join(X1,composition(join(sk2,X0),X1))
| ~ spl13_17 ),
inference(superposition,[],[f1919,f9]) ).
fof(f1950,plain,
( ! [X0,X1] : join(X0,composition(sk2,X1)) = join(X0,composition(sk2,join(X0,X1)))
| ~ spl13_17 ),
inference(superposition,[],[f1919,f346]) ).
fof(f2011,plain,
( ! [X0,X1] : join(X0,composition(sk1,X1)) = join(X0,composition(sk1,join(X0,X1)))
| ~ spl13_16 ),
inference(superposition,[],[f1877,f346]) ).
fof(f2075,plain,
( ! [X0,X1] : join(X0,X1) = join(X1,join(X0,X1))
| ~ spl13_11 ),
inference(superposition,[],[f1631,f1]) ).
fof(f2091,plain,
( ! [X0,X1] : complement(X0) = join(complement(join(X0,X1)),complement(X0))
| ~ spl13_11 ),
inference(superposition,[],[f1631,f694]) ).
fof(f2092,plain,
( ! [X0,X1] : complement(X0) = join(complement(join(X1,X0)),complement(X0))
| ~ spl13_11 ),
inference(superposition,[],[f1631,f703]) ).
fof(f2128,plain,
( ! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X1,X0)))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f2092,f1]) ).
fof(f2129,plain,
( ! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X0,X1)))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f2091,f1]) ).
fof(f2134,plain,
( ! [X0,X1] : complement(join(complement(X1),X0)) = complement(join(X0,complement(X1)))
| ~ spl13_11 ),
inference(backward_demodulation,[],[f1723,f2075]) ).
fof(f2142,plain,
( ! [X0,X1] : join(X0,X1) = join(X0,complement(join(X0,complement(X1))))
| ~ spl13_11 ),
inference(backward_demodulation,[],[f882,f2128]) ).
fof(f2146,plain,
( ! [X0,X1] : join(X0,complement(X1)) = join(X0,complement(join(X1,join(X0,X1))))
| ~ spl13_11 ),
inference(backward_demodulation,[],[f1038,f2142]) ).
fof(f2152,plain,
( ! [X0,X1] : join(X0,complement(X1)) = join(X0,complement(join(X0,X1)))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f2146,f2075]) ).
fof(f2167,plain,
( ! [X0] : complement(composition(sk1,complement(X0))) = join(X0,complement(composition(sk1,complement(X0))))
| ~ spl13_11
| ~ spl13_16 ),
inference(backward_demodulation,[],[f1904,f2152]) ).
fof(f2168,plain,
( ! [X0] : complement(composition(sk2,complement(X0))) = join(X0,complement(composition(sk2,complement(X0))))
| ~ spl13_11
| ~ spl13_17 ),
inference(backward_demodulation,[],[f1946,f2152]) ).
fof(f2171,plain,
( ! [X0] : complement(composition(sk1,X0)) = join(complement(X0),complement(composition(sk1,X0)))
| ~ spl13_11
| ~ spl13_16 ),
inference(backward_demodulation,[],[f1890,f2152]) ).
fof(f2172,plain,
( ! [X0] : complement(composition(sk2,X0)) = join(complement(X0),complement(composition(sk2,X0)))
| ~ spl13_11
| ~ spl13_17 ),
inference(backward_demodulation,[],[f1932,f2152]) ).
fof(f2178,plain,
( ! [X0,X1] : join(X0,complement(join(complement(X0),X1))) = X0
| ~ spl13_11 ),
inference(superposition,[],[f2129,f667]) ).
fof(f2220,plain,
( complement(sF8) = join(complement(sF8),complement(sF10))
| ~ spl13_11
| ~ spl13_12 ),
inference(superposition,[],[f2129,f261]) ).
fof(f2237,plain,
( complement(sF8) = join(complement(sF8),sF11)
| ~ spl13_9
| ~ spl13_11
| ~ spl13_12 ),
inference(forward_demodulation,[],[f2220,f183]) ).
fof(f2251,plain,
( complement(sF8) = join(sF11,complement(sF8))
| ~ spl13_9
| ~ spl13_11
| ~ spl13_12 ),
inference(forward_demodulation,[],[f2237,f1]) ).
fof(f2261,plain,
( sk1 = join(sF11,sk1)
| ~ spl13_9
| ~ spl13_11
| ~ spl13_12
| ~ spl13_18 ),
inference(forward_demodulation,[],[f2251,f1046]) ).
fof(f2370,plain,
( ! [X0,X1] : join(X1,complement(X0)) = join(X1,complement(join(X0,X1)))
| ~ spl13_11 ),
inference(superposition,[],[f2152,f1]) ).
fof(f2465,plain,
( sF8 = join(complement(sF0),complement(sk1))
| ~ spl13_7
| ~ spl13_11
| ~ spl13_16 ),
inference(backward_demodulation,[],[f978,f2370]) ).
fof(f2493,plain,
( sF8 = join(complement(sF0),sF8)
| ~ spl13_7
| ~ spl13_11
| ~ spl13_16 ),
inference(forward_demodulation,[],[f2465,f151]) ).
fof(f2516,plain,
( sF8 = join(sF8,complement(sF0))
| ~ spl13_7
| ~ spl13_11
| ~ spl13_16 ),
inference(forward_demodulation,[],[f2493,f1]) ).
fof(f2670,plain,
( join(sF9,complement(sF8)) = join(sF9,complement(sF10))
| ~ spl13_11
| ~ spl13_12 ),
inference(superposition,[],[f2370,f261]) ).
fof(f2718,plain,
( join(sF9,complement(sF8)) = join(sF9,sF11)
| ~ spl13_9
| ~ spl13_11
| ~ spl13_12 ),
inference(forward_demodulation,[],[f2670,f183]) ).
fof(f2748,plain,
( join(sF9,sk1) = join(sF9,sF11)
| ~ spl13_9
| ~ spl13_11
| ~ spl13_12
| ~ spl13_18 ),
inference(forward_demodulation,[],[f2718,f1046]) ).
fof(f2769,plain,
( sk2 = join(sF11,complement(join(sF9,sF11)))
| ~ spl13_5
| ~ spl13_7
| ~ spl13_9
| ~ spl13_11
| ~ spl13_12
| ~ spl13_18 ),
inference(backward_demodulation,[],[f1015,f2748]) ).
fof(f2782,plain,
( sk2 = join(sF11,complement(sF9))
| ~ spl13_5
| ~ spl13_7
| ~ spl13_9
| ~ spl13_11
| ~ spl13_12
| ~ spl13_18 ),
inference(forward_demodulation,[],[f2769,f2370]) ).
fof(f2790,plain,
( sk2 = join(sF11,sk2)
| ~ spl13_5
| ~ spl13_7
| ~ spl13_9
| ~ spl13_11
| ~ spl13_12
| ~ spl13_18
| ~ spl13_19 ),
inference(forward_demodulation,[],[f2782,f1051]) ).
fof(f2827,plain,
( ! [X0] : composition(top,X0) = join(X0,composition(top,X0))
| ~ spl13_11 ),
inference(superposition,[],[f1437,f1667]) ).
fof(f2845,definition,
( spl13_20
<=> sk3 = join(sF2,sk3) ),
introduced(definition,[new_symbols(definition,[spl13_20])],[avatar_definition]) ).
fof(f2847,plain,
( sk3 = join(sF2,sk3)
| ~ spl13_20 ),
inference(avatar_component_clause,[],[f2845]) ).
fof(f2848,plain,
( spl13_20
| ~ spl13_14
| ~ spl13_16 ),
inference(avatar_split_clause,[],[f1573,f482,f271,f2845]) ).
fof(f2854,plain,
( complement(sF2) = join(complement(sF2),complement(sk3))
| ~ spl13_11
| ~ spl13_20 ),
inference(superposition,[],[f2129,f2847]) ).
fof(f2857,plain,
( sF3 = join(sF3,complement(sk3))
| ~ spl13_8
| ~ spl13_11
| ~ spl13_20 ),
inference(forward_demodulation,[],[f2854,f168]) ).
fof(f2926,plain,
( composition(join(sF11,sk1),sk3) = join(sF12,sF2)
| ~ spl13_4
| ~ spl13_14 ),
inference(superposition,[],[f134,f273]) ).
fof(f2927,plain,
( composition(join(sF11,sk2),sk3) = join(sF12,sF4)
| ~ spl13_4
| ~ spl13_15 ),
inference(superposition,[],[f134,f285]) ).
fof(f2947,plain,
( composition(join(sF11,sk2),sk3) = join(sF4,sF12)
| ~ spl13_4
| ~ spl13_15 ),
inference(forward_demodulation,[],[f2927,f1]) ).
fof(f2948,plain,
( composition(join(sF11,sk1),sk3) = join(sF2,sF12)
| ~ spl13_4
| ~ spl13_14 ),
inference(forward_demodulation,[],[f2926,f1]) ).
fof(f2950,plain,
( composition(sk2,sk3) = join(sF4,sF12)
| ~ spl13_4
| ~ spl13_5
| ~ spl13_7
| ~ spl13_9
| ~ spl13_11
| ~ spl13_12
| ~ spl13_15
| ~ spl13_18
| ~ spl13_19 ),
inference(forward_demodulation,[],[f2947,f2790]) ).
fof(f2951,plain,
( composition(sk1,sk3) = join(sF2,sF12)
| ~ spl13_4
| ~ spl13_9
| ~ spl13_11
| ~ spl13_12
| ~ spl13_14
| ~ spl13_18 ),
inference(forward_demodulation,[],[f2948,f2261]) ).
fof(f2953,plain,
( sF4 = join(sF4,sF12)
| ~ spl13_4
| ~ spl13_5
| ~ spl13_7
| ~ spl13_9
| ~ spl13_11
| ~ spl13_12
| ~ spl13_15
| ~ spl13_18
| ~ spl13_19 ),
inference(forward_demodulation,[],[f2950,f285]) ).
fof(f2954,plain,
( sF2 = join(sF2,sF12)
| ~ spl13_4
| ~ spl13_9
| ~ spl13_11
| ~ spl13_12
| ~ spl13_14
| ~ spl13_18 ),
inference(forward_demodulation,[],[f2951,f273]) ).
fof(f3003,plain,
! [X0] : join(X0,converse(complement(converse(X0)))) = converse(top),
inference(superposition,[],[f226,f15]) ).
fof(f3010,plain,
( ! [X0] : converse(converse(X0)) = join(X0,converse(composition(converse(X0),sk1)))
| ~ spl13_16 ),
inference(superposition,[],[f226,f539]) ).
fof(f3011,plain,
( ! [X0] : converse(converse(X0)) = join(X0,converse(composition(converse(X0),sk2)))
| ~ spl13_17 ),
inference(superposition,[],[f226,f579]) ).
fof(f3016,plain,
( ! [X0] : converse(converse(X0)) = join(X0,converse(zero))
| ~ spl13_11 ),
inference(superposition,[],[f226,f1700]) ).
fof(f3021,plain,
! [X2,X0,X1] : composition(join(X0,converse(X1)),converse(X2)) = converse(composition(X2,join(converse(X0),X1))),
inference(superposition,[],[f12,f226]) ).
fof(f3028,plain,
! [X2,X0,X1] : join(composition(X2,converse(X0)),converse(composition(X0,X1))) = converse(composition(X0,join(converse(X2),X1))),
inference(backward_demodulation,[],[f297,f3021]) ).
fof(f3030,plain,
( ! [X0] : join(X0,converse(zero)) = X0
| ~ spl13_11 ),
inference(forward_demodulation,[],[f3016,f10]) ).
fof(f3034,plain,
( ! [X0] : converse(converse(X0)) = join(X0,composition(converse(sk2),X0))
| ~ spl13_17 ),
inference(forward_demodulation,[],[f3011,f295]) ).
fof(f3035,plain,
( ! [X0] : converse(converse(X0)) = join(X0,composition(converse(sk1),X0))
| ~ spl13_16 ),
inference(forward_demodulation,[],[f3010,f295]) ).
fof(f3056,plain,
( ! [X0] : join(X0,composition(converse(sk2),X0)) = X0
| ~ spl13_17 ),
inference(forward_demodulation,[],[f3034,f10]) ).
fof(f3057,plain,
( ! [X0] : join(X0,composition(converse(sk1),X0)) = X0
| ~ spl13_16 ),
inference(forward_demodulation,[],[f3035,f10]) ).
fof(f3312,plain,
! [X2,X3,X0,X1] : join(composition(X1,X2),join(X3,composition(X0,X2))) = join(X3,composition(join(X0,X1),X2)),
inference(superposition,[],[f219,f9]) ).
fof(f3404,plain,
( ! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X1,join(X0,join(X1,X2)))
| ~ spl13_11 ),
inference(superposition,[],[f1631,f219]) ).
fof(f3431,plain,
! [X2,X3,X0,X1] : join(X0,join(X1,join(X2,X3))) = join(X2,join(X3,join(X0,X1))),
inference(superposition,[],[f2,f219]) ).
fof(f4083,plain,
! [X0,X1] : composition(complement(join(complement(X0),complement(composition(X1,converse(sF0))))),complement(join(complement(sF0),complement(composition(converse(X0),X1))))) = join(complement(join(complement(X0),complement(X1))),composition(complement(join(complement(X0),complement(composition(X1,converse(sF0))))),complement(join(complement(sF0),complement(composition(converse(X0),X1)))))),
inference(superposition,[],[f29,f68]) ).
fof(f4191,plain,
! [X0,X1] : composition(complement(join(complement(X0),complement(composition(X1,sF0)))),complement(join(complement(sF0),complement(composition(converse(X0),X1))))) = join(complement(join(complement(X0),complement(X1))),composition(complement(join(complement(X0),complement(composition(X1,sF0)))),complement(join(complement(sF0),complement(composition(converse(X0),X1)))))),
inference(forward_demodulation,[],[f4083,f1420]) ).
fof(f4212,plain,
! [X0,X1] : composition(complement(join(complement(X0),complement(X1))),complement(join(complement(sF0),complement(composition(converse(X0),X1))))) = join(complement(join(complement(X0),complement(X1))),composition(complement(join(complement(X0),complement(X1))),complement(join(complement(sF0),complement(composition(converse(X0),X1)))))),
inference(forward_demodulation,[],[f4191,f68]) ).
fof(f4228,plain,
! [X0,X1] : composition(complement(join(complement(X0),complement(X1))),complement(join(complement(sF0),complement(composition(converse(X0),X1))))) = composition(complement(join(complement(X0),complement(X1))),join(sF0,complement(join(complement(sF0),complement(composition(converse(X0),X1)))))),
inference(forward_demodulation,[],[f4212,f394]) ).
fof(f4237,plain,
( ! [X0,X1] : composition(complement(join(complement(X0),complement(X1))),complement(join(complement(sF0),complement(composition(converse(X0),X1))))) = composition(complement(join(complement(X0),complement(X1))),sF0)
| ~ spl13_11 ),
inference(forward_demodulation,[],[f4228,f2178]) ).
fof(f4240,plain,
( ! [X0,X1] : complement(join(complement(X0),complement(X1))) = composition(complement(join(complement(X0),complement(X1))),complement(join(complement(sF0),complement(composition(converse(X0),X1)))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f4237,f68]) ).
fof(f4249,plain,
( ! [X0] : complement(join(complement(composition(sk1,complement(join(complement(sk3),complement(composition(converse(sk1),X0)))))),complement(X0))) = join(complement(join(complement(sF2),complement(X0))),complement(join(complement(composition(sk1,complement(join(complement(sk3),complement(composition(converse(sk1),X0)))))),complement(X0))))
| ~ spl13_14 ),
inference(superposition,[],[f30,f273]) ).
fof(f4250,plain,
( ! [X0] : complement(join(complement(composition(sk2,complement(join(complement(sk3),complement(composition(converse(sk2),X0)))))),complement(X0))) = join(complement(join(complement(sF4),complement(X0))),complement(join(complement(composition(sk2,complement(join(complement(sk3),complement(composition(converse(sk2),X0)))))),complement(X0))))
| ~ spl13_15 ),
inference(superposition,[],[f30,f285]) ).
fof(f4284,plain,
( ! [X0,X1] : complement(join(complement(composition(X0,complement(join(complement(X1),complement(composition(converse(X0),top)))))),zero)) = join(complement(join(complement(composition(X0,X1)),zero)),complement(join(complement(composition(X0,complement(join(complement(X1),complement(composition(converse(X0),top)))))),zero)))
| ~ spl13_11 ),
inference(superposition,[],[f30,f256]) ).
fof(f4336,plain,
( ! [X0,X1] : complement(join(zero,complement(composition(X0,complement(join(complement(X1),complement(composition(converse(X0),top)))))))) = join(complement(join(complement(composition(X0,X1)),zero)),complement(join(zero,complement(composition(X0,complement(join(complement(X1),complement(composition(converse(X0),top)))))))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f4284,f2134]) ).
fof(f4370,plain,
( ! [X0] : complement(join(complement(X0),complement(composition(sk2,complement(join(complement(sk3),complement(composition(converse(sk2),X0)))))))) = join(complement(join(complement(sF4),complement(X0))),complement(join(complement(X0),complement(composition(sk2,complement(join(complement(sk3),complement(composition(converse(sk2),X0)))))))))
| ~ spl13_11
| ~ spl13_15 ),
inference(forward_demodulation,[],[f4250,f2134]) ).
fof(f4371,plain,
( ! [X0] : complement(join(complement(X0),complement(composition(sk1,complement(join(complement(sk3),complement(composition(converse(sk1),X0)))))))) = join(complement(join(complement(sF2),complement(X0))),complement(join(complement(X0),complement(composition(sk1,complement(join(complement(sk3),complement(composition(converse(sk1),X0)))))))))
| ~ spl13_11
| ~ spl13_14 ),
inference(forward_demodulation,[],[f4249,f2134]) ).
fof(f4399,plain,
( ! [X0,X1] : complement(complement(composition(X0,complement(join(complement(X1),complement(composition(converse(X0),top))))))) = join(complement(join(complement(composition(X0,X1)),zero)),complement(complement(composition(X0,complement(join(complement(X1),complement(composition(converse(X0),top))))))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f4336,f1577]) ).
fof(f4412,plain,
( ! [X0] : complement(join(complement(X0),complement(composition(sk2,complement(join(complement(sk3),complement(composition(converse(sk2),X0)))))))) = join(complement(join(sF5,complement(X0))),complement(join(complement(X0),complement(composition(sk2,complement(join(complement(sk3),complement(composition(converse(sk2),X0)))))))))
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15 ),
inference(forward_demodulation,[],[f4370,f198]) ).
fof(f4413,plain,
( ! [X0] : complement(join(complement(X0),complement(composition(sk1,complement(join(complement(sk3),complement(composition(converse(sk1),X0)))))))) = join(complement(join(sF3,complement(X0))),complement(join(complement(X0),complement(composition(sk1,complement(join(complement(sk3),complement(composition(converse(sk1),X0)))))))))
| ~ spl13_8
| ~ spl13_11
| ~ spl13_14 ),
inference(forward_demodulation,[],[f4371,f168]) ).
fof(f4427,plain,
( ! [X0,X1] : composition(X0,complement(join(complement(X1),complement(composition(converse(X0),top))))) = join(complement(join(complement(composition(X0,X1)),zero)),composition(X0,complement(join(complement(X1),complement(composition(converse(X0),top))))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f4399,f667]) ).
fof(f4447,plain,
( ! [X0,X1] : composition(X0,complement(join(complement(X1),complement(composition(converse(X0),top))))) = join(complement(join(zero,complement(composition(X0,X1)))),composition(X0,complement(join(complement(X1),complement(composition(converse(X0),top))))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f4427,f2134]) ).
fof(f4463,plain,
( ! [X0,X1] : composition(X0,complement(join(complement(X1),complement(composition(converse(X0),top))))) = join(complement(complement(composition(X0,X1))),composition(X0,complement(join(complement(X1),complement(composition(converse(X0),top))))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f4447,f1577]) ).
fof(f4474,plain,
( ! [X0,X1] : composition(X0,complement(join(complement(X1),complement(composition(converse(X0),top))))) = join(composition(X0,X1),composition(X0,complement(join(complement(X1),complement(composition(converse(X0),top))))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f4463,f667]) ).
fof(f4485,plain,
( ! [X0,X1] : composition(X0,complement(join(complement(X1),complement(composition(converse(X0),top))))) = composition(X0,join(X1,complement(join(complement(X1),complement(composition(converse(X0),top))))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f4474,f346]) ).
fof(f4491,plain,
( ! [X0,X1] : composition(X0,X1) = composition(X0,complement(join(complement(X1),complement(composition(converse(X0),top)))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f4485,f2178]) ).
fof(f4504,plain,
( ! [X0] : composition(X0,top) = composition(X0,complement(join(zero,complement(composition(converse(X0),top)))))
| ~ spl13_11 ),
inference(superposition,[],[f4491,f256]) ).
fof(f4513,plain,
( ! [X0,X1] : composition(converse(X0),X1) = composition(converse(X0),complement(join(complement(X1),complement(composition(X0,top)))))
| ~ spl13_11 ),
inference(superposition,[],[f4491,f10]) ).
fof(f4539,plain,
( ! [X0] : complement(join(complement(X0),complement(composition(converse(converse(sk1)),top)))) = join(complement(join(complement(X0),complement(composition(converse(converse(sk1)),top)))),composition(converse(sk1),X0))
| ~ spl13_11
| ~ spl13_16 ),
inference(superposition,[],[f3057,f4491]) ).
fof(f4540,plain,
( ! [X0] : complement(join(complement(X0),complement(composition(converse(converse(sk2)),top)))) = join(complement(join(complement(X0),complement(composition(converse(converse(sk2)),top)))),composition(converse(sk2),X0))
| ~ spl13_11
| ~ spl13_17 ),
inference(superposition,[],[f3056,f4491]) ).
fof(f4541,plain,
( ! [X0] : complement(composition(sk1,X0)) = join(join(complement(X0),complement(composition(converse(sk1),top))),complement(composition(sk1,X0)))
| ~ spl13_11
| ~ spl13_16 ),
inference(superposition,[],[f2167,f4491]) ).
fof(f4545,plain,
( ! [X0] : complement(composition(sk2,X0)) = join(join(complement(X0),complement(composition(converse(sk2),top))),complement(composition(sk2,X0)))
| ~ spl13_11
| ~ spl13_17 ),
inference(superposition,[],[f2168,f4491]) ).
fof(f4554,plain,
( ! [X0] : complement(composition(sk2,X0)) = join(complement(X0),join(complement(composition(converse(sk2),top)),complement(composition(sk2,X0))))
| ~ spl13_11
| ~ spl13_17 ),
inference(forward_demodulation,[],[f4545,f2]) ).
fof(f4558,plain,
( ! [X0] : complement(composition(sk1,X0)) = join(complement(X0),join(complement(composition(converse(sk1),top)),complement(composition(sk1,X0))))
| ~ spl13_11
| ~ spl13_16 ),
inference(forward_demodulation,[],[f4541,f2]) ).
fof(f4559,plain,
( ! [X0] : complement(join(complement(X0),complement(composition(converse(converse(sk2)),top)))) = join(composition(converse(sk2),X0),complement(join(complement(X0),complement(composition(converse(converse(sk2)),top)))))
| ~ spl13_11
| ~ spl13_17 ),
inference(forward_demodulation,[],[f4540,f1]) ).
fof(f4560,plain,
( ! [X0] : complement(join(complement(X0),complement(composition(converse(converse(sk1)),top)))) = join(composition(converse(sk1),X0),complement(join(complement(X0),complement(composition(converse(converse(sk1)),top)))))
| ~ spl13_11
| ~ spl13_16 ),
inference(forward_demodulation,[],[f4539,f1]) ).
fof(f4580,plain,
( ! [X0] : composition(X0,top) = composition(X0,complement(complement(composition(converse(X0),top))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f4504,f1577]) ).
fof(f4591,plain,
( ! [X0] : complement(join(complement(X0),complement(composition(sk2,top)))) = join(composition(converse(sk2),X0),complement(join(complement(X0),complement(composition(sk2,top)))))
| ~ spl13_11
| ~ spl13_17 ),
inference(forward_demodulation,[],[f4559,f10]) ).
fof(f4592,plain,
( ! [X0] : complement(join(complement(X0),complement(composition(sk1,top)))) = join(composition(converse(sk1),X0),complement(join(complement(X0),complement(composition(sk1,top)))))
| ~ spl13_11
| ~ spl13_16 ),
inference(forward_demodulation,[],[f4560,f10]) ).
fof(f4605,plain,
( ! [X0] : composition(X0,top) = composition(X0,composition(converse(X0),top))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f4580,f667]) ).
fof(f4643,plain,
( composition(converse(converse(sk1)),top) = join(composition(converse(converse(sk1)),top),composition(converse(sk1),top))
| ~ spl13_11
| ~ spl13_16 ),
inference(superposition,[],[f3057,f4605]) ).
fof(f4644,plain,
( composition(converse(converse(sk2)),top) = join(composition(converse(converse(sk2)),top),composition(converse(sk2),top))
| ~ spl13_11
| ~ spl13_17 ),
inference(superposition,[],[f3056,f4605]) ).
fof(f4647,plain,
( composition(converse(sk1),top) = join(composition(converse(sk1),top),composition(sk1,top))
| ~ spl13_11
| ~ spl13_16 ),
inference(superposition,[],[f1540,f4605]) ).
fof(f4650,plain,
( composition(converse(sk2),top) = join(composition(converse(sk2),top),composition(sk2,top))
| ~ spl13_11
| ~ spl13_17 ),
inference(superposition,[],[f1539,f4605]) ).
fof(f4653,plain,
( composition(converse(sk2),top) = composition(join(converse(sk2),sk2),top)
| ~ spl13_11
| ~ spl13_17 ),
inference(forward_demodulation,[],[f4650,f9]) ).
fof(f4656,plain,
( composition(converse(sk1),top) = composition(join(converse(sk1),sk1),top)
| ~ spl13_11
| ~ spl13_16 ),
inference(forward_demodulation,[],[f4647,f9]) ).
fof(f4659,plain,
( composition(converse(converse(sk2)),top) = composition(join(converse(converse(sk2)),converse(sk2)),top)
| ~ spl13_11
| ~ spl13_17 ),
inference(forward_demodulation,[],[f4644,f9]) ).
fof(f4660,plain,
( composition(converse(converse(sk1)),top) = composition(join(converse(converse(sk1)),converse(sk1)),top)
| ~ spl13_11
| ~ spl13_16 ),
inference(forward_demodulation,[],[f4643,f9]) ).
fof(f4682,plain,
( composition(converse(sk2),top) = composition(join(sk2,converse(sk2)),top)
| ~ spl13_11
| ~ spl13_17 ),
inference(forward_demodulation,[],[f4653,f82]) ).
fof(f4685,plain,
( composition(converse(sk1),top) = composition(join(sk1,converse(sk1)),top)
| ~ spl13_11
| ~ spl13_16 ),
inference(forward_demodulation,[],[f4656,f82]) ).
fof(f4688,plain,
( composition(converse(converse(sk2)),top) = composition(join(converse(sk2),converse(converse(sk2))),top)
| ~ spl13_11
| ~ spl13_17 ),
inference(forward_demodulation,[],[f4659,f82]) ).
fof(f4689,plain,
( composition(converse(converse(sk1)),top) = composition(join(converse(sk1),converse(converse(sk1))),top)
| ~ spl13_11
| ~ spl13_16 ),
inference(forward_demodulation,[],[f4660,f82]) ).
fof(f4706,plain,
( composition(converse(converse(sk2)),top) = composition(converse(join(sk2,converse(sk2))),top)
| ~ spl13_11
| ~ spl13_17 ),
inference(forward_demodulation,[],[f4688,f11]) ).
fof(f4707,plain,
( composition(converse(converse(sk1)),top) = composition(converse(join(sk1,converse(sk1))),top)
| ~ spl13_11
| ~ spl13_16 ),
inference(forward_demodulation,[],[f4689,f11]) ).
fof(f4713,plain,
( composition(converse(converse(sk2)),top) = composition(join(converse(sk2),sk2),top)
| ~ spl13_11
| ~ spl13_17 ),
inference(forward_demodulation,[],[f4706,f227]) ).
fof(f4714,plain,
( composition(converse(converse(sk1)),top) = composition(join(converse(sk1),sk1),top)
| ~ spl13_11
| ~ spl13_16 ),
inference(forward_demodulation,[],[f4707,f227]) ).
fof(f4718,plain,
( composition(converse(converse(sk2)),top) = composition(join(sk2,converse(sk2)),top)
| ~ spl13_11
| ~ spl13_17 ),
inference(forward_demodulation,[],[f4713,f82]) ).
fof(f4719,plain,
( composition(converse(converse(sk1)),top) = composition(join(sk1,converse(sk1)),top)
| ~ spl13_11
| ~ spl13_16 ),
inference(forward_demodulation,[],[f4714,f82]) ).
fof(f4721,plain,
( composition(converse(sk2),top) = composition(converse(converse(sk2)),top)
| ~ spl13_11
| ~ spl13_17 ),
inference(forward_demodulation,[],[f4718,f4682]) ).
fof(f4722,plain,
( composition(converse(sk1),top) = composition(converse(converse(sk1)),top)
| ~ spl13_11
| ~ spl13_16 ),
inference(forward_demodulation,[],[f4719,f4685]) ).
fof(f4724,plain,
( composition(sk2,top) = composition(converse(sk2),top)
| ~ spl13_11
| ~ spl13_17 ),
inference(forward_demodulation,[],[f4721,f10]) ).
fof(f4725,plain,
( composition(sk1,top) = composition(converse(sk1),top)
| ~ spl13_11
| ~ spl13_16 ),
inference(forward_demodulation,[],[f4722,f10]) ).
fof(f4727,plain,
( ! [X0] : complement(composition(sk2,X0)) = join(complement(X0),join(complement(composition(sk2,top)),complement(composition(sk2,X0))))
| ~ spl13_11
| ~ spl13_17 ),
inference(backward_demodulation,[],[f4554,f4724]) ).
fof(f4731,plain,
( ! [X0] : complement(composition(sk1,X0)) = join(complement(X0),join(complement(composition(sk1,top)),complement(composition(sk1,X0))))
| ~ spl13_11
| ~ spl13_16 ),
inference(backward_demodulation,[],[f4558,f4725]) ).
fof(f4972,definition,
( spl13_22
<=> sF2 = complement(sF3) ),
introduced(definition,[new_symbols(definition,[spl13_22])],[avatar_definition]) ).
fof(f4974,plain,
( sF2 = complement(sF3)
| ~ spl13_22 ),
inference(avatar_component_clause,[],[f4972]) ).
fof(f4975,plain,
( spl13_22
| ~ spl13_8
| ~ spl13_11 ),
inference(avatar_split_clause,[],[f679,f254,f166,f4972]) ).
fof(f4982,definition,
( spl13_24
<=> sF4 = complement(sF5) ),
introduced(definition,[new_symbols(definition,[spl13_24])],[avatar_definition]) ).
fof(f4984,plain,
( sF4 = complement(sF5)
| ~ spl13_24 ),
inference(avatar_component_clause,[],[f4982]) ).
fof(f4985,plain,
( spl13_24
| ~ spl13_10
| ~ spl13_11 ),
inference(avatar_split_clause,[],[f680,f254,f196,f4982]) ).
fof(f5048,plain,
( ! [X0,X1] : composition(complement(join(complement(X0),complement(composition(complement(composition(X0,top)),converse(X1))))),complement(join(complement(X1),complement(zero)))) = join(complement(join(complement(composition(X0,X1)),complement(complement(composition(X0,top))))),composition(complement(join(complement(X0),complement(composition(complement(composition(X0,top)),converse(X1))))),complement(join(complement(X1),complement(zero)))))
| ~ spl13_11 ),
inference(superposition,[],[f29,f1604]) ).
fof(f5077,plain,
( ! [X0,X1] : composition(complement(join(complement(X0),complement(composition(complement(composition(X0,top)),converse(X1))))),complement(join(complement(X1),top))) = join(complement(join(complement(composition(X0,X1)),complement(complement(composition(X0,top))))),composition(complement(join(complement(X0),complement(composition(complement(composition(X0,top)),converse(X1))))),complement(join(complement(X1),top))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f5048,f1388]) ).
fof(f5090,plain,
( ! [X0,X1] : composition(complement(join(complement(X0),complement(composition(complement(composition(X0,top)),converse(X1))))),complement(join(top,complement(X1)))) = join(complement(join(complement(composition(X0,X1)),complement(complement(composition(X0,top))))),composition(complement(join(complement(X0),complement(composition(complement(composition(X0,top)),converse(X1))))),complement(join(top,complement(X1)))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f5077,f2134]) ).
fof(f5101,plain,
( ! [X0,X1] : composition(complement(join(complement(X0),complement(composition(complement(composition(X0,top)),converse(X1))))),complement(top)) = join(complement(join(complement(composition(X0,X1)),complement(complement(composition(X0,top))))),composition(complement(join(complement(X0),complement(composition(complement(composition(X0,top)),converse(X1))))),complement(top)))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f5090,f1665]) ).
fof(f5108,plain,
( ! [X0,X1] : composition(complement(join(complement(X0),complement(composition(complement(composition(X0,top)),converse(X1))))),zero) = join(complement(join(complement(composition(X0,X1)),complement(complement(composition(X0,top))))),composition(complement(join(complement(X0),complement(composition(complement(composition(X0,top)),converse(X1))))),zero))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f5101,f256]) ).
fof(f5113,plain,
( ! [X0,X1] : composition(complement(join(complement(X0),complement(composition(complement(composition(X0,top)),converse(X1))))),zero) = join(complement(join(complement(composition(X0,X1)),composition(X0,top))),composition(complement(join(complement(X0),complement(composition(complement(composition(X0,top)),converse(X1))))),zero))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f5108,f667]) ).
fof(f5130,plain,
( ! [X0] : join(X0,composition(sk1,complement(X0))) = join(X0,composition(sk1,top))
| ~ spl13_16 ),
inference(superposition,[],[f2011,f15]) ).
fof(f5425,plain,
( ! [X0] : join(X0,composition(sk2,complement(X0))) = join(X0,composition(sk2,top))
| ~ spl13_17 ),
inference(superposition,[],[f1950,f15]) ).
fof(f5455,plain,
( join(sF0,composition(sk2,sF0)) = join(sF0,composition(sk2,sk1))
| ~ spl13_16
| ~ spl13_17 ),
inference(superposition,[],[f1950,f484]) ).
fof(f5533,plain,
( sF0 = join(sF0,composition(sk2,sk1))
| ~ spl13_16
| ~ spl13_17 ),
inference(forward_demodulation,[],[f5455,f1539]) ).
fof(f6180,plain,
( join(sF6,complement(composition(sk1,complement(sF5)))) = join(sF3,complement(composition(sk1,complement(sF5))))
| ~ spl13_11
| ~ spl13_13
| ~ spl13_16 ),
inference(superposition,[],[f269,f2167]) ).
fof(f6239,plain,
( join(sF6,complement(composition(sk1,sF4))) = join(sF3,complement(composition(sk1,sF4)))
| ~ spl13_11
| ~ spl13_13
| ~ spl13_16
| ~ spl13_24 ),
inference(forward_demodulation,[],[f6180,f4984]) ).
fof(f6280,definition,
( spl13_27
<=> sk1 = join(sF11,sk1) ),
introduced(definition,[new_symbols(definition,[spl13_27])],[avatar_definition]) ).
fof(f6282,plain,
( sk1 = join(sF11,sk1)
| ~ spl13_27 ),
inference(avatar_component_clause,[],[f6280]) ).
fof(f6283,plain,
( spl13_27
| ~ spl13_9
| ~ spl13_11
| ~ spl13_12
| ~ spl13_18 ),
inference(avatar_split_clause,[],[f2261,f1044,f259,f254,f181,f6280]) ).
fof(f6453,plain,
! [X2,X0,X1] : converse(composition(X0,join(converse(X1),X2))) = join(converse(composition(X0,X2)),composition(X1,converse(X0))),
inference(superposition,[],[f1,f3028]) ).
fof(f6458,plain,
( ! [X2,X0,X1] : complement(composition(X1,converse(X0))) = join(complement(converse(composition(X0,join(converse(X1),X2)))),complement(join(composition(X1,converse(X0)),complement(converse(composition(X0,X2))))))
| ~ spl13_11 ),
inference(superposition,[],[f694,f3028]) ).
fof(f6472,plain,
! [X2,X0,X1] : converse(composition(X0,join(converse(X1),X2))) = composition(join(converse(X2),X1),converse(X0)),
inference(forward_demodulation,[],[f6453,f298]) ).
fof(f6497,plain,
! [X2,X0,X1] : join(converse(composition(X0,X1)),composition(X2,converse(X0))) = converse(composition(X0,join(converse(X2),X1))),
inference(backward_demodulation,[],[f298,f6472]) ).
fof(f6656,definition,
( spl13_28
<=> top = complement(zero) ),
introduced(definition,[new_symbols(definition,[spl13_28])],[avatar_definition]) ).
fof(f6658,plain,
( top = complement(zero)
| ~ spl13_28 ),
inference(avatar_component_clause,[],[f6656]) ).
fof(f6659,plain,
( spl13_28
| ~ spl13_11 ),
inference(avatar_split_clause,[],[f1388,f254,f6656]) ).
fof(f6680,plain,
( ! [X0] : join(X0,complement(converse(complement(converse(X0))))) = join(X0,complement(converse(top)))
| ~ spl13_11 ),
inference(superposition,[],[f2152,f3003]) ).
fof(f6691,plain,
( top = converse(top)
| ~ spl13_11 ),
inference(superposition,[],[f1665,f3003]) ).
fof(f6719,plain,
( ! [X0] : join(X0,complement(top)) = join(X0,complement(converse(complement(converse(X0)))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f6680,f6691]) ).
fof(f6751,plain,
( ! [X0] : join(X0,zero) = join(X0,complement(converse(complement(converse(X0)))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f6719,f256]) ).
fof(f6768,plain,
( ! [X0] : join(X0,complement(converse(complement(converse(X0))))) = X0
| ~ spl13_11 ),
inference(forward_demodulation,[],[f6751,f1700]) ).
fof(f6879,definition,
( spl13_29
<=> top = converse(top) ),
introduced(definition,[new_symbols(definition,[spl13_29])],[avatar_definition]) ).
fof(f6881,plain,
( top = converse(top)
| ~ spl13_29 ),
inference(avatar_component_clause,[],[f6879]) ).
fof(f6882,plain,
( spl13_29
| ~ spl13_11 ),
inference(avatar_split_clause,[],[f6691,f254,f6879]) ).
fof(f6887,plain,
( ! [X0] : composition(top,converse(X0)) = converse(composition(X0,top))
| ~ spl13_29 ),
inference(superposition,[],[f12,f6881]) ).
fof(f7379,definition,
( spl13_33
<=> sF0 = converse(sF0) ),
introduced(definition,[new_symbols(definition,[spl13_33])],[avatar_definition]) ).
fof(f7381,plain,
( sF0 = converse(sF0)
| ~ spl13_33 ),
inference(avatar_component_clause,[],[f7379]) ).
fof(f7382,plain,
spl13_33,
inference(avatar_split_clause,[],[f1420,f7379]) ).
fof(f7393,plain,
( ! [X0] : join(sF0,converse(X0)) = converse(join(sF0,X0))
| ~ spl13_33 ),
inference(superposition,[],[f226,f7381]) ).
fof(f7479,definition,
( spl13_34
<=> sF2 = join(sF2,sF12) ),
introduced(definition,[new_symbols(definition,[spl13_34])],[avatar_definition]) ).
fof(f7481,plain,
( sF2 = join(sF2,sF12)
| ~ spl13_34 ),
inference(avatar_component_clause,[],[f7479]) ).
fof(f7482,plain,
( spl13_34
| ~ spl13_4
| ~ spl13_9
| ~ spl13_11
| ~ spl13_12
| ~ spl13_14
| ~ spl13_18 ),
inference(avatar_split_clause,[],[f2954,f1044,f271,f259,f254,f181,f128,f7479]) ).
fof(f7494,plain,
( complement(sF12) = join(complement(sF12),complement(sF2))
| ~ spl13_11
| ~ spl13_34 ),
inference(superposition,[],[f2128,f7481]) ).
fof(f7498,plain,
( complement(sF12) = join(complement(sF2),complement(sF12))
| ~ spl13_11
| ~ spl13_34 ),
inference(forward_demodulation,[],[f7494,f1]) ).
fof(f7506,plain,
( complement(sF12) = join(sF3,complement(sF12))
| ~ spl13_8
| ~ spl13_11
| ~ spl13_34 ),
inference(forward_demodulation,[],[f7498,f168]) ).
fof(f7521,plain,
( ! [X0] : join(X0,composition(top,X0)) = join(X0,composition(complement(sk2),X0))
| ~ spl13_17 ),
inference(superposition,[],[f1949,f15]) ).
fof(f7632,plain,
( ! [X0] : join(X0,composition(top,X0)) = join(X0,composition(sF9,X0))
| ~ spl13_5
| ~ spl13_17 ),
inference(forward_demodulation,[],[f7521,f141]) ).
fof(f7667,plain,
( ! [X0] : composition(top,X0) = join(X0,composition(sF9,X0))
| ~ spl13_5
| ~ spl13_11
| ~ spl13_17 ),
inference(forward_demodulation,[],[f7632,f2827]) ).
fof(f7724,plain,
( top = composition(top,top)
| ~ spl13_5
| ~ spl13_11
| ~ spl13_17 ),
inference(superposition,[],[f1665,f7667]) ).
fof(f8127,definition,
( spl13_35
<=> sF4 = join(sF4,sF12) ),
introduced(definition,[new_symbols(definition,[spl13_35])],[avatar_definition]) ).
fof(f8129,plain,
( sF4 = join(sF4,sF12)
| ~ spl13_35 ),
inference(avatar_component_clause,[],[f8127]) ).
fof(f8130,plain,
( spl13_35
| ~ spl13_4
| ~ spl13_5
| ~ spl13_7
| ~ spl13_9
| ~ spl13_11
| ~ spl13_12
| ~ spl13_15
| ~ spl13_18
| ~ spl13_19 ),
inference(avatar_split_clause,[],[f2953,f1049,f1044,f283,f259,f254,f181,f149,f139,f128,f8127]) ).
fof(f8142,plain,
( complement(sF12) = join(complement(sF12),complement(sF4))
| ~ spl13_11
| ~ spl13_35 ),
inference(superposition,[],[f2128,f8129]) ).
fof(f8146,plain,
( complement(sF12) = join(complement(sF4),complement(sF12))
| ~ spl13_11
| ~ spl13_35 ),
inference(forward_demodulation,[],[f8142,f1]) ).
fof(f8154,plain,
( complement(sF12) = join(sF5,complement(sF12))
| ~ spl13_10
| ~ spl13_11
| ~ spl13_35 ),
inference(forward_demodulation,[],[f8146,f198]) ).
fof(f8194,plain,
( zero = converse(zero)
| ~ spl13_11 ),
inference(superposition,[],[f1577,f3030]) ).
fof(f8268,definition,
( spl13_36
<=> zero = converse(zero) ),
introduced(definition,[new_symbols(definition,[spl13_36])],[avatar_definition]) ).
fof(f8270,plain,
( zero = converse(zero)
| ~ spl13_36 ),
inference(avatar_component_clause,[],[f8268]) ).
fof(f8271,plain,
( spl13_36
| ~ spl13_11 ),
inference(avatar_split_clause,[],[f8194,f254,f8268]) ).
fof(f8288,plain,
( ! [X0,X1] : converse(composition(zero,join(converse(X1),X0))) = join(converse(composition(zero,X0)),composition(X1,zero))
| ~ spl13_36 ),
inference(superposition,[],[f6497,f8270]) ).
fof(f8614,plain,
( ! [X0] : join(X0,complement(composition(sk1,complement(X0)))) = join(X0,complement(join(X0,composition(sk1,top))))
| ~ spl13_11
| ~ spl13_16 ),
inference(superposition,[],[f2152,f5130]) ).
fof(f8651,plain,
( ! [X0] : join(X0,complement(composition(sk1,complement(X0)))) = join(X0,complement(composition(sk1,top)))
| ~ spl13_11
| ~ spl13_16 ),
inference(forward_demodulation,[],[f8614,f2152]) ).
fof(f8687,plain,
( ! [X0] : complement(composition(sk1,complement(X0))) = join(X0,complement(composition(sk1,top)))
| ~ spl13_11
| ~ spl13_16 ),
inference(forward_demodulation,[],[f8651,f2167]) ).
fof(f8710,plain,
( ! [X0] : complement(complement(composition(sk1,complement(complement(X0))))) = join(composition(converse(sk1),X0),complement(complement(composition(sk1,complement(complement(X0))))))
| ~ spl13_11
| ~ spl13_16 ),
inference(backward_demodulation,[],[f4592,f8687]) ).
fof(f8726,plain,
( ! [X0] : composition(sk1,complement(complement(X0))) = join(composition(converse(sk1),X0),composition(sk1,complement(complement(X0))))
| ~ spl13_11
| ~ spl13_16 ),
inference(forward_demodulation,[],[f8710,f667]) ).
fof(f8740,plain,
( ! [X0] : composition(sk1,X0) = join(composition(converse(sk1),X0),composition(sk1,X0))
| ~ spl13_11
| ~ spl13_16 ),
inference(forward_demodulation,[],[f8726,f667]) ).
fof(f8751,plain,
( ! [X0] : composition(sk1,X0) = composition(join(converse(sk1),sk1),X0)
| ~ spl13_11
| ~ spl13_16 ),
inference(forward_demodulation,[],[f8740,f9]) ).
fof(f8757,plain,
( ! [X0] : composition(sk1,X0) = composition(join(sk1,converse(sk1)),X0)
| ~ spl13_11
| ~ spl13_16 ),
inference(forward_demodulation,[],[f8751,f82]) ).
fof(f8777,plain,
( ! [X0,X1] : join(X1,complement(composition(sk1,complement(X0)))) = join(X0,join(complement(composition(sk1,top)),X1))
| ~ spl13_11
| ~ spl13_16 ),
inference(superposition,[],[f219,f8687]) ).
fof(f8791,plain,
( ! [X0,X1] : complement(composition(sk1,complement(join(X0,X1)))) = join(X0,join(X1,complement(composition(sk1,top))))
| ~ spl13_11
| ~ spl13_16 ),
inference(superposition,[],[f2,f8687]) ).
fof(f8805,plain,
( ! [X0] : converse(complement(composition(sk1,complement(converse(X0))))) = join(X0,converse(complement(composition(sk1,top))))
| ~ spl13_11
| ~ spl13_16 ),
inference(superposition,[],[f226,f8687]) ).
fof(f8812,plain,
( join(sF3,complement(composition(sk1,complement(sF5)))) = join(sF6,complement(composition(sk1,top)))
| ~ spl13_11
| ~ spl13_13
| ~ spl13_16 ),
inference(superposition,[],[f269,f8687]) ).
fof(f8815,plain,
( complement(composition(sk1,complement(sF6))) = join(sF3,complement(composition(sk1,complement(sF5))))
| ~ spl13_11
| ~ spl13_13
| ~ spl13_16 ),
inference(forward_demodulation,[],[f8812,f8687]) ).
fof(f8831,plain,
( ! [X0,X1] : complement(composition(sk1,complement(join(X0,X1)))) = join(X0,complement(composition(sk1,complement(X1))))
| ~ spl13_11
| ~ spl13_16 ),
inference(forward_demodulation,[],[f8791,f8687]) ).
fof(f8840,plain,
( ! [X0] : complement(composition(sk1,X0)) = join(complement(composition(sk1,X0)),complement(composition(sk1,complement(complement(X0)))))
| ~ spl13_11
| ~ spl13_16 ),
inference(backward_demodulation,[],[f4731,f8777]) ).
fof(f8853,plain,
( complement(composition(sk1,complement(sF6))) = join(sF3,complement(composition(sk1,sF4)))
| ~ spl13_11
| ~ spl13_13
| ~ spl13_16
| ~ spl13_24 ),
inference(forward_demodulation,[],[f8815,f4984]) ).
fof(f8867,plain,
( ! [X0] : complement(complement(composition(sk1,complement(join(complement(X0),join(complement(sk3),complement(composition(converse(sk1),X0)))))))) = join(complement(join(sF3,complement(X0))),complement(complement(composition(sk1,complement(join(complement(X0),join(complement(sk3),complement(composition(converse(sk1),X0)))))))))
| ~ spl13_8
| ~ spl13_11
| ~ spl13_14
| ~ spl13_16 ),
inference(backward_demodulation,[],[f4413,f8831]) ).
fof(f8876,plain,
( ! [X0] : complement(composition(sk1,X0)) = complement(composition(sk1,complement(join(complement(composition(sk1,X0)),complement(X0)))))
| ~ spl13_11
| ~ spl13_16 ),
inference(forward_demodulation,[],[f8840,f8831]) ).
fof(f8884,plain,
( complement(composition(sk1,sF7)) = join(sF3,complement(composition(sk1,sF4)))
| ~ spl13_2
| ~ spl13_11
| ~ spl13_13
| ~ spl13_16
| ~ spl13_24 ),
inference(forward_demodulation,[],[f8853,f107]) ).
fof(f8893,plain,
( ! [X0] : composition(sk1,complement(join(complement(X0),join(complement(sk3),complement(composition(converse(sk1),X0)))))) = join(complement(join(sF3,complement(X0))),composition(sk1,complement(join(complement(X0),join(complement(sk3),complement(composition(converse(sk1),X0)))))))
| ~ spl13_8
| ~ spl13_11
| ~ spl13_14
| ~ spl13_16 ),
inference(forward_demodulation,[],[f8867,f667]) ).
fof(f8901,plain,
( ! [X0] : complement(composition(sk1,X0)) = complement(composition(sk1,complement(join(complement(X0),complement(composition(sk1,X0))))))
| ~ spl13_11
| ~ spl13_16 ),
inference(forward_demodulation,[],[f8876,f2134]) ).
fof(f8904,plain,
( complement(composition(sk1,sF7)) = join(sF6,complement(composition(sk1,sF4)))
| ~ spl13_2
| ~ spl13_11
| ~ spl13_13
| ~ spl13_16
| ~ spl13_24 ),
inference(backward_demodulation,[],[f6239,f8884]) ).
fof(f8918,plain,
( ! [X0] : complement(composition(sk1,X0)) = complement(composition(sk1,complement(complement(composition(sk1,X0)))))
| ~ spl13_11
| ~ spl13_16 ),
inference(forward_demodulation,[],[f8901,f2171]) ).
fof(f8926,plain,
( ! [X0] : complement(composition(sk1,X0)) = complement(composition(sk1,composition(sk1,X0)))
| ~ spl13_11
| ~ spl13_16 ),
inference(forward_demodulation,[],[f8918,f667]) ).
fof(f8941,plain,
( ! [X0,X1] : join(X1,complement(composition(sk1,X0))) = complement(composition(sk1,complement(join(X1,complement(X0)))))
| ~ spl13_11
| ~ spl13_16 ),
inference(superposition,[],[f8831,f667]) ).
fof(f9155,plain,
( complement(sF2) = complement(composition(sk1,sF2))
| ~ spl13_11
| ~ spl13_14
| ~ spl13_16 ),
inference(superposition,[],[f8926,f273]) ).
fof(f9171,plain,
( ! [X0] : composition(sk1,composition(sk1,X0)) = complement(complement(composition(sk1,X0)))
| ~ spl13_11
| ~ spl13_16 ),
inference(superposition,[],[f667,f8926]) ).
fof(f9194,plain,
( ! [X0] : composition(sk1,X0) = composition(sk1,composition(sk1,X0))
| ~ spl13_11
| ~ spl13_16 ),
inference(forward_demodulation,[],[f9171,f667]) ).
fof(f9206,plain,
( sF3 = complement(composition(sk1,sF2))
| ~ spl13_8
| ~ spl13_11
| ~ spl13_14
| ~ spl13_16 ),
inference(forward_demodulation,[],[f9155,f168]) ).
fof(f9351,definition,
( spl13_40
<=> sF3 = complement(composition(sk1,sF2)) ),
introduced(definition,[new_symbols(definition,[spl13_40])],[avatar_definition]) ).
fof(f9353,plain,
( sF3 = complement(composition(sk1,sF2))
| ~ spl13_40 ),
inference(avatar_component_clause,[],[f9351]) ).
fof(f9354,plain,
( spl13_40
| ~ spl13_8
| ~ spl13_11
| ~ spl13_14
| ~ spl13_16 ),
inference(avatar_split_clause,[],[f9206,f482,f271,f254,f166,f9351]) ).
fof(f9369,plain,
( complement(sF3) = composition(sk1,sF2)
| ~ spl13_11
| ~ spl13_40 ),
inference(superposition,[],[f667,f9353]) ).
fof(f9391,plain,
( sF2 = composition(sk1,sF2)
| ~ spl13_11
| ~ spl13_22
| ~ spl13_40 ),
inference(forward_demodulation,[],[f9369,f4974]) ).
fof(f9710,plain,
( ! [X0] : join(X0,complement(composition(sk2,complement(X0)))) = join(X0,complement(join(X0,composition(sk2,top))))
| ~ spl13_11
| ~ spl13_17 ),
inference(superposition,[],[f2152,f5425]) ).
fof(f9747,plain,
( ! [X0] : join(X0,complement(composition(sk2,complement(X0)))) = join(X0,complement(composition(sk2,top)))
| ~ spl13_11
| ~ spl13_17 ),
inference(forward_demodulation,[],[f9710,f2152]) ).
fof(f9783,plain,
( ! [X0] : complement(composition(sk2,complement(X0))) = join(X0,complement(composition(sk2,top)))
| ~ spl13_11
| ~ spl13_17 ),
inference(forward_demodulation,[],[f9747,f2168]) ).
fof(f9806,plain,
( ! [X0] : complement(complement(composition(sk2,complement(complement(X0))))) = join(composition(converse(sk2),X0),complement(complement(composition(sk2,complement(complement(X0))))))
| ~ spl13_11
| ~ spl13_17 ),
inference(backward_demodulation,[],[f4591,f9783]) ).
fof(f9822,plain,
( ! [X0] : composition(sk2,complement(complement(X0))) = join(composition(converse(sk2),X0),composition(sk2,complement(complement(X0))))
| ~ spl13_11
| ~ spl13_17 ),
inference(forward_demodulation,[],[f9806,f667]) ).
fof(f9836,plain,
( ! [X0] : composition(sk2,X0) = join(composition(converse(sk2),X0),composition(sk2,X0))
| ~ spl13_11
| ~ spl13_17 ),
inference(forward_demodulation,[],[f9822,f667]) ).
fof(f9847,plain,
( ! [X0] : composition(sk2,X0) = composition(join(converse(sk2),sk2),X0)
| ~ spl13_11
| ~ spl13_17 ),
inference(forward_demodulation,[],[f9836,f9]) ).
fof(f9853,plain,
( ! [X0] : composition(sk2,X0) = composition(join(sk2,converse(sk2)),X0)
| ~ spl13_11
| ~ spl13_17 ),
inference(forward_demodulation,[],[f9847,f82]) ).
fof(f9873,plain,
( ! [X0,X1] : join(X1,complement(composition(sk2,complement(X0)))) = join(X0,join(complement(composition(sk2,top)),X1))
| ~ spl13_11
| ~ spl13_17 ),
inference(superposition,[],[f219,f9783]) ).
fof(f9887,plain,
( ! [X0,X1] : complement(composition(sk2,complement(join(X0,X1)))) = join(X0,join(X1,complement(composition(sk2,top))))
| ~ spl13_11
| ~ spl13_17 ),
inference(superposition,[],[f2,f9783]) ).
fof(f9901,plain,
( ! [X0] : converse(complement(composition(sk2,complement(converse(X0))))) = join(X0,converse(complement(composition(sk2,top))))
| ~ spl13_11
| ~ spl13_17 ),
inference(superposition,[],[f226,f9783]) ).
fof(f9910,plain,
( join(sF8,complement(composition(sk2,complement(sF9)))) = join(sF10,complement(composition(sk2,top)))
| ~ spl13_11
| ~ spl13_12
| ~ spl13_17 ),
inference(superposition,[],[f263,f9783]) ).
fof(f9911,plain,
( complement(composition(sk2,complement(sF10))) = join(sF8,complement(composition(sk2,complement(sF9))))
| ~ spl13_11
| ~ spl13_12
| ~ spl13_17 ),
inference(forward_demodulation,[],[f9910,f9783]) ).
fof(f9929,plain,
( ! [X0,X1] : complement(composition(sk2,complement(join(X0,X1)))) = join(X0,complement(composition(sk2,complement(X1))))
| ~ spl13_11
| ~ spl13_17 ),
inference(forward_demodulation,[],[f9887,f9783]) ).
fof(f9938,plain,
( ! [X0] : complement(composition(sk2,X0)) = join(complement(composition(sk2,X0)),complement(composition(sk2,complement(complement(X0)))))
| ~ spl13_11
| ~ spl13_17 ),
inference(backward_demodulation,[],[f4727,f9873]) ).
fof(f9950,plain,
( complement(composition(sk2,complement(sF10))) = join(sF8,complement(composition(sk2,sk2)))
| ~ spl13_11
| ~ spl13_12
| ~ spl13_17
| ~ spl13_19 ),
inference(forward_demodulation,[],[f9911,f1051]) ).
fof(f9971,plain,
( ! [X0] : complement(complement(composition(sk2,complement(join(complement(X0),join(complement(sk3),complement(composition(converse(sk2),X0)))))))) = join(complement(join(sF5,complement(X0))),complement(complement(composition(sk2,complement(join(complement(X0),join(complement(sk3),complement(composition(converse(sk2),X0)))))))))
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_17 ),
inference(backward_demodulation,[],[f4412,f9929]) ).
fof(f9998,plain,
( ! [X0] : complement(composition(sk2,X0)) = complement(composition(sk2,complement(join(complement(composition(sk2,X0)),complement(X0)))))
| ~ spl13_11
| ~ spl13_17 ),
inference(forward_demodulation,[],[f9938,f9929]) ).
fof(f10005,plain,
( complement(composition(sk2,sF11)) = join(sF8,complement(composition(sk2,sk2)))
| ~ spl13_9
| ~ spl13_11
| ~ spl13_12
| ~ spl13_17
| ~ spl13_19 ),
inference(forward_demodulation,[],[f9950,f183]) ).
fof(f10034,plain,
( ! [X0] : composition(sk2,complement(join(complement(X0),join(complement(sk3),complement(composition(converse(sk2),X0)))))) = join(complement(join(sF5,complement(X0))),composition(sk2,complement(join(complement(X0),join(complement(sk3),complement(composition(converse(sk2),X0)))))))
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_17 ),
inference(forward_demodulation,[],[f9971,f667]) ).
fof(f10046,plain,
( ! [X0] : complement(composition(sk2,X0)) = complement(composition(sk2,complement(join(complement(X0),complement(composition(sk2,X0))))))
| ~ spl13_11
| ~ spl13_17 ),
inference(forward_demodulation,[],[f9998,f2134]) ).
fof(f10069,plain,
( ! [X0] : complement(composition(sk2,X0)) = complement(composition(sk2,complement(complement(composition(sk2,X0)))))
| ~ spl13_11
| ~ spl13_17 ),
inference(forward_demodulation,[],[f10046,f2172]) ).
fof(f10083,plain,
( ! [X0] : complement(composition(sk2,X0)) = complement(composition(sk2,composition(sk2,X0)))
| ~ spl13_11
| ~ spl13_17 ),
inference(forward_demodulation,[],[f10069,f667]) ).
fof(f10117,plain,
( ! [X0,X1] : join(X1,complement(composition(sk2,X0))) = complement(composition(sk2,complement(join(X1,complement(X0)))))
| ~ spl13_11
| ~ spl13_17 ),
inference(superposition,[],[f9929,f667]) ).
fof(f10332,plain,
( complement(sk2) = complement(composition(sk2,sk2))
| ~ spl13_11
| ~ spl13_17 ),
inference(superposition,[],[f10083,f68]) ).
fof(f10347,plain,
( ! [X0] : composition(sk2,composition(sk2,X0)) = complement(complement(composition(sk2,X0)))
| ~ spl13_11
| ~ spl13_17 ),
inference(superposition,[],[f667,f10083]) ).
fof(f10373,plain,
( ! [X0] : composition(sk2,X0) = composition(sk2,composition(sk2,X0))
| ~ spl13_11
| ~ spl13_17 ),
inference(forward_demodulation,[],[f10347,f667]) ).
fof(f10384,plain,
( sF9 = complement(composition(sk2,sk2))
| ~ spl13_5
| ~ spl13_11
| ~ spl13_17 ),
inference(forward_demodulation,[],[f10332,f141]) ).
fof(f10414,plain,
( join(sF8,sF9) = complement(composition(sk2,sF11))
| ~ spl13_5
| ~ spl13_9
| ~ spl13_11
| ~ spl13_12
| ~ spl13_17
| ~ spl13_19 ),
inference(backward_demodulation,[],[f10005,f10384]) ).
fof(f10432,plain,
( sF10 = complement(composition(sk2,sF11))
| ~ spl13_5
| ~ spl13_9
| ~ spl13_11
| ~ spl13_12
| ~ spl13_17
| ~ spl13_19 ),
inference(forward_demodulation,[],[f10414,f261]) ).
fof(f10659,definition,
( spl13_43
<=> sF10 = complement(composition(sk2,sF11)) ),
introduced(definition,[new_symbols(definition,[spl13_43])],[avatar_definition]) ).
fof(f10661,plain,
( sF10 = complement(composition(sk2,sF11))
| ~ spl13_43 ),
inference(avatar_component_clause,[],[f10659]) ).
fof(f10662,plain,
( spl13_43
| ~ spl13_5
| ~ spl13_9
| ~ spl13_11
| ~ spl13_12
| ~ spl13_17
| ~ spl13_19 ),
inference(avatar_split_clause,[],[f10432,f1049,f573,f259,f254,f181,f139,f10659]) ).
fof(f10677,plain,
( complement(sF10) = composition(sk2,sF11)
| ~ spl13_11
| ~ spl13_43 ),
inference(superposition,[],[f667,f10661]) ).
fof(f10701,plain,
( sF11 = composition(sk2,sF11)
| ~ spl13_9
| ~ spl13_11
| ~ spl13_43 ),
inference(forward_demodulation,[],[f10677,f183]) ).
fof(f10926,definition,
( spl13_46
<=> sF11 = composition(sk2,sF11) ),
introduced(definition,[new_symbols(definition,[spl13_46])],[avatar_definition]) ).
fof(f10928,plain,
( sF11 = composition(sk2,sF11)
| ~ spl13_46 ),
inference(avatar_component_clause,[],[f10926]) ).
fof(f10929,plain,
( spl13_46
| ~ spl13_9
| ~ spl13_11
| ~ spl13_43 ),
inference(avatar_split_clause,[],[f10701,f10659,f254,f181,f10926]) ).
fof(f10934,plain,
( ! [X0] : composition(sF11,X0) = composition(sk2,composition(sF11,X0))
| ~ spl13_46 ),
inference(superposition,[],[f7,f10928]) ).
fof(f11293,plain,
( ! [X0,X1] : complement(join(complement(composition(complement(join(complement(X0),complement(composition(top,converse(X1))))),X1)),zero)) = join(complement(join(complement(composition(X0,X1)),zero)),complement(join(complement(composition(complement(join(complement(X0),complement(composition(top,converse(X1))))),X1)),zero)))
| ~ spl13_11 ),
inference(superposition,[],[f31,f256]) ).
fof(f11367,plain,
( ! [X0,X1] : complement(join(zero,complement(composition(complement(join(complement(X0),complement(composition(top,converse(X1))))),X1)))) = join(complement(join(complement(composition(X0,X1)),zero)),complement(join(zero,complement(composition(complement(join(complement(X0),complement(composition(top,converse(X1))))),X1)))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f11293,f2134]) ).
fof(f11462,plain,
( ! [X0,X1] : complement(complement(composition(complement(join(complement(X0),complement(composition(top,converse(X1))))),X1))) = join(complement(join(complement(composition(X0,X1)),zero)),complement(complement(composition(complement(join(complement(X0),complement(composition(top,converse(X1))))),X1))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f11367,f1577]) ).
fof(f11509,plain,
( ! [X0,X1] : composition(complement(join(complement(X0),complement(composition(top,converse(X1))))),X1) = join(complement(join(complement(composition(X0,X1)),zero)),composition(complement(join(complement(X0),complement(composition(top,converse(X1))))),X1))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f11462,f667]) ).
fof(f11545,plain,
( ! [X0,X1] : composition(complement(join(complement(X0),complement(converse(composition(X1,top))))),X1) = join(complement(join(complement(composition(X0,X1)),zero)),composition(complement(join(complement(X0),complement(converse(composition(X1,top))))),X1))
| ~ spl13_11
| ~ spl13_29 ),
inference(forward_demodulation,[],[f11509,f6887]) ).
fof(f11574,plain,
( ! [X0,X1] : composition(complement(join(complement(X0),complement(converse(composition(X1,top))))),X1) = join(complement(join(zero,complement(composition(X0,X1)))),composition(complement(join(complement(X0),complement(converse(composition(X1,top))))),X1))
| ~ spl13_11
| ~ spl13_29 ),
inference(forward_demodulation,[],[f11545,f2134]) ).
fof(f11598,plain,
( ! [X0,X1] : composition(complement(join(complement(X0),complement(converse(composition(X1,top))))),X1) = join(complement(complement(composition(X0,X1))),composition(complement(join(complement(X0),complement(converse(composition(X1,top))))),X1))
| ~ spl13_11
| ~ spl13_29 ),
inference(forward_demodulation,[],[f11574,f1577]) ).
fof(f11616,plain,
( ! [X0,X1] : composition(complement(join(complement(X0),complement(converse(composition(X1,top))))),X1) = join(composition(X0,X1),composition(complement(join(complement(X0),complement(converse(composition(X1,top))))),X1))
| ~ spl13_11
| ~ spl13_29 ),
inference(forward_demodulation,[],[f11598,f667]) ).
fof(f11629,plain,
( ! [X0,X1] : composition(complement(join(complement(X0),complement(converse(composition(X1,top))))),X1) = composition(join(X0,complement(join(complement(X0),complement(converse(composition(X1,top)))))),X1)
| ~ spl13_11
| ~ spl13_29 ),
inference(forward_demodulation,[],[f11616,f9]) ).
fof(f11637,plain,
( ! [X0,X1] : composition(X0,X1) = composition(complement(join(complement(X0),complement(converse(composition(X1,top))))),X1)
| ~ spl13_11
| ~ spl13_29 ),
inference(forward_demodulation,[],[f11629,f2178]) ).
fof(f11774,plain,
( ! [X0] : complement(join(complement(X0),complement(complement(composition(X0,top))))) = composition(complement(join(complement(X0),complement(complement(composition(X0,top))))),complement(join(complement(sF0),complement(zero))))
| ~ spl13_11 ),
inference(superposition,[],[f4240,f1604]) ).
fof(f11808,plain,
( ! [X0] : complement(join(complement(X0),complement(complement(composition(X0,top))))) = composition(complement(join(complement(X0),complement(complement(composition(X0,top))))),complement(join(complement(zero),complement(sF0))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f11774,f2134]) ).
fof(f11855,plain,
( ! [X0] : complement(join(complement(X0),complement(complement(composition(X0,top))))) = composition(complement(join(complement(X0),complement(complement(composition(X0,top))))),complement(join(top,complement(sF0))))
| ~ spl13_11
| ~ spl13_28 ),
inference(forward_demodulation,[],[f11808,f6658]) ).
fof(f11877,plain,
( ! [X0] : complement(join(complement(X0),complement(complement(composition(X0,top))))) = composition(complement(join(complement(X0),complement(complement(composition(X0,top))))),complement(top))
| ~ spl13_11
| ~ spl13_28 ),
inference(forward_demodulation,[],[f11855,f1665]) ).
fof(f11891,plain,
( ! [X0] : complement(join(complement(X0),complement(complement(composition(X0,top))))) = composition(complement(join(complement(X0),complement(complement(composition(X0,top))))),zero)
| ~ spl13_11
| ~ spl13_28 ),
inference(forward_demodulation,[],[f11877,f256]) ).
fof(f11898,plain,
( ! [X0] : complement(join(complement(X0),composition(X0,top))) = composition(complement(join(complement(X0),composition(X0,top))),zero)
| ~ spl13_11
| ~ spl13_28 ),
inference(forward_demodulation,[],[f11891,f667]) ).
fof(f12063,plain,
! [X2,X0,X1] : join(composition(X1,converse(X0)),converse(X2)) = converse(join(composition(X0,converse(X1)),X2)),
inference(superposition,[],[f226,f294]) ).
fof(f12064,plain,
! [X2,X0,X1] : join(converse(X2),composition(X1,converse(X0))) = converse(join(X2,composition(X0,converse(X1)))),
inference(superposition,[],[f227,f294]) ).
fof(f13084,plain,
( ! [X0] : composition(zero,X0) = composition(zero,complement(join(complement(X0),complement(composition(zero,top)))))
| ~ spl13_11
| ~ spl13_36 ),
inference(superposition,[],[f4513,f8270]) ).
fof(f13259,plain,
( ! [X0] : complement(complement(converse(complement(converse(complement(X0)))))) = join(complement(join(X0,complement(converse(complement(converse(complement(X0))))))),complement(complement(X0)))
| ~ spl13_11 ),
inference(superposition,[],[f792,f6768]) ).
fof(f13269,plain,
( ! [X0] : converse(converse(X0)) = join(X0,converse(complement(converse(complement(converse(converse(X0)))))))
| ~ spl13_11 ),
inference(superposition,[],[f226,f6768]) ).
fof(f13286,plain,
( ! [X0] : join(X0,converse(complement(converse(complement(X0))))) = X0
| ~ spl13_11 ),
inference(forward_demodulation,[],[f13269,f10]) ).
fof(f13296,plain,
( ! [X0] : complement(complement(converse(complement(converse(complement(X0)))))) = join(complement(complement(X0)),complement(join(X0,complement(converse(complement(converse(complement(X0))))))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f13259,f1]) ).
fof(f13324,plain,
( ! [X0] : complement(complement(converse(complement(converse(complement(X0)))))) = join(X0,complement(join(X0,complement(converse(complement(converse(complement(X0))))))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f13296,f667]) ).
fof(f13337,plain,
( ! [X0] : complement(complement(converse(complement(converse(complement(X0)))))) = join(X0,complement(complement(converse(complement(converse(complement(X0)))))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f13324,f2152]) ).
fof(f13342,plain,
( ! [X0] : converse(complement(converse(complement(X0)))) = join(X0,converse(complement(converse(complement(X0)))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f13337,f667]) ).
fof(f13345,plain,
( ! [X0] : converse(complement(converse(complement(X0)))) = X0
| ~ spl13_11 ),
inference(forward_demodulation,[],[f13342,f13286]) ).
fof(f13364,plain,
( ! [X0] : converse(X0) = complement(converse(complement(X0)))
| ~ spl13_11 ),
inference(superposition,[],[f10,f13345]) ).
fof(f13536,plain,
( ! [X0] : complement(converse(X0)) = converse(complement(X0))
| ~ spl13_11 ),
inference(superposition,[],[f667,f13364]) ).
fof(f13563,plain,
( ! [X0,X1] : converse(complement(X0)) = join(converse(complement(X0)),composition(X1,complement(converse(composition(X0,X1)))))
| ~ spl13_11 ),
inference(backward_demodulation,[],[f300,f13536]) ).
fof(f13594,plain,
( ! [X0] : join(X0,converse(complement(composition(sk1,top)))) = converse(complement(composition(sk1,converse(complement(X0)))))
| ~ spl13_11
| ~ spl13_16 ),
inference(backward_demodulation,[],[f8805,f13536]) ).
fof(f13596,plain,
( ! [X0] : join(X0,converse(complement(composition(sk2,top)))) = converse(complement(composition(sk2,converse(complement(X0)))))
| ~ spl13_11
| ~ spl13_17 ),
inference(backward_demodulation,[],[f9901,f13536]) ).
fof(f13610,plain,
( ! [X2,X0,X1] : complement(composition(X1,converse(X0))) = join(complement(converse(composition(X0,join(converse(X1),X2)))),complement(join(composition(X1,converse(X0)),converse(complement(composition(X0,X2))))))
| ~ spl13_11 ),
inference(backward_demodulation,[],[f6458,f13536]) ).
fof(f13620,plain,
( ! [X0,X1] : composition(X0,X1) = composition(complement(join(complement(X0),converse(complement(composition(X1,top))))),X1)
| ~ spl13_11
| ~ spl13_29 ),
inference(backward_demodulation,[],[f11637,f13536]) ).
fof(f13693,plain,
( ! [X2,X0,X1] : complement(composition(X1,converse(X0))) = join(complement(converse(composition(X0,join(converse(X1),X2)))),complement(converse(join(composition(X0,converse(X1)),complement(composition(X0,X2))))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f13610,f12063]) ).
fof(f13725,plain,
( ! [X0,X1] : converse(complement(X0)) = join(converse(complement(X0)),composition(X1,converse(complement(composition(X0,X1)))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f13563,f13536]) ).
fof(f13749,plain,
( ! [X2,X0,X1] : complement(composition(X1,converse(X0))) = join(complement(converse(composition(X0,join(converse(X1),X2)))),converse(complement(join(composition(X0,converse(X1)),complement(composition(X0,X2))))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f13693,f13536]) ).
fof(f13766,plain,
( ! [X0,X1] : converse(complement(X0)) = converse(join(complement(X0),composition(complement(composition(X0,X1)),converse(X1))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f13725,f12064]) ).
fof(f13781,plain,
( ! [X2,X0,X1] : complement(composition(X1,converse(X0))) = join(converse(complement(composition(X0,join(converse(X1),X2)))),converse(complement(join(composition(X0,converse(X1)),complement(composition(X0,X2))))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f13749,f13536]) ).
fof(f13797,plain,
( ! [X2,X0,X1] : complement(composition(X1,converse(X0))) = converse(join(complement(composition(X0,join(converse(X1),X2))),complement(join(composition(X0,converse(X1)),complement(composition(X0,X2))))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f13781,f11]) ).
fof(f13805,plain,
( ! [X0,X1] : complement(composition(X1,converse(X0))) = converse(complement(composition(X0,converse(X1))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f13797,f713]) ).
fof(f13813,plain,
( ! [X0] : join(X0,converse(complement(composition(sk2,top)))) = complement(composition(complement(X0),converse(sk2)))
| ~ spl13_11
| ~ spl13_17 ),
inference(backward_demodulation,[],[f13596,f13805]) ).
fof(f13814,plain,
( ! [X0] : join(X0,converse(complement(composition(sk1,top)))) = complement(composition(complement(X0),converse(sk1)))
| ~ spl13_11
| ~ spl13_16 ),
inference(backward_demodulation,[],[f13594,f13805]) ).
fof(f14054,plain,
( ! [X0,X1] : join(X1,complement(composition(sk1,X0))) = complement(composition(sk1,complement(join(complement(X0),X1))))
| ~ spl13_11
| ~ spl13_16 ),
inference(superposition,[],[f8941,f1]) ).
fof(f14073,plain,
( ! [X0,X1] : join(X0,complement(composition(sk1,X1))) = join(complement(complement(join(X0,complement(X1)))),join(X0,complement(composition(sk1,X1))))
| ~ spl13_11
| ~ spl13_16 ),
inference(superposition,[],[f2171,f8941]) ).
fof(f14090,plain,
( ! [X0,X1] : complement(join(X0,complement(composition(sk1,X1)))) = composition(sk1,complement(join(X0,complement(X1))))
| ~ spl13_11
| ~ spl13_16 ),
inference(superposition,[],[f667,f8941]) ).
fof(f14149,plain,
( ! [X0,X1] : join(X0,complement(composition(sk1,X1))) = join(join(X0,complement(composition(sk1,X1))),complement(complement(join(X0,complement(X1)))))
| ~ spl13_11
| ~ spl13_16 ),
inference(forward_demodulation,[],[f14073,f1]) ).
fof(f14210,plain,
( ! [X0,X1] : join(X0,complement(composition(sk1,X1))) = join(X0,join(complement(composition(sk1,X1)),complement(complement(join(X0,complement(X1))))))
| ~ spl13_11
| ~ spl13_16 ),
inference(forward_demodulation,[],[f14149,f2]) ).
fof(f14243,plain,
( ! [X0,X1] : join(X0,complement(composition(sk1,X1))) = join(X0,join(complement(composition(sk1,X1)),join(X0,complement(X1))))
| ~ spl13_11
| ~ spl13_16 ),
inference(forward_demodulation,[],[f14210,f667]) ).
fof(f14262,plain,
( ! [X0,X1] : join(X0,complement(composition(sk1,X1))) = join(X0,join(complement(X1),join(X0,complement(composition(sk1,X1)))))
| ~ spl13_11
| ~ spl13_16 ),
inference(forward_demodulation,[],[f14243,f3431]) ).
fof(f14271,plain,
( ! [X0,X1] : join(X0,complement(composition(sk1,X1))) = join(complement(X1),join(X0,complement(composition(sk1,X1))))
| ~ spl13_11
| ~ spl13_16 ),
inference(forward_demodulation,[],[f14262,f3404]) ).
fof(f15052,definition,
( spl13_50
<=> sF8 = join(sF8,complement(sF0)) ),
introduced(definition,[new_symbols(definition,[spl13_50])],[avatar_definition]) ).
fof(f15054,plain,
( sF8 = join(sF8,complement(sF0))
| ~ spl13_50 ),
inference(avatar_component_clause,[],[f15052]) ).
fof(f15055,plain,
( spl13_50
| ~ spl13_7
| ~ spl13_11
| ~ spl13_16 ),
inference(avatar_split_clause,[],[f2516,f482,f254,f149,f15052]) ).
fof(f15122,plain,
( ! [X0] : join(X0,complement(composition(sk2,composition(sk1,top)))) = complement(composition(sk2,complement(complement(composition(sk1,complement(X0))))))
| ~ spl13_11
| ~ spl13_16
| ~ spl13_17 ),
inference(superposition,[],[f10117,f8687]) ).
fof(f15144,plain,
( complement(composition(sk2,complement(sF8))) = join(sF8,complement(composition(sk2,sF0)))
| ~ spl13_11
| ~ spl13_17
| ~ spl13_50 ),
inference(superposition,[],[f10117,f15054]) ).
fof(f15148,plain,
( ! [X0,X1] : join(X0,complement(composition(sk2,X1))) = join(complement(complement(join(X0,complement(X1)))),join(X0,complement(composition(sk2,X1))))
| ~ spl13_11
| ~ spl13_17 ),
inference(superposition,[],[f2172,f10117]) ).
fof(f15165,plain,
( ! [X0,X1] : complement(join(X0,complement(composition(sk2,X1)))) = composition(sk2,complement(join(X0,complement(X1))))
| ~ spl13_11
| ~ spl13_17 ),
inference(superposition,[],[f667,f10117]) ).
fof(f15235,plain,
( ! [X0,X1] : join(X0,complement(composition(sk2,X1))) = join(join(X0,complement(composition(sk2,X1))),complement(complement(join(X0,complement(X1)))))
| ~ spl13_11
| ~ spl13_17 ),
inference(forward_demodulation,[],[f15148,f1]) ).
fof(f15238,plain,
( complement(composition(sk2,complement(sF8))) = join(sF8,complement(sk2))
| ~ spl13_11
| ~ spl13_17
| ~ spl13_50 ),
inference(forward_demodulation,[],[f15144,f68]) ).
fof(f15258,plain,
( ! [X0] : join(X0,complement(composition(sk2,composition(sk1,top)))) = complement(composition(sk2,composition(sk1,complement(X0))))
| ~ spl13_11
| ~ spl13_16
| ~ spl13_17 ),
inference(forward_demodulation,[],[f15122,f667]) ).
fof(f15302,plain,
( ! [X0,X1] : join(X0,complement(composition(sk2,X1))) = join(X0,join(complement(composition(sk2,X1)),complement(complement(join(X0,complement(X1))))))
| ~ spl13_11
| ~ spl13_17 ),
inference(forward_demodulation,[],[f15235,f2]) ).
fof(f15304,plain,
( join(sF8,sF9) = complement(composition(sk2,complement(sF8)))
| ~ spl13_5
| ~ spl13_11
| ~ spl13_17
| ~ spl13_50 ),
inference(forward_demodulation,[],[f15238,f141]) ).
fof(f15338,plain,
( ! [X0,X1] : join(X0,complement(composition(sk2,X1))) = join(X0,join(complement(composition(sk2,X1)),join(X0,complement(X1))))
| ~ spl13_11
| ~ spl13_17 ),
inference(forward_demodulation,[],[f15302,f667]) ).
fof(f15340,plain,
( join(sF8,sF9) = complement(composition(sk2,sk1))
| ~ spl13_5
| ~ spl13_11
| ~ spl13_17
| ~ spl13_18
| ~ spl13_50 ),
inference(forward_demodulation,[],[f15304,f1046]) ).
fof(f15358,plain,
( ! [X0,X1] : join(X0,complement(composition(sk2,X1))) = join(X0,join(complement(X1),join(X0,complement(composition(sk2,X1)))))
| ~ spl13_11
| ~ spl13_17 ),
inference(forward_demodulation,[],[f15338,f3431]) ).
fof(f15359,plain,
( sF10 = complement(composition(sk2,sk1))
| ~ spl13_5
| ~ spl13_11
| ~ spl13_12
| ~ spl13_17
| ~ spl13_18
| ~ spl13_50 ),
inference(forward_demodulation,[],[f15340,f261]) ).
fof(f15368,plain,
( ! [X0,X1] : join(X0,complement(composition(sk2,X1))) = join(complement(X1),join(X0,complement(composition(sk2,X1))))
| ~ spl13_11
| ~ spl13_17 ),
inference(forward_demodulation,[],[f15358,f3404]) ).
fof(f15389,definition,
( spl13_51
<=> sF10 = complement(composition(sk2,sk1)) ),
introduced(definition,[new_symbols(definition,[spl13_51])],[avatar_definition]) ).
fof(f15391,plain,
( sF10 = complement(composition(sk2,sk1))
| ~ spl13_51 ),
inference(avatar_component_clause,[],[f15389]) ).
fof(f15392,plain,
( spl13_51
| ~ spl13_5
| ~ spl13_11
| ~ spl13_12
| ~ spl13_17
| ~ spl13_18
| ~ spl13_50 ),
inference(avatar_split_clause,[],[f15359,f15052,f1044,f573,f259,f254,f139,f15389]) ).
fof(f15411,plain,
( complement(sF10) = composition(sk2,sk1)
| ~ spl13_11
| ~ spl13_51 ),
inference(superposition,[],[f667,f15391]) ).
fof(f15439,plain,
( sF11 = composition(sk2,sk1)
| ~ spl13_9
| ~ spl13_11
| ~ spl13_51 ),
inference(forward_demodulation,[],[f15411,f183]) ).
fof(f15459,plain,
( sF0 = join(sF0,sF11)
| ~ spl13_9
| ~ spl13_11
| ~ spl13_16
| ~ spl13_17
| ~ spl13_51 ),
inference(backward_demodulation,[],[f5533,f15439]) ).
fof(f15497,plain,
( sF0 = join(sF11,sF0)
| ~ spl13_9
| ~ spl13_11
| ~ spl13_16
| ~ spl13_17
| ~ spl13_51 ),
inference(forward_demodulation,[],[f15459,f1]) ).
fof(f15510,plain,
( join(sF12,sk3) = composition(sF0,sk3)
| ~ spl13_4
| ~ spl13_9
| ~ spl13_11
| ~ spl13_16
| ~ spl13_17
| ~ spl13_51 ),
inference(backward_demodulation,[],[f1563,f15497]) ).
fof(f15514,plain,
( sk3 = join(sF12,sk3)
| ~ spl13_4
| ~ spl13_9
| ~ spl13_11
| ~ spl13_16
| ~ spl13_17
| ~ spl13_51 ),
inference(forward_demodulation,[],[f15510,f1425]) ).
fof(f15525,definition,
( spl13_52
<=> sF11 = composition(sk2,sk1) ),
introduced(definition,[new_symbols(definition,[spl13_52])],[avatar_definition]) ).
fof(f15527,plain,
( sF11 = composition(sk2,sk1)
| ~ spl13_52 ),
inference(avatar_component_clause,[],[f15525]) ).
fof(f15528,plain,
( spl13_52
| ~ spl13_9
| ~ spl13_11
| ~ spl13_51 ),
inference(avatar_split_clause,[],[f15439,f15389,f254,f181,f15525]) ).
fof(f15537,plain,
( ! [X0] : composition(sF11,X0) = composition(sk2,composition(sk1,X0))
| ~ spl13_52 ),
inference(superposition,[],[f7,f15527]) ).
fof(f15572,plain,
( ! [X0] : join(X0,complement(composition(sk2,composition(sk1,top)))) = complement(composition(sF11,complement(X0)))
| ~ spl13_11
| ~ spl13_16
| ~ spl13_17
| ~ spl13_52 ),
inference(backward_demodulation,[],[f15258,f15537]) ).
fof(f15594,plain,
( ! [X0] : complement(composition(sF11,complement(X0))) = join(X0,complement(composition(sF11,top)))
| ~ spl13_11
| ~ spl13_16
| ~ spl13_17
| ~ spl13_52 ),
inference(forward_demodulation,[],[f15572,f15537]) ).
fof(f15623,definition,
( spl13_53
<=> sk3 = join(sF12,sk3) ),
introduced(definition,[new_symbols(definition,[spl13_53])],[avatar_definition]) ).
fof(f15625,plain,
( sk3 = join(sF12,sk3)
| ~ spl13_53 ),
inference(avatar_component_clause,[],[f15623]) ).
fof(f15626,plain,
( spl13_53
| ~ spl13_4
| ~ spl13_9
| ~ spl13_11
| ~ spl13_16
| ~ spl13_17
| ~ spl13_51 ),
inference(avatar_split_clause,[],[f15514,f15389,f573,f482,f254,f181,f128,f15623]) ).
fof(f15637,plain,
( complement(sF12) = join(complement(sF12),complement(sk3))
| ~ spl13_11
| ~ spl13_53 ),
inference(superposition,[],[f2129,f15625]) ).
fof(f16924,plain,
( ! [X0] : complement(join(complement(X0),converse(complement(composition(sk1,top))))) = join(complement(join(complement(X0),converse(complement(composition(sk1,top))))),composition(X0,sk1))
| ~ spl13_11
| ~ spl13_16
| ~ spl13_29 ),
inference(superposition,[],[f539,f13620]) ).
fof(f16925,plain,
( ! [X0] : complement(join(complement(X0),converse(complement(composition(sk2,top))))) = join(complement(join(complement(X0),converse(complement(composition(sk2,top))))),composition(X0,sk2))
| ~ spl13_11
| ~ spl13_17
| ~ spl13_29 ),
inference(superposition,[],[f579,f13620]) ).
fof(f16936,plain,
( ! [X0] : complement(join(complement(X0),converse(complement(composition(sk2,top))))) = join(composition(X0,sk2),complement(join(complement(X0),converse(complement(composition(sk2,top))))))
| ~ spl13_11
| ~ spl13_17
| ~ spl13_29 ),
inference(forward_demodulation,[],[f16925,f1]) ).
fof(f16937,plain,
( ! [X0] : complement(join(complement(X0),converse(complement(composition(sk1,top))))) = join(composition(X0,sk1),complement(join(complement(X0),converse(complement(composition(sk1,top))))))
| ~ spl13_11
| ~ spl13_16
| ~ spl13_29 ),
inference(forward_demodulation,[],[f16924,f1]) ).
fof(f16981,plain,
( ! [X0] : complement(complement(composition(complement(complement(X0)),converse(sk2)))) = join(composition(X0,sk2),complement(complement(composition(complement(complement(X0)),converse(sk2)))))
| ~ spl13_11
| ~ spl13_17
| ~ spl13_29 ),
inference(forward_demodulation,[],[f16936,f13813]) ).
fof(f16982,plain,
( ! [X0] : complement(complement(composition(complement(complement(X0)),converse(sk1)))) = join(composition(X0,sk1),complement(complement(composition(complement(complement(X0)),converse(sk1)))))
| ~ spl13_11
| ~ spl13_16
| ~ spl13_29 ),
inference(forward_demodulation,[],[f16937,f13814]) ).
fof(f17004,plain,
( ! [X0] : composition(complement(complement(X0)),converse(sk2)) = join(composition(X0,sk2),composition(complement(complement(X0)),converse(sk2)))
| ~ spl13_11
| ~ spl13_17
| ~ spl13_29 ),
inference(forward_demodulation,[],[f16981,f667]) ).
fof(f17005,plain,
( ! [X0] : composition(complement(complement(X0)),converse(sk1)) = join(composition(X0,sk1),composition(complement(complement(X0)),converse(sk1)))
| ~ spl13_11
| ~ spl13_16
| ~ spl13_29 ),
inference(forward_demodulation,[],[f16982,f667]) ).
fof(f17020,plain,
( ! [X0] : composition(X0,converse(sk2)) = join(composition(X0,sk2),composition(X0,converse(sk2)))
| ~ spl13_11
| ~ spl13_17
| ~ spl13_29 ),
inference(forward_demodulation,[],[f17004,f667]) ).
fof(f17021,plain,
( ! [X0] : composition(X0,converse(sk1)) = join(composition(X0,sk1),composition(X0,converse(sk1)))
| ~ spl13_11
| ~ spl13_16
| ~ spl13_29 ),
inference(forward_demodulation,[],[f17005,f667]) ).
fof(f17030,plain,
( ! [X0] : composition(X0,converse(sk2)) = composition(X0,join(sk2,converse(sk2)))
| ~ spl13_11
| ~ spl13_17
| ~ spl13_29 ),
inference(forward_demodulation,[],[f17020,f346]) ).
fof(f17031,plain,
( ! [X0] : composition(X0,converse(sk1)) = composition(X0,join(sk1,converse(sk1)))
| ~ spl13_11
| ~ spl13_16
| ~ spl13_29 ),
inference(forward_demodulation,[],[f17021,f346]) ).
fof(f20830,plain,
( ! [X0,X1] : converse(converse(complement(X0))) = join(complement(X0),composition(complement(composition(X0,X1)),converse(X1)))
| ~ spl13_11 ),
inference(superposition,[],[f10,f13766]) ).
fof(f20861,plain,
( ! [X0,X1] : complement(X0) = join(complement(X0),composition(complement(composition(X0,X1)),converse(X1)))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f20830,f10]) ).
fof(f21231,definition,
( spl13_67
<=> complement(sF12) = join(sF3,complement(sF12)) ),
introduced(definition,[new_symbols(definition,[spl13_67])],[avatar_definition]) ).
fof(f21233,plain,
( complement(sF12) = join(sF3,complement(sF12))
| ~ spl13_67 ),
inference(avatar_component_clause,[],[f21231]) ).
fof(f21234,plain,
( spl13_67
| ~ spl13_8
| ~ spl13_11
| ~ spl13_34 ),
inference(avatar_split_clause,[],[f7506,f7479,f254,f166,f21231]) ).
fof(f21463,definition,
( spl13_68
<=> complement(sF12) = join(sF5,complement(sF12)) ),
introduced(definition,[new_symbols(definition,[spl13_68])],[avatar_definition]) ).
fof(f21465,plain,
( complement(sF12) = join(sF5,complement(sF12))
| ~ spl13_68 ),
inference(avatar_component_clause,[],[f21463]) ).
fof(f21466,plain,
( spl13_68
| ~ spl13_10
| ~ spl13_11
| ~ spl13_35 ),
inference(avatar_split_clause,[],[f8154,f8127,f254,f196,f21463]) ).
fof(f21468,plain,
( join(sF3,complement(sF12)) = join(sF6,complement(sF12))
| ~ spl13_13
| ~ spl13_68 ),
inference(superposition,[],[f269,f21465]) ).
fof(f21500,plain,
( complement(sF12) = join(sF6,complement(sF12))
| ~ spl13_13
| ~ spl13_67
| ~ spl13_68 ),
inference(forward_demodulation,[],[f21468,f21233]) ).
fof(f21863,definition,
( spl13_69
<=> top = composition(top,top) ),
introduced(definition,[new_symbols(definition,[spl13_69])],[avatar_definition]) ).
fof(f21865,plain,
( top = composition(top,top)
| ~ spl13_69 ),
inference(avatar_component_clause,[],[f21863]) ).
fof(f21866,plain,
( spl13_69
| ~ spl13_5
| ~ spl13_11
| ~ spl13_17 ),
inference(avatar_split_clause,[],[f7724,f573,f254,f139,f21863]) ).
fof(f21874,plain,
( ! [X0] : complement(join(complement(composition(complement(join(complement(top),complement(composition(X0,converse(top))))),top)),complement(X0))) = join(complement(join(complement(top),complement(X0))),complement(join(complement(composition(complement(join(complement(top),complement(composition(X0,converse(top))))),top)),complement(X0))))
| ~ spl13_69 ),
inference(superposition,[],[f31,f21865]) ).
fof(f21886,plain,
( complement(top) = join(complement(top),composition(complement(top),converse(top)))
| ~ spl13_11
| ~ spl13_69 ),
inference(superposition,[],[f20861,f21865]) ).
fof(f21887,plain,
( complement(top) = composition(complement(top),join(sF0,converse(top)))
| ~ spl13_11
| ~ spl13_69 ),
inference(forward_demodulation,[],[f21886,f394]) ).
fof(f21899,plain,
( ! [X0] : complement(join(complement(X0),complement(composition(complement(join(complement(top),complement(composition(X0,converse(top))))),top)))) = join(complement(join(complement(top),complement(X0))),complement(join(complement(X0),complement(composition(complement(join(complement(top),complement(composition(X0,converse(top))))),top)))))
| ~ spl13_11
| ~ spl13_69 ),
inference(forward_demodulation,[],[f21874,f2134]) ).
fof(f21906,plain,
( complement(top) = composition(complement(top),converse(join(sF0,top)))
| ~ spl13_11
| ~ spl13_33
| ~ spl13_69 ),
inference(forward_demodulation,[],[f21887,f7393]) ).
fof(f21915,plain,
( ! [X0] : complement(join(complement(X0),complement(composition(complement(join(complement(top),complement(composition(X0,top)))),top)))) = join(complement(join(complement(top),complement(X0))),complement(join(complement(X0),complement(composition(complement(join(complement(top),complement(composition(X0,top)))),top)))))
| ~ spl13_11
| ~ spl13_29
| ~ spl13_69 ),
inference(forward_demodulation,[],[f21899,f6881]) ).
fof(f21922,plain,
( complement(top) = composition(complement(top),converse(join(top,sF0)))
| ~ spl13_11
| ~ spl13_33
| ~ spl13_69 ),
inference(forward_demodulation,[],[f21906,f1]) ).
fof(f21929,plain,
( ! [X0] : complement(join(complement(X0),complement(composition(complement(join(zero,complement(composition(X0,top)))),top)))) = join(complement(join(zero,complement(X0))),complement(join(complement(X0),complement(composition(complement(join(zero,complement(composition(X0,top)))),top)))))
| ~ spl13_11
| ~ spl13_29
| ~ spl13_69 ),
inference(forward_demodulation,[],[f21915,f256]) ).
fof(f21934,plain,
( complement(top) = composition(complement(top),converse(top))
| ~ spl13_11
| ~ spl13_33
| ~ spl13_69 ),
inference(forward_demodulation,[],[f21922,f1665]) ).
fof(f21938,plain,
( ! [X0] : complement(join(complement(X0),complement(composition(complement(complement(composition(X0,top))),top)))) = join(complement(join(zero,complement(X0))),complement(join(complement(X0),complement(composition(complement(complement(composition(X0,top))),top)))))
| ~ spl13_11
| ~ spl13_29
| ~ spl13_69 ),
inference(forward_demodulation,[],[f21929,f1577]) ).
fof(f21942,plain,
( complement(top) = composition(complement(top),top)
| ~ spl13_11
| ~ spl13_29
| ~ spl13_33
| ~ spl13_69 ),
inference(forward_demodulation,[],[f21934,f6881]) ).
fof(f21943,plain,
( ! [X0] : complement(join(complement(X0),complement(composition(composition(X0,top),top)))) = join(complement(join(zero,complement(X0))),complement(join(complement(X0),complement(composition(composition(X0,top),top)))))
| ~ spl13_11
| ~ spl13_29
| ~ spl13_69 ),
inference(forward_demodulation,[],[f21938,f667]) ).
fof(f21947,plain,
( zero = composition(zero,top)
| ~ spl13_11
| ~ spl13_29
| ~ spl13_33
| ~ spl13_69 ),
inference(forward_demodulation,[],[f21942,f256]) ).
fof(f21948,plain,
( ! [X0] : complement(join(complement(X0),complement(composition(X0,composition(top,top))))) = join(complement(join(zero,complement(X0))),complement(join(complement(X0),complement(composition(X0,composition(top,top))))))
| ~ spl13_11
| ~ spl13_29
| ~ spl13_69 ),
inference(forward_demodulation,[],[f21943,f7]) ).
fof(f21952,plain,
( ! [X0] : composition(zero,X0) = composition(zero,complement(join(complement(X0),complement(zero))))
| ~ spl13_11
| ~ spl13_29
| ~ spl13_33
| ~ spl13_36
| ~ spl13_69 ),
inference(backward_demodulation,[],[f13084,f21947]) ).
fof(f21954,plain,
( ! [X0] : complement(join(complement(X0),complement(composition(X0,top)))) = join(complement(join(zero,complement(X0))),complement(join(complement(X0),complement(composition(X0,top)))))
| ~ spl13_11
| ~ spl13_29
| ~ spl13_69 ),
inference(forward_demodulation,[],[f21948,f21865]) ).
fof(f21958,plain,
( ! [X0] : composition(zero,X0) = composition(zero,complement(join(complement(X0),top)))
| ~ spl13_11
| ~ spl13_28
| ~ spl13_29
| ~ spl13_33
| ~ spl13_36
| ~ spl13_69 ),
inference(forward_demodulation,[],[f21952,f6658]) ).
fof(f21959,plain,
( ! [X0] : complement(join(complement(X0),complement(composition(X0,top)))) = join(complement(complement(X0)),complement(join(complement(X0),complement(composition(X0,top)))))
| ~ spl13_11
| ~ spl13_29
| ~ spl13_69 ),
inference(forward_demodulation,[],[f21954,f1577]) ).
fof(f21962,plain,
( ! [X0] : composition(zero,X0) = composition(zero,complement(join(top,complement(X0))))
| ~ spl13_11
| ~ spl13_28
| ~ spl13_29
| ~ spl13_33
| ~ spl13_36
| ~ spl13_69 ),
inference(forward_demodulation,[],[f21958,f2134]) ).
fof(f21963,plain,
( ! [X0] : complement(complement(X0)) = complement(join(complement(X0),complement(composition(X0,top))))
| ~ spl13_11
| ~ spl13_29
| ~ spl13_69 ),
inference(forward_demodulation,[],[f21959,f2129]) ).
fof(f21965,plain,
( ! [X0] : composition(zero,X0) = composition(zero,complement(top))
| ~ spl13_11
| ~ spl13_28
| ~ spl13_29
| ~ spl13_33
| ~ spl13_36
| ~ spl13_69 ),
inference(forward_demodulation,[],[f21962,f1665]) ).
fof(f21966,plain,
( ! [X0] : complement(join(complement(X0),complement(composition(X0,top)))) = X0
| ~ spl13_11
| ~ spl13_29
| ~ spl13_69 ),
inference(forward_demodulation,[],[f21963,f667]) ).
fof(f21968,plain,
( ! [X0] : composition(zero,X0) = composition(zero,zero)
| ~ spl13_11
| ~ spl13_28
| ~ spl13_29
| ~ spl13_33
| ~ spl13_36
| ~ spl13_69 ),
inference(forward_demodulation,[],[f21965,f256]) ).
fof(f23508,definition,
( spl13_79
<=> sF3 = join(sF3,complement(sk3)) ),
introduced(definition,[new_symbols(definition,[spl13_79])],[avatar_definition]) ).
fof(f23510,plain,
( sF3 = join(sF3,complement(sk3))
| ~ spl13_79 ),
inference(avatar_component_clause,[],[f23508]) ).
fof(f23511,plain,
( spl13_79
| ~ spl13_8
| ~ spl13_11
| ~ spl13_20 ),
inference(avatar_split_clause,[],[f2857,f2845,f254,f166,f23508]) ).
fof(f23517,plain,
( ! [X0] : join(X0,sF3) = join(sF3,join(complement(sk3),X0))
| ~ spl13_79 ),
inference(superposition,[],[f219,f23510]) ).
fof(f23926,plain,
( ! [X0] : join(complement(X0),X0) = join(complement(X0),complement(complement(composition(X0,top))))
| ~ spl13_11
| ~ spl13_29
| ~ spl13_69 ),
inference(superposition,[],[f2152,f21966]) ).
fof(f24005,plain,
( ! [X0] : join(complement(X0),X0) = join(complement(X0),composition(X0,top))
| ~ spl13_11
| ~ spl13_29
| ~ spl13_69 ),
inference(forward_demodulation,[],[f23926,f667]) ).
fof(f24058,plain,
( ! [X0] : join(X0,complement(X0)) = join(complement(X0),composition(X0,top))
| ~ spl13_11
| ~ spl13_29
| ~ spl13_69 ),
inference(forward_demodulation,[],[f24005,f1]) ).
fof(f24083,plain,
( ! [X0] : top = join(complement(X0),composition(X0,top))
| ~ spl13_11
| ~ spl13_29
| ~ spl13_69 ),
inference(forward_demodulation,[],[f24058,f15]) ).
fof(f24097,plain,
( complement(top) = composition(complement(top),zero)
| ~ spl13_11
| ~ spl13_28
| ~ spl13_29
| ~ spl13_69 ),
inference(backward_demodulation,[],[f11898,f24083]) ).
fof(f24104,plain,
( zero = composition(zero,zero)
| ~ spl13_11
| ~ spl13_28
| ~ spl13_29
| ~ spl13_69 ),
inference(forward_demodulation,[],[f24097,f256]) ).
fof(f24108,plain,
( ! [X0] : zero = composition(zero,X0)
| ~ spl13_11
| ~ spl13_28
| ~ spl13_29
| ~ spl13_33
| ~ spl13_36
| ~ spl13_69 ),
inference(backward_demodulation,[],[f21968,f24104]) ).
fof(f24118,plain,
( ! [X0,X1] : converse(composition(zero,join(converse(X1),X0))) = join(converse(zero),composition(X1,zero))
| ~ spl13_11
| ~ spl13_28
| ~ spl13_29
| ~ spl13_33
| ~ spl13_36
| ~ spl13_69 ),
inference(backward_demodulation,[],[f8288,f24108]) ).
fof(f24132,plain,
( ! [X0,X1] : converse(composition(zero,join(converse(X1),X0))) = join(zero,composition(X1,zero))
| ~ spl13_11
| ~ spl13_28
| ~ spl13_29
| ~ spl13_33
| ~ spl13_36
| ~ spl13_69 ),
inference(forward_demodulation,[],[f24118,f8270]) ).
fof(f24142,plain,
( ! [X0,X1] : composition(X1,zero) = converse(composition(zero,join(converse(X1),X0)))
| ~ spl13_11
| ~ spl13_28
| ~ spl13_29
| ~ spl13_33
| ~ spl13_36
| ~ spl13_69 ),
inference(forward_demodulation,[],[f24132,f1577]) ).
fof(f24147,plain,
( ! [X1] : converse(zero) = composition(X1,zero)
| ~ spl13_11
| ~ spl13_28
| ~ spl13_29
| ~ spl13_33
| ~ spl13_36
| ~ spl13_69 ),
inference(forward_demodulation,[],[f24142,f24108]) ).
fof(f24151,plain,
( ! [X1] : zero = composition(X1,zero)
| ~ spl13_11
| ~ spl13_28
| ~ spl13_29
| ~ spl13_33
| ~ spl13_36
| ~ spl13_69 ),
inference(forward_demodulation,[],[f24147,f8270]) ).
fof(f24169,plain,
( ! [X0,X1] : zero = join(complement(join(complement(composition(X0,X1)),composition(X0,top))),zero)
| ~ spl13_11
| ~ spl13_28
| ~ spl13_29
| ~ spl13_33
| ~ spl13_36
| ~ spl13_69 ),
inference(backward_demodulation,[],[f5113,f24151]) ).
fof(f24172,plain,
( ! [X0,X1] : zero = join(zero,complement(join(complement(composition(X0,X1)),composition(X0,top))))
| ~ spl13_11
| ~ spl13_28
| ~ spl13_29
| ~ spl13_33
| ~ spl13_36
| ~ spl13_69 ),
inference(forward_demodulation,[],[f24169,f1]) ).
fof(f24181,plain,
( ! [X0,X1] : zero = complement(join(complement(composition(X0,X1)),composition(X0,top)))
| ~ spl13_11
| ~ spl13_28
| ~ spl13_29
| ~ spl13_33
| ~ spl13_36
| ~ spl13_69 ),
inference(forward_demodulation,[],[f24172,f1577]) ).
fof(f24596,plain,
( ! [X0,X1] : complement(complement(composition(X0,X1))) = join(zero,complement(join(complement(composition(X0,top)),complement(composition(X0,X1)))))
| ~ spl13_11
| ~ spl13_28
| ~ spl13_29
| ~ spl13_33
| ~ spl13_36
| ~ spl13_69 ),
inference(superposition,[],[f688,f24181]) ).
fof(f24686,plain,
( ! [X0,X1] : complement(complement(composition(X0,X1))) = complement(join(complement(composition(X0,top)),complement(composition(X0,X1))))
| ~ spl13_11
| ~ spl13_28
| ~ spl13_29
| ~ spl13_33
| ~ spl13_36
| ~ spl13_69 ),
inference(forward_demodulation,[],[f24596,f1577]) ).
fof(f24755,plain,
( ! [X0,X1] : composition(X0,X1) = complement(join(complement(composition(X0,top)),complement(composition(X0,X1))))
| ~ spl13_11
| ~ spl13_28
| ~ spl13_29
| ~ spl13_33
| ~ spl13_36
| ~ spl13_69 ),
inference(forward_demodulation,[],[f24686,f667]) ).
fof(f27083,plain,
( sF12 = complement(join(complement(composition(sF11,top)),complement(sF12)))
| ~ spl13_4
| ~ spl13_11
| ~ spl13_28
| ~ spl13_29
| ~ spl13_33
| ~ spl13_36
| ~ spl13_69 ),
inference(superposition,[],[f24755,f130]) ).
fof(f27256,plain,
( sF12 = complement(join(complement(sF12),complement(composition(sF11,top))))
| ~ spl13_4
| ~ spl13_11
| ~ spl13_28
| ~ spl13_29
| ~ spl13_33
| ~ spl13_36
| ~ spl13_69 ),
inference(forward_demodulation,[],[f27083,f2134]) ).
fof(f27333,plain,
( sF12 = complement(complement(composition(sF11,complement(complement(sF12)))))
| ~ spl13_4
| ~ spl13_11
| ~ spl13_16
| ~ spl13_17
| ~ spl13_28
| ~ spl13_29
| ~ spl13_33
| ~ spl13_36
| ~ spl13_52
| ~ spl13_69 ),
inference(forward_demodulation,[],[f27256,f15594]) ).
fof(f27381,plain,
( sF12 = composition(sF11,complement(complement(sF12)))
| ~ spl13_4
| ~ spl13_11
| ~ spl13_16
| ~ spl13_17
| ~ spl13_28
| ~ spl13_29
| ~ spl13_33
| ~ spl13_36
| ~ spl13_52
| ~ spl13_69 ),
inference(forward_demodulation,[],[f27333,f667]) ).
fof(f27412,plain,
( sF12 = composition(sF11,sF12)
| ~ spl13_4
| ~ spl13_11
| ~ spl13_16
| ~ spl13_17
| ~ spl13_28
| ~ spl13_29
| ~ spl13_33
| ~ spl13_36
| ~ spl13_52
| ~ spl13_69 ),
inference(forward_demodulation,[],[f27381,f667]) ).
fof(f27426,definition,
( spl13_89
<=> sF12 = composition(sF11,sF12) ),
introduced(definition,[new_symbols(definition,[spl13_89])],[avatar_definition]) ).
fof(f27428,plain,
( sF12 = composition(sF11,sF12)
| ~ spl13_89 ),
inference(avatar_component_clause,[],[f27426]) ).
fof(f27429,plain,
( spl13_89
| ~ spl13_4
| ~ spl13_11
| ~ spl13_16
| ~ spl13_17
| ~ spl13_28
| ~ spl13_29
| ~ spl13_33
| ~ spl13_36
| ~ spl13_52
| ~ spl13_69 ),
inference(avatar_split_clause,[],[f27412,f21863,f15525,f8268,f7379,f6879,f6656,f573,f482,f254,f128,f27426]) ).
fof(f27434,plain,
( ! [X0] : composition(join(sF11,X0),sF12) = join(sF12,composition(X0,sF12))
| ~ spl13_89 ),
inference(superposition,[],[f9,f27428]) ).
fof(f27440,plain,
( ! [X0] : join(sF12,composition(sF11,X0)) = composition(sF11,join(sF12,X0))
| ~ spl13_89 ),
inference(superposition,[],[f346,f27428]) ).
fof(f27441,plain,
( ! [X0] : join(composition(sF11,X0),sF12) = composition(sF11,join(X0,sF12))
| ~ spl13_89 ),
inference(superposition,[],[f346,f27428]) ).
fof(f27459,plain,
( ! [X0] : join(sF12,composition(sF11,X0)) = composition(sF11,join(X0,sF12))
| ~ spl13_89 ),
inference(forward_demodulation,[],[f27441,f1]) ).
fof(f27460,plain,
( ! [X0] : composition(sF11,join(sk3,X0)) = composition(sF11,join(sF12,X0))
| ~ spl13_4
| ~ spl13_89 ),
inference(forward_demodulation,[],[f27440,f368]) ).
fof(f27465,plain,
( ! [X0] : composition(join(sF11,X0),sF12) = composition(join(sF0,X0),sF12)
| ~ spl13_89 ),
inference(forward_demodulation,[],[f27434,f1437]) ).
fof(f27471,plain,
( ! [X0] : composition(sF11,join(sk3,X0)) = composition(sF11,join(X0,sF12))
| ~ spl13_4
| ~ spl13_89 ),
inference(forward_demodulation,[],[f27459,f368]) ).
fof(f27489,plain,
( ! [X0] : composition(sF11,join(sF12,X0)) = composition(sF11,join(X0,sF12))
| ~ spl13_4
| ~ spl13_89 ),
inference(forward_demodulation,[],[f27471,f27460]) ).
fof(f28156,plain,
( composition(sk1,sF0) = join(sk1,converse(sk1))
| ~ spl13_11
| ~ spl13_16 ),
inference(superposition,[],[f68,f8757]) ).
fof(f28159,plain,
( sk1 = join(sk1,converse(sk1))
| ~ spl13_11
| ~ spl13_16 ),
inference(forward_demodulation,[],[f28156,f68]) ).
fof(f28203,plain,
( ! [X0] : composition(X0,sk1) = composition(X0,converse(sk1))
| ~ spl13_11
| ~ spl13_16
| ~ spl13_29 ),
inference(backward_demodulation,[],[f17031,f28159]) ).
fof(f28403,plain,
( converse(sk1) = composition(sF0,sk1)
| ~ spl13_11
| ~ spl13_16
| ~ spl13_29 ),
inference(superposition,[],[f1425,f28203]) ).
fof(f28414,plain,
( sk1 = converse(sk1)
| ~ spl13_11
| ~ spl13_16
| ~ spl13_29 ),
inference(forward_demodulation,[],[f28403,f1425]) ).
fof(f28519,plain,
( ! [X0] : composition(sk1,complement(join(complement(X0),join(complement(sk3),complement(composition(sk1,X0)))))) = join(complement(join(sF3,complement(X0))),composition(sk1,complement(join(complement(X0),join(complement(sk3),complement(composition(sk1,X0)))))))
| ~ spl13_8
| ~ spl13_11
| ~ spl13_14
| ~ spl13_16
| ~ spl13_29 ),
inference(backward_demodulation,[],[f8893,f28414]) ).
fof(f28657,plain,
( ! [X0] : composition(sk1,complement(join(complement(sk3),complement(composition(sk1,X0))))) = join(complement(join(sF3,complement(X0))),composition(sk1,complement(join(complement(sk3),complement(composition(sk1,X0))))))
| ~ spl13_8
| ~ spl13_11
| ~ spl13_14
| ~ spl13_16
| ~ spl13_29 ),
inference(forward_demodulation,[],[f28519,f14271]) ).
fof(f28713,plain,
( ! [X0] : complement(join(complement(sk3),complement(composition(sk1,composition(sk1,X0))))) = join(complement(join(sF3,complement(X0))),complement(join(complement(sk3),complement(composition(sk1,composition(sk1,X0))))))
| ~ spl13_8
| ~ spl13_11
| ~ spl13_14
| ~ spl13_16
| ~ spl13_29 ),
inference(forward_demodulation,[],[f28657,f14090]) ).
fof(f28741,plain,
( ! [X0] : complement(join(complement(sk3),complement(composition(sk1,X0)))) = join(complement(join(sF3,complement(X0))),complement(join(complement(sk3),complement(composition(sk1,X0)))))
| ~ spl13_8
| ~ spl13_11
| ~ spl13_14
| ~ spl13_16
| ~ spl13_29 ),
inference(forward_demodulation,[],[f28713,f9194]) ).
fof(f28918,plain,
( complement(join(complement(sk3),complement(composition(sk1,sF4)))) = join(complement(join(sF3,sF5)),complement(join(complement(sk3),complement(composition(sk1,sF4)))))
| ~ spl13_8
| ~ spl13_10
| ~ spl13_11
| ~ spl13_14
| ~ spl13_16
| ~ spl13_29 ),
inference(superposition,[],[f28741,f198]) ).
fof(f28958,plain,
( ! [X0] : join(sF3,complement(X0)) = join(join(sF3,complement(X0)),complement(complement(join(complement(sk3),complement(composition(sk1,X0))))))
| ~ spl13_8
| ~ spl13_11
| ~ spl13_14
| ~ spl13_16
| ~ spl13_29 ),
inference(superposition,[],[f2178,f28741]) ).
fof(f28994,plain,
( ! [X0] : join(sF3,complement(X0)) = join(sF3,join(complement(X0),complement(complement(join(complement(sk3),complement(composition(sk1,X0)))))))
| ~ spl13_8
| ~ spl13_11
| ~ spl13_14
| ~ spl13_16
| ~ spl13_29 ),
inference(forward_demodulation,[],[f28958,f2]) ).
fof(f29024,plain,
( complement(join(complement(sk3),complement(composition(sk1,sF4)))) = join(complement(sF6),complement(join(complement(sk3),complement(composition(sk1,sF4)))))
| ~ spl13_8
| ~ spl13_10
| ~ spl13_11
| ~ spl13_13
| ~ spl13_14
| ~ spl13_16
| ~ spl13_29 ),
inference(forward_demodulation,[],[f28918,f267]) ).
fof(f29045,plain,
( ! [X0] : join(sF3,complement(X0)) = join(sF3,join(complement(X0),join(complement(sk3),complement(composition(sk1,X0)))))
| ~ spl13_8
| ~ spl13_11
| ~ spl13_14
| ~ spl13_16
| ~ spl13_29 ),
inference(forward_demodulation,[],[f28994,f667]) ).
fof(f29067,plain,
( complement(join(complement(sk3),complement(composition(sk1,sF4)))) = join(sF7,complement(join(complement(sk3),complement(composition(sk1,sF4)))))
| ~ spl13_2
| ~ spl13_8
| ~ spl13_10
| ~ spl13_11
| ~ spl13_13
| ~ spl13_14
| ~ spl13_16
| ~ spl13_29 ),
inference(forward_demodulation,[],[f29024,f107]) ).
fof(f29085,plain,
( ! [X0] : join(sF3,complement(X0)) = join(sF3,join(complement(sk3),complement(composition(sk1,X0))))
| ~ spl13_8
| ~ spl13_11
| ~ spl13_14
| ~ spl13_16
| ~ spl13_29 ),
inference(forward_demodulation,[],[f29045,f14271]) ).
fof(f29114,plain,
( ! [X0] : join(sF3,complement(X0)) = join(complement(composition(sk1,X0)),sF3)
| ~ spl13_8
| ~ spl13_11
| ~ spl13_14
| ~ spl13_16
| ~ spl13_29
| ~ spl13_79 ),
inference(forward_demodulation,[],[f29085,f23517]) ).
fof(f29134,plain,
( ! [X0] : join(sF3,complement(X0)) = join(sF3,complement(composition(sk1,X0)))
| ~ spl13_8
| ~ spl13_11
| ~ spl13_14
| ~ spl13_16
| ~ spl13_29
| ~ spl13_79 ),
inference(forward_demodulation,[],[f29114,f1]) ).
fof(f29156,plain,
( complement(composition(sk1,sF7)) = join(sF3,complement(sF4))
| ~ spl13_2
| ~ spl13_8
| ~ spl13_11
| ~ spl13_13
| ~ spl13_14
| ~ spl13_16
| ~ spl13_24
| ~ spl13_29
| ~ spl13_79 ),
inference(backward_demodulation,[],[f8884,f29134]) ).
fof(f29171,plain,
( join(sF3,sF5) = complement(composition(sk1,sF7))
| ~ spl13_2
| ~ spl13_8
| ~ spl13_10
| ~ spl13_11
| ~ spl13_13
| ~ spl13_14
| ~ spl13_16
| ~ spl13_24
| ~ spl13_29
| ~ spl13_79 ),
inference(forward_demodulation,[],[f29156,f198]) ).
fof(f29187,plain,
( sF6 = complement(composition(sk1,sF7))
| ~ spl13_2
| ~ spl13_8
| ~ spl13_10
| ~ spl13_11
| ~ spl13_13
| ~ spl13_14
| ~ spl13_16
| ~ spl13_24
| ~ spl13_29
| ~ spl13_79 ),
inference(forward_demodulation,[],[f29171,f267]) ).
fof(f29202,plain,
( sF6 = join(sF6,complement(composition(sk1,sF4)))
| ~ spl13_2
| ~ spl13_8
| ~ spl13_10
| ~ spl13_11
| ~ spl13_13
| ~ spl13_14
| ~ spl13_16
| ~ spl13_24
| ~ spl13_29
| ~ spl13_79 ),
inference(backward_demodulation,[],[f8904,f29187]) ).
fof(f29712,definition,
( spl13_98
<=> complement(join(complement(sk3),complement(composition(sk1,sF4)))) = join(sF7,complement(join(complement(sk3),complement(composition(sk1,sF4))))) ),
introduced(definition,[new_symbols(definition,[spl13_98])],[avatar_definition]) ).
fof(f29714,plain,
( complement(join(complement(sk3),complement(composition(sk1,sF4)))) = join(sF7,complement(join(complement(sk3),complement(composition(sk1,sF4)))))
| ~ spl13_98 ),
inference(avatar_component_clause,[],[f29712]) ).
fof(f29715,plain,
( spl13_98
| ~ spl13_2
| ~ spl13_8
| ~ spl13_10
| ~ spl13_11
| ~ spl13_13
| ~ spl13_14
| ~ spl13_16
| ~ spl13_29 ),
inference(avatar_split_clause,[],[f29067,f6879,f482,f271,f265,f254,f196,f166,f105,f29712]) ).
fof(f31014,plain,
( ! [X0] : join(X0,complement(composition(sk1,sF2))) = complement(composition(sk1,complement(join(sF3,X0))))
| ~ spl13_8
| ~ spl13_11
| ~ spl13_16 ),
inference(superposition,[],[f14054,f168]) ).
fof(f31349,plain,
( ! [X0] : join(X0,complement(sF2)) = complement(composition(sk1,complement(join(sF3,X0))))
| ~ spl13_8
| ~ spl13_11
| ~ spl13_16
| ~ spl13_22
| ~ spl13_40 ),
inference(forward_demodulation,[],[f31014,f9391]) ).
fof(f31482,plain,
( ! [X0] : join(X0,sF3) = complement(composition(sk1,complement(join(sF3,X0))))
| ~ spl13_8
| ~ spl13_11
| ~ spl13_16
| ~ spl13_22
| ~ spl13_40 ),
inference(forward_demodulation,[],[f31349,f168]) ).
fof(f32919,plain,
( join(complement(sF12),sF3) = complement(composition(sk1,complement(complement(sF12))))
| ~ spl13_8
| ~ spl13_11
| ~ spl13_16
| ~ spl13_22
| ~ spl13_40
| ~ spl13_67 ),
inference(superposition,[],[f31482,f21233]) ).
fof(f33170,plain,
( join(complement(sF12),sF3) = complement(composition(sk1,sF12))
| ~ spl13_8
| ~ spl13_11
| ~ spl13_16
| ~ spl13_22
| ~ spl13_40
| ~ spl13_67 ),
inference(forward_demodulation,[],[f32919,f667]) ).
fof(f33286,plain,
( join(sF3,complement(sF12)) = complement(composition(sk1,sF12))
| ~ spl13_8
| ~ spl13_11
| ~ spl13_16
| ~ spl13_22
| ~ spl13_40
| ~ spl13_67 ),
inference(forward_demodulation,[],[f33170,f1]) ).
fof(f33372,plain,
( complement(sF12) = complement(composition(sk1,sF12))
| ~ spl13_8
| ~ spl13_11
| ~ spl13_16
| ~ spl13_22
| ~ spl13_40
| ~ spl13_67 ),
inference(forward_demodulation,[],[f33286,f21233]) ).
fof(f33594,plain,
! [X2,X3,X0,X1] : join(composition(join(X3,X1),X2),X0) = join(composition(X3,X2),join(X0,composition(X1,X2))),
inference(superposition,[],[f214,f1]) ).
fof(f33607,plain,
! [X2,X0,X1] : join(composition(X0,X1),top) = join(composition(join(X0,X2),X1),complement(composition(X2,X1))),
inference(superposition,[],[f214,f15]) ).
fof(f33782,plain,
( ! [X2,X0,X1] : top = join(composition(join(X0,X2),X1),complement(composition(X2,X1)))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f33607,f1667]) ).
fof(f33793,plain,
! [X2,X3,X0,X1] : join(composition(join(X3,X1),X2),X0) = join(X0,composition(join(X1,X3),X2)),
inference(forward_demodulation,[],[f33594,f3312]) ).
fof(f34272,plain,
( ! [X2,X0,X1] : join(composition(join(X0,X1),X2),complement(complement(composition(X1,X2)))) = join(composition(join(X0,X1),X2),complement(top))
| ~ spl13_11 ),
inference(superposition,[],[f2152,f33782]) ).
fof(f34284,plain,
( ! [X2,X0,X1] : join(composition(join(X0,X1),X2),complement(complement(composition(X1,X2)))) = join(composition(join(X0,X1),X2),zero)
| ~ spl13_11 ),
inference(forward_demodulation,[],[f34272,f256]) ).
fof(f34413,plain,
( ! [X2,X0,X1] : composition(join(X0,X1),X2) = join(composition(join(X0,X1),X2),complement(complement(composition(X1,X2))))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f34284,f1700]) ).
fof(f34476,plain,
( ! [X2,X0,X1] : composition(join(X0,X1),X2) = join(composition(join(X0,X1),X2),composition(X1,X2))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f34413,f667]) ).
fof(f34505,plain,
( ! [X2,X0,X1] : composition(join(X0,X1),X2) = join(composition(X1,X2),composition(join(X1,X0),X2))
| ~ spl13_11 ),
inference(forward_demodulation,[],[f34476,f33793]) ).
fof(f34513,plain,
( ! [X2,X0,X1] : composition(join(X0,X1),X2) = composition(join(X1,join(X1,X0)),X2)
| ~ spl13_11 ),
inference(forward_demodulation,[],[f34505,f9]) ).
fof(f34517,plain,
( ! [X2,X0,X1] : composition(join(X0,X1),X2) = composition(join(X1,X0),X2)
| ~ spl13_11 ),
inference(forward_demodulation,[],[f34513,f1631]) ).
fof(f35545,plain,
( composition(sk2,sF0) = join(sk2,converse(sk2))
| ~ spl13_11
| ~ spl13_17 ),
inference(superposition,[],[f68,f9853]) ).
fof(f35548,plain,
( sk2 = join(sk2,converse(sk2))
| ~ spl13_11
| ~ spl13_17 ),
inference(forward_demodulation,[],[f35545,f68]) ).
fof(f35598,plain,
( ! [X0] : composition(X0,sk2) = composition(X0,converse(sk2))
| ~ spl13_11
| ~ spl13_17
| ~ spl13_29 ),
inference(backward_demodulation,[],[f17030,f35548]) ).
fof(f35806,plain,
( converse(sk2) = composition(sF0,sk2)
| ~ spl13_11
| ~ spl13_17
| ~ spl13_29 ),
inference(superposition,[],[f1425,f35598]) ).
fof(f35818,plain,
( sk2 = converse(sk2)
| ~ spl13_11
| ~ spl13_17
| ~ spl13_29 ),
inference(forward_demodulation,[],[f35806,f1425]) ).
fof(f35930,plain,
( ! [X0] : composition(sk2,complement(join(complement(X0),join(complement(sk3),complement(composition(sk2,X0)))))) = join(complement(join(sF5,complement(X0))),composition(sk2,complement(join(complement(X0),join(complement(sk3),complement(composition(sk2,X0)))))))
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_17
| ~ spl13_29 ),
inference(backward_demodulation,[],[f10034,f35818]) ).
fof(f36116,plain,
( ! [X0] : composition(sk2,complement(join(complement(sk3),complement(composition(sk2,X0))))) = join(complement(join(sF5,complement(X0))),composition(sk2,complement(join(complement(sk3),complement(composition(sk2,X0))))))
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_17
| ~ spl13_29 ),
inference(forward_demodulation,[],[f35930,f15368]) ).
fof(f36178,plain,
( ! [X0] : complement(join(complement(sk3),complement(composition(sk2,composition(sk2,X0))))) = join(complement(join(sF5,complement(X0))),complement(join(complement(sk3),complement(composition(sk2,composition(sk2,X0))))))
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_17
| ~ spl13_29 ),
inference(forward_demodulation,[],[f36116,f15165]) ).
fof(f36213,plain,
( ! [X0] : complement(join(complement(sk3),complement(composition(sk2,X0)))) = join(complement(join(sF5,complement(X0))),complement(join(complement(sk3),complement(composition(sk2,X0)))))
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_17
| ~ spl13_29 ),
inference(forward_demodulation,[],[f36178,f10373]) ).
fof(f36499,plain,
( complement(join(complement(sk3),complement(composition(sk2,composition(sk1,top))))) = join(complement(complement(composition(sk1,complement(sF5)))),complement(join(complement(sk3),complement(composition(sk2,composition(sk1,top))))))
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_29 ),
inference(superposition,[],[f36213,f8687]) ).
fof(f36501,plain,
( complement(join(complement(sk3),complement(composition(sk2,composition(sF11,top))))) = join(complement(complement(composition(sF11,complement(sF5)))),complement(join(complement(sk3),complement(composition(sk2,composition(sF11,top))))))
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_29
| ~ spl13_52 ),
inference(superposition,[],[f36213,f15594]) ).
fof(f36576,plain,
( complement(join(complement(sk3),complement(composition(sF11,top)))) = join(complement(complement(composition(sF11,complement(sF5)))),complement(join(complement(sk3),complement(composition(sF11,top)))))
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_29
| ~ spl13_46
| ~ spl13_52 ),
inference(forward_demodulation,[],[f36501,f10934]) ).
fof(f36578,plain,
( complement(join(complement(sk3),complement(composition(sF11,top)))) = join(complement(complement(composition(sk1,complement(sF5)))),complement(join(complement(sk3),complement(composition(sF11,top)))))
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_29
| ~ spl13_52 ),
inference(forward_demodulation,[],[f36499,f15537]) ).
fof(f36628,plain,
( complement(complement(composition(sF11,complement(complement(sk3))))) = join(complement(complement(composition(sF11,complement(sF5)))),complement(complement(composition(sF11,complement(complement(sk3))))))
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_29
| ~ spl13_46
| ~ spl13_52 ),
inference(forward_demodulation,[],[f36576,f15594]) ).
fof(f36630,plain,
( complement(complement(composition(sF11,complement(complement(sk3))))) = join(complement(complement(composition(sk1,complement(sF5)))),complement(complement(composition(sF11,complement(complement(sk3))))))
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_29
| ~ spl13_52 ),
inference(forward_demodulation,[],[f36578,f15594]) ).
fof(f36670,plain,
( composition(sF11,complement(complement(sk3))) = join(complement(complement(composition(sF11,complement(sF5)))),composition(sF11,complement(complement(sk3))))
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_29
| ~ spl13_46
| ~ spl13_52 ),
inference(forward_demodulation,[],[f36628,f667]) ).
fof(f36672,plain,
( composition(sF11,complement(complement(sk3))) = join(complement(complement(composition(sk1,complement(sF5)))),composition(sF11,complement(complement(sk3))))
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_29
| ~ spl13_52 ),
inference(forward_demodulation,[],[f36630,f667]) ).
fof(f36700,plain,
( composition(sF11,complement(complement(sk3))) = join(composition(sF11,complement(complement(sk3))),complement(complement(composition(sF11,complement(sF5)))))
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_29
| ~ spl13_46
| ~ spl13_52 ),
inference(forward_demodulation,[],[f36670,f1]) ).
fof(f36702,plain,
( composition(sF11,complement(complement(sk3))) = join(composition(sF11,complement(complement(sk3))),complement(complement(composition(sk1,complement(sF5)))))
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_29
| ~ spl13_52 ),
inference(forward_demodulation,[],[f36672,f1]) ).
fof(f36722,plain,
( composition(sF11,complement(complement(sk3))) = join(composition(sF11,complement(complement(sk3))),composition(sF11,complement(sF5)))
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_29
| ~ spl13_46
| ~ spl13_52 ),
inference(forward_demodulation,[],[f36700,f667]) ).
fof(f36724,plain,
( composition(sF11,complement(complement(sk3))) = join(composition(sF11,complement(complement(sk3))),composition(sk1,complement(sF5)))
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_29
| ~ spl13_52 ),
inference(forward_demodulation,[],[f36702,f667]) ).
fof(f36741,plain,
( composition(sF11,complement(complement(sk3))) = composition(sF11,join(complement(complement(sk3)),complement(sF5)))
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_29
| ~ spl13_46
| ~ spl13_52 ),
inference(forward_demodulation,[],[f36722,f346]) ).
fof(f36743,plain,
( composition(sF11,complement(complement(sk3))) = join(composition(sk1,complement(sF5)),composition(sF11,complement(complement(sk3))))
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_29
| ~ spl13_52 ),
inference(forward_demodulation,[],[f36724,f1]) ).
fof(f36756,plain,
( composition(sF11,complement(complement(sk3))) = composition(sF11,join(complement(sF5),complement(complement(sk3))))
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_29
| ~ spl13_46
| ~ spl13_52 ),
inference(forward_demodulation,[],[f36741,f1]) ).
fof(f36758,plain,
( composition(sF11,sk3) = join(composition(sk1,complement(sF5)),composition(sF11,sk3))
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_29
| ~ spl13_52 ),
inference(forward_demodulation,[],[f36743,f667]) ).
fof(f36769,plain,
( composition(sF11,sk3) = composition(sF11,join(complement(sF5),sk3))
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_29
| ~ spl13_46
| ~ spl13_52 ),
inference(forward_demodulation,[],[f36756,f667]) ).
fof(f36771,plain,
( composition(sF11,sk3) = join(composition(sF11,sk3),composition(sk1,complement(sF5)))
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_29
| ~ spl13_52 ),
inference(forward_demodulation,[],[f36758,f1]) ).
fof(f36781,plain,
( composition(sF11,sk3) = composition(sF11,join(sk3,complement(sF5)))
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_29
| ~ spl13_46
| ~ spl13_52 ),
inference(forward_demodulation,[],[f36769,f1]) ).
fof(f36783,plain,
( composition(sF11,sk3) = join(composition(sF11,sk3),composition(sk1,sF4))
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_24
| ~ spl13_29
| ~ spl13_52 ),
inference(forward_demodulation,[],[f36771,f4984]) ).
fof(f36793,plain,
( composition(sF11,sk3) = composition(sF11,join(sF12,complement(sF5)))
| ~ spl13_4
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_29
| ~ spl13_46
| ~ spl13_52
| ~ spl13_89 ),
inference(forward_demodulation,[],[f36781,f27460]) ).
fof(f36795,plain,
( sF12 = join(sF12,composition(sk1,sF4))
| ~ spl13_4
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_24
| ~ spl13_29
| ~ spl13_52 ),
inference(forward_demodulation,[],[f36783,f130]) ).
fof(f36804,plain,
( composition(sF11,sk3) = composition(sF11,join(sF12,sF4))
| ~ spl13_4
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_24
| ~ spl13_29
| ~ spl13_46
| ~ spl13_52
| ~ spl13_89 ),
inference(forward_demodulation,[],[f36793,f4984]) ).
fof(f36812,plain,
( composition(sF11,sk3) = composition(sF11,join(sF4,sF12))
| ~ spl13_4
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_24
| ~ spl13_29
| ~ spl13_46
| ~ spl13_52
| ~ spl13_89 ),
inference(forward_demodulation,[],[f36804,f27489]) ).
fof(f36819,plain,
( composition(sF11,sk3) = composition(sF11,sF4)
| ~ spl13_4
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_24
| ~ spl13_29
| ~ spl13_35
| ~ spl13_46
| ~ spl13_52
| ~ spl13_89 ),
inference(forward_demodulation,[],[f36812,f8129]) ).
fof(f36824,plain,
( sF12 = composition(sF11,sF4)
| ~ spl13_4
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_24
| ~ spl13_29
| ~ spl13_35
| ~ spl13_46
| ~ spl13_52
| ~ spl13_89 ),
inference(forward_demodulation,[],[f36819,f130]) ).
fof(f36830,definition,
( spl13_112
<=> sF12 = composition(sF11,sF4) ),
introduced(definition,[new_symbols(definition,[spl13_112])],[avatar_definition]) ).
fof(f36832,plain,
( sF12 = composition(sF11,sF4)
| ~ spl13_112 ),
inference(avatar_component_clause,[],[f36830]) ).
fof(f36833,plain,
( spl13_112
| ~ spl13_4
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_24
| ~ spl13_29
| ~ spl13_35
| ~ spl13_46
| ~ spl13_52
| ~ spl13_89 ),
inference(avatar_split_clause,[],[f36824,f27426,f15525,f10926,f8127,f6879,f4982,f573,f482,f283,f254,f196,f128,f36830]) ).
fof(f36839,plain,
( ! [X0] : composition(join(sF11,X0),sF4) = join(sF12,composition(X0,sF4))
| ~ spl13_112 ),
inference(superposition,[],[f9,f36832]) ).
fof(f36877,plain,
( sF12 = composition(join(sF11,sk1),sF4)
| ~ spl13_4
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_24
| ~ spl13_29
| ~ spl13_52
| ~ spl13_112 ),
inference(backward_demodulation,[],[f36795,f36839]) ).
fof(f36905,plain,
( sF12 = composition(sk1,sF4)
| ~ spl13_4
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_24
| ~ spl13_27
| ~ spl13_29
| ~ spl13_52
| ~ spl13_112 ),
inference(forward_demodulation,[],[f36877,f6282]) ).
fof(f36916,plain,
( sF6 = join(sF6,complement(sF12))
| ~ spl13_2
| ~ spl13_4
| ~ spl13_8
| ~ spl13_10
| ~ spl13_11
| ~ spl13_13
| ~ spl13_14
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_24
| ~ spl13_27
| ~ spl13_29
| ~ spl13_52
| ~ spl13_79
| ~ spl13_112 ),
inference(backward_demodulation,[],[f29202,f36905]) ).
fof(f36919,plain,
( complement(join(complement(sk3),complement(sF12))) = join(sF7,complement(join(complement(sk3),complement(sF12))))
| ~ spl13_4
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_24
| ~ spl13_27
| ~ spl13_29
| ~ spl13_52
| ~ spl13_98
| ~ spl13_112 ),
inference(backward_demodulation,[],[f29714,f36905]) ).
fof(f36938,plain,
( complement(join(complement(sF12),complement(sk3))) = join(sF7,complement(join(complement(sF12),complement(sk3))))
| ~ spl13_4
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_24
| ~ spl13_27
| ~ spl13_29
| ~ spl13_52
| ~ spl13_98
| ~ spl13_112 ),
inference(forward_demodulation,[],[f36919,f2134]) ).
fof(f36939,plain,
( sF6 = complement(sF12)
| ~ spl13_2
| ~ spl13_4
| ~ spl13_8
| ~ spl13_10
| ~ spl13_11
| ~ spl13_13
| ~ spl13_14
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_24
| ~ spl13_27
| ~ spl13_29
| ~ spl13_52
| ~ spl13_67
| ~ spl13_68
| ~ spl13_79
| ~ spl13_112 ),
inference(forward_demodulation,[],[f36916,f21500]) ).
fof(f36948,plain,
( complement(complement(sF12)) = join(sF7,complement(complement(sF12)))
| ~ spl13_4
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_24
| ~ spl13_27
| ~ spl13_29
| ~ spl13_52
| ~ spl13_53
| ~ spl13_98
| ~ spl13_112 ),
inference(forward_demodulation,[],[f36938,f15637]) ).
fof(f36977,plain,
( sF6 = complement(composition(sk1,sF12))
| ~ spl13_2
| ~ spl13_4
| ~ spl13_8
| ~ spl13_10
| ~ spl13_11
| ~ spl13_13
| ~ spl13_14
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_22
| ~ spl13_24
| ~ spl13_27
| ~ spl13_29
| ~ spl13_40
| ~ spl13_52
| ~ spl13_67
| ~ spl13_68
| ~ spl13_79
| ~ spl13_112 ),
inference(backward_demodulation,[],[f33372,f36939]) ).
fof(f37005,plain,
( sF12 = join(sF7,sF12)
| ~ spl13_4
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_24
| ~ spl13_27
| ~ spl13_29
| ~ spl13_52
| ~ spl13_53
| ~ spl13_98
| ~ spl13_112 ),
inference(forward_demodulation,[],[f36948,f667]) ).
fof(f37034,definition,
( spl13_115
<=> sF6 = complement(composition(sk1,sF12)) ),
introduced(definition,[new_symbols(definition,[spl13_115])],[avatar_definition]) ).
fof(f37036,plain,
( sF6 = complement(composition(sk1,sF12))
| ~ spl13_115 ),
inference(avatar_component_clause,[],[f37034]) ).
fof(f37037,plain,
( spl13_115
| ~ spl13_2
| ~ spl13_4
| ~ spl13_8
| ~ spl13_10
| ~ spl13_11
| ~ spl13_13
| ~ spl13_14
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_22
| ~ spl13_24
| ~ spl13_27
| ~ spl13_29
| ~ spl13_40
| ~ spl13_52
| ~ spl13_67
| ~ spl13_68
| ~ spl13_79
| ~ spl13_112 ),
inference(avatar_split_clause,[],[f36977,f36830,f23508,f21463,f21231,f15525,f9351,f6879,f6280,f4982,f4972,f573,f482,f283,f271,f265,f254,f196,f166,f128,f105,f37034]) ).
fof(f37063,plain,
( complement(sF6) = composition(sk1,sF12)
| ~ spl13_11
| ~ spl13_115 ),
inference(superposition,[],[f667,f37036]) ).
fof(f37116,plain,
( sF7 = composition(sk1,sF12)
| ~ spl13_2
| ~ spl13_11
| ~ spl13_115 ),
inference(forward_demodulation,[],[f37063,f107]) ).
fof(f37260,definition,
( spl13_116
<=> sF7 = composition(sk1,sF12) ),
introduced(definition,[new_symbols(definition,[spl13_116])],[avatar_definition]) ).
fof(f37262,plain,
( sF7 = composition(sk1,sF12)
| ~ spl13_116 ),
inference(avatar_component_clause,[],[f37260]) ).
fof(f37263,plain,
( spl13_116
| ~ spl13_2
| ~ spl13_11
| ~ spl13_115 ),
inference(avatar_split_clause,[],[f37116,f37034,f254,f105,f37260]) ).
fof(f37291,plain,
( join(sF12,sF7) = composition(join(sk1,sF0),sF12)
| ~ spl13_116 ),
inference(superposition,[],[f1451,f37262]) ).
fof(f37299,plain,
( join(sF12,sF7) = composition(join(sF0,sk1),sF12)
| ~ spl13_11
| ~ spl13_116 ),
inference(forward_demodulation,[],[f37291,f34517]) ).
fof(f37335,plain,
( join(sF12,sF7) = composition(join(sF11,sk1),sF12)
| ~ spl13_11
| ~ spl13_89
| ~ spl13_116 ),
inference(forward_demodulation,[],[f37299,f27465]) ).
fof(f37353,plain,
( composition(sk1,sF12) = join(sF12,sF7)
| ~ spl13_11
| ~ spl13_27
| ~ spl13_89
| ~ spl13_116 ),
inference(forward_demodulation,[],[f37335,f6282]) ).
fof(f37365,plain,
( composition(sk1,sF12) = join(sF7,sF12)
| ~ spl13_11
| ~ spl13_27
| ~ spl13_89
| ~ spl13_116 ),
inference(forward_demodulation,[],[f37353,f1]) ).
fof(f37373,plain,
( sF12 = composition(sk1,sF12)
| ~ spl13_4
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_24
| ~ spl13_27
| ~ spl13_29
| ~ spl13_52
| ~ spl13_53
| ~ spl13_89
| ~ spl13_98
| ~ spl13_112
| ~ spl13_116 ),
inference(forward_demodulation,[],[f37365,f37005]) ).
fof(f37377,plain,
( sF7 = sF12
| ~ spl13_4
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_24
| ~ spl13_27
| ~ spl13_29
| ~ spl13_52
| ~ spl13_53
| ~ spl13_89
| ~ spl13_98
| ~ spl13_112
| ~ spl13_116 ),
inference(forward_demodulation,[],[f37373,f37262]) ).
fof(f37381,plain,
( $false
| ~ spl13_4
| spl13_6
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_24
| ~ spl13_27
| ~ spl13_29
| ~ spl13_52
| ~ spl13_53
| ~ spl13_89
| ~ spl13_98
| ~ spl13_112
| ~ spl13_116 ),
inference(forward_subsumption_resolution,[],[f37377,f146]) ).
fof(f37382,plain,
( ~ spl13_4
| spl13_6
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_24
| ~ spl13_27
| ~ spl13_29
| ~ spl13_52
| ~ spl13_53
| ~ spl13_89
| ~ spl13_98
| ~ spl13_112
| ~ spl13_116 ),
inference(avatar_contradiction_clause,[],[f37381]) ).
cnf(s2,plain,
spl13_2,
inference(sat_conversion,[],[f108]) ).
cnf(s4,plain,
spl13_4,
inference(sat_conversion,[],[f131]) ).
cnf(s5,plain,
spl13_5,
inference(sat_conversion,[],[f142]) ).
cnf(s6,plain,
~ spl13_6,
inference(sat_conversion,[],[f147]) ).
cnf(s7,plain,
spl13_7,
inference(sat_conversion,[],[f152]) ).
cnf(s8,plain,
spl13_8,
inference(sat_conversion,[],[f169]) ).
cnf(s9,plain,
spl13_9,
inference(sat_conversion,[],[f184]) ).
cnf(s10,plain,
spl13_10,
inference(sat_conversion,[],[f199]) ).
cnf(s11,plain,
spl13_11,
inference(sat_conversion,[],[f257]) ).
cnf(s12,plain,
spl13_12,
inference(sat_conversion,[],[f262]) ).
cnf(s13,plain,
spl13_13,
inference(sat_conversion,[],[f268]) ).
cnf(s14,plain,
spl13_14,
inference(sat_conversion,[],[f274]) ).
cnf(s15,plain,
spl13_15,
inference(sat_conversion,[],[f286]) ).
cnf(s16,plain,
spl13_16,
inference(sat_conversion,[],[f485]) ).
cnf(s17,plain,
spl13_17,
inference(sat_conversion,[],[f576]) ).
cnf(s18,plain,
( ~ spl13_7
| ~ spl13_11
| spl13_18 ),
inference(sat_conversion,[],[f1047]) ).
cnf(s19,plain,
( ~ spl13_5
| ~ spl13_11
| spl13_19 ),
inference(sat_conversion,[],[f1052]) ).
cnf(s20,plain,
( ~ spl13_14
| ~ spl13_16
| spl13_20 ),
inference(sat_conversion,[],[f2848]) ).
cnf(s22,plain,
( ~ spl13_8
| ~ spl13_11
| spl13_22 ),
inference(sat_conversion,[],[f4975]) ).
cnf(s24,plain,
( ~ spl13_10
| ~ spl13_11
| spl13_24 ),
inference(sat_conversion,[],[f4985]) ).
cnf(s27,plain,
( ~ spl13_9
| ~ spl13_11
| ~ spl13_12
| ~ spl13_18
| spl13_27 ),
inference(sat_conversion,[],[f6283]) ).
cnf(s28,plain,
( ~ spl13_11
| spl13_28 ),
inference(sat_conversion,[],[f6659]) ).
cnf(s29,plain,
( ~ spl13_11
| spl13_29 ),
inference(sat_conversion,[],[f6882]) ).
cnf(s33,plain,
spl13_33,
inference(sat_conversion,[],[f7382]) ).
cnf(s34,plain,
( ~ spl13_4
| ~ spl13_9
| ~ spl13_11
| ~ spl13_12
| ~ spl13_14
| ~ spl13_18
| spl13_34 ),
inference(sat_conversion,[],[f7482]) ).
cnf(s35,plain,
( ~ spl13_4
| ~ spl13_5
| ~ spl13_7
| ~ spl13_9
| ~ spl13_11
| ~ spl13_12
| ~ spl13_15
| ~ spl13_18
| ~ spl13_19
| spl13_35 ),
inference(sat_conversion,[],[f8130]) ).
cnf(s36,plain,
( ~ spl13_11
| spl13_36 ),
inference(sat_conversion,[],[f8271]) ).
cnf(s40,plain,
( ~ spl13_8
| ~ spl13_11
| ~ spl13_14
| ~ spl13_16
| spl13_40 ),
inference(sat_conversion,[],[f9354]) ).
cnf(s43,plain,
( ~ spl13_5
| ~ spl13_9
| ~ spl13_11
| ~ spl13_12
| ~ spl13_17
| ~ spl13_19
| spl13_43 ),
inference(sat_conversion,[],[f10662]) ).
cnf(s46,plain,
( ~ spl13_9
| ~ spl13_11
| ~ spl13_43
| spl13_46 ),
inference(sat_conversion,[],[f10929]) ).
cnf(s50,plain,
( ~ spl13_7
| ~ spl13_11
| ~ spl13_16
| spl13_50 ),
inference(sat_conversion,[],[f15055]) ).
cnf(s51,plain,
( ~ spl13_5
| ~ spl13_11
| ~ spl13_12
| ~ spl13_17
| ~ spl13_18
| ~ spl13_50
| spl13_51 ),
inference(sat_conversion,[],[f15392]) ).
cnf(s52,plain,
( ~ spl13_9
| ~ spl13_11
| ~ spl13_51
| spl13_52 ),
inference(sat_conversion,[],[f15528]) ).
cnf(s53,plain,
( ~ spl13_4
| ~ spl13_9
| ~ spl13_11
| ~ spl13_16
| ~ spl13_17
| ~ spl13_51
| spl13_53 ),
inference(sat_conversion,[],[f15626]) ).
cnf(s67,plain,
( ~ spl13_8
| ~ spl13_11
| ~ spl13_34
| spl13_67 ),
inference(sat_conversion,[],[f21234]) ).
cnf(s68,plain,
( ~ spl13_10
| ~ spl13_11
| ~ spl13_35
| spl13_68 ),
inference(sat_conversion,[],[f21466]) ).
cnf(s69,plain,
( ~ spl13_5
| ~ spl13_11
| ~ spl13_17
| spl13_69 ),
inference(sat_conversion,[],[f21866]) ).
cnf(s79,plain,
( ~ spl13_8
| ~ spl13_11
| ~ spl13_20
| spl13_79 ),
inference(sat_conversion,[],[f23511]) ).
cnf(s89,plain,
( ~ spl13_4
| ~ spl13_11
| ~ spl13_16
| ~ spl13_17
| ~ spl13_28
| ~ spl13_29
| ~ spl13_33
| ~ spl13_36
| ~ spl13_52
| ~ spl13_69
| spl13_89 ),
inference(sat_conversion,[],[f27429]) ).
cnf(s98,plain,
( ~ spl13_2
| ~ spl13_8
| ~ spl13_10
| ~ spl13_11
| ~ spl13_13
| ~ spl13_14
| ~ spl13_16
| ~ spl13_29
| spl13_98 ),
inference(sat_conversion,[],[f29715]) ).
cnf(s112,plain,
( ~ spl13_4
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_24
| ~ spl13_29
| ~ spl13_35
| ~ spl13_46
| ~ spl13_52
| ~ spl13_89
| spl13_112 ),
inference(sat_conversion,[],[f36833]) ).
cnf(s115,plain,
( ~ spl13_2
| ~ spl13_4
| ~ spl13_8
| ~ spl13_10
| ~ spl13_11
| ~ spl13_13
| ~ spl13_14
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_22
| ~ spl13_24
| ~ spl13_27
| ~ spl13_29
| ~ spl13_40
| ~ spl13_52
| ~ spl13_67
| ~ spl13_68
| ~ spl13_79
| ~ spl13_112
| spl13_115 ),
inference(sat_conversion,[],[f37037]) ).
cnf(s116,plain,
( ~ spl13_2
| ~ spl13_11
| ~ spl13_115
| spl13_116 ),
inference(sat_conversion,[],[f37263]) ).
cnf(s118,plain,
( ~ spl13_4
| spl13_6
| ~ spl13_10
| ~ spl13_11
| ~ spl13_15
| ~ spl13_16
| ~ spl13_17
| ~ spl13_24
| ~ spl13_27
| ~ spl13_29
| ~ spl13_52
| ~ spl13_53
| ~ spl13_89
| ~ spl13_98
| ~ spl13_112
| ~ spl13_116 ),
inference(sat_conversion,[],[f37382]) ).
cnf(s125,plain,
spl13_20,
inference(rat,[],[s20,s16,s14]) ).
cnf(s130,plain,
spl13_36,
inference(rat,[],[s36,s11]) ).
cnf(s131,plain,
spl13_29,
inference(rat,[],[s29,s11]) ).
cnf(s132,plain,
spl13_28,
inference(rat,[],[s28,s11]) ).
cnf(s140,plain,
spl13_24,
inference(rat,[],[s24,s11,s10]) ).
cnf(s145,plain,
spl13_79,
inference(rat,[],[s79,s11,s125,s8]) ).
cnf(s147,plain,
spl13_40,
inference(rat,[],[s40,s11,s16,s14,s8]) ).
cnf(s149,plain,
spl13_22,
inference(rat,[],[s22,s11,s8]) ).
cnf(s155,plain,
spl13_50,
inference(rat,[],[s50,s11,s16,s7]) ).
cnf(s158,plain,
spl13_18,
inference(rat,[],[s18,s11,s7]) ).
cnf(s161,plain,
spl13_27,
inference(rat,[],[s27,s9,s11,s12,s158]) ).
cnf(s164,plain,
spl13_69,
inference(rat,[],[s69,s11,s17,s5]) ).
cnf(s168,plain,
spl13_51,
inference(rat,[],[s51,s158,s155,s11,s17,s12,s5]) ).
cnf(s171,plain,
spl13_19,
inference(rat,[],[s19,s11,s5]) ).
cnf(s173,plain,
spl13_52,
inference(rat,[],[s52,s9,s11,s168]) ).
cnf(s179,plain,
spl13_43,
inference(rat,[],[s43,s5,s9,s17,s12,s11,s171]) ).
cnf(s186,plain,
spl13_46,
inference(rat,[],[s46,s9,s11,s179]) ).
cnf(s190,plain,
spl13_89,
inference(rat,[],[s89,s173,s164,s132,s130,s33,s131,s11,s17,s16,s4]) ).
cnf(s191,plain,
spl13_53,
inference(rat,[],[s53,s168,s9,s17,s16,s11,s4]) ).
cnf(s192,plain,
spl13_35,
inference(rat,[],[s35,s171,s5,s158,s15,s12,s11,s9,s7,s4]) ).
cnf(s193,plain,
spl13_34,
inference(rat,[],[s34,s158,s9,s14,s12,s11,s4]) ).
cnf(s196,plain,
spl13_68,
inference(rat,[],[s68,s10,s11,s192]) ).
cnf(s197,plain,
spl13_112,
inference(rat,[],[s112,s190,s4,s173,s186,s140,s131,s10,s17,s16,s15,s11,s192]) ).
cnf(s200,plain,
spl13_67,
inference(rat,[],[s67,s8,s11,s193]) ).
cnf(s201,plain,
spl13_115,
inference(rat,[],[s115,s200,s197,s145,s196,s4,s173,s147,s131,s161,s140,s149,s17,s16,s15,s14,s13,s11,s10,s8,s2]) ).
cnf(s202,plain,
spl13_98,
inference(rat,[],[s98,s8,s131,s16,s14,s13,s11,s10,s2]) ).
cnf(s210,plain,
spl13_116,
inference(rat,[],[s116,s2,s11,s201]) ).
cnf(s213,plain,
$false,
inference(rat,[],[s118,s197,s191,s190,s4,s173,s6,s131,s161,s140,s17,s16,s15,s11,s10,s210,s202]) ).
fof(f37388,plain,
$false,
inference(avatar_sat_refutation,[],[s213]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL029-3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.37 % Computer : n003.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 22:55:41 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 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
% 17.76/3.37 % (1016082)Detected a unit-equality problem, will run specialized UEQ schedule.
% 17.76/3.37 % (1016087)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=745531845:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 17.76/3.37 % (1016091)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=2710123291:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 17.76/3.37 % (1016093)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=4065657752:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 17.76/3.37 % (1016088)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=887051766:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 17.76/3.37 % (1016089)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=2632065579:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 17.76/3.37 % (1016090)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=328549660:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 17.76/3.37 % (1016092)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=4153524039:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 17.76/3.37 % (1016090)Instruction limit reached!
% 17.76/3.37 % (1016090)------------------------------
% 17.76/3.37 % (1016090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.76/3.37 % (1016090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.76/3.37 % (1016090)CaDiCaL version: 2.1.3
% 17.76/3.37 % (1016090)Termination reason: Instruction limit
% 17.76/3.37 % (1016090)Termination phase: Saturation
% 17.76/3.37 % (1016090)Time elapsed: 0.082 s
% 17.76/3.37 % (1016090)Peak memory usage: 89 MB
% 17.76/3.37 % (1016090)Instructions burned: 137 (million)
% 17.76/3.37 % (1016091)Instruction limit reached!
% 17.76/3.37 % (1016091)------------------------------
% 17.76/3.37 % (1016091)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.76/3.37 % (1016091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.76/3.37 % (1016091)CaDiCaL version: 2.1.3
% 17.76/3.37 % (1016091)Termination reason: Instruction limit
% 17.76/3.37 % (1016091)Termination phase: Saturation
% 17.76/3.37 % (1016091)Time elapsed: 0.103 s
% 17.76/3.37 % (1016091)Peak memory usage: 89 MB
% 17.76/3.37 % (1016091)Instructions burned: 181 (million)
% 17.76/3.37 % (1016092)Instruction limit reached!
% 17.76/3.37 % (1016092)------------------------------
% 17.76/3.37 % (1016092)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.76/3.37 % (1016092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.76/3.37 % (1016092)CaDiCaL version: 2.1.3
% 17.76/3.37 % (1016092)Termination reason: Instruction limit
% 17.76/3.37 % (1016092)Termination phase: Saturation
% 17.76/3.37 % (1016092)Time elapsed: 0.167 s
% 17.76/3.37 % (1016092)Peak memory usage: 90 MB
% 17.76/3.37 % (1016092)Instructions burned: 258 (million)
% 17.76/3.37 % (1016101)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=3919201900:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2997 on theBenchmark for (2997ds/2051Mi)
% 17.76/3.37 % (1016102)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2457605418:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 17.76/3.37 % (1016103)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=2583636802:i=215:ep=RSTC_2996 on theBenchmark for (2996ds/215Mi)
% 17.76/3.37 % (1016103)Instruction limit reached!
% 17.76/3.37 % (1016103)------------------------------
% 17.76/3.37 % (1016103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.76/3.37 % (1016103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.76/3.37 % (1016103)CaDiCaL version: 2.1.3
% 17.76/3.37 % (1016103)Termination reason: Instruction limit
% 17.76/3.37 % (1016103)Termination phase: Saturation
% 17.76/3.37 % (1016103)Time elapsed: 0.121 s
% 17.76/3.37 % (1016103)Peak memory usage: 92 MB
% 17.76/3.37 % (1016103)Instructions burned: 216 (million)
% 17.76/3.37 % (1016107)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=3098087647:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2993 on theBenchmark for (2993ds/317Mi)
% 17.76/3.37 % (1016093)Instruction limit reached!
% 17.76/3.37 % (1016093)------------------------------
% 17.76/3.37 % (1016093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.76/3.37 % (1016093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.76/3.37 % (1016093)CaDiCaL version: 2.1.3
% 17.76/3.37 % (1016093)Termination reason: Instruction limit
% 17.76/3.37 % (1016093)Termination phase: Saturation
% 17.76/3.37 % (1016093)Time elapsed: 0.640 s
% 17.76/3.37 % (1016093)Peak memory usage: 101 MB
% 17.76/3.37 % (1016093)Instructions burned: 1189 (million)
% 17.76/3.37 % (1016107)Instruction limit reached!
% 17.76/3.37 % (1016107)------------------------------
% 17.76/3.37 % (1016107)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.76/3.37 % (1016107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.76/3.37 % (1016107)CaDiCaL version: 2.1.3
% 17.76/3.37 % (1016107)Termination reason: Instruction limit
% 17.76/3.37 % (1016107)Termination phase: Saturation
% 17.76/3.37 % (1016107)Time elapsed: 0.181 s
% 17.76/3.37 % (1016107)Peak memory usage: 91 MB
% 17.76/3.37 % (1016107)Instructions burned: 318 (million)
% 17.76/3.37 % (1016109)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=698316661:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2991 on theBenchmark for (2991ds/12125Mi)
% 17.76/3.37 % (1016110)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=3575307153:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2990 on theBenchmark for (2990ds/2836Mi)
% 17.76/3.37 % (1016101)Instruction limit reached!
% 17.76/3.37 % (1016101)------------------------------
% 17.76/3.37 % (1016101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.76/3.37 % (1016101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.76/3.37 % (1016101)CaDiCaL version: 2.1.3
% 17.76/3.37 % (1016101)Termination reason: Instruction limit
% 17.76/3.37 % (1016101)Termination phase: Saturation
% 17.76/3.37 % (1016101)Time elapsed: 1.314 s
% 17.76/3.37 % (1016101)Peak memory usage: 141 MB
% 17.76/3.37 % (1016101)Instructions burned: 2053 (million)
% 17.76/3.37 % (1016113)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2539891074:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2982 on theBenchmark for (2982ds/14534Mi)
% 17.76/3.37 % (1016087)First to succeed.
% 17.76/3.37 % (1016087)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1016082"
% 17.76/3.37 % (1016087)Refutation found. Thanks to Tanya!
% 17.76/3.37 % SZS status Unsatisfiable for theBenchmark
% 17.76/3.37 % SZS output start Proof for theBenchmark
% See solution above
% 18.38/3.57 % (1016087)------------------------------
% 18.38/3.57 % (1016087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.38/3.57 % (1016087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.38/3.57 % (1016087)CaDiCaL version: 2.1.3
% 18.38/3.57 % (1016087)Termination reason: Refutation
% 18.38/3.57 % (1016087)Time elapsed: 2.202 s
% 18.38/3.57 % (1016087)Peak memory usage: 187 MB
% 18.38/3.57 % (1016087)Instructions burned: 6481 (million)
% 18.38/3.57 % (1016087)------------------------------
% 18.38/3.57 % (1016087)------------------------------
% 18.38/3.57 % (1016082)Success in time 2.516 s
% 18.38/3.57 % Vampire exiting
%------------------------------------------------------------------------------