%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT192-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 : n017.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:12 AM UTC 2026
% Result : Unsatisfiable 70.05s 12.69s
% Output : Refutation 82.95s
% Verified :
% SZS Type : Refutation
% Derivation depth : 77
% Number of leaves : 18
% Syntax : Number of formulae : 533 ( 480 unt; 7 def)
% Number of atoms : 594 ( 574 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 124 ( 63 ~; 59 |; 0 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 13 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 3 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 10 con; 0-2 aty)
% Number of variables : 995 ( 0 sgn 995 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
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] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(X1,join(X2,meet(X0,X1))),meet(X2,join(X0,X1)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',equation_H22) ).
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(f33,plain,
! [X2,X0,X1] : join(meet(X0,meet(X0,X1)),meet(X0,X2)) = meet(X0,join(meet(meet(X0,X1),join(X2,meet(X0,meet(X0,X1)))),meet(X2,X0))),
inference(superposition,[],[f12,f4]) ).
fof(f35,plain,
! [X2,X0,X1] : join(meet(meet(X1,join(X2,meet(X0,X1))),meet(X2,join(X0,X1))),meet(meet(X1,join(X2,meet(X0,X1))),X0)) = meet(meet(X1,join(X2,meet(X0,X1))),join(meet(meet(X2,join(X0,X1)),join(X0,meet(meet(X1,join(X2,meet(X0,X1))),meet(X2,join(X0,X1))))),join(meet(X0,X1),meet(X0,X2)))),
inference(superposition,[],[f12,f12]) ).
fof(f37,plain,
! [X2,X0,X1] : join(meet(meet(X1,join(X2,meet(X0,X1))),meet(X2,join(X0,X1))),meet(meet(X1,join(X2,meet(X0,X1))),X0)) = meet(X1,meet(join(X2,meet(X0,X1)),join(meet(meet(X2,join(X0,X1)),join(X0,meet(meet(X1,join(X2,meet(X0,X1))),meet(X2,join(X0,X1))))),join(meet(X0,X1),meet(X0,X2))))),
inference(forward_demodulation,[],[f35,f7]) ).
fof(f39,plain,
! [X2,X0,X1] : join(meet(X0,meet(X0,X1)),meet(X0,X2)) = meet(X0,join(meet(X2,X0),meet(meet(X0,X1),join(X2,meet(X0,meet(X0,X1)))))),
inference(forward_demodulation,[],[f33,f6]) ).
fof(f44,plain,
! [X2,X0,X1] : join(meet(meet(X1,join(X2,meet(X0,X1))),meet(X2,join(X0,X1))),meet(meet(X1,join(X2,meet(X0,X1))),X0)) = meet(X1,meet(join(X2,meet(X0,X1)),join(join(meet(X0,X1),meet(X0,X2)),meet(meet(X2,join(X0,X1)),join(X0,meet(meet(X1,join(X2,meet(X0,X1))),meet(X2,join(X0,X1)))))))),
inference(forward_demodulation,[],[f37,f6]) ).
fof(f46,plain,
! [X2,X0,X1] : join(meet(X0,meet(X0,X1)),meet(X0,X2)) = meet(X0,join(meet(X2,X0),meet(X0,meet(X1,join(X2,meet(X0,meet(X0,X1))))))),
inference(forward_demodulation,[],[f39,f7]) ).
fof(f49,plain,
! [X2,X0,X1] : join(meet(meet(X1,join(X2,meet(X0,X1))),meet(X2,join(X0,X1))),meet(meet(X1,join(X2,meet(X0,X1))),X0)) = meet(X1,meet(join(X2,meet(X0,X1)),join(meet(X0,X1),join(meet(X0,X2),meet(meet(X2,join(X0,X1)),join(X0,meet(meet(X1,join(X2,meet(X0,X1))),meet(X2,join(X0,X1))))))))),
inference(forward_demodulation,[],[f44,f8]) ).
fof(f53,plain,
! [X2,X0,X1] : join(meet(meet(X1,join(X2,meet(X0,X1))),meet(X2,join(X0,X1))),meet(meet(X1,join(X2,meet(X0,X1))),X0)) = meet(X1,meet(join(X2,meet(X0,X1)),join(meet(X0,X1),join(meet(X0,X2),meet(X2,meet(join(X0,X1),join(X0,meet(meet(X1,join(X2,meet(X0,X1))),meet(X2,join(X0,X1)))))))))),
inference(forward_demodulation,[],[f49,f7]) ).
fof(f56,plain,
! [X2,X0,X1] : join(meet(meet(X2,join(X0,X1)),meet(X1,join(X2,meet(X0,X1)))),meet(meet(X1,join(X2,meet(X0,X1))),X0)) = meet(X1,meet(join(X2,meet(X0,X1)),join(meet(X0,X1),join(meet(X0,X2),meet(X2,meet(join(X0,X1),join(X0,meet(meet(X2,join(X0,X1)),meet(X1,join(X2,meet(X0,X1))))))))))),
inference(forward_demodulation,[],[f53,f5]) ).
fof(f58,plain,
! [X2,X0,X1] : join(meet(X2,meet(join(X0,X1),meet(X1,join(X2,meet(X0,X1))))),meet(meet(X1,join(X2,meet(X0,X1))),X0)) = meet(X1,meet(join(X2,meet(X0,X1)),join(meet(X0,X1),join(meet(X0,X2),meet(X2,meet(join(X0,X1),join(X0,meet(X2,meet(join(X0,X1),meet(X1,join(X2,meet(X0,X1)))))))))))),
inference(forward_demodulation,[],[f56,f7]) ).
fof(f59,plain,
! [X2,X0,X1] : meet(X1,meet(join(X2,meet(X0,X1)),join(meet(X0,X1),join(meet(X0,X2),meet(X2,meet(join(X0,X1),join(X0,meet(X2,meet(join(X0,X1),meet(X1,join(X2,meet(X0,X1)))))))))))) = join(meet(meet(X1,join(X2,meet(X0,X1))),X0),meet(X2,meet(join(X0,X1),meet(X1,join(X2,meet(X0,X1)))))),
inference(forward_demodulation,[],[f58,f6]) ).
fof(f60,plain,
! [X2,X0,X1] : meet(X1,meet(join(X2,meet(X0,X1)),join(meet(X0,X1),join(meet(X0,X2),meet(X2,meet(join(X0,X1),join(X0,meet(X2,meet(join(X0,X1),meet(X1,join(X2,meet(X0,X1)))))))))))) = join(meet(X0,meet(X1,join(X2,meet(X0,X1)))),meet(X2,meet(join(X0,X1),meet(X1,join(X2,meet(X0,X1)))))),
inference(forward_demodulation,[],[f59,f5]) ).
fof(f62,plain,
b = join(b,sF2),
inference(superposition,[],[f4,f25]) ).
fof(f65,plain,
c = join(c,sF3),
inference(superposition,[],[f4,f26]) ).
fof(f70,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X1,X2)) = meet(X1,join(meet(X0,join(X2,meet(X0,X1))),meet(X2,join(X1,X0)))),
inference(superposition,[],[f12,f5]) ).
fof(f71,plain,
! [X0,X1] : join(X1,meet(X0,X1)) = X1,
inference(superposition,[],[f4,f5]) ).
fof(f74,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X1,X2)) = meet(X1,join(meet(X2,join(X1,X0)),meet(X0,join(X2,meet(X0,X1))))),
inference(forward_demodulation,[],[f70,f6]) ).
fof(f81,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(X1,join(meet(X0,X1),X2)),meet(X2,join(X0,X1)))),
inference(superposition,[],[f12,f6]) ).
fof(f83,plain,
! [X0,X1] : meet(X1,join(X0,X1)) = X1,
inference(superposition,[],[f3,f6]) ).
fof(f86,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(X2,join(X0,X1)),meet(X1,join(meet(X0,X1),X2)))),
inference(forward_demodulation,[],[f81,f6]) ).
fof(f89,plain,
! [X0,X1] : join(X0,X1) = join(join(X0,X1),X0),
inference(superposition,[],[f71,f3]) ).
fof(f92,plain,
a = join(a,sF3),
inference(superposition,[],[f71,f26]) ).
fof(f96,plain,
! [X2,X0,X1] : join(meet(X0,meet(X1,X0)),meet(X0,X2)) = meet(X0,join(meet(meet(X1,X0),join(X2,meet(X0,meet(X1,X0)))),meet(X2,X0))),
inference(superposition,[],[f12,f71]) ).
fof(f98,plain,
! [X2,X0,X1] : join(meet(X0,meet(X1,X0)),meet(X0,X2)) = meet(X0,join(meet(X2,X0),meet(meet(X1,X0),join(X2,meet(X0,meet(X1,X0)))))),
inference(forward_demodulation,[],[f96,f6]) ).
fof(f101,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X0,X1)),
inference(forward_demodulation,[],[f89,f6]) ).
fof(f102,plain,
! [X2,X0,X1] : join(meet(X0,meet(X1,X0)),meet(X0,X2)) = meet(X0,join(meet(X2,X0),meet(X1,meet(X0,join(X2,meet(X0,meet(X1,X0))))))),
inference(forward_demodulation,[],[f98,f7]) ).
fof(f112,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X0,X1),X2)),
inference(superposition,[],[f8,f4]) ).
fof(f113,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X1,X0),X2)),
inference(superposition,[],[f8,f71]) ).
fof(f116,plain,
! [X0] : join(b,join(c,X0)) = join(sF0,X0),
inference(superposition,[],[f8,f15]) ).
fof(f122,plain,
! [X2,X0,X1] : join(X0,X1) = join(X0,join(X1,meet(join(X0,X1),X2))),
inference(superposition,[],[f4,f8]) ).
fof(f124,plain,
! [X2,X0,X1] : join(X0,X1) = join(X0,join(X1,meet(X2,join(X0,X1)))),
inference(superposition,[],[f71,f8]) ).
fof(f126,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f6,f8]) ).
fof(f134,plain,
! [X0,X1] : meet(X0,X1) = meet(meet(X0,X1),X0),
inference(superposition,[],[f83,f4]) ).
fof(f135,plain,
! [X0,X1] : meet(X1,X0) = meet(meet(X1,X0),X0),
inference(superposition,[],[f83,f71]) ).
fof(f147,plain,
! [X0,X1] : meet(X1,X0) = meet(X0,meet(X1,X0)),
inference(forward_demodulation,[],[f135,f5]) ).
fof(f148,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X0,X1)),
inference(forward_demodulation,[],[f134,f5]) ).
fof(f151,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X0,X2)) = meet(X0,join(meet(X2,X0),meet(X1,meet(X0,join(X2,meet(X1,X0)))))),
inference(backward_demodulation,[],[f102,f147]) ).
fof(f152,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(X2,X0),meet(X0,meet(X1,join(X2,meet(X0,X1)))))),
inference(backward_demodulation,[],[f46,f148]) ).
fof(f161,plain,
! [X0,X1] :
( join(X0,X1) != one
| meet(X1,X0) != zero
| complement(X1) = X0 ),
inference(superposition,[],[f11,f6]) ).
fof(f180,plain,
! [X0] : join(sF2,join(sF3,X0)) = join(sF4,X0),
inference(superposition,[],[f8,f23]) ).
fof(f183,plain,
sF3 = meet(sF3,sF4),
inference(superposition,[],[f83,f23]) ).
fof(f201,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X0,X1),X2)),
inference(superposition,[],[f7,f3]) ).
fof(f203,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X1,X0),X2)),
inference(superposition,[],[f7,f83]) ).
fof(f204,plain,
! [X0] : meet(sF2,X0) = meet(b,meet(a,X0)),
inference(superposition,[],[f7,f25]) ).
fof(f205,plain,
! [X0] : meet(c,meet(a,X0)) = meet(sF3,X0),
inference(superposition,[],[f7,f26]) ).
fof(f214,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X2,meet(X0,X1)),
inference(superposition,[],[f5,f7]) ).
fof(f220,plain,
! [X2,X0,X1] : meet(X0,X1) = meet(X0,meet(X1,join(X2,meet(X0,X1)))),
inference(superposition,[],[f83,f7]) ).
fof(f223,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(X2,X0),meet(X0,X1))),
inference(backward_demodulation,[],[f152,f220]) ).
fof(f224,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X0,X2)) = meet(X0,join(meet(X2,X0),meet(X1,X0))),
inference(backward_demodulation,[],[f151,f220]) ).
fof(f225,plain,
! [X2,X0,X1] : meet(X1,meet(join(X2,meet(X0,X1)),join(meet(X0,X1),join(meet(X0,X2),meet(X2,meet(join(X0,X1),join(X0,meet(X2,meet(join(X0,X1),meet(X1,join(X2,meet(X0,X1)))))))))))) = join(meet(X0,X1),meet(X2,meet(join(X0,X1),meet(X1,join(X2,meet(X0,X1)))))),
inference(backward_demodulation,[],[f60,f220]) ).
fof(f233,plain,
! [X2,X0,X1] : meet(X1,meet(join(X2,meet(X0,X1)),join(meet(X0,X1),join(meet(X0,X2),meet(X2,meet(join(X0,X1),join(X0,meet(X2,meet(X1,meet(join(X2,meet(X0,X1)),join(X0,X1))))))))))) = join(meet(X0,X1),meet(X2,meet(X1,meet(join(X2,meet(X0,X1)),join(X0,X1))))),
inference(forward_demodulation,[],[f225,f214]) ).
fof(f238,plain,
! [X2,X0,X1] : meet(X1,meet(join(X2,meet(X0,X1)),join(meet(X0,X1),join(meet(X0,X2),meet(X2,meet(join(X0,X1),join(X0,meet(X2,meet(X1,meet(join(X0,X1),join(X2,meet(X0,X1)))))))))))) = join(meet(X0,X1),meet(X2,meet(X1,meet(join(X0,X1),join(X2,meet(X0,X1)))))),
inference(forward_demodulation,[],[f233,f5]) ).
fof(f241,plain,
! [X2,X0,X1] : meet(X1,meet(join(X2,meet(X0,X1)),join(meet(X0,X1),join(meet(X0,X2),meet(X2,meet(join(X0,X1),join(X0,meet(X2,meet(X1,join(X2,meet(X0,X1))))))))))) = join(meet(X0,X1),meet(X2,meet(X1,join(X2,meet(X0,X1))))),
inference(forward_demodulation,[],[f238,f203]) ).
fof(f254,plain,
! [X2,X0,X1] : join(X1,X0) = join(X1,join(X0,meet(X1,X2))),
inference(superposition,[],[f112,f6]) ).
fof(f261,plain,
! [X2,X0,X1] : join(meet(X0,X2),X1) = meet(join(meet(X0,X2),X1),join(X0,X1)),
inference(superposition,[],[f83,f112]) ).
fof(f264,plain,
! [X2,X0,X1] : join(meet(X0,X2),X1) = meet(join(X0,X1),join(meet(X0,X2),X1)),
inference(forward_demodulation,[],[f261,f5]) ).
fof(f277,plain,
! [X0] : meet(X0,one) = X0,
inference(superposition,[],[f3,f9]) ).
fof(f279,plain,
! [X0,X1] : join(meet(X0,complement(X0)),meet(X0,X1)) = meet(X0,join(meet(complement(X0),join(X1,meet(X0,complement(X0)))),meet(X1,one))),
inference(superposition,[],[f12,f9]) ).
fof(f281,plain,
! [X0,X1] : join(X0,complement(meet(X0,X1))) = join(X0,one),
inference(superposition,[],[f112,f9]) ).
fof(f282,plain,
! [X0,X1] : one = join(X0,join(X1,complement(join(X0,X1)))),
inference(superposition,[],[f8,f9]) ).
fof(f284,plain,
! [X0,X1] : join(meet(X0,complement(X0)),meet(X0,X1)) = meet(X0,join(meet(X1,one),meet(complement(X0),join(X1,meet(X0,complement(X0)))))),
inference(forward_demodulation,[],[f279,f6]) ).
fof(f285,plain,
! [X0,X1] : join(zero,meet(X0,X1)) = meet(X0,join(meet(X1,one),meet(complement(X0),join(X1,zero)))),
inference(forward_demodulation,[],[f284,f10]) ).
fof(f286,plain,
! [X0,X1] : join(zero,meet(X0,X1)) = meet(X0,join(X1,meet(complement(X0),join(X1,zero)))),
inference(forward_demodulation,[],[f285,f277]) ).
fof(f292,plain,
! [X0] : meet(one,X0) = X0,
inference(superposition,[],[f5,f277]) ).
fof(f318,plain,
! [X0] : one = join(X0,one),
inference(superposition,[],[f83,f292]) ).
fof(f321,plain,
! [X0,X1] : one = join(X0,complement(meet(X0,X1))),
inference(backward_demodulation,[],[f281,f318]) ).
fof(f399,plain,
! [X0,X1] : one = join(X1,complement(meet(X0,X1))),
inference(superposition,[],[f321,f5]) ).
fof(f412,plain,
! [X2,X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(X0,X2)) = meet(X0,join(meet(complement(meet(X0,X1)),join(X2,meet(X0,complement(meet(X0,X1))))),meet(X2,one))),
inference(superposition,[],[f12,f321]) ).
fof(f418,plain,
! [X2,X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(X0,X2)) = meet(X0,join(meet(X2,one),meet(complement(meet(X0,X1)),join(X2,meet(X0,complement(meet(X0,X1))))))),
inference(forward_demodulation,[],[f412,f6]) ).
fof(f421,plain,
! [X2,X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(X0,X2)) = meet(X0,join(X2,meet(complement(meet(X0,X1)),join(X2,meet(X0,complement(meet(X0,X1))))))),
inference(forward_demodulation,[],[f418,f277]) ).
fof(f424,plain,
! [X0] : join(X0,zero) = X0,
inference(superposition,[],[f4,f10]) ).
fof(f430,plain,
! [X0,X1] : zero = meet(X0,meet(X1,complement(meet(X0,X1)))),
inference(superposition,[],[f7,f10]) ).
fof(f435,plain,
! [X0,X1] : join(zero,meet(X0,X1)) = meet(X0,join(X1,meet(complement(X0),X1))),
inference(backward_demodulation,[],[f286,f424]) ).
fof(f437,plain,
! [X0,X1] : meet(X0,X1) = join(zero,meet(X0,X1)),
inference(forward_demodulation,[],[f435,f71]) ).
fof(f449,plain,
! [X0] : join(zero,X0) = X0,
inference(superposition,[],[f437,f277]) ).
fof(f455,plain,
! [X0] : zero = meet(zero,X0),
inference(superposition,[],[f4,f437]) ).
fof(f457,plain,
! [X0] : zero = meet(X0,zero),
inference(superposition,[],[f71,f437]) ).
fof(f495,plain,
one = complement(zero),
inference(superposition,[],[f9,f449]) ).
fof(f521,plain,
! [X0,X1] : join(meet(X0,zero),meet(X0,X1)) = meet(X0,join(meet(zero,join(X1,meet(X0,zero))),meet(X1,X0))),
inference(superposition,[],[f12,f424]) ).
fof(f526,plain,
! [X0,X1] : join(meet(X0,zero),meet(X0,X1)) = meet(X0,join(meet(X1,X0),meet(zero,join(X1,meet(X0,zero))))),
inference(forward_demodulation,[],[f521,f6]) ).
fof(f528,plain,
! [X0,X1] : join(meet(X0,zero),meet(X0,X1)) = meet(X0,join(meet(X1,X0),zero)),
inference(forward_demodulation,[],[f526,f455]) ).
fof(f529,plain,
! [X0,X1] : join(meet(X0,zero),meet(X0,X1)) = meet(X0,join(zero,meet(X1,X0))),
inference(forward_demodulation,[],[f528,f6]) ).
fof(f530,plain,
! [X0,X1] : meet(X0,meet(X1,X0)) = join(meet(X0,zero),meet(X0,X1)),
inference(forward_demodulation,[],[f529,f449]) ).
fof(f531,plain,
! [X0,X1] : meet(X0,meet(X1,X0)) = join(zero,meet(X0,X1)),
inference(forward_demodulation,[],[f530,f457]) ).
fof(f532,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X1,X0)),
inference(forward_demodulation,[],[f531,f449]) ).
fof(f540,plain,
meet(a,b) = meet(a,sF2),
inference(superposition,[],[f532,f25]) ).
fof(f542,plain,
meet(sF0,a) = meet(sF0,sF1),
inference(superposition,[],[f532,f17]) ).
fof(f546,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(meet(X1,X0),X2)),
inference(superposition,[],[f7,f532]) ).
fof(f555,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X1,meet(X0,X2))),
inference(forward_demodulation,[],[f546,f7]) ).
fof(f557,plain,
meet(a,sF0) = meet(sF0,sF1),
inference(forward_demodulation,[],[f542,f5]) ).
fof(f559,plain,
meet(b,a) = meet(a,sF2),
inference(forward_demodulation,[],[f540,f5]) ).
fof(f566,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X0,meet(X1,meet(X0,X2))),
inference(forward_demodulation,[],[f555,f7]) ).
fof(f568,plain,
sF1 = meet(sF0,sF1),
inference(forward_demodulation,[],[f557,f17]) ).
fof(f570,plain,
sF2 = meet(a,sF2),
inference(forward_demodulation,[],[f559,f25]) ).
fof(f591,plain,
! [X0] : meet(b,X0) = meet(b,meet(sF0,X0)),
inference(superposition,[],[f201,f15]) ).
fof(f594,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(X1,meet(X0,join(X1,X2))),
inference(superposition,[],[f201,f5]) ).
fof(f612,plain,
! [X2,X0,X1] : meet(meet(join(X0,X2),X1),X0) = meet(meet(join(X0,X2),X1),meet(X0,X1)),
inference(superposition,[],[f532,f201]) ).
fof(f616,plain,
! [X2,X0,X1] : meet(meet(join(X0,X2),X1),X0) = meet(meet(X0,X1),meet(join(X0,X2),X1)),
inference(forward_demodulation,[],[f612,f5]) ).
fof(f630,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,X1)) = meet(X1,meet(join(X2,meet(X0,X1)),join(meet(X0,X1),join(meet(X0,X2),meet(X2,meet(join(X0,X1),join(X0,meet(X2,X1)))))))),
inference(backward_demodulation,[],[f241,f594]) ).
fof(f632,plain,
! [X2,X0,X1] : meet(meet(join(X0,X2),X1),X0) = meet(X1,meet(meet(X0,X1),join(X0,X2))),
inference(forward_demodulation,[],[f616,f214]) ).
fof(f638,plain,
! [X2,X0,X1] : meet(meet(join(X0,X2),X1),X0) = meet(X1,meet(X0,meet(X1,join(X0,X2)))),
inference(forward_demodulation,[],[f632,f7]) ).
fof(f639,plain,
! [X2,X0,X1] : meet(meet(join(X0,X2),X1),X0) = meet(X1,meet(X0,join(X0,X2))),
inference(forward_demodulation,[],[f638,f566]) ).
fof(f640,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(meet(join(X0,X2),X1),X0),
inference(forward_demodulation,[],[f639,f3]) ).
fof(f641,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(X0,meet(join(X0,X2),X1)),
inference(forward_demodulation,[],[f640,f5]) ).
fof(f646,plain,
! [X0] : join(a,X0) = join(a,join(sF2,X0)),
inference(superposition,[],[f112,f570]) ).
fof(f772,plain,
! [X0,X1] : zero = meet(X1,meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f430,f5]) ).
fof(f930,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,f282]) ).
fof(f937,plain,
! [X0,X1] :
( zero != meet(X0,join(X1,complement(join(X0,X1))))
| complement(X0) = join(X1,complement(join(X0,X1))) ),
inference(trivial_inequality_removal,[],[f930]) ).
fof(f966,plain,
! [X2,X0,X1] : join(meet(X1,X0),X2) = join(meet(X1,X0),join(meet(X0,X1),X2)),
inference(superposition,[],[f113,f532]) ).
fof(f982,plain,
! [X2,X0,X1] : join(X2,X0) = join(X2,join(X0,meet(X1,X2))),
inference(superposition,[],[f113,f6]) ).
fof(f1557,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(meet(X0,X1),meet(X0,X2)),
inference(superposition,[],[f203,f4]) ).
fof(f1574,plain,
! [X2,X0,X1] : meet(X2,X0) = meet(X2,meet(X0,join(X1,X2))),
inference(superposition,[],[f203,f5]) ).
fof(f1651,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X2,meet(X0,X1))),
inference(forward_demodulation,[],[f1557,f214]) ).
fof(f1668,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X2,X1)),
inference(forward_demodulation,[],[f1651,f566]) ).
fof(f1933,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,complement(meet(X0,X1)))) = meet(X0,join(meet(complement(meet(X0,X1)),join(X0,X1)),meet(X1,one))),
inference(superposition,[],[f86,f9]) ).
fof(f1991,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,complement(meet(X0,X1)))) = meet(X0,join(meet(X1,one),meet(complement(meet(X0,X1)),join(X0,X1)))),
inference(forward_demodulation,[],[f1933,f6]) ).
fof(f2064,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,complement(meet(X0,X1)))) = meet(X0,join(meet(X1,one),meet(join(X0,X1),complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f1991,f5]) ).
fof(f2120,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,complement(meet(X0,X1)))) = meet(X0,join(X1,meet(join(X0,X1),complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f2064,f277]) ).
fof(f2254,plain,
! [X0,X1] : join(meet(X0,meet(X1,X0)),meet(X0,complement(meet(X0,meet(X1,X0))))) = meet(X0,join(meet(X1,X0),meet(X0,complement(meet(X0,meet(X1,X0)))))),
inference(superposition,[],[f2120,f71]) ).
fof(f2260,plain,
! [X0,X1] : join(meet(X0,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,[],[f2120,f321]) ).
fof(f2261,plain,
! [X0,X1] : join(meet(X0,complement(meet(X1,X0))),meet(X0,complement(meet(X0,complement(meet(X1,X0)))))) = meet(X0,join(complement(meet(X1,X0)),meet(one,complement(meet(X0,complement(meet(X1,X0))))))),
inference(superposition,[],[f2120,f399]) ).
fof(f2388,plain,
! [X0,X1] : join(meet(X0,complement(meet(X1,X0))),meet(X0,complement(meet(X0,complement(meet(X1,X0)))))) = meet(X0,join(complement(meet(X1,X0)),complement(meet(X0,complement(meet(X1,X0)))))),
inference(forward_demodulation,[],[f2261,f292]) ).
fof(f2389,plain,
! [X0,X1] : join(meet(X0,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,[],[f2260,f292]) ).
fof(f2395,plain,
! [X0,X1] : join(meet(X0,meet(X1,X0)),meet(X0,complement(meet(X0,meet(X1,X0))))) = join(meet(X0,complement(meet(X0,meet(X1,X0)))),meet(X0,X1)),
inference(forward_demodulation,[],[f2254,f223]) ).
fof(f2438,plain,
! [X0,X1] : meet(X0,one) = join(meet(X0,complement(meet(X1,X0))),meet(X0,complement(meet(X0,complement(meet(X1,X0)))))),
inference(forward_demodulation,[],[f2388,f399]) ).
fof(f2439,plain,
! [X0,X1] : meet(X0,one) = join(meet(X0,complement(meet(X0,X1))),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f2389,f399]) ).
fof(f2443,plain,
! [X0,X1] : join(meet(X0,meet(X1,X0)),meet(X0,complement(meet(X0,meet(X1,X0))))) = join(meet(X0,X1),meet(X0,complement(meet(X0,meet(X1,X0))))),
inference(forward_demodulation,[],[f2395,f6]) ).
fof(f2468,plain,
! [X0,X1] : join(meet(X0,complement(meet(X1,X0))),meet(X0,complement(meet(X0,complement(meet(X1,X0)))))) = X0,
inference(forward_demodulation,[],[f2438,f277]) ).
fof(f2469,plain,
! [X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))) = X0,
inference(forward_demodulation,[],[f2439,f277]) ).
fof(f2473,plain,
! [X0,X1] : join(meet(X1,X0),meet(X0,complement(meet(X1,X0)))) = join(meet(X0,X1),meet(X0,complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f2443,f147]) ).
fof(f2671,plain,
meet(sF3,sF0) = meet(c,sF1),
inference(superposition,[],[f205,f17]) ).
fof(f2711,plain,
meet(c,sF1) = meet(sF0,sF3),
inference(forward_demodulation,[],[f2671,f5]) ).
fof(f2757,plain,
sF2 = meet(sF2,b),
inference(superposition,[],[f83,f62]) ).
fof(f2761,plain,
! [X0] : meet(sF2,X0) = meet(sF2,meet(b,X0)),
inference(superposition,[],[f203,f62]) ).
fof(f2767,plain,
! [X0] : meet(sF2,X0) = meet(b,meet(X0,sF2)),
inference(forward_demodulation,[],[f2761,f214]) ).
fof(f2768,plain,
sF2 = meet(b,sF2),
inference(forward_demodulation,[],[f2757,f5]) ).
fof(f2796,plain,
join(b,c) = join(sF0,sF3),
inference(superposition,[],[f116,f65]) ).
fof(f2818,plain,
sF0 = join(sF0,sF3),
inference(forward_demodulation,[],[f2796,f15]) ).
fof(f3263,plain,
! [X0] : meet(sF0,meet(sF3,X0)) = meet(X0,meet(c,sF1)),
inference(superposition,[],[f214,f2711]) ).
fof(f3615,plain,
! [X2,X3,X0,X1] : join(X3,join(X0,X1)) = join(X3,join(X0,join(X1,meet(X2,X3)))),
inference(superposition,[],[f113,f126]) ).
fof(f3741,plain,
meet(sF2,sF0) = meet(b,sF1),
inference(superposition,[],[f204,f17]) ).
fof(f3789,plain,
meet(b,sF1) = meet(sF0,sF2),
inference(forward_demodulation,[],[f3741,f5]) ).
fof(f3912,plain,
meet(sF2,sF0) = meet(sF2,meet(b,sF1)),
inference(superposition,[],[f532,f3789]) ).
fof(f3918,plain,
meet(sF2,sF0) = meet(sF1,meet(sF2,b)),
inference(forward_demodulation,[],[f3912,f214]) ).
fof(f3924,plain,
meet(sF2,sF0) = meet(b,meet(sF1,sF2)),
inference(forward_demodulation,[],[f3918,f214]) ).
fof(f3927,plain,
meet(sF2,sF0) = meet(sF2,sF1),
inference(forward_demodulation,[],[f3924,f2767]) ).
fof(f3929,plain,
meet(sF2,sF0) = meet(sF1,sF2),
inference(forward_demodulation,[],[f3927,f5]) ).
fof(f3930,plain,
meet(sF0,sF2) = meet(sF1,sF2),
inference(forward_demodulation,[],[f3929,f5]) ).
fof(f3931,plain,
meet(b,sF1) = meet(sF1,sF2),
inference(forward_demodulation,[],[f3930,f3789]) ).
fof(f4596,plain,
! [X0] : join(meet(c,sF1),meet(sF3,X0)) = meet(sF3,join(meet(X0,join(sF3,sF0)),meet(sF0,join(X0,meet(c,sF1))))),
inference(superposition,[],[f74,f2711]) ).
fof(f4689,plain,
! [X0] : join(meet(c,sF1),meet(sF3,X0)) = meet(sF3,join(meet(X0,join(sF0,sF3)),meet(sF0,join(X0,meet(c,sF1))))),
inference(forward_demodulation,[],[f4596,f6]) ).
fof(f4790,plain,
! [X0] : join(meet(c,sF1),meet(sF3,X0)) = meet(sF3,join(meet(X0,sF0),meet(sF0,join(X0,meet(c,sF1))))),
inference(forward_demodulation,[],[f4689,f2818]) ).
fof(f5870,plain,
! [X0,X1] : join(complement(meet(X0,X1)),X0) = join(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))),
inference(superposition,[],[f113,f2469]) ).
fof(f5923,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,[],[f5870,f6]) ).
fof(f5964,plain,
! [X0,X1] : one = join(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f5923,f321]) ).
fof(f6147,plain,
! [X0,X1] :
( one != one
| zero != meet(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1))))))
| meet(X0,complement(meet(X0,complement(meet(X0,X1))))) = complement(complement(meet(X0,X1))) ),
inference(superposition,[],[f11,f5964]) ).
fof(f6166,plain,
! [X0,X1] :
( zero != meet(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1))))))
| meet(X0,complement(meet(X0,complement(meet(X0,X1))))) = complement(complement(meet(X0,X1))) ),
inference(trivial_inequality_removal,[],[f6147]) ).
fof(f6183,plain,
! [X0,X1] : meet(X0,complement(meet(X0,complement(meet(X0,X1))))) = complement(complement(meet(X0,X1))),
inference(forward_subsumption_resolution,[],[f6166,f772]) ).
fof(f6226,plain,
! [X0,X1] : join(meet(X0,complement(meet(X0,X1))),complement(complement(meet(X0,X1)))) = X0,
inference(backward_demodulation,[],[f2469,f6183]) ).
fof(f6263,plain,
! [X0,X1] : join(complement(complement(meet(X0,X1))),meet(X0,complement(meet(X0,X1)))) = X0,
inference(forward_demodulation,[],[f6226,f6]) ).
fof(f6372,plain,
! [X0,X1] : meet(X1,complement(meet(X1,complement(meet(X0,X1))))) = complement(complement(meet(X0,X1))),
inference(superposition,[],[f6183,f5]) ).
fof(f6398,plain,
! [X0] : meet(X0,complement(meet(X0,complement(X0)))) = complement(complement(X0)),
inference(superposition,[],[f6183,f277]) ).
fof(f6496,plain,
! [X0] : meet(X0,complement(zero)) = complement(complement(X0)),
inference(forward_demodulation,[],[f6398,f10]) ).
fof(f6520,plain,
! [X0,X1] : join(meet(X0,complement(meet(X1,X0))),complement(complement(meet(X1,X0)))) = X0,
inference(backward_demodulation,[],[f2468,f6372]) ).
fof(f6553,plain,
! [X0] : meet(X0,one) = complement(complement(X0)),
inference(forward_demodulation,[],[f6496,f495]) ).
fof(f6570,plain,
! [X0,X1] : join(complement(complement(meet(X1,X0))),meet(X0,complement(meet(X1,X0)))) = X0,
inference(forward_demodulation,[],[f6520,f6]) ).
fof(f6584,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_demodulation,[],[f6553,f277]) ).
fof(f6600,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,complement(meet(X0,complement(meet(X0,X1))))),
inference(backward_demodulation,[],[f6183,f6584]) ).
fof(f6605,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,complement(meet(X0,X1)))) = X0,
inference(backward_demodulation,[],[f6263,f6584]) ).
fof(f6607,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,complement(meet(X1,complement(meet(X0,X1))))),
inference(backward_demodulation,[],[f6372,f6584]) ).
fof(f6622,plain,
! [X0,X1] : join(meet(X1,X0),meet(X0,complement(meet(X1,X0)))) = X0,
inference(backward_demodulation,[],[f6570,f6584]) ).
fof(f6694,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,complement(meet(X1,X0)))) = X0,
inference(backward_demodulation,[],[f2473,f6622]) ).
fof(f6697,plain,
! [X0,X1] : meet(X0,join(X1,meet(join(X0,X1),complement(meet(X0,X1))))) = X0,
inference(backward_demodulation,[],[f2120,f6605]) ).
fof(f6808,plain,
! [X0,X1] : join(X1,X0) = join(X1,meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f113,f6605]) ).
fof(f6826,plain,
! [X2,X0,X1] : join(X2,X0) = join(meet(X0,X1),join(meet(X0,complement(meet(X0,X1))),X2)),
inference(superposition,[],[f126,f6605]) ).
fof(f6833,plain,
! [X0,X1] :
( zero != meet(meet(X0,X1),join(meet(X0,complement(meet(X0,X1))),complement(X0)))
| complement(meet(X0,X1)) = join(meet(X0,complement(meet(X0,X1))),complement(X0)) ),
inference(superposition,[],[f937,f6605]) ).
fof(f6836,plain,
! [X0,X1] :
( zero != meet(X0,meet(X1,join(meet(X0,complement(meet(X0,X1))),complement(X0))))
| complement(meet(X0,X1)) = join(meet(X0,complement(meet(X0,X1))),complement(X0)) ),
inference(forward_demodulation,[],[f6833,f7]) ).
fof(f6889,plain,
! [X0,X1] :
( zero != meet(X0,meet(X1,join(complement(X0),meet(X0,complement(meet(X0,X1))))))
| complement(meet(X0,X1)) = join(meet(X0,complement(meet(X0,X1))),complement(X0)) ),
inference(forward_demodulation,[],[f6836,f6]) ).
fof(f6923,plain,
! [X0,X1] :
( complement(meet(X0,X1)) = join(complement(X0),meet(X0,complement(meet(X0,X1))))
| zero != meet(X0,meet(X1,join(complement(X0),meet(X0,complement(meet(X0,X1)))))) ),
inference(forward_demodulation,[],[f6889,f6]) ).
fof(f7048,plain,
! [X0,X1] : join(X1,X0) = join(X0,meet(join(X1,X0),complement(X0))),
inference(superposition,[],[f6622,f83]) ).
fof(f7064,plain,
sF3 = join(meet(c,sF1),meet(sF3,complement(meet(c,sF1)))),
inference(superposition,[],[f6622,f2711]) ).
fof(f7071,plain,
! [X0,X1] : join(X1,X0) = join(X1,meet(X0,complement(meet(X1,X0)))),
inference(superposition,[],[f112,f6622]) ).
fof(f7095,plain,
! [X0,X1] :
( zero != meet(meet(X1,X0),join(meet(X0,complement(meet(X1,X0))),complement(X0)))
| complement(meet(X1,X0)) = join(meet(X0,complement(meet(X1,X0))),complement(X0)) ),
inference(superposition,[],[f937,f6622]) ).
fof(f7098,plain,
! [X0,X1] :
( zero != meet(X1,meet(X0,join(meet(X0,complement(meet(X1,X0))),complement(X0))))
| complement(meet(X1,X0)) = join(meet(X0,complement(meet(X1,X0))),complement(X0)) ),
inference(forward_demodulation,[],[f7095,f7]) ).
fof(f7133,plain,
! [X0,X1] : join(X1,X0) = join(X0,meet(complement(X0),join(X1,X0))),
inference(forward_demodulation,[],[f7048,f5]) ).
fof(f7153,plain,
! [X0,X1] :
( zero != meet(X1,meet(X0,join(complement(X0),meet(X0,complement(meet(X1,X0))))))
| complement(meet(X1,X0)) = join(meet(X0,complement(meet(X1,X0))),complement(X0)) ),
inference(forward_demodulation,[],[f7098,f6]) ).
fof(f7190,plain,
! [X0,X1] :
( complement(meet(X1,X0)) = join(complement(X0),meet(X0,complement(meet(X1,X0))))
| zero != meet(X1,meet(X0,join(complement(X0),meet(X0,complement(meet(X1,X0)))))) ),
inference(forward_demodulation,[],[f7153,f6]) ).
fof(f7683,plain,
! [X0,X1] : join(meet(X1,X0),X0) = join(meet(X1,X0),meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f6808,f532]) ).
fof(f7728,plain,
! [X0,X1] : join(meet(X1,complement(meet(X1,X0))),meet(complement(meet(X1,X0)),X0)) = meet(complement(meet(X1,X0)),join(meet(X0,join(complement(meet(X1,X0)),X1)),meet(X1,join(X0,X1)))),
inference(superposition,[],[f74,f6808]) ).
fof(f7783,plain,
! [X0,X1] : join(meet(X1,complement(meet(X1,X0))),meet(complement(meet(X1,X0)),X0)) = meet(complement(meet(X1,X0)),join(meet(X1,join(X0,X1)),meet(X0,join(complement(meet(X1,X0)),X1)))),
inference(forward_demodulation,[],[f7728,f6]) ).
fof(f7823,plain,
! [X0,X1] : join(X0,meet(X1,X0)) = join(meet(X1,X0),meet(X0,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f7683,f6]) ).
fof(f7844,plain,
! [X0,X1] : join(meet(X1,complement(meet(X1,X0))),meet(complement(meet(X1,X0)),X0)) = meet(complement(meet(X1,X0)),join(meet(X1,join(X0,X1)),meet(X0,join(X1,complement(meet(X1,X0)))))),
inference(forward_demodulation,[],[f7783,f6]) ).
fof(f7870,plain,
! [X0,X1] : join(meet(X1,X0),meet(X0,complement(meet(X0,X1)))) = X0,
inference(forward_demodulation,[],[f7823,f71]) ).
fof(f7885,plain,
! [X0,X1] : join(meet(X1,complement(meet(X1,X0))),meet(complement(meet(X1,X0)),X0)) = meet(complement(meet(X1,X0)),join(meet(X1,join(X0,X1)),meet(X0,one))),
inference(forward_demodulation,[],[f7844,f321]) ).
fof(f7910,plain,
! [X0,X1] : join(meet(X1,complement(meet(X1,X0))),meet(complement(meet(X1,X0)),X0)) = meet(complement(meet(X1,X0)),join(meet(X0,one),meet(X1,join(X0,X1)))),
inference(forward_demodulation,[],[f7885,f6]) ).
fof(f7919,plain,
! [X0,X1] : join(meet(X1,complement(meet(X1,X0))),meet(complement(meet(X1,X0)),X0)) = meet(complement(meet(X1,X0)),join(meet(X0,one),X1)),
inference(forward_demodulation,[],[f7910,f83]) ).
fof(f7924,plain,
! [X0,X1] : meet(complement(meet(X1,X0)),join(X0,X1)) = join(meet(X1,complement(meet(X1,X0))),meet(complement(meet(X1,X0)),X0)),
inference(forward_demodulation,[],[f7919,f277]) ).
fof(f7927,plain,
! [X0,X1] : meet(complement(meet(X1,X0)),join(X0,X1)) = join(meet(X1,complement(meet(X1,X0))),meet(X0,complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f7924,f5]) ).
fof(f7929,plain,
! [X0,X1] : meet(join(X0,X1),complement(meet(X1,X0))) = join(meet(X1,complement(meet(X1,X0))),meet(X0,complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f7927,f5]) ).
fof(f8205,plain,
! [X0,X1] : join(X1,meet(join(X0,X1),complement(meet(X0,X1)))) = join(join(X1,meet(join(X0,X1),complement(meet(X0,X1)))),X0),
inference(superposition,[],[f71,f6697]) ).
fof(f8255,plain,
! [X0,X1] : join(X1,meet(join(X0,X1),complement(meet(X0,X1)))) = join(X0,join(X1,meet(join(X0,X1),complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f8205,f6]) ).
fof(f8343,plain,
! [X0,X1] : join(X0,X1) = join(X1,meet(join(X0,X1),complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f8255,f122]) ).
fof(f8636,plain,
! [X2,X0,X1] : join(X2,X0) = join(meet(X0,X1),join(meet(X0,complement(meet(X1,X0))),X2)),
inference(superposition,[],[f126,f6694]) ).
fof(f9055,plain,
! [X0,X1] : join(X1,X0) = join(X0,meet(join(X1,X0),complement(meet(X0,X1)))),
inference(superposition,[],[f8343,f5]) ).
fof(f9381,plain,
! [X0,X1] : join(X1,complement(X0)) = join(complement(X0),meet(X0,join(X1,complement(X0)))),
inference(superposition,[],[f7133,f6584]) ).
fof(f9448,plain,
! [X2,X0,X1] : join(meet(X1,X2),meet(X1,meet(complement(meet(X1,X2)),join(X0,meet(X1,X2))))) = meet(X1,join(meet(meet(complement(meet(X1,X2)),join(X0,meet(X1,X2))),join(X1,X2)),meet(X2,join(X0,meet(X1,X2))))),
inference(superposition,[],[f86,f7133]) ).
fof(f9459,plain,
! [X2,X0,X1] : join(meet(X1,X2),meet(X1,meet(complement(meet(X1,X2)),join(X0,meet(X1,X2))))) = meet(X1,join(meet(X2,join(X0,meet(X1,X2))),meet(meet(complement(meet(X1,X2)),join(X0,meet(X1,X2))),join(X1,X2)))),
inference(forward_demodulation,[],[f9448,f6]) ).
fof(f9510,plain,
! [X2,X0,X1] : join(meet(X1,X2),meet(X1,meet(complement(meet(X1,X2)),join(X0,meet(X1,X2))))) = meet(X1,join(meet(X2,join(X0,meet(X1,X2))),meet(join(X1,X2),meet(complement(meet(X1,X2)),join(X0,meet(X1,X2)))))),
inference(forward_demodulation,[],[f9459,f5]) ).
fof(f9610,plain,
! [X0,X1] : meet(join(X0,X1),complement(meet(join(X0,X1),complement(X0)))) = X0,
inference(superposition,[],[f6607,f3]) ).
fof(f9735,plain,
! [X0,X1] : meet(join(X0,X1),complement(meet(complement(X0),join(X0,X1)))) = X0,
inference(forward_demodulation,[],[f9610,f5]) ).
fof(f10174,plain,
! [X2,X0,X1] : meet(meet(X1,join(X2,meet(X0,X1))),X0) = meet(meet(X1,join(X2,meet(X0,X1))),join(meet(X0,X1),meet(X0,X2))),
inference(superposition,[],[f594,f12]) ).
fof(f10202,plain,
! [X2,X0,X1] : meet(X1,join(X0,X2)) = join(meet(X1,join(X0,X2)),meet(X0,X1)),
inference(superposition,[],[f71,f594]) ).
fof(f10267,plain,
! [X2,X0,X1] : meet(X1,join(X0,X2)) = join(meet(X0,X1),meet(X1,join(X0,X2))),
inference(forward_demodulation,[],[f10202,f6]) ).
fof(f10288,plain,
! [X2,X0,X1] : meet(meet(X1,join(X2,meet(X0,X1))),X0) = meet(X1,meet(join(X2,meet(X0,X1)),join(meet(X0,X1),meet(X0,X2)))),
inference(forward_demodulation,[],[f10174,f7]) ).
fof(f10321,plain,
! [X0] : join(meet(c,sF1),meet(sF3,X0)) = meet(sF3,meet(sF0,join(X0,meet(c,sF1)))),
inference(backward_demodulation,[],[f4790,f10267]) ).
fof(f10334,plain,
! [X2,X0,X1] : meet(X0,meet(X1,join(X2,meet(X0,X1)))) = meet(X1,meet(join(X2,meet(X0,X1)),join(meet(X0,X1),meet(X0,X2)))),
inference(forward_demodulation,[],[f10288,f5]) ).
fof(f10348,plain,
! [X0] : join(meet(c,sF1),meet(sF3,X0)) = meet(sF0,meet(join(X0,meet(c,sF1)),sF3)),
inference(forward_demodulation,[],[f10321,f214]) ).
fof(f10363,plain,
! [X2,X0,X1] : meet(X0,X1) = meet(X1,meet(join(X2,meet(X0,X1)),join(meet(X0,X1),meet(X0,X2)))),
inference(forward_demodulation,[],[f10334,f220]) ).
fof(f10368,plain,
! [X0] : join(meet(c,sF1),meet(sF3,X0)) = meet(sF0,meet(sF3,join(X0,meet(c,sF1)))),
inference(forward_demodulation,[],[f10348,f5]) ).
fof(f10373,plain,
! [X0] : join(meet(c,sF1),meet(sF3,X0)) = meet(join(X0,meet(c,sF1)),meet(c,sF1)),
inference(forward_demodulation,[],[f10368,f3263]) ).
fof(f10374,plain,
! [X0] : join(meet(c,sF1),meet(sF3,X0)) = meet(meet(c,sF1),join(X0,meet(c,sF1))),
inference(forward_demodulation,[],[f10373,f5]) ).
fof(f10375,plain,
! [X0] : meet(c,sF1) = join(meet(c,sF1),meet(sF3,X0)),
inference(forward_demodulation,[],[f10374,f83]) ).
fof(f10376,plain,
sF3 = meet(c,sF1),
inference(backward_demodulation,[],[f7064,f10375]) ).
fof(f10406,plain,
sF1 = join(sF1,sF3),
inference(superposition,[],[f71,f10376]) ).
fof(f10995,plain,
! [X0,X1] :
( zero != meet(meet(X1,X0),join(meet(X0,complement(meet(X0,X1))),complement(X0)))
| complement(meet(X1,X0)) = join(meet(X0,complement(meet(X0,X1))),complement(X0)) ),
inference(superposition,[],[f937,f7870]) ).
fof(f11004,plain,
! [X0,X1] :
( zero != meet(X1,meet(X0,join(meet(X0,complement(meet(X0,X1))),complement(X0))))
| complement(meet(X1,X0)) = join(meet(X0,complement(meet(X0,X1))),complement(X0)) ),
inference(forward_demodulation,[],[f10995,f7]) ).
fof(f11119,plain,
! [X0,X1] :
( zero != meet(X1,meet(X0,join(complement(X0),meet(X0,complement(meet(X0,X1))))))
| complement(meet(X1,X0)) = join(meet(X0,complement(meet(X0,X1))),complement(X0)) ),
inference(forward_demodulation,[],[f11004,f6]) ).
fof(f11216,plain,
! [X0,X1] :
( complement(meet(X1,X0)) = join(complement(X0),meet(X0,complement(meet(X0,X1))))
| zero != meet(X1,meet(X0,join(complement(X0),meet(X0,complement(meet(X0,X1)))))) ),
inference(forward_demodulation,[],[f11119,f6]) ).
fof(f11493,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = meet(join(X1,meet(X2,X0)),join(X0,X1)),
inference(superposition,[],[f83,f982]) ).
fof(f11538,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = meet(join(X0,X1),join(X1,meet(X2,X0))),
inference(forward_demodulation,[],[f11493,f5]) ).
fof(f11591,plain,
! [X2,X0,X1] : meet(X0,X1) = meet(X1,join(meet(X0,X1),meet(X0,X2))),
inference(backward_demodulation,[],[f10363,f11538]) ).
fof(f12017,plain,
! [X2,X0,X1] : meet(join(X1,X2),X0) = join(meet(X0,X1),meet(meet(join(X1,X2),X0),complement(meet(meet(join(X1,X2),X0),X1)))),
inference(superposition,[],[f7870,f641]) ).
fof(f12039,plain,
! [X2,X0,X1] : meet(join(X1,X2),X0) = join(meet(X0,X1),meet(join(X1,X2),meet(X0,complement(meet(meet(join(X1,X2),X0),X1))))),
inference(forward_demodulation,[],[f12017,f7]) ).
fof(f12118,plain,
! [X2,X0,X1] : meet(join(X1,X2),X0) = join(meet(X0,X1),meet(join(X1,X2),meet(X0,complement(meet(X1,meet(join(X1,X2),X0)))))),
inference(forward_demodulation,[],[f12039,f5]) ).
fof(f12166,plain,
! [X2,X0,X1] : meet(join(X1,X2),X0) = join(meet(X0,X1),meet(join(X1,X2),meet(X0,complement(meet(X1,X0))))),
inference(forward_demodulation,[],[f12118,f201]) ).
fof(f12552,plain,
! [X2,X0,X1] : meet(meet(X0,join(X2,meet(X0,X1))),X1) = meet(meet(X0,join(X2,meet(X0,X1))),join(meet(X0,X1),meet(X1,X2))),
inference(superposition,[],[f1574,f74]) ).
fof(f12674,plain,
! [X2,X0,X1] : meet(meet(X0,join(X2,meet(X0,X1))),X1) = meet(X0,meet(join(X2,meet(X0,X1)),join(meet(X0,X1),meet(X1,X2)))),
inference(forward_demodulation,[],[f12552,f7]) ).
fof(f12738,plain,
! [X2,X0,X1] : meet(meet(X0,join(X2,meet(X0,X1))),X1) = meet(X0,join(meet(X0,X1),meet(X1,X2))),
inference(forward_demodulation,[],[f12674,f11538]) ).
fof(f12769,plain,
! [X2,X0,X1] : meet(X1,meet(X0,join(X2,meet(X0,X1)))) = meet(X0,join(meet(X0,X1),meet(X1,X2))),
inference(forward_demodulation,[],[f12738,f5]) ).
fof(f12800,plain,
! [X0,X1] :
( one != one
| zero != meet(join(X1,complement(join(X0,X1))),X0)
| complement(join(X1,complement(join(X0,X1)))) = X0 ),
inference(superposition,[],[f161,f282]) ).
fof(f12833,plain,
! [X0,X1] :
( zero != meet(join(X1,complement(join(X0,X1))),X0)
| complement(join(X1,complement(join(X0,X1)))) = X0 ),
inference(trivial_inequality_removal,[],[f12800]) ).
fof(f12850,plain,
! [X0,X1] :
( zero != meet(X0,join(X1,complement(join(X0,X1))))
| complement(join(X1,complement(join(X0,X1)))) = X0 ),
inference(forward_demodulation,[],[f12833,f5]) ).
fof(f13021,plain,
! [X2,X0,X1] : meet(zero,X2) = meet(X0,meet(X2,meet(X1,complement(meet(X0,X1))))),
inference(superposition,[],[f1668,f430]) ).
fof(f13043,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X1,meet(X2,complement(meet(X1,complement(meet(X0,X1)))))),
inference(superposition,[],[f1668,f6607]) ).
fof(f13093,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X0,meet(X2,X1)),
inference(superposition,[],[f7,f1668]) ).
fof(f13280,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X1,meet(X2,complement(meet(X1,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f13043,f7]) ).
fof(f13300,plain,
! [X2,X0,X1] : zero = meet(X0,meet(X2,meet(X1,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f13021,f455]) ).
fof(f13862,plain,
! [X2,X0,X1] : meet(X0,X1) = meet(X0,join(meet(X0,X1),meet(X1,X2))),
inference(superposition,[],[f11591,f5]) ).
fof(f14159,plain,
! [X2,X0,X1] : meet(X0,X1) = meet(X1,meet(X0,join(X2,meet(X0,X1)))),
inference(backward_demodulation,[],[f12769,f13862]) ).
fof(f14293,plain,
join(sF1,sF2) = join(sF1,meet(sF2,complement(meet(b,sF1)))),
inference(superposition,[],[f7071,f3931]) ).
fof(f14975,plain,
! [X2,X3,X0,X1] : join(join(meet(X2,X0),meet(X0,X1)),X3) = join(join(meet(X2,X0),meet(X0,X1)),join(join(meet(X0,X1),meet(X0,X2)),X3)),
inference(superposition,[],[f113,f223]) ).
fof(f15040,plain,
! [X2,X3,X0,X1] : join(join(meet(X2,X0),meet(X0,X1)),X3) = join(meet(X2,X0),join(meet(X0,X1),join(join(meet(X0,X1),meet(X0,X2)),X3))),
inference(forward_demodulation,[],[f14975,f8]) ).
fof(f15189,plain,
! [X2,X3,X0,X1] : join(join(meet(X2,X0),meet(X0,X1)),X3) = join(meet(X2,X0),join(meet(X0,X1),join(meet(X0,X1),join(meet(X0,X2),X3)))),
inference(forward_demodulation,[],[f15040,f8]) ).
fof(f15305,plain,
! [X2,X3,X0,X1] : join(join(meet(X2,X0),meet(X0,X1)),X3) = join(meet(X2,X0),join(meet(X0,X1),join(meet(X0,X2),X3))),
inference(forward_demodulation,[],[f15189,f101]) ).
fof(f15394,plain,
! [X2,X3,X0,X1] : join(meet(X2,X0),join(meet(X0,X1),X3)) = join(meet(X2,X0),join(meet(X0,X1),join(meet(X0,X2),X3))),
inference(forward_demodulation,[],[f15305,f8]) ).
fof(f15628,plain,
! [X0] : join(sF4,X0) = join(sF2,join(X0,sF3)),
inference(superposition,[],[f180,f6]) ).
fof(f16197,plain,
! [X2,X3,X0,X1] : join(meet(X2,X1),join(X3,X0)) = join(meet(X2,X1),join(X0,join(meet(X1,X2),X3))),
inference(superposition,[],[f966,f126]) ).
fof(f16300,plain,
! [X2,X3,X0,X1] : join(meet(X2,X0),join(meet(X0,X1),X3)) = join(meet(X2,X0),join(X3,meet(X0,X1))),
inference(backward_demodulation,[],[f15394,f16197]) ).
fof(f18553,plain,
join(a,sF3) = join(a,sF4),
inference(superposition,[],[f646,f23]) ).
fof(f18677,plain,
a = join(a,sF4),
inference(forward_demodulation,[],[f18553,f92]) ).
fof(f18714,plain,
sF4 = meet(sF4,a),
inference(superposition,[],[f83,f18677]) ).
fof(f18750,plain,
sF4 = meet(a,sF4),
inference(forward_demodulation,[],[f18714,f5]) ).
fof(f18772,plain,
meet(sF3,sF4) = meet(c,sF4),
inference(superposition,[],[f205,f18750]) ).
fof(f18843,plain,
sF3 = meet(c,sF4),
inference(forward_demodulation,[],[f18772,f183]) ).
fof(f19428,plain,
! [X2,X3,X0,X1] : join(join(meet(X0,X1),meet(X1,X2)),X3) = meet(join(X1,X3),join(join(meet(X0,X1),meet(X1,X2)),X3)),
inference(superposition,[],[f264,f74]) ).
fof(f19638,plain,
! [X2,X3,X0,X1] : join(meet(X0,X1),join(meet(X1,X2),X3)) = meet(join(X1,X3),join(meet(X0,X1),join(meet(X1,X2),X3))),
inference(forward_demodulation,[],[f19428,f8]) ).
fof(f20384,plain,
! [X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(X1,complement(meet(X0,X1)))) = meet(complement(meet(X0,X1)),meet(join(X1,meet(X0,complement(meet(X0,X1)))),join(meet(X0,complement(meet(X0,X1))),join(meet(X0,X1),meet(X1,meet(join(X0,complement(meet(X0,X1))),join(X0,X1))))))),
inference(superposition,[],[f630,f7071]) ).
fof(f20385,plain,
! [X0,X1] : join(meet(X0,complement(meet(X1,X0))),meet(X1,complement(meet(X1,X0)))) = meet(complement(meet(X1,X0)),meet(join(X1,meet(X0,complement(meet(X1,X0)))),join(meet(X0,complement(meet(X1,X0))),join(meet(X0,X1),meet(X1,meet(join(X0,complement(meet(X1,X0))),join(X0,X1))))))),
inference(superposition,[],[f630,f6808]) ).
fof(f20585,plain,
! [X0,X1] : join(meet(X0,complement(meet(X1,X0))),meet(X1,complement(meet(X1,X0)))) = meet(complement(meet(X1,X0)),meet(join(X1,meet(X0,complement(meet(X1,X0)))),join(meet(X0,X1),join(meet(X1,meet(join(X0,complement(meet(X1,X0))),join(X0,X1))),meet(X0,complement(meet(X1,X0))))))),
inference(forward_demodulation,[],[f20385,f126]) ).
fof(f20586,plain,
! [X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(X1,complement(meet(X0,X1)))) = meet(complement(meet(X0,X1)),meet(join(X1,meet(X0,complement(meet(X0,X1)))),join(meet(X0,X1),join(meet(X1,meet(join(X0,complement(meet(X0,X1))),join(X0,X1))),meet(X0,complement(meet(X0,X1))))))),
inference(forward_demodulation,[],[f20384,f126]) ).
fof(f20906,plain,
! [X0,X1] : join(meet(X0,complement(meet(X1,X0))),meet(X1,complement(meet(X1,X0)))) = meet(complement(meet(X1,X0)),join(meet(X0,X1),join(meet(X1,meet(join(X0,complement(meet(X1,X0))),join(X0,X1))),meet(X0,complement(meet(X1,X0)))))),
inference(forward_demodulation,[],[f20585,f19638]) ).
fof(f20907,plain,
! [X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(X1,complement(meet(X0,X1)))) = meet(complement(meet(X0,X1)),join(meet(X0,X1),join(meet(X1,meet(join(X0,complement(meet(X0,X1))),join(X0,X1))),meet(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f20586,f19638]) ).
fof(f21177,plain,
! [X0,X1] : join(meet(X0,complement(meet(X1,X0))),meet(X1,complement(meet(X1,X0)))) = meet(complement(meet(X1,X0)),join(meet(X0,X1),join(meet(X0,complement(meet(X1,X0))),meet(X1,meet(join(X0,complement(meet(X1,X0))),join(X0,X1)))))),
inference(forward_demodulation,[],[f20906,f16300]) ).
fof(f21178,plain,
! [X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(X1,complement(meet(X0,X1)))) = meet(complement(meet(X0,X1)),join(meet(X0,X1),join(meet(X0,complement(meet(X0,X1))),meet(X1,meet(join(X0,complement(meet(X0,X1))),join(X0,X1)))))),
inference(forward_demodulation,[],[f20907,f16300]) ).
fof(f21376,plain,
! [X0,X1] : join(meet(X0,complement(meet(X1,X0))),meet(X1,complement(meet(X1,X0)))) = meet(complement(meet(X1,X0)),join(meet(X1,meet(join(X0,complement(meet(X1,X0))),join(X0,X1))),X0)),
inference(forward_demodulation,[],[f21177,f8636]) ).
fof(f21377,plain,
! [X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(X1,complement(meet(X0,X1)))) = meet(complement(meet(X0,X1)),join(meet(X1,meet(join(X0,complement(meet(X0,X1))),join(X0,X1))),X0)),
inference(forward_demodulation,[],[f21178,f6826]) ).
fof(f21536,plain,
! [X0,X1] : join(meet(X0,complement(meet(X1,X0))),meet(X1,complement(meet(X1,X0)))) = meet(complement(meet(X1,X0)),join(X0,meet(X1,meet(join(X0,complement(meet(X1,X0))),join(X0,X1))))),
inference(forward_demodulation,[],[f21376,f6]) ).
fof(f21537,plain,
! [X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(X1,complement(meet(X0,X1)))) = meet(complement(meet(X0,X1)),join(X0,meet(X1,meet(join(X0,complement(meet(X0,X1))),join(X0,X1))))),
inference(forward_demodulation,[],[f21377,f6]) ).
fof(f21662,plain,
! [X0,X1] : join(meet(X0,complement(meet(X1,X0))),meet(X1,complement(meet(X1,X0)))) = meet(complement(meet(X1,X0)),join(X0,meet(X1,join(X0,complement(meet(X1,X0)))))),
inference(forward_demodulation,[],[f21536,f1574]) ).
fof(f21663,plain,
! [X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(X1,complement(meet(X0,X1)))) = meet(complement(meet(X0,X1)),join(X0,meet(X1,join(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f21537,f1574]) ).
fof(f21760,plain,
! [X0,X1] : join(meet(X0,complement(meet(X1,X0))),meet(X1,complement(meet(X1,X0)))) = meet(complement(meet(X1,X0)),join(X0,meet(X1,one))),
inference(forward_demodulation,[],[f21662,f399]) ).
fof(f21761,plain,
! [X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(X1,complement(meet(X0,X1)))) = meet(complement(meet(X0,X1)),join(X0,meet(X1,one))),
inference(forward_demodulation,[],[f21663,f321]) ).
fof(f21829,plain,
! [X0,X1] : join(meet(X0,complement(meet(X1,X0))),meet(X1,complement(meet(X1,X0)))) = meet(complement(meet(X1,X0)),join(X0,X1)),
inference(forward_demodulation,[],[f21760,f277]) ).
fof(f21830,plain,
! [X0,X1] : meet(complement(meet(X0,X1)),join(X0,X1)) = join(meet(X0,complement(meet(X0,X1))),meet(X1,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f21761,f277]) ).
fof(f21882,plain,
! [X0,X1] : meet(join(X0,X1),complement(meet(X1,X0))) = join(meet(X0,complement(meet(X1,X0))),meet(X1,complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f21829,f5]) ).
fof(f21883,plain,
! [X0,X1] : meet(complement(meet(X0,X1)),join(X0,X1)) = meet(join(X1,X0),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f21830,f7929]) ).
fof(f21916,plain,
! [X0,X1] : meet(join(X0,X1),complement(meet(X0,X1))) = meet(join(X1,X0),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f21883,f5]) ).
fof(f23330,plain,
! [X0,X1] : join(X1,X0) = join(X0,meet(join(X0,X1),complement(meet(X1,X0)))),
inference(superposition,[],[f8343,f21916]) ).
fof(f23350,plain,
! [X2,X0,X1] : meet(join(X1,X0),meet(complement(meet(X1,X0)),X2)) = meet(X2,meet(join(X0,X1),complement(meet(X1,X0)))),
inference(superposition,[],[f214,f21916]) ).
fof(f23408,plain,
! [X2,X0,X1] : meet(X2,meet(join(X0,X1),complement(meet(X0,X1)))) = meet(join(X1,X0),meet(complement(meet(X0,X1)),X2)),
inference(superposition,[],[f214,f21916]) ).
fof(f28397,plain,
! [X2,X0,X1] : meet(X0,join(X2,meet(X0,X1))) = join(meet(X0,X1),meet(meet(X0,join(X2,meet(X0,X1))),complement(meet(X0,X1)))),
inference(superposition,[],[f6622,f14159]) ).
fof(f28469,plain,
! [X2,X0,X1] : meet(X0,join(X2,meet(X0,X1))) = join(meet(X0,X1),meet(complement(meet(X0,X1)),meet(X0,join(X2,meet(X0,X1))))),
inference(forward_demodulation,[],[f28397,f5]) ).
fof(f28635,plain,
! [X2,X0,X1] : meet(X0,join(X2,meet(X0,X1))) = join(meet(X0,X1),meet(X0,meet(join(X2,meet(X0,X1)),complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f28469,f214]) ).
fof(f28736,plain,
! [X2,X0,X1] : meet(X0,join(X2,meet(X0,X1))) = join(meet(X0,X1),meet(X0,meet(complement(meet(X0,X1)),join(X2,meet(X0,X1))))),
inference(forward_demodulation,[],[f28635,f13093]) ).
fof(f28785,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(X1,X2))) = meet(X1,join(meet(X2,join(X0,meet(X1,X2))),meet(join(X1,X2),meet(complement(meet(X1,X2)),join(X0,meet(X1,X2)))))),
inference(backward_demodulation,[],[f9510,f28736]) ).
fof(f35628,plain,
! [X0,X1] : join(X1,meet(X0,complement(meet(X1,X0)))) = join(X1,meet(join(X0,X1),complement(meet(X1,X0)))),
inference(superposition,[],[f254,f21882]) ).
fof(f35671,plain,
! [X0,X1] :
( zero != meet(meet(X0,complement(meet(X1,X0))),join(meet(X1,complement(meet(X1,X0))),complement(meet(join(X0,X1),complement(meet(X1,X0))))))
| meet(X0,complement(meet(X1,X0))) = complement(join(meet(X1,complement(meet(X1,X0))),complement(meet(join(X0,X1),complement(meet(X1,X0)))))) ),
inference(superposition,[],[f12850,f21882]) ).
fof(f35682,plain,
! [X0,X1] :
( zero != meet(X0,meet(complement(meet(X1,X0)),join(meet(X1,complement(meet(X1,X0))),complement(meet(join(X0,X1),complement(meet(X1,X0)))))))
| meet(X0,complement(meet(X1,X0))) = complement(join(meet(X1,complement(meet(X1,X0))),complement(meet(join(X0,X1),complement(meet(X1,X0)))))) ),
inference(forward_demodulation,[],[f35671,f7]) ).
fof(f35716,plain,
! [X0,X1] : join(X0,X1) = join(X1,meet(X0,complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f35628,f9055]) ).
fof(f36384,plain,
! [X0,X1] : join(X0,X1) = join(X1,meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f35716,f5]) ).
fof(f37065,plain,
! [X2,X0,X1] : join(meet(X1,X2),meet(X1,meet(X0,complement(meet(X0,meet(X1,X2)))))) = meet(X1,join(meet(meet(X0,complement(meet(X0,meet(X1,X2)))),join(X1,X2)),meet(X2,join(X0,meet(X1,X2))))),
inference(superposition,[],[f86,f36384]) ).
fof(f37089,plain,
! [X2,X0,X1] : join(meet(X1,X2),meet(X1,meet(X0,complement(meet(X0,meet(X1,X2)))))) = meet(X1,join(meet(X2,join(X0,meet(X1,X2))),meet(meet(X0,complement(meet(X0,meet(X1,X2)))),join(X1,X2)))),
inference(forward_demodulation,[],[f37065,f6]) ).
fof(f37193,plain,
! [X2,X0,X1] : join(meet(X1,X2),meet(X1,meet(X0,complement(meet(X0,meet(X1,X2)))))) = meet(X1,join(meet(X2,join(X0,meet(X1,X2))),meet(join(X1,X2),meet(X0,complement(meet(X0,meet(X1,X2))))))),
inference(forward_demodulation,[],[f37089,f5]) ).
fof(f37362,plain,
join(sF2,c) = join(sF4,c),
inference(superposition,[],[f15628,f65]) ).
fof(f37363,plain,
join(sF2,sF1) = join(sF4,sF1),
inference(superposition,[],[f15628,f10406]) ).
fof(f37446,plain,
join(sF2,sF1) = join(sF1,sF4),
inference(forward_demodulation,[],[f37363,f6]) ).
fof(f37447,plain,
join(sF2,c) = join(c,sF4),
inference(forward_demodulation,[],[f37362,f6]) ).
fof(f37468,plain,
join(sF1,sF2) = join(sF1,sF4),
inference(forward_demodulation,[],[f37446,f6]) ).
fof(f37469,plain,
join(c,sF2) = join(c,sF4),
inference(forward_demodulation,[],[f37447,f6]) ).
fof(f38319,plain,
meet(b,sF2) = meet(b,meet(b,sF1)),
inference(superposition,[],[f591,f3789]) ).
fof(f38492,plain,
meet(b,sF2) = meet(b,sF1),
inference(forward_demodulation,[],[f38319,f148]) ).
fof(f38560,plain,
sF2 = meet(b,sF1),
inference(forward_demodulation,[],[f38492,f2768]) ).
fof(f38621,plain,
join(sF1,sF2) = join(sF1,meet(sF2,complement(sF2))),
inference(backward_demodulation,[],[f14293,f38560]) ).
fof(f38682,plain,
join(sF1,zero) = join(sF1,sF2),
inference(forward_demodulation,[],[f38621,f10]) ).
fof(f38709,plain,
join(zero,sF1) = join(sF1,sF2),
inference(forward_demodulation,[],[f38682,f6]) ).
fof(f38732,plain,
sF1 = join(sF1,sF2),
inference(forward_demodulation,[],[f38709,f449]) ).
fof(f38744,plain,
sF1 = join(sF1,sF4),
inference(backward_demodulation,[],[f37468,f38732]) ).
fof(f38908,plain,
sF4 = meet(sF4,sF1),
inference(superposition,[],[f83,f38744]) ).
fof(f38957,plain,
sF4 = meet(sF1,sF4),
inference(forward_demodulation,[],[f38908,f5]) ).
fof(f39002,plain,
one = join(sF1,complement(sF4)),
inference(superposition,[],[f321,f38957]) ).
fof(f39460,plain,
( one != one
| zero != meet(complement(sF4),sF1)
| sF1 = complement(complement(sF4)) ),
inference(superposition,[],[f161,f39002]) ).
fof(f39484,plain,
( zero != meet(complement(sF4),sF1)
| sF1 = complement(complement(sF4)) ),
inference(trivial_inequality_removal,[],[f39460]) ).
fof(f39508,plain,
( zero != meet(sF1,complement(sF4))
| sF1 = complement(complement(sF4)) ),
inference(forward_demodulation,[],[f39484,f5]) ).
fof(f39521,definition,
( spl5_42
<=> complement(sF1) = complement(sF4) ),
introduced(definition,[new_symbols(definition,[spl5_42])],[avatar_definition]) ).
fof(f39523,plain,
( complement(sF1) = complement(sF4)
| ~ spl5_42 ),
inference(avatar_component_clause,[],[f39521]) ).
fof(f39525,definition,
( spl5_43
<=> zero = meet(sF1,complement(sF4)) ),
introduced(definition,[new_symbols(definition,[spl5_43])],[avatar_definition]) ).
fof(f39527,plain,
( zero != meet(sF1,complement(sF4))
| spl5_43 ),
inference(avatar_component_clause,[],[f39525]) ).
fof(f39546,plain,
( sF1 = sF4
| zero != meet(sF1,complement(sF4)) ),
inference(forward_demodulation,[],[f39508,f6584]) ).
fof(f39557,plain,
zero != meet(sF1,complement(sF4)),
inference(forward_subsumption_resolution,[],[f39546,f24]) ).
fof(f39560,plain,
~ spl5_43,
inference(avatar_split_clause,[],[f39557,f39525]) ).
fof(f40374,plain,
! [X2,X0,X1] : join(X2,meet(complement(meet(X0,X1)),join(X2,meet(X0,complement(meet(X0,X1)))))) = join(join(X2,meet(complement(meet(X0,X1)),join(X2,meet(X0,complement(meet(X0,X1)))))),join(meet(X0,complement(meet(X0,X1))),meet(X0,X2))),
inference(superposition,[],[f71,f421]) ).
fof(f40530,plain,
! [X2,X0,X1] : join(X2,meet(complement(meet(X0,X1)),join(X2,meet(X0,complement(meet(X0,X1)))))) = join(join(meet(X0,complement(meet(X0,X1))),meet(X0,X2)),join(X2,meet(complement(meet(X0,X1)),join(X2,meet(X0,complement(meet(X0,X1))))))),
inference(forward_demodulation,[],[f40374,f6]) ).
fof(f40658,plain,
! [X2,X0,X1] : join(X2,meet(complement(meet(X0,X1)),join(X2,meet(X0,complement(meet(X0,X1)))))) = join(X2,join(meet(complement(meet(X0,X1)),join(X2,meet(X0,complement(meet(X0,X1))))),join(meet(X0,complement(meet(X0,X1))),meet(X0,X2)))),
inference(forward_demodulation,[],[f40530,f126]) ).
fof(f40756,plain,
! [X2,X0,X1] : join(X2,meet(complement(meet(X0,X1)),join(X2,meet(X0,complement(meet(X0,X1)))))) = join(X2,join(meet(complement(meet(X0,X1)),join(X2,meet(X0,complement(meet(X0,X1))))),meet(X0,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f40658,f3615]) ).
fof(f40828,plain,
! [X2,X0,X1] : join(X2,meet(complement(meet(X0,X1)),join(X2,meet(X0,complement(meet(X0,X1)))))) = join(X2,join(meet(X0,complement(meet(X0,X1))),meet(complement(meet(X0,X1)),join(X2,meet(X0,complement(meet(X0,X1))))))),
inference(forward_demodulation,[],[f40756,f6]) ).
fof(f40868,plain,
! [X2,X0,X1] : join(X2,meet(X0,complement(meet(X0,X1)))) = join(X2,meet(complement(meet(X0,X1)),join(X2,meet(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f40828,f124]) ).
fof(f40893,plain,
! [X2,X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(X0,X2)) = meet(X0,join(X2,meet(X0,complement(meet(X0,X1))))),
inference(backward_demodulation,[],[f421,f40868]) ).
fof(f40954,plain,
! [X0,X1] :
( zero != meet(X1,join(meet(X0,complement(meet(X0,X1))),meet(X0,complement(X0))))
| complement(meet(X1,X0)) = join(complement(X0),meet(X0,complement(meet(X0,X1)))) ),
inference(backward_demodulation,[],[f11216,f40893]) ).
fof(f40967,plain,
! [X0,X1] :
( zero != meet(X1,join(meet(X0,complement(X0)),meet(X0,complement(meet(X0,X1)))))
| complement(meet(X1,X0)) = join(complement(X0),meet(X0,complement(meet(X0,X1)))) ),
inference(forward_demodulation,[],[f40954,f6]) ).
fof(f40976,plain,
! [X0,X1] :
( zero != meet(X1,join(zero,meet(X0,complement(meet(X0,X1)))))
| complement(meet(X1,X0)) = join(complement(X0),meet(X0,complement(meet(X0,X1)))) ),
inference(forward_demodulation,[],[f40967,f10]) ).
fof(f40988,plain,
! [X0,X1] :
( zero != meet(X1,meet(X0,complement(meet(X0,X1))))
| complement(meet(X1,X0)) = join(complement(X0),meet(X0,complement(meet(X0,X1)))) ),
inference(forward_demodulation,[],[f40976,f449]) ).
fof(f40994,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(X0),meet(X0,complement(meet(X0,X1)))),
inference(forward_subsumption_resolution,[],[f40988,f772]) ).
fof(f40999,plain,
! [X0,X1] :
( zero != meet(X0,meet(X1,complement(meet(X1,X0))))
| complement(meet(X0,X1)) = join(complement(X0),meet(X0,complement(meet(X0,X1)))) ),
inference(backward_demodulation,[],[f6923,f40994]) ).
fof(f41005,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X0),meet(X0,complement(meet(X0,X1)))),
inference(forward_subsumption_resolution,[],[f40999,f772]) ).
fof(f41096,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(X2,meet(X0,X1))),
inference(superposition,[],[f40893,f6600]) ).
fof(f41097,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X0,X1))) = join(meet(X0,X1),meet(X1,X2)),
inference(superposition,[],[f40893,f6607]) ).
fof(f41479,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(X1,X2))) = meet(X1,join(join(meet(X1,X2),meet(X2,X0)),meet(join(X1,X2),meet(complement(meet(X1,X2)),join(X0,meet(X1,X2)))))),
inference(backward_demodulation,[],[f28785,f41097]) ).
fof(f41495,plain,
! [X2,X0,X1] : join(meet(X1,X2),meet(X1,meet(X0,complement(meet(X0,meet(X1,X2)))))) = meet(X1,join(join(meet(X1,X2),meet(X2,X0)),meet(join(X1,X2),meet(X0,complement(meet(X0,meet(X1,X2))))))),
inference(backward_demodulation,[],[f37193,f41097]) ).
fof(f41557,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X0,X2)) = join(meet(X1,X0),meet(X0,meet(X2,X0))),
inference(backward_demodulation,[],[f224,f41097]) ).
fof(f41915,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = join(meet(X0,X1),meet(X0,meet(X2,X0))),
inference(backward_demodulation,[],[f223,f41096]) ).
fof(f41939,plain,
! [X0,X1] :
( zero != meet(X1,join(meet(X0,complement(meet(X1,X0))),meet(X0,complement(X0))))
| complement(meet(X1,X0)) = join(complement(X0),meet(X0,complement(meet(X1,X0)))) ),
inference(backward_demodulation,[],[f7190,f41096]) ).
fof(f42229,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X0,X2)) = join(meet(X1,X0),meet(X2,X0)),
inference(forward_demodulation,[],[f41557,f147]) ).
fof(f42276,plain,
! [X2,X0,X1] : join(meet(X1,X2),meet(X1,meet(X0,complement(meet(X0,meet(X1,X2)))))) = meet(X1,join(meet(X1,X2),join(meet(X2,X0),meet(join(X1,X2),meet(X0,complement(meet(X0,meet(X1,X2)))))))),
inference(forward_demodulation,[],[f41495,f8]) ).
fof(f42292,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(X1,X2))) = meet(X1,join(meet(X1,X2),join(meet(X2,X0),meet(join(X1,X2),meet(complement(meet(X1,X2)),join(X0,meet(X1,X2))))))),
inference(forward_demodulation,[],[f41479,f8]) ).
fof(f42479,plain,
! [X0,X1] :
( zero != meet(X1,join(meet(X0,complement(X0)),meet(X0,complement(meet(X1,X0)))))
| complement(meet(X1,X0)) = join(complement(X0),meet(X0,complement(meet(X1,X0)))) ),
inference(forward_demodulation,[],[f41939,f6]) ).
fof(f42493,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = join(meet(X0,X1),meet(X2,X0)),
inference(forward_demodulation,[],[f41915,f147]) ).
fof(f42812,plain,
! [X2,X0,X1] : join(meet(X1,X2),meet(X1,X0)) = meet(X1,join(meet(X1,X2),join(meet(X2,X0),meet(join(X1,X2),meet(complement(meet(X1,X2)),join(X0,meet(X1,X2))))))),
inference(forward_demodulation,[],[f42292,f41096]) ).
fof(f42950,plain,
! [X0,X1] :
( zero != meet(X1,join(zero,meet(X0,complement(meet(X1,X0)))))
| complement(meet(X1,X0)) = join(complement(X0),meet(X0,complement(meet(X1,X0)))) ),
inference(forward_demodulation,[],[f42479,f10]) ).
fof(f43263,plain,
! [X0,X1] :
( zero != meet(X1,meet(X0,complement(meet(X1,X0))))
| complement(meet(X1,X0)) = join(complement(X0),meet(X0,complement(meet(X1,X0)))) ),
inference(forward_demodulation,[],[f42950,f449]) ).
fof(f43478,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(X0),meet(X0,complement(meet(X1,X0)))),
inference(forward_subsumption_resolution,[],[f43263,f430]) ).
fof(f43708,plain,
! [X2,X3,X0,X1] : join(meet(X1,X3),meet(X0,meet(X1,X2))) = join(meet(X1,X3),meet(meet(X2,X0),X1)),
inference(superposition,[],[f42493,f214]) ).
fof(f43823,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(X0,X1)) = join(meet(X0,X1),meet(X2,X0)),
inference(superposition,[],[f6,f42493]) ).
fof(f43867,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = join(X1,join(meet(X0,X1),meet(X0,X2))),
inference(superposition,[],[f113,f42493]) ).
fof(f43887,plain,
! [X2,X3,X0,X1] : join(X3,join(meet(X0,X1),meet(X0,X2))) = join(meet(X2,X0),join(X3,meet(X0,X1))),
inference(superposition,[],[f126,f42493]) ).
fof(f43939,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = join(X1,meet(X0,X2)),
inference(forward_demodulation,[],[f43867,f113]) ).
fof(f44006,plain,
! [X2,X3,X0,X1] : join(meet(X1,X3),meet(X0,meet(X1,X2))) = join(meet(X1,X3),meet(X2,meet(X0,X1))),
inference(forward_demodulation,[],[f43708,f7]) ).
fof(f44127,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(meet(X1,X0)),meet(meet(X1,X0),complement(meet(X0,X1)))),
inference(superposition,[],[f43478,f532]) ).
fof(f44204,plain,
! [X0,X1] : complement(X1) = meet(complement(X1),complement(meet(X0,X1))),
inference(superposition,[],[f3,f43478]) ).
fof(f44221,plain,
! [X2,X0,X1] : meet(complement(X1),X2) = meet(complement(X1),meet(X2,complement(meet(X0,X1)))),
inference(superposition,[],[f594,f43478]) ).
fof(f44310,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(meet(X1,X0)),meet(X1,meet(X0,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f44127,f7]) ).
fof(f44363,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(meet(X1,X0)),zero),
inference(forward_demodulation,[],[f44310,f772]) ).
fof(f44397,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(zero,complement(meet(X1,X0))),
inference(forward_demodulation,[],[f44363,f6]) ).
fof(f44421,plain,
! [X0,X1] : complement(meet(X0,X1)) = complement(meet(X1,X0)),
inference(forward_demodulation,[],[f44397,f449]) ).
fof(f44443,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(X0,meet(complement(X0),complement(meet(complement(X0),X1)))),
inference(superposition,[],[f41005,f6584]) ).
fof(f44519,plain,
! [X0,X1] : join(complement(X0),meet(X0,X1)) = complement(meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f41005,f6600]) ).
fof(f44520,plain,
! [X0,X1] : complement(meet(X1,complement(meet(X0,X1)))) = join(complement(X1),meet(X0,X1)),
inference(superposition,[],[f41005,f6607]) ).
fof(f44619,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X1,meet(X2,join(complement(X1),meet(X0,X1)))),
inference(backward_demodulation,[],[f13280,f44520]) ).
fof(f44982,plain,
! [X0,X1] : meet(X0,complement(meet(X0,X1))) = complement(join(complement(X0),meet(X0,X1))),
inference(superposition,[],[f6584,f44519]) ).
fof(f45317,plain,
! [X0,X1] : complement(meet(X1,complement(meet(X0,X1)))) = join(complement(X1),meet(X1,X0)),
inference(superposition,[],[f44519,f44421]) ).
fof(f45519,plain,
! [X0,X1] : complement(meet(X1,complement(X0))) = join(X0,meet(complement(X0),complement(meet(complement(X0),X1)))),
inference(superposition,[],[f40994,f6584]) ).
fof(f46421,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,X1)) = join(meet(X1,X2),meet(X0,X1)),
inference(superposition,[],[f6,f42229]) ).
fof(f46428,plain,
! [X2,X3,X0,X1] : join(meet(X0,X1),join(meet(X1,X2),X3)) = join(X3,join(meet(X0,X1),meet(X2,X1))),
inference(superposition,[],[f126,f42229]) ).
fof(f48695,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(join(X0,X1)),complement(X0)),
inference(superposition,[],[f44204,f3]) ).
fof(f48869,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X0),complement(join(X0,X1))),
inference(forward_demodulation,[],[f48695,f5]) ).
fof(f49166,plain,
! [X0,X1] : join(complement(complement(X0)),complement(join(X0,X1))) = complement(meet(complement(X0),complement(complement(join(X0,X1))))),
inference(superposition,[],[f44519,f48869]) ).
fof(f49167,plain,
! [X0,X1] : complement(meet(complement(X0),join(X0,X1))) = join(complement(complement(X0)),complement(join(X0,X1))),
inference(forward_demodulation,[],[f49166,f6584]) ).
fof(f49227,plain,
! [X0,X1] : join(X0,complement(join(X0,X1))) = complement(meet(complement(X0),join(X0,X1))),
inference(forward_demodulation,[],[f49167,f6584]) ).
fof(f49261,plain,
! [X0,X1] : meet(join(X0,X1),join(X0,complement(join(X0,X1)))) = X0,
inference(backward_demodulation,[],[f9735,f49227]) ).
fof(f49350,plain,
! [X0,X1] : complement(X0) = meet(complement(meet(X0,X1)),join(complement(X0),complement(complement(meet(X0,X1))))),
inference(superposition,[],[f49261,f41005]) ).
fof(f49398,plain,
! [X0,X1] : meet(X1,X0) = meet(X1,join(X0,complement(join(X0,X1)))),
inference(superposition,[],[f203,f49261]) ).
fof(f49539,plain,
! [X0,X1] : complement(X0) = meet(complement(meet(X0,X1)),join(complement(X0),meet(X0,X1))),
inference(forward_demodulation,[],[f49350,f6584]) ).
fof(f49726,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(X1,complement(join(X0,X1)))),
inference(superposition,[],[f49398,f6]) ).
fof(f49733,plain,
! [X0,X1] : meet(meet(join(X0,X1),complement(meet(X0,X1))),X1) = meet(meet(join(X0,X1),complement(meet(X0,X1))),join(X1,complement(join(X0,X1)))),
inference(superposition,[],[f49398,f8343]) ).
fof(f49735,plain,
! [X0,X1] : meet(meet(join(X1,X0),complement(meet(X0,X1))),X1) = meet(meet(join(X1,X0),complement(meet(X0,X1))),join(X1,complement(join(X0,X1)))),
inference(superposition,[],[f49398,f23330]) ).
fof(f50081,plain,
! [X0,X1] : meet(meet(join(X1,X0),complement(meet(X0,X1))),X1) = meet(join(X1,complement(join(X0,X1))),meet(join(X1,X0),complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f49735,f5]) ).
fof(f50083,plain,
! [X0,X1] : meet(meet(join(X0,X1),complement(meet(X0,X1))),X1) = meet(join(X1,complement(join(X0,X1))),meet(join(X0,X1),complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f49733,f5]) ).
fof(f50092,plain,
! [X0,X1] :
( complement(X0) = join(X1,complement(join(X0,X1)))
| meet(X0,X1) != zero ),
inference(backward_demodulation,[],[f937,f49726]) ).
fof(f50210,plain,
! [X0,X1] : meet(meet(join(X1,X0),complement(meet(X0,X1))),X1) = meet(join(X0,X1),meet(complement(meet(X0,X1)),join(X1,complement(join(X0,X1))))),
inference(forward_demodulation,[],[f50081,f23350]) ).
fof(f50212,plain,
! [X0,X1] : meet(meet(join(X0,X1),complement(meet(X0,X1))),X1) = meet(join(X1,X0),meet(complement(meet(X0,X1)),join(X1,complement(join(X0,X1))))),
inference(forward_demodulation,[],[f50083,f23408]) ).
fof(f50281,plain,
! [X0,X1] : meet(X1,meet(join(X1,X0),complement(meet(X0,X1)))) = meet(join(X0,X1),meet(complement(meet(X0,X1)),join(X1,complement(join(X0,X1))))),
inference(forward_demodulation,[],[f50210,f5]) ).
fof(f50283,plain,
! [X0,X1] : meet(X1,meet(join(X0,X1),complement(meet(X0,X1)))) = meet(join(X1,X0),meet(complement(meet(X0,X1)),join(X1,complement(join(X0,X1))))),
inference(forward_demodulation,[],[f50212,f5]) ).
fof(f50323,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(join(X0,X1),meet(complement(meet(X0,X1)),join(X1,complement(join(X0,X1))))),
inference(forward_demodulation,[],[f50281,f201]) ).
fof(f50325,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(join(X1,X0),meet(complement(meet(X0,X1)),join(X1,complement(join(X0,X1))))),
inference(forward_demodulation,[],[f50283,f203]) ).
fof(f50415,plain,
! [X0,X1] :
( complement(X0) = join(meet(X1,complement(meet(X1,X0))),complement(join(X0,X1)))
| zero != meet(X0,meet(X1,complement(meet(X1,X0)))) ),
inference(superposition,[],[f50092,f6808]) ).
fof(f50455,plain,
! [X0,X1] :
( complement(meet(X0,complement(meet(X1,X0)))) = join(meet(X1,complement(meet(X1,X0))),complement(meet(join(X0,X1),complement(meet(X1,X0)))))
| zero != meet(meet(X0,complement(meet(X1,X0))),meet(X1,complement(meet(X1,X0)))) ),
inference(superposition,[],[f50092,f21882]) ).
fof(f50629,plain,
! [X0,X1] :
( join(complement(X0),meet(X1,X0)) = join(meet(X1,complement(meet(X1,X0))),complement(meet(join(X0,X1),complement(meet(X1,X0)))))
| zero != meet(meet(X0,complement(meet(X1,X0))),meet(X1,complement(meet(X1,X0)))) ),
inference(forward_demodulation,[],[f50455,f44520]) ).
fof(f50666,plain,
! [X0,X1] : complement(X0) = join(meet(X1,complement(meet(X1,X0))),complement(join(X0,X1))),
inference(forward_subsumption_resolution,[],[f50415,f772]) ).
fof(f50707,plain,
! [X0,X1] :
( zero != meet(complement(meet(X1,X0)),meet(meet(X0,complement(meet(X1,X0))),X1))
| join(complement(X0),meet(X1,X0)) = join(meet(X1,complement(meet(X1,X0))),complement(meet(join(X0,X1),complement(meet(X1,X0))))) ),
inference(forward_demodulation,[],[f50629,f214]) ).
fof(f50740,plain,
! [X0,X1] : complement(X0) = join(complement(join(X0,X1)),meet(X1,complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f50666,f6]) ).
fof(f50759,plain,
! [X0,X1] :
( zero != meet(X1,meet(complement(meet(X1,X0)),meet(X0,complement(meet(X1,X0)))))
| join(complement(X0),meet(X1,X0)) = join(meet(X1,complement(meet(X1,X0))),complement(meet(join(X0,X1),complement(meet(X1,X0))))) ),
inference(forward_demodulation,[],[f50707,f214]) ).
fof(f50789,plain,
! [X0,X1] : join(complement(X0),meet(X1,X0)) = join(meet(X1,complement(meet(X1,X0))),complement(meet(join(X0,X1),complement(meet(X1,X0))))),
inference(forward_subsumption_resolution,[],[f50759,f13300]) ).
fof(f50804,plain,
! [X0,X1] :
( meet(X0,complement(meet(X1,X0))) = complement(join(complement(X0),meet(X1,X0)))
| zero != meet(X0,meet(complement(meet(X1,X0)),join(meet(X1,complement(meet(X1,X0))),complement(meet(join(X0,X1),complement(meet(X1,X0))))))) ),
inference(backward_demodulation,[],[f35682,f50789]) ).
fof(f50813,plain,
! [X0,X1] :
( zero != meet(X0,meet(complement(meet(X1,X0)),join(complement(X0),meet(X1,X0))))
| meet(X0,complement(meet(X1,X0))) = complement(join(complement(X0),meet(X1,X0))) ),
inference(forward_demodulation,[],[f50804,f50789]) ).
fof(f50814,plain,
! [X0,X1] :
( zero != meet(X1,meet(X0,complement(meet(X1,X0))))
| meet(X0,complement(meet(X1,X0))) = complement(join(complement(X0),meet(X1,X0))) ),
inference(forward_demodulation,[],[f50813,f44619]) ).
fof(f50815,plain,
! [X0,X1] : meet(X0,complement(meet(X1,X0))) = complement(join(complement(X0),meet(X1,X0))),
inference(forward_subsumption_resolution,[],[f50814,f430]) ).
fof(f52072,plain,
complement(sF1) = join(complement(join(sF1,c)),meet(c,complement(sF3))),
inference(superposition,[],[f50740,f10376]) ).
fof(f52086,plain,
complement(sF4) = join(complement(join(sF4,c)),meet(c,complement(sF3))),
inference(superposition,[],[f50740,f18843]) ).
fof(f52101,plain,
! [X0,X1] : join(X1,complement(join(X0,X1))) = join(X1,complement(X0)),
inference(superposition,[],[f254,f50740]) ).
fof(f52106,plain,
! [X0,X1] : meet(X1,complement(meet(X1,X0))) = meet(meet(X1,complement(meet(X1,X0))),complement(X0)),
inference(superposition,[],[f83,f50740]) ).
fof(f52117,plain,
! [X2,X0,X1] : meet(meet(X1,complement(meet(X1,X0))),X2) = meet(meet(X1,complement(meet(X1,X0))),meet(complement(X0),X2)),
inference(superposition,[],[f203,f50740]) ).
fof(f52165,plain,
! [X2,X0,X1] : meet(meet(X1,complement(meet(X1,X0))),X2) = meet(complement(X0),meet(X2,meet(X1,complement(meet(X1,X0))))),
inference(forward_demodulation,[],[f52117,f214]) ).
fof(f52175,plain,
! [X0,X1] : meet(X1,complement(meet(X1,X0))) = meet(complement(X0),meet(X1,complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f52106,f5]) ).
fof(f52182,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(X1,complement(X0))),
inference(backward_demodulation,[],[f49726,f52101]) ).
fof(f52186,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(join(X0,X1),meet(complement(meet(X0,X1)),join(X1,complement(X0)))),
inference(backward_demodulation,[],[f50323,f52101]) ).
fof(f52188,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(join(X1,X0),meet(complement(meet(X0,X1)),join(X1,complement(X0)))),
inference(backward_demodulation,[],[f50325,f52101]) ).
fof(f52248,plain,
complement(sF4) = join(complement(join(c,sF4)),meet(c,complement(sF3))),
inference(forward_demodulation,[],[f52086,f6]) ).
fof(f52262,plain,
complement(sF1) = join(complement(join(c,sF1)),meet(c,complement(sF3))),
inference(forward_demodulation,[],[f52072,f6]) ).
fof(f52432,plain,
! [X2,X0,X1] : meet(X1,meet(complement(meet(X1,X0)),X2)) = meet(complement(X0),meet(X2,meet(X1,complement(meet(X1,X0))))),
inference(forward_demodulation,[],[f52165,f7]) ).
fof(f52435,plain,
! [X0,X1] : meet(complement(X0),X1) = meet(X1,complement(meet(X1,X0))),
inference(forward_demodulation,[],[f52175,f44221]) ).
fof(f52454,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(join(X1,X0),meet(join(X1,complement(X0)),complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f52188,f13093]) ).
fof(f52456,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(join(X0,X1),meet(join(X1,complement(X0)),complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f52186,f13093]) ).
fof(f52457,plain,
! [X0,X1] : join(X1,complement(X0)) = join(complement(X0),meet(X0,X1)),
inference(backward_demodulation,[],[f9381,f52182]) ).
fof(f52485,plain,
complement(sF4) = join(complement(join(c,sF2)),meet(c,complement(sF3))),
inference(forward_demodulation,[],[f52248,f37469]) ).
fof(f52727,plain,
! [X0,X1] : join(complement(X0),meet(X0,X1)) = complement(meet(complement(X1),X0)),
inference(backward_demodulation,[],[f44519,f52435]) ).
fof(f52737,plain,
! [X0,X1] : meet(complement(X1),X0) = complement(join(complement(X0),meet(X0,X1))),
inference(backward_demodulation,[],[f44982,f52435]) ).
fof(f52766,plain,
! [X2,X0,X1] : meet(X1,meet(complement(meet(X1,X0)),X2)) = meet(complement(X0),meet(X2,meet(complement(X0),X1))),
inference(backward_demodulation,[],[f52432,f52435]) ).
fof(f52799,plain,
! [X2,X0,X1] : join(meet(X1,X2),meet(X1,meet(complement(meet(X1,X2)),X0))) = meet(X1,join(meet(X1,X2),join(meet(X2,X0),meet(join(X1,X2),meet(complement(meet(X1,X2)),X0))))),
inference(backward_demodulation,[],[f42276,f52435]) ).
fof(f52856,plain,
! [X0,X1] : complement(meet(X1,complement(X0))) = join(X0,meet(complement(X1),complement(X0))),
inference(backward_demodulation,[],[f45519,f52435]) ).
fof(f52857,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(X0,meet(complement(X1),complement(X0))),
inference(backward_demodulation,[],[f44443,f52435]) ).
fof(f52922,plain,
! [X0,X1] : join(X0,complement(X1)) = complement(meet(X1,complement(meet(X0,X1)))),
inference(backward_demodulation,[],[f45317,f52457]) ).
fof(f52924,plain,
! [X0,X1] : complement(X0) = meet(complement(meet(X0,X1)),join(X1,complement(X0))),
inference(backward_demodulation,[],[f49539,f52457]) ).
fof(f53215,plain,
! [X2,X0,X1] : meet(X1,meet(complement(meet(X1,X0)),X2)) = meet(complement(X0),meet(X2,X1)),
inference(forward_demodulation,[],[f52766,f566]) ).
fof(f53228,plain,
! [X0,X1] : meet(complement(X1),X0) = complement(join(X1,complement(X0))),
inference(forward_demodulation,[],[f52737,f52457]) ).
fof(f53233,plain,
! [X0,X1] : join(X1,complement(X0)) = complement(meet(complement(X1),X0)),
inference(forward_demodulation,[],[f52727,f52457]) ).
fof(f53343,plain,
! [X0,X1] : complement(X0) = meet(join(X1,complement(X0)),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f52924,f5]) ).
fof(f53344,plain,
! [X0,X1] : join(X0,complement(X1)) = join(complement(X1),meet(X0,X1)),
inference(backward_demodulation,[],[f44520,f52922]) ).
fof(f53549,plain,
! [X2,X0,X1] : meet(X1,join(meet(X1,X2),join(meet(X2,X0),meet(join(X1,X2),meet(complement(meet(X1,X2)),X0))))) = join(meet(X1,X2),meet(complement(X2),meet(X0,X1))),
inference(backward_demodulation,[],[f52799,f53215]) ).
fof(f53613,plain,
! [X0,X1] : join(X0,complement(X1)) = join(X0,meet(complement(X1),complement(X0))),
inference(backward_demodulation,[],[f52857,f53233]) ).
fof(f53689,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(join(X0,X1),complement(X0)),
inference(backward_demodulation,[],[f52456,f53343]) ).
fof(f53690,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(join(X1,X0),complement(X0)),
inference(backward_demodulation,[],[f52454,f53343]) ).
fof(f53719,plain,
! [X0,X1] : meet(X0,complement(meet(X1,X0))) = complement(join(X1,complement(X0))),
inference(backward_demodulation,[],[f50815,f53344]) ).
fof(f53924,plain,
! [X0,X1] : join(X0,complement(X1)) = complement(meet(X1,complement(X0))),
inference(backward_demodulation,[],[f52856,f53613]) ).
fof(f53936,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(complement(X0),join(X1,X0)),
inference(forward_demodulation,[],[f53690,f5]) ).
fof(f53937,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(complement(X0),join(X0,X1)),
inference(forward_demodulation,[],[f53689,f5]) ).
fof(f53991,plain,
! [X0,X1] : meet(X0,complement(meet(X1,X0))) = meet(complement(X1),X0),
inference(forward_demodulation,[],[f53719,f53228]) ).
fof(f54245,plain,
! [X2,X0,X1] : meet(join(X1,X2),X0) = join(meet(X0,X1),meet(join(X1,X2),meet(complement(X1),X0))),
inference(backward_demodulation,[],[f12166,f53991]) ).
fof(f54298,plain,
! [X0,X1] : meet(complement(X0),X1) = meet(complement(X0),join(X1,X0)),
inference(backward_demodulation,[],[f53936,f53991]) ).
fof(f54299,plain,
! [X0,X1] : meet(complement(X0),X1) = meet(complement(X0),join(X0,X1)),
inference(backward_demodulation,[],[f53937,f53991]) ).
fof(f54569,plain,
! [X2,X0,X1] : join(meet(X1,X2),meet(X1,X0)) = meet(X1,join(meet(X1,X2),join(meet(X2,X0),meet(join(X1,X2),meet(complement(meet(X1,X2)),X0))))),
inference(backward_demodulation,[],[f42812,f54298]) ).
fof(f54580,plain,
! [X2,X0,X1] : meet(join(X1,X2),X0) = join(meet(X0,X1),meet(complement(X1),meet(X0,join(X1,X2)))),
inference(forward_demodulation,[],[f54245,f44006]) ).
fof(f54694,plain,
! [X2,X0,X1] : join(meet(X1,X2),meet(X1,X0)) = join(meet(X1,X2),meet(complement(X2),meet(X0,X1))),
inference(backward_demodulation,[],[f53549,f54569]) ).
fof(f54959,plain,
meet(c,complement(sF3)) = meet(complement(a),c),
inference(superposition,[],[f52435,f26]) ).
fof(f54965,plain,
meet(c,complement(sF3)) = meet(complement(sF1),c),
inference(superposition,[],[f52435,f10376]) ).
fof(f55106,plain,
meet(c,complement(sF3)) = meet(c,complement(sF1)),
inference(forward_demodulation,[],[f54965,f5]) ).
fof(f55111,plain,
meet(c,complement(sF3)) = meet(c,complement(a)),
inference(forward_demodulation,[],[f54959,f5]) ).
fof(f55291,plain,
complement(sF1) = join(complement(join(c,sF1)),meet(c,complement(sF1))),
inference(backward_demodulation,[],[f52262,f55106]) ).
fof(f55293,plain,
complement(sF4) = join(complement(join(c,sF2)),meet(c,complement(sF1))),
inference(backward_demodulation,[],[f52485,f55106]) ).
fof(f55316,plain,
meet(c,complement(sF1)) = meet(c,complement(a)),
inference(backward_demodulation,[],[f55106,f55111]) ).
fof(f55458,plain,
complement(sF1) = join(complement(join(c,sF1)),meet(c,complement(a))),
inference(backward_demodulation,[],[f55291,f55316]) ).
fof(f55460,plain,
complement(sF4) = join(complement(join(c,sF2)),meet(c,complement(a))),
inference(backward_demodulation,[],[f55293,f55316]) ).
fof(f55537,plain,
complement(sF4) = join(meet(c,complement(a)),complement(join(c,sF2))),
inference(forward_demodulation,[],[f55460,f6]) ).
fof(f55538,plain,
complement(sF1) = join(meet(c,complement(a)),complement(join(c,sF1))),
inference(forward_demodulation,[],[f55458,f6]) ).
fof(f56209,plain,
! [X2,X0,X1] : meet(meet(complement(X0),X1),X2) = meet(complement(X0),meet(X2,join(X0,X1))),
inference(superposition,[],[f1668,f54299]) ).
fof(f56237,plain,
! [X2,X0,X1] : meet(complement(X0),meet(X1,X2)) = meet(complement(X0),meet(X2,join(X0,X1))),
inference(forward_demodulation,[],[f56209,f7]) ).
fof(f56353,plain,
! [X2,X0,X1] : meet(join(X1,X2),X0) = join(meet(X0,X1),meet(complement(X1),meet(X2,X0))),
inference(backward_demodulation,[],[f54580,f56237]) ).
fof(f56433,plain,
! [X2,X0,X1] : join(meet(X1,X2),meet(X1,X0)) = meet(join(X2,X0),X1),
inference(backward_demodulation,[],[f54694,f56353]) ).
fof(f56572,plain,
! [X2,X0,X1] : meet(X0,join(X2,meet(X0,X1))) = meet(join(X1,X2),X0),
inference(backward_demodulation,[],[f41096,f56433]) ).
fof(f56683,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,X0)) = meet(join(X2,X1),X0),
inference(backward_demodulation,[],[f43823,f56433]) ).
fof(f56685,plain,
! [X2,X3,X0,X1] : join(X3,meet(join(X1,X2),X0)) = join(meet(X2,X0),join(X3,meet(X0,X1))),
inference(backward_demodulation,[],[f43887,f56433]) ).
fof(f57839,plain,
! [X2,X3,X0,X1] : join(X3,meet(join(X1,X2),X0)) = join(meet(X2,X0),join(meet(X0,X1),X3)),
inference(backward_demodulation,[],[f16300,f56685]) ).
fof(f57945,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,X1)) = meet(join(X0,X2),X1),
inference(backward_demodulation,[],[f46421,f56683]) ).
fof(f58909,plain,
! [X2,X3,X0,X1] : join(X3,meet(join(X2,X0),X1)) = join(X3,join(meet(X0,X1),meet(X2,X1))),
inference(backward_demodulation,[],[f46428,f57839]) ).
fof(f60354,plain,
! [X2,X3,X0,X1] : join(X3,meet(join(X0,X2),X1)) = join(X3,meet(join(X2,X0),X1)),
inference(forward_demodulation,[],[f58909,f57945]) ).
fof(f70673,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = join(join(X1,meet(X2,X0)),meet(join(X0,X1),X2)),
inference(superposition,[],[f71,f56572]) ).
fof(f70750,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = join(X1,join(meet(X2,X0),meet(join(X0,X1),X2))),
inference(forward_demodulation,[],[f70673,f8]) ).
fof(f70858,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = join(X1,meet(join(join(X0,X1),X0),X2)),
inference(forward_demodulation,[],[f70750,f56683]) ).
fof(f70945,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = join(X1,meet(join(X0,join(X0,X1)),X2)),
inference(forward_demodulation,[],[f70858,f60354]) ).
fof(f71069,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = join(X1,meet(join(X0,X1),X2)),
inference(forward_demodulation,[],[f70945,f101]) ).
fof(f73040,plain,
! [X0] : join(c,meet(sF0,X0)) = join(c,meet(X0,b)),
inference(superposition,[],[f71069,f15]) ).
fof(f74505,plain,
! [X2,X0,X1] : complement(meet(join(X0,complement(X1)),X2)) = join(meet(X1,complement(X0)),complement(X2)),
inference(superposition,[],[f53233,f53924]) ).
fof(f74534,plain,
complement(sF1) = complement(meet(join(a,complement(c)),join(c,sF1))),
inference(backward_demodulation,[],[f55538,f74505]) ).
fof(f74535,plain,
complement(sF4) = complement(meet(join(a,complement(c)),join(c,sF2))),
inference(backward_demodulation,[],[f55537,f74505]) ).
fof(f74580,plain,
complement(sF4) = complement(meet(join(c,sF2),join(a,complement(c)))),
inference(forward_demodulation,[],[f74535,f44421]) ).
fof(f74581,plain,
complement(sF1) = complement(meet(join(c,sF1),join(a,complement(c)))),
inference(forward_demodulation,[],[f74534,f44421]) ).
fof(f82116,plain,
join(c,sF1) = join(c,meet(sF1,b)),
inference(superposition,[],[f73040,f568]) ).
fof(f82194,plain,
join(c,sF1) = join(c,meet(b,sF1)),
inference(forward_demodulation,[],[f82116,f43939]) ).
fof(f82252,plain,
join(c,sF2) = join(c,sF1),
inference(forward_demodulation,[],[f82194,f38560]) ).
fof(f82300,plain,
complement(sF4) = complement(meet(join(c,sF1),join(a,complement(c)))),
inference(backward_demodulation,[],[f74580,f82252]) ).
fof(f82326,plain,
complement(sF1) = complement(sF4),
inference(forward_demodulation,[],[f82300,f74581]) ).
fof(f82338,plain,
spl5_42,
inference(avatar_split_clause,[],[f82326,f39521]) ).
fof(f82358,plain,
( zero != meet(sF1,complement(sF1))
| ~ spl5_42
| spl5_43 ),
inference(backward_demodulation,[],[f39527,f39523]) ).
fof(f82395,plain,
( $false
| ~ spl5_42
| spl5_43 ),
inference(forward_subsumption_resolution,[],[f82358,f10]) ).
fof(f82396,plain,
( ~ spl5_42
| spl5_43 ),
inference(avatar_contradiction_clause,[],[f82395]) ).
cnf(s24,plain,
~ spl5_43,
inference(sat_conversion,[],[f39560]) ).
cnf(s30,plain,
spl5_42,
inference(sat_conversion,[],[f82338]) ).
cnf(s31,plain,
( ~ spl5_42
| spl5_43 ),
inference(sat_conversion,[],[f82396]) ).
cnf(s32,plain,
spl5_43,
inference(rat,[],[s31,s30]) ).
cnf(s34,plain,
$false,
inference(rat,[],[s24,s32]) ).
fof(f82403,plain,
$false,
inference(avatar_sat_refutation,[],[s34]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT192-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.14/0.41 % Computer : n017.cluster.edu
% 0.14/0.41 % Model : x86_64 x86_64
% 0.14/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.41 % Memory : 8046.5625MB
% 0.14/0.41 % OS : Linux 6.8.0-71-generic
% 0.14/0.41 % CPULimit : 300
% 0.14/0.41 % WCLimit : 300
% 0.14/0.41 % DateTime : Sun Sep 27 14:00:20 UTC 2026
% 0.14/0.42 % CPUTime :
% 0.14/0.42 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.21/0.48 Running first-order theorem proving
% 0.21/0.48 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
% 19.47/3.93 % (2577795)Input is clausal, will run a generic CNF schedule.
% 19.47/3.93 % (2577805)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2139319276:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 19.47/3.93 % (2577804)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1903855041:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 19.47/3.93 % (2577802)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2618181403:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 19.47/3.93 % (2577801)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1461025725:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 19.47/3.93 % (2577800)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=4233712111:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 19.47/3.93 % (2577806)dis-21_1_sil=8000:lcm=predicate:random_seed=303390005: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)
% 19.47/3.93 % (2577803)lrs+10_1_sil=8000:sp=occurrence:random_seed=3510151039:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 19.47/3.93 % (2577806)Refutation not found, incomplete strategy
% 19.47/3.93 % (2577806)------------------------------
% 19.47/3.93 % (2577806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.47/3.93 % (2577806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.47/3.93 % (2577806)CaDiCaL version: 2.1.3
% 19.47/3.93 % (2577806)Termination reason: Refutation not found, incomplete strategy
% 19.47/3.93 % (2577806)Time elapsed: 0.003 s
% 19.47/3.93 % (2577806)Peak memory usage: 88 MB
% 19.47/3.93 % (2577806)Instructions burned: 1 (million)
% 19.47/3.93 % (2577805)Instruction limit reached!
% 19.47/3.93 % (2577805)------------------------------
% 19.47/3.93 % (2577805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.47/3.93 % (2577805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.47/3.93 % (2577805)CaDiCaL version: 2.1.3
% 19.47/3.93 % (2577805)Termination reason: Instruction limit
% 19.47/3.93 % (2577805)Termination phase: Saturation
% 19.47/3.93 % (2577805)Time elapsed: 0.082 s
% 19.47/3.93 % (2577805)Peak memory usage: 89 MB
% 19.47/3.93 % (2577805)Instructions burned: 181 (million)
% 19.47/3.93 % (2577804)Instruction limit reached!
% 19.47/3.93 % (2577804)------------------------------
% 19.47/3.93 % (2577804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.47/3.93 % (2577804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.47/3.93 % (2577804)CaDiCaL version: 2.1.3
% 19.47/3.93 % (2577804)Termination reason: Instruction limit
% 19.47/3.93 % (2577804)Termination phase: Saturation
% 19.47/3.93 % (2577804)Time elapsed: 0.114 s
% 19.47/3.93 % (2577804)Peak memory usage: 89 MB
% 19.47/3.93 % (2577804)Instructions burned: 114 (million)
% 19.47/3.93 % (2577803)Instruction limit reached!
% 19.47/3.93 % (2577803)------------------------------
% 19.47/3.93 % (2577803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.47/3.93 % (2577803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.47/3.93 % (2577803)CaDiCaL version: 2.1.3
% 19.47/3.93 % (2577803)Termination reason: Instruction limit
% 19.47/3.93 % (2577803)Termination phase: Saturation
% 19.47/3.93 % (2577803)Time elapsed: 0.104 s
% 19.47/3.93 % (2577803)Peak memory usage: 88 MB
% 19.47/3.93 % (2577803)Instructions burned: 108 (million)
% 19.47/3.93 % (2577814)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=4034982001:i=143:sd=2:aac=none:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/143Mi)
% 19.47/3.93 % (2577814)Refutation not found, incomplete strategy
% 19.47/3.93 % (2577814)------------------------------
% 19.47/3.93 % (2577814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.47/3.93 % (2577814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.47/3.93 % (2577814)CaDiCaL version: 2.1.3
% 19.47/3.93 % (2577814)Termination reason: Refutation not found, incomplete strategy
% 19.47/3.93 % (2577814)Time elapsed: 0.002 s
% 19.47/3.93 % (2577814)Peak memory usage: 88 MB
% 19.47/3.93 % (2577815)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1539699025:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 39.12/6.56 % (2577815)Refutation not found, incomplete strategy
% 39.12/6.56 % (2577815)------------------------------
% 39.12/6.56 % (2577815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.12/6.56 % (2577815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.12/6.56 % (2577815)CaDiCaL version: 2.1.3
% 39.12/6.56 % (2577815)Termination reason: Refutation not found, incomplete strategy
% 39.12/6.56 % (2577815)Time elapsed: 0.003 s
% 39.12/6.56 % (2577815)Peak memory usage: 88 MB
% 39.12/6.56 % (2577815)Instructions burned: 1 (million)
% 39.12/6.56 % (2577806)------------------------------
% 39.12/6.56 % (2577806)------------------------------
% 39.12/6.56 % (2577816)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=203595253:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 39.12/6.56 % (2577816)Refutation not found, incomplete strategy
% 39.12/6.56 % (2577816)------------------------------
% 39.12/6.56 % (2577816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.12/6.56 % (2577816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.12/6.56 % (2577816)CaDiCaL version: 2.1.3
% 39.12/6.56 % (2577816)Termination reason: Refutation not found, incomplete strategy
% 39.12/6.56 % (2577816)Time elapsed: 0.003 s
% 39.12/6.56 % (2577816)Peak memory usage: 88 MB
% 39.12/6.56 % (2577814)------------------------------
% 39.12/6.56 % (2577814)------------------------------
% 39.12/6.56 % (2577819)lrs+10_64_to=lpo:sil=8000:random_seed=2661951166:i=126:bd=preordered_2992 on theBenchmark for (2992ds/126Mi)
% 39.12/6.56 % (2577815)------------------------------
% 39.12/6.56 % (2577815)------------------------------
% 39.12/6.56 % (2577821)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1842573180:avsq=on:i=194:fgj=on:bd=preordered_2991 on theBenchmark for (2991ds/194Mi)
% 39.12/6.56 % (2577819)Instruction limit reached!
% 39.12/6.56 % (2577819)------------------------------
% 39.12/6.56 % (2577819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.12/6.56 % (2577819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.12/6.56 % (2577819)CaDiCaL version: 2.1.3
% 39.12/6.56 % (2577819)Termination reason: Instruction limit
% 39.12/6.56 % (2577819)Termination phase: Saturation
% 39.12/6.56 % (2577819)Time elapsed: 0.121 s
% 39.12/6.56 % (2577819)Peak memory usage: 88 MB
% 39.12/6.56 % (2577819)Instructions burned: 126 (million)
% 39.12/6.56 % (2577816)------------------------------
% 39.12/6.56 % (2577816)------------------------------
% 39.12/6.56 % (2577821)Instruction limit reached!
% 39.12/6.56 % (2577821)------------------------------
% 39.12/6.56 % (2577821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.12/6.56 % (2577821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.12/6.56 % (2577821)CaDiCaL version: 2.1.3
% 39.12/6.56 % (2577821)Termination reason: Instruction limit
% 39.12/6.56 % (2577821)Termination phase: Saturation
% 39.12/6.56 % (2577821)Time elapsed: 0.186 s
% 39.12/6.56 % (2577821)Peak memory usage: 90 MB
% 39.12/6.56 % (2577821)Instructions burned: 195 (million)
% 39.12/6.56 % (2577823)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3029602636:i=157:gtg=all_2989 on theBenchmark for (2989ds/157Mi)
% 39.12/6.56 % (2577825)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=959790060:i=3394:sd=4:ss=included:sgt=64_2988 on theBenchmark for (2988ds/3394Mi)
% 39.12/6.56 % (2577826)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=2813189293:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2988 on theBenchmark for (2988ds/106Mi)
% 39.12/6.56 % (2577823)Instruction limit reached!
% 39.12/6.56 % (2577823)------------------------------
% 39.12/6.56 % (2577823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.12/6.56 % (2577823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.12/6.56 % (2577823)CaDiCaL version: 2.1.3
% 39.12/6.56 % (2577823)Termination reason: Instruction limit
% 39.12/6.56 % (2577823)Termination phase: Saturation
% 39.12/6.56 % (2577823)Time elapsed: 0.165 s
% 39.12/6.56 % (2577823)Peak memory usage: 90 MB
% 39.12/6.56 % (2577823)Instructions burned: 157 (million)
% 39.12/6.56 % (2577826)Instruction limit reached!
% 39.12/6.56 % (2577826)------------------------------
% 60.52/9.65 % (2577826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.52/9.65 % (2577826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.52/9.65 % (2577826)CaDiCaL version: 2.1.3
% 60.52/9.65 % (2577826)Termination reason: Instruction limit
% 60.52/9.65 % (2577826)Termination phase: Saturation
% 60.52/9.65 % (2577826)Time elapsed: 0.113 s
% 60.52/9.65 % (2577826)Peak memory usage: 89 MB
% 60.52/9.65 % (2577826)Instructions burned: 107 (million)
% 60.52/9.65 % (2577827)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2965616513:i=107_2987 on theBenchmark for (2987ds/107Mi)
% 60.52/9.65 % (2577827)Refutation not found, incomplete strategy
% 60.52/9.65 % (2577827)------------------------------
% 60.52/9.65 % (2577827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.52/9.65 % (2577827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.52/9.65 % (2577827)CaDiCaL version: 2.1.3
% 60.52/9.65 % (2577827)Termination reason: Refutation not found, incomplete strategy
% 60.52/9.65 % (2577827)Time elapsed: 0.002 s
% 60.52/9.65 % (2577827)Peak memory usage: 87 MB
% 60.52/9.65 % (2577831)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2891225730:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2985 on theBenchmark for (2985ds/242Mi)
% 60.52/9.65 % (2577832)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=284261420:cond=fast:i=5208:av=off_2984 on theBenchmark for (2984ds/5208Mi)
% 60.52/9.65 % (2577827)------------------------------
% 60.52/9.65 % (2577827)------------------------------
% 60.52/9.65 % (2577831)Instruction limit reached!
% 60.52/9.65 % (2577831)------------------------------
% 60.52/9.65 % (2577831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.52/9.65 % (2577831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.52/9.65 % (2577831)CaDiCaL version: 2.1.3
% 60.52/9.65 % (2577831)Termination reason: Instruction limit
% 60.52/9.65 % (2577831)Termination phase: Saturation
% 60.52/9.65 % (2577831)Time elapsed: 0.243 s
% 60.52/9.65 % (2577831)Peak memory usage: 90 MB
% 60.52/9.65 % (2577831)Instructions burned: 242 (million)
% 60.52/9.65 % (2577836)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=759461214:i=134:sd=2:doe=on:ss=axioms:sgt=14_2980 on theBenchmark for (2980ds/134Mi)
% 60.52/9.65 % (2577837)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3301592873:i=499:bd=all_2979 on theBenchmark for (2979ds/499Mi)
% 60.52/9.65 % (2577836)Instruction limit reached!
% 60.52/9.65 % (2577836)------------------------------
% 60.52/9.65 % (2577836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.52/9.65 % (2577836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.52/9.65 % (2577836)CaDiCaL version: 2.1.3
% 60.52/9.65 % (2577836)Termination reason: Instruction limit
% 60.52/9.65 % (2577836)Termination phase: Saturation
% 60.52/9.65 % (2577836)Time elapsed: 0.117 s
% 60.52/9.65 % (2577836)Peak memory usage: 89 MB
% 60.52/9.65 % (2577836)Instructions burned: 136 (million)
% 60.52/9.65 % (2577840)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1419133148:i=191:fgj=on:bd=all_2976 on theBenchmark for (2976ds/191Mi)
% 60.52/9.65 % (2577837)Instruction limit reached!
% 60.52/9.65 % (2577837)------------------------------
% 60.52/9.65 % (2577837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.52/9.65 % (2577837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.52/9.65 % (2577837)CaDiCaL version: 2.1.3
% 60.52/9.65 % (2577837)Termination reason: Instruction limit
% 60.52/9.65 % (2577837)Termination phase: Saturation
% 60.52/9.65 % (2577837)Time elapsed: 0.528 s
% 60.52/9.65 % (2577837)Peak memory usage: 94 MB
% 60.52/9.65 % (2577837)Instructions burned: 499 (million)
% 60.52/9.65 % (2577840)Instruction limit reached!
% 60.52/9.65 % (2577840)------------------------------
% 60.52/9.65 % (2577840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.52/9.65 % (2577840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.52/9.65 % (2577840)CaDiCaL version: 2.1.3
% 60.52/9.65 % (2577840)Termination reason: Instruction limit
% 60.52/9.65 % (2577840)Termination phase: Saturation
% 60.52/9.65 % (2577840)Time elapsed: 0.193 s
% 60.52/9.65 % (2577840)Peak memory usage: 91 MB
% 60.52/9.65 % (2577840)Instructions burned: 192 (million)
% 70.05/12.69 % (2577843)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2141721878:cond=on:i=156:bs=on:gtg=exists_all:er=known_2971 on theBenchmark for (2971ds/156Mi)
% 70.05/12.69 % (2577842)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3342911614:i=264:kws=precedence:fsr=off_2971 on theBenchmark for (2971ds/264Mi)
% 70.05/12.69 % (2577843)Instruction limit reached!
% 70.05/12.69 % (2577843)------------------------------
% 70.05/12.69 % (2577843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.05/12.69 % (2577843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.05/12.69 % (2577843)CaDiCaL version: 2.1.3
% 70.05/12.69 % (2577843)Termination reason: Instruction limit
% 70.05/12.69 % (2577843)Termination phase: Saturation
% 70.05/12.69 % (2577843)Time elapsed: 0.151 s
% 70.05/12.69 % (2577843)Peak memory usage: 89 MB
% 70.05/12.69 % (2577843)Instructions burned: 156 (million)
% 70.05/12.69 % (2577842)Instruction limit reached!
% 70.05/12.69 % (2577842)------------------------------
% 70.05/12.69 % (2577842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.05/12.69 % (2577842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.05/12.69 % (2577842)CaDiCaL version: 2.1.3
% 70.05/12.69 % (2577842)Termination reason: Instruction limit
% 70.05/12.69 % (2577842)Termination phase: Saturation
% 70.05/12.69 % (2577842)Time elapsed: 0.264 s
% 70.05/12.69 % (2577842)Peak memory usage: 92 MB
% 70.05/12.69 % (2577842)Instructions burned: 264 (million)
% 70.05/12.69 % (2577848)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=3712673627:i=3256:kws=precedence:bd=preordered:av=off_2966 on theBenchmark for (2966ds/3256Mi)
% 70.05/12.69 % (2577849)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2076432511:i=537:av=off:ss=included_2965 on theBenchmark for (2965ds/537Mi)
% 70.05/12.69 % (2577849)Instruction limit reached!
% 70.05/12.69 % (2577849)------------------------------
% 70.05/12.69 % (2577849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.05/12.69 % (2577849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.05/12.69 % (2577849)CaDiCaL version: 2.1.3
% 70.05/12.69 % (2577849)Termination reason: Instruction limit
% 70.05/12.69 % (2577849)Termination phase: Saturation
% 70.05/12.69 % (2577849)Time elapsed: 0.494 s
% 70.05/12.69 % (2577849)Peak memory usage: 93 MB
% 70.05/12.69 % (2577849)Instructions burned: 537 (million)
% 70.05/12.69 % (2577852)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=568268112:i=180:bd=preordered:av=off_2957 on theBenchmark for (2957ds/180Mi)
% 70.05/12.69 % (2577852)Instruction limit reached!
% 70.05/12.69 % (2577852)------------------------------
% 70.05/12.69 % (2577852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.05/12.69 % (2577852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.05/12.69 % (2577852)CaDiCaL version: 2.1.3
% 70.05/12.69 % (2577852)Termination reason: Instruction limit
% 70.05/12.69 % (2577852)Termination phase: Saturation
% 70.05/12.69 % (2577852)Time elapsed: 0.168 s
% 70.05/12.69 % (2577852)Peak memory usage: 88 MB
% 70.05/12.69 % (2577852)Instructions burned: 181 (million)
% 70.05/12.69 % (2577825)Instruction limit reached!
% 70.05/12.69 % (2577825)------------------------------
% 70.05/12.69 % (2577825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.05/12.69 % (2577825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.05/12.69 % (2577825)CaDiCaL version: 2.1.3
% 70.05/12.69 % (2577825)Termination reason: Instruction limit
% 70.05/12.69 % (2577825)Termination phase: Saturation
% 70.05/12.69 % (2577825)Time elapsed: 3.377 s
% 70.05/12.69 % (2577825)Peak memory usage: 150 MB
% 70.05/12.69 % (2577825)Instructions burned: 3394 (million)
% 70.05/12.69 % (2577854)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=1043149532:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2953 on theBenchmark for (2953ds/10307Mi)
% 70.05/12.69 % (2577855)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=1463638243:i=412:gtgl=4:gtg=exists_all_2952 on theBenchmark for (2952ds/412Mi)
% 70.05/12.69 % (2577855)Instruction limit reached!
% 70.05/12.69 % (2577855)------------------------------
% 70.05/12.69 % (2577855)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.05/12.69 % (2577855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.05/12.69 % (2577855)CaDiCaL version: 2.1.3
% 70.05/12.69 % (2577855)Termination reason: Instruction limit
% 70.05/12.69 % (2577855)Termination phase: Saturation
% 70.05/12.69 % (2577855)Time elapsed: 0.410 s
% 70.05/12.69 % (2577855)Peak memory usage: 94 MB
% 70.05/12.69 % (2577855)Instructions burned: 413 (million)
% 70.05/12.69 % (2577858)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=1536500202:s2pl=no:i=8478:s2at=4:nm=6_2944 on theBenchmark for (2944ds/8478Mi)
% 70.05/12.69 % (2577848)Instruction limit reached!
% 70.05/12.69 % (2577848)------------------------------
% 70.05/12.69 % (2577848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.05/12.69 % (2577848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.05/12.69 % (2577848)CaDiCaL version: 2.1.3
% 70.05/12.69 % (2577848)Termination reason: Instruction limit
% 70.05/12.69 % (2577848)Termination phase: Saturation
% 70.05/12.69 % (2577848)Time elapsed: 3.293 s
% 70.05/12.69 % (2577848)Peak memory usage: 149 MB
% 70.05/12.69 % (2577848)Instructions burned: 3256 (million)
% 70.05/12.69 % (2577832)Instruction limit reached!
% 70.05/12.69 % (2577832)------------------------------
% 70.05/12.69 % (2577832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.05/12.69 % (2577832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.05/12.69 % (2577832)CaDiCaL version: 2.1.3
% 70.05/12.69 % (2577832)Termination reason: Instruction limit
% 70.05/12.69 % (2577832)Termination phase: Saturation
% 70.05/12.69 % (2577832)Time elapsed: 5.383 s
% 70.05/12.69 % (2577832)Peak memory usage: 170 MB
% 70.05/12.69 % (2577832)Instructions burned: 5208 (million)
% 70.05/12.69 % (2577860)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=81681583:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2930 on theBenchmark for (2930ds/303Mi)
% 70.05/12.69 % (2577860)Refutation not found, incomplete strategy
% 70.05/12.69 % (2577860)------------------------------
% 70.05/12.69 % (2577860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.05/12.69 % (2577860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.05/12.69 % (2577860)CaDiCaL version: 2.1.3
% 70.05/12.69 % (2577860)Termination reason: Refutation not found, incomplete strategy
% 70.05/12.69 % (2577860)Time elapsed: 0.003 s
% 70.05/12.69 % (2577860)Peak memory usage: 88 MB
% 70.05/12.69 % (2577860)Instructions burned: 1 (million)
% 70.05/12.69 % (2577862)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=1866247726:st=4:i=720:sd=3:fsr=off:ss=axioms_2927 on theBenchmark for (2927ds/720Mi)
% 70.05/12.69 % (2577862)Refutation not found, incomplete strategy
% 70.05/12.69 % (2577862)------------------------------
% 70.05/12.69 % (2577862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.05/12.69 % (2577862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.05/12.69 % (2577862)CaDiCaL version: 2.1.3
% 70.05/12.69 % (2577862)Termination reason: Refutation not found, incomplete strategy
% 70.05/12.69 % (2577862)Time elapsed: 0.002 s
% 70.05/12.69 % (2577862)Peak memory usage: 88 MB
% 70.05/12.69 % (2577860)------------------------------
% 70.05/12.69 % (2577860)------------------------------
% 70.05/12.69 % (2577864)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=532018548:i=598:bs=on:bd=preordered:av=off:ss=axioms_2923 on theBenchmark for (2923ds/598Mi)
% 70.05/12.69 % (2577862)------------------------------
% 70.05/12.69 % (2577862)------------------------------
% 70.05/12.69 % (2577866)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=3030892907:i=2989:sd=3:ss=axioms:sgt=60_2920 on theBenchmark for (2920ds/2989Mi)
% 70.05/12.69 % (2577864)Instruction limit reached!
% 70.05/12.69 % (2577864)------------------------------
% 70.05/12.69 % (2577864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.05/12.69 % (2577864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.05/12.69 % (2577864)CaDiCaL version: 2.1.3
% 70.05/12.69 % (2577864)Termination reason: Instruction limit
% 70.05/12.69 % (2577864)Termination phase: Saturation
% 70.05/12.69 % (2577864)Time elapsed: 0.651 s
% 70.05/12.69 % (2577864)Peak memory usage: 94 MB
% 70.05/12.69 % (2577864)Instructions burned: 599 (million)
% 70.05/12.69 % (2577868)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=734261080:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2913 on theBenchmark for (2913ds/1997Mi)
% 70.05/12.69 % (2577868)Instruction limit reached!
% 70.05/12.69 % (2577868)------------------------------
% 70.05/12.69 % (2577868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.05/12.69 % (2577868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.05/12.69 % (2577868)CaDiCaL version: 2.1.3
% 70.05/12.69 % (2577868)Termination reason: Instruction limit
% 70.05/12.69 % (2577868)Termination phase: Saturation
% 70.05/12.69 % (2577868)Time elapsed: 2.091 s
% 70.05/12.69 % (2577868)Peak memory usage: 138 MB
% 70.05/12.69 % (2577868)Instructions burned: 1997 (million)
% 70.05/12.69 % (2577802)First to succeed.
% 70.05/12.69 % (2577802)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2577795"
% 70.05/12.69 % (2577870)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=1434438643:i=2088:bd=preordered:av=off_2889 on theBenchmark for (2889ds/2088Mi)
% 70.05/12.69 % (2577866)Instruction limit reached!
% 70.05/12.69 % (2577866)------------------------------
% 70.05/12.69 % (2577866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.05/12.69 % (2577866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.05/12.69 % (2577866)CaDiCaL version: 2.1.3
% 70.05/12.69 % (2577866)Termination reason: Instruction limit
% 70.05/12.69 % (2577866)Termination phase: Saturation
% 70.05/12.69 % (2577866)Time elapsed: 3.075 s
% 70.05/12.69 % (2577866)Peak memory usage: 147 MB
% 70.05/12.69 % (2577866)Instructions burned: 2989 (million)
% 70.05/12.69 % (2577800)Also succeeded, but the first one will report.
% 70.05/12.69 % (2577802)Refutation found. Thanks to Tanya!
% 70.05/12.69 % SZS status Unsatisfiable for theBenchmark
% 70.05/12.69 % SZS output start Proof for theBenchmark
% See solution above
% 82.95/12.94 % (2577802)------------------------------
% 82.95/12.94 % (2577802)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.95/12.94 % (2577802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.95/12.94 % (2577802)CaDiCaL version: 2.1.3
% 82.95/12.94 % (2577802)Termination reason: Refutation
% 82.95/12.94 % (2577802)Time elapsed: 10.849 s
% 82.95/12.94 % (2577802)Peak memory usage: 204 MB
% 82.95/12.94 % (2577802)Instructions burned: 10536 (million)
% 82.95/12.94 % (2577802)------------------------------
% 82.95/12.94 % (2577802)------------------------------
% 82.95/12.94 % (2577795)Success in time 11.63 s
% 82.95/12.94 % Vampire exiting
%------------------------------------------------------------------------------