%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : REL045-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:34:07 PM UTC 2026
% Result : Unsatisfiable 46.03s 7.58s
% Output : Refutation 46.69s
% Verified :
% SZS Type : Refutation
% Derivation depth : 54
% Number of leaves : 31
% Syntax : Number of formulae : 278 ( 123 unt; 17 def)
% Number of atoms : 640 ( 240 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 715 ( 353 ~; 349 |; 0 &)
% ( 13 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 15 ( 13 usr; 14 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 8 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(f7,axiom,
! [X2,X0,X1] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',composition_associativity_5) ).
fof(f8,axiom,
! [X0] : composition(X0,one) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',composition_identity_6) ).
fof(f9,axiom,
! [X2,X0,X1] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',composition_distributivity_7) ).
fof(f10,axiom,
! [X0] : converse(converse(X0)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_idempotence_8) ).
fof(f11,axiom,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_additivity_9) ).
fof(f12,axiom,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_multiplicativity_10) ).
fof(f13,axiom,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_cancellativity_11) ).
fof(f14,plain,
! [X0,X1] : complement(X1) = join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)),
inference(reorient_equations,[],[f13]) ).
fof(f15,axiom,
! [X0] : top = join(X0,complement(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',def_top_12) ).
fof(f16,axiom,
! [X0] : zero = meet(X0,complement(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',def_zero_13) ).
fof(f17,negated_conjecture,
join(sk1,composition(composition(sk1,converse(sk1)),sk1)) != composition(composition(sk1,converse(sk1)),sk1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals_14) ).
fof(f18,plain,
composition(composition(sk1,converse(sk1)),sk1) != join(sk1,composition(composition(sk1,converse(sk1)),sk1)),
inference(reorient_equations,[],[f17]) ).
fof(f19,plain,
! [X0] : zero = complement(join(complement(X0),complement(complement(X0)))),
inference(definition_unfolding,[],[f16,f6]) ).
fof(f20,definition,
sF0 = converse(sk1),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f21,plain,
converse(sk1) = sF0,
inference(reorient_equations,[],[f20]) ).
fof(f22,definition,
sF1 = composition(sk1,sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f23,plain,
composition(sk1,sF0) = sF1,
inference(reorient_equations,[],[f22]) ).
fof(f24,definition,
sF2 = composition(sF1,sk1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f25,plain,
composition(sF1,sk1) = sF2,
inference(reorient_equations,[],[f24]) ).
fof(f26,definition,
sF3 = join(sk1,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f27,plain,
join(sk1,sF2) = sF3,
inference(reorient_equations,[],[f26]) ).
fof(f28,plain,
sF2 != sF3,
inference(definition_folding,[],[f18,f27,f25,f23,f21,f25,f23,f21]) ).
fof(f29,plain,
zero = complement(top),
inference(backward_demodulation,[],[f19,f15]) ).
fof(f30,plain,
sF3 = join(sF2,sk1),
inference(forward_demodulation,[],[f27,f1]) ).
fof(f32,definition,
( spl4_1
<=> sF3 = join(sF2,sk1) ),
introduced(definition,[new_symbols(definition,[spl4_1])],[avatar_definition]) ).
fof(f34,plain,
( sF3 = join(sF2,sk1)
| ~ spl4_1 ),
inference(avatar_component_clause,[],[f32]) ).
fof(f35,plain,
spl4_1,
inference(avatar_split_clause,[],[f30,f32]) ).
fof(f37,definition,
( spl4_2
<=> sF2 = sF3 ),
introduced(definition,[new_symbols(definition,[spl4_2])],[avatar_definition]) ).
fof(f39,plain,
( sF2 != sF3
| spl4_2 ),
inference(avatar_component_clause,[],[f37]) ).
fof(f40,plain,
~ spl4_2,
inference(avatar_split_clause,[],[f28,f37]) ).
fof(f42,definition,
( spl4_3
<=> converse(sk1) = sF0 ),
introduced(definition,[new_symbols(definition,[spl4_3])],[avatar_definition]) ).
fof(f44,plain,
( converse(sk1) = sF0
| ~ spl4_3 ),
inference(avatar_component_clause,[],[f42]) ).
fof(f45,plain,
spl4_3,
inference(avatar_split_clause,[],[f21,f42]) ).
fof(f47,definition,
( spl4_4
<=> composition(sF1,sk1) = sF2 ),
introduced(definition,[new_symbols(definition,[spl4_4])],[avatar_definition]) ).
fof(f49,plain,
( composition(sF1,sk1) = sF2
| ~ spl4_4 ),
inference(avatar_component_clause,[],[f47]) ).
fof(f50,plain,
spl4_4,
inference(avatar_split_clause,[],[f25,f47]) ).
fof(f63,plain,
( sk1 = converse(sF0)
| ~ spl4_3 ),
inference(superposition,[],[f10,f44]) ).
fof(f65,definition,
( spl4_5
<=> composition(sk1,sF0) = sF1 ),
introduced(definition,[new_symbols(definition,[spl4_5])],[avatar_definition]) ).
fof(f67,plain,
( composition(sk1,sF0) = sF1
| ~ spl4_5 ),
inference(avatar_component_clause,[],[f65]) ).
fof(f68,plain,
spl4_5,
inference(avatar_split_clause,[],[f23,f65]) ).
fof(f73,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(f78,plain,
! [X0,X1] : join(complement(join(complement(X1),complement(X0))),complement(join(X0,complement(X1)))) = X1,
inference(superposition,[],[f4,f1]) ).
fof(f82,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))) = X0,
inference(superposition,[],[f1,f4]) ).
fof(f83,plain,
! [X0,X1] : join(complement(join(X0,complement(X1))),complement(join(complement(X1),complement(X0)))) = X1,
inference(forward_demodulation,[],[f78,f1]) ).
fof(f88,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,[],[f73,f1]) ).
fof(f90,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,[],[f88,f2]) ).
fof(f96,plain,
! [X0,X1] : complement(X1) = join(composition(X0,complement(composition(converse(X0),X1))),complement(X1)),
inference(superposition,[],[f14,f10]) ).
fof(f107,plain,
! [X0,X1] : complement(X1) = join(complement(X1),composition(X0,complement(composition(converse(X0),X1)))),
inference(forward_demodulation,[],[f96,f1]) ).
fof(f113,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(f115,plain,
! [X2,X0,X1] : join(complement(X0),X2) = join(composition(converse(X1),complement(composition(X1,X0))),join(complement(X0),X2)),
inference(superposition,[],[f2,f14]) ).
fof(f120,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f1,f2]) ).
fof(f121,plain,
! [X2,X0,X1] : join(complement(X0),X2) = join(complement(X0),join(X2,composition(converse(X1),complement(composition(X1,X0))))),
inference(forward_demodulation,[],[f115,f120]) ).
fof(f122,plain,
! [X2,X0,X1] : join(X0,X2) = join(complement(join(complement(X0),X1)),join(X2,complement(join(complement(X0),complement(X1))))),
inference(forward_demodulation,[],[f113,f120]) ).
fof(f129,plain,
( ! [X0] : composition(sk1,composition(sF0,X0)) = composition(sF1,X0)
| ~ spl4_5 ),
inference(superposition,[],[f7,f67]) ).
fof(f140,definition,
( spl4_6
<=> zero = complement(top) ),
introduced(definition,[new_symbols(definition,[spl4_6])],[avatar_definition]) ).
fof(f142,plain,
( zero = complement(top)
| ~ spl4_6 ),
inference(avatar_component_clause,[],[f140]) ).
fof(f143,plain,
spl4_6,
inference(avatar_split_clause,[],[f29,f140]) ).
fof(f145,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(top,X1),
inference(superposition,[],[f2,f15]) ).
fof(f147,plain,
! [X0] : join(complement(top),complement(join(complement(X0),complement(X0)))) = X0,
inference(superposition,[],[f4,f15]) ).
fof(f150,plain,
( ! [X0] : join(zero,complement(join(complement(X0),complement(X0)))) = X0
| ~ spl4_6 ),
inference(forward_demodulation,[],[f147,f142]) ).
fof(f159,plain,
( ! [X0] : converse(join(sk1,X0)) = join(sF0,converse(X0))
| ~ spl4_3 ),
inference(superposition,[],[f11,f44]) ).
fof(f160,plain,
! [X0,X1] : converse(join(converse(X0),X1)) = join(X0,converse(X1)),
inference(superposition,[],[f11,f10]) ).
fof(f162,plain,
! [X0,X1] : converse(join(X1,converse(X0))) = join(converse(X1),X0),
inference(superposition,[],[f11,f10]) ).
fof(f165,plain,
! [X2,X0,X1] : join(converse(X0),join(converse(X1),X2)) = join(converse(join(X0,X1)),X2),
inference(superposition,[],[f2,f11]) ).
fof(f177,plain,
! [X0,X1] : composition(converse(X1),X0) = converse(composition(converse(X0),X1)),
inference(superposition,[],[f12,f10]) ).
fof(f182,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(f189,plain,
! [X0] : converse(converse(X0)) = composition(converse(one),X0),
inference(superposition,[],[f177,f8]) ).
fof(f201,plain,
! [X0] : composition(converse(one),X0) = X0,
inference(forward_demodulation,[],[f189,f10]) ).
fof(f213,plain,
! [X0] : complement(X0) = join(complement(X0),composition(one,complement(X0))),
inference(superposition,[],[f107,f201]) ).
fof(f219,plain,
one = converse(one),
inference(superposition,[],[f8,f201]) ).
fof(f222,plain,
! [X0] : composition(one,X0) = X0,
inference(backward_demodulation,[],[f201,f219]) ).
fof(f229,plain,
! [X0] : complement(X0) = join(complement(X0),complement(X0)),
inference(backward_demodulation,[],[f213,f222]) ).
fof(f233,plain,
( ! [X0] : join(zero,complement(complement(X0))) = X0
| ~ spl4_6 ),
inference(backward_demodulation,[],[f150,f229]) ).
fof(f277,plain,
! [X0,X1] : join(complement(join(X0,complement(X1))),complement(join(complement(X0),complement(X1)))) = X1,
inference(superposition,[],[f83,f1]) ).
fof(f279,plain,
! [X0,X1] : join(X1,complement(X0)) = join(complement(join(complement(join(X1,complement(X0))),complement(complement(join(complement(X0),complement(X1)))))),complement(X0)),
inference(superposition,[],[f4,f83]) ).
fof(f281,plain,
! [X0,X1] : join(X1,complement(X0)) = join(complement(X0),complement(join(complement(join(X1,complement(X0))),complement(complement(join(complement(X0),complement(X1))))))),
inference(forward_demodulation,[],[f279,f1]) ).
fof(f345,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),complement(complement(X1))))) = join(complement(join(complement(X0),X1)),X0),
inference(superposition,[],[f122,f4]) ).
fof(f346,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),X0) = join(X0,complement(join(X1,complement(X0)))),
inference(superposition,[],[f122,f83]) ).
fof(f347,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,[],[f122,f229]) ).
fof(f354,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),complement(X1)))) = X0,
inference(forward_demodulation,[],[f347,f82]) ).
fof(f355,plain,
! [X0,X1] : join(X0,complement(join(X1,complement(X0)))) = join(X0,complement(join(complement(X0),X1))),
inference(forward_demodulation,[],[f346,f1]) ).
fof(f356,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),complement(complement(X1))))) = join(X0,complement(join(complement(X0),X1))),
inference(forward_demodulation,[],[f345,f1]) ).
fof(f368,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),X1))) = X0,
inference(forward_demodulation,[],[f356,f354]) ).
fof(f376,plain,
! [X0,X1] : join(X0,complement(join(X1,complement(X0)))) = X0,
inference(backward_demodulation,[],[f355,f368]) ).
fof(f382,plain,
! [X0,X1] : join(complement(X0),complement(X1)) = join(complement(X0),complement(join(complement(X0),X1))),
inference(backward_demodulation,[],[f90,f376]) ).
fof(f389,plain,
! [X0,X1] : join(complement(join(X1,complement(X0))),complement(complement(join(complement(X0),complement(X1))))) = join(complement(join(X1,complement(X0))),complement(X0)),
inference(superposition,[],[f382,f83]) ).
fof(f394,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = join(complement(X1),complement(join(X0,complement(X1)))),
inference(superposition,[],[f382,f1]) ).
fof(f395,plain,
! [X0] : join(complement(X0),complement(complement(complement(X0)))) = join(complement(X0),complement(top)),
inference(superposition,[],[f382,f15]) ).
fof(f401,plain,
! [X0,X1] : join(X0,complement(X0)) = join(complement(join(complement(X0),X1)),join(complement(X0),complement(complement(X1)))),
inference(superposition,[],[f122,f382]) ).
fof(f406,plain,
! [X0,X1] : join(X0,complement(X0)) = join(complement(complement(X1)),join(complement(join(complement(X0),X1)),complement(X0))),
inference(forward_demodulation,[],[f401,f120]) ).
fof(f411,plain,
( ! [X0] : join(complement(X0),complement(complement(complement(X0)))) = join(complement(X0),zero)
| ~ spl4_6 ),
inference(forward_demodulation,[],[f395,f142]) ).
fof(f418,plain,
! [X0,X1] : join(complement(join(X1,complement(X0))),complement(complement(join(complement(X0),complement(X1))))) = join(complement(X0),complement(join(X1,complement(X0)))),
inference(forward_demodulation,[],[f389,f1]) ).
fof(f420,plain,
! [X0,X1] : join(X0,complement(X0)) = join(complement(complement(X1)),join(complement(X0),complement(join(complement(X0),X1)))),
inference(forward_demodulation,[],[f406,f1]) ).
fof(f423,plain,
( ! [X0] : join(complement(X0),complement(complement(complement(X0)))) = join(zero,complement(X0))
| ~ spl4_6 ),
inference(forward_demodulation,[],[f411,f1]) ).
fof(f429,plain,
! [X0,X1] : join(complement(X0),complement(X1)) = join(complement(join(X1,complement(X0))),complement(complement(join(complement(X0),complement(X1))))),
inference(forward_demodulation,[],[f418,f394]) ).
fof(f431,plain,
! [X0,X1] : join(X0,complement(X0)) = join(complement(complement(X1)),join(complement(X0),complement(X1))),
inference(forward_demodulation,[],[f420,f382]) ).
fof(f439,plain,
! [X0,X1] : join(X1,complement(X0)) = join(complement(X0),complement(join(complement(X0),complement(X1)))),
inference(backward_demodulation,[],[f281,f429]) ).
fof(f441,plain,
! [X0,X1] : join(X0,complement(X0)) = join(complement(X1),join(complement(complement(X1)),complement(X0))),
inference(forward_demodulation,[],[f431,f120]) ).
fof(f444,plain,
! [X0,X1] : join(X1,complement(X0)) = join(complement(X0),complement(complement(X1))),
inference(forward_demodulation,[],[f439,f382]) ).
fof(f447,plain,
! [X0] : join(X0,complement(X0)) = join(top,complement(X0)),
inference(forward_demodulation,[],[f441,f145]) ).
fof(f450,plain,
( ! [X0] : join(complement(X0),complement(X0)) = join(zero,complement(X0))
| ~ spl4_6 ),
inference(backward_demodulation,[],[f423,f444]) ).
fof(f456,plain,
! [X0] : top = join(top,complement(X0)),
inference(forward_demodulation,[],[f447,f15]) ).
fof(f460,plain,
( ! [X0] : complement(X0) = join(zero,complement(X0))
| ~ spl4_6 ),
inference(forward_demodulation,[],[f450,f229]) ).
fof(f466,plain,
( ! [X0] : complement(complement(X0)) = X0
| ~ spl4_6 ),
inference(backward_demodulation,[],[f233,f460]) ).
fof(f498,plain,
( ! [X0,X1] : complement(X0) = join(complement(join(X0,complement(X1))),complement(join(X0,X1)))
| ~ spl4_6 ),
inference(superposition,[],[f4,f466]) ).
fof(f503,plain,
( ! [X0,X1] : complement(X0) = join(complement(join(X1,X0)),complement(join(X0,complement(X1))))
| ~ spl4_6 ),
inference(superposition,[],[f83,f466]) ).
fof(f507,plain,
( ! [X0] : join(X0,X0) = X0
| ~ spl4_6 ),
inference(superposition,[],[f229,f466]) ).
fof(f508,plain,
( ! [X0,X1] : join(X0,complement(X1)) = join(X0,complement(join(X0,X1)))
| ~ spl4_6 ),
inference(superposition,[],[f382,f466]) ).
fof(f516,plain,
( ! [X0,X1] : complement(X0) = join(complement(join(X0,X1)),complement(join(X0,complement(X1))))
| ~ spl4_6 ),
inference(forward_demodulation,[],[f498,f1]) ).
fof(f518,plain,
( ! [X0] : join(zero,X0) = X0
| ~ spl4_6 ),
inference(superposition,[],[f460,f466]) ).
fof(f524,plain,
( ! [X0] : top = join(top,X0)
| ~ spl4_6 ),
inference(superposition,[],[f456,f466]) ).
fof(f527,plain,
( ! [X0,X1] : top = join(X0,join(complement(X0),X1))
| ~ spl4_6 ),
inference(backward_demodulation,[],[f145,f524]) ).
fof(f534,plain,
( ! [X0] : join(X0,zero) = X0
| ~ spl4_6 ),
inference(superposition,[],[f1,f518]) ).
fof(f619,plain,
( ! [X0] : top = join(X0,top)
| ~ spl4_6 ),
inference(superposition,[],[f1,f524]) ).
fof(f777,plain,
! [X0] : join(X0,converse(complement(converse(X0)))) = converse(top),
inference(superposition,[],[f160,f15]) ).
fof(f784,plain,
! [X2,X0,X1] : composition(join(X0,converse(X1)),converse(X2)) = converse(composition(X2,join(converse(X0),X1))),
inference(superposition,[],[f12,f160]) ).
fof(f816,plain,
( top = converse(top)
| ~ spl4_6 ),
inference(superposition,[],[f524,f777]) ).
fof(f821,plain,
( ! [X0] : top = join(X0,converse(complement(converse(X0))))
| ~ spl4_6 ),
inference(backward_demodulation,[],[f777,f816]) ).
fof(f898,plain,
( ! [X0] : composition(join(converse(sF0),X0),converse(sk1)) = join(converse(sF1),composition(X0,converse(sk1)))
| ~ spl4_5 ),
inference(superposition,[],[f182,f67]) ).
fof(f908,plain,
! [X2,X0,X1] : composition(join(converse(X2),converse(X1)),converse(X0)) = join(converse(composition(X0,X2)),converse(composition(X0,X1))),
inference(superposition,[],[f182,f12]) ).
fof(f922,plain,
! [X2,X0,X1] : composition(join(converse(X2),converse(X1)),converse(X0)) = converse(join(composition(X0,X2),composition(X0,X1))),
inference(forward_demodulation,[],[f908,f11]) ).
fof(f929,plain,
( ! [X0] : composition(join(converse(sF0),X0),sF0) = join(converse(sF1),composition(X0,sF0))
| ~ spl4_3
| ~ spl4_5 ),
inference(forward_demodulation,[],[f898,f44]) ).
fof(f939,plain,
! [X2,X0,X1] : converse(join(composition(X0,X2),composition(X0,X1))) = converse(composition(X0,join(converse(converse(X2)),X1))),
inference(forward_demodulation,[],[f922,f784]) ).
fof(f942,plain,
( ! [X0] : composition(join(sk1,X0),sF0) = join(converse(sF1),composition(X0,sF0))
| ~ spl4_3
| ~ spl4_5 ),
inference(forward_demodulation,[],[f929,f63]) ).
fof(f948,plain,
! [X2,X0,X1] : converse(join(composition(X0,X2),composition(X0,X1))) = converse(composition(X0,join(X2,X1))),
inference(forward_demodulation,[],[f939,f10]) ).
fof(f974,plain,
! [X2,X0,X1] : join(composition(X0,X1),composition(X0,X2)) = converse(converse(composition(X0,join(X1,X2)))),
inference(superposition,[],[f10,f948]) ).
fof(f992,plain,
! [X2,X0,X1] : composition(X0,join(X1,X2)) = join(composition(X0,X1),composition(X0,X2)),
inference(forward_demodulation,[],[f974,f10]) ).
fof(f1024,plain,
! [X0,X1] : join(X0,composition(X0,X1)) = composition(X0,join(one,X1)),
inference(superposition,[],[f992,f8]) ).
fof(f1046,plain,
! [X2,X3,X0,X1] : join(composition(X0,join(X1,X2)),X3) = join(composition(X0,X1),join(composition(X0,X2),X3)),
inference(superposition,[],[f2,f992]) ).
fof(f1180,plain,
! [X0] : join(X0,composition(X0,complement(one))) = composition(X0,top),
inference(superposition,[],[f1024,f15]) ).
fof(f1384,plain,
( ! [X0] : zero = join(composition(converse(X0),complement(composition(X0,top))),zero)
| ~ spl4_6 ),
inference(superposition,[],[f14,f142]) ).
fof(f1394,plain,
( ! [X0] : zero = join(zero,composition(converse(X0),complement(composition(X0,top))))
| ~ spl4_6 ),
inference(forward_demodulation,[],[f1384,f1]) ).
fof(f1399,plain,
( ! [X0] : zero = composition(converse(X0),complement(composition(X0,top)))
| ~ spl4_6 ),
inference(forward_demodulation,[],[f1394,f518]) ).
fof(f1425,plain,
( ! [X0,X1] : composition(converse(X0),join(X1,complement(composition(X0,top)))) = join(composition(converse(X0),X1),zero)
| ~ spl4_6 ),
inference(superposition,[],[f992,f1399]) ).
fof(f1428,plain,
( ! [X0,X1] : join(zero,composition(converse(X0),X1)) = composition(converse(X0),join(X1,complement(composition(X0,top))))
| ~ spl4_6 ),
inference(forward_demodulation,[],[f1425,f1]) ).
fof(f1440,plain,
( ! [X0,X1] : composition(converse(X0),X1) = composition(converse(X0),join(X1,complement(composition(X0,top))))
| ~ spl4_6 ),
inference(forward_demodulation,[],[f1428,f518]) ).
fof(f1459,definition,
( spl4_8
<=> sk1 = converse(sF0) ),
introduced(definition,[new_symbols(definition,[spl4_8])],[avatar_definition]) ).
fof(f1461,plain,
( sk1 = converse(sF0)
| ~ spl4_8 ),
inference(avatar_component_clause,[],[f1459]) ).
fof(f1462,plain,
( spl4_8
| ~ spl4_3 ),
inference(avatar_split_clause,[],[f63,f42,f1459]) ).
fof(f1467,plain,
( ! [X0] : converse(composition(X0,sF0)) = composition(sk1,converse(X0))
| ~ spl4_8 ),
inference(superposition,[],[f12,f1461]) ).
fof(f1611,plain,
( ! [X0,X1] : join(sF0,join(converse(X0),X1)) = join(converse(join(sk1,X0)),X1)
| ~ spl4_3 ),
inference(superposition,[],[f2,f159]) ).
fof(f1623,plain,
( ! [X0,X1] : join(X1,complement(X0)) = join(X1,complement(join(X0,X1)))
| ~ spl4_6 ),
inference(superposition,[],[f508,f1]) ).
fof(f1628,plain,
( ! [X0] : join(X0,complement(top)) = join(X0,complement(converse(complement(converse(X0)))))
| ~ spl4_6 ),
inference(superposition,[],[f508,f821]) ).
fof(f1644,plain,
( join(sF2,complement(sk1)) = join(sF2,complement(sF3))
| ~ spl4_1
| ~ spl4_6 ),
inference(superposition,[],[f508,f34]) ).
fof(f1689,plain,
( ! [X0] : join(X0,zero) = join(X0,complement(converse(complement(converse(X0)))))
| ~ spl4_6 ),
inference(forward_demodulation,[],[f1628,f142]) ).
fof(f1708,plain,
( ! [X0] : join(X0,complement(converse(complement(converse(X0))))) = X0
| ~ spl4_6 ),
inference(forward_demodulation,[],[f1689,f534]) ).
fof(f1879,plain,
! [X2,X0,X1] : join(converse(X1),join(X2,converse(X0))) = join(X2,converse(join(X0,X1))),
inference(superposition,[],[f120,f11]) ).
fof(f2182,plain,
( ! [X0] : converse(converse(X0)) = join(X0,converse(complement(converse(complement(converse(converse(X0)))))))
| ~ spl4_6 ),
inference(superposition,[],[f160,f1708]) ).
fof(f2187,plain,
( ! [X0] : join(X0,converse(complement(converse(complement(X0))))) = X0
| ~ spl4_6 ),
inference(forward_demodulation,[],[f2182,f10]) ).
fof(f2230,plain,
( join(sk1,complement(sF2)) = join(sk1,complement(sF3))
| ~ spl4_1
| ~ spl4_6 ),
inference(superposition,[],[f1623,f34]) ).
fof(f2510,plain,
( ! [X0,X1] : complement(X0) = join(complement(join(X1,X0)),complement(join(complement(X1),X0)))
| ~ spl4_6 ),
inference(superposition,[],[f277,f466]) ).
fof(f2523,plain,
( ! [X0] : converse(complement(converse(complement(X0)))) = join(complement(join(X0,complement(converse(complement(converse(complement(X0))))))),complement(complement(X0)))
| ~ spl4_6 ),
inference(superposition,[],[f277,f1708]) ).
fof(f2555,plain,
( ! [X0] : converse(complement(converse(complement(X0)))) = join(complement(complement(X0)),complement(join(X0,complement(converse(complement(converse(complement(X0))))))))
| ~ spl4_6 ),
inference(forward_demodulation,[],[f2523,f1]) ).
fof(f2600,plain,
( ! [X0] : converse(complement(converse(complement(X0)))) = join(X0,complement(join(X0,complement(converse(complement(converse(complement(X0))))))))
| ~ spl4_6 ),
inference(forward_demodulation,[],[f2555,f466]) ).
fof(f2637,plain,
( ! [X0] : converse(complement(converse(complement(X0)))) = join(X0,complement(complement(converse(complement(converse(complement(X0)))))))
| ~ spl4_6 ),
inference(forward_demodulation,[],[f2600,f508]) ).
fof(f2666,plain,
( ! [X0] : converse(complement(converse(complement(X0)))) = join(X0,converse(complement(converse(complement(X0)))))
| ~ spl4_6 ),
inference(forward_demodulation,[],[f2637,f466]) ).
fof(f2690,plain,
( ! [X0] : converse(complement(converse(complement(X0)))) = X0
| ~ spl4_6 ),
inference(forward_demodulation,[],[f2666,f2187]) ).
fof(f2705,plain,
( ! [X0] : complement(X0) = converse(complement(converse(X0)))
| ~ spl4_6 ),
inference(superposition,[],[f2690,f466]) ).
fof(f2804,plain,
( ! [X0] : complement(converse(X0)) = converse(complement(X0))
| ~ spl4_6 ),
inference(superposition,[],[f10,f2705]) ).
fof(f2805,plain,
( ! [X0,X1] : converse(join(complement(converse(X0)),X1)) = join(complement(X0),converse(X1))
| ~ spl4_6 ),
inference(superposition,[],[f11,f2705]) ).
fof(f2905,plain,
( ! [X0] : join(complement(sF0),converse(X0)) = converse(join(complement(sk1),X0))
| ~ spl4_6
| ~ spl4_8 ),
inference(superposition,[],[f2805,f1461]) ).
fof(f3000,definition,
( spl4_12
<=> top = converse(top) ),
introduced(definition,[new_symbols(definition,[spl4_12])],[avatar_definition]) ).
fof(f3002,plain,
( top = converse(top)
| ~ spl4_12 ),
inference(avatar_component_clause,[],[f3000]) ).
fof(f3003,plain,
( spl4_12
| ~ spl4_6 ),
inference(avatar_split_clause,[],[f816,f140,f3000]) ).
fof(f3014,plain,
( ! [X0] : composition(converse(X0),top) = converse(composition(top,X0))
| ~ spl4_12 ),
inference(superposition,[],[f177,f3002]) ).
fof(f3134,plain,
( composition(join(sk1,sk1),sF0) = join(converse(sF1),sF1)
| ~ spl4_3
| ~ spl4_5 ),
inference(superposition,[],[f942,f67]) ).
fof(f3154,plain,
( composition(join(sk1,sk1),sF0) = join(sF1,converse(sF1))
| ~ spl4_3
| ~ spl4_5 ),
inference(forward_demodulation,[],[f3134,f1]) ).
fof(f3159,plain,
( composition(sk1,sF0) = join(sF1,converse(sF1))
| ~ spl4_3
| ~ spl4_5
| ~ spl4_6 ),
inference(forward_demodulation,[],[f3154,f507]) ).
fof(f3161,plain,
( sF1 = join(sF1,converse(sF1))
| ~ spl4_3
| ~ spl4_5
| ~ spl4_6 ),
inference(forward_demodulation,[],[f3159,f67]) ).
fof(f3166,definition,
( spl4_13
<=> sF1 = join(sF1,converse(sF1)) ),
introduced(definition,[new_symbols(definition,[spl4_13])],[avatar_definition]) ).
fof(f3168,plain,
( sF1 = join(sF1,converse(sF1))
| ~ spl4_13 ),
inference(avatar_component_clause,[],[f3166]) ).
fof(f3169,plain,
( spl4_13
| ~ spl4_3
| ~ spl4_5
| ~ spl4_6 ),
inference(avatar_split_clause,[],[f3161,f140,f65,f42,f3166]) ).
fof(f3640,plain,
! [X2,X0,X1] : join(composition(converse(X1),join(X2,complement(composition(X1,X0)))),complement(X0)) = join(composition(converse(X1),X2),complement(X0)),
inference(superposition,[],[f1046,f14]) ).
fof(f3705,plain,
! [X2,X0,X1] : join(composition(converse(X1),X2),complement(X0)) = join(complement(X0),composition(converse(X1),join(X2,complement(composition(X1,X0))))),
inference(forward_demodulation,[],[f3640,f1]) ).
fof(f3777,plain,
( converse(sF1) = join(converse(sF1),sF1)
| ~ spl4_13 ),
inference(superposition,[],[f162,f3168]) ).
fof(f3807,plain,
( converse(sF1) = join(sF1,converse(sF1))
| ~ spl4_13 ),
inference(forward_demodulation,[],[f3777,f1]) ).
fof(f3830,plain,
( sF1 = converse(sF1)
| ~ spl4_13 ),
inference(forward_demodulation,[],[f3807,f3168]) ).
fof(f3865,definition,
( spl4_14
<=> sF1 = converse(sF1) ),
introduced(definition,[new_symbols(definition,[spl4_14])],[avatar_definition]) ).
fof(f3867,plain,
( sF1 = converse(sF1)
| ~ spl4_14 ),
inference(avatar_component_clause,[],[f3865]) ).
fof(f3868,plain,
( spl4_14
| ~ spl4_13 ),
inference(avatar_split_clause,[],[f3830,f3166,f3865]) ).
fof(f3880,plain,
( ! [X0] : converse(composition(sF1,X0)) = composition(converse(X0),sF1)
| ~ spl4_14 ),
inference(superposition,[],[f177,f3867]) ).
fof(f5493,plain,
( ! [X0] : top = join(X0,composition(complement(X0),top))
| ~ spl4_6 ),
inference(superposition,[],[f527,f1180]) ).
fof(f6053,plain,
( ! [X0] : composition(converse(X0),top) = composition(converse(X0),composition(X0,top))
| ~ spl4_6 ),
inference(superposition,[],[f1440,f15]) ).
fof(f6092,plain,
( ! [X0] : converse(composition(top,X0)) = composition(converse(X0),composition(X0,top))
| ~ spl4_6
| ~ spl4_12 ),
inference(forward_demodulation,[],[f6053,f3014]) ).
fof(f6304,plain,
! [X2,X0,X1] : join(complement(X1),X2) = join(complement(X1),join(X2,composition(X0,complement(composition(converse(X0),X1))))),
inference(superposition,[],[f121,f10]) ).
fof(f7330,plain,
! [X2,X0,X1] : join(complement(X2),composition(X0,X1)) = join(complement(X2),composition(X0,join(X1,complement(composition(converse(X0),X2))))),
inference(superposition,[],[f6304,f992]) ).
fof(f7944,definition,
( spl4_21
<=> join(sk1,complement(sF2)) = join(sk1,complement(sF3)) ),
introduced(definition,[new_symbols(definition,[spl4_21])],[avatar_definition]) ).
fof(f7946,plain,
( join(sk1,complement(sF2)) = join(sk1,complement(sF3))
| ~ spl4_21 ),
inference(avatar_component_clause,[],[f7944]) ).
fof(f7947,plain,
( spl4_21
| ~ spl4_1
| ~ spl4_6 ),
inference(avatar_split_clause,[],[f2230,f140,f32,f7944]) ).
fof(f7957,plain,
( complement(complement(sF2)) = join(complement(join(sk1,complement(sF3))),complement(join(complement(sF2),complement(sk1))))
| ~ spl4_6
| ~ spl4_21 ),
inference(superposition,[],[f503,f7946]) ).
fof(f7975,plain,
( sF2 = join(complement(join(sk1,complement(sF3))),complement(join(complement(sF2),complement(sk1))))
| ~ spl4_6
| ~ spl4_21 ),
inference(forward_demodulation,[],[f7957,f466]) ).
fof(f8010,definition,
( spl4_22
<=> join(sF2,complement(sk1)) = join(sF2,complement(sF3)) ),
introduced(definition,[new_symbols(definition,[spl4_22])],[avatar_definition]) ).
fof(f8012,plain,
( join(sF2,complement(sk1)) = join(sF2,complement(sF3))
| ~ spl4_22 ),
inference(avatar_component_clause,[],[f8010]) ).
fof(f8013,plain,
( spl4_22
| ~ spl4_1
| ~ spl4_6 ),
inference(avatar_split_clause,[],[f1644,f140,f32,f8010]) ).
fof(f8699,plain,
( converse(composition(top,sF0)) = composition(sk1,composition(sF0,top))
| ~ spl4_6
| ~ spl4_8
| ~ spl4_12 ),
inference(superposition,[],[f6092,f1461]) ).
fof(f8749,plain,
( composition(sF1,top) = converse(composition(top,sF0))
| ~ spl4_5
| ~ spl4_6
| ~ spl4_8
| ~ spl4_12 ),
inference(forward_demodulation,[],[f8699,f129]) ).
fof(f8913,plain,
( composition(sk1,top) = converse(composition(top,sF0))
| ~ spl4_8
| ~ spl4_12 ),
inference(superposition,[],[f1467,f3002]) ).
fof(f8958,plain,
( composition(sk1,top) = composition(sF1,top)
| ~ spl4_5
| ~ spl4_6
| ~ spl4_8
| ~ spl4_12 ),
inference(forward_demodulation,[],[f8913,f8749]) ).
fof(f9269,plain,
! [X2,X0,X1] : join(converse(X2),join(X0,converse(X1))) = join(converse(join(X2,X1)),X0),
inference(superposition,[],[f165,f1]) ).
fof(f9359,plain,
! [X2,X0,X1] : join(X0,converse(join(X1,X2))) = join(converse(join(X2,X1)),X0),
inference(forward_demodulation,[],[f9269,f1879]) ).
fof(f11390,plain,
( ! [X0] : converse(top) = join(complement(X0),converse(composition(complement(complement(converse(X0))),top)))
| ~ spl4_6 ),
inference(superposition,[],[f2805,f5493]) ).
fof(f11414,plain,
( ! [X0] : converse(top) = join(complement(X0),converse(composition(converse(X0),top)))
| ~ spl4_6 ),
inference(forward_demodulation,[],[f11390,f466]) ).
fof(f11446,plain,
( ! [X0] : converse(top) = join(complement(X0),composition(converse(top),X0))
| ~ spl4_6 ),
inference(forward_demodulation,[],[f11414,f177]) ).
fof(f11462,plain,
( ! [X0] : top = join(complement(X0),composition(top,X0))
| ~ spl4_6
| ~ spl4_12 ),
inference(forward_demodulation,[],[f11446,f3002]) ).
fof(f16784,plain,
! [X0,X1] : join(composition(converse(X0),composition(X0,X1)),complement(X1)) = join(complement(X1),composition(converse(X0),top)),
inference(superposition,[],[f3705,f15]) ).
fof(f16855,plain,
( ! [X0,X1] : join(composition(converse(X0),composition(X0,X1)),complement(X1)) = join(complement(X1),converse(composition(top,X0)))
| ~ spl4_12 ),
inference(forward_demodulation,[],[f16784,f3014]) ).
fof(f16914,plain,
( ! [X0,X1] : join(complement(X1),converse(composition(top,X0))) = join(complement(X1),composition(converse(X0),composition(X0,X1)))
| ~ spl4_12 ),
inference(forward_demodulation,[],[f16855,f1]) ).
fof(f18306,plain,
! [X0,X1] : join(complement(X0),composition(X1,top)) = join(complement(X0),composition(X1,composition(converse(X1),X0))),
inference(superposition,[],[f7330,f15]) ).
fof(f18498,plain,
( ! [X0] : join(complement(X0),composition(sk1,top)) = join(complement(X0),composition(sk1,composition(sF0,X0)))
| ~ spl4_3 ),
inference(superposition,[],[f18306,f44]) ).
fof(f18596,plain,
( ! [X0] : join(complement(X0),composition(sk1,top)) = join(complement(X0),composition(sF1,X0))
| ~ spl4_3
| ~ spl4_5 ),
inference(forward_demodulation,[],[f18498,f129]) ).
fof(f18636,plain,
( ! [X0] : join(complement(X0),composition(sF1,top)) = join(complement(X0),composition(sF1,X0))
| ~ spl4_3
| ~ spl4_5
| ~ spl4_6
| ~ spl4_8
| ~ spl4_12 ),
inference(forward_demodulation,[],[f18596,f8958]) ).
fof(f18704,plain,
( join(complement(sk1),sF2) = join(complement(sk1),composition(sF1,top))
| ~ spl4_3
| ~ spl4_4
| ~ spl4_5
| ~ spl4_6
| ~ spl4_8
| ~ spl4_12 ),
inference(superposition,[],[f18636,f49]) ).
fof(f18820,plain,
( join(sF2,complement(sk1)) = join(complement(sk1),composition(sF1,top))
| ~ spl4_3
| ~ spl4_4
| ~ spl4_5
| ~ spl4_6
| ~ spl4_8
| ~ spl4_12 ),
inference(forward_demodulation,[],[f18704,f1]) ).
fof(f18843,plain,
( join(sF2,complement(sF3)) = join(complement(sk1),composition(sF1,top))
| ~ spl4_3
| ~ spl4_4
| ~ spl4_5
| ~ spl4_6
| ~ spl4_8
| ~ spl4_12
| ~ spl4_22 ),
inference(forward_demodulation,[],[f18820,f8012]) ).
fof(f29236,plain,
( ! [X0,X1] : join(complement(sF0),join(converse(X0),X1)) = join(converse(join(complement(sk1),X0)),X1)
| ~ spl4_6
| ~ spl4_8 ),
inference(superposition,[],[f2,f2905]) ).
fof(f41735,plain,
( join(complement(sF0),converse(composition(top,sk1))) = join(complement(sF0),composition(converse(sk1),sF1))
| ~ spl4_5
| ~ spl4_12 ),
inference(superposition,[],[f16914,f67]) ).
fof(f41928,plain,
( join(complement(sF0),converse(composition(top,sk1))) = join(complement(sF0),converse(composition(sF1,sk1)))
| ~ spl4_5
| ~ spl4_12
| ~ spl4_14 ),
inference(forward_demodulation,[],[f41735,f3880]) ).
fof(f42034,plain,
( join(complement(sF0),converse(composition(top,sk1))) = converse(join(complement(sk1),composition(sF1,sk1)))
| ~ spl4_5
| ~ spl4_6
| ~ spl4_8
| ~ spl4_12
| ~ spl4_14 ),
inference(forward_demodulation,[],[f41928,f2905]) ).
fof(f42114,plain,
( join(complement(sF0),converse(composition(top,sk1))) = converse(join(complement(sk1),composition(sF1,top)))
| ~ spl4_3
| ~ spl4_5
| ~ spl4_6
| ~ spl4_8
| ~ spl4_12
| ~ spl4_14 ),
inference(forward_demodulation,[],[f42034,f18636]) ).
fof(f42182,plain,
( converse(join(sF2,complement(sF3))) = join(complement(sF0),converse(composition(top,sk1)))
| ~ spl4_3
| ~ spl4_4
| ~ spl4_5
| ~ spl4_6
| ~ spl4_8
| ~ spl4_12
| ~ spl4_14
| ~ spl4_22 ),
inference(forward_demodulation,[],[f42114,f18843]) ).
fof(f42231,plain,
( converse(join(sF2,complement(sF3))) = converse(join(complement(sk1),composition(top,sk1)))
| ~ spl4_3
| ~ spl4_4
| ~ spl4_5
| ~ spl4_6
| ~ spl4_8
| ~ spl4_12
| ~ spl4_14
| ~ spl4_22 ),
inference(forward_demodulation,[],[f42182,f2905]) ).
fof(f42270,plain,
( converse(top) = converse(join(sF2,complement(sF3)))
| ~ spl4_3
| ~ spl4_4
| ~ spl4_5
| ~ spl4_6
| ~ spl4_8
| ~ spl4_12
| ~ spl4_14
| ~ spl4_22 ),
inference(forward_demodulation,[],[f42231,f11462]) ).
fof(f42299,plain,
( top = converse(join(sF2,complement(sF3)))
| ~ spl4_3
| ~ spl4_4
| ~ spl4_5
| ~ spl4_6
| ~ spl4_8
| ~ spl4_12
| ~ spl4_14
| ~ spl4_22 ),
inference(forward_demodulation,[],[f42270,f3002]) ).
fof(f59382,plain,
( ! [X0] : join(converse(join(complement(sk1),sF2)),X0) = join(X0,converse(join(sF2,complement(sF3))))
| ~ spl4_22 ),
inference(superposition,[],[f9359,f8012]) ).
fof(f59386,plain,
( ! [X0] : join(X0,converse(sF3)) = join(converse(join(sk1,sF2)),X0)
| ~ spl4_1 ),
inference(superposition,[],[f9359,f34]) ).
fof(f60095,plain,
( ! [X0] : join(X0,converse(sF3)) = join(sF0,join(converse(sF2),X0))
| ~ spl4_1
| ~ spl4_3 ),
inference(forward_demodulation,[],[f59386,f1611]) ).
fof(f60099,plain,
( ! [X0] : join(X0,top) = join(converse(join(complement(sk1),sF2)),X0)
| ~ spl4_3
| ~ spl4_4
| ~ spl4_5
| ~ spl4_6
| ~ spl4_8
| ~ spl4_12
| ~ spl4_14
| ~ spl4_22 ),
inference(forward_demodulation,[],[f59382,f42299]) ).
fof(f60445,plain,
( ! [X0] : join(X0,top) = join(complement(sF0),join(converse(sF2),X0))
| ~ spl4_3
| ~ spl4_4
| ~ spl4_5
| ~ spl4_6
| ~ spl4_8
| ~ spl4_12
| ~ spl4_14
| ~ spl4_22 ),
inference(forward_demodulation,[],[f60099,f29236]) ).
fof(f60626,plain,
( ! [X0] : top = join(complement(sF0),join(converse(sF2),X0))
| ~ spl4_3
| ~ spl4_4
| ~ spl4_5
| ~ spl4_6
| ~ spl4_8
| ~ spl4_12
| ~ spl4_14
| ~ spl4_22 ),
inference(forward_demodulation,[],[f60445,f619]) ).
fof(f60885,plain,
( ! [X0] : complement(join(converse(sF2),X0)) = join(complement(join(X0,converse(sF3))),complement(join(complement(sF0),join(converse(sF2),X0))))
| ~ spl4_1
| ~ spl4_3
| ~ spl4_6 ),
inference(superposition,[],[f2510,f60095]) ).
fof(f60928,plain,
( ! [X0] : complement(join(converse(sF2),X0)) = join(complement(join(X0,converse(sF3))),complement(top))
| ~ spl4_1
| ~ spl4_3
| ~ spl4_4
| ~ spl4_5
| ~ spl4_6
| ~ spl4_8
| ~ spl4_12
| ~ spl4_14
| ~ spl4_22 ),
inference(forward_demodulation,[],[f60885,f60626]) ).
fof(f61012,plain,
( ! [X0] : complement(join(converse(sF2),X0)) = join(complement(top),complement(join(X0,converse(sF3))))
| ~ spl4_1
| ~ spl4_3
| ~ spl4_4
| ~ spl4_5
| ~ spl4_6
| ~ spl4_8
| ~ spl4_12
| ~ spl4_14
| ~ spl4_22 ),
inference(forward_demodulation,[],[f60928,f1]) ).
fof(f61079,plain,
( ! [X0] : complement(join(converse(sF2),X0)) = join(zero,complement(join(X0,converse(sF3))))
| ~ spl4_1
| ~ spl4_3
| ~ spl4_4
| ~ spl4_5
| ~ spl4_6
| ~ spl4_8
| ~ spl4_12
| ~ spl4_14
| ~ spl4_22 ),
inference(forward_demodulation,[],[f61012,f142]) ).
fof(f61135,plain,
( ! [X0] : complement(join(converse(sF2),X0)) = complement(join(X0,converse(sF3)))
| ~ spl4_1
| ~ spl4_3
| ~ spl4_4
| ~ spl4_5
| ~ spl4_6
| ~ spl4_8
| ~ spl4_12
| ~ spl4_14
| ~ spl4_22 ),
inference(forward_demodulation,[],[f61079,f518]) ).
fof(f61992,plain,
( ! [X0] : complement(converse(sF2)) = join(complement(join(converse(sF2),X0)),complement(join(complement(X0),converse(sF3))))
| ~ spl4_1
| ~ spl4_3
| ~ spl4_4
| ~ spl4_5
| ~ spl4_6
| ~ spl4_8
| ~ spl4_12
| ~ spl4_14
| ~ spl4_22 ),
inference(superposition,[],[f516,f61135]) ).
fof(f62086,plain,
( ! [X0] : complement(converse(sF3)) = join(complement(join(converse(sF2),X0)),complement(join(complement(X0),converse(sF3))))
| ~ spl4_1
| ~ spl4_3
| ~ spl4_4
| ~ spl4_5
| ~ spl4_6
| ~ spl4_8
| ~ spl4_12
| ~ spl4_14
| ~ spl4_22 ),
inference(superposition,[],[f2510,f61135]) ).
fof(f62269,plain,
( complement(converse(sF2)) = complement(converse(sF3))
| ~ spl4_1
| ~ spl4_3
| ~ spl4_4
| ~ spl4_5
| ~ spl4_6
| ~ spl4_8
| ~ spl4_12
| ~ spl4_14
| ~ spl4_22 ),
inference(forward_demodulation,[],[f61992,f62086]) ).
fof(f62578,definition,
( spl4_74
<=> complement(converse(sF2)) = complement(converse(sF3)) ),
introduced(definition,[new_symbols(definition,[spl4_74])],[avatar_definition]) ).
fof(f62580,plain,
( complement(converse(sF2)) = complement(converse(sF3))
| ~ spl4_74 ),
inference(avatar_component_clause,[],[f62578]) ).
fof(f62581,plain,
( spl4_74
| ~ spl4_1
| ~ spl4_3
| ~ spl4_4
| ~ spl4_5
| ~ spl4_6
| ~ spl4_8
| ~ spl4_12
| ~ spl4_14
| ~ spl4_22 ),
inference(avatar_split_clause,[],[f62269,f8010,f3865,f3000,f1459,f140,f65,f47,f42,f32,f62578]) ).
fof(f62622,plain,
( complement(converse(converse(sF2))) = converse(complement(converse(sF3)))
| ~ spl4_6
| ~ spl4_74 ),
inference(superposition,[],[f2804,f62580]) ).
fof(f62704,plain,
( complement(converse(converse(sF2))) = complement(converse(converse(sF3)))
| ~ spl4_6
| ~ spl4_74 ),
inference(forward_demodulation,[],[f62622,f2804]) ).
fof(f62765,plain,
( complement(sF3) = complement(converse(converse(sF2)))
| ~ spl4_6
| ~ spl4_74 ),
inference(forward_demodulation,[],[f62704,f10]) ).
fof(f63035,plain,
( complement(sF2) = complement(sF3)
| ~ spl4_6
| ~ spl4_74 ),
inference(forward_demodulation,[],[f62765,f10]) ).
fof(f63102,plain,
( sF2 = join(complement(join(sk1,complement(sF3))),complement(join(complement(sF3),complement(sk1))))
| ~ spl4_6
| ~ spl4_21
| ~ spl4_74 ),
inference(backward_demodulation,[],[f7975,f63035]) ).
fof(f63319,plain,
( sF2 = complement(complement(sF3))
| ~ spl4_6
| ~ spl4_21
| ~ spl4_74 ),
inference(forward_demodulation,[],[f63102,f503]) ).
fof(f63339,plain,
( sF2 = sF3
| ~ spl4_6
| ~ spl4_21
| ~ spl4_74 ),
inference(forward_demodulation,[],[f63319,f466]) ).
fof(f63843,plain,
( $false
| spl4_2
| ~ spl4_6
| ~ spl4_21
| ~ spl4_74 ),
inference(forward_subsumption_resolution,[],[f63339,f39]) ).
fof(f63844,plain,
( spl4_2
| ~ spl4_6
| ~ spl4_21
| ~ spl4_74 ),
inference(avatar_contradiction_clause,[],[f63843]) ).
cnf(s1,plain,
spl4_1,
inference(sat_conversion,[],[f35]) ).
cnf(s2,plain,
~ spl4_2,
inference(sat_conversion,[],[f40]) ).
cnf(s3,plain,
spl4_3,
inference(sat_conversion,[],[f45]) ).
cnf(s4,plain,
spl4_4,
inference(sat_conversion,[],[f50]) ).
cnf(s5,plain,
spl4_5,
inference(sat_conversion,[],[f68]) ).
cnf(s6,plain,
spl4_6,
inference(sat_conversion,[],[f143]) ).
cnf(s8,plain,
( ~ spl4_3
| spl4_8 ),
inference(sat_conversion,[],[f1462]) ).
cnf(s12,plain,
( ~ spl4_6
| spl4_12 ),
inference(sat_conversion,[],[f3003]) ).
cnf(s13,plain,
( ~ spl4_3
| ~ spl4_5
| ~ spl4_6
| spl4_13 ),
inference(sat_conversion,[],[f3169]) ).
cnf(s14,plain,
( ~ spl4_13
| spl4_14 ),
inference(sat_conversion,[],[f3868]) ).
cnf(s21,plain,
( ~ spl4_1
| ~ spl4_6
| spl4_21 ),
inference(sat_conversion,[],[f7947]) ).
cnf(s22,plain,
( ~ spl4_1
| ~ spl4_6
| spl4_22 ),
inference(sat_conversion,[],[f8013]) ).
cnf(s74,plain,
( ~ spl4_1
| ~ spl4_3
| ~ spl4_4
| ~ spl4_5
| ~ spl4_6
| ~ spl4_8
| ~ spl4_12
| ~ spl4_14
| ~ spl4_22
| spl4_74 ),
inference(sat_conversion,[],[f62581]) ).
cnf(s75,plain,
( spl4_2
| ~ spl4_6
| ~ spl4_21
| ~ spl4_74 ),
inference(sat_conversion,[],[f63844]) ).
cnf(s78,plain,
spl4_12,
inference(rat,[],[s12,s6]) ).
cnf(s92,plain,
spl4_13,
inference(rat,[],[s13,s5,s6,s3]) ).
cnf(s93,plain,
spl4_8,
inference(rat,[],[s8,s3]) ).
cnf(s95,plain,
spl4_14,
inference(rat,[],[s14,s92]) ).
cnf(s128,plain,
spl4_22,
inference(rat,[],[s22,s6,s1]) ).
cnf(s129,plain,
spl4_21,
inference(rat,[],[s21,s6,s1]) ).
cnf(s136,plain,
spl4_74,
inference(rat,[],[s74,s1,s93,s95,s78,s3,s6,s5,s4,s128]) ).
cnf(s137,plain,
$false,
inference(rat,[],[s75,s2,s6,s136,s129]) ).
fof(f64056,plain,
$false,
inference(avatar_sat_refutation,[],[s137]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : REL045-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.19/0.46 % Computer : n014.cluster.edu
% 0.19/0.46 % Model : x86_64 x86_64
% 0.19/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.46 % Memory : 8046.5625MB
% 0.19/0.46 % OS : Linux 6.8.0-71-generic
% 0.19/0.46 % CPULimit : 300
% 0.19/0.46 % WCLimit : 300
% 0.19/0.46 % DateTime : Sun Sep 27 22:56:32 UTC 2026
% 0.19/0.46 % CPUTime :
% 0.19/0.46 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.23/0.52 Running first-order theorem proving
% 0.23/0.52 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
% 46.03/7.58 % (1265778)Detected a unit-equality problem, will run specialized UEQ schedule.
% 46.03/7.58 % (1265791)lrs+1002_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal:acc=on:s2agt=16:kmz=on:sac=on:random_seed=143309286:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 46.03/7.58 % (1265796)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=3949690733:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 46.03/7.58 % (1265792)lrs+11_1_ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=535119127:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 46.03/7.58 % (1265793)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=2877280492:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 46.03/7.58 % (1265794)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=144731574:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 46.03/7.58 % (1265795)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=2864030213:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 46.03/7.58 % (1265797)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=304099815:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 46.03/7.58 % (1265794)Instruction limit reached!
% 46.03/7.58 % (1265794)------------------------------
% 46.03/7.58 % (1265794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.03/7.58 % (1265794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.03/7.58 % (1265794)CaDiCaL version: 2.1.3
% 46.03/7.58 % (1265794)Termination reason: Instruction limit
% 46.03/7.58 % (1265794)Termination phase: Saturation
% 46.03/7.58 % (1265794)Time elapsed: 0.142 s
% 46.03/7.58 % (1265794)Peak memory usage: 89 MB
% 46.03/7.58 % (1265794)Instructions burned: 137 (million)
% 46.03/7.58 % (1265795)Instruction limit reached!
% 46.03/7.58 % (1265795)------------------------------
% 46.03/7.58 % (1265795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.03/7.58 % (1265795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.03/7.58 % (1265795)CaDiCaL version: 2.1.3
% 46.03/7.58 % (1265795)Termination reason: Instruction limit
% 46.03/7.58 % (1265795)Termination phase: Saturation
% 46.03/7.58 % (1265795)Time elapsed: 0.180 s
% 46.03/7.58 % (1265795)Peak memory usage: 89 MB
% 46.03/7.58 % (1265795)Instructions burned: 181 (million)
% 46.03/7.58 % (1265796)Instruction limit reached!
% 46.03/7.58 % (1265796)------------------------------
% 46.03/7.58 % (1265796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.03/7.58 % (1265796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.03/7.58 % (1265796)CaDiCaL version: 2.1.3
% 46.03/7.58 % (1265796)Termination reason: Instruction limit
% 46.03/7.58 % (1265796)Termination phase: Saturation
% 46.03/7.58 % (1265796)Time elapsed: 0.268 s
% 46.03/7.58 % (1265796)Peak memory usage: 90 MB
% 46.03/7.58 % (1265796)Instructions burned: 257 (million)
% 46.03/7.58 % (1265808)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2556050074:i=4948:ss=axioms:sgt=16_2995 on theBenchmark for (2995ds/4948Mi)
% 46.03/7.58 % (1265807)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=2574304543:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2996 on theBenchmark for (2996ds/2051Mi)
% 46.03/7.58 % (1265809)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=1527639087:i=215:ep=RSTC_2995 on theBenchmark for (2995ds/215Mi)
% 46.03/7.58 % (1265809)Instruction limit reached!
% 46.03/7.58 % (1265809)------------------------------
% 46.03/7.58 % (1265809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.03/7.58 % (1265809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.03/7.58 % (1265809)CaDiCaL version: 2.1.3
% 46.03/7.58 % (1265809)Termination reason: Instruction limit
% 46.03/7.58 % (1265809)Termination phase: Saturation
% 46.03/7.58 % (1265809)Time elapsed: 0.181 s
% 46.03/7.58 % (1265809)Peak memory usage: 90 MB
% 46.03/7.58 % (1265809)Instructions burned: 215 (million)
% 46.03/7.58 % (1265813)lrs+11_1_sil=16000:tgt=full:fde=none:sp=reverse_frequency:lma=off:fs=off:acc=on:bsr=unit_only:rp=on:random_seed=1270323508:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2991 on theBenchmark for (2991ds/317Mi)
% 46.03/7.58 % (1265797)Instruction limit reached!
% 46.03/7.58 % (1265797)------------------------------
% 46.03/7.58 % (1265797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.03/7.58 % (1265797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.03/7.58 % (1265797)CaDiCaL version: 2.1.3
% 46.03/7.58 % (1265797)Termination reason: Instruction limit
% 46.03/7.58 % (1265797)Termination phase: Saturation
% 46.03/7.58 % (1265797)Time elapsed: 1.125 s
% 46.03/7.58 % (1265797)Peak memory usage: 99 MB
% 46.03/7.58 % (1265797)Instructions burned: 1187 (million)
% 46.03/7.58 % (1265813)Instruction limit reached!
% 46.03/7.58 % (1265813)------------------------------
% 46.03/7.58 % (1265813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.03/7.58 % (1265813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.03/7.58 % (1265813)CaDiCaL version: 2.1.3
% 46.03/7.58 % (1265813)Termination reason: Instruction limit
% 46.03/7.58 % (1265813)Termination phase: Saturation
% 46.03/7.58 % (1265813)Time elapsed: 0.327 s
% 46.03/7.58 % (1265813)Peak memory usage: 93 MB
% 46.03/7.58 % (1265813)Instructions burned: 317 (million)
% 46.03/7.58 % (1265815)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=arity:lcm=predicate:urr=on:s2agt=16:br=off:random_seed=2602652794:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2986 on theBenchmark for (2986ds/12125Mi)
% 46.03/7.58 % (1265816)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=460487883:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2985 on theBenchmark for (2985ds/2836Mi)
% 46.03/7.58 % (1265807)Instruction limit reached!
% 46.03/7.58 % (1265807)------------------------------
% 46.03/7.58 % (1265807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.03/7.58 % (1265807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.03/7.58 % (1265807)CaDiCaL version: 2.1.3
% 46.03/7.58 % (1265807)Termination reason: Instruction limit
% 46.03/7.58 % (1265807)Termination phase: Saturation
% 46.03/7.58 % (1265807)Time elapsed: 2.130 s
% 46.03/7.58 % (1265807)Peak memory usage: 141 MB
% 46.03/7.58 % (1265807)Instructions burned: 2051 (million)
% 46.03/7.58 % (1265823)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1777227484:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2972 on theBenchmark for (2972ds/14534Mi)
% 46.03/7.58 % (1265816)Instruction limit reached!
% 46.03/7.58 % (1265816)------------------------------
% 46.03/7.58 % (1265816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.03/7.58 % (1265816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.03/7.58 % (1265816)CaDiCaL version: 2.1.3
% 46.03/7.58 % (1265816)Termination reason: Instruction limit
% 46.03/7.58 % (1265816)Termination phase: Saturation
% 46.03/7.58 % (1265816)Time elapsed: 3.121 s
% 46.03/7.58 % (1265816)Peak memory usage: 139 MB
% 46.03/7.58 % (1265816)Instructions burned: 2836 (million)
% 46.03/7.58 % (1265831)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=3543676272:i=11832:s2at=3:bs=on:bd=preordered:fsd=on_2951 on theBenchmark for (2951ds/11832Mi)
% 46.03/7.58 % (1265808)Instruction limit reached!
% 46.03/7.58 % (1265808)------------------------------
% 46.03/7.58 % (1265808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.03/7.58 % (1265808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.03/7.58 % (1265808)CaDiCaL version: 2.1.3
% 46.03/7.58 % (1265808)Termination reason: Instruction limit
% 46.03/7.58 % (1265808)Termination phase: Saturation
% 46.03/7.58 % (1265808)Time elapsed: 5.084 s
% 46.03/7.58 % (1265808)Peak memory usage: 164 MB
% 46.03/7.58 % (1265808)Instructions burned: 4949 (million)
% 46.03/7.58 % (1265833)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:drc=off:fde=unused:sp=const_min:spb=goal:fd=preordered:random_seed=3291244776:i=2279:fgj=on:bd=all_2943 on theBenchmark for (2943ds/2279Mi)
% 46.03/7.58 % (1265791)First to succeed.
% 46.03/7.58 % (1265791)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1265778"
% 46.03/7.58 % (1265791)Refutation found. Thanks to Tanya!
% 46.03/7.58 % SZS status Unsatisfiable for theBenchmark
% 46.03/7.58 % SZS output start Proof for theBenchmark
% See solution above
% 46.69/7.71 % (1265791)------------------------------
% 46.69/7.71 % (1265791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.69/7.71 % (1265791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.69/7.71 % (1265791)CaDiCaL version: 2.1.3
% 46.69/7.71 % (1265791)Termination reason: Refutation
% 46.69/7.71 % (1265791)Time elapsed: 6.055 s
% 46.69/7.71 % (1265791)Peak memory usage: 233 MB
% 46.69/7.71 % (1265791)Instructions burned: 10745 (million)
% 46.69/7.71 % (1265791)------------------------------
% 46.69/7.71 % (1265791)------------------------------
% 46.69/7.71 % (1265778)Success in time 6.48 s
% 46.69/7.71 % Vampire exiting
%------------------------------------------------------------------------------