%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : REL022-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n004.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:49 PM UTC 2026
% Result : Unsatisfiable 13.36s 2.74s
% Output : Refutation 13.86s
% Verified :
% SZS Type : Refutation
% Derivation depth : 46
% Number of leaves : 51
% Syntax : Number of formulae : 390 ( 132 unt; 36 def)
% Number of atoms : 1040 ( 319 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 1279 ( 629 ~; 624 |; 0 &)
% ( 26 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 28 ( 26 usr; 27 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 15 con; 0-2 aty)
% Number of variables : 239 ( 0 sgn 239 !; 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,negated_conjecture,
composition(sk1,top) = sk1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals_14) ).
fof(f18,plain,
sk1 = composition(sk1,top),
inference(reorient_equations,[],[f17]) ).
fof(f19,negated_conjecture,
join(meet(sk1,sk2),composition(meet(sk1,one),sk2)) != composition(meet(sk1,one),sk2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals_15) ).
fof(f20,plain,
composition(meet(sk1,one),sk2) != join(meet(sk1,sk2),composition(meet(sk1,one),sk2)),
inference(reorient_equations,[],[f19]) ).
fof(f21,plain,
! [X0] : zero = complement(join(complement(X0),complement(complement(X0)))),
inference(definition_unfolding,[],[f16,f6]) ).
fof(f22,plain,
composition(complement(join(complement(sk1),complement(one))),sk2) != join(complement(join(complement(sk1),complement(sk2))),composition(complement(join(complement(sk1),complement(one))),sk2)),
inference(definition_unfolding,[],[f20,f6,f6,f6]) ).
fof(f23,definition,
sF0 = composition(sk1,top),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f24,plain,
composition(sk1,top) = sF0,
inference(reorient_equations,[],[f23]) ).
fof(f25,plain,
sk1 = sF0,
inference(definition_folding,[],[f18,f24]) ).
fof(f26,definition,
sF1 = complement(sk1),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f27,plain,
complement(sk1) = sF1,
inference(reorient_equations,[],[f26]) ).
fof(f28,definition,
sF2 = complement(one),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f29,plain,
complement(one) = sF2,
inference(reorient_equations,[],[f28]) ).
fof(f30,definition,
sF3 = join(sF1,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f31,plain,
join(sF1,sF2) = sF3,
inference(reorient_equations,[],[f30]) ).
fof(f32,definition,
sF4 = complement(sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f33,plain,
complement(sF3) = sF4,
inference(reorient_equations,[],[f32]) ).
fof(f34,definition,
sF5 = composition(sF4,sk2),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f35,plain,
composition(sF4,sk2) = sF5,
inference(reorient_equations,[],[f34]) ).
fof(f36,definition,
sF6 = complement(sk2),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f37,plain,
complement(sk2) = sF6,
inference(reorient_equations,[],[f36]) ).
fof(f38,definition,
sF7 = join(sF1,sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f39,plain,
join(sF1,sF6) = sF7,
inference(reorient_equations,[],[f38]) ).
fof(f40,definition,
sF8 = complement(sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f41,plain,
complement(sF7) = sF8,
inference(reorient_equations,[],[f40]) ).
fof(f42,definition,
sF9 = join(sF8,sF5),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f43,plain,
join(sF8,sF5) = sF9,
inference(reorient_equations,[],[f42]) ).
fof(f44,plain,
sF5 != sF9,
inference(definition_folding,[],[f22,f43,f35,f33,f31,f29,f27,f41,f39,f37,f27,f35,f33,f31,f29,f27]) ).
fof(f45,plain,
zero = complement(top),
inference(backward_demodulation,[],[f21,f15]) ).
fof(f46,plain,
sF0 = composition(sF0,top),
inference(forward_demodulation,[],[f24,f25]) ).
fof(f47,plain,
sF1 = complement(sF0),
inference(forward_demodulation,[],[f27,f25]) ).
fof(f48,plain,
sF3 = join(sF2,sF1),
inference(forward_demodulation,[],[f31,f1]) ).
fof(f49,plain,
sF7 = join(sF6,sF1),
inference(forward_demodulation,[],[f39,f1]) ).
fof(f51,definition,
( spl10_1
<=> sF0 = composition(sF0,top) ),
introduced(definition,[new_symbols(definition,[spl10_1])],[avatar_definition]) ).
fof(f53,plain,
( sF0 = composition(sF0,top)
| ~ spl10_1 ),
inference(avatar_component_clause,[],[f51]) ).
fof(f54,plain,
spl10_1,
inference(avatar_split_clause,[],[f46,f51]) ).
fof(f63,plain,
! [X2,X0,X1] : join(composition(X0,X1),composition(X2,X1)) = composition(join(X2,X0),X1),
inference(superposition,[],[f9,f1]) ).
fof(f64,plain,
! [X2,X0,X1] : composition(join(X0,X2),X1) = composition(join(X2,X0),X1),
inference(forward_demodulation,[],[f63,f9]) ).
fof(f69,definition,
( spl10_3
<=> sF5 = sF9 ),
introduced(definition,[new_symbols(definition,[spl10_3])],[avatar_definition]) ).
fof(f71,plain,
( sF5 != sF9
| spl10_3 ),
inference(avatar_component_clause,[],[f69]) ).
fof(f72,plain,
~ spl10_3,
inference(avatar_split_clause,[],[f44,f69]) ).
fof(f74,plain,
( ! [X0] : composition(join(sF0,X0),top) = join(sF0,composition(X0,top))
| ~ spl10_1 ),
inference(superposition,[],[f9,f53]) ).
fof(f78,definition,
( spl10_4
<=> composition(sF4,sk2) = sF5 ),
introduced(definition,[new_symbols(definition,[spl10_4])],[avatar_definition]) ).
fof(f80,plain,
( composition(sF4,sk2) = sF5
| ~ spl10_4 ),
inference(avatar_component_clause,[],[f78]) ).
fof(f81,plain,
spl10_4,
inference(avatar_split_clause,[],[f35,f78]) ).
fof(f87,definition,
( spl10_5
<=> join(sF8,sF5) = sF9 ),
introduced(definition,[new_symbols(definition,[spl10_5])],[avatar_definition]) ).
fof(f89,plain,
( join(sF8,sF5) = sF9
| ~ spl10_5 ),
inference(avatar_component_clause,[],[f87]) ).
fof(f90,plain,
spl10_5,
inference(avatar_split_clause,[],[f43,f87]) ).
fof(f93,plain,
! [X0,X1] : join(complement(join(complement(X0),complement(X1))),complement(join(complement(X1),X0))) = X1,
inference(superposition,[],[f4,f1]) ).
fof(f104,plain,
! [X0,X1] : join(complement(join(complement(X1),X0)),complement(join(complement(X0),complement(X1)))) = X1,
inference(forward_demodulation,[],[f93,f1]) ).
fof(f110,definition,
( spl10_6
<=> complement(sk2) = sF6 ),
introduced(definition,[new_symbols(definition,[spl10_6])],[avatar_definition]) ).
fof(f112,plain,
( complement(sk2) = sF6
| ~ spl10_6 ),
inference(avatar_component_clause,[],[f110]) ).
fof(f113,plain,
spl10_6,
inference(avatar_split_clause,[],[f37,f110]) ).
fof(f119,definition,
( spl10_7
<=> sF1 = complement(sF0) ),
introduced(definition,[new_symbols(definition,[spl10_7])],[avatar_definition]) ).
fof(f121,plain,
( sF1 = complement(sF0)
| ~ spl10_7 ),
inference(avatar_component_clause,[],[f119]) ).
fof(f122,plain,
spl10_7,
inference(avatar_split_clause,[],[f47,f119]) ).
fof(f128,plain,
( top = join(sF0,sF1)
| ~ spl10_7 ),
inference(superposition,[],[f15,f121]) ).
fof(f130,plain,
! [X0] : join(complement(join(complement(X0),complement(complement(complement(X0))))),complement(top)) = X0,
inference(superposition,[],[f4,f15]) ).
fof(f131,plain,
! [X0] : join(complement(top),complement(join(complement(X0),complement(complement(complement(X0)))))) = X0,
inference(forward_demodulation,[],[f130,f1]) ).
fof(f133,plain,
( top = join(sF1,sF0)
| ~ spl10_7 ),
inference(forward_demodulation,[],[f128,f1]) ).
fof(f135,plain,
! [X0] : join(zero,complement(join(complement(X0),complement(complement(complement(X0)))))) = X0,
inference(forward_demodulation,[],[f131,f45]) ).
fof(f136,plain,
! [X0,X1] : complement(X1) = join(composition(X0,complement(composition(converse(X0),X1))),complement(X1)),
inference(superposition,[],[f14,f10]) ).
fof(f137,plain,
( complement(top) = join(composition(converse(sF0),complement(sF0)),complement(top))
| ~ spl10_1 ),
inference(superposition,[],[f14,f53]) ).
fof(f148,plain,
( complement(top) = join(complement(top),composition(converse(sF0),complement(sF0)))
| ~ spl10_1 ),
inference(forward_demodulation,[],[f137,f1]) ).
fof(f149,plain,
! [X0,X1] : complement(X1) = join(complement(X1),composition(X0,complement(composition(converse(X0),X1)))),
inference(forward_demodulation,[],[f136,f1]) ).
fof(f151,plain,
( complement(top) = join(complement(top),composition(converse(sF0),sF1))
| ~ spl10_1
| ~ spl10_7 ),
inference(forward_demodulation,[],[f148,f121]) ).
fof(f152,plain,
( zero = join(zero,composition(converse(sF0),sF1))
| ~ spl10_1
| ~ spl10_7 ),
inference(forward_demodulation,[],[f151,f45]) ).
fof(f154,definition,
( spl10_8
<=> complement(sF7) = sF8 ),
introduced(definition,[new_symbols(definition,[spl10_8])],[avatar_definition]) ).
fof(f156,plain,
( complement(sF7) = sF8
| ~ spl10_8 ),
inference(avatar_component_clause,[],[f154]) ).
fof(f157,plain,
spl10_8,
inference(avatar_split_clause,[],[f41,f154]) ).
fof(f170,definition,
( spl10_9
<=> complement(sF3) = sF4 ),
introduced(definition,[new_symbols(definition,[spl10_9])],[avatar_definition]) ).
fof(f172,plain,
( complement(sF3) = sF4
| ~ spl10_9 ),
inference(avatar_component_clause,[],[f170]) ).
fof(f173,plain,
spl10_9,
inference(avatar_split_clause,[],[f33,f170]) ).
fof(f185,plain,
! [X0,X1] : converse(join(converse(X0),X1)) = join(X0,converse(X1)),
inference(superposition,[],[f11,f10]) ).
fof(f197,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(top,X1),
inference(superposition,[],[f2,f15]) ).
fof(f199,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(f208,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f1,f2]) ).
fof(f211,plain,
! [X2,X0,X1] : join(X0,X2) = join(complement(join(complement(X0),X1)),join(X2,complement(join(complement(X0),complement(X1))))),
inference(forward_demodulation,[],[f199,f208]) ).
fof(f224,definition,
( spl10_10
<=> sF7 = join(sF6,sF1) ),
introduced(definition,[new_symbols(definition,[spl10_10])],[avatar_definition]) ).
fof(f226,plain,
( sF7 = join(sF6,sF1)
| ~ spl10_10 ),
inference(avatar_component_clause,[],[f224]) ).
fof(f227,plain,
spl10_10,
inference(avatar_split_clause,[],[f49,f224]) ).
fof(f228,plain,
( ! [X0] : join(sF6,join(sF1,X0)) = join(sF7,X0)
| ~ spl10_10 ),
inference(superposition,[],[f2,f226]) ).
fof(f230,definition,
( spl10_11
<=> sF3 = join(sF2,sF1) ),
introduced(definition,[new_symbols(definition,[spl10_11])],[avatar_definition]) ).
fof(f232,plain,
( sF3 = join(sF2,sF1)
| ~ spl10_11 ),
inference(avatar_component_clause,[],[f230]) ).
fof(f233,plain,
spl10_11,
inference(avatar_split_clause,[],[f48,f230]) ).
fof(f236,definition,
( spl10_12
<=> complement(one) = sF2 ),
introduced(definition,[new_symbols(definition,[spl10_12])],[avatar_definition]) ).
fof(f238,plain,
( complement(one) = sF2
| ~ spl10_12 ),
inference(avatar_component_clause,[],[f236]) ).
fof(f239,plain,
spl10_12,
inference(avatar_split_clause,[],[f29,f236]) ).
fof(f250,definition,
( spl10_13
<=> zero = complement(top) ),
introduced(definition,[new_symbols(definition,[spl10_13])],[avatar_definition]) ).
fof(f252,plain,
( zero = complement(top)
| ~ spl10_13 ),
inference(avatar_component_clause,[],[f250]) ).
fof(f253,plain,
spl10_13,
inference(avatar_split_clause,[],[f45,f250]) ).
fof(f271,plain,
! [X0] : complement(X0) = join(complement(join(complement(complement(X0)),X0)),complement(top)),
inference(superposition,[],[f104,f15]) ).
fof(f279,plain,
! [X0] : complement(X0) = join(complement(top),complement(join(complement(complement(X0)),X0))),
inference(forward_demodulation,[],[f271,f1]) ).
fof(f295,plain,
! [X0] : complement(X0) = join(complement(top),complement(join(X0,complement(complement(X0))))),
inference(forward_demodulation,[],[f279,f1]) ).
fof(f301,plain,
( ! [X0] : complement(X0) = join(zero,complement(join(X0,complement(complement(X0)))))
| ~ spl10_13 ),
inference(forward_demodulation,[],[f295,f252]) ).
fof(f306,plain,
( ! [X0] : complement(complement(X0)) = X0
| ~ spl10_13 ),
inference(backward_demodulation,[],[f135,f301]) ).
fof(f314,plain,
( one = complement(sF2)
| ~ spl10_12
| ~ spl10_13 ),
inference(superposition,[],[f306,f238]) ).
fof(f315,plain,
( sk2 = complement(sF6)
| ~ spl10_6
| ~ spl10_13 ),
inference(superposition,[],[f306,f112]) ).
fof(f316,plain,
( sF0 = complement(sF1)
| ~ spl10_7
| ~ spl10_13 ),
inference(superposition,[],[f306,f121]) ).
fof(f318,plain,
( sF7 = complement(sF8)
| ~ spl10_8
| ~ spl10_13 ),
inference(superposition,[],[f306,f156]) ).
fof(f319,plain,
( ! [X0,X1] : complement(X0) = join(complement(join(X0,complement(X1))),complement(join(X0,X1)))
| ~ spl10_13 ),
inference(superposition,[],[f4,f306]) ).
fof(f324,plain,
( ! [X0,X1] : complement(X0) = join(complement(join(X0,X1)),complement(join(complement(X1),X0)))
| ~ spl10_13 ),
inference(superposition,[],[f104,f306]) ).
fof(f329,plain,
( ! [X0,X1] : complement(X0) = join(complement(join(X0,X1)),complement(join(X0,complement(X1))))
| ~ spl10_13 ),
inference(forward_demodulation,[],[f319,f1]) ).
fof(f337,plain,
( ! [X0,X1] : complement(X1) = join(complement(join(X0,X1)),complement(join(X1,complement(X0))))
| ~ spl10_13 ),
inference(superposition,[],[f329,f1]) ).
fof(f414,plain,
! [X0,X1] : composition(converse(X1),X0) = converse(composition(converse(X0),X1)),
inference(superposition,[],[f12,f10]) ).
fof(f415,plain,
! [X0,X1] : complement(converse(X0)) = join(composition(converse(converse(X1)),complement(converse(composition(X0,X1)))),complement(converse(X0))),
inference(superposition,[],[f14,f12]) ).
fof(f417,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(f418,plain,
! [X0,X1] : complement(converse(X0)) = join(complement(converse(X0)),composition(converse(converse(X1)),complement(converse(composition(X0,X1))))),
inference(forward_demodulation,[],[f415,f1]) ).
fof(f419,plain,
! [X0,X1] : complement(converse(X0)) = join(complement(converse(X0)),composition(X1,complement(converse(composition(X0,X1))))),
inference(forward_demodulation,[],[f418,f10]) ).
fof(f425,plain,
! [X2,X0,X1] : composition(join(converse(X2),converse(X1)),converse(X0)) = join(converse(composition(X0,X2)),converse(composition(X0,X1))),
inference(superposition,[],[f417,f12]) ).
fof(f436,plain,
! [X2,X0,X1] : composition(join(converse(X2),converse(X1)),converse(X0)) = converse(join(composition(X0,X2),composition(X0,X1))),
inference(forward_demodulation,[],[f425,f11]) ).
fof(f439,plain,
! [X2,X0,X1] : converse(join(composition(X0,X2),composition(X0,X1))) = composition(converse(join(X2,X1)),converse(X0)),
inference(forward_demodulation,[],[f436,f11]) ).
fof(f441,plain,
! [X2,X0,X1] : converse(join(composition(X0,X2),composition(X0,X1))) = converse(composition(X0,join(X2,X1))),
inference(forward_demodulation,[],[f439,f12]) ).
fof(f454,plain,
! [X2,X0,X1] : join(composition(X0,X1),composition(X0,X2)) = converse(converse(composition(X0,join(X1,X2)))),
inference(superposition,[],[f10,f441]) ).
fof(f466,plain,
! [X2,X0,X1] : composition(X0,join(X1,X2)) = join(composition(X0,X1),composition(X0,X2)),
inference(forward_demodulation,[],[f454,f10]) ).
fof(f487,plain,
! [X0,X1] : composition(X0,join(one,X1)) = join(X0,composition(X0,X1)),
inference(superposition,[],[f466,f8]) ).
fof(f491,plain,
! [X0,X1] : composition(X0,join(X1,one)) = join(composition(X0,X1),X0),
inference(superposition,[],[f466,f8]) ).
fof(f500,plain,
! [X2,X3,X0,X1] : join(composition(X0,join(X1,X2)),X3) = join(composition(X0,X1),join(composition(X0,X2),X3)),
inference(superposition,[],[f2,f466]) ).
fof(f509,plain,
! [X0,X1] : join(X0,composition(X0,X1)) = composition(X0,join(X1,one)),
inference(forward_demodulation,[],[f491,f1]) ).
fof(f513,plain,
( ! [X0,X1] : complement(X1) = join(complement(join(X0,X1)),complement(join(complement(X0),X1)))
| ~ spl10_13 ),
inference(superposition,[],[f324,f1]) ).
fof(f530,plain,
( ! [X0] : complement(X0) = join(complement(join(X0,sF0)),complement(join(sF1,X0)))
| ~ spl10_7
| ~ spl10_13 ),
inference(superposition,[],[f324,f121]) ).
fof(f539,plain,
( ! [X0,X1] : join(X0,X1) = join(complement(complement(X0)),complement(join(complement(join(X0,X1)),join(complement(X1),X0))))
| ~ spl10_13 ),
inference(superposition,[],[f4,f324]) ).
fof(f548,plain,
( ! [X0,X1] : join(X0,X1) = join(complement(complement(X0)),complement(join(X0,join(complement(join(X0,X1)),complement(X1)))))
| ~ spl10_13 ),
inference(forward_demodulation,[],[f539,f208]) ).
fof(f566,plain,
( ! [X0,X1] : join(X0,X1) = join(complement(complement(X0)),complement(join(X0,join(complement(X1),complement(join(X0,X1))))))
| ~ spl10_13 ),
inference(forward_demodulation,[],[f548,f1]) ).
fof(f581,plain,
( ! [X0,X1] : join(X0,X1) = join(X0,complement(join(X0,join(complement(X1),complement(join(X0,X1))))))
| ~ spl10_13 ),
inference(forward_demodulation,[],[f566,f306]) ).
fof(f699,plain,
( ! [X0,X1] : join(X1,complement(join(complement(X0),X1))) = join(complement(join(complement(X1),X0)),complement(complement(X0)))
| ~ spl10_13 ),
inference(superposition,[],[f211,f324]) ).
fof(f714,plain,
( ! [X0,X1] : join(X1,complement(join(complement(X0),X1))) = join(complement(complement(X0)),complement(join(complement(X1),X0)))
| ~ spl10_13 ),
inference(forward_demodulation,[],[f699,f1]) ).
fof(f745,plain,
( ! [X0,X1] : join(X1,complement(join(complement(X0),X1))) = join(X0,complement(join(complement(X1),X0)))
| ~ spl10_13 ),
inference(forward_demodulation,[],[f714,f306]) ).
fof(f783,definition,
( spl10_14
<=> sk2 = complement(sF6) ),
introduced(definition,[new_symbols(definition,[spl10_14])],[avatar_definition]) ).
fof(f785,plain,
( sk2 = complement(sF6)
| ~ spl10_14 ),
inference(avatar_component_clause,[],[f783]) ).
fof(f786,plain,
( spl10_14
| ~ spl10_6
| ~ spl10_13 ),
inference(avatar_split_clause,[],[f315,f250,f110,f783]) ).
fof(f790,plain,
! [X0] : converse(converse(X0)) = composition(converse(one),X0),
inference(superposition,[],[f414,f8]) ).
fof(f808,plain,
! [X0] : composition(converse(one),X0) = X0,
inference(forward_demodulation,[],[f790,f10]) ).
fof(f826,plain,
! [X0] : complement(X0) = join(complement(X0),composition(one,complement(X0))),
inference(superposition,[],[f149,f808]) ).
fof(f829,plain,
! [X0,X1] : composition(join(converse(one),X1),X0) = join(X0,composition(X1,X0)),
inference(superposition,[],[f9,f808]) ).
fof(f835,plain,
one = converse(one),
inference(superposition,[],[f8,f808]) ).
fof(f838,plain,
! [X0] : composition(one,X0) = X0,
inference(backward_demodulation,[],[f808,f835]) ).
fof(f845,plain,
! [X0,X1] : join(X0,composition(X1,X0)) = composition(join(one,X1),X0),
inference(forward_demodulation,[],[f829,f835]) ).
fof(f851,plain,
! [X0] : complement(X0) = join(complement(X0),complement(X0)),
inference(backward_demodulation,[],[f826,f838]) ).
fof(f872,plain,
( ! [X0] : join(X0,X0) = X0
| ~ spl10_13 ),
inference(superposition,[],[f851,f306]) ).
fof(f883,plain,
( ! [X0] : complement(complement(X0)) = join(complement(complement(X0)),complement(join(complement(X0),complement(complement(X0)))))
| ~ spl10_13 ),
inference(superposition,[],[f329,f851]) ).
fof(f885,plain,
( ! [X0] : complement(complement(X0)) = join(X0,complement(join(complement(complement(complement(X0))),X0)))
| ~ spl10_13 ),
inference(forward_demodulation,[],[f883,f745]) ).
fof(f896,plain,
( ! [X0] : complement(complement(X0)) = join(X0,complement(join(X0,complement(complement(complement(X0))))))
| ~ spl10_13 ),
inference(forward_demodulation,[],[f885,f1]) ).
fof(f903,plain,
( ! [X0] : complement(complement(X0)) = join(X0,complement(join(X0,complement(X0))))
| ~ spl10_13 ),
inference(forward_demodulation,[],[f896,f306]) ).
fof(f909,plain,
( ! [X0] : complement(complement(X0)) = join(X0,complement(top))
| ~ spl10_13 ),
inference(forward_demodulation,[],[f903,f15]) ).
fof(f915,plain,
( ! [X0] : complement(complement(X0)) = join(X0,zero)
| ~ spl10_13 ),
inference(forward_demodulation,[],[f909,f252]) ).
fof(f921,plain,
( ! [X0] : join(X0,zero) = X0
| ~ spl10_13 ),
inference(forward_demodulation,[],[f915,f306]) ).
fof(f954,plain,
( ! [X0] : join(zero,X0) = X0
| ~ spl10_13 ),
inference(superposition,[],[f1,f921]) ).
fof(f956,plain,
( ! [X0] : complement(zero) = join(complement(join(zero,X0)),complement(complement(X0)))
| ~ spl10_13 ),
inference(superposition,[],[f324,f921]) ).
fof(f959,plain,
( ! [X0] : complement(zero) = join(complement(complement(X0)),complement(join(zero,X0)))
| ~ spl10_13 ),
inference(forward_demodulation,[],[f956,f1]) ).
fof(f960,plain,
( zero = composition(converse(sF0),sF1)
| ~ spl10_1
| ~ spl10_7
| ~ spl10_13 ),
inference(backward_demodulation,[],[f152,f954]) ).
fof(f962,plain,
( ! [X0] : join(complement(complement(X0)),complement(X0)) = complement(zero)
| ~ spl10_13 ),
inference(forward_demodulation,[],[f959,f954]) ).
fof(f963,plain,
( ! [X0] : join(complement(X0),complement(complement(X0))) = complement(zero)
| ~ spl10_13 ),
inference(forward_demodulation,[],[f962,f1]) ).
fof(f964,plain,
( top = complement(zero)
| ~ spl10_13 ),
inference(forward_demodulation,[],[f963,f15]) ).
fof(f973,plain,
( ! [X0,X1] : join(X0,X1) = join(X0,join(X0,X1))
| ~ spl10_13 ),
inference(superposition,[],[f2,f872]) ).
fof(f1007,definition,
( spl10_16
<=> sF0 = complement(sF1) ),
introduced(definition,[new_symbols(definition,[spl10_16])],[avatar_definition]) ).
fof(f1009,plain,
( sF0 = complement(sF1)
| ~ spl10_16 ),
inference(avatar_component_clause,[],[f1007]) ).
fof(f1010,plain,
( spl10_16
| ~ spl10_7
| ~ spl10_13 ),
inference(avatar_split_clause,[],[f316,f250,f119,f1007]) ).
fof(f1047,plain,
( complement(sF1) = join(complement(sF3),complement(join(sF1,complement(sF2))))
| ~ spl10_11
| ~ spl10_13 ),
inference(superposition,[],[f337,f232]) ).
fof(f1069,plain,
( ! [X0,X1] : complement(complement(join(X0,complement(X1)))) = join(complement(join(complement(join(X0,complement(X1))),join(X1,X0))),complement(complement(X0)))
| ~ spl10_13 ),
inference(superposition,[],[f324,f337]) ).
fof(f1079,plain,
( ! [X0,X1] : complement(complement(join(X0,complement(X1)))) = join(complement(complement(X0)),complement(join(complement(join(X0,complement(X1))),join(X1,X0))))
| ~ spl10_13 ),
inference(forward_demodulation,[],[f1069,f1]) ).
fof(f1092,plain,
( complement(sF1) = join(complement(sF3),complement(join(sF1,one)))
| ~ spl10_11
| ~ spl10_12
| ~ spl10_13 ),
inference(forward_demodulation,[],[f1047,f314]) ).
fof(f1106,plain,
( ! [X0,X1] : complement(complement(join(X0,complement(X1)))) = join(complement(complement(X0)),complement(join(join(X1,X0),complement(join(X0,complement(X1))))))
| ~ spl10_13 ),
inference(forward_demodulation,[],[f1079,f1]) ).
fof(f1118,plain,
( complement(sF1) = join(sF4,complement(join(sF1,one)))
| ~ spl10_9
| ~ spl10_11
| ~ spl10_12
| ~ spl10_13 ),
inference(forward_demodulation,[],[f1092,f172]) ).
fof(f1131,plain,
( ! [X0,X1] : complement(complement(join(X0,complement(X1)))) = join(complement(complement(X0)),complement(join(X1,join(X0,complement(join(X0,complement(X1)))))))
| ~ spl10_13 ),
inference(forward_demodulation,[],[f1106,f2]) ).
fof(f1140,plain,
( sF0 = join(sF4,complement(join(sF1,one)))
| ~ spl10_9
| ~ spl10_11
| ~ spl10_12
| ~ spl10_13
| ~ spl10_16 ),
inference(forward_demodulation,[],[f1118,f1009]) ).
fof(f1150,plain,
( ! [X0,X1] : complement(complement(join(X0,complement(X1)))) = join(X0,complement(join(X1,join(X0,complement(join(X0,complement(X1)))))))
| ~ spl10_13 ),
inference(forward_demodulation,[],[f1131,f306]) ).
fof(f1162,plain,
( ! [X0,X1] : join(X0,complement(X1)) = join(X0,complement(join(X1,join(X0,complement(join(X0,complement(X1)))))))
| ~ spl10_13 ),
inference(forward_demodulation,[],[f1150,f306]) ).
fof(f1209,plain,
( ! [X0,X1] : join(top,complement(join(X0,complement(X1)))) = join(join(X1,X0),complement(X0))
| ~ spl10_13 ),
inference(superposition,[],[f197,f337]) ).
fof(f1211,plain,
( ! [X0] : join(X0,complement(X0)) = join(top,complement(X0))
| ~ spl10_13 ),
inference(superposition,[],[f197,f872]) ).
fof(f1235,plain,
( ! [X0] : top = join(top,complement(X0))
| ~ spl10_13 ),
inference(forward_demodulation,[],[f1211,f15]) ).
fof(f1237,plain,
( ! [X0,X1] : join(top,complement(join(X0,complement(X1)))) = join(X1,join(X0,complement(X0)))
| ~ spl10_13 ),
inference(forward_demodulation,[],[f1209,f2]) ).
fof(f1252,plain,
( ! [X0,X1] : join(top,complement(join(X0,complement(X1)))) = join(X1,top)
| ~ spl10_13 ),
inference(forward_demodulation,[],[f1237,f15]) ).
fof(f1258,plain,
( ! [X1] : top = join(X1,top)
| ~ spl10_13 ),
inference(forward_demodulation,[],[f1252,f1235]) ).
fof(f1470,plain,
( ! [X0,X1] : join(X0,X1) = join(X1,join(X0,X1))
| ~ spl10_13 ),
inference(superposition,[],[f973,f1]) ).
fof(f1478,plain,
( ! [X0,X1] : complement(X0) = join(complement(join(X0,X1)),complement(X0))
| ~ spl10_13 ),
inference(superposition,[],[f973,f329]) ).
fof(f1479,plain,
( ! [X0,X1] : complement(X0) = join(complement(join(X1,X0)),complement(X0))
| ~ spl10_13 ),
inference(superposition,[],[f973,f337]) ).
fof(f1521,plain,
( ! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X1,X0)))
| ~ spl10_13 ),
inference(forward_demodulation,[],[f1479,f1]) ).
fof(f1522,plain,
( ! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X0,X1)))
| ~ spl10_13 ),
inference(forward_demodulation,[],[f1478,f1]) ).
fof(f1532,plain,
( ! [X0,X1] : join(X0,X1) = join(X0,complement(join(X0,complement(X1))))
| ~ spl10_13 ),
inference(backward_demodulation,[],[f581,f1521]) ).
fof(f1536,plain,
( ! [X0,X1] : join(X0,complement(X1)) = join(X0,complement(join(X1,join(X0,X1))))
| ~ spl10_13 ),
inference(backward_demodulation,[],[f1162,f1532]) ).
fof(f1542,plain,
( ! [X0,X1] : join(X0,complement(X1)) = join(X0,complement(join(X0,X1)))
| ~ spl10_13 ),
inference(forward_demodulation,[],[f1536,f1470]) ).
fof(f1589,plain,
( complement(sF2) = join(complement(sF2),complement(sF3))
| ~ spl10_11
| ~ spl10_13 ),
inference(superposition,[],[f1522,f232]) ).
fof(f1615,plain,
( complement(sF2) = join(complement(sF2),sF4)
| ~ spl10_9
| ~ spl10_11
| ~ spl10_13 ),
inference(forward_demodulation,[],[f1589,f172]) ).
fof(f1628,plain,
( complement(sF2) = join(sF4,complement(sF2))
| ~ spl10_9
| ~ spl10_11
| ~ spl10_13 ),
inference(forward_demodulation,[],[f1615,f1]) ).
fof(f1638,plain,
( one = join(sF4,one)
| ~ spl10_9
| ~ spl10_11
| ~ spl10_12
| ~ spl10_13 ),
inference(forward_demodulation,[],[f1628,f314]) ).
fof(f1653,plain,
( ! [X0,X1] : join(X1,complement(X0)) = join(X1,complement(join(X0,X1)))
| ~ spl10_13 ),
inference(superposition,[],[f1542,f1]) ).
fof(f1824,plain,
( join(sF1,complement(sF2)) = join(sF1,complement(sF3))
| ~ spl10_11
| ~ spl10_13 ),
inference(superposition,[],[f1653,f232]) ).
fof(f1873,plain,
( join(sF1,complement(sF2)) = join(sF1,sF4)
| ~ spl10_9
| ~ spl10_11
| ~ spl10_13 ),
inference(forward_demodulation,[],[f1824,f172]) ).
fof(f1902,plain,
( join(sF1,complement(sF2)) = join(sF4,sF1)
| ~ spl10_9
| ~ spl10_11
| ~ spl10_13 ),
inference(forward_demodulation,[],[f1873,f1]) ).
fof(f1922,plain,
( join(sF1,one) = join(sF4,sF1)
| ~ spl10_9
| ~ spl10_11
| ~ spl10_12
| ~ spl10_13 ),
inference(forward_demodulation,[],[f1902,f314]) ).
fof(f1935,plain,
( sF0 = join(sF4,complement(join(sF4,sF1)))
| ~ spl10_9
| ~ spl10_11
| ~ spl10_12
| ~ spl10_13
| ~ spl10_16 ),
inference(backward_demodulation,[],[f1140,f1922]) ).
fof(f1945,plain,
( sF0 = join(sF4,complement(sF1))
| ~ spl10_9
| ~ spl10_11
| ~ spl10_12
| ~ spl10_13
| ~ spl10_16 ),
inference(forward_demodulation,[],[f1935,f1542]) ).
fof(f1954,plain,
( sF0 = join(sF4,sF0)
| ~ spl10_9
| ~ spl10_11
| ~ spl10_12
| ~ spl10_13
| ~ spl10_16 ),
inference(forward_demodulation,[],[f1945,f1009]) ).
fof(f2012,plain,
( ! [X0] : converse(converse(X0)) = join(X0,converse(zero))
| ~ spl10_13 ),
inference(superposition,[],[f185,f921]) ).
fof(f2025,plain,
( ! [X0] : join(X0,converse(zero)) = X0
| ~ spl10_13 ),
inference(forward_demodulation,[],[f2012,f10]) ).
fof(f2478,definition,
( spl10_18
<=> one = join(sF4,one) ),
introduced(definition,[new_symbols(definition,[spl10_18])],[avatar_definition]) ).
fof(f2480,plain,
( one = join(sF4,one)
| ~ spl10_18 ),
inference(avatar_component_clause,[],[f2478]) ).
fof(f2481,plain,
( spl10_18
| ~ spl10_9
| ~ spl10_11
| ~ spl10_12
| ~ spl10_13 ),
inference(avatar_split_clause,[],[f1638,f250,f236,f230,f170,f2478]) ).
fof(f2552,plain,
( complement(sF5) = join(complement(sF5),complement(sF9))
| ~ spl10_5
| ~ spl10_13 ),
inference(superposition,[],[f1521,f89]) ).
fof(f2581,plain,
( complement(sF5) = join(complement(sF9),complement(sF5))
| ~ spl10_5
| ~ spl10_13 ),
inference(forward_demodulation,[],[f2552,f1]) ).
fof(f2877,definition,
( spl10_20
<=> zero = composition(converse(sF0),sF1) ),
introduced(definition,[new_symbols(definition,[spl10_20])],[avatar_definition]) ).
fof(f2879,plain,
( zero = composition(converse(sF0),sF1)
| ~ spl10_20 ),
inference(avatar_component_clause,[],[f2877]) ).
fof(f2880,plain,
( spl10_20
| ~ spl10_1
| ~ spl10_7
| ~ spl10_13 ),
inference(avatar_split_clause,[],[f960,f250,f119,f51,f2877]) ).
fof(f2915,definition,
( spl10_21
<=> sF7 = complement(sF8) ),
introduced(definition,[new_symbols(definition,[spl10_21])],[avatar_definition]) ).
fof(f2917,plain,
( sF7 = complement(sF8)
| ~ spl10_21 ),
inference(avatar_component_clause,[],[f2915]) ).
fof(f2918,plain,
( spl10_21
| ~ spl10_8
| ~ spl10_13 ),
inference(avatar_split_clause,[],[f318,f250,f154,f2915]) ).
fof(f3439,plain,
( ! [X0] : composition(X0,one) = join(X0,composition(X0,sF4))
| ~ spl10_18 ),
inference(superposition,[],[f509,f2480]) ).
fof(f3503,plain,
( ! [X0] : join(X0,composition(X0,sF4)) = X0
| ~ spl10_18 ),
inference(forward_demodulation,[],[f3439,f8]) ).
fof(f3621,plain,
( ! [X0] : composition(one,X0) = join(X0,composition(composition(one,sF4),X0))
| ~ spl10_18 ),
inference(superposition,[],[f845,f3503]) ).
fof(f3631,plain,
( ! [X0] : composition(one,X0) = join(X0,composition(one,composition(sF4,X0)))
| ~ spl10_18 ),
inference(forward_demodulation,[],[f3621,f7]) ).
fof(f3652,plain,
( ! [X0] : composition(one,X0) = join(X0,composition(sF4,X0))
| ~ spl10_18 ),
inference(forward_demodulation,[],[f3631,f838]) ).
fof(f3660,plain,
( ! [X0] : join(X0,composition(sF4,X0)) = X0
| ~ spl10_18 ),
inference(forward_demodulation,[],[f3652,f838]) ).
fof(f3665,definition,
( spl10_24
<=> top = join(sF1,sF0) ),
introduced(definition,[new_symbols(definition,[spl10_24])],[avatar_definition]) ).
fof(f3667,plain,
( top = join(sF1,sF0)
| ~ spl10_24 ),
inference(avatar_component_clause,[],[f3665]) ).
fof(f3668,plain,
( spl10_24
| ~ spl10_7 ),
inference(avatar_split_clause,[],[f133,f119,f3665]) ).
fof(f3971,plain,
( complement(converse(converse(sF0))) = join(complement(converse(converse(sF0))),composition(sF1,complement(converse(zero))))
| ~ spl10_20 ),
inference(superposition,[],[f419,f2879]) ).
fof(f4012,plain,
( complement(sF0) = join(complement(sF0),composition(sF1,complement(converse(zero))))
| ~ spl10_20 ),
inference(forward_demodulation,[],[f3971,f10]) ).
fof(f4027,plain,
( sF1 = join(sF1,composition(sF1,complement(converse(zero))))
| ~ spl10_7
| ~ spl10_20 ),
inference(forward_demodulation,[],[f4012,f121]) ).
fof(f4035,plain,
( sF1 = composition(sF1,join(one,complement(converse(zero))))
| ~ spl10_7
| ~ spl10_20 ),
inference(forward_demodulation,[],[f4027,f487]) ).
fof(f4038,definition,
( spl10_25
<=> join(sF1,one) = join(sF4,sF1) ),
introduced(definition,[new_symbols(definition,[spl10_25])],[avatar_definition]) ).
fof(f4040,plain,
( join(sF1,one) = join(sF4,sF1)
| ~ spl10_25 ),
inference(avatar_component_clause,[],[f4038]) ).
fof(f4041,plain,
( spl10_25
| ~ spl10_9
| ~ spl10_11
| ~ spl10_12
| ~ spl10_13 ),
inference(avatar_split_clause,[],[f1922,f250,f236,f230,f170,f4038]) ).
fof(f4976,definition,
( spl10_27
<=> top = complement(zero) ),
introduced(definition,[new_symbols(definition,[spl10_27])],[avatar_definition]) ).
fof(f4978,plain,
( top = complement(zero)
| ~ spl10_27 ),
inference(avatar_component_clause,[],[f4976]) ).
fof(f4979,plain,
( spl10_27
| ~ spl10_13 ),
inference(avatar_split_clause,[],[f964,f250,f4976]) ).
fof(f5103,plain,
! [X2,X3,X0,X1] : join(composition(X0,join(X3,X2)),composition(X1,X2)) = join(composition(X0,X3),composition(join(X0,X1),X2)),
inference(superposition,[],[f500,f9]) ).
fof(f5292,plain,
( ! [X0,X1] : join(X1,X0) = join(X0,join(composition(sF4,X0),X1))
| ~ spl10_18 ),
inference(superposition,[],[f208,f3660]) ).
fof(f5305,plain,
( ! [X0] : complement(composition(sF4,complement(X0))) = join(complement(join(X0,composition(sF4,complement(X0)))),complement(complement(X0)))
| ~ spl10_13
| ~ spl10_18 ),
inference(superposition,[],[f513,f3660]) ).
fof(f5329,plain,
( ! [X0] : complement(composition(sF4,complement(X0))) = join(complement(complement(X0)),complement(join(X0,composition(sF4,complement(X0)))))
| ~ spl10_13
| ~ spl10_18 ),
inference(forward_demodulation,[],[f5305,f1]) ).
fof(f5351,plain,
( ! [X0] : complement(composition(sF4,complement(X0))) = join(X0,complement(join(X0,composition(sF4,complement(X0)))))
| ~ spl10_13
| ~ spl10_18 ),
inference(forward_demodulation,[],[f5329,f306]) ).
fof(f5357,plain,
( ! [X0] : complement(composition(sF4,complement(X0))) = join(X0,complement(composition(sF4,complement(X0))))
| ~ spl10_13
| ~ spl10_18 ),
inference(forward_demodulation,[],[f5351,f1542]) ).
fof(f5364,plain,
( ! [X0,X1] : join(composition(sF4,X1),X0) = join(X0,composition(sF4,join(X0,X1)))
| ~ spl10_18 ),
inference(superposition,[],[f5292,f466]) ).
fof(f5521,plain,
( ! [X0,X1] : join(composition(sF4,X0),X1) = join(X1,composition(sF4,join(X0,X1)))
| ~ spl10_18 ),
inference(superposition,[],[f5364,f1]) ).
fof(f5528,plain,
( ! [X0] : join(composition(sF4,complement(X0)),X0) = join(X0,composition(sF4,top))
| ~ spl10_18 ),
inference(superposition,[],[f5364,f15]) ).
fof(f5685,plain,
( ! [X0] : join(X0,composition(sF4,complement(X0))) = join(X0,composition(sF4,top))
| ~ spl10_18 ),
inference(forward_demodulation,[],[f5528,f1]) ).
fof(f5807,plain,
( join(composition(sF4,sF1),sF0) = join(sF0,composition(sF4,top))
| ~ spl10_18
| ~ spl10_24 ),
inference(superposition,[],[f5521,f3667]) ).
fof(f5902,plain,
( join(composition(sF4,sF1),sF0) = composition(join(sF0,sF4),top)
| ~ spl10_1
| ~ spl10_18
| ~ spl10_24 ),
inference(forward_demodulation,[],[f5807,f74]) ).
fof(f5953,plain,
( join(composition(sF4,sF1),sF0) = composition(join(sF4,sF0),top)
| ~ spl10_1
| ~ spl10_18
| ~ spl10_24 ),
inference(forward_demodulation,[],[f5902,f64]) ).
fof(f5981,plain,
( composition(sF0,top) = join(composition(sF4,sF1),sF0)
| ~ spl10_1
| ~ spl10_9
| ~ spl10_11
| ~ spl10_12
| ~ spl10_13
| ~ spl10_16
| ~ spl10_18
| ~ spl10_24 ),
inference(forward_demodulation,[],[f5953,f1954]) ).
fof(f5992,plain,
( composition(sF0,top) = join(sF0,composition(sF4,sF1))
| ~ spl10_1
| ~ spl10_9
| ~ spl10_11
| ~ spl10_12
| ~ spl10_13
| ~ spl10_16
| ~ spl10_18
| ~ spl10_24 ),
inference(forward_demodulation,[],[f5981,f1]) ).
fof(f5996,plain,
( sF0 = join(sF0,composition(sF4,sF1))
| ~ spl10_1
| ~ spl10_9
| ~ spl10_11
| ~ spl10_12
| ~ spl10_13
| ~ spl10_16
| ~ spl10_18
| ~ spl10_24 ),
inference(forward_demodulation,[],[f5992,f53]) ).
fof(f6130,plain,
( join(sF7,composition(sF4,top)) = join(sF7,composition(sF4,sF8))
| ~ spl10_8
| ~ spl10_18 ),
inference(superposition,[],[f5685,f156]) ).
fof(f6190,plain,
( ! [X0] : join(X0,complement(join(X0,composition(sF4,complement(X0))))) = join(X0,complement(composition(sF4,top)))
| ~ spl10_13
| ~ spl10_18 ),
inference(superposition,[],[f1542,f5685]) ).
fof(f6196,plain,
( ! [X0] : join(X0,complement(composition(sF4,complement(X0)))) = join(X0,complement(composition(sF4,top)))
| ~ spl10_13
| ~ spl10_18 ),
inference(forward_demodulation,[],[f6190,f1542]) ).
fof(f6240,plain,
( ! [X0] : complement(composition(sF4,complement(X0))) = join(X0,complement(composition(sF4,top)))
| ~ spl10_13
| ~ spl10_18 ),
inference(forward_demodulation,[],[f6196,f5357]) ).
fof(f6342,plain,
( complement(composition(sF4,sF1)) = join(complement(join(composition(sF4,sF1),sF0)),complement(sF1))
| ~ spl10_7
| ~ spl10_13
| ~ spl10_18 ),
inference(superposition,[],[f530,f3660]) ).
fof(f6405,plain,
( complement(composition(sF4,sF1)) = join(complement(sF1),complement(join(composition(sF4,sF1),sF0)))
| ~ spl10_7
| ~ spl10_13
| ~ spl10_18 ),
inference(forward_demodulation,[],[f6342,f1]) ).
fof(f6456,plain,
( complement(composition(sF4,sF1)) = join(complement(sF1),complement(join(sF0,composition(sF4,sF1))))
| ~ spl10_7
| ~ spl10_13
| ~ spl10_18 ),
inference(forward_demodulation,[],[f6405,f1]) ).
fof(f6498,plain,
( complement(composition(sF4,sF1)) = join(complement(sF1),complement(sF0))
| ~ spl10_1
| ~ spl10_7
| ~ spl10_9
| ~ spl10_11
| ~ spl10_12
| ~ spl10_13
| ~ spl10_16
| ~ spl10_18
| ~ spl10_24 ),
inference(forward_demodulation,[],[f6456,f5996]) ).
fof(f6527,plain,
( complement(composition(sF4,sF1)) = join(complement(sF1),sF1)
| ~ spl10_1
| ~ spl10_7
| ~ spl10_9
| ~ spl10_11
| ~ spl10_12
| ~ spl10_13
| ~ spl10_16
| ~ spl10_18
| ~ spl10_24 ),
inference(forward_demodulation,[],[f6498,f121]) ).
fof(f6554,plain,
( join(sF1,complement(sF1)) = complement(composition(sF4,sF1))
| ~ spl10_1
| ~ spl10_7
| ~ spl10_9
| ~ spl10_11
| ~ spl10_12
| ~ spl10_13
| ~ spl10_16
| ~ spl10_18
| ~ spl10_24 ),
inference(forward_demodulation,[],[f6527,f1]) ).
fof(f6577,plain,
( top = complement(composition(sF4,sF1))
| ~ spl10_1
| ~ spl10_7
| ~ spl10_9
| ~ spl10_11
| ~ spl10_12
| ~ spl10_13
| ~ spl10_16
| ~ spl10_18
| ~ spl10_24 ),
inference(forward_demodulation,[],[f6554,f15]) ).
fof(f6625,definition,
( spl10_28
<=> top = complement(composition(sF4,sF1)) ),
introduced(definition,[new_symbols(definition,[spl10_28])],[avatar_definition]) ).
fof(f6627,plain,
( top = complement(composition(sF4,sF1))
| ~ spl10_28 ),
inference(avatar_component_clause,[],[f6625]) ).
fof(f6628,plain,
( spl10_28
| ~ spl10_1
| ~ spl10_7
| ~ spl10_9
| ~ spl10_11
| ~ spl10_12
| ~ spl10_13
| ~ spl10_16
| ~ spl10_18
| ~ spl10_24 ),
inference(avatar_split_clause,[],[f6577,f3665,f2478,f1007,f250,f236,f230,f170,f119,f51,f6625]) ).
fof(f6635,plain,
( complement(top) = composition(sF4,sF1)
| ~ spl10_13
| ~ spl10_28 ),
inference(superposition,[],[f306,f6627]) ).
fof(f6652,plain,
( zero = composition(sF4,sF1)
| ~ spl10_13
| ~ spl10_28 ),
inference(forward_demodulation,[],[f6635,f252]) ).
fof(f6716,definition,
( spl10_29
<=> zero = composition(sF4,sF1) ),
introduced(definition,[new_symbols(definition,[spl10_29])],[avatar_definition]) ).
fof(f6718,plain,
( zero = composition(sF4,sF1)
| ~ spl10_29 ),
inference(avatar_component_clause,[],[f6716]) ).
fof(f6719,plain,
( spl10_29
| ~ spl10_13
| ~ spl10_28 ),
inference(avatar_split_clause,[],[f6652,f6625,f250,f6716]) ).
fof(f6729,plain,
( ! [X0] : join(composition(sF4,X0),zero) = composition(sF4,join(X0,sF1))
| ~ spl10_29 ),
inference(superposition,[],[f466,f6718]) ).
fof(f6744,plain,
( ! [X0] : join(zero,composition(sF4,X0)) = composition(sF4,join(X0,sF1))
| ~ spl10_29 ),
inference(forward_demodulation,[],[f6729,f1]) ).
fof(f6757,plain,
( ! [X0] : composition(sF4,X0) = composition(sF4,join(X0,sF1))
| ~ spl10_13
| ~ spl10_29 ),
inference(forward_demodulation,[],[f6744,f954]) ).
fof(f7182,plain,
! [X2,X0,X1] : join(composition(X0,X1),composition(join(X0,X2),complement(X1))) = join(composition(X0,top),composition(X2,complement(X1))),
inference(superposition,[],[f5103,f15]) ).
fof(f7643,plain,
! [X2,X0,X1] : join(composition(X1,top),composition(X0,complement(X2))) = join(composition(X1,X2),composition(join(X0,X1),complement(X2))),
inference(superposition,[],[f7182,f1]) ).
fof(f7695,plain,
( ! [X0] : join(composition(sF1,top),composition(one,complement(X0))) = join(composition(sF1,X0),composition(join(sF4,sF1),complement(X0)))
| ~ spl10_25 ),
inference(superposition,[],[f7182,f4040]) ).
fof(f7807,plain,
( ! [X0] : join(composition(sF1,X0),composition(join(sF4,sF1),complement(X0))) = join(composition(sF1,top),complement(X0))
| ~ spl10_25 ),
inference(forward_demodulation,[],[f7695,f838]) ).
fof(f7876,plain,
( ! [X0] : join(composition(sF1,top),complement(X0)) = join(composition(sF1,top),composition(sF4,complement(X0)))
| ~ spl10_25 ),
inference(forward_demodulation,[],[f7807,f7643]) ).
fof(f8548,plain,
( complement(complement(composition(sF4,top))) = join(complement(join(complement(composition(sF4,top)),sF0)),complement(complement(composition(sF4,complement(sF1)))))
| ~ spl10_7
| ~ spl10_13
| ~ spl10_18 ),
inference(superposition,[],[f530,f6240]) ).
fof(f8550,plain,
( join(sF7,complement(composition(sF4,top))) = join(sF6,complement(composition(sF4,complement(sF1))))
| ~ spl10_10
| ~ spl10_13
| ~ spl10_18 ),
inference(superposition,[],[f228,f6240]) ).
fof(f8555,plain,
( join(sF7,complement(composition(sF4,top))) = join(sF6,complement(composition(sF4,sF0)))
| ~ spl10_10
| ~ spl10_13
| ~ spl10_16
| ~ spl10_18 ),
inference(forward_demodulation,[],[f8550,f1009]) ).
fof(f8557,plain,
( complement(complement(composition(sF4,top))) = join(complement(complement(composition(sF4,complement(sF1)))),complement(join(complement(composition(sF4,top)),sF0)))
| ~ spl10_7
| ~ spl10_13
| ~ spl10_18 ),
inference(forward_demodulation,[],[f8548,f1]) ).
fof(f8593,plain,
( join(sF6,complement(composition(sF4,sF0))) = complement(composition(sF4,complement(sF7)))
| ~ spl10_10
| ~ spl10_13
| ~ spl10_16
| ~ spl10_18 ),
inference(forward_demodulation,[],[f8555,f6240]) ).
fof(f8595,plain,
( complement(complement(composition(sF4,top))) = join(complement(complement(composition(sF4,complement(sF1)))),complement(join(sF0,complement(composition(sF4,top)))))
| ~ spl10_7
| ~ spl10_13
| ~ spl10_18 ),
inference(forward_demodulation,[],[f8557,f1]) ).
fof(f8622,plain,
( join(sF6,complement(composition(sF4,sF0))) = complement(composition(sF4,sF8))
| ~ spl10_8
| ~ spl10_10
| ~ spl10_13
| ~ spl10_16
| ~ spl10_18 ),
inference(forward_demodulation,[],[f8593,f156]) ).
fof(f8624,plain,
( complement(complement(composition(sF4,top))) = join(complement(complement(composition(sF4,complement(sF1)))),complement(complement(composition(sF4,complement(sF0)))))
| ~ spl10_7
| ~ spl10_13
| ~ spl10_18 ),
inference(forward_demodulation,[],[f8595,f6240]) ).
fof(f8637,plain,
( complement(complement(composition(sF4,top))) = join(complement(complement(composition(sF4,complement(sF1)))),composition(sF4,complement(sF0)))
| ~ spl10_7
| ~ spl10_13
| ~ spl10_18 ),
inference(forward_demodulation,[],[f8624,f306]) ).
fof(f8648,plain,
( complement(complement(composition(sF4,top))) = join(composition(sF4,complement(sF0)),complement(complement(composition(sF4,complement(sF1)))))
| ~ spl10_7
| ~ spl10_13
| ~ spl10_18 ),
inference(forward_demodulation,[],[f8637,f1]) ).
fof(f8656,plain,
( complement(complement(composition(sF4,top))) = join(composition(sF4,complement(sF0)),composition(sF4,complement(sF1)))
| ~ spl10_7
| ~ spl10_13
| ~ spl10_18 ),
inference(forward_demodulation,[],[f8648,f306]) ).
fof(f8662,plain,
( complement(complement(composition(sF4,top))) = join(composition(sF4,complement(sF1)),composition(sF4,complement(sF0)))
| ~ spl10_7
| ~ spl10_13
| ~ spl10_18 ),
inference(forward_demodulation,[],[f8656,f1]) ).
fof(f8668,plain,
( complement(complement(composition(sF4,top))) = composition(sF4,join(complement(sF1),complement(sF0)))
| ~ spl10_7
| ~ spl10_13
| ~ spl10_18 ),
inference(forward_demodulation,[],[f8662,f466]) ).
fof(f8670,plain,
( complement(complement(composition(sF4,top))) = composition(sF4,join(complement(sF1),sF1))
| ~ spl10_7
| ~ spl10_13
| ~ spl10_18 ),
inference(forward_demodulation,[],[f8668,f121]) ).
fof(f8672,plain,
( composition(sF4,complement(sF1)) = complement(complement(composition(sF4,top)))
| ~ spl10_7
| ~ spl10_13
| ~ spl10_18
| ~ spl10_29 ),
inference(forward_demodulation,[],[f8670,f6757]) ).
fof(f8673,plain,
( composition(sF4,top) = composition(sF4,complement(sF1))
| ~ spl10_7
| ~ spl10_13
| ~ spl10_18
| ~ spl10_29 ),
inference(forward_demodulation,[],[f8672,f306]) ).
fof(f8674,plain,
( composition(sF4,top) = composition(sF4,sF0)
| ~ spl10_7
| ~ spl10_13
| ~ spl10_16
| ~ spl10_18
| ~ spl10_29 ),
inference(forward_demodulation,[],[f8673,f1009]) ).
fof(f8679,plain,
( complement(composition(sF4,sF8)) = join(sF6,complement(composition(sF4,top)))
| ~ spl10_7
| ~ spl10_8
| ~ spl10_10
| ~ spl10_13
| ~ spl10_16
| ~ spl10_18
| ~ spl10_29 ),
inference(backward_demodulation,[],[f8622,f8674]) ).
fof(f8682,plain,
( complement(composition(sF4,sF8)) = complement(composition(sF4,complement(sF6)))
| ~ spl10_7
| ~ spl10_8
| ~ spl10_10
| ~ spl10_13
| ~ spl10_16
| ~ spl10_18
| ~ spl10_29 ),
inference(forward_demodulation,[],[f8679,f6240]) ).
fof(f8686,plain,
( complement(composition(sF4,sk2)) = complement(composition(sF4,sF8))
| ~ spl10_7
| ~ spl10_8
| ~ spl10_10
| ~ spl10_13
| ~ spl10_14
| ~ spl10_16
| ~ spl10_18
| ~ spl10_29 ),
inference(forward_demodulation,[],[f8682,f785]) ).
fof(f8688,plain,
( complement(sF5) = complement(composition(sF4,sF8))
| ~ spl10_4
| ~ spl10_7
| ~ spl10_8
| ~ spl10_10
| ~ spl10_13
| ~ spl10_14
| ~ spl10_16
| ~ spl10_18
| ~ spl10_29 ),
inference(forward_demodulation,[],[f8686,f80]) ).
fof(f8691,definition,
( spl10_35
<=> complement(sF5) = complement(composition(sF4,sF8)) ),
introduced(definition,[new_symbols(definition,[spl10_35])],[avatar_definition]) ).
fof(f8693,plain,
( complement(sF5) = complement(composition(sF4,sF8))
| ~ spl10_35 ),
inference(avatar_component_clause,[],[f8691]) ).
fof(f8694,plain,
( spl10_35
| ~ spl10_4
| ~ spl10_7
| ~ spl10_8
| ~ spl10_10
| ~ spl10_13
| ~ spl10_14
| ~ spl10_16
| ~ spl10_18
| ~ spl10_29 ),
inference(avatar_split_clause,[],[f8688,f6716,f2478,f1007,f783,f250,f224,f154,f119,f78,f8691]) ).
fof(f8701,plain,
( composition(sF4,sF8) = complement(complement(sF5))
| ~ spl10_13
| ~ spl10_35 ),
inference(superposition,[],[f306,f8693]) ).
fof(f8719,plain,
( sF5 = composition(sF4,sF8)
| ~ spl10_13
| ~ spl10_35 ),
inference(forward_demodulation,[],[f8701,f306]) ).
fof(f8728,plain,
( join(sF7,sF5) = join(sF7,composition(sF4,top))
| ~ spl10_8
| ~ spl10_13
| ~ spl10_18
| ~ spl10_35 ),
inference(backward_demodulation,[],[f6130,f8719]) ).
fof(f8755,definition,
( spl10_36
<=> sF5 = composition(sF4,sF8) ),
introduced(definition,[new_symbols(definition,[spl10_36])],[avatar_definition]) ).
fof(f8757,plain,
( sF5 = composition(sF4,sF8)
| ~ spl10_36 ),
inference(avatar_component_clause,[],[f8755]) ).
fof(f8758,plain,
( spl10_36
| ~ spl10_13
| ~ spl10_35 ),
inference(avatar_split_clause,[],[f8719,f8691,f250,f8755]) ).
fof(f8760,plain,
( sF8 = join(sF8,sF5)
| ~ spl10_18
| ~ spl10_36 ),
inference(superposition,[],[f3660,f8757]) ).
fof(f8788,plain,
( sF8 = sF9
| ~ spl10_5
| ~ spl10_18
| ~ spl10_36 ),
inference(forward_demodulation,[],[f8760,f89]) ).
fof(f8809,plain,
( sF5 != sF8
| spl10_3
| ~ spl10_5
| ~ spl10_18
| ~ spl10_36 ),
inference(backward_demodulation,[],[f71,f8788]) ).
fof(f8817,plain,
( complement(sF5) = join(complement(sF8),complement(sF5))
| ~ spl10_5
| ~ spl10_13
| ~ spl10_18
| ~ spl10_36 ),
inference(backward_demodulation,[],[f2581,f8788]) ).
fof(f8896,plain,
( complement(sF5) = join(sF7,complement(sF5))
| ~ spl10_5
| ~ spl10_13
| ~ spl10_18
| ~ spl10_21
| ~ spl10_36 ),
inference(forward_demodulation,[],[f8817,f2917]) ).
fof(f8929,definition,
( spl10_38
<=> sF5 = sF8 ),
introduced(definition,[new_symbols(definition,[spl10_38])],[avatar_definition]) ).
fof(f8931,plain,
( sF5 != sF8
| spl10_38 ),
inference(avatar_component_clause,[],[f8929]) ).
fof(f8932,plain,
( ~ spl10_38
| spl10_3
| ~ spl10_5
| ~ spl10_18
| ~ spl10_36 ),
inference(avatar_split_clause,[],[f8809,f8755,f2478,f87,f69,f8929]) ).
fof(f9484,plain,
( zero = converse(zero)
| ~ spl10_13 ),
inference(superposition,[],[f954,f2025]) ).
fof(f9496,plain,
( sF1 = composition(sF1,join(one,complement(zero)))
| ~ spl10_7
| ~ spl10_13
| ~ spl10_20 ),
inference(backward_demodulation,[],[f4035,f9484]) ).
fof(f9534,plain,
( sF1 = composition(sF1,join(one,top))
| ~ spl10_7
| ~ spl10_13
| ~ spl10_20
| ~ spl10_27 ),
inference(forward_demodulation,[],[f9496,f4978]) ).
fof(f9556,plain,
( sF1 = composition(sF1,top)
| ~ spl10_7
| ~ spl10_13
| ~ spl10_20
| ~ spl10_27 ),
inference(forward_demodulation,[],[f9534,f1258]) ).
fof(f9571,plain,
( ! [X0] : join(sF1,complement(X0)) = join(sF1,composition(sF4,complement(X0)))
| ~ spl10_7
| ~ spl10_13
| ~ spl10_20
| ~ spl10_25
| ~ spl10_27 ),
inference(backward_demodulation,[],[f7876,f9556]) ).
fof(f9740,plain,
( ! [X0] : join(sF1,X0) = join(sF1,composition(sF4,X0))
| ~ spl10_7
| ~ spl10_13
| ~ spl10_20
| ~ spl10_25
| ~ spl10_27 ),
inference(superposition,[],[f9571,f306]) ).
fof(f9880,plain,
( ! [X0] : join(sF6,join(sF1,X0)) = join(sF7,composition(sF4,X0))
| ~ spl10_7
| ~ spl10_10
| ~ spl10_13
| ~ spl10_20
| ~ spl10_25
| ~ spl10_27 ),
inference(superposition,[],[f228,f9740]) ).
fof(f9924,plain,
( ! [X0] : join(sF7,X0) = join(sF7,composition(sF4,X0))
| ~ spl10_7
| ~ spl10_10
| ~ spl10_13
| ~ spl10_20
| ~ spl10_25
| ~ spl10_27 ),
inference(forward_demodulation,[],[f9880,f228]) ).
fof(f9949,plain,
( join(sF7,sF5) = join(sF7,top)
| ~ spl10_7
| ~ spl10_8
| ~ spl10_10
| ~ spl10_13
| ~ spl10_18
| ~ spl10_20
| ~ spl10_25
| ~ spl10_27
| ~ spl10_35 ),
inference(backward_demodulation,[],[f8728,f9924]) ).
fof(f9965,plain,
( top = join(sF7,sF5)
| ~ spl10_7
| ~ spl10_8
| ~ spl10_10
| ~ spl10_13
| ~ spl10_18
| ~ spl10_20
| ~ spl10_25
| ~ spl10_27
| ~ spl10_35 ),
inference(forward_demodulation,[],[f9949,f1258]) ).
fof(f9974,definition,
( spl10_44
<=> top = join(sF7,sF5) ),
introduced(definition,[new_symbols(definition,[spl10_44])],[avatar_definition]) ).
fof(f9976,plain,
( top = join(sF7,sF5)
| ~ spl10_44 ),
inference(avatar_component_clause,[],[f9974]) ).
fof(f9977,plain,
( spl10_44
| ~ spl10_7
| ~ spl10_8
| ~ spl10_10
| ~ spl10_13
| ~ spl10_18
| ~ spl10_20
| ~ spl10_25
| ~ spl10_27
| ~ spl10_35 ),
inference(avatar_split_clause,[],[f9965,f8691,f4976,f4038,f2877,f2478,f250,f224,f154,f119,f9974]) ).
fof(f9981,plain,
( complement(sF7) = join(complement(top),complement(join(complement(sF5),sF7)))
| ~ spl10_13
| ~ spl10_44 ),
inference(superposition,[],[f324,f9976]) ).
fof(f10006,plain,
( complement(sF7) = join(complement(top),complement(join(sF7,complement(sF5))))
| ~ spl10_13
| ~ spl10_44 ),
inference(forward_demodulation,[],[f9981,f1]) ).
fof(f10018,plain,
( complement(sF7) = join(complement(top),complement(complement(sF5)))
| ~ spl10_5
| ~ spl10_13
| ~ spl10_18
| ~ spl10_21
| ~ spl10_36
| ~ spl10_44 ),
inference(forward_demodulation,[],[f10006,f8896]) ).
fof(f10028,plain,
( complement(sF7) = join(complement(top),sF5)
| ~ spl10_5
| ~ spl10_13
| ~ spl10_18
| ~ spl10_21
| ~ spl10_36
| ~ spl10_44 ),
inference(forward_demodulation,[],[f10018,f306]) ).
fof(f10037,plain,
( complement(sF7) = join(sF5,complement(top))
| ~ spl10_5
| ~ spl10_13
| ~ spl10_18
| ~ spl10_21
| ~ spl10_36
| ~ spl10_44 ),
inference(forward_demodulation,[],[f10028,f1]) ).
fof(f10061,plain,
( complement(sF7) = join(sF5,zero)
| ~ spl10_5
| ~ spl10_13
| ~ spl10_18
| ~ spl10_21
| ~ spl10_36
| ~ spl10_44 ),
inference(forward_demodulation,[],[f10037,f252]) ).
fof(f10073,plain,
( complement(sF7) = join(zero,sF5)
| ~ spl10_5
| ~ spl10_13
| ~ spl10_18
| ~ spl10_21
| ~ spl10_36
| ~ spl10_44 ),
inference(forward_demodulation,[],[f10061,f1]) ).
fof(f10085,plain,
( sF5 = complement(sF7)
| ~ spl10_5
| ~ spl10_13
| ~ spl10_18
| ~ spl10_21
| ~ spl10_36
| ~ spl10_44 ),
inference(forward_demodulation,[],[f10073,f954]) ).
fof(f10091,plain,
( sF5 = sF8
| ~ spl10_5
| ~ spl10_8
| ~ spl10_13
| ~ spl10_18
| ~ spl10_21
| ~ spl10_36
| ~ spl10_44 ),
inference(forward_demodulation,[],[f10085,f156]) ).
fof(f10093,plain,
( $false
| ~ spl10_5
| ~ spl10_8
| ~ spl10_13
| ~ spl10_18
| ~ spl10_21
| ~ spl10_36
| spl10_38
| ~ spl10_44 ),
inference(forward_subsumption_resolution,[],[f10091,f8931]) ).
fof(f10094,plain,
( ~ spl10_5
| ~ spl10_8
| ~ spl10_13
| ~ spl10_18
| ~ spl10_21
| ~ spl10_36
| spl10_38
| ~ spl10_44 ),
inference(avatar_contradiction_clause,[],[f10093]) ).
cnf(s1,plain,
spl10_1,
inference(sat_conversion,[],[f54]) ).
cnf(s3,plain,
~ spl10_3,
inference(sat_conversion,[],[f72]) ).
cnf(s4,plain,
spl10_4,
inference(sat_conversion,[],[f81]) ).
cnf(s5,plain,
spl10_5,
inference(sat_conversion,[],[f90]) ).
cnf(s6,plain,
spl10_6,
inference(sat_conversion,[],[f113]) ).
cnf(s7,plain,
spl10_7,
inference(sat_conversion,[],[f122]) ).
cnf(s8,plain,
spl10_8,
inference(sat_conversion,[],[f157]) ).
cnf(s9,plain,
spl10_9,
inference(sat_conversion,[],[f173]) ).
cnf(s10,plain,
spl10_10,
inference(sat_conversion,[],[f227]) ).
cnf(s11,plain,
spl10_11,
inference(sat_conversion,[],[f233]) ).
cnf(s12,plain,
spl10_12,
inference(sat_conversion,[],[f239]) ).
cnf(s13,plain,
spl10_13,
inference(sat_conversion,[],[f253]) ).
cnf(s14,plain,
( ~ spl10_6
| ~ spl10_13
| spl10_14 ),
inference(sat_conversion,[],[f786]) ).
cnf(s16,plain,
( ~ spl10_7
| ~ spl10_13
| spl10_16 ),
inference(sat_conversion,[],[f1010]) ).
cnf(s18,plain,
( ~ spl10_9
| ~ spl10_11
| ~ spl10_12
| ~ spl10_13
| spl10_18 ),
inference(sat_conversion,[],[f2481]) ).
cnf(s20,plain,
( ~ spl10_1
| ~ spl10_7
| ~ spl10_13
| spl10_20 ),
inference(sat_conversion,[],[f2880]) ).
cnf(s21,plain,
( ~ spl10_8
| ~ spl10_13
| spl10_21 ),
inference(sat_conversion,[],[f2918]) ).
cnf(s24,plain,
( ~ spl10_7
| spl10_24 ),
inference(sat_conversion,[],[f3668]) ).
cnf(s25,plain,
( ~ spl10_9
| ~ spl10_11
| ~ spl10_12
| ~ spl10_13
| spl10_25 ),
inference(sat_conversion,[],[f4041]) ).
cnf(s27,plain,
( ~ spl10_13
| spl10_27 ),
inference(sat_conversion,[],[f4979]) ).
cnf(s28,plain,
( ~ spl10_1
| ~ spl10_7
| ~ spl10_9
| ~ spl10_11
| ~ spl10_12
| ~ spl10_13
| ~ spl10_16
| ~ spl10_18
| ~ spl10_24
| spl10_28 ),
inference(sat_conversion,[],[f6628]) ).
cnf(s29,plain,
( ~ spl10_13
| ~ spl10_28
| spl10_29 ),
inference(sat_conversion,[],[f6719]) ).
cnf(s35,plain,
( ~ spl10_4
| ~ spl10_7
| ~ spl10_8
| ~ spl10_10
| ~ spl10_13
| ~ spl10_14
| ~ spl10_16
| ~ spl10_18
| ~ spl10_29
| spl10_35 ),
inference(sat_conversion,[],[f8694]) ).
cnf(s36,plain,
( ~ spl10_13
| ~ spl10_35
| spl10_36 ),
inference(sat_conversion,[],[f8758]) ).
cnf(s38,plain,
( spl10_3
| ~ spl10_5
| ~ spl10_18
| ~ spl10_36
| ~ spl10_38 ),
inference(sat_conversion,[],[f8932]) ).
cnf(s44,plain,
( ~ spl10_7
| ~ spl10_8
| ~ spl10_10
| ~ spl10_13
| ~ spl10_18
| ~ spl10_20
| ~ spl10_25
| ~ spl10_27
| ~ spl10_35
| spl10_44 ),
inference(sat_conversion,[],[f9977]) ).
cnf(s47,plain,
( ~ spl10_5
| ~ spl10_8
| ~ spl10_13
| ~ spl10_18
| ~ spl10_21
| ~ spl10_36
| spl10_38
| ~ spl10_44 ),
inference(sat_conversion,[],[f10094]) ).
cnf(s49,plain,
spl10_27,
inference(rat,[],[s27,s13]) ).
cnf(s53,plain,
spl10_25,
inference(rat,[],[s25,s11,s13,s12,s9]) ).
cnf(s55,plain,
spl10_18,
inference(rat,[],[s18,s11,s13,s12,s9]) ).
cnf(s56,plain,
spl10_21,
inference(rat,[],[s21,s13,s8]) ).
cnf(s57,plain,
spl10_24,
inference(rat,[],[s24,s7]) ).
cnf(s58,plain,
spl10_16,
inference(rat,[],[s16,s13,s7]) ).
cnf(s62,plain,
spl10_14,
inference(rat,[],[s14,s13,s6]) ).
cnf(s67,plain,
spl10_28,
inference(rat,[],[s28,s58,s57,s55,s7,s13,s12,s11,s9,s1]) ).
cnf(s68,plain,
spl10_20,
inference(rat,[],[s20,s7,s13,s1]) ).
cnf(s69,plain,
spl10_29,
inference(rat,[],[s29,s13,s67]) ).
cnf(s72,plain,
spl10_35,
inference(rat,[],[s35,s4,s62,s55,s58,s7,s13,s10,s8,s69]) ).
cnf(s73,plain,
spl10_36,
inference(rat,[],[s36,s13,s72]) ).
cnf(s74,plain,
spl10_44,
inference(rat,[],[s44,s68,s7,s49,s53,s8,s55,s13,s10,s72]) ).
cnf(s77,plain,
spl10_38,
inference(rat,[],[s47,s74,s5,s56,s8,s55,s13,s73]) ).
cnf(s78,plain,
$false,
inference(rat,[],[s38,s3,s5,s55,s77,s73]) ).
fof(f10095,plain,
$false,
inference(avatar_sat_refutation,[],[s78]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : REL022-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.39 % Computer : n004.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sun Sep 27 22:52:37 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 13.36/2.74 % (3975682)Detected a unit-equality problem, will run specialized UEQ schedule.
% 13.36/2.74 % (3975691)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=178194778:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 13.36/2.74 % (3975689)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=140507040:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 13.36/2.74 % (3975692)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=15992635:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 13.36/2.74 % (3975693)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=2047326074:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 13.36/2.74 % (3975690)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=3451575538:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 13.36/2.74 % (3975688)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=3642089557:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 13.36/2.74 % (3975687)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=806426400:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 13.36/2.74 % (3975691)Instruction limit reached!
% 13.36/2.74 % (3975691)------------------------------
% 13.36/2.74 % (3975691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.36/2.74 % (3975691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.36/2.74 % (3975691)CaDiCaL version: 2.1.3
% 13.36/2.74 % (3975691)Termination reason: Instruction limit
% 13.36/2.74 % (3975691)Termination phase: Saturation
% 13.36/2.74 % (3975691)Time elapsed: 0.057 s
% 13.36/2.74 % (3975691)Peak memory usage: 89 MB
% 13.36/2.74 % (3975691)Instructions burned: 183 (million)
% 13.36/2.74 % (3975690)Instruction limit reached!
% 13.36/2.74 % (3975690)------------------------------
% 13.36/2.74 % (3975690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.36/2.74 % (3975690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.36/2.74 % (3975690)CaDiCaL version: 2.1.3
% 13.36/2.74 % (3975690)Termination reason: Instruction limit
% 13.36/2.74 % (3975690)Termination phase: Saturation
% 13.36/2.74 % (3975690)Time elapsed: 0.085 s
% 13.36/2.74 % (3975690)Peak memory usage: 89 MB
% 13.36/2.74 % (3975690)Instructions burned: 137 (million)
% 13.36/2.74 % (3975701)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=3362006857:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2998 on theBenchmark for (2998ds/2051Mi)
% 13.36/2.74 % (3975692)Instruction limit reached!
% 13.36/2.74 % (3975692)------------------------------
% 13.36/2.74 % (3975692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.36/2.74 % (3975692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.36/2.74 % (3975692)CaDiCaL version: 2.1.3
% 13.36/2.74 % (3975692)Termination reason: Instruction limit
% 13.36/2.74 % (3975692)Termination phase: Saturation
% 13.36/2.74 % (3975692)Time elapsed: 0.169 s
% 13.36/2.74 % (3975692)Peak memory usage: 90 MB
% 13.36/2.74 % (3975692)Instructions burned: 258 (million)
% 13.36/2.74 % (3975702)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=39436524:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 13.36/2.74 % (3975704)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=2808078023:i=215:ep=RSTC_2996 on theBenchmark for (2996ds/215Mi)
% 13.36/2.74 % (3975704)Instruction limit reached!
% 13.36/2.74 % (3975704)------------------------------
% 13.36/2.74 % (3975704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.36/2.74 % (3975704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.36/2.74 % (3975704)CaDiCaL version: 2.1.3
% 13.36/2.74 % (3975704)Termination reason: Instruction limit
% 13.36/2.74 % (3975704)Termination phase: Saturation
% 13.36/2.74 % (3975704)Time elapsed: 0.121 s
% 13.36/2.74 % (3975704)Peak memory usage: 92 MB
% 13.36/2.74 % (3975704)Instructions burned: 215 (million)
% 13.36/2.74 % (3975707)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=2613256603: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)
% 13.36/2.74 % (3975693)Instruction limit reached!
% 13.36/2.74 % (3975693)------------------------------
% 13.36/2.74 % (3975693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.36/2.74 % (3975693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.36/2.74 % (3975693)CaDiCaL version: 2.1.3
% 13.36/2.74 % (3975693)Termination reason: Instruction limit
% 13.36/2.74 % (3975693)Termination phase: Saturation
% 13.36/2.74 % (3975693)Time elapsed: 0.642 s
% 13.36/2.74 % (3975693)Peak memory usage: 98 MB
% 13.36/2.74 % (3975693)Instructions burned: 1187 (million)
% 13.36/2.74 % (3975707)Instruction limit reached!
% 13.36/2.74 % (3975707)------------------------------
% 13.36/2.74 % (3975707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.36/2.74 % (3975707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.36/2.74 % (3975707)CaDiCaL version: 2.1.3
% 13.36/2.74 % (3975707)Termination reason: Instruction limit
% 13.36/2.74 % (3975707)Termination phase: Saturation
% 13.36/2.74 % (3975707)Time elapsed: 0.192 s
% 13.36/2.74 % (3975707)Peak memory usage: 92 MB
% 13.36/2.74 % (3975707)Instructions burned: 317 (million)
% 13.36/2.74 % (3975709)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=4244877165:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2991 on theBenchmark for (2991ds/12125Mi)
% 13.36/2.74 % (3975701)Instruction limit reached!
% 13.36/2.74 % (3975701)------------------------------
% 13.36/2.74 % (3975701)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.36/2.74 % (3975701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.36/2.74 % (3975701)CaDiCaL version: 2.1.3
% 13.36/2.74 % (3975701)Termination reason: Instruction limit
% 13.36/2.74 % (3975701)Termination phase: Saturation
% 13.36/2.74 % (3975701)Time elapsed: 0.752 s
% 13.36/2.74 % (3975701)Peak memory usage: 141 MB
% 13.36/2.74 % (3975701)Instructions burned: 2053 (million)
% 13.36/2.74 % (3975711)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=1337180601:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2990 on theBenchmark for (2990ds/2836Mi)
% 13.36/2.74 % (3975712)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3562478570:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2989 on theBenchmark for (2989ds/14534Mi)
% 13.36/2.74 % (3975687)First to succeed.
% 13.36/2.74 % (3975687)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3975682"
% 13.36/2.74 % (3975687)Refutation found. Thanks to Tanya!
% 13.36/2.74 % SZS status Unsatisfiable for theBenchmark
% 13.36/2.74 % SZS output start Proof for theBenchmark
% See solution above
% 13.86/2.94 % (3975687)------------------------------
% 13.86/2.94 % (3975687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.86/2.94 % (3975687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.86/2.94 % (3975687)CaDiCaL version: 2.1.3
% 13.86/2.94 % (3975687)Termination reason: Refutation
% 13.86/2.94 % (3975687)Time elapsed: 1.439 s
% 13.86/2.94 % (3975687)Peak memory usage: 144 MB
% 13.86/2.94 % (3975687)Instructions burned: 2284 (million)
% 13.86/2.94 % (3975687)------------------------------
% 13.86/2.94 % (3975687)------------------------------
% 13.86/2.94 % (3975682)Success in time 1.873 s
% 13.86/2.94 % Vampire exiting
%------------------------------------------------------------------------------