%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT179-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 : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:46:09 AM UTC 2026
% Result : Unsatisfiable 47.19s 7.89s
% Output : Refutation 48.01s
% Verified :
% SZS Type : Refutation
% Derivation depth : 82
% Number of leaves : 20
% Syntax : Number of formulae : 599 ( 572 unt; 7 def)
% Number of atoms : 635 ( 615 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 74 ( 38 ~; 34 |; 0 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 12 ( 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 : 1286 ( 0 sgn1286 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : meet(X0,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',idempotence_of_meet) ).
fof(f2,axiom,
! [X0] : join(X0,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',idempotence_of_join) ).
fof(f3,axiom,
! [X0,X1] : meet(X0,join(X0,X1)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',absorption1) ).
fof(f4,axiom,
! [X0,X1] : join(X0,meet(X0,X1)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',absorption2) ).
fof(f5,axiom,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_of_meet) ).
fof(f6,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_of_join) ).
fof(f7,axiom,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_meet) ).
fof(f8,axiom,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X0,join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_join) ).
fof(f9,axiom,
! [X0] : join(X0,complement(X0)) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement_join) ).
fof(f10,axiom,
! [X0] : meet(X0,complement(X0)) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement_meet) ).
fof(f11,axiom,
! [X0,X1] :
( join(X0,X1) != one
| meet(X0,X1) != zero
| complement(X0) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meet_join_complement) ).
fof(f12,axiom,
! [X2,X0,X1] : meet(X0,join(X1,meet(X0,X2))) = meet(X0,join(X1,meet(X2,join(meet(X0,join(X1,X2)),meet(X1,X2))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',equation_H2) ).
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(f30,plain,
c = join(c,sF3),
inference(superposition,[],[f4,f26]) ).
fof(f32,plain,
! [X0,X1] : join(X1,meet(X0,X1)) = X1,
inference(superposition,[],[f4,f5]) ).
fof(f34,plain,
! [X0,X1] : meet(X1,join(X0,X1)) = X1,
inference(superposition,[],[f3,f6]) ).
fof(f35,plain,
! [X0,X1] : join(X0,X1) = join(join(X0,X1),X0),
inference(superposition,[],[f32,f3]) ).
fof(f39,plain,
a = join(a,sF3),
inference(superposition,[],[f32,f26]) ).
fof(f41,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X0,X1)),
inference(forward_demodulation,[],[f35,f6]) ).
fof(f42,plain,
b = meet(b,sF0),
inference(superposition,[],[f3,f15]) ).
fof(f43,plain,
! [X0,X1] : meet(X0,X1) = meet(meet(X0,X1),X0),
inference(superposition,[],[f34,f4]) ).
fof(f44,plain,
! [X0,X1] : meet(X1,X0) = meet(meet(X1,X0),X0),
inference(superposition,[],[f34,f32]) ).
fof(f48,plain,
! [X0,X1] : join(X1,X0) = join(join(X1,X0),X0),
inference(superposition,[],[f32,f34]) ).
fof(f50,plain,
! [X0,X1] : join(X1,X0) = join(X0,join(X1,X0)),
inference(forward_demodulation,[],[f48,f6]) ).
fof(f51,plain,
! [X0,X1] : meet(X1,X0) = meet(X0,meet(X1,X0)),
inference(forward_demodulation,[],[f44,f5]) ).
fof(f52,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X0,X1)),
inference(forward_demodulation,[],[f43,f5]) ).
fof(f53,plain,
! [X2,X0,X1] : join(X0,join(meet(X0,X1),X2)) = join(X0,X2),
inference(superposition,[],[f8,f4]) ).
fof(f54,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X1,X0),X2)),
inference(superposition,[],[f8,f32]) ).
fof(f67,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f6,f8]) ).
fof(f76,plain,
! [X0,X1] :
( join(X0,X1) != one
| meet(X1,X0) != zero
| complement(X1) = X0 ),
inference(superposition,[],[f11,f6]) ).
fof(f95,plain,
! [X0] : join(sF2,join(sF3,X0)) = join(sF4,X0),
inference(superposition,[],[f8,f23]) ).
fof(f96,plain,
sF3 = meet(sF3,sF4),
inference(superposition,[],[f34,f23]) ).
fof(f111,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X0,X1),X2)),
inference(superposition,[],[f7,f3]) ).
fof(f112,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X1,X0),X2)),
inference(superposition,[],[f7,f34]) ).
fof(f114,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X1,meet(X0,X2)),
inference(superposition,[],[f7,f5]) ).
fof(f116,plain,
! [X0] : meet(a,meet(sF0,X0)) = meet(sF1,X0),
inference(superposition,[],[f7,f17]) ).
fof(f118,plain,
! [X0] : meet(c,meet(a,X0)) = meet(sF3,X0),
inference(superposition,[],[f7,f26]) ).
fof(f123,plain,
! [X2,X0,X1] : join(X2,meet(X0,meet(X1,X2))) = X2,
inference(superposition,[],[f32,f7]) ).
fof(f125,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X2,meet(X0,X1)),
inference(superposition,[],[f5,f7]) ).
fof(f126,plain,
! [X2,X0,X1] : meet(X0,X1) = join(meet(X0,X1),meet(X0,meet(X1,X2))),
inference(superposition,[],[f4,f7]) ).
fof(f128,plain,
! [X2,X0,X1] : meet(X0,X1) = meet(X0,meet(X1,join(X2,meet(X0,X1)))),
inference(superposition,[],[f34,f7]) ).
fof(f134,plain,
! [X2,X0,X1] : meet(X2,join(X1,meet(X2,X0))) = meet(X2,join(X1,meet(X0,join(meet(X2,join(X0,X1)),meet(X1,X0))))),
inference(superposition,[],[f12,f6]) ).
fof(f142,plain,
! [X2,X0,X1] : meet(X2,join(X0,meet(X2,X1))) = meet(X2,join(X0,meet(X1,join(meet(join(X0,X1),X2),meet(X0,X1))))),
inference(superposition,[],[f12,f5]) ).
fof(f144,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(X1,join(X0,X2)))) = meet(X1,join(X0,meet(join(X0,X2),join(meet(X1,join(X0,join(X0,X2))),X0)))),
inference(superposition,[],[f12,f3]) ).
fof(f148,plain,
! [X2,X0,X1] : meet(X2,join(X1,meet(X2,X0))) = meet(X2,join(X1,meet(X0,join(meet(X2,join(X1,X0)),meet(X0,X1))))),
inference(superposition,[],[f12,f5]) ).
fof(f154,plain,
! [X2,X0,X1] : meet(X2,join(X0,meet(X2,X1))) = meet(X2,join(X0,meet(X1,join(meet(X0,X1),meet(X2,join(X0,X1)))))),
inference(superposition,[],[f12,f6]) ).
fof(f157,plain,
! [X2,X3,X0,X1] : meet(X3,join(join(X0,X1),meet(X3,X2))) = meet(X3,join(X0,join(X1,meet(X2,join(meet(X3,join(join(X0,X1),X2)),meet(join(X0,X1),X2)))))),
inference(superposition,[],[f12,f8]) ).
fof(f169,plain,
! [X2,X3,X0,X1] : meet(X3,join(join(X0,X1),meet(X3,X2))) = meet(X3,join(X0,join(X1,meet(X2,join(meet(join(X0,X1),X2),meet(X3,join(join(X0,X1),X2))))))),
inference(forward_demodulation,[],[f157,f6]) ).
fof(f175,plain,
! [X2,X0,X1] : meet(X2,join(X1,meet(X2,X0))) = meet(X2,join(X1,meet(X0,join(meet(X0,X1),meet(X2,join(X1,X0)))))),
inference(forward_demodulation,[],[f148,f6]) ).
fof(f179,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(X1,join(X0,X2)))) = meet(X1,join(X0,meet(join(X0,X2),join(X0,meet(X1,join(X0,join(X0,X2))))))),
inference(forward_demodulation,[],[f144,f6]) ).
fof(f181,plain,
! [X2,X0,X1] : meet(X2,join(X0,meet(X2,X1))) = meet(X2,join(X0,meet(X1,join(meet(X0,X1),meet(join(X0,X1),X2))))),
inference(forward_demodulation,[],[f142,f6]) ).
fof(f188,plain,
! [X2,X0,X1] : meet(X2,join(X1,meet(X2,X0))) = meet(X2,join(X1,meet(X0,join(meet(X1,X0),meet(X2,join(X0,X1)))))),
inference(forward_demodulation,[],[f134,f6]) ).
fof(f196,plain,
! [X2,X3,X0,X1] : meet(X3,join(join(X0,X1),meet(X3,X2))) = meet(X3,join(X0,join(X1,meet(X2,join(meet(join(X0,X1),X2),meet(X3,join(X0,join(X1,X2)))))))),
inference(forward_demodulation,[],[f169,f8]) ).
fof(f199,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(X1,join(X0,X2)))) = meet(X1,join(X0,meet(join(X0,X2),join(X0,meet(X1,join(X0,X2)))))),
inference(forward_demodulation,[],[f179,f41]) ).
fof(f207,plain,
! [X2,X3,X0,X1] : meet(X3,join(X0,join(X1,meet(X2,join(meet(join(X0,X1),X2),meet(X3,join(X0,join(X1,X2)))))))) = meet(X3,join(X0,join(X1,meet(X3,X2)))),
inference(forward_demodulation,[],[f196,f8]) ).
fof(f218,plain,
! [X0] : meet(X0,one) = X0,
inference(superposition,[],[f3,f9]) ).
fof(f220,plain,
! [X0,X1] : meet(X0,join(X1,meet(X0,complement(X1)))) = meet(X0,join(X1,meet(complement(X1),join(meet(X0,one),meet(X1,complement(X1)))))),
inference(superposition,[],[f12,f9]) ).
fof(f222,plain,
! [X0,X1] : one = join(X0,join(X1,complement(join(X0,X1)))),
inference(superposition,[],[f8,f9]) ).
fof(f224,plain,
! [X0,X1] : meet(X0,join(X1,meet(X0,complement(X1)))) = meet(X0,join(X1,meet(complement(X1),join(meet(X0,one),zero)))),
inference(forward_demodulation,[],[f220,f10]) ).
fof(f225,plain,
! [X0,X1] : meet(X0,join(X1,meet(X0,complement(X1)))) = meet(X0,join(X1,meet(complement(X1),join(zero,meet(X0,one))))),
inference(forward_demodulation,[],[f224,f6]) ).
fof(f226,plain,
! [X0,X1] : meet(X0,join(X1,meet(X0,complement(X1)))) = meet(X0,join(X1,meet(complement(X1),join(zero,X0)))),
inference(forward_demodulation,[],[f225,f218]) ).
fof(f239,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(X1,meet(X0,join(X1,X2))),
inference(superposition,[],[f111,f5]) ).
fof(f244,plain,
! [X2,X0,X1] : meet(join(X0,X2),X1) = join(meet(join(X0,X2),X1),meet(X0,X1)),
inference(superposition,[],[f32,f111]) ).
fof(f248,plain,
! [X2,X0,X1] : meet(join(X0,X2),X1) = join(meet(X0,X1),meet(join(X0,X2),X1)),
inference(forward_demodulation,[],[f244,f6]) ).
fof(f263,plain,
! [X0,X1] : meet(X0,meet(complement(X0),X1)) = meet(zero,X1),
inference(superposition,[],[f7,f10]) ).
fof(f265,plain,
! [X0] : join(X0,zero) = X0,
inference(superposition,[],[f4,f10]) ).
fof(f266,plain,
! [X0,X1] : zero = meet(X0,meet(X1,complement(meet(X0,X1)))),
inference(superposition,[],[f7,f10]) ).
fof(f267,plain,
! [X0,X1] : meet(X0,complement(join(X0,X1))) = meet(X0,zero),
inference(superposition,[],[f111,f10]) ).
fof(f276,plain,
! [X0] : join(zero,X0) = X0,
inference(superposition,[],[f6,f265]) ).
fof(f280,plain,
! [X0] : zero = meet(zero,X0),
inference(superposition,[],[f34,f265]) ).
fof(f283,plain,
! [X0,X1] : zero = meet(X0,meet(complement(X0),X1)),
inference(backward_demodulation,[],[f263,f280]) ).
fof(f285,plain,
! [X0,X1] : meet(X0,join(X1,meet(X0,complement(X1)))) = meet(X0,join(X1,meet(complement(X1),X0))),
inference(backward_demodulation,[],[f226,f276]) ).
fof(f301,plain,
! [X0] : zero = meet(X0,zero),
inference(superposition,[],[f32,f276]) ).
fof(f303,plain,
one = complement(zero),
inference(superposition,[],[f9,f276]) ).
fof(f307,plain,
! [X0,X1] : zero = meet(X0,complement(join(X0,X1))),
inference(backward_demodulation,[],[f267,f301]) ).
fof(f423,plain,
! [X0,X1] : zero = meet(X1,complement(join(X0,X1))),
inference(superposition,[],[f307,f6]) ).
fof(f433,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X0,complement(join(X1,X2))))) = meet(X0,join(X1,meet(complement(join(X1,X2)),join(meet(X0,join(X1,complement(join(X1,X2)))),zero)))),
inference(superposition,[],[f12,f307]) ).
fof(f434,plain,
! [X2,X0,X1] : meet(X0,meet(complement(join(X0,X1)),X2)) = meet(zero,X2),
inference(superposition,[],[f7,f307]) ).
fof(f440,plain,
! [X2,X0,X1] : zero = meet(X0,meet(complement(join(X0,X1)),X2)),
inference(forward_demodulation,[],[f434,f280]) ).
fof(f441,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X0,complement(join(X1,X2))))) = meet(X0,join(X1,meet(complement(join(X1,X2)),join(zero,meet(X0,join(X1,complement(join(X1,X2)))))))),
inference(forward_demodulation,[],[f433,f6]) ).
fof(f443,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X0,complement(join(X1,X2))))) = meet(X0,join(X1,meet(complement(join(X1,X2)),meet(X0,join(X1,complement(join(X1,X2))))))),
inference(forward_demodulation,[],[f441,f276]) ).
fof(f451,plain,
! [X0] : meet(one,X0) = X0,
inference(superposition,[],[f5,f218]) ).
fof(f484,plain,
! [X0] : one = join(X0,one),
inference(superposition,[],[f34,f451]) ).
fof(f581,plain,
! [X0,X1] : join(X0,one) = join(X0,complement(meet(X0,X1))),
inference(superposition,[],[f53,f9]) ).
fof(f590,plain,
! [X2,X0,X1] : join(meet(X0,X2),X1) = meet(join(meet(X0,X2),X1),join(X0,X1)),
inference(superposition,[],[f34,f53]) ).
fof(f597,plain,
! [X2,X0,X1] : join(meet(X0,X2),X1) = meet(join(X0,X1),join(meet(X0,X2),X1)),
inference(forward_demodulation,[],[f590,f5]) ).
fof(f601,plain,
! [X0,X1] : one = join(X0,complement(meet(X0,X1))),
inference(forward_demodulation,[],[f581,f484]) ).
fof(f612,plain,
! [X0,X1] : zero = meet(meet(X0,X1),complement(X0)),
inference(superposition,[],[f423,f4]) ).
fof(f642,plain,
! [X0,X1] : zero = meet(complement(X0),meet(X0,X1)),
inference(forward_demodulation,[],[f612,f5]) ).
fof(f645,plain,
! [X0,X1] : zero = meet(X0,meet(X1,complement(X0))),
inference(forward_demodulation,[],[f642,f125]) ).
fof(f682,plain,
! [X0,X1] : one = join(X1,complement(meet(X0,X1))),
inference(superposition,[],[f601,f5]) ).
fof(f705,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X0,complement(meet(X1,X2))))) = meet(X0,join(X1,meet(complement(meet(X1,X2)),join(meet(X0,one),meet(X1,complement(meet(X1,X2))))))),
inference(superposition,[],[f12,f601]) ).
fof(f718,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X0,complement(meet(X1,X2))))) = meet(X0,join(X1,meet(complement(meet(X1,X2)),join(X0,meet(X1,complement(meet(X1,X2))))))),
inference(forward_demodulation,[],[f705,f218]) ).
fof(f732,plain,
! [X2,X0,X1] : join(join(X1,X0),X2) = join(join(X1,X0),join(X0,X2)),
inference(superposition,[],[f54,f34]) ).
fof(f745,plain,
! [X0] : join(a,X0) = join(a,join(sF2,X0)),
inference(superposition,[],[f54,f25]) ).
fof(f748,plain,
! [X2,X0,X1] : join(X2,X0) = join(X2,join(X0,meet(X1,X2))),
inference(superposition,[],[f54,f6]) ).
fof(f792,plain,
! [X2,X0,X1] : join(join(X1,X0),X2) = join(X0,join(X2,join(X1,X0))),
inference(forward_demodulation,[],[f732,f67]) ).
fof(f805,plain,
! [X2,X0,X1] : join(X1,join(X0,X2)) = join(X0,join(X2,join(X1,X0))),
inference(forward_demodulation,[],[f792,f8]) ).
fof(f810,plain,
! [X0,X1] : zero = meet(X1,meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f266,f5]) ).
fof(f838,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X0,meet(X2,complement(meet(X1,X2)))))) = meet(X0,join(X1,meet(meet(X2,complement(meet(X1,X2))),join(meet(X0,join(X1,meet(X2,complement(meet(X1,X2))))),zero)))),
inference(superposition,[],[f12,f266]) ).
fof(f851,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X0,meet(X2,complement(meet(X1,X2)))))) = meet(X0,join(X1,meet(X2,meet(complement(meet(X1,X2)),join(meet(X0,join(X1,meet(X2,complement(meet(X1,X2))))),zero))))),
inference(forward_demodulation,[],[f838,f7]) ).
fof(f868,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X0,meet(X2,complement(meet(X1,X2)))))) = meet(X0,join(X1,meet(X2,meet(complement(meet(X1,X2)),join(zero,meet(X0,join(X1,meet(X2,complement(meet(X1,X2)))))))))),
inference(forward_demodulation,[],[f851,f6]) ).
fof(f873,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X0,meet(X2,complement(meet(X1,X2)))))) = meet(X0,join(X1,meet(X2,meet(complement(meet(X1,X2)),meet(X0,join(X1,meet(X2,complement(meet(X1,X2))))))))),
inference(forward_demodulation,[],[f868,f276]) ).
fof(f880,plain,
! [X0,X1] : one = join(join(X0,X1),complement(X0)),
inference(superposition,[],[f682,f3]) ).
fof(f927,plain,
! [X0,X1] : one = join(complement(X0),join(X0,X1)),
inference(forward_demodulation,[],[f880,f6]) ).
fof(f935,plain,
! [X0,X1] : one = join(X0,join(X1,complement(X0))),
inference(forward_demodulation,[],[f927,f67]) ).
fof(f939,plain,
! [X0,X1] : one = join(X1,join(X0,complement(join(X0,X1)))),
inference(superposition,[],[f222,f6]) ).
fof(f1010,plain,
! [X2,X0,X1] : meet(meet(X1,X0),X2) = meet(meet(X1,X0),meet(X0,X2)),
inference(superposition,[],[f112,f32]) ).
fof(f1022,plain,
! [X0] : meet(c,X0) = meet(c,meet(sF0,X0)),
inference(superposition,[],[f112,f15]) ).
fof(f1025,plain,
! [X2,X0,X1] : meet(X2,X0) = meet(X2,meet(X0,join(X1,X2))),
inference(superposition,[],[f112,f5]) ).
fof(f1079,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X0,complement(join(X1,X2))))) = meet(X0,join(X1,meet(complement(join(X1,X2)),X0))),
inference(backward_demodulation,[],[f443,f1025]) ).
fof(f1088,plain,
! [X2,X0,X1] : meet(meet(X1,X0),X2) = meet(X0,meet(X2,meet(X1,X0))),
inference(forward_demodulation,[],[f1010,f125]) ).
fof(f1101,plain,
! [X2,X0,X1] : meet(X1,meet(X0,X2)) = meet(X0,meet(X2,meet(X1,X0))),
inference(forward_demodulation,[],[f1088,f7]) ).
fof(f1536,plain,
! [X0,X1] :
( one != one
| zero != meet(X0,join(X1,complement(join(X1,X0))))
| complement(X0) = join(X1,complement(join(X1,X0))) ),
inference(superposition,[],[f11,f939]) ).
fof(f1551,plain,
! [X0,X1] :
( zero != meet(X0,join(X1,complement(join(X1,X0))))
| complement(X0) = join(X1,complement(join(X1,X0))) ),
inference(trivial_inequality_removal,[],[f1536]) ).
fof(f1670,plain,
! [X2,X0,X1] : meet(X2,X0) = meet(X0,meet(join(X1,X0),X2)),
inference(superposition,[],[f125,f34]) ).
fof(f1697,plain,
! [X0,X1] : meet(X1,X0) = meet(X0,meet(meet(X1,X0),X1)),
inference(superposition,[],[f1,f125]) ).
fof(f1758,plain,
! [X0,X1] : meet(X1,X0) = meet(X0,meet(X1,meet(X1,X0))),
inference(forward_demodulation,[],[f1697,f5]) ).
fof(f1813,plain,
! [X0,X1] : meet(X1,X0) = meet(X1,meet(X0,X1)),
inference(forward_demodulation,[],[f1758,f1101]) ).
fof(f1871,plain,
! [X2,X0,X1] : join(X2,X0) = join(X0,join(meet(X0,X1),X2)),
inference(superposition,[],[f67,f4]) ).
fof(f1872,plain,
! [X2,X0,X1] : join(X2,X0) = join(X0,join(meet(X1,X0),X2)),
inference(superposition,[],[f67,f32]) ).
fof(f1902,plain,
! [X0,X1] : join(X1,X0) = join(X0,join(join(X1,X0),X1)),
inference(superposition,[],[f2,f67]) ).
fof(f1963,plain,
! [X0,X1] : join(X1,X0) = join(X0,join(X1,join(X1,X0))),
inference(forward_demodulation,[],[f1902,f6]) ).
fof(f2012,plain,
! [X0,X1] : join(X1,X0) = join(X1,join(X0,X1)),
inference(forward_demodulation,[],[f1963,f805]) ).
fof(f2096,plain,
sF3 = meet(c,sF3),
inference(superposition,[],[f52,f26]) ).
fof(f2149,plain,
meet(sF3,sF0) = meet(c,sF1),
inference(superposition,[],[f118,f17]) ).
fof(f2221,plain,
meet(c,sF1) = meet(sF0,sF3),
inference(forward_demodulation,[],[f2149,f5]) ).
fof(f3162,plain,
sF1 = meet(sF0,sF1),
inference(superposition,[],[f51,f17]) ).
fof(f3358,plain,
! [X2,X3,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X1,meet(X2,join(X3,meet(X0,X1))))),
inference(superposition,[],[f7,f1025]) ).
fof(f3374,plain,
! [X2,X3,X0,X1] : meet(X0,meet(X1,X2)) = meet(X0,meet(X1,meet(X2,join(X3,meet(X0,X1))))),
inference(forward_demodulation,[],[f3358,f7]) ).
fof(f3420,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X0,meet(X2,complement(meet(X1,X2)))))) = meet(X0,join(X1,meet(X2,meet(complement(meet(X1,X2)),X0)))),
inference(backward_demodulation,[],[f873,f3374]) ).
fof(f3620,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X0,meet(complement(X1),X2)))) = meet(X0,join(X1,meet(meet(complement(X1),X2),join(zero,meet(X0,join(X1,meet(complement(X1),X2))))))),
inference(superposition,[],[f154,f283]) ).
fof(f3643,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X0,meet(complement(X1),X2)))) = meet(X0,join(X1,meet(complement(X1),meet(X2,join(zero,meet(X0,join(X1,meet(complement(X1),X2)))))))),
inference(forward_demodulation,[],[f3620,f7]) ).
fof(f3658,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X0,meet(complement(X1),X2)))) = meet(X0,join(X1,meet(complement(X1),meet(X2,meet(X0,join(X1,meet(complement(X1),X2))))))),
inference(forward_demodulation,[],[f3643,f276]) ).
fof(f3667,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(complement(X1),meet(X2,X0)))) = meet(X0,join(X1,meet(X0,meet(complement(X1),X2)))),
inference(forward_demodulation,[],[f3658,f3374]) ).
fof(f4024,plain,
! [X0] :
( one != one
| zero != meet(complement(X0),X0)
| complement(complement(X0)) = X0 ),
inference(superposition,[],[f76,f9]) ).
fof(f4043,plain,
! [X0] :
( zero != meet(complement(X0),X0)
| complement(complement(X0)) = X0 ),
inference(trivial_inequality_removal,[],[f4024]) ).
fof(f4056,plain,
! [X0] :
( meet(X0,complement(X0)) != zero
| complement(complement(X0)) = X0 ),
inference(forward_demodulation,[],[f4043,f5]) ).
fof(f4073,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_subsumption_resolution,[],[f4056,f10]) ).
fof(f4083,plain,
! [X0,X1] : meet(X1,join(complement(X0),meet(X1,X0))) = meet(X1,join(complement(X0),meet(X0,X1))),
inference(superposition,[],[f285,f4073]) ).
fof(f4329,plain,
! [X2,X0,X1] : meet(X0,zero) = meet(X0,meet(X1,complement(join(X0,X2)))),
inference(superposition,[],[f111,f645]) ).
fof(f4341,plain,
! [X2,X0,X1] : zero = meet(X0,meet(X1,complement(join(X0,X2)))),
inference(forward_demodulation,[],[f4329,f301]) ).
fof(f4383,plain,
! [X0] : meet(sF1,X0) = meet(a,meet(X0,sF0)),
inference(superposition,[],[f116,f5]) ).
fof(f4605,plain,
! [X2,X0,X1] : join(X0,one) = join(X0,join(X1,complement(meet(X2,X0)))),
inference(superposition,[],[f54,f935]) ).
fof(f4606,plain,
! [X2,X0,X1] : join(X0,one) = join(X0,join(X2,complement(meet(X0,X1)))),
inference(superposition,[],[f53,f935]) ).
fof(f4619,plain,
! [X2,X0,X1] : one = join(X0,join(X2,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f4606,f484]) ).
fof(f4620,plain,
! [X2,X0,X1] : one = join(X0,join(X1,complement(meet(X2,X0)))),
inference(forward_demodulation,[],[f4605,f484]) ).
fof(f4810,plain,
! [X0] : join(sF4,X0) = join(sF2,join(X0,sF3)),
inference(superposition,[],[f95,f6]) ).
fof(f5208,plain,
! [X2,X0,X1] : meet(X1,join(meet(X2,X0),meet(X1,X0))) = meet(X1,join(meet(X2,X0),meet(X0,join(meet(meet(X2,X0),X0),meet(X1,X0))))),
inference(superposition,[],[f188,f32]) ).
fof(f5222,plain,
! [X2,X0,X1] : meet(X0,join(complement(meet(X1,X2)),meet(X0,X1))) = meet(X0,join(complement(meet(X1,X2)),meet(X1,join(meet(complement(meet(X1,X2)),X1),meet(X0,one))))),
inference(superposition,[],[f188,f601]) ).
fof(f5244,plain,
! [X0,X1] : meet(X0,join(meet(X0,complement(X1)),meet(X0,X1))) = meet(X0,join(meet(X0,complement(X1)),meet(X1,join(meet(meet(X0,complement(X1)),X1),meet(X0,join(X1,meet(complement(X1),X0))))))),
inference(superposition,[],[f188,f285]) ).
fof(f5245,plain,
! [X0,X1] : meet(X0,join(meet(complement(X1),X0),meet(X0,X1))) = meet(X0,join(meet(complement(X1),X0),meet(X1,join(meet(meet(complement(X1),X0),X1),meet(X0,join(X1,meet(X0,complement(X1)))))))),
inference(superposition,[],[f188,f285]) ).
fof(f5246,plain,
! [X0,X1] : meet(X0,join(meet(X0,X1),meet(X0,complement(X1)))) = meet(X0,join(meet(X0,X1),meet(complement(X1),join(meet(meet(X0,X1),complement(X1)),meet(X0,join(complement(X1),meet(X1,X0))))))),
inference(superposition,[],[f188,f4083]) ).
fof(f5247,plain,
! [X0,X1] : meet(X0,join(meet(X1,X0),meet(X0,complement(X1)))) = meet(X0,join(meet(X1,X0),meet(complement(X1),join(meet(meet(X1,X0),complement(X1)),meet(X0,join(complement(X1),meet(X0,X1))))))),
inference(superposition,[],[f188,f4083]) ).
fof(f5331,plain,
! [X0,X1] : meet(X0,join(meet(X1,X0),meet(X0,complement(X1)))) = meet(X0,join(meet(X1,X0),meet(complement(X1),join(meet(complement(X1),meet(X1,X0)),meet(X0,join(complement(X1),meet(X0,X1))))))),
inference(forward_demodulation,[],[f5247,f5]) ).
fof(f5332,plain,
! [X0,X1] : meet(X0,join(meet(X0,X1),meet(X0,complement(X1)))) = meet(X0,join(meet(X0,X1),meet(complement(X1),join(meet(complement(X1),meet(X0,X1)),meet(X0,join(complement(X1),meet(X1,X0))))))),
inference(forward_demodulation,[],[f5246,f5]) ).
fof(f5333,plain,
! [X0,X1] : meet(X0,join(meet(complement(X1),X0),meet(X0,X1))) = meet(X0,join(meet(complement(X1),X0),meet(X1,join(meet(X1,meet(complement(X1),X0)),meet(X0,join(X1,meet(X0,complement(X1)))))))),
inference(forward_demodulation,[],[f5245,f5]) ).
fof(f5334,plain,
! [X0,X1] : meet(X0,join(meet(X0,complement(X1)),meet(X0,X1))) = meet(X0,join(meet(X0,complement(X1)),meet(X1,join(meet(X1,meet(X0,complement(X1))),meet(X0,join(X1,meet(complement(X1),X0))))))),
inference(forward_demodulation,[],[f5244,f5]) ).
fof(f5354,plain,
! [X2,X0,X1] : meet(X0,join(complement(meet(X1,X2)),meet(X0,X1))) = meet(X0,join(complement(meet(X1,X2)),meet(X1,join(meet(complement(meet(X1,X2)),X1),X0)))),
inference(forward_demodulation,[],[f5222,f218]) ).
fof(f5368,plain,
! [X2,X0,X1] : meet(X1,join(meet(X2,X0),meet(X1,X0))) = meet(X1,join(meet(X2,X0),meet(X0,join(meet(X0,meet(X2,X0)),meet(X1,X0))))),
inference(forward_demodulation,[],[f5208,f5]) ).
fof(f5433,plain,
! [X0,X1] : meet(X0,join(meet(X1,X0),meet(X0,complement(X1)))) = meet(X0,join(meet(X1,X0),meet(complement(X1),join(meet(X1,meet(X0,complement(X1))),meet(X0,join(complement(X1),meet(X0,X1))))))),
inference(forward_demodulation,[],[f5331,f125]) ).
fof(f5434,plain,
! [X0,X1] : meet(X0,join(meet(X0,X1),meet(X0,complement(X1)))) = meet(X0,join(meet(X0,X1),meet(complement(X1),join(meet(X1,meet(complement(X1),X0)),meet(X0,join(complement(X1),meet(X1,X0))))))),
inference(forward_demodulation,[],[f5332,f125]) ).
fof(f5435,plain,
! [X0,X1] : meet(X0,join(meet(complement(X1),X0),meet(X0,X1))) = meet(X0,join(meet(complement(X1),X0),meet(X1,join(zero,meet(X0,join(X1,meet(X0,complement(X1)))))))),
inference(forward_demodulation,[],[f5333,f283]) ).
fof(f5436,plain,
! [X0,X1] : meet(X0,join(meet(X0,complement(X1)),meet(X0,X1))) = meet(X0,join(meet(X0,complement(X1)),meet(X1,join(zero,meet(X0,join(X1,meet(complement(X1),X0))))))),
inference(forward_demodulation,[],[f5334,f645]) ).
fof(f5450,plain,
! [X2,X0,X1] : meet(X0,join(complement(meet(X1,X2)),meet(X0,X1))) = meet(X0,join(complement(meet(X1,X2)),meet(X1,join(meet(X1,complement(meet(X1,X2))),X0)))),
inference(forward_demodulation,[],[f5354,f5]) ).
fof(f5464,plain,
! [X2,X0,X1] : meet(X1,join(meet(X2,X0),meet(X1,X0))) = meet(X1,join(meet(X2,X0),meet(X0,join(meet(X2,X0),meet(X1,X0))))),
inference(forward_demodulation,[],[f5368,f51]) ).
fof(f5509,plain,
! [X0,X1] : meet(X0,join(meet(X1,X0),meet(X0,complement(X1)))) = meet(X0,join(meet(X1,X0),meet(complement(X1),join(zero,meet(X0,join(complement(X1),meet(X0,X1))))))),
inference(forward_demodulation,[],[f5433,f645]) ).
fof(f5510,plain,
! [X0,X1] : meet(X0,join(meet(X0,X1),meet(X0,complement(X1)))) = meet(X0,join(meet(X0,X1),meet(complement(X1),join(zero,meet(X0,join(complement(X1),meet(X1,X0))))))),
inference(forward_demodulation,[],[f5434,f283]) ).
fof(f5511,plain,
! [X0,X1] : meet(X0,join(meet(complement(X1),X0),meet(X0,X1))) = meet(X0,join(meet(complement(X1),X0),meet(X1,meet(X0,join(X1,meet(X0,complement(X1))))))),
inference(forward_demodulation,[],[f5435,f276]) ).
fof(f5512,plain,
! [X0,X1] : meet(X0,join(meet(X0,complement(X1)),meet(X0,X1))) = meet(X0,join(meet(X0,complement(X1)),meet(X1,meet(X0,join(X1,meet(complement(X1),X0)))))),
inference(forward_demodulation,[],[f5436,f276]) ).
fof(f5540,plain,
! [X0,X1] : meet(X0,join(meet(X1,X0),meet(X0,complement(X1)))) = meet(X0,join(meet(X1,X0),meet(complement(X1),meet(X0,join(complement(X1),meet(X0,X1)))))),
inference(forward_demodulation,[],[f5509,f276]) ).
fof(f5541,plain,
! [X0,X1] : meet(X0,join(meet(X0,X1),meet(X0,complement(X1)))) = meet(X0,join(meet(X0,X1),meet(complement(X1),meet(X0,join(complement(X1),meet(X1,X0)))))),
inference(forward_demodulation,[],[f5510,f276]) ).
fof(f5542,plain,
! [X0,X1] : meet(X0,join(meet(complement(X1),X0),meet(X0,X1))) = meet(X0,join(meet(complement(X1),X0),meet(X1,X0))),
inference(forward_demodulation,[],[f5511,f239]) ).
fof(f5543,plain,
! [X0,X1] : meet(X0,join(meet(X0,complement(X1)),meet(X0,X1))) = meet(X0,join(meet(X0,complement(X1)),meet(X1,X0))),
inference(forward_demodulation,[],[f5512,f239]) ).
fof(f5551,plain,
! [X0,X1] : meet(X0,join(meet(X1,X0),meet(X0,complement(X1)))) = meet(X0,join(meet(X1,X0),meet(complement(X1),X0))),
inference(forward_demodulation,[],[f5540,f239]) ).
fof(f5552,plain,
! [X0,X1] : meet(X0,join(meet(X0,X1),meet(X0,complement(X1)))) = meet(X0,join(meet(X0,X1),meet(complement(X1),X0))),
inference(forward_demodulation,[],[f5541,f239]) ).
fof(f5553,plain,
! [X0,X1] : meet(X0,join(meet(complement(X1),X0),meet(X0,X1))) = meet(X0,join(meet(X1,X0),meet(complement(X1),X0))),
inference(forward_demodulation,[],[f5542,f6]) ).
fof(f5554,plain,
! [X0,X1] : meet(X0,join(meet(X0,complement(X1)),meet(X0,X1))) = meet(X0,join(meet(X1,X0),meet(X0,complement(X1)))),
inference(forward_demodulation,[],[f5543,f6]) ).
fof(f5556,plain,
! [X0,X1] : meet(X0,join(meet(X1,X0),meet(complement(X1),X0))) = meet(X0,join(meet(X0,X1),meet(complement(X1),X0))),
inference(forward_demodulation,[],[f5553,f6]) ).
fof(f5557,plain,
! [X0,X1] : meet(X0,join(meet(X0,X1),meet(X0,complement(X1)))) = meet(X0,join(meet(X1,X0),meet(X0,complement(X1)))),
inference(forward_demodulation,[],[f5554,f6]) ).
fof(f5673,plain,
! [X2,X0,X1] : meet(X0,join(complement(join(X1,X2)),meet(X0,X1))) = meet(X0,join(complement(join(X1,X2)),meet(X1,join(zero,meet(X0,join(complement(join(X1,X2)),X1)))))),
inference(superposition,[],[f175,f307]) ).
fof(f5892,plain,
! [X2,X0,X1] : meet(X0,join(complement(join(X1,X2)),meet(X0,X1))) = meet(X0,join(complement(join(X1,X2)),meet(X1,meet(X0,join(complement(join(X1,X2)),X1))))),
inference(forward_demodulation,[],[f5673,f276]) ).
fof(f5968,plain,
! [X2,X0,X1] : meet(X0,join(complement(join(X1,X2)),meet(X0,X1))) = meet(X0,join(complement(join(X1,X2)),meet(X1,X0))),
inference(forward_demodulation,[],[f5892,f1025]) ).
fof(f6081,plain,
join(a,sF3) = join(a,sF4),
inference(superposition,[],[f745,f23]) ).
fof(f6182,plain,
a = join(a,sF4),
inference(forward_demodulation,[],[f6081,f39]) ).
fof(f6217,plain,
sF4 = meet(sF4,a),
inference(superposition,[],[f34,f6182]) ).
fof(f6247,plain,
sF4 = meet(a,sF4),
inference(forward_demodulation,[],[f6217,f5]) ).
fof(f6257,plain,
meet(sF3,sF4) = meet(c,sF4),
inference(superposition,[],[f118,f6247]) ).
fof(f6283,plain,
sF3 = meet(c,sF4),
inference(forward_demodulation,[],[f6257,f96]) ).
fof(f6571,plain,
! [X2,X3,X0,X1] : meet(meet(X1,X0),X3) = meet(X0,meet(X1,meet(join(X2,meet(X1,X0)),X3))),
inference(superposition,[],[f112,f114]) ).
fof(f6632,plain,
! [X2,X3,X0,X1] : meet(X1,meet(X0,X3)) = meet(X0,meet(X1,meet(join(X2,meet(X1,X0)),X3))),
inference(forward_demodulation,[],[f6571,f7]) ).
fof(f7418,plain,
! [X2,X0,X1] : meet(meet(join(X0,X1),X2),join(X0,meet(meet(join(X0,X1),X2),X1))) = meet(meet(join(X0,X1),X2),join(X0,meet(X1,join(meet(X0,X1),meet(join(X0,X1),X2))))),
inference(superposition,[],[f181,f52]) ).
fof(f7579,plain,
! [X2,X0,X1] : meet(meet(join(X0,X1),X2),join(X0,meet(meet(join(X0,X1),X2),X1))) = meet(join(X0,X1),meet(X2,join(X0,meet(X1,join(meet(X0,X1),meet(join(X0,X1),X2)))))),
inference(forward_demodulation,[],[f7418,f7]) ).
fof(f7701,plain,
! [X2,X0,X1] : meet(meet(join(X0,X1),X2),join(X0,meet(meet(join(X0,X1),X2),X1))) = meet(join(X0,X1),meet(X2,join(X0,meet(X2,X1)))),
inference(forward_demodulation,[],[f7579,f181]) ).
fof(f7763,plain,
! [X2,X0,X1] : meet(join(X0,X1),meet(X2,join(X0,meet(X2,X1)))) = meet(join(X0,X1),meet(X2,join(X0,meet(meet(join(X0,X1),X2),X1)))),
inference(forward_demodulation,[],[f7701,f7]) ).
fof(f7801,plain,
! [X2,X0,X1] : meet(join(X0,X1),meet(X2,join(X0,meet(X2,X1)))) = meet(join(X0,X1),meet(X2,join(X0,meet(X1,meet(join(X0,X1),X2))))),
inference(forward_demodulation,[],[f7763,f5]) ).
fof(f7824,plain,
! [X2,X0,X1] : meet(join(X0,X1),meet(X2,join(X0,meet(X2,X1)))) = meet(join(X0,X1),meet(X2,join(X0,meet(X1,X2)))),
inference(forward_demodulation,[],[f7801,f112]) ).
fof(f7994,plain,
! [X0,X1] : meet(X1,X0) = join(meet(X1,X0),meet(X0,X1)),
inference(superposition,[],[f126,f51]) ).
fof(f8179,plain,
! [X2,X0,X1] : join(meet(X1,X2),X0) = meet(join(X0,X1),join(meet(X1,X2),X0)),
inference(superposition,[],[f597,f6]) ).
fof(f8180,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(X0,X1),meet(X0,X2))),
inference(superposition,[],[f597,f4]) ).
fof(f8181,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,X0)) = meet(X0,join(meet(X0,X1),meet(X2,X0))),
inference(superposition,[],[f597,f32]) ).
fof(f8401,plain,
! [X0,X1] : meet(X0,join(meet(X1,X0),meet(complement(X1),X0))) = join(meet(X0,X1),meet(complement(X1),X0)),
inference(backward_demodulation,[],[f5556,f8181]) ).
fof(f8402,plain,
! [X0,X1] : meet(X0,join(meet(X0,X1),meet(X0,complement(X1)))) = join(meet(X0,X1),meet(complement(X1),X0)),
inference(backward_demodulation,[],[f5552,f8181]) ).
fof(f8403,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,complement(X1))) = meet(X0,join(meet(X1,X0),meet(X0,complement(X1)))),
inference(backward_demodulation,[],[f5557,f8180]) ).
fof(f8451,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,complement(X1))) = join(meet(X0,X1),meet(complement(X1),X0)),
inference(forward_demodulation,[],[f8402,f8180]) ).
fof(f8452,plain,
! [X0,X1] : meet(X0,join(meet(X1,X0),meet(X0,complement(X1)))) = join(meet(X0,X1),meet(complement(X1),X0)),
inference(backward_demodulation,[],[f5551,f8401]) ).
fof(f8505,plain,
! [X2,X0,X1] : join(meet(meet(join(X0,X2),X1),X0),meet(meet(join(X0,X2),X1),complement(X0))) = meet(meet(join(X0,X2),X1),join(meet(X0,X1),meet(meet(join(X0,X2),X1),complement(X0)))),
inference(superposition,[],[f8403,f111]) ).
fof(f8697,plain,
! [X2,X0,X1] : join(meet(meet(join(X0,X2),X1),X0),meet(meet(join(X0,X2),X1),complement(X0))) = meet(join(X0,X2),meet(X1,join(meet(X0,X1),meet(meet(join(X0,X2),X1),complement(X0))))),
inference(forward_demodulation,[],[f8505,f7]) ).
fof(f8786,plain,
! [X2,X0,X1] : join(meet(meet(join(X0,X2),X1),X0),meet(complement(X0),meet(join(X0,X2),X1))) = meet(join(X0,X2),meet(X1,join(meet(X0,X1),meet(complement(X0),meet(join(X0,X2),X1))))),
inference(forward_demodulation,[],[f8697,f5]) ).
fof(f8850,plain,
! [X2,X0,X1] : meet(join(X0,X2),meet(X1,join(meet(X0,X1),meet(complement(X0),meet(join(X0,X2),X1))))) = join(meet(X0,meet(join(X0,X2),X1)),meet(complement(X0),meet(join(X0,X2),X1))),
inference(forward_demodulation,[],[f8786,f5]) ).
fof(f8900,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(complement(X0),meet(join(X0,X2),X1))) = meet(join(X0,X2),meet(X1,join(meet(X0,X1),meet(complement(X0),meet(join(X0,X2),X1))))),
inference(forward_demodulation,[],[f8850,f111]) ).
fof(f9334,plain,
! [X2,X0,X1] : meet(X1,join(complement(join(X0,X2)),meet(X1,X0))) = meet(X1,join(meet(X0,X1),complement(join(X0,X2)))),
inference(superposition,[],[f5968,f6]) ).
fof(f9342,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),meet(X0,complement(join(X1,X2))))) = meet(X0,join(meet(X0,X1),meet(complement(join(X1,X2)),join(meet(meet(X0,X1),complement(join(X1,X2))),meet(X0,join(complement(join(X1,X2)),meet(X1,X0))))))),
inference(superposition,[],[f188,f5968]) ).
fof(f9386,plain,
! [X2,X0,X1] : meet(X0,join(meet(X1,X0),meet(X0,complement(join(X1,X2))))) = meet(X0,join(meet(X1,X0),meet(complement(join(X1,X2)),join(meet(meet(X1,X0),complement(join(X1,X2))),meet(X0,join(complement(join(X1,X2)),meet(X0,X1))))))),
inference(superposition,[],[f188,f5968]) ).
fof(f9457,plain,
! [X2,X0,X1] : meet(X0,join(meet(X1,X0),meet(X0,complement(join(X1,X2))))) = meet(X0,join(meet(X1,X0),meet(complement(join(X1,X2)),join(meet(X1,meet(X0,complement(join(X1,X2)))),meet(X0,join(complement(join(X1,X2)),meet(X0,X1))))))),
inference(forward_demodulation,[],[f9386,f7]) ).
fof(f9487,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),meet(X0,complement(join(X1,X2))))) = meet(X0,join(meet(X0,X1),meet(complement(join(X1,X2)),join(meet(X0,meet(X1,complement(join(X1,X2)))),meet(X0,join(complement(join(X1,X2)),meet(X1,X0))))))),
inference(forward_demodulation,[],[f9342,f7]) ).
fof(f9535,plain,
! [X2,X0,X1] : meet(X0,join(meet(X1,X0),meet(X0,complement(join(X1,X2))))) = meet(X0,join(meet(X1,X0),meet(complement(join(X1,X2)),join(zero,meet(X0,join(complement(join(X1,X2)),meet(X0,X1))))))),
inference(forward_demodulation,[],[f9457,f4341]) ).
fof(f9552,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),meet(X0,complement(join(X1,X2))))) = meet(X0,join(meet(X0,X1),meet(complement(join(X1,X2)),join(meet(X0,zero),meet(X0,join(complement(join(X1,X2)),meet(X1,X0))))))),
inference(forward_demodulation,[],[f9487,f307]) ).
fof(f9586,plain,
! [X2,X0,X1] : meet(X0,join(meet(X1,X0),meet(X0,complement(join(X1,X2))))) = meet(X0,join(meet(X1,X0),meet(complement(join(X1,X2)),meet(X0,join(complement(join(X1,X2)),meet(X0,X1)))))),
inference(forward_demodulation,[],[f9535,f276]) ).
fof(f9593,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),meet(X0,complement(join(X1,X2))))) = meet(X0,join(meet(X0,X1),meet(complement(join(X1,X2)),join(zero,meet(X0,join(complement(join(X1,X2)),meet(X1,X0))))))),
inference(forward_demodulation,[],[f9552,f301]) ).
fof(f9618,plain,
! [X2,X0,X1] : meet(X0,join(meet(X1,X0),meet(X0,complement(join(X1,X2))))) = meet(X0,join(meet(X1,X0),meet(complement(join(X1,X2)),X0))),
inference(forward_demodulation,[],[f9586,f239]) ).
fof(f9624,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),meet(X0,complement(join(X1,X2))))) = meet(X0,join(meet(X0,X1),meet(complement(join(X1,X2)),meet(X0,join(complement(join(X1,X2)),meet(X1,X0)))))),
inference(forward_demodulation,[],[f9593,f276]) ).
fof(f9637,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),meet(X0,complement(join(X1,X2))))) = meet(X0,join(meet(X0,X1),meet(complement(join(X1,X2)),X0))),
inference(forward_demodulation,[],[f9624,f239]) ).
fof(f9645,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),meet(X0,complement(join(X1,X2))))) = join(meet(X0,X1),meet(complement(join(X1,X2)),X0)),
inference(forward_demodulation,[],[f9637,f8181]) ).
fof(f9649,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,complement(join(X1,X2)))) = join(meet(X0,X1),meet(complement(join(X1,X2)),X0)),
inference(forward_demodulation,[],[f9645,f8180]) ).
fof(f9912,plain,
meet(c,sF3) = meet(c,meet(c,sF1)),
inference(superposition,[],[f1022,f2221]) ).
fof(f10056,plain,
meet(c,sF3) = meet(c,sF1),
inference(forward_demodulation,[],[f9912,f52]) ).
fof(f10084,plain,
sF3 = meet(c,sF1),
inference(forward_demodulation,[],[f10056,f2096]) ).
fof(f10118,plain,
sF1 = join(sF1,sF3),
inference(superposition,[],[f32,f10084]) ).
fof(f10274,plain,
! [X2,X0,X1] : meet(join(X1,X2),X0) = join(meet(X0,X1),meet(join(X1,X2),X0)),
inference(superposition,[],[f248,f5]) ).
fof(f10289,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X0,X2)) = join(X0,meet(join(X0,X1),join(X0,X2))),
inference(superposition,[],[f248,f3]) ).
fof(f10290,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X2,X0)) = join(X0,meet(join(X0,X1),join(X2,X0))),
inference(superposition,[],[f248,f34]) ).
fof(f10544,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(X1,join(X0,X2)))) = meet(X1,meet(join(X0,X2),join(X0,meet(X1,join(X0,X2))))),
inference(backward_demodulation,[],[f199,f10289]) ).
fof(f10602,plain,
! [X2,X0,X1] : meet(X1,join(X0,X2)) = meet(X1,join(X0,meet(X1,join(X0,X2)))),
inference(forward_demodulation,[],[f10544,f128]) ).
fof(f10747,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,join(X1,X2)),meet(X0,X1))) = meet(X0,join(meet(X0,join(X1,X2)),meet(X1,join(meet(meet(X0,join(X1,X2)),X1),meet(X0,join(X1,X2)))))),
inference(superposition,[],[f188,f10602]) ).
fof(f10822,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,join(X1,X2)),meet(X0,X1))) = meet(X0,join(meet(X0,join(X1,X2)),meet(X1,join(meet(X0,join(X1,X2)),meet(meet(X0,join(X1,X2)),X1))))),
inference(forward_demodulation,[],[f10747,f6]) ).
fof(f10865,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,join(X1,X2)),meet(X0,X1))) = meet(X0,join(meet(X0,join(X1,X2)),meet(X1,meet(X0,join(X1,X2))))),
inference(forward_demodulation,[],[f10822,f4]) ).
fof(f10874,plain,
! [X2,X0,X1] : meet(X0,meet(X0,join(X1,X2))) = meet(X0,join(meet(X0,join(X1,X2)),meet(X0,X1))),
inference(forward_demodulation,[],[f10865,f32]) ).
fof(f10877,plain,
! [X2,X0,X1] : meet(X0,meet(X0,join(X1,X2))) = join(meet(X0,join(X1,X2)),meet(X0,X1)),
inference(forward_demodulation,[],[f10874,f8180]) ).
fof(f10879,plain,
! [X2,X0,X1] : meet(X0,meet(X0,join(X1,X2))) = join(meet(X0,X1),meet(X0,join(X1,X2))),
inference(forward_demodulation,[],[f10877,f6]) ).
fof(f10881,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = join(meet(X0,X1),meet(X0,join(X1,X2))),
inference(forward_demodulation,[],[f10879,f52]) ).
fof(f10886,plain,
! [X2,X0,X1] : meet(X1,join(meet(X0,X1),X2)) = join(meet(X0,X1),meet(X1,join(meet(X0,X1),X2))),
inference(superposition,[],[f10881,f51]) ).
fof(f10954,plain,
! [X2,X0,X1] : meet(X2,join(X0,X1)) = join(meet(X2,X1),meet(X2,join(X0,X1))),
inference(superposition,[],[f10881,f50]) ).
fof(f11128,plain,
! [X2,X0,X1] : meet(X1,join(meet(X2,X0),meet(X1,X0))) = meet(X1,meet(X0,join(meet(X2,X0),meet(X1,X0)))),
inference(backward_demodulation,[],[f5464,f10886]) ).
fof(f11167,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(X1,join(meet(X2,X0),meet(X1,X0))),
inference(forward_demodulation,[],[f11128,f128]) ).
fof(f11271,plain,
meet(a,b) = meet(sF1,b),
inference(superposition,[],[f4383,f42]) ).
fof(f11341,plain,
meet(a,b) = meet(b,sF1),
inference(forward_demodulation,[],[f11271,f5]) ).
fof(f11361,plain,
meet(b,a) = meet(b,sF1),
inference(forward_demodulation,[],[f11341,f5]) ).
fof(f11370,plain,
sF2 = meet(b,sF1),
inference(forward_demodulation,[],[f11361,f25]) ).
fof(f11406,plain,
sF1 = join(sF1,sF2),
inference(superposition,[],[f32,f11370]) ).
fof(f12880,plain,
! [X2,X0,X1] : meet(X0,join(meet(complement(join(X1,X2)),X0),meet(X0,X1))) = meet(X0,join(meet(complement(join(X1,X2)),X0),meet(X1,join(meet(meet(complement(join(X1,X2)),X0),X1),meet(X0,join(X1,meet(X0,complement(join(X1,X2))))))))),
inference(superposition,[],[f188,f1079]) ).
fof(f12960,plain,
! [X2,X0,X1] : meet(X0,join(meet(complement(join(X1,X2)),X0),meet(X0,X1))) = meet(X0,join(meet(complement(join(X1,X2)),X0),meet(X1,join(meet(X1,meet(complement(join(X1,X2)),X0)),meet(X0,join(X1,meet(X0,complement(join(X1,X2))))))))),
inference(forward_demodulation,[],[f12880,f5]) ).
fof(f13035,plain,
! [X2,X0,X1] : meet(X0,join(meet(complement(join(X1,X2)),X0),meet(X0,X1))) = meet(X0,join(meet(complement(join(X1,X2)),X0),meet(X1,join(zero,meet(X0,join(X1,meet(X0,complement(join(X1,X2))))))))),
inference(forward_demodulation,[],[f12960,f440]) ).
fof(f13086,plain,
! [X2,X0,X1] : meet(X0,join(meet(complement(join(X1,X2)),X0),meet(X0,X1))) = meet(X0,join(meet(complement(join(X1,X2)),X0),meet(X1,meet(X0,join(X1,meet(X0,complement(join(X1,X2)))))))),
inference(forward_demodulation,[],[f13035,f276]) ).
fof(f13112,plain,
! [X2,X0,X1] : meet(X0,join(meet(complement(join(X1,X2)),X0),meet(X0,X1))) = meet(X0,join(meet(complement(join(X1,X2)),X0),meet(X1,X0))),
inference(forward_demodulation,[],[f13086,f239]) ).
fof(f13131,plain,
! [X2,X0,X1] : meet(X0,join(meet(X1,X0),meet(complement(join(X1,X2)),X0))) = meet(X0,join(meet(complement(join(X1,X2)),X0),meet(X0,X1))),
inference(forward_demodulation,[],[f13112,f6]) ).
fof(f13136,plain,
! [X2,X0,X1] : meet(X0,join(meet(X1,X0),meet(complement(join(X1,X2)),X0))) = meet(X0,join(meet(X0,X1),meet(complement(join(X1,X2)),X0))),
inference(forward_demodulation,[],[f13131,f6]) ).
fof(f13141,plain,
! [X2,X0,X1] : meet(X0,join(meet(X1,X0),meet(complement(join(X1,X2)),X0))) = join(meet(X0,X1),meet(complement(join(X1,X2)),X0)),
inference(forward_demodulation,[],[f13136,f8181]) ).
fof(f13144,plain,
! [X2,X0,X1] : meet(X0,join(meet(X1,X0),meet(X0,complement(join(X1,X2))))) = join(meet(X0,X1),meet(complement(join(X1,X2)),X0)),
inference(backward_demodulation,[],[f9618,f13141]) ).
fof(f13228,plain,
! [X2,X3,X0,X1] : join(meet(meet(X0,join(X1,X2)),X3),meet(X0,X1)) = meet(meet(X0,join(X1,X2)),join(meet(meet(X0,join(X1,X2)),X3),meet(X0,X1))),
inference(superposition,[],[f8179,f10881]) ).
fof(f13294,plain,
! [X0,X1] : join(X0,X1) = meet(join(X1,X0),join(X0,X1)),
inference(superposition,[],[f8179,f218]) ).
fof(f13493,plain,
! [X2,X3,X0,X1] : join(meet(meet(X0,join(X1,X2)),X3),meet(X0,X1)) = meet(X0,meet(join(X1,X2),join(meet(meet(X0,join(X1,X2)),X3),meet(X0,X1)))),
inference(forward_demodulation,[],[f13228,f7]) ).
fof(f13565,plain,
! [X2,X3,X0,X1] : join(meet(X0,X1),meet(meet(X0,join(X1,X2)),X3)) = meet(X0,meet(join(X1,X2),join(meet(X0,X1),meet(meet(X0,join(X1,X2)),X3)))),
inference(forward_demodulation,[],[f13493,f6]) ).
fof(f13602,plain,
! [X2,X3,X0,X1] : join(meet(X0,X1),meet(X0,meet(join(X1,X2),X3))) = meet(X0,meet(join(X1,X2),join(meet(X0,X1),meet(X0,meet(join(X1,X2),X3))))),
inference(forward_demodulation,[],[f13565,f7]) ).
fof(f14092,plain,
join(sF2,c) = join(sF4,c),
inference(superposition,[],[f4810,f30]) ).
fof(f14093,plain,
join(sF2,sF1) = join(sF4,sF1),
inference(superposition,[],[f4810,f10118]) ).
fof(f14168,plain,
join(sF2,sF1) = join(sF1,sF4),
inference(forward_demodulation,[],[f14093,f6]) ).
fof(f14169,plain,
join(sF2,c) = join(c,sF4),
inference(forward_demodulation,[],[f14092,f6]) ).
fof(f14188,plain,
join(sF1,sF2) = join(sF1,sF4),
inference(forward_demodulation,[],[f14168,f6]) ).
fof(f14189,plain,
join(c,sF2) = join(c,sF4),
inference(forward_demodulation,[],[f14169,f6]) ).
fof(f14198,plain,
sF1 = join(sF1,sF4),
inference(forward_demodulation,[],[f14188,f11406]) ).
fof(f14210,plain,
sF4 = meet(sF4,sF1),
inference(superposition,[],[f34,f14198]) ).
fof(f14253,plain,
sF4 = meet(sF1,sF4),
inference(forward_demodulation,[],[f14210,f5]) ).
fof(f14297,plain,
one = join(sF1,complement(sF4)),
inference(superposition,[],[f601,f14253]) ).
fof(f16250,plain,
! [X2,X0,X1] : join(meet(X1,X0),X2) = join(meet(X1,X0),join(meet(X0,X1),X2)),
inference(superposition,[],[f54,f1813]) ).
fof(f17778,plain,
( one != one
| zero != meet(complement(sF4),sF1)
| sF1 = complement(complement(sF4)) ),
inference(superposition,[],[f76,f14297]) ).
fof(f17807,plain,
( zero != meet(complement(sF4),sF1)
| sF1 = complement(complement(sF4)) ),
inference(trivial_inequality_removal,[],[f17778]) ).
fof(f17835,plain,
( zero != meet(sF1,complement(sF4))
| sF1 = complement(complement(sF4)) ),
inference(forward_demodulation,[],[f17807,f5]) ).
fof(f17843,definition,
( spl5_56
<=> complement(sF4) = complement(sF1) ),
introduced(definition,[new_symbols(definition,[spl5_56])],[avatar_definition]) ).
fof(f17845,plain,
( complement(sF4) = complement(sF1)
| ~ spl5_56 ),
inference(avatar_component_clause,[],[f17843]) ).
fof(f17847,definition,
( spl5_57
<=> zero = meet(sF1,complement(sF4)) ),
introduced(definition,[new_symbols(definition,[spl5_57])],[avatar_definition]) ).
fof(f17849,plain,
( zero != meet(sF1,complement(sF4))
| spl5_57 ),
inference(avatar_component_clause,[],[f17847]) ).
fof(f17873,plain,
( sF1 = sF4
| zero != meet(sF1,complement(sF4)) ),
inference(forward_demodulation,[],[f17835,f4073]) ).
fof(f17886,plain,
zero != meet(sF1,complement(sF4)),
inference(forward_subsumption_resolution,[],[f17873,f24]) ).
fof(f17892,plain,
~ spl5_57,
inference(avatar_split_clause,[],[f17886,f17847]) ).
fof(f18142,plain,
! [X0,X1] : zero = meet(join(X1,X0),complement(join(X0,X1))),
inference(superposition,[],[f423,f2012]) ).
fof(f18419,plain,
! [X2,X0,X1] : meet(X1,X0) = join(meet(X1,X0),meet(X2,meet(X0,X1))),
inference(superposition,[],[f123,f1813]) ).
fof(f20208,plain,
! [X2,X0,X1] : meet(X2,meet(X1,X0)) = meet(X2,join(meet(X0,X1),meet(X2,meet(X1,X0)))),
inference(superposition,[],[f11167,f1813]) ).
fof(f20583,plain,
! [X2,X0,X1] : meet(X2,meet(X0,X1)) = meet(X2,meet(X1,X0)),
inference(forward_demodulation,[],[f20208,f18419]) ).
fof(f20856,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(meet(X2,X1),X0),
inference(superposition,[],[f5,f20583]) ).
fof(f23291,plain,
! [X0,X1] : join(X1,meet(complement(X1),X0)) = join(X1,join(meet(X0,X1),meet(X0,complement(X1)))),
inference(superposition,[],[f54,f8451]) ).
fof(f23364,plain,
! [X0,X1] : join(X1,meet(X0,complement(X1))) = join(X1,meet(complement(X1),X0)),
inference(forward_demodulation,[],[f23291,f54]) ).
fof(f23622,plain,
! [X2,X0,X1] : meet(X2,join(X0,meet(X2,meet(X1,complement(X0))))) = meet(X2,join(X0,meet(meet(X1,complement(X0)),join(meet(X0,meet(X1,complement(X0))),meet(join(X0,meet(complement(X0),X1)),X2))))),
inference(superposition,[],[f181,f23364]) ).
fof(f23795,plain,
! [X2,X0,X1] : meet(X2,join(X0,meet(X2,meet(X1,complement(X0))))) = meet(X2,join(X0,meet(X1,meet(complement(X0),join(meet(X0,meet(X1,complement(X0))),meet(join(X0,meet(complement(X0),X1)),X2)))))),
inference(forward_demodulation,[],[f23622,f7]) ).
fof(f23842,plain,
! [X2,X0,X1] : meet(X2,join(X0,meet(X2,meet(X1,complement(X0))))) = meet(X2,join(X0,meet(X1,meet(complement(X0),join(zero,meet(join(X0,meet(complement(X0),X1)),X2)))))),
inference(forward_demodulation,[],[f23795,f645]) ).
fof(f23863,plain,
! [X2,X0,X1] : meet(X2,join(X0,meet(X2,meet(X1,complement(X0))))) = meet(X2,join(X0,meet(X1,meet(complement(X0),meet(join(X0,meet(complement(X0),X1)),X2))))),
inference(forward_demodulation,[],[f23842,f276]) ).
fof(f23877,plain,
! [X2,X0,X1] : meet(X2,join(X0,meet(X2,meet(X1,complement(X0))))) = meet(X2,join(X0,meet(complement(X0),meet(X1,X2)))),
inference(forward_demodulation,[],[f23863,f6632]) ).
fof(f24692,plain,
! [X2,X0,X1] : meet(X2,join(X0,meet(X2,meet(join(complement(X1),meet(X0,X1)),complement(meet(X0,join(complement(X1),meet(X1,X0)))))))) = meet(X2,join(X0,meet(join(complement(X1),meet(X0,X1)),meet(complement(meet(X0,join(complement(X1),meet(X1,X0)))),X2)))),
inference(superposition,[],[f3420,f4083]) ).
fof(f29301,plain,
! [X2,X0,X1] : join(X0,X2) = join(X2,join(X0,meet(X1,X2))),
inference(superposition,[],[f1872,f6]) ).
fof(f31017,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X1,X2)) = meet(X1,join(meet(X0,X1),meet(X1,X2))),
inference(superposition,[],[f8180,f51]) ).
fof(f31281,plain,
! [X2,X3,X0,X1] : meet(join(meet(X0,X1),meet(X0,X2)),X3) = meet(join(meet(X0,X1),meet(X0,X2)),meet(X0,X3)),
inference(superposition,[],[f114,f8180]) ).
fof(f31373,plain,
! [X2,X3,X0,X1] : meet(join(meet(X0,X1),meet(X0,X2)),X3) = meet(X0,meet(X3,join(meet(X0,X1),meet(X0,X2)))),
inference(forward_demodulation,[],[f31281,f125]) ).
fof(f31502,plain,
! [X0,X1] : join(meet(X1,X0),meet(X0,complement(X1))) = join(meet(X0,X1),meet(complement(X1),X0)),
inference(backward_demodulation,[],[f8452,f31017]) ).
fof(f31504,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X0,complement(join(X1,X2)))) = join(meet(X0,X1),meet(complement(join(X1,X2)),X0)),
inference(backward_demodulation,[],[f13144,f31017]) ).
fof(f31530,plain,
! [X2,X3,X0,X1] : join(meet(X0,X1),meet(X0,meet(join(X1,X2),X3))) = meet(join(meet(X0,X1),meet(X0,meet(join(X1,X2),X3))),join(X1,X2)),
inference(backward_demodulation,[],[f13602,f31373]) ).
fof(f31612,plain,
! [X2,X3,X0,X1] : join(meet(X0,X1),meet(X0,meet(join(X1,X2),X3))) = meet(join(X1,X2),join(meet(X0,X1),meet(X0,meet(join(X1,X2),X3)))),
inference(forward_demodulation,[],[f31530,f5]) ).
fof(f31911,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X1,complement(join(X0,X2)))) = join(meet(X1,X0),meet(X1,complement(join(X0,X2)))),
inference(superposition,[],[f9649,f31504]) ).
fof(f33749,plain,
! [X2,X0,X1] : join(X0,X1) = join(X1,join(X0,meet(X1,X2))),
inference(superposition,[],[f1871,f6]) ).
fof(f34262,plain,
! [X2,X0,X1] : meet(X2,join(X0,X1)) = meet(X2,join(X1,join(X0,meet(X2,X1)))),
inference(superposition,[],[f207,f33749]) ).
fof(f34287,plain,
! [X2,X3,X0,X1] : meet(join(X0,meet(X1,X2)),X3) = meet(join(X0,meet(X1,X2)),meet(join(X0,X1),X3)),
inference(superposition,[],[f112,f33749]) ).
fof(f34380,plain,
! [X2,X3,X0,X1] : meet(join(X0,meet(X1,X2)),X3) = meet(join(X0,X1),meet(X3,join(X0,meet(X1,X2)))),
inference(forward_demodulation,[],[f34287,f125]) ).
fof(f34397,plain,
! [X2,X0,X1] : meet(X2,join(X0,X1)) = meet(X2,join(X1,X0)),
inference(forward_demodulation,[],[f34262,f748]) ).
fof(f34463,plain,
! [X2,X0,X1] : meet(join(X0,X1),meet(X2,join(X0,meet(X2,X1)))) = meet(join(X0,meet(X1,X2)),X2),
inference(backward_demodulation,[],[f7824,f34380]) ).
fof(f34509,plain,
! [X2,X0,X1] : meet(X2,join(X0,meet(X1,X2))) = meet(join(X0,X1),meet(X2,join(X0,meet(X2,X1)))),
inference(forward_demodulation,[],[f34463,f5]) ).
fof(f34574,plain,
! [X2,X3,X0,X1] : meet(X3,join(X0,join(X1,X2))) = meet(X3,join(X2,join(X0,X1))),
inference(superposition,[],[f34397,f8]) ).
fof(f34760,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(X2,X1),X0),
inference(superposition,[],[f5,f34397]) ).
fof(f35180,plain,
! [X2,X0,X1] : meet(join(X0,X1),X2) = meet(join(X1,X0),X2),
inference(superposition,[],[f5,f34760]) ).
fof(f36025,plain,
! [X2,X3,X0,X1] : join(X2,meet(join(X3,X1),X0)) = join(meet(join(X3,X1),X0),join(meet(X0,X1),X2)),
inference(superposition,[],[f1872,f1670]) ).
fof(f36102,plain,
! [X2,X3,X0,X1] : join(X2,meet(join(X3,X1),X0)) = join(meet(X0,X1),join(X2,meet(join(X3,X1),X0))),
inference(forward_demodulation,[],[f36025,f67]) ).
fof(f39214,plain,
! [X2,X3,X0,X1] : meet(X2,join(X0,meet(X3,X1))) = meet(join(X0,meet(X3,X1)),meet(join(X0,X1),X2)),
inference(superposition,[],[f1670,f29301]) ).
fof(f39285,plain,
! [X2,X3,X0,X1] : meet(X2,join(X0,meet(X3,X1))) = meet(join(X0,X1),meet(X2,join(X0,meet(X3,X1)))),
inference(forward_demodulation,[],[f39214,f125]) ).
fof(f39422,plain,
! [X2,X0,X1] : meet(X2,join(X0,meet(X2,X1))) = meet(X2,join(X0,meet(X1,X2))),
inference(backward_demodulation,[],[f34509,f39285]) ).
fof(f43921,plain,
! [X0,X1] : meet(complement(meet(X0,complement(meet(X0,X1)))),join(complement(meet(X0,X1)),meet(complement(meet(X0,complement(meet(X0,X1)))),X0))) = meet(complement(meet(X0,complement(meet(X0,X1)))),join(complement(meet(X0,X1)),meet(X0,one))),
inference(superposition,[],[f5450,f9]) ).
fof(f44141,plain,
! [X0,X1] : meet(complement(meet(X0,complement(meet(X0,X1)))),join(complement(meet(X0,X1)),meet(complement(meet(X0,complement(meet(X0,X1)))),X0))) = meet(complement(meet(X0,complement(meet(X0,X1)))),join(meet(X0,one),complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f43921,f34397]) ).
fof(f44276,plain,
! [X0,X1] : meet(complement(meet(X0,complement(meet(X0,X1)))),join(complement(meet(X0,X1)),meet(complement(meet(X0,complement(meet(X0,X1)))),X0))) = meet(complement(meet(X0,complement(meet(X0,X1)))),join(X0,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f44141,f218]) ).
fof(f44374,plain,
! [X0,X1] : meet(complement(meet(X0,complement(meet(X0,X1)))),join(complement(meet(X0,X1)),meet(complement(meet(X0,complement(meet(X0,X1)))),X0))) = meet(join(complement(meet(X0,X1)),X0),complement(meet(X0,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f44276,f34760]) ).
fof(f44430,plain,
! [X0,X1] : meet(complement(meet(X0,complement(meet(X0,X1)))),join(complement(meet(X0,X1)),meet(complement(meet(X0,complement(meet(X0,X1)))),X0))) = meet(join(X0,complement(meet(X0,X1))),complement(meet(X0,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f44374,f35180]) ).
fof(f44473,plain,
! [X0,X1] : meet(complement(meet(X0,complement(meet(X0,X1)))),join(complement(meet(X0,X1)),meet(complement(meet(X0,complement(meet(X0,X1)))),X0))) = meet(one,complement(meet(X0,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f44430,f601]) ).
fof(f44513,plain,
! [X0,X1] : complement(meet(X0,complement(meet(X0,X1)))) = meet(complement(meet(X0,complement(meet(X0,X1)))),join(complement(meet(X0,X1)),meet(complement(meet(X0,complement(meet(X0,X1)))),X0))),
inference(forward_demodulation,[],[f44473,f451]) ).
fof(f44543,plain,
! [X0,X1] : complement(meet(X0,complement(meet(X0,X1)))) = meet(complement(meet(X0,complement(meet(X0,X1)))),join(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1))))))),
inference(forward_demodulation,[],[f44513,f39422]) ).
fof(f44766,plain,
! [X0,X1] : meet(complement(meet(X0,X1)),join(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))))) = meet(complement(meet(X0,X1)),join(X0,complement(meet(X0,complement(meet(X0,X1)))))),
inference(superposition,[],[f718,f44543]) ).
fof(f44780,plain,
! [X0,X1] : join(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))) = join(join(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))),complement(meet(X0,complement(meet(X0,X1))))),
inference(superposition,[],[f32,f44543]) ).
fof(f44875,plain,
! [X0,X1] : join(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))) = join(complement(meet(X0,complement(meet(X0,X1)))),join(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1))))))),
inference(forward_demodulation,[],[f44780,f6]) ).
fof(f44885,plain,
! [X0,X1] : meet(complement(meet(X0,X1)),one) = meet(complement(meet(X0,X1)),join(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))))),
inference(forward_demodulation,[],[f44766,f601]) ).
fof(f44957,plain,
! [X0,X1] : join(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))) = join(complement(meet(X0,X1)),join(meet(X0,complement(meet(X0,complement(meet(X0,X1))))),complement(meet(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f44875,f67]) ).
fof(f44966,plain,
! [X0,X1] : meet(one,complement(meet(X0,X1))) = meet(complement(meet(X0,X1)),join(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))))),
inference(forward_demodulation,[],[f44885,f5]) ).
fof(f45024,plain,
! [X0,X1] : one = join(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f44957,f4620]) ).
fof(f45033,plain,
! [X0,X1] : complement(meet(X0,X1)) = meet(complement(meet(X0,X1)),join(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))))),
inference(forward_demodulation,[],[f44966,f451]) ).
fof(f45326,plain,
! [X0,X1] :
( one != one
| zero != meet(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1))))))
| complement(complement(meet(X0,X1))) = meet(X0,complement(meet(X0,complement(meet(X0,X1))))) ),
inference(superposition,[],[f11,f45024]) ).
fof(f45383,plain,
! [X0,X1] :
( zero != meet(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1))))))
| complement(complement(meet(X0,X1))) = meet(X0,complement(meet(X0,complement(meet(X0,X1))))) ),
inference(trivial_inequality_removal,[],[f45326]) ).
fof(f45430,plain,
! [X0,X1] : complement(complement(meet(X0,X1))) = meet(X0,complement(meet(X0,complement(meet(X0,X1))))),
inference(forward_subsumption_resolution,[],[f45383,f810]) ).
fof(f45542,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,complement(meet(X0,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f45430,f4073]) ).
fof(f45735,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,complement(meet(X1,complement(meet(X0,X1))))),
inference(superposition,[],[f45542,f1670]) ).
fof(f45761,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,complement(meet(X0,complement(join(meet(X0,X1),meet(X0,X2)))))),
inference(superposition,[],[f45542,f8180]) ).
fof(f46355,plain,
! [X0,X1] : join(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1)))))) = join(join(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1)))))),complement(meet(X0,X1))),
inference(superposition,[],[f32,f45033]) ).
fof(f46452,plain,
! [X0,X1] : join(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1)))))) = join(complement(meet(X0,X1)),join(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))))),
inference(forward_demodulation,[],[f46355,f6]) ).
fof(f46536,plain,
! [X0,X1] : join(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1)))))) = join(X0,join(meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))),complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f46452,f67]) ).
fof(f46596,plain,
! [X0,X1] : one = join(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f46536,f4619]) ).
fof(f46866,plain,
! [X0,X1] :
( one != one
| zero != meet(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))))
| complement(X0) = meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))) ),
inference(superposition,[],[f11,f46596]) ).
fof(f46948,plain,
! [X0,X1] :
( zero != meet(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))))
| complement(X0) = meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))) ),
inference(trivial_inequality_removal,[],[f46866]) ).
fof(f47015,plain,
! [X0,X1] : complement(X0) = meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))),
inference(forward_subsumption_resolution,[],[f46948,f266]) ).
fof(f47395,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(join(X0,X1)),complement(meet(join(X1,X0),complement(join(X0,X1))))),
inference(superposition,[],[f47015,f13294]) ).
fof(f47460,plain,
! [X0,X1] : complement(X0) = meet(complement(meet(X0,X1)),complement(X0)),
inference(superposition,[],[f52,f47015]) ).
fof(f47566,plain,
! [X0,X1] : complement(X0) = meet(complement(X0),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f47460,f5]) ).
fof(f47615,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(join(X0,X1)),complement(zero)),
inference(forward_demodulation,[],[f47395,f18142]) ).
fof(f47703,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(zero),complement(join(X0,X1))),
inference(forward_demodulation,[],[f47615,f5]) ).
fof(f47747,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(one,complement(join(X0,X1))),
inference(forward_demodulation,[],[f47703,f303]) ).
fof(f47753,plain,
! [X0,X1] : complement(join(X0,X1)) = complement(join(X1,X0)),
inference(forward_demodulation,[],[f47747,f451]) ).
fof(f47761,plain,
! [X0,X1] : meet(X0,complement(meet(complement(X0),X1))) = X0,
inference(superposition,[],[f47566,f4073]) ).
fof(f47787,plain,
! [X0,X1] : complement(X1) = meet(complement(X1),complement(meet(X0,X1))),
inference(superposition,[],[f47566,f1670]) ).
fof(f48164,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(complement(meet(complement(X0),X1)),X0),
inference(superposition,[],[f32,f47761]) ).
fof(f48303,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(X0,complement(meet(complement(X0),X1))),
inference(forward_demodulation,[],[f48164,f6]) ).
fof(f48516,plain,
! [X2,X0,X1] : meet(X2,join(complement(complement(meet(complement(X0),X1))),meet(X2,X0))) = meet(X2,join(meet(X0,X2),complement(complement(meet(complement(X0),X1))))),
inference(superposition,[],[f9334,f48303]) ).
fof(f48561,plain,
! [X2,X0,X1] : meet(X2,join(meet(complement(X0),X1),meet(X2,X0))) = meet(X2,join(meet(X0,X2),meet(complement(X0),X1))),
inference(forward_demodulation,[],[f48516,f4073]) ).
fof(f49214,plain,
! [X0,X1] : complement(meet(X0,X1)) = complement(join(meet(X1,X0),meet(X0,X1))),
inference(superposition,[],[f47753,f7994]) ).
fof(f49310,plain,
! [X0,X1] : complement(meet(X0,X1)) = complement(meet(X1,X0)),
inference(forward_demodulation,[],[f49214,f7994]) ).
fof(f50551,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(join(X0,X1)),complement(X0)),
inference(superposition,[],[f47787,f3]) ).
fof(f50552,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(join(X1,X0)),complement(X0)),
inference(superposition,[],[f47787,f34]) ).
fof(f50697,plain,
! [X2,X0,X1] : join(X1,complement(meet(X2,X0))) = join(complement(meet(X2,X0)),join(complement(X0),X1)),
inference(superposition,[],[f1872,f47787]) ).
fof(f50751,plain,
! [X2,X0,X1] : join(X1,complement(meet(X2,X0))) = join(complement(X0),join(X1,complement(meet(X2,X0)))),
inference(forward_demodulation,[],[f50697,f67]) ).
fof(f50816,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(X0),complement(join(X1,X0))),
inference(forward_demodulation,[],[f50552,f5]) ).
fof(f50817,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X0),complement(join(X0,X1))),
inference(forward_demodulation,[],[f50551,f5]) ).
fof(f51006,plain,
! [X0,X1] : meet(X1,X0) = meet(X1,complement(meet(X1,complement(meet(X0,X1))))),
inference(superposition,[],[f45542,f49310]) ).
fof(f51101,plain,
! [X0,X1] : meet(join(X0,X1),X0) = meet(join(X0,X1),complement(meet(join(X0,X1),complement(X0)))),
inference(superposition,[],[f51006,f3]) ).
fof(f51102,plain,
! [X0,X1] : meet(join(X1,X0),X0) = meet(join(X1,X0),complement(meet(join(X1,X0),complement(X0)))),
inference(superposition,[],[f51006,f34]) ).
fof(f51216,plain,
! [X0,X1] : meet(X0,complement(meet(X1,X0))) = meet(X0,complement(meet(X0,X1))),
inference(superposition,[],[f45542,f51006]) ).
fof(f51220,plain,
! [X0,X1] : join(meet(X0,meet(X0,complement(meet(X1,X0)))),meet(complement(meet(X0,complement(meet(X1,X0)))),X0)) = join(meet(meet(X0,complement(meet(X1,X0))),X0),meet(X0,X1)),
inference(superposition,[],[f31502,f51006]) ).
fof(f51380,plain,
! [X0,X1] : join(meet(X0,meet(X0,complement(meet(X1,X0)))),meet(complement(meet(X0,complement(meet(X1,X0)))),X0)) = join(meet(X0,X1),meet(meet(X0,complement(meet(X1,X0))),X0)),
inference(forward_demodulation,[],[f51220,f6]) ).
fof(f51487,plain,
! [X0,X1] : meet(join(X1,X0),X0) = meet(join(X1,X0),complement(meet(complement(X0),join(X1,X0)))),
inference(forward_demodulation,[],[f51102,f51216]) ).
fof(f51488,plain,
! [X0,X1] : meet(join(X0,X1),X0) = meet(join(X0,X1),complement(meet(complement(X0),join(X0,X1)))),
inference(forward_demodulation,[],[f51101,f51216]) ).
fof(f51553,plain,
! [X0,X1] : join(meet(X0,meet(X0,complement(meet(X1,X0)))),meet(complement(meet(X0,complement(meet(X1,X0)))),X0)) = join(meet(X0,X1),meet(X0,meet(X0,complement(meet(X1,X0))))),
inference(forward_demodulation,[],[f51380,f5]) ).
fof(f51640,plain,
! [X0,X1] : meet(X0,join(X1,X0)) = meet(join(X1,X0),complement(meet(complement(X0),join(X1,X0)))),
inference(forward_demodulation,[],[f51487,f5]) ).
fof(f51641,plain,
! [X0,X1] : meet(X0,join(X0,X1)) = meet(join(X0,X1),complement(meet(complement(X0),join(X0,X1)))),
inference(forward_demodulation,[],[f51488,f5]) ).
fof(f51686,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,complement(meet(X1,X0)))) = join(meet(X0,complement(meet(X1,X0))),meet(complement(meet(X0,complement(meet(X1,X0)))),X0)),
inference(forward_demodulation,[],[f51553,f52]) ).
fof(f51723,plain,
! [X0,X1] : meet(join(X1,X0),complement(meet(complement(X0),join(X1,X0)))) = X0,
inference(forward_demodulation,[],[f51640,f34]) ).
fof(f51724,plain,
! [X0,X1] : meet(join(X0,X1),complement(meet(complement(X0),join(X0,X1)))) = X0,
inference(forward_demodulation,[],[f51641,f3]) ).
fof(f51754,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,complement(meet(X1,X0)))) = join(meet(X0,complement(meet(X1,X0))),meet(X0,complement(meet(X0,complement(meet(X1,X0)))))),
inference(forward_demodulation,[],[f51686,f23364]) ).
fof(f51800,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,complement(meet(X1,X0)))) = join(meet(X0,complement(meet(X1,X0))),meet(X1,X0)),
inference(forward_demodulation,[],[f51754,f45735]) ).
fof(f51829,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,complement(meet(X1,X0)))) = join(meet(X1,X0),meet(X0,complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f51800,f6]) ).
fof(f51993,plain,
! [X0,X1] : join(meet(X0,meet(X0,X1)),meet(complement(meet(X0,X1)),X0)) = join(meet(meet(X0,X1),X0),meet(X0,complement(meet(X1,X0)))),
inference(superposition,[],[f31502,f51216]) ).
fof(f52050,plain,
! [X2,X0,X1] : meet(X2,meet(X0,complement(meet(X1,X0)))) = meet(meet(complement(meet(X0,X1)),X0),X2),
inference(superposition,[],[f20856,f51216]) ).
fof(f52068,plain,
! [X2,X0,X1] : meet(X1,meet(join(X0,X1),complement(meet(X2,join(X0,X1))))) = meet(X1,complement(meet(join(X0,X1),X2))),
inference(superposition,[],[f112,f51216]) ).
fof(f52108,plain,
! [X2,X0,X1] : meet(X1,complement(meet(X2,join(X0,X1)))) = meet(X1,complement(meet(join(X0,X1),X2))),
inference(forward_demodulation,[],[f52068,f112]) ).
fof(f52118,plain,
! [X2,X0,X1] : meet(X2,meet(X0,complement(meet(X1,X0)))) = meet(complement(meet(X0,X1)),meet(X0,X2)),
inference(forward_demodulation,[],[f52050,f7]) ).
fof(f52146,plain,
! [X0,X1] : join(meet(X0,meet(X0,X1)),meet(complement(meet(X0,X1)),X0)) = join(meet(X0,meet(X0,X1)),meet(X0,complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f51993,f5]) ).
fof(f52231,plain,
! [X2,X0,X1] : meet(X0,meet(X2,complement(meet(X0,X1)))) = meet(X2,meet(X0,complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f52118,f125]) ).
fof(f52248,plain,
! [X0,X1] : join(meet(X0,X1),meet(complement(meet(X0,X1)),X0)) = join(meet(X0,X1),meet(X0,complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f52146,f52]) ).
fof(f52301,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,complement(meet(X0,X1)))) = join(meet(X0,X1),meet(X0,complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f52248,f23364]) ).
fof(f54748,plain,
! [X2,X0,X1] : complement(join(meet(X1,X0),X2)) = meet(complement(meet(X0,X1)),complement(join(meet(X1,X0),X2))),
inference(superposition,[],[f50817,f49310]) ).
fof(f54751,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = meet(X0,complement(join(complement(X0),X1))),
inference(superposition,[],[f50817,f4073]) ).
fof(f55143,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),X1))) = X0,
inference(superposition,[],[f4,f54751]) ).
fof(f55156,plain,
! [X2,X0,X1] : meet(X2,X0) = join(meet(X2,X0),meet(X2,complement(join(complement(X0),X1)))),
inference(superposition,[],[f126,f54751]) ).
fof(f55204,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = meet(X0,complement(meet(X0,complement(complement(join(complement(X0),X1)))))),
inference(superposition,[],[f45542,f54751]) ).
fof(f55260,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = meet(X0,complement(meet(X0,join(complement(X0),X1)))),
inference(forward_demodulation,[],[f55204,f4073]) ).
fof(f55926,plain,
! [X0,X1] : join(X1,complement(join(X0,complement(X1)))) = X1,
inference(superposition,[],[f55143,f47753]) ).
fof(f56186,plain,
! [X2,X0,X1] : join(X2,X0) = join(X0,join(complement(join(X1,complement(X0))),X2)),
inference(superposition,[],[f67,f55926]) ).
fof(f56199,plain,
! [X2,X3,X0,X1] : meet(X1,join(X0,join(complement(join(X2,complement(X0))),meet(X1,X3)))) = meet(X1,join(X0,join(complement(join(X2,complement(X0))),meet(X3,join(meet(X0,X3),meet(X1,join(X0,join(complement(join(X2,complement(X0))),X3)))))))),
inference(superposition,[],[f207,f55926]) ).
fof(f56311,plain,
! [X2,X3,X0,X1] : meet(X1,join(X0,join(complement(join(X2,complement(X0))),meet(X1,X3)))) = meet(X1,join(X0,join(complement(join(X2,complement(X0))),meet(X3,join(meet(X0,X3),meet(X1,join(X3,X0))))))),
inference(backward_demodulation,[],[f56199,f56186]) ).
fof(f56359,plain,
! [X2,X3,X0,X1] : meet(X1,join(X0,join(complement(join(X2,complement(X0))),meet(X1,X3)))) = meet(X1,join(meet(X3,join(meet(X0,X3),meet(X1,join(X3,X0)))),X0)),
inference(forward_demodulation,[],[f56311,f56186]) ).
fof(f56379,plain,
! [X2,X3,X0,X1] : meet(X1,join(X0,meet(X3,join(meet(X0,X3),meet(X1,join(X3,X0)))))) = meet(X1,join(X0,join(complement(join(X2,complement(X0))),meet(X1,X3)))),
inference(forward_demodulation,[],[f56359,f34397]) ).
fof(f56382,plain,
! [X3,X0,X1] : meet(X1,join(meet(X1,X3),X0)) = meet(X1,join(X0,meet(X3,join(meet(X0,X3),meet(X1,join(X3,X0)))))),
inference(forward_demodulation,[],[f56379,f56186]) ).
fof(f60179,plain,
! [X0,X1] : meet(complement(X1),X0) = join(meet(complement(X1),X0),complement(join(complement(X0),X1))),
inference(superposition,[],[f55156,f50816]) ).
fof(f60557,plain,
! [X0,X1] : meet(complement(X1),complement(X0)) = join(meet(complement(X1),complement(X0)),complement(join(X0,X1))),
inference(superposition,[],[f60179,f4073]) ).
fof(f60618,plain,
! [X0,X1] : join(complement(X1),X0) = join(join(complement(X1),X0),complement(meet(complement(X0),X1))),
inference(superposition,[],[f55926,f60179]) ).
fof(f60719,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(X1),join(X0,complement(meet(complement(X0),X1)))),
inference(forward_demodulation,[],[f60618,f8]) ).
fof(f60771,plain,
! [X0,X1] : meet(complement(X1),complement(X0)) = join(complement(join(X0,X1)),meet(complement(X1),complement(X0))),
inference(forward_demodulation,[],[f60557,f6]) ).
fof(f60852,plain,
! [X0,X1] : join(complement(X1),X0) = join(X0,complement(meet(complement(X0),X1))),
inference(forward_demodulation,[],[f60719,f50751]) ).
fof(f60935,plain,
! [X0,X1] : join(complement(X1),X0) = complement(meet(complement(X0),X1)),
inference(backward_demodulation,[],[f48303,f60852]) ).
fof(f61222,plain,
! [X0,X1] : meet(join(X1,X0),join(complement(join(X1,X0)),X0)) = X0,
inference(backward_demodulation,[],[f51723,f60935]) ).
fof(f61224,plain,
! [X0,X1] : meet(join(X0,X1),join(complement(join(X0,X1)),X0)) = X0,
inference(backward_demodulation,[],[f51724,f60935]) ).
fof(f61281,plain,
! [X0,X1] : meet(join(X0,X1),join(X0,complement(join(X0,X1)))) = X0,
inference(forward_demodulation,[],[f61224,f34397]) ).
fof(f61283,plain,
! [X0,X1] : meet(join(X1,X0),join(X0,complement(join(X1,X0)))) = X0,
inference(forward_demodulation,[],[f61222,f34397]) ).
fof(f61444,plain,
! [X2,X0,X1] : complement(meet(complement(meet(X0,X1)),X2)) = join(complement(X2),meet(X1,X0)),
inference(superposition,[],[f60935,f49310]) ).
fof(f61445,plain,
! [X2,X0,X1] : complement(meet(join(complement(X0),X1),X2)) = join(complement(X2),meet(complement(X1),X0)),
inference(superposition,[],[f60935,f60935]) ).
fof(f61448,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X1),complement(X0)),
inference(superposition,[],[f60935,f4073]) ).
fof(f61452,plain,
! [X0,X1] : complement(complement(X0)) = join(complement(complement(meet(X0,complement(meet(X0,X1))))),meet(X0,X1)),
inference(superposition,[],[f60935,f47015]) ).
fof(f61550,plain,
! [X0,X1] : join(complement(X0),X1) = complement(meet(X0,complement(X1))),
inference(superposition,[],[f49310,f60935]) ).
fof(f61555,plain,
! [X0,X1] : meet(X0,complement(meet(X0,complement(X1)))) = meet(X0,join(complement(X0),X1)),
inference(superposition,[],[f51216,f60935]) ).
fof(f61571,plain,
! [X0,X1] : meet(complement(X1),X0) = complement(join(complement(X0),X1)),
inference(superposition,[],[f4073,f60935]) ).
fof(f61636,plain,
! [X0,X1] : meet(complement(X1),X0) = meet(X0,complement(meet(X0,join(complement(X0),X1)))),
inference(backward_demodulation,[],[f55260,f61571]) ).
fof(f62022,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(complement(X0),join(meet(X0,X1),meet(X0,X2)))),
inference(backward_demodulation,[],[f45761,f61555]) ).
fof(f62345,plain,
! [X0,X1] : complement(complement(X0)) = join(meet(X0,X1),complement(complement(meet(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f61452,f6]) ).
fof(f62486,plain,
! [X0,X1] : meet(complement(X1),complement(X0)) = complement(meet(join(complement(complement(X0)),X1),join(X0,X1))),
inference(backward_demodulation,[],[f60771,f61445]) ).
fof(f62487,plain,
! [X2,X0,X1] : join(complement(X2),meet(X0,X1)) = join(complement(X2),meet(X1,X0)),
inference(forward_demodulation,[],[f61444,f60935]) ).
fof(f62909,plain,
! [X0,X1] : complement(complement(X0)) = join(meet(X0,X1),meet(X0,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f62345,f4073]) ).
fof(f62993,plain,
! [X0,X1] : meet(complement(X1),complement(X0)) = complement(meet(join(X0,X1),join(complement(complement(X0)),X1))),
inference(forward_demodulation,[],[f62486,f49310]) ).
fof(f63247,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,complement(meet(X0,X1)))) = X0,
inference(forward_demodulation,[],[f62909,f4073]) ).
fof(f63269,plain,
! [X0,X1] : meet(complement(X1),complement(X0)) = complement(meet(join(X0,X1),join(X0,X1))),
inference(forward_demodulation,[],[f62993,f4073]) ).
fof(f63388,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,complement(meet(X1,X0)))) = X0,
inference(backward_demodulation,[],[f52301,f63247]) ).
fof(f63405,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X1),complement(X0)),
inference(forward_demodulation,[],[f63269,f1]) ).
fof(f63471,plain,
! [X0,X1] : join(meet(X1,X0),meet(X0,complement(meet(X1,X0)))) = X0,
inference(backward_demodulation,[],[f51829,f63388]) ).
fof(f63530,plain,
! [X2,X0,X1] : complement(join(meet(X1,X0),X2)) = complement(join(join(meet(X1,X0),X2),meet(X0,X1))),
inference(backward_demodulation,[],[f54748,f63405]) ).
fof(f63827,plain,
! [X2,X0,X1] : complement(join(meet(X1,X0),X2)) = complement(join(meet(X0,X1),join(meet(X1,X0),X2))),
inference(forward_demodulation,[],[f63530,f47753]) ).
fof(f63991,plain,
! [X2,X0,X1] : complement(join(meet(X0,X1),X2)) = complement(join(meet(X1,X0),X2)),
inference(forward_demodulation,[],[f63827,f16250]) ).
fof(f65037,plain,
! [X0,X1] : join(X1,X0) = join(X1,meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f54,f63247]) ).
fof(f65457,plain,
! [X0,X1] : join(X1,X0) = join(X1,meet(X0,complement(meet(X1,X0)))),
inference(superposition,[],[f65037,f51216]) ).
fof(f65509,plain,
! [X0,X1] :
( zero != meet(meet(X1,complement(meet(X1,X0))),join(X0,complement(join(X0,X1))))
| join(X0,complement(join(X0,X1))) = complement(meet(X1,complement(meet(X1,X0)))) ),
inference(superposition,[],[f1551,f65037]) ).
fof(f65595,plain,
! [X0,X1] :
( zero != meet(X1,meet(complement(meet(X1,X0)),join(X0,complement(join(X0,X1)))))
| join(X0,complement(join(X0,X1))) = complement(meet(X1,complement(meet(X1,X0)))) ),
inference(forward_demodulation,[],[f65509,f7]) ).
fof(f65771,plain,
! [X0,X1] :
( join(X0,complement(join(X0,X1))) = join(complement(X1),meet(X1,X0))
| zero != meet(X1,meet(complement(meet(X1,X0)),join(X0,complement(join(X0,X1))))) ),
inference(forward_demodulation,[],[f65595,f61550]) ).
fof(f66558,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(X0,meet(X2,X1)),
inference(superposition,[],[f62487,f4073]) ).
fof(f66897,plain,
! [X2,X3,X0,X1] : join(X3,meet(X0,meet(X1,X2))) = join(X3,meet(X0,meet(X2,X1))),
inference(superposition,[],[f66558,f20856]) ).
fof(f66899,plain,
! [X2,X3,X0,X1] : join(X3,meet(X2,meet(X0,X1))) = join(X3,meet(X0,meet(X1,X2))),
inference(superposition,[],[f66558,f7]) ).
fof(f67315,plain,
! [X2,X0,X1] : complement(join(X2,meet(complement(X1),X0))) = meet(join(complement(X0),X1),complement(X2)),
inference(superposition,[],[f63405,f60935]) ).
fof(f67318,plain,
! [X0,X1] : meet(X0,complement(X1)) = complement(join(X1,complement(X0))),
inference(superposition,[],[f63405,f4073]) ).
fof(f67436,plain,
! [X2,X0,X1] : meet(X2,complement(join(X0,X1))) = meet(X2,meet(complement(X0),complement(X1))),
inference(superposition,[],[f20583,f63405]) ).
fof(f67468,plain,
! [X2,X0,X1] : join(X2,complement(join(X0,X1))) = join(X2,meet(complement(X0),complement(X1))),
inference(superposition,[],[f66558,f63405]) ).
fof(f67469,plain,
! [X2,X0,X1] : join(X2,complement(join(X0,X1))) = join(X2,complement(join(X1,X0))),
inference(forward_demodulation,[],[f67468,f63405]) ).
fof(f67501,plain,
! [X2,X0,X1] : meet(X2,complement(join(X0,X1))) = meet(X2,complement(join(X1,X0))),
inference(forward_demodulation,[],[f67436,f63405]) ).
fof(f67719,plain,
! [X2,X0,X1] : meet(X2,join(X0,meet(join(complement(X1),meet(X0,X1)),meet(complement(meet(X0,join(complement(X1),meet(X1,X0)))),X2)))) = meet(X2,join(X0,meet(X2,complement(join(meet(X0,join(complement(X1),meet(X1,X0))),meet(complement(meet(X0,X1)),X1)))))),
inference(backward_demodulation,[],[f24692,f67315]) ).
fof(f67965,plain,
! [X2,X0,X1] : meet(X2,join(X0,meet(join(complement(X1),meet(X0,X1)),meet(complement(meet(X0,join(complement(X1),meet(X1,X0)))),X2)))) = meet(X2,join(X0,meet(X2,complement(join(meet(complement(meet(X0,X1)),X1),meet(X0,join(complement(X1),meet(X1,X0)))))))),
inference(forward_demodulation,[],[f67719,f67501]) ).
fof(f68088,plain,
! [X2,X0,X1] : meet(X2,join(X0,meet(join(complement(X1),meet(X0,X1)),meet(complement(meet(X0,join(complement(X1),meet(X1,X0)))),X2)))) = meet(X2,join(X0,meet(X2,complement(join(meet(X1,complement(meet(X0,X1))),meet(X0,join(complement(X1),meet(X1,X0)))))))),
inference(forward_demodulation,[],[f67965,f63991]) ).
fof(f68454,plain,
! [X2,X0,X1] : meet(X2,complement(join(X0,X1))) = complement(join(X0,join(X1,complement(X2)))),
inference(superposition,[],[f67318,f8]) ).
fof(f68505,plain,
! [X2,X0,X1] : join(meet(X0,complement(X1)),complement(X2)) = complement(meet(X2,join(X1,complement(X0)))),
inference(superposition,[],[f61448,f67318]) ).
fof(f69260,plain,
! [X0,X1] : meet(X1,X0) = meet(X1,join(X0,complement(join(X0,X1)))),
inference(superposition,[],[f112,f61281]) ).
fof(f69754,plain,
! [X0,X1] : meet(X1,complement(X0)) = meet(X1,complement(meet(join(complement(X0),X1),X0))),
inference(superposition,[],[f69260,f61448]) ).
fof(f69799,plain,
! [X0,X1] : zero = meet(X0,meet(join(X1,complement(join(X1,X0))),complement(meet(X0,X1)))),
inference(superposition,[],[f266,f69260]) ).
fof(f69931,plain,
! [X0,X1] : zero = meet(X0,meet(complement(meet(X0,X1)),join(X1,complement(join(X1,X0))))),
inference(forward_demodulation,[],[f69799,f20583]) ).
fof(f69962,plain,
! [X0,X1] : meet(X1,complement(X0)) = meet(X1,complement(meet(X0,join(complement(X0),X1)))),
inference(forward_demodulation,[],[f69754,f52108]) ).
fof(f70124,plain,
! [X0,X1] :
( zero != zero
| join(X0,complement(join(X0,X1))) = join(complement(X1),meet(X1,X0)) ),
inference(backward_demodulation,[],[f65771,f69931]) ).
fof(f70125,plain,
! [X0,X1] : join(X0,complement(join(X0,X1))) = join(complement(X1),meet(X1,X0)),
inference(trivial_inequality_removal,[],[f70124]) ).
fof(f70560,plain,
! [X0,X1] : join(X1,complement(join(X0,X1))) = join(complement(X0),meet(X0,X1)),
inference(superposition,[],[f70125,f47753]) ).
fof(f70570,plain,
! [X2,X0,X1] : join(meet(X0,complement(X1)),meet(join(X1,complement(X0)),X2)) = join(X2,complement(join(X2,join(X1,complement(X0))))),
inference(superposition,[],[f70125,f67318]) ).
fof(f70609,plain,
! [X0,X1] : complement(join(complement(X0),meet(X0,X1))) = meet(join(X1,X0),complement(X1)),
inference(superposition,[],[f67318,f70125]) ).
fof(f70612,plain,
! [X0,X1] : meet(X1,join(complement(X0),meet(X0,X1))) = X1,
inference(superposition,[],[f3,f70125]) ).
fof(f70617,plain,
! [X0,X1] : join(complement(X0),meet(X0,X1)) = join(X1,join(complement(X0),meet(X0,X1))),
inference(superposition,[],[f41,f70125]) ).
fof(f70662,plain,
! [X2,X0,X1] : join(meet(X2,X1),meet(complement(join(complement(X0),meet(X0,X1))),X2)) = join(meet(X1,X2),meet(X2,complement(join(complement(X0),meet(X0,X1))))),
inference(superposition,[],[f31504,f70125]) ).
fof(f70709,plain,
! [X0,X1] : join(complement(X1),X0) = join(X0,join(X0,complement(join(X0,X1)))),
inference(superposition,[],[f29301,f70125]) ).
fof(f70712,plain,
! [X0,X1] : join(X0,complement(join(X0,X1))) = join(complement(X1),meet(X0,X1)),
inference(superposition,[],[f66558,f70125]) ).
fof(f70722,plain,
! [X2,X0,X1] : join(complement(X1),join(meet(X1,X0),X2)) = join(X2,join(X0,complement(join(X0,X1)))),
inference(superposition,[],[f67,f70125]) ).
fof(f70812,plain,
! [X0,X1] : join(X0,complement(join(X0,X1))) = join(complement(X1),X0),
inference(forward_demodulation,[],[f70709,f41]) ).
fof(f70841,plain,
! [X2,X0,X1] : join(meet(X2,X1),meet(meet(complement(meet(X0,X1)),X0),X2)) = join(meet(X1,X2),meet(X2,meet(complement(meet(X0,X1)),X0))),
inference(forward_demodulation,[],[f70662,f61571]) ).
fof(f70873,plain,
! [X0,X1] : join(X1,complement(X0)) = join(complement(X0),meet(X0,X1)),
inference(forward_demodulation,[],[f70617,f748]) ).
fof(f70921,plain,
! [X2,X0,X1] : meet(X2,join(X0,meet(join(complement(X1),meet(X0,X1)),meet(complement(X0),X2)))) = meet(X2,join(X0,meet(X2,complement(join(meet(X1,complement(meet(X0,X1))),X0))))),
inference(backward_demodulation,[],[f68088,f70612]) ).
fof(f70933,plain,
! [X0,X1] : meet(complement(X1),join(X1,X0)) = complement(join(complement(X0),meet(X0,X1))),
inference(forward_demodulation,[],[f70609,f5]) ).
fof(f70955,plain,
! [X2,X0,X1] : join(X2,meet(X0,complement(join(X2,X1)))) = join(meet(X0,complement(X1)),meet(join(X1,complement(X0)),X2)),
inference(forward_demodulation,[],[f70570,f68454]) ).
fof(f71018,plain,
! [X0,X1] : meet(X1,X0) = meet(X1,join(complement(X1),X0)),
inference(backward_demodulation,[],[f69260,f70812]) ).
fof(f71048,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(X1),meet(X1,X0)),
inference(backward_demodulation,[],[f70125,f70812]) ).
fof(f71055,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(X1),meet(X0,X1)),
inference(backward_demodulation,[],[f70712,f70812]) ).
fof(f71057,plain,
! [X2,X0,X1] : join(complement(X1),join(meet(X1,X0),X2)) = join(X2,join(complement(X1),X0)),
inference(backward_demodulation,[],[f70722,f70812]) ).
fof(f71190,plain,
! [X2,X0,X1] : join(meet(X2,X1),meet(meet(complement(meet(X0,X1)),X0),X2)) = join(meet(X1,X2),meet(X2,meet(X0,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f70841,f66897]) ).
fof(f71264,plain,
! [X0,X1] : join(X1,complement(join(X0,X1))) = join(X1,complement(X0)),
inference(backward_demodulation,[],[f70560,f70873]) ).
fof(f71350,plain,
! [X2,X0,X1] : meet(X2,join(X0,meet(join(complement(X1),meet(X0,X1)),meet(complement(X0),X2)))) = meet(X2,join(X0,meet(X2,complement(join(X0,meet(X1,complement(meet(X0,X1)))))))),
inference(forward_demodulation,[],[f70921,f67501]) ).
fof(f71382,plain,
! [X0,X1] : meet(complement(meet(X0,X1)),X0) = meet(complement(X1),join(X1,X0)),
inference(forward_demodulation,[],[f70933,f61571]) ).
fof(f71547,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(X0,X2),join(complement(X0),X1))),
inference(backward_demodulation,[],[f62022,f71057]) ).
fof(f71610,plain,
! [X0,X1] : meet(complement(X1),X0) = meet(X0,complement(meet(X0,X1))),
inference(backward_demodulation,[],[f61636,f71018]) ).
fof(f71616,plain,
! [X0,X1] : meet(X1,complement(X0)) = meet(X1,complement(meet(X0,X1))),
inference(backward_demodulation,[],[f69962,f71018]) ).
fof(f71691,plain,
! [X2,X0,X1] : join(meet(X1,X2),meet(X2,meet(X0,complement(meet(X0,X1))))) = join(meet(X2,X1),meet(complement(meet(X0,X1)),meet(X0,X2))),
inference(forward_demodulation,[],[f71190,f7]) ).
fof(f71794,plain,
! [X0,X1] : meet(join(X1,X0),join(X0,complement(X1))) = X0,
inference(backward_demodulation,[],[f61283,f71264]) ).
fof(f71900,plain,
! [X2,X0,X1] : meet(X2,join(X0,meet(X2,complement(join(X0,X1))))) = meet(X2,join(X0,meet(join(complement(X1),meet(X0,X1)),meet(complement(X0),X2)))),
inference(forward_demodulation,[],[f71350,f65457]) ).
fof(f71928,plain,
! [X0,X1] : meet(X0,complement(meet(X0,X1))) = meet(complement(X1),join(X1,X0)),
inference(forward_demodulation,[],[f71382,f5]) ).
fof(f72030,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(complement(X0),join(X1,meet(X0,X2)))),
inference(forward_demodulation,[],[f71547,f34574]) ).
fof(f72197,plain,
! [X2,X0,X1] : meet(X2,meet(X0,complement(X1))) = meet(X0,meet(X2,complement(meet(X0,X1)))),
inference(backward_demodulation,[],[f52231,f71616]) ).
fof(f72214,plain,
! [X0,X1] : join(meet(X1,X0),meet(X0,complement(X1))) = X0,
inference(backward_demodulation,[],[f63471,f71616]) ).
fof(f72393,plain,
! [X0,X1] : join(X1,X0) = join(X1,meet(complement(X1),X0)),
inference(backward_demodulation,[],[f65037,f71610]) ).
fof(f72529,plain,
! [X2,X0,X1] : join(meet(X1,X2),meet(X2,meet(X0,complement(meet(X0,X1))))) = join(meet(X2,X1),meet(X0,meet(X2,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f71691,f66899]) ).
fof(f72670,plain,
! [X2,X0,X1] : meet(X2,join(X0,meet(X2,complement(join(X0,X1))))) = meet(X2,join(X0,meet(complement(X0),meet(X2,join(complement(X1),meet(X0,X1)))))),
inference(forward_demodulation,[],[f71900,f66899]) ).
fof(f72688,plain,
! [X0,X1] : meet(complement(X1),X0) = meet(complement(X1),join(X1,X0)),
inference(forward_demodulation,[],[f71928,f71610]) ).
fof(f72760,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X0,X2))) = join(meet(X0,X1),meet(X0,X2)),
inference(forward_demodulation,[],[f72030,f71018]) ).
fof(f73293,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X2,X0))) = meet(X0,join(X1,meet(X0,meet(complement(X1),X2)))),
inference(backward_demodulation,[],[f3667,f72393]) ).
fof(f73304,plain,
! [X2,X0,X1] : meet(X2,join(X0,meet(X1,X2))) = meet(X2,join(X0,meet(X2,meet(X1,complement(X0))))),
inference(backward_demodulation,[],[f23877,f72393]) ).
fof(f73503,plain,
! [X2,X0,X1] : join(meet(X2,X1),meet(X2,meet(X0,complement(X1)))) = join(meet(X1,X2),meet(X2,meet(X0,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f72529,f72197]) ).
fof(f73558,plain,
! [X2,X0,X1] : meet(X2,join(X0,meet(X2,join(complement(X1),meet(X0,X1))))) = meet(X2,join(X0,meet(X2,complement(join(X0,X1))))),
inference(forward_demodulation,[],[f72670,f72393]) ).
fof(f73650,plain,
! [X2,X0,X1] : meet(X2,join(X1,meet(X0,join(meet(X1,X0),meet(X2,join(X0,X1)))))) = join(meet(X2,X1),meet(X2,X0)),
inference(backward_demodulation,[],[f188,f72760]) ).
fof(f73788,plain,
! [X2,X0,X1] : meet(X2,join(X0,meet(X1,X2))) = join(meet(X2,X0),meet(X2,X1)),
inference(backward_demodulation,[],[f39422,f72760]) ).
fof(f74115,plain,
! [X2,X0,X1] : meet(X2,join(meet(X0,X2),meet(complement(X0),X1))) = join(meet(X2,meet(complement(X0),X1)),meet(X2,X0)),
inference(backward_demodulation,[],[f48561,f72760]) ).
fof(f75045,plain,
! [X2,X0,X1] : meet(X2,join(X0,meet(X1,X2))) = join(meet(X2,X0),meet(X2,meet(X1,complement(X0)))),
inference(forward_demodulation,[],[f73304,f72760]) ).
fof(f75053,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X2,X0))) = join(meet(X0,X1),meet(X0,meet(complement(X1),X2))),
inference(forward_demodulation,[],[f73293,f72760]) ).
fof(f75206,plain,
! [X2,X0,X1] : join(meet(X1,X2),meet(X2,meet(complement(X1),X0))) = join(meet(X2,X1),meet(X2,meet(X0,complement(X1)))),
inference(forward_demodulation,[],[f73503,f71610]) ).
fof(f75243,plain,
! [X2,X0,X1] : meet(X2,join(X0,meet(X2,join(complement(X1),meet(X0,X1))))) = join(meet(X2,X0),meet(X2,complement(join(X0,X1)))),
inference(forward_demodulation,[],[f73558,f72760]) ).
fof(f75634,plain,
! [X2,X0,X1] : join(meet(X2,X0),meet(X2,meet(complement(X0),X1))) = meet(X2,join(meet(X0,X2),meet(complement(X0),X1))),
inference(forward_demodulation,[],[f74115,f6]) ).
fof(f76277,plain,
! [X3,X0,X1] : meet(X1,join(meet(X1,X3),X0)) = join(meet(X1,X0),meet(X1,X3)),
inference(backward_demodulation,[],[f56382,f73650]) ).
fof(f76538,plain,
! [X2,X0,X1] : join(meet(X2,X0),meet(X2,X1)) = join(meet(X2,X0),meet(X2,meet(X1,complement(X0)))),
inference(forward_demodulation,[],[f75045,f73788]) ).
fof(f76544,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = join(meet(X0,X1),meet(X0,meet(complement(X1),X2))),
inference(forward_demodulation,[],[f75053,f73788]) ).
fof(f76677,plain,
! [X2,X0,X1] : join(meet(X2,X0),meet(X2,complement(join(X0,X1)))) = join(meet(X2,X0),meet(X2,join(complement(X1),meet(X0,X1)))),
inference(forward_demodulation,[],[f75243,f72760]) ).
fof(f76917,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(complement(X0),meet(join(X0,X2),X1))) = meet(join(X0,X2),join(meet(X1,X0),meet(X1,meet(complement(X0),meet(join(X0,X2),X1))))),
inference(backward_demodulation,[],[f8900,f75634]) ).
fof(f77718,plain,
! [X2,X0,X1] : join(meet(X1,X2),meet(X2,meet(complement(X1),X0))) = join(meet(X2,X1),meet(X2,X0)),
inference(backward_demodulation,[],[f75206,f76538]) ).
fof(f77822,plain,
! [X2,X0,X1] : join(meet(X2,X0),meet(X2,complement(join(X0,X1)))) = join(meet(X2,X0),meet(X2,join(complement(X1),X0))),
inference(forward_demodulation,[],[f76677,f71055]) ).
fof(f77979,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(complement(X0),meet(join(X0,X2),X1))) = meet(join(X0,X2),join(meet(X1,X0),meet(X1,meet(join(X0,X2),X1)))),
inference(forward_demodulation,[],[f76917,f76544]) ).
fof(f78606,plain,
! [X2,X0,X1] : join(meet(X2,X0),meet(X2,complement(join(X0,X1)))) = meet(X2,join(complement(X1),X0)),
inference(forward_demodulation,[],[f77822,f10954]) ).
fof(f78691,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(complement(X0),meet(join(X0,X2),X1))) = join(meet(X1,X0),meet(X1,meet(join(X0,X2),X1))),
inference(forward_demodulation,[],[f77979,f31612]) ).
fof(f79118,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X1,complement(join(X0,X2)))) = meet(X1,join(complement(X2),X0)),
inference(backward_demodulation,[],[f31911,f78606]) ).
fof(f79257,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(complement(X0),meet(join(X0,X2),X1))) = join(meet(X1,X0),meet(join(X0,X2),X1)),
inference(forward_demodulation,[],[f78691,f51]) ).
fof(f79735,plain,
! [X2,X0,X1] : meet(join(X0,X2),X1) = join(meet(X0,X1),meet(complement(X0),meet(join(X0,X2),X1))),
inference(forward_demodulation,[],[f79257,f10274]) ).
fof(f80786,plain,
! [X2,X0,X1] : join(meet(X0,complement(X1)),X2) = join(meet(X0,complement(X1)),meet(join(X1,complement(X0)),X2)),
inference(superposition,[],[f71048,f67318]) ).
fof(f80847,plain,
join(complement(c),sF3) = join(complement(c),a),
inference(superposition,[],[f71048,f26]) ).
fof(f80849,plain,
join(complement(c),sF3) = join(complement(c),sF1),
inference(superposition,[],[f71048,f10084]) ).
fof(f80851,plain,
join(complement(c),sF3) = join(complement(c),sF4),
inference(superposition,[],[f71048,f6283]) ).
fof(f80964,plain,
join(complement(c),sF1) = join(complement(c),sF4),
inference(backward_demodulation,[],[f80851,f80849]) ).
fof(f80966,plain,
join(complement(c),sF3) = join(a,complement(c)),
inference(forward_demodulation,[],[f80847,f6]) ).
fof(f81009,plain,
! [X2,X0,X1] : join(meet(X0,complement(X1)),X2) = join(X2,meet(X0,complement(join(X2,X1)))),
inference(backward_demodulation,[],[f70955,f80786]) ).
fof(f81045,plain,
join(complement(c),sF1) = join(a,complement(c)),
inference(backward_demodulation,[],[f80849,f80966]) ).
fof(f81118,plain,
join(complement(c),sF4) = join(a,complement(c)),
inference(backward_demodulation,[],[f80964,f81045]) ).
fof(f81692,plain,
meet(c,complement(sF3)) = meet(complement(a),c),
inference(superposition,[],[f71610,f26]) ).
fof(f81694,plain,
meet(c,complement(sF3)) = meet(complement(sF1),c),
inference(superposition,[],[f71610,f10084]) ).
fof(f81853,plain,
meet(c,complement(sF3)) = meet(c,complement(sF1)),
inference(forward_demodulation,[],[f81694,f5]) ).
fof(f81855,plain,
meet(c,complement(sF3)) = meet(c,complement(a)),
inference(forward_demodulation,[],[f81692,f5]) ).
fof(f81967,plain,
meet(c,complement(a)) = meet(c,complement(sF1)),
inference(backward_demodulation,[],[f81853,f81855]) ).
fof(f83341,plain,
! [X2,X0,X1] : meet(X2,meet(complement(X0),X1)) = meet(complement(X0),meet(join(X0,X1),X2)),
inference(superposition,[],[f125,f72688]) ).
fof(f83401,plain,
! [X2,X0,X1] : meet(join(X0,X2),X1) = join(meet(X0,X1),meet(X1,meet(complement(X0),X2))),
inference(backward_demodulation,[],[f79735,f83341]) ).
fof(f83533,plain,
! [X2,X0,X1] : meet(join(X1,X0),X2) = join(meet(X2,X1),meet(X2,X0)),
inference(backward_demodulation,[],[f77718,f83401]) ).
fof(f83701,plain,
! [X3,X0,X1] : meet(join(X0,X3),X1) = meet(X1,join(meet(X1,X3),X0)),
inference(backward_demodulation,[],[f76277,f83533]) ).
fof(f103226,plain,
sF4 = meet(join(c,sF2),join(sF4,complement(c))),
inference(superposition,[],[f71794,f14189]) ).
fof(f103430,plain,
sF4 = meet(join(c,sF2),join(complement(c),sF4)),
inference(forward_demodulation,[],[f103226,f34397]) ).
fof(f103553,plain,
sF4 = meet(join(c,sF2),join(a,complement(c))),
inference(forward_demodulation,[],[f103430,f81118]) ).
fof(f104173,plain,
! [X2,X0,X1] : join(meet(X2,X1),X0) = join(join(meet(X2,X1),X0),meet(join(X0,X1),X2)),
inference(superposition,[],[f32,f83701]) ).
fof(f104286,plain,
! [X2,X0,X1] : join(meet(X2,X1),X0) = join(meet(X2,X1),join(X0,meet(join(X0,X1),X2))),
inference(forward_demodulation,[],[f104173,f8]) ).
fof(f104514,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X1),X2)) = join(meet(X2,X1),X0),
inference(forward_demodulation,[],[f104286,f36102]) ).
fof(f104732,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X2,X0)) = join(meet(join(X2,X0),X1),X0),
inference(backward_demodulation,[],[f10290,f104514]) ).
fof(f105005,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X2,X0)) = join(X0,meet(join(X2,X0),X1)),
inference(forward_demodulation,[],[f104732,f6]) ).
fof(f108444,plain,
complement(sF1) = join(meet(c,complement(a)),meet(complement(sF1),complement(c))),
inference(superposition,[],[f72214,f81967]) ).
fof(f108453,plain,
complement(sF1) = join(meet(c,complement(a)),meet(complement(c),complement(sF1))),
inference(forward_demodulation,[],[f108444,f66558]) ).
fof(f108481,plain,
complement(sF1) = join(meet(c,complement(a)),complement(join(sF1,c))),
inference(forward_demodulation,[],[f108453,f63405]) ).
fof(f108505,plain,
complement(sF1) = join(meet(c,complement(a)),complement(join(c,sF1))),
inference(forward_demodulation,[],[f108481,f67469]) ).
fof(f108521,plain,
complement(sF1) = complement(meet(join(c,sF1),join(a,complement(c)))),
inference(forward_demodulation,[],[f108505,f68505]) ).
fof(f116359,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(complement(X2),X0)) = join(X0,meet(join(X0,X1),complement(join(X0,X2)))),
inference(superposition,[],[f79118,f3]) ).
fof(f116898,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(complement(X2),X0)) = join(meet(join(X0,X1),complement(X2)),X0),
inference(forward_demodulation,[],[f116359,f81009]) ).
fof(f117132,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(complement(X2),X0)) = join(X0,meet(join(X0,X1),complement(X2))),
inference(forward_demodulation,[],[f116898,f6]) ).
fof(f117323,plain,
! [X2,X0,X1] : join(meet(complement(X2),X1),X0) = meet(join(X0,X1),join(complement(X2),X0)),
inference(forward_demodulation,[],[f117132,f104514]) ).
fof(f117443,plain,
! [X2,X0,X1] : join(meet(complement(X2),X1),X0) = join(X0,meet(join(complement(X2),X0),X1)),
inference(forward_demodulation,[],[f117323,f105005]) ).
fof(f117769,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(X2,meet(join(X0,X2),X1)),
inference(superposition,[],[f117443,f4073]) ).
fof(f118594,plain,
! [X0] : join(meet(b,X0),c) = join(c,meet(sF0,X0)),
inference(superposition,[],[f117769,f15]) ).
fof(f118947,plain,
! [X0] : join(c,meet(b,X0)) = join(c,meet(sF0,X0)),
inference(forward_demodulation,[],[f118594,f6]) ).
fof(f120931,plain,
join(c,sF1) = join(c,meet(b,sF1)),
inference(superposition,[],[f118947,f3162]) ).
fof(f121117,plain,
join(c,sF2) = join(c,sF1),
inference(forward_demodulation,[],[f120931,f11370]) ).
fof(f121173,plain,
sF4 = meet(join(c,sF1),join(a,complement(c))),
inference(backward_demodulation,[],[f103553,f121117]) ).
fof(f121206,plain,
complement(sF4) = complement(sF1),
inference(backward_demodulation,[],[f108521,f121173]) ).
fof(f121225,plain,
spl5_56,
inference(avatar_split_clause,[],[f121206,f17843]) ).
fof(f121258,plain,
( zero != meet(sF1,complement(sF1))
| ~ spl5_56
| spl5_57 ),
inference(backward_demodulation,[],[f17849,f17845]) ).
fof(f121347,plain,
( $false
| ~ spl5_56
| spl5_57 ),
inference(forward_subsumption_resolution,[],[f121258,f10]) ).
fof(f121348,plain,
( ~ spl5_56
| spl5_57 ),
inference(avatar_contradiction_clause,[],[f121347]) ).
cnf(s36,plain,
~ spl5_57,
inference(sat_conversion,[],[f17892]) ).
cnf(s60,plain,
spl5_56,
inference(sat_conversion,[],[f121225]) ).
cnf(s61,plain,
( ~ spl5_56
| spl5_57 ),
inference(sat_conversion,[],[f121348]) ).
cnf(s62,plain,
spl5_57,
inference(rat,[],[s61,s60]) ).
cnf(s63,plain,
$false,
inference(rat,[],[s36,s62]) ).
fof(f121358,plain,
$false,
inference(avatar_sat_refutation,[],[s63]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT179-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.10 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.22/0.47 % Computer : n013.cluster.edu
% 0.22/0.47 % Model : x86_64 x86_64
% 0.22/0.47 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.22/0.47 % Memory : 8046.5625MB
% 0.22/0.47 % OS : Linux 6.8.0-71-generic
% 0.22/0.47 % CPULimit : 300
% 0.22/0.47 % WCLimit : 300
% 0.22/0.47 % DateTime : Sun Sep 27 14:04:07 UTC 2026
% 0.22/0.48 % CPUTime :
% 0.22/0.48 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.27/0.54 Running first-order theorem proving
% 0.27/0.54 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
% 15.90/3.44 % (257733)Input is clausal, will run a generic CNF schedule.
% 15.90/3.44 % (257740)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1879147857:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 15.90/3.44 % (257738)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=2128330405:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 15.90/3.44 % (257739)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1756338836:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 15.90/3.44 % (257741)lrs+10_1_sil=8000:sp=occurrence:random_seed=2635086251:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 15.90/3.44 % (257742)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3784158407:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 15.90/3.44 % (257743)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=410507845:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 15.90/3.44 % (257744)dis-21_1_sil=8000:lcm=predicate:random_seed=2169227600: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)
% 15.90/3.44 % (257744)Refutation not found, incomplete strategy
% 15.90/3.44 % (257744)------------------------------
% 15.90/3.44 % (257744)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.90/3.44 % (257744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.90/3.44 % (257744)CaDiCaL version: 2.1.3
% 15.90/3.44 % (257744)Termination reason: Refutation not found, incomplete strategy
% 15.90/3.44 % (257744)Time elapsed: 0.003 s
% 15.90/3.44 % (257744)Peak memory usage: 88 MB
% 15.90/3.44 % (257744)Instructions burned: 1 (million)
% 15.90/3.44 % (257741)Instruction limit reached!
% 15.90/3.44 % (257741)------------------------------
% 15.90/3.44 % (257741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.90/3.44 % (257741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.90/3.44 % (257741)CaDiCaL version: 2.1.3
% 15.90/3.44 % (257741)Termination reason: Instruction limit
% 15.90/3.44 % (257741)Termination phase: Saturation
% 15.90/3.44 % (257741)Time elapsed: 0.105 s
% 15.90/3.44 % (257741)Peak memory usage: 88 MB
% 15.90/3.44 % (257741)Instructions burned: 107 (million)
% 15.90/3.44 % (257742)Instruction limit reached!
% 15.90/3.44 % (257742)------------------------------
% 15.90/3.44 % (257742)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.90/3.44 % (257742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.90/3.44 % (257742)CaDiCaL version: 2.1.3
% 15.90/3.44 % (257742)Termination reason: Instruction limit
% 15.90/3.44 % (257742)Termination phase: Saturation
% 15.90/3.44 % (257742)Time elapsed: 0.112 s
% 15.90/3.44 % (257742)Peak memory usage: 89 MB
% 15.90/3.44 % (257742)Instructions burned: 114 (million)
% 15.90/3.44 % (257743)Instruction limit reached!
% 15.90/3.44 % (257743)------------------------------
% 15.90/3.44 % (257743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.90/3.44 % (257743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.90/3.44 % (257743)CaDiCaL version: 2.1.3
% 15.90/3.44 % (257743)Termination reason: Instruction limit
% 15.90/3.44 % (257743)Termination phase: Saturation
% 15.90/3.44 % (257743)Time elapsed: 0.169 s
% 15.90/3.44 % (257743)Peak memory usage: 89 MB
% 15.90/3.44 % (257743)Instructions burned: 181 (million)
% 15.90/3.44 % (257752)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=3084396328:i=143:sd=2:aac=none:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/143Mi)
% 15.90/3.44 % (257753)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1864851253: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)
% 15.90/3.44 % (257752)Refutation not found, incomplete strategy
% 15.90/3.44 % (257752)------------------------------
% 15.90/3.44 % (257752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.90/3.44 % (257752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.90/3.44 % (257752)CaDiCaL version: 2.1.3
% 15.90/3.44 % (257752)Termination reason: Refutation not found, incomplete strategy
% 25.10/4.86 % (257752)Time elapsed: 0.002 s
% 25.10/4.86 % (257752)Peak memory usage: 88 MB
% 25.10/4.86 % (257753)Refutation not found, incomplete strategy
% 25.10/4.86 % (257753)------------------------------
% 25.10/4.86 % (257753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.10/4.86 % (257753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.10/4.86 % (257753)CaDiCaL version: 2.1.3
% 25.10/4.86 % (257753)Termination reason: Refutation not found, incomplete strategy
% 25.10/4.86 % (257753)Time elapsed: 0.002 s
% 25.10/4.86 % (257753)Peak memory usage: 88 MB
% 25.10/4.86 % (257753)Instructions burned: 1 (million)
% 25.10/4.86 % (257754)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1000260863:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 25.10/4.86 % (257754)Refutation not found, incomplete strategy
% 25.10/4.86 % (257754)------------------------------
% 25.10/4.86 % (257754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.10/4.86 % (257754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.10/4.86 % (257754)CaDiCaL version: 2.1.3
% 25.10/4.86 % (257754)Termination reason: Refutation not found, incomplete strategy
% 25.10/4.86 % (257754)Time elapsed: 0.002 s
% 25.10/4.86 % (257754)Peak memory usage: 88 MB
% 25.10/4.86 % (257744)------------------------------
% 25.10/4.86 % (257744)------------------------------
% 25.10/4.86 % (257767)lrs+10_64_to=lpo:sil=8000:random_seed=3707842937:i=126:bd=preordered_2993 on theBenchmark for (2993ds/126Mi)
% 25.10/4.86 % (257752)------------------------------
% 25.10/4.86 % (257752)------------------------------
% 25.10/4.86 % (257753)------------------------------
% 25.10/4.86 % (257753)------------------------------
% 25.10/4.86 % (257767)Instruction limit reached!
% 25.10/4.86 % (257767)------------------------------
% 25.10/4.86 % (257767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.10/4.86 % (257767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.10/4.86 % (257767)CaDiCaL version: 2.1.3
% 25.10/4.86 % (257767)Termination reason: Instruction limit
% 25.10/4.86 % (257767)Termination phase: Saturation
% 25.10/4.86 % (257767)Time elapsed: 0.122 s
% 25.10/4.86 % (257767)Peak memory usage: 88 MB
% 25.10/4.86 % (257767)Instructions burned: 126 (million)
% 25.10/4.86 % (257754)------------------------------
% 25.10/4.86 % (257754)------------------------------
% 25.10/4.86 % (257769)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1879771992:avsq=on:i=194:fgj=on:bd=preordered_2990 on theBenchmark for (2990ds/194Mi)
% 25.10/4.86 % (257770)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2900714559:i=157:gtg=all_2990 on theBenchmark for (2990ds/157Mi)
% 25.10/4.86 % (257771)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1312564736:i=3394:sd=4:ss=included:sgt=64_2989 on theBenchmark for (2989ds/3394Mi)
% 25.10/4.86 % (257772)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=3892388356:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2989 on theBenchmark for (2989ds/106Mi)
% 25.10/4.86 % (257770)Instruction limit reached!
% 25.10/4.86 % (257770)------------------------------
% 25.10/4.86 % (257770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.10/4.86 % (257770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.10/4.87 % (257770)CaDiCaL version: 2.1.3
% 25.10/4.87 % (257770)Termination reason: Instruction limit
% 25.10/4.87 % (257770)Termination phase: Saturation
% 25.10/4.87 % (257770)Time elapsed: 0.095 s
% 25.10/4.87 % (257770)Peak memory usage: 90 MB
% 25.10/4.87 % (257770)Instructions burned: 158 (million)
% 25.10/4.87 % (257772)Instruction limit reached!
% 25.10/4.87 % (257772)------------------------------
% 25.10/4.87 % (257772)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.10/4.87 % (257772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.10/4.87 % (257772)CaDiCaL version: 2.1.3
% 25.10/4.87 % (257772)Termination reason: Instruction limit
% 25.10/4.87 % (257772)Termination phase: Saturation
% 25.10/4.87 % (257772)Time elapsed: 0.065 s
% 25.10/4.87 % (257772)Peak memory usage: 89 MB
% 25.10/4.87 % (257772)Instructions burned: 107 (million)
% 25.10/4.87 % (257769)Instruction limit reached!
% 25.10/4.87 % (257769)------------------------------
% 25.10/4.87 % (257769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.10/4.87 % (257769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.84/6.72 % (257769)CaDiCaL version: 2.1.3
% 38.84/6.72 % (257769)Termination reason: Instruction limit
% 38.84/6.72 % (257769)Termination phase: Saturation
% 38.84/6.72 % (257769)Time elapsed: 0.117 s
% 38.84/6.72 % (257769)Peak memory usage: 90 MB
% 38.84/6.72 % (257769)Instructions burned: 195 (million)
% 38.84/6.72 % (257777)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=589499186:i=107_2986 on theBenchmark for (2986ds/107Mi)
% 38.84/6.72 % (257777)Refutation not found, incomplete strategy
% 38.84/6.72 % (257777)------------------------------
% 38.84/6.72 % (257777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.84/6.72 % (257777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.84/6.72 % (257777)CaDiCaL version: 2.1.3
% 38.84/6.72 % (257777)Termination reason: Refutation not found, incomplete strategy
% 38.84/6.72 % (257777)Time elapsed: 0.001 s
% 38.84/6.72 % (257777)Peak memory usage: 87 MB
% 38.84/6.72 % (257778)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1255549483:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2986 on theBenchmark for (2986ds/242Mi)
% 38.84/6.72 % (257779)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2328179228:cond=fast:i=5208:av=off_2986 on theBenchmark for (2986ds/5208Mi)
% 38.84/6.72 % (257778)Instruction limit reached!
% 38.84/6.72 % (257778)------------------------------
% 38.84/6.72 % (257778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.84/6.72 % (257778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.84/6.72 % (257778)CaDiCaL version: 2.1.3
% 38.84/6.72 % (257778)Termination reason: Instruction limit
% 38.84/6.72 % (257778)Termination phase: Saturation
% 38.84/6.72 % (257778)Time elapsed: 0.142 s
% 38.84/6.72 % (257778)Peak memory usage: 90 MB
% 38.84/6.72 % (257778)Instructions burned: 244 (million)
% 38.84/6.72 % (257777)------------------------------
% 38.84/6.72 % (257777)------------------------------
% 38.84/6.72 % (257783)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2789655254:i=134:sd=2:doe=on:ss=axioms:sgt=14_2984 on theBenchmark for (2984ds/134Mi)
% 38.84/6.72 % (257783)Instruction limit reached!
% 38.84/6.72 % (257783)------------------------------
% 38.84/6.72 % (257783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.84/6.72 % (257783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.84/6.72 % (257783)CaDiCaL version: 2.1.3
% 38.84/6.72 % (257783)Termination reason: Instruction limit
% 38.84/6.72 % (257783)Termination phase: Saturation
% 38.84/6.72 % (257783)Time elapsed: 0.078 s
% 38.84/6.72 % (257783)Peak memory usage: 89 MB
% 38.84/6.72 % (257783)Instructions burned: 134 (million)
% 38.84/6.72 % (257784)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1453508740:i=499:bd=all_2983 on theBenchmark for (2983ds/499Mi)
% 38.84/6.72 % (257786)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1700141023:i=191:fgj=on:bd=all_2982 on theBenchmark for (2982ds/191Mi)
% 38.84/6.72 % (257786)Instruction limit reached!
% 38.84/6.72 % (257786)------------------------------
% 38.84/6.72 % (257786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.84/6.72 % (257786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.84/6.72 % (257786)CaDiCaL version: 2.1.3
% 38.84/6.72 % (257786)Termination reason: Instruction limit
% 38.84/6.72 % (257786)Termination phase: Saturation
% 38.84/6.72 % (257786)Time elapsed: 0.120 s
% 38.84/6.72 % (257786)Peak memory usage: 91 MB
% 38.84/6.72 % (257786)Instructions burned: 193 (million)
% 38.84/6.72 % (257784)Instruction limit reached!
% 38.84/6.72 % (257784)------------------------------
% 38.84/6.72 % (257784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.84/6.72 % (257784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.84/6.72 % (257784)CaDiCaL version: 2.1.3
% 38.84/6.72 % (257784)Termination reason: Instruction limit
% 38.84/6.72 % (257784)Termination phase: Saturation
% 38.84/6.72 % (257784)Time elapsed: 0.310 s
% 38.84/6.72 % (257784)Peak memory usage: 94 MB
% 38.84/6.72 % (257784)Instructions burned: 500 (million)
% 38.84/6.72 % (257790)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=885759770:i=264:kws=precedence:fsr=off_2979 on theBenchmark for (2979ds/264Mi)
% 47.19/7.89 % (257808)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3819691912:cond=on:i=156:bs=on:gtg=exists_all:er=known_2978 on theBenchmark for (2978ds/156Mi)
% 47.19/7.89 % (257790)Instruction limit reached!
% 47.19/7.89 % (257790)------------------------------
% 47.19/7.89 % (257790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.19/7.89 % (257790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.19/7.89 % (257790)CaDiCaL version: 2.1.3
% 47.19/7.89 % (257790)Termination reason: Instruction limit
% 47.19/7.89 % (257790)Termination phase: Saturation
% 47.19/7.89 % (257790)Time elapsed: 0.157 s
% 47.19/7.89 % (257790)Peak memory usage: 92 MB
% 47.19/7.89 % (257790)Instructions burned: 264 (million)
% 47.19/7.89 % (257808)Instruction limit reached!
% 47.19/7.89 % (257808)------------------------------
% 47.19/7.89 % (257808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.19/7.89 % (257808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.19/7.89 % (257808)CaDiCaL version: 2.1.3
% 47.19/7.89 % (257808)Termination reason: Instruction limit
% 47.19/7.89 % (257808)Termination phase: Saturation
% 47.19/7.89 % (257808)Time elapsed: 0.094 s
% 47.19/7.89 % (257808)Peak memory usage: 89 MB
% 47.19/7.89 % (257808)Instructions burned: 156 (million)
% 47.19/7.89 % (257892)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1804164007:i=537:av=off:ss=included_2976 on theBenchmark for (2976ds/537Mi)
% 47.19/7.89 % (257888)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=1730006831:i=3256:kws=precedence:bd=preordered:av=off_2976 on theBenchmark for (2976ds/3256Mi)
% 47.19/7.89 % (257892)Instruction limit reached!
% 47.19/7.89 % (257892)------------------------------
% 47.19/7.89 % (257892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.19/7.89 % (257892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.19/7.89 % (257892)CaDiCaL version: 2.1.3
% 47.19/7.89 % (257892)Termination reason: Instruction limit
% 47.19/7.89 % (257892)Termination phase: Saturation
% 47.19/7.89 % (257892)Time elapsed: 0.287 s
% 47.19/7.89 % (257892)Peak memory usage: 93 MB
% 47.19/7.89 % (257892)Instructions burned: 538 (million)
% 47.19/7.89 % (257950)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1677285359:i=180:bd=preordered:av=off_2972 on theBenchmark for (2972ds/180Mi)
% 47.19/7.89 % (257950)Instruction limit reached!
% 47.19/7.89 % (257950)------------------------------
% 47.19/7.89 % (257950)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.19/7.89 % (257950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.19/7.89 % (257950)CaDiCaL version: 2.1.3
% 47.19/7.89 % (257950)Termination reason: Instruction limit
% 47.19/7.89 % (257950)Termination phase: Saturation
% 47.19/7.89 % (257950)Time elapsed: 0.101 s
% 47.19/7.89 % (257950)Peak memory usage: 88 MB
% 47.19/7.89 % (257950)Instructions burned: 180 (million)
% 47.19/7.89 % (257952)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=3181728225:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2969 on theBenchmark for (2969ds/10307Mi)
% 47.19/7.89 % (257771)Instruction limit reached!
% 47.19/7.89 % (257771)------------------------------
% 47.19/7.89 % (257771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.19/7.89 % (257771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.19/7.89 % (257771)CaDiCaL version: 2.1.3
% 47.19/7.89 % (257771)Termination reason: Instruction limit
% 47.19/7.89 % (257771)Termination phase: Saturation
% 47.19/7.89 % (257771)Time elapsed: 2.035 s
% 47.19/7.89 % (257771)Peak memory usage: 152 MB
% 47.19/7.89 % (257771)Instructions burned: 3395 (million)
% 47.19/7.89 % (257954)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=3123128975:i=412:gtgl=4:gtg=exists_all_2967 on theBenchmark for (2967ds/412Mi)
% 47.19/7.89 % (257954)Instruction limit reached!
% 47.19/7.89 % (257954)------------------------------
% 47.19/7.89 % (257954)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.19/7.89 % (257954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.19/7.89 % (257954)CaDiCaL version: 2.1.3
% 47.19/7.89 % (257954)Termination reason: Instruction limit
% 47.19/7.89 % (257954)Termination phase: Saturation
% 47.19/7.89 % (257954)Time elapsed: 0.238 s
% 47.19/7.89 % (257954)Peak memory usage: 94 MB
% 47.19/7.89 % (257954)Instructions burned: 412 (million)
% 47.19/7.89 % (257956)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=3542328824:s2pl=no:i=8478:s2at=4:nm=6_2963 on theBenchmark for (2963ds/8478Mi)
% 47.19/7.89 % (257888)Instruction limit reached!
% 47.19/7.89 % (257888)------------------------------
% 47.19/7.89 % (257888)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.19/7.89 % (257888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.19/7.89 % (257888)CaDiCaL version: 2.1.3
% 47.19/7.89 % (257888)Termination reason: Instruction limit
% 47.19/7.89 % (257888)Termination phase: Saturation
% 47.19/7.89 % (257888)Time elapsed: 1.981 s
% 47.19/7.89 % (257888)Peak memory usage: 151 MB
% 47.19/7.89 % (257888)Instructions burned: 3257 (million)
% 47.19/7.89 % (257958)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=505807548:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2955 on theBenchmark for (2955ds/303Mi)
% 47.19/7.89 % (257958)Refutation not found, incomplete strategy
% 47.19/7.89 % (257958)------------------------------
% 47.19/7.89 % (257958)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.19/7.89 % (257958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.19/7.89 % (257958)CaDiCaL version: 2.1.3
% 47.19/7.89 % (257958)Termination reason: Refutation not found, incomplete strategy
% 47.19/7.89 % (257958)Time elapsed: 0.002 s
% 47.19/7.89 % (257958)Peak memory usage: 88 MB
% 47.19/7.89 % (257958)Instructions burned: 1 (million)
% 47.19/7.89 % (257779)Instruction limit reached!
% 47.19/7.89 % (257779)------------------------------
% 47.19/7.89 % (257779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.19/7.89 % (257779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.19/7.89 % (257779)CaDiCaL version: 2.1.3
% 47.19/7.89 % (257779)Termination reason: Instruction limit
% 47.19/7.89 % (257779)Termination phase: Saturation
% 47.19/7.89 % (257779)Time elapsed: 3.170 s
% 47.19/7.89 % (257779)Peak memory usage: 167 MB
% 47.19/7.89 % (257779)Instructions burned: 5209 (million)
% 47.19/7.89 % (257960)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=1452310820:st=4:i=720:sd=3:fsr=off:ss=axioms_2953 on theBenchmark for (2953ds/720Mi)
% 47.19/7.89 % (257960)Refutation not found, incomplete strategy
% 47.19/7.89 % (257960)------------------------------
% 47.19/7.89 % (257960)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.19/7.89 % (257960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.19/7.89 % (257960)CaDiCaL version: 2.1.3
% 47.19/7.89 % (257960)Termination reason: Refutation not found, incomplete strategy
% 47.19/7.89 % (257960)Time elapsed: 0.001 s
% 47.19/7.89 % (257960)Peak memory usage: 88 MB
% 47.19/7.89 % (257958)------------------------------
% 47.19/7.89 % (257958)------------------------------
% 47.19/7.89 % (257962)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3264569508:i=598:bs=on:bd=preordered:av=off:ss=axioms_2951 on theBenchmark for (2951ds/598Mi)
% 47.19/7.89 % (257960)------------------------------
% 47.19/7.89 % (257960)------------------------------
% 47.19/7.89 % (257964)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=120467676:i=2989:sd=3:ss=axioms:sgt=60_2949 on theBenchmark for (2949ds/2989Mi)
% 47.19/7.89 % (257962)Instruction limit reached!
% 47.19/7.89 % (257962)------------------------------
% 47.19/7.89 % (257962)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.19/7.89 % (257962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.19/7.89 % (257962)CaDiCaL version: 2.1.3
% 47.19/7.89 % (257962)Termination reason: Instruction limit
% 47.19/7.89 % (257962)Termination phase: Saturation
% 47.19/7.89 % (257962)Time elapsed: 0.375 s
% 47.19/7.89 % (257962)Peak memory usage: 95 MB
% 47.19/7.89 % (257962)Instructions burned: 598 (million)
% 47.19/7.89 % (257966)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=165456497:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2946 on theBenchmark for (2946ds/1997Mi)
% 47.19/7.89 % (257740)First to succeed.
% 47.19/7.89 % (257740)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-257733"
% 47.19/7.89 % (257740)Refutation found. Thanks to Tanya!
% 47.19/7.89 % SZS status Unsatisfiable for theBenchmark
% 47.19/7.89 % SZS output start Proof for theBenchmark
% See solution above
% 48.01/8.09 % (257740)------------------------------
% 48.01/8.09 % (257740)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.01/8.09 % (257740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.01/8.09 % (257740)CaDiCaL version: 2.1.3
% 48.01/8.09 % (257740)Termination reason: Refutation
% 48.01/8.09 % (257740)Time elapsed: 6.307 s
% 48.01/8.09 % (257740)Peak memory usage: 247 MB
% 48.01/8.09 % (257740)Instructions burned: 16584 (million)
% 48.01/8.09 % (257740)------------------------------
% 48.01/8.09 % (257740)------------------------------
% 48.01/8.09 % (257733)Success in time 6.653 s
% 48.01/8.09 % Vampire exiting
%------------------------------------------------------------------------------