%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT204-1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n007.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 11:46:14 AM UTC 2026
% Result : Unsatisfiable 44.22s 8.07s
% Output : Refutation 51.84s
% Verified :
% SZS Type : Refutation
% Derivation depth : 98
% Number of leaves : 12
% Syntax : Number of formulae : 401 ( 379 unt; 0 def)
% Number of atoms : 426 ( 425 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 52 ( 27 ~; 25 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 4 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 5 con; 0-2 aty)
% Number of variables : 991 ( 991 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X0] : join(X0,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',idempotence_of_join) ).
fof(f3,axiom,
! [X0,X1] : meet(X0,join(X0,X1)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',absorption1) ).
fof(f4,axiom,
! [X0,X1] : join(X0,meet(X0,X1)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',absorption2) ).
fof(f5,axiom,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_of_meet) ).
fof(f6,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_of_join) ).
fof(f7,axiom,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_meet) ).
fof(f8,axiom,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X0,join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_join) ).
fof(f9,axiom,
! [X0] : join(X0,complement(X0)) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement_join) ).
fof(f10,axiom,
! [X0] : meet(X0,complement(X0)) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement_meet) ).
fof(f11,axiom,
! [X0,X1] :
( join(X0,X1) != one
| meet(X0,X1) != zero
| complement(X0) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meet_join_complement) ).
fof(f12,axiom,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,join(X1,meet(join(X0,X1),join(X2,meet(X0,X1))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',equation_H58) ).
fof(f13,negated_conjecture,
meet(a,join(b,c)) != join(meet(a,b),meet(a,c)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_distributivity) ).
fof(f15,plain,
! [X0,X1] : meet(X1,join(X0,X1)) = X1,
inference(superposition,[],[f3,f6]) ).
fof(f17,plain,
! [X0,X1] : join(X1,meet(X0,X1)) = X1,
inference(superposition,[],[f4,f5]) ).
fof(f22,plain,
! [X0,X1] : join(X0,X1) = join(join(X0,X1),X0),
inference(superposition,[],[f17,f3]) ).
fof(f24,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X0,X1)),
inference(forward_demodulation,[],[f22,f6]) ).
fof(f27,plain,
! [X0,X1] : meet(X0,X1) = meet(meet(X0,X1),X0),
inference(superposition,[],[f15,f4]) ).
fof(f28,plain,
! [X0,X1] : meet(X1,X0) = meet(meet(X1,X0),X0),
inference(superposition,[],[f15,f17]) ).
fof(f29,plain,
! [X0,X1] : join(X1,X0) = join(join(X1,X0),X0),
inference(superposition,[],[f17,f15]) ).
fof(f31,plain,
! [X0,X1] : join(X1,X0) = join(X0,join(X1,X0)),
inference(forward_demodulation,[],[f29,f6]) ).
fof(f32,plain,
! [X0,X1] : meet(X1,X0) = meet(X0,meet(X1,X0)),
inference(forward_demodulation,[],[f28,f5]) ).
fof(f33,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X0,X1)),
inference(forward_demodulation,[],[f27,f5]) ).
fof(f36,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X0,X1),X2)),
inference(superposition,[],[f7,f3]) ).
fof(f37,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X1,X0),X2)),
inference(superposition,[],[f7,f15]) ).
fof(f44,plain,
! [X2,X0,X1] : meet(X0,X1) = join(meet(X0,X1),meet(X0,meet(X1,X2))),
inference(superposition,[],[f4,f7]) ).
fof(f46,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X2,meet(X0,X1)),
inference(superposition,[],[f5,f7]) ).
fof(f53,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X0,X1),X2)),
inference(superposition,[],[f8,f4]) ).
fof(f54,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X1,X0),X2)),
inference(superposition,[],[f8,f17]) ).
fof(f63,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f6,f8]) ).
fof(f64,plain,
! [X2,X0,X1] : join(X0,X1) = join(X0,join(X1,meet(join(X0,X1),X2))),
inference(superposition,[],[f4,f8]) ).
fof(f74,plain,
! [X2,X0,X1] : join(X1,X0) = join(X1,join(X0,meet(X1,X2))),
inference(superposition,[],[f53,f6]) ).
fof(f80,plain,
! [X2,X0,X1] : join(meet(X0,X2),X1) = meet(join(meet(X0,X2),X1),join(X0,X1)),
inference(superposition,[],[f15,f53]) ).
fof(f84,plain,
! [X2,X0,X1] : join(meet(X0,X2),X1) = meet(join(X0,X1),join(meet(X0,X2),X1)),
inference(forward_demodulation,[],[f80,f5]) ).
fof(f97,plain,
! [X0] : meet(X0,one) = X0,
inference(superposition,[],[f3,f9]) ).
fof(f98,plain,
! [X0,X1] : one = join(X0,join(X1,complement(join(X0,X1)))),
inference(superposition,[],[f8,f9]) ).
fof(f100,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(zero,X1)),
inference(superposition,[],[f53,f10]) ).
fof(f101,plain,
! [X0,X1] : meet(X0,meet(complement(X0),X1)) = meet(zero,X1),
inference(superposition,[],[f7,f10]) ).
fof(f103,plain,
! [X0] : join(X0,zero) = X0,
inference(superposition,[],[f4,f10]) ).
fof(f104,plain,
! [X0,X1] : zero = meet(X0,meet(X1,complement(meet(X0,X1)))),
inference(superposition,[],[f7,f10]) ).
fof(f110,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(one,X1)),
inference(superposition,[],[f36,f9]) ).
fof(f113,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(X1,meet(X0,join(X1,X2))),
inference(superposition,[],[f36,f5]) ).
fof(f117,plain,
! [X0,X1] : meet(X0,complement(join(X0,X1))) = meet(X0,zero),
inference(superposition,[],[f36,f10]) ).
fof(f135,plain,
! [X2,X0,X1] : meet(X1,join(X0,X2)) = meet(X1,join(X0,meet(join(X0,X1),join(X2,meet(X1,X0))))),
inference(superposition,[],[f12,f6]) ).
fof(f136,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = meet(X0,join(meet(X0,X1),meet(X0,join(X2,meet(X0,meet(X0,X1)))))),
inference(superposition,[],[f12,f4]) ).
fof(f147,plain,
! [X0,X1] : meet(X0,join(complement(X0),X1)) = meet(X0,join(complement(X0),meet(join(X0,complement(X0)),join(X1,zero)))),
inference(superposition,[],[f12,f10]) ).
fof(f152,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,join(X1,meet(join(X0,X1),join(meet(X0,X1),X2)))),
inference(superposition,[],[f12,f6]) ).
fof(f159,plain,
! [X2,X3,X0,X1] : meet(X0,meet(join(X1,meet(join(X0,X1),join(X2,meet(X0,X1)))),X3)) = meet(meet(X0,join(X1,X2)),X3),
inference(superposition,[],[f7,f12]) ).
fof(f167,plain,
! [X2,X3,X0,X1] : meet(X0,meet(join(X1,meet(join(X0,X1),join(X2,meet(X0,X1)))),X3)) = meet(X0,meet(join(X1,X2),X3)),
inference(forward_demodulation,[],[f159,f7]) ).
fof(f173,plain,
! [X0,X1] : meet(X0,join(complement(X0),X1)) = meet(X0,join(complement(X0),meet(join(X0,complement(X0)),X1))),
inference(forward_demodulation,[],[f147,f103]) ).
fof(f180,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = meet(X0,join(meet(X0,X1),meet(X0,join(X2,meet(X0,X1))))),
inference(forward_demodulation,[],[f136,f33]) ).
fof(f186,plain,
! [X0,X1] : meet(X0,join(complement(X0),X1)) = meet(X0,join(complement(X0),meet(one,X1))),
inference(forward_demodulation,[],[f173,f9]) ).
fof(f210,plain,
! [X0] : meet(one,X0) = X0,
inference(superposition,[],[f5,f97]) ).
fof(f213,plain,
! [X0] : one = join(one,X0),
inference(superposition,[],[f17,f97]) ).
fof(f228,plain,
! [X0,X1] : meet(one,join(X0,X1)) = meet(one,join(X0,meet(one,join(X1,meet(one,X0))))),
inference(superposition,[],[f12,f213]) ).
fof(f236,plain,
! [X0,X1] : meet(one,join(X0,X1)) = join(X0,meet(one,join(X1,meet(one,X0)))),
inference(forward_demodulation,[],[f228,f210]) ).
fof(f240,plain,
! [X0,X1] : meet(one,join(X0,X1)) = join(X0,join(X1,meet(one,X0))),
inference(forward_demodulation,[],[f236,f210]) ).
fof(f242,plain,
! [X0,X1] : join(X0,join(X1,X0)) = meet(one,join(X0,X1)),
inference(forward_demodulation,[],[f240,f210]) ).
fof(f244,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X1,X0)),
inference(forward_demodulation,[],[f242,f210]) ).
fof(f264,plain,
zero = complement(one),
inference(superposition,[],[f10,f210]) ).
fof(f369,plain,
! [X0] : join(zero,X0) = X0,
inference(superposition,[],[f6,f103]) ).
fof(f373,plain,
! [X0] : zero = meet(zero,X0),
inference(superposition,[],[f15,f103]) ).
fof(f394,plain,
! [X0] : zero = meet(X0,zero),
inference(superposition,[],[f17,f369]) ).
fof(f398,plain,
one = complement(zero),
inference(superposition,[],[f9,f369]) ).
fof(f463,plain,
! [X0,X1] : zero = meet(X1,meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f104,f5]) ).
fof(f488,plain,
! [X2,X0,X1] : meet(X0,join(meet(X1,complement(meet(X0,X1))),X2)) = meet(X0,join(meet(X1,complement(meet(X0,X1))),meet(join(X0,meet(X1,complement(meet(X0,X1)))),join(X2,zero)))),
inference(superposition,[],[f12,f104]) ).
fof(f501,plain,
! [X2,X0,X1] : meet(X0,join(meet(X1,complement(meet(X0,X1))),X2)) = meet(X0,join(meet(X1,complement(meet(X0,X1))),meet(join(X0,meet(X1,complement(meet(X0,X1)))),X2))),
inference(forward_demodulation,[],[f488,f103]) ).
fof(f534,plain,
! [X2,X0,X1] : join(join(meet(X0,X2),X1),X0) = join(join(meet(X0,X2),X1),join(X0,X1)),
inference(superposition,[],[f244,f53]) ).
fof(f545,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X0,join(join(X1,X0),X2)),
inference(superposition,[],[f8,f244]) ).
fof(f548,plain,
! [X0,X1] : join(X1,X0) = meet(join(X1,X0),join(X0,X1)),
inference(superposition,[],[f15,f244]) ).
fof(f558,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X0,join(X1,join(X0,X2))),
inference(forward_demodulation,[],[f545,f8]) ).
fof(f565,plain,
! [X2,X0,X1] : join(join(meet(X0,X2),X1),X0) = join(join(X0,X1),join(meet(X0,X2),X1)),
inference(forward_demodulation,[],[f534,f6]) ).
fof(f568,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X0,join(X1,join(X0,X2))),
inference(forward_demodulation,[],[f558,f8]) ).
fof(f572,plain,
! [X2,X0,X1] : join(join(meet(X0,X2),X1),X0) = join(X1,join(join(X0,X1),meet(X0,X2))),
inference(forward_demodulation,[],[f565,f63]) ).
fof(f576,plain,
! [X2,X0,X1] : join(join(meet(X0,X2),X1),X0) = join(X1,join(X0,join(X1,meet(X0,X2)))),
inference(forward_demodulation,[],[f572,f8]) ).
fof(f577,plain,
! [X2,X0,X1] : join(join(meet(X0,X2),X1),X0) = join(X1,join(X0,meet(X0,X2))),
inference(forward_demodulation,[],[f576,f568]) ).
fof(f578,plain,
! [X2,X0,X1] : join(X1,X0) = join(join(meet(X0,X2),X1),X0),
inference(forward_demodulation,[],[f577,f4]) ).
fof(f579,plain,
! [X2,X0,X1] : join(X1,X0) = join(X0,join(meet(X0,X2),X1)),
inference(forward_demodulation,[],[f578,f6]) ).
fof(f763,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(join(X0,X1),join(X0,X2)),
inference(superposition,[],[f54,f3]) ).
fof(f773,plain,
! [X2,X0,X1] : join(X2,X0) = join(X2,join(X0,meet(X1,X2))),
inference(superposition,[],[f54,f6]) ).
fof(f826,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X0,join(X2,join(X0,X1))),
inference(forward_demodulation,[],[f763,f63]) ).
fof(f837,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X0,join(X2,X1)),
inference(forward_demodulation,[],[f826,f568]) ).
fof(f923,plain,
! [X2,X0,X1] : meet(X1,join(meet(complement(X1),X0),X2)) = meet(X1,join(meet(complement(X1),X0),meet(join(X1,meet(complement(X1),X0)),join(X2,meet(zero,X0))))),
inference(superposition,[],[f12,f101]) ).
fof(f946,plain,
! [X2,X0,X1] : meet(X1,join(meet(complement(X1),X0),X2)) = meet(X1,join(meet(complement(X1),X0),meet(join(X1,meet(complement(X1),X0)),join(X2,zero)))),
inference(forward_demodulation,[],[f923,f373]) ).
fof(f973,plain,
! [X2,X0,X1] : meet(X1,join(meet(complement(X1),X0),X2)) = meet(X1,join(meet(complement(X1),X0),meet(join(X1,meet(complement(X1),X0)),X2))),
inference(forward_demodulation,[],[f946,f103]) ).
fof(f1017,plain,
! [X0,X1] :
( one != one
| zero != meet(X0,join(X1,complement(join(X0,X1))))
| complement(X0) = join(X1,complement(join(X0,X1))) ),
inference(superposition,[],[f11,f98]) ).
fof(f1028,plain,
! [X0,X1] :
( zero != meet(X0,join(X1,complement(join(X0,X1))))
| complement(X0) = join(X1,complement(join(X0,X1))) ),
inference(trivial_inequality_removal,[],[f1017]) ).
fof(f1074,plain,
! [X0,X1] :
( zero != meet(X1,join(X0,complement(join(X0,X1))))
| complement(X1) = join(X0,complement(join(X0,X1))) ),
inference(superposition,[],[f1028,f6]) ).
fof(f1174,plain,
! [X0,X1] : meet(X0,zero) = meet(X0,complement(join(X1,X0))),
inference(superposition,[],[f37,f10]) ).
fof(f1215,plain,
! [X0,X1] : zero = meet(X0,complement(join(X1,X0))),
inference(forward_demodulation,[],[f1174,f394]) ).
fof(f1385,plain,
! [X0,X1] : join(X1,X0) = join(X0,join(X0,X1)),
inference(superposition,[],[f579,f97]) ).
fof(f1423,plain,
! [X2,X0,X1] : join(meet(X1,X2),X0) = meet(join(meet(X1,X2),X0),join(X0,X1)),
inference(superposition,[],[f15,f579]) ).
fof(f1445,plain,
! [X2,X0,X1] : join(meet(X1,X2),X0) = meet(join(X0,X1),join(meet(X1,X2),X0)),
inference(forward_demodulation,[],[f1423,f5]) ).
fof(f2077,plain,
! [X2,X0,X1] : meet(X1,join(meet(complement(X1),X0),X2)) = meet(X1,join(meet(complement(X1),X0),meet(join(X1,meet(complement(X1),X0)),join(meet(zero,X0),X2)))),
inference(superposition,[],[f152,f101]) ).
fof(f2192,plain,
! [X2,X0,X1] : meet(X1,join(meet(complement(X1),X0),X2)) = meet(X1,join(meet(complement(X1),X0),join(meet(zero,X0),X2))),
inference(forward_demodulation,[],[f2077,f973]) ).
fof(f2248,plain,
! [X2,X0,X1] : meet(X1,join(meet(complement(X1),X0),X2)) = meet(X1,join(meet(zero,X0),join(X2,meet(complement(X1),X0)))),
inference(forward_demodulation,[],[f2192,f63]) ).
fof(f2283,plain,
! [X2,X0,X1] : meet(X1,join(meet(complement(X1),X0),X2)) = meet(X1,join(zero,join(X2,meet(complement(X1),X0)))),
inference(forward_demodulation,[],[f2248,f373]) ).
fof(f2299,plain,
! [X2,X0,X1] : meet(X1,join(meet(complement(X1),X0),X2)) = meet(X1,join(X2,meet(complement(X1),X0))),
inference(forward_demodulation,[],[f2283,f369]) ).
fof(f2315,plain,
! [X2,X0,X1] : join(meet(join(X1,X0),X2),X1) = meet(join(X0,X1),join(meet(join(X1,X0),X2),X1)),
inference(superposition,[],[f1445,f1385]) ).
fof(f2316,plain,
! [X2,X0,X1] : join(meet(join(X1,X0),X2),X0) = meet(join(X0,X1),join(meet(join(X1,X0),X2),X0)),
inference(superposition,[],[f1445,f244]) ).
fof(f2336,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = meet(join(X2,X1),join(meet(X0,X1),X2)),
inference(superposition,[],[f1445,f32]) ).
fof(f2361,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = meet(join(join(meet(X1,X2),X0),X1),join(X0,meet(X1,X2))),
inference(superposition,[],[f1445,f1385]) ).
fof(f2417,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = meet(join(X0,meet(X1,X2)),join(join(meet(X1,X2),X0),X1)),
inference(forward_demodulation,[],[f2361,f5]) ).
fof(f2436,plain,
! [X2,X0,X1] : join(X0,meet(join(X1,X0),X2)) = meet(join(X0,X1),join(X0,meet(join(X1,X0),X2))),
inference(forward_demodulation,[],[f2316,f6]) ).
fof(f2437,plain,
! [X2,X0,X1] : join(X1,meet(join(X1,X0),X2)) = meet(join(X0,X1),join(X1,meet(join(X1,X0),X2))),
inference(forward_demodulation,[],[f2315,f6]) ).
fof(f2458,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = meet(join(X0,meet(X1,X2)),join(X1,join(meet(X1,X2),X0))),
inference(forward_demodulation,[],[f2417,f6]) ).
fof(f2487,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = meet(join(X0,meet(X1,X2)),join(X1,X0)),
inference(forward_demodulation,[],[f2458,f53]) ).
fof(f2500,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = meet(join(X1,X0),join(X0,meet(X1,X2))),
inference(forward_demodulation,[],[f2487,f5]) ).
fof(f2673,plain,
! [X0,X1] : zero = meet(X0,complement(join(X0,X1))),
inference(superposition,[],[f1215,f6]) ).
fof(f2796,plain,
! [X2,X0,X1] : meet(X0,join(complement(join(X0,X1)),X2)) = meet(X0,join(complement(join(X0,X1)),meet(join(X0,complement(join(X0,X1))),join(zero,X2)))),
inference(superposition,[],[f152,f2673]) ).
fof(f2814,plain,
! [X2,X0,X1] : meet(X0,join(complement(join(X0,X1)),X2)) = meet(X0,join(complement(join(X0,X1)),meet(join(X0,complement(join(X0,X1))),X2))),
inference(forward_demodulation,[],[f2796,f369]) ).
fof(f2874,plain,
! [X2,X0,X1] : meet(X0,join(complement(join(X0,X1)),X2)) = meet(X0,join(complement(join(X0,X1)),meet(join(X0,complement(join(X0,X1))),join(meet(X0,zero),X2)))),
inference(superposition,[],[f152,f117]) ).
fof(f2891,plain,
! [X2,X0,X1] : meet(X0,join(complement(join(X0,X1)),X2)) = meet(X0,join(complement(join(X0,X1)),join(meet(X0,zero),X2))),
inference(forward_demodulation,[],[f2874,f2814]) ).
fof(f2919,plain,
! [X2,X0,X1] : meet(X0,join(complement(join(X0,X1)),X2)) = meet(X0,join(meet(X0,zero),join(X2,complement(join(X0,X1))))),
inference(forward_demodulation,[],[f2891,f63]) ).
fof(f2930,plain,
! [X2,X0,X1] : meet(X0,join(complement(join(X0,X1)),X2)) = meet(X0,join(zero,join(X2,complement(join(X0,X1))))),
inference(forward_demodulation,[],[f2919,f394]) ).
fof(f2935,plain,
! [X2,X0,X1] : meet(X0,join(complement(join(X0,X1)),X2)) = meet(X0,join(X2,complement(join(X0,X1)))),
inference(forward_demodulation,[],[f2930,f369]) ).
fof(f3569,plain,
! [X2,X0,X1] : meet(X2,join(complement(X2),meet(X1,X0))) = meet(X2,join(complement(X2),meet(X0,meet(one,X1)))),
inference(superposition,[],[f186,f46]) ).
fof(f3575,plain,
! [X2,X0,X1] : meet(X2,join(complement(X2),join(X0,meet(join(one,X0),join(X1,meet(one,X0)))))) = meet(X2,join(complement(X2),meet(one,join(X0,X1)))),
inference(superposition,[],[f186,f12]) ).
fof(f3584,plain,
! [X0,X1] : meet(X1,join(complement(X1),X0)) = meet(X1,join(meet(one,X0),complement(X1))),
inference(superposition,[],[f186,f6]) ).
fof(f3637,plain,
! [X0,X1] : meet(X1,join(complement(X1),X0)) = meet(X1,join(X0,complement(X1))),
inference(forward_demodulation,[],[f3584,f210]) ).
fof(f3645,plain,
! [X2,X0,X1] : meet(X2,join(complement(X2),join(X0,meet(join(one,X0),join(X1,meet(one,X0)))))) = meet(X2,join(complement(X2),join(X0,X1))),
inference(forward_demodulation,[],[f3575,f186]) ).
fof(f3651,plain,
! [X2,X0,X1] : meet(X2,join(complement(X2),meet(X0,X1))) = meet(X2,join(complement(X2),meet(X1,X0))),
inference(forward_demodulation,[],[f3569,f110]) ).
fof(f3671,plain,
! [X2,X0,X1] : meet(X2,join(complement(X2),join(X0,X1))) = meet(X2,join(complement(X2),join(X0,meet(join(one,X0),join(X1,X0))))),
inference(forward_demodulation,[],[f3645,f210]) ).
fof(f3690,plain,
! [X2,X0,X1] : meet(X2,join(complement(X2),join(X0,X1))) = meet(X2,join(complement(X2),join(X0,meet(one,join(X1,X0))))),
inference(forward_demodulation,[],[f3671,f213]) ).
fof(f3702,plain,
! [X2,X0,X1] : meet(X2,join(complement(X2),join(X0,X1))) = meet(X2,join(complement(X2),join(X0,join(X1,X0)))),
inference(forward_demodulation,[],[f3690,f210]) ).
fof(f3710,plain,
! [X2,X0,X1] : meet(X2,join(complement(X2),join(X0,X1))) = meet(X2,join(complement(X2),join(X1,X0))),
inference(forward_demodulation,[],[f3702,f31]) ).
fof(f3726,plain,
! [X2,X0,X1] : meet(X2,join(complement(X2),join(X0,X1))) = meet(X2,join(X0,join(X1,complement(X2)))),
inference(superposition,[],[f3637,f8]) ).
fof(f4148,plain,
! [X2,X0,X1] : join(meet(join(X0,X1),X2),X1) = meet(join(X0,X1),join(meet(join(X0,X1),X2),X1)),
inference(superposition,[],[f1445,f31]) ).
fof(f4168,plain,
! [X2,X0,X1] : join(X1,meet(join(X0,X1),X2)) = meet(join(X0,X1),join(X1,meet(join(X0,X1),X2))),
inference(forward_demodulation,[],[f4148,f6]) ).
fof(f4442,plain,
! [X0,X1] :
( zero != meet(join(X0,complement(join(X1,X0))),join(X1,complement(one)))
| join(X1,complement(one)) = complement(join(X0,complement(join(X1,X0)))) ),
inference(superposition,[],[f1074,f98]) ).
fof(f4448,plain,
! [X0] :
( zero != meet(complement(X0),join(X0,complement(one)))
| complement(complement(X0)) = join(X0,complement(one)) ),
inference(superposition,[],[f1074,f9]) ).
fof(f4477,plain,
! [X0] :
( zero != meet(complement(X0),join(X0,zero))
| complement(complement(X0)) = join(X0,complement(one)) ),
inference(forward_demodulation,[],[f4448,f264]) ).
fof(f4480,plain,
! [X0,X1] :
( zero != meet(join(X1,complement(one)),join(X0,complement(join(X1,X0))))
| join(X1,complement(one)) = complement(join(X0,complement(join(X1,X0)))) ),
inference(forward_demodulation,[],[f4442,f5]) ).
fof(f4495,plain,
! [X0] :
( zero != meet(complement(X0),X0)
| complement(complement(X0)) = join(X0,complement(one)) ),
inference(forward_demodulation,[],[f4477,f103]) ).
fof(f4498,plain,
! [X0,X1] :
( zero != meet(join(X1,zero),join(X0,complement(join(X1,X0))))
| join(X1,complement(one)) = complement(join(X0,complement(join(X1,X0)))) ),
inference(forward_demodulation,[],[f4480,f264]) ).
fof(f4507,plain,
! [X0] :
( meet(X0,complement(X0)) != zero
| complement(complement(X0)) = join(X0,complement(one)) ),
inference(forward_demodulation,[],[f4495,f5]) ).
fof(f4510,plain,
! [X0,X1] :
( zero != meet(X1,join(X0,complement(join(X1,X0))))
| join(X1,complement(one)) = complement(join(X0,complement(join(X1,X0)))) ),
inference(forward_demodulation,[],[f4498,f103]) ).
fof(f4516,plain,
! [X0] : complement(complement(X0)) = join(X0,complement(one)),
inference(forward_subsumption_resolution,[],[f4507,f10]) ).
fof(f4519,plain,
! [X0,X1] :
( join(X1,zero) = complement(join(X0,complement(join(X1,X0))))
| zero != meet(X1,join(X0,complement(join(X1,X0)))) ),
inference(forward_demodulation,[],[f4510,f264]) ).
fof(f4523,plain,
! [X0] : join(X0,zero) = complement(complement(X0)),
inference(forward_demodulation,[],[f4516,f264]) ).
fof(f4526,plain,
! [X0,X1] :
( zero != meet(X1,join(X0,complement(join(X1,X0))))
| complement(join(X0,complement(join(X1,X0)))) = X1 ),
inference(forward_demodulation,[],[f4519,f103]) ).
fof(f4528,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_demodulation,[],[f4523,f103]) ).
fof(f4734,plain,
! [X0,X1] : meet(X0,join(meet(complement(X0),X1),zero)) = meet(X0,join(meet(complement(X0),X1),complement(join(X0,meet(complement(X0),X1))))),
inference(superposition,[],[f973,f10]) ).
fof(f4796,plain,
! [X0,X1] : meet(X0,join(meet(complement(X0),X1),complement(join(X0,meet(complement(X0),X1))))) = meet(X0,join(zero,meet(complement(X0),X1))),
inference(forward_demodulation,[],[f4734,f2299]) ).
fof(f4845,plain,
! [X0,X1] : meet(X0,meet(complement(X0),X1)) = meet(X0,join(meet(complement(X0),X1),complement(join(X0,meet(complement(X0),X1))))),
inference(forward_demodulation,[],[f4796,f369]) ).
fof(f4875,plain,
! [X0,X1] : meet(zero,X1) = meet(X0,join(meet(complement(X0),X1),complement(join(X0,meet(complement(X0),X1))))),
inference(forward_demodulation,[],[f4845,f101]) ).
fof(f4886,plain,
! [X0,X1] : zero = meet(X0,join(meet(complement(X0),X1),complement(join(X0,meet(complement(X0),X1))))),
inference(forward_demodulation,[],[f4875,f373]) ).
fof(f4968,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(X1,X2)) = meet(join(X1,X0),join(X1,meet(join(X0,X1),join(X2,meet(join(X1,X0),X1))))),
inference(superposition,[],[f135,f1385]) ).
fof(f4970,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(X0,X2)) = meet(join(X1,X0),join(X0,meet(join(X0,X1),join(X2,meet(join(X1,X0),X0))))),
inference(superposition,[],[f135,f244]) ).
fof(f5154,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(X0,X2)) = join(X0,meet(join(X0,X1),join(X2,meet(join(X1,X0),X0)))),
inference(forward_demodulation,[],[f4970,f2437]) ).
fof(f5156,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(X1,X2)) = join(X1,meet(join(X0,X1),join(X2,meet(join(X1,X0),X1)))),
inference(forward_demodulation,[],[f4968,f2436]) ).
fof(f5212,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X1),join(X2,meet(X0,join(X1,X0))))) = meet(join(X1,X0),join(X0,X2)),
inference(forward_demodulation,[],[f5154,f5]) ).
fof(f5214,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(X1,X2)) = join(X1,meet(join(X0,X1),join(X2,meet(X1,join(X1,X0))))),
inference(forward_demodulation,[],[f5156,f5]) ).
fof(f5253,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(X0,X2)) = join(X0,meet(join(X0,X1),join(X2,X0))),
inference(forward_demodulation,[],[f5212,f15]) ).
fof(f5255,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(X1,X2)) = join(X1,meet(join(X0,X1),join(X2,X1))),
inference(forward_demodulation,[],[f5214,f3]) ).
fof(f5417,plain,
! [X2,X0,X1] : meet(X2,join(complement(X2),join(complement(one),meet(X1,X0)))) = meet(X2,join(complement(X2),meet(one,join(complement(one),meet(X0,X1))))),
inference(superposition,[],[f186,f3651]) ).
fof(f5421,plain,
! [X2,X0,X1] : meet(X2,join(complement(X2),join(complement(one),meet(X1,X0)))) = meet(X2,join(complement(X2),join(complement(one),meet(X0,X1)))),
inference(forward_demodulation,[],[f5417,f186]) ).
fof(f5468,plain,
! [X2,X0,X1] : meet(X2,join(complement(X2),join(zero,meet(X1,X0)))) = meet(X2,join(complement(X2),join(zero,meet(X0,X1)))),
inference(forward_demodulation,[],[f5421,f264]) ).
fof(f5488,plain,
! [X2,X0,X1] : meet(X2,join(complement(X2),join(zero,meet(X1,X0)))) = meet(X2,join(zero,join(meet(X0,X1),complement(X2)))),
inference(forward_demodulation,[],[f5468,f3726]) ).
fof(f5501,plain,
! [X2,X0,X1] : meet(X2,join(meet(X0,X1),complement(X2))) = meet(X2,join(complement(X2),join(zero,meet(X1,X0)))),
inference(forward_demodulation,[],[f5488,f369]) ).
fof(f5513,plain,
! [X2,X0,X1] : meet(X2,join(meet(X0,X1),complement(X2))) = meet(X2,join(zero,join(meet(X1,X0),complement(X2)))),
inference(forward_demodulation,[],[f5501,f3726]) ).
fof(f5522,plain,
! [X2,X0,X1] : meet(X2,join(meet(X0,X1),complement(X2))) = meet(X2,join(meet(X1,X0),complement(X2))),
inference(forward_demodulation,[],[f5513,f369]) ).
fof(f5555,plain,
! [X2,X0,X1] : meet(complement(X0),join(meet(X1,X2),X0)) = meet(complement(X0),join(meet(X2,X1),X0)),
inference(superposition,[],[f5522,f4528]) ).
fof(f5626,plain,
! [X2,X3,X0,X1] : meet(X0,join(meet(X3,X2),complement(join(X0,X1)))) = meet(X0,meet(join(X0,X1),join(meet(X2,X3),complement(join(X0,X1))))),
inference(superposition,[],[f36,f5522]) ).
fof(f5637,plain,
! [X2,X3,X0,X1] : meet(X0,join(meet(X3,X2),complement(join(X0,X1)))) = meet(X0,join(meet(X2,X3),complement(join(X0,X1)))),
inference(forward_demodulation,[],[f5626,f36]) ).
fof(f6397,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X0,join(X2,X1)),
inference(superposition,[],[f8,f837]) ).
fof(f7284,plain,
! [X2,X0,X1] : meet(X2,meet(X1,X0)) = meet(X2,meet(X0,meet(one,X1))),
inference(superposition,[],[f110,f46]) ).
fof(f7304,plain,
! [X2,X0,X1] : meet(X2,join(complement(one),join(X1,X0))) = meet(X2,meet(one,join(complement(one),join(X0,X1)))),
inference(superposition,[],[f110,f3710]) ).
fof(f7417,plain,
! [X2,X0,X1] : meet(X2,join(complement(one),join(X1,X0))) = meet(X2,join(complement(one),join(X0,X1))),
inference(forward_demodulation,[],[f7304,f110]) ).
fof(f7435,plain,
! [X2,X0,X1] : meet(X2,meet(X0,X1)) = meet(X2,meet(X1,X0)),
inference(forward_demodulation,[],[f7284,f110]) ).
fof(f7453,plain,
! [X2,X0,X1] : meet(X2,join(zero,join(X1,X0))) = meet(X2,join(zero,join(X0,X1))),
inference(forward_demodulation,[],[f7417,f264]) ).
fof(f7470,plain,
! [X2,X0,X1] : meet(X2,join(X0,X1)) = meet(X2,join(zero,join(X1,X0))),
inference(forward_demodulation,[],[f7453,f369]) ).
fof(f7482,plain,
! [X2,X0,X1] : meet(X2,join(X0,X1)) = meet(X2,join(X1,X0)),
inference(forward_demodulation,[],[f7470,f369]) ).
fof(f7528,plain,
! [X2,X3,X0,X1] : meet(X3,join(X2,join(X0,X1))) = meet(X3,join(X0,join(X1,X2))),
inference(superposition,[],[f7482,f8]) ).
fof(f7625,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(X2,X1),X0),
inference(superposition,[],[f5,f7482]) ).
fof(f7653,plain,
! [X2,X3,X0,X1] : meet(meet(X0,X1),join(X2,X3)) = meet(X0,meet(X1,join(X3,X2))),
inference(superposition,[],[f7,f7482]) ).
fof(f7658,plain,
! [X2,X0,X1] : join(meet(X1,X2),X0) = meet(join(X0,X1),join(X0,meet(X1,X2))),
inference(superposition,[],[f1445,f7482]) ).
fof(f7678,plain,
! [X2,X3,X0,X1] : meet(X0,meet(X1,join(X2,X3))) = meet(X0,meet(X1,join(X3,X2))),
inference(forward_demodulation,[],[f7653,f7]) ).
fof(f7832,plain,
! [X2,X0,X1] : meet(join(X0,X1),X2) = meet(join(X1,X0),X2),
inference(superposition,[],[f5,f7625]) ).
fof(f9415,plain,
! [X2,X0,X1] : meet(complement(X0),join(X0,meet(X2,X1))) = meet(complement(X0),join(meet(X1,X2),X0)),
inference(superposition,[],[f7482,f5555]) ).
fof(f9941,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(X0,X1),meet(X0,X2))),
inference(superposition,[],[f84,f4]) ).
fof(f10369,plain,
! [X0,X1] : meet(X1,X0) = join(meet(X1,X0),meet(X0,X1)),
inference(superposition,[],[f44,f32]) ).
fof(f10752,plain,
! [X0,X1] : meet(X0,X1) = join(meet(X1,X0),meet(X0,X1)),
inference(superposition,[],[f31,f10369]) ).
fof(f10767,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(meet(X0,X1),join(X2,meet(X1,X0))),
inference(superposition,[],[f837,f10369]) ).
fof(f12327,plain,
! [X2,X0,X1] : join(X2,meet(X0,X1)) = join(X2,join(meet(X1,X0),meet(X0,X1))),
inference(superposition,[],[f6397,f10369]) ).
fof(f12451,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(join(X2,X1),X0),
inference(superposition,[],[f6,f6397]) ).
fof(f12609,plain,
! [X2,X0,X1] : join(X2,meet(X0,X1)) = join(X2,meet(X1,X0)),
inference(forward_demodulation,[],[f12327,f10369]) ).
fof(f13640,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(meet(X2,X1),X0),
inference(superposition,[],[f6,f12609]) ).
fof(f13687,plain,
! [X2,X3,X0,X1] : meet(join(meet(X2,X1),X0),X3) = meet(X3,join(X0,meet(X1,X2))),
inference(superposition,[],[f7625,f12609]) ).
fof(f13699,plain,
! [X2,X3,X0,X1] : meet(X0,join(X1,meet(X3,X2))) = meet(X0,join(X1,meet(join(X0,X1),join(meet(X0,X1),meet(X2,X3))))),
inference(superposition,[],[f152,f12609]) ).
fof(f13721,plain,
! [X2,X3,X0,X1] : meet(X0,join(X1,meet(X2,X3))) = meet(X0,join(X1,meet(X3,X2))),
inference(forward_demodulation,[],[f13699,f152]) ).
fof(f13891,plain,
! [X2,X3,X0,X1] : join(meet(X0,join(X1,X2)),X3) = join(X3,meet(join(X2,X1),X0)),
inference(superposition,[],[f13640,f7482]) ).
fof(f13958,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(meet(X1,X0),X2),
inference(superposition,[],[f6,f13640]) ).
fof(f14674,plain,
! [X0,X1] : one = join(meet(X0,X1),complement(meet(X1,X0))),
inference(superposition,[],[f9,f13958]) ).
fof(f16169,plain,
! [X0,X1] :
( one != one
| zero != meet(meet(X0,X1),complement(meet(X1,X0)))
| complement(meet(X0,X1)) = complement(meet(X1,X0)) ),
inference(superposition,[],[f11,f14674]) ).
fof(f16210,plain,
! [X0,X1] :
( zero != meet(meet(X0,X1),complement(meet(X1,X0)))
| complement(meet(X0,X1)) = complement(meet(X1,X0)) ),
inference(trivial_inequality_removal,[],[f16169]) ).
fof(f16240,plain,
! [X0,X1] :
( zero != meet(X0,meet(X1,complement(meet(X1,X0))))
| complement(meet(X0,X1)) = complement(meet(X1,X0)) ),
inference(forward_demodulation,[],[f16210,f7]) ).
fof(f16367,plain,
! [X0,X1] : complement(meet(X0,X1)) = complement(meet(X1,X0)),
inference(forward_subsumption_resolution,[],[f16240,f463]) ).
fof(f16566,plain,
! [X0,X1] : complement(join(X0,X1)) = complement(meet(join(X1,X0),join(X0,X1))),
inference(superposition,[],[f16367,f548]) ).
fof(f16635,plain,
! [X0,X1] : complement(join(X0,X1)) = complement(join(X1,X0)),
inference(forward_demodulation,[],[f16566,f548]) ).
fof(f17160,plain,
! [X0,X1] :
( zero != zero
| complement(X0) = join(meet(complement(X0),X1),complement(join(X0,meet(complement(X0),X1)))) ),
inference(superposition,[],[f1028,f4886]) ).
fof(f17216,plain,
! [X0,X1] : complement(X0) = join(meet(complement(X0),X1),complement(join(X0,meet(complement(X0),X1)))),
inference(trivial_inequality_removal,[],[f17160]) ).
fof(f17378,plain,
! [X0,X1] : join(meet(X0,X1),complement(join(complement(X0),meet(X0,X1)))) = X0,
inference(superposition,[],[f17216,f4528]) ).
fof(f17453,plain,
! [X0,X1] : join(X1,complement(X0)) = join(X1,complement(join(X0,meet(complement(X0),X1)))),
inference(superposition,[],[f54,f17216]) ).
fof(f17483,plain,
! [X2,X0,X1] : meet(complement(join(X0,meet(complement(X0),X1))),join(meet(complement(X0),X1),X2)) = meet(complement(join(X0,meet(complement(X0),X1))),join(meet(complement(X0),X1),meet(complement(X0),join(X2,meet(complement(join(X0,meet(complement(X0),X1))),meet(complement(X0),X1)))))),
inference(superposition,[],[f135,f17216]) ).
fof(f17527,plain,
! [X2,X0,X1] : meet(complement(join(X0,meet(complement(X0),X1))),join(meet(complement(X0),X1),X2)) = meet(complement(join(X0,meet(complement(X0),X1))),join(meet(complement(X0),X1),meet(complement(X0),join(X2,meet(meet(complement(X0),X1),complement(join(X0,meet(complement(X0),X1)))))))),
inference(forward_demodulation,[],[f17483,f13721]) ).
fof(f17597,plain,
! [X2,X0,X1] : meet(complement(join(X0,meet(complement(X0),X1))),join(meet(complement(X0),X1),X2)) = meet(complement(join(X0,meet(complement(X0),X1))),join(meet(complement(X0),X1),meet(complement(X0),join(X2,zero)))),
inference(forward_demodulation,[],[f17527,f1215]) ).
fof(f17630,plain,
! [X2,X0,X1] : meet(complement(join(X0,meet(complement(X0),X1))),join(meet(complement(X0),X1),X2)) = meet(complement(join(X0,meet(complement(X0),X1))),join(meet(complement(X0),X1),meet(complement(X0),X2))),
inference(forward_demodulation,[],[f17597,f103]) ).
fof(f17665,plain,
! [X0,X1] : join(meet(X0,X1),complement(join(complement(X1),meet(X0,X1)))) = X1,
inference(superposition,[],[f17378,f32]) ).
fof(f21257,plain,
! [X2,X3,X0,X1] : join(meet(join(X0,X1),join(X1,X2)),X3) = join(X1,join(X3,meet(join(X1,X0),join(X2,X1)))),
inference(superposition,[],[f837,f5253]) ).
fof(f22286,plain,
! [X2,X3,X0,X1,X4] : meet(X4,join(meet(X0,join(X1,X2)),X3)) = meet(X4,join(meet(join(X2,X1),X0),X3)),
inference(superposition,[],[f7482,f13891]) ).
fof(f32540,plain,
! [X0,X1] : join(X0,X1) = join(X0,complement(join(complement(join(X0,X1)),X0))),
inference(superposition,[],[f17665,f3]) ).
fof(f32541,plain,
! [X0,X1] : join(X1,X0) = join(X0,complement(join(complement(join(X1,X0)),X0))),
inference(superposition,[],[f17665,f15]) ).
fof(f32790,plain,
! [X0,X1] : join(X1,X0) = join(X0,complement(join(X0,complement(join(X1,X0))))),
inference(forward_demodulation,[],[f32541,f16635]) ).
fof(f32791,plain,
! [X0,X1] : join(X0,X1) = join(X0,complement(join(X0,complement(join(X0,X1))))),
inference(forward_demodulation,[],[f32540,f16635]) ).
fof(f33060,plain,
! [X0,X1] : join(X1,X0) = join(X1,complement(join(X1,complement(join(X0,X1))))),
inference(superposition,[],[f32791,f16635]) ).
fof(f33539,plain,
! [X2,X0,X1] : join(X2,join(X0,meet(X1,X2))) = join(X2,complement(join(meet(X1,X2),complement(join(X0,meet(X1,X2)))))),
inference(superposition,[],[f54,f32790]) ).
fof(f33568,plain,
! [X2,X0,X1] : join(X2,X0) = join(X2,complement(join(meet(X1,X2),complement(join(X0,meet(X1,X2)))))),
inference(forward_demodulation,[],[f33539,f773]) ).
fof(f33929,plain,
! [X0,X1] : join(X0,complement(join(X1,X0))) = join(X0,complement(join(X0,X1))),
inference(superposition,[],[f32791,f33060]) ).
fof(f34465,plain,
! [X2,X0,X1] : join(X0,complement(join(X0,meet(X1,X2)))) = join(X0,complement(join(meet(X2,X1),X0))),
inference(superposition,[],[f33929,f12609]) ).
fof(f34478,plain,
! [X2,X0,X1] : join(meet(X2,X1),complement(join(X0,meet(X2,X1)))) = join(meet(X2,X1),complement(join(X0,meet(X1,X2)))),
inference(superposition,[],[f33929,f13640]) ).
fof(f34502,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(join(X1,X0)),join(X0,complement(join(X0,X1)))),
inference(superposition,[],[f15,f33929]) ).
fof(f36445,plain,
! [X0,X1] : meet(X0,join(meet(X1,complement(meet(X0,X1))),zero)) = meet(X0,join(meet(X1,complement(meet(X0,X1))),complement(join(X0,meet(X1,complement(meet(X0,X1))))))),
inference(superposition,[],[f501,f10]) ).
fof(f36627,plain,
! [X0,X1] : meet(X0,join(meet(X1,complement(meet(X0,X1))),complement(join(X0,meet(X1,complement(meet(X0,X1))))))) = meet(X0,join(zero,meet(X1,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f36445,f7482]) ).
fof(f36789,plain,
! [X0,X1] : meet(X0,meet(X1,complement(meet(X0,X1)))) = meet(X0,join(meet(X1,complement(meet(X0,X1))),complement(join(X0,meet(X1,complement(meet(X0,X1))))))),
inference(forward_demodulation,[],[f36627,f369]) ).
fof(f36887,plain,
! [X0,X1] : zero = meet(X0,join(meet(X1,complement(meet(X0,X1))),complement(join(X0,meet(X1,complement(meet(X0,X1))))))),
inference(forward_demodulation,[],[f36789,f104]) ).
fof(f59215,plain,
! [X2,X0,X1] : join(X1,X0) = join(X1,meet(join(X0,X1),join(X0,X2))),
inference(superposition,[],[f64,f5255]) ).
fof(f59862,plain,
! [X2,X0,X1] : join(X1,meet(X0,X2)) = join(X1,meet(join(meet(X0,X2),X1),X0)),
inference(superposition,[],[f59215,f17378]) ).
fof(f59935,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(meet(join(X1,X0),join(X1,X2)),X0)) = meet(join(X1,X0),join(meet(join(X1,X0),join(X1,X2)),meet(join(X1,X0),join(X0,X1)))),
inference(superposition,[],[f180,f59215]) ).
fof(f60163,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(meet(join(X1,X0),join(X1,X2)),X0)) = join(meet(join(X1,X0),join(X1,X2)),meet(join(X1,X0),join(X0,X1))),
inference(forward_demodulation,[],[f59935,f9941]) ).
fof(f60194,plain,
! [X2,X0,X1] : join(X1,meet(X0,X2)) = join(X1,meet(X0,join(meet(X0,X2),X1))),
inference(forward_demodulation,[],[f59862,f12609]) ).
fof(f60344,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(meet(join(X1,X0),join(X1,X2)),X0)) = join(meet(join(X1,X0),join(X1,X2)),join(X1,X0)),
inference(forward_demodulation,[],[f60163,f548]) ).
fof(f60449,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(meet(join(X1,X0),join(X1,X2)),X0)) = join(join(X1,X0),meet(join(X1,X0),join(X1,X2))),
inference(forward_demodulation,[],[f60344,f6]) ).
fof(f60497,plain,
! [X2,X0,X1] : join(X1,X0) = meet(join(X1,X0),join(meet(join(X1,X0),join(X1,X2)),X0)),
inference(forward_demodulation,[],[f60449,f4]) ).
fof(f60529,plain,
! [X2,X0,X1] : join(X1,X0) = meet(join(X1,X0),join(X0,meet(join(X1,X0),join(X1,X2)))),
inference(forward_demodulation,[],[f60497,f7482]) ).
fof(f60549,plain,
! [X2,X0,X1] : join(X1,X0) = join(X0,meet(join(X1,X0),join(X1,X2))),
inference(forward_demodulation,[],[f60529,f4168]) ).
fof(f60720,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(X2,meet(join(meet(X0,X1),X2),X0)),
inference(superposition,[],[f60549,f17378]) ).
fof(f61071,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(X2,meet(X0,join(meet(X0,X1),X2))),
inference(forward_demodulation,[],[f60720,f12609]) ).
fof(f66654,plain,
! [X0,X1] : meet(complement(join(X0,meet(complement(X0),X1))),meet(complement(X0),X1)) = meet(complement(join(X0,meet(complement(X0),X1))),join(meet(complement(X0),X1),X1)),
inference(superposition,[],[f17630,f2]) ).
fof(f66807,plain,
! [X0,X1] : meet(complement(join(X0,meet(complement(X0),X1))),meet(complement(X0),X1)) = meet(complement(join(X0,meet(complement(X0),X1))),join(X1,meet(complement(X0),X1))),
inference(forward_demodulation,[],[f66654,f7482]) ).
fof(f66959,plain,
! [X0,X1] : meet(complement(join(X0,meet(complement(X0),X1))),meet(complement(X0),X1)) = meet(complement(join(X0,meet(complement(X0),X1))),X1),
inference(forward_demodulation,[],[f66807,f17]) ).
fof(f67040,plain,
! [X0,X1] : meet(complement(join(X0,meet(complement(X0),X1))),meet(complement(X0),X1)) = meet(X1,complement(join(X0,meet(complement(X0),X1)))),
inference(forward_demodulation,[],[f66959,f5]) ).
fof(f67104,plain,
! [X0,X1] : meet(meet(complement(X0),X1),complement(join(X0,meet(complement(X0),X1)))) = meet(X1,complement(join(X0,meet(complement(X0),X1)))),
inference(forward_demodulation,[],[f67040,f5]) ).
fof(f67161,plain,
! [X0,X1] : zero = meet(X1,complement(join(X0,meet(complement(X0),X1)))),
inference(forward_demodulation,[],[f67104,f1215]) ).
fof(f68754,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = meet(join(complement(join(meet(X1,X2),complement(join(X0,meet(X1,X2))))),X2),join(X0,meet(X1,X2))),
inference(superposition,[],[f2336,f32790]) ).
fof(f68955,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = meet(join(meet(X2,X1),X0),join(complement(join(meet(X1,X2),complement(join(X0,meet(X1,X2))))),X2)),
inference(forward_demodulation,[],[f68754,f13687]) ).
fof(f69166,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = meet(join(meet(X2,X1),X0),join(X2,complement(join(meet(X1,X2),complement(join(X0,meet(X1,X2))))))),
inference(forward_demodulation,[],[f68955,f7482]) ).
fof(f69313,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = meet(join(meet(X2,X1),X0),join(X2,X0)),
inference(forward_demodulation,[],[f69166,f33568]) ).
fof(f69404,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = meet(join(X0,X2),join(meet(X2,X1),X0)),
inference(forward_demodulation,[],[f69313,f7625]) ).
fof(f69853,plain,
! [X2,X0,X1] : meet(join(meet(X2,X1),X0),join(X0,X2)) = join(join(X0,meet(X1,X2)),meet(join(meet(X2,X1),X0),join(X0,X2))),
inference(superposition,[],[f10752,f69404]) ).
fof(f69892,plain,
! [X2,X0,X1] : meet(join(meet(X2,X1),X0),join(X0,X2)) = join(join(X0,meet(X1,X2)),meet(join(X0,X2),join(meet(X2,X1),X0))),
inference(forward_demodulation,[],[f69853,f12609]) ).
fof(f70223,plain,
! [X2,X0,X1] : meet(join(meet(X2,X1),X0),join(X0,X2)) = join(X0,join(meet(X1,X2),meet(join(X0,X2),join(meet(X2,X1),X0)))),
inference(forward_demodulation,[],[f69892,f8]) ).
fof(f70476,plain,
! [X2,X0,X1] : meet(join(meet(X2,X1),X0),join(X0,X2)) = join(meet(join(X2,X0),join(X0,meet(X2,X1))),meet(X1,X2)),
inference(forward_demodulation,[],[f70223,f21257]) ).
fof(f70634,plain,
! [X2,X0,X1] : meet(join(meet(X2,X1),X0),join(X0,X2)) = join(meet(X1,X2),meet(join(X2,X0),join(X0,meet(X2,X1)))),
inference(forward_demodulation,[],[f70476,f6]) ).
fof(f70734,plain,
! [X2,X0,X1] : meet(join(meet(X2,X1),X0),join(X0,X2)) = join(meet(X1,X2),join(X0,meet(X2,X1))),
inference(forward_demodulation,[],[f70634,f2500]) ).
fof(f70805,plain,
! [X2,X0,X1] : join(meet(X1,X2),X0) = meet(join(meet(X2,X1),X0),join(X0,X2)),
inference(forward_demodulation,[],[f70734,f10767]) ).
fof(f70846,plain,
! [X2,X0,X1] : join(meet(X1,X2),X0) = meet(join(X2,X0),join(meet(X2,X1),X0)),
inference(forward_demodulation,[],[f70805,f7625]) ).
fof(f70939,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(meet(X0,X2),join(zero,X1))) = join(meet(X2,X0),join(zero,X1)),
inference(superposition,[],[f70846,f100]) ).
fof(f71574,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(meet(X0,X2),join(zero,X1))) = join(zero,join(X1,meet(X2,X0))),
inference(forward_demodulation,[],[f70939,f63]) ).
fof(f71821,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = meet(join(X0,X1),join(meet(X0,X2),join(zero,X1))),
inference(forward_demodulation,[],[f71574,f369]) ).
fof(f71954,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = meet(join(X0,X1),join(zero,join(X1,meet(X0,X2)))),
inference(forward_demodulation,[],[f71821,f7528]) ).
fof(f72039,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = meet(join(X0,X1),join(X1,meet(X0,X2))),
inference(forward_demodulation,[],[f71954,f369]) ).
fof(f72352,plain,
! [X2,X0,X1] : meet(join(X0,X2),join(meet(X0,X1),X2)) = join(X2,meet(join(meet(X0,X1),X2),X0)),
inference(superposition,[],[f72039,f61071]) ).
fof(f72641,plain,
! [X2,X0,X1] : meet(join(X0,X2),join(meet(X0,X1),X2)) = join(X2,meet(X0,join(meet(X0,X1),X2))),
inference(forward_demodulation,[],[f72352,f12609]) ).
fof(f72897,plain,
! [X2,X0,X1] : join(X2,meet(X0,X1)) = meet(join(X0,X2),join(meet(X0,X1),X2)),
inference(forward_demodulation,[],[f72641,f60194]) ).
fof(f81233,plain,
! [X0,X1] : zero = meet(X0,join(meet(complement(join(X1,X0)),complement(zero)),complement(join(X0,meet(complement(join(X1,X0)),complement(zero)))))),
inference(superposition,[],[f36887,f1215]) ).
fof(f81613,plain,
! [X0,X1] : zero = meet(X0,join(meet(complement(zero),complement(join(X1,X0))),complement(join(X0,meet(complement(join(X1,X0)),complement(zero)))))),
inference(forward_demodulation,[],[f81233,f5637]) ).
fof(f81792,plain,
! [X0,X1] : zero = meet(X0,join(meet(complement(zero),complement(join(X1,X0))),complement(join(X0,meet(complement(zero),complement(join(X1,X0))))))),
inference(forward_demodulation,[],[f81613,f34478]) ).
fof(f81923,plain,
! [X0,X1] : zero = meet(X0,join(meet(one,complement(join(X1,X0))),complement(join(X0,meet(one,complement(join(X1,X0))))))),
inference(forward_demodulation,[],[f81792,f398]) ).
fof(f82006,plain,
! [X0,X1] : zero = meet(X0,join(complement(join(X1,X0)),complement(join(X0,complement(join(X1,X0)))))),
inference(forward_demodulation,[],[f81923,f210]) ).
fof(f82251,plain,
! [X0,X1] :
( zero != zero
| complement(X0) = join(complement(join(X1,X0)),complement(join(X0,complement(join(X1,X0))))) ),
inference(superposition,[],[f1028,f82006]) ).
fof(f82389,plain,
! [X0,X1] : complement(X0) = join(complement(join(X1,X0)),complement(join(X0,complement(join(X1,X0))))),
inference(trivial_inequality_removal,[],[f82251]) ).
fof(f82998,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X0),complement(join(meet(X0,X1),complement(X0)))),
inference(superposition,[],[f82389,f4]) ).
fof(f83083,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(join(complement(X0),meet(X1,X0))),complement(X0)),
inference(superposition,[],[f82389,f17665]) ).
fof(f83105,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(join(X1,X0)),complement(X0)),
inference(superposition,[],[f3,f82389]) ).
fof(f83110,plain,
! [X0,X1] : complement(X0) = join(complement(join(X1,X0)),complement(X0)),
inference(superposition,[],[f24,f82389]) ).
fof(f83297,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X1,X0))),
inference(forward_demodulation,[],[f83110,f6]) ).
fof(f83301,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(X0),complement(join(X1,X0))),
inference(forward_demodulation,[],[f83105,f5]) ).
fof(f83316,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(X0),complement(join(complement(X0),meet(X1,X0)))),
inference(forward_demodulation,[],[f83083,f6]) ).
fof(f83384,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X0),complement(join(complement(X0),meet(X1,X0)))),
inference(forward_demodulation,[],[f82998,f34465]) ).
fof(f83646,plain,
! [X0,X1] : complement(X0) = meet(complement(meet(X0,X1)),complement(X0)),
inference(superposition,[],[f83301,f4]) ).
fof(f83943,plain,
! [X0,X1] : complement(X0) = meet(complement(X0),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f83646,f5]) ).
fof(f84198,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(meet(X0,X1)),complement(X0)),
inference(superposition,[],[f17,f83943]) ).
fof(f84347,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X0),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f84198,f6]) ).
fof(f84486,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(X0,complement(meet(complement(X0),X1))),
inference(superposition,[],[f84347,f4528]) ).
fof(f84617,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X1),complement(meet(X0,X1))),
inference(superposition,[],[f84347,f16367]) ).
fof(f84958,plain,
! [X0,X1] : complement(X0) = join(complement(join(X0,X1)),complement(X0)),
inference(superposition,[],[f84617,f3]) ).
fof(f85105,plain,
! [X2,X0,X1] : join(complement(meet(X0,X1)),X2) = join(complement(X1),join(X2,complement(meet(X0,X1)))),
inference(superposition,[],[f837,f84617]) ).
fof(f85282,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X0,X1))),
inference(forward_demodulation,[],[f84958,f6]) ).
fof(f85447,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),X1))) = X0,
inference(superposition,[],[f85282,f4528]) ).
fof(f86576,plain,
! [X2,X0,X1] : meet(complement(meet(complement(X0),X1)),join(meet(X0,X2),complement(meet(complement(X0),X1)))) = join(complement(meet(complement(X0),X1)),meet(X0,X2)),
inference(superposition,[],[f72897,f84486]) ).
fof(f86622,plain,
! [X2,X0,X1] : complement(meet(complement(X0),X1)) = join(complement(meet(complement(X0),X1)),meet(X0,X2)),
inference(forward_demodulation,[],[f86576,f15]) ).
fof(f86930,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = meet(complement(join(complement(X0),X1)),X0),
inference(superposition,[],[f15,f85447]) ).
fof(f87156,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = meet(X0,complement(join(complement(X0),X1))),
inference(forward_demodulation,[],[f86930,f5]) ).
fof(f87412,plain,
! [X2,X0,X1] : meet(X2,X0) = join(meet(X2,X0),meet(X2,complement(join(complement(X0),X1)))),
inference(superposition,[],[f44,f87156]) ).
fof(f87449,plain,
! [X2,X0,X1] : join(complement(join(complement(X0),X1)),X2) = meet(join(X2,X0),join(X2,complement(join(complement(X0),X1)))),
inference(superposition,[],[f7658,f87156]) ).
fof(f87931,plain,
! [X2,X0,X1] : join(complement(meet(X0,X1)),X2) = join(X2,join(complement(join(complement(X0),meet(X1,X0))),complement(X0))),
inference(superposition,[],[f12451,f83384]) ).
fof(f87979,plain,
! [X2,X0,X1] : join(complement(meet(X0,X1)),X2) = join(X2,join(complement(X0),complement(join(complement(X0),meet(X1,X0))))),
inference(forward_demodulation,[],[f87931,f6397]) ).
fof(f88191,plain,
! [X2,X0,X1] : join(complement(meet(X0,X1)),X2) = join(X2,complement(meet(X1,X0))),
inference(forward_demodulation,[],[f87979,f83316]) ).
fof(f89332,plain,
! [X0,X1] : meet(complement(X1),X0) = join(meet(complement(X1),X0),complement(join(complement(X0),X1))),
inference(superposition,[],[f87412,f83301]) ).
fof(f89970,plain,
! [X0,X1] : meet(X0,X1) = join(meet(X0,X1),complement(join(complement(X1),complement(X0)))),
inference(superposition,[],[f89332,f4528]) ).
fof(f91375,plain,
! [X0,X1] : complement(complement(join(complement(X1),complement(X0)))) = join(complement(complement(join(complement(X1),complement(X0)))),complement(meet(X0,X1))),
inference(superposition,[],[f83297,f89970]) ).
fof(f91379,plain,
! [X0,X1] : complement(complement(join(complement(X1),complement(X0)))) = join(complement(meet(X1,X0)),complement(complement(join(complement(X1),complement(X0))))),
inference(forward_demodulation,[],[f91375,f88191]) ).
fof(f91574,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = join(complement(meet(X1,X0)),join(complement(X1),complement(X0))),
inference(forward_demodulation,[],[f91379,f4528]) ).
fof(f91713,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = join(complement(X0),join(complement(meet(X1,X0)),complement(X1))),
inference(forward_demodulation,[],[f91574,f63]) ).
fof(f91805,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = join(complement(X0),join(complement(X1),complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f91713,f6397]) ).
fof(f91865,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = join(complement(meet(X1,X0)),complement(X1)),
inference(forward_demodulation,[],[f91805,f85105]) ).
fof(f91913,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = join(complement(X1),complement(meet(X1,X0))),
inference(forward_demodulation,[],[f91865,f6]) ).
fof(f91940,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(X1),complement(X0)),
inference(forward_demodulation,[],[f91913,f84347]) ).
fof(f92000,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(X0,complement(X1)),
inference(superposition,[],[f91940,f4528]) ).
fof(f92007,plain,
! [X0,X1] : join(complement(X1),X0) = complement(meet(X1,complement(X0))),
inference(superposition,[],[f91940,f4528]) ).
fof(f92214,plain,
! [X0,X1] : complement(complement(X1)) = join(complement(complement(meet(X0,X1))),complement(join(complement(X1),complement(complement(meet(X0,X1)))))),
inference(superposition,[],[f82389,f91940]) ).
fof(f92221,plain,
! [X0,X1] : complement(complement(X1)) = complement(meet(complement(meet(X0,X1)),join(complement(X1),complement(complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f92214,f91940]) ).
fof(f92358,plain,
! [X0,X1] : complement(complement(X1)) = join(meet(X0,X1),complement(join(complement(X1),complement(complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f92221,f92000]) ).
fof(f92420,plain,
! [X0,X1] : complement(complement(X1)) = join(meet(X0,X1),complement(complement(meet(X1,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f92358,f91940]) ).
fof(f92453,plain,
! [X0,X1] : complement(complement(X1)) = join(meet(X0,X1),meet(X1,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f92420,f4528]) ).
fof(f92469,plain,
! [X0,X1] : join(meet(X0,X1),meet(X1,complement(meet(X0,X1)))) = X1,
inference(forward_demodulation,[],[f92453,f4528]) ).
fof(f92543,plain,
! [X0,X1] : meet(X0,complement(X1)) = complement(join(complement(X0),X1)),
inference(superposition,[],[f4528,f92007]) ).
fof(f92795,plain,
! [X2,X0,X1] : join(X0,complement(join(X2,X1))) = complement(meet(complement(X0),join(X1,X2))),
inference(superposition,[],[f92000,f7482]) ).
fof(f92883,plain,
! [X0,X1] : meet(complement(X0),X1) = complement(join(X0,complement(X1))),
inference(superposition,[],[f4528,f92000]) ).
fof(f93017,plain,
! [X2,X0,X1] : join(X0,complement(join(X1,X2))) = join(X0,complement(join(X2,X1))),
inference(forward_demodulation,[],[f92795,f92000]) ).
fof(f93217,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(X1),complement(X0)),
inference(superposition,[],[f92883,f4528]) ).
fof(f93548,plain,
! [X2,X0,X1] : complement(join(X2,meet(X0,complement(X1)))) = meet(complement(X2),join(complement(X0),X1)),
inference(superposition,[],[f93217,f92007]) ).
fof(f93665,plain,
! [X2,X0,X1] : meet(X2,complement(join(X0,X1))) = meet(X2,meet(complement(X1),complement(X0))),
inference(superposition,[],[f7435,f93217]) ).
fof(f93765,plain,
! [X2,X0,X1] : meet(X2,complement(join(X0,X1))) = meet(X2,complement(join(X1,X0))),
inference(forward_demodulation,[],[f93665,f93217]) ).
fof(f99004,plain,
! [X0,X1] : join(X1,X0) = join(X1,meet(X0,complement(meet(X1,X0)))),
inference(superposition,[],[f53,f92469]) ).
fof(f99896,plain,
! [X0,X1] : zero = meet(X0,join(meet(X1,complement(meet(X0,X1))),complement(join(X0,X1)))),
inference(superposition,[],[f36887,f99004]) ).
fof(f99981,plain,
! [X0,X1] :
( zero != meet(X0,join(meet(X1,complement(meet(X0,X1))),complement(join(X0,X1))))
| complement(join(meet(X1,complement(meet(X0,X1))),complement(join(X0,X1)))) = X0 ),
inference(superposition,[],[f4526,f99004]) ).
fof(f100160,plain,
! [X0,X1] :
( zero != meet(X0,join(complement(join(X0,X1)),meet(X1,complement(meet(X0,X1)))))
| complement(join(meet(X1,complement(meet(X0,X1))),complement(join(X0,X1)))) = X0 ),
inference(forward_demodulation,[],[f99981,f2935]) ).
fof(f100219,plain,
! [X0,X1] : zero = meet(X0,join(complement(join(X0,X1)),meet(X1,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f99896,f2935]) ).
fof(f100418,plain,
! [X0,X1] :
( complement(join(complement(join(X0,X1)),meet(X1,complement(meet(X0,X1))))) = X0
| zero != meet(X0,join(complement(join(X0,X1)),meet(X1,complement(meet(X0,X1))))) ),
inference(forward_demodulation,[],[f100160,f16635]) ).
fof(f100609,plain,
! [X0,X1] : complement(join(complement(join(X0,X1)),meet(X1,complement(meet(X0,X1))))) = X0,
inference(forward_subsumption_resolution,[],[f100418,f100219]) ).
fof(f100732,plain,
! [X0,X1] : meet(complement(complement(join(X0,X1))),join(complement(X1),meet(X0,X1))) = X0,
inference(forward_demodulation,[],[f100609,f93548]) ).
fof(f100804,plain,
! [X0,X1] : meet(join(X0,X1),join(complement(X1),meet(X0,X1))) = X0,
inference(forward_demodulation,[],[f100732,f4528]) ).
fof(f101308,plain,
! [X2,X3,X0,X1] : meet(X3,join(X0,complement(join(X1,X2)))) = meet(join(complement(join(X2,X1)),X0),X3),
inference(superposition,[],[f7625,f93017]) ).
fof(f103603,plain,
! [X0,X1] : meet(complement(X1),X0) = meet(complement(X1),join(X0,X1)),
inference(superposition,[],[f113,f100804]) ).
fof(f103615,plain,
! [X0,X1] : join(complement(X1),meet(X0,X1)) = join(join(complement(X1),meet(X0,X1)),X0),
inference(superposition,[],[f17,f100804]) ).
fof(f103663,plain,
! [X2,X0,X1] : meet(complement(X1),join(X1,X0)) = meet(complement(X1),join(meet(join(complement(X2),meet(X0,X2)),join(X0,X2)),X1)),
inference(superposition,[],[f9415,f100804]) ).
fof(f103759,plain,
! [X2,X0,X1] : meet(complement(X1),join(X1,X0)) = meet(complement(X1),join(meet(join(X0,X2),join(meet(X0,X2),complement(X2))),X1)),
inference(forward_demodulation,[],[f103663,f22286]) ).
fof(f103801,plain,
! [X0,X1] : join(complement(X1),meet(X0,X1)) = join(X0,join(complement(X1),meet(X0,X1))),
inference(forward_demodulation,[],[f103615,f6]) ).
fof(f104070,plain,
! [X2,X0,X1] : meet(complement(X1),join(X1,X0)) = meet(complement(X1),meet(join(X0,X2),join(meet(X0,X2),complement(X2)))),
inference(forward_demodulation,[],[f103759,f103603]) ).
fof(f104096,plain,
! [X0,X1] : join(X0,complement(X1)) = join(complement(X1),meet(X0,X1)),
inference(forward_demodulation,[],[f103801,f74]) ).
fof(f104312,plain,
! [X2,X0,X1] : meet(complement(X1),join(X1,X0)) = meet(complement(X1),meet(join(X0,X2),join(complement(X2),meet(X0,X2)))),
inference(forward_demodulation,[],[f104070,f7678]) ).
fof(f104495,plain,
! [X0,X1] : meet(complement(X1),X0) = meet(complement(X1),join(X1,X0)),
inference(forward_demodulation,[],[f104312,f100804]) ).
fof(f105134,plain,
! [X0,X1] : join(complement(complement(join(X1,meet(complement(X1),X0)))),zero) = join(X0,complement(complement(join(X1,meet(complement(X1),X0))))),
inference(superposition,[],[f104096,f67161]) ).
fof(f105188,plain,
! [X0,X1] : join(complement(complement(X1)),complement(join(X0,X1))) = join(complement(X0),complement(complement(X1))),
inference(superposition,[],[f104096,f93217]) ).
fof(f105241,plain,
! [X0,X1] : join(X0,complement(X1)) = join(complement(X1),meet(X1,X0)),
inference(superposition,[],[f12609,f104096]) ).
fof(f105295,plain,
! [X2,X0,X1] : join(join(X0,complement(X1)),X2) = join(complement(X1),join(X2,meet(X0,X1))),
inference(superposition,[],[f837,f104096]) ).
fof(f105430,plain,
! [X2,X0,X1] : join(X0,join(complement(X1),X2)) = join(complement(X1),join(X2,meet(X0,X1))),
inference(forward_demodulation,[],[f105295,f8]) ).
fof(f105501,plain,
! [X0,X1] : complement(meet(X0,complement(X1))) = join(complement(complement(X1)),complement(join(X0,X1))),
inference(forward_demodulation,[],[f105188,f91940]) ).
fof(f105542,plain,
! [X0,X1] : join(join(X1,meet(complement(X1),X0)),zero) = join(X0,join(X1,meet(complement(X1),X0))),
inference(forward_demodulation,[],[f105134,f4528]) ).
fof(f105712,plain,
! [X0,X1] : complement(meet(X0,complement(X1))) = complement(meet(complement(X1),join(X0,X1))),
inference(forward_demodulation,[],[f105501,f91940]) ).
fof(f105747,plain,
! [X0,X1] : join(X0,X1) = join(join(X1,meet(complement(X1),X0)),zero),
inference(forward_demodulation,[],[f105542,f773]) ).
fof(f105849,plain,
! [X0,X1] : join(X1,complement(join(X0,X1))) = complement(meet(X0,complement(X1))),
inference(forward_demodulation,[],[f105712,f92000]) ).
fof(f105877,plain,
! [X0,X1] : join(X0,X1) = join(zero,join(X1,meet(complement(X1),X0))),
inference(forward_demodulation,[],[f105747,f6]) ).
fof(f105937,plain,
! [X0,X1] : join(X1,complement(join(X0,X1))) = join(complement(X0),X1),
inference(forward_demodulation,[],[f105849,f92007]) ).
fof(f105952,plain,
! [X0,X1] : join(X0,X1) = join(X1,meet(complement(X1),X0)),
inference(forward_demodulation,[],[f105877,f369]) ).
fof(f106859,plain,
! [X0,X1] : join(X0,complement(join(X0,X1))) = join(X0,complement(X1)),
inference(superposition,[],[f17453,f105952]) ).
fof(f107014,plain,
! [X0,X1] : meet(join(X0,X1),join(complement(meet(complement(X1),X0)),meet(X1,meet(complement(X1),X0)))) = X1,
inference(superposition,[],[f100804,f105952]) ).
fof(f107082,plain,
! [X0,X1] : meet(join(X0,X1),complement(meet(complement(X1),X0))) = X1,
inference(forward_demodulation,[],[f107014,f86622]) ).
fof(f107313,plain,
! [X0,X1] : meet(join(X0,X1),join(X1,complement(X0))) = X1,
inference(forward_demodulation,[],[f107082,f92000]) ).
fof(f107861,plain,
! [X0,X1] : join(complement(X0),complement(complement(meet(X0,X1)))) = join(complement(X0),complement(complement(X1))),
inference(superposition,[],[f106859,f91940]) ).
fof(f108009,plain,
! [X0,X1] : complement(join(complement(join(X0,X1)),X0)) = meet(complement(join(complement(join(X0,X1)),X0)),join(X0,complement(join(X0,complement(X1))))),
inference(superposition,[],[f34502,f106859]) ).
fof(f108118,plain,
! [X0,X1] : complement(join(complement(join(X0,X1)),X0)) = meet(join(complement(join(complement(X1),X0)),X0),complement(join(complement(join(X0,X1)),X0))),
inference(forward_demodulation,[],[f108009,f101308]) ).
fof(f108217,plain,
! [X0,X1] : complement(meet(X0,complement(X1))) = join(complement(X0),complement(complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f107861,f91940]) ).
fof(f108326,plain,
! [X0,X1] : complement(join(complement(join(X0,X1)),X0)) = meet(join(complement(join(complement(X1),X0)),X0),complement(join(X0,complement(join(X0,X1))))),
inference(forward_demodulation,[],[f108118,f93765]) ).
fof(f108397,plain,
! [X0,X1] : complement(meet(X0,complement(X1))) = complement(meet(X0,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f108217,f91940]) ).
fof(f108461,plain,
! [X0,X1] : complement(join(complement(join(X0,X1)),X0)) = meet(join(X0,complement(join(complement(X1),X0))),complement(join(X0,complement(join(X0,X1))))),
inference(forward_demodulation,[],[f108326,f7832]) ).
fof(f108504,plain,
! [X0,X1] : join(complement(X0),meet(X0,X1)) = complement(meet(X0,complement(X1))),
inference(forward_demodulation,[],[f108397,f92007]) ).
fof(f108547,plain,
! [X0,X1] : complement(join(complement(join(X0,X1)),X0)) = meet(join(X0,complement(join(complement(X1),X0))),meet(complement(X0),join(X0,X1))),
inference(forward_demodulation,[],[f108461,f92883]) ).
fof(f108577,plain,
! [X0,X1] : join(complement(X0),X1) = join(complement(X0),meet(X0,X1)),
inference(forward_demodulation,[],[f108504,f92007]) ).
fof(f108604,plain,
! [X0,X1] : complement(join(complement(join(X0,X1)),X0)) = meet(meet(complement(X0),join(X0,X1)),join(X0,complement(join(complement(X1),X0)))),
inference(forward_demodulation,[],[f108547,f5]) ).
fof(f108636,plain,
! [X0,X1] : complement(join(complement(join(X0,X1)),X0)) = meet(complement(X0),meet(join(X0,X1),join(X0,complement(join(complement(X1),X0))))),
inference(forward_demodulation,[],[f108604,f7]) ).
fof(f108651,plain,
! [X0,X1] : complement(join(complement(join(X0,X1)),X0)) = meet(complement(X0),join(complement(join(complement(X1),X0)),X0)),
inference(forward_demodulation,[],[f108636,f87449]) ).
fof(f108658,plain,
! [X0,X1] : complement(join(complement(join(X0,X1)),X0)) = meet(complement(X0),join(X0,complement(join(complement(X1),X0)))),
inference(forward_demodulation,[],[f108651,f7482]) ).
fof(f108664,plain,
! [X0,X1] : complement(join(complement(join(X0,X1)),X0)) = meet(complement(X0),complement(join(complement(X1),X0))),
inference(forward_demodulation,[],[f108658,f104495]) ).
fof(f108667,plain,
! [X0,X1] : complement(join(complement(X1),X0)) = complement(join(complement(join(X0,X1)),X0)),
inference(forward_demodulation,[],[f108664,f83301]) ).
fof(f108669,plain,
! [X0,X1] : complement(join(X0,complement(join(X0,X1)))) = complement(join(complement(X1),X0)),
inference(forward_demodulation,[],[f108667,f16635]) ).
fof(f108671,plain,
! [X0,X1] : meet(X1,complement(X0)) = complement(join(X0,complement(join(X0,X1)))),
inference(forward_demodulation,[],[f108669,f92543]) ).
fof(f108673,plain,
! [X0,X1] : meet(X1,complement(X0)) = meet(complement(X0),join(X0,X1)),
inference(forward_demodulation,[],[f108671,f92883]) ).
fof(f108692,plain,
! [X2,X0,X1] : join(complement(X0),meet(X0,X1)) = join(complement(X0),meet(join(X2,X0),X1)),
inference(superposition,[],[f108577,f37]) ).
fof(f109205,plain,
! [X2,X0,X1] : join(X1,complement(X0)) = join(complement(X0),meet(join(X2,X0),X1)),
inference(forward_demodulation,[],[f108692,f105241]) ).
fof(f109622,plain,
! [X0,X1] : meet(X1,X0) = meet(X0,join(complement(X0),X1)),
inference(superposition,[],[f108673,f4528]) ).
fof(f110804,plain,
! [X2,X0,X1] : meet(join(X2,X0),X1) = meet(X1,join(X0,join(complement(X1),X2))),
inference(superposition,[],[f109622,f63]) ).
fof(f116101,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = meet(join(X0,X1),join(join(X1,meet(X2,X0)),complement(X0))),
inference(superposition,[],[f107313,f773]) ).
fof(f116254,plain,
! [X2,X0,X1] : meet(X0,meet(join(X0,X1),join(X2,meet(X0,X1)))) = meet(X0,meet(join(X1,X2),join(meet(join(X0,X1),join(X2,meet(X0,X1))),complement(X1)))),
inference(superposition,[],[f167,f107313]) ).
fof(f116477,plain,
! [X2,X0,X1] : meet(X0,meet(join(X0,X1),join(X2,meet(X0,X1)))) = meet(X0,meet(join(X1,X2),join(complement(X1),meet(join(X0,X1),join(X2,meet(X0,X1)))))),
inference(forward_demodulation,[],[f116254,f7678]) ).
fof(f116586,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = meet(join(X0,X1),join(complement(X0),join(X1,meet(X2,X0)))),
inference(forward_demodulation,[],[f116101,f7482]) ).
fof(f116679,plain,
! [X2,X0,X1] : meet(X0,meet(join(X0,X1),join(X2,meet(X0,X1)))) = meet(X0,meet(join(X1,X2),join(join(X2,meet(X0,X1)),complement(X1)))),
inference(forward_demodulation,[],[f116477,f109205]) ).
fof(f116756,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = meet(join(X0,X1),join(X2,join(complement(X0),X1))),
inference(forward_demodulation,[],[f116586,f105430]) ).
fof(f116817,plain,
! [X2,X0,X1] : meet(X0,meet(join(X0,X1),join(X2,meet(X0,X1)))) = meet(X0,meet(join(X1,X2),join(complement(X1),join(X2,meet(X0,X1))))),
inference(forward_demodulation,[],[f116679,f7678]) ).
fof(f116912,plain,
! [X2,X0,X1] : meet(X0,meet(join(X0,X1),join(X2,meet(X0,X1)))) = meet(X0,meet(join(X1,X2),join(X0,join(complement(X1),X2)))),
inference(forward_demodulation,[],[f116817,f105430]) ).
fof(f116970,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,meet(join(X0,X1),join(X2,meet(X0,X1)))),
inference(forward_demodulation,[],[f116912,f113]) ).
fof(f117005,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,join(X2,meet(X0,X1))),
inference(forward_demodulation,[],[f116970,f36]) ).
fof(f119220,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X2,join(complement(X0),X1))) = meet(join(X0,X1),join(complement(join(X0,X1)),join(X2,X1))),
inference(superposition,[],[f3726,f105937]) ).
fof(f119513,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X1,join(complement(join(X0,X1)),X2))) = meet(join(X0,X1),join(X2,join(complement(X0),X1))),
inference(forward_demodulation,[],[f119220,f7528]) ).
fof(f119713,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = meet(join(X0,X1),join(X1,join(complement(join(X0,X1)),X2))),
inference(forward_demodulation,[],[f119513,f116756]) ).
fof(f119854,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = meet(join(X2,X1),join(X0,X1)),
inference(forward_demodulation,[],[f119713,f110804]) ).
fof(f120166,plain,
! [X2,X0,X1] : meet(X0,join(X2,meet(X0,X1))) = join(meet(X0,X1),meet(X0,X2)),
inference(superposition,[],[f119854,f4]) ).
fof(f120980,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = join(meet(X0,X1),meet(X0,X2)),
inference(forward_demodulation,[],[f120166,f117005]) ).
fof(f122024,plain,
meet(a,join(b,c)) != meet(a,join(b,c)),
inference(superposition,[],[f13,f120980]) ).
fof(f122232,plain,
$false,
inference(trivial_inequality_removal,[],[f122024]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LAT204-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.18/0.43 % Computer : n007.cluster.edu
% 0.18/0.43 % Model : x86_64 x86_64
% 0.18/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.43 % Memory : 8046.5625MB
% 0.18/0.43 % OS : Linux 6.8.0-71-generic
% 0.18/0.43 % CPULimit : 300
% 0.18/0.43 % WCLimit : 300
% 0.18/0.43 % DateTime : Sun Sep 27 14:03:55 UTC 2026
% 0.18/0.43 % CPUTime :
% 0.18/0.43 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.22/0.49 Running first-order theorem proving
% 0.22/0.49 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 20.72/3.76 % (1437508)Input is clausal, will run a generic CNF schedule.
% 20.72/3.76 % (1437514)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1900653192:i=132376:av=off_3000 on theBenchmark for (3000ds/132376Mi)
% 20.72/3.76 % (1437518)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3373795435:s2a=on:i=180:gtg=position_3000 on theBenchmark for (3000ds/180Mi)
% 20.72/3.76 % (1437516)lrs+10_1_sil=8000:sp=occurrence:random_seed=3448065606:i=107:sd=3:ss=axioms:sgt=8_3000 on theBenchmark for (3000ds/107Mi)
% 20.72/3.76 % (1437519)dis-21_1_sil=8000:lcm=predicate:random_seed=3272034214:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_3000 on theBenchmark for (3000ds/117Mi)
% 20.72/3.76 % (1437515)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3429915585:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_3000 on theBenchmark for (3000ds/137899Mi)
% 20.72/3.76 % (1437517)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=56795837:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_3000 on theBenchmark for (3000ds/114Mi)
% 20.72/3.76 % (1437513)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2660410922:i=140167_3000 on theBenchmark for (3000ds/140167Mi)
% 20.72/3.76 % (1437519)Refutation not found, incomplete strategy
% 20.72/3.76 % (1437519)------------------------------
% 20.72/3.76 % (1437519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.72/3.76 % (1437519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.72/3.76 % (1437519)CaDiCaL version: 2.1.3
% 20.72/3.76 % (1437519)Termination reason: Refutation not found, incomplete strategy
% 20.72/3.76 % (1437519)Time elapsed: 0.003 s
% 20.72/3.76 % (1437519)Peak memory usage: 88 MB
% 20.72/3.76 % (1437519)Instructions burned: 1 (million)
% 20.72/3.76 % (1437516)Instruction limit reached!
% 20.72/3.76 % (1437516)------------------------------
% 20.72/3.76 % (1437516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.72/3.76 % (1437516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.72/3.76 % (1437516)CaDiCaL version: 2.1.3
% 20.72/3.76 % (1437516)Termination reason: Instruction limit
% 20.72/3.76 % (1437516)Termination phase: Saturation
% 20.72/3.76 % (1437516)Time elapsed: 0.102 s
% 20.72/3.76 % (1437516)Peak memory usage: 88 MB
% 20.72/3.76 % (1437516)Instructions burned: 108 (million)
% 20.72/3.76 % (1437517)Instruction limit reached!
% 20.72/3.76 % (1437517)------------------------------
% 20.72/3.76 % (1437517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.72/3.76 % (1437517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.72/3.76 % (1437517)CaDiCaL version: 2.1.3
% 20.72/3.76 % (1437517)Termination reason: Instruction limit
% 20.72/3.76 % (1437517)Termination phase: Saturation
% 20.72/3.76 % (1437517)Time elapsed: 0.115 s
% 20.72/3.76 % (1437517)Peak memory usage: 89 MB
% 20.72/3.76 % (1437517)Instructions burned: 116 (million)
% 20.72/3.76 % (1437518)Instruction limit reached!
% 20.72/3.76 % (1437518)------------------------------
% 20.72/3.76 % (1437518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.72/3.76 % (1437518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.72/3.76 % (1437518)CaDiCaL version: 2.1.3
% 20.72/3.76 % (1437518)Termination reason: Instruction limit
% 20.72/3.76 % (1437518)Termination phase: Saturation
% 20.72/3.76 % (1437518)Time elapsed: 0.162 s
% 20.72/3.76 % (1437518)Peak memory usage: 89 MB
% 20.72/3.76 % (1437518)Instructions burned: 181 (million)
% 20.72/3.76 % (1437519)------------------------------
% 20.72/3.76 % (1437519)------------------------------
% 20.72/3.76 % (1437527)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=127323772:i=143:sd=2:aac=none:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/143Mi)
% 20.72/3.76 % (1437528)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1113961742:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 20.72/3.76 % (1437527)Refutation not found, incomplete strategy
% 20.72/3.76 % (1437527)------------------------------
% 20.72/3.76 % (1437527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.72/3.76 % (1437527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.30/6.08 % (1437528)Refutation not found, incomplete strategy
% 37.30/6.08 % (1437528)------------------------------
% 37.30/6.08 % (1437528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.30/6.08 % (1437528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.30/6.08 % (1437528)CaDiCaL version: 2.1.3
% 37.30/6.08 % (1437527)CaDiCaL version: 2.1.3
% 37.30/6.08 % (1437527)Termination reason: Refutation not found, incomplete strategy
% 37.30/6.08 % (1437527)Time elapsed: 0.002 s
% 37.30/6.08 % (1437527)Peak memory usage: 88 MB
% 37.30/6.08 % (1437528)Termination reason: Refutation not found, incomplete strategy
% 37.30/6.08 % (1437528)Time elapsed: 0.002 s
% 37.30/6.08 % (1437528)Peak memory usage: 88 MB
% 37.30/6.08 % (1437528)Instructions burned: 1 (million)
% 37.30/6.08 % (1437529)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1970017734:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 37.30/6.08 % (1437529)Refutation not found, incomplete strategy
% 37.30/6.08 % (1437529)------------------------------
% 37.30/6.08 % (1437529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.30/6.08 % (1437529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.30/6.08 % (1437529)CaDiCaL version: 2.1.3
% 37.30/6.08 % (1437529)Termination reason: Refutation not found, incomplete strategy
% 37.30/6.08 % (1437529)Time elapsed: 0.002 s
% 37.30/6.08 % (1437529)Peak memory usage: 87 MB
% 37.30/6.08 % (1437530)lrs+10_64_to=lpo:sil=8000:random_seed=449462878:i=126:bd=preordered_2993 on theBenchmark for (2993ds/126Mi)
% 37.30/6.08 % (1437530)Instruction limit reached!
% 37.30/6.08 % (1437530)------------------------------
% 37.30/6.08 % (1437530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.30/6.08 % (1437530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.30/6.08 % (1437530)CaDiCaL version: 2.1.3
% 37.30/6.08 % (1437530)Termination reason: Instruction limit
% 37.30/6.08 % (1437530)Termination phase: Saturation
% 37.30/6.08 % (1437530)Time elapsed: 0.118 s
% 37.30/6.08 % (1437530)Peak memory usage: 88 MB
% 37.30/6.08 % (1437530)Instructions burned: 126 (million)
% 37.30/6.08 % (1437527)------------------------------
% 37.30/6.08 % (1437527)------------------------------
% 37.30/6.08 % (1437529)------------------------------
% 37.30/6.08 % (1437529)------------------------------
% 37.30/6.08 % (1437528)------------------------------
% 37.30/6.08 % (1437528)------------------------------
% 37.30/6.08 % (1437535)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1683731049:avsq=on:i=194:fgj=on:bd=preordered_2990 on theBenchmark for (2990ds/194Mi)
% 37.30/6.08 % (1437536)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1046566334:i=157:gtg=all_2989 on theBenchmark for (2989ds/157Mi)
% 37.30/6.08 % (1437537)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=882523112:i=3394:sd=4:ss=included:sgt=64_2989 on theBenchmark for (2989ds/3394Mi)
% 37.30/6.08 % (1437538)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=3417248599:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2989 on theBenchmark for (2989ds/106Mi)
% 37.30/6.08 % (1437535)Instruction limit reached!
% 37.30/6.08 % (1437535)------------------------------
% 37.30/6.08 % (1437535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.30/6.08 % (1437535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.30/6.08 % (1437535)CaDiCaL version: 2.1.3
% 37.30/6.08 % (1437535)Termination reason: Instruction limit
% 37.30/6.08 % (1437535)Termination phase: Saturation
% 37.30/6.08 % (1437535)Time elapsed: 0.180 s
% 37.30/6.08 % (1437535)Peak memory usage: 90 MB
% 37.30/6.08 % (1437535)Instructions burned: 195 (million)
% 37.30/6.08 % (1437536)Instruction limit reached!
% 37.30/6.08 % (1437536)------------------------------
% 37.30/6.08 % (1437536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.30/6.08 % (1437536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.30/6.08 % (1437536)CaDiCaL version: 2.1.3
% 37.30/6.08 % (1437536)Termination reason: Instruction limit
% 37.30/6.08 % (1437536)Termination phase: Saturation
% 37.30/6.08 % (1437536)Time elapsed: 0.154 s
% 37.30/6.08 % (1437536)Peak memory usage: 90 MB
% 37.30/6.08 % (1437536)Instructions burned: 158 (million)
% 37.30/6.08 % (1437538)Instruction limit reached!
% 37.30/6.08 % (1437538)------------------------------
% 44.22/8.07 % (1437538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.22/8.07 % (1437538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.22/8.07 % (1437538)CaDiCaL version: 2.1.3
% 44.22/8.07 % (1437538)Termination reason: Instruction limit
% 44.22/8.07 % (1437538)Termination phase: Saturation
% 44.22/8.07 % (1437538)Time elapsed: 0.114 s
% 44.22/8.07 % (1437538)Peak memory usage: 89 MB
% 44.22/8.07 % (1437538)Instructions burned: 106 (million)
% 44.22/8.07 % (1437543)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1534161705:i=107_2985 on theBenchmark for (2985ds/107Mi)
% 44.22/8.07 % (1437543)Refutation not found, incomplete strategy
% 44.22/8.07 % (1437543)------------------------------
% 44.22/8.07 % (1437543)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.22/8.07 % (1437543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.22/8.07 % (1437543)CaDiCaL version: 2.1.3
% 44.22/8.07 % (1437543)Termination reason: Refutation not found, incomplete strategy
% 44.22/8.07 % (1437543)Time elapsed: 0.002 s
% 44.22/8.07 % (1437543)Peak memory usage: 87 MB
% 44.22/8.07 % (1437545)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2732081764:cond=fast:i=5208:av=off_2985 on theBenchmark for (2985ds/5208Mi)
% 44.22/8.07 % (1437544)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=663721974:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2985 on theBenchmark for (2985ds/242Mi)
% 44.22/8.07 % (1437544)Instruction limit reached!
% 44.22/8.07 % (1437544)------------------------------
% 44.22/8.07 % (1437544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.22/8.07 % (1437544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.22/8.07 % (1437544)CaDiCaL version: 2.1.3
% 44.22/8.07 % (1437544)Termination reason: Instruction limit
% 44.22/8.07 % (1437544)Termination phase: Saturation
% 44.22/8.07 % (1437544)Time elapsed: 0.241 s
% 44.22/8.07 % (1437544)Peak memory usage: 90 MB
% 44.22/8.07 % (1437544)Instructions burned: 242 (million)
% 44.22/8.07 % (1437543)------------------------------
% 44.22/8.07 % (1437543)------------------------------
% 44.22/8.07 % (1437549)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=343661502:i=134:sd=2:doe=on:ss=axioms:sgt=14_2980 on theBenchmark for (2980ds/134Mi)
% 44.22/8.07 % (1437549)Instruction limit reached!
% 44.22/8.07 % (1437549)------------------------------
% 44.22/8.07 % (1437549)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.22/8.07 % (1437549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.22/8.07 % (1437549)CaDiCaL version: 2.1.3
% 44.22/8.07 % (1437549)Termination reason: Instruction limit
% 44.22/8.07 % (1437549)Termination phase: Saturation
% 44.22/8.07 % (1437549)Time elapsed: 0.124 s
% 44.22/8.07 % (1437549)Peak memory usage: 89 MB
% 44.22/8.07 % (1437549)Instructions burned: 135 (million)
% 44.22/8.07 % (1437550)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2856035515:i=499:bd=all_2978 on theBenchmark for (2978ds/499Mi)
% 44.22/8.07 % (1437552)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1784038516:i=191:fgj=on:bd=all_2976 on theBenchmark for (2976ds/191Mi)
% 44.22/8.07 % (1437552)Instruction limit reached!
% 44.22/8.07 % (1437552)------------------------------
% 44.22/8.07 % (1437552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.22/8.07 % (1437552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.22/8.07 % (1437552)CaDiCaL version: 2.1.3
% 44.22/8.07 % (1437552)Termination reason: Instruction limit
% 44.22/8.07 % (1437552)Termination phase: Saturation
% 44.22/8.07 % (1437552)Time elapsed: 0.192 s
% 44.22/8.07 % (1437552)Peak memory usage: 91 MB
% 44.22/8.07 % (1437552)Instructions burned: 191 (million)
% 44.22/8.07 % (1437550)Instruction limit reached!
% 44.22/8.07 % (1437550)------------------------------
% 44.22/8.07 % (1437550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.22/8.07 % (1437550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.22/8.07 % (1437550)CaDiCaL version: 2.1.3
% 44.22/8.07 % (1437550)Termination reason: Instruction limit
% 44.22/8.07 % (1437550)Termination phase: Saturation
% 44.22/8.07 % (1437550)Time elapsed: 0.523 s
% 44.22/8.07 % (1437550)Peak memory usage: 94 MB
% 44.22/8.07 % (1437550)Instructions burned: 499 (million)
% 44.22/8.07 % (1437555)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1863100958:i=264:kws=precedence:fsr=off_2971 on theBenchmark for (2971ds/264Mi)
% 44.22/8.07 % (1437558)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2938624754:cond=on:i=156:bs=on:gtg=exists_all:er=known_2970 on theBenchmark for (2970ds/156Mi)
% 44.22/8.07 % (1437558)Instruction limit reached!
% 44.22/8.07 % (1437558)------------------------------
% 44.22/8.07 % (1437558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.22/8.07 % (1437558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.22/8.07 % (1437558)CaDiCaL version: 2.1.3
% 44.22/8.07 % (1437558)Termination reason: Instruction limit
% 44.22/8.07 % (1437558)Termination phase: Saturation
% 44.22/8.07 % (1437558)Time elapsed: 0.158 s
% 44.22/8.07 % (1437558)Peak memory usage: 89 MB
% 44.22/8.07 % (1437558)Instructions burned: 157 (million)
% 44.22/8.07 % (1437555)Instruction limit reached!
% 44.22/8.07 % (1437555)------------------------------
% 44.22/8.07 % (1437555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.22/8.07 % (1437555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.22/8.07 % (1437555)CaDiCaL version: 2.1.3
% 44.22/8.07 % (1437555)Termination reason: Instruction limit
% 44.22/8.07 % (1437555)Termination phase: Saturation
% 44.22/8.07 % (1437555)Time elapsed: 0.254 s
% 44.22/8.07 % (1437555)Peak memory usage: 92 MB
% 44.22/8.07 % (1437555)Instructions burned: 264 (million)
% 44.22/8.07 % (1437562)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1783770091:i=537:av=off:ss=included_2965 on theBenchmark for (2965ds/537Mi)
% 44.22/8.07 % (1437561)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=551592611:i=3256:kws=precedence:bd=preordered:av=off_2966 on theBenchmark for (2966ds/3256Mi)
% 44.22/8.07 % (1437562)Instruction limit reached!
% 44.22/8.07 % (1437562)------------------------------
% 44.22/8.07 % (1437562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.22/8.07 % (1437562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.22/8.07 % (1437562)CaDiCaL version: 2.1.3
% 44.22/8.07 % (1437562)Termination reason: Instruction limit
% 44.22/8.07 % (1437562)Termination phase: Saturation
% 44.22/8.07 % (1437562)Time elapsed: 0.485 s
% 44.22/8.07 % (1437562)Peak memory usage: 93 MB
% 44.22/8.07 % (1437562)Instructions burned: 537 (million)
% 44.22/8.07 % (1437565)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3354054634:i=180:bd=preordered:av=off_2958 on theBenchmark for (2958ds/180Mi)
% 44.22/8.07 % (1437537)Instruction limit reached!
% 44.22/8.07 % (1437537)------------------------------
% 44.22/8.07 % (1437537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.22/8.07 % (1437537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.22/8.07 % (1437537)CaDiCaL version: 2.1.3
% 44.22/8.07 % (1437537)Termination reason: Instruction limit
% 44.22/8.07 % (1437537)Termination phase: Saturation
% 44.22/8.07 % (1437537)Time elapsed: 3.345 s
% 44.22/8.07 % (1437537)Peak memory usage: 149 MB
% 44.22/8.07 % (1437537)Instructions burned: 3395 (million)
% 44.22/8.07 % (1437565)Instruction limit reached!
% 44.22/8.07 % (1437565)------------------------------
% 44.22/8.07 % (1437565)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.22/8.07 % (1437565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.22/8.07 % (1437565)CaDiCaL version: 2.1.3
% 44.22/8.07 % (1437565)Termination reason: Instruction limit
% 44.22/8.07 % (1437565)Termination phase: Saturation
% 44.22/8.07 % (1437565)Time elapsed: 0.164 s
% 44.22/8.07 % (1437565)Peak memory usage: 88 MB
% 44.22/8.07 % (1437565)Instructions burned: 181 (million)
% 44.22/8.07 % (1437568)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=1753523564:i=412:gtgl=4:gtg=exists_all_2953 on theBenchmark for (2953ds/412Mi)
% 44.22/8.07 % (1437567)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=2463445241:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2953 on theBenchmark for (2953ds/10307Mi)
% 44.22/8.07 % (1437568)Instruction limit reached!
% 44.22/8.07 % (1437568)------------------------------
% 44.22/8.07 % (1437568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.22/8.07 % (1437568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.22/8.07 % (1437568)CaDiCaL version: 2.1.3
% 44.22/8.07 % (1437568)Termination reason: Instruction limit
% 44.22/8.07 % (1437568)Termination phase: Saturation
% 44.22/8.07 % (1437568)Time elapsed: 0.367 s
% 44.22/8.07 % (1437568)Peak memory usage: 94 MB
% 44.22/8.07 % (1437568)Instructions burned: 413 (million)
% 44.22/8.07 % (1437571)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=1525246016:s2pl=no:i=8478:s2at=4:nm=6_2947 on theBenchmark for (2947ds/8478Mi)
% 44.22/8.07 % (1437545)Instruction limit reached!
% 44.22/8.07 % (1437545)------------------------------
% 44.22/8.07 % (1437545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.22/8.07 % (1437545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.22/8.07 % (1437545)CaDiCaL version: 2.1.3
% 44.22/8.07 % (1437545)Termination reason: Instruction limit
% 44.22/8.07 % (1437545)Termination phase: Saturation
% 44.22/8.07 % (1437545)Time elapsed: 5.173 s
% 44.22/8.07 % (1437545)Peak memory usage: 168 MB
% 44.22/8.07 % (1437545)Instructions burned: 5209 (million)
% 44.22/8.07 % (1437514)First to succeed.
% 44.22/8.07 % (1437514)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1437508"
% 44.22/8.07 % (1437561)Instruction limit reached!
% 44.22/8.07 % (1437561)------------------------------
% 44.22/8.07 % (1437561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.22/8.07 % (1437561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.22/8.07 % (1437561)CaDiCaL version: 2.1.3
% 44.22/8.07 % (1437561)Termination reason: Instruction limit
% 44.22/8.07 % (1437561)Termination phase: Saturation
% 44.22/8.07 % (1437561)Time elapsed: 3.326 s
% 44.22/8.07 % (1437561)Peak memory usage: 148 MB
% 44.22/8.07 % (1437561)Instructions burned: 3256 (million)
% 44.22/8.07 % (1437514)Refutation found. Thanks to Tanya!
% 44.22/8.07 % SZS status Unsatisfiable for theBenchmark
% 44.22/8.07 % SZS output start Proof for theBenchmark
% See solution above
% 51.84/8.28 % (1437514)------------------------------
% 51.84/8.28 % (1437514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.84/8.28 % (1437514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.84/8.28 % (1437514)CaDiCaL version: 2.1.3
% 51.84/8.28 % (1437514)Termination reason: Refutation
% 51.84/8.28 % (1437514)Time elapsed: 6.799 s
% 51.84/8.28 % (1437514)Peak memory usage: 220 MB
% 51.84/8.28 % (1437514)Instructions burned: 12083 (million)
% 51.84/8.28 % (1437514)------------------------------
% 51.84/8.28 % (1437514)------------------------------
% 51.84/8.28 % (1437508)Success in time 7.248 s
% 51.84/8.28 % Vampire exiting
%------------------------------------------------------------------------------