%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : REL027+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n003.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:22 PM UTC 2026
% Result : Theorem 138.61s 33.38s
% Output : Refutation 138.61s
% Verified :
% SZS Type : Refutation
% Derivation depth : 152
% Number of leaves : 15
% Syntax : Number of formulae : 473 ( 443 unt; 2 def)
% Number of atoms : 507 ( 473 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 65 ( 31 ~; 26 |; 4 &)
% ( 2 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 3 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 4 con; 0-2 aty)
% Number of variables : 514 ( 0 sgn 513 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001+0.ax',maddux1_join_commutativity) ).
fof(f2,axiom,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001+0.ax',maddux2_join_associativity) ).
fof(f3,axiom,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001+0.ax',maddux3_a_kind_of_de_Morgan) ).
fof(f4,axiom,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001+0.ax',maddux4_definiton_of_meet) ).
fof(f6,axiom,
! [X0] : composition(X0,one) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/REL001+0.ax',composition_identity) ).
fof(f7,axiom,
! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001+0.ax',composition_distributivity) ).
fof(f8,axiom,
! [X0] : converse(converse(X0)) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/REL001+0.ax',converse_idempotence) ).
fof(f9,axiom,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001+0.ax',converse_additivity) ).
fof(f10,axiom,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001+0.ax',converse_multiplicativity) ).
fof(f11,axiom,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001+0.ax',converse_cancellativity) ).
fof(f12,axiom,
! [X0] : top = join(X0,complement(X0)),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001+0.ax',def_top) ).
fof(f13,axiom,
! [X0] : zero = meet(X0,complement(X0)),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001+0.ax',def_zero) ).
fof(f14,conjecture,
! [X0] :
( join(X0,one) = one
=> ( join(meet(complement(composition(X0,top)),one),meet(complement(X0),one)) = meet(complement(X0),one)
& join(meet(complement(X0),one),meet(complement(composition(X0,top)),one)) = meet(complement(composition(X0,top)),one) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f15,negated_conjecture,
~ ! [X0] :
( join(X0,one) = one
=> ( join(meet(complement(composition(X0,top)),one),meet(complement(X0),one)) = meet(complement(X0),one)
& join(meet(complement(X0),one),meet(complement(composition(X0,top)),one)) = meet(complement(composition(X0,top)),one) ) ),
inference(negated_conjecture,[status(cth)],[f14]) ).
fof(f16,plain,
? [X0] :
( ( meet(complement(X0),one) != join(meet(complement(composition(X0,top)),one),meet(complement(X0),one))
| meet(complement(composition(X0,top)),one) != join(meet(complement(X0),one),meet(complement(composition(X0,top)),one)) )
& join(X0,one) = one ),
inference(ennf_transformation,[],[f15]) ).
fof(f17,plain,
( ( meet(complement(sK0),one) != join(meet(complement(composition(sK0,top)),one),meet(complement(sK0),one))
| meet(complement(composition(sK0,top)),one) != join(meet(complement(sK0),one),meet(complement(composition(sK0,top)),one)) )
& one = join(sK0,one) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X0,sK0)],[f16]) ).
fof(f18,plain,
! [X0,X1] : join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f19,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
inference(cnf_transformation,[],[f2]) ).
fof(f20,plain,
! [X0,X1] : join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) = X0,
inference(cnf_transformation,[],[f3]) ).
fof(f21,plain,
! [X0,X1] : complement(join(complement(X0),complement(X1))) = meet(X0,X1),
inference(cnf_transformation,[],[f4]) ).
fof(f23,plain,
! [X0] : composition(X0,one) = X0,
inference(cnf_transformation,[],[f6]) ).
fof(f24,plain,
! [X2,X0,X1] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
inference(cnf_transformation,[],[f7]) ).
fof(f25,plain,
! [X0] : converse(converse(X0)) = X0,
inference(cnf_transformation,[],[f8]) ).
fof(f26,plain,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
inference(cnf_transformation,[],[f9]) ).
fof(f27,plain,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
inference(cnf_transformation,[],[f10]) ).
fof(f28,plain,
! [X0,X1] : complement(X1) = join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)),
inference(cnf_transformation,[],[f11]) ).
fof(f29,plain,
! [X0] : top = join(X0,complement(X0)),
inference(cnf_transformation,[],[f12]) ).
fof(f30,plain,
! [X0] : zero = meet(X0,complement(X0)),
inference(cnf_transformation,[],[f13]) ).
fof(f31,plain,
one = join(sK0,one),
inference(cnf_transformation,[],[f17]) ).
fof(f32,plain,
( meet(complement(sK0),one) != join(meet(complement(composition(sK0,top)),one),meet(complement(sK0),one))
| meet(complement(composition(sK0,top)),one) != join(meet(complement(sK0),one),meet(complement(composition(sK0,top)),one)) ),
inference(cnf_transformation,[],[f17]) ).
fof(f33,plain,
! [X0] : zero = complement(join(complement(X0),complement(complement(X0)))),
inference(definition_unfolding,[],[f30,f21]) ).
fof(f34,plain,
( complement(join(complement(complement(sK0)),complement(one))) != join(complement(join(complement(complement(composition(sK0,top))),complement(one))),complement(join(complement(complement(sK0)),complement(one))))
| complement(join(complement(complement(composition(sK0,top))),complement(one))) != join(complement(join(complement(complement(sK0)),complement(one))),complement(join(complement(complement(composition(sK0,top))),complement(one)))) ),
inference(definition_unfolding,[],[f32,f21,f21,f21,f21,f21,f21]) ).
fof(f36,definition,
( spl1_1
<=> complement(join(complement(complement(composition(sK0,top))),complement(one))) = join(complement(join(complement(complement(sK0)),complement(one))),complement(join(complement(complement(composition(sK0,top))),complement(one)))) ),
introduced(definition,[new_symbols(definition,[spl1_1])],[avatar_definition]) ).
fof(f38,plain,
( complement(join(complement(complement(composition(sK0,top))),complement(one))) != join(complement(join(complement(complement(sK0)),complement(one))),complement(join(complement(complement(composition(sK0,top))),complement(one))))
| spl1_1 ),
inference(avatar_component_clause,[],[f36]) ).
fof(f40,definition,
( spl1_2
<=> complement(join(complement(complement(sK0)),complement(one))) = join(complement(join(complement(complement(composition(sK0,top))),complement(one))),complement(join(complement(complement(sK0)),complement(one)))) ),
introduced(definition,[new_symbols(definition,[spl1_2])],[avatar_definition]) ).
fof(f42,plain,
( complement(join(complement(complement(sK0)),complement(one))) != join(complement(join(complement(complement(composition(sK0,top))),complement(one))),complement(join(complement(complement(sK0)),complement(one))))
| spl1_2 ),
inference(avatar_component_clause,[],[f40]) ).
fof(f43,plain,
( ~ spl1_1
| ~ spl1_2 ),
inference(avatar_split_clause,[],[f34,f40,f36]) ).
fof(f44,plain,
one = join(one,sK0),
inference(superposition,[],[f18,f31]) ).
fof(f50,plain,
( complement(join(complement(one),complement(complement(composition(sK0,top))))) != join(complement(join(complement(complement(sK0)),complement(one))),complement(join(complement(one),complement(complement(composition(sK0,top))))))
| spl1_1 ),
inference(superposition,[],[f38,f18]) ).
fof(f52,plain,
( complement(join(complement(one),complement(complement(composition(sK0,top))))) != join(complement(join(complement(one),complement(complement(sK0)))),complement(join(complement(one),complement(complement(composition(sK0,top))))))
| spl1_1 ),
inference(forward_demodulation,[],[f50,f18]) ).
fof(f56,plain,
zero = complement(top),
inference(forward_demodulation,[],[f33,f29]) ).
fof(f58,plain,
! [X0,X1] : converse(join(converse(X0),X1)) = join(X0,converse(X1)),
inference(superposition,[],[f26,f25]) ).
fof(f59,plain,
! [X0,X1] : converse(join(X1,converse(X0))) = join(converse(X1),X0),
inference(superposition,[],[f26,f25]) ).
fof(f64,plain,
! [X0,X1] : converse(composition(X1,converse(X0))) = composition(X0,converse(X1)),
inference(superposition,[],[f27,f25]) ).
fof(f65,plain,
! [X0,X1] : converse(composition(converse(X0),X1)) = composition(converse(X1),X0),
inference(superposition,[],[f27,f25]) ).
fof(f69,plain,
! [X0] : join(X0,converse(complement(converse(X0)))) = converse(top),
inference(superposition,[],[f58,f29]) ).
fof(f109,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(top,X1),
inference(superposition,[],[f19,f29]) ).
fof(f114,plain,
! [X0] : join(one,join(sK0,X0)) = join(one,X0),
inference(superposition,[],[f19,f44]) ).
fof(f117,plain,
! [X0] : join(one,X0) = join(sK0,join(one,X0)),
inference(superposition,[],[f19,f31]) ).
fof(f118,plain,
! [X0,X1] : top = join(X0,join(X1,complement(join(X0,X1)))),
inference(superposition,[],[f19,f29]) ).
fof(f133,plain,
converse(top) = join(sK0,converse(top)),
inference(superposition,[],[f117,f69]) ).
fof(f137,plain,
converse(converse(top)) = join(converse(sK0),top),
inference(superposition,[],[f59,f133]) ).
fof(f138,plain,
! [X0] : join(converse(top),X0) = join(sK0,join(converse(top),X0)),
inference(superposition,[],[f19,f133]) ).
fof(f139,plain,
converse(converse(top)) = join(top,converse(sK0)),
inference(forward_demodulation,[],[f137,f18]) ).
fof(f140,plain,
top = join(top,converse(sK0)),
inference(forward_demodulation,[],[f139,f25]) ).
fof(f142,plain,
! [X0] : join(top,X0) = join(top,join(converse(sK0),X0)),
inference(superposition,[],[f19,f140]) ).
fof(f144,plain,
join(one,top) = join(one,complement(sK0)),
inference(superposition,[],[f114,f29]) ).
fof(f145,plain,
! [X0] : join(one,X0) = join(one,join(X0,sK0)),
inference(superposition,[],[f114,f18]) ).
fof(f147,plain,
join(one,converse(top)) = join(one,converse(complement(converse(sK0)))),
inference(superposition,[],[f114,f69]) ).
fof(f153,plain,
! [X0] : join(one,join(complement(sK0),X0)) = join(join(one,top),X0),
inference(superposition,[],[f19,f144]) ).
fof(f154,plain,
! [X0] : join(one,join(complement(sK0),X0)) = join(one,join(top,X0)),
inference(forward_demodulation,[],[f153,f19]) ).
fof(f171,plain,
! [X0,X1] : join(one,join(X0,X1)) = join(one,join(X0,join(X1,sK0))),
inference(superposition,[],[f145,f19]) ).
fof(f173,plain,
! [X0,X1] : join(join(one,X0),X1) = join(one,join(join(X0,sK0),X1)),
inference(superposition,[],[f19,f145]) ).
fof(f174,plain,
! [X0,X1] : join(join(one,X0),X1) = join(one,join(X0,join(sK0,X1))),
inference(forward_demodulation,[],[f173,f19]) ).
fof(f175,plain,
! [X0,X1] : join(one,join(X0,X1)) = join(one,join(X0,join(sK0,X1))),
inference(forward_demodulation,[],[f174,f19]) ).
fof(f182,plain,
! [X0] : join(top,converse(X0)) = join(top,converse(join(sK0,X0))),
inference(superposition,[],[f142,f26]) ).
fof(f184,plain,
! [X0] : join(top,X0) = join(top,join(X0,converse(sK0))),
inference(superposition,[],[f142,f18]) ).
fof(f186,plain,
join(top,converse(complement(converse(converse(sK0))))) = join(top,converse(top)),
inference(superposition,[],[f142,f69]) ).
fof(f190,plain,
join(top,converse(top)) = join(top,converse(complement(sK0))),
inference(forward_demodulation,[],[f186,f25]) ).
fof(f200,plain,
! [X0,X1] : join(join(top,X0),X1) = join(top,join(join(X0,converse(sK0)),X1)),
inference(superposition,[],[f19,f184]) ).
fof(f201,plain,
! [X0,X1] : join(join(top,X0),X1) = join(top,join(X0,join(converse(sK0),X1))),
inference(forward_demodulation,[],[f200,f19]) ).
fof(f202,plain,
! [X0,X1] : join(top,join(X0,X1)) = join(top,join(X0,join(converse(sK0),X1))),
inference(forward_demodulation,[],[f201,f19]) ).
fof(f204,plain,
join(converse(top),complement(sK0)) = converse(join(top,converse(top))),
inference(superposition,[],[f59,f190]) ).
fof(f207,plain,
join(converse(top),complement(sK0)) = join(converse(top),top),
inference(forward_demodulation,[],[f204,f59]) ).
fof(f208,plain,
join(top,converse(top)) = join(converse(top),complement(sK0)),
inference(forward_demodulation,[],[f207,f18]) ).
fof(f209,plain,
join(top,converse(top)) = join(complement(sK0),converse(top)),
inference(forward_demodulation,[],[f208,f18]) ).
fof(f211,plain,
! [X0] : join(join(top,converse(top)),X0) = join(complement(sK0),join(converse(top),X0)),
inference(superposition,[],[f19,f209]) ).
fof(f212,plain,
! [X0] : join(top,join(converse(top),X0)) = join(complement(sK0),join(converse(top),X0)),
inference(forward_demodulation,[],[f211,f19]) ).
fof(f217,plain,
join(converse(one),complement(converse(sK0))) = converse(join(one,converse(top))),
inference(superposition,[],[f59,f147]) ).
fof(f218,plain,
! [X0] : join(one,join(converse(complement(converse(sK0))),X0)) = join(join(one,converse(top)),X0),
inference(superposition,[],[f19,f147]) ).
fof(f219,plain,
! [X0] : join(one,join(converse(complement(converse(sK0))),X0)) = join(one,join(converse(top),X0)),
inference(forward_demodulation,[],[f218,f19]) ).
fof(f220,plain,
join(converse(one),complement(converse(sK0))) = join(converse(one),top),
inference(forward_demodulation,[],[f217,f59]) ).
fof(f221,plain,
join(converse(one),complement(converse(sK0))) = join(top,converse(one)),
inference(forward_demodulation,[],[f220,f18]) ).
fof(f222,plain,
! [X0] : converse(join(top,X0)) = join(sK0,converse(join(top,X0))),
inference(superposition,[],[f138,f26]) ).
fof(f224,plain,
! [X0] : join(X0,converse(top)) = join(sK0,join(X0,converse(top))),
inference(superposition,[],[f138,f18]) ).
fof(f230,plain,
! [X0] : join(converse(one),join(complement(converse(sK0)),X0)) = join(join(top,converse(one)),X0),
inference(superposition,[],[f19,f221]) ).
fof(f231,plain,
! [X0] : join(converse(one),join(complement(converse(sK0)),X0)) = join(top,join(converse(one),X0)),
inference(forward_demodulation,[],[f230,f19]) ).
fof(f245,plain,
! [X0] : join(converse(sK0),join(top,X0)) = converse(converse(join(top,X0))),
inference(superposition,[],[f59,f222]) ).
fof(f246,plain,
! [X0,X1] : join(converse(join(top,X0)),X1) = join(sK0,join(converse(join(top,X0)),X1)),
inference(superposition,[],[f19,f222]) ).
fof(f247,plain,
! [X0] : join(top,X0) = join(converse(sK0),join(top,X0)),
inference(forward_demodulation,[],[f245,f25]) ).
fof(f256,plain,
! [X0] : join(X0,top) = join(converse(sK0),join(X0,top)),
inference(superposition,[],[f247,f18]) ).
fof(f276,plain,
! [X0,X1] : join(X0,join(X1,converse(top))) = join(sK0,join(X0,join(X1,converse(top)))),
inference(superposition,[],[f224,f19]) ).
fof(f291,plain,
! [X0,X1] : join(top,join(converse(join(sK0,X0)),X1)) = join(join(top,converse(X0)),X1),
inference(superposition,[],[f19,f182]) ).
fof(f292,plain,
! [X0,X1] : join(top,join(converse(join(sK0,X0)),X1)) = join(top,join(converse(X0),X1)),
inference(forward_demodulation,[],[f291,f19]) ).
fof(f341,plain,
! [X0] : join(one,join(top,X0)) = join(one,join(X0,complement(sK0))),
inference(superposition,[],[f154,f18]) ).
fof(f365,plain,
! [X0,X1] : join(join(one,join(top,X0)),X1) = join(one,join(join(X0,complement(sK0)),X1)),
inference(superposition,[],[f19,f341]) ).
fof(f366,plain,
! [X0,X1] : join(join(one,join(top,X0)),X1) = join(one,join(X0,join(complement(sK0),X1))),
inference(forward_demodulation,[],[f365,f19]) ).
fof(f369,plain,
! [X0,X1] : join(one,join(join(top,X0),X1)) = join(one,join(X0,join(complement(sK0),X1))),
inference(forward_demodulation,[],[f366,f19]) ).
fof(f370,plain,
! [X0,X1] : join(one,join(top,join(X0,X1))) = join(one,join(X0,join(complement(sK0),X1))),
inference(forward_demodulation,[],[f369,f19]) ).
fof(f425,plain,
! [X2,X0,X1] : join(one,join(X2,join(X0,X1))) = join(one,join(X2,join(X0,join(X1,sK0)))),
inference(superposition,[],[f171,f19]) ).
fof(f462,plain,
! [X0] : join(one,join(X0,top)) = join(one,join(X0,complement(sK0))),
inference(superposition,[],[f175,f29]) ).
fof(f467,plain,
! [X0,X1] : join(one,join(join(sK0,X0),X1)) = join(one,join(X1,X0)),
inference(superposition,[],[f175,f18]) ).
fof(f487,plain,
! [X0,X1] : join(one,join(sK0,join(X0,X1))) = join(one,join(X1,X0)),
inference(forward_demodulation,[],[f467,f19]) ).
fof(f492,plain,
! [X0,X1] : join(one,join(X0,X1)) = join(one,join(X1,X0)),
inference(forward_demodulation,[],[f487,f114]) ).
fof(f496,plain,
! [X2,X0,X1] : join(one,join(X2,join(X0,X1))) = join(one,join(X0,join(X1,X2))),
inference(superposition,[],[f492,f19]) ).
fof(f506,plain,
! [X0,X1] : join(one,join(converse(X1),converse(X0))) = join(one,converse(join(X0,X1))),
inference(superposition,[],[f492,f26]) ).
fof(f548,plain,
! [X0,X1] : join(one,converse(join(X0,X1))) = join(one,converse(join(X1,X0))),
inference(forward_demodulation,[],[f506,f26]) ).
fof(f578,plain,
! [X0,X1] : join(one,join(join(X0,complement(sK0)),X1)) = join(join(one,join(X0,top)),X1),
inference(superposition,[],[f19,f462]) ).
fof(f579,plain,
! [X0,X1] : join(one,join(join(X0,complement(sK0)),X1)) = join(one,join(join(X0,top),X1)),
inference(forward_demodulation,[],[f578,f19]) ).
fof(f584,plain,
! [X0,X1] : join(one,join(join(X0,complement(sK0)),X1)) = join(one,join(X0,join(top,X1))),
inference(forward_demodulation,[],[f579,f19]) ).
fof(f585,plain,
! [X0,X1] : join(one,join(X0,join(complement(sK0),X1))) = join(one,join(X0,join(top,X1))),
inference(forward_demodulation,[],[f584,f19]) ).
fof(f785,plain,
! [X2,X0,X1] : join(one,converse(join(X2,join(X0,X1)))) = join(one,converse(join(X0,join(X1,X2)))),
inference(superposition,[],[f548,f19]) ).
fof(f802,plain,
! [X2,X0,X1] : join(one,join(converse(join(X1,X0)),X2)) = join(join(one,converse(join(X0,X1))),X2),
inference(superposition,[],[f19,f548]) ).
fof(f803,plain,
! [X2,X0,X1] : join(one,join(converse(join(X1,X0)),X2)) = join(one,join(converse(join(X0,X1)),X2)),
inference(forward_demodulation,[],[f802,f19]) ).
fof(f1138,plain,
! [X0] : join(top,join(X0,converse(complement(converse(converse(sK0)))))) = join(top,join(X0,converse(top))),
inference(superposition,[],[f202,f69]) ).
fof(f1140,plain,
! [X0,X1] : join(top,join(join(converse(sK0),X0),X1)) = join(top,join(X1,X0)),
inference(superposition,[],[f202,f18]) ).
fof(f1197,plain,
! [X0,X1] : join(top,join(converse(sK0),join(X0,X1))) = join(top,join(X1,X0)),
inference(forward_demodulation,[],[f1140,f19]) ).
fof(f1199,plain,
! [X0] : join(top,join(X0,converse(top))) = join(top,join(X0,converse(complement(sK0)))),
inference(forward_demodulation,[],[f1138,f25]) ).
fof(f1203,plain,
! [X0,X1] : join(top,join(X0,X1)) = join(top,join(X1,X0)),
inference(forward_demodulation,[],[f1197,f142]) ).
fof(f1207,plain,
! [X2,X0,X1] : join(top,join(X2,join(X0,X1))) = join(top,join(X0,join(X1,X2))),
inference(superposition,[],[f1203,f19]) ).
fof(f1266,plain,
! [X2,X0,X1] : join(join(top,join(X0,X1)),X2) = join(top,join(join(X1,X0),X2)),
inference(superposition,[],[f19,f1203]) ).
fof(f1267,plain,
! [X2,X0,X1] : join(join(top,join(X0,X1)),X2) = join(top,join(X1,join(X0,X2))),
inference(forward_demodulation,[],[f1266,f19]) ).
fof(f1279,plain,
! [X2,X0,X1] : join(top,join(join(X0,X1),X2)) = join(top,join(X1,join(X0,X2))),
inference(forward_demodulation,[],[f1267,f19]) ).
fof(f1285,plain,
! [X2,X0,X1] : join(top,join(X0,join(X1,X2))) = join(top,join(X1,join(X0,X2))),
inference(forward_demodulation,[],[f1279,f19]) ).
fof(f1641,plain,
! [X0] : join(top,converse(join(top,X0))) = join(complement(sK0),converse(join(top,X0))),
inference(superposition,[],[f212,f26]) ).
fof(f2110,plain,
! [X0] : join(top,join(converse(X0),converse(top))) = join(top,converse(join(X0,complement(sK0)))),
inference(superposition,[],[f1199,f26]) ).
fof(f2155,plain,
! [X0] : join(top,converse(join(X0,top))) = join(top,converse(join(X0,complement(sK0)))),
inference(forward_demodulation,[],[f2110,f26]) ).
fof(f2277,plain,
! [X0] : join(top,converse(join(X0,top))) = join(complement(sK0),converse(join(X0,top))),
inference(superposition,[],[f1641,f18]) ).
fof(f2284,plain,
! [X0] : converse(join(top,converse(join(top,X0)))) = join(converse(complement(sK0)),join(top,X0)),
inference(superposition,[],[f59,f1641]) ).
fof(f2287,plain,
! [X0] : join(converse(top),join(top,X0)) = join(converse(complement(sK0)),join(top,X0)),
inference(forward_demodulation,[],[f2284,f59]) ).
fof(f2526,plain,
! [X0] : converse(join(top,converse(join(X0,top)))) = join(converse(top),join(X0,complement(sK0))),
inference(superposition,[],[f59,f2155]) ).
fof(f2529,plain,
! [X0] : join(converse(top),join(X0,top)) = join(converse(top),join(X0,complement(sK0))),
inference(forward_demodulation,[],[f2526,f59]) ).
fof(f2608,plain,
! [X0] : converse(join(top,converse(join(X0,top)))) = join(converse(complement(sK0)),join(X0,top)),
inference(superposition,[],[f59,f2277]) ).
fof(f2611,plain,
! [X0] : join(converse(top),join(X0,top)) = join(converse(complement(sK0)),join(X0,top)),
inference(forward_demodulation,[],[f2608,f59]) ).
fof(f2664,plain,
! [X0] : join(converse(top),join(top,X0)) = join(join(top,X0),converse(complement(sK0))),
inference(superposition,[],[f18,f2287]) ).
fof(f2697,plain,
! [X0] : join(converse(top),join(top,X0)) = join(top,join(X0,converse(complement(sK0)))),
inference(forward_demodulation,[],[f2664,f19]) ).
fof(f2723,plain,
! [X0] : join(converse(top),join(top,X0)) = join(top,join(X0,converse(top))),
inference(forward_demodulation,[],[f2697,f1199]) ).
fof(f2771,plain,
! [X0] : join(converse(top),join(X0,top)) = join(top,join(X0,converse(top))),
inference(superposition,[],[f2723,f18]) ).
fof(f3273,plain,
! [X0] : join(top,join(X0,converse(top))) = join(converse(top),join(X0,complement(sK0))),
inference(forward_demodulation,[],[f2529,f2771]) ).
fof(f3298,plain,
! [X0] : join(top,converse(join(X0,complement(sK0)))) = converse(join(top,join(X0,converse(top)))),
inference(superposition,[],[f58,f3273]) ).
fof(f3312,plain,
! [X0] : join(top,converse(join(X0,top))) = converse(join(top,join(X0,converse(top)))),
inference(forward_demodulation,[],[f3298,f2155]) ).
fof(f3350,plain,
! [X0] : join(top,join(X0,converse(top))) = join(converse(complement(sK0)),join(X0,top)),
inference(forward_demodulation,[],[f2611,f2771]) ).
fof(f3503,plain,
! [X0] : join(top,join(X0,converse(top))) = join(join(X0,top),converse(complement(sK0))),
inference(superposition,[],[f18,f3350]) ).
fof(f3538,plain,
! [X0] : join(X0,join(top,converse(complement(sK0)))) = join(top,join(X0,converse(top))),
inference(forward_demodulation,[],[f3503,f19]) ).
fof(f3567,plain,
! [X0] : join(X0,join(top,converse(top))) = join(top,join(X0,converse(top))),
inference(forward_demodulation,[],[f3538,f190]) ).
fof(f3585,plain,
! [X0] : join(top,join(converse(top),X0)) = join(X0,join(top,converse(top))),
inference(superposition,[],[f3567,f18]) ).
fof(f3634,plain,
! [X0] : join(top,converse(join(X0,top))) = converse(join(X0,join(top,converse(top)))),
inference(superposition,[],[f3312,f3567]) ).
fof(f3795,plain,
! [X0] : join(X0,converse(join(top,converse(top)))) = converse(join(top,join(converse(top),converse(X0)))),
inference(superposition,[],[f58,f3585]) ).
fof(f3812,plain,
! [X0] : converse(join(top,converse(join(top,X0)))) = join(X0,converse(join(top,converse(top)))),
inference(forward_demodulation,[],[f3795,f26]) ).
fof(f3828,plain,
! [X0] : converse(join(top,converse(join(top,X0)))) = join(X0,join(converse(top),top)),
inference(forward_demodulation,[],[f3812,f59]) ).
fof(f3837,plain,
! [X0] : join(X0,join(top,converse(top))) = converse(join(top,converse(join(top,X0)))),
inference(forward_demodulation,[],[f3828,f18]) ).
fof(f3845,plain,
! [X0] : join(converse(top),join(top,X0)) = join(X0,join(top,converse(top))),
inference(forward_demodulation,[],[f3837,f59]) ).
fof(f5346,plain,
! [X0] : join(one,join(converse(top),converse(X0))) = join(one,converse(join(complement(converse(sK0)),X0))),
inference(superposition,[],[f219,f26]) ).
fof(f5409,plain,
! [X0] : join(one,converse(join(top,X0))) = join(one,converse(join(complement(converse(sK0)),X0))),
inference(forward_demodulation,[],[f5346,f26]) ).
fof(f5653,plain,
! [X0] : join(converse(one),join(complement(converse(sK0)),X0)) = converse(join(one,converse(join(top,X0)))),
inference(superposition,[],[f59,f5409]) ).
fof(f5656,plain,
! [X0] : join(converse(one),join(complement(converse(sK0)),X0)) = join(converse(one),join(top,X0)),
inference(forward_demodulation,[],[f5653,f59]) ).
fof(f5665,plain,
! [X0] : join(top,join(converse(one),X0)) = join(converse(one),join(top,X0)),
inference(forward_demodulation,[],[f5656,f231]) ).
fof(f5719,plain,
! [X0] : join(top,join(converse(one),X0)) = join(converse(one),join(X0,top)),
inference(superposition,[],[f5665,f18]) ).
fof(f5722,plain,
join(converse(one),converse(top)) = join(top,join(converse(one),converse(complement(converse(top))))),
inference(superposition,[],[f5665,f69]) ).
fof(f5730,plain,
! [X0] : join(one,converse(join(top,X0))) = converse(join(top,join(converse(one),X0))),
inference(superposition,[],[f58,f5665]) ).
fof(f5745,plain,
join(converse(one),converse(top)) = join(top,converse(join(one,complement(converse(top))))),
inference(forward_demodulation,[],[f5722,f26]) ).
fof(f5789,plain,
converse(join(one,top)) = join(top,converse(join(one,complement(converse(top))))),
inference(forward_demodulation,[],[f5745,f26]) ).
fof(f5924,plain,
converse(converse(join(one,top))) = join(converse(top),join(one,complement(converse(top)))),
inference(superposition,[],[f59,f5789]) ).
fof(f5926,plain,
join(one,top) = join(converse(top),join(one,complement(converse(top)))),
inference(forward_demodulation,[],[f5924,f25]) ).
fof(f5973,plain,
! [X0] : join(one,converse(join(top,X0))) = converse(join(top,join(X0,converse(one)))),
inference(superposition,[],[f5730,f18]) ).
fof(f5978,plain,
converse(join(top,converse(top))) = join(one,converse(join(top,converse(complement(converse(converse(one))))))),
inference(superposition,[],[f5730,f69]) ).
fof(f6031,plain,
converse(join(top,converse(top))) = join(one,join(converse(top),complement(converse(converse(one))))),
inference(forward_demodulation,[],[f5978,f59]) ).
fof(f6053,plain,
converse(join(top,converse(top))) = join(one,join(converse(top),complement(one))),
inference(forward_demodulation,[],[f6031,f25]) ).
fof(f6066,plain,
converse(join(top,converse(top))) = join(one,join(complement(one),converse(top))),
inference(forward_demodulation,[],[f6053,f492]) ).
fof(f6073,plain,
join(converse(top),top) = join(one,join(complement(one),converse(top))),
inference(forward_demodulation,[],[f6066,f59]) ).
fof(f6077,plain,
join(top,converse(top)) = join(one,join(complement(one),converse(top))),
inference(forward_demodulation,[],[f6073,f18]) ).
fof(f6081,plain,
! [X0] : join(join(top,converse(top)),X0) = join(one,join(join(complement(one),converse(top)),X0)),
inference(superposition,[],[f19,f6077]) ).
fof(f6082,plain,
! [X0] : join(join(top,converse(top)),X0) = join(one,join(complement(one),join(converse(top),X0))),
inference(forward_demodulation,[],[f6081,f19]) ).
fof(f6083,plain,
! [X0] : join(top,join(converse(top),X0)) = join(one,join(complement(one),join(converse(top),X0))),
inference(forward_demodulation,[],[f6082,f19]) ).
fof(f7470,plain,
! [X0,X1] : join(X0,converse(join(top,X1))) = join(sK0,join(X0,converse(join(top,X1)))),
inference(superposition,[],[f246,f18]) ).
fof(f7517,plain,
! [X0,X1] : join(X1,converse(join(X0,top))) = join(sK0,join(X1,converse(join(X0,top)))),
inference(superposition,[],[f276,f26]) ).
fof(f7773,plain,
! [X0,X1] : join(one,join(X0,top)) = join(one,join(X1,join(complement(X1),X0))),
inference(superposition,[],[f496,f29]) ).
fof(f9270,plain,
! [X0,X1] : join(one,join(X0,top)) = join(one,join(X1,join(X0,complement(X1)))),
inference(superposition,[],[f7773,f18]) ).
fof(f10830,plain,
! [X0] : join(top,top) = join(top,join(converse(X0),complement(converse(join(sK0,X0))))),
inference(superposition,[],[f292,f29]) ).
fof(f11055,plain,
! [X0] : join(top,top) = join(top,join(converse(X0),complement(converse(join(sK0,join(sK0,X0)))))),
inference(superposition,[],[f10830,f292]) ).
fof(f20874,plain,
! [X2,X0,X1] : join(top,join(X0,join(X1,X2))) = join(top,join(X0,join(X2,X1))),
inference(superposition,[],[f1285,f1207]) ).
fof(f40007,plain,
join(top,join(one,top)) = join(one,join(complement(one),join(one,top))),
inference(superposition,[],[f6083,f5926]) ).
fof(f40019,plain,
join(top,top) = join(one,join(complement(one),top)),
inference(superposition,[],[f6083,f29]) ).
fof(f40096,plain,
join(top,top) = join(one,join(top,complement(one))),
inference(forward_demodulation,[],[f40019,f492]) ).
fof(f40104,plain,
join(top,join(one,top)) = join(one,join(one,join(top,complement(one)))),
inference(forward_demodulation,[],[f40007,f496]) ).
fof(f40138,plain,
join(one,join(top,top)) = join(top,join(one,top)),
inference(forward_demodulation,[],[f40104,f9270]) ).
fof(f40182,plain,
! [X0] : join(join(top,top),X0) = join(one,join(join(top,complement(one)),X0)),
inference(superposition,[],[f19,f40096]) ).
fof(f40203,plain,
! [X0] : join(join(top,top),X0) = join(one,join(top,join(complement(one),X0))),
inference(forward_demodulation,[],[f40182,f19]) ).
fof(f40208,plain,
! [X0] : join(top,join(top,X0)) = join(one,join(top,join(complement(one),X0))),
inference(forward_demodulation,[],[f40203,f19]) ).
fof(f40233,plain,
! [X0] : join(top,join(join(one,top),X0)) = join(join(one,join(top,top)),X0),
inference(superposition,[],[f19,f40138]) ).
fof(f40254,plain,
! [X0] : join(top,join(join(one,top),X0)) = join(one,join(join(top,top),X0)),
inference(forward_demodulation,[],[f40233,f19]) ).
fof(f40266,plain,
! [X0] : join(top,join(join(one,top),X0)) = join(one,join(top,join(top,X0))),
inference(forward_demodulation,[],[f40254,f19]) ).
fof(f40277,plain,
! [X0] : join(top,join(one,join(top,X0))) = join(one,join(top,join(top,X0))),
inference(forward_demodulation,[],[f40266,f19]) ).
fof(f41073,plain,
! [X0] : join(one,join(top,join(X0,top))) = join(top,join(one,join(X0,top))),
inference(superposition,[],[f40277,f18]) ).
fof(f43549,plain,
! [X0] : join(top,top) = join(top,join(X0,complement(converse(join(sK0,join(sK0,converse(X0))))))),
inference(superposition,[],[f11055,f25]) ).
fof(f47534,plain,
! [X0] : join(top,top) = join(top,join(join(top,X0),complement(converse(join(sK0,converse(join(top,X0))))))),
inference(superposition,[],[f43549,f7470]) ).
fof(f47535,plain,
! [X0] : join(top,top) = join(top,join(join(X0,top),complement(converse(join(sK0,converse(join(X0,top))))))),
inference(superposition,[],[f43549,f7517]) ).
fof(f47693,plain,
! [X0] : join(top,top) = join(top,join(X0,join(top,complement(converse(join(sK0,converse(join(X0,top)))))))),
inference(forward_demodulation,[],[f47535,f19]) ).
fof(f47694,plain,
! [X0] : join(top,top) = join(top,join(top,join(X0,complement(converse(join(sK0,converse(join(top,X0)))))))),
inference(forward_demodulation,[],[f47534,f19]) ).
fof(f47752,plain,
! [X0] : join(top,top) = join(top,join(X0,join(top,complement(join(converse(sK0),join(X0,top)))))),
inference(forward_demodulation,[],[f47693,f59]) ).
fof(f47753,plain,
! [X0] : join(top,top) = join(top,join(top,join(X0,complement(join(converse(sK0),join(top,X0)))))),
inference(forward_demodulation,[],[f47694,f59]) ).
fof(f47789,plain,
! [X0] : join(top,top) = join(top,join(X0,join(top,complement(join(X0,top))))),
inference(forward_demodulation,[],[f47752,f256]) ).
fof(f47790,plain,
! [X0] : join(top,top) = join(top,join(top,join(X0,complement(join(top,X0))))),
inference(forward_demodulation,[],[f47753,f247]) ).
fof(f47884,plain,
join(top,top) = join(one,join(top,join(top,complement(join(one,top))))),
inference(superposition,[],[f47789,f40277]) ).
fof(f48834,plain,
! [X0,X1] : complement(X1) = join(complement(X1),composition(converse(X0),complement(composition(X0,X1)))),
inference(forward_demodulation,[],[f28,f18]) ).
fof(f71297,plain,
! [X0,X1] : join(one,join(X0,join(complement(X0),X1))) = join(one,join(join(X1,sK0),top)),
inference(superposition,[],[f7773,f425]) ).
fof(f71465,plain,
! [X0,X1] : join(one,join(X0,join(complement(X0),X1))) = join(one,join(top,join(X1,sK0))),
inference(forward_demodulation,[],[f71297,f492]) ).
fof(f71693,plain,
! [X0,X1] : join(one,join(X0,join(complement(X0),X1))) = join(one,join(top,X1)),
inference(forward_demodulation,[],[f71465,f171]) ).
fof(f71843,plain,
! [X0,X1] : join(one,join(top,X0)) = join(one,join(X1,join(X0,complement(X1)))),
inference(superposition,[],[f71693,f18]) ).
fof(f84795,plain,
! [X0,X1] : join(one,converse(join(X0,top))) = join(one,converse(join(X1,join(complement(X1),X0)))),
inference(superposition,[],[f785,f29]) ).
fof(f89947,plain,
! [X0,X1] : join(one,converse(join(X0,top))) = join(one,converse(join(X1,join(X0,complement(X1))))),
inference(superposition,[],[f84795,f18]) ).
fof(f90961,plain,
! [X0,X1] : converse(join(one,converse(join(X0,top)))) = join(converse(one),join(X1,join(X0,complement(X1)))),
inference(superposition,[],[f59,f89947]) ).
fof(f90985,plain,
! [X0,X1] : join(converse(one),join(X0,top)) = join(converse(one),join(X1,join(X0,complement(X1)))),
inference(forward_demodulation,[],[f90961,f59]) ).
fof(f91047,plain,
! [X0,X1] : join(top,join(converse(one),X0)) = join(converse(one),join(X1,join(X0,complement(X1)))),
inference(forward_demodulation,[],[f90985,f5719]) ).
fof(f92555,plain,
! [X0,X1] : join(one,top) = join(one,join(converse(join(X1,X0)),complement(converse(join(X0,X1))))),
inference(superposition,[],[f803,f29]) ).
fof(f92631,plain,
! [X0,X1] : join(one,converse(top)) = join(one,join(converse(join(X0,X1)),converse(complement(converse(converse(join(X1,X0))))))),
inference(superposition,[],[f803,f69]) ).
fof(f93162,plain,
! [X0,X1] : join(one,converse(top)) = join(one,converse(join(join(X0,X1),complement(converse(converse(join(X1,X0))))))),
inference(forward_demodulation,[],[f92631,f26]) ).
fof(f93384,plain,
! [X0,X1] : join(one,converse(top)) = join(one,converse(join(X0,join(X1,complement(converse(converse(join(X1,X0)))))))),
inference(forward_demodulation,[],[f93162,f19]) ).
fof(f93533,plain,
! [X0,X1] : join(one,converse(top)) = join(one,converse(join(X0,join(X1,complement(join(X1,X0)))))),
inference(forward_demodulation,[],[f93384,f25]) ).
fof(f93707,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))) = X0,
inference(forward_demodulation,[],[f20,f18]) ).
fof(f94388,plain,
! [X0,X1] : join(one,top) = join(one,join(converse(join(converse(X1),converse(X0))),complement(converse(converse(join(X0,X1)))))),
inference(superposition,[],[f92555,f26]) ).
fof(f95096,plain,
! [X0,X1] : join(one,top) = join(one,join(complement(converse(converse(join(X0,X1)))),converse(join(converse(X1),converse(X0))))),
inference(forward_demodulation,[],[f94388,f492]) ).
fof(f96093,plain,
! [X0,X1] : join(one,top) = join(one,join(complement(converse(converse(join(X0,X1)))),join(X1,converse(converse(X0))))),
inference(forward_demodulation,[],[f95096,f58]) ).
fof(f97020,plain,
! [X0,X1] : join(one,top) = join(one,join(X1,join(converse(converse(X0)),complement(converse(converse(join(X0,X1))))))),
inference(forward_demodulation,[],[f96093,f496]) ).
fof(f97666,plain,
! [X0,X1] : join(one,top) = join(one,join(X1,join(converse(converse(X0)),complement(join(X0,X1))))),
inference(forward_demodulation,[],[f97020,f25]) ).
fof(f98102,plain,
! [X0,X1] : join(one,top) = join(one,join(X1,join(X0,complement(join(X0,X1))))),
inference(forward_demodulation,[],[f97666,f25]) ).
fof(f99017,plain,
! [X0,X1] : join(one,top) = join(one,join(X0,join(X1,complement(join(X0,X1))))),
inference(superposition,[],[f98102,f18]) ).
fof(f99561,plain,
! [X0] : join(one,top) = join(one,join(X0,join(top,complement(join(complement(sK0),X0))))),
inference(superposition,[],[f98102,f585]) ).
fof(f99562,plain,
! [X0] : join(one,top) = join(one,join(top,join(X0,complement(join(complement(sK0),X0))))),
inference(superposition,[],[f98102,f370]) ).
fof(f99564,plain,
! [X0] : join(one,top) = join(one,join(X0,complement(join(sK0,X0)))),
inference(superposition,[],[f98102,f175]) ).
fof(f99585,plain,
! [X0] : join(one,top) = join(one,join(X0,complement(join(X0,sK0)))),
inference(superposition,[],[f98102,f114]) ).
fof(f101683,plain,
! [X0,X1] : join(join(one,top),X1) = join(one,join(join(X0,complement(join(sK0,X0))),X1)),
inference(superposition,[],[f19,f99564]) ).
fof(f101716,plain,
! [X0,X1] : join(join(one,top),X1) = join(one,join(X0,join(complement(join(sK0,X0)),X1))),
inference(forward_demodulation,[],[f101683,f19]) ).
fof(f101767,plain,
! [X0,X1] : join(one,join(top,X1)) = join(one,join(X0,join(complement(join(sK0,X0)),X1))),
inference(forward_demodulation,[],[f101716,f19]) ).
fof(f101917,plain,
! [X0] : join(top,join(one,top)) = join(top,join(X0,join(one,complement(join(X0,sK0))))),
inference(superposition,[],[f1285,f99585]) ).
fof(f101950,plain,
! [X0,X1] : join(join(one,top),X1) = join(one,join(join(X0,complement(join(X0,sK0))),X1)),
inference(superposition,[],[f19,f99585]) ).
fof(f101983,plain,
! [X0,X1] : join(join(one,top),X1) = join(one,join(X0,join(complement(join(X0,sK0)),X1))),
inference(forward_demodulation,[],[f101950,f19]) ).
fof(f102004,plain,
! [X0] : join(one,join(top,top)) = join(top,join(X0,join(one,complement(join(X0,sK0))))),
inference(forward_demodulation,[],[f101917,f40138]) ).
fof(f102039,plain,
! [X0,X1] : join(one,join(top,X1)) = join(one,join(X0,join(complement(join(X0,sK0)),X1))),
inference(forward_demodulation,[],[f101983,f19]) ).
fof(f107553,plain,
join(one,top) = join(top,join(top,complement(join(complement(sK0),complement(one))))),
inference(superposition,[],[f40208,f99562]) ).
fof(f107655,plain,
join(one,top) = join(top,join(top,complement(join(complement(one),complement(sK0))))),
inference(forward_demodulation,[],[f107553,f18]) ).
fof(f109970,plain,
! [X0,X1] : join(one,converse(top)) = join(one,converse(join(X0,join(X1,complement(join(X0,X1)))))),
inference(superposition,[],[f93533,f18]) ).
fof(f110568,plain,
! [X0,X1] : converse(join(one,converse(top))) = join(converse(one),join(X0,join(X1,complement(join(X1,X0))))),
inference(superposition,[],[f59,f93533]) ).
fof(f110600,plain,
! [X0,X1] : join(converse(one),top) = join(converse(one),join(X0,join(X1,complement(join(X1,X0))))),
inference(forward_demodulation,[],[f110568,f59]) ).
fof(f111187,plain,
! [X0,X1] : join(top,converse(one)) = join(converse(one),join(X0,join(X1,complement(join(X1,X0))))),
inference(forward_demodulation,[],[f110600,f18]) ).
fof(f130557,plain,
! [X0] : join(one,join(top,complement(X0))) = join(one,join(top,complement(join(sK0,X0)))),
inference(superposition,[],[f101767,f71843]) ).
fof(f131295,plain,
! [X0] : join(one,join(top,complement(X0))) = join(one,join(top,complement(join(X0,sK0)))),
inference(superposition,[],[f130557,f18]) ).
fof(f137767,plain,
sK0 = join(complement(join(top,converse(top))),complement(join(complement(sK0),complement(converse(top))))),
inference(superposition,[],[f93707,f209]) ).
fof(f137799,plain,
! [X0] : join(one,join(complement(X0),X0)) = join(one,join(top,complement(join(complement(X0),complement(sK0))))),
inference(superposition,[],[f102039,f93707]) ).
fof(f137860,plain,
! [X0] : join(one,join(X0,complement(X0))) = join(one,join(top,complement(join(complement(X0),complement(sK0))))),
inference(forward_demodulation,[],[f137799,f492]) ).
fof(f137885,plain,
! [X0] : join(one,top) = join(one,join(top,complement(join(complement(X0),complement(sK0))))),
inference(forward_demodulation,[],[f137860,f29]) ).
fof(f137913,plain,
! [X0] : join(one,top) = join(one,join(top,complement(join(complement(sK0),complement(X0))))),
inference(superposition,[],[f137885,f18]) ).
fof(f138144,plain,
join(one,join(top,complement(join(complement(sK0),complement(converse(top)))))) = join(one,join(join(top,converse(top)),sK0)),
inference(superposition,[],[f71693,f137767]) ).
fof(f138202,plain,
join(one,join(top,converse(top))) = join(one,join(top,complement(join(complement(sK0),complement(converse(top)))))),
inference(forward_demodulation,[],[f138144,f145]) ).
fof(f138223,plain,
join(one,top) = join(one,join(top,converse(top))),
inference(forward_demodulation,[],[f138202,f137913]) ).
fof(f138285,plain,
join(one,top) = join(one,join(converse(join(join(top,converse(top)),one)),complement(converse(join(one,top))))),
inference(superposition,[],[f92555,f138223]) ).
fof(f138302,plain,
join(one,top) = join(one,join(complement(converse(join(one,top))),converse(join(join(top,converse(top)),one)))),
inference(forward_demodulation,[],[f138285,f492]) ).
fof(f138332,plain,
join(one,top) = join(one,join(complement(converse(join(one,top))),converse(join(one,join(top,converse(top)))))),
inference(forward_demodulation,[],[f138302,f18]) ).
fof(f138346,plain,
join(one,top) = join(one,join(complement(converse(join(one,top))),join(top,converse(join(one,top))))),
inference(forward_demodulation,[],[f138332,f3634]) ).
fof(f138353,plain,
join(one,top) = join(one,join(top,join(converse(join(one,top)),complement(converse(join(one,top)))))),
inference(forward_demodulation,[],[f138346,f496]) ).
fof(f138358,plain,
join(one,top) = join(one,join(top,top)),
inference(forward_demodulation,[],[f138353,f29]) ).
fof(f138385,plain,
! [X0] : join(join(one,top),X0) = join(one,join(join(top,top),X0)),
inference(superposition,[],[f19,f138358]) ).
fof(f138406,plain,
join(one,converse(top)) = join(one,converse(join(one,join(join(top,top),complement(join(one,top)))))),
inference(superposition,[],[f109970,f138358]) ).
fof(f138411,plain,
join(one,converse(top)) = join(one,converse(join(one,join(top,join(top,complement(join(one,top))))))),
inference(forward_demodulation,[],[f138406,f19]) ).
fof(f138430,plain,
! [X0] : join(join(one,top),X0) = join(one,join(top,join(top,X0))),
inference(forward_demodulation,[],[f138385,f19]) ).
fof(f138443,plain,
join(one,converse(top)) = join(one,converse(join(top,top))),
inference(forward_demodulation,[],[f138411,f47884]) ).
fof(f138456,plain,
! [X0] : join(one,join(top,X0)) = join(one,join(top,join(top,X0))),
inference(forward_demodulation,[],[f138430,f19]) ).
fof(f139534,plain,
join(one,converse(top)) = join(one,join(top,converse(top))),
inference(superposition,[],[f138456,f69]) ).
fof(f139571,plain,
join(one,join(one,top)) = join(one,join(top,complement(join(complement(one),complement(sK0))))),
inference(superposition,[],[f138456,f107655]) ).
fof(f140053,plain,
join(one,top) = join(one,join(one,top)),
inference(forward_demodulation,[],[f139571,f137885]) ).
fof(f140084,plain,
join(one,converse(top)) = join(one,top),
inference(forward_demodulation,[],[f139534,f138223]) ).
fof(f140254,plain,
join(converse(one),top) = converse(join(one,top)),
inference(superposition,[],[f59,f140084]) ).
fof(f140298,plain,
join(top,converse(one)) = converse(join(one,top)),
inference(forward_demodulation,[],[f140254,f18]) ).
fof(f140385,plain,
join(one,converse(top)) = join(one,converse(join(one,join(join(one,top),complement(join(one,top)))))),
inference(superposition,[],[f109970,f140053]) ).
fof(f140386,plain,
join(top,converse(one)) = join(converse(one),join(join(one,top),join(one,complement(join(one,top))))),
inference(superposition,[],[f111187,f140053]) ).
fof(f140389,plain,
join(top,converse(one)) = join(top,join(converse(one),one)),
inference(forward_demodulation,[],[f140386,f91047]) ).
fof(f140390,plain,
join(one,converse(top)) = join(one,converse(join(one,top))),
inference(forward_demodulation,[],[f140385,f29]) ).
fof(f140419,plain,
join(top,converse(one)) = join(top,join(one,converse(one))),
inference(forward_demodulation,[],[f140389,f1203]) ).
fof(f140420,plain,
join(one,top) = join(one,converse(join(one,top))),
inference(forward_demodulation,[],[f140390,f140084]) ).
fof(f140794,plain,
join(one,top) = join(one,join(top,converse(one))),
inference(forward_demodulation,[],[f140420,f140298]) ).
fof(f141276,plain,
join(top,top) = join(top,join(top,join(join(one,converse(one)),complement(join(top,converse(one)))))),
inference(superposition,[],[f47790,f140419]) ).
fof(f141291,plain,
join(top,join(top,converse(one))) = join(top,join(one,join(top,converse(one)))),
inference(superposition,[],[f1285,f140419]) ).
fof(f141336,plain,
join(top,join(top,converse(one))) = join(one,join(top,join(top,converse(one)))),
inference(forward_demodulation,[],[f141291,f40277]) ).
fof(f141347,plain,
join(top,top) = join(top,join(top,join(one,join(converse(one),complement(join(top,converse(one))))))),
inference(forward_demodulation,[],[f141276,f19]) ).
fof(f141373,plain,
join(top,join(top,converse(one))) = join(one,join(top,converse(one))),
inference(forward_demodulation,[],[f141336,f138456]) ).
fof(f141382,plain,
join(top,top) = join(top,join(one,join(join(converse(one),complement(join(top,converse(one)))),top))),
inference(forward_demodulation,[],[f141347,f1207]) ).
fof(f141407,plain,
join(one,top) = join(top,join(top,converse(one))),
inference(forward_demodulation,[],[f141373,f140794]) ).
fof(f141415,plain,
join(top,top) = join(top,join(one,join(top,join(converse(one),complement(join(top,converse(one))))))),
inference(forward_demodulation,[],[f141382,f20874]) ).
fof(f141443,plain,
join(top,top) = join(one,join(top,join(top,join(converse(one),complement(join(top,converse(one))))))),
inference(forward_demodulation,[],[f141415,f40277]) ).
fof(f141464,plain,
join(top,top) = join(one,join(top,join(converse(one),complement(join(top,converse(one)))))),
inference(forward_demodulation,[],[f141443,f138456]) ).
fof(f141482,plain,
join(one,top) = join(top,top),
inference(forward_demodulation,[],[f141464,f99017]) ).
fof(f141589,plain,
! [X0] : join(join(one,top),X0) = join(top,join(top,X0)),
inference(superposition,[],[f19,f141482]) ).
fof(f141629,plain,
! [X0] : join(one,join(top,X0)) = join(top,join(top,X0)),
inference(forward_demodulation,[],[f141589,f19]) ).
fof(f141703,plain,
converse(join(one,top)) = join(one,converse(join(top,top))),
inference(superposition,[],[f5973,f141407]) ).
fof(f141799,plain,
join(one,converse(top)) = converse(join(one,top)),
inference(forward_demodulation,[],[f141703,f138443]) ).
fof(f141833,plain,
join(one,top) = converse(join(one,top)),
inference(forward_demodulation,[],[f141799,f140084]) ).
fof(f142147,plain,
converse(top) = join(join(one,top),converse(complement(join(one,top)))),
inference(superposition,[],[f69,f141833]) ).
fof(f142185,plain,
converse(top) = join(one,join(top,converse(complement(join(one,top))))),
inference(forward_demodulation,[],[f142147,f19]) ).
fof(f142943,plain,
join(one,converse(top)) = join(top,converse(top)),
inference(superposition,[],[f141629,f69]) ).
fof(f143839,plain,
join(one,top) = join(top,converse(top)),
inference(forward_demodulation,[],[f142943,f140084]) ).
fof(f152800,plain,
join(top,converse(top)) = join(one,join(top,join(top,converse(complement(join(one,top)))))),
inference(superposition,[],[f40277,f142185]) ).
fof(f152864,plain,
join(top,converse(top)) = join(one,join(top,converse(complement(join(one,top))))),
inference(forward_demodulation,[],[f152800,f138456]) ).
fof(f152889,plain,
converse(top) = join(top,converse(top)),
inference(forward_demodulation,[],[f152864,f142185]) ).
fof(f152995,plain,
converse(converse(top)) = join(converse(top),top),
inference(superposition,[],[f59,f152889]) ).
fof(f153043,plain,
converse(converse(top)) = join(top,converse(top)),
inference(forward_demodulation,[],[f152995,f18]) ).
fof(f153098,plain,
converse(converse(top)) = join(one,top),
inference(forward_demodulation,[],[f153043,f143839]) ).
fof(f153133,plain,
top = join(one,top),
inference(forward_demodulation,[],[f153098,f25]) ).
fof(f153202,plain,
top = converse(top),
inference(superposition,[],[f141833,f153133]) ).
fof(f153247,plain,
! [X0] : join(top,X0) = join(one,join(top,X0)),
inference(superposition,[],[f19,f153133]) ).
fof(f153439,plain,
! [X0] : join(top,join(top,X0)) = join(X0,join(top,top)),
inference(superposition,[],[f3845,f153202]) ).
fof(f153516,plain,
! [X0] : converse(composition(top,X0)) = composition(converse(X0),top),
inference(superposition,[],[f27,f153202]) ).
fof(f153618,plain,
! [X0] : join(top,join(top,X0)) = join(X0,join(one,top)),
inference(forward_demodulation,[],[f153439,f141482]) ).
fof(f153681,plain,
! [X0] : join(X0,top) = join(top,join(top,X0)),
inference(forward_demodulation,[],[f153618,f153133]) ).
fof(f156046,plain,
! [X0] : join(one,top) = join(top,complement(join(complement(sK0),complement(X0)))),
inference(superposition,[],[f137913,f153247]) ).
fof(f156529,plain,
! [X0] : top = join(top,complement(join(complement(sK0),complement(X0)))),
inference(forward_demodulation,[],[f156046,f153133]) ).
fof(f168082,plain,
! [X0] : join(top,join(one,join(top,top))) = join(join(X0,join(one,complement(join(X0,sK0)))),top),
inference(superposition,[],[f153681,f102004]) ).
fof(f169582,plain,
! [X0] : join(top,join(one,join(top,top))) = join(X0,join(join(one,complement(join(X0,sK0))),top)),
inference(forward_demodulation,[],[f168082,f19]) ).
fof(f170263,plain,
! [X0] : join(top,join(one,join(top,top))) = join(X0,join(one,join(complement(join(X0,sK0)),top))),
inference(forward_demodulation,[],[f169582,f19]) ).
fof(f170822,plain,
! [X0] : join(top,join(one,join(top,top))) = join(X0,join(one,join(top,complement(join(X0,sK0))))),
inference(forward_demodulation,[],[f170263,f492]) ).
fof(f171159,plain,
! [X0] : join(top,join(one,join(top,top))) = join(X0,join(one,join(top,complement(X0)))),
inference(forward_demodulation,[],[f170822,f131295]) ).
fof(f171342,plain,
! [X0] : join(top,join(one,join(top,top))) = join(X0,join(top,complement(X0))),
inference(forward_demodulation,[],[f171159,f153247]) ).
fof(f171443,plain,
! [X0] : join(one,join(top,join(top,top))) = join(X0,join(top,complement(X0))),
inference(forward_demodulation,[],[f171342,f41073]) ).
fof(f171517,plain,
! [X0] : join(one,join(top,top)) = join(X0,join(top,complement(X0))),
inference(forward_demodulation,[],[f171443,f138456]) ).
fof(f171561,plain,
! [X0] : join(one,top) = join(X0,join(top,complement(X0))),
inference(forward_demodulation,[],[f171517,f138358]) ).
fof(f171579,plain,
! [X0] : top = join(X0,join(top,complement(X0))),
inference(forward_demodulation,[],[f171561,f153133]) ).
fof(f207618,plain,
! [X0] : join(one,top) = join(one,join(complement(X0),top)),
inference(superposition,[],[f99561,f156529]) ).
fof(f207740,plain,
! [X0] : join(one,top) = join(one,join(top,complement(X0))),
inference(forward_demodulation,[],[f207618,f492]) ).
fof(f207790,plain,
! [X0] : join(one,top) = join(top,complement(X0)),
inference(forward_demodulation,[],[f207740,f153247]) ).
fof(f207830,plain,
! [X0] : top = join(top,complement(X0)),
inference(forward_demodulation,[],[f207790,f153133]) ).
fof(f207911,plain,
! [X0] : top = join(X0,top),
inference(superposition,[],[f171579,f207830]) ).
fof(f208399,plain,
! [X0] : top = join(top,X0),
inference(superposition,[],[f207911,f18]) ).
fof(f208540,plain,
! [X0] : join(complement(top),complement(join(complement(X0),complement(top)))) = X0,
inference(superposition,[],[f93707,f207911]) ).
fof(f208735,plain,
! [X0] : join(zero,complement(join(complement(X0),zero))) = X0,
inference(forward_demodulation,[],[f208540,f56]) ).
fof(f208860,plain,
! [X0] : join(zero,complement(join(zero,complement(X0)))) = X0,
inference(forward_demodulation,[],[f208735,f18]) ).
fof(f210940,plain,
zero = join(zero,complement(top)),
inference(superposition,[],[f208860,f29]) ).
fof(f211021,plain,
zero = join(zero,zero),
inference(forward_demodulation,[],[f210940,f56]) ).
fof(f211073,plain,
! [X0] : join(zero,X0) = join(zero,join(zero,X0)),
inference(superposition,[],[f19,f211021]) ).
fof(f211136,plain,
! [X0] : join(zero,X0) = X0,
inference(superposition,[],[f211073,f208860]) ).
fof(f211366,plain,
! [X0] : join(X0,zero) = X0,
inference(superposition,[],[f211136,f18]) ).
fof(f211388,plain,
! [X0] : join(zero,complement(complement(X0))) = X0,
inference(superposition,[],[f208860,f211136]) ).
fof(f212146,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_demodulation,[],[f211388,f211136]) ).
fof(f213523,plain,
( complement(join(complement(one),complement(complement(composition(sK0,top))))) != join(complement(join(complement(one),sK0)),complement(join(complement(one),complement(complement(composition(sK0,top))))))
| spl1_1 ),
inference(superposition,[],[f52,f212146]) ).
fof(f213650,plain,
( complement(join(complement(one),composition(sK0,top))) != join(complement(join(complement(one),sK0)),complement(join(complement(one),composition(sK0,top))))
| spl1_1 ),
inference(forward_demodulation,[],[f213523,f212146]) ).
fof(f213688,plain,
( complement(join(complement(one),composition(sK0,top))) != join(complement(join(sK0,complement(one))),complement(join(complement(one),composition(sK0,top))))
| spl1_1 ),
inference(forward_demodulation,[],[f213650,f18]) ).
fof(f278035,plain,
! [X0,X1] : top = join(X0,join(complement(X0),X1)),
inference(forward_demodulation,[],[f109,f208399]) ).
fof(f278065,plain,
! [X0,X1] : top = join(join(complement(X0),X1),X0),
inference(superposition,[],[f278035,f93707]) ).
fof(f278067,plain,
! [X0,X1] : top = join(X1,join(X0,complement(X1))),
inference(superposition,[],[f278035,f18]) ).
fof(f278483,plain,
! [X0,X1] : join(complement(top),complement(join(complement(X0),complement(join(complement(complement(X0)),X1))))) = X0,
inference(superposition,[],[f93707,f278035]) ).
fof(f279207,plain,
! [X0,X1] : join(complement(top),complement(join(complement(X0),complement(join(X0,X1))))) = X0,
inference(forward_demodulation,[],[f278483,f212146]) ).
fof(f279401,plain,
! [X0,X1] : top = join(complement(X0),join(X1,X0)),
inference(forward_demodulation,[],[f278065,f19]) ).
fof(f279591,plain,
! [X0,X1] : join(zero,complement(join(complement(X0),complement(join(X0,X1))))) = X0,
inference(forward_demodulation,[],[f279207,f56]) ).
fof(f279806,plain,
! [X0,X1] : complement(join(complement(X0),complement(join(X0,X1)))) = X0,
inference(forward_demodulation,[],[f279591,f211136]) ).
fof(f280368,plain,
! [X0,X1] : join(complement(top),complement(join(complement(X0),complement(join(X1,complement(complement(X0))))))) = X0,
inference(superposition,[],[f93707,f278067]) ).
fof(f280916,plain,
! [X0,X1] : join(complement(top),complement(join(complement(X0),complement(join(X1,X0))))) = X0,
inference(forward_demodulation,[],[f280368,f212146]) ).
fof(f281251,plain,
! [X0,X1] : join(zero,complement(join(complement(X0),complement(join(X1,X0))))) = X0,
inference(forward_demodulation,[],[f280916,f56]) ).
fof(f281462,plain,
! [X0,X1] : complement(join(complement(X0),complement(join(X1,X0)))) = X0,
inference(forward_demodulation,[],[f281251,f211136]) ).
fof(f281724,plain,
! [X0,X1] : top = join(complement(composition(converse(X1),complement(composition(X1,X0)))),complement(X0)),
inference(superposition,[],[f279401,f48834]) ).
fof(f281731,plain,
! [X2,X0,X1] : top = join(complement(composition(X1,X2)),composition(join(X0,X1),X2)),
inference(superposition,[],[f279401,f24]) ).
fof(f283567,plain,
! [X0,X1] : top = join(complement(X0),complement(composition(converse(X1),complement(composition(X1,X0))))),
inference(forward_demodulation,[],[f281724,f18]) ).
fof(f288305,plain,
! [X0] : top = join(X0,join(converse(complement(converse(X0))),complement(converse(top)))),
inference(superposition,[],[f118,f69]) ).
fof(f289322,plain,
! [X0,X1] : join(complement(top),complement(join(complement(X0),complement(join(X1,complement(join(complement(X0),X1))))))) = X0,
inference(superposition,[],[f93707,f118]) ).
fof(f289839,plain,
! [X0,X1] : join(zero,complement(join(complement(X0),complement(join(X1,complement(join(complement(X0),X1))))))) = X0,
inference(forward_demodulation,[],[f289322,f56]) ).
fof(f290378,plain,
! [X0] : top = join(X0,join(complement(converse(top)),converse(complement(converse(X0))))),
inference(forward_demodulation,[],[f288305,f18]) ).
fof(f290520,plain,
! [X0,X1] : complement(join(complement(X0),complement(join(X1,complement(join(complement(X0),X1)))))) = X0,
inference(forward_demodulation,[],[f289839,f211136]) ).
fof(f290963,plain,
! [X0] : top = join(X0,join(complement(top),converse(complement(converse(X0))))),
inference(forward_demodulation,[],[f290378,f153202]) ).
fof(f291344,plain,
! [X0] : top = join(X0,join(zero,converse(complement(converse(X0))))),
inference(forward_demodulation,[],[f290963,f56]) ).
fof(f291562,plain,
! [X0] : top = join(X0,converse(complement(converse(X0)))),
inference(forward_demodulation,[],[f291344,f211136]) ).
fof(f291860,plain,
! [X0] : join(complement(top),complement(join(complement(X0),complement(converse(complement(converse(complement(X0)))))))) = X0,
inference(superposition,[],[f93707,f291562]) ).
fof(f292202,plain,
! [X0] : join(zero,complement(join(complement(X0),complement(converse(complement(converse(complement(X0)))))))) = X0,
inference(forward_demodulation,[],[f291860,f56]) ).
fof(f292421,plain,
! [X0] : complement(join(complement(X0),complement(converse(complement(converse(complement(X0))))))) = X0,
inference(forward_demodulation,[],[f292202,f211136]) ).
fof(f294078,plain,
! [X0] : complement(X0) = complement(join(complement(complement(X0)),complement(complement(X0)))),
inference(superposition,[],[f279806,f48834]) ).
fof(f295300,plain,
! [X0] : complement(X0) = complement(join(X0,X0)),
inference(forward_demodulation,[],[f294078,f212146]) ).
fof(f296436,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))) = join(X0,X0),
inference(superposition,[],[f93707,f295300]) ).
fof(f296496,plain,
! [X0] : join(X0,X0) = X0,
inference(forward_demodulation,[],[f296436,f93707]) ).
fof(f296733,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X0,X1)),
inference(superposition,[],[f19,f296496]) ).
fof(f299004,plain,
! [X0,X1] : join(X0,X1) = join(X1,join(X0,X1)),
inference(superposition,[],[f296733,f18]) ).
fof(f299029,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),X0) = X0,
inference(superposition,[],[f296733,f93707]) ).
fof(f301755,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),X1))) = X0,
inference(forward_demodulation,[],[f299029,f18]) ).
fof(f307690,plain,
! [X0,X1] : join(X1,complement(join(X0,complement(X1)))) = X1,
inference(superposition,[],[f301755,f18]) ).
fof(f308842,plain,
! [X0,X1] : join(X0,X1) = join(join(X0,X1),X0),
inference(superposition,[],[f307690,f279806]) ).
fof(f309378,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X1,X0)),
inference(forward_demodulation,[],[f308842,f19]) ).
fof(f310644,plain,
! [X0,X1] : join(join(X0,X1),join(X0,X1)) = join(join(X0,X1),X0),
inference(superposition,[],[f309378,f296733]) ).
fof(f313127,plain,
! [X0,X1] : join(join(X0,X1),join(X0,X1)) = join(X0,join(X1,X0)),
inference(forward_demodulation,[],[f310644,f19]) ).
fof(f314041,plain,
! [X0,X1] : join(X1,X0) = join(join(X0,X1),join(X0,X1)),
inference(forward_demodulation,[],[f313127,f299004]) ).
fof(f314772,plain,
! [X0,X1] : join(X1,X0) = join(X0,join(X1,join(X0,X1))),
inference(forward_demodulation,[],[f314041,f19]) ).
fof(f315375,plain,
! [X0,X1] : join(X1,X0) = join(X0,join(X0,X1)),
inference(forward_demodulation,[],[f314772,f299004]) ).
fof(f319184,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X1,join(join(X1,X0),X2)),
inference(superposition,[],[f19,f315375]) ).
fof(f319445,plain,
! [X0,X1] : converse(join(X0,converse(X1))) = join(X1,converse(join(converse(X1),X0))),
inference(superposition,[],[f58,f315375]) ).
fof(f320181,plain,
! [X0,X1] : converse(join(X0,converse(X1))) = join(X1,join(X1,converse(X0))),
inference(forward_demodulation,[],[f319445,f58]) ).
fof(f320368,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X1,join(X1,join(X0,X2))),
inference(forward_demodulation,[],[f319184,f19]) ).
fof(f321744,plain,
! [X0,X1] : join(X1,converse(X0)) = converse(join(X0,converse(X1))),
inference(forward_demodulation,[],[f320181,f296733]) ).
fof(f321900,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X1,join(X0,X2)),
inference(forward_demodulation,[],[f320368,f296733]) ).
fof(f335874,plain,
! [X2,X0,X1] : join(complement(X0),complement(join(X1,X0))) = complement(join(X0,complement(join(join(complement(X0),complement(join(X1,X0))),X2)))),
inference(superposition,[],[f279806,f281462]) ).
fof(f335885,plain,
! [X2,X0,X1] : join(complement(X0),complement(join(X1,X0))) = complement(join(X0,complement(join(complement(X0),join(complement(join(X1,X0)),X2))))),
inference(forward_demodulation,[],[f335874,f19]) ).
fof(f336739,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X1,X0))),
inference(forward_demodulation,[],[f335885,f301755]) ).
fof(f411265,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X1,join(X0,X2)),
inference(superposition,[],[f321900,f19]) ).
fof(f433482,plain,
! [X2,X0,X1] : join(X1,join(X2,X0)) = join(X2,join(X0,X1)),
inference(superposition,[],[f411265,f18]) ).
fof(f460014,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X0,join(X2,X1)),
inference(superposition,[],[f433482,f411265]) ).
fof(f462604,plain,
! [X0,X1] : complement(join(X1,X0)) = complement(join(X0,join(join(X1,X0),X1))),
inference(superposition,[],[f295300,f433482]) ).
fof(f463526,plain,
! [X0,X1] : complement(join(X1,X0)) = complement(join(X0,join(X1,join(X0,X1)))),
inference(forward_demodulation,[],[f462604,f19]) ).
fof(f466517,plain,
! [X0,X1] : complement(join(X1,X0)) = complement(join(X0,join(X0,X1))),
inference(forward_demodulation,[],[f463526,f299004]) ).
fof(f468760,plain,
! [X0,X1] : complement(join(X0,X1)) = complement(join(X1,X0)),
inference(forward_demodulation,[],[f466517,f296733]) ).
fof(f511957,plain,
! [X0] : top = join(complement(composition(sK0,X0)),composition(one,X0)),
inference(superposition,[],[f281731,f44]) ).
fof(f513148,plain,
! [X0] : top = join(composition(one,X0),complement(composition(sK0,X0))),
inference(forward_demodulation,[],[f511957,f18]) ).
fof(f540103,plain,
! [X0,X1] : join(complement(X0),complement(join(X1,X0))) = complement(join(X0,complement(converse(complement(converse(X0)))))),
inference(superposition,[],[f292421,f281462]) ).
fof(f540347,plain,
! [X0] : complement(X0) = complement(join(X0,complement(converse(complement(converse(X0)))))),
inference(forward_demodulation,[],[f540103,f336739]) ).
fof(f541664,plain,
! [X0] : complement(join(complement(X0),complement(converse(complement(converse(complement(X0))))))) = join(X0,complement(converse(complement(converse(X0))))),
inference(superposition,[],[f292421,f540347]) ).
fof(f541682,plain,
! [X0] : join(X0,complement(converse(complement(converse(X0))))) = X0,
inference(forward_demodulation,[],[f541664,f292421]) ).
fof(f542344,plain,
! [X0] : converse(converse(X0)) = join(X0,converse(complement(converse(complement(converse(converse(X0))))))),
inference(superposition,[],[f58,f541682]) ).
fof(f542616,plain,
! [X0] : join(X0,converse(complement(converse(complement(X0))))) = X0,
inference(forward_demodulation,[],[f542344,f25]) ).
fof(f543343,plain,
! [X0] : converse(complement(converse(complement(X0)))) = complement(join(complement(converse(complement(converse(complement(X0))))),complement(X0))),
inference(superposition,[],[f281462,f542616]) ).
fof(f543883,plain,
! [X0] : converse(complement(converse(complement(X0)))) = complement(join(complement(X0),complement(converse(complement(converse(complement(X0))))))),
inference(forward_demodulation,[],[f543343,f468760]) ).
fof(f544074,plain,
! [X0] : converse(complement(converse(complement(X0)))) = X0,
inference(forward_demodulation,[],[f543883,f292421]) ).
fof(f544451,plain,
! [X0] : converse(X0) = complement(converse(complement(X0))),
inference(superposition,[],[f25,f544074]) ).
fof(f544809,plain,
! [X0] : converse(complement(X0)) = complement(join(converse(X0),complement(converse(complement(converse(converse(X0))))))),
inference(superposition,[],[f292421,f544451]) ).
fof(f544827,plain,
! [X0] : complement(converse(X0)) = converse(complement(X0)),
inference(forward_demodulation,[],[f544809,f540347]) ).
fof(f557733,plain,
! [X0,X1] : join(X1,complement(join(complement(X0),X1))) = join(join(X1,complement(join(complement(X0),X1))),X0),
inference(superposition,[],[f307690,f290520]) ).
fof(f557930,plain,
! [X0,X1] : join(X1,complement(join(complement(X0),X1))) = join(X1,join(complement(join(complement(X0),X1)),X0)),
inference(forward_demodulation,[],[f557733,f19]) ).
fof(f558138,plain,
! [X0,X1] : join(X1,complement(join(complement(X0),X1))) = join(X1,join(X0,complement(join(complement(X0),X1)))),
inference(forward_demodulation,[],[f557930,f460014]) ).
fof(f558249,plain,
! [X0,X1] : join(X1,X0) = join(X1,complement(join(complement(X0),X1))),
inference(forward_demodulation,[],[f558138,f301755]) ).
fof(f558516,plain,
! [X0,X1] : join(X0,X1) = join(X0,complement(join(X0,complement(X1)))),
inference(superposition,[],[f558249,f18]) ).
fof(f746028,plain,
! [X0] : top = join(complement(one),complement(composition(converse(X0),complement(X0)))),
inference(superposition,[],[f283567,f23]) ).
fof(f747527,plain,
! [X0] : top = join(complement(one),complement(composition(converse(join(complement(X0),complement(converse(complement(converse(complement(X0))))))),X0))),
inference(superposition,[],[f746028,f292421]) ).
fof(f747793,plain,
! [X0] : top = join(complement(one),complement(composition(converse(complement(X0)),X0))),
inference(forward_demodulation,[],[f747527,f541682]) ).
fof(f747942,plain,
! [X0] : top = join(complement(one),complement(composition(complement(converse(X0)),X0))),
inference(forward_demodulation,[],[f747793,f544827]) ).
fof(f749323,plain,
top = join(complement(one),complement(complement(converse(one)))),
inference(superposition,[],[f747942,f23]) ).
fof(f749554,plain,
top = join(complement(one),converse(one)),
inference(forward_demodulation,[],[f749323,f212146]) ).
fof(f749974,plain,
converse(top) = join(converse(complement(one)),one),
inference(superposition,[],[f59,f749554]) ).
fof(f750126,plain,
converse(top) = join(one,converse(complement(one))),
inference(forward_demodulation,[],[f749974,f18]) ).
fof(f750218,plain,
converse(top) = join(one,complement(converse(one))),
inference(forward_demodulation,[],[f750126,f544827]) ).
fof(f750282,plain,
top = join(one,complement(converse(one))),
inference(forward_demodulation,[],[f750218,f153202]) ).
fof(f750432,plain,
join(one,converse(one)) = join(one,complement(top)),
inference(superposition,[],[f558516,f750282]) ).
fof(f750589,plain,
join(one,converse(one)) = join(one,zero),
inference(forward_demodulation,[],[f750432,f56]) ).
fof(f750701,plain,
one = join(one,converse(one)),
inference(forward_demodulation,[],[f750589,f211366]) ).
fof(f750894,plain,
one = converse(one),
inference(superposition,[],[f321744,f750701]) ).
fof(f751235,plain,
! [X0] : composition(converse(X0),one) = converse(composition(one,X0)),
inference(superposition,[],[f65,f750894]) ).
fof(f751378,plain,
! [X0] : converse(X0) = converse(composition(one,X0)),
inference(forward_demodulation,[],[f751235,f23]) ).
fof(f752338,plain,
! [X0] : converse(converse(X0)) = composition(one,X0),
inference(superposition,[],[f25,f751378]) ).
fof(f752517,plain,
! [X0] : composition(one,X0) = X0,
inference(forward_demodulation,[],[f752338,f25]) ).
fof(f752628,plain,
! [X0] : top = join(X0,complement(composition(sK0,X0))),
inference(superposition,[],[f513148,f752517]) ).
fof(f752686,plain,
! [X0,X1] : composition(join(one,X1),X0) = join(X0,composition(X1,X0)),
inference(superposition,[],[f24,f752517]) ).
fof(f752913,plain,
! [X0] : join(X0,complement(top)) = join(X0,composition(sK0,X0)),
inference(superposition,[],[f558516,f752628]) ).
fof(f753674,plain,
! [X0] : join(X0,zero) = join(X0,composition(sK0,X0)),
inference(forward_demodulation,[],[f752913,f56]) ).
fof(f753953,plain,
! [X0] : join(X0,composition(sK0,X0)) = X0,
inference(forward_demodulation,[],[f753674,f211366]) ).
fof(f754586,plain,
! [X0,X1] : join(X1,X0) = join(X0,join(X1,composition(sK0,X0))),
inference(superposition,[],[f411265,f753953]) ).
fof(f930480,plain,
! [X0] : composition(top,X0) = join(X0,composition(complement(one),X0)),
inference(superposition,[],[f752686,f29]) ).
fof(f933064,plain,
! [X0] : converse(composition(top,converse(X0))) = join(X0,converse(composition(complement(one),converse(X0)))),
inference(superposition,[],[f58,f930480]) ).
fof(f933409,plain,
! [X0] : converse(composition(top,converse(X0))) = join(X0,composition(X0,converse(complement(one)))),
inference(forward_demodulation,[],[f933064,f64]) ).
fof(f933743,plain,
! [X0] : converse(composition(top,converse(X0))) = join(X0,composition(X0,complement(converse(one)))),
inference(forward_demodulation,[],[f933409,f544827]) ).
fof(f933968,plain,
! [X0] : converse(composition(top,converse(X0))) = join(X0,composition(X0,complement(one))),
inference(forward_demodulation,[],[f933743,f750894]) ).
fof(f934098,plain,
! [X0] : composition(converse(converse(X0)),top) = join(X0,composition(X0,complement(one))),
inference(forward_demodulation,[],[f933968,f153516]) ).
fof(f934148,plain,
! [X0] : composition(X0,top) = join(X0,composition(X0,complement(one))),
inference(forward_demodulation,[],[f934098,f25]) ).
fof(f1002544,plain,
join(sK0,complement(one)) = join(complement(one),composition(sK0,top)),
inference(superposition,[],[f754586,f934148]) ).
fof(f1097369,plain,
( complement(join(sK0,complement(one))) != join(complement(join(sK0,complement(one))),complement(join(sK0,complement(one))))
| spl1_1 ),
inference(superposition,[],[f213688,f1002544]) ).
fof(f1097551,plain,
( $false
| spl1_1 ),
inference(forward_subsumption_resolution,[],[f1097369,f296496]) ).
fof(f1097552,plain,
spl1_1,
inference(avatar_contradiction_clause,[],[f1097551]) ).
fof(f1097609,plain,
( complement(join(complement(complement(sK0)),complement(one))) != join(complement(join(complement(complement(sK0)),complement(one))),complement(join(complement(complement(composition(sK0,top))),complement(one))))
| spl1_2 ),
inference(forward_demodulation,[],[f42,f18]) ).
fof(f1097611,plain,
( complement(join(complement(complement(sK0)),complement(one))) != join(complement(join(complement(complement(sK0)),complement(one))),complement(join(complement(one),complement(complement(composition(sK0,top))))))
| spl1_2 ),
inference(forward_demodulation,[],[f1097609,f468760]) ).
fof(f1097613,plain,
( complement(join(complement(complement(sK0)),complement(one))) != join(complement(join(complement(complement(sK0)),complement(one))),complement(join(complement(one),composition(sK0,top))))
| spl1_2 ),
inference(forward_demodulation,[],[f1097611,f212146]) ).
fof(f1097615,plain,
( complement(join(complement(complement(sK0)),complement(one))) != join(complement(join(complement(one),composition(sK0,top))),complement(join(complement(complement(sK0)),complement(one))))
| spl1_2 ),
inference(forward_demodulation,[],[f1097613,f18]) ).
fof(f1097617,plain,
( complement(join(complement(one),complement(complement(sK0)))) != join(complement(join(complement(one),composition(sK0,top))),complement(join(complement(one),complement(complement(sK0)))))
| spl1_2 ),
inference(forward_demodulation,[],[f1097615,f468760]) ).
fof(f1097619,plain,
( complement(join(complement(one),complement(complement(sK0)))) != join(complement(join(complement(one),complement(complement(sK0)))),complement(join(complement(one),composition(sK0,top))))
| spl1_2 ),
inference(forward_demodulation,[],[f1097617,f18]) ).
fof(f1097621,plain,
( complement(join(complement(one),complement(complement(sK0)))) != join(complement(join(complement(one),complement(complement(sK0)))),complement(join(sK0,complement(one))))
| spl1_2 ),
inference(forward_demodulation,[],[f1097619,f1002544]) ).
fof(f1097623,plain,
( complement(join(complement(one),complement(complement(sK0)))) != join(complement(join(sK0,complement(one))),complement(join(complement(one),complement(complement(sK0)))))
| spl1_2 ),
inference(forward_demodulation,[],[f1097621,f18]) ).
fof(f1097625,plain,
( complement(join(complement(one),sK0)) != join(complement(join(sK0,complement(one))),complement(join(complement(one),sK0)))
| spl1_2 ),
inference(forward_demodulation,[],[f1097623,f212146]) ).
fof(f1097626,plain,
( complement(join(sK0,complement(one))) != join(complement(join(sK0,complement(one))),complement(join(sK0,complement(one))))
| spl1_2 ),
inference(forward_demodulation,[],[f1097625,f468760]) ).
fof(f1097627,plain,
( $false
| spl1_2 ),
inference(forward_subsumption_resolution,[],[f1097626,f296496]) ).
fof(f1097628,plain,
spl1_2,
inference(avatar_contradiction_clause,[],[f1097627]) ).
cnf(s16,plain,
( ~ spl1_1
| ~ spl1_2 ),
inference(sat_conversion,[],[f43]) ).
cnf(s72415,plain,
spl1_1,
inference(sat_conversion,[],[f1097552]) ).
cnf(s72442,plain,
spl1_2,
inference(sat_conversion,[],[f1097628]) ).
cnf(s72443,plain,
$false,
inference(rat,[],[s16,s72442,s72415]) ).
fof(f1097629,plain,
$false,
inference(avatar_sat_refutation,[],[s72443]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL027+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.14/0.39 % Computer : n003.cluster.edu
% 0.14/0.39 % Model : x86_64 x86_64
% 0.14/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.39 % Memory : 8046.5625MB
% 0.14/0.39 % OS : Linux 6.8.0-71-generic
% 0.14/0.39 % CPULimit : 300
% 0.14/0.39 % WCLimit : 300
% 0.14/0.39 % DateTime : Sun Sep 27 22:54:57 UTC 2026
% 0.14/0.39 % CPUTime :
% 0.14/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.14/0.44 Running first-order model finding
% 0.14/0.44 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 28.82/4.54 % (1015418)Will run a generic schedule for satisfiability detection.
% 28.82/4.54 % (1015423)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2404611969_2999 on theBenchmark for (2999ds/0Mi)
% 28.82/4.54 % TRYING [1]
% 28.82/4.54 % TRYING [2]
% 28.82/4.54 % TRYING [3]
% 28.82/4.54 % (1015424)% WARNING: option uhcvi not known.
% 28.82/4.54 % TRYING [4]
% 28.82/4.54 % (1015426)dis+10_1_sil=32000:sp=arity:random_seed=1215594134:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 28.82/4.54 % (1015424)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3575236205:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 28.82/4.54 % (1015427)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3415876832:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 28.82/4.54 % (1015425)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=929850131:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 28.82/4.54 % (1015428)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=811213858:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 28.82/4.54 % (1015429)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1338116471:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 28.82/4.54 % TRYING [5]
% 28.82/4.54 % (1015426)Instruction limit reached!
% 28.82/4.54 % (1015426)------------------------------
% 28.82/4.54 % (1015426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.82/4.54 % (1015426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.82/4.54 % (1015426)CaDiCaL version: 2.1.3
% 28.82/4.54 % (1015426)Termination reason: Instruction limit
% 28.82/4.54 % (1015426)Termination phase: Saturation
% 28.82/4.54 % (1015426)Time elapsed: 0.097 s
% 28.82/4.54 % (1015426)Peak memory usage: 12 MB
% 28.82/4.54 % (1015426)Instructions burned: 104 (million)
% 28.82/4.54 % (1015427)Instruction limit reached!
% 28.82/4.54 % (1015427)------------------------------
% 28.82/4.54 % (1015427)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.82/4.54 % (1015427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.82/4.54 % (1015427)CaDiCaL version: 2.1.3
% 28.82/4.54 % (1015427)Termination reason: Instruction limit
% 28.82/4.54 % (1015427)Termination phase: Saturation
% 28.82/4.54 % (1015427)Time elapsed: 0.117 s
% 28.82/4.54 % (1015427)Peak memory usage: 13 MB
% 28.82/4.54 % (1015427)Instructions burned: 116 (million)
% 28.82/4.54 % (1015439)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1727458746:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 28.82/4.54 % TRYING [1]
% 28.82/4.54 % TRYING [2]
% 28.82/4.54 % (1015428)Instruction limit reached!
% 28.82/4.54 % (1015428)------------------------------
% 28.82/4.54 % (1015428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.82/4.54 % (1015428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.82/4.54 % (1015428)CaDiCaL version: 2.1.3
% 28.82/4.54 % (1015428)Termination reason: Instruction limit
% 28.82/4.54 % (1015428)Termination phase: Saturation
% 28.82/4.54 % (1015428)Time elapsed: 0.130 s
% 28.82/4.54 % (1015428)Peak memory usage: 13 MB
% 28.82/4.54 % (1015428)Instructions burned: 131 (million)
% 28.82/4.54 % TRYING [3]
% 28.82/4.54 % TRYING [4]
% 28.82/4.54 % (1015440)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3115929353:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 28.82/4.54 % (1015442)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1975567894:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 28.82/4.54 % TRYING [6]
% 28.82/4.54 % (1015429)Instruction limit reached!
% 28.82/4.54 % (1015429)------------------------------
% 28.82/4.54 % (1015429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.82/4.54 % (1015429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.82/4.54 % (1015429)CaDiCaL version: 2.1.3
% 28.82/4.54 % (1015429)Termination reason: Instruction limit
% 28.82/4.54 % (1015429)Termination phase: Saturation
% 28.82/4.54 % (1015429)Time elapsed: 0.161 s
% 28.82/4.54 % (1015429)Peak memory usage: 13 MB
% 28.82/4.54 % (1015429)Instructions burned: 159 (million)
% 28.82/4.54 % (1015445)ott-21_1_sil=16000:fs=off:random_seed=3686940946:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 28.82/4.54 % TRYING [5]
% 28.82/4.54 % (1015440)Instruction limit reached!
% 28.82/4.54 % (1015440)------------------------------
% 28.82/4.54 % (1015440)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 87.79/12.82 % (1015440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.79/12.82 % (1015440)CaDiCaL version: 2.1.3
% 87.79/12.82 % (1015440)Termination reason: Instruction limit
% 87.79/12.82 % (1015440)Termination phase: Saturation
% 87.79/12.82 % (1015440)Time elapsed: 0.140 s
% 87.79/12.82 % (1015440)Peak memory usage: 13 MB
% 87.79/12.82 % (1015440)Instructions burned: 131 (million)
% 87.79/12.82 % (1015445)Instruction limit reached!
% 87.79/12.82 % (1015445)------------------------------
% 87.79/12.82 % (1015445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 87.79/12.82 % (1015445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.79/12.82 % (1015445)CaDiCaL version: 2.1.3
% 87.79/12.82 % (1015445)Termination reason: Instruction limit
% 87.79/12.82 % (1015445)Termination phase: Saturation
% 87.79/12.82 % (1015445)Time elapsed: 0.141 s
% 87.79/12.82 % (1015445)Peak memory usage: 12 MB
% 87.79/12.82 % (1015445)Instructions burned: 180 (million)
% 87.79/12.82 % (1015447)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4037415027:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 87.79/12.82 % (1015449)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1488529549:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 87.79/12.82 % TRYING [1]
% 87.79/12.82 % TRYING [2]
% 87.79/12.82 % TRYING [3]
% 87.79/12.82 % TRYING [4]
% 87.79/12.82 % TRYING [5]
% 87.79/12.82 % TRYING [6]
% 87.79/12.82 % TRYING [7]
% 87.79/12.82 % (1015442)Instruction limit reached!
% 87.79/12.82 % (1015442)------------------------------
% 87.79/12.82 % (1015442)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 87.79/12.82 % (1015442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.79/12.82 % (1015442)CaDiCaL version: 2.1.3
% 87.79/12.82 % (1015442)Termination reason: Instruction limit
% 87.79/12.82 % (1015442)Termination phase: Saturation
% 87.79/12.82 % (1015442)Time elapsed: 0.557 s
% 87.79/12.82 % (1015442)Peak memory usage: 19 MB
% 87.79/12.82 % (1015442)Instructions burned: 685 (million)
% 87.79/12.82 % (1015439)Instruction limit reached!
% 87.79/12.82 % (1015439)------------------------------
% 87.79/12.82 % (1015439)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 87.79/12.82 % (1015439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.79/12.82 % (1015439)CaDiCaL version: 2.1.3
% 87.79/12.82 % (1015439)Termination reason: Instruction limit
% 87.79/12.82 % (1015439)Termination phase: Finite model building SAT solving
% 87.79/12.82 % (1015439)Time elapsed: 0.600 s
% 87.79/12.82 % (1015439)Peak memory usage: 26 MB
% 87.79/12.82 % (1015439)Instructions burned: 715 (million)
% 87.79/12.82 % TRYING [6]
% 87.79/12.82 % (1015456)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2201918022:i=1179_2992 on theBenchmark for (2992ds/1179Mi)
% 87.79/12.82 % (1015457)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=525227994:i=889:ins=1_2992 on theBenchmark for (2992ds/889Mi)
% 87.79/12.82 % (1015447)Instruction limit reached!
% 87.79/12.82 % (1015447)------------------------------
% 87.79/12.82 % (1015447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 87.79/12.82 % (1015447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.79/12.82 % (1015447)CaDiCaL version: 2.1.3
% 87.79/12.82 % (1015447)Termination reason: Instruction limit
% 87.79/12.82 % (1015447)Termination phase: Saturation
% 87.79/12.82 % (1015447)Time elapsed: 0.441 s
% 87.79/12.82 % (1015447)Peak memory usage: 15 MB
% 87.79/12.82 % (1015447)Instructions burned: 477 (million)
% 87.79/12.82 % (1015461)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3894801763:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2991 on theBenchmark for (2991ds/692Mi)
% 87.79/12.82 % TRYING [14]
% 87.79/12.82 % (1015449)Instruction limit reached!
% 87.79/12.82 % (1015449)------------------------------
% 87.79/12.82 % (1015449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 87.79/12.82 % (1015449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.79/12.82 % (1015449)CaDiCaL version: 2.1.3
% 87.79/12.82 % (1015449)Termination reason: Instruction limit
% 87.79/12.82 % (1015449)Termination phase: Finite model building SAT solving
% 87.79/12.82 % (1015449)Time elapsed: 0.599 s
% 87.79/12.82 % (1015449)Peak memory usage: 22 MB
% 87.79/12.82 % (1015449)Instructions burned: 866 (million)
% 87.79/12.82 % (1015463)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3937319072:i=879:kws=inv_precedence:fsr=off_2990 on theBenchmark for (2990ds/879Mi)
% 177.05/25.41 % (1015457)Instruction limit reached!
% 177.05/25.41 % (1015457)------------------------------
% 177.05/25.41 % (1015457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.05/25.41 % (1015457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.05/25.41 % (1015457)CaDiCaL version: 2.1.3
% 177.05/25.41 % (1015457)Termination reason: Instruction limit
% 177.05/25.41 % (1015457)Termination phase: Finite model building constraint generation
% 177.05/25.41 % (1015457)Time elapsed: 0.558 s
% 177.05/25.41 % (1015457)Peak memory usage: 82 MB
% 177.05/25.41 % (1015457)Instructions burned: 889 (million)
% 177.05/25.41 % (1015467)fmb+10_1_sil=64000:random_seed=1246358799:i=22061:nm=2:gsp=on_2986 on theBenchmark for (2986ds/22061Mi)
% 177.05/25.41 % TRYING [1]
% 177.05/25.41 % TRYING [2]
% 177.05/25.41 % TRYING [3]
% 177.05/25.41 % TRYING [4]
% 177.05/25.41 % TRYING [5]
% 177.05/25.41 % (1015461)Instruction limit reached!
% 177.05/25.41 % (1015461)------------------------------
% 177.05/25.41 % (1015461)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.05/25.41 % (1015461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.05/25.41 % (1015461)CaDiCaL version: 2.1.3
% 177.05/25.41 % (1015461)Termination reason: Instruction limit
% 177.05/25.41 % (1015461)Termination phase: Saturation
% 177.05/25.41 % (1015461)Time elapsed: 0.681 s
% 177.05/25.41 % (1015461)Peak memory usage: 16 MB
% 177.05/25.41 % (1015461)Instructions burned: 692 (million)
% 177.05/25.41 % (1015469)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1932344965:i=9515:nm=5_2984 on theBenchmark for (2984ds/9515Mi)
% 177.05/25.41 % TRYING [20]
% 177.05/25.41 % TRYING [6]
% 177.05/25.41 % (1015456)Instruction limit reached!
% 177.05/25.41 % (1015456)------------------------------
% 177.05/25.41 % (1015456)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.05/25.41 % (1015456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.05/25.41 % (1015456)CaDiCaL version: 2.1.3
% 177.05/25.41 % (1015456)Termination reason: Instruction limit
% 177.05/25.41 % (1015456)Termination phase: Saturation
% 177.05/25.41 % (1015456)Time elapsed: 1.069 s
% 177.05/25.41 % (1015456)Peak memory usage: 22 MB
% 177.05/25.41 % (1015456)Instructions burned: 1179 (million)
% 177.05/25.41 % (1015463)Instruction limit reached!
% 177.05/25.41 % (1015463)------------------------------
% 177.05/25.41 % (1015463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.05/25.41 % (1015463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.05/25.41 % (1015463)CaDiCaL version: 2.1.3
% 177.05/25.41 % (1015463)Termination reason: Instruction limit
% 177.05/25.41 % (1015463)Termination phase: Saturation
% 177.05/25.41 % (1015463)Time elapsed: 0.817 s
% 177.05/25.41 % (1015463)Peak memory usage: 19 MB
% 177.05/25.41 % (1015463)Instructions burned: 879 (million)
% 177.05/25.41 % (1015471)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=476654018:fmbsr=1.7:i=920_2981 on theBenchmark for (2981ds/920Mi)
% 177.05/25.41 % TRYING [8]
% 177.05/25.41 % (1015472)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=986166375:i=5131_2981 on theBenchmark for (2981ds/5131Mi)
% 177.05/25.41 % TRYING [8]
% 177.05/25.41 % TRYING [7]
% 177.05/25.41 % (1015471)Instruction limit reached!
% 177.05/25.41 % (1015471)------------------------------
% 177.05/25.41 % (1015471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.05/25.41 % (1015471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.05/25.41 % (1015471)CaDiCaL version: 2.1.3
% 177.05/25.41 % (1015471)Termination reason: Instruction limit
% 177.05/25.41 % (1015471)Termination phase: Finite model building SAT solving
% 177.05/25.41 % (1015471)Time elapsed: 0.734 s
% 177.05/25.41 % (1015471)Peak memory usage: 65 MB
% 177.05/25.41 % (1015471)Instructions burned: 921 (million)
% 177.05/25.41 % (1015477)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2645837487:i=1472:ins=7:fdi=8:gsp=on_2973 on theBenchmark for (2973ds/1472Mi)
% 177.05/25.41 % (1015477)Instruction limit reached!
% 177.05/25.41 % (1015477)------------------------------
% 177.05/25.41 % (1015477)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.05/25.41 % (1015477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.05/25.41 % (1015477)CaDiCaL version: 2.1.3
% 177.05/25.41 % (1015477)Termination reason: Instruction limit
% 177.05/25.41 % (1015477)Termination phase: Saturation
% 177.05/25.41 % (1015477)Time elapsed: 1.409 s
% 177.05/25.41 % (1015477)Peak memory usage: 27 MB
% 177.05/25.41 % (1015477)Instructions burned: 1473 (million)
% 177.05/25.41 % (1015479)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2374637169:i=6324_2959 on theBenchmark for (2959ds/6324Mi)
% 138.61/33.38 % TRYING [77]
% 138.61/33.38 % TRYING [8]
% 138.61/33.38 % (1015472)Instruction limit reached!
% 138.61/33.38 % (1015472)------------------------------
% 138.61/33.38 % (1015472)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.61/33.38 % (1015472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.61/33.38 % (1015472)CaDiCaL version: 2.1.3
% 138.61/33.38 % (1015472)Termination reason: Instruction limit
% 138.61/33.38 % (1015472)Termination phase: Saturation
% 138.61/33.38 % (1015472)Time elapsed: 4.741 s
% 138.61/33.38 % (1015472)Peak memory usage: 51 MB
% 138.61/33.38 % (1015472)Instructions burned: 5132 (million)
% 138.61/33.38 % (1015483)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4010953133:fmbsr=2.30978:i=2174_2933 on theBenchmark for (2933ds/2174Mi)
% 138.61/33.38 % TRYING [16]
% 138.61/33.38 % (1015483)Instruction limit reached!
% 138.61/33.38 % (1015483)------------------------------
% 138.61/33.38 % (1015483)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.61/33.38 % (1015483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.61/33.38 % (1015483)CaDiCaL version: 2.1.3
% 138.61/33.38 % (1015483)Termination reason: Instruction limit
% 138.61/33.38 % (1015483)Termination phase: Finite model building constraint generation
% 138.61/33.38 % (1015483)Time elapsed: 1.496 s
% 138.61/33.38 % (1015483)Peak memory usage: 135 MB
% 138.61/33.38 % (1015483)Instructions burned: 2174 (million)
% 138.61/33.38 % (1015493)ott-2_1_sil=16000:newcnf=on:random_seed=1716283024:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2917 on theBenchmark for (2917ds/869Mi)
% 138.61/33.38 % TRYING [9]
% 138.61/33.38 % (1015479)Instruction limit reached!
% 138.61/33.38 % (1015479)------------------------------
% 138.61/33.38 % (1015479)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.61/33.38 % (1015479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.61/33.38 % (1015479)CaDiCaL version: 2.1.3
% 138.61/33.38 % (1015479)Termination reason: Instruction limit
% 138.61/33.38 % (1015479)Termination phase: Finite model building constraint generation
% 138.61/33.38 % (1015479)Time elapsed: 4.389 s
% 138.61/33.38 % (1015479)Peak memory usage: 515 MB
% 138.61/33.38 % (1015479)Instructions burned: 6324 (million)
% 138.61/33.38 % (1015495)ott+10_1_sil=32000:tgt=ground:random_seed=931515225:i=5114:av=off_2914 on theBenchmark for (2914ds/5114Mi)
% 138.61/33.38 % (1015469)Instruction limit reached!
% 138.61/33.38 % (1015469)------------------------------
% 138.61/33.38 % (1015469)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.61/33.38 % (1015469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.61/33.38 % (1015469)CaDiCaL version: 2.1.3
% 138.61/33.38 % (1015469)Termination reason: Instruction limit
% 138.61/33.38 % (1015469)Termination phase: Finite model building constraint generation
% 138.61/33.38 % (1015469)Time elapsed: 7.085 s
% 138.61/33.38 % (1015469)Peak memory usage: 671 MB
% 138.61/33.38 % (1015469)Instructions burned: 9515 (million)
% 138.61/33.38 % (1015497)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=618605759:i=54282_2911 on theBenchmark for (2911ds/54282Mi)
% 138.61/33.38 % TRYING [1]
% 138.61/33.38 % TRYING [2]
% 138.61/33.38 % TRYING [3]
% 138.61/33.38 % TRYING [4]
% 138.61/33.38 % TRYING [9]
% 138.61/33.38 % TRYING [5]
% 138.61/33.38 % (1015493)Instruction limit reached!
% 138.61/33.38 % (1015493)------------------------------
% 138.61/33.38 % (1015493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.61/33.38 % (1015493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.61/33.38 % (1015493)CaDiCaL version: 2.1.3
% 138.61/33.38 % (1015493)Termination reason: Instruction limit
% 138.61/33.38 % (1015493)Termination phase: Saturation
% 138.61/33.38 % (1015493)Time elapsed: 0.767 s
% 138.61/33.38 % (1015493)Peak memory usage: 18 MB
% 138.61/33.38 % (1015493)Instructions burned: 870 (million)
% 138.61/33.38 % (1015499)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1290568708:i=3512:aac=none_2909 on theBenchmark for (2909ds/3512Mi)
% 138.61/33.38 % TRYING [6]
% 138.61/33.38 % TRYING [7]
% 138.61/33.38 % (1015499)Instruction limit reached!
% 138.61/33.38 % (1015499)------------------------------
% 138.61/33.38 % (1015499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.61/33.38 % (1015499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.61/33.38 % (1015499)CaDiCaL version: 2.1.3
% 138.61/33.38 % (1015499)Termination reason: Instruction limit
% 138.61/33.38 % (1015499)Termination phase: Saturation
% 138.61/33.38 % (1015499)Time elapsed: 3.278 s
% 138.61/33.38 % (1015499)Peak memory usage: 40 MB
% 138.61/33.38 % (1015499)Instructions burned: 3512 (million)
% 138.61/33.38 % (1015507)dis+21_1_sil=32000:sas=cadical:random_seed=1877399185:i=3773:amm=off_2876 on theBenchmark for (2876ds/3773Mi)
% 138.61/33.38 % TRYING [8]
% 138.61/33.38 % (1015495)Instruction limit reached!
% 138.61/33.38 % (1015495)------------------------------
% 138.61/33.38 % (1015495)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.61/33.38 % (1015495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.61/33.38 % (1015495)CaDiCaL version: 2.1.3
% 138.61/33.38 % (1015495)Termination reason: Instruction limit
% 138.61/33.38 % (1015495)Termination phase: Saturation
% 138.61/33.38 % (1015495)Time elapsed: 4.711 s
% 138.61/33.38 % (1015495)Peak memory usage: 55 MB
% 138.61/33.38 % (1015495)Instructions burned: 5114 (million)
% 138.61/33.38 % (1015513)ott+11_1_sil=16000:gs=on:random_seed=1311327561:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2866 on theBenchmark for (2866ds/2251Mi)
% 138.61/33.38 % (1015513)Instruction limit reached!
% 138.61/33.38 % (1015513)------------------------------
% 138.61/33.38 % (1015513)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.61/33.38 % (1015513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.61/33.38 % (1015513)CaDiCaL version: 2.1.3
% 138.61/33.38 % (1015513)Termination reason: Instruction limit
% 138.61/33.38 % (1015513)Termination phase: Saturation
% 138.61/33.38 % (1015513)Time elapsed: 2.113 s
% 138.61/33.38 % (1015513)Peak memory usage: 26 MB
% 138.61/33.38 % (1015513)Instructions burned: 2252 (million)
% 138.61/33.38 % (1015515)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1643543189:fmbsr=1.6:i=67534_2845 on theBenchmark for (2845ds/67534Mi)
% 138.61/33.38 % (1015507)Instruction limit reached!
% 138.61/33.38 % (1015507)------------------------------
% 138.61/33.38 % (1015507)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.61/33.38 % (1015507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.61/33.38 % (1015507)CaDiCaL version: 2.1.3
% 138.61/33.38 % (1015507)Termination reason: Instruction limit
% 138.61/33.38 % (1015507)Termination phase: Saturation
% 138.61/33.38 % (1015507)Time elapsed: 3.166 s
% 138.61/33.38 % (1015507)Peak memory usage: 42 MB
% 138.61/33.38 % (1015507)Instructions burned: 3773 (million)
% 138.61/33.38 % TRYING [7]
% 138.61/33.38 % (1015517)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=4026860831:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2844 on theBenchmark for (2844ds/4591Mi)
% 138.61/33.38 % TRYING [8]
% 138.61/33.38 % (1015517)Instruction limit reached!
% 138.61/33.38 % (1015517)------------------------------
% 138.61/33.38 % (1015517)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.61/33.38 % (1015517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.61/33.38 % (1015517)CaDiCaL version: 2.1.3
% 138.61/33.38 % (1015517)Termination reason: Instruction limit
% 138.61/33.38 % (1015517)Termination phase: Saturation
% 138.61/33.38 % (1015517)Time elapsed: 4.188 s
% 138.61/33.38 % (1015517)Peak memory usage: 75 MB
% 138.61/33.38 % (1015517)Instructions burned: 4592 (million)
% 138.61/33.38 % (1015523)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3049671525:i=29340_2802 on theBenchmark for (2802ds/29340Mi)
% 138.61/33.38 % (1015467)Instruction limit reached!
% 138.61/33.38 % (1015467)------------------------------
% 138.61/33.38 % (1015467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.61/33.38 % (1015467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.61/33.38 % (1015467)CaDiCaL version: 2.1.3
% 138.61/33.38 % (1015467)Termination reason: Instruction limit
% 138.61/33.38 % (1015467)Termination phase: Finite model building SAT solving
% 138.61/33.38 % (1015467)Time elapsed: 18.765 s
% 138.61/33.38 % (1015467)Peak memory usage: 112 MB
% 138.61/33.38 % (1015467)Instructions burned: 22061 (million)
% 138.61/33.38 % (1015525)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2794799643:i=5211_2798 on theBenchmark for (2798ds/5211Mi)
% 138.61/33.38 % TRYING [9]
% 138.61/33.38 % TRYING [9]
% 138.61/33.38 % TRYING [10]
% 138.61/33.38 % (1015525)Instruction limit reached!
% 138.61/33.38 % (1015525)------------------------------
% 138.61/33.38 % (1015525)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.61/33.38 % (1015525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.61/33.38 % (1015525)CaDiCaL version: 2.1.3
% 138.61/33.38 % (1015525)Termination reason: Instruction limit
% 138.61/33.38 % (1015525)Termination phase: Saturation
% 138.61/33.38 % (1015525)Time elapsed: 4.731 s
% 138.61/33.38 % (1015525)Peak memory usage: 51 MB
% 138.61/33.38 % (1015525)Instructions burned: 5211 (million)
% 138.61/33.38 % (1015529)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=4257681416:i=5497:nm=2_2750 on theBenchmark for (2750ds/5497Mi)
% 138.61/33.38 % TRYING [17]
% 138.61/33.38 % (1015529)Instruction limit reached!
% 138.61/33.38 % (1015529)------------------------------
% 138.61/33.38 % (1015529)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.61/33.38 % (1015529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.61/33.38 % (1015529)CaDiCaL version: 2.1.3
% 138.61/33.38 % (1015529)Termination reason: Instruction limit
% 138.61/33.38 % (1015529)Termination phase: Finite model building constraint generation
% 138.61/33.38 % (1015529)Time elapsed: 3.922 s
% 138.61/33.38 % (1015529)Peak memory usage: 392 MB
% 138.61/33.38 % (1015529)Instructions burned: 5497 (million)
% 138.61/33.38 % (1015531)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1740600163:fmbsr=2:i=46332_2709 on theBenchmark for (2709ds/46332Mi)
% 138.61/33.38 % TRYING [15]
% 138.61/33.38 % (1015425) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1015418-1015425"...
% 138.61/33.38 % (1015425)...printing done.
% 138.61/33.38 % (1015425)Refutation found. Thanks to Tanya!
% 138.61/33.38 % SZS status Theorem for theBenchmark
% 138.61/33.38 % SZS output start Proof for theBenchmark
% See solution above
% 138.61/33.40 % (1015425)------------------------------
% 138.61/33.40 % (1015425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.61/33.40 % (1015425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.61/33.40 % (1015425)CaDiCaL version: 2.1.3
% 138.61/33.40 % (1015425)Termination reason: Refutation
% 138.61/33.40 % (1015425)Time elapsed: 32.702 s
% 138.61/33.40 % (1015425)Peak memory usage: 240 MB
% 138.61/33.40 % (1015425)Instructions burned: 34885 (million)
% 138.61/33.40 % (1015418)Success in time 32.927 s
% 138.61/33.40 % Vampire exiting
%------------------------------------------------------------------------------