%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : REL033-4 : 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 : n008.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:34:00 PM UTC 2026
% Result : Unsatisfiable 35.58s 5.98s
% Output : Refutation 36.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 65
% Number of leaves : 28
% Syntax : Number of formulae : 311 ( 295 unt; 14 def)
% Number of atoms : 328 ( 305 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 : 10 ( 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 : 372 ( 0 sgn 372 !; 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(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,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_18) ).
fof(f26,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,[],[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(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,[],[f26,f6,f6,f6,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 = composition(sk2,sk3),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f38,plain,
composition(sk2,sk3) = sF2,
inference(reorient_equations,[],[f37]) ).
fof(f39,definition,
sF3 = complement(sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f40,plain,
complement(sF2) = sF3,
inference(reorient_equations,[],[f39]) ).
fof(f41,definition,
sF4 = join(sF1,sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f42,plain,
join(sF1,sF3) = sF4,
inference(reorient_equations,[],[f41]) ).
fof(f43,definition,
sF5 = complement(sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f44,plain,
complement(sF4) = sF5,
inference(reorient_equations,[],[f43]) ).
fof(f45,definition,
sF6 = complement(sk2),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f46,plain,
complement(sk2) = sF6,
inference(reorient_equations,[],[f45]) ).
fof(f47,definition,
sF7 = join(sF1,sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f48,plain,
join(sF1,sF6) = sF7,
inference(reorient_equations,[],[f47]) ).
fof(f49,definition,
sF8 = complement(sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f50,plain,
complement(sF7) = sF8,
inference(reorient_equations,[],[f49]) ).
fof(f51,definition,
sF9 = composition(sF8,sk3),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f52,plain,
composition(sF8,sk3) = sF9,
inference(reorient_equations,[],[f51]) ).
fof(f53,definition,
sF10 = join(sF9,sF5),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f54,plain,
join(sF9,sF5) = sF10,
inference(reorient_equations,[],[f53]) ).
fof(f55,definition,
sF11 = join(sF5,sF9),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f56,plain,
join(sF5,sF9) = sF11,
inference(reorient_equations,[],[f55]) ).
fof(f57,plain,
( sF5 != sF10
| sF9 != sF11 ),
inference(definition_folding,[],[f31,f56,f52,f50,f48,f46,f36,f44,f42,f40,f38,f36,f52,f50,f48,f46,f36,f54,f44,f42,f40,f38,f36,f52,f50,f48,f46,f36,f44,f42,f40,f38,f36]) ).
fof(f59,definition,
( spl12_1
<=> sF9 = sF11 ),
introduced(definition,[new_symbols(definition,[spl12_1])],[avatar_definition]) ).
fof(f61,plain,
( sF9 != sF11
| spl12_1 ),
inference(avatar_component_clause,[],[f59]) ).
fof(f63,definition,
( spl12_2
<=> sF5 = sF10 ),
introduced(definition,[new_symbols(definition,[spl12_2])],[avatar_definition]) ).
fof(f64,plain,
( sF5 = sF10
| ~ spl12_2 ),
inference(avatar_component_clause,[],[f63]) ).
fof(f66,plain,
( ~ spl12_1
| ~ spl12_2 ),
inference(avatar_split_clause,[],[f57,f63,f59]) ).
fof(f67,plain,
zero = complement(top),
inference(backward_demodulation,[],[f27,f15]) ).
fof(f68,plain,
sk1 = composition(sk1,top),
inference(forward_demodulation,[],[f33,f34]) ).
fof(f69,plain,
sF4 = join(sF3,sF1),
inference(forward_demodulation,[],[f42,f1]) ).
fof(f70,plain,
sF7 = join(sF6,sF1),
inference(forward_demodulation,[],[f48,f1]) ).
fof(f71,plain,
sF10 = join(sF5,sF9),
inference(forward_demodulation,[],[f54,f1]) ).
fof(f72,plain,
sF4 = join(sF3,complement(sk1)),
inference(forward_demodulation,[],[f69,f36]) ).
fof(f73,plain,
sF7 = join(sF6,complement(sk1)),
inference(forward_demodulation,[],[f70,f36]) ).
fof(f74,plain,
sF10 = sF11,
inference(backward_demodulation,[],[f56,f71]) ).
fof(f75,plain,
sF7 = join(complement(sk2),complement(sk1)),
inference(forward_demodulation,[],[f73,f46]) ).
fof(f76,plain,
( sF9 != sF10
| spl12_1 ),
inference(forward_demodulation,[],[f61,f74]) ).
fof(f77,plain,
! [X0,X1] : join(complement(X0),complement(X1)) = join(complement(X0),complement(join(complement(join(complement(X0),complement(X1))),join(complement(X0),X1)))),
inference(superposition,[],[f4,f4]) ).
fof(f80,plain,
! [X0,X1] : join(complement(X0),complement(X1)) = join(complement(X0),complement(join(join(complement(X0),X1),complement(join(complement(X0),complement(X1)))))),
inference(forward_demodulation,[],[f77,f1]) ).
fof(f81,plain,
! [X0,X1] : join(complement(X0),complement(X1)) = join(complement(X0),complement(join(complement(X0),join(X1,complement(join(complement(X0),complement(X1))))))),
inference(forward_demodulation,[],[f80,f2]) ).
fof(f97,plain,
! [X0,X1] : join(complement(join(complement(X0),complement(X1))),complement(join(complement(X1),X0))) = X1,
inference(superposition,[],[f4,f1]) ).
fof(f99,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))) = X0,
inference(superposition,[],[f4,f1]) ).
fof(f102,plain,
! [X0,X1] : join(complement(join(complement(X1),X0)),complement(join(complement(X0),complement(X1)))) = X1,
inference(forward_demodulation,[],[f97,f1]) ).
fof(f105,plain,
! [X0,X1] : complement(X1) = join(composition(X0,complement(composition(converse(X0),X1))),complement(X1)),
inference(superposition,[],[f14,f10]) ).
fof(f106,plain,
complement(top) = join(composition(converse(sk1),complement(sk1)),complement(top)),
inference(superposition,[],[f14,f68]) ).
fof(f113,plain,
complement(top) = join(complement(top),composition(converse(sk1),complement(sk1))),
inference(forward_demodulation,[],[f106,f1]) ).
fof(f114,plain,
! [X0,X1] : complement(X1) = join(complement(X1),composition(X0,complement(composition(converse(X0),X1)))),
inference(forward_demodulation,[],[f105,f1]) ).
fof(f115,plain,
zero = join(zero,composition(converse(sk1),complement(sk1))),
inference(forward_demodulation,[],[f113,f67]) ).
fof(f116,plain,
! [X0,X1] : converse(join(converse(X0),X1)) = join(X0,converse(X1)),
inference(superposition,[],[f11,f10]) ).
fof(f117,plain,
! [X0,X1] : converse(join(X1,converse(X0))) = join(converse(X1),X0),
inference(superposition,[],[f11,f10]) ).
fof(f124,plain,
! [X0] : composition(join(sF8,X0),sk3) = join(sF9,composition(X0,sk3)),
inference(superposition,[],[f9,f52]) ).
fof(f133,plain,
! [X0,X1] : composition(X0,converse(X1)) = converse(composition(X1,converse(X0))),
inference(superposition,[],[f12,f10]) ).
fof(f134,plain,
! [X0,X1] : composition(converse(X1),X0) = converse(composition(converse(X0),X1)),
inference(superposition,[],[f12,f10]) ).
fof(f135,plain,
! [X0,X1] : complement(converse(X0)) = join(composition(converse(converse(X1)),complement(converse(composition(X0,X1)))),complement(converse(X0))),
inference(superposition,[],[f14,f12]) ).
fof(f137,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(f138,plain,
! [X0,X1] : complement(converse(X0)) = join(complement(converse(X0)),composition(converse(converse(X1)),complement(converse(composition(X0,X1))))),
inference(forward_demodulation,[],[f135,f1]) ).
fof(f139,plain,
! [X0,X1] : complement(converse(X0)) = join(complement(converse(X0)),composition(X1,complement(converse(composition(X0,X1))))),
inference(forward_demodulation,[],[f138,f10]) ).
fof(f175,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X1,join(X0,X2)),
inference(superposition,[],[f2,f1]) ).
fof(f176,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(top,X1),
inference(superposition,[],[f2,f15]) ).
fof(f178,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(f187,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f1,f2]) ).
fof(f190,plain,
! [X2,X0,X1] : join(X0,X2) = join(complement(join(complement(X0),X1)),join(X2,complement(join(complement(X0),complement(X1))))),
inference(forward_demodulation,[],[f178,f187]) ).
fof(f203,plain,
! [X0] : join(sF3,join(complement(sk1),X0)) = join(sF4,X0),
inference(superposition,[],[f2,f72]) ).
fof(f259,plain,
! [X0] : converse(converse(X0)) = composition(converse(one),X0),
inference(superposition,[],[f134,f8]) ).
fof(f271,plain,
! [X0] : composition(converse(one),X0) = X0,
inference(forward_demodulation,[],[f259,f10]) ).
fof(f284,plain,
! [X0] : complement(X0) = join(complement(X0),composition(one,complement(X0))),
inference(superposition,[],[f114,f271]) ).
fof(f289,plain,
one = converse(one),
inference(superposition,[],[f8,f271]) ).
fof(f292,plain,
! [X0] : composition(one,X0) = X0,
inference(backward_demodulation,[],[f271,f289]) ).
fof(f299,plain,
! [X0] : complement(X0) = join(complement(X0),complement(X0)),
inference(backward_demodulation,[],[f284,f292]) ).
fof(f385,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(X1,top),
inference(superposition,[],[f187,f15]) ).
fof(f444,plain,
! [X0] : join(X0,complement(X0)) = join(top,complement(X0)),
inference(superposition,[],[f176,f299]) ).
fof(f448,plain,
! [X0] : join(X0,top) = join(top,complement(complement(X0))),
inference(superposition,[],[f176,f15]) ).
fof(f468,plain,
! [X0] : top = join(top,complement(X0)),
inference(forward_demodulation,[],[f444,f15]) ).
fof(f476,plain,
! [X0] : top = join(X0,top),
inference(backward_demodulation,[],[f448,f468]) ).
fof(f481,plain,
! [X0,X1] : top = join(X0,join(complement(X0),X1)),
inference(backward_demodulation,[],[f385,f476]) ).
fof(f485,plain,
! [X1] : top = join(top,X1),
inference(backward_demodulation,[],[f176,f481]) ).
fof(f535,plain,
! [X2,X0,X1] : composition(join(converse(X2),converse(X1)),converse(X0)) = join(converse(composition(X0,X2)),converse(composition(X0,X1))),
inference(superposition,[],[f137,f12]) ).
fof(f543,plain,
! [X2,X0,X1] : composition(join(converse(X2),converse(X1)),converse(X0)) = converse(join(composition(X0,X2),composition(X0,X1))),
inference(forward_demodulation,[],[f535,f11]) ).
fof(f553,plain,
! [X2,X0,X1] : converse(join(composition(X0,X2),composition(X0,X1))) = composition(converse(join(X2,X1)),converse(X0)),
inference(forward_demodulation,[],[f543,f11]) ).
fof(f559,plain,
! [X2,X0,X1] : converse(join(composition(X0,X2),composition(X0,X1))) = converse(composition(X0,join(X2,X1))),
inference(forward_demodulation,[],[f553,f12]) ).
fof(f583,plain,
! [X2,X0,X1] : join(composition(X0,X1),composition(X0,X2)) = converse(converse(composition(X0,join(X1,X2)))),
inference(superposition,[],[f10,f559]) ).
fof(f598,plain,
! [X2,X0,X1] : composition(X0,join(X1,X2)) = join(composition(X0,X1),composition(X0,X2)),
inference(forward_demodulation,[],[f583,f10]) ).
fof(f632,plain,
! [X0,X1] : join(X0,composition(X0,X1)) = composition(X0,join(one,X1)),
inference(superposition,[],[f598,f8]) ).
fof(f636,plain,
! [X0] : composition(sk1,join(top,X0)) = join(sk1,composition(sk1,X0)),
inference(superposition,[],[f598,f68]) ).
fof(f651,plain,
! [X2,X3,X0,X1] : join(X3,composition(X0,join(X1,X2))) = join(composition(X0,X2),join(X3,composition(X0,X1))),
inference(superposition,[],[f187,f598]) ).
fof(f652,plain,
! [X2,X3,X0,X1] : join(composition(X0,join(X1,X2)),X3) = join(composition(X0,X1),join(composition(X0,X2),X3)),
inference(superposition,[],[f2,f598]) ).
fof(f664,plain,
! [X0] : composition(sk1,top) = join(sk1,composition(sk1,X0)),
inference(forward_demodulation,[],[f636,f485]) ).
fof(f671,plain,
! [X0] : composition(sk1,top) = composition(sk1,join(one,X0)),
inference(forward_demodulation,[],[f664,f632]) ).
fof(f676,plain,
! [X0] : sk1 = composition(sk1,join(one,X0)),
inference(forward_demodulation,[],[f671,f68]) ).
fof(f727,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),X0) = join(X0,complement(join(complement(X0),complement(complement(X1))))),
inference(superposition,[],[f190,f4]) ).
fof(f728,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,[],[f190,f299]) ).
fof(f744,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),complement(X1)))) = X0,
inference(forward_demodulation,[],[f728,f99]) ).
fof(f745,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),X1))) = join(X0,complement(join(complement(X0),complement(complement(X1))))),
inference(forward_demodulation,[],[f727,f1]) ).
fof(f763,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),X1))) = X0,
inference(forward_demodulation,[],[f745,f744]) ).
fof(f796,plain,
sk2 = join(sk2,complement(sF7)),
inference(superposition,[],[f763,f75]) ).
fof(f798,plain,
! [X2,X0,X1] : join(complement(X0),X2) = join(join(complement(X0),X2),complement(join(X0,X1))),
inference(superposition,[],[f763,f190]) ).
fof(f800,plain,
! [X0,X1] : join(X1,complement(join(X0,complement(X1)))) = X1,
inference(superposition,[],[f763,f1]) ).
fof(f805,plain,
! [X0] : join(X0,complement(top)) = X0,
inference(superposition,[],[f763,f476]) ).
fof(f807,plain,
! [X0,X1] : join(X0,X0) = join(complement(join(complement(X0),X1)),X0),
inference(superposition,[],[f190,f763]) ).
fof(f815,plain,
! [X2,X0,X1] : join(X0,X1) = join(complement(complement(X0)),join(X1,complement(join(complement(X0),complement(complement(join(complement(complement(X0)),X2))))))),
inference(superposition,[],[f190,f763]) ).
fof(f823,plain,
! [X0,X1] : join(X0,X0) = join(X0,complement(join(complement(X0),X1))),
inference(forward_demodulation,[],[f807,f1]) ).
fof(f824,plain,
! [X0] : join(X0,zero) = X0,
inference(forward_demodulation,[],[f805,f67]) ).
fof(f829,plain,
! [X0,X1] : join(complement(X0),complement(X1)) = join(complement(X0),complement(join(complement(X0),X1))),
inference(backward_demodulation,[],[f81,f800]) ).
fof(f830,plain,
! [X2,X0,X1] : join(complement(X0),X2) = join(complement(X0),join(X2,complement(join(X0,X1)))),
inference(forward_demodulation,[],[f798,f2]) ).
fof(f831,plain,
sk2 = join(sk2,sF8),
inference(forward_demodulation,[],[f796,f50]) ).
fof(f837,plain,
! [X0] : join(X0,X0) = X0,
inference(forward_demodulation,[],[f823,f763]) ).
fof(f841,plain,
! [X0,X1] : join(X0,X1) = join(complement(complement(X0)),X1),
inference(backward_demodulation,[],[f815,f830]) ).
fof(f895,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X0,X1))),
inference(superposition,[],[f763,f841]) ).
fof(f909,plain,
! [X0,X1] : complement(complement(X0)) = join(X0,complement(join(complement(complement(complement(X0))),X1))),
inference(superposition,[],[f763,f841]) ).
fof(f911,plain,
! [X0,X1] : complement(complement(X0)) = join(X0,complement(join(complement(X0),X1))),
inference(forward_demodulation,[],[f909,f841]) ).
fof(f930,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_demodulation,[],[f911,f763]) ).
fof(f1035,plain,
top = complement(zero),
inference(superposition,[],[f930,f67]) ).
fof(f1048,plain,
! [X0,X1] : join(X0,complement(X1)) = join(X0,complement(join(X0,X1))),
inference(superposition,[],[f829,f930]) ).
fof(f1055,plain,
! [X0,X1] : join(X1,complement(join(X0,X1))) = join(X1,complement(X0)),
inference(superposition,[],[f1048,f1]) ).
fof(f1060,plain,
! [X0,X1] : join(X0,complement(complement(join(X0,X1)))) = join(X0,complement(join(X0,complement(X1)))),
inference(superposition,[],[f1048,f1048]) ).
fof(f1091,plain,
! [X0,X1] : join(X0,complement(complement(X1))) = join(X0,complement(complement(join(X0,X1)))),
inference(forward_demodulation,[],[f1060,f1048]) ).
fof(f1103,plain,
! [X0,X1] : join(X0,complement(complement(X1))) = join(X0,join(X0,X1)),
inference(forward_demodulation,[],[f1091,f930]) ).
fof(f1114,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X0,X1)),
inference(forward_demodulation,[],[f1103,f930]) ).
fof(f1136,plain,
join(complement(sk1),complement(complement(sk2))) = join(complement(sk1),complement(sF7)),
inference(superposition,[],[f1055,f75]) ).
fof(f1150,plain,
! [X0,X1] : join(X0,complement(join(X0,complement(X1)))) = join(X0,complement(complement(join(X1,X0)))),
inference(superposition,[],[f1048,f1055]) ).
fof(f1158,plain,
! [X0,X1] : join(X0,complement(join(X0,complement(X1)))) = join(X0,join(X1,X0)),
inference(forward_demodulation,[],[f1150,f930]) ).
fof(f1169,plain,
join(complement(sk1),complement(complement(sk2))) = join(complement(sk1),sF8),
inference(forward_demodulation,[],[f1136,f50]) ).
fof(f1180,plain,
! [X0,X1] : join(X0,complement(complement(X1))) = join(X0,join(X1,X0)),
inference(forward_demodulation,[],[f1158,f1048]) ).
fof(f1184,plain,
join(complement(sk1),sF8) = join(complement(sk1),sk2),
inference(forward_demodulation,[],[f1169,f930]) ).
fof(f1193,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X1,X0)),
inference(forward_demodulation,[],[f1180,f930]) ).
fof(f1195,plain,
join(complement(sk1),sF8) = join(sk2,complement(sk1)),
inference(forward_demodulation,[],[f1184,f1]) ).
fof(f1212,plain,
! [X0] : join(zero,X0) = X0,
inference(superposition,[],[f1,f824]) ).
fof(f1226,plain,
zero = composition(converse(sk1),complement(sk1)),
inference(backward_demodulation,[],[f115,f1212]) ).
fof(f1264,plain,
! [X2,X0,X1] : join(X2,join(X0,X1)) = join(X0,join(join(X1,X0),X2)),
inference(superposition,[],[f187,f1193]) ).
fof(f1276,plain,
! [X2,X0,X1] : join(X2,join(X0,X1)) = join(X0,join(X1,join(X0,X2))),
inference(forward_demodulation,[],[f1264,f2]) ).
fof(f1340,plain,
! [X0,X1] : complement(X1) = join(complement(X1),complement(join(X0,X1))),
inference(superposition,[],[f895,f1]) ).
fof(f1423,plain,
complement(complement(sk1)) = join(complement(complement(sk1)),complement(sF7)),
inference(superposition,[],[f1340,f75]) ).
fof(f1425,plain,
! [X0,X1] : complement(complement(join(X1,X0))) = join(complement(complement(join(X1,X0))),complement(complement(X0))),
inference(superposition,[],[f1340,f1340]) ).
fof(f1454,plain,
! [X0,X1] : complement(complement(join(X1,X0))) = join(complement(complement(X0)),complement(complement(join(X1,X0)))),
inference(forward_demodulation,[],[f1425,f1]) ).
fof(f1456,plain,
complement(complement(sk1)) = join(complement(sF7),complement(complement(sk1))),
inference(forward_demodulation,[],[f1423,f1]) ).
fof(f1469,plain,
! [X0,X1] : join(X1,X0) = join(complement(complement(X0)),join(X1,X0)),
inference(forward_demodulation,[],[f1454,f930]) ).
fof(f1471,plain,
sk1 = join(complement(sF7),sk1),
inference(forward_demodulation,[],[f1456,f930]) ).
fof(f1480,plain,
! [X0,X1] : join(X1,X0) = join(X0,join(complement(complement(X0)),X1)),
inference(forward_demodulation,[],[f1469,f187]) ).
fof(f1482,plain,
sk1 = join(sk1,complement(sF7)),
inference(forward_demodulation,[],[f1471,f1]) ).
fof(f1487,plain,
! [X0,X1] : join(X1,X0) = join(X0,join(X0,X1)),
inference(forward_demodulation,[],[f1480,f930]) ).
fof(f1489,plain,
sk1 = join(sk1,sF8),
inference(forward_demodulation,[],[f1482,f50]) ).
fof(f1526,plain,
! [X0,X1] : join(X1,X0) = join(X0,join(X1,X0)),
inference(superposition,[],[f187,f837]) ).
fof(f1829,plain,
! [X0,X1] : complement(X0) = join(complement(join(X0,X1)),complement(join(complement(X1),X0))),
inference(superposition,[],[f102,f930]) ).
fof(f2061,plain,
! [X0] : converse(top) = join(X0,converse(complement(converse(X0)))),
inference(superposition,[],[f116,f15]) ).
fof(f2810,plain,
! [X2,X0,X1] : join(join(X2,X0),X1) = join(X1,join(X0,join(X1,X2))),
inference(superposition,[],[f1487,f187]) ).
fof(f2924,plain,
! [X2,X0,X1] : join(X2,join(X1,X0)) = join(join(X2,X0),X1),
inference(forward_demodulation,[],[f2810,f1276]) ).
fof(f3003,plain,
composition(join(sF8,sk2),sk3) = join(sF9,sF2),
inference(superposition,[],[f124,f38]) ).
fof(f3038,plain,
composition(join(sF8,sk2),sk3) = join(sF2,sF9),
inference(forward_demodulation,[],[f3003,f1]) ).
fof(f3045,plain,
join(sF2,sF9) = composition(join(sk2,sF8),sk3),
inference(forward_demodulation,[],[f3038,f1]) ).
fof(f3049,plain,
composition(sk2,sk3) = join(sF2,sF9),
inference(forward_demodulation,[],[f3045,f831]) ).
fof(f3050,plain,
sF2 = join(sF2,sF9),
inference(forward_demodulation,[],[f3049,f38]) ).
fof(f3058,plain,
complement(sF9) = join(complement(sF9),complement(sF2)),
inference(superposition,[],[f1340,f3050]) ).
fof(f3061,plain,
complement(sF9) = join(complement(sF2),complement(sF9)),
inference(forward_demodulation,[],[f3058,f1]) ).
fof(f3065,plain,
complement(sF9) = join(sF3,complement(sF9)),
inference(forward_demodulation,[],[f3061,f40]) ).
fof(f3109,plain,
! [X2,X0,X1] : join(composition(X0,join(X1,one)),X2) = join(composition(X0,X1),join(X0,X2)),
inference(superposition,[],[f652,f8]) ).
fof(f3115,plain,
! [X0,X1] : join(composition(sk1,join(X0,top)),X1) = join(composition(sk1,X0),join(sk1,X1)),
inference(superposition,[],[f652,f68]) ).
fof(f3118,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,[],[f652,f9]) ).
fof(f3127,plain,
! [X2,X3,X0,X1] : join(composition(X0,join(X3,X1)),join(X2,composition(X0,X1))) = join(composition(X0,X3),join(composition(X0,X1),X2)),
inference(superposition,[],[f652,f1193]) ).
fof(f3193,plain,
! [X2,X3,X0,X1] : join(composition(X0,join(X3,X1)),join(X2,composition(X0,X1))) = join(composition(X0,join(X3,X1)),X2),
inference(forward_demodulation,[],[f3127,f652]) ).
fof(f3200,plain,
! [X0,X1] : join(composition(sk1,join(X0,top)),X1) = join(sk1,join(X1,composition(sk1,X0))),
inference(forward_demodulation,[],[f3115,f187]) ).
fof(f3206,plain,
! [X2,X0,X1] : join(composition(X0,join(X1,one)),X2) = join(X0,join(X2,composition(X0,X1))),
inference(forward_demodulation,[],[f3109,f187]) ).
fof(f3227,plain,
! [X2,X3,X0,X1] : join(composition(X0,join(X3,X1)),X2) = join(X2,composition(X0,join(X1,join(X3,X1)))),
inference(forward_demodulation,[],[f3193,f651]) ).
fof(f3231,plain,
! [X0,X1] : join(composition(sk1,top),X1) = join(sk1,join(X1,composition(sk1,X0))),
inference(forward_demodulation,[],[f3200,f476]) ).
fof(f3248,plain,
! [X2,X3,X0,X1] : join(composition(X0,join(X3,X1)),X2) = join(X2,composition(X0,join(X1,X3))),
inference(forward_demodulation,[],[f3227,f1193]) ).
fof(f3250,plain,
! [X0,X1] : join(composition(sk1,top),X1) = join(composition(sk1,join(X0,one)),X1),
inference(forward_demodulation,[],[f3231,f3206]) ).
fof(f3259,plain,
! [X0,X1] : join(sk1,X1) = join(composition(sk1,join(X0,one)),X1),
inference(forward_demodulation,[],[f3250,f68]) ).
fof(f3278,plain,
! [X0] : join(X0,complement(converse(complement(converse(X0))))) = join(X0,complement(converse(top))),
inference(superposition,[],[f1048,f2061]) ).
fof(f3279,plain,
! [X0] : join(converse(complement(converse(X0))),complement(X0)) = join(converse(complement(converse(X0))),complement(converse(top))),
inference(superposition,[],[f1055,f2061]) ).
fof(f3292,plain,
top = converse(top),
inference(superposition,[],[f485,f2061]) ).
fof(f3313,plain,
! [X0] : join(converse(complement(converse(X0))),complement(X0)) = join(complement(converse(top)),converse(complement(converse(X0)))),
inference(forward_demodulation,[],[f3279,f1]) ).
fof(f3314,plain,
! [X0] : join(X0,complement(top)) = join(X0,complement(converse(complement(converse(X0))))),
inference(forward_demodulation,[],[f3278,f3292]) ).
fof(f3339,plain,
! [X0] : join(converse(complement(converse(X0))),complement(X0)) = join(complement(top),converse(complement(converse(X0)))),
inference(forward_demodulation,[],[f3313,f3292]) ).
fof(f3340,plain,
! [X0] : join(X0,zero) = join(X0,complement(converse(complement(converse(X0))))),
inference(forward_demodulation,[],[f3314,f67]) ).
fof(f3355,plain,
! [X0] : join(converse(complement(converse(X0))),complement(X0)) = join(zero,converse(complement(converse(X0)))),
inference(forward_demodulation,[],[f3339,f67]) ).
fof(f3356,plain,
! [X0] : join(X0,complement(converse(complement(converse(X0))))) = X0,
inference(forward_demodulation,[],[f3340,f824]) ).
fof(f3363,plain,
! [X0] : converse(complement(converse(X0))) = join(converse(complement(converse(X0))),complement(X0)),
inference(forward_demodulation,[],[f3355,f1212]) ).
fof(f3368,plain,
! [X0] : converse(complement(converse(X0))) = join(complement(X0),converse(complement(converse(X0)))),
inference(forward_demodulation,[],[f3363,f1]) ).
fof(f3395,plain,
! [X0] : converse(converse(X0)) = join(X0,converse(complement(converse(complement(converse(converse(X0))))))),
inference(superposition,[],[f116,f3356]) ).
fof(f3400,plain,
! [X0] : join(X0,converse(complement(converse(complement(X0))))) = X0,
inference(forward_demodulation,[],[f3395,f10]) ).
fof(f3426,plain,
! [X0] : converse(composition(X0,top)) = composition(top,converse(X0)),
inference(superposition,[],[f12,f3292]) ).
fof(f3526,plain,
! [X0] : complement(X0) = join(complement(X0),converse(complement(converse(X0)))),
inference(superposition,[],[f3400,f930]) ).
fof(f3570,plain,
! [X0] : complement(X0) = converse(complement(converse(X0))),
inference(backward_demodulation,[],[f3368,f3526]) ).
fof(f3663,plain,
! [X0] : complement(converse(X0)) = converse(complement(X0)),
inference(superposition,[],[f10,f3570]) ).
fof(f3681,plain,
! [X0,X1] : converse(complement(X0)) = join(converse(complement(X0)),composition(X1,complement(converse(composition(X0,X1))))),
inference(backward_demodulation,[],[f139,f3663]) ).
fof(f3727,plain,
! [X0,X1] : converse(complement(X0)) = join(converse(complement(X0)),composition(X1,converse(complement(composition(X0,X1))))),
inference(forward_demodulation,[],[f3681,f3663]) ).
fof(f4021,plain,
! [X2,X0,X1] : join(complement(X0),X2) = join(complement(join(X1,X0)),join(complement(X0),X2)),
inference(superposition,[],[f175,f1340]) ).
fof(f4155,plain,
! [X2,X0,X1] : join(complement(X0),X2) = join(complement(X0),join(X2,complement(join(X1,X0)))),
inference(forward_demodulation,[],[f4021,f187]) ).
fof(f4619,plain,
! [X0,X1] : complement(X1) = join(complement(join(X0,X1)),complement(join(complement(X0),X1))),
inference(superposition,[],[f1829,f1]) ).
fof(f4723,plain,
! [X0,X1] : join(complement(join(X0,X1)),complement(complement(X0))) = join(complement(join(X0,X1)),complement(complement(join(complement(X1),X0)))),
inference(superposition,[],[f1048,f1829]) ).
fof(f4734,plain,
! [X0,X1] : join(complement(join(X0,X1)),complement(complement(X0))) = join(complement(join(X0,X1)),join(complement(X1),X0)),
inference(forward_demodulation,[],[f4723,f930]) ).
fof(f4820,plain,
! [X0,X1] : join(complement(join(X0,X1)),complement(complement(X0))) = join(join(complement(X1),X0),complement(join(X0,X1))),
inference(forward_demodulation,[],[f4734,f1]) ).
fof(f4880,plain,
! [X0,X1] : join(complement(join(X0,X1)),complement(complement(X0))) = join(complement(X1),join(X0,complement(join(X0,X1)))),
inference(forward_demodulation,[],[f4820,f2]) ).
fof(f4922,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(join(X0,X1)),complement(complement(X0))),
inference(forward_demodulation,[],[f4880,f4155]) ).
fof(f4961,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(join(X0,X1)),X0),
inference(forward_demodulation,[],[f4922,f930]) ).
fof(f4990,plain,
! [X0,X1] : join(complement(X1),X0) = join(X0,complement(join(X0,X1))),
inference(forward_demodulation,[],[f4961,f1]) ).
fof(f6193,plain,
! [X2,X0,X1] : join(composition(X0,X1),composition(join(X0,X2),complement(X1))) = join(composition(X0,top),composition(X2,complement(X1))),
inference(superposition,[],[f3118,f15]) ).
fof(f6263,plain,
! [X0,X1] : join(composition(X0,X1),composition(join(X0,sF8),sk3)) = join(composition(X0,join(X1,sk3)),sF9),
inference(superposition,[],[f3118,f52]) ).
fof(f6279,plain,
! [X0,X1] : join(composition(sk1,join(top,X0)),composition(X1,X0)) = join(sk1,composition(join(sk1,X1),X0)),
inference(superposition,[],[f3118,f68]) ).
fof(f6462,plain,
! [X0,X1] : join(sk1,composition(join(sk1,X1),X0)) = join(composition(sk1,top),composition(X1,X0)),
inference(forward_demodulation,[],[f6279,f485]) ).
fof(f6475,plain,
! [X0,X1] : join(composition(X0,X1),composition(join(X0,sF8),sk3)) = join(sF9,composition(X0,join(sk3,X1))),
inference(forward_demodulation,[],[f6263,f3248]) ).
fof(f6533,plain,
! [X0,X1] : join(sk1,composition(join(sk1,X1),X0)) = join(sk1,composition(X1,X0)),
inference(forward_demodulation,[],[f6462,f68]) ).
fof(f6591,plain,
! [X0] : join(sk1,composition(sk1,X0)) = join(sk1,composition(sF8,X0)),
inference(superposition,[],[f6533,f1489]) ).
fof(f6663,plain,
! [X0] : composition(sk1,join(one,X0)) = join(sk1,composition(sF8,X0)),
inference(forward_demodulation,[],[f6591,f632]) ).
fof(f6680,plain,
! [X0] : sk1 = join(sk1,composition(sF8,X0)),
inference(forward_demodulation,[],[f6663,f676]) ).
fof(f6824,plain,
! [X2,X0,X1] : join(composition(X1,top),composition(X0,complement(X2))) = join(composition(X1,X2),composition(join(X0,X1),complement(X2))),
inference(superposition,[],[f6193,f1]) ).
fof(f6854,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,[],[f6193,f1195]) ).
fof(f6980,plain,
! [X0] : join(composition(complement(sk1),top),composition(sF8,complement(X0))) = join(composition(complement(sk1),top),composition(sk2,complement(X0))),
inference(backward_demodulation,[],[f6854,f6824]) ).
fof(f8724,plain,
! [X2,X0,X1] : composition(X0,join(X1,X2)) = join(composition(X0,X2),composition(X0,join(X1,X2))),
inference(superposition,[],[f1526,f598]) ).
fof(f8873,plain,
! [X2,X0,X1] : composition(X0,join(X1,X2)) = composition(X0,join(X2,join(X1,X2))),
inference(forward_demodulation,[],[f8724,f598]) ).
fof(f8936,plain,
! [X2,X0,X1] : composition(X0,join(X2,X1)) = composition(X0,join(X1,X2)),
inference(forward_demodulation,[],[f8873,f1193]) ).
fof(f9316,plain,
! [X0,X1] : join(sk1,composition(sk1,X0)) = composition(sk1,join(join(X1,one),X0)),
inference(superposition,[],[f598,f3259]) ).
fof(f9408,plain,
! [X0,X1] : join(sk1,composition(sk1,X0)) = composition(sk1,join(X1,join(one,X0))),
inference(forward_demodulation,[],[f9316,f2]) ).
fof(f9460,plain,
! [X0,X1] : composition(sk1,join(one,X0)) = composition(sk1,join(X1,join(one,X0))),
inference(forward_demodulation,[],[f9408,f632]) ).
fof(f9496,plain,
! [X0,X1] : sk1 = composition(sk1,join(X1,join(one,X0))),
inference(forward_demodulation,[],[f9460,f676]) ).
fof(f9671,plain,
! [X2,X0,X1] : join(converse(X2),composition(X1,converse(X0))) = converse(join(X2,composition(X0,converse(X1)))),
inference(superposition,[],[f117,f133]) ).
fof(f9681,plain,
! [X0,X1] : converse(complement(X0)) = converse(join(complement(X0),composition(complement(composition(X0,X1)),converse(X1)))),
inference(backward_demodulation,[],[f3727,f9671]) ).
fof(f12909,plain,
converse(complement(converse(sk1))) = converse(join(complement(converse(sk1)),composition(complement(zero),converse(complement(sk1))))),
inference(superposition,[],[f9681,f1226]) ).
fof(f12966,plain,
converse(complement(converse(sk1))) = converse(join(complement(converse(sk1)),composition(top,converse(complement(sk1))))),
inference(forward_demodulation,[],[f12909,f1035]) ).
fof(f12988,plain,
converse(complement(converse(sk1))) = converse(join(complement(converse(sk1)),converse(composition(complement(sk1),top)))),
inference(forward_demodulation,[],[f12966,f3426]) ).
fof(f12997,plain,
converse(complement(converse(sk1))) = join(converse(complement(converse(sk1))),composition(complement(sk1),top)),
inference(forward_demodulation,[],[f12988,f117]) ).
fof(f13004,plain,
converse(complement(converse(sk1))) = join(composition(complement(sk1),top),converse(complement(converse(sk1)))),
inference(forward_demodulation,[],[f12997,f1]) ).
fof(f13010,plain,
converse(converse(complement(sk1))) = join(composition(complement(sk1),top),converse(converse(complement(sk1)))),
inference(forward_demodulation,[],[f13004,f3663]) ).
fof(f13013,plain,
complement(sk1) = join(composition(complement(sk1),top),complement(sk1)),
inference(forward_demodulation,[],[f13010,f10]) ).
fof(f13015,plain,
complement(sk1) = join(complement(sk1),composition(complement(sk1),top)),
inference(forward_demodulation,[],[f13013,f1]) ).
fof(f13016,plain,
complement(sk1) = composition(complement(sk1),join(one,top)),
inference(forward_demodulation,[],[f13015,f632]) ).
fof(f13017,plain,
complement(sk1) = composition(complement(sk1),top),
inference(forward_demodulation,[],[f13016,f476]) ).
fof(f13023,plain,
! [X0] : join(complement(sk1),composition(sF8,complement(X0))) = join(complement(sk1),composition(sk2,complement(X0))),
inference(backward_demodulation,[],[f6980,f13017]) ).
fof(f13184,plain,
! [X0,X1] : join(composition(complement(sk1),join(top,X0)),composition(X1,X0)) = join(complement(sk1),composition(join(complement(sk1),X1),X0)),
inference(superposition,[],[f3118,f13017]) ).
fof(f13195,plain,
! [X0,X1] : join(complement(sk1),composition(join(complement(sk1),X1),X0)) = join(composition(complement(sk1),top),composition(X1,X0)),
inference(forward_demodulation,[],[f13184,f485]) ).
fof(f13221,plain,
! [X0,X1] : join(complement(sk1),composition(join(complement(sk1),X1),X0)) = join(complement(sk1),composition(X1,X0)),
inference(forward_demodulation,[],[f13195,f13017]) ).
fof(f14024,plain,
! [X0] : join(sk1,composition(join(sk1,sF8),sk3)) = join(sF9,composition(sk1,join(sk3,join(one,X0)))),
inference(superposition,[],[f6475,f676]) ).
fof(f14032,plain,
! [X0,X1] : join(sF9,composition(X0,join(sk3,X1))) = join(composition(X0,X1),composition(join(sF8,X0),sk3)),
inference(superposition,[],[f6475,f1]) ).
fof(f14066,plain,
! [X0,X1] : join(sF9,composition(X0,join(sk3,X1))) = join(composition(X0,X1),join(sF9,composition(X0,join(sk3,X1)))),
inference(superposition,[],[f1114,f6475]) ).
fof(f14087,plain,
! [X0,X1] : join(sF9,composition(X0,join(sk3,X1))) = join(sF9,composition(X0,join(join(sk3,X1),X1))),
inference(forward_demodulation,[],[f14066,f651]) ).
fof(f14116,plain,
join(sk1,composition(join(sk1,sF8),sk3)) = join(sF9,sk1),
inference(forward_demodulation,[],[f14024,f9496]) ).
fof(f14136,plain,
! [X0,X1] : join(sF9,composition(X0,join(sk3,X1))) = join(sF9,composition(X0,join(X1,join(sk3,X1)))),
inference(forward_demodulation,[],[f14087,f8936]) ).
fof(f14156,plain,
join(sk1,sF9) = join(sk1,composition(join(sk1,sF8),sk3)),
inference(forward_demodulation,[],[f14116,f1]) ).
fof(f14171,plain,
! [X0,X1] : join(sF9,composition(X0,join(sk3,X1))) = join(sF9,composition(X0,join(X1,sk3))),
inference(forward_demodulation,[],[f14136,f1193]) ).
fof(f14183,plain,
join(sk1,sF9) = join(sk1,composition(sF8,sk3)),
inference(forward_demodulation,[],[f14156,f6533]) ).
fof(f14194,plain,
sk1 = join(sk1,sF9),
inference(forward_demodulation,[],[f14183,f6680]) ).
fof(f14218,plain,
complement(sF9) = join(complement(sk1),complement(join(complement(sk1),sF9))),
inference(superposition,[],[f4619,f14194]) ).
fof(f14224,plain,
complement(sF9) = join(complement(sk1),complement(sF9)),
inference(forward_demodulation,[],[f14218,f1048]) ).
fof(f15675,plain,
! [X0] : join(complement(sk1),composition(sF8,X0)) = join(complement(sk1),composition(sk2,X0)),
inference(superposition,[],[f13023,f930]) ).
fof(f15999,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X0,join(X2,X1)),
inference(superposition,[],[f2,f2924]) ).
fof(f16326,plain,
! [X2,X3,X0,X1] : join(X3,composition(join(X0,X1),X2)) = join(X3,join(composition(X1,X2),composition(X0,X2))),
inference(superposition,[],[f15999,f9]) ).
fof(f16468,plain,
! [X2,X0,X1] : join(X0,complement(join(X0,join(X1,X2)))) = join(complement(join(X2,X1)),X0),
inference(superposition,[],[f4990,f15999]) ).
fof(f16537,plain,
! [X2,X0,X1] : join(X0,complement(join(X1,X2))) = join(complement(join(X2,X1)),X0),
inference(forward_demodulation,[],[f16468,f1048]) ).
fof(f16596,plain,
! [X2,X3,X0,X1] : join(X3,composition(join(X0,X1),X2)) = join(X3,composition(join(X1,X0),X2)),
inference(forward_demodulation,[],[f16326,f9]) ).
fof(f21960,plain,
join(sF3,complement(sF9)) = join(sF4,complement(sF9)),
inference(superposition,[],[f203,f14224]) ).
fof(f22016,plain,
complement(sF9) = join(sF4,complement(sF9)),
inference(forward_demodulation,[],[f21960,f3065]) ).
fof(f22069,plain,
complement(sF4) = join(complement(sF4),complement(complement(sF9))),
inference(superposition,[],[f895,f22016]) ).
fof(f22099,plain,
complement(sF4) = join(complement(sF4),sF9),
inference(forward_demodulation,[],[f22069,f930]) ).
fof(f22113,plain,
complement(sF4) = join(sF9,complement(sF4)),
inference(forward_demodulation,[],[f22099,f1]) ).
fof(f22120,plain,
sF5 = join(sF9,sF5),
inference(forward_demodulation,[],[f22113,f44]) ).
fof(f22133,plain,
sF5 = join(sF5,sF9),
inference(forward_demodulation,[],[f22120,f1]) ).
fof(f22144,plain,
sF5 = sF10,
inference(forward_demodulation,[],[f22133,f71]) ).
fof(f22153,plain,
spl12_2,
inference(avatar_split_clause,[],[f22144,f63]) ).
fof(f22160,plain,
( complement(sF4) = sF10
| ~ spl12_2 ),
inference(backward_demodulation,[],[f44,f64]) ).
fof(f25377,plain,
join(sF9,composition(complement(sk1),join(sk3,top))) = join(complement(sk1),composition(join(sF8,complement(sk1)),sk3)),
inference(superposition,[],[f14032,f13017]) ).
fof(f25552,plain,
join(sF9,composition(complement(sk1),join(sk3,top))) = join(complement(sk1),composition(join(complement(sk1),sF8),sk3)),
inference(forward_demodulation,[],[f25377,f16596]) ).
fof(f25613,plain,
join(sF9,composition(complement(sk1),join(sk3,top))) = join(complement(sk1),composition(sF8,sk3)),
inference(forward_demodulation,[],[f25552,f13221]) ).
fof(f25657,plain,
join(sF9,composition(complement(sk1),join(sk3,top))) = join(complement(sk1),composition(sk2,sk3)),
inference(forward_demodulation,[],[f25613,f15675]) ).
fof(f25683,plain,
join(complement(sk1),sF2) = join(sF9,composition(complement(sk1),join(sk3,top))),
inference(forward_demodulation,[],[f25657,f38]) ).
fof(f25693,plain,
join(complement(sk1),sF2) = join(sF9,composition(complement(sk1),join(top,sk3))),
inference(forward_demodulation,[],[f25683,f14171]) ).
fof(f25698,plain,
join(complement(sk1),sF2) = join(sF9,composition(complement(sk1),top)),
inference(forward_demodulation,[],[f25693,f485]) ).
fof(f25700,plain,
join(complement(sk1),sF2) = join(sF9,complement(sk1)),
inference(forward_demodulation,[],[f25698,f13017]) ).
fof(f25702,plain,
join(complement(sk1),sF2) = join(complement(sk1),sF9),
inference(forward_demodulation,[],[f25700,f1]) ).
fof(f25704,plain,
join(sF2,complement(sk1)) = join(complement(sk1),sF9),
inference(forward_demodulation,[],[f25702,f1]) ).
fof(f25723,plain,
join(complement(sk1),complement(join(sF2,complement(sk1)))) = join(complement(sk1),complement(sF9)),
inference(superposition,[],[f1048,f25704]) ).
fof(f25758,plain,
complement(sF9) = join(complement(sk1),complement(join(sF2,complement(sk1)))),
inference(forward_demodulation,[],[f25723,f14224]) ).
fof(f25781,plain,
complement(sF9) = join(complement(sk1),complement(sF2)),
inference(forward_demodulation,[],[f25758,f1055]) ).
fof(f25797,plain,
complement(sF9) = join(complement(sk1),sF3),
inference(forward_demodulation,[],[f25781,f40]) ).
fof(f25811,plain,
join(sF3,complement(sk1)) = complement(sF9),
inference(forward_demodulation,[],[f25797,f1]) ).
fof(f25822,plain,
sF4 = complement(sF9),
inference(forward_demodulation,[],[f25811,f72]) ).
fof(f26029,plain,
! [X0] : sF9 = join(complement(join(sF4,complement(X0))),complement(join(sF4,X0))),
inference(superposition,[],[f4,f25822]) ).
fof(f26090,plain,
! [X0] : sF9 = join(complement(join(sF4,X0)),complement(join(complement(X0),sF4))),
inference(forward_demodulation,[],[f26029,f16537]) ).
fof(f26102,plain,
complement(sF4) = sF9,
inference(forward_demodulation,[],[f26090,f1829]) ).
fof(f26107,plain,
( sF9 = sF10
| ~ spl12_2 ),
inference(forward_demodulation,[],[f26102,f22160]) ).
fof(f26109,plain,
( $false
| spl12_1
| ~ spl12_2 ),
inference(forward_subsumption_resolution,[],[f26107,f76]) ).
fof(f26110,plain,
( spl12_1
| ~ spl12_2 ),
inference(avatar_contradiction_clause,[],[f26109]) ).
cnf(s1,plain,
( ~ spl12_1
| ~ spl12_2 ),
inference(sat_conversion,[],[f66]) ).
cnf(s2,plain,
spl12_2,
inference(sat_conversion,[],[f22153]) ).
cnf(s8,plain,
( spl12_1
| ~ spl12_2 ),
inference(sat_conversion,[],[f26110]) ).
cnf(s9,plain,
spl12_1,
inference(rat,[],[s8,s2]) ).
cnf(s10,plain,
$false,
inference(rat,[],[s1,s2,s9]) ).
fof(f26122,plain,
$false,
inference(avatar_sat_refutation,[],[s10]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL033-4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.39 % Computer : n008.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sun Sep 27 22:55:39 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.43 Running first-order theorem proving
% 0.11/0.43 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
% 17.92/3.49 % (1700736)Input is clausal, will run a generic CNF schedule.
% 17.92/3.49 % (1700825)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3504536754:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 17.92/3.49 % (1700820)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=1295342681:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 17.92/3.49 % (1700824)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2344926701:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 17.92/3.49 % (1700823)lrs+10_1_sil=8000:sp=occurrence:random_seed=1248590124:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 17.92/3.49 % (1700822)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3444948345:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 17.92/3.49 % (1700821)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1591174996:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 17.92/3.49 % (1700825)Instruction limit reached!
% 17.92/3.49 % (1700825)------------------------------
% 17.92/3.49 % (1700825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.92/3.49 % (1700825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.92/3.49 % (1700825)CaDiCaL version: 2.1.3
% 17.92/3.49 % (1700825)Termination reason: Instruction limit
% 17.92/3.49 % (1700825)Termination phase: Saturation
% 17.92/3.49 % (1700825)Time elapsed: 0.093 s
% 17.92/3.49 % (1700825)Peak memory usage: 90 MB
% 17.92/3.49 % (1700825)Instructions burned: 181 (million)
% 17.92/3.49 % (1700827)dis-21_1_sil=8000:lcm=predicate:random_seed=818392975: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)
% 17.92/3.49 % (1700827)Refutation not found, incomplete strategy
% 17.92/3.49 % (1700827)------------------------------
% 17.92/3.49 % (1700827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.92/3.49 % (1700827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.92/3.49 % (1700827)CaDiCaL version: 2.1.3
% 17.92/3.49 % (1700827)Termination reason: Refutation not found, incomplete strategy
% 17.92/3.49 % (1700827)Time elapsed: 0.002 s
% 17.92/3.49 % (1700827)Peak memory usage: 88 MB
% 17.92/3.49 % (1700827)Instructions burned: 1 (million)
% 17.92/3.49 % (1700823)Instruction limit reached!
% 17.92/3.49 % (1700823)------------------------------
% 17.92/3.49 % (1700823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.92/3.49 % (1700823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.92/3.49 % (1700823)CaDiCaL version: 2.1.3
% 17.92/3.49 % (1700823)Termination reason: Instruction limit
% 17.92/3.49 % (1700823)Termination phase: Saturation
% 17.92/3.49 % (1700823)Time elapsed: 0.111 s
% 17.92/3.49 % (1700823)Peak memory usage: 89 MB
% 17.92/3.49 % (1700823)Instructions burned: 108 (million)
% 17.92/3.49 % (1700824)Instruction limit reached!
% 17.92/3.49 % (1700824)------------------------------
% 17.92/3.49 % (1700824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.92/3.49 % (1700824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.92/3.49 % (1700824)CaDiCaL version: 2.1.3
% 17.92/3.49 % (1700824)Termination reason: Instruction limit
% 17.92/3.49 % (1700824)Termination phase: Saturation
% 17.92/3.49 % (1700824)Time elapsed: 0.113 s
% 17.92/3.49 % (1700824)Peak memory usage: 89 MB
% 17.92/3.49 % (1700824)Instructions burned: 114 (million)
% 17.92/3.49 % (1700849)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=4108824558:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 17.92/3.49 % (1700849)Instruction limit reached!
% 17.92/3.49 % (1700849)------------------------------
% 17.92/3.49 % (1700849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.92/3.49 % (1700849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.92/3.49 % (1700849)CaDiCaL version: 2.1.3
% 17.92/3.49 % (1700849)Termination reason: Instruction limit
% 17.92/3.49 % (1700849)Termination phase: Saturation
% 17.92/3.49 % (1700849)Time elapsed: 0.049 s
% 17.92/3.49 % (1700849)Peak memory usage: 89 MB
% 17.92/3.49 % (1700849)Instructions burned: 145 (million)
% 17.92/3.49 % (1700853)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2147934633:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 35.58/5.98 % (1700854)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3458000954:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 35.58/5.98 % (1700827)------------------------------
% 35.58/5.98 % (1700827)------------------------------
% 35.58/5.98 % (1700861)lrs+10_64_to=lpo:sil=8000:random_seed=734000630:i=126:bd=preordered_2994 on theBenchmark for (2994ds/126Mi)
% 35.58/5.98 % (1700853)Instruction limit reached!
% 35.58/5.98 % (1700853)------------------------------
% 35.58/5.98 % (1700853)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.58/5.98 % (1700853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.58/5.98 % (1700853)CaDiCaL version: 2.1.3
% 35.58/5.98 % (1700853)Termination reason: Instruction limit
% 35.58/5.98 % (1700853)Termination phase: Saturation
% 35.58/5.98 % (1700853)Time elapsed: 0.186 s
% 35.58/5.98 % (1700853)Peak memory usage: 91 MB
% 35.58/5.98 % (1700853)Instructions burned: 189 (million)
% 35.58/5.98 % (1700854)Instruction limit reached!
% 35.58/5.98 % (1700854)------------------------------
% 35.58/5.98 % (1700854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.58/5.98 % (1700854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.58/5.98 % (1700854)CaDiCaL version: 2.1.3
% 35.58/5.98 % (1700854)Termination reason: Instruction limit
% 35.58/5.98 % (1700854)Termination phase: Saturation
% 35.58/5.98 % (1700854)Time elapsed: 0.222 s
% 35.58/5.98 % (1700854)Peak memory usage: 90 MB
% 35.58/5.98 % (1700854)Instructions burned: 220 (million)
% 35.58/5.98 % (1700861)Instruction limit reached!
% 35.58/5.98 % (1700861)------------------------------
% 35.58/5.98 % (1700861)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.58/5.98 % (1700861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.58/5.98 % (1700861)CaDiCaL version: 2.1.3
% 35.58/5.98 % (1700861)Termination reason: Instruction limit
% 35.58/5.98 % (1700861)Termination phase: Saturation
% 35.58/5.98 % (1700861)Time elapsed: 0.067 s
% 35.58/5.98 % (1700861)Peak memory usage: 89 MB
% 35.58/5.98 % (1700861)Instructions burned: 126 (million)
% 35.58/5.98 % (1700864)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2244827794:avsq=on:i=194:fgj=on:bd=preordered_2993 on theBenchmark for (2993ds/194Mi)
% 35.58/5.98 % (1700870)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1024459586:i=157:gtg=all_2991 on theBenchmark for (2991ds/157Mi)
% 35.58/5.98 % (1700871)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3247441326:i=3394:sd=4:ss=included:sgt=64_2991 on theBenchmark for (2991ds/3394Mi)
% 35.58/5.98 % (1700864)Instruction limit reached!
% 35.58/5.98 % (1700864)------------------------------
% 35.58/5.98 % (1700864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.58/5.98 % (1700864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.58/5.98 % (1700864)CaDiCaL version: 2.1.3
% 35.58/5.98 % (1700864)Termination reason: Instruction limit
% 35.58/5.98 % (1700864)Termination phase: Saturation
% 35.58/5.98 % (1700864)Time elapsed: 0.209 s
% 35.58/5.98 % (1700864)Peak memory usage: 90 MB
% 35.58/5.98 % (1700864)Instructions burned: 194 (million)
% 35.58/5.98 % (1700870)Instruction limit reached!
% 35.58/5.98 % (1700870)------------------------------
% 35.58/5.98 % (1700870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.58/5.98 % (1700870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.58/5.98 % (1700870)CaDiCaL version: 2.1.3
% 35.58/5.98 % (1700870)Termination reason: Instruction limit
% 35.58/5.98 % (1700870)Termination phase: Saturation
% 35.58/5.98 % (1700870)Time elapsed: 0.146 s
% 35.58/5.98 % (1700870)Peak memory usage: 91 MB
% 35.58/5.98 % (1700870)Instructions burned: 157 (million)
% 35.58/5.98 % (1700872)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=3699159329:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2991 on theBenchmark for (2991ds/106Mi)
% 35.58/5.98 % (1700872)Instruction limit reached!
% 35.58/5.98 % (1700872)------------------------------
% 35.58/5.98 % (1700872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.58/5.98 % (1700872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.58/5.98 % (1700872)CaDiCaL version: 2.1.3
% 35.58/5.98 % (1700872)Termination reason: Instruction limit
% 35.58/5.98 % (1700872)Termination phase: Saturation
% 35.58/5.98 % (1700872)Time elapsed: 0.108 s
% 35.58/5.98 % (1700872)Peak memory usage: 89 MB
% 35.58/5.98 % (1700872)Instructions burned: 107 (million)
% 35.58/5.98 % (1700878)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1516502151:i=107_2988 on theBenchmark for (2988ds/107Mi)
% 35.58/5.98 % (1700879)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=765643523:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2988 on theBenchmark for (2988ds/242Mi)
% 35.58/5.98 % (1700878)Instruction limit reached!
% 35.58/5.98 % (1700878)------------------------------
% 35.58/5.98 % (1700878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.58/5.98 % (1700878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.58/5.98 % (1700878)CaDiCaL version: 2.1.3
% 35.58/5.98 % (1700878)Termination reason: Instruction limit
% 35.58/5.98 % (1700878)Termination phase: Saturation
% 35.58/5.98 % (1700878)Time elapsed: 0.071 s
% 35.58/5.98 % (1700878)Peak memory usage: 89 MB
% 35.58/5.98 % (1700878)Instructions burned: 108 (million)
% 35.58/5.98 % (1700881)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2092951783:cond=fast:i=5208:av=off_2987 on theBenchmark for (2987ds/5208Mi)
% 35.58/5.98 % (1700879)Instruction limit reached!
% 35.58/5.98 % (1700879)------------------------------
% 35.58/5.98 % (1700879)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.58/5.98 % (1700879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.58/5.98 % (1700879)CaDiCaL version: 2.1.3
% 35.58/5.98 % (1700879)Termination reason: Instruction limit
% 35.58/5.98 % (1700879)Termination phase: Saturation
% 35.58/5.98 % (1700879)Time elapsed: 0.219 s
% 35.58/5.98 % (1700879)Peak memory usage: 89 MB
% 35.58/5.98 % (1700879)Instructions burned: 243 (million)
% 35.58/5.98 % (1700886)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3901925760:i=134:sd=2:doe=on:ss=axioms:sgt=14_2985 on theBenchmark for (2985ds/134Mi)
% 35.58/5.98 % (1700886)Instruction limit reached!
% 35.58/5.98 % (1700886)------------------------------
% 35.58/5.98 % (1700886)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.58/5.98 % (1700886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.58/5.98 % (1700886)CaDiCaL version: 2.1.3
% 35.58/5.98 % (1700886)Termination reason: Instruction limit
% 35.58/5.98 % (1700886)Termination phase: Saturation
% 35.58/5.98 % (1700886)Time elapsed: 0.127 s
% 35.58/5.98 % (1700886)Peak memory usage: 89 MB
% 35.58/5.98 % (1700886)Instructions burned: 134 (million)
% 35.58/5.98 % (1700892)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=217997733:i=499:bd=all_2983 on theBenchmark for (2983ds/499Mi)
% 35.58/5.98 % (1700894)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=4006765800:i=191:fgj=on:bd=all_2981 on theBenchmark for (2981ds/191Mi)
% 35.58/5.98 % (1700894)Instruction limit reached!
% 35.58/5.98 % (1700894)------------------------------
% 35.58/5.98 % (1700894)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.58/5.98 % (1700894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.58/5.98 % (1700894)CaDiCaL version: 2.1.3
% 35.58/5.98 % (1700894)Termination reason: Instruction limit
% 35.58/5.98 % (1700894)Termination phase: Saturation
% 35.58/5.98 % (1700894)Time elapsed: 0.199 s
% 35.58/5.98 % (1700894)Peak memory usage: 90 MB
% 35.58/5.98 % (1700894)Instructions burned: 191 (million)
% 35.58/5.98 % (1700892)Instruction limit reached!
% 35.58/5.98 % (1700892)------------------------------
% 35.58/5.98 % (1700892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.58/5.98 % (1700892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.58/5.98 % (1700892)CaDiCaL version: 2.1.3
% 35.58/5.98 % (1700892)Termination reason: Instruction limit
% 35.58/5.98 % (1700892)Termination phase: Saturation
% 35.58/5.98 % (1700892)Time elapsed: 0.532 s
% 35.58/5.98 % (1700892)Peak memory usage: 94 MB
% 35.58/5.98 % (1700892)Instructions burned: 499 (million)
% 35.58/5.98 % (1700899)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2430962652:i=264:kws=precedence:fsr=off_2976 on theBenchmark for (2976ds/264Mi)
% 35.58/5.98 % (1700900)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3011454734:cond=on:i=156:bs=on:gtg=exists_all:er=known_2975 on theBenchmark for (2975ds/156Mi)
% 35.58/5.98 % (1700900)Instruction limit reached!
% 35.58/5.98 % (1700900)------------------------------
% 35.58/5.98 % (1700900)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.58/5.98 % (1700900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.58/5.98 % (1700900)CaDiCaL version: 2.1.3
% 35.58/5.98 % (1700900)Termination reason: Instruction limit
% 35.58/5.98 % (1700900)Termination phase: Saturation
% 35.58/5.98 % (1700900)Time elapsed: 0.143 s
% 35.58/5.98 % (1700900)Peak memory usage: 89 MB
% 35.58/5.98 % (1700900)Instructions burned: 156 (million)
% 35.58/5.98 % (1700899)Instruction limit reached!
% 35.58/5.98 % (1700899)------------------------------
% 35.58/5.98 % (1700899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.58/5.98 % (1700899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.58/5.98 % (1700899)CaDiCaL version: 2.1.3
% 35.58/5.98 % (1700899)Termination reason: Instruction limit
% 35.58/5.98 % (1700899)Termination phase: Saturation
% 35.58/5.98 % (1700899)Time elapsed: 0.257 s
% 35.58/5.98 % (1700899)Peak memory usage: 91 MB
% 35.58/5.98 % (1700899)Instructions burned: 265 (million)
% 35.58/5.98 % (1700903)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=3677028980:i=3256:kws=precedence:bd=preordered:av=off_2972 on theBenchmark for (2972ds/3256Mi)
% 35.58/5.98 % (1700904)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=496959736:i=537:av=off:ss=included_2971 on theBenchmark for (2971ds/537Mi)
% 35.58/5.98 % (1700904)Instruction limit reached!
% 35.58/5.98 % (1700904)------------------------------
% 35.58/5.98 % (1700904)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.58/5.98 % (1700904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.58/5.98 % (1700904)CaDiCaL version: 2.1.3
% 35.58/5.98 % (1700904)Termination reason: Instruction limit
% 35.58/5.98 % (1700904)Termination phase: Saturation
% 35.58/5.98 % (1700904)Time elapsed: 0.485 s
% 35.58/5.98 % (1700904)Peak memory usage: 93 MB
% 35.58/5.98 % (1700904)Instructions burned: 538 (million)
% 35.58/5.98 % (1700911)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1184705829:i=180:bd=preordered:av=off_2963 on theBenchmark for (2963ds/180Mi)
% 35.58/5.98 % (1700911)Instruction limit reached!
% 35.58/5.98 % (1700911)------------------------------
% 35.58/5.98 % (1700911)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.58/5.98 % (1700911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.58/5.98 % (1700911)CaDiCaL version: 2.1.3
% 35.58/5.98 % (1700911)Termination reason: Instruction limit
% 35.58/5.98 % (1700911)Termination phase: Saturation
% 35.58/5.98 % (1700911)Time elapsed: 0.180 s
% 35.58/5.98 % (1700911)Peak memory usage: 90 MB
% 35.58/5.98 % (1700911)Instructions burned: 180 (million)
% 35.58/5.98 % (1700913)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=3740050036:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2959 on theBenchmark for (2959ds/10307Mi)
% 35.58/5.98 % (1700822)First to succeed.
% 35.58/5.98 % (1700822)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1700736"
% 35.58/5.98 % (1700871)Instruction limit reached!
% 35.58/5.98 % (1700871)------------------------------
% 35.58/5.98 % (1700871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.58/5.98 % (1700871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.58/5.98 % (1700871)CaDiCaL version: 2.1.3
% 35.58/5.98 % (1700871)Termination reason: Instruction limit
% 35.58/5.98 % (1700871)Termination phase: Saturation
% 35.58/5.98 % (1700871)Time elapsed: 3.551 s
% 35.58/5.98 % (1700871)Peak memory usage: 149 MB
% 35.58/5.98 % (1700871)Instructions burned: 3394 (million)
% 35.58/5.98 % (1700915)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=3773627870:i=412:gtgl=4:gtg=exists_all_2952 on theBenchmark for (2952ds/412Mi)
% 35.58/5.98 % (1700822)Refutation found. Thanks to Tanya!
% 35.58/5.98 % SZS status Unsatisfiable for theBenchmark
% 35.58/5.98 % SZS output start Proof for theBenchmark
% See solution above
% 36.60/6.25 % (1700822)------------------------------
% 36.60/6.25 % (1700822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.60/6.25 % (1700822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.60/6.25 % (1700822)CaDiCaL version: 2.1.3
% 36.60/6.25 % (1700822)Termination reason: Refutation
% 36.60/6.25 % (1700822)Time elapsed: 4.412 s
% 36.60/6.25 % (1700822)Peak memory usage: 160 MB
% 36.60/6.25 % (1700822)Instructions burned: 4223 (million)
% 36.60/6.25 % (1700822)------------------------------
% 36.60/6.25 % (1700822)------------------------------
% 36.60/6.25 % (1700736)Success in time 5.106 s
% 36.60/6.25 % Vampire exiting
%------------------------------------------------------------------------------