%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : REL021-2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n014.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:48 PM UTC 2026
% Result : Unsatisfiable 24.49s 4.58s
% Output : Refutation 25.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 43
% Syntax : Number of formulae : 271 ( 118 unt; 28 def)
% Number of atoms : 632 ( 223 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 712 ( 351 ~; 343 |; 0 &)
% ( 18 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 20 ( 18 usr; 19 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 15 con; 0-2 aty)
% Number of variables : 174 ( 0 sgn 174 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maddux1_join_commutativity_1) ).
fof(f2,axiom,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maddux2_join_associativity_2) ).
fof(f3,axiom,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maddux3_a_kind_of_de_Morgan_3) ).
fof(f4,plain,
! [X0,X1] : join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) = X0,
inference(reorient_equations,[],[f3]) ).
fof(f5,axiom,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maddux4_definiton_of_meet_4) ).
fof(f6,plain,
! [X0,X1] : complement(join(complement(X0),complement(X1))) = meet(X0,X1),
inference(reorient_equations,[],[f5]) ).
fof(f7,axiom,
! [X2,X0,X1] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',composition_associativity_5) ).
fof(f8,axiom,
! [X0] : composition(X0,one) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',composition_identity_6) ).
fof(f9,axiom,
! [X2,X0,X1] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',composition_distributivity_7) ).
fof(f10,axiom,
! [X0] : converse(converse(X0)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_idempotence_8) ).
fof(f11,axiom,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_additivity_9) ).
fof(f12,axiom,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_multiplicativity_10) ).
fof(f13,axiom,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_cancellativity_11) ).
fof(f14,plain,
! [X0,X1] : complement(X1) = join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)),
inference(reorient_equations,[],[f13]) ).
fof(f15,axiom,
! [X0] : top = join(X0,complement(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',def_top_12) ).
fof(f16,axiom,
! [X0] : zero = meet(X0,complement(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',def_zero_13) ).
fof(f23,negated_conjecture,
composition(sk1,top) = sk1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals_17) ).
fof(f24,plain,
sk1 = composition(sk1,top),
inference(reorient_equations,[],[f23]) ).
fof(f25,negated_conjecture,
join(composition(meet(sk1,one),sk2),meet(sk1,sk2)) != meet(sk1,sk2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals_18) ).
fof(f26,plain,
meet(sk1,sk2) != join(composition(meet(sk1,one),sk2),meet(sk1,sk2)),
inference(reorient_equations,[],[f25]) ).
fof(f27,plain,
! [X0] : zero = complement(join(complement(X0),complement(complement(X0)))),
inference(definition_unfolding,[],[f16,f6]) ).
fof(f31,plain,
complement(join(complement(sk1),complement(sk2))) != join(composition(complement(join(complement(sk1),complement(one))),sk2),complement(join(complement(sk1),complement(sk2)))),
inference(definition_unfolding,[],[f26,f6,f6,f6]) ).
fof(f32,definition,
sF0 = composition(sk1,top),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f33,plain,
composition(sk1,top) = sF0,
inference(reorient_equations,[],[f32]) ).
fof(f34,plain,
sk1 = sF0,
inference(definition_folding,[],[f24,f33]) ).
fof(f35,definition,
sF1 = complement(sk1),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f36,plain,
complement(sk1) = sF1,
inference(reorient_equations,[],[f35]) ).
fof(f37,definition,
sF2 = complement(sk2),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f38,plain,
complement(sk2) = sF2,
inference(reorient_equations,[],[f37]) ).
fof(f39,definition,
sF3 = join(sF1,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f40,plain,
join(sF1,sF2) = sF3,
inference(reorient_equations,[],[f39]) ).
fof(f41,definition,
sF4 = complement(sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f42,plain,
complement(sF3) = sF4,
inference(reorient_equations,[],[f41]) ).
fof(f43,definition,
sF5 = complement(one),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f44,plain,
complement(one) = sF5,
inference(reorient_equations,[],[f43]) ).
fof(f45,definition,
sF6 = join(sF1,sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f46,plain,
join(sF1,sF5) = sF6,
inference(reorient_equations,[],[f45]) ).
fof(f47,definition,
sF7 = complement(sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f48,plain,
complement(sF6) = sF7,
inference(reorient_equations,[],[f47]) ).
fof(f49,definition,
sF8 = composition(sF7,sk2),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f50,plain,
composition(sF7,sk2) = sF8,
inference(reorient_equations,[],[f49]) ).
fof(f51,definition,
sF9 = join(sF8,sF4),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f52,plain,
join(sF8,sF4) = sF9,
inference(reorient_equations,[],[f51]) ).
fof(f53,plain,
sF4 != sF9,
inference(definition_folding,[],[f31,f52,f42,f40,f38,f36,f50,f48,f46,f44,f36,f42,f40,f38,f36]) ).
fof(f54,plain,
zero = complement(top),
inference(backward_demodulation,[],[f27,f15]) ).
fof(f55,plain,
sF0 = composition(sF0,top),
inference(forward_demodulation,[],[f33,f34]) ).
fof(f56,plain,
sF1 = complement(sF0),
inference(forward_demodulation,[],[f36,f34]) ).
fof(f57,plain,
sF3 = join(sF2,sF1),
inference(forward_demodulation,[],[f40,f1]) ).
fof(f58,plain,
sF6 = join(sF5,sF1),
inference(forward_demodulation,[],[f46,f1]) ).
fof(f66,definition,
( spl10_1
<=> sF0 = composition(sF0,top) ),
introduced(definition,[new_symbols(definition,[spl10_1])],[avatar_definition]) ).
fof(f68,plain,
( sF0 = composition(sF0,top)
| ~ spl10_1 ),
inference(avatar_component_clause,[],[f66]) ).
fof(f69,plain,
spl10_1,
inference(avatar_split_clause,[],[f55,f66]) ).
fof(f78,plain,
! [X0,X1] : join(complement(join(complement(X0),complement(X1))),complement(join(complement(X1),X0))) = X1,
inference(superposition,[],[f4,f1]) ).
fof(f79,plain,
! [X0,X1] : join(complement(join(complement(X1),complement(X0))),complement(join(X0,complement(X1)))) = X1,
inference(superposition,[],[f4,f1]) ).
fof(f80,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))) = X0,
inference(superposition,[],[f4,f1]) ).
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(f83,plain,
! [X0,X1] : join(complement(join(X0,complement(X1))),complement(join(complement(X1),complement(X0)))) = X1,
inference(forward_demodulation,[],[f79,f1]) ).
fof(f84,plain,
! [X0,X1] : join(complement(join(complement(X1),X0)),complement(join(complement(X0),complement(X1)))) = X1,
inference(forward_demodulation,[],[f78,f1]) ).
fof(f91,definition,
( spl10_2
<=> complement(sF3) = sF4 ),
introduced(definition,[new_symbols(definition,[spl10_2])],[avatar_definition]) ).
fof(f93,plain,
( complement(sF3) = sF4
| ~ spl10_2 ),
inference(avatar_component_clause,[],[f91]) ).
fof(f94,plain,
spl10_2,
inference(avatar_split_clause,[],[f42,f91]) ).
fof(f106,definition,
( spl10_4
<=> zero = complement(top) ),
introduced(definition,[new_symbols(definition,[spl10_4])],[avatar_definition]) ).
fof(f108,plain,
( zero = complement(top)
| ~ spl10_4 ),
inference(avatar_component_clause,[],[f106]) ).
fof(f109,plain,
spl10_4,
inference(avatar_split_clause,[],[f54,f106]) ).
fof(f111,definition,
( spl10_5
<=> sF4 = sF9 ),
introduced(definition,[new_symbols(definition,[spl10_5])],[avatar_definition]) ).
fof(f113,plain,
( sF4 != sF9
| spl10_5 ),
inference(avatar_component_clause,[],[f111]) ).
fof(f114,plain,
~ spl10_5,
inference(avatar_split_clause,[],[f53,f111]) ).
fof(f116,definition,
( spl10_6
<=> sF1 = complement(sF0) ),
introduced(definition,[new_symbols(definition,[spl10_6])],[avatar_definition]) ).
fof(f118,plain,
( sF1 = complement(sF0)
| ~ spl10_6 ),
inference(avatar_component_clause,[],[f116]) ).
fof(f119,plain,
spl10_6,
inference(avatar_split_clause,[],[f56,f116]) ).
fof(f125,plain,
( top = join(sF0,sF1)
| ~ spl10_6 ),
inference(superposition,[],[f15,f118]) ).
fof(f127,plain,
! [X0] : join(complement(join(complement(X0),complement(complement(complement(X0))))),complement(top)) = X0,
inference(superposition,[],[f4,f15]) ).
fof(f128,plain,
! [X0] : join(complement(top),complement(join(complement(X0),complement(complement(complement(X0)))))) = X0,
inference(forward_demodulation,[],[f127,f1]) ).
fof(f130,plain,
( top = join(sF1,sF0)
| ~ spl10_6 ),
inference(forward_demodulation,[],[f125,f1]) ).
fof(f131,plain,
( ! [X0] : join(zero,complement(join(complement(X0),complement(complement(complement(X0)))))) = X0
| ~ spl10_4 ),
inference(forward_demodulation,[],[f128,f108]) ).
fof(f133,definition,
( spl10_7
<=> join(sF8,sF4) = sF9 ),
introduced(definition,[new_symbols(definition,[spl10_7])],[avatar_definition]) ).
fof(f135,plain,
( join(sF8,sF4) = sF9
| ~ spl10_7 ),
inference(avatar_component_clause,[],[f133]) ).
fof(f136,plain,
spl10_7,
inference(avatar_split_clause,[],[f52,f133]) ).
fof(f137,plain,
! [X0,X1] : complement(X1) = join(composition(X0,complement(composition(converse(X0),X1))),complement(X1)),
inference(superposition,[],[f14,f10]) ).
fof(f146,plain,
! [X0,X1] : complement(X1) = join(complement(X1),composition(X0,complement(composition(converse(X0),X1)))),
inference(forward_demodulation,[],[f137,f1]) ).
fof(f148,definition,
( spl10_8
<=> complement(sk2) = sF2 ),
introduced(definition,[new_symbols(definition,[spl10_8])],[avatar_definition]) ).
fof(f150,plain,
( complement(sk2) = sF2
| ~ spl10_8 ),
inference(avatar_component_clause,[],[f148]) ).
fof(f151,plain,
spl10_8,
inference(avatar_split_clause,[],[f38,f148]) ).
fof(f162,plain,
( ! [X0] : composition(join(sF0,X0),top) = join(sF0,composition(X0,top))
| ~ spl10_1 ),
inference(superposition,[],[f9,f68]) ).
fof(f170,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(top,X1),
inference(superposition,[],[f2,f15]) ).
fof(f180,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f1,f2]) ).
fof(f207,definition,
( spl10_9
<=> sF6 = join(sF5,sF1) ),
introduced(definition,[new_symbols(definition,[spl10_9])],[avatar_definition]) ).
fof(f209,plain,
( sF6 = join(sF5,sF1)
| ~ spl10_9 ),
inference(avatar_component_clause,[],[f207]) ).
fof(f210,plain,
spl10_9,
inference(avatar_split_clause,[],[f58,f207]) ).
fof(f213,definition,
( spl10_10
<=> complement(sF6) = sF7 ),
introduced(definition,[new_symbols(definition,[spl10_10])],[avatar_definition]) ).
fof(f215,plain,
( complement(sF6) = sF7
| ~ spl10_10 ),
inference(avatar_component_clause,[],[f213]) ).
fof(f216,plain,
spl10_10,
inference(avatar_split_clause,[],[f48,f213]) ).
fof(f229,definition,
( spl10_11
<=> sF3 = join(sF2,sF1) ),
introduced(definition,[new_symbols(definition,[spl10_11])],[avatar_definition]) ).
fof(f231,plain,
( sF3 = join(sF2,sF1)
| ~ spl10_11 ),
inference(avatar_component_clause,[],[f229]) ).
fof(f232,plain,
spl10_11,
inference(avatar_split_clause,[],[f57,f229]) ).
fof(f235,definition,
( spl10_12
<=> complement(one) = sF5 ),
introduced(definition,[new_symbols(definition,[spl10_12])],[avatar_definition]) ).
fof(f237,plain,
( complement(one) = sF5
| ~ spl10_12 ),
inference(avatar_component_clause,[],[f235]) ).
fof(f238,plain,
spl10_12,
inference(avatar_split_clause,[],[f44,f235]) ).
fof(f296,plain,
! [X0,X1] : composition(converse(X1),X0) = converse(composition(converse(X0),X1)),
inference(superposition,[],[f12,f10]) ).
fof(f299,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(f306,plain,
! [X2,X0,X1] : composition(join(converse(X2),converse(X1)),converse(X0)) = join(converse(composition(X0,X2)),converse(composition(X0,X1))),
inference(superposition,[],[f299,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(f320,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(f322,plain,
! [X2,X0,X1] : converse(join(composition(X0,X2),composition(X0,X1))) = converse(composition(X0,join(X2,X1))),
inference(forward_demodulation,[],[f320,f12]) ).
fof(f333,plain,
! [X2,X0,X1] : join(composition(X0,X1),composition(X0,X2)) = converse(converse(composition(X0,join(X1,X2)))),
inference(superposition,[],[f10,f322]) ).
fof(f345,plain,
! [X2,X0,X1] : composition(X0,join(X1,X2)) = join(composition(X0,X1),composition(X0,X2)),
inference(forward_demodulation,[],[f333,f10]) ).
fof(f369,plain,
! [X0,X1] : composition(X0,join(X1,one)) = join(composition(X0,X1),X0),
inference(superposition,[],[f345,f8]) ).
fof(f382,plain,
! [X0,X1] : join(X0,composition(X0,X1)) = composition(X0,join(X1,one)),
inference(forward_demodulation,[],[f369,f1]) ).
fof(f387,definition,
( spl10_13
<=> composition(sF7,sk2) = sF8 ),
introduced(definition,[new_symbols(definition,[spl10_13])],[avatar_definition]) ).
fof(f389,plain,
( composition(sF7,sk2) = sF8
| ~ spl10_13 ),
inference(avatar_component_clause,[],[f387]) ).
fof(f390,plain,
spl10_13,
inference(avatar_split_clause,[],[f50,f387]) ).
fof(f430,plain,
( ! [X0] : join(complement(join(top,complement(X0))),complement(join(complement(X0),zero))) = X0
| ~ spl10_4 ),
inference(superposition,[],[f83,f108]) ).
fof(f456,plain,
( ! [X0] : join(complement(join(top,complement(X0))),complement(join(zero,complement(X0)))) = X0
| ~ spl10_4 ),
inference(forward_demodulation,[],[f430,f1]) ).
fof(f469,plain,
( ! [X0] : join(complement(join(zero,complement(X0))),complement(join(top,complement(X0)))) = X0
| ~ spl10_4 ),
inference(forward_demodulation,[],[f456,f1]) ).
fof(f495,plain,
! [X0] : complement(X0) = join(complement(join(complement(complement(X0)),X0)),complement(top)),
inference(superposition,[],[f84,f15]) ).
fof(f510,plain,
! [X0] : complement(X0) = join(complement(top),complement(join(complement(complement(X0)),X0))),
inference(forward_demodulation,[],[f495,f1]) ).
fof(f533,plain,
! [X0] : complement(X0) = join(complement(top),complement(join(X0,complement(complement(X0))))),
inference(forward_demodulation,[],[f510,f1]) ).
fof(f541,plain,
( ! [X0] : complement(X0) = join(zero,complement(join(X0,complement(complement(X0)))))
| ~ spl10_4 ),
inference(forward_demodulation,[],[f533,f108]) ).
fof(f547,plain,
( ! [X0] : complement(complement(X0)) = X0
| ~ spl10_4 ),
inference(backward_demodulation,[],[f131,f541]) ).
fof(f554,plain,
( ! [X0] : complement(X0) = join(zero,complement(join(X0,X0)))
| ~ spl10_4 ),
inference(backward_demodulation,[],[f541,f547]) ).
fof(f566,plain,
( one = complement(sF5)
| ~ spl10_4
| ~ spl10_12 ),
inference(superposition,[],[f547,f237]) ).
fof(f568,plain,
( sk2 = complement(sF2)
| ~ spl10_4
| ~ spl10_8 ),
inference(superposition,[],[f547,f150]) ).
fof(f569,plain,
( sF0 = complement(sF1)
| ~ spl10_4
| ~ spl10_6 ),
inference(superposition,[],[f547,f118]) ).
fof(f576,plain,
( ! [X0,X1] : complement(X0) = join(complement(join(X0,X1)),complement(join(X0,complement(X1))))
| ~ spl10_4 ),
inference(superposition,[],[f80,f547]) ).
fof(f579,plain,
( ! [X0,X1] : complement(X0) = join(complement(join(X1,X0)),complement(join(X0,complement(X1))))
| ~ spl10_4 ),
inference(superposition,[],[f83,f547]) ).
fof(f581,plain,
( ! [X0,X1] : complement(X0) = join(complement(join(X0,X1)),complement(join(complement(X1),X0)))
| ~ spl10_4 ),
inference(superposition,[],[f84,f547]) ).
fof(f618,plain,
( complement(sF5) = join(complement(sF6),complement(join(sF5,complement(sF1))))
| ~ spl10_4
| ~ spl10_9 ),
inference(superposition,[],[f576,f209]) ).
fof(f651,plain,
( complement(sF5) = join(complement(sF6),complement(join(sF5,sF0)))
| ~ spl10_4
| ~ spl10_6
| ~ spl10_9 ),
inference(forward_demodulation,[],[f618,f569]) ).
fof(f665,plain,
( complement(sF5) = join(sF7,complement(join(sF5,sF0)))
| ~ spl10_4
| ~ spl10_6
| ~ spl10_9
| ~ spl10_10 ),
inference(forward_demodulation,[],[f651,f215]) ).
fof(f676,plain,
( one = join(sF7,complement(join(sF5,sF0)))
| ~ spl10_4
| ~ spl10_6
| ~ spl10_9
| ~ spl10_10
| ~ spl10_12 ),
inference(forward_demodulation,[],[f665,f566]) ).
fof(f694,plain,
( ! [X0,X1] : complement(complement(join(X0,complement(X1)))) = join(complement(complement(X0)),complement(join(complement(join(X0,complement(X1))),complement(complement(join(X1,X0))))))
| ~ spl10_4 ),
inference(superposition,[],[f579,f579]) ).
fof(f701,plain,
( complement(sF1) = join(complement(sF6),complement(join(sF1,complement(sF5))))
| ~ spl10_4
| ~ spl10_9 ),
inference(superposition,[],[f579,f209]) ).
fof(f715,plain,
( ! [X0,X1] : complement(complement(join(X0,X1))) = join(complement(join(join(X0,complement(X1)),complement(join(X0,X1)))),complement(complement(X0)))
| ~ spl10_4 ),
inference(superposition,[],[f579,f576]) ).
fof(f730,plain,
( ! [X0,X1] : complement(complement(join(X0,X1))) = join(complement(complement(X0)),complement(join(join(X0,complement(X1)),complement(join(X0,X1)))))
| ~ spl10_4 ),
inference(forward_demodulation,[],[f715,f1]) ).
fof(f737,plain,
( complement(sF1) = join(complement(sF6),complement(join(sF1,one)))
| ~ spl10_4
| ~ spl10_9
| ~ spl10_12 ),
inference(forward_demodulation,[],[f701,f566]) ).
fof(f740,plain,
( ! [X0,X1] : complement(complement(join(X0,complement(X1)))) = join(complement(complement(X0)),complement(join(complement(complement(join(X1,X0))),complement(join(X0,complement(X1))))))
| ~ spl10_4 ),
inference(forward_demodulation,[],[f694,f1]) ).
fof(f751,plain,
( ! [X0,X1] : complement(complement(join(X0,X1))) = join(complement(complement(X0)),complement(join(X0,join(complement(X1),complement(join(X0,X1))))))
| ~ spl10_4 ),
inference(forward_demodulation,[],[f730,f2]) ).
fof(f754,plain,
( complement(sF1) = join(sF7,complement(join(sF1,one)))
| ~ spl10_4
| ~ spl10_9
| ~ spl10_10
| ~ spl10_12 ),
inference(forward_demodulation,[],[f737,f215]) ).
fof(f756,plain,
( ! [X0,X1] : complement(complement(join(X0,complement(X1)))) = join(complement(complement(X0)),complement(join(join(X1,X0),complement(join(X0,complement(X1))))))
| ~ spl10_4 ),
inference(forward_demodulation,[],[f740,f547]) ).
fof(f764,plain,
( ! [X0,X1] : complement(complement(join(X0,X1))) = join(X0,complement(join(X0,join(complement(X1),complement(join(X0,X1))))))
| ~ spl10_4 ),
inference(forward_demodulation,[],[f751,f547]) ).
fof(f766,plain,
( sF0 = join(sF7,complement(join(sF1,one)))
| ~ spl10_4
| ~ spl10_6
| ~ spl10_9
| ~ spl10_10
| ~ spl10_12 ),
inference(forward_demodulation,[],[f754,f569]) ).
fof(f768,plain,
( ! [X0,X1] : complement(complement(join(X0,complement(X1)))) = join(complement(complement(X0)),complement(join(X1,join(X0,complement(join(X0,complement(X1)))))))
| ~ spl10_4 ),
inference(forward_demodulation,[],[f756,f2]) ).
fof(f775,plain,
( ! [X0,X1] : join(X0,X1) = join(X0,complement(join(X0,join(complement(X1),complement(join(X0,X1))))))
| ~ spl10_4 ),
inference(forward_demodulation,[],[f764,f547]) ).
fof(f776,plain,
( ! [X0,X1] : complement(complement(join(X0,complement(X1)))) = join(X0,complement(join(X1,join(X0,complement(join(X0,complement(X1)))))))
| ~ spl10_4 ),
inference(forward_demodulation,[],[f768,f547]) ).
fof(f782,plain,
( ! [X0,X1] : join(X0,complement(X1)) = join(X0,complement(join(X1,join(X0,complement(join(X0,complement(X1)))))))
| ~ spl10_4 ),
inference(forward_demodulation,[],[f776,f547]) ).
fof(f785,definition,
( spl10_14
<=> sk2 = complement(sF2) ),
introduced(definition,[new_symbols(definition,[spl10_14])],[avatar_definition]) ).
fof(f787,plain,
( sk2 = complement(sF2)
| ~ spl10_14 ),
inference(avatar_component_clause,[],[f785]) ).
fof(f788,plain,
( spl10_14
| ~ spl10_4
| ~ spl10_8 ),
inference(avatar_split_clause,[],[f568,f148,f106,f785]) ).
fof(f809,plain,
( ! [X0] : complement(X0) = join(complement(join(X0,sF0)),complement(join(sF1,X0)))
| ~ spl10_4
| ~ spl10_6 ),
inference(superposition,[],[f581,f118]) ).
fof(f1159,plain,
! [X0] : converse(converse(X0)) = composition(converse(one),X0),
inference(superposition,[],[f296,f8]) ).
fof(f1177,plain,
! [X0] : composition(converse(one),X0) = X0,
inference(forward_demodulation,[],[f1159,f10]) ).
fof(f1195,plain,
! [X0] : complement(X0) = join(complement(X0),composition(one,complement(X0))),
inference(superposition,[],[f146,f1177]) ).
fof(f1198,plain,
! [X0,X1] : composition(join(converse(one),X1),X0) = join(X0,composition(X1,X0)),
inference(superposition,[],[f9,f1177]) ).
fof(f1204,plain,
one = converse(one),
inference(superposition,[],[f8,f1177]) ).
fof(f1207,plain,
! [X0] : composition(one,X0) = X0,
inference(backward_demodulation,[],[f1177,f1204]) ).
fof(f1215,plain,
! [X0,X1] : join(X0,composition(X1,X0)) = composition(join(one,X1),X0),
inference(forward_demodulation,[],[f1198,f1204]) ).
fof(f1220,plain,
! [X0] : complement(X0) = join(complement(X0),complement(X0)),
inference(backward_demodulation,[],[f1195,f1207]) ).
fof(f1242,plain,
( ! [X0] : join(X0,X0) = X0
| ~ spl10_4 ),
inference(superposition,[],[f1220,f547]) ).
fof(f1250,plain,
! [X0] : join(X0,complement(X0)) = join(top,complement(X0)),
inference(superposition,[],[f170,f1220]) ).
fof(f1266,plain,
! [X0] : top = join(top,complement(X0)),
inference(forward_demodulation,[],[f1250,f15]) ).
fof(f1268,plain,
( ! [X0] : complement(X0) = join(zero,complement(X0))
| ~ spl10_4 ),
inference(backward_demodulation,[],[f554,f1242]) ).
fof(f1281,plain,
( ! [X0] : join(complement(join(zero,complement(X0))),complement(top)) = X0
| ~ spl10_4 ),
inference(backward_demodulation,[],[f469,f1266]) ).
fof(f1297,plain,
( ! [X0] : join(complement(top),complement(join(zero,complement(X0)))) = X0
| ~ spl10_4 ),
inference(forward_demodulation,[],[f1281,f1]) ).
fof(f1325,plain,
( ! [X0] : join(complement(top),complement(complement(X0))) = X0
| ~ spl10_4 ),
inference(forward_demodulation,[],[f1297,f1268]) ).
fof(f1342,plain,
( ! [X0] : join(complement(top),X0) = X0
| ~ spl10_4 ),
inference(forward_demodulation,[],[f1325,f547]) ).
fof(f1355,plain,
( ! [X0] : join(zero,X0) = X0
| ~ spl10_4 ),
inference(forward_demodulation,[],[f1342,f108]) ).
fof(f1420,plain,
( ! [X0,X1] : join(X0,X1) = join(X0,join(X0,X1))
| ~ spl10_4 ),
inference(superposition,[],[f2,f1242]) ).
fof(f1557,plain,
( ! [X0,X1] : join(X0,X1) = join(X1,join(X0,X1))
| ~ spl10_4 ),
inference(superposition,[],[f1420,f1]) ).
fof(f1565,plain,
( ! [X0,X1] : complement(X0) = join(complement(join(X1,X0)),complement(X0))
| ~ spl10_4 ),
inference(superposition,[],[f1420,f579]) ).
fof(f1600,plain,
( ! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X1,X0)))
| ~ spl10_4 ),
inference(forward_demodulation,[],[f1565,f1]) ).
fof(f1613,plain,
( ! [X0,X1] : join(X0,X1) = join(X0,complement(join(X0,complement(X1))))
| ~ spl10_4 ),
inference(backward_demodulation,[],[f775,f1600]) ).
fof(f1617,plain,
( ! [X0,X1] : join(X0,complement(X1)) = join(X0,complement(join(X1,join(X0,X1))))
| ~ spl10_4 ),
inference(backward_demodulation,[],[f782,f1613]) ).
fof(f1623,plain,
( ! [X0,X1] : join(X0,complement(X1)) = join(X0,complement(join(X0,X1)))
| ~ spl10_4 ),
inference(forward_demodulation,[],[f1617,f1557]) ).
fof(f1642,plain,
( ! [X0,X1] : join(X1,complement(X0)) = join(X1,complement(join(X0,X1)))
| ~ spl10_4 ),
inference(superposition,[],[f1623,f1]) ).
fof(f1658,plain,
( join(sF5,complement(sF1)) = join(sF5,complement(sF6))
| ~ spl10_4
| ~ spl10_9 ),
inference(superposition,[],[f1623,f209]) ).
fof(f1691,plain,
( join(sF5,complement(sF1)) = join(sF5,sF7)
| ~ spl10_4
| ~ spl10_9
| ~ spl10_10 ),
inference(forward_demodulation,[],[f1658,f215]) ).
fof(f1718,plain,
( join(sF5,sF0) = join(sF5,sF7)
| ~ spl10_4
| ~ spl10_6
| ~ spl10_9
| ~ spl10_10 ),
inference(forward_demodulation,[],[f1691,f569]) ).
fof(f1738,plain,
( one = join(sF7,complement(join(sF5,sF7)))
| ~ spl10_4
| ~ spl10_6
| ~ spl10_9
| ~ spl10_10
| ~ spl10_12 ),
inference(backward_demodulation,[],[f676,f1718]) ).
fof(f1753,plain,
( one = join(sF7,complement(sF5))
| ~ spl10_4
| ~ spl10_6
| ~ spl10_9
| ~ spl10_10
| ~ spl10_12 ),
inference(forward_demodulation,[],[f1738,f1642]) ).
fof(f1763,plain,
( one = join(sF7,one)
| ~ spl10_4
| ~ spl10_6
| ~ spl10_9
| ~ spl10_10
| ~ spl10_12 ),
inference(forward_demodulation,[],[f1753,f566]) ).
fof(f1795,plain,
( join(sF1,complement(sF2)) = join(sF1,complement(sF3))
| ~ spl10_4
| ~ spl10_11 ),
inference(superposition,[],[f1642,f231]) ).
fof(f1796,plain,
( join(sF1,complement(sF5)) = join(sF1,complement(sF6))
| ~ spl10_4
| ~ spl10_9 ),
inference(superposition,[],[f1642,f209]) ).
fof(f1830,plain,
( join(sF1,complement(sF5)) = join(sF1,sF7)
| ~ spl10_4
| ~ spl10_9
| ~ spl10_10 ),
inference(forward_demodulation,[],[f1796,f215]) ).
fof(f1831,plain,
( join(sF1,complement(sF2)) = join(sF1,sF4)
| ~ spl10_2
| ~ spl10_4
| ~ spl10_11 ),
inference(forward_demodulation,[],[f1795,f93]) ).
fof(f1855,plain,
( join(sF1,complement(sF5)) = join(sF7,sF1)
| ~ spl10_4
| ~ spl10_9
| ~ spl10_10 ),
inference(forward_demodulation,[],[f1830,f1]) ).
fof(f1856,plain,
( join(sF1,sk2) = join(sF1,sF4)
| ~ spl10_2
| ~ spl10_4
| ~ spl10_11
| ~ spl10_14 ),
inference(forward_demodulation,[],[f1831,f787]) ).
fof(f1873,plain,
( join(sF1,one) = join(sF7,sF1)
| ~ spl10_4
| ~ spl10_9
| ~ spl10_10
| ~ spl10_12 ),
inference(forward_demodulation,[],[f1855,f566]) ).
fof(f1883,plain,
( sF0 = join(sF7,complement(join(sF7,sF1)))
| ~ spl10_4
| ~ spl10_6
| ~ spl10_9
| ~ spl10_10
| ~ spl10_12 ),
inference(backward_demodulation,[],[f766,f1873]) ).
fof(f1890,plain,
( sF0 = join(sF7,complement(sF1))
| ~ spl10_4
| ~ spl10_6
| ~ spl10_9
| ~ spl10_10
| ~ spl10_12 ),
inference(forward_demodulation,[],[f1883,f1623]) ).
fof(f1896,plain,
( sF0 = join(sF7,sF0)
| ~ spl10_4
| ~ spl10_6
| ~ spl10_9
| ~ spl10_10
| ~ spl10_12 ),
inference(forward_demodulation,[],[f1890,f569]) ).
fof(f4823,definition,
( spl10_23
<=> one = join(sF7,one) ),
introduced(definition,[new_symbols(definition,[spl10_23])],[avatar_definition]) ).
fof(f4825,plain,
( one = join(sF7,one)
| ~ spl10_23 ),
inference(avatar_component_clause,[],[f4823]) ).
fof(f4826,plain,
( spl10_23
| ~ spl10_4
| ~ spl10_6
| ~ spl10_9
| ~ spl10_10
| ~ spl10_12 ),
inference(avatar_split_clause,[],[f1763,f235,f213,f207,f116,f106,f4823]) ).
fof(f4827,plain,
( ! [X0] : composition(X0,one) = join(X0,composition(X0,sF7))
| ~ spl10_23 ),
inference(superposition,[],[f382,f4825]) ).
fof(f4844,plain,
( ! [X0] : join(X0,composition(X0,sF7)) = X0
| ~ spl10_23 ),
inference(forward_demodulation,[],[f4827,f8]) ).
fof(f4885,plain,
( ! [X0] : composition(one,X0) = join(X0,composition(composition(one,sF7),X0))
| ~ spl10_23 ),
inference(superposition,[],[f1215,f4844]) ).
fof(f4895,plain,
( ! [X0] : composition(one,X0) = join(X0,composition(one,composition(sF7,X0)))
| ~ spl10_23 ),
inference(forward_demodulation,[],[f4885,f7]) ).
fof(f4915,plain,
( ! [X0] : composition(one,X0) = join(X0,composition(sF7,X0))
| ~ spl10_23 ),
inference(forward_demodulation,[],[f4895,f1207]) ).
fof(f4923,plain,
( ! [X0] : join(X0,composition(sF7,X0)) = X0
| ~ spl10_23 ),
inference(forward_demodulation,[],[f4915,f1207]) ).
fof(f5365,definition,
( spl10_24
<=> top = join(sF1,sF0) ),
introduced(definition,[new_symbols(definition,[spl10_24])],[avatar_definition]) ).
fof(f5367,plain,
( top = join(sF1,sF0)
| ~ spl10_24 ),
inference(avatar_component_clause,[],[f5365]) ).
fof(f5368,plain,
( spl10_24
| ~ spl10_6 ),
inference(avatar_split_clause,[],[f130,f116,f5365]) ).
fof(f6293,plain,
( ! [X0,X1] : join(X1,X0) = join(X0,join(composition(sF7,X0),X1))
| ~ spl10_23 ),
inference(superposition,[],[f180,f4923]) ).
fof(f6369,plain,
( ! [X0,X1] : join(composition(sF7,X1),X0) = join(X0,composition(sF7,join(X0,X1)))
| ~ spl10_23 ),
inference(superposition,[],[f6293,f345]) ).
fof(f6529,plain,
( ! [X0,X1] : join(composition(sF7,X0),X1) = join(X1,composition(sF7,join(X0,X1)))
| ~ spl10_23 ),
inference(superposition,[],[f6369,f1]) ).
fof(f6815,plain,
( join(composition(sF7,sF1),sF0) = join(sF0,composition(sF7,top))
| ~ spl10_23
| ~ spl10_24 ),
inference(superposition,[],[f6529,f5367]) ).
fof(f6905,plain,
( join(composition(sF7,sF1),sF0) = composition(join(sF0,sF7),top)
| ~ spl10_1
| ~ spl10_23
| ~ spl10_24 ),
inference(forward_demodulation,[],[f6815,f162]) ).
fof(f6958,plain,
( join(composition(sF7,sF1),sF0) = composition(join(sF7,sF0),top)
| ~ spl10_1
| ~ spl10_23
| ~ spl10_24 ),
inference(forward_demodulation,[],[f6905,f82]) ).
fof(f6991,plain,
( composition(sF0,top) = join(composition(sF7,sF1),sF0)
| ~ spl10_1
| ~ spl10_4
| ~ spl10_6
| ~ spl10_9
| ~ spl10_10
| ~ spl10_12
| ~ spl10_23
| ~ spl10_24 ),
inference(forward_demodulation,[],[f6958,f1896]) ).
fof(f7002,plain,
( composition(sF0,top) = join(sF0,composition(sF7,sF1))
| ~ spl10_1
| ~ spl10_4
| ~ spl10_6
| ~ spl10_9
| ~ spl10_10
| ~ spl10_12
| ~ spl10_23
| ~ spl10_24 ),
inference(forward_demodulation,[],[f6991,f1]) ).
fof(f7008,plain,
( sF0 = join(sF0,composition(sF7,sF1))
| ~ spl10_1
| ~ spl10_4
| ~ spl10_6
| ~ spl10_9
| ~ spl10_10
| ~ spl10_12
| ~ spl10_23
| ~ spl10_24 ),
inference(forward_demodulation,[],[f7002,f68]) ).
fof(f7694,plain,
( complement(composition(sF7,sF1)) = join(complement(join(composition(sF7,sF1),sF0)),complement(sF1))
| ~ spl10_4
| ~ spl10_6
| ~ spl10_23 ),
inference(superposition,[],[f809,f4923]) ).
fof(f7759,plain,
( complement(composition(sF7,sF1)) = join(complement(sF1),complement(join(composition(sF7,sF1),sF0)))
| ~ spl10_4
| ~ spl10_6
| ~ spl10_23 ),
inference(forward_demodulation,[],[f7694,f1]) ).
fof(f7809,plain,
( complement(composition(sF7,sF1)) = join(complement(sF1),complement(join(sF0,composition(sF7,sF1))))
| ~ spl10_4
| ~ spl10_6
| ~ spl10_23 ),
inference(forward_demodulation,[],[f7759,f1]) ).
fof(f7851,plain,
( join(complement(sF1),complement(sF0)) = complement(composition(sF7,sF1))
| ~ spl10_1
| ~ spl10_4
| ~ spl10_6
| ~ spl10_9
| ~ spl10_10
| ~ spl10_12
| ~ spl10_23
| ~ spl10_24 ),
inference(forward_demodulation,[],[f7809,f7008]) ).
fof(f7883,plain,
( join(complement(sF1),sF1) = complement(composition(sF7,sF1))
| ~ spl10_1
| ~ spl10_4
| ~ spl10_6
| ~ spl10_9
| ~ spl10_10
| ~ spl10_12
| ~ spl10_23
| ~ spl10_24 ),
inference(forward_demodulation,[],[f7851,f118]) ).
fof(f7912,plain,
( join(sF1,complement(sF1)) = complement(composition(sF7,sF1))
| ~ spl10_1
| ~ spl10_4
| ~ spl10_6
| ~ spl10_9
| ~ spl10_10
| ~ spl10_12
| ~ spl10_23
| ~ spl10_24 ),
inference(forward_demodulation,[],[f7883,f1]) ).
fof(f7937,plain,
( top = complement(composition(sF7,sF1))
| ~ spl10_1
| ~ spl10_4
| ~ spl10_6
| ~ spl10_9
| ~ spl10_10
| ~ spl10_12
| ~ spl10_23
| ~ spl10_24 ),
inference(forward_demodulation,[],[f7912,f15]) ).
fof(f7992,definition,
( spl10_28
<=> top = complement(composition(sF7,sF1)) ),
introduced(definition,[new_symbols(definition,[spl10_28])],[avatar_definition]) ).
fof(f7994,plain,
( top = complement(composition(sF7,sF1))
| ~ spl10_28 ),
inference(avatar_component_clause,[],[f7992]) ).
fof(f7995,plain,
( spl10_28
| ~ spl10_1
| ~ spl10_4
| ~ spl10_6
| ~ spl10_9
| ~ spl10_10
| ~ spl10_12
| ~ spl10_23
| ~ spl10_24 ),
inference(avatar_split_clause,[],[f7937,f5365,f4823,f235,f213,f207,f116,f106,f66,f7992]) ).
fof(f8009,plain,
( complement(top) = composition(sF7,sF1)
| ~ spl10_4
| ~ spl10_28 ),
inference(superposition,[],[f547,f7994]) ).
fof(f8030,plain,
( zero = composition(sF7,sF1)
| ~ spl10_4
| ~ spl10_28 ),
inference(forward_demodulation,[],[f8009,f108]) ).
fof(f9239,definition,
( spl10_30
<=> zero = composition(sF7,sF1) ),
introduced(definition,[new_symbols(definition,[spl10_30])],[avatar_definition]) ).
fof(f9241,plain,
( zero = composition(sF7,sF1)
| ~ spl10_30 ),
inference(avatar_component_clause,[],[f9239]) ).
fof(f9242,plain,
( spl10_30
| ~ spl10_4
| ~ spl10_28 ),
inference(avatar_split_clause,[],[f8030,f7992,f106,f9239]) ).
fof(f9254,plain,
( ! [X0] : join(zero,composition(sF7,X0)) = composition(sF7,join(sF1,X0))
| ~ spl10_30 ),
inference(superposition,[],[f345,f9241]) ).
fof(f9267,plain,
( ! [X0] : composition(sF7,X0) = composition(sF7,join(sF1,X0))
| ~ spl10_4
| ~ spl10_30 ),
inference(forward_demodulation,[],[f9254,f1355]) ).
fof(f11362,definition,
( spl10_36
<=> join(sF1,sk2) = join(sF1,sF4) ),
introduced(definition,[new_symbols(definition,[spl10_36])],[avatar_definition]) ).
fof(f11364,plain,
( join(sF1,sk2) = join(sF1,sF4)
| ~ spl10_36 ),
inference(avatar_component_clause,[],[f11362]) ).
fof(f11365,plain,
( spl10_36
| ~ spl10_2
| ~ spl10_4
| ~ spl10_11
| ~ spl10_14 ),
inference(avatar_split_clause,[],[f1856,f785,f229,f106,f91,f11362]) ).
fof(f11385,plain,
( join(composition(sF7,sF1),sF4) = join(sF4,composition(sF7,join(sF1,sk2)))
| ~ spl10_23
| ~ spl10_36 ),
inference(superposition,[],[f6529,f11364]) ).
fof(f11388,plain,
( join(sF4,composition(sF7,sk2)) = join(composition(sF7,sF1),sF4)
| ~ spl10_4
| ~ spl10_23
| ~ spl10_30
| ~ spl10_36 ),
inference(forward_demodulation,[],[f11385,f9267]) ).
fof(f11405,plain,
( join(sF4,composition(sF7,sk2)) = join(sF4,composition(sF7,sF1))
| ~ spl10_4
| ~ spl10_23
| ~ spl10_30
| ~ spl10_36 ),
inference(forward_demodulation,[],[f11388,f1]) ).
fof(f11417,plain,
( join(sF4,composition(sF7,sk2)) = join(sF4,zero)
| ~ spl10_4
| ~ spl10_23
| ~ spl10_30
| ~ spl10_36 ),
inference(forward_demodulation,[],[f11405,f9241]) ).
fof(f11427,plain,
( join(sF4,composition(sF7,sk2)) = join(zero,sF4)
| ~ spl10_4
| ~ spl10_23
| ~ spl10_30
| ~ spl10_36 ),
inference(forward_demodulation,[],[f11417,f1]) ).
fof(f11436,plain,
( sF4 = join(sF4,composition(sF7,sk2))
| ~ spl10_4
| ~ spl10_23
| ~ spl10_30
| ~ spl10_36 ),
inference(forward_demodulation,[],[f11427,f1355]) ).
fof(f11444,plain,
( sF4 = join(sF4,sF8)
| ~ spl10_4
| ~ spl10_13
| ~ spl10_23
| ~ spl10_30
| ~ spl10_36 ),
inference(forward_demodulation,[],[f11436,f389]) ).
fof(f11451,plain,
( sF4 = join(sF8,sF4)
| ~ spl10_4
| ~ spl10_13
| ~ spl10_23
| ~ spl10_30
| ~ spl10_36 ),
inference(forward_demodulation,[],[f11444,f1]) ).
fof(f11456,plain,
( sF4 = sF9
| ~ spl10_4
| ~ spl10_7
| ~ spl10_13
| ~ spl10_23
| ~ spl10_30
| ~ spl10_36 ),
inference(forward_demodulation,[],[f11451,f135]) ).
fof(f11460,plain,
( $false
| ~ spl10_4
| spl10_5
| ~ spl10_7
| ~ spl10_13
| ~ spl10_23
| ~ spl10_30
| ~ spl10_36 ),
inference(forward_subsumption_resolution,[],[f11456,f113]) ).
fof(f11461,plain,
( ~ spl10_4
| spl10_5
| ~ spl10_7
| ~ spl10_13
| ~ spl10_23
| ~ spl10_30
| ~ spl10_36 ),
inference(avatar_contradiction_clause,[],[f11460]) ).
cnf(s1,plain,
spl10_1,
inference(sat_conversion,[],[f69]) ).
cnf(s2,plain,
spl10_2,
inference(sat_conversion,[],[f94]) ).
cnf(s4,plain,
spl10_4,
inference(sat_conversion,[],[f109]) ).
cnf(s5,plain,
~ spl10_5,
inference(sat_conversion,[],[f114]) ).
cnf(s6,plain,
spl10_6,
inference(sat_conversion,[],[f119]) ).
cnf(s7,plain,
spl10_7,
inference(sat_conversion,[],[f136]) ).
cnf(s8,plain,
spl10_8,
inference(sat_conversion,[],[f151]) ).
cnf(s9,plain,
spl10_9,
inference(sat_conversion,[],[f210]) ).
cnf(s10,plain,
spl10_10,
inference(sat_conversion,[],[f216]) ).
cnf(s11,plain,
spl10_11,
inference(sat_conversion,[],[f232]) ).
cnf(s12,plain,
spl10_12,
inference(sat_conversion,[],[f238]) ).
cnf(s13,plain,
spl10_13,
inference(sat_conversion,[],[f390]) ).
cnf(s14,plain,
( ~ spl10_4
| ~ spl10_8
| spl10_14 ),
inference(sat_conversion,[],[f788]) ).
cnf(s23,plain,
( ~ spl10_4
| ~ spl10_6
| ~ spl10_9
| ~ spl10_10
| ~ spl10_12
| spl10_23 ),
inference(sat_conversion,[],[f4826]) ).
cnf(s24,plain,
( ~ spl10_6
| spl10_24 ),
inference(sat_conversion,[],[f5368]) ).
cnf(s28,plain,
( ~ spl10_1
| ~ spl10_4
| ~ spl10_6
| ~ spl10_9
| ~ spl10_10
| ~ spl10_12
| ~ spl10_23
| ~ spl10_24
| spl10_28 ),
inference(sat_conversion,[],[f7995]) ).
cnf(s30,plain,
( ~ spl10_4
| ~ spl10_28
| spl10_30 ),
inference(sat_conversion,[],[f9242]) ).
cnf(s36,plain,
( ~ spl10_2
| ~ spl10_4
| ~ spl10_11
| ~ spl10_14
| spl10_36 ),
inference(sat_conversion,[],[f11365]) ).
cnf(s37,plain,
( ~ spl10_4
| spl10_5
| ~ spl10_7
| ~ spl10_13
| ~ spl10_23
| ~ spl10_30
| ~ spl10_36 ),
inference(sat_conversion,[],[f11461]) ).
cnf(s40,plain,
spl10_24,
inference(rat,[],[s24,s6]) ).
cnf(s44,plain,
spl10_23,
inference(rat,[],[s23,s6,s12,s10,s9,s4]) ).
cnf(s50,plain,
spl10_14,
inference(rat,[],[s14,s8,s4]) ).
cnf(s51,plain,
spl10_36,
inference(rat,[],[s36,s50,s4,s11,s2]) ).
cnf(s56,plain,
~ spl10_30,
inference(rat,[],[s37,s44,s4,s5,s13,s7,s51]) ).
cnf(s57,plain,
~ spl10_28,
inference(rat,[],[s30,s4,s56]) ).
cnf(s58,plain,
~ spl10_1,
inference(rat,[],[s28,s44,s40,s4,s12,s10,s9,s6,s57]) ).
cnf(s59,plain,
$false,
inference(rat,[],[s1,s58]) ).
fof(f11466,plain,
$false,
inference(avatar_sat_refutation,[],[s59]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL021-2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.17/0.43 % Computer : n014.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Sun Sep 27 22:52:32 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.17/0.43 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.23/0.49 Running first-order theorem proving
% 0.23/0.49 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 24.49/4.58 % (1258269)Detected a unit-equality problem, will run specialized UEQ schedule.
% 24.49/4.58 % (1258288)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=626329615:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 24.49/4.58 % (1258283)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=1971913038:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 24.49/4.58 % (1258287)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=2660810437:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 24.49/4.58 % (1258286)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=401253200:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 24.49/4.58 % (1258285)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=575742925:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 24.49/4.58 % (1258284)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=3061867377:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 24.49/4.58 % (1258282)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=4011950388:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 24.49/4.58 % (1258285)Instruction limit reached!
% 24.49/4.58 % (1258285)------------------------------
% 24.49/4.58 % (1258285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.49/4.58 % (1258285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.49/4.58 % (1258285)CaDiCaL version: 2.1.3
% 24.49/4.58 % (1258285)Termination reason: Instruction limit
% 24.49/4.58 % (1258285)Termination phase: Saturation
% 24.49/4.58 % (1258285)Time elapsed: 0.133 s
% 24.49/4.58 % (1258285)Peak memory usage: 89 MB
% 24.49/4.58 % (1258285)Instructions burned: 136 (million)
% 24.49/4.58 % (1258286)Instruction limit reached!
% 24.49/4.58 % (1258286)------------------------------
% 24.49/4.58 % (1258286)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.49/4.58 % (1258286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.49/4.58 % (1258286)CaDiCaL version: 2.1.3
% 24.49/4.58 % (1258286)Termination reason: Instruction limit
% 24.49/4.58 % (1258286)Termination phase: Saturation
% 24.49/4.58 % (1258286)Time elapsed: 0.155 s
% 24.49/4.58 % (1258286)Peak memory usage: 90 MB
% 24.49/4.58 % (1258286)Instructions burned: 181 (million)
% 24.49/4.58 % (1258287)Instruction limit reached!
% 24.49/4.58 % (1258287)------------------------------
% 24.49/4.58 % (1258287)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.49/4.58 % (1258287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.49/4.58 % (1258287)CaDiCaL version: 2.1.3
% 24.49/4.58 % (1258287)Termination reason: Instruction limit
% 24.49/4.58 % (1258287)Termination phase: Saturation
% 24.49/4.58 % (1258287)Time elapsed: 0.258 s
% 24.49/4.58 % (1258287)Peak memory usage: 90 MB
% 24.49/4.58 % (1258287)Instructions burned: 257 (million)
% 24.49/4.58 % (1258298)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=1364984282:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2996 on theBenchmark for (2996ds/2051Mi)
% 24.49/4.58 % (1258299)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1371552251:i=4948:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/4948Mi)
% 24.49/4.58 % (1258300)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=919888169:i=215:ep=RSTC_2995 on theBenchmark for (2995ds/215Mi)
% 24.49/4.58 % (1258300)Instruction limit reached!
% 24.49/4.58 % (1258300)------------------------------
% 24.49/4.58 % (1258300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.49/4.58 % (1258300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.49/4.58 % (1258300)CaDiCaL version: 2.1.3
% 24.49/4.58 % (1258300)Termination reason: Instruction limit
% 24.49/4.58 % (1258300)Termination phase: Saturation
% 24.49/4.58 % (1258300)Time elapsed: 0.197 s
% 24.49/4.58 % (1258300)Peak memory usage: 92 MB
% 24.49/4.58 % (1258300)Instructions burned: 215 (million)
% 24.49/4.58 % (1258304)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=1817102536:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2991 on theBenchmark for (2991ds/317Mi)
% 24.49/4.58 % (1258288)Instruction limit reached!
% 24.49/4.58 % (1258288)------------------------------
% 24.49/4.58 % (1258288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.49/4.58 % (1258288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.49/4.58 % (1258288)CaDiCaL version: 2.1.3
% 24.49/4.58 % (1258288)Termination reason: Instruction limit
% 24.49/4.58 % (1258288)Termination phase: Saturation
% 24.49/4.58 % (1258288)Time elapsed: 1.028 s
% 24.49/4.58 % (1258288)Peak memory usage: 101 MB
% 24.49/4.58 % (1258288)Instructions burned: 1187 (million)
% 24.49/4.58 % (1258304)Instruction limit reached!
% 24.49/4.58 % (1258304)------------------------------
% 24.49/4.58 % (1258304)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.49/4.58 % (1258304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.49/4.58 % (1258304)CaDiCaL version: 2.1.3
% 24.49/4.58 % (1258304)Termination reason: Instruction limit
% 24.49/4.58 % (1258304)Termination phase: Saturation
% 24.49/4.58 % (1258304)Time elapsed: 0.152 s
% 24.49/4.58 % (1258304)Peak memory usage: 90 MB
% 24.49/4.58 % (1258304)Instructions burned: 319 (million)
% 24.49/4.58 % (1258307)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=458091781:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2987 on theBenchmark for (2987ds/2836Mi)
% 24.49/4.58 % (1258306)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=268232648:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2988 on theBenchmark for (2988ds/12125Mi)
% 24.49/4.58 % (1258298)Instruction limit reached!
% 24.49/4.58 % (1258298)------------------------------
% 24.49/4.58 % (1258298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.49/4.58 % (1258298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.49/4.58 % (1258298)CaDiCaL version: 2.1.3
% 24.49/4.58 % (1258298)Termination reason: Instruction limit
% 24.49/4.58 % (1258298)Termination phase: Saturation
% 24.49/4.58 % (1258298)Time elapsed: 2.217 s
% 24.49/4.58 % (1258298)Peak memory usage: 141 MB
% 24.49/4.58 % (1258298)Instructions burned: 2051 (million)
% 24.49/4.58 % (1258314)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1430864436:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2972 on theBenchmark for (2972ds/14534Mi)
% 24.49/4.58 % (1258307)Instruction limit reached!
% 24.49/4.58 % (1258307)------------------------------
% 24.49/4.58 % (1258307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.49/4.58 % (1258307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.49/4.58 % (1258307)CaDiCaL version: 2.1.3
% 24.49/4.58 % (1258307)Termination reason: Instruction limit
% 24.49/4.58 % (1258307)Termination phase: Saturation
% 24.49/4.58 % (1258307)Time elapsed: 1.650 s
% 24.49/4.58 % (1258307)Peak memory usage: 131 MB
% 24.49/4.58 % (1258307)Instructions burned: 2837 (million)
% 24.49/4.58 % (1258282)First to succeed.
% 24.49/4.58 % (1258282)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1258269"
% 24.49/4.58 % (1258316)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=339059978:i=11832:s2at=3:bs=on:bd=preordered:fsd=on_2969 on theBenchmark for (2969ds/11832Mi)
% 24.49/4.58 % (1258282)Refutation found. Thanks to Tanya!
% 24.49/4.58 % SZS status Unsatisfiable for theBenchmark
% 24.49/4.58 % SZS output start Proof for theBenchmark
% See solution above
% 25.62/4.73 % (1258282)------------------------------
% 25.62/4.73 % (1258282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.62/4.73 % (1258282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.62/4.73 % (1258282)CaDiCaL version: 2.1.3
% 25.62/4.73 % (1258282)Termination reason: Refutation
% 25.62/4.73 % (1258282)Time elapsed: 2.877 s
% 25.62/4.73 % (1258282)Peak memory usage: 148 MB
% 25.62/4.73 % (1258282)Instructions burned: 2720 (million)
% 25.62/4.73 % (1258282)------------------------------
% 25.62/4.73 % (1258282)------------------------------
% 25.62/4.73 % (1258269)Success in time 3.512 s
% 25.62/4.73 % Vampire exiting
%------------------------------------------------------------------------------