%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : REL022+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:33:49 PM UTC 2026
% Result : Theorem 28.40s 4.96s
% Output : Refutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 63
% Number of leaves : 26
% Syntax : Number of formulae : 329 ( 325 unt; 10 def)
% Number of atoms : 333 ( 332 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 10 ( 6 ~; 0 |; 2 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 15 con; 0-2 aty)
% Number of variables : 324 ( 322 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',maddux1_join_commutativity) ).
fof(f2,axiom,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',maddux2_join_associativity) ).
fof(f3,axiom,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',maddux3_a_kind_of_de_Morgan) ).
fof(f4,axiom,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',maddux4_definiton_of_meet) ).
fof(f5,axiom,
! [X0,X1,X2] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',composition_associativity) ).
fof(f6,axiom,
! [X0] : composition(X0,one) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',composition_identity) ).
fof(f7,axiom,
! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',composition_distributivity) ).
fof(f8,axiom,
! [X0] : converse(converse(X0)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',converse_idempotence) ).
fof(f9,axiom,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',converse_additivity) ).
fof(f10,axiom,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',converse_multiplicativity) ).
fof(f11,axiom,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',converse_cancellativity) ).
fof(f12,axiom,
! [X0] : top = join(X0,complement(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',def_top) ).
fof(f13,axiom,
! [X0] : zero = meet(X0,complement(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',def_zero) ).
fof(f14,axiom,
! [X0,X1,X2] : join(meet(composition(X0,X1),X2),composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2)))) = composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dedekind_law) ).
fof(f15,axiom,
! [X0,X1,X2] : join(meet(composition(X0,X1),X2),meet(composition(X0,meet(X1,composition(converse(X0),X2))),X2)) = meet(composition(X0,meet(X1,composition(converse(X0),X2))),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',modular_law_1) ).
fof(f17,conjecture,
! [X0,X1] :
( composition(X0,top) = X0
=> join(meet(X0,X1),composition(meet(X0,one),X1)) = composition(meet(X0,one),X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f18,negated_conjecture,
~ ! [X0,X1] :
( composition(X0,top) = X0
=> join(meet(X0,X1),composition(meet(X0,one),X1)) = composition(meet(X0,one),X1) ),
inference(negated_conjecture,[status(cth)],[f17]) ).
fof(f19,plain,
? [X0,X1] :
( composition(meet(X0,one),X1) != join(meet(X0,X1),composition(meet(X0,one),X1))
& composition(X0,top) = X0 ),
inference(ennf_transformation,[],[f18]) ).
fof(f20,plain,
( composition(meet(sK0,one),sK1) != join(meet(sK0,sK1),composition(meet(sK0,one),sK1))
& sK0 = composition(sK0,top) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(X1,sK1)],[f19]) ).
fof(f21,plain,
! [X0,X1] : join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f22,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
inference(cnf_transformation,[],[f2]) ).
fof(f23,plain,
! [X0,X1] : join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) = X0,
inference(cnf_transformation,[],[f3]) ).
fof(f24,plain,
! [X0,X1] : complement(join(complement(X0),complement(X1))) = meet(X0,X1),
inference(cnf_transformation,[],[f4]) ).
fof(f25,plain,
! [X2,X0,X1] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
inference(cnf_transformation,[],[f5]) ).
fof(f26,plain,
! [X0] : composition(X0,one) = X0,
inference(cnf_transformation,[],[f6]) ).
fof(f27,plain,
! [X2,X0,X1] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
inference(cnf_transformation,[],[f7]) ).
fof(f28,plain,
! [X0] : converse(converse(X0)) = X0,
inference(cnf_transformation,[],[f8]) ).
fof(f29,plain,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
inference(cnf_transformation,[],[f9]) ).
fof(f30,plain,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
inference(cnf_transformation,[],[f10]) ).
fof(f31,plain,
! [X0,X1] : complement(X1) = join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)),
inference(cnf_transformation,[],[f11]) ).
fof(f32,plain,
! [X0] : top = join(X0,complement(X0)),
inference(cnf_transformation,[],[f12]) ).
fof(f33,plain,
! [X0] : zero = meet(X0,complement(X0)),
inference(cnf_transformation,[],[f13]) ).
fof(f34,plain,
! [X2,X0,X1] : composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2))) = join(meet(composition(X0,X1),X2),composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2)))),
inference(cnf_transformation,[],[f14]) ).
fof(f35,plain,
! [X2,X0,X1] : meet(composition(X0,meet(X1,composition(converse(X0),X2))),X2) = join(meet(composition(X0,X1),X2),meet(composition(X0,meet(X1,composition(converse(X0),X2))),X2)),
inference(cnf_transformation,[],[f15]) ).
fof(f37,plain,
sK0 = composition(sK0,top),
inference(cnf_transformation,[],[f20]) ).
fof(f38,plain,
composition(meet(sK0,one),sK1) != join(meet(sK0,sK1),composition(meet(sK0,one),sK1)),
inference(cnf_transformation,[],[f20]) ).
fof(f39,plain,
! [X0] : zero = complement(join(complement(X0),complement(complement(X0)))),
inference(definition_unfolding,[],[f33,f24]) ).
fof(f40,plain,
! [X2,X0,X1] : composition(complement(join(complement(X0),complement(composition(X2,converse(X1))))),complement(join(complement(X1),complement(composition(converse(X0),X2))))) = join(complement(join(complement(composition(X0,X1)),complement(X2))),composition(complement(join(complement(X0),complement(composition(X2,converse(X1))))),complement(join(complement(X1),complement(composition(converse(X0),X2)))))),
inference(definition_unfolding,[],[f34,f24,f24,f24,f24,f24]) ).
fof(f41,plain,
! [X2,X0,X1] : complement(join(complement(composition(X0,complement(join(complement(X1),complement(composition(converse(X0),X2)))))),complement(X2))) = join(complement(join(complement(composition(X0,X1)),complement(X2))),complement(join(complement(composition(X0,complement(join(complement(X1),complement(composition(converse(X0),X2)))))),complement(X2)))),
inference(definition_unfolding,[],[f35,f24,f24,f24,f24,f24]) ).
fof(f43,plain,
composition(complement(join(complement(sK0),complement(one))),sK1) != join(complement(join(complement(sK0),complement(sK1))),composition(complement(join(complement(sK0),complement(one))),sK1)),
inference(definition_unfolding,[],[f38,f24,f24,f24]) ).
fof(f44,definition,
sF2 = complement(sK0),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f45,plain,
complement(sK0) = sF2,
inference(reorient_equations,[],[f44]) ).
fof(f46,definition,
sF3 = complement(one),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f47,plain,
complement(one) = sF3,
inference(reorient_equations,[],[f46]) ).
fof(f48,definition,
sF4 = join(sF2,sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f49,plain,
join(sF2,sF3) = sF4,
inference(reorient_equations,[],[f48]) ).
fof(f50,definition,
sF5 = complement(sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f51,plain,
complement(sF4) = sF5,
inference(reorient_equations,[],[f50]) ).
fof(f52,definition,
sF6 = composition(sF5,sK1),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f53,plain,
composition(sF5,sK1) = sF6,
inference(reorient_equations,[],[f52]) ).
fof(f54,definition,
sF7 = complement(sK1),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f55,plain,
complement(sK1) = sF7,
inference(reorient_equations,[],[f54]) ).
fof(f56,definition,
sF8 = join(sF2,sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f57,plain,
join(sF2,sF7) = sF8,
inference(reorient_equations,[],[f56]) ).
fof(f58,definition,
sF9 = complement(sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f59,plain,
complement(sF8) = sF9,
inference(reorient_equations,[],[f58]) ).
fof(f60,definition,
sF10 = join(sF9,sF6),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f61,plain,
join(sF9,sF6) = sF10,
inference(reorient_equations,[],[f60]) ).
fof(f62,plain,
sF6 != sF10,
inference(definition_folding,[],[f43,f61,f53,f51,f49,f47,f45,f59,f57,f55,f45,f53,f51,f49,f47,f45]) ).
fof(f63,definition,
sF11 = composition(sK0,top),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f64,plain,
composition(sK0,top) = sF11,
inference(reorient_equations,[],[f63]) ).
fof(f65,plain,
sK0 = sF11,
inference(definition_folding,[],[f37,f64]) ).
fof(f66,plain,
sK0 = composition(sK0,top),
inference(forward_demodulation,[],[f64,f65]) ).
fof(f73,plain,
! [X0,X1] : converse(join(converse(X0),X1)) = join(X0,converse(X1)),
inference(superposition,[],[f29,f28]) ).
fof(f79,plain,
top = join(sK0,sF2),
inference(superposition,[],[f32,f45]) ).
fof(f96,plain,
! [X0,X1] : join(complement(join(complement(X0),complement(X1))),complement(join(complement(X1),X0))) = X1,
inference(superposition,[],[f23,f21]) ).
fof(f97,plain,
! [X0,X1] : join(complement(join(complement(X1),complement(X0))),complement(join(X0,complement(X1)))) = X1,
inference(superposition,[],[f23,f21]) ).
fof(f98,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))) = X0,
inference(superposition,[],[f23,f21]) ).
fof(f104,plain,
! [X0,X1] : converse(composition(X1,converse(X0))) = composition(X0,converse(X1)),
inference(superposition,[],[f30,f28]) ).
fof(f105,plain,
! [X0,X1] : converse(composition(converse(X0),X1)) = composition(converse(X1),X0),
inference(superposition,[],[f30,f28]) ).
fof(f106,plain,
! [X0] : composition(join(sF5,X0),sK1) = join(sF6,composition(X0,sK1)),
inference(superposition,[],[f27,f53]) ).
fof(f107,plain,
! [X0] : composition(join(sK0,X0),top) = join(sK0,composition(X0,top)),
inference(superposition,[],[f27,f66]) ).
fof(f108,plain,
! [X2,X0,X1] : composition(join(converse(X1),X2),converse(X0)) = join(converse(composition(X0,X1)),composition(X2,converse(X0))),
inference(superposition,[],[f27,f30]) ).
fof(f156,plain,
! [X0,X1] : join(complement(join(complement(X1),X0)),complement(join(complement(X0),complement(X1)))) = X1,
inference(superposition,[],[f98,f21]) ).
fof(f163,plain,
! [X2,X0,X1] : composition(join(converse(X2),converse(X1)),converse(X0)) = join(converse(composition(X0,X2)),converse(composition(X0,X1))),
inference(superposition,[],[f108,f30]) ).
fof(f172,plain,
! [X2,X0,X1] : composition(join(converse(X2),converse(X1)),converse(X0)) = converse(join(composition(X0,X2),composition(X0,X1))),
inference(forward_demodulation,[],[f163,f29]) ).
fof(f175,plain,
! [X2,X0,X1] : converse(join(composition(X0,X2),composition(X0,X1))) = composition(converse(join(X2,X1)),converse(X0)),
inference(forward_demodulation,[],[f172,f29]) ).
fof(f177,plain,
! [X2,X0,X1] : converse(join(composition(X0,X2),composition(X0,X1))) = converse(composition(X0,join(X2,X1))),
inference(forward_demodulation,[],[f175,f30]) ).
fof(f266,plain,
! [X2,X0,X1] : join(composition(X0,X1),composition(X0,X2)) = converse(converse(composition(X0,join(X1,X2)))),
inference(superposition,[],[f28,f177]) ).
fof(f277,plain,
! [X2,X0,X1] : composition(X0,join(X1,X2)) = join(composition(X0,X1),composition(X0,X2)),
inference(forward_demodulation,[],[f266,f28]) ).
fof(f291,plain,
! [X0,X1] : composition(X0,join(one,X1)) = join(X0,composition(X0,X1)),
inference(superposition,[],[f277,f26]) ).
fof(f293,plain,
! [X0] : composition(sK0,join(top,X0)) = join(sK0,composition(sK0,X0)),
inference(superposition,[],[f277,f66]) ).
fof(f297,plain,
! [X0] : composition(sK0,join(X0,top)) = join(composition(sK0,X0),sK0),
inference(superposition,[],[f277,f66]) ).
fof(f304,plain,
! [X2,X0,X1] : join(composition(X0,X2),composition(X0,X1)) = composition(X0,join(X1,X2)),
inference(superposition,[],[f21,f277]) ).
fof(f305,plain,
! [X2,X0,X1] : composition(X0,join(X2,X1)) = composition(X0,join(X1,X2)),
inference(forward_demodulation,[],[f304,f277]) ).
fof(f309,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(top,X1),
inference(superposition,[],[f22,f32]) ).
fof(f313,plain,
! [X2,X0,X1] : join(X0,X2) = join(complement(join(complement(X0),complement(X1))),join(complement(join(complement(X0),X1)),X2)),
inference(superposition,[],[f22,f23]) ).
fof(f322,plain,
! [X0] : join(sF2,join(sF7,X0)) = join(sF8,X0),
inference(superposition,[],[f22,f57]) ).
fof(f331,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f21,f22]) ).
fof(f391,plain,
zero = complement(top),
inference(superposition,[],[f39,f32]) ).
fof(f583,plain,
! [X0] : converse(converse(X0)) = composition(converse(one),X0),
inference(superposition,[],[f105,f26]) ).
fof(f597,plain,
! [X0] : composition(converse(one),X0) = X0,
inference(forward_demodulation,[],[f583,f28]) ).
fof(f611,plain,
! [X0,X1] : composition(join(converse(one),X1),X0) = join(X0,composition(X1,X0)),
inference(superposition,[],[f27,f597]) ).
fof(f619,plain,
one = converse(one),
inference(superposition,[],[f26,f597]) ).
fof(f627,plain,
! [X0,X1] : join(X0,composition(X1,X0)) = composition(join(one,X1),X0),
inference(forward_demodulation,[],[f611,f619]) ).
fof(f634,plain,
! [X0] : composition(one,X0) = X0,
inference(superposition,[],[f597,f619]) ).
fof(f650,plain,
! [X0] : complement(X0) = join(composition(converse(one),complement(X0)),complement(X0)),
inference(superposition,[],[f31,f634]) ).
fof(f663,plain,
! [X0] : complement(X0) = join(complement(X0),complement(X0)),
inference(forward_demodulation,[],[f650,f597]) ).
fof(f683,plain,
! [X0,X1] : join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) = join(X0,complement(join(complement(X0),X1))),
inference(superposition,[],[f313,f663]) ).
fof(f687,plain,
! [X0,X1] : join(complement(X0),X1) = join(complement(X0),join(complement(X0),X1)),
inference(superposition,[],[f22,f663]) ).
fof(f690,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),X1))) = X0,
inference(forward_demodulation,[],[f683,f23]) ).
fof(f710,plain,
! [X0] : join(X0,complement(complement(X0))) = X0,
inference(superposition,[],[f690,f690]) ).
fof(f715,plain,
! [X0] : join(X0,zero) = X0,
inference(superposition,[],[f690,f39]) ).
fof(f719,plain,
! [X2,X0,X1] : join(X1,X0) = join(complement(join(complement(X0),X2)),join(X1,X0)),
inference(superposition,[],[f331,f690]) ).
fof(f810,plain,
! [X0] : join(zero,X0) = X0,
inference(superposition,[],[f21,f715]) ).
fof(f858,plain,
! [X0,X1] : join(X1,X0) = join(complement(complement(X0)),join(X1,X0)),
inference(superposition,[],[f331,f710]) ).
fof(f861,plain,
! [X0,X1] : join(X0,X1) = join(complement(complement(X0)),join(complement(join(complement(X0),complement(complement(X0)))),X1)),
inference(superposition,[],[f313,f710]) ).
fof(f879,plain,
! [X0,X1] : join(X0,X1) = join(complement(complement(X0)),join(zero,X1)),
inference(forward_demodulation,[],[f861,f39]) ).
fof(f884,plain,
! [X0,X1] : join(X0,X1) = join(complement(complement(X0)),X1),
inference(forward_demodulation,[],[f879,f810]) ).
fof(f888,plain,
! [X0] : join(one,X0) = join(complement(sF3),X0),
inference(superposition,[],[f884,f47]) ).
fof(f889,plain,
! [X0] : join(top,X0) = join(complement(zero),X0),
inference(superposition,[],[f884,f391]) ).
fof(f890,plain,
! [X0] : join(sK0,X0) = join(complement(sF2),X0),
inference(superposition,[],[f884,f45]) ).
fof(f892,plain,
! [X0] : join(sF4,X0) = join(complement(sF5),X0),
inference(superposition,[],[f884,f51]) ).
fof(f911,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X0,X1))),
inference(superposition,[],[f690,f884]) ).
fof(f920,plain,
! [X0,X1] : join(X0,X1) = join(X1,complement(complement(X0))),
inference(superposition,[],[f21,f884]) ).
fof(f929,plain,
! [X0] : complement(complement(X0)) = join(X0,zero),
inference(superposition,[],[f715,f884]) ).
fof(f930,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_demodulation,[],[f929,f715]) ).
fof(f956,plain,
one = complement(sF3),
inference(superposition,[],[f930,f47]) ).
fof(f957,plain,
top = complement(zero),
inference(superposition,[],[f930,f391]) ).
fof(f958,plain,
sK0 = complement(sF2),
inference(superposition,[],[f930,f45]) ).
fof(f960,plain,
sF4 = complement(sF5),
inference(superposition,[],[f930,f51]) ).
fof(f961,plain,
sF8 = complement(sF9),
inference(superposition,[],[f930,f59]) ).
fof(f967,plain,
! [X0] : top = join(complement(X0),X0),
inference(superposition,[],[f32,f930]) ).
fof(f970,plain,
! [X0,X1] : complement(X0) = join(complement(join(complement(X1),X0)),complement(join(X0,X1))),
inference(superposition,[],[f96,f930]) ).
fof(f1061,plain,
! [X0] : zero = join(zero,complement(join(top,X0))),
inference(superposition,[],[f911,f391]) ).
fof(f1069,plain,
! [X0,X1] : complement(X1) = join(complement(X1),complement(join(X0,X1))),
inference(superposition,[],[f911,f21]) ).
fof(f1092,plain,
complement(sF2) = join(complement(sF2),complement(sF4)),
inference(superposition,[],[f911,f49]) ).
fof(f1127,plain,
complement(sF2) = join(sK0,complement(sF4)),
inference(forward_demodulation,[],[f1092,f890]) ).
fof(f1137,plain,
! [X0] : zero = complement(join(top,X0)),
inference(forward_demodulation,[],[f1061,f810]) ).
fof(f1143,plain,
complement(sF2) = join(sK0,sF5),
inference(forward_demodulation,[],[f1127,f51]) ).
fof(f1152,plain,
sK0 = join(sK0,sF5),
inference(forward_demodulation,[],[f1143,f958]) ).
fof(f1179,plain,
sK0 = join(sF5,sK0),
inference(superposition,[],[f21,f1152]) ).
fof(f1189,plain,
complement(sF5) = join(complement(sF5),complement(sK0)),
inference(superposition,[],[f911,f1179]) ).
fof(f1194,plain,
complement(sF5) = join(sF4,complement(sK0)),
inference(forward_demodulation,[],[f1189,f892]) ).
fof(f1195,plain,
complement(sF5) = join(sF4,sF2),
inference(forward_demodulation,[],[f1194,f45]) ).
fof(f1196,plain,
sF4 = join(sF4,sF2),
inference(forward_demodulation,[],[f1195,f960]) ).
fof(f1215,plain,
! [X0] : complement(zero) = join(complement(zero),complement(X0)),
inference(superposition,[],[f1069,f715]) ).
fof(f1234,plain,
complement(sF3) = join(complement(sF3),complement(sF4)),
inference(superposition,[],[f1069,f49]) ).
fof(f1271,plain,
complement(sF3) = join(one,complement(sF4)),
inference(forward_demodulation,[],[f1234,f888]) ).
fof(f1281,plain,
! [X0] : complement(zero) = join(top,complement(X0)),
inference(forward_demodulation,[],[f1215,f889]) ).
fof(f1289,plain,
complement(sF3) = join(one,sF5),
inference(forward_demodulation,[],[f1271,f51]) ).
fof(f1299,plain,
! [X0] : top = join(top,complement(X0)),
inference(forward_demodulation,[],[f1281,f957]) ).
fof(f1304,plain,
one = join(one,sF5),
inference(forward_demodulation,[],[f1289,f956]) ).
fof(f1432,plain,
! [X0] : top = join(top,X0),
inference(superposition,[],[f1299,f930]) ).
fof(f1529,plain,
! [X0,X1] : composition(X0,one) = join(X0,composition(X0,complement(join(complement(one),X1)))),
inference(superposition,[],[f291,f690]) ).
fof(f1597,plain,
! [X0,X1] : composition(X0,one) = join(X0,composition(X0,complement(join(sF3,X1)))),
inference(forward_demodulation,[],[f1529,f47]) ).
fof(f1611,plain,
! [X0,X1] : join(X0,composition(X0,complement(join(sF3,X1)))) = X0,
inference(forward_demodulation,[],[f1597,f26]) ).
fof(f1663,plain,
! [X0,X1] : join(complement(join(complement(join(complement(complement(X1)),X0)),complement(X1))),complement(join(top,X0))) = X1,
inference(superposition,[],[f96,f309]) ).
fof(f1678,plain,
! [X0,X1] : join(complement(join(complement(join(complement(complement(X1)),X0)),complement(X1))),zero) = X1,
inference(forward_demodulation,[],[f1663,f1137]) ).
fof(f1727,plain,
! [X0,X1] : complement(join(complement(join(complement(complement(X1)),X0)),complement(X1))) = X1,
inference(forward_demodulation,[],[f1678,f715]) ).
fof(f1741,plain,
! [X0,X1] : complement(join(complement(join(X1,X0)),complement(X1))) = X1,
inference(forward_demodulation,[],[f1727,f884]) ).
fof(f1782,plain,
! [X0,X1] : complement(join(complement(complement(X1)),X0)) = join(complement(join(top,X0)),complement(join(join(complement(complement(X1)),X0),X1))),
inference(superposition,[],[f970,f309]) ).
fof(f1793,plain,
! [X0,X1] : complement(X1) = join(complement(join(complement(X0),X1)),complement(join(X0,X1))),
inference(superposition,[],[f970,f21]) ).
fof(f1842,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(complement(X0)),complement(join(complement(join(complement(X1),X0)),join(X0,X1)))),
inference(superposition,[],[f23,f970]) ).
fof(f1849,plain,
! [X0,X1] : join(X0,X1) = join(complement(join(complement(join(X0,X1)),complement(complement(join(complement(X1),X0))))),complement(complement(X0))),
inference(superposition,[],[f97,f970]) ).
fof(f1860,plain,
! [X0,X1] : join(X0,X1) = join(X0,complement(join(complement(join(X0,X1)),complement(complement(join(complement(X1),X0)))))),
inference(forward_demodulation,[],[f1849,f920]) ).
fof(f1867,plain,
! [X0,X1] : join(complement(X1),X0) = join(X0,complement(join(complement(join(complement(X1),X0)),join(X0,X1)))),
inference(forward_demodulation,[],[f1842,f884]) ).
fof(f1907,plain,
! [X0,X1] : complement(join(complement(complement(X1)),X0)) = join(complement(join(top,X0)),complement(join(complement(complement(X1)),join(X0,X1)))),
inference(forward_demodulation,[],[f1782,f22]) ).
fof(f1922,plain,
! [X0,X1] : join(X0,X1) = join(X0,complement(join(join(complement(X1),X0),complement(join(X0,X1))))),
inference(forward_demodulation,[],[f1860,f920]) ).
fof(f1929,plain,
! [X0,X1] : join(complement(X1),X0) = join(X0,complement(join(X0,X1))),
inference(forward_demodulation,[],[f1867,f719]) ).
fof(f1955,plain,
! [X0,X1] : complement(join(complement(complement(X1)),X0)) = join(complement(join(top,X0)),complement(join(X0,X1))),
inference(forward_demodulation,[],[f1907,f858]) ).
fof(f1963,plain,
! [X0,X1] : join(X0,X1) = join(X0,complement(join(complement(X1),join(X0,complement(join(X0,X1)))))),
inference(forward_demodulation,[],[f1922,f22]) ).
fof(f1979,plain,
! [X0,X1] : complement(join(complement(complement(X1)),X0)) = join(zero,complement(join(X0,X1))),
inference(forward_demodulation,[],[f1955,f1137]) ).
fof(f1983,plain,
! [X0,X1] : join(X0,X1) = join(X0,complement(join(complement(X1),join(complement(X1),X0)))),
inference(forward_demodulation,[],[f1963,f1929]) ).
fof(f1990,plain,
! [X0,X1] : complement(join(X0,X1)) = complement(join(complement(complement(X1)),X0)),
inference(forward_demodulation,[],[f1979,f810]) ).
fof(f1991,plain,
! [X0,X1] : join(X0,X1) = join(X0,complement(join(complement(X1),X0))),
inference(forward_demodulation,[],[f1983,f687]) ).
fof(f1994,plain,
! [X0,X1] : complement(join(X0,X1)) = complement(join(X1,X0)),
inference(forward_demodulation,[],[f1990,f884]) ).
fof(f1997,plain,
! [X0,X1] : join(complement(X0),X1) = join(X1,complement(join(X0,X1))),
inference(superposition,[],[f1929,f21]) ).
fof(f2000,plain,
! [X0,X1] : join(X1,complement(join(top,X0))) = join(complement(join(complement(X1),X0)),X1),
inference(superposition,[],[f1929,f309]) ).
fof(f2011,plain,
! [X0,X1] : join(complement(complement(join(complement(X0),complement(X1)))),complement(join(complement(X0),X1))) = join(complement(join(complement(X0),X1)),complement(X0)),
inference(superposition,[],[f1929,f98]) ).
fof(f2030,plain,
join(complement(sF3),sF2) = join(sF2,complement(sF4)),
inference(superposition,[],[f1929,f49]) ).
fof(f2032,plain,
join(complement(sF6),sF9) = join(sF9,complement(sF10)),
inference(superposition,[],[f1929,f61]) ).
fof(f2090,plain,
join(complement(sF3),sF2) = join(sF2,sF5),
inference(forward_demodulation,[],[f2030,f51]) ).
fof(f2102,plain,
! [X0,X1] : join(join(complement(X0),complement(X1)),complement(join(complement(X0),X1))) = join(complement(join(complement(X0),X1)),complement(X0)),
inference(forward_demodulation,[],[f2011,f884]) ).
fof(f2111,plain,
! [X0,X1] : join(X1,zero) = join(complement(join(complement(X1),X0)),X1),
inference(forward_demodulation,[],[f2000,f1137]) ).
fof(f2125,plain,
join(sF2,sF5) = join(one,sF2),
inference(forward_demodulation,[],[f2090,f888]) ).
fof(f2137,plain,
! [X0,X1] : join(complement(X0),join(complement(X1),complement(join(complement(X0),X1)))) = join(complement(join(complement(X0),X1)),complement(X0)),
inference(forward_demodulation,[],[f2102,f22]) ).
fof(f2144,plain,
! [X0,X1] : join(complement(join(complement(X1),X0)),X1) = X1,
inference(forward_demodulation,[],[f2111,f715]) ).
fof(f2159,plain,
! [X0,X1] : join(complement(X0),complement(X1)) = join(complement(join(complement(X0),X1)),complement(X0)),
inference(forward_demodulation,[],[f2137,f1069]) ).
fof(f2191,plain,
! [X0,X1] : join(complement(complement(join(complement(X0),complement(X1)))),complement(join(X1,complement(X0)))) = join(complement(join(X1,complement(X0))),complement(X0)),
inference(superposition,[],[f1997,f97]) ).
fof(f2208,plain,
join(complement(sF2),sF3) = join(sF3,complement(sF4)),
inference(superposition,[],[f1997,f49]) ).
fof(f2276,plain,
join(complement(sF2),sF3) = join(sF3,sF5),
inference(forward_demodulation,[],[f2208,f51]) ).
fof(f2282,plain,
! [X0,X1] : join(complement(join(X1,complement(X0))),complement(X0)) = join(join(complement(X0),complement(X1)),complement(join(X1,complement(X0)))),
inference(forward_demodulation,[],[f2191,f884]) ).
fof(f2309,plain,
join(sF3,sF5) = join(sK0,sF3),
inference(forward_demodulation,[],[f2276,f890]) ).
fof(f2313,plain,
! [X0,X1] : join(complement(join(X1,complement(X0))),complement(X0)) = join(complement(X0),join(complement(X1),complement(join(X1,complement(X0))))),
inference(forward_demodulation,[],[f2282,f22]) ).
fof(f2333,plain,
! [X0,X1] : join(complement(X0),complement(X1)) = join(complement(join(X1,complement(X0))),complement(X0)),
inference(forward_demodulation,[],[f2313,f911]) ).
fof(f2401,plain,
! [X0,X1] : join(complement(join(complement(complement(X0)),X1)),X0) = join(complement(join(complement(complement(X0)),X1)),complement(complement(X0))),
inference(superposition,[],[f1991,f690]) ).
fof(f2490,plain,
! [X0,X1] : join(complement(join(complement(complement(X0)),X1)),X0) = join(complement(complement(X0)),complement(X1)),
inference(forward_demodulation,[],[f2401,f2159]) ).
fof(f2545,plain,
! [X0,X1] : join(X0,complement(X1)) = join(complement(join(complement(complement(X0)),X1)),X0),
inference(forward_demodulation,[],[f2490,f884]) ).
fof(f2583,plain,
! [X0,X1] : join(X0,complement(X1)) = join(complement(join(X0,X1)),X0),
inference(forward_demodulation,[],[f2545,f884]) ).
fof(f2691,plain,
! [X0,X1] : complement(X0) = join(complement(join(X0,X1)),complement(X0)),
inference(superposition,[],[f2144,f884]) ).
fof(f2743,plain,
! [X0] : composition(sK0,top) = join(composition(sK0,complement(join(complement(top),X0))),sK0),
inference(superposition,[],[f297,f2144]) ).
fof(f2746,plain,
! [X0] : composition(sK0,top) = join(composition(sK0,complement(join(zero,X0))),sK0),
inference(forward_demodulation,[],[f2743,f391]) ).
fof(f2774,plain,
! [X0] : composition(sK0,top) = join(composition(sK0,complement(X0)),sK0),
inference(forward_demodulation,[],[f2746,f810]) ).
fof(f2789,plain,
! [X0] : sK0 = join(composition(sK0,complement(X0)),sK0),
inference(forward_demodulation,[],[f2774,f66]) ).
fof(f2817,plain,
join(sF2,sF5) = join(sF2,one),
inference(superposition,[],[f21,f2125]) ).
fof(f2825,plain,
join(complement(one),sF2) = join(sF2,complement(join(sF2,sF5))),
inference(superposition,[],[f1997,f2125]) ).
fof(f2826,plain,
join(complement(one),sF2) = join(complement(sF5),sF2),
inference(forward_demodulation,[],[f2825,f1929]) ).
fof(f2831,plain,
join(sF4,sF2) = join(complement(one),sF2),
inference(forward_demodulation,[],[f2826,f892]) ).
fof(f2833,plain,
join(sF3,sF2) = join(sF4,sF2),
inference(forward_demodulation,[],[f2831,f47]) ).
fof(f2834,plain,
sF4 = join(sF3,sF2),
inference(forward_demodulation,[],[f2833,f1196]) ).
fof(f3120,plain,
! [X0,X1] : join(X1,complement(X0)) = join(complement(join(X0,X1)),X1),
inference(superposition,[],[f2583,f1994]) ).
fof(f3379,plain,
complement(sF3) = join(complement(join(complement(sF2),sF3)),complement(sF4)),
inference(superposition,[],[f970,f2834]) ).
fof(f3390,plain,
complement(sF3) = join(complement(join(complement(sF2),sF3)),sF5),
inference(forward_demodulation,[],[f3379,f51]) ).
fof(f3397,plain,
complement(sF3) = join(complement(join(sK0,sF3)),sF5),
inference(forward_demodulation,[],[f3390,f890]) ).
fof(f3401,plain,
complement(sF3) = join(complement(join(sF3,sF5)),sF5),
inference(forward_demodulation,[],[f3397,f2309]) ).
fof(f3403,plain,
complement(sF3) = join(sF5,complement(sF3)),
inference(forward_demodulation,[],[f3401,f3120]) ).
fof(f3404,plain,
one = join(sF5,one),
inference(forward_demodulation,[],[f3403,f956]) ).
fof(f3529,plain,
complement(sF5) = join(complement(join(complement(sK0),sF5)),complement(sK0)),
inference(superposition,[],[f1793,f1152]) ).
fof(f3623,plain,
complement(sF5) = join(complement(sK0),complement(sF5)),
inference(forward_demodulation,[],[f3529,f2159]) ).
fof(f3710,plain,
sF4 = join(complement(sK0),sF4),
inference(forward_demodulation,[],[f3623,f960]) ).
fof(f3779,plain,
sF4 = join(sF2,sF4),
inference(forward_demodulation,[],[f3710,f45]) ).
fof(f4110,plain,
! [X0] : composition(one,X0) = join(X0,composition(sF5,X0)),
inference(superposition,[],[f627,f1304]) ).
fof(f4131,plain,
! [X0] : join(X0,composition(sF5,X0)) = X0,
inference(forward_demodulation,[],[f4110,f634]) ).
fof(f4152,plain,
! [X0,X1] : join(X1,X0) = join(X0,join(composition(sF5,X0),X1)),
inference(superposition,[],[f331,f4131]) ).
fof(f4156,plain,
! [X0] : complement(composition(sF5,X0)) = join(complement(composition(sF5,X0)),complement(X0)),
inference(superposition,[],[f1069,f4131]) ).
fof(f4160,plain,
! [X0] : join(complement(X0),X0) = join(X0,complement(composition(sF5,X0))),
inference(superposition,[],[f2583,f4131]) ).
fof(f4194,plain,
! [X0] : top = join(X0,complement(composition(sF5,X0))),
inference(forward_demodulation,[],[f4160,f967]) ).
fof(f5364,plain,
! [X0] : converse(top) = join(X0,converse(complement(converse(X0)))),
inference(superposition,[],[f73,f32]) ).
fof(f5425,plain,
composition(sK0,top) = join(sK0,composition(sF5,top)),
inference(superposition,[],[f107,f1152]) ).
fof(f5481,plain,
sK0 = join(sK0,composition(sF5,top)),
inference(forward_demodulation,[],[f5425,f66]) ).
fof(f5582,plain,
! [X0,X1] : composition(complement(join(complement(X0),complement(composition(X1,converse(one))))),complement(join(sF3,complement(composition(converse(X0),X1))))) = join(complement(join(complement(composition(X0,one)),complement(X1))),composition(complement(join(complement(X0),complement(composition(X1,converse(one))))),complement(join(sF3,complement(composition(converse(X0),X1)))))),
inference(superposition,[],[f40,f47]) ).
fof(f5656,plain,
! [X0,X1] : composition(complement(join(complement(X0),complement(composition(X1,one)))),complement(join(sF3,complement(composition(converse(X0),X1))))) = join(complement(join(complement(composition(X0,one)),complement(X1))),composition(complement(join(complement(X0),complement(composition(X1,one)))),complement(join(sF3,complement(composition(converse(X0),X1)))))),
inference(forward_demodulation,[],[f5582,f619]) ).
fof(f5706,plain,
! [X0,X1] : composition(complement(join(complement(X0),complement(X1))),complement(join(sF3,complement(composition(converse(X0),X1))))) = join(complement(join(complement(composition(X0,one)),complement(X1))),composition(complement(join(complement(X0),complement(X1))),complement(join(sF3,complement(composition(converse(X0),X1)))))),
inference(forward_demodulation,[],[f5656,f26]) ).
fof(f5740,plain,
! [X0,X1] : composition(complement(join(complement(X0),complement(X1))),complement(join(sF3,complement(composition(converse(X0),X1))))) = join(complement(join(complement(X0),complement(X1))),composition(complement(join(complement(X0),complement(X1))),complement(join(sF3,complement(composition(converse(X0),X1)))))),
inference(forward_demodulation,[],[f5706,f26]) ).
fof(f5760,plain,
! [X0,X1] : complement(join(complement(X0),complement(X1))) = composition(complement(join(complement(X0),complement(X1))),complement(join(sF3,complement(composition(converse(X0),X1))))),
inference(forward_demodulation,[],[f5740,f1611]) ).
fof(f5777,plain,
! [X0] : sK0 = join(composition(sK0,X0),sK0),
inference(superposition,[],[f2789,f930]) ).
fof(f7266,plain,
composition(one,sK1) = join(sF6,composition(one,sK1)),
inference(superposition,[],[f106,f3404]) ).
fof(f7333,plain,
sK1 = join(sF6,sK1),
inference(forward_demodulation,[],[f7266,f634]) ).
fof(f7353,plain,
complement(sF6) = join(complement(join(complement(sK1),sF6)),complement(sK1)),
inference(superposition,[],[f970,f7333]) ).
fof(f7361,plain,
complement(sF6) = join(complement(sK1),complement(sF6)),
inference(forward_demodulation,[],[f7353,f2159]) ).
fof(f7365,plain,
complement(sF6) = join(sF7,complement(sF6)),
inference(forward_demodulation,[],[f7361,f55]) ).
fof(f7408,plain,
! [X0,X1] : join(composition(sF5,X1),X0) = join(X0,composition(sF5,join(X0,X1))),
inference(superposition,[],[f4152,f277]) ).
fof(f8354,plain,
complement(sF9) = join(complement(sF10),complement(sF9)),
inference(superposition,[],[f2691,f61]) ).
fof(f8461,plain,
sF8 = join(complement(sF10),sF8),
inference(forward_demodulation,[],[f8354,f961]) ).
fof(f10009,plain,
join(sF8,complement(sF6)) = join(sF2,complement(sF6)),
inference(superposition,[],[f322,f7365]) ).
fof(f14187,plain,
! [X0] : composition(sK0,join(top,X0)) = join(composition(sK0,X0),sK0),
inference(superposition,[],[f297,f305]) ).
fof(f14197,plain,
! [X0] : sK0 = composition(sK0,join(top,X0)),
inference(forward_demodulation,[],[f14187,f5777]) ).
fof(f14265,plain,
! [X0] : sK0 = join(sK0,composition(sK0,X0)),
inference(forward_demodulation,[],[f14197,f293]) ).
fof(f17604,plain,
! [X0] : complement(join(top,X0)) = join(composition(converse(sK0),complement(join(sK0,composition(sK0,X0)))),complement(join(top,X0))),
inference(superposition,[],[f31,f293]) ).
fof(f17629,plain,
! [X0] : zero = join(composition(converse(sK0),complement(join(sK0,composition(sK0,X0)))),zero),
inference(forward_demodulation,[],[f17604,f1137]) ).
fof(f17678,plain,
! [X0] : zero = composition(converse(sK0),complement(join(sK0,composition(sK0,X0)))),
inference(forward_demodulation,[],[f17629,f715]) ).
fof(f17707,plain,
zero = composition(converse(sK0),complement(sK0)),
inference(forward_demodulation,[],[f17678,f14265]) ).
fof(f17720,plain,
zero = composition(converse(sK0),sF2),
inference(forward_demodulation,[],[f17707,f45]) ).
fof(f17745,plain,
! [X0] : composition(converse(sK0),join(sF2,X0)) = join(zero,composition(converse(sK0),X0)),
inference(superposition,[],[f277,f17720]) ).
fof(f17747,plain,
composition(converse(sK0),join(one,sF2)) = join(converse(sK0),zero),
inference(superposition,[],[f291,f17720]) ).
fof(f17756,plain,
converse(sK0) = composition(converse(sK0),join(one,sF2)),
inference(forward_demodulation,[],[f17747,f715]) ).
fof(f17758,plain,
! [X0] : composition(converse(sK0),X0) = composition(converse(sK0),join(sF2,X0)),
inference(forward_demodulation,[],[f17745,f810]) ).
fof(f17771,plain,
converse(sK0) = composition(converse(sK0),join(sF2,sF5)),
inference(forward_demodulation,[],[f17756,f2125]) ).
fof(f17781,plain,
converse(sK0) = composition(converse(sK0),sF5),
inference(forward_demodulation,[],[f17771,f17758]) ).
fof(f23756,plain,
join(sK0,composition(sF5,top)) = join(composition(sF5,sF2),sK0),
inference(superposition,[],[f7408,f79]) ).
fof(f23767,plain,
sK0 = join(composition(sF5,sF2),sK0),
inference(forward_demodulation,[],[f23756,f5481]) ).
fof(f23826,plain,
composition(sF5,sF2) = complement(join(complement(sK0),complement(composition(sF5,sF2)))),
inference(superposition,[],[f1741,f23767]) ).
fof(f23863,plain,
composition(sF5,sF2) = complement(join(sF2,complement(composition(sF5,sF2)))),
inference(forward_demodulation,[],[f23826,f45]) ).
fof(f23879,plain,
complement(top) = composition(sF5,sF2),
inference(forward_demodulation,[],[f23863,f4194]) ).
fof(f23888,plain,
zero = composition(sF5,sF2),
inference(forward_demodulation,[],[f23879,f391]) ).
fof(f23906,plain,
! [X0] : join(zero,composition(sF5,X0)) = composition(sF5,join(sF2,X0)),
inference(superposition,[],[f277,f23888]) ).
fof(f23907,plain,
! [X0] : join(composition(sF5,X0),zero) = composition(sF5,join(X0,sF2)),
inference(superposition,[],[f277,f23888]) ).
fof(f23914,plain,
! [X0] : composition(sF5,X0) = composition(sF5,join(X0,sF2)),
inference(forward_demodulation,[],[f23907,f715]) ).
fof(f23915,plain,
! [X0] : composition(sF5,X0) = composition(sF5,join(sF2,X0)),
inference(forward_demodulation,[],[f23906,f810]) ).
fof(f24343,plain,
composition(sF5,one) = composition(sF5,join(sF2,sF5)),
inference(superposition,[],[f23915,f2817]) ).
fof(f24360,plain,
! [X0] : composition(sF5,join(complement(X0),sF2)) = composition(sF5,complement(join(sF2,X0))),
inference(superposition,[],[f23915,f1929]) ).
fof(f24438,plain,
! [X0] : composition(sF5,complement(X0)) = composition(sF5,complement(join(sF2,X0))),
inference(forward_demodulation,[],[f24360,f23914]) ).
fof(f24448,plain,
composition(sF5,one) = composition(sF5,sF5),
inference(forward_demodulation,[],[f24343,f23915]) ).
fof(f24473,plain,
sF5 = composition(sF5,sF5),
inference(forward_demodulation,[],[f24448,f26]) ).
fof(f24485,plain,
! [X0] : composition(sF5,X0) = composition(sF5,composition(sF5,X0)),
inference(superposition,[],[f25,f24473]) ).
fof(f24805,plain,
composition(converse(sF5),sK0) = converse(converse(sK0)),
inference(superposition,[],[f105,f17781]) ).
fof(f24836,plain,
sK0 = composition(converse(sF5),sK0),
inference(forward_demodulation,[],[f24805,f28]) ).
fof(f27025,plain,
join(complement(sF8),complement(sF6)) = join(complement(sF6),complement(join(sF2,complement(sF6)))),
inference(superposition,[],[f1997,f10009]) ).
fof(f27029,plain,
join(complement(sF6),complement(sF8)) = join(complement(join(sF2,complement(sF6))),complement(sF6)),
inference(superposition,[],[f3120,f10009]) ).
fof(f27038,plain,
join(complement(sF6),complement(sF8)) = join(complement(sF6),complement(sF2)),
inference(forward_demodulation,[],[f27029,f2333]) ).
fof(f27042,plain,
join(complement(sF8),complement(sF6)) = join(complement(sF2),complement(sF6)),
inference(forward_demodulation,[],[f27025,f1997]) ).
fof(f27056,plain,
join(complement(sF6),complement(sF8)) = join(complement(sF6),sK0),
inference(forward_demodulation,[],[f27038,f958]) ).
fof(f27058,plain,
join(complement(sF8),complement(sF6)) = join(sK0,complement(sF6)),
inference(forward_demodulation,[],[f27042,f890]) ).
fof(f27066,plain,
join(complement(sF6),sF9) = join(complement(sF6),sK0),
inference(forward_demodulation,[],[f27056,f59]) ).
fof(f27067,plain,
join(sF9,complement(sF6)) = join(sK0,complement(sF6)),
inference(forward_demodulation,[],[f27058,f59]) ).
fof(f27069,plain,
join(sF9,complement(sF10)) = join(complement(sF6),sK0),
inference(forward_demodulation,[],[f27066,f2032]) ).
fof(f27089,plain,
join(sF9,complement(sF10)) = join(sK0,complement(sF6)),
inference(superposition,[],[f21,f27069]) ).
fof(f27152,plain,
join(sF9,complement(sF10)) = join(sF9,complement(sF6)),
inference(forward_demodulation,[],[f27089,f27067]) ).
fof(f27200,plain,
sF10 = join(complement(join(complement(sF10),complement(sF9))),complement(join(sF9,complement(sF6)))),
inference(superposition,[],[f97,f27152]) ).
fof(f27244,plain,
sF10 = join(complement(join(complement(sF10),sF8)),complement(join(sF9,complement(sF6)))),
inference(forward_demodulation,[],[f27200,f961]) ).
fof(f27259,plain,
sF10 = join(complement(sF8),complement(join(sF9,complement(sF6)))),
inference(forward_demodulation,[],[f27244,f8461]) ).
fof(f27267,plain,
sF10 = join(sF9,complement(join(sF9,complement(sF6)))),
inference(forward_demodulation,[],[f27259,f59]) ).
fof(f27271,plain,
sF10 = join(complement(complement(sF6)),sF9),
inference(forward_demodulation,[],[f27267,f1929]) ).
fof(f27275,plain,
sF10 = join(sF6,sF9),
inference(forward_demodulation,[],[f27271,f884]) ).
fof(f27780,plain,
! [X0] : join(X0,complement(converse(complement(converse(X0))))) = join(complement(converse(top)),X0),
inference(superposition,[],[f2583,f5364]) ).
fof(f27819,plain,
top = converse(top),
inference(superposition,[],[f1432,f5364]) ).
fof(f27867,plain,
! [X0] : join(complement(top),X0) = join(X0,complement(converse(complement(converse(X0))))),
inference(forward_demodulation,[],[f27780,f27819]) ).
fof(f27926,plain,
! [X0] : join(zero,X0) = join(X0,complement(converse(complement(converse(X0))))),
inference(forward_demodulation,[],[f27867,f391]) ).
fof(f27961,plain,
! [X0] : join(X0,complement(converse(complement(converse(X0))))) = X0,
inference(forward_demodulation,[],[f27926,f810]) ).
fof(f28065,plain,
! [X0] : converse(complement(converse(complement(X0)))) = join(complement(join(complement(converse(complement(converse(complement(X0))))),X0)),complement(complement(X0))),
inference(superposition,[],[f156,f27961]) ).
fof(f28097,plain,
! [X0] : converse(converse(X0)) = join(X0,converse(complement(converse(complement(converse(converse(X0))))))),
inference(superposition,[],[f73,f27961]) ).
fof(f28118,plain,
! [X0] : join(X0,converse(complement(converse(complement(X0))))) = X0,
inference(forward_demodulation,[],[f28097,f28]) ).
fof(f28148,plain,
! [X0] : converse(complement(converse(complement(X0)))) = join(X0,complement(join(complement(converse(complement(converse(complement(X0))))),X0))),
inference(forward_demodulation,[],[f28065,f920]) ).
fof(f28188,plain,
! [X0] : converse(complement(converse(complement(X0)))) = join(X0,converse(complement(converse(complement(X0))))),
inference(forward_demodulation,[],[f28148,f1991]) ).
fof(f28207,plain,
! [X0] : converse(complement(converse(complement(X0)))) = X0,
inference(forward_demodulation,[],[f28188,f28118]) ).
fof(f28231,plain,
sF3 = converse(complement(converse(one))),
inference(superposition,[],[f28207,f956]) ).
fof(f28239,plain,
! [X0] : converse(X0) = complement(converse(complement(X0))),
inference(superposition,[],[f28,f28207]) ).
fof(f28264,plain,
sF3 = converse(complement(one)),
inference(forward_demodulation,[],[f28231,f619]) ).
fof(f28276,plain,
sF3 = converse(sF3),
inference(forward_demodulation,[],[f28264,f47]) ).
fof(f28295,plain,
converse(sF2) = complement(converse(sK0)),
inference(superposition,[],[f28239,f958]) ).
fof(f28298,plain,
converse(sF5) = complement(converse(sF4)),
inference(superposition,[],[f28239,f960]) ).
fof(f28492,plain,
! [X0] : join(sF3,converse(X0)) = converse(join(sF3,X0)),
inference(superposition,[],[f73,f28276]) ).
fof(f29248,plain,
complement(join(complement(sK0),complement(sF5))) = composition(complement(join(complement(sK0),complement(sF5))),complement(join(sF3,complement(converse(sK0))))),
inference(superposition,[],[f5760,f17781]) ).
fof(f29282,plain,
complement(join(complement(sK0),complement(sF5))) = composition(complement(join(complement(sK0),complement(sF5))),complement(join(sF3,converse(sF2)))),
inference(forward_demodulation,[],[f29248,f28295]) ).
fof(f29349,plain,
complement(join(complement(sK0),complement(sF5))) = composition(complement(join(complement(sK0),complement(sF5))),complement(converse(join(sF3,sF2)))),
inference(forward_demodulation,[],[f29282,f28492]) ).
fof(f29380,plain,
complement(join(complement(sK0),complement(sF5))) = composition(complement(join(complement(sK0),complement(sF5))),complement(converse(sF4))),
inference(forward_demodulation,[],[f29349,f2834]) ).
fof(f29397,plain,
complement(join(complement(sK0),complement(sF5))) = composition(complement(join(complement(sK0),complement(sF5))),converse(sF5)),
inference(forward_demodulation,[],[f29380,f28298]) ).
fof(f29408,plain,
complement(join(complement(sK0),sF4)) = composition(complement(join(complement(sK0),sF4)),converse(sF5)),
inference(forward_demodulation,[],[f29397,f960]) ).
fof(f29413,plain,
complement(join(sF2,sF4)) = composition(complement(join(sF2,sF4)),converse(sF5)),
inference(forward_demodulation,[],[f29408,f45]) ).
fof(f29417,plain,
complement(sF4) = composition(complement(sF4),converse(sF5)),
inference(forward_demodulation,[],[f29413,f3779]) ).
fof(f29419,plain,
sF5 = composition(sF5,converse(sF5)),
inference(forward_demodulation,[],[f29417,f51]) ).
fof(f29424,plain,
sF5 = converse(sF5),
inference(superposition,[],[f104,f29419]) ).
fof(f29480,plain,
sK0 = composition(sF5,sK0),
inference(superposition,[],[f24836,f29424]) ).
fof(f29526,plain,
! [X0] : complement(join(complement(composition(sF5,complement(join(complement(sK0),complement(composition(converse(sF5),X0)))))),complement(X0))) = join(complement(join(complement(sK0),complement(X0))),complement(join(complement(composition(sF5,complement(join(complement(sK0),complement(composition(converse(sF5),X0)))))),complement(X0)))),
inference(superposition,[],[f41,f29480]) ).
fof(f29544,plain,
! [X0] : complement(join(complement(composition(sF5,complement(join(complement(sK0),complement(composition(sF5,X0)))))),complement(X0))) = join(complement(join(complement(sK0),complement(X0))),complement(join(complement(composition(sF5,complement(join(complement(sK0),complement(composition(sF5,X0)))))),complement(X0)))),
inference(forward_demodulation,[],[f29526,f29424]) ).
fof(f29555,plain,
! [X0] : complement(join(complement(composition(sF5,complement(join(sF2,complement(composition(sF5,X0)))))),complement(X0))) = join(complement(join(sF2,complement(X0))),complement(join(complement(composition(sF5,complement(join(sF2,complement(composition(sF5,X0)))))),complement(X0)))),
inference(forward_demodulation,[],[f29544,f45]) ).
fof(f29558,plain,
! [X0] : complement(join(complement(composition(sF5,complement(complement(composition(sF5,X0))))),complement(X0))) = join(complement(join(sF2,complement(X0))),complement(join(complement(composition(sF5,complement(complement(composition(sF5,X0))))),complement(X0)))),
inference(forward_demodulation,[],[f29555,f24438]) ).
fof(f29561,plain,
! [X0] : complement(join(complement(composition(sF5,composition(sF5,X0))),complement(X0))) = join(complement(join(sF2,complement(X0))),complement(join(complement(composition(sF5,composition(sF5,X0))),complement(X0)))),
inference(forward_demodulation,[],[f29558,f930]) ).
fof(f29563,plain,
! [X0] : complement(join(complement(composition(sF5,X0)),complement(X0))) = join(complement(join(sF2,complement(X0))),complement(join(complement(composition(sF5,X0)),complement(X0)))),
inference(forward_demodulation,[],[f29561,f24485]) ).
fof(f29565,plain,
! [X0] : complement(complement(composition(sF5,X0))) = join(complement(join(sF2,complement(X0))),complement(complement(composition(sF5,X0)))),
inference(forward_demodulation,[],[f29563,f4156]) ).
fof(f29566,plain,
! [X0] : complement(complement(composition(sF5,X0))) = join(composition(sF5,X0),complement(join(sF2,complement(X0)))),
inference(forward_demodulation,[],[f29565,f920]) ).
fof(f29567,plain,
! [X0] : composition(sF5,X0) = join(composition(sF5,X0),complement(join(sF2,complement(X0)))),
inference(forward_demodulation,[],[f29566,f930]) ).
fof(f29768,plain,
composition(sF5,sK1) = join(composition(sF5,sK1),complement(join(sF2,sF7))),
inference(superposition,[],[f29567,f55]) ).
fof(f29853,plain,
composition(sF5,sK1) = join(composition(sF5,sK1),complement(sF8)),
inference(forward_demodulation,[],[f29768,f57]) ).
fof(f29898,plain,
composition(sF5,sK1) = join(composition(sF5,sK1),sF9),
inference(forward_demodulation,[],[f29853,f59]) ).
fof(f29922,plain,
sF6 = join(sF6,sF9),
inference(forward_demodulation,[],[f29898,f53]) ).
fof(f29938,plain,
sF6 = sF10,
inference(forward_demodulation,[],[f29922,f27275]) ).
fof(f29949,plain,
$false,
inference(forward_subsumption_resolution,[],[f29938,f62]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL022+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n015.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 22:56:01 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.42 Running first-order theorem proving
% 0.13/0.42 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 20.66/3.93 % (2103409)Detected formulas, will run a generic FOF schedule.
% 20.66/3.93 % (2103429)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=792451647:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 20.66/3.93 % (2103432)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=478673947:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 20.66/3.93 % (2103431)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=4242804995:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 20.66/3.93 % (2103430)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2761309440:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 20.66/3.93 % (2103428)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1484173131:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 20.66/3.93 % (2103427)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=4112640944:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 20.66/3.93 % (2103433)dis-21_1_sil=8000:lcm=predicate:random_seed=127396493:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 20.66/3.93 % (2103433)Refutation not found, incomplete strategy
% 20.66/3.93 % (2103433)------------------------------
% 20.66/3.93 % (2103433)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.66/3.93 % (2103433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.66/3.93 % (2103433)CaDiCaL version: 2.1.3
% 20.66/3.93 % (2103433)Termination reason: Refutation not found, incomplete strategy
% 20.66/3.93 % (2103433)Time elapsed: 0.002 s
% 20.66/3.93 % (2103433)Peak memory usage: 88 MB
% 20.66/3.93 % (2103433)Instructions burned: 1 (million)
% 20.66/3.93 % (2103430)Instruction limit reached!
% 20.66/3.93 % (2103430)------------------------------
% 20.66/3.93 % (2103430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.66/3.93 % (2103430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.66/3.93 % (2103430)CaDiCaL version: 2.1.3
% 20.66/3.93 % (2103430)Termination reason: Instruction limit
% 20.66/3.93 % (2103430)Termination phase: Saturation
% 20.66/3.93 % (2103430)Time elapsed: 0.100 s
% 20.66/3.93 % (2103430)Peak memory usage: 89 MB
% 20.66/3.93 % (2103430)Instructions burned: 110 (million)
% 20.66/3.93 % (2103432)Instruction limit reached!
% 20.66/3.93 % (2103432)------------------------------
% 20.66/3.93 % (2103432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.66/3.93 % (2103432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.66/3.93 % (2103432)CaDiCaL version: 2.1.3
% 20.66/3.93 % (2103432)Termination reason: Instruction limit
% 20.66/3.93 % (2103432)Termination phase: Saturation
% 20.66/3.93 % (2103432)Time elapsed: 0.126 s
% 20.66/3.93 % (2103432)Peak memory usage: 90 MB
% 20.66/3.93 % (2103432)Instructions burned: 139 (million)
% 20.66/3.93 % (2103431)Instruction limit reached!
% 20.66/3.93 % (2103431)------------------------------
% 20.66/3.93 % (2103431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.66/3.93 % (2103431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.66/3.93 % (2103431)CaDiCaL version: 2.1.3
% 20.66/3.93 % (2103431)Termination reason: Instruction limit
% 20.66/3.93 % (2103431)Termination phase: Saturation
% 20.66/3.93 % (2103431)Time elapsed: 0.152 s
% 20.66/3.93 % (2103431)Peak memory usage: 88 MB
% 20.66/3.93 % (2103431)Instructions burned: 120 (million)
% 20.66/3.93 % (2103449)lrs+10_1_sil=8000:sp=occurrence:random_seed=3045355862:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 20.66/3.93 % (2103450)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2618692243:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 20.66/3.93 % (2103433)------------------------------
% 20.66/3.93 % (2103433)------------------------------
% 20.66/3.93 % (2103451)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1418115348:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 20.66/3.93 % (2103450)Instruction limit reached!
% 20.66/3.93 % (2103450)------------------------------
% 20.66/3.93 % (2103450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.40/4.96 % (2103450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.40/4.96 % (2103450)CaDiCaL version: 2.1.3
% 28.40/4.96 % (2103450)Termination reason: Instruction limit
% 28.40/4.96 % (2103450)Termination phase: Saturation
% 28.40/4.96 % (2103450)Time elapsed: 0.158 s
% 28.40/4.96 % (2103450)Peak memory usage: 90 MB
% 28.40/4.96 % (2103450)Instructions burned: 157 (million)
% 28.40/4.96 % (2103464)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=2200369799:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 28.40/4.96 % (2103449)Instruction limit reached!
% 28.40/4.96 % (2103449)------------------------------
% 28.40/4.96 % (2103449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.40/4.96 % (2103449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.40/4.96 % (2103449)CaDiCaL version: 2.1.3
% 28.40/4.96 % (2103449)Termination reason: Instruction limit
% 28.40/4.96 % (2103449)Termination phase: Saturation
% 28.40/4.96 % (2103449)Time elapsed: 0.272 s
% 28.40/4.96 % (2103449)Peak memory usage: 92 MB
% 28.40/4.96 % (2103449)Instructions burned: 285 (million)
% 28.40/4.96 % (2103464)Instruction limit reached!
% 28.40/4.96 % (2103464)------------------------------
% 28.40/4.96 % (2103464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.40/4.96 % (2103464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.40/4.96 % (2103464)CaDiCaL version: 2.1.3
% 28.40/4.96 % (2103464)Termination reason: Instruction limit
% 28.40/4.96 % (2103464)Termination phase: Saturation
% 28.40/4.96 % (2103464)Time elapsed: 0.132 s
% 28.40/4.96 % (2103464)Peak memory usage: 92 MB
% 28.40/4.96 % (2103464)Instructions burned: 250 (million)
% 28.40/4.96 % (2103451)Instruction limit reached!
% 28.40/4.96 % (2103451)------------------------------
% 28.40/4.96 % (2103451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.40/4.96 % (2103451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.40/4.96 % (2103451)CaDiCaL version: 2.1.3
% 28.40/4.96 % (2103451)Termination reason: Instruction limit
% 28.40/4.96 % (2103451)Termination phase: Saturation
% 28.40/4.96 % (2103451)Time elapsed: 0.281 s
% 28.40/4.96 % (2103451)Peak memory usage: 92 MB
% 28.40/4.96 % (2103451)Instructions burned: 325 (million)
% 28.40/4.96 % (2103467)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=122992807:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 28.40/4.96 % (2103470)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=347343860:i=2350_2992 on theBenchmark for (2992ds/2350Mi)
% 28.40/4.96 % (2103474)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3516187437:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 28.40/4.96 % (2103473)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=318645290:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 28.40/4.96 % (2103474)Refutation not found, incomplete strategy
% 28.40/4.96 % (2103474)------------------------------
% 28.40/4.96 % (2103474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.40/4.96 % (2103474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.40/4.96 % (2103474)CaDiCaL version: 2.1.3
% 28.40/4.96 % (2103474)Termination reason: Refutation not found, incomplete strategy
% 28.40/4.96 % (2103474)Time elapsed: 0.002 s
% 28.40/4.96 % (2103474)Peak memory usage: 87 MB
% 28.40/4.96 % (2103474)Instructions burned: 1 (million)
% 28.40/4.96 % (2103473)Instruction limit reached!
% 28.40/4.96 % (2103473)------------------------------
% 28.40/4.96 % (2103473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.40/4.96 % (2103473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.40/4.96 % (2103473)CaDiCaL version: 2.1.3
% 28.40/4.96 % (2103473)Termination reason: Instruction limit
% 28.40/4.96 % (2103473)Termination phase: Saturation
% 28.40/4.96 % (2103473)Time elapsed: 0.112 s
% 28.40/4.96 % (2103473)Peak memory usage: 90 MB
% 28.40/4.96 % (2103473)Instructions burned: 114 (million)
% 28.40/4.96 % (2103467)Instruction limit reached!
% 28.40/4.96 % (2103467)------------------------------
% 28.40/4.96 % (2103467)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.40/4.96 % (2103467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.40/4.96 % (2103467)CaDiCaL version: 2.1.3
% 28.40/4.96 % (2103467)Termination reason: Instruction limit
% 28.40/4.96 % (2103467)Termination phase: Saturation
% 28.40/4.96 % (2103467)Time elapsed: 0.285 s
% 28.40/4.96 % (2103467)Peak memory usage: 92 MB
% 28.40/4.96 % (2103467)Instructions burned: 294 (million)
% 28.40/4.96 % (2103486)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4169451707:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2988 on theBenchmark for (2988ds/114Mi)
% 28.40/4.96 % (2103474)------------------------------
% 28.40/4.96 % (2103474)------------------------------
% 28.40/4.96 % (2103487)lrs+10_1_sil=8000:sp=occurrence:random_seed=2910420356:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2988 on theBenchmark for (2988ds/907Mi)
% 28.40/4.96 % (2103486)Instruction limit reached!
% 28.40/4.96 % (2103486)------------------------------
% 28.40/4.96 % (2103486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.40/4.96 % (2103486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.40/4.96 % (2103486)CaDiCaL version: 2.1.3
% 28.40/4.96 % (2103486)Termination reason: Instruction limit
% 28.40/4.96 % (2103486)Termination phase: Saturation
% 28.40/4.96 % (2103486)Time elapsed: 0.100 s
% 28.40/4.96 % (2103486)Peak memory usage: 89 MB
% 28.40/4.96 % (2103486)Instructions burned: 114 (million)
% 28.40/4.96 % (2103489)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3919409018:i=437:sd=1:aac=none:ss=included_2986 on theBenchmark for (2986ds/437Mi)
% 28.40/4.96 % (2103494)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=4057211638:i=5202:ss=axioms:sgt=16_2985 on theBenchmark for (2985ds/5202Mi)
% 28.40/4.96 % (2103489)Instruction limit reached!
% 28.40/4.96 % (2103489)------------------------------
% 28.40/4.96 % (2103489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.40/4.96 % (2103489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.40/4.96 % (2103489)CaDiCaL version: 2.1.3
% 28.40/4.96 % (2103489)Termination reason: Instruction limit
% 28.40/4.96 % (2103489)Termination phase: Saturation
% 28.40/4.96 % (2103489)Time elapsed: 0.394 s
% 28.40/4.96 % (2103489)Peak memory usage: 91 MB
% 28.40/4.96 % (2103489)Instructions burned: 437 (million)
% 28.40/4.96 % (2103502)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1760836065:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2980 on theBenchmark for (2980ds/134Mi)
% 28.40/4.96 % (2103502)Refutation not found, incomplete strategy
% 28.40/4.96 % (2103502)------------------------------
% 28.40/4.96 % (2103502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.40/4.96 % (2103502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.40/4.96 % (2103502)CaDiCaL version: 2.1.3
% 28.40/4.96 % (2103502)Termination reason: Refutation not found, incomplete strategy
% 28.40/4.96 % (2103502)Time elapsed: 0.004 s
% 28.40/4.96 % (2103502)Peak memory usage: 89 MB
% 28.40/4.96 % (2103502)Instructions burned: 2 (million)
% 28.40/4.96 % (2103487)Instruction limit reached!
% 28.40/4.96 % (2103487)------------------------------
% 28.40/4.96 % (2103487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.40/4.96 % (2103487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.40/4.96 % (2103487)CaDiCaL version: 2.1.3
% 28.40/4.96 % (2103487)Termination reason: Instruction limit
% 28.40/4.96 % (2103487)Termination phase: Saturation
% 28.40/4.96 % (2103487)Time elapsed: 0.891 s
% 28.40/4.96 % (2103487)Peak memory usage: 98 MB
% 28.40/4.96 % (2103487)Instructions burned: 909 (million)
% 28.40/4.96 % (2103506)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3473660009:st=8:i=592:sd=3:ep=RST:ss=axioms_2977 on theBenchmark for (2977ds/592Mi)
% 28.40/4.96 % (2103502)------------------------------
% 28.40/4.96 % (2103502)------------------------------
% 28.40/4.96 % (2103509)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2641220890:st=3:i=13193:sd=3:ss=axioms_2974 on theBenchmark for (2974ds/13193Mi)
% 28.40/4.96 % (2103506)Instruction limit reached!
% 28.40/4.96 % (2103506)------------------------------
% 28.40/4.96 % (2103506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.40/4.96 % (2103506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.40/4.96 % (2103506)CaDiCaL version: 2.1.3
% 28.40/4.96 % (2103506)Termination reason: Instruction limit
% 28.40/4.96 % (2103506)Termination phase: Saturation
% 28.40/4.96 % (2103506)Time elapsed: 0.585 s
% 28.40/4.96 % (2103506)Peak memory usage: 94 MB
% 28.40/4.96 % (2103506)Instructions burned: 592 (million)
% 28.40/4.96 % (2103470)Instruction limit reached!
% 28.40/4.96 % (2103470)------------------------------
% 28.40/4.96 % (2103470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.40/4.96 % (2103470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.40/4.96 % (2103470)CaDiCaL version: 2.1.3
% 28.40/4.96 % (2103470)Termination reason: Instruction limit
% 28.40/4.96 % (2103470)Termination phase: Saturation
% 28.40/4.96 % (2103470)Time elapsed: 2.218 s
% 28.40/4.96 % (2103470)Peak memory usage: 142 MB
% 28.40/4.96 % (2103470)Instructions burned: 2350 (million)
% 28.40/4.96 % (2103516)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2114036105:i=134:gtgl=5:slsql=off:gtg=exists_sym_2968 on theBenchmark for (2968ds/134Mi)
% 28.40/4.96 % (2103514)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=436996192:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2969 on theBenchmark for (2969ds/125Mi)
% 28.40/4.96 % (2103516)Instruction limit reached!
% 28.40/4.96 % (2103516)------------------------------
% 28.40/4.96 % (2103516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.40/4.96 % (2103516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.40/4.96 % (2103516)CaDiCaL version: 2.1.3
% 28.40/4.96 % (2103516)Termination reason: Instruction limit
% 28.40/4.96 % (2103516)Termination phase: Saturation
% 28.40/4.96 % (2103516)Time elapsed: 0.133 s
% 28.40/4.96 % (2103516)Peak memory usage: 90 MB
% 28.40/4.96 % (2103516)Instructions burned: 134 (million)
% 28.40/4.96 % (2103514)Instruction limit reached!
% 28.40/4.96 % (2103514)------------------------------
% 28.40/4.96 % (2103514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.40/4.96 % (2103514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.40/4.96 % (2103514)CaDiCaL version: 2.1.3
% 28.40/4.96 % (2103514)Termination reason: Instruction limit
% 28.40/4.96 % (2103514)Termination phase: Saturation
% 28.40/4.96 % (2103514)Time elapsed: 0.145 s
% 28.40/4.96 % (2103514)Peak memory usage: 91 MB
% 28.40/4.96 % (2103514)Instructions burned: 125 (million)
% 28.40/4.96 % (2103520)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=865863082:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2965 on theBenchmark for (2965ds/141Mi)
% 28.40/4.96 % (2103521)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3462467219:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2965 on theBenchmark for (2965ds/431Mi)
% 28.40/4.96 % (2103520)Refutation not found, incomplete strategy
% 28.40/4.96 % (2103520)------------------------------
% 28.40/4.96 % (2103520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.40/4.96 % (2103520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.40/4.96 % (2103520)CaDiCaL version: 2.1.3
% 28.40/4.96 % (2103520)Termination reason: Refutation not found, incomplete strategy
% 28.40/4.96 % (2103520)Time elapsed: 0.002 s
% 28.40/4.96 % (2103520)Peak memory usage: 88 MB
% 28.40/4.96 % (2103521)Refutation not found, incomplete strategy
% 28.40/4.96 % (2103521)------------------------------
% 28.40/4.96 % (2103521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.40/4.96 % (2103521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.40/4.96 % (2103521)CaDiCaL version: 2.1.3
% 28.40/4.96 % (2103521)Termination reason: Refutation not found, incomplete strategy
% 28.40/4.96 % (2103521)Time elapsed: 0.002 s
% 28.40/4.96 % (2103521)Peak memory usage: 88 MB
% 28.40/4.96 % (2103521)Instructions burned: 1 (million)
% 28.40/4.96 % (2103427)First to succeed.
% 28.40/4.96 % (2103427)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2103409"
% 28.40/4.96 % (2103520)------------------------------
% 28.40/4.96 % (2103520)------------------------------
% 28.40/4.96 % (2103521)------------------------------
% 28.40/4.96 % (2103521)------------------------------
% 28.40/4.96 % (2103427)Refutation found. Thanks to Tanya!
% 28.40/4.96 % SZS status Theorem for theBenchmark
% 28.40/4.96 % SZS output start Proof for theBenchmark
% See solution above
% 0.18/5.26 % (2103427)------------------------------
% 0.18/5.26 % (2103427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.18/5.26 % (2103427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/5.26 % (2103427)CaDiCaL version: 2.1.3
% 0.18/5.26 % (2103427)Termination reason: Refutation
% 0.18/5.26 % (2103427)Time elapsed: 3.613 s
% 0.18/5.26 % (2103427)Peak memory usage: 154 MB
% 0.18/5.26 % (2103427)Instructions burned: 3564 (million)
% 0.18/5.26 % (2103427)------------------------------
% 0.18/5.26 % (2103427)------------------------------
% 0.18/5.26 % (2103409)Success in time 4.091 s
% 0.18/5.26 % Vampire exiting
%------------------------------------------------------------------------------