%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : REL033-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 : n015.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:59 PM UTC 2026
% Result : Unsatisfiable 13.88s 2.86s
% Output : Refutation 14.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 72
% Number of leaves : 28
% Syntax : Number of formulae : 329 ( 313 unt; 14 def)
% Number of atoms : 346 ( 323 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 37 ( 20 ~; 15 |; 0 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 3 prp; 0-2 aty)
% Number of functors : 23 ( 23 usr; 18 con; 0-2 aty)
% Number of variables : 277 ( 0 sgn 277 !; 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(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(f17,negated_conjecture,
composition(sk1,top) = sk1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals_14) ).
fof(f18,plain,
sk1 = composition(sk1,top),
inference(reorient_equations,[],[f17]) ).
fof(f19,negated_conjecture,
( join(composition(meet(sk1,sk2),sk3),meet(sk1,composition(sk2,sk3))) != meet(sk1,composition(sk2,sk3))
| join(meet(sk1,composition(sk2,sk3)),composition(meet(sk1,sk2),sk3)) != composition(meet(sk1,sk2),sk3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals_15) ).
fof(f20,plain,
( meet(sk1,composition(sk2,sk3)) != join(composition(meet(sk1,sk2),sk3),meet(sk1,composition(sk2,sk3)))
| composition(meet(sk1,sk2),sk3) != join(meet(sk1,composition(sk2,sk3)),composition(meet(sk1,sk2),sk3)) ),
inference(reorient_equations,[],[f19]) ).
fof(f21,plain,
! [X0] : zero = complement(join(complement(X0),complement(complement(X0)))),
inference(definition_unfolding,[],[f16,f6]) ).
fof(f22,plain,
( complement(join(complement(sk1),complement(composition(sk2,sk3)))) != join(composition(complement(join(complement(sk1),complement(sk2))),sk3),complement(join(complement(sk1),complement(composition(sk2,sk3)))))
| composition(complement(join(complement(sk1),complement(sk2))),sk3) != join(complement(join(complement(sk1),complement(composition(sk2,sk3)))),composition(complement(join(complement(sk1),complement(sk2))),sk3)) ),
inference(definition_unfolding,[],[f20,f6,f6,f6,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 = composition(sk2,sk3),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f29,plain,
composition(sk2,sk3) = sF2,
inference(reorient_equations,[],[f28]) ).
fof(f30,definition,
sF3 = complement(sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f31,plain,
complement(sF2) = sF3,
inference(reorient_equations,[],[f30]) ).
fof(f32,definition,
sF4 = join(sF1,sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f33,plain,
join(sF1,sF3) = sF4,
inference(reorient_equations,[],[f32]) ).
fof(f34,definition,
sF5 = complement(sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f35,plain,
complement(sF4) = 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 = composition(sF8,sk3),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f43,plain,
composition(sF8,sk3) = sF9,
inference(reorient_equations,[],[f42]) ).
fof(f44,definition,
sF10 = join(sF9,sF5),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f45,plain,
join(sF9,sF5) = sF10,
inference(reorient_equations,[],[f44]) ).
fof(f46,definition,
sF11 = join(sF5,sF9),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f47,plain,
join(sF5,sF9) = sF11,
inference(reorient_equations,[],[f46]) ).
fof(f48,plain,
( sF5 != sF10
| sF9 != sF11 ),
inference(definition_folding,[],[f22,f47,f43,f41,f39,f37,f27,f35,f33,f31,f29,f27,f43,f41,f39,f37,f27,f45,f35,f33,f31,f29,f27,f43,f41,f39,f37,f27,f35,f33,f31,f29,f27]) ).
fof(f50,definition,
( spl12_1
<=> sF9 = sF11 ),
introduced(definition,[new_symbols(definition,[spl12_1])],[avatar_definition]) ).
fof(f52,plain,
( sF9 != sF11
| spl12_1 ),
inference(avatar_component_clause,[],[f50]) ).
fof(f54,definition,
( spl12_2
<=> sF5 = sF10 ),
introduced(definition,[new_symbols(definition,[spl12_2])],[avatar_definition]) ).
fof(f55,plain,
( sF5 = sF10
| ~ spl12_2 ),
inference(avatar_component_clause,[],[f54]) ).
fof(f57,plain,
( ~ spl12_1
| ~ spl12_2 ),
inference(avatar_split_clause,[],[f48,f54,f50]) ).
fof(f58,plain,
zero = complement(top),
inference(backward_demodulation,[],[f21,f15]) ).
fof(f59,plain,
sk1 = composition(sk1,top),
inference(forward_demodulation,[],[f24,f25]) ).
fof(f60,plain,
sF4 = join(sF3,sF1),
inference(forward_demodulation,[],[f33,f1]) ).
fof(f61,plain,
sF7 = join(sF6,sF1),
inference(forward_demodulation,[],[f39,f1]) ).
fof(f62,plain,
sF10 = join(sF5,sF9),
inference(forward_demodulation,[],[f45,f1]) ).
fof(f63,plain,
sF4 = join(sF3,complement(sk1)),
inference(forward_demodulation,[],[f60,f27]) ).
fof(f64,plain,
sF7 = join(sF6,complement(sk1)),
inference(forward_demodulation,[],[f61,f27]) ).
fof(f65,plain,
sF10 = sF11,
inference(backward_demodulation,[],[f47,f62]) ).
fof(f66,plain,
sF7 = join(complement(sk2),complement(sk1)),
inference(forward_demodulation,[],[f64,f37]) ).
fof(f67,plain,
( sF9 != sF10
| spl12_1 ),
inference(forward_demodulation,[],[f52,f65]) ).
fof(f72,plain,
complement(top) = join(composition(converse(sk1),complement(sk1)),complement(top)),
inference(superposition,[],[f14,f59]) ).
fof(f75,plain,
complement(top) = join(complement(top),composition(converse(sk1),complement(sk1))),
inference(forward_demodulation,[],[f72,f1]) ).
fof(f77,plain,
zero = join(zero,composition(converse(sk1),complement(sk1))),
inference(forward_demodulation,[],[f75,f58]) ).
fof(f88,plain,
! [X0] : composition(join(sF8,X0),sk3) = join(sF9,composition(X0,sk3)),
inference(superposition,[],[f9,f43]) ).
fof(f90,plain,
! [X0,X1] : converse(join(converse(X0),X1)) = join(X0,converse(X1)),
inference(superposition,[],[f11,f10]) ).
fof(f91,plain,
! [X0,X1] : converse(join(X1,converse(X0))) = join(converse(X1),X0),
inference(superposition,[],[f11,f10]) ).
fof(f105,plain,
! [X0,X1] : join(complement(join(complement(X0),complement(X1))),complement(join(complement(X1),X0))) = X1,
inference(superposition,[],[f4,f1]) ).
fof(f122,plain,
! [X0,X1] : join(complement(join(complement(X1),X0)),complement(join(complement(X0),complement(X1)))) = X1,
inference(forward_demodulation,[],[f105,f1]) ).
fof(f143,plain,
! [X0,X1] : converse(composition(X1,converse(X0))) = composition(X0,converse(X1)),
inference(superposition,[],[f12,f10]) ).
fof(f144,plain,
! [X0,X1] : composition(converse(X1),X0) = converse(composition(converse(X0),X1)),
inference(superposition,[],[f12,f10]) ).
fof(f145,plain,
! [X0,X1] : complement(converse(X0)) = join(composition(converse(converse(X1)),complement(converse(composition(X0,X1)))),complement(converse(X0))),
inference(superposition,[],[f14,f12]) ).
fof(f147,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(f148,plain,
! [X0,X1] : complement(converse(X0)) = join(complement(converse(X0)),composition(converse(converse(X1)),complement(converse(composition(X0,X1))))),
inference(forward_demodulation,[],[f145,f1]) ).
fof(f149,plain,
! [X0,X1] : complement(converse(X0)) = join(complement(converse(X0)),composition(X1,complement(converse(composition(X0,X1))))),
inference(forward_demodulation,[],[f148,f10]) ).
fof(f154,plain,
! [X0] : join(complement(top),complement(join(complement(X0),complement(X0)))) = X0,
inference(superposition,[],[f4,f15]) ).
fof(f155,plain,
! [X0] : join(complement(join(complement(X0),complement(complement(complement(X0))))),complement(top)) = X0,
inference(superposition,[],[f4,f15]) ).
fof(f156,plain,
! [X0] : join(complement(top),complement(join(complement(X0),complement(complement(complement(X0)))))) = X0,
inference(forward_demodulation,[],[f155,f1]) ).
fof(f157,plain,
! [X0] : join(zero,complement(join(complement(X0),complement(X0)))) = X0,
inference(forward_demodulation,[],[f154,f58]) ).
fof(f159,plain,
! [X0] : join(zero,complement(join(complement(X0),complement(complement(complement(X0)))))) = X0,
inference(forward_demodulation,[],[f156,f58]) ).
fof(f168,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(top,X1),
inference(superposition,[],[f2,f15]) ).
fof(f170,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(f179,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f1,f2]) ).
fof(f182,plain,
! [X2,X0,X1] : join(X0,X2) = join(complement(join(complement(X0),X1)),join(X2,complement(join(complement(X0),complement(X1))))),
inference(forward_demodulation,[],[f170,f179]) ).
fof(f199,plain,
! [X0] : join(sF3,join(complement(sk1),X0)) = join(sF4,X0),
inference(superposition,[],[f2,f63]) ).
fof(f203,plain,
! [X0] : converse(converse(X0)) = composition(converse(one),X0),
inference(superposition,[],[f144,f8]) ).
fof(f213,plain,
! [X0] : composition(converse(one),X0) = X0,
inference(forward_demodulation,[],[f203,f10]) ).
fof(f222,plain,
! [X0] : complement(X0) = join(complement(composition(one,X0)),complement(X0)),
inference(superposition,[],[f14,f213]) ).
fof(f229,plain,
one = converse(one),
inference(superposition,[],[f8,f213]) ).
fof(f230,plain,
! [X0] : composition(one,X0) = X0,
inference(backward_demodulation,[],[f213,f229]) ).
fof(f235,plain,
! [X0] : complement(X0) = join(complement(X0),complement(composition(one,X0))),
inference(forward_demodulation,[],[f222,f1]) ).
fof(f238,plain,
! [X0] : complement(X0) = join(complement(X0),complement(X0)),
inference(forward_demodulation,[],[f235,f230]) ).
fof(f240,plain,
! [X0] : join(zero,complement(complement(X0))) = X0,
inference(backward_demodulation,[],[f157,f238]) ).
fof(f264,plain,
sF2 = join(zero,complement(sF3)),
inference(superposition,[],[f240,f31]) ).
fof(f265,plain,
sF4 = join(zero,complement(sF5)),
inference(superposition,[],[f240,f35]) ).
fof(f266,plain,
sF7 = join(zero,complement(sF8)),
inference(superposition,[],[f240,f41]) ).
fof(f301,plain,
! [X2,X0,X1] : composition(join(converse(X2),converse(X1)),converse(X0)) = join(converse(composition(X0,X2)),converse(composition(X0,X1))),
inference(superposition,[],[f147,f12]) ).
fof(f307,plain,
! [X2,X0,X1] : composition(join(converse(X2),converse(X1)),converse(X0)) = converse(join(composition(X0,X2),composition(X0,X1))),
inference(forward_demodulation,[],[f301,f11]) ).
fof(f317,plain,
! [X2,X0,X1] : converse(join(composition(X0,X2),composition(X0,X1))) = composition(converse(join(X2,X1)),converse(X0)),
inference(forward_demodulation,[],[f307,f11]) ).
fof(f323,plain,
! [X2,X0,X1] : converse(join(composition(X0,X2),composition(X0,X1))) = converse(composition(X0,join(X2,X1))),
inference(forward_demodulation,[],[f317,f12]) ).
fof(f347,plain,
! [X2,X0,X1] : join(composition(X0,X1),composition(X0,X2)) = converse(converse(composition(X0,join(X1,X2)))),
inference(superposition,[],[f10,f323]) ).
fof(f362,plain,
! [X2,X0,X1] : composition(X0,join(X1,X2)) = join(composition(X0,X1),composition(X0,X2)),
inference(forward_demodulation,[],[f347,f10]) ).
fof(f392,plain,
! [X0,X1] : join(X0,composition(X0,X1)) = composition(X0,join(one,X1)),
inference(superposition,[],[f362,f8]) ).
fof(f403,plain,
! [X0] : composition(sk1,join(X0,top)) = join(composition(sk1,X0),sk1),
inference(superposition,[],[f362,f59]) ).
fof(f410,plain,
! [X2,X3,X0,X1] : join(composition(X0,join(X1,X2)),X3) = join(composition(X0,X1),join(composition(X0,X2),X3)),
inference(superposition,[],[f2,f362]) ).
fof(f415,plain,
! [X0] : join(sk1,composition(sk1,X0)) = composition(sk1,join(X0,top)),
inference(forward_demodulation,[],[f403,f1]) ).
fof(f425,plain,
! [X0] : composition(sk1,join(X0,top)) = composition(sk1,join(one,X0)),
inference(forward_demodulation,[],[f415,f392]) ).
fof(f460,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(X1,top),
inference(superposition,[],[f179,f15]) ).
fof(f516,plain,
! [X0] : join(complement(sk2),join(complement(sk1),X0)) = join(sF7,X0),
inference(superposition,[],[f2,f66]) ).
fof(f531,plain,
! [X0] : join(X0,top) = join(top,complement(complement(X0))),
inference(superposition,[],[f168,f15]) ).
fof(f562,plain,
! [X0] : join(X0,complement(X0)) = join(top,complement(X0)),
inference(superposition,[],[f168,f238]) ).
fof(f568,plain,
! [X0] : top = join(top,complement(X0)),
inference(forward_demodulation,[],[f562,f15]) ).
fof(f573,plain,
! [X0] : top = join(X0,top),
inference(backward_demodulation,[],[f531,f568]) ).
fof(f578,plain,
! [X0,X1] : top = join(X0,join(complement(X0),X1)),
inference(backward_demodulation,[],[f460,f573]) ).
fof(f579,plain,
! [X0] : composition(sk1,top) = composition(sk1,join(one,X0)),
inference(backward_demodulation,[],[f425,f573]) ).
fof(f583,plain,
! [X0] : sk1 = composition(sk1,join(one,X0)),
inference(forward_demodulation,[],[f579,f59]) ).
fof(f584,plain,
! [X1] : top = join(top,X1),
inference(backward_demodulation,[],[f168,f578]) ).
fof(f654,plain,
! [X0] : complement(X0) = join(complement(join(complement(complement(X0)),X0)),complement(top)),
inference(superposition,[],[f122,f15]) ).
fof(f665,plain,
! [X0] : complement(X0) = join(complement(top),complement(join(complement(complement(X0)),X0))),
inference(forward_demodulation,[],[f654,f1]) ).
fof(f679,plain,
! [X0] : complement(X0) = join(complement(top),complement(join(X0,complement(complement(X0))))),
inference(forward_demodulation,[],[f665,f1]) ).
fof(f688,plain,
! [X0] : complement(X0) = join(zero,complement(join(X0,complement(complement(X0))))),
inference(forward_demodulation,[],[f679,f58]) ).
fof(f695,plain,
! [X0] : complement(complement(X0)) = X0,
inference(backward_demodulation,[],[f159,f688]) ).
fof(f699,plain,
! [X0] : join(zero,X0) = X0,
inference(backward_demodulation,[],[f240,f695]) ).
fof(f719,plain,
sF2 = complement(sF3),
inference(backward_demodulation,[],[f264,f699]) ).
fof(f720,plain,
sF4 = complement(sF5),
inference(backward_demodulation,[],[f265,f699]) ).
fof(f721,plain,
sF7 = complement(sF8),
inference(backward_demodulation,[],[f266,f699]) ).
fof(f722,plain,
zero = composition(converse(sk1),complement(sk1)),
inference(backward_demodulation,[],[f77,f699]) ).
fof(f740,plain,
! [X0] : join(X0,zero) = X0,
inference(superposition,[],[f1,f699]) ).
fof(f743,plain,
top = complement(zero),
inference(superposition,[],[f15,f699]) ).
fof(f752,plain,
! [X0,X1] : complement(X0) = join(complement(join(X0,complement(X1))),complement(join(X0,X1))),
inference(superposition,[],[f4,f695]) ).
fof(f758,plain,
! [X0,X1] : complement(X0) = join(complement(join(X0,X1)),complement(join(complement(X1),X0))),
inference(superposition,[],[f122,f695]) ).
fof(f759,plain,
! [X0] : join(X0,X0) = X0,
inference(superposition,[],[f238,f695]) ).
fof(f773,plain,
! [X0,X1] : complement(X0) = join(complement(join(X0,X1)),complement(join(X0,complement(X1)))),
inference(forward_demodulation,[],[f752,f1]) ).
fof(f817,plain,
! [X0,X1] : join(X0,X1) = join(complement(complement(X0)),complement(join(complement(join(X0,X1)),join(X0,complement(X1))))),
inference(superposition,[],[f4,f773]) ).
fof(f824,plain,
! [X0,X1] : join(X0,X1) = join(complement(complement(X0)),complement(join(complement(X1),join(complement(join(X0,X1)),X0)))),
inference(forward_demodulation,[],[f817,f179]) ).
fof(f854,plain,
! [X0,X1] : join(X0,X1) = join(complement(complement(X0)),complement(join(complement(X1),join(X0,complement(join(X0,X1)))))),
inference(forward_demodulation,[],[f824,f1]) ).
fof(f872,plain,
! [X0,X1] : join(X0,X1) = join(X0,complement(join(complement(X1),join(X0,complement(join(X0,X1)))))),
inference(forward_demodulation,[],[f854,f695]) ).
fof(f910,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X0,X1)),
inference(superposition,[],[f2,f759]) ).
fof(f948,plain,
! [X0,X1] : complement(X1) = join(complement(join(X0,X1)),complement(join(complement(X0),X1))),
inference(superposition,[],[f758,f1]) ).
fof(f975,plain,
! [X0,X1] : complement(complement(join(complement(X1),X0))) = join(complement(join(complement(join(complement(X1),X0)),join(X0,X1))),complement(complement(X0))),
inference(superposition,[],[f758,f758]) ).
fof(f1008,plain,
! [X0,X1] : complement(complement(join(complement(X1),X0))) = join(complement(complement(X0)),complement(join(complement(join(complement(X1),X0)),join(X0,X1)))),
inference(forward_demodulation,[],[f975,f1]) ).
fof(f1043,plain,
! [X0,X1] : complement(complement(join(complement(X1),X0))) = join(complement(complement(X0)),complement(join(join(X0,X1),complement(join(complement(X1),X0))))),
inference(forward_demodulation,[],[f1008,f1]) ).
fof(f1067,plain,
! [X0,X1] : complement(complement(join(complement(X1),X0))) = join(complement(complement(X0)),complement(join(X0,join(X1,complement(join(complement(X1),X0)))))),
inference(forward_demodulation,[],[f1043,f2]) ).
fof(f1085,plain,
! [X0,X1] : complement(complement(join(complement(X1),X0))) = join(X0,complement(join(X0,join(X1,complement(join(complement(X1),X0)))))),
inference(forward_demodulation,[],[f1067,f695]) ).
fof(f1099,plain,
! [X0,X1] : join(complement(X1),X0) = join(X0,complement(join(X0,join(X1,complement(join(complement(X1),X0)))))),
inference(forward_demodulation,[],[f1085,f695]) ).
fof(f1110,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(complement(complement(X0)),join(X2,complement(join(complement(join(X0,X1)),complement(complement(join(X0,complement(X1)))))))),
inference(superposition,[],[f182,f773]) ).
fof(f1140,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))) = join(X0,complement(join(complement(X0),complement(X1)))),
inference(superposition,[],[f182,f759]) ).
fof(f1174,plain,
! [X0,X1] : complement(complement(X0)) = join(X0,complement(join(complement(X0),complement(X1)))),
inference(forward_demodulation,[],[f1140,f773]) ).
fof(f1196,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(complement(complement(X0)),join(X2,complement(join(complement(join(X0,X1)),join(X0,complement(X1)))))),
inference(forward_demodulation,[],[f1110,f695]) ).
fof(f1208,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),complement(X1)))) = X0,
inference(forward_demodulation,[],[f1174,f695]) ).
fof(f1224,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(complement(complement(X0)),join(X2,complement(join(complement(X1),join(complement(join(X0,X1)),X0))))),
inference(forward_demodulation,[],[f1196,f179]) ).
fof(f1242,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(complement(complement(X0)),join(X2,complement(join(complement(X1),join(X0,complement(join(X0,X1))))))),
inference(forward_demodulation,[],[f1224,f1]) ).
fof(f1255,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X0,join(X2,complement(join(complement(X1),join(X0,complement(join(X0,X1))))))),
inference(forward_demodulation,[],[f1242,f695]) ).
fof(f1265,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X0,join(X2,complement(join(complement(X1),join(X0,complement(join(X0,X1))))))),
inference(forward_demodulation,[],[f1255,f2]) ).
fof(f1278,plain,
! [X0,X1] : join(X1,complement(join(complement(X1),X0))) = X1,
inference(superposition,[],[f1208,f695]) ).
fof(f1286,plain,
sk2 = join(sk2,complement(sF7)),
inference(superposition,[],[f1208,f66]) ).
fof(f1319,plain,
sk2 = join(sk2,sF8),
inference(forward_demodulation,[],[f1286,f41]) ).
fof(f1324,plain,
! [X0,X1] : join(complement(X1),X0) = join(X0,complement(join(X0,X1))),
inference(backward_demodulation,[],[f1099,f1278]) ).
fof(f1337,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X0,join(X2,complement(join(complement(X1),join(complement(X1),X0))))),
inference(backward_demodulation,[],[f1265,f1324]) ).
fof(f1339,plain,
! [X0,X1] : join(X0,X1) = join(X0,complement(join(complement(X1),join(complement(X1),X0)))),
inference(backward_demodulation,[],[f872,f1324]) ).
fof(f1349,plain,
! [X0,X1] : join(X0,X1) = join(X0,complement(join(complement(X1),X0))),
inference(forward_demodulation,[],[f1339,f910]) ).
fof(f1351,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X0,join(X2,complement(join(complement(X1),X0)))),
inference(forward_demodulation,[],[f1337,f910]) ).
fof(f1359,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X0,X1))),
inference(superposition,[],[f1278,f695]) ).
fof(f1429,plain,
! [X0,X1] : complement(X1) = join(complement(X1),complement(join(X0,X1))),
inference(superposition,[],[f1359,f1]) ).
fof(f1449,plain,
complement(sF3) = join(complement(sF3),complement(sF4)),
inference(superposition,[],[f1359,f63]) ).
fof(f1470,plain,
complement(sF3) = join(complement(sF3),sF5),
inference(forward_demodulation,[],[f1449,f35]) ).
fof(f1487,plain,
complement(sF3) = join(sF5,complement(sF3)),
inference(forward_demodulation,[],[f1470,f1]) ).
fof(f1496,plain,
sF2 = join(sF5,sF2),
inference(forward_demodulation,[],[f1487,f719]) ).
fof(f1501,plain,
sF2 = join(sF2,sF5),
inference(forward_demodulation,[],[f1496,f1]) ).
fof(f1523,plain,
complement(complement(sk1)) = join(complement(complement(sk1)),complement(sF7)),
inference(superposition,[],[f1429,f66]) ).
fof(f1534,plain,
complement(complement(sk1)) = join(complement(complement(sk1)),complement(sF4)),
inference(superposition,[],[f1429,f63]) ).
fof(f1555,plain,
complement(complement(sk1)) = join(complement(sF4),complement(complement(sk1))),
inference(forward_demodulation,[],[f1534,f1]) ).
fof(f1559,plain,
complement(complement(sk1)) = join(complement(complement(sk1)),sF8),
inference(forward_demodulation,[],[f1523,f41]) ).
fof(f1568,plain,
sk1 = join(complement(sF4),sk1),
inference(forward_demodulation,[],[f1555,f695]) ).
fof(f1572,plain,
complement(complement(sk1)) = join(sF8,complement(complement(sk1))),
inference(forward_demodulation,[],[f1559,f1]) ).
fof(f1580,plain,
sk1 = join(sk1,complement(sF4)),
inference(forward_demodulation,[],[f1568,f1]) ).
fof(f1583,plain,
sk1 = join(sF8,sk1),
inference(forward_demodulation,[],[f1572,f695]) ).
fof(f1588,plain,
sk1 = join(sk1,sF5),
inference(forward_demodulation,[],[f1580,f35]) ).
fof(f1591,plain,
sk1 = join(sk1,sF8),
inference(forward_demodulation,[],[f1583,f1]) ).
fof(f1596,plain,
! [X0] : join(sk1,X0) = join(sk1,join(sF5,X0)),
inference(superposition,[],[f2,f1588]) ).
fof(f1627,plain,
! [X0,X1] : join(X1,complement(join(X0,X1))) = join(X1,complement(X0)),
inference(superposition,[],[f1349,f695]) ).
fof(f1635,plain,
join(complement(sk1),sk2) = join(complement(sk1),complement(sF7)),
inference(superposition,[],[f1349,f66]) ).
fof(f1695,plain,
join(complement(sk1),sk2) = join(complement(sk1),sF8),
inference(forward_demodulation,[],[f1635,f41]) ).
fof(f1728,plain,
join(sk2,complement(sk1)) = join(complement(sk1),sF8),
inference(forward_demodulation,[],[f1695,f1]) ).
fof(f1765,plain,
! [X0,X1] : join(X0,complement(X1)) = join(X0,complement(join(X0,X1))),
inference(superposition,[],[f1627,f1]) ).
fof(f1771,plain,
! [X2,X0,X1] : join(X2,complement(join(X0,X1))) = join(X2,complement(join(X0,join(X1,X2)))),
inference(superposition,[],[f1627,f2]) ).
fof(f1783,plain,
join(complement(sk1),complement(sF3)) = join(complement(sk1),complement(sF4)),
inference(superposition,[],[f1627,f63]) ).
fof(f1799,plain,
! [X2,X0,X1] : join(join(X0,X1),complement(X2)) = join(X0,join(X1,complement(join(X2,join(X0,X1))))),
inference(superposition,[],[f2,f1627]) ).
fof(f1810,plain,
! [X2,X0,X1] : join(X0,join(X1,complement(X2))) = join(X0,join(X1,complement(join(X2,join(X0,X1))))),
inference(forward_demodulation,[],[f1799,f2]) ).
fof(f1825,plain,
join(complement(sk1),complement(sF3)) = join(complement(sk1),sF5),
inference(forward_demodulation,[],[f1783,f35]) ).
fof(f1844,plain,
! [X2,X0,X1] : join(X0,join(X1,complement(X2))) = join(X0,join(X1,complement(join(X2,X0)))),
inference(forward_demodulation,[],[f1810,f1771]) ).
fof(f1852,plain,
join(complement(sk1),sF5) = join(complement(sk1),sF2),
inference(forward_demodulation,[],[f1825,f719]) ).
fof(f1867,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X0,join(X2,complement(complement(X1)))),
inference(backward_demodulation,[],[f1351,f1844]) ).
fof(f1872,plain,
join(complement(sk1),sF5) = join(sF2,complement(sk1)),
inference(forward_demodulation,[],[f1852,f1]) ).
fof(f1881,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X0,join(X2,X1)),
inference(forward_demodulation,[],[f1867,f695]) ).
fof(f2076,plain,
join(sF2,complement(sF2)) = join(complement(sF5),sF2),
inference(superposition,[],[f1324,f1501]) ).
fof(f2080,plain,
join(sF2,complement(sF2)) = join(sF2,complement(sF5)),
inference(forward_demodulation,[],[f2076,f1]) ).
fof(f2083,plain,
join(sF2,complement(sF2)) = join(sF2,sF4),
inference(forward_demodulation,[],[f2080,f720]) ).
fof(f2085,plain,
top = join(sF2,sF4),
inference(forward_demodulation,[],[f2083,f15]) ).
fof(f2312,plain,
! [X2,X0,X1] : join(X0,complement(join(X0,join(X1,X2)))) = join(X0,complement(join(X2,X1))),
inference(superposition,[],[f1765,f1881]) ).
fof(f2322,plain,
! [X2,X0,X1] : join(complement(join(X1,X2)),X0) = join(X0,complement(join(X2,X1))),
inference(forward_demodulation,[],[f2312,f1324]) ).
fof(f2996,plain,
! [X0] : converse(top) = join(X0,converse(complement(converse(X0)))),
inference(superposition,[],[f90,f15]) ).
fof(f3066,plain,
composition(join(sF8,sk2),sk3) = join(sF9,sF2),
inference(superposition,[],[f88,f29]) ).
fof(f3102,plain,
composition(join(sF8,sk2),sk3) = join(sF2,sF9),
inference(forward_demodulation,[],[f3066,f1]) ).
fof(f3106,plain,
join(sF2,sF9) = composition(join(sk2,sF8),sk3),
inference(forward_demodulation,[],[f3102,f1]) ).
fof(f3108,plain,
composition(sk2,sk3) = join(sF2,sF9),
inference(forward_demodulation,[],[f3106,f1319]) ).
fof(f3109,plain,
sF2 = join(sF2,sF9),
inference(forward_demodulation,[],[f3108,f29]) ).
fof(f3118,plain,
complement(sF9) = join(complement(sF9),complement(sF2)),
inference(superposition,[],[f1429,f3109]) ).
fof(f3121,plain,
complement(sF9) = join(complement(sF2),complement(sF9)),
inference(forward_demodulation,[],[f3118,f1]) ).
fof(f3124,plain,
complement(sF9) = join(sF3,complement(sF9)),
inference(forward_demodulation,[],[f3121,f31]) ).
fof(f3744,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,[],[f410,f9]) ).
fof(f5276,plain,
! [X2,X0,X1] : join(composition(X0,X1),composition(join(X0,X2),complement(X1))) = join(composition(X0,top),composition(X2,complement(X1))),
inference(superposition,[],[f3744,f15]) ).
fof(f5351,plain,
! [X0,X1] : join(composition(sk1,join(top,X0)),composition(X1,X0)) = join(sk1,composition(join(sk1,X1),X0)),
inference(superposition,[],[f3744,f59]) ).
fof(f5530,plain,
! [X0,X1] : join(sk1,composition(join(sk1,X1),X0)) = join(composition(sk1,top),composition(X1,X0)),
inference(forward_demodulation,[],[f5351,f584]) ).
fof(f5594,plain,
! [X0,X1] : join(sk1,composition(join(sk1,X1),X0)) = join(sk1,composition(X1,X0)),
inference(forward_demodulation,[],[f5530,f59]) ).
fof(f6503,plain,
! [X0] : join(X0,complement(converse(complement(converse(X0))))) = join(X0,complement(converse(top))),
inference(superposition,[],[f1765,f2996]) ).
fof(f6520,plain,
top = converse(top),
inference(superposition,[],[f584,f2996]) ).
fof(f6547,plain,
! [X0] : join(X0,complement(top)) = join(X0,complement(converse(complement(converse(X0))))),
inference(forward_demodulation,[],[f6503,f6520]) ).
fof(f6586,plain,
! [X0] : join(X0,zero) = join(X0,complement(converse(complement(converse(X0))))),
inference(forward_demodulation,[],[f6547,f58]) ).
fof(f6612,plain,
! [X0] : join(X0,complement(converse(complement(converse(X0))))) = X0,
inference(forward_demodulation,[],[f6586,f740]) ).
fof(f6647,plain,
! [X0] : converse(composition(X0,top)) = composition(top,converse(X0)),
inference(superposition,[],[f12,f6520]) ).
fof(f6829,plain,
! [X0] : complement(complement(converse(complement(converse(complement(X0)))))) = join(complement(join(X0,complement(converse(complement(converse(complement(X0))))))),complement(complement(X0))),
inference(superposition,[],[f948,f6612]) ).
fof(f6836,plain,
! [X0] : converse(converse(X0)) = join(X0,converse(complement(converse(complement(converse(converse(X0))))))),
inference(superposition,[],[f90,f6612]) ).
fof(f6843,plain,
! [X0] : join(X0,converse(complement(converse(complement(X0))))) = X0,
inference(forward_demodulation,[],[f6836,f10]) ).
fof(f6850,plain,
! [X0] : complement(complement(converse(complement(converse(complement(X0)))))) = join(complement(complement(X0)),complement(join(X0,complement(converse(complement(converse(complement(X0)))))))),
inference(forward_demodulation,[],[f6829,f1]) ).
fof(f6876,plain,
! [X0] : complement(complement(converse(complement(converse(complement(X0)))))) = join(X0,complement(join(X0,complement(converse(complement(converse(complement(X0)))))))),
inference(forward_demodulation,[],[f6850,f695]) ).
fof(f6888,plain,
! [X0] : complement(complement(converse(complement(converse(complement(X0)))))) = join(complement(complement(converse(complement(converse(complement(X0)))))),X0),
inference(forward_demodulation,[],[f6876,f1324]) ).
fof(f6893,plain,
! [X0] : complement(complement(converse(complement(converse(complement(X0)))))) = join(X0,complement(complement(converse(complement(converse(complement(X0))))))),
inference(forward_demodulation,[],[f6888,f1]) ).
fof(f6894,plain,
! [X0] : converse(complement(converse(complement(X0)))) = join(X0,converse(complement(converse(complement(X0))))),
inference(forward_demodulation,[],[f6893,f695]) ).
fof(f6895,plain,
! [X0] : converse(complement(converse(complement(X0)))) = X0,
inference(forward_demodulation,[],[f6894,f6843]) ).
fof(f6907,plain,
! [X0] : converse(X0) = complement(converse(complement(X0))),
inference(superposition,[],[f10,f6895]) ).
fof(f7026,plain,
! [X0] : complement(converse(X0)) = converse(complement(X0)),
inference(superposition,[],[f695,f6907]) ).
fof(f7039,plain,
! [X0,X1] : converse(complement(X0)) = join(converse(complement(X0)),composition(X1,complement(converse(composition(X0,X1))))),
inference(backward_demodulation,[],[f149,f7026]) ).
fof(f7093,plain,
! [X0,X1] : converse(complement(X0)) = join(converse(complement(X0)),composition(X1,converse(complement(composition(X0,X1))))),
inference(forward_demodulation,[],[f7039,f7026]) ).
fof(f7416,plain,
! [X0] : join(sk1,composition(sk1,X0)) = join(sk1,composition(sF8,X0)),
inference(superposition,[],[f5594,f1591]) ).
fof(f7493,plain,
! [X0] : composition(sk1,join(one,X0)) = join(sk1,composition(sF8,X0)),
inference(forward_demodulation,[],[f7416,f392]) ).
fof(f7511,plain,
! [X0] : sk1 = join(sk1,composition(sF8,X0)),
inference(forward_demodulation,[],[f7493,f583]) ).
fof(f8494,plain,
! [X2,X0,X1] : join(composition(X1,top),composition(X0,complement(X2))) = join(composition(X1,X2),composition(join(X0,X1),complement(X2))),
inference(superposition,[],[f5276,f1]) ).
fof(f8840,plain,
! [X0] : join(composition(complement(sk1),top),composition(sF8,complement(X0))) = join(composition(complement(sk1),X0),composition(join(sk2,complement(sk1)),complement(X0))),
inference(superposition,[],[f5276,f1728]) ).
fof(f8841,plain,
! [X0] : join(composition(complement(sk1),top),composition(sF8,complement(X0))) = join(composition(complement(sk1),top),composition(sk2,complement(X0))),
inference(forward_demodulation,[],[f8840,f8494]) ).
fof(f9619,plain,
join(sF4,sF8) = join(sF3,join(sk2,complement(sk1))),
inference(superposition,[],[f199,f1728]) ).
fof(f9715,plain,
join(sF4,sF8) = join(sk2,join(complement(sk1),sF3)),
inference(forward_demodulation,[],[f9619,f179]) ).
fof(f9742,plain,
join(sF4,sF8) = join(sk2,join(sF3,complement(sk1))),
inference(forward_demodulation,[],[f9715,f1881]) ).
fof(f9751,plain,
join(sF4,sF8) = join(sk2,sF4),
inference(forward_demodulation,[],[f9742,f63]) ).
fof(f9781,plain,
join(sF4,complement(sF8)) = join(sF4,complement(join(sk2,sF4))),
inference(superposition,[],[f1765,f9751]) ).
fof(f9797,plain,
join(sF4,complement(sF8)) = join(sF4,complement(sk2)),
inference(forward_demodulation,[],[f9781,f1627]) ).
fof(f9814,plain,
join(sF4,complement(sF8)) = join(complement(sk2),sF4),
inference(forward_demodulation,[],[f9797,f1]) ).
fof(f9822,plain,
join(sF4,sF7) = join(complement(sk2),sF4),
inference(forward_demodulation,[],[f9814,f721]) ).
fof(f9966,plain,
! [X2,X0,X1] : join(converse(X2),composition(X1,converse(X0))) = converse(join(X2,composition(X0,converse(X1)))),
inference(superposition,[],[f91,f143]) ).
fof(f9978,plain,
! [X0,X1] : converse(complement(X0)) = converse(join(complement(X0),composition(complement(composition(X0,X1)),converse(X1)))),
inference(backward_demodulation,[],[f7093,f9966]) ).
fof(f13518,plain,
join(sF7,sF5) = join(complement(sk2),join(sF2,complement(sk1))),
inference(superposition,[],[f516,f1872]) ).
fof(f13645,plain,
join(sF7,sF5) = join(sF2,join(complement(sk1),complement(sk2))),
inference(forward_demodulation,[],[f13518,f179]) ).
fof(f13684,plain,
join(sF7,sF5) = join(sF2,join(complement(sk2),complement(sk1))),
inference(forward_demodulation,[],[f13645,f1881]) ).
fof(f13696,plain,
join(sF7,sF5) = join(sF2,sF7),
inference(forward_demodulation,[],[f13684,f66]) ).
fof(f13729,plain,
join(sF7,complement(sF5)) = join(sF7,complement(join(sF2,sF7))),
inference(superposition,[],[f1765,f13696]) ).
fof(f13747,plain,
join(sF7,complement(sF5)) = join(sF7,complement(sF2)),
inference(forward_demodulation,[],[f13729,f1627]) ).
fof(f13767,plain,
join(sF7,complement(sF5)) = join(sF7,sF3),
inference(forward_demodulation,[],[f13747,f31]) ).
fof(f13779,plain,
join(sF7,complement(sF5)) = join(sF3,sF7),
inference(forward_demodulation,[],[f13767,f1]) ).
fof(f13787,plain,
join(sF7,sF4) = join(sF3,sF7),
inference(forward_demodulation,[],[f13779,f720]) ).
fof(f13793,plain,
join(sF4,sF7) = join(sF3,sF7),
inference(forward_demodulation,[],[f13787,f1]) ).
fof(f13797,plain,
join(complement(sk2),sF4) = join(sF3,sF7),
inference(forward_demodulation,[],[f13793,f9822]) ).
fof(f17913,plain,
join(sk1,sF9) = join(sk1,sF10),
inference(superposition,[],[f1596,f62]) ).
fof(f18099,plain,
complement(sF9) = join(complement(sF9),complement(join(sk1,sF10))),
inference(superposition,[],[f1429,f17913]) ).
fof(f18797,plain,
sk1 = join(sk1,sF9),
inference(superposition,[],[f7511,f43]) ).
fof(f18862,plain,
sk1 = join(sk1,sF10),
inference(backward_demodulation,[],[f17913,f18797]) ).
fof(f18878,plain,
complement(sF9) = join(complement(sF9),complement(sk1)),
inference(backward_demodulation,[],[f18099,f18862]) ).
fof(f18891,plain,
complement(sF9) = join(complement(sk1),complement(sF9)),
inference(forward_demodulation,[],[f18878,f1]) ).
fof(f19208,plain,
join(sF7,complement(sF9)) = join(complement(sk2),complement(sF9)),
inference(superposition,[],[f516,f18891]) ).
fof(f19209,plain,
join(sF3,complement(sF9)) = join(sF4,complement(sF9)),
inference(superposition,[],[f199,f18891]) ).
fof(f19269,plain,
complement(sF9) = join(sF4,complement(sF9)),
inference(forward_demodulation,[],[f19209,f3124]) ).
fof(f19327,plain,
complement(sF4) = join(complement(sF4),complement(complement(sF9))),
inference(superposition,[],[f1359,f19269]) ).
fof(f19350,plain,
complement(sF4) = join(complement(sF4),sF9),
inference(forward_demodulation,[],[f19327,f695]) ).
fof(f19365,plain,
complement(sF4) = join(sF9,complement(sF4)),
inference(forward_demodulation,[],[f19350,f1]) ).
fof(f19373,plain,
sF5 = join(sF9,sF5),
inference(forward_demodulation,[],[f19365,f35]) ).
fof(f19386,plain,
sF5 = join(sF5,sF9),
inference(forward_demodulation,[],[f19373,f1]) ).
fof(f19397,plain,
sF5 = sF10,
inference(forward_demodulation,[],[f19386,f62]) ).
fof(f19406,plain,
spl12_2,
inference(avatar_split_clause,[],[f19397,f54]) ).
fof(f19413,plain,
( complement(sF4) = sF10
| ~ spl12_2 ),
inference(backward_demodulation,[],[f35,f55]) ).
fof(f23826,plain,
converse(complement(converse(sk1))) = converse(join(complement(converse(sk1)),composition(complement(zero),converse(complement(sk1))))),
inference(superposition,[],[f9978,f722]) ).
fof(f23885,plain,
converse(complement(converse(sk1))) = converse(join(complement(converse(sk1)),composition(top,converse(complement(sk1))))),
inference(forward_demodulation,[],[f23826,f743]) ).
fof(f23904,plain,
converse(complement(converse(sk1))) = converse(join(complement(converse(sk1)),converse(composition(complement(sk1),top)))),
inference(forward_demodulation,[],[f23885,f6647]) ).
fof(f23915,plain,
converse(complement(converse(sk1))) = join(converse(complement(converse(sk1))),composition(complement(sk1),top)),
inference(forward_demodulation,[],[f23904,f91]) ).
fof(f23924,plain,
converse(complement(converse(sk1))) = join(composition(complement(sk1),top),converse(complement(converse(sk1)))),
inference(forward_demodulation,[],[f23915,f1]) ).
fof(f23930,plain,
converse(converse(complement(sk1))) = join(composition(complement(sk1),top),converse(converse(complement(sk1)))),
inference(forward_demodulation,[],[f23924,f7026]) ).
fof(f23932,plain,
complement(sk1) = join(composition(complement(sk1),top),complement(sk1)),
inference(forward_demodulation,[],[f23930,f10]) ).
fof(f23934,plain,
complement(sk1) = join(complement(sk1),composition(complement(sk1),top)),
inference(forward_demodulation,[],[f23932,f1]) ).
fof(f23935,plain,
complement(sk1) = composition(complement(sk1),join(one,top)),
inference(forward_demodulation,[],[f23934,f392]) ).
fof(f23936,plain,
complement(sk1) = composition(complement(sk1),top),
inference(forward_demodulation,[],[f23935,f573]) ).
fof(f23937,plain,
! [X0] : join(complement(sk1),composition(sF8,complement(X0))) = join(complement(sk1),composition(sk2,complement(X0))),
inference(backward_demodulation,[],[f8841,f23936]) ).
fof(f24618,plain,
! [X0] : join(sF7,composition(sF8,complement(X0))) = join(complement(sk2),join(complement(sk1),composition(sk2,complement(X0)))),
inference(superposition,[],[f516,f23937]) ).
fof(f24619,plain,
! [X0] : join(sF4,composition(sF8,complement(X0))) = join(sF3,join(complement(sk1),composition(sk2,complement(X0)))),
inference(superposition,[],[f199,f23937]) ).
fof(f24690,plain,
! [X0] : join(sF4,composition(sF8,complement(X0))) = join(sF4,composition(sk2,complement(X0))),
inference(forward_demodulation,[],[f24619,f199]) ).
fof(f24691,plain,
! [X0] : join(sF7,composition(sF8,complement(X0))) = join(sF7,composition(sk2,complement(X0))),
inference(forward_demodulation,[],[f24618,f516]) ).
fof(f24764,plain,
! [X0] : join(sF7,composition(sF8,X0)) = join(sF7,composition(sk2,X0)),
inference(superposition,[],[f24691,f695]) ).
fof(f24870,plain,
join(sF7,sF9) = join(sF7,composition(sk2,sk3)),
inference(superposition,[],[f24764,f43]) ).
fof(f24951,plain,
join(sF7,sF2) = join(sF7,sF9),
inference(forward_demodulation,[],[f24870,f29]) ).
fof(f24974,plain,
join(sF2,sF7) = join(sF7,sF9),
inference(forward_demodulation,[],[f24951,f1]) ).
fof(f25009,plain,
join(sF7,complement(join(sF2,sF7))) = join(sF7,complement(sF9)),
inference(superposition,[],[f1765,f24974]) ).
fof(f25035,plain,
join(sF7,complement(join(sF2,sF7))) = join(complement(sk2),complement(sF9)),
inference(forward_demodulation,[],[f25009,f19208]) ).
fof(f25056,plain,
join(sF7,complement(sF2)) = join(complement(sk2),complement(sF9)),
inference(forward_demodulation,[],[f25035,f1627]) ).
fof(f25068,plain,
join(sF7,sF3) = join(complement(sk2),complement(sF9)),
inference(forward_demodulation,[],[f25056,f31]) ).
fof(f25076,plain,
join(sF3,sF7) = join(complement(sk2),complement(sF9)),
inference(forward_demodulation,[],[f25068,f1]) ).
fof(f25080,plain,
join(complement(sk2),sF4) = join(complement(sk2),complement(sF9)),
inference(forward_demodulation,[],[f25076,f13797]) ).
fof(f25117,plain,
complement(complement(sF9)) = join(complement(join(complement(sk2),sF4)),complement(join(complement(complement(sk2)),complement(sF9)))),
inference(superposition,[],[f948,f25080]) ).
fof(f25157,plain,
complement(complement(sF9)) = join(complement(join(complement(sk2),sF4)),complement(join(sk2,complement(sF9)))),
inference(forward_demodulation,[],[f25117,f695]) ).
fof(f25180,plain,
sF9 = join(complement(join(complement(sk2),sF4)),complement(join(sk2,complement(sF9)))),
inference(forward_demodulation,[],[f25157,f695]) ).
fof(f32049,plain,
! [X0] : join(sF4,composition(sF8,X0)) = join(sF4,composition(sk2,X0)),
inference(superposition,[],[f24690,f695]) ).
fof(f32160,plain,
join(sF4,sF9) = join(sF4,composition(sk2,sk3)),
inference(superposition,[],[f32049,f43]) ).
fof(f32259,plain,
join(sF4,sF9) = join(sF4,sF2),
inference(forward_demodulation,[],[f32160,f29]) ).
fof(f32283,plain,
join(sF4,sF9) = join(sF2,sF4),
inference(forward_demodulation,[],[f32259,f1]) ).
fof(f32291,plain,
top = join(sF4,sF9),
inference(forward_demodulation,[],[f32283,f2085]) ).
fof(f32316,plain,
join(sF4,complement(top)) = join(sF4,complement(sF9)),
inference(superposition,[],[f1765,f32291]) ).
fof(f32350,plain,
complement(sF9) = join(sF4,complement(top)),
inference(forward_demodulation,[],[f32316,f19269]) ).
fof(f32375,plain,
complement(sF9) = join(complement(top),sF4),
inference(forward_demodulation,[],[f32350,f1]) ).
fof(f32392,plain,
complement(sF9) = join(zero,sF4),
inference(forward_demodulation,[],[f32375,f58]) ).
fof(f32404,plain,
sF4 = complement(sF9),
inference(forward_demodulation,[],[f32392,f699]) ).
fof(f32543,plain,
sF9 = join(complement(join(complement(sk2),sF4)),complement(join(sk2,sF4))),
inference(backward_demodulation,[],[f25180,f32404]) ).
fof(f32602,plain,
sF9 = join(complement(join(sF4,sk2)),complement(join(complement(sk2),sF4))),
inference(forward_demodulation,[],[f32543,f2322]) ).
fof(f32670,plain,
complement(sF4) = sF9,
inference(forward_demodulation,[],[f32602,f758]) ).
fof(f32693,plain,
( sF9 = sF10
| ~ spl12_2 ),
inference(forward_demodulation,[],[f32670,f19413]) ).
fof(f32698,plain,
( $false
| spl12_1
| ~ spl12_2 ),
inference(forward_subsumption_resolution,[],[f32693,f67]) ).
fof(f32699,plain,
( spl12_1
| ~ spl12_2 ),
inference(avatar_contradiction_clause,[],[f32698]) ).
cnf(s1,plain,
( ~ spl12_1
| ~ spl12_2 ),
inference(sat_conversion,[],[f57]) ).
cnf(s2,plain,
spl12_2,
inference(sat_conversion,[],[f19406]) ).
cnf(s11,plain,
( spl12_1
| ~ spl12_2 ),
inference(sat_conversion,[],[f32699]) ).
cnf(s12,plain,
spl12_1,
inference(rat,[],[s11,s2]) ).
cnf(s13,plain,
$false,
inference(rat,[],[s1,s2,s12]) ).
fof(f32700,plain,
$false,
inference(avatar_sat_refutation,[],[s13]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL033-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.12/0.37 % Computer : n015.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 22:58:16 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.41 Running first-order theorem proving
% 0.12/0.41 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
% 11.79/2.53 % (2106802)Input is clausal, will run a generic CNF schedule.
% 11.79/2.53 % (2106809)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=972869427:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 11.79/2.53 % (2106811)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2706889309:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 11.79/2.53 % (2106807)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=4276363790:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 11.79/2.53 % (2106808)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2865205154:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 11.79/2.53 % (2106813)dis-21_1_sil=8000:lcm=predicate:random_seed=3575304231:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 11.79/2.53 % (2106810)lrs+10_1_sil=8000:sp=occurrence:random_seed=2881516526:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 11.79/2.53 % (2106813)Refutation not found, incomplete strategy
% 11.79/2.53 % (2106813)------------------------------
% 11.79/2.53 % (2106813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.79/2.53 % (2106813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.79/2.53 % (2106813)CaDiCaL version: 2.1.3
% 11.79/2.53 % (2106813)Termination reason: Refutation not found, incomplete strategy
% 11.79/2.53 % (2106813)Time elapsed: 0.002 s
% 11.79/2.53 % (2106813)Peak memory usage: 88 MB
% 11.79/2.53 % (2106813)Instructions burned: 1 (million)
% 11.79/2.53 % (2106812)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4145272476:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 11.79/2.53 % (2106810)Instruction limit reached!
% 11.79/2.53 % (2106810)------------------------------
% 11.79/2.53 % (2106810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.79/2.53 % (2106810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.79/2.53 % (2106810)CaDiCaL version: 2.1.3
% 11.79/2.53 % (2106810)Termination reason: Instruction limit
% 11.79/2.53 % (2106810)Termination phase: Saturation
% 11.79/2.53 % (2106810)Time elapsed: 0.069 s
% 11.79/2.53 % (2106810)Peak memory usage: 89 MB
% 11.79/2.53 % (2106810)Instructions burned: 108 (million)
% 11.79/2.53 % (2106811)Instruction limit reached!
% 11.79/2.53 % (2106811)------------------------------
% 11.79/2.53 % (2106811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.79/2.53 % (2106811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.79/2.53 % (2106811)CaDiCaL version: 2.1.3
% 11.79/2.53 % (2106811)Termination reason: Instruction limit
% 11.79/2.53 % (2106811)Termination phase: Saturation
% 11.79/2.53 % (2106811)Time elapsed: 0.072 s
% 11.79/2.53 % (2106811)Peak memory usage: 89 MB
% 11.79/2.53 % (2106811)Instructions burned: 115 (million)
% 11.79/2.53 % (2106812)Instruction limit reached!
% 11.79/2.53 % (2106812)------------------------------
% 11.79/2.53 % (2106812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.79/2.53 % (2106812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.79/2.53 % (2106812)CaDiCaL version: 2.1.3
% 11.79/2.53 % (2106812)Termination reason: Instruction limit
% 11.79/2.53 % (2106812)Termination phase: Saturation
% 11.79/2.53 % (2106812)Time elapsed: 0.105 s
% 11.79/2.53 % (2106812)Peak memory usage: 90 MB
% 11.79/2.53 % (2106812)Instructions burned: 180 (million)
% 11.79/2.53 % (2106822)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2514047832:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 11.79/2.53 % (2106821)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=1515249396:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 11.79/2.53 % (2106813)------------------------------
% 11.79/2.53 % (2106813)------------------------------
% 11.79/2.53 % (2106823)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=4107287215:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 11.79/2.53 % (2106821)Instruction limit reached!
% 11.79/2.53 % (2106821)------------------------------
% 13.88/2.86 % (2106821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.88/2.86 % (2106821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.88/2.86 % (2106821)CaDiCaL version: 2.1.3
% 13.88/2.86 % (2106821)Termination reason: Instruction limit
% 13.88/2.86 % (2106821)Termination phase: Saturation
% 13.88/2.86 % (2106821)Time elapsed: 0.080 s
% 13.88/2.86 % (2106821)Peak memory usage: 89 MB
% 13.88/2.86 % (2106821)Instructions burned: 143 (million)
% 13.88/2.86 % (2106822)Instruction limit reached!
% 13.88/2.86 % (2106822)------------------------------
% 13.88/2.86 % (2106822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.88/2.86 % (2106822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.88/2.86 % (2106822)CaDiCaL version: 2.1.3
% 13.88/2.86 % (2106822)Termination reason: Instruction limit
% 13.88/2.86 % (2106822)Termination phase: Saturation
% 13.88/2.86 % (2106822)Time elapsed: 0.118 s
% 13.88/2.86 % (2106822)Peak memory usage: 91 MB
% 13.88/2.86 % (2106822)Instructions burned: 189 (million)
% 13.88/2.86 % (2106823)Instruction limit reached!
% 13.88/2.86 % (2106823)------------------------------
% 13.88/2.86 % (2106823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.88/2.86 % (2106823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.88/2.86 % (2106823)CaDiCaL version: 2.1.3
% 13.88/2.86 % (2106823)Termination reason: Instruction limit
% 13.88/2.86 % (2106823)Termination phase: Saturation
% 13.88/2.86 % (2106823)Time elapsed: 0.127 s
% 13.88/2.86 % (2106823)Peak memory usage: 91 MB
% 13.88/2.86 % (2106823)Instructions burned: 219 (million)
% 13.88/2.86 % (2106826)lrs+10_64_to=lpo:sil=8000:random_seed=1343789292:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 13.88/2.86 % (2106828)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2028149465:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 13.88/2.86 % (2106826)Instruction limit reached!
% 13.88/2.86 % (2106826)------------------------------
% 13.88/2.86 % (2106826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.88/2.86 % (2106826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.88/2.86 % (2106826)CaDiCaL version: 2.1.3
% 13.88/2.86 % (2106826)Termination reason: Instruction limit
% 13.88/2.86 % (2106826)Termination phase: Saturation
% 13.88/2.86 % (2106826)Time elapsed: 0.077 s
% 13.88/2.86 % (2106826)Peak memory usage: 89 MB
% 13.88/2.86 % (2106826)Instructions burned: 127 (million)
% 13.88/2.86 % (2106829)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2223296103:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 13.88/2.86 % (2106831)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1243320056:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 13.88/2.86 % (2106828)Instruction limit reached!
% 13.88/2.86 % (2106828)------------------------------
% 13.88/2.86 % (2106828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.88/2.86 % (2106828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.88/2.86 % (2106828)CaDiCaL version: 2.1.3
% 13.88/2.86 % (2106828)Termination reason: Instruction limit
% 13.88/2.86 % (2106828)Termination phase: Saturation
% 13.88/2.86 % (2106828)Time elapsed: 0.121 s
% 13.88/2.86 % (2106828)Peak memory usage: 90 MB
% 13.88/2.86 % (2106828)Instructions burned: 195 (million)
% 13.88/2.86 % (2106829)Instruction limit reached!
% 13.88/2.86 % (2106829)------------------------------
% 13.88/2.86 % (2106829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.88/2.86 % (2106829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.88/2.86 % (2106829)CaDiCaL version: 2.1.3
% 13.88/2.86 % (2106829)Termination reason: Instruction limit
% 13.88/2.86 % (2106829)Termination phase: Saturation
% 13.88/2.86 % (2106829)Time elapsed: 0.101 s
% 13.88/2.86 % (2106829)Peak memory usage: 91 MB
% 13.88/2.86 % (2106829)Instructions burned: 157 (million)
% 13.88/2.86 % (2106833)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=3406990073:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 13.88/2.86 % (2106833)Instruction limit reached!
% 13.88/2.86 % (2106833)------------------------------
% 13.88/2.86 % (2106833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.88/2.86 % (2106833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.88/2.86 % (2106833)CaDiCaL version: 2.1.3
% 13.88/2.86 % (2106833)Termination reason: Instruction limit
% 13.88/2.86 % (2106833)Termination phase: Saturation
% 13.88/2.86 % (2106833)Time elapsed: 0.065 s
% 13.88/2.86 % (2106833)Peak memory usage: 89 MB
% 13.88/2.86 % (2106833)Instructions burned: 107 (million)
% 13.88/2.86 % (2106836)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3612042821:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 13.88/2.86 % (2106837)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2842387848:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 13.88/2.86 % (2106836)Instruction limit reached!
% 13.88/2.86 % (2106836)------------------------------
% 13.88/2.86 % (2106836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.88/2.86 % (2106836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.88/2.86 % (2106836)CaDiCaL version: 2.1.3
% 13.88/2.86 % (2106836)Termination reason: Instruction limit
% 13.88/2.86 % (2106836)Termination phase: Saturation
% 13.88/2.86 % (2106836)Time elapsed: 0.066 s
% 13.88/2.86 % (2106836)Peak memory usage: 88 MB
% 13.88/2.86 % (2106836)Instructions burned: 108 (million)
% 13.88/2.86 % (2106839)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3850838041:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 13.88/2.86 % (2106837)Instruction limit reached!
% 13.88/2.86 % (2106837)------------------------------
% 13.88/2.86 % (2106837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.88/2.86 % (2106837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.88/2.86 % (2106837)CaDiCaL version: 2.1.3
% 13.88/2.86 % (2106837)Termination reason: Instruction limit
% 13.88/2.86 % (2106837)Termination phase: Saturation
% 13.88/2.86 % (2106837)Time elapsed: 0.120 s
% 13.88/2.86 % (2106837)Peak memory usage: 88 MB
% 13.88/2.86 % (2106837)Instructions burned: 242 (million)
% 13.88/2.86 % (2106842)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1747947998:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi)
% 13.88/2.86 % (2106844)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2191597415:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi)
% 13.88/2.86 % (2106842)Instruction limit reached!
% 13.88/2.86 % (2106842)------------------------------
% 13.88/2.86 % (2106842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.88/2.86 % (2106842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.88/2.86 % (2106842)CaDiCaL version: 2.1.3
% 13.88/2.86 % (2106842)Termination reason: Instruction limit
% 13.88/2.86 % (2106842)Termination phase: Saturation
% 13.88/2.86 % (2106842)Time elapsed: 0.080 s
% 13.88/2.86 % (2106842)Peak memory usage: 89 MB
% 13.88/2.86 % (2106842)Instructions burned: 135 (million)
% 13.88/2.86 % (2106847)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1244128804:i=191:fgj=on:bd=all_2987 on theBenchmark for (2987ds/191Mi)
% 13.88/2.86 % (2106847)Instruction limit reached!
% 13.88/2.86 % (2106847)------------------------------
% 13.88/2.86 % (2106847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.88/2.86 % (2106847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.88/2.86 % (2106847)CaDiCaL version: 2.1.3
% 13.88/2.86 % (2106847)Termination reason: Instruction limit
% 13.88/2.86 % (2106847)Termination phase: Saturation
% 13.88/2.86 % (2106847)Time elapsed: 0.124 s
% 13.88/2.86 % (2106847)Peak memory usage: 90 MB
% 13.88/2.86 % (2106847)Instructions burned: 192 (million)
% 13.88/2.86 % (2106844)Instruction limit reached!
% 13.88/2.86 % (2106844)------------------------------
% 13.88/2.86 % (2106844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.88/2.86 % (2106844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.88/2.86 % (2106844)CaDiCaL version: 2.1.3
% 13.88/2.86 % (2106844)Termination reason: Instruction limit
% 13.88/2.86 % (2106844)Termination phase: Saturation
% 13.88/2.86 % (2106844)Time elapsed: 0.327 s
% 13.88/2.86 % (2106844)Peak memory usage: 94 MB
% 13.88/2.86 % (2106844)Instructions burned: 500 (million)
% 13.88/2.86 % (2106849)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=964288757:i=264:kws=precedence:fsr=off_2984 on theBenchmark for (2984ds/264Mi)
% 13.88/2.86 % (2106850)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=800262095:cond=on:i=156:bs=on:gtg=exists_all:er=known_2984 on theBenchmark for (2984ds/156Mi)
% 13.88/2.86 % (2106850)Instruction limit reached!
% 13.88/2.86 % (2106850)------------------------------
% 13.88/2.86 % (2106850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.88/2.86 % (2106850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.88/2.86 % (2106850)CaDiCaL version: 2.1.3
% 13.88/2.86 % (2106850)Termination reason: Instruction limit
% 13.88/2.86 % (2106850)Termination phase: Saturation
% 13.88/2.86 % (2106850)Time elapsed: 0.095 s
% 13.88/2.86 % (2106850)Peak memory usage: 89 MB
% 13.88/2.86 % (2106850)Instructions burned: 157 (million)
% 13.88/2.86 % (2106809)First to succeed.
% 13.88/2.86 % (2106809)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2106802"
% 13.88/2.86 % (2106849)Instruction limit reached!
% 13.88/2.86 % (2106849)------------------------------
% 13.88/2.86 % (2106849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.88/2.86 % (2106849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.88/2.86 % (2106849)CaDiCaL version: 2.1.3
% 13.88/2.86 % (2106849)Termination reason: Instruction limit
% 13.88/2.86 % (2106849)Termination phase: Saturation
% 13.88/2.86 % (2106849)Time elapsed: 0.160 s
% 13.88/2.86 % (2106849)Peak memory usage: 92 MB
% 13.88/2.86 % (2106849)Instructions burned: 264 (million)
% 13.88/2.86 % (2106853)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=1344170325:i=3256:kws=precedence:bd=preordered:av=off_2982 on theBenchmark for (2982ds/3256Mi)
% 13.88/2.86 % (2106809)Refutation found. Thanks to Tanya!
% 13.88/2.86 % SZS status Unsatisfiable for theBenchmark
% 13.88/2.86 % SZS output start Proof for theBenchmark
% See solution above
% 14.72/3.06 % (2106809)------------------------------
% 14.72/3.06 % (2106809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.72/3.06 % (2106809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.72/3.06 % (2106809)CaDiCaL version: 2.1.3
% 14.72/3.06 % (2106809)Termination reason: Refutation
% 14.72/3.06 % (2106809)Time elapsed: 1.698 s
% 14.72/3.06 % (2106809)Peak memory usage: 167 MB
% 14.72/3.06 % (2106809)Instructions burned: 4852 (million)
% 14.72/3.06 % (2106809)------------------------------
% 14.72/3.06 % (2106809)------------------------------
% 14.72/3.06 % (2106802)Success in time 1.997 s
% 14.72/3.06 % Vampire exiting
%------------------------------------------------------------------------------