%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT180-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 : n019.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:09 AM UTC 2026
% Result : Unsatisfiable 21.83s 6.81s
% Output : Refutation 0.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 113
% Number of leaves : 18
% Syntax : Number of formulae : 658 ( 622 unt; 5 def)
% Number of atoms : 699 ( 698 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 84 ( 43 ~; 41 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 4 avg)
% Maximal term depth : 13 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 10 con; 0-2 aty)
% Number of variables : 1641 (1641 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : meet(X0,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',idempotence_of_meet) ).
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,meet(X0,X2))) = meet(X0,join(X1,meet(X2,join(X1,meet(X0,join(X2,meet(X0,X1))))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',equation_H3) ).
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(f14,definition,
sF0 = join(b,c),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f15,plain,
join(b,c) = sF0,
inference(reorient_equations,[],[f14]) ).
fof(f16,definition,
sF1 = meet(a,sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f17,plain,
meet(a,sF0) = sF1,
inference(reorient_equations,[],[f16]) ).
fof(f18,definition,
sF2 = meet(a,b),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f19,plain,
meet(a,b) = sF2,
inference(reorient_equations,[],[f18]) ).
fof(f20,definition,
sF3 = meet(a,c),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f21,plain,
meet(a,c) = sF3,
inference(reorient_equations,[],[f20]) ).
fof(f22,definition,
sF4 = join(sF2,sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f23,plain,
join(sF2,sF3) = sF4,
inference(reorient_equations,[],[f22]) ).
fof(f24,plain,
sF1 != sF4,
inference(definition_folding,[],[f13,f23,f21,f19,f17,f15]) ).
fof(f25,plain,
sF2 = meet(b,a),
inference(forward_demodulation,[],[f19,f5]) ).
fof(f26,plain,
sF3 = meet(c,a),
inference(forward_demodulation,[],[f21,f5]) ).
fof(f32,plain,
! [X0,X1] : join(X1,meet(X0,X1)) = X1,
inference(superposition,[],[f4,f5]) ).
fof(f34,plain,
! [X0,X1] : meet(X1,join(X0,X1)) = X1,
inference(superposition,[],[f3,f6]) ).
fof(f35,plain,
! [X0,X1] : join(X0,X1) = join(join(X0,X1),X0),
inference(superposition,[],[f32,f3]) ).
fof(f38,plain,
a = join(a,sF2),
inference(superposition,[],[f32,f25]) ).
fof(f41,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X0,X1)),
inference(forward_demodulation,[],[f35,f6]) ).
fof(f43,plain,
! [X0,X1] : meet(X0,X1) = meet(meet(X0,X1),X0),
inference(superposition,[],[f34,f4]) ).
fof(f44,plain,
! [X0,X1] : meet(X1,X0) = meet(meet(X1,X0),X0),
inference(superposition,[],[f34,f32]) ).
fof(f48,plain,
! [X0,X1] : join(X1,X0) = join(join(X1,X0),X0),
inference(superposition,[],[f32,f34]) ).
fof(f50,plain,
! [X0,X1] : join(X1,X0) = join(X0,join(X1,X0)),
inference(forward_demodulation,[],[f48,f6]) ).
fof(f51,plain,
! [X0,X1] : meet(X1,X0) = meet(X0,meet(X1,X0)),
inference(forward_demodulation,[],[f44,f5]) ).
fof(f52,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X0,X1)),
inference(forward_demodulation,[],[f43,f5]) ).
fof(f53,plain,
! [X2,X0,X1] : join(X0,join(meet(X0,X1),X2)) = join(X0,X2),
inference(superposition,[],[f8,f4]) ).
fof(f54,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X1,X0),X2)),
inference(superposition,[],[f8,f32]) ).
fof(f56,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X1,join(X0,X2)),
inference(superposition,[],[f8,f6]) ).
fof(f63,plain,
! [X2,X0,X1] : join(X0,X1) = join(X0,join(X1,meet(join(X0,X1),X2))),
inference(superposition,[],[f4,f8]) ).
fof(f65,plain,
! [X2,X0,X1] : meet(X2,join(X0,join(X1,X2))) = X2,
inference(superposition,[],[f34,f8]) ).
fof(f67,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f6,f8]) ).
fof(f68,plain,
! [X2,X0,X1] : join(X0,X1) = meet(join(X0,X1),join(X0,join(X1,X2))),
inference(superposition,[],[f3,f8]) ).
fof(f94,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X0,X1),X2)),
inference(superposition,[],[f7,f3]) ).
fof(f95,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X1,X0),X2)),
inference(superposition,[],[f7,f34]) ).
fof(f97,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X1,meet(X0,X2)),
inference(superposition,[],[f7,f5]) ).
fof(f108,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X2,meet(X0,X1)),
inference(superposition,[],[f5,f7]) ).
fof(f109,plain,
! [X2,X0,X1] : meet(X0,X1) = join(meet(X0,X1),meet(X0,meet(X1,X2))),
inference(superposition,[],[f4,f7]) ).
fof(f139,plain,
! [X2,X0,X1] : meet(X0,join(X0,X1)) = meet(X0,join(X2,join(X0,X1))),
inference(superposition,[],[f94,f34]) ).
fof(f141,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(X1,meet(X0,join(X1,X2))),
inference(superposition,[],[f94,f5]) ).
fof(f145,plain,
! [X2,X0,X1] : meet(join(X0,X2),X1) = join(meet(join(X0,X2),X1),meet(X0,X1)),
inference(superposition,[],[f32,f94]) ).
fof(f149,plain,
! [X2,X0,X1] : meet(join(X0,X2),X1) = join(meet(X0,X1),meet(join(X0,X2),X1)),
inference(forward_demodulation,[],[f145,f6]) ).
fof(f153,plain,
! [X2,X0,X1] : meet(X0,join(X2,join(X0,X1))) = X0,
inference(forward_demodulation,[],[f139,f3]) ).
fof(f162,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(X1,X2))) = meet(X1,join(X0,meet(X2,join(X0,meet(X1,join(X2,meet(X0,X1))))))),
inference(superposition,[],[f12,f5]) ).
fof(f171,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X0,X2))) = meet(X0,join(X1,meet(X2,join(X1,meet(X0,join(meet(X0,X1),X2)))))),
inference(superposition,[],[f12,f6]) ).
fof(f181,plain,
! [X2,X3,X0,X1] : meet(X3,join(join(X0,X1),meet(X3,X2))) = meet(X3,join(X0,join(X1,meet(X2,join(join(X0,X1),meet(X3,join(X2,meet(X3,join(X0,X1))))))))),
inference(superposition,[],[f12,f8]) ).
fof(f195,plain,
! [X2,X3,X0,X1] : meet(X3,join(join(X0,X1),meet(X3,X2))) = meet(X3,join(X0,join(X1,meet(X2,join(X0,join(X1,meet(X3,join(X2,meet(X3,join(X0,X1)))))))))),
inference(forward_demodulation,[],[f181,f8]) ).
fof(f210,plain,
! [X2,X3,X0,X1] : meet(X3,join(X0,join(X1,meet(X2,join(X0,join(X1,meet(X3,join(X2,meet(X3,join(X0,X1)))))))))) = meet(X3,join(X0,join(X1,meet(X3,X2)))),
inference(forward_demodulation,[],[f195,f8]) ).
fof(f238,plain,
! [X0] : meet(X0,one) = X0,
inference(superposition,[],[f3,f9]) ).
fof(f242,plain,
! [X0,X1] : one = join(X0,join(X1,complement(join(X0,X1)))),
inference(superposition,[],[f8,f9]) ).
fof(f245,plain,
! [X0,X1] : meet(X0,join(complement(X0),meet(X0,X1))) = meet(X0,join(complement(X0),meet(X1,join(complement(X0),meet(X0,join(X1,zero)))))),
inference(superposition,[],[f12,f10]) ).
fof(f248,plain,
! [X0] : join(X0,zero) = X0,
inference(superposition,[],[f4,f10]) ).
fof(f249,plain,
! [X0,X1] : zero = meet(X0,meet(X1,complement(meet(X0,X1)))),
inference(superposition,[],[f7,f10]) ).
fof(f251,plain,
! [X0,X1] : meet(X0,join(complement(X0),meet(X0,X1))) = meet(X0,join(complement(X0),meet(X1,join(complement(X0),meet(X0,X1))))),
inference(forward_demodulation,[],[f245,f248]) ).
fof(f257,plain,
! [X0] : join(zero,X0) = X0,
inference(superposition,[],[f6,f248]) ).
fof(f280,plain,
! [X0,X1] : meet(X1,join(zero,meet(X1,X0))) = meet(X1,meet(X0,join(zero,meet(X1,join(X0,meet(X1,zero)))))),
inference(superposition,[],[f12,f257]) ).
fof(f282,plain,
! [X0,X1] : meet(X1,join(zero,meet(X1,X0))) = meet(X1,meet(X0,meet(X1,join(X0,meet(X1,zero))))),
inference(forward_demodulation,[],[f280,f257]) ).
fof(f290,plain,
! [X0,X1] : meet(X1,join(zero,meet(X1,X0))) = meet(X1,meet(X0,X1)),
inference(forward_demodulation,[],[f282,f141]) ).
fof(f293,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,join(zero,meet(X1,X0))),
inference(forward_demodulation,[],[f290,f51]) ).
fof(f295,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,meet(X1,X0)),
inference(forward_demodulation,[],[f293,f257]) ).
fof(f356,plain,
! [X0] : one = join(one,X0),
inference(superposition,[],[f32,f238]) ).
fof(f358,plain,
! [X0] : meet(one,X0) = X0,
inference(superposition,[],[f5,f238]) ).
fof(f381,plain,
! [X0] : one = join(X0,one),
inference(superposition,[],[f34,f358]) ).
fof(f385,plain,
zero = complement(one),
inference(superposition,[],[f10,f358]) ).
fof(f458,plain,
! [X2,X0,X1] : join(X1,X0) = join(X1,join(X0,meet(X1,X2))),
inference(superposition,[],[f53,f6]) ).
fof(f462,plain,
! [X0,X1] : join(X0,one) = join(X0,complement(meet(X0,X1))),
inference(superposition,[],[f53,f9]) ).
fof(f470,plain,
! [X2,X0,X1] : join(meet(X0,X2),X1) = meet(join(meet(X0,X2),X1),join(X0,X1)),
inference(superposition,[],[f34,f53]) ).
fof(f477,plain,
! [X2,X0,X1] : join(meet(X0,X2),X1) = meet(join(X0,X1),join(meet(X0,X2),X1)),
inference(forward_demodulation,[],[f470,f5]) ).
fof(f481,plain,
! [X0,X1] : one = join(X0,complement(meet(X0,X1))),
inference(forward_demodulation,[],[f462,f381]) ).
fof(f548,plain,
! [X0,X1] : meet(X1,X0) = join(meet(X1,X0),meet(X0,X1)),
inference(superposition,[],[f32,f295]) ).
fof(f621,plain,
! [X0,X1] : one = join(X1,complement(meet(X0,X1))),
inference(superposition,[],[f481,f295]) ).
fof(f664,plain,
! [X0,X1] : zero = meet(X1,meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f249,f5]) ).
fof(f739,plain,
! [X2,X0,X1] : join(meet(X1,X0),X2) = join(meet(X1,X0),join(meet(X0,X1),X2)),
inference(superposition,[],[f54,f295]) ).
fof(f741,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(join(X0,X1),join(X0,X2)),
inference(superposition,[],[f54,f3]) ).
fof(f757,plain,
! [X2,X0,X1] : join(X2,X0) = join(X2,join(X0,meet(X1,X2))),
inference(superposition,[],[f54,f6]) ).
fof(f776,plain,
! [X2,X3,X0,X1] : join(join(X0,X1),X2) = join(X0,join(X1,join(meet(X3,join(X0,X1)),X2))),
inference(superposition,[],[f8,f54]) ).
fof(f779,plain,
! [X2,X3,X0,X1] : join(X0,join(X1,X2)) = join(X0,join(X1,join(meet(X3,join(X0,X1)),X2))),
inference(forward_demodulation,[],[f776,f8]) ).
fof(f798,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X0,join(X2,join(X0,X1))),
inference(forward_demodulation,[],[f741,f67]) ).
fof(f810,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X0,join(X2,join(X0,X1))),
inference(forward_demodulation,[],[f798,f8]) ).
fof(f829,plain,
! [X2,X0,X1] : meet(X2,X0) = meet(X2,meet(X0,join(X1,X2))),
inference(superposition,[],[f95,f5]) ).
fof(f902,plain,
! [X0,X1] : one = join(X1,join(X0,complement(join(X0,X1)))),
inference(superposition,[],[f242,f6]) ).
fof(f928,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,f242]) ).
fof(f938,plain,
! [X0,X1] :
( zero != meet(X0,join(X1,complement(join(X0,X1))))
| complement(X0) = join(X1,complement(join(X0,X1))) ),
inference(trivial_inequality_removal,[],[f928]) ).
fof(f1308,plain,
! [X0,X1] : meet(X1,join(complement(X1),meet(X0,X1))) = meet(X1,join(complement(X1),meet(X0,join(complement(X1),meet(X0,X1))))),
inference(superposition,[],[f251,f5]) ).
fof(f1490,plain,
sF2 = meet(sF2,a),
inference(superposition,[],[f34,f38]) ).
fof(f1499,plain,
sF2 = meet(a,sF2),
inference(forward_demodulation,[],[f1490,f5]) ).
fof(f2072,plain,
! [X2,X3,X0,X1] : join(X2,join(X3,X0)) = join(X2,join(X0,join(meet(X1,X2),X3))),
inference(superposition,[],[f54,f67]) ).
fof(f2073,plain,
! [X2,X3,X0,X1] : join(X1,join(X3,X0)) = join(X1,join(X0,join(meet(X1,X2),X3))),
inference(superposition,[],[f53,f67]) ).
fof(f2095,plain,
! [X2,X3,X0,X1] : join(X0,join(X1,join(X2,X3))) = join(X2,join(X3,join(X0,X1))),
inference(superposition,[],[f8,f67]) ).
fof(f2181,plain,
! [X0,X1] : one = join(meet(X1,X0),complement(meet(X0,X1))),
inference(superposition,[],[f621,f295]) ).
fof(f2186,plain,
! [X0,X1] : one = join(join(X0,X1),complement(X0)),
inference(superposition,[],[f621,f3]) ).
fof(f2223,plain,
! [X2,X0,X1] : one = join(X0,join(X1,complement(meet(X2,join(X0,X1))))),
inference(superposition,[],[f8,f621]) ).
fof(f2248,plain,
! [X0,X1] : one = join(complement(X0),join(X0,X1)),
inference(forward_demodulation,[],[f2186,f6]) ).
fof(f2265,plain,
! [X0,X1] : one = join(X0,join(X1,complement(X0))),
inference(forward_demodulation,[],[f2248,f67]) ).
fof(f2302,plain,
! [X0,X1] :
( zero != meet(X1,join(X0,complement(join(X0,X1))))
| complement(X1) = join(X0,complement(join(X0,X1))) ),
inference(superposition,[],[f938,f6]) ).
fof(f3232,plain,
! [X2,X0,X1] : meet(X0,join(join(complement(X0),meet(X1,join(complement(X0),meet(X0,X1)))),meet(X0,X2))) = meet(X0,join(join(complement(X0),meet(X1,join(complement(X0),meet(X0,X1)))),meet(X2,join(join(complement(X0),meet(X1,join(complement(X0),meet(X0,X1)))),meet(X0,join(meet(X0,join(complement(X0),meet(X0,X1))),X2)))))),
inference(superposition,[],[f171,f251]) ).
fof(f3267,plain,
! [X0,X1] : meet(X0,join(X1,meet(X0,complement(meet(X0,X1))))) = meet(X0,join(X1,meet(complement(meet(X0,X1)),join(X1,meet(X0,one))))),
inference(superposition,[],[f171,f9]) ).
fof(f3359,plain,
! [X0,X1] : meet(X0,join(X1,meet(X0,complement(meet(X0,X1))))) = meet(X0,join(X1,meet(complement(meet(X0,X1)),join(X1,X0)))),
inference(forward_demodulation,[],[f3267,f238]) ).
fof(f3378,plain,
! [X2,X0,X1] : meet(X0,join(join(complement(X0),meet(X1,join(complement(X0),meet(X0,X1)))),meet(X0,X2))) = meet(X0,join(complement(X0),join(meet(X1,join(complement(X0),meet(X0,X1))),meet(X2,join(join(complement(X0),meet(X1,join(complement(X0),meet(X0,X1)))),meet(X0,join(meet(X0,join(complement(X0),meet(X0,X1))),X2))))))),
inference(forward_demodulation,[],[f3232,f8]) ).
fof(f3409,plain,
! [X0,X1] : meet(X0,join(X1,meet(X0,complement(meet(X0,X1))))) = meet(X0,join(X1,meet(join(X1,X0),complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f3359,f5]) ).
fof(f3420,plain,
! [X2,X0,X1] : meet(X0,join(join(complement(X0),meet(X1,join(complement(X0),meet(X0,X1)))),meet(X0,X2))) = meet(X0,join(complement(X0),join(meet(X1,join(complement(X0),meet(X0,X1))),meet(X2,join(complement(X0),join(meet(X1,join(complement(X0),meet(X0,X1))),meet(X0,join(meet(X0,join(complement(X0),meet(X0,X1))),X2)))))))),
inference(forward_demodulation,[],[f3378,f8]) ).
fof(f3447,plain,
! [X2,X0,X1] : meet(X0,join(complement(X0),join(meet(X1,join(complement(X0),meet(X0,X1))),meet(X0,X2)))) = meet(X0,join(complement(X0),join(meet(X1,join(complement(X0),meet(X0,X1))),meet(X2,join(complement(X0),join(meet(X1,join(complement(X0),meet(X0,X1))),meet(X0,join(meet(X0,join(complement(X0),meet(X0,X1))),X2)))))))),
inference(forward_demodulation,[],[f3420,f8]) ).
fof(f3473,plain,
! [X0,X1] : meet(X0,join(X1,meet(X0,complement(meet(X0,X1))))) = meet(X0,join(X1,meet(join(X0,X1),complement(meet(X0,X1))))),
inference(superposition,[],[f3409,f6]) ).
fof(f3498,plain,
! [X0,X1] : meet(X1,join(X0,meet(X1,complement(meet(X0,X1))))) = meet(X1,join(X0,meet(join(X0,X1),complement(meet(X0,X1))))),
inference(superposition,[],[f3409,f5]) ).
fof(f3549,plain,
! [X0,X1] : join(X1,meet(join(X1,X0),complement(meet(X0,X1)))) = join(join(X1,meet(join(X1,X0),complement(meet(X0,X1)))),meet(X0,join(X1,meet(X0,complement(meet(X0,X1)))))),
inference(superposition,[],[f32,f3409]) ).
fof(f3586,plain,
! [X0,X1] : join(X1,meet(join(X1,X0),complement(meet(X0,X1)))) = join(X1,join(meet(join(X1,X0),complement(meet(X0,X1))),meet(X0,join(X1,meet(X0,complement(meet(X0,X1))))))),
inference(forward_demodulation,[],[f3549,f8]) ).
fof(f4236,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X0,meet(join(X0,X1),X2))) = meet(join(X0,X1),join(X0,meet(X2,join(X0,meet(join(X0,X1),join(X2,X0)))))),
inference(superposition,[],[f162,f3]) ).
fof(f4244,plain,
! [X0,X1] : meet(complement(X0),join(X0,meet(complement(X0),X1))) = meet(complement(X0),join(X0,meet(X1,join(X0,meet(complement(X0),join(X1,zero)))))),
inference(superposition,[],[f162,f10]) ).
fof(f4259,plain,
! [X0] : meet(a,join(c,meet(a,X0))) = meet(a,join(c,meet(X0,join(c,meet(a,join(X0,sF3)))))),
inference(superposition,[],[f162,f26]) ).
fof(f4378,plain,
! [X0,X1] : meet(complement(X0),join(X0,meet(complement(X0),X1))) = meet(complement(X0),join(X0,meet(X1,join(X0,meet(complement(X0),X1))))),
inference(forward_demodulation,[],[f4244,f248]) ).
fof(f4641,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,[],[f2302,f242]) ).
fof(f4642,plain,
! [X0,X1] :
( zero != meet(join(X0,complement(join(X0,X1))),join(X1,complement(one)))
| join(X1,complement(one)) = complement(join(X0,complement(join(X0,X1)))) ),
inference(superposition,[],[f2302,f902]) ).
fof(f4649,plain,
! [X0] :
( zero != meet(complement(X0),join(X0,complement(one)))
| join(X0,complement(one)) = complement(complement(X0)) ),
inference(superposition,[],[f2302,f9]) ).
fof(f4705,plain,
! [X0] :
( zero != meet(complement(X0),join(X0,zero))
| join(X0,complement(one)) = complement(complement(X0)) ),
inference(forward_demodulation,[],[f4649,f385]) ).
fof(f4707,plain,
! [X0,X1] :
( zero != meet(join(X1,complement(one)),join(X0,complement(join(X0,X1))))
| join(X1,complement(one)) = complement(join(X0,complement(join(X0,X1)))) ),
inference(forward_demodulation,[],[f4642,f5]) ).
fof(f4708,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,[],[f4641,f5]) ).
fof(f4720,plain,
! [X0] :
( zero != meet(complement(X0),X0)
| join(X0,complement(one)) = complement(complement(X0)) ),
inference(forward_demodulation,[],[f4705,f248]) ).
fof(f4722,plain,
! [X0,X1] :
( zero != meet(join(X1,zero),join(X0,complement(join(X0,X1))))
| join(X1,complement(one)) = complement(join(X0,complement(join(X0,X1)))) ),
inference(forward_demodulation,[],[f4707,f385]) ).
fof(f4723,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,[],[f4708,f385]) ).
fof(f4730,plain,
! [X0] :
( meet(X0,complement(X0)) != zero
| join(X0,complement(one)) = complement(complement(X0)) ),
inference(forward_demodulation,[],[f4720,f5]) ).
fof(f4732,plain,
! [X0,X1] :
( zero != meet(X1,join(X0,complement(join(X0,X1))))
| join(X1,complement(one)) = complement(join(X0,complement(join(X0,X1)))) ),
inference(forward_demodulation,[],[f4722,f248]) ).
fof(f4733,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,[],[f4723,f248]) ).
fof(f4739,plain,
! [X0] : join(X0,complement(one)) = complement(complement(X0)),
inference(forward_subsumption_resolution,[],[f4730,f10]) ).
fof(f4741,plain,
! [X0,X1] :
( join(X1,zero) = complement(join(X0,complement(join(X0,X1))))
| zero != meet(X1,join(X0,complement(join(X0,X1)))) ),
inference(forward_demodulation,[],[f4732,f385]) ).
fof(f4742,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,[],[f4733,f385]) ).
fof(f4746,plain,
! [X0] : join(X0,zero) = complement(complement(X0)),
inference(forward_demodulation,[],[f4739,f385]) ).
fof(f4748,plain,
! [X0,X1] :
( complement(join(X0,complement(join(X0,X1)))) = X1
| zero != meet(X1,join(X0,complement(join(X0,X1)))) ),
inference(forward_demodulation,[],[f4741,f248]) ).
fof(f4749,plain,
! [X0,X1] :
( complement(join(X0,complement(join(X1,X0)))) = X1
| zero != meet(X1,join(X0,complement(join(X1,X0)))) ),
inference(forward_demodulation,[],[f4742,f248]) ).
fof(f4751,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_demodulation,[],[f4746,f248]) ).
fof(f4863,plain,
! [X2,X0,X1] : join(meet(X1,X0),X2) = join(meet(X1,X0),join(X2,meet(X0,X1))),
inference(superposition,[],[f757,f295]) ).
fof(f4866,plain,
! [X2,X3,X0,X1] : join(meet(X2,X0),X3) = join(meet(X2,X0),join(X3,meet(X0,meet(X1,X2)))),
inference(superposition,[],[f757,f108]) ).
fof(f4878,plain,
! [X2,X3,X0,X1] : join(join(X1,meet(X2,join(X1,meet(X0,join(meet(X0,X1),X2))))),X3) = join(join(X1,meet(X2,join(X1,meet(X0,join(meet(X0,X1),X2))))),join(X3,meet(X0,join(X1,meet(X0,X2))))),
inference(superposition,[],[f757,f171]) ).
fof(f4880,plain,
! [X2,X0,X1] : join(join(complement(X0),meet(X1,join(complement(X0),meet(X0,X1)))),X2) = join(join(complement(X0),meet(X1,join(complement(X0),meet(X0,X1)))),join(X2,meet(X0,join(complement(X0),meet(X0,X1))))),
inference(superposition,[],[f757,f251]) ).
fof(f4988,plain,
! [X2,X0,X1] : join(join(complement(X0),meet(X1,join(complement(X0),meet(X0,X1)))),X2) = join(meet(X0,join(complement(X0),meet(X0,X1))),join(join(complement(X0),meet(X1,join(complement(X0),meet(X0,X1)))),X2)),
inference(forward_demodulation,[],[f4880,f67]) ).
fof(f4990,plain,
! [X2,X3,X0,X1] : join(join(X1,meet(X2,join(X1,meet(X0,join(meet(X0,X1),X2))))),X3) = join(meet(X0,join(X1,meet(X0,X2))),join(join(X1,meet(X2,join(X1,meet(X0,join(meet(X0,X1),X2))))),X3)),
inference(forward_demodulation,[],[f4878,f67]) ).
fof(f5010,plain,
! [X2,X0,X1] : join(complement(X0),join(meet(X1,join(complement(X0),meet(X0,X1))),X2)) = join(meet(X0,join(complement(X0),meet(X0,X1))),join(complement(X0),join(meet(X1,join(complement(X0),meet(X0,X1))),X2))),
inference(forward_demodulation,[],[f4988,f8]) ).
fof(f5012,plain,
! [X2,X3,X0,X1] : join(X1,join(meet(X2,join(X1,meet(X0,join(meet(X0,X1),X2)))),X3)) = join(meet(X0,join(X1,meet(X0,X2))),join(X1,join(meet(X2,join(X1,meet(X0,join(meet(X0,X1),X2)))),X3))),
inference(forward_demodulation,[],[f4990,f8]) ).
fof(f5021,plain,
! [X2,X0,X1] : join(complement(X0),join(meet(X1,join(complement(X0),meet(X0,X1))),X2)) = join(complement(X0),join(join(meet(X1,join(complement(X0),meet(X0,X1))),X2),meet(X0,join(complement(X0),meet(X0,X1))))),
inference(forward_demodulation,[],[f5010,f67]) ).
fof(f5022,plain,
! [X2,X3,X0,X1] : join(X1,join(meet(X2,join(X1,meet(X0,join(meet(X0,X1),X2)))),X3)) = join(X1,join(join(meet(X2,join(X1,meet(X0,join(meet(X0,X1),X2)))),X3),meet(X0,join(X1,meet(X0,X2))))),
inference(forward_demodulation,[],[f5012,f67]) ).
fof(f5028,plain,
! [X2,X0,X1] : join(complement(X0),join(meet(X1,join(complement(X0),meet(X0,X1))),X2)) = join(complement(X0),join(meet(X1,join(complement(X0),meet(X0,X1))),join(X2,meet(X0,join(complement(X0),meet(X0,X1)))))),
inference(forward_demodulation,[],[f5021,f8]) ).
fof(f5029,plain,
! [X2,X3,X0,X1] : join(X1,join(meet(X2,join(X1,meet(X0,join(meet(X0,X1),X2)))),X3)) = join(X1,join(meet(X0,join(X1,meet(X0,X2))),join(meet(X2,join(X1,meet(X0,join(meet(X0,X1),X2)))),X3))),
inference(forward_demodulation,[],[f5022,f6]) ).
fof(f5422,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X1,join(X0,meet(X1,X2))))) = meet(X1,join(X2,meet(join(X0,meet(X1,X2)),join(X2,meet(X1,join(X0,meet(X1,X2))))))),
inference(superposition,[],[f171,f50]) ).
fof(f5775,plain,
! [X0,X1] : meet(X0,join(join(X1,complement(join(X0,X1))),meet(X0,complement(meet(X0,join(X1,complement(join(X0,X1)))))))) = meet(X0,join(join(X1,complement(join(X0,X1))),meet(one,complement(meet(X0,join(X1,complement(join(X0,X1)))))))),
inference(superposition,[],[f3473,f242]) ).
fof(f5781,plain,
! [X0,X1] : meet(X0,join(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1))))))) = meet(X0,join(complement(meet(X0,X1)),meet(one,complement(meet(X0,complement(meet(X0,X1))))))),
inference(superposition,[],[f3473,f481]) ).
fof(f5963,plain,
! [X0,X1] : meet(X0,join(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1))))))) = meet(X0,join(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f5781,f358]) ).
fof(f5969,plain,
! [X0,X1] : meet(X0,join(join(X1,complement(join(X0,X1))),meet(X0,complement(meet(X0,join(X1,complement(join(X0,X1)))))))) = meet(X0,join(X1,join(complement(join(X0,X1)),meet(one,complement(meet(X0,join(X1,complement(join(X0,X1))))))))),
inference(forward_demodulation,[],[f5775,f8]) ).
fof(f6025,plain,
! [X0,X1] : meet(X0,one) = meet(X0,join(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1))))))),
inference(forward_demodulation,[],[f5963,f621]) ).
fof(f6031,plain,
! [X0,X1] : meet(X0,join(join(X1,complement(join(X0,X1))),meet(X0,complement(meet(X0,join(X1,complement(join(X0,X1)))))))) = meet(X0,join(X1,join(complement(join(X0,X1)),complement(meet(X0,join(X1,complement(join(X0,X1)))))))),
inference(forward_demodulation,[],[f5969,f358]) ).
fof(f6071,plain,
! [X0,X1] : meet(X0,join(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1))))))) = X0,
inference(forward_demodulation,[],[f6025,f238]) ).
fof(f6075,plain,
! [X0,X1] : meet(X0,one) = meet(X0,join(join(X1,complement(join(X0,X1))),meet(X0,complement(meet(X0,join(X1,complement(join(X0,X1)))))))),
inference(forward_demodulation,[],[f6031,f2223]) ).
fof(f6099,plain,
! [X0,X1] : meet(X0,one) = meet(X0,join(X1,join(complement(join(X0,X1)),meet(X0,complement(meet(X0,join(X1,complement(join(X0,X1))))))))),
inference(forward_demodulation,[],[f6075,f8]) ).
fof(f6116,plain,
! [X0,X1] : meet(X0,join(X1,join(complement(join(X0,X1)),meet(X0,complement(meet(X0,join(X1,complement(join(X0,X1))))))))) = X0,
inference(forward_demodulation,[],[f6099,f238]) ).
fof(f6187,plain,
! [X0,X1] : meet(join(X1,meet(join(X0,X1),complement(meet(X0,X1)))),join(X0,meet(join(X1,meet(join(X0,X1),complement(meet(X0,X1)))),complement(meet(X0,join(X1,meet(X0,complement(meet(X0,X1))))))))) = meet(join(X1,meet(join(X0,X1),complement(meet(X0,X1)))),join(X0,meet(join(X0,join(X1,meet(join(X0,X1),complement(meet(X0,X1))))),complement(meet(X0,join(X1,meet(X0,complement(meet(X0,X1))))))))),
inference(superposition,[],[f3498,f3473]) ).
fof(f6316,plain,
! [X0,X1] : meet(join(X1,meet(join(X0,X1),complement(meet(X0,X1)))),join(X0,meet(join(X1,meet(join(X0,X1),complement(meet(X0,X1)))),complement(meet(X0,join(X1,meet(X0,complement(meet(X0,X1))))))))) = meet(join(X1,meet(join(X0,X1),complement(meet(X0,X1)))),join(X0,meet(complement(meet(X0,join(X1,meet(X0,complement(meet(X0,X1)))))),join(X0,join(X1,meet(join(X0,X1),complement(meet(X0,X1)))))))),
inference(forward_demodulation,[],[f6187,f5]) ).
fof(f6388,plain,
! [X0,X1] : meet(join(X1,meet(join(X0,X1),complement(meet(X0,X1)))),join(X0,meet(join(X1,meet(join(X0,X1),complement(meet(X0,X1)))),complement(meet(X0,join(X1,meet(X0,complement(meet(X0,X1))))))))) = meet(join(X1,meet(join(X0,X1),complement(meet(X0,X1)))),join(X0,meet(complement(meet(X0,join(X1,meet(X0,complement(meet(X0,X1)))))),join(X0,X1)))),
inference(forward_demodulation,[],[f6316,f63]) ).
fof(f6437,plain,
! [X0,X1] : meet(join(X1,meet(join(X0,X1),complement(meet(X0,X1)))),join(X0,meet(join(X1,meet(join(X0,X1),complement(meet(X0,X1)))),complement(meet(X0,join(X1,meet(X0,complement(meet(X0,X1))))))))) = meet(join(X1,meet(join(X0,X1),complement(meet(X0,X1)))),join(X0,meet(join(X0,X1),complement(meet(X0,join(X1,meet(X0,complement(meet(X0,X1))))))))),
inference(forward_demodulation,[],[f6388,f5]) ).
fof(f7366,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(X0,meet(X1,join(X2,meet(X1,X0)))),
inference(superposition,[],[f34,f97]) ).
fof(f7701,plain,
! [X2,X0,X1] : join(meet(meet(X1,X0),X1),X2) = join(meet(meet(X1,X0),X1),join(meet(X0,X1),X2)),
inference(superposition,[],[f739,f295]) ).
fof(f7901,plain,
! [X2,X0,X1] : join(meet(meet(X1,X0),X1),X2) = join(meet(X0,X1),join(X2,meet(meet(X1,X0),X1))),
inference(forward_demodulation,[],[f7701,f67]) ).
fof(f8010,plain,
! [X2,X0,X1] : join(meet(X1,meet(X1,X0)),X2) = join(meet(X0,X1),join(X2,meet(X1,meet(X1,X0)))),
inference(forward_demodulation,[],[f7901,f5]) ).
fof(f8086,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(meet(X1,meet(X1,X0)),X2),
inference(forward_demodulation,[],[f8010,f4866]) ).
fof(f8094,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(meet(X1,X0),X2),
inference(forward_demodulation,[],[f8086,f52]) ).
fof(f8248,plain,
! [X2,X0,X1] : meet(complement(X0),join(join(X0,meet(X1,join(X0,meet(complement(X0),X1)))),meet(complement(X0),X2))) = meet(complement(X0),join(join(X0,meet(X1,join(X0,meet(complement(X0),X1)))),meet(X2,join(join(X0,meet(X1,join(X0,meet(complement(X0),X1)))),meet(complement(X0),join(meet(complement(X0),join(X0,meet(complement(X0),X1))),X2)))))),
inference(superposition,[],[f171,f4378]) ).
fof(f8259,plain,
! [X2,X0,X1] : join(join(X0,meet(X1,join(X0,meet(complement(X0),X1)))),X2) = join(join(X0,meet(X1,join(X0,meet(complement(X0),X1)))),join(X2,meet(complement(X0),join(X0,meet(complement(X0),X1))))),
inference(superposition,[],[f757,f4378]) ).
fof(f8266,plain,
! [X2,X0,X1] : join(join(X0,meet(X1,join(X0,meet(complement(X0),X1)))),X2) = join(meet(complement(X0),join(X0,meet(complement(X0),X1))),join(join(X0,meet(X1,join(X0,meet(complement(X0),X1)))),X2)),
inference(forward_demodulation,[],[f8259,f67]) ).
fof(f8273,plain,
! [X2,X0,X1] : meet(complement(X0),join(join(X0,meet(X1,join(X0,meet(complement(X0),X1)))),meet(complement(X0),X2))) = meet(complement(X0),join(X0,join(meet(X1,join(X0,meet(complement(X0),X1))),meet(X2,join(join(X0,meet(X1,join(X0,meet(complement(X0),X1)))),meet(complement(X0),join(meet(complement(X0),join(X0,meet(complement(X0),X1))),X2))))))),
inference(forward_demodulation,[],[f8248,f8]) ).
fof(f8315,plain,
! [X2,X0,X1] : join(X0,join(meet(X1,join(X0,meet(complement(X0),X1))),X2)) = join(meet(complement(X0),join(X0,meet(complement(X0),X1))),join(X0,join(meet(X1,join(X0,meet(complement(X0),X1))),X2))),
inference(forward_demodulation,[],[f8266,f8]) ).
fof(f8319,plain,
! [X2,X0,X1] : meet(complement(X0),join(join(X0,meet(X1,join(X0,meet(complement(X0),X1)))),meet(complement(X0),X2))) = meet(complement(X0),join(X0,join(meet(X1,join(X0,meet(complement(X0),X1))),meet(X2,join(X0,join(meet(X1,join(X0,meet(complement(X0),X1))),meet(complement(X0),join(meet(complement(X0),join(X0,meet(complement(X0),X1))),X2)))))))),
inference(forward_demodulation,[],[f8273,f8]) ).
fof(f8345,plain,
! [X2,X0,X1] : join(X0,join(meet(X1,join(X0,meet(complement(X0),X1))),X2)) = join(X0,join(join(meet(X1,join(X0,meet(complement(X0),X1))),X2),meet(complement(X0),join(X0,meet(complement(X0),X1))))),
inference(forward_demodulation,[],[f8315,f67]) ).
fof(f8347,plain,
! [X2,X0,X1] : meet(complement(X0),join(X0,join(meet(X1,join(X0,meet(complement(X0),X1))),meet(X2,join(X0,join(meet(X1,join(X0,meet(complement(X0),X1))),meet(complement(X0),join(meet(complement(X0),join(X0,meet(complement(X0),X1))),X2)))))))) = meet(complement(X0),join(X0,join(meet(X1,join(X0,meet(complement(X0),X1))),meet(complement(X0),X2)))),
inference(forward_demodulation,[],[f8319,f8]) ).
fof(f8363,plain,
! [X2,X0,X1] : join(X0,join(meet(X1,join(X0,meet(complement(X0),X1))),X2)) = join(X0,join(meet(X1,join(X0,meet(complement(X0),X1))),join(X2,meet(complement(X0),join(X0,meet(complement(X0),X1)))))),
inference(forward_demodulation,[],[f8345,f8]) ).
fof(f8401,plain,
! [X2,X0,X1] : join(one,X2) = join(complement(meet(X0,X1)),join(X0,X2)),
inference(superposition,[],[f56,f481]) ).
fof(f8579,plain,
! [X2,X0,X1] : join(one,X2) = join(X0,join(X2,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f8401,f67]) ).
fof(f8623,plain,
! [X2,X0,X1] : one = join(X0,join(X2,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f8579,f356]) ).
fof(f9070,plain,
! [X2,X3,X0,X1] : join(X3,X2) = meet(join(X3,X2),join(X3,join(X0,join(X1,X2)))),
inference(superposition,[],[f68,f67]) ).
fof(f9150,plain,
! [X2,X0,X1] : one = join(join(X0,join(X1,X2)),complement(join(X0,X1))),
inference(superposition,[],[f621,f68]) ).
fof(f9164,plain,
! [X2,X0,X1] : one = join(complement(join(X0,X1)),join(X0,join(X1,X2))),
inference(forward_demodulation,[],[f9150,f6]) ).
fof(f9228,plain,
! [X2,X0,X1] : one = join(X0,join(join(X1,X2),complement(join(X0,X1)))),
inference(forward_demodulation,[],[f9164,f67]) ).
fof(f9249,plain,
! [X2,X0,X1] : one = join(X0,join(X1,join(X2,complement(join(X0,X1))))),
inference(forward_demodulation,[],[f9228,f8]) ).
fof(f9286,plain,
! [X2,X0,X1] : meet(join(X1,X2),X0) = join(meet(X0,X1),meet(join(X1,X2),X0)),
inference(superposition,[],[f149,f5]) ).
fof(f9302,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X2,X0)) = join(X0,meet(join(X0,X1),join(X2,X0))),
inference(superposition,[],[f149,f34]) ).
fof(f9522,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X0,meet(join(X0,X1),X2))) = meet(join(X0,X1),join(X0,meet(X2,meet(join(X0,X1),join(X2,X0))))),
inference(backward_demodulation,[],[f4236,f9302]) ).
fof(f9575,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X0,meet(join(X0,X1),X2))) = meet(join(X0,X1),join(X0,meet(X2,join(X0,X1)))),
inference(forward_demodulation,[],[f9522,f141]) ).
fof(f10684,plain,
! [X2,X0,X1] : join(meet(X1,X2),X0) = meet(join(X0,X1),join(meet(X1,X2),X0)),
inference(superposition,[],[f477,f6]) ).
fof(f10685,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(X0,X1),meet(X0,X2))),
inference(superposition,[],[f477,f4]) ).
fof(f11798,plain,
! [X2,X0,X1] : join(X2,meet(X1,X0)) = join(meet(X0,X1),X2),
inference(superposition,[],[f6,f8094]) ).
fof(f11808,plain,
! [X2,X3,X0,X1] : join(X3,meet(X1,X0)) = meet(join(X3,meet(X1,X0)),join(X3,join(meet(X0,X1),X2))),
inference(superposition,[],[f68,f8094]) ).
fof(f11832,plain,
! [X2,X3,X0,X1] : join(X2,meet(X1,X0)) = join(X2,join(meet(X0,X1),meet(X2,X3))),
inference(superposition,[],[f458,f8094]) ).
fof(f11880,plain,
! [X2,X0,X1] : join(X2,meet(X0,X1)) = join(X2,meet(X1,X0)),
inference(forward_demodulation,[],[f11832,f458]) ).
fof(f12118,plain,
! [X2,X3,X0,X1] : join(meet(X0,X1),meet(X2,X3)) = join(meet(X1,X0),meet(X3,X2)),
inference(superposition,[],[f11798,f11798]) ).
fof(f12222,plain,
! [X2,X3,X0,X1] : join(join(X0,X1),meet(X2,X3)) = join(X0,join(X1,meet(X3,X2))),
inference(superposition,[],[f67,f11798]) ).
fof(f12234,plain,
! [X2,X3,X0,X1] : join(X0,join(X1,meet(X2,X3))) = join(X0,join(X1,meet(X3,X2))),
inference(forward_demodulation,[],[f12222,f8]) ).
fof(f12564,plain,
! [X2,X3,X0,X1] : join(X3,meet(X0,meet(X1,X2))) = join(X3,meet(X2,meet(X0,X1))),
inference(superposition,[],[f11880,f7]) ).
fof(f13142,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,f2181]) ).
fof(f13171,plain,
! [X0,X1] :
( zero != meet(meet(X0,X1),complement(meet(X1,X0)))
| complement(meet(X0,X1)) = complement(meet(X1,X0)) ),
inference(trivial_inequality_removal,[],[f13142]) ).
fof(f13194,plain,
! [X0,X1] :
( zero != meet(X0,meet(X1,complement(meet(X1,X0))))
| complement(meet(X0,X1)) = complement(meet(X1,X0)) ),
inference(forward_demodulation,[],[f13171,f7]) ).
fof(f13326,plain,
! [X0,X1] : complement(meet(X0,X1)) = complement(meet(X1,X0)),
inference(forward_subsumption_resolution,[],[f13194,f664]) ).
fof(f15402,plain,
! [X2,X0,X1] : join(meet(join(X0,X1),X2),X0) = meet(join(X0,X1),join(meet(join(X0,X1),X2),X0)),
inference(superposition,[],[f10684,f41]) ).
fof(f15403,plain,
! [X2,X0,X1] : join(meet(join(X0,X1),X2),X1) = meet(join(X0,X1),join(meet(join(X0,X1),X2),X1)),
inference(superposition,[],[f10684,f50]) ).
fof(f15707,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,[],[f15403,f6]) ).
fof(f15708,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X1),X2)) = meet(join(X0,X1),join(X0,meet(join(X0,X1),X2))),
inference(forward_demodulation,[],[f15402,f6]) ).
fof(f15778,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X1),X2)) = meet(join(X0,X1),join(X0,meet(X2,join(X0,X1)))),
inference(backward_demodulation,[],[f9575,f15708]) ).
fof(f15857,plain,
! [X2,X0,X1] : join(X1,meet(join(X0,X1),X2)) = meet(join(X0,X1),join(X1,meet(X2,join(X0,X1)))),
inference(superposition,[],[f15778,f50]) ).
fof(f15916,plain,
! [X0,X1] : join(X1,meet(join(X1,meet(join(X0,X1),complement(meet(X0,X1)))),X0)) = meet(join(X1,meet(join(X0,X1),complement(meet(X0,X1)))),join(X1,meet(X0,join(X1,meet(X0,complement(meet(X0,X1))))))),
inference(superposition,[],[f15778,f3473]) ).
fof(f15971,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(complement(join(X0,X1)),join(X0,meet(join(X0,X1),X2)))) = meet(join(X0,X1),join(complement(join(X0,X1)),meet(join(X0,meet(X2,join(X0,X1))),join(complement(join(X0,X1)),join(X0,meet(join(X0,X1),X2)))))),
inference(superposition,[],[f251,f15778]) ).
fof(f16014,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X0,join(meet(join(X0,X1),X2),complement(join(X0,X1))))) = meet(join(X0,X1),join(complement(join(X0,X1)),meet(join(X0,meet(X2,join(X0,X1))),join(X0,join(meet(join(X0,X1),X2),complement(join(X0,X1))))))),
inference(forward_demodulation,[],[f15971,f67]) ).
fof(f16056,plain,
! [X0,X1] : join(X1,meet(X0,join(X1,meet(join(X0,X1),complement(meet(X0,X1)))))) = meet(join(X1,meet(join(X0,X1),complement(meet(X0,X1)))),join(X1,meet(X0,join(X1,meet(X0,complement(meet(X0,X1))))))),
inference(forward_demodulation,[],[f15916,f11880]) ).
fof(f16113,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X0,join(meet(join(X0,X1),X2),complement(join(X0,X1))))) = meet(join(X0,X1),join(complement(join(X0,X1)),join(X0,meet(X2,join(X0,X1))))),
inference(forward_demodulation,[],[f16014,f11808]) ).
fof(f16145,plain,
! [X0,X1] : join(X1,meet(X0,join(X1,meet(X0,complement(meet(X0,X1)))))) = meet(join(X1,meet(join(X0,X1),complement(meet(X0,X1)))),join(X1,meet(X0,join(X1,meet(X0,complement(meet(X0,X1))))))),
inference(forward_demodulation,[],[f16056,f3473]) ).
fof(f16170,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X0,join(meet(join(X0,X1),X2),complement(join(X0,X1))))) = meet(join(X0,X1),join(X0,join(meet(X2,join(X0,X1)),complement(join(X0,X1))))),
inference(forward_demodulation,[],[f16113,f67]) ).
fof(f16203,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X0,join(meet(join(X0,X1),X2),complement(join(X0,X1))))) = meet(join(X0,X1),join(X0,join(complement(join(X0,X1)),meet(X2,join(X0,X1))))),
inference(forward_demodulation,[],[f16170,f6]) ).
fof(f16217,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X0,join(complement(join(X0,X1)),meet(X2,join(X0,X1))))) = meet(join(X0,X1),join(X0,join(complement(join(X0,X1)),meet(join(X0,X1),X2)))),
inference(forward_demodulation,[],[f16203,f6]) ).
fof(f16381,plain,
! [X2,X3,X0,X1,X4] : meet(X2,join(X0,join(join(X1,meet(X3,X0)),meet(X2,X4)))) = meet(X2,join(X0,join(join(X1,meet(X3,X0)),meet(X4,join(X0,join(join(X1,meet(X3,X0)),meet(X2,join(X4,meet(X2,join(X0,X1)))))))))),
inference(superposition,[],[f210,f757]) ).
fof(f16512,plain,
! [X2,X0,X1] : meet(X1,join(X0,join(X2,meet(X1,X0)))) = meet(X1,join(X0,join(X2,X0))),
inference(superposition,[],[f210,f3]) ).
fof(f16669,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = meet(X1,join(X0,join(X2,meet(X1,X0)))),
inference(forward_demodulation,[],[f16512,f50]) ).
fof(f16770,plain,
! [X2,X3,X0,X1,X4] : meet(X2,join(X0,join(join(X1,meet(X3,X0)),meet(X2,X4)))) = meet(X2,join(X0,join(X1,join(meet(X3,X0),meet(X4,join(X0,join(join(X1,meet(X3,X0)),meet(X2,join(X4,meet(X2,join(X0,X1))))))))))),
inference(forward_demodulation,[],[f16381,f8]) ).
fof(f16827,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = meet(X1,join(X0,X2)),
inference(forward_demodulation,[],[f16669,f757]) ).
fof(f16896,plain,
! [X2,X3,X0,X1,X4] : meet(X2,join(X0,join(join(X1,meet(X3,X0)),meet(X2,X4)))) = meet(X2,join(X0,join(meet(X4,join(X0,join(join(X1,meet(X3,X0)),meet(X2,join(X4,meet(X2,join(X0,X1))))))),X1))),
inference(forward_demodulation,[],[f16770,f2072]) ).
fof(f17005,plain,
! [X2,X3,X0,X1,X4] : meet(X2,join(X0,join(join(X1,meet(X3,X0)),meet(X2,X4)))) = meet(X2,join(X0,join(X1,meet(X4,join(X0,join(join(X1,meet(X3,X0)),meet(X2,join(X4,meet(X2,join(X0,X1)))))))))),
inference(forward_demodulation,[],[f16896,f6]) ).
fof(f17053,plain,
! [X2,X3,X0,X1,X4] : meet(X2,join(X0,join(join(X1,meet(X3,X0)),meet(X2,X4)))) = meet(X2,join(X0,join(X1,meet(X4,join(X0,join(X1,join(meet(X3,X0),meet(X2,join(X4,meet(X2,join(X0,X1))))))))))),
inference(forward_demodulation,[],[f17005,f8]) ).
fof(f17083,plain,
! [X2,X3,X0,X1,X4] : meet(X2,join(X0,join(join(X1,meet(X3,X0)),meet(X2,X4)))) = meet(X2,join(X0,join(X1,meet(X4,join(X0,join(meet(X2,join(X4,meet(X2,join(X0,X1)))),X1)))))),
inference(forward_demodulation,[],[f17053,f2072]) ).
fof(f17106,plain,
! [X2,X3,X0,X1,X4] : meet(X2,join(X0,join(join(X1,meet(X3,X0)),meet(X2,X4)))) = meet(X2,join(X0,join(X1,meet(X4,join(X0,join(X1,meet(X2,join(X4,meet(X2,join(X0,X1)))))))))),
inference(forward_demodulation,[],[f17083,f6]) ).
fof(f17115,plain,
! [X2,X3,X0,X1,X4] : meet(X2,join(X0,join(join(X1,meet(X3,X0)),meet(X2,X4)))) = meet(X2,join(X0,join(X1,meet(X2,X4)))),
inference(forward_demodulation,[],[f17106,f210]) ).
fof(f17121,plain,
! [X2,X3,X0,X1,X4] : meet(X2,join(X0,join(X1,meet(X2,X4)))) = meet(X2,join(X0,join(X1,join(meet(X3,X0),meet(X2,X4))))),
inference(forward_demodulation,[],[f17115,f8]) ).
fof(f17126,plain,
! [X2,X0,X1,X4] : meet(X2,join(X0,join(X1,meet(X2,X4)))) = meet(X2,join(X0,join(meet(X2,X4),X1))),
inference(forward_demodulation,[],[f17121,f2072]) ).
fof(f17162,plain,
! [X2,X3,X0,X1] : meet(X3,join(X0,meet(X1,X2))) = meet(X3,join(X0,meet(X2,X1))),
inference(superposition,[],[f16827,f11798]) ).
fof(f17165,plain,
! [X2,X0,X1] : meet(X2,meet(X0,X1)) = meet(X2,join(meet(X1,X0),meet(X0,X1))),
inference(superposition,[],[f16827,f548]) ).
fof(f17167,plain,
! [X2,X3,X0,X1] : meet(X3,join(X2,join(X0,X1))) = meet(X3,join(X0,join(X1,X2))),
inference(superposition,[],[f16827,f8]) ).
fof(f17276,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(X2,X1),X0),
inference(superposition,[],[f5,f16827]) ).
fof(f17322,plain,
! [X2,X3,X0,X1] : meet(meet(X0,X1),join(X2,X3)) = meet(X0,meet(X1,join(X3,X2))),
inference(superposition,[],[f7,f16827]) ).
fof(f17349,plain,
! [X2,X3,X0,X1] : meet(X0,meet(X1,join(X2,X3))) = meet(X0,meet(X1,join(X3,X2))),
inference(forward_demodulation,[],[f17322,f7]) ).
fof(f17388,plain,
! [X2,X0,X1] : meet(X2,meet(X0,X1)) = meet(X2,meet(X1,X0)),
inference(forward_demodulation,[],[f17165,f548]) ).
fof(f17603,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(meet(X2,X1),X0),
inference(superposition,[],[f5,f17388]) ).
fof(f18798,plain,
! [X2,X0,X1] : join(X1,meet(join(X1,X0),X2)) = meet(join(X1,X0),join(X1,meet(join(X0,X1),X2))),
inference(superposition,[],[f15778,f17276]) ).
fof(f18804,plain,
! [X2,X0,X1] : meet(join(X0,X1),X2) = meet(join(X1,X0),X2),
inference(superposition,[],[f5,f17276]) ).
fof(f18914,plain,
! [X2,X3,X0,X1] : join(X3,meet(X0,join(X1,X2))) = join(X3,meet(X0,join(X2,X1))),
inference(superposition,[],[f11880,f17276]) ).
fof(f19332,plain,
! [X2,X0,X1] : meet(join(meet(X0,X1),X2),X0) = join(meet(X0,X1),meet(join(meet(X0,X1),X2),X0)),
inference(superposition,[],[f9286,f52]) ).
fof(f19727,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,join(meet(X0,X1),X2))) = meet(join(meet(X0,X1),X2),X0),
inference(forward_demodulation,[],[f19332,f11880]) ).
fof(f19849,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = join(meet(X0,X1),meet(X0,join(meet(X0,X1),X2))),
inference(forward_demodulation,[],[f19727,f5]) ).
fof(f20563,plain,
! [X0,X1] : join(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))) = join(join(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))),X0),
inference(superposition,[],[f32,f6071]) ).
fof(f20650,plain,
! [X0,X1] : join(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))) = join(X0,join(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1))))))),
inference(forward_demodulation,[],[f20563,f6]) ).
fof(f20710,plain,
! [X0,X1] : join(X0,complement(meet(X0,X1))) = join(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f20650,f458]) ).
fof(f20760,plain,
! [X0,X1] : one = join(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f20710,f481]) ).
fof(f20962,plain,
! [X0,X1] : meet(complement(meet(X0,complement(meet(X0,X1)))),join(X0,meet(complement(meet(X0,complement(meet(X0,X1)))),complement(meet(X0,X1))))) = meet(complement(meet(X0,complement(meet(X0,X1)))),join(X0,meet(complement(meet(X0,X1)),join(X0,meet(complement(meet(X0,complement(meet(X0,X1)))),one))))),
inference(superposition,[],[f162,f20760]) ).
fof(f20967,plain,
! [X0,X1] :
( one != one
| zero != meet(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1))))))
| complement(complement(meet(X0,X1))) = meet(X0,complement(meet(X0,complement(meet(X0,X1))))) ),
inference(superposition,[],[f11,f20760]) ).
fof(f21002,plain,
! [X0,X1] :
( zero != meet(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1))))))
| complement(complement(meet(X0,X1))) = meet(X0,complement(meet(X0,complement(meet(X0,X1))))) ),
inference(trivial_inequality_removal,[],[f20967]) ).
fof(f21030,plain,
! [X0,X1] : complement(complement(meet(X0,X1))) = meet(X0,complement(meet(X0,complement(meet(X0,X1))))),
inference(forward_subsumption_resolution,[],[f21002,f664]) ).
fof(f21034,plain,
! [X0,X1] : meet(complement(meet(X0,complement(meet(X0,X1)))),join(X0,meet(complement(meet(X0,complement(meet(X0,X1)))),complement(meet(X0,X1))))) = meet(complement(meet(X0,complement(meet(X0,X1)))),join(X0,meet(complement(meet(X0,X1)),join(X0,meet(one,complement(meet(X0,complement(meet(X0,X1))))))))),
inference(forward_demodulation,[],[f20962,f17162]) ).
fof(f21114,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,complement(meet(X0,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f21030,f4751]) ).
fof(f21116,plain,
! [X0,X1] : meet(complement(meet(X0,complement(meet(X0,X1)))),join(X0,meet(complement(meet(X0,complement(meet(X0,X1)))),complement(meet(X0,X1))))) = meet(complement(meet(X0,complement(meet(X0,X1)))),join(X0,meet(complement(meet(X0,X1)),join(X0,complement(meet(X0,complement(meet(X0,X1)))))))),
inference(forward_demodulation,[],[f21034,f358]) ).
fof(f21148,plain,
! [X0,X1] : meet(complement(meet(X0,complement(meet(X0,X1)))),join(X0,meet(complement(meet(X0,complement(meet(X0,X1)))),complement(meet(X0,X1))))) = meet(complement(meet(X0,complement(meet(X0,X1)))),join(X0,meet(complement(meet(X0,X1)),one))),
inference(forward_demodulation,[],[f21116,f481]) ).
fof(f21174,plain,
! [X0,X1] : meet(complement(meet(X0,complement(meet(X0,X1)))),join(X0,meet(complement(meet(X0,complement(meet(X0,X1)))),complement(meet(X0,X1))))) = meet(complement(meet(X0,complement(meet(X0,X1)))),join(X0,meet(one,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f21148,f17162]) ).
fof(f21191,plain,
! [X0,X1] : meet(complement(meet(X0,complement(meet(X0,X1)))),join(X0,meet(complement(meet(X0,complement(meet(X0,X1)))),complement(meet(X0,X1))))) = meet(complement(meet(X0,complement(meet(X0,X1)))),join(X0,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f21174,f358]) ).
fof(f21203,plain,
! [X0,X1] : meet(complement(meet(X0,complement(meet(X0,X1)))),join(X0,meet(complement(meet(X0,complement(meet(X0,X1)))),complement(meet(X0,X1))))) = meet(join(complement(meet(X0,X1)),X0),complement(meet(X0,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f21191,f17276]) ).
fof(f21210,plain,
! [X0,X1] : meet(join(X0,complement(meet(X0,X1))),complement(meet(X0,complement(meet(X0,X1))))) = meet(complement(meet(X0,complement(meet(X0,X1)))),join(X0,meet(complement(meet(X0,complement(meet(X0,X1)))),complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f21203,f18804]) ).
fof(f21216,plain,
! [X0,X1] : meet(join(X0,complement(meet(X0,X1))),complement(meet(X0,complement(meet(X0,X1))))) = meet(complement(meet(X0,complement(meet(X0,X1)))),join(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))))),
inference(forward_demodulation,[],[f21210,f17162]) ).
fof(f21221,plain,
! [X0,X1] : meet(one,complement(meet(X0,complement(meet(X0,X1))))) = meet(complement(meet(X0,complement(meet(X0,X1)))),join(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))))),
inference(forward_demodulation,[],[f21216,f481]) ).
fof(f21226,plain,
! [X0,X1] : complement(meet(X0,complement(meet(X0,X1)))) = meet(complement(meet(X0,complement(meet(X0,X1)))),join(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))))),
inference(forward_demodulation,[],[f21221,f358]) ).
fof(f21243,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,complement(meet(X1,complement(meet(X0,X1))))),
inference(superposition,[],[f21114,f51]) ).
fof(f21327,plain,
! [X0,X1] : meet(X1,X0) = meet(X1,complement(meet(X1,complement(meet(X0,X1))))),
inference(superposition,[],[f21114,f13326]) ).
fof(f21630,plain,
! [X0,X1] : meet(join(X0,X1),X0) = meet(join(X0,X1),complement(meet(join(X0,X1),complement(X0)))),
inference(superposition,[],[f21327,f3]) ).
fof(f21708,plain,
! [X0,X1] : meet(X0,complement(meet(X1,X0))) = meet(X0,complement(meet(X0,X1))),
inference(superposition,[],[f21114,f21327]) ).
fof(f21728,plain,
! [X0,X1] : meet(X0,join(complement(X0),meet(X0,X1))) = meet(X0,join(complement(X0),meet(complement(meet(X0,complement(meet(X1,X0)))),join(complement(X0),meet(X0,X1))))),
inference(superposition,[],[f251,f21327]) ).
fof(f21751,plain,
! [X2,X0,X1] : meet(X2,meet(X0,X1)) = meet(meet(complement(meet(X0,complement(meet(X1,X0)))),X0),X2),
inference(superposition,[],[f17603,f21327]) ).
fof(f21783,plain,
! [X2,X0,X1] : meet(X2,meet(X0,X1)) = meet(complement(meet(X0,complement(meet(X1,X0)))),meet(X0,X2)),
inference(forward_demodulation,[],[f21751,f7]) ).
fof(f21801,plain,
! [X0,X1] : meet(X0,join(complement(X0),meet(X0,X1))) = meet(X0,join(complement(X0),meet(join(complement(X0),meet(X0,X1)),complement(meet(X0,complement(meet(X1,X0))))))),
inference(forward_demodulation,[],[f21728,f17162]) ).
fof(f21881,plain,
! [X0,X1] : meet(join(X0,X1),X0) = meet(join(X0,X1),complement(meet(complement(X0),join(X0,X1)))),
inference(forward_demodulation,[],[f21630,f21708]) ).
fof(f21908,plain,
! [X2,X0,X1] : meet(X2,meet(X0,X1)) = meet(X0,meet(X2,complement(meet(X0,complement(meet(X1,X0)))))),
inference(forward_demodulation,[],[f21783,f108]) ).
fof(f21991,plain,
! [X0,X1] : meet(X0,join(X0,X1)) = meet(join(X0,X1),complement(meet(complement(X0),join(X0,X1)))),
inference(forward_demodulation,[],[f21881,f5]) ).
fof(f22070,plain,
! [X0,X1] : meet(join(X0,X1),complement(meet(complement(X0),join(X0,X1)))) = X0,
inference(forward_demodulation,[],[f21991,f3]) ).
fof(f22253,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(meet(X1,X0)),meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f32,f21708]) ).
fof(f22321,plain,
! [X2,X0,X1] : meet(X0,meet(complement(meet(X0,X1)),X2)) = meet(X2,meet(X0,complement(meet(X1,X0)))),
inference(superposition,[],[f108,f21708]) ).
fof(f22352,plain,
! [X2,X0,X1] : meet(X2,meet(X0,complement(meet(X1,X0)))) = meet(meet(complement(meet(X0,X1)),X0),X2),
inference(superposition,[],[f17603,f21708]) ).
fof(f22384,plain,
! [X2,X0,X1] : meet(X2,meet(X0,complement(meet(X1,X0)))) = meet(complement(meet(X0,X1)),meet(X0,X2)),
inference(forward_demodulation,[],[f22352,f7]) ).
fof(f22468,plain,
! [X2,X0,X1] : meet(X0,meet(X2,complement(meet(X0,X1)))) = meet(X2,meet(X0,complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f22384,f108]) ).
fof(f22679,plain,
! [X0,X1] : meet(X1,join(complement(X1),meet(X0,X1))) = meet(X1,join(complement(X1),meet(complement(meet(X1,complement(meet(X0,X1)))),join(complement(X1),meet(X0,X1))))),
inference(superposition,[],[f251,f21243]) ).
fof(f22754,plain,
! [X0,X1] : meet(X1,join(complement(X1),meet(X0,X1))) = meet(X1,join(complement(X1),meet(join(complement(X1),meet(X0,X1)),complement(meet(X1,complement(meet(X0,X1))))))),
inference(forward_demodulation,[],[f22679,f17162]) ).
fof(f23027,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(meet(X0,X1)),meet(complement(meet(X1,complement(meet(X0,X1)))),complement(meet(complement(meet(X1,complement(meet(X0,X1)))),X1)))),
inference(superposition,[],[f22253,f21243]) ).
fof(f23043,plain,
! [X0,X1] : complement(meet(complement(X0),join(X0,meet(complement(X0),X1)))) = join(complement(meet(complement(X0),join(X0,meet(complement(X0),X1)))),meet(join(X0,meet(X1,join(X0,meet(complement(X0),X1)))),complement(meet(join(X0,meet(X1,join(X0,meet(complement(X0),X1)))),complement(X0))))),
inference(superposition,[],[f22253,f4378]) ).
fof(f23371,plain,
! [X0,X1] : complement(meet(complement(X0),join(X0,meet(complement(X0),X1)))) = join(complement(meet(complement(X0),join(X0,meet(complement(X0),X1)))),meet(join(X0,meet(X1,join(X0,meet(complement(X0),X1)))),complement(meet(complement(X0),join(X0,meet(X1,join(X0,meet(complement(X0),X1)))))))),
inference(forward_demodulation,[],[f23043,f21708]) ).
fof(f23383,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(meet(X0,X1)),meet(complement(meet(X1,complement(meet(X0,X1)))),complement(meet(X1,complement(meet(X1,complement(meet(X0,X1)))))))),
inference(forward_demodulation,[],[f23027,f21708]) ).
fof(f23546,plain,
! [X0,X1] : complement(meet(complement(X0),join(X0,meet(complement(X0),X1)))) = join(complement(meet(complement(X0),join(X0,meet(complement(X0),X1)))),X0),
inference(forward_demodulation,[],[f23371,f22070]) ).
fof(f23553,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(meet(X0,X1)),meet(complement(meet(X1,complement(meet(X0,X1)))),complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f23383,f21327]) ).
fof(f23645,plain,
! [X0,X1] : complement(meet(complement(X0),join(X0,meet(complement(X0),X1)))) = join(X0,complement(meet(complement(X0),join(X0,meet(complement(X0),X1))))),
inference(forward_demodulation,[],[f23546,f6]) ).
fof(f23646,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(meet(X0,X1)),meet(complement(meet(X1,X0)),complement(meet(X1,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f23553,f11880]) ).
fof(f24556,plain,
! [X0,X1] : join(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1)))))) = join(join(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1)))))),complement(meet(X0,complement(meet(X0,X1))))),
inference(superposition,[],[f32,f21226]) ).
fof(f24630,plain,
! [X0,X1] : join(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1)))))) = join(complement(meet(X0,complement(meet(X0,X1)))),join(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))))),
inference(forward_demodulation,[],[f24556,f6]) ).
fof(f24702,plain,
! [X0,X1] : join(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1)))))) = join(X0,join(meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))),complement(meet(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f24630,f67]) ).
fof(f24750,plain,
! [X0,X1] : one = join(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f24702,f8623]) ).
fof(f24988,plain,
! [X0,X1] :
( one != one
| zero != meet(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))))
| complement(X0) = meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))) ),
inference(superposition,[],[f11,f24750]) ).
fof(f25044,plain,
! [X0,X1] :
( zero != meet(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))))
| complement(X0) = meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))) ),
inference(trivial_inequality_removal,[],[f24988]) ).
fof(f25088,plain,
! [X0,X1] : complement(X0) = meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))),
inference(forward_subsumption_resolution,[],[f25044,f249]) ).
fof(f25459,plain,
! [X0,X1] : complement(X0) = meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X1,X0))))),
inference(superposition,[],[f25088,f21708]) ).
fof(f25476,plain,
! [X0,X1] : complement(X0) = meet(complement(meet(X0,X1)),complement(X0)),
inference(superposition,[],[f52,f25088]) ).
fof(f25559,plain,
! [X0,X1] : complement(X0) = meet(complement(X0),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f25476,f5]) ).
fof(f25576,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(meet(X0,X1)),complement(X1)),
inference(backward_demodulation,[],[f23646,f25459]) ).
fof(f25678,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X1),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f25576,f6]) ).
fof(f25868,plain,
! [X0,X1] : complement(X1) = meet(complement(X1),complement(meet(X0,X1))),
inference(superposition,[],[f25559,f13326]) ).
fof(f25889,plain,
! [X2,X0,X1] : meet(join(complement(X0),X1),complement(meet(X0,X2))) = join(complement(X0),meet(join(complement(X0),X1),complement(meet(X0,X2)))),
inference(superposition,[],[f149,f25559]) ).
fof(f25951,plain,
! [X0,X1] : meet(X0,join(complement(X0),meet(X0,X1))) = meet(X0,meet(join(complement(X0),meet(X0,X1)),complement(meet(X0,complement(meet(X1,X0)))))),
inference(backward_demodulation,[],[f21801,f25889]) ).
fof(f25952,plain,
! [X0,X1] : meet(X1,join(complement(X1),meet(X0,X1))) = meet(X1,meet(join(complement(X1),meet(X0,X1)),complement(meet(X1,complement(meet(X0,X1)))))),
inference(backward_demodulation,[],[f22754,f25889]) ).
fof(f26003,plain,
! [X0,X1] : meet(X1,join(complement(X1),meet(X0,X1))) = meet(join(complement(X1),meet(X0,X1)),meet(X1,X0)),
inference(forward_demodulation,[],[f25952,f21908]) ).
fof(f26004,plain,
! [X0,X1] : meet(X0,join(complement(X0),meet(X0,X1))) = meet(join(complement(X0),meet(X0,X1)),meet(X0,X1)),
inference(forward_demodulation,[],[f25951,f21908]) ).
fof(f26022,plain,
! [X0,X1] : meet(X1,join(complement(X1),meet(X0,X1))) = meet(meet(X1,X0),join(complement(X1),meet(X0,X1))),
inference(forward_demodulation,[],[f26003,f5]) ).
fof(f26023,plain,
! [X0,X1] : meet(X0,join(complement(X0),meet(X0,X1))) = meet(meet(X0,X1),join(complement(X0),meet(X0,X1))),
inference(forward_demodulation,[],[f26004,f5]) ).
fof(f26033,plain,
! [X0,X1] : meet(X1,join(complement(X1),meet(X0,X1))) = meet(X1,meet(X0,join(complement(X1),meet(X0,X1)))),
inference(forward_demodulation,[],[f26022,f7]) ).
fof(f26034,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(complement(X0),meet(X0,X1))),
inference(forward_demodulation,[],[f26023,f34]) ).
fof(f26039,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,join(complement(X1),meet(X0,X1))),
inference(forward_demodulation,[],[f26033,f7366]) ).
fof(f26050,plain,
! [X2,X0,X1] : meet(X0,join(complement(X0),join(meet(X1,join(complement(X0),meet(X0,X1))),meet(X0,X2)))) = meet(X0,join(complement(X0),join(meet(X1,join(complement(X0),meet(X0,X1))),meet(X2,join(complement(X0),join(meet(X1,join(complement(X0),meet(X0,X1))),meet(X0,join(meet(X0,X1),X2)))))))),
inference(backward_demodulation,[],[f3447,f26034]) ).
fof(f26055,plain,
! [X2,X0,X1] : join(complement(X0),join(meet(X1,join(complement(X0),meet(X0,X1))),X2)) = join(complement(X0),join(meet(X1,join(complement(X0),meet(X0,X1))),join(X2,meet(X0,X1)))),
inference(backward_demodulation,[],[f5028,f26034]) ).
fof(f26084,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,join(complement(X1),meet(X0,join(complement(X1),meet(X0,X1))))),
inference(backward_demodulation,[],[f1308,f26039]) ).
fof(f26088,plain,
! [X2,X0,X1] : join(complement(X0),join(meet(X1,join(complement(X0),meet(X0,X1))),X2)) = join(complement(X0),join(meet(X0,X1),join(meet(X1,join(complement(X0),meet(X0,X1))),X2))),
inference(forward_demodulation,[],[f26055,f67]) ).
fof(f26096,plain,
! [X2,X0,X1] : join(complement(X0),join(meet(X1,join(complement(X0),meet(X0,X1))),X2)) = join(complement(X0),join(meet(X0,X1),X2)),
inference(forward_demodulation,[],[f26088,f779]) ).
fof(f26102,plain,
! [X2,X0,X1] : meet(X0,join(complement(X0),join(meet(X1,join(complement(X0),meet(X0,X1))),meet(X0,X2)))) = meet(X0,join(complement(X0),join(meet(X0,X1),meet(X2,join(complement(X0),join(meet(X1,join(complement(X0),meet(X0,X1))),meet(X0,join(meet(X0,X1),X2)))))))),
inference(backward_demodulation,[],[f26050,f26096]) ).
fof(f26116,plain,
! [X2,X0,X1] : meet(X0,join(complement(X0),join(meet(X1,join(complement(X0),meet(X0,X1))),meet(X0,X2)))) = meet(X0,join(complement(X0),join(meet(X0,X1),meet(X2,join(complement(X0),join(meet(X0,X1),meet(X0,join(meet(X0,X1),X2)))))))),
inference(forward_demodulation,[],[f26102,f26096]) ).
fof(f26118,plain,
! [X2,X0,X1] : meet(X0,join(complement(X0),join(meet(X1,join(complement(X0),meet(X0,X1))),meet(X0,X2)))) = meet(X0,join(complement(X0),join(meet(X0,X1),meet(X2,join(complement(X0),meet(X0,join(meet(X0,X1),X2))))))),
inference(forward_demodulation,[],[f26116,f19849]) ).
fof(f26119,plain,
! [X2,X0,X1] : meet(X0,join(complement(X0),join(meet(X0,X1),meet(X0,X2)))) = meet(X0,join(complement(X0),join(meet(X0,X1),meet(X2,join(complement(X0),meet(X0,join(meet(X0,X1),X2))))))),
inference(forward_demodulation,[],[f26118,f26096]) ).
fof(f26122,plain,
! [X0,X1] : meet(complement(X0),X1) = meet(complement(X0),join(X0,meet(complement(X0),X1))),
inference(superposition,[],[f26034,f4751]) ).
fof(f26176,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X1),X2)) = meet(join(X0,X1),join(complement(join(X0,X1)),join(X0,meet(join(X0,X1),X2)))),
inference(superposition,[],[f26034,f15778]) ).
fof(f26406,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X1),X2)) = meet(join(X0,X1),join(X0,join(meet(join(X0,X1),X2),complement(join(X0,X1))))),
inference(forward_demodulation,[],[f26176,f17167]) ).
fof(f26436,plain,
! [X2,X0,X1] : meet(complement(X0),join(X0,join(meet(X1,join(X0,meet(complement(X0),X1))),meet(complement(X0),X2)))) = meet(complement(X0),join(X0,join(meet(X1,join(X0,meet(complement(X0),X1))),meet(X2,join(X0,join(meet(X1,join(X0,meet(complement(X0),X1))),meet(complement(X0),join(meet(complement(X0),X1),X2)))))))),
inference(backward_demodulation,[],[f8347,f26122]) ).
fof(f26439,plain,
! [X2,X0,X1] : join(X0,join(meet(X1,join(X0,meet(complement(X0),X1))),X2)) = join(X0,join(meet(X1,join(X0,meet(complement(X0),X1))),join(X2,meet(complement(X0),X1)))),
inference(backward_demodulation,[],[f8363,f26122]) ).
fof(f26450,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(X0,complement(meet(complement(X0),X1))),
inference(backward_demodulation,[],[f23645,f26122]) ).
fof(f26520,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X1),X2)) = meet(join(X0,X1),join(X0,join(complement(join(X0,X1)),meet(join(X0,X1),X2)))),
inference(forward_demodulation,[],[f26406,f17126]) ).
fof(f26537,plain,
! [X2,X0,X1] : join(X0,join(meet(X1,join(X0,meet(complement(X0),X1))),X2)) = join(X0,join(meet(complement(X0),X1),join(meet(X1,join(X0,meet(complement(X0),X1))),X2))),
inference(forward_demodulation,[],[f26439,f67]) ).
fof(f26577,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X1),X2)) = meet(join(X0,X1),join(X0,join(complement(join(X0,X1)),meet(X2,join(X0,X1))))),
inference(backward_demodulation,[],[f16217,f26520]) ).
fof(f26579,plain,
! [X2,X0,X1] : join(X0,join(meet(X1,join(X0,meet(complement(X0),X1))),X2)) = join(X0,join(meet(complement(X0),X1),X2)),
inference(forward_demodulation,[],[f26537,f779]) ).
fof(f26601,plain,
! [X2,X0,X1] : meet(complement(X0),join(X0,join(meet(X1,join(X0,meet(complement(X0),X1))),meet(complement(X0),X2)))) = meet(complement(X0),join(X0,join(meet(complement(X0),X1),meet(X2,join(X0,join(meet(X1,join(X0,meet(complement(X0),X1))),meet(complement(X0),join(meet(complement(X0),X1),X2)))))))),
inference(backward_demodulation,[],[f26436,f26579]) ).
fof(f26618,plain,
! [X2,X0,X1] : meet(complement(X0),join(X0,join(meet(X1,join(X0,meet(complement(X0),X1))),meet(complement(X0),X2)))) = meet(complement(X0),join(X0,join(meet(complement(X0),X1),meet(X2,join(X0,join(meet(complement(X0),X1),meet(complement(X0),join(meet(complement(X0),X1),X2)))))))),
inference(forward_demodulation,[],[f26601,f26579]) ).
fof(f26626,plain,
! [X2,X0,X1] : meet(complement(X0),join(X0,join(meet(X1,join(X0,meet(complement(X0),X1))),meet(complement(X0),X2)))) = meet(complement(X0),join(X0,join(meet(complement(X0),X1),meet(X2,join(X0,meet(complement(X0),join(meet(complement(X0),X1),X2))))))),
inference(forward_demodulation,[],[f26618,f19849]) ).
fof(f26632,plain,
! [X2,X0,X1] : meet(complement(X0),join(X0,join(meet(complement(X0),X1),meet(X2,join(X0,meet(complement(X0),join(meet(complement(X0),X1),X2))))))) = meet(complement(X0),join(X0,join(meet(complement(X0),X1),meet(complement(X0),X2)))),
inference(forward_demodulation,[],[f26626,f26579]) ).
fof(f26853,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(join(X0,X1)),complement(X0)),
inference(superposition,[],[f25868,f3]) ).
fof(f26854,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(join(X1,X0)),complement(X0)),
inference(superposition,[],[f25868,f34]) ).
fof(f26944,plain,
! [X2,X0,X1] : join(complement(meet(X1,X0)),X2) = join(complement(meet(X1,X0)),join(complement(X0),X2)),
inference(superposition,[],[f54,f25868]) ).
fof(f27013,plain,
! [X2,X0,X1] : join(complement(meet(X1,X0)),X2) = join(complement(X0),join(X2,complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f26944,f67]) ).
fof(f27051,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(X0),complement(join(X1,X0))),
inference(forward_demodulation,[],[f26854,f5]) ).
fof(f27052,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X0),complement(join(X0,X1))),
inference(forward_demodulation,[],[f26853,f5]) ).
fof(f27427,plain,
! [X0,X1] : complement(X0) = join(complement(join(X0,X1)),complement(X0)),
inference(superposition,[],[f25678,f3]) ).
fof(f27428,plain,
! [X0,X1] : complement(X0) = join(complement(join(X1,X0)),complement(X0)),
inference(superposition,[],[f25678,f34]) ).
fof(f27589,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X1,X0))),
inference(forward_demodulation,[],[f27428,f6]) ).
fof(f27590,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X0,X1))),
inference(forward_demodulation,[],[f27427,f6]) ).
fof(f27643,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),X1))) = X0,
inference(superposition,[],[f27590,f4751]) ).
fof(f27913,plain,
! [X2,X0,X1] : meet(complement(join(X1,X0)),X2) = meet(complement(join(X1,X0)),meet(complement(X0),X2)),
inference(superposition,[],[f95,f27589]) ).
fof(f27947,plain,
! [X2,X0,X1] : meet(complement(join(X1,X0)),X2) = meet(complement(X0),meet(X2,complement(join(X1,X0)))),
inference(forward_demodulation,[],[f27913,f108]) ).
fof(f28090,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = meet(complement(join(complement(X0),X1)),X0),
inference(superposition,[],[f34,f27643]) ).
fof(f28094,plain,
! [X2,X0,X1] : join(X2,X0) = join(X0,join(complement(join(complement(X0),X1)),X2)),
inference(superposition,[],[f67,f27643]) ).
fof(f28103,plain,
! [X2,X3,X0,X1] : meet(X1,join(X0,join(complement(join(complement(X0),X2)),meet(X1,X3)))) = meet(X1,join(X0,join(complement(join(complement(X0),X2)),meet(X3,join(X0,join(complement(join(complement(X0),X2)),meet(X1,join(X3,meet(X1,X0))))))))),
inference(superposition,[],[f210,f27643]) ).
fof(f28172,plain,
! [X2,X3,X0,X1] : meet(X1,join(meet(X1,X3),X0)) = meet(X1,join(X0,join(complement(join(complement(X0),X2)),meet(X3,join(X0,join(complement(join(complement(X0),X2)),meet(X1,join(X3,meet(X1,X0))))))))),
inference(backward_demodulation,[],[f28103,f28094]) ).
fof(f28175,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = meet(X0,complement(join(complement(X0),X1))),
inference(forward_demodulation,[],[f28090,f5]) ).
fof(f28212,plain,
! [X2,X3,X0,X1] : meet(X1,join(meet(X1,X3),X0)) = meet(X1,join(meet(X3,join(X0,join(complement(join(complement(X0),X2)),meet(X1,join(X3,meet(X1,X0)))))),X0)),
inference(forward_demodulation,[],[f28172,f28094]) ).
fof(f28222,plain,
! [X2,X3,X0,X1] : meet(X1,join(meet(X1,X3),X0)) = meet(X1,join(X0,meet(X3,join(X0,join(complement(join(complement(X0),X2)),meet(X1,join(X3,meet(X1,X0)))))))),
inference(forward_demodulation,[],[f28212,f16827]) ).
fof(f28224,plain,
! [X3,X0,X1] : meet(X1,join(meet(X1,X3),X0)) = meet(X1,join(X0,meet(X3,join(meet(X1,join(X3,meet(X1,X0))),X0)))),
inference(forward_demodulation,[],[f28222,f28094]) ).
fof(f28226,plain,
! [X3,X0,X1] : meet(X1,join(meet(X1,X3),X0)) = meet(X1,join(X0,meet(X3,join(X0,meet(X1,join(X3,meet(X1,X0))))))),
inference(forward_demodulation,[],[f28224,f18914]) ).
fof(f28284,plain,
! [X2,X0,X1] : meet(X2,X0) = join(meet(X2,X0),meet(X2,complement(join(complement(X0),X1)))),
inference(superposition,[],[f109,f28175]) ).
fof(f28850,plain,
! [X2,X0,X1] : complement(join(X0,meet(X1,X2))) = meet(complement(meet(X2,X1)),complement(join(X0,meet(X1,X2)))),
inference(superposition,[],[f27052,f11798]) ).
fof(f29080,plain,
! [X0,X1] : meet(join(X0,X1),join(complement(join(X0,X1)),X0)) = X0,
inference(superposition,[],[f26039,f3]) ).
fof(f29230,plain,
! [X2,X0,X1] : meet(X2,meet(X0,join(X1,X2))) = meet(X2,join(complement(join(X1,X2)),meet(X0,join(X1,X2)))),
inference(superposition,[],[f95,f26039]) ).
fof(f29249,plain,
! [X2,X0,X1] : meet(X2,X0) = meet(X2,join(complement(join(X1,X2)),meet(X0,join(X1,X2)))),
inference(forward_demodulation,[],[f29230,f829]) ).
fof(f29340,plain,
! [X0,X1] : meet(join(X0,X1),join(X0,complement(join(X0,X1)))) = X0,
inference(forward_demodulation,[],[f29080,f16827]) ).
fof(f29584,plain,
! [X0,X1] : meet(X1,X0) = meet(X1,join(X0,complement(join(X0,X1)))),
inference(superposition,[],[f95,f29340]) ).
fof(f29623,plain,
! [X0,X1] : meet(join(X0,X1),join(join(X0,complement(join(X0,X1))),meet(join(X0,X1),complement(X0)))) = meet(join(X0,X1),join(join(X0,complement(join(X0,X1))),meet(join(join(X0,X1),join(X0,complement(join(X0,X1)))),complement(X0)))),
inference(superposition,[],[f3473,f29340]) ).
fof(f29665,plain,
! [X0,X1] : meet(join(X0,X1),join(join(X0,complement(join(X0,X1))),meet(join(X0,X1),complement(X0)))) = meet(join(X0,X1),join(join(X0,complement(join(X0,X1))),meet(complement(X0),join(join(X0,X1),join(X0,complement(join(X0,X1))))))),
inference(forward_demodulation,[],[f29623,f17162]) ).
fof(f29703,plain,
! [X0,X1] :
( meet(X1,X0) != zero
| complement(join(X0,complement(join(X0,X1)))) = X1 ),
inference(backward_demodulation,[],[f4748,f29584]) ).
fof(f29745,plain,
! [X0,X1] : meet(join(X0,X1),join(join(X0,complement(join(X0,X1))),meet(join(X0,X1),complement(X0)))) = meet(join(X0,X1),join(X0,join(complement(join(X0,X1)),meet(complement(X0),join(join(X0,X1),join(X0,complement(join(X0,X1)))))))),
inference(forward_demodulation,[],[f29665,f8]) ).
fof(f29788,plain,
! [X0,X1] : meet(join(X0,X1),join(join(X0,complement(join(X0,X1))),meet(join(X0,X1),complement(X0)))) = meet(join(X0,X1),join(X0,join(complement(join(X0,X1)),meet(complement(X0),join(X0,join(complement(join(X0,X1)),join(X0,X1))))))),
inference(forward_demodulation,[],[f29745,f17167]) ).
fof(f29810,plain,
! [X0,X1] : meet(join(X0,X1),join(join(X0,complement(join(X0,X1))),meet(join(X0,X1),complement(X0)))) = meet(join(X0,X1),join(X0,join(complement(join(X0,X1)),meet(complement(X0),join(X0,join(X1,join(X0,complement(join(X0,X1))))))))),
inference(forward_demodulation,[],[f29788,f2095]) ).
fof(f29820,plain,
! [X0,X1] : meet(join(X0,X1),join(join(X0,complement(join(X0,X1))),meet(join(X0,X1),complement(X0)))) = meet(join(X0,X1),join(X0,join(complement(join(X0,X1)),meet(complement(X0),one)))),
inference(forward_demodulation,[],[f29810,f9249]) ).
fof(f29825,plain,
! [X0,X1] : meet(join(X0,X1),join(join(X0,complement(join(X0,X1))),meet(join(X0,X1),complement(X0)))) = meet(join(X0,X1),join(X0,join(complement(join(X0,X1)),meet(one,complement(X0))))),
inference(forward_demodulation,[],[f29820,f12234]) ).
fof(f29828,plain,
! [X0,X1] : meet(join(X0,X1),join(join(X0,complement(join(X0,X1))),meet(join(X0,X1),complement(X0)))) = meet(join(X0,X1),join(X0,join(complement(join(X0,X1)),complement(X0)))),
inference(forward_demodulation,[],[f29825,f358]) ).
fof(f29831,plain,
! [X0,X1] : meet(join(X0,X1),one) = meet(join(X0,X1),join(join(X0,complement(join(X0,X1))),meet(join(X0,X1),complement(X0)))),
inference(forward_demodulation,[],[f29828,f2265]) ).
fof(f29834,plain,
! [X0,X1] : meet(join(X0,X1),one) = meet(join(X0,X1),join(join(X0,complement(join(X0,X1))),meet(complement(X0),join(X0,X1)))),
inference(forward_demodulation,[],[f29831,f17162]) ).
fof(f29837,plain,
! [X0,X1] : meet(join(X0,X1),one) = meet(join(X0,X1),join(X0,join(complement(join(X0,X1)),meet(complement(X0),join(X0,X1))))),
inference(forward_demodulation,[],[f29834,f8]) ).
fof(f29840,plain,
! [X0,X1] : meet(join(X0,X1),one) = join(X0,meet(join(X0,X1),complement(X0))),
inference(forward_demodulation,[],[f29837,f26577]) ).
fof(f29843,plain,
! [X0,X1] : meet(join(X0,X1),one) = join(X0,meet(complement(X0),join(X0,X1))),
inference(forward_demodulation,[],[f29840,f11880]) ).
fof(f29845,plain,
! [X0,X1] : meet(one,join(X0,X1)) = join(X0,meet(complement(X0),join(X0,X1))),
inference(forward_demodulation,[],[f29843,f5]) ).
fof(f29847,plain,
! [X0,X1] : join(X0,X1) = join(X0,meet(complement(X0),join(X0,X1))),
inference(forward_demodulation,[],[f29845,f358]) ).
fof(f29853,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(X1,complement(join(X0,X1)))),
inference(superposition,[],[f29584,f6]) ).
fof(f29959,plain,
! [X2,X0,X1] : meet(X0,join(join(X1,complement(join(X1,X0))),meet(X0,X2))) = meet(X0,join(join(X1,complement(join(X1,X0))),meet(X2,join(join(X1,complement(join(X1,X0))),meet(X0,join(meet(X0,X1),X2)))))),
inference(superposition,[],[f171,f29584]) ).
fof(f30060,plain,
! [X2,X0,X1] : meet(X0,join(join(X1,complement(join(X1,X0))),meet(X0,X2))) = meet(X0,join(X1,join(complement(join(X1,X0)),meet(X2,join(join(X1,complement(join(X1,X0))),meet(X0,join(meet(X0,X1),X2))))))),
inference(forward_demodulation,[],[f29959,f8]) ).
fof(f30148,plain,
! [X0,X1] : meet(X0,join(X1,join(complement(join(X0,X1)),meet(X0,complement(meet(X0,X1)))))) = X0,
inference(backward_demodulation,[],[f6116,f29853]) ).
fof(f30149,plain,
! [X0,X1] :
( meet(X1,X0) != zero
| complement(join(X0,complement(join(X1,X0)))) = X1 ),
inference(backward_demodulation,[],[f4749,f29853]) ).
fof(f30181,plain,
! [X2,X0,X1] : meet(X0,join(join(X1,complement(join(X1,X0))),meet(X0,X2))) = meet(X0,join(X1,join(complement(join(X1,X0)),meet(X2,join(X1,join(complement(join(X1,X0)),meet(X0,join(meet(X0,X1),X2)))))))),
inference(forward_demodulation,[],[f30060,f8]) ).
fof(f30273,plain,
! [X2,X0,X1] : meet(X0,join(X1,join(complement(join(X1,X0)),meet(X0,X2)))) = meet(X0,join(X1,join(complement(join(X1,X0)),meet(X2,join(X1,join(complement(join(X1,X0)),meet(X0,join(meet(X0,X1),X2)))))))),
inference(forward_demodulation,[],[f30181,f8]) ).
fof(f30726,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X2),X1)) = meet(X0,join(join(meet(X0,X2),X1),complement(join(X0,X1)))),
inference(superposition,[],[f29853,f53]) ).
fof(f30788,plain,
! [X2,X0,X1] : meet(X2,join(X1,X0)) = meet(X2,join(X0,join(X1,complement(join(X2,join(X1,X0)))))),
inference(superposition,[],[f29853,f56]) ).
fof(f30994,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X2),X1)) = meet(X0,join(complement(join(X0,X1)),join(meet(X0,X2),X1))),
inference(forward_demodulation,[],[f30726,f16827]) ).
fof(f31087,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X2),X1)) = meet(X0,join(X1,join(complement(join(X0,X1)),meet(X0,X2)))),
inference(forward_demodulation,[],[f30994,f17167]) ).
fof(f31142,plain,
! [X0,X1] : meet(X0,join(meet(X0,complement(meet(X0,X1))),X1)) = X0,
inference(backward_demodulation,[],[f30148,f31087]) ).
fof(f31172,plain,
! [X0,X1] : meet(X0,join(X1,meet(X0,complement(meet(X0,X1))))) = X0,
inference(forward_demodulation,[],[f31142,f16827]) ).
fof(f31191,plain,
! [X0,X1] : join(X1,meet(join(X1,X0),complement(meet(X0,X1)))) = join(X1,join(meet(join(X1,X0),complement(meet(X0,X1))),X0)),
inference(backward_demodulation,[],[f3586,f31172]) ).
fof(f31207,plain,
! [X0,X1] : meet(join(X1,meet(join(X0,X1),complement(meet(X0,X1)))),join(X0,meet(join(X1,meet(join(X0,X1),complement(meet(X0,X1)))),complement(X0)))) = meet(join(X1,meet(join(X0,X1),complement(meet(X0,X1)))),join(X0,meet(join(X0,X1),complement(X0)))),
inference(backward_demodulation,[],[f6437,f31172]) ).
fof(f31212,plain,
! [X0,X1] : join(X1,X0) = meet(join(X1,meet(join(X0,X1),complement(meet(X0,X1)))),join(X1,X0)),
inference(backward_demodulation,[],[f16145,f31172]) ).
fof(f31268,plain,
! [X0,X1] : join(X1,X0) = meet(join(X0,X1),join(X1,meet(join(X0,X1),complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f31212,f17276]) ).
fof(f31271,plain,
! [X0,X1] : meet(join(X1,meet(join(X0,X1),complement(meet(X0,X1)))),join(X0,meet(join(X1,meet(join(X0,X1),complement(meet(X0,X1)))),complement(X0)))) = meet(join(X1,meet(join(X0,X1),complement(meet(X0,X1)))),join(X0,meet(complement(X0),join(X0,X1)))),
inference(forward_demodulation,[],[f31207,f17162]) ).
fof(f31285,plain,
! [X0,X1] : join(X1,meet(join(X1,X0),complement(meet(X0,X1)))) = join(X1,join(X0,meet(join(X1,X0),complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f31191,f6]) ).
fof(f31301,plain,
! [X0,X1] : join(X1,X0) = join(X1,meet(join(X0,X1),complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f31268,f15707]) ).
fof(f31304,plain,
! [X0,X1] : meet(join(X1,meet(join(X0,X1),complement(meet(X0,X1)))),join(X0,meet(join(X1,meet(join(X0,X1),complement(meet(X0,X1)))),complement(X0)))) = meet(join(X1,meet(join(X0,X1),complement(meet(X0,X1)))),join(X0,X1)),
inference(forward_demodulation,[],[f31271,f29847]) ).
fof(f31316,plain,
! [X0,X1] : join(X1,X0) = join(X1,meet(join(X1,X0),complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f31285,f63]) ).
fof(f31340,plain,
! [X0,X1] : meet(join(X1,meet(join(X0,X1),complement(meet(X0,X1)))),join(X0,meet(join(X1,meet(join(X0,X1),complement(meet(X0,X1)))),complement(X0)))) = meet(join(X1,X0),join(X1,meet(join(X0,X1),complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f31304,f17276]) ).
fof(f31377,plain,
! [X0,X1] : join(X1,meet(join(X1,X0),complement(meet(X0,X1)))) = meet(join(X1,meet(join(X0,X1),complement(meet(X0,X1)))),join(X0,meet(join(X1,meet(join(X0,X1),complement(meet(X0,X1)))),complement(X0)))),
inference(forward_demodulation,[],[f31340,f18798]) ).
fof(f31391,plain,
! [X0,X1] : join(X1,meet(join(X1,X0),complement(meet(X0,X1)))) = meet(join(X1,meet(join(X0,X1),complement(meet(X0,X1)))),join(X0,meet(complement(X0),join(X1,meet(join(X0,X1),complement(meet(X0,X1))))))),
inference(forward_demodulation,[],[f31377,f17162]) ).
fof(f31396,plain,
! [X0,X1] : join(X1,meet(join(X1,X0),complement(meet(X0,X1)))) = meet(join(X1,X0),join(X0,meet(complement(X0),join(X1,X0)))),
inference(forward_demodulation,[],[f31391,f31301]) ).
fof(f31398,plain,
! [X0,X1] : join(X1,meet(join(X1,X0),complement(meet(X0,X1)))) = join(X0,meet(join(X1,X0),complement(X0))),
inference(forward_demodulation,[],[f31396,f15857]) ).
fof(f31400,plain,
! [X0,X1] : join(X1,meet(join(X1,X0),complement(meet(X0,X1)))) = join(X0,meet(complement(X0),join(X1,X0))),
inference(forward_demodulation,[],[f31398,f11880]) ).
fof(f31401,plain,
! [X0,X1] : join(X1,X0) = join(X0,meet(complement(X0),join(X1,X0))),
inference(forward_demodulation,[],[f31400,f31316]) ).
fof(f31483,plain,
! [X0,X1] : join(meet(X1,X0),X1) = join(meet(X1,X0),meet(join(meet(X1,X0),X1),complement(meet(X0,X1)))),
inference(superposition,[],[f31316,f295]) ).
fof(f31580,plain,
! [X0,X1] : join(X0,X1) = join(X0,meet(join(X0,X1),complement(meet(X0,X1)))),
inference(superposition,[],[f31316,f13326]) ).
fof(f31701,plain,
! [X0,X1] : meet(X1,join(X0,X1)) = meet(X1,join(X0,meet(X1,complement(meet(X0,X1))))),
inference(backward_demodulation,[],[f3498,f31580]) ).
fof(f31824,plain,
! [X0,X1] : join(meet(X1,X0),X1) = join(meet(X1,X0),meet(complement(meet(X0,X1)),join(meet(X1,X0),X1))),
inference(forward_demodulation,[],[f31483,f11880]) ).
fof(f31919,plain,
! [X0,X1] : meet(X1,join(X0,meet(X1,complement(meet(X0,X1))))) = X1,
inference(forward_demodulation,[],[f31701,f34]) ).
fof(f31996,plain,
! [X0,X1] : join(meet(X1,X0),X1) = join(meet(X1,X0),meet(complement(meet(X0,X1)),join(X1,meet(X1,X0)))),
inference(forward_demodulation,[],[f31824,f18914]) ).
fof(f32142,plain,
! [X0,X1] : join(meet(X1,X0),X1) = join(meet(X1,X0),meet(complement(meet(X0,X1)),X1)),
inference(forward_demodulation,[],[f31996,f4]) ).
fof(f32272,plain,
! [X0,X1] : join(meet(X1,X0),X1) = join(meet(X1,X0),meet(X1,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f32142,f11880]) ).
fof(f32351,plain,
! [X0,X1] : join(X1,meet(X1,X0)) = join(meet(X1,X0),meet(X1,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f32272,f6]) ).
fof(f32390,plain,
! [X0,X1] : join(meet(X1,X0),meet(X1,complement(meet(X0,X1)))) = X1,
inference(forward_demodulation,[],[f32351,f4]) ).
fof(f32603,plain,
! [X0,X1] : join(X1,meet(X0,complement(meet(X1,X0)))) = join(join(X1,meet(X0,complement(meet(X1,X0)))),X0),
inference(superposition,[],[f32,f31919]) ).
fof(f32713,plain,
! [X0,X1] : join(X1,meet(X0,complement(meet(X1,X0)))) = join(X0,join(X1,meet(X0,complement(meet(X1,X0))))),
inference(forward_demodulation,[],[f32603,f6]) ).
fof(f32831,plain,
! [X0,X1] : join(X0,X1) = join(X1,meet(X0,complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f32713,f458]) ).
fof(f33772,plain,
! [X0,X1] : join(X1,complement(join(X0,X1))) = join(meet(join(X1,complement(join(X0,X1))),X0),meet(join(X1,complement(join(X0,X1))),complement(meet(X0,X1)))),
inference(superposition,[],[f32390,f29853]) ).
fof(f33852,plain,
! [X0,X1] : join(X1,X0) = join(X1,meet(X0,complement(meet(X1,X0)))),
inference(superposition,[],[f54,f32390]) ).
fof(f34019,plain,
! [X0,X1] : join(X1,complement(join(X0,X1))) = join(meet(join(X1,complement(join(X0,X1))),X0),meet(complement(meet(X0,X1)),join(X1,complement(join(X0,X1))))),
inference(forward_demodulation,[],[f33772,f11880]) ).
fof(f34218,plain,
! [X0,X1] : join(X1,complement(join(X0,X1))) = join(meet(X0,join(X1,complement(join(X0,X1)))),meet(join(X1,complement(join(X0,X1))),complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f34019,f12118]) ).
fof(f34374,plain,
! [X0,X1] : join(X1,complement(join(X0,X1))) = join(meet(X0,join(X1,complement(join(X0,X1)))),meet(complement(meet(X0,X1)),join(X1,complement(join(X0,X1))))),
inference(forward_demodulation,[],[f34218,f11880]) ).
fof(f34477,plain,
! [X0,X1] : join(X1,complement(join(X0,X1))) = join(meet(X0,X1),meet(complement(meet(X0,X1)),join(X1,complement(join(X0,X1))))),
inference(forward_demodulation,[],[f34374,f29853]) ).
fof(f34602,plain,
! [X2,X0,X1] : join(X2,meet(X0,X1)) = join(X2,meet(meet(X0,X1),complement(meet(X0,meet(X1,X2))))),
inference(superposition,[],[f33852,f108]) ).
fof(f34902,plain,
! [X2,X0,X1] : join(X2,meet(X0,X1)) = join(X2,meet(X0,meet(X1,complement(meet(X0,meet(X1,X2)))))),
inference(forward_demodulation,[],[f34602,f7]) ).
fof(f35163,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(meet(complement(X1),join(X0,X1)),join(X1,X2)),
inference(superposition,[],[f56,f31401]) ).
fof(f35164,plain,
! [X2,X0,X1] : join(X2,join(X0,X1)) = join(X1,join(meet(complement(X1),join(X0,X1)),X2)),
inference(superposition,[],[f67,f31401]) ).
fof(f35173,plain,
! [X2,X3,X0,X1] : meet(X2,join(X1,join(meet(complement(X1),join(X0,X1)),meet(X2,X3)))) = meet(X2,join(X1,join(meet(complement(X1),join(X0,X1)),meet(X3,join(X1,join(meet(complement(X1),join(X0,X1)),meet(X2,join(X3,meet(X2,join(X0,X1)))))))))),
inference(superposition,[],[f210,f31401]) ).
fof(f35197,plain,
! [X2,X0,X1] : join(X2,join(X0,meet(X1,X2))) = join(X2,meet(complement(meet(X1,X2)),join(X0,meet(X1,X2)))),
inference(superposition,[],[f54,f31401]) ).
fof(f35198,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X1,meet(complement(meet(X1,X2)),join(X0,meet(X1,X2)))))) = meet(X1,join(X2,meet(meet(complement(meet(X1,X2)),join(X0,meet(X1,X2))),join(X2,meet(X1,join(X0,meet(X1,X2))))))),
inference(superposition,[],[f171,f31401]) ).
fof(f35229,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X1,meet(complement(meet(X1,X2)),join(X0,meet(X1,X2)))))) = meet(X1,join(X2,meet(join(X2,meet(X1,join(X0,meet(X1,X2)))),meet(complement(meet(X1,X2)),join(X0,meet(X1,X2)))))),
inference(forward_demodulation,[],[f35198,f17162]) ).
fof(f35230,plain,
! [X2,X0,X1] : join(X2,X0) = join(X2,meet(complement(meet(X1,X2)),join(X0,meet(X1,X2)))),
inference(forward_demodulation,[],[f35197,f757]) ).
fof(f35249,plain,
! [X2,X3,X0,X1] : meet(X2,join(X1,join(meet(complement(X1),join(X0,X1)),meet(X2,X3)))) = meet(X2,join(meet(X3,join(X1,join(meet(complement(X1),join(X0,X1)),meet(X2,join(X3,meet(X2,join(X0,X1))))))),join(X0,X1))),
inference(backward_demodulation,[],[f35173,f35164]) ).
fof(f35250,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X1,join(X2,meet(complement(X1),join(X0,X1)))),
inference(forward_demodulation,[],[f35163,f67]) ).
fof(f35320,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X1,meet(complement(meet(X1,X2)),join(X0,meet(X1,X2)))))) = meet(X1,join(X2,meet(join(X0,meet(X1,X2)),meet(join(X2,meet(X1,join(X0,meet(X1,X2)))),complement(meet(X1,X2)))))),
inference(forward_demodulation,[],[f35229,f12564]) ).
fof(f35335,plain,
! [X2,X3,X0,X1] : meet(X2,join(X1,join(meet(complement(X1),join(X0,X1)),meet(X2,X3)))) = meet(X2,join(X0,join(X1,meet(X3,join(X1,join(meet(complement(X1),join(X0,X1)),meet(X2,join(X3,meet(X2,join(X0,X1)))))))))),
inference(forward_demodulation,[],[f35249,f17167]) ).
fof(f35336,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X1,join(X2,meet(complement(X1),join(X0,X1)))),
inference(forward_demodulation,[],[f35250,f8]) ).
fof(f35374,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X1,meet(complement(meet(X1,X2)),join(X0,meet(X1,X2)))))) = meet(X1,join(X2,meet(complement(meet(X1,X2)),meet(join(X0,meet(X1,X2)),join(X2,meet(X1,join(X0,meet(X1,X2)))))))),
inference(forward_demodulation,[],[f35320,f12564]) ).
fof(f35383,plain,
! [X2,X3,X0,X1] : meet(X2,join(X1,join(meet(complement(X1),join(X0,X1)),meet(X2,X3)))) = meet(X2,join(X0,join(X1,meet(X3,join(meet(X2,join(X3,meet(X2,join(X0,X1)))),join(X0,X1)))))),
inference(forward_demodulation,[],[f35335,f35164]) ).
fof(f35399,plain,
! [X2,X3,X0,X1] : meet(X2,join(X1,join(meet(complement(X1),join(X0,X1)),meet(X2,X3)))) = meet(X2,join(X0,join(X1,meet(X3,join(join(X0,X1),meet(X2,join(X3,meet(X2,join(X0,X1))))))))),
inference(forward_demodulation,[],[f35383,f18914]) ).
fof(f35407,plain,
! [X2,X3,X0,X1] : meet(X2,join(X0,join(X1,meet(X3,join(X0,join(X1,meet(X2,join(X3,meet(X2,join(X0,X1)))))))))) = meet(X2,join(X1,join(meet(complement(X1),join(X0,X1)),meet(X2,X3)))),
inference(forward_demodulation,[],[f35399,f8]) ).
fof(f35412,plain,
! [X2,X3,X0,X1] : meet(X2,join(X0,join(X1,meet(X3,join(X0,join(X1,meet(X2,join(X3,meet(X2,join(X0,X1)))))))))) = meet(X2,join(meet(X2,X3),join(X0,X1))),
inference(forward_demodulation,[],[f35407,f35164]) ).
fof(f35731,plain,
! [X0,X1] : meet(complement(X1),X0) = join(meet(complement(X1),X0),complement(join(complement(X0),X1))),
inference(superposition,[],[f28284,f27051]) ).
fof(f35766,plain,
! [X2,X0,X1] : join(complement(join(X0,X1)),X2) = meet(join(X2,complement(X1)),join(complement(join(X0,X1)),X2)),
inference(superposition,[],[f10684,f27051]) ).
fof(f36460,plain,
! [X0,X1] : meet(complement(X1),complement(X0)) = join(meet(complement(X1),complement(X0)),complement(join(X0,X1))),
inference(superposition,[],[f35731,f4751]) ).
fof(f36546,plain,
! [X0,X1] : complement(complement(join(complement(X1),X0))) = join(complement(complement(join(complement(X1),X0))),complement(meet(complement(X0),X1))),
inference(superposition,[],[f27589,f35731]) ).
fof(f36550,plain,
! [X0,X1] : meet(meet(complement(X0),X1),complement(join(complement(X1),X0))) = meet(meet(complement(X0),X1),join(complement(join(complement(X1),X0)),complement(meet(complement(X0),X1)))),
inference(superposition,[],[f29853,f35731]) ).
fof(f36555,plain,
! [X0,X1] : meet(meet(complement(X0),X1),complement(join(complement(X1),X0))) = meet(complement(X0),meet(X1,join(complement(join(complement(X1),X0)),complement(meet(complement(X0),X1))))),
inference(forward_demodulation,[],[f36550,f7]) ).
fof(f36557,plain,
! [X0,X1] : complement(complement(join(complement(X1),X0))) = join(complement(meet(complement(X0),X1)),complement(complement(join(complement(X1),X0)))),
inference(forward_demodulation,[],[f36546,f6]) ).
fof(f36615,plain,
! [X0,X1] : meet(complement(X1),complement(X0)) = join(complement(join(X0,X1)),meet(complement(X1),complement(X0))),
inference(forward_demodulation,[],[f36460,f6]) ).
fof(f36648,plain,
! [X0,X1] : meet(complement(X0),meet(X1,join(complement(join(complement(X1),X0)),complement(meet(complement(X0),X1))))) = meet(complement(X0),meet(X1,complement(join(complement(X1),X0)))),
inference(forward_demodulation,[],[f36555,f7]) ).
fof(f36650,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(meet(complement(X0),X1)),join(complement(X1),X0)),
inference(forward_demodulation,[],[f36557,f4751]) ).
fof(f36718,plain,
! [X0,X1] : meet(complement(X0),meet(X1,join(complement(join(complement(X1),X0)),complement(meet(complement(X0),X1))))) = meet(complement(join(complement(X1),X0)),X1),
inference(forward_demodulation,[],[f36648,f27947]) ).
fof(f36720,plain,
! [X0,X1] : join(complement(X1),X0) = join(join(complement(X1),X0),complement(meet(complement(X0),X1))),
inference(forward_demodulation,[],[f36650,f6]) ).
fof(f36775,plain,
! [X0,X1] : meet(X1,complement(join(complement(X1),X0))) = meet(complement(X0),meet(X1,join(complement(join(complement(X1),X0)),complement(meet(complement(X0),X1))))),
inference(forward_demodulation,[],[f36718,f5]) ).
fof(f36777,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(X1),join(X0,complement(meet(complement(X0),X1)))),
inference(forward_demodulation,[],[f36720,f8]) ).
fof(f36815,plain,
! [X0,X1] : complement(join(complement(X1),X0)) = meet(complement(X0),meet(X1,join(complement(join(complement(X1),X0)),complement(meet(complement(X0),X1))))),
inference(forward_demodulation,[],[f36775,f28175]) ).
fof(f36817,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(meet(complement(X0),X1)),X0),
inference(forward_demodulation,[],[f36777,f27013]) ).
fof(f36840,plain,
! [X0,X1] : join(complement(X1),X0) = join(X0,complement(meet(complement(X0),X1))),
inference(forward_demodulation,[],[f36817,f6]) ).
fof(f36859,plain,
! [X0,X1] : join(complement(X1),X0) = complement(meet(complement(X0),X1)),
inference(backward_demodulation,[],[f26450,f36840]) ).
fof(f36934,plain,
! [X0,X1] : complement(join(complement(X1),X0)) = meet(complement(X0),meet(X1,join(complement(join(complement(X1),X0)),join(complement(X1),X0)))),
inference(backward_demodulation,[],[f36815,f36859]) ).
fof(f37061,plain,
! [X0,X1] : complement(join(complement(X1),X0)) = meet(complement(X0),meet(X1,join(join(complement(X1),X0),complement(join(complement(X1),X0))))),
inference(forward_demodulation,[],[f36934,f17349]) ).
fof(f37096,plain,
! [X0,X1] : meet(complement(X0),meet(X1,one)) = complement(join(complement(X1),X0)),
inference(forward_demodulation,[],[f37061,f9]) ).
fof(f37104,plain,
! [X0,X1] : meet(one,meet(complement(X0),X1)) = complement(join(complement(X1),X0)),
inference(forward_demodulation,[],[f37096,f108]) ).
fof(f37108,plain,
! [X0,X1] : meet(complement(X0),X1) = complement(join(complement(X1),X0)),
inference(forward_demodulation,[],[f37104,f358]) ).
fof(f37331,plain,
! [X2,X0,X1] : complement(meet(join(complement(X0),X1),X2)) = join(complement(X2),meet(complement(X1),X0)),
inference(superposition,[],[f36859,f36859]) ).
fof(f37394,plain,
! [X0,X1] : join(complement(X0),X1) = complement(meet(X0,complement(X1))),
inference(superposition,[],[f13326,f36859]) ).
fof(f37412,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(X1),meet(X0,join(complement(X0),X1))),
inference(superposition,[],[f33852,f36859]) ).
fof(f37821,plain,
! [X0,X1] : meet(complement(X1),complement(X0)) = complement(meet(join(complement(complement(X0)),X1),join(X0,X1))),
inference(backward_demodulation,[],[f36615,f37331]) ).
fof(f38049,plain,
! [X0,X1] : meet(complement(X1),complement(X0)) = complement(meet(join(X0,X1),join(complement(complement(X0)),X1))),
inference(forward_demodulation,[],[f37821,f13326]) ).
fof(f38176,plain,
! [X0,X1] : meet(complement(X1),complement(X0)) = complement(meet(join(X0,X1),join(X0,X1))),
inference(forward_demodulation,[],[f38049,f4751]) ).
fof(f38257,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X1),complement(X0)),
inference(forward_demodulation,[],[f38176,f1]) ).
fof(f38347,plain,
! [X2,X0,X1] : complement(join(X0,meet(X1,X2))) = complement(join(join(X0,meet(X1,X2)),meet(X2,X1))),
inference(backward_demodulation,[],[f28850,f38257]) ).
fof(f38472,plain,
! [X2,X0,X1] : complement(join(X0,meet(X1,X2))) = complement(join(meet(X2,X1),join(X0,meet(X1,X2)))),
inference(forward_demodulation,[],[f38347,f6]) ).
fof(f38566,plain,
! [X2,X0,X1] : complement(join(X0,meet(X1,X2))) = complement(join(meet(X2,X1),X0)),
inference(forward_demodulation,[],[f38472,f4863]) ).
fof(f38898,plain,
! [X2,X0,X1] : complement(join(meet(complement(X0),X1),X2)) = meet(complement(X2),join(complement(X1),X0)),
inference(superposition,[],[f37108,f37108]) ).
fof(f38907,plain,
! [X0,X1] : meet(complement(X0),X1) = complement(join(X0,complement(X1))),
inference(superposition,[],[f37108,f6]) ).
fof(f39020,plain,
! [X0,X1] :
( meet(complement(X0),join(X0,X1)) = X1
| meet(X1,X0) != zero ),
inference(backward_demodulation,[],[f29703,f38907]) ).
fof(f39025,plain,
! [X0,X1] :
( meet(complement(X0),join(X1,X0)) = X1
| meet(X1,X0) != zero ),
inference(backward_demodulation,[],[f30149,f38907]) ).
fof(f39266,plain,
! [X0,X1] :
( meet(complement(meet(X0,complement(meet(X1,X0)))),join(X0,X1)) = X1
| zero != meet(X1,meet(X0,complement(meet(X1,X0)))) ),
inference(superposition,[],[f39025,f32831]) ).
fof(f39477,plain,
! [X0,X1] : meet(complement(meet(X0,complement(meet(X1,X0)))),join(X0,X1)) = X1,
inference(forward_subsumption_resolution,[],[f39266,f249]) ).
fof(f39537,plain,
! [X0,X1] : meet(join(X1,X0),complement(meet(X0,complement(meet(X1,X0))))) = X1,
inference(forward_demodulation,[],[f39477,f17276]) ).
fof(f39589,plain,
! [X0,X1] : meet(join(X1,X0),join(complement(X0),meet(X1,X0))) = X1,
inference(forward_demodulation,[],[f39537,f37394]) ).
fof(f39721,plain,
! [X2,X0,X1] : complement(join(meet(complement(X0),X1),X2)) = meet(complement(X2),join(X0,complement(X1))),
inference(superposition,[],[f37108,f38907]) ).
fof(f39735,plain,
! [X0,X1] : join(X1,complement(join(X0,X1))) = join(meet(X0,X1),complement(join(meet(complement(X1),join(X0,X1)),meet(X0,X1)))),
inference(backward_demodulation,[],[f34477,f39721]) ).
fof(f39801,plain,
! [X0,X1] : join(X1,complement(join(X0,X1))) = join(meet(X0,X1),complement(join(meet(X0,X1),meet(join(X0,X1),complement(X1))))),
inference(forward_demodulation,[],[f39735,f38566]) ).
fof(f39842,plain,
! [X0,X1] : join(X1,complement(join(X0,X1))) = join(meet(X0,X1),complement(join(meet(X0,X1),meet(complement(X1),join(X0,X1))))),
inference(forward_demodulation,[],[f39801,f11880]) ).
fof(f39950,plain,
! [X2,X0,X1] : join(X2,complement(join(X0,X1))) = join(meet(complement(X0),complement(X1)),X2),
inference(superposition,[],[f11798,f38257]) ).
fof(f39952,plain,
! [X2,X0,X1] : join(X2,complement(join(X0,X1))) = join(X2,meet(complement(X0),complement(X1))),
inference(superposition,[],[f11880,f38257]) ).
fof(f39991,plain,
! [X2,X0,X1] : join(X2,complement(join(X0,X1))) = join(X2,complement(join(X1,X0))),
inference(forward_demodulation,[],[f39952,f38257]) ).
fof(f39993,plain,
! [X2,X0,X1] : join(X2,complement(join(X0,X1))) = join(complement(join(X1,X0)),X2),
inference(forward_demodulation,[],[f39950,f38257]) ).
fof(f40616,plain,
! [X0,X1] :
( meet(X1,complement(meet(X0,X1))) = meet(complement(X0),join(X0,X1))
| zero != meet(meet(X1,complement(meet(X0,X1))),X0) ),
inference(superposition,[],[f39020,f33852]) ).
fof(f40617,plain,
! [X0,X1] :
( meet(X0,complement(meet(X1,X0))) = meet(complement(X1),join(X0,X1))
| zero != meet(meet(X0,complement(meet(X1,X0))),X1) ),
inference(superposition,[],[f39020,f32831]) ).
fof(f40852,plain,
! [X0,X1] :
( zero != meet(X1,meet(X0,complement(meet(X1,X0))))
| meet(X0,complement(meet(X1,X0))) = meet(complement(X1),join(X0,X1)) ),
inference(forward_demodulation,[],[f40617,f5]) ).
fof(f40853,plain,
! [X0,X1] :
( zero != meet(X0,meet(X1,complement(meet(X0,X1))))
| meet(X1,complement(meet(X0,X1))) = meet(complement(X0),join(X0,X1)) ),
inference(forward_demodulation,[],[f40616,f5]) ).
fof(f40931,plain,
! [X0,X1] : meet(X0,complement(meet(X1,X0))) = meet(complement(X1),join(X0,X1)),
inference(forward_subsumption_resolution,[],[f40852,f249]) ).
fof(f40932,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(complement(X0),join(X0,X1)),
inference(forward_subsumption_resolution,[],[f40853,f249]) ).
fof(f41267,plain,
! [X0,X1] : meet(complement(X1),X0) = meet(complement(X1),join(X0,X1)),
inference(superposition,[],[f141,f39589]) ).
fof(f41274,plain,
! [X0,X1] : join(complement(X1),meet(X0,X1)) = join(join(complement(X1),meet(X0,X1)),X0),
inference(superposition,[],[f32,f39589]) ).
fof(f41275,plain,
! [X0,X1] : meet(join(complement(X1),meet(X0,X1)),X0) = X0,
inference(superposition,[],[f51,f39589]) ).
fof(f41286,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(join(complement(X1),meet(X0,X1)),meet(join(X0,X1),X2))) = meet(join(X0,X1),join(join(complement(X1),meet(X0,X1)),meet(X2,join(join(complement(X1),meet(X0,X1)),meet(join(X0,X1),join(X0,X2)))))),
inference(superposition,[],[f171,f39589]) ).
fof(f41299,plain,
! [X2,X0,X1] : join(join(complement(X1),meet(X0,X1)),X2) = join(join(complement(X1),meet(X0,X1)),join(X2,X0)),
inference(superposition,[],[f757,f39589]) ).
fof(f41332,plain,
! [X2,X0,X1] : join(join(complement(X1),meet(X0,X1)),X2) = join(X0,join(join(complement(X1),meet(X0,X1)),X2)),
inference(forward_demodulation,[],[f41299,f67]) ).
fof(f41345,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(join(complement(X1),meet(X0,X1)),meet(join(X0,X1),X2))) = meet(join(X0,X1),join(complement(X1),join(meet(X0,X1),meet(X2,join(join(complement(X1),meet(X0,X1)),meet(join(X0,X1),join(X0,X2))))))),
inference(forward_demodulation,[],[f41286,f8]) ).
fof(f41355,plain,
! [X0,X1] : meet(X0,join(complement(X1),meet(X0,X1))) = X0,
inference(forward_demodulation,[],[f41275,f5]) ).
fof(f41356,plain,
! [X0,X1] : join(complement(X1),meet(X0,X1)) = join(X0,join(complement(X1),meet(X0,X1))),
inference(forward_demodulation,[],[f41274,f6]) ).
fof(f41366,plain,
! [X0,X1] : join(X1,X0) = join(X0,meet(complement(X0),X1)),
inference(backward_demodulation,[],[f31401,f41267]) ).
fof(f41371,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X1,join(X2,meet(complement(X1),X0))),
inference(backward_demodulation,[],[f35336,f41267]) ).
fof(f41383,plain,
! [X0,X1] : join(X1,complement(join(X0,X1))) = join(meet(X0,X1),complement(join(meet(X0,X1),meet(complement(X1),X0)))),
inference(backward_demodulation,[],[f39842,f41267]) ).
fof(f41384,plain,
! [X0,X1] : meet(X0,complement(meet(X1,X0))) = meet(complement(X1),X0),
inference(backward_demodulation,[],[f40931,f41267]) ).
fof(f41386,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(complement(meet(X1,X2)),meet(join(X0,meet(X1,X2)),join(X2,meet(X1,join(X0,meet(X1,X2)))))))) = meet(X1,join(X2,meet(X1,meet(complement(meet(X1,X2)),X0)))),
inference(backward_demodulation,[],[f35374,f41267]) ).
fof(f41388,plain,
! [X2,X0,X1] : join(X2,X0) = join(X2,meet(complement(meet(X1,X2)),X0)),
inference(backward_demodulation,[],[f35230,f41267]) ).
fof(f41544,plain,
! [X2,X0,X1] : join(complement(X1),join(meet(X0,X1),X2)) = join(X0,join(complement(X1),join(meet(X0,X1),X2))),
inference(forward_demodulation,[],[f41332,f8]) ).
fof(f41557,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(join(complement(X1),meet(X0,X1)),meet(join(X0,X1),X2))) = meet(join(X0,X1),join(complement(X1),join(meet(X0,X1),meet(X2,join(complement(X1),join(meet(X0,X1),meet(join(X0,X1),join(X0,X2)))))))),
inference(forward_demodulation,[],[f41345,f8]) ).
fof(f41562,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,join(complement(X1),X0)),
inference(backward_demodulation,[],[f26084,f41355]) ).
fof(f41563,plain,
! [X0,X1] : join(complement(X1),meet(X0,X1)) = join(X0,complement(X1)),
inference(forward_demodulation,[],[f41356,f458]) ).
fof(f41596,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(join(X0,meet(X1,X2)),join(X2,meet(X1,join(X0,meet(X1,X2))))))) = meet(X1,join(X2,meet(X1,meet(complement(meet(X1,X2)),X0)))),
inference(forward_demodulation,[],[f41386,f41388]) ).
fof(f41606,plain,
! [X2,X0,X1] : meet(X0,meet(complement(meet(X0,X1)),X2)) = meet(X2,meet(complement(X1),X0)),
inference(backward_demodulation,[],[f22321,f41384]) ).
fof(f41617,plain,
! [X2,X0,X1] : meet(X2,meet(complement(X1),X0)) = meet(X0,meet(X2,complement(meet(X0,X1)))),
inference(backward_demodulation,[],[f22468,f41384]) ).
fof(f41629,plain,
! [X0,X1] : join(meet(X1,X0),meet(complement(X0),X1)) = X1,
inference(backward_demodulation,[],[f32390,f41384]) ).
fof(f41653,plain,
! [X0,X1] : meet(complement(X0),X1) = meet(complement(X0),join(X0,X1)),
inference(backward_demodulation,[],[f40932,f41384]) ).
fof(f41691,plain,
! [X2,X0,X1] : meet(complement(X0),join(X0,join(meet(complement(X0),X1),meet(X2,join(X0,meet(complement(X0),join(meet(complement(X0),X1),X2))))))) = meet(complement(X0),join(X2,join(X0,meet(complement(X0),X1)))),
inference(backward_demodulation,[],[f26632,f41371]) ).
fof(f41863,plain,
! [X2,X0,X1] : join(complement(X1),join(meet(X0,X1),X2)) = join(X0,join(X2,complement(X1))),
inference(forward_demodulation,[],[f41544,f2073]) ).
fof(f41870,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(complement(X1),join(meet(X0,X1),meet(join(X0,X1),X2)))) = meet(join(X0,X1),join(complement(X1),join(meet(X0,X1),meet(X2,join(complement(X1),join(meet(X0,X1),meet(join(X0,X1),join(X0,X2)))))))),
inference(forward_demodulation,[],[f41557,f8]) ).
fof(f41882,plain,
! [X0,X1] : join(complement(X1),meet(X1,X0)) = join(complement(X1),X0),
inference(backward_demodulation,[],[f37412,f41562]) ).
fof(f41918,plain,
! [X2,X0,X1] : meet(X0,join(complement(X0),join(meet(X0,X1),meet(X2,join(complement(X0),meet(X0,join(meet(X0,X1),X2))))))) = meet(join(meet(X0,X1),meet(X0,X2)),X0),
inference(backward_demodulation,[],[f26119,f41562]) ).
fof(f41979,plain,
! [X0,X1] : meet(join(X1,X0),join(X1,complement(X0))) = X1,
inference(backward_demodulation,[],[f39589,f41563]) ).
fof(f42000,plain,
! [X2,X0,X1] : meet(X2,X0) = meet(X2,join(X0,complement(join(X1,X2)))),
inference(backward_demodulation,[],[f29249,f41563]) ).
fof(f42002,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X1),X2)) = meet(join(X0,X1),join(X0,join(X2,complement(join(X0,X1))))),
inference(backward_demodulation,[],[f26577,f41563]) ).
fof(f42045,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X1,join(X0,meet(X1,X2))))) = meet(X1,join(X2,meet(X1,meet(complement(meet(X1,X2)),X0)))),
inference(forward_demodulation,[],[f41596,f5422]) ).
fof(f42111,plain,
! [X0,X1] : join(X1,complement(join(X0,X1))) = join(meet(X0,X1),complement(X0)),
inference(backward_demodulation,[],[f41383,f41629]) ).
fof(f42130,plain,
! [X2,X0,X1] : join(X2,meet(X0,X1)) = join(X2,meet(X1,meet(complement(meet(X1,X2)),X0))),
inference(backward_demodulation,[],[f34902,f41617]) ).
fof(f42210,plain,
! [X2,X0,X1] : meet(complement(X0),join(X0,join(meet(complement(X0),X1),meet(X2,join(X0,meet(complement(X0),join(meet(complement(X0),X1),X2))))))) = meet(complement(X0),join(X2,join(X1,X0))),
inference(forward_demodulation,[],[f41691,f41366]) ).
fof(f42444,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(complement(X1),join(meet(X0,X1),meet(join(X0,X1),X2)))) = meet(join(X0,X1),join(X0,join(meet(X2,join(complement(X1),join(meet(X0,X1),meet(join(X0,X1),join(X0,X2))))),complement(X1)))),
inference(forward_demodulation,[],[f41870,f41863]) ).
fof(f42485,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),meet(X0,X2))) = meet(X0,join(complement(X0),join(meet(X0,X1),meet(X2,join(complement(X0),meet(X0,join(meet(X0,X1),X2))))))),
inference(forward_demodulation,[],[f41918,f5]) ).
fof(f42607,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X1,join(X0,meet(X1,X2))))) = meet(X1,join(X2,meet(X0,meet(complement(X2),X1)))),
inference(forward_demodulation,[],[f42045,f41606]) ).
fof(f42633,plain,
! [X0,X1] : join(X1,complement(join(X0,X1))) = join(complement(X0),meet(X0,X1)),
inference(forward_demodulation,[],[f42111,f6]) ).
fof(f42636,plain,
! [X2,X0,X1] : join(X2,meet(X0,X1)) = join(X2,meet(X0,meet(complement(X2),X1))),
inference(forward_demodulation,[],[f42130,f41606]) ).
fof(f42749,plain,
! [X2,X0,X1] : meet(complement(X0),join(X2,join(X1,X0))) = meet(complement(X0),join(meet(complement(X0),X1),meet(X2,join(X0,meet(complement(X0),join(meet(complement(X0),X1),X2)))))),
inference(forward_demodulation,[],[f42210,f41653]) ).
fof(f42914,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(complement(X1),join(meet(X0,X1),meet(join(X0,X1),X2)))) = meet(join(X0,X1),join(X0,join(complement(X1),meet(X2,join(complement(X1),join(meet(X0,X1),meet(join(X0,X1),join(X0,X2)))))))),
inference(forward_demodulation,[],[f42444,f6]) ).
fof(f42942,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),meet(X0,X2))) = meet(join(meet(X0,X1),meet(X2,join(complement(X0),meet(X0,join(meet(X0,X1),X2))))),X0),
inference(forward_demodulation,[],[f42485,f41562]) ).
fof(f43097,plain,
! [X0,X1] : join(X1,complement(join(X0,X1))) = join(complement(X0),X1),
inference(forward_demodulation,[],[f42633,f41882]) ).
fof(f43098,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X0,X1))) = meet(X1,join(X2,meet(X1,join(X0,meet(X1,X2))))),
inference(backward_demodulation,[],[f42607,f42636]) ).
fof(f43149,plain,
! [X2,X0,X1] : meet(complement(X0),join(X2,join(X1,X0))) = meet(complement(X0),join(meet(complement(X0),X1),meet(X2,join(join(meet(complement(X0),X1),X2),X0)))),
inference(forward_demodulation,[],[f42749,f41366]) ).
fof(f43287,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(complement(X1),join(meet(X0,X1),meet(join(X0,X1),X2)))) = meet(join(X0,X1),join(X0,join(complement(X1),meet(X2,join(X0,join(meet(join(X0,X1),join(X0,X2)),complement(X1))))))),
inference(forward_demodulation,[],[f42914,f41863]) ).
fof(f43300,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),meet(X0,X2))) = meet(X0,join(meet(X0,X1),meet(X2,join(complement(X0),meet(X0,join(meet(X0,X1),X2)))))),
inference(forward_demodulation,[],[f42942,f5]) ).
fof(f43483,plain,
! [X2,X0,X1] : meet(complement(X0),join(X2,join(X1,X0))) = meet(complement(X0),join(meet(complement(X0),X1),meet(X2,join(X0,join(meet(complement(X0),X1),X2))))),
inference(forward_demodulation,[],[f43149,f18914]) ).
fof(f43560,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(complement(X1),join(meet(X0,X1),meet(join(X0,X1),X2)))) = meet(join(X0,X1),join(X0,join(complement(X1),meet(X2,join(X0,join(complement(X1),meet(join(X0,X1),join(X0,X2)))))))),
inference(forward_demodulation,[],[f43287,f6]) ).
fof(f43565,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),meet(X0,X2))) = meet(X0,join(meet(X0,X1),meet(X2,join(complement(X0),join(meet(X0,X1),X2))))),
inference(forward_demodulation,[],[f43300,f41882]) ).
fof(f43690,plain,
! [X2,X0,X1] : meet(complement(X0),join(meet(complement(X0),X1),X2)) = meet(complement(X0),join(X2,join(X1,X0))),
inference(forward_demodulation,[],[f43483,f65]) ).
fof(f43738,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X0,join(complement(X1),meet(X2,join(X0,join(complement(X1),meet(join(X0,X1),join(X0,X2)))))))) = meet(join(X0,X1),join(X0,join(meet(join(X0,X1),X2),complement(X1)))),
inference(forward_demodulation,[],[f43560,f41863]) ).
fof(f43741,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = meet(X0,join(meet(X0,X1),meet(X0,X2))),
inference(forward_demodulation,[],[f43565,f65]) ).
fof(f43852,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X0,join(complement(X1),meet(X2,join(X0,join(complement(X1),meet(join(X0,X1),join(X0,X2)))))))) = meet(join(X0,X1),join(X0,join(complement(X1),meet(join(X0,X1),X2)))),
inference(forward_demodulation,[],[f43738,f17126]) ).
fof(f43854,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = join(meet(X0,X1),meet(X0,X2)),
inference(forward_demodulation,[],[f43741,f10685]) ).
fof(f43946,plain,
! [X2,X3,X0,X1] : join(X1,join(meet(X2,join(X1,join(meet(X0,X1),meet(X0,X2)))),X3)) = join(X1,join(meet(X0,join(X1,meet(X0,X2))),join(meet(X2,join(X1,join(meet(X0,X1),meet(X0,X2)))),X3))),
inference(backward_demodulation,[],[f5029,f43854]) ).
fof(f43959,plain,
! [X3,X0,X1] : meet(X1,join(X0,meet(X3,join(X0,meet(X1,join(X3,meet(X1,X0))))))) = join(meet(X1,X3),meet(X1,X0)),
inference(backward_demodulation,[],[f28226,f43854]) ).
fof(f43960,plain,
! [X2,X0,X1] : meet(X0,join(X1,join(complement(join(X1,X0)),meet(X0,X2)))) = meet(X0,join(X1,join(complement(join(X1,X0)),meet(X2,join(X1,join(complement(join(X1,X0)),join(meet(X0,X1),meet(X0,X2)))))))),
inference(backward_demodulation,[],[f30273,f43854]) ).
fof(f44000,plain,
! [X2,X3,X0,X1] : meet(X2,join(X0,join(X1,meet(X3,join(X0,join(X1,meet(X2,join(X3,meet(X2,join(X0,X1)))))))))) = join(meet(X2,X3),meet(X2,join(X0,X1))),
inference(backward_demodulation,[],[f35412,f43854]) ).
fof(f44003,plain,
! [X2,X0,X1] : join(meet(complement(X0),X1),meet(complement(X0),X2)) = meet(complement(X0),join(X2,join(X1,X0))),
inference(backward_demodulation,[],[f43690,f43854]) ).
fof(f44059,plain,
! [X2,X3,X0,X1] : meet(X3,join(X0,join(X1,meet(X3,X2)))) = join(meet(X3,X2),meet(X3,join(X0,X1))),
inference(backward_demodulation,[],[f210,f44000]) ).
fof(f44085,plain,
! [X2,X0,X1] : meet(X0,join(X1,join(complement(join(X1,X0)),meet(X0,X2)))) = meet(X0,join(X1,join(complement(join(X1,X0)),meet(X2,join(X1,join(meet(X0,X2),complement(join(X1,X0)))))))),
inference(forward_demodulation,[],[f43960,f2072]) ).
fof(f44086,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X0,X2))) = join(meet(X0,X2),meet(X0,X1)),
inference(backward_demodulation,[],[f12,f43959]) ).
fof(f44094,plain,
! [X2,X3,X0,X1] : join(X1,join(meet(X2,join(X1,meet(X0,X2))),X3)) = join(X1,join(meet(X0,join(X1,meet(X0,X2))),join(meet(X2,join(X1,meet(X0,X2))),X3))),
inference(forward_demodulation,[],[f43946,f54]) ).
fof(f44189,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X0,join(complement(X1),meet(X2,join(X0,join(complement(X1),meet(join(X0,X1),join(X0,X2)))))))) = join(meet(join(X0,X1),X2),meet(join(X0,X1),join(X0,complement(X1)))),
inference(backward_demodulation,[],[f43852,f44059]) ).
fof(f44226,plain,
! [X2,X0,X1] : meet(X0,join(X1,join(complement(join(X1,X0)),meet(X2,join(X1,join(meet(X0,X2),complement(join(X1,X0)))))))) = join(meet(X0,X2),meet(X0,join(X1,complement(join(X1,X0))))),
inference(forward_demodulation,[],[f44085,f44059]) ).
fof(f44272,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X0,X1))) = meet(X1,join(X2,join(meet(X1,X2),meet(X1,X0)))),
inference(backward_demodulation,[],[f43098,f44086]) ).
fof(f44402,plain,
! [X0] : meet(a,join(c,meet(X0,join(c,meet(a,join(X0,sF3)))))) = join(meet(a,X0),meet(a,c)),
inference(backward_demodulation,[],[f4259,f44086]) ).
fof(f44523,plain,
! [X2,X3,X0,X1] : join(X1,join(meet(X2,join(X1,meet(X0,X2))),X3)) = join(X1,join(join(meet(X0,X2),meet(X0,X1)),join(meet(X2,join(X1,meet(X0,X2))),X3))),
inference(forward_demodulation,[],[f44094,f44086]) ).
fof(f44574,plain,
! [X2,X0,X1] : join(meet(join(X0,X1),X2),X0) = meet(join(X0,X1),join(X0,join(complement(X1),meet(X2,join(X0,join(complement(X1),meet(join(X0,X1),join(X0,X2)))))))),
inference(forward_demodulation,[],[f44189,f41979]) ).
fof(f44626,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(X0,X1)) = meet(X0,join(X1,join(complement(join(X1,X0)),meet(X2,join(X1,join(meet(X0,X2),complement(join(X1,X0)))))))),
inference(forward_demodulation,[],[f44226,f42000]) ).
fof(f44741,plain,
! [X0] : meet(a,join(c,meet(X0,join(c,meet(a,join(X0,sF3)))))) = join(meet(a,X0),meet(c,a)),
inference(forward_demodulation,[],[f44402,f11880]) ).
fof(f44827,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X0,X1))) = join(meet(X1,X0),meet(X1,join(X2,meet(X1,X2)))),
inference(forward_demodulation,[],[f44272,f44059]) ).
fof(f44861,plain,
! [X2,X3,X0,X1] : join(X1,join(meet(X2,join(X1,meet(X0,X2))),X3)) = join(X1,join(meet(X0,X2),join(meet(X0,X1),join(meet(X2,join(X1,meet(X0,X2))),X3)))),
inference(forward_demodulation,[],[f44523,f8]) ).
fof(f44903,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X1),X2)) = meet(join(X0,X1),join(X0,join(complement(X1),meet(X2,join(X0,join(complement(X1),meet(join(X0,X1),join(X0,X2)))))))),
inference(forward_demodulation,[],[f44574,f6]) ).
fof(f45027,plain,
! [X0] : meet(a,join(c,meet(X0,join(c,meet(a,join(X0,sF3)))))) = join(meet(a,X0),sF3),
inference(forward_demodulation,[],[f44741,f26]) ).
fof(f45111,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X0,X1))) = join(meet(X1,X0),join(meet(X1,X2),meet(X1,X2))),
inference(forward_demodulation,[],[f44827,f44086]) ).
fof(f45139,plain,
! [X2,X3,X0,X1] : join(X1,join(meet(X2,join(X1,meet(X0,X2))),X3)) = join(X1,join(join(meet(X2,join(X1,meet(X0,X2))),X3),meet(X0,X2))),
inference(forward_demodulation,[],[f44861,f2072]) ).
fof(f45229,plain,
! [X0] : meet(a,join(c,meet(X0,join(c,meet(a,join(X0,sF3)))))) = join(sF3,meet(a,X0)),
inference(forward_demodulation,[],[f45027,f6]) ).
fof(f45287,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X0,X1))) = join(meet(X1,X0),meet(X1,X2)),
inference(forward_demodulation,[],[f45111,f2]) ).
fof(f45311,plain,
! [X2,X3,X0,X1] : join(X1,join(meet(X2,join(X1,meet(X0,X2))),X3)) = join(X1,join(meet(X0,X2),join(meet(X2,join(X1,meet(X0,X2))),X3))),
inference(forward_demodulation,[],[f45139,f6]) ).
fof(f45516,plain,
! [X2,X3,X0,X1] : join(X1,join(meet(X0,X2),X3)) = join(X1,join(meet(X2,join(X1,meet(X0,X2))),X3)),
inference(forward_demodulation,[],[f45311,f779]) ).
fof(f45674,plain,
! [X2,X3,X0,X1] : join(X1,join(meet(X0,X2),X3)) = join(X1,join(join(meet(X2,X0),meet(X2,X1)),X3)),
inference(forward_demodulation,[],[f45516,f45287]) ).
fof(f45766,plain,
! [X2,X3,X0,X1] : join(X1,join(meet(X0,X2),X3)) = join(X1,join(meet(X2,X0),join(meet(X2,X1),X3))),
inference(forward_demodulation,[],[f45674,f8]) ).
fof(f45833,plain,
! [X2,X3,X0,X1] : join(X1,join(meet(X0,X2),X3)) = join(X1,join(X3,meet(X2,X0))),
inference(forward_demodulation,[],[f45766,f2072]) ).
fof(f46084,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),meet(X0,X2))) = meet(join(X2,meet(X0,X1)),X0),
inference(superposition,[],[f295,f44086]) ).
fof(f46110,plain,
! [X2,X0,X1] : join(complement(join(X2,meet(complement(X0),X1))),X0) = complement(join(meet(complement(X0),X1),meet(complement(X0),X2))),
inference(superposition,[],[f36859,f44086]) ).
fof(f46126,plain,
! [X2,X0,X1] : join(complement(join(X2,meet(complement(X0),X1))),X0) = complement(meet(complement(X0),join(X2,join(X1,X0)))),
inference(forward_demodulation,[],[f46110,f44003]) ).
fof(f46149,plain,
! [X2,X0,X1] : meet(X0,join(X2,meet(X0,X1))) = meet(X0,join(meet(X0,X1),meet(X0,X2))),
inference(forward_demodulation,[],[f46084,f5]) ).
fof(f46347,plain,
! [X2,X0,X1] : join(complement(join(X2,meet(complement(X0),X1))),X0) = join(complement(join(X2,join(X1,X0))),X0),
inference(forward_demodulation,[],[f46126,f36859]) ).
fof(f46367,plain,
! [X2,X0,X1] : meet(X0,join(X2,meet(X0,X1))) = join(meet(X0,X2),meet(X0,meet(X0,X1))),
inference(forward_demodulation,[],[f46149,f44086]) ).
fof(f46526,plain,
! [X2,X0,X1] : join(complement(join(X2,meet(complement(X0),X1))),X0) = join(X0,complement(join(X2,join(X1,X0)))),
inference(forward_demodulation,[],[f46347,f6]) ).
fof(f46540,plain,
! [X2,X0,X1] : meet(X0,join(X2,meet(X0,X1))) = join(meet(X0,X2),meet(X0,X1)),
inference(forward_demodulation,[],[f46367,f52]) ).
fof(f46675,plain,
! [X2,X0,X1] : join(X0,complement(join(X2,join(X1,X0)))) = join(X0,complement(join(X2,meet(complement(X0),X1)))),
inference(forward_demodulation,[],[f46526,f6]) ).
fof(f47111,plain,
! [X2,X0,X1] : meet(join(X0,X1),X2) = meet(X2,join(X0,join(X1,complement(X2)))),
inference(superposition,[],[f41562,f67]) ).
fof(f47112,plain,
! [X2,X0,X1] : meet(join(X2,X0),X1) = meet(X1,join(X0,join(complement(X1),X2))),
inference(superposition,[],[f41562,f67]) ).
fof(f47244,plain,
! [X2,X0,X1] : meet(join(X0,X2),join(X0,X1)) = join(X0,meet(join(X0,X1),X2)),
inference(backward_demodulation,[],[f42002,f47111]) ).
fof(f47317,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X1),X2)) = meet(join(X0,X1),join(X0,join(complement(X1),meet(X2,join(X0,join(complement(X1),join(X0,meet(join(X0,X2),X1)))))))),
inference(backward_demodulation,[],[f44903,f47244]) ).
fof(f47331,plain,
! [X2,X3,X0,X1] : join(X3,X2) = join(X3,meet(join(X3,join(X0,join(X1,X2))),X2)),
inference(backward_demodulation,[],[f9070,f47244]) ).
fof(f47481,plain,
! [X2,X3,X0,X1] : join(X3,X2) = join(X3,meet(X2,join(X3,join(X0,join(X1,X2))))),
inference(forward_demodulation,[],[f47331,f11880]) ).
fof(f47494,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X1),X2)) = join(X0,meet(join(X0,join(complement(X1),meet(X2,join(X0,join(complement(X1),join(X0,meet(join(X0,X2),X1))))))),X1)),
inference(forward_demodulation,[],[f47317,f47244]) ).
fof(f47550,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X1),X2)) = join(X0,meet(X1,join(X0,join(complement(X1),meet(X2,join(X0,join(complement(X1),join(X0,meet(join(X0,X2),X1))))))))),
inference(forward_demodulation,[],[f47494,f11880]) ).
fof(f47584,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X1),X2)) = join(X0,meet(join(meet(X2,join(X0,join(complement(X1),join(X0,meet(join(X0,X2),X1))))),X0),X1)),
inference(forward_demodulation,[],[f47550,f47112]) ).
fof(f47605,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X1),X2)) = join(X0,meet(X1,join(meet(X2,join(X0,join(complement(X1),join(X0,meet(join(X0,X2),X1))))),X0))),
inference(forward_demodulation,[],[f47584,f11880]) ).
fof(f47619,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X1),X2)) = join(X0,meet(X1,join(X0,meet(X2,join(X0,join(complement(X1),join(X0,meet(join(X0,X2),X1)))))))),
inference(forward_demodulation,[],[f47605,f18914]) ).
fof(f47625,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X1),X2)) = join(X0,meet(X1,join(X0,meet(X2,join(X0,join(meet(join(X0,X2),X1),complement(X1))))))),
inference(forward_demodulation,[],[f47619,f810]) ).
fof(f47628,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X1),X2)) = join(X0,meet(X1,join(X0,meet(X2,join(X0,join(complement(X1),meet(X1,join(X0,X2)))))))),
inference(forward_demodulation,[],[f47625,f45833]) ).
fof(f47631,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X1),X2)) = join(X0,meet(X1,join(X0,meet(X2,join(X0,join(complement(X1),join(X0,X2))))))),
inference(forward_demodulation,[],[f47628,f41882]) ).
fof(f47633,plain,
! [X2,X0,X1] : join(X0,meet(X1,join(X0,X2))) = join(X0,meet(join(X0,X1),X2)),
inference(forward_demodulation,[],[f47631,f47481]) ).
fof(f47658,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X2,X0)) = join(X0,meet(X1,join(X0,join(X2,X0)))),
inference(backward_demodulation,[],[f9302,f47633]) ).
fof(f47747,plain,
! [X2,X0,X1] : join(X0,meet(X1,join(X2,X0))) = meet(join(X0,X1),join(X2,X0)),
inference(forward_demodulation,[],[f47658,f50]) ).
fof(f47799,plain,
! [X2,X0,X1] : join(complement(join(X0,X1)),X2) = join(X2,meet(complement(X1),join(complement(join(X0,X1)),X2))),
inference(backward_demodulation,[],[f35766,f47747]) ).
fof(f47854,plain,
! [X2,X0,X1] : join(complement(join(X0,X1)),X2) = join(X2,complement(join(meet(complement(X2),join(X0,X1)),X1))),
inference(forward_demodulation,[],[f47799,f38898]) ).
fof(f47889,plain,
! [X2,X0,X1] : join(complement(join(X0,X1)),X2) = join(X2,complement(join(X1,meet(complement(X2),join(X0,X1))))),
inference(forward_demodulation,[],[f47854,f39991]) ).
fof(f47924,plain,
! [X2,X0,X1] : join(complement(join(X0,X1)),X2) = join(X2,complement(join(X1,join(join(X0,X1),X2)))),
inference(forward_demodulation,[],[f47889,f46675]) ).
fof(f47950,plain,
! [X2,X0,X1] : join(complement(join(X0,X1)),X2) = join(X2,complement(join(X1,join(X0,join(X1,X2))))),
inference(forward_demodulation,[],[f47924,f8]) ).
fof(f47971,plain,
! [X2,X0,X1] : join(complement(join(X0,X1)),X2) = join(X2,complement(join(X1,join(X2,X0)))),
inference(forward_demodulation,[],[f47950,f810]) ).
fof(f47989,plain,
! [X2,X0,X1] : meet(X2,join(X1,X0)) = meet(X2,join(X0,join(complement(join(X0,X2)),X1))),
inference(backward_demodulation,[],[f30788,f47971]) ).
fof(f48012,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(X0,X1)) = meet(X0,join(meet(X2,join(X1,join(meet(X0,X2),complement(join(X1,X0))))),X1)),
inference(backward_demodulation,[],[f44626,f47989]) ).
fof(f48022,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(X0,X1)) = meet(X0,join(X1,meet(X2,join(X1,join(meet(X0,X2),complement(join(X1,X0))))))),
inference(forward_demodulation,[],[f48012,f16827]) ).
fof(f49061,plain,
! [X2,X0,X1] : join(join(complement(X0),X1),X2) = join(meet(X0,X1),join(complement(X0),X2)),
inference(superposition,[],[f56,f41882]) ).
fof(f49086,plain,
! [X2,X0,X1] : join(join(complement(X0),X1),X2) = join(complement(X0),join(X2,meet(X0,X1))),
inference(forward_demodulation,[],[f49061,f67]) ).
fof(f49146,plain,
! [X2,X0,X1] : join(complement(X0),join(X1,X2)) = join(complement(X0),join(X2,meet(X0,X1))),
inference(forward_demodulation,[],[f49086,f8]) ).
fof(f50815,plain,
! [X2,X0,X1] : join(join(X1,meet(X0,X2)),complement(join(X0,X1))) = join(complement(X0),join(X1,meet(X0,X2))),
inference(superposition,[],[f43097,f458]) ).
fof(f51027,plain,
! [X2,X0,X1] : join(join(X1,meet(X0,X2)),complement(join(X0,X1))) = join(complement(X0),join(X2,X1)),
inference(forward_demodulation,[],[f50815,f49146]) ).
fof(f51101,plain,
! [X2,X0,X1] : join(complement(X0),join(X2,X1)) = join(complement(join(X1,X0)),join(X1,meet(X0,X2))),
inference(forward_demodulation,[],[f51027,f39993]) ).
fof(f51165,plain,
! [X2,X0,X1] : join(X1,join(meet(X0,X2),complement(join(X1,X0)))) = join(complement(X0),join(X2,X1)),
inference(forward_demodulation,[],[f51101,f67]) ).
fof(f51204,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(X0,X1)) = meet(X0,join(X1,meet(X2,join(complement(X0),join(X2,X1))))),
inference(backward_demodulation,[],[f48022,f51165]) ).
fof(f51229,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = join(meet(X0,X2),meet(X0,X1)),
inference(forward_demodulation,[],[f51204,f153]) ).
fof(f51253,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X0,X2))) = meet(X0,join(X1,X2)),
inference(backward_demodulation,[],[f44086,f51229]) ).
fof(f51286,plain,
! [X2,X0,X1] : meet(X0,join(X2,meet(X0,X1))) = meet(X0,join(X1,X2)),
inference(backward_demodulation,[],[f46540,f51229]) ).
fof(f52029,plain,
! [X2,X3,X0,X1] : meet(X0,join(X2,meet(X0,X1))) = meet(X0,join(X2,meet(X1,join(X0,X3)))),
inference(superposition,[],[f51253,f141]) ).
fof(f52043,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X0,X1))) = meet(X1,join(X2,join(complement(X1),X0))),
inference(superposition,[],[f51253,f41562]) ).
fof(f52246,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X0,X1))) = meet(join(X0,X2),X1),
inference(forward_demodulation,[],[f52043,f47112]) ).
fof(f52260,plain,
! [X2,X3,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,join(X2,meet(X1,join(X0,X3)))),
inference(forward_demodulation,[],[f52029,f51286]) ).
fof(f52415,plain,
! [X0] : join(sF3,meet(a,X0)) = meet(a,join(c,meet(X0,join(a,c)))),
inference(backward_demodulation,[],[f45229,f52260]) ).
fof(f52556,plain,
! [X0] : meet(a,join(X0,c)) = join(sF3,meet(a,X0)),
inference(forward_demodulation,[],[f52415,f52260]) ).
fof(f56234,plain,
! [X0] : meet(a,join(X0,sF2)) = meet(join(b,X0),a),
inference(superposition,[],[f52246,f25]) ).
fof(f56434,plain,
! [X0] : meet(a,join(b,X0)) = meet(a,join(X0,sF2)),
inference(forward_demodulation,[],[f56234,f5]) ).
fof(f67935,plain,
join(sF3,sF2) = meet(a,join(sF2,c)),
inference(superposition,[],[f52556,f1499]) ).
fof(f68132,plain,
join(sF3,sF2) = meet(a,join(c,sF2)),
inference(forward_demodulation,[],[f67935,f16827]) ).
fof(f68210,plain,
meet(a,join(b,c)) = join(sF3,sF2),
inference(forward_demodulation,[],[f68132,f56434]) ).
fof(f68260,plain,
meet(a,join(b,c)) = join(sF2,sF3),
inference(forward_demodulation,[],[f68210,f6]) ).
fof(f68295,plain,
meet(a,join(b,c)) = sF4,
inference(forward_demodulation,[],[f68260,f23]) ).
fof(f68318,plain,
meet(a,sF0) = sF4,
inference(forward_demodulation,[],[f68295,f15]) ).
fof(f68326,plain,
sF1 = sF4,
inference(forward_demodulation,[],[f68318,f17]) ).
fof(f68332,plain,
$false,
inference(forward_subsumption_resolution,[],[f68326,f24]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT180-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.09 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.20/0.47 % Computer : n019.cluster.edu
% 0.20/0.47 % Model : x86_64 x86_64
% 0.20/0.47 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.47 % Memory : 8046.5625MB
% 0.20/0.47 % OS : Linux 6.8.0-71-generic
% 0.20/0.47 % CPULimit : 300
% 0.20/0.47 % WCLimit : 300
% 0.20/0.47 % DateTime : Sun Sep 27 14:04:48 UTC 2026
% 0.20/0.47 % CPUTime :
% 0.20/0.47 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.25/0.53 Running first-order theorem proving
% 0.25/0.53 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
% 18.79/3.89 % (3119623)Input is clausal, will run a generic CNF schedule.
% 18.79/3.89 % (3119634)dis-21_1_sil=8000:lcm=predicate:random_seed=3624076591:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 18.79/3.89 % (3119634)Refutation not found, incomplete strategy
% 18.79/3.89 % (3119634)------------------------------
% 18.79/3.89 % (3119634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.79/3.89 % (3119634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.79/3.89 % (3119634)CaDiCaL version: 2.1.3
% 18.79/3.89 % (3119634)Termination reason: Refutation not found, incomplete strategy
% 18.79/3.89 % (3119634)Time elapsed: 0.002 s
% 18.79/3.89 % (3119634)Peak memory usage: 88 MB
% 18.79/3.89 % (3119634)Instructions burned: 1 (million)
% 18.79/3.89 % (3119633)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3809827122:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 18.79/3.89 % (3119631)lrs+10_1_sil=8000:sp=occurrence:random_seed=4274439115:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 18.79/3.89 % (3119629)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2987593812:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 18.79/3.89 % (3119630)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=787570591:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 18.79/3.89 % (3119628)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=2662596454:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 18.79/3.89 % (3119632)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=177265518:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 18.79/3.89 % (3119631)Instruction limit reached!
% 18.79/3.89 % (3119631)------------------------------
% 18.79/3.89 % (3119631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.79/3.89 % (3119631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.79/3.89 % (3119631)CaDiCaL version: 2.1.3
% 18.79/3.89 % (3119631)Termination reason: Instruction limit
% 18.79/3.89 % (3119631)Termination phase: Saturation
% 18.79/3.89 % (3119631)Time elapsed: 0.102 s
% 18.79/3.89 % (3119631)Peak memory usage: 89 MB
% 18.79/3.89 % (3119631)Instructions burned: 107 (million)
% 18.79/3.89 % (3119632)Instruction limit reached!
% 18.79/3.89 % (3119632)------------------------------
% 18.79/3.89 % (3119632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.79/3.89 % (3119632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.79/3.89 % (3119632)CaDiCaL version: 2.1.3
% 18.79/3.89 % (3119632)Termination reason: Instruction limit
% 18.79/3.89 % (3119632)Termination phase: Saturation
% 18.79/3.89 % (3119632)Time elapsed: 0.112 s
% 18.79/3.89 % (3119632)Peak memory usage: 89 MB
% 18.79/3.89 % (3119632)Instructions burned: 114 (million)
% 18.79/3.89 % (3119633)Instruction limit reached!
% 18.79/3.89 % (3119633)------------------------------
% 18.79/3.89 % (3119633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.79/3.89 % (3119633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.79/3.89 % (3119633)CaDiCaL version: 2.1.3
% 18.79/3.89 % (3119633)Termination reason: Instruction limit
% 18.79/3.89 % (3119633)Termination phase: Saturation
% 18.79/3.89 % (3119633)Time elapsed: 0.168 s
% 18.79/3.89 % (3119633)Peak memory usage: 89 MB
% 18.79/3.89 % (3119633)Instructions burned: 181 (million)
% 18.79/3.89 % (3119634)------------------------------
% 18.79/3.89 % (3119634)------------------------------
% 18.79/3.89 % (3119642)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=1895713761:i=143:sd=2:aac=none:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/143Mi)
% 18.79/3.89 % (3119642)Refutation not found, incomplete strategy
% 18.79/3.89 % (3119642)------------------------------
% 18.79/3.89 % (3119642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.79/3.89 % (3119642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.79/3.89 % (3119642)CaDiCaL version: 2.1.3
% 18.79/3.89 % (3119642)Termination reason: Refutation not found, incomplete strategy
% 18.79/3.89 % (3119642)Time elapsed: 0.001 s
% 18.79/3.89 % (3119642)Peak memory usage: 88 MB
% 39.70/6.71 % (3119643)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2926128290:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2995 on theBenchmark for (2995ds/189Mi)
% 39.70/6.71 % (3119643)Refutation not found, incomplete strategy
% 39.70/6.71 % (3119643)------------------------------
% 39.70/6.71 % (3119643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.70/6.71 % (3119643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.70/6.71 % (3119643)CaDiCaL version: 2.1.3
% 39.70/6.71 % (3119643)Termination reason: Refutation not found, incomplete strategy
% 39.70/6.71 % (3119643)Time elapsed: 0.003 s
% 39.70/6.71 % (3119643)Peak memory usage: 88 MB
% 39.70/6.71 % (3119643)Instructions burned: 1 (million)
% 39.70/6.71 % (3119644)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1750305920:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 39.70/6.71 % (3119644)Refutation not found, incomplete strategy
% 39.70/6.71 % (3119644)------------------------------
% 39.70/6.71 % (3119644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.70/6.71 % (3119644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.70/6.71 % (3119644)CaDiCaL version: 2.1.3
% 39.70/6.71 % (3119644)Termination reason: Refutation not found, incomplete strategy
% 39.70/6.71 % (3119644)Time elapsed: 0.002 s
% 39.70/6.71 % (3119644)Peak memory usage: 88 MB
% 39.70/6.71 % (3119645)lrs+10_64_to=lpo:sil=8000:random_seed=631191254:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 39.70/6.71 % (3119645)Instruction limit reached!
% 39.70/6.71 % (3119645)------------------------------
% 39.70/6.71 % (3119645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.70/6.71 % (3119645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.70/6.71 % (3119645)CaDiCaL version: 2.1.3
% 39.70/6.71 % (3119645)Termination reason: Instruction limit
% 39.70/6.71 % (3119645)Termination phase: Saturation
% 39.70/6.71 % (3119645)Time elapsed: 0.118 s
% 39.70/6.71 % (3119645)Peak memory usage: 88 MB
% 39.70/6.71 % (3119645)Instructions burned: 126 (million)
% 39.70/6.71 % (3119642)------------------------------
% 39.70/6.71 % (3119642)------------------------------
% 39.70/6.71 % (3119643)------------------------------
% 39.70/6.71 % (3119643)------------------------------
% 39.70/6.71 % (3119651)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1085066979:i=157:gtg=all_2991 on theBenchmark for (2991ds/157Mi)
% 39.70/6.71 % (3119644)------------------------------
% 39.70/6.71 % (3119644)------------------------------
% 39.70/6.71 % (3119650)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3772548758:avsq=on:i=194:fgj=on:bd=preordered_2991 on theBenchmark for (2991ds/194Mi)
% 39.70/6.71 % (3119651)Instruction limit reached!
% 39.70/6.71 % (3119651)------------------------------
% 39.70/6.71 % (3119651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.70/6.71 % (3119651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.70/6.71 % (3119651)CaDiCaL version: 2.1.3
% 39.70/6.71 % (3119651)Termination reason: Instruction limit
% 39.70/6.71 % (3119651)Termination phase: Saturation
% 39.70/6.71 % (3119651)Time elapsed: 0.159 s
% 39.70/6.71 % (3119651)Peak memory usage: 90 MB
% 39.70/6.71 % (3119651)Instructions burned: 157 (million)
% 39.70/6.71 % (3119652)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1615804380:i=3394:sd=4:ss=included:sgt=64_2989 on theBenchmark for (2989ds/3394Mi)
% 39.70/6.71 % (3119650)Instruction limit reached!
% 39.70/6.71 % (3119650)------------------------------
% 39.70/6.71 % (3119650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.70/6.71 % (3119650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.70/6.71 % (3119650)CaDiCaL version: 2.1.3
% 39.70/6.71 % (3119650)Termination reason: Instruction limit
% 39.70/6.71 % (3119650)Termination phase: Saturation
% 39.70/6.71 % (3119650)Time elapsed: 0.194 s
% 39.70/6.71 % (3119650)Peak memory usage: 90 MB
% 39.70/6.71 % (3119650)Instructions burned: 194 (million)
% 39.70/6.71 % (3119654)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=2845994458:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2988 on theBenchmark for (2988ds/106Mi)
% 39.70/6.71 % (3119654)Instruction limit reached!
% 39.70/6.71 % (3119654)------------------------------
% 21.83/6.81 % (3119654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.83/6.81 % (3119654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.83/6.81 % (3119654)CaDiCaL version: 2.1.3
% 21.83/6.81 % (3119654)Termination reason: Instruction limit
% 21.83/6.81 % (3119654)Termination phase: Saturation
% 21.83/6.81 % (3119654)Time elapsed: 0.110 s
% 21.83/6.81 % (3119654)Peak memory usage: 89 MB
% 21.83/6.81 % (3119654)Instructions burned: 106 (million)
% 21.83/6.81 % (3119669)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=276708531:i=107_2987 on theBenchmark for (2987ds/107Mi)
% 21.83/6.81 % (3119669)Refutation not found, incomplete strategy
% 21.83/6.81 % (3119669)------------------------------
% 21.83/6.81 % (3119669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.83/6.81 % (3119669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.83/6.81 % (3119669)CaDiCaL version: 2.1.3
% 21.83/6.81 % (3119669)Termination reason: Refutation not found, incomplete strategy
% 21.83/6.81 % (3119669)Time elapsed: 0.002 s
% 21.83/6.81 % (3119669)Peak memory usage: 87 MB
% 21.83/6.81 % (3119675)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=73233198:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2986 on theBenchmark for (2986ds/242Mi)
% 21.83/6.81 % (3119677)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=587421732:cond=fast:i=5208:av=off_2984 on theBenchmark for (2984ds/5208Mi)
% 21.83/6.81 % (3119675)Instruction limit reached!
% 21.83/6.81 % (3119675)------------------------------
% 21.83/6.81 % (3119675)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.83/6.81 % (3119675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.83/6.81 % (3119675)CaDiCaL version: 2.1.3
% 21.83/6.81 % (3119675)Termination reason: Instruction limit
% 21.83/6.81 % (3119675)Termination phase: Saturation
% 21.83/6.81 % (3119675)Time elapsed: 0.251 s
% 21.83/6.81 % (3119675)Peak memory usage: 90 MB
% 21.83/6.81 % (3119675)Instructions burned: 242 (million)
% 21.83/6.81 % (3119669)------------------------------
% 21.83/6.81 % (3119669)------------------------------
% 21.83/6.81 % (3119681)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2599273667:i=134:sd=2:doe=on:ss=axioms:sgt=14_2980 on theBenchmark for (2980ds/134Mi)
% 21.83/6.81 % (3119682)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2697860326:i=499:bd=all_2979 on theBenchmark for (2979ds/499Mi)
% 21.83/6.81 % (3119681)Instruction limit reached!
% 21.83/6.81 % (3119681)------------------------------
% 21.83/6.81 % (3119681)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.83/6.81 % (3119681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.83/6.81 % (3119681)CaDiCaL version: 2.1.3
% 21.83/6.81 % (3119681)Termination reason: Instruction limit
% 21.83/6.81 % (3119681)Termination phase: Saturation
% 21.83/6.81 % (3119681)Time elapsed: 0.133 s
% 21.83/6.81 % (3119681)Peak memory usage: 89 MB
% 21.83/6.81 % (3119681)Instructions burned: 134 (million)
% 21.83/6.81 % (3119685)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1611622254:i=191:fgj=on:bd=all_2976 on theBenchmark for (2976ds/191Mi)
% 21.83/6.81 % (3119685)Instruction limit reached!
% 21.83/6.81 % (3119685)------------------------------
% 21.83/6.81 % (3119685)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.83/6.81 % (3119685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.83/6.81 % (3119685)CaDiCaL version: 2.1.3
% 21.83/6.81 % (3119685)Termination reason: Instruction limit
% 21.83/6.81 % (3119685)Termination phase: Saturation
% 21.83/6.81 % (3119685)Time elapsed: 0.210 s
% 21.83/6.81 % (3119685)Peak memory usage: 91 MB
% 21.83/6.81 % (3119685)Instructions burned: 191 (million)
% 21.83/6.81 % (3119682)Instruction limit reached!
% 21.83/6.81 % (3119682)------------------------------
% 21.83/6.81 % (3119682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.83/6.81 % (3119682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.83/6.81 % (3119682)CaDiCaL version: 2.1.3
% 21.83/6.81 % (3119682)Termination reason: Instruction limit
% 21.83/6.81 % (3119682)Termination phase: Saturation
% 21.83/6.81 % (3119682)Time elapsed: 0.499 s
% 21.83/6.81 % (3119682)Peak memory usage: 94 MB
% 21.83/6.81 % (3119682)Instructions burned: 500 (million)
% 21.83/6.81 % (3119687)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=682353168:i=264:kws=precedence:fsr=off_2971 on theBenchmark for (2971ds/264Mi)
% 21.83/6.81 % (3119688)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2647871806:cond=on:i=156:bs=on:gtg=exists_all:er=known_2971 on theBenchmark for (2971ds/156Mi)
% 21.83/6.81 % (3119688)Instruction limit reached!
% 21.83/6.81 % (3119688)------------------------------
% 21.83/6.81 % (3119688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.83/6.81 % (3119688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.83/6.81 % (3119688)CaDiCaL version: 2.1.3
% 21.83/6.81 % (3119688)Termination reason: Instruction limit
% 21.83/6.81 % (3119688)Termination phase: Saturation
% 21.83/6.81 % (3119688)Time elapsed: 0.155 s
% 21.83/6.81 % (3119688)Peak memory usage: 89 MB
% 21.83/6.81 % (3119688)Instructions burned: 157 (million)
% 21.83/6.81 % (3119687)Instruction limit reached!
% 21.83/6.81 % (3119687)------------------------------
% 21.83/6.81 % (3119687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.83/6.81 % (3119687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.83/6.81 % (3119687)CaDiCaL version: 2.1.3
% 21.83/6.81 % (3119687)Termination reason: Instruction limit
% 21.83/6.81 % (3119687)Termination phase: Saturation
% 21.83/6.81 % (3119687)Time elapsed: 0.261 s
% 21.83/6.81 % (3119687)Peak memory usage: 92 MB
% 21.83/6.81 % (3119687)Instructions burned: 264 (million)
% 21.83/6.81 % (3119691)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=1233581938:i=3256:kws=precedence:bd=preordered:av=off_2967 on theBenchmark for (2967ds/3256Mi)
% 21.83/6.81 % (3119692)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=342377199:i=537:av=off:ss=included_2966 on theBenchmark for (2966ds/537Mi)
% 21.83/6.81 % (3119692)Instruction limit reached!
% 21.83/6.81 % (3119692)------------------------------
% 21.83/6.81 % (3119692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.83/6.81 % (3119692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.83/6.81 % (3119692)CaDiCaL version: 2.1.3
% 21.83/6.81 % (3119692)Termination reason: Instruction limit
% 21.83/6.81 % (3119692)Termination phase: Saturation
% 21.83/6.81 % (3119692)Time elapsed: 0.506 s
% 21.83/6.81 % (3119692)Peak memory usage: 93 MB
% 21.83/6.81 % (3119692)Instructions burned: 537 (million)
% 21.83/6.81 % (3119697)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1432674229:i=180:bd=preordered:av=off_2957 on theBenchmark for (2957ds/180Mi)
% 21.83/6.81 % (3119697)Instruction limit reached!
% 21.83/6.81 % (3119697)------------------------------
% 21.83/6.81 % (3119697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.83/6.81 % (3119697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.83/6.81 % (3119697)CaDiCaL version: 2.1.3
% 21.83/6.81 % (3119697)Termination reason: Instruction limit
% 21.83/6.81 % (3119697)Termination phase: Saturation
% 21.83/6.81 % (3119697)Time elapsed: 0.180 s
% 21.83/6.81 % (3119697)Peak memory usage: 88 MB
% 21.83/6.81 % (3119697)Instructions burned: 181 (million)
% 21.83/6.81 % (3119652)Instruction limit reached!
% 21.83/6.81 % (3119652)------------------------------
% 21.83/6.81 % (3119652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.83/6.81 % (3119652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.83/6.81 % (3119652)CaDiCaL version: 2.1.3
% 21.83/6.81 % (3119652)Termination reason: Instruction limit
% 21.83/6.81 % (3119652)Termination phase: Saturation
% 21.83/6.81 % (3119652)Time elapsed: 3.582 s
% 21.83/6.81 % (3119652)Peak memory usage: 150 MB
% 21.83/6.81 % (3119652)Instructions burned: 3394 (million)
% 21.83/6.81 % (3119699)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=3453602966:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2952 on theBenchmark for (2952ds/10307Mi)
% 21.83/6.81 % (3119700)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=1091309170:i=412:gtgl=4:gtg=exists_all_2950 on theBenchmark for (2950ds/412Mi)
% 21.83/6.81 % (3119630)First to succeed.
% 21.83/6.81 % (3119630)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3119623"
% 21.83/6.81 % (3119700)Instruction limit reached!
% 21.83/6.81 % (3119700)------------------------------
% 21.83/6.81 % (3119700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.83/6.81 % (3119700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.83/6.81 % (3119700)CaDiCaL version: 2.1.3
% 21.83/6.81 % (3119700)Termination reason: Instruction limit
% 21.83/6.81 % (3119700)Termination phase: Saturation
% 21.83/6.81 % (3119700)Time elapsed: 0.409 s
% 21.83/6.81 % (3119700)Peak memory usage: 94 MB
% 21.83/6.81 % (3119700)Instructions burned: 412 (million)
% 21.83/6.81 % (3119630)Refutation found. Thanks to Tanya!
% 21.83/6.81 % SZS status Unsatisfiable for theBenchmark
% 21.83/6.81 % SZS output start Proof for theBenchmark
% See solution above
% 0.29/7.16 % (3119630)------------------------------
% 0.29/7.16 % (3119630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.29/7.16 % (3119630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/7.16 % (3119630)CaDiCaL version: 2.1.3
% 0.29/7.16 % (3119630)Termination reason: Refutation
% 0.29/7.16 % (3119630)Time elapsed: 5.183 s
% 0.29/7.16 % (3119630)Peak memory usage: 184 MB
% 0.29/7.16 % (3119630)Instructions burned: 8246 (million)
% 0.29/7.16 % (3119630)------------------------------
% 0.29/7.16 % (3119630)------------------------------
% 0.29/7.16 % (3119623)Success in time 5.751 s
% 0.29/7.16 % Vampire exiting
%------------------------------------------------------------------------------